From 5aad659a85ebec7f37de7a0b2b4331d4153e1c13 Mon Sep 17 00:00:00 2001
From: Burkhart Wolff <wolff@lri.fr>
Date: Thu, 1 Jul 2021 13:12:18 +0200
Subject: [PATCH 1/2] some observations on invariant code generation

---
 src/ontologies/Conceptual/Conceptual.thy | 32 +++++++++++++++++++++---
 1 file changed, 29 insertions(+), 3 deletions(-)

diff --git a/src/ontologies/Conceptual/Conceptual.thy b/src/ontologies/Conceptual/Conceptual.thy
index 556400e..e34f02c 100755
--- a/src/ontologies/Conceptual/Conceptual.thy
+++ b/src/ontologies/Conceptual/Conceptual.thy
@@ -57,15 +57,41 @@ doc_class F  =
    b           :: "(A \<times> C) set"  <= "{}"       (* This is a relation link, roughly corresponding
                                                  to an association class. It can be used to track
                                                  claims to result - relations, for example.*) 
-   invariant b :: "\<lambda>\<sigma>::F. r \<sigma> \<noteq> [] \<and> card(b \<sigma>) \<ge> 3"
-        and  c :: "\<lambda>\<sigma>::F. properties \<sigma> \<noteq> []"
+   b'          :: "(A \<times> C) list"  <= "[]"
+   invariant br :: "\<lambda>\<sigma>::F. r \<sigma> \<noteq> [] \<and> card(b \<sigma>) \<ge> 3"
+        and  br':: "\<lambda>\<sigma>::F. r \<sigma> \<noteq> [] \<and> length(b' \<sigma>) \<ge> 3"
+        and  cr :: "\<lambda>\<sigma>::F. properties \<sigma> \<noteq> []"
+
+text\<open>The effect of the invariant declaration is to provide intern definitions for validation 
+functions of this invariant. They can be referenced as follows:\<close>
+thm br_inv_def
+thm br'_inv_def
+thm cr_inv_def
+
+text\<open>Now, we can use these definitions in order to generate code for these validation functions.
+Note, however, that not everything that we can write in an invariant (basically: HOL) is executable,
+or even compilable by the code generator setup:\<close>
+
+ML\<open> val cr_inv_code = @{code "cr_inv"} \<close> \<comment>\<open>works albeit thm is abstract ...\<close>
+text\<open>while in :\<close>
+(*
+ML\<open> val br_inv_code = @{code "br_inv"} \<close> \<comment>\<open>does not work ...\<close>
+*)
+text\<open>... the compilation fails due to the fact that nothing prevents the user 
+     to define an infinite relation between \<^typ>\<open>A\<close> and  \<^typ>\<open>C\<close>. However, the alternative
+variant: \<close>
+
+ML\<open> val br'_inv_code = @{code "br'_inv"} \<close> \<comment>\<open>does work ...\<close>
+
+text\<open>... is compilable ...\<close>
+
 
 
 doc_class G = C +
    g :: "thm"  <= "@{thm \<open>HOL.refl\<close>}"
 
 doc_class M = 
-   trace :: "(A + C + D + F) list"
+   ok :: "unit"
    accepts "A ~~ \<lbrace>C || D\<rbrace>\<^sup>* ~~ \<lbrakk>F\<rbrakk>"
 
 

From 9f9bc25618bcfc91bb434e7ab911b9c4c9e500d8 Mon Sep 17 00:00:00 2001
From: Burkhart Wolff <wolff@lri.fr>
Date: Thu, 1 Jul 2021 16:25:31 +0200
Subject: [PATCH 2/2] no message

---
 src/tests/Concept_ExampleInvariant.thy | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/src/tests/Concept_ExampleInvariant.thy b/src/tests/Concept_ExampleInvariant.thy
index 7fd00c0..a363f76 100755
--- a/src/tests/Concept_ExampleInvariant.thy
+++ b/src/tests/Concept_ExampleInvariant.thy
@@ -58,7 +58,7 @@ subsection*[d::A, x = "4"] \<open> Lorem ipsum dolor sit amet, ... \<close>
 (* test : update should not fail, invariant still valid *)
 update_instance*[d::A, x += "1"]
 
-(* test : with the next step it should fail :
+(* test : with the next step it should fail : 
 update_instance*[d::A, x += "1"]
 *)
 
@@ -101,19 +101,20 @@ open_monitor*[struct::M]
 
 subsection*[a::A, x = "3"]       \<open> Lorem ipsum dolor sit amet, ... \<close>
 
-text*[c1::C, x = "''beta''"]  \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ...  \<close>
+text*[c1::C, x = "''beta''"]     \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ...  \<close>
 
-text*[d1::E, a1 = "X3"]       \<open> ... phasellus amet id massa nunc, pede suscipit repellendus, ... \<close>
+text*[d1::E, a1 = "X3"]          \<open> ... phasellus amet id massa nunc, pede suscipit repellendus, ... \<close>
     
-text*[c2:: C, x = "''delta''"] \<open> ... in ut tortor eleifend augue pretium consectetuer...  \<close>
+text*[c2:: C, x = "''delta''"]   \<open> ... in ut tortor eleifend augue pretium consectetuer...  \<close>
 
 subsection*[f::E]                \<open> Lectus accumsan velit ultrices, ... }\<close>
 
 (*
-section*[f2::E]               \<open> Lectus accumsan velit ultrices, ... }\<close>
+section*[f2::E]                  \<open> Lectus accumsan velit ultrices, ... }\<close>
 *)
 
-ML\<open>val term = AttributeAccess.compute_attr_access (Context.Proof @{context}) "trace" "struct" @{here} @{here} ;
+ML\<open>val term = AttributeAccess.compute_attr_access 
+                  (Context.Proof @{context}) "trace" "struct" @{here} @{here} ;
    fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S)
    val string_pair_list = map conv (HOLogic.dest_list term)
   \<close>