diff --git a/Isabelle_DOF-Unit-Tests/AssnsLemmaThmEtc.thy b/Isabelle_DOF-Unit-Tests/AssnsLemmaThmEtc.thy index 1b59307..85f1d56 100644 --- a/Isabelle_DOF-Unit-Tests/AssnsLemmaThmEtc.thy +++ b/Isabelle_DOF-Unit-Tests/AssnsLemmaThmEtc.thy @@ -11,58 +11,140 @@ * SPDX-License-Identifier: BSD-2-Clause *************************************************************************) +chapter\Testing Freeform and Formal Elements from the scholarly-paper Ontology\ + theory AssnsLemmaThmEtc imports "Isabelle_DOF-Ontologies.Conceptual" "Isabelle_DOF.scholarly_paper" "Isabelle_DOF-Unit-Tests_document" + TestKit begin -section\Elementary Creation of Doc-items and Access of their Attibutes\ +section\Test Objective\ + +text\Testing Core Elements for \<^theory>\Isabelle_DOF.scholarly_paper\ wrt. to +existance, controlability via implicit and explicit default classes, and potential +LaTeX Layout.\ text\Current status:\ print_doc_classes print_doc_items +section\An Example for use-before-declaration of Formal Content\ -section\Definitions, Lemmas, Theorems, Assertions\ - -term\True\ text*[aa::F, properties = "[@{term ''True''}]"] \Our definition of the HOL-Logic has the following properties:\ assert*\F.properties @{F \aa\} = [@{term ''True''}]\ text\For now, as the term annotation is not bound to a meta logic which will translate \<^term>\[@{term ''True''}]\ to \<^term>\[True]\, we can not use the HOL \<^const>\True\ constant -in the assertion. -\ +in the assertion.\ ML\ @{term "[@{term \True \ True \}]"}; (* with isa-check *) \ -Definition*[e1]\dfgdfg\ +ML\ + (* Checking the default classes which should be in a neutral(unset) state. *) + (* Note that in this state, the "implicit default" is "math_content". *) + @{assert} (Config.get_global @{theory} Definition_default_class = ""); + @{assert} (Config.get_global @{theory} Lemma_default_class = ""); + @{assert} (Config.get_global @{theory} Theorem_default_class = ""); + @{assert} (Config.get_global @{theory} Proposition_default_class = ""); + @{assert} (Config.get_global @{theory} Premise_default_class = ""); + @{assert} (Config.get_global @{theory} Corollary_default_class = ""); + @{assert} (Config.get_global @{theory} Consequence_default_class = ""); + @{assert} (Config.get_global @{theory} Assumption_default_class = ""); + @{assert} (Config.get_global @{theory} Hypothesis_default_class = ""); + @{assert} (Config.get_global @{theory} Consequence_default_class = ""); + @{assert} (Config.get_global @{theory} Assertion_default_class = ""); + @{assert} (Config.get_global @{theory} Proof_default_class = ""); + @{assert} (Config.get_global @{theory} Example_default_class = ""); +\ -definition*[e1bis] e :: int where "e = 1" -Theorem*[e2]\dfgdfg\ +Definition*[e1]\Lorem ipsum dolor sit amet, ... \ +text\Note that this should yield a warning since \<^theory_text>\Definition*\ uses as "implicit default" the class + \<^doc_class>\math_content\ which has no \<^term>\text_element.level\ set, however in this context, + it is required to be a positive number since it is \<^term>\text_element.referentiable\ . + This is intended behaviour in order to give the user a nudge to be more specific.\ -theorem*[e2bis] f : "e = 1+0" unfolding e_def by simp +text\A repair looks like this:\ +declare [[Definition_default_class = "definition"]] -Lemma*[e3]\ \ +text\Now, define a forward reference to the formal content: \ + +declare_reference*[e1bisbis::"definition"] + +text\... which makes it possible to refer in a freeform definition to its formal counterpart +which will appear textually later. With this pragmatics, an "out-of-order-presentation" +can be achieved within \<^theory>\Isabelle_DOF.scholarly_paper\ for the most common cases.\ + +(*<*) (*LATEX FAILS *) +Definition*[e1bis::"definition", short_name="\Nice lemma.\"] + \Lorem ipsum dolor sit amet, ... + This is formally defined as follows in @{definition (unchecked) "e1bisbis"}\ +(*>*) +definition*[e1bisbis, status=formal] e :: int where "e = 2" + +section\Tests for Theorems, Assertions, Assumptions, Hypothesis, etc.\ + +declare [[Theorem_default_class = "theorem", + Premise_default_class = "premise", + Hypothesis_default_class = "hypothesis", + Assumption_default_class = "assumption", + Conclusion_default_class = "conclusion", + Consequence_default_class = "consequence", + Assertion_default_class = "assertion", + Corollary_default_class = "corollary", + Proof_default_class = "math_proof", + Conclusion_default_class = "conclusion_stmt"]] + +Theorem*[e2]\... suspendisse non arcu malesuada mollis, nibh morbi, ... \ + +theorem*[e2bis, status=formal] f : "e = 1+1" unfolding e_def by simp + +Lemma*[e3,level="Some 2"]\... phasellus amet id massa nunc, pede suscipit repellendus, ... \ +(*<*)(*LATEX FAILS *) +Proof*[d10, short_name="\Induction over Tinea pedis.\"]\Freeform Proof\ + +lemma*[dfgd::"lemma"] q: "All (\x. X \ Y \ True)" oops +text-assert-error\@{lemma dfgd} \\Undefined instance:\ \ \oops‘ed objects are not referentiable.\ + +text\... in ut tortor eleifend augue pretium consectetuer... + Lectus accumsan velit ultrices, ...\ + +Proposition*[d2::"proposition"]\"Freeform Proposition"\ + +Assumption*[d3] \"Freeform Assertion"\ + +Premise*[d4]\"Freeform Premise"\ + +Corollary*[d5]\"Freeform Corollary"\ + +Consequence*[d6::scholarly_paper.consequence]\"Freeform Consequence"\ \ \longname just for test\ + +declare_reference*[ababa::scholarly_paper.assertion] +Assertion*[d7]\Freeform Assumption with forward reference to the formal + @{assertion (unchecked) ababa}.\ +assert*[ababa::assertion] "3 < (4::int)" +assert*[ababab::assertion] "0 < (4::int)" + + +Conclusion*[d8]\"Freeform Conclusion"\ + +Hypothesis*[d9]\"Freeform Hypothesis"\ + +Example*[d11::math_example]\"Freeform Example"\ -lemma*[dfgd] q: "All (\x. X \ Y \ True)" oops text\An example for the ontology specification character of the short-cuts such as @{command "assert*"}: in the following, we use the same notation referring to a completely different class. "F" and "assertion" have only in common that they posses the attribute @{const [names_short] \properties\}: \ - -text\Creation just like that: \ -assert*[ababa::assertion] "3 < (4::int)" -assert*[ababab::assertion] "0 < (4::int)" - +(*>*) end (*>*) 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 4ac5e08..c715096 100644 --- a/Isabelle_DOF-Unit-Tests/Concept_Example_Low_Level_Invariant.thy +++ b/Isabelle_DOF-Unit-Tests/Concept_Example_Low_Level_Invariant.thy @@ -13,7 +13,7 @@ chapter\Testing hand-programmed (low-level) Invariants\ -theory Concept_Example_Low_Level_Invariant +theory Concept_Example_Low_Level_Invariant imports "Isabelle_DOF-Unit-Tests_document" "Isabelle_DOF-Ontologies.Conceptual" (* we use the generic "Conceptual" ontology *) @@ -122,7 +122,7 @@ in DOF_core.add_ml_invariant binding (DOF_core.make_ml_invariant (check_M_invari section\Example: Monitor Class Invariant\ open_monitor*[struct::M] - + subsection*[a::A, x = "3"] \ Lorem ipsum dolor sit amet, ... \ text*[c1::C, x = "''beta''"] \ ... suspendisse non arcu malesuada mollis, nibh morbi, ... \