diff --git a/Isabelle_DOF-Unit-Tests/Concept_Example_Low_Level_Invariant.thy b/Isabelle_DOF-Unit-Tests/Concept_Example_Low_Level_Invariant.thy index b5eb951..d376993 100644 --- a/Isabelle_DOF-Unit-Tests/Concept_Example_Low_Level_Invariant.thy +++ b/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 \ +(* borderline test *) text*[d0::A, x = "5"] \Lorem ipsum dolor sit amet, ...\ text-assert-error[d1::A, x = "6"]\Lorem ipsum dolor sit amet, ...\\class A invariant violation\ @@ -75,7 +76,7 @@ subsection*[d::A, x = "4"] \ Lorem ipsum dolor sit amet, ... \ (* invariant still valid *) update_instance*[d::A, x += "1"] -(* invariant no longer *) +(* invariant no longer holds*) update_instance-assert-error[d::A, x += "1"]\class A invariant violation\ diff --git a/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy b/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy index 7fb4162..8fc937f 100644 --- a/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy +++ b/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy @@ -13,12 +13,10 @@ chapter\Creating and Referencing Ontological Instances\ -theory - Concept_OntoReferencing - imports - "Isabelle_DOF-Unit-Tests_document" - "Isabelle_DOF-Ontologies.Conceptual" - "TestKit" +theory Concept_OntoReferencing + imports "TestKit" + "Isabelle_DOF-Unit-Tests_document" + "Isabelle_DOF-Ontologies.Conceptual" begin section\Test Purpose.\ @@ -89,9 +87,7 @@ ML*[c4::C]\fun fac x = if x = 0 then 1 else x * (fac(x-1))\ (* TODO lemma*[e5::E] asd: "True" by simp -(* Correct report: "Duplicate instance declaration.. " -declare_reference*[c1::C] \ \forward declaration\ -*) +declare_reference-assert-error[c1::C]\Duplicate instance declaration\ \ \forward declaration\ declare_reference*[e6::E] @@ -101,7 +97,7 @@ definition*[e6::E] facu :: "nat \ nat" where "facu arg = undefined" text\As shown in @{E [display]\e5\} following from @{E [display]\e6\}\ -(* BUG: why is option [display] necessary ? *) +(* BUG ?: why is option [display] necessary ? *) text\As shown in @{C [display]\c4\}\ diff --git a/Isabelle_DOF-Unit-Tests/Latex_Tests.thy b/Isabelle_DOF-Unit-Tests/Latex_Tests.thy index b83db27..84c703f 100644 --- a/Isabelle_DOF-Unit-Tests/Latex_Tests.thy +++ b/Isabelle_DOF-Unit-Tests/Latex_Tests.thy @@ -11,23 +11,25 @@ * SPDX-License-Identifier: BSD-2-Clause *************************************************************************) -theory - Latex_Tests -imports - "Isabelle_DOF-Unit-Tests_document" - "TestKit" -keywords "Figure*" :: document_body (* still experimental feature *) +theory Latex_Tests + imports "TestKit" + "Isabelle_DOF-Unit-Tests_document" + keywords "Figure*" :: document_body (* still experimental feature *) begin -section\Elementary Creation of Doc-items and Access of their Attibutes\ +section\Test Purpose.\ +text\ Testing the generation of LaTeX code. Serves in particular during development. \ text\Output status:\ print_doc_classes print_doc_items +section\Elementary Creation of Doc-items and Access of their Attibutes\ + + text\And here a tex - text macro.\ text\Pythons ReStructuredText (RST). @{url \https://de.wikipedia.org/wiki/ReStructuredText\}. Tool: Sphinx. @@ -109,6 +111,8 @@ setup\DOF_lib.define_macro (Binding.make("blong",\<^here>)) "\\blong{" "}" text-latex\ \<^blong>\asd\ outer \<^blong>\syntax| ! see {syntax, outer}\ \ (*>*) +section\Experimental Code and Test of advanced LaTeX for free-form text units\ + ML\ fun report_text ctxt text = @@ -237,8 +241,7 @@ text-latex\ -section\Section Experiments of picture-content\ - +section\Experimental Section for Multiple Figure Content\ ML\ diff --git a/Isabelle_DOF-Unit-Tests/Ontology_Matching_Example.thy b/Isabelle_DOF-Unit-Tests/Ontology_Matching_Example.thy index 239ff4b..eb4dcda 100644 --- a/Isabelle_DOF-Unit-Tests/Ontology_Matching_Example.thy +++ b/Isabelle_DOF-Unit-Tests/Ontology_Matching_Example.thy @@ -1,11 +1,32 @@ -chapter\Ontologys Mathing\ +(************************************************************************* + * 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\Ontologys Matching\ theory Ontology_Matching_Example - imports "Isabelle_DOF.Isa_DOF" - "Isabelle_DOF-Unit-Tests_document" + imports TestKit + "Isabelle_DOF.Isa_DOF" + "Isabelle_DOF-Unit-Tests_document" begin +section\Test Purpose.\ +text\ 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. \ + +section\The Scenario.\ + text\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\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 - last_name :: UTF8 - age :: nat - married_to :: "string option" + first_name :: UTF8 + last_name :: UTF8 + age :: nat + married_to :: "string option" invariant a :: "age \ < 18 \ married_to \ = None" + + doc_class B = - name :: string - adult :: bool - is_married :: bool + name :: string + adult :: bool + is_married :: bool invariant b :: "is_married \ \ adult \" text\We define the mapping between the two classes, @@ -39,6 +62,15 @@ definition A_to_B_morphism , adult = (age X \ 18) , is_married = (married_to X \ None) \" +text\Sanity check: Invariants are non-contradictory, i.e. there is a witness.\ + +lemma inv_a_satisfyable : " Ex (a_inv::A \ bool)" + unfolding a_inv_def + apply(rule_tac x ="\Ontology_Matching_Example.A.tag_attribute = xxx, + first_name = yyy, last_name = zzz, age = 17, + married_to = None\" in exI) + by auto + text\Now we check that the invariant is preserved through the morphism:\ 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\This also implies that B invariants are non-contradictory: \ + +lemma inv_b_preserved : "\x. (b_inv::B \ bool) x" + apply(rule_tac x ="A_to_B_morphism \Ontology_Matching_Example.A.tag_attribute = xxx, + first_name = yyy, last_name = zzz, age = 17, + married_to = None\" 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}) \ ({X::B. b_inv X})" using inv_a_preserved diff --git a/Isabelle_DOF-Unit-Tests/TestKit.thy b/Isabelle_DOF-Unit-Tests/TestKit.thy index 41b8e86..7fd0f4d 100644 --- a/Isabelle_DOF-Unit-Tests/TestKit.thy +++ b/Isabelle_DOF-Unit-Tests/TestKit.thy @@ -16,9 +16,10 @@ theory imports "Isabelle_DOF-Unit-Tests_document" "Isabelle_DOF-Ontologies.Conceptual" -keywords "text-" "text-latex" :: document_body - and "text-assert-error" :: document_body - and "update_instance-assert-error" :: document_body +keywords "text-" "text-latex" :: document_body + and "text-assert-error" :: document_body + and "update_instance-assert-error" :: document_body + and "declare_reference-assert-error" :: document_body begin @@ -151,11 +152,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>\declare_reference-assert-error\ + "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}); - \ (* auto-tests *) @@ -163,7 +179,5 @@ text-latex\dfg\ text-assert-error[aaaa::A]\ @{A \sdf\}\\reference ontologically inconsistent\ -ML\String.isPrefix "ab" "abc"\ - end (*>*)