Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF

Isabelle_DOF-Unit-Tests/Concept_Example_Low_Level_Invariant.thy

@@ -67,6 +67,7 @@ let fun check_A_invariant oid {is_monitor:bool} ctxt =
 in DOF_core.add_ml_invariant bind (DOF_core.make_ml_invariant (check_A_invariant, cid_long)) thy end
 \<close>
 
+(* borderline test *)
 text*[d0::A, x = "5"]            \<open>Lorem ipsum dolor sit amet, ...\<close>
 text-assert-error[d1::A, x = "6"]\<open>Lorem ipsum dolor sit amet, ...\<close>\<open>class A invariant violation\<close>
 
@@ -75,7 +76,7 @@ subsection*[d::A, x = "4"] \<open> Lorem ipsum dolor sit amet, ... \<close>
 (* invariant still valid *)
 update_instance*[d::A, x += "1"]
 
-(* invariant no longer *)
+(* invariant no longer holds*)
 update_instance-assert-error[d::A, x += "1"]\<open>class A invariant violation\<close>
 
 

Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy

@@ -13,12 +13,10 @@
 
 chapter\<open>Creating and Referencing Ontological Instances\<close>
 
-theory 
+theory   Concept_OntoReferencing
-  Concept_OntoReferencing
+  imports   "TestKit"
-  imports 
+            "Isabelle_DOF-Unit-Tests_document"
-  "Isabelle_DOF-Unit-Tests_document"
+            "Isabelle_DOF-Ontologies.Conceptual" 
-  "Isabelle_DOF-Ontologies.Conceptual" 
-  "TestKit"
 begin
 
 section\<open>Test Purpose.\<close>
@@ -89,9 +87,7 @@ ML*[c4::C]\<open>fun fac x = if x = 0 then 1 else x * (fac(x-1))\<close> (* TODO
 
 lemma*[e5::E] asd: "True" by simp
 
-(* Correct report: "Duplicate instance declaration.. " 
+declare_reference-assert-error[c1::C]\<open>Duplicate instance declaration\<close>     \<comment> \<open>forward declaration\<close>
-declare_reference*[c1::C]     \<comment> \<open>forward declaration\<close>
-*)
 
 declare_reference*[e6::E] 
 
@@ -101,7 +97,7 @@ definition*[e6::E] facu :: "nat \<Rightarrow> nat" where "facu arg = undefined"
 
 
 text\<open>As shown in @{E [display]\<open>e5\<close>} following from  @{E [display]\<open>e6\<close>}\<close> 
-(* BUG: why is option [display] necessary ? *)
+(* BUG ?: why is option [display] necessary ? *)
 
 text\<open>As shown in @{C [display]\<open>c4\<close>}\<close>
 

Isabelle_DOF-Unit-Tests/Latex_Tests.thy

@@ -11,23 +11,25 @@
  *   SPDX-License-Identifier: BSD-2-Clause
  *************************************************************************)
 
-theory 
+theory   Latex_Tests
-  Latex_Tests
+  imports    "TestKit"
-imports 
+             "Isabelle_DOF-Unit-Tests_document"  
-  "Isabelle_DOF-Unit-Tests_document"
+  keywords   "Figure*"          :: document_body  (* still experimental feature *)
-  "TestKit"
-keywords   "Figure*"          :: document_body  (* still experimental feature *)
 
 begin
 
-section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>
 
+section\<open>Test Purpose.\<close>
+text\<open> Testing the generation of LaTeX code. Serves in particular during development. \<close>
 
 text\<open>Output status:\<close>
 print_doc_classes
 print_doc_items
 
 
+section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>
+
+
 text\<open>And here a tex - text macro.\<close>
 text\<open>Pythons ReStructuredText (RST). 
      @{url \<open>https://de.wikipedia.org/wiki/ReStructuredText\<close>}. Tool: Sphinx.
@@ -109,6 +111,8 @@ setup\<open>DOF_lib.define_macro (Binding.make("blong",\<^here>)) "\\blong{" "}"
 text-latex\<open> \<^blong>\<open>asd\<close> outer  \<^blong>\<open>syntax| ! see {syntax, outer}\<close> \<close>
 (*>*)
 
+section\<open>Experimental Code and Test of advanced LaTeX for free-form text units\<close>
+
 ML\<open>
 
 fun report_text ctxt text =
@@ -237,8 +241,7 @@ text-latex\<open>
 
 
 
-section\<open>Section Experiments of picture-content\<close>
+section\<open>Experimental Section for Multiple Figure Content\<close>
-
 
 ML\<open>
 

Isabelle_DOF-Unit-Tests/Ontology_Matching_Example.thy

@@ -1,11 +1,32 @@
-chapter\<open>Ontologys Mathing\<close>
+(*************************************************************************
+ * Copyright (C) 
+ *               2019-2023 The University of Exeter 
+ *               2018-2023 The University of Paris-Saclay
+ *               2018      The University of Sheffield
+ *
+ * License:
+ *   This program can be redistributed and/or modified under the terms
+ *   of the 2-clause BSD-style license.
+ *
+ *   SPDX-License-Identifier: BSD-2-Clause
+ *************************************************************************)
+
+chapter\<open>Ontologys Matching\<close>
 
 theory Ontology_Matching_Example
-  imports "Isabelle_DOF.Isa_DOF"
+  imports TestKit
-  "Isabelle_DOF-Unit-Tests_document"
+          "Isabelle_DOF.Isa_DOF"
+          "Isabelle_DOF-Unit-Tests_document"
 
 begin
 
+section\<open>Test Purpose.\<close>
+text\<open> This is merely an example that shows that the generated invariants 
+      fit nicely together; i.e. allow for sensible consistency and invariant
+      preservation proofs related to ontological matchings. \<close>
+
+section\<open>The Scenario.\<close>
+
 text\<open>Using HOL, we can define a mapping between two ontologies.
   It is called ontology matching or ontology alignment.
   Here is an example which show how to map two classes.
@@ -14,19 +35,21 @@ text\<open>Using HOL, we can define a mapping between two ontologies.
 type_synonym UTF8 = string
 
 definition utf8_to_string
-  where "utf8_to_string x = x"
+  where "utf8_to_string xx = xx"
 
 
 doc_class A =
-  first_name :: UTF8
+  first_name  :: UTF8
-  last_name :: UTF8
+  last_name   :: UTF8
-  age :: nat
+  age         :: nat
-  married_to :: "string option"
+  married_to  :: "string option"
   invariant a :: "age \<sigma> < 18 \<longrightarrow> married_to \<sigma> = None"
+
+
 doc_class B =
-  name :: string 
+  name        :: string 
-  adult :: bool
+  adult       :: bool
-  is_married :: bool
+  is_married  :: bool
   invariant b :: "is_married \<sigma> \<longrightarrow> adult \<sigma>"
 
 text\<open>We define the mapping between the two classes,
@@ -39,6 +62,15 @@ definition A_to_B_morphism
           , adult = (age X \<ge> 18)
           , is_married = (married_to X \<noteq> None) \<rparr>" 
 
+text\<open>Sanity check: Invariants are non-contradictory, i.e. there is a witness.\<close>
+
+lemma inv_a_satisfyable : " Ex (a_inv::A \<Rightarrow> bool)"
+  unfolding a_inv_def
+  apply(rule_tac x ="\<lparr>Ontology_Matching_Example.A.tag_attribute = xxx, 
+                      first_name = yyy, last_name = zzz, age = 17, 
+                      married_to = None\<rparr>" in exI)
+  by auto
+
 text\<open>Now we check that the invariant is preserved through the morphism:\<close>
 
 lemma inv_a_preserved :
@@ -46,6 +78,15 @@ lemma inv_a_preserved :
   unfolding a_inv_def b_inv_def A_to_B_morphism_def
   by auto
 
+text\<open>This also implies that B invariants are non-contradictory: \<close>
+
+lemma inv_b_preserved : "\<exists>x. (b_inv::B \<Rightarrow> bool) x"
+   apply(rule_tac x ="A_to_B_morphism \<lparr>Ontology_Matching_Example.A.tag_attribute = xxx, 
+                                       first_name = yyy, last_name = zzz, age = 17, 
+                                        married_to = None\<rparr>" in exI)
+   by(rule inv_a_preserved,auto simp: a_inv_def)
+
+
 lemma A_morphism_B_total :
   "A_to_B_morphism ` ({X::A. a_inv X}) \<subseteq> ({X::B. b_inv X})"
   using inv_a_preserved

Isabelle_DOF-Unit-Tests/TestKit.thy

@@ -16,36 +16,18 @@ theory
 imports 
   "Isabelle_DOF-Unit-Tests_document"
   "Isabelle_DOF-Ontologies.Conceptual"
-keywords "text-" "text-latex"           :: document_body
+keywords "text-" "text-latex"             :: document_body
-    and  "text-assert-error"            :: document_body
+    and  "text-assert-error"              :: document_body
-    and  "update_instance-assert-error" :: document_body
+    and  "update_instance-assert-error"   :: document_body
+    and  "declare_reference-assert-error" :: document_body
 
 begin
 
-section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>
+section\<open>Testing Commands (exec-catch-verify - versions of std commands)\<close>
-
-
-text\<open>Current status:\<close>
-print_doc_classes
-print_doc_items
-
-(* this corresponds to low-level accesses : *)
-ML\<open>
-val docitem_tab = DOF_core.get_instances \<^context>;
-val isa_transformer_tab = DOF_core.get_isa_transformers \<^context>;
-val docclass_tab = DOF_core.get_onto_classes \<^context>;
-
-Name_Space.dest_table docitem_tab;
-Name_Space.dest_table isa_transformer_tab;
-Name_Space.dest_table docclass_tab;
-app;
-\<close>
 
 
 ML\<open> 
 
-val _ = Document_Output.document_output
-
 fun gen_enriched_document_command2 name {body} cid_transform attr_transform markdown
                                   (((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t,
                                      xstring_opt:(xstring * Position.T) option),
@@ -151,11 +133,26 @@ val _ =
                         (ODL_Meta_Args_Parser.attributes_upd -- Parse.document_source
                          >> (Toplevel.theory o update_instance_command)); 
 
+val _ = 
+  let fun create_and_check_docitem ((((oid, pos),cid_pos),doc_attrs),src) thy=
+                  (Value_Command.Docitem_Parser.create_and_check_docitem
+                          {is_monitor = false} {is_inline=true}
+                          {define = false} oid pos (cid_pos) (doc_attrs) thy)
+                   handle ERROR msg => (if error_match src msg 
+                          then (writeln ("Correct error:"^msg^":reported.");thy)
+                          else error"Wrong error reported")
+  in  Outer_Syntax.command \<^command_keyword>\<open>declare_reference-assert-error\<close>
+                       "declare document reference"
+                       (ODL_Meta_Args_Parser.attributes -- Parse.document_source
+                        >> (Toplevel.theory o create_and_check_docitem))
+  end;
+
+
+
 val _ =
   Outer_Syntax.command ("text-latex", \<^here>) "formal comment (primary style)"
     (Parse.opt_target -- Parse.document_source >> document_command2 {markdown = true});
 
-
 \<close>
 
 (* auto-tests *)
@@ -163,7 +160,5 @@ text-latex\<open>dfg\<close>
 
 text-assert-error[aaaa::A]\<open> @{A \<open>sdf\<close>}\<close>\<open>reference ontologically inconsistent\<close>
 
-ML\<open>String.isPrefix "ab" "abc"\<close>
-
 end
 (*>*)