From d86e708154b81a658197316aa14003e18164c744 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Sun, 3 Jan 2021 14:07:21 +0100 Subject: [PATCH] a first imprfect solution for the assert* problem; 4th chapter roughly completed. --- examples/CENELEC_50128/mini_odo/mini_odo.thy | 4 +- .../Isabelle_DOF-Manual/04_RefMan.thy | 143 ++++++++++++------ src/DOF/Isa_COL.thy | 25 --- src/ontologies/Conceptual/Conceptual.thy | 2 +- .../scholarly_paper/scholarly_paper.thy | 68 ++++++++- src/tests/AssnsLemmaThmEtc.thy | 1 + 6 files changed, 161 insertions(+), 82 deletions(-) diff --git a/examples/CENELEC_50128/mini_odo/mini_odo.thy b/examples/CENELEC_50128/mini_odo/mini_odo.thy index 1d9da10..f3b5e92 100755 --- a/examples/CENELEC_50128/mini_odo/mini_odo.thy +++ b/examples/CENELEC_50128/mini_odo/mini_odo.thy @@ -534,14 +534,14 @@ text\ text\Examples for declaration of typed doc-items "assumption" and "hypothesis", concepts defined in the underlying ontology @{theory "Isabelle_DOF.CENELEC_50128"}. \ -text*[ass1::assumption, long_name="Some ''assumption one''"] \ The subsystem Y is safe. \ +text*[ass2::assumption, long_name="Some ''assumption one''"] \ The subsystem Y is safe. \ text*[hyp1::hypothesis] \ P not equal NP \ text\A real example fragment from a larger project, declaring a text-element as a "safety-related application condition", a concept defined in the @{theory "Isabelle_DOF.CENELEC_50128"} ontology:\ -text*[hyp2::hypothesis]\Under the assumption @{assumption \ass1\} we establish the following: ... \ +text*[hyp2::hypothesis]\Under the assumption @{assumption \ass2\} we establish the following: ... \ text*[ass122::SRAC, long_name="Some ''ass122''"] \ The overall sampling frequence of the odometer subsystem is therefore 14 khz, which includes sampling, computing and diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index c922c26..c089ee5 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -16,7 +16,7 @@ theory "04_RefMan" imports "03_GuidedTour" - "Isabelle_DOF.Isa_COL" + "Isabelle_DOF.technical_report" begin declare_reference*[infrastructure::technical] @@ -539,6 +539,8 @@ It extends \<^verbatim>\COL\ by the following concepts: .5 scholarly\_paper.corollary\DTcomment{Freeform}. .5 scholarly\_paper.math\_example\DTcomment{Freeform}. .5 scholarly\_paper.math\_semiformal\DTcomment{Freeform}. +.5 scholarly\_paper.math\_formal\DTcomment{Formal(=Checked) Content}. +.6 scholarly\_paper.assertion\DTcomment{Assertions}. .4 scholarly\_paper.tech\_example\DTcomment{...}. .4 scholarly\_paper.math\_motivation\DTcomment{...}. .4 scholarly\_paper.math\_explanation\DTcomment{...}. @@ -554,6 +556,8 @@ It extends \<^verbatim>\COL\ by the following concepts: \end{minipage} \end{center} +TODO: There are some slight problems in the hierarchy ... + \ text\A pivotal abstract class in the hierarchy is: @@ -599,6 +603,7 @@ of the \<^isadof> language: \ '[' meta_args ']' '\' text '\' ) + | @@{command "assert*"} '[' meta_args ']' '\' term '\' \ \ @@ -613,6 +618,11 @@ of @{typ \math_content\} might be introduced in a derived ontology definition. \ +text\While this library is intended to give a lot of space to freeform text elements in +order to counterbalance Isabelle's standard view, it should not be forgot that the real strength +of Isabelle is its ability to handle both - and to establish links between both worlds. +Therefore the formal assertion command has been integrated to capture some form of formal content.\ + subsubsection*["text-elements-expls"::example]\Examples\ @@ -634,6 +644,21 @@ text\ \ +text\Assertions allow for logical statements to be checked in the global context). +This is particularly useful to explore formal definitions wrt. to their border cases. \ + +assert*[ass1::assertion, short_name = "\This is an assertion\"] \last [3] < (4::int)\ + +text\We want to check the consequences of this definition and can add the following statements: +@{boxed_theory_text [display]\ +text*[claim::assertion]\For non-empty lists, our definition yields indeed + the last element of a list.\ +assert*[claim1::assertion] "last[4::int] = 4" +assert*[claim2::assertion] "last[1,2,3,4::int] = 4" +\} +\ + + text\ As mentioned before, the command macros of \<^theory_text>\Definition*\, \<^theory_text>\Lemma*\ and \<^theory_text>\Theorem*\ set the default class to the super-class of @{typ \definition\}. @@ -653,33 +678,17 @@ which allows the above example be shortened to: \} \ - -subsection\ASSERTIONS : NEED TO BE INTEGRATED. TODO.\ - -text\ -Similarly, we provide "minimal" instances of the \<^boxed_theory_text>\ASSERTION_ALIKES\ -and \<^boxed_theory_text>\FORMAL_STATEMENT_ALIKE\ shadow classes: -@{boxed_theory_text [display]\ -doc_class assertions = - properties :: "term list" - -doc_class "thms" = - properties :: "thm list" -\} - -\ - - subsection\The Ontology \<^theory>\Isabelle_DOF.technical_report\\ (*<*) ML\val toLaTeX = String.translate (fn c => if c = #"_" then "\\_" else String.implode[c])\ ML\writeln (DOF_core.print_doc_class_tree - @{context} (fn (n,l) => String.isPrefix "technical_report" l - orelse String.isPrefix "Isa_COL" l) + @{context} (fn (n,l) => true (* String.isPrefix "technical_report" l + orelse String.isPrefix "Isa_COL" l *)) toLaTeX)\ (*>*) text\ The \<^verbatim>\technical_report\ ontology extends \<^verbatim>\scholarly_paper\ by concepts needed -for larger reports in the domain of mathematics and engineering. +for larger reports in the domain of mathematics and engineering. The concepts are fairly +high-level arranged at root-class level, % \begin{center} @@ -688,6 +697,12 @@ for larger reports in the domain of mathematics and engineering. .0 . .1 technical\_report.front\_matter\DTcomment{...}. .1 technical\_report.table\_of\_contents\DTcomment{...}. +.1 Isa\_COL.text\_element\DTcomment{...}. +.2 scholarly\_paper.text\_section\DTcomment{...}. +.4 technical\_report.code\DTcomment{...}. +.5 technical\_report.SML\DTcomment{...}. +.5 technical\_report.ISAR\DTcomment{...}. +.5 technical\_report.LATEX\DTcomment{...}. .1 technical\_report.index\DTcomment{...}. .1 ... .1 technical\_report.report\DTcomment{...}. @@ -698,10 +713,67 @@ for larger reports in the domain of mathematics and engineering. subsection\A Domain-Specific Ontology: \<^theory>\Isabelle_DOF.CENELEC_50128\\ +(*<*) +ML\val toLaTeX = String.translate (fn c => if c = #"_" then "\\_" else String.implode[c])\ +ML\writeln (DOF_core.print_doc_class_tree + @{context} (fn (n,l) => true (* String.isPrefix "technical_report" l + orelse String.isPrefix "Isa_COL" l *)) + toLaTeX)\ +(*>*) +text\ The \<^verbatim>\CENELEC_50128\ is qn exqmple of q domqin-specific ontology. It +is based on \<^verbatim>\technical_report\ since we assume that this kind of format will be most +appropriate for this type of long-and-tedious documents, +% +\begin{center} +\begin{minipage}{.9\textwidth} +\dirtree{% +.0 . +.1 CENELEC\_50128.judgement\DTcomment{...}. +.1 CENELEC\_50128.test\_item\DTcomment{...}. +.2 CENELEC\_50128.test\_case\DTcomment{...}. +.2 CENELEC\_50128.test\_tool\DTcomment{...}. +.2 CENELEC\_50128.test\_result\DTcomment{...}. +.2 CENELEC\_50128.test\_adm\_role\DTcomment{...}. +.2 CENELEC\_50128.test\_environment\DTcomment{...}. +.2 CENELEC\_50128.test\_requirement\DTcomment{...}. +.2 CENELEC\_50128.test\_specification\DTcomment{...}. +.1 CENELEC\_50128.objectives\DTcomment{...}. +.1 CENELEC\_50128.design\_item\DTcomment{...}. +.2 CENELEC\_50128.interface\DTcomment{...}. +.1 CENELEC\_50128.sub\_requirement\DTcomment{...}. +.1 CENELEC\_50128.test\_documentation\DTcomment{...}. +.1 Isa\_COL.text\_element\DTcomment{...}. +.2 CENELEC\_50128.requirement\DTcomment{...}. +.3 CENELEC\_50128.AC\DTcomment{...}. +.4 CENELEC\_50128.EC\DTcomment{...}. +.5 CENELEC\_50128.SRAC\DTcomment{...}. +.3 CENELEC\_50128.TC\DTcomment{...}. +.3 CENELEC\_50128.FnI\DTcomment{...}. +.3 CENELEC\_50128.SIR\DTcomment{...}. +.3 CENELEC\_50128.CoAS\DTcomment{...}. +.3 CENELEC\_50128.HtbC\DTcomment{...}. +.3 CENELEC\_50128.SILA\DTcomment{...}. +.3 CENELEC\_50128.assumption\DTcomment{...}. +.3 CENELEC\_50128.hypothesis\DTcomment{...}. +.4 CENELEC\_50128.security\_hyp\DTcomment{...}. +.3 CENELEC\_50128.safety\_requirement\DTcomment{...}. +.2 CENELEC\_50128.cenelec\_text\DTcomment{...}. +.3 CENELEC\_50128.SWAS\DTcomment{...}. +.3 [...]. +.2 scholarly\_paper.text\_section\DTcomment{...}. +.3 scholarly\_paper.technical\DTcomment{...}. +.4 scholarly\_paper.math\_content\DTcomment{...}. +.5 CENELEC\_50128.semi\_formal\_content\DTcomment{...}. +.1 ... +} +\end{minipage} +\end{center} +\ +(* TODO : Rearrange ontology hierarchies. *) -subsubsection\Example: Text Elemens with Levels\ +subsubsection\Examples\ text\ The category ``exported constraint (EC)'' is, in the file \<^file>\../../../src/ontologies/CENELEC_50128/CENELEC_50128.thy\ defined as follows: @@ -757,33 +829,6 @@ can now be defined as follows: \end{ltx} \ -subsubsection\Example: Assertions\ -text\Assertions are a common feature to validate properties of models, presented as a collection -of Isabelle/HOL definitions. They are particularly relevant for highlighting corner cases of a -formal model. For example, assume a definition: \ - -definition last :: "'a list \ 'a" where "last S = hd(rev S)" - -(* Old stuff using abstract classes. -(*<*) -text*[claim::assertions]\For non-empty lists, our definition yields indeed the last element of a list.\ -assert*[claim::assertions] "last[4::int] = 4" -assert*[claim::assertions] "last[1,2,3,4::int] = 4" -(*>*) -*) -text\We want to check the consequences of this definition and can add the following statements: -@{boxed_theory_text [display]\ -text*[claim::assertions]\For non-empty lists, our definition yields indeed - the last element of a list.\ -assert*[claim1::assertions] "last[4::int] = 4" -assert*[claim2::assertions] "last[1,2,3,4::int] = 4" -\} -\ - -text\As an \<^boxed_theory_text>\ASSERTION_ALIKES\, the \<^boxed_theory_text>\assertions\ class possesses a -\<^boxed_theory_text>\properties\ attribute. The \<^boxed_theory_text>\assert*\ command evaluates its argument; -in case it evaluates to true the property is added to the property list of the \<^boxed_theory_text>\claim\ - -text-element. Commands like \<^boxed_theory_text>\Definitions*\ or \<^boxed_theory_text>\Theorem*\ work analogously.\ subsubsection\For Isabelle Hackers: Defining New Top-Level Commands\ diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy index ffe2f96..e13af5c 100755 --- a/src/DOF/Isa_COL.thy +++ b/src/DOF/Isa_COL.thy @@ -28,7 +28,6 @@ theory Isa_COL "subsection*" "subsubsection*" "paragraph*" "subparagraph*" "figure*" "side_by_side_figure*" :: document_body - and "assert*" :: thy_decl begin @@ -120,30 +119,6 @@ fun enriched_document_cmd_exp ncid (S: (string * string) list) = end; end (* local *) -fun assertion_cmd'((((((oid,pos),cid_pos),doc_attrs),name_opt:string option),modes : string list), - prop) = - let fun conv_2_holstring thy = (bstring_to_holstring (Proof_Context.init_global thy)) - fun conv_attrs thy = (("properties",pos),"[@{termrepr ''"^conv_2_holstring thy prop ^" ''}]") - ::doc_attrs - fun conv_attrs' thy = map (fn ((lhs,pos),rhs) => (((lhs,pos),"+="),rhs)) (conv_attrs thy) - fun mks thy = case DOF_core.get_object_global_opt oid thy of - SOME NONE => (error("update of declared but not created doc_item:" ^ oid)) - | SOME _ => (update_instance_command (((oid,pos),cid_pos),conv_attrs' thy) thy) - | NONE => (create_and_check_docitem - {is_monitor = false} {is_inline = false} - oid pos cid_pos (conv_attrs thy) thy) - val check = (assert_cmd name_opt modes prop) o Proof_Context.init_global - in - (* Toplevel.keep (check o Toplevel.context_of) *) - Toplevel.theory (fn thy => (check thy; mks thy)) - end - - -val _ = - Outer_Syntax.command @{command_keyword "assert*"} - "evaluate and print term" - (attributes -- opt_evaluator -- opt_modes -- Parse.term >> assertion_cmd'); - val _ = Outer_Syntax.command ("title*", @{here}) "section heading" diff --git a/src/ontologies/Conceptual/Conceptual.thy b/src/ontologies/Conceptual/Conceptual.thy index c00586f..135a891 100755 --- a/src/ontologies/Conceptual/Conceptual.thy +++ b/src/ontologies/Conceptual/Conceptual.thy @@ -49,7 +49,7 @@ doc_class E = D + -doc_class F = +doc_class F = properties :: "term list" r :: "thm list" u :: "file" diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index eab2540..daa7d55 100755 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -11,12 +11,13 @@ * SPDX-License-Identifier: BSD-2-Clause *************************************************************************) -section\An example ontology for a scholarly paper\ +section\An example ontology for scientific, MINT-oriented papers.\ theory scholarly_paper imports "../../DOF/Isa_COL" keywords "author*" "abstract*" "Definition*" "Lemma*" "Theorem*" :: document_body + and "assert*" :: thy_decl begin @@ -123,7 +124,7 @@ A formal statement can, but must not have a reference to true formal Isabelle/Is subsection\Technical Content and its Formats\ -datatype status = semiformal | description +datatype status = formal | semiformal | description text\The class \<^verbatim>\technical\ regroups a number of text-elements that contain typical "technical content" in mathematical or engineering papers: definitions, theorems, lemmas, examples. \ @@ -154,7 +155,7 @@ doc_class example = text_section + short_name :: string <= "''''" -subsection\Mathematical Content\ +subsection\Freeform Mathematical Content\ text\We follow in our enumeration referentiable mathematical content class the AMS style and its provided \<^emph>\theorem environments\ (see \<^verbatim>\texdoc amslatex\). We add, however, the concepts @@ -258,7 +259,7 @@ doc_class "math_example" = math_content + invariant d5 :: "\ \::math_example. mcc \ = expl" -subsection\Ontological Macros \<^verbatim>\Definition*\ , \<^verbatim>\Lemma**\, \<^verbatim>\Theorem*\ ... \ +subsubsection\Ontological Macros \<^verbatim>\Definition*\ , \<^verbatim>\Lemma**\, \<^verbatim>\Theorem*\ ... \ text\These ontological macros allow notations are defined for the class \<^typ>\math_content\ in order to allow for a variety of free-form formats; @@ -334,6 +335,62 @@ val _ = let fun use_Theorem_default thy = end \ + +subsection\Formal Mathematical Content\ +text\While this library is intended to give a lot of space to freeform text elements in +order to counterbalance Isabelle's standard view, it should not be forgot that the real strength +of Isabelle is its ability to handle both - and to establish links between both worlds. Therefore:\ + +doc_class math_formal = math_content + + referentiable :: bool <= False + status :: status <= "formal" + properties :: "term list" +type_synonym math_fc = math_formal + +doc_class assertion = math_formal + + referentiable :: bool <= True (* No support in Backend yet. *) + status :: status <= "formal" + properties :: "term list" + + +ML\ +(* TODO : Rework this code and make it closer to Definition*. There is still + a rest of "abstract classes in it: any class possessing a properties attribute + is admissible to this command, not just ... *) +local open ODL_Command_Parser in + +fun assertion_cmd'((((((oid,pos),cid_pos),doc_attrs),name_opt:string option),modes : string list), + prop) = + let fun conv_2_holstring thy = (bstring_to_holstring (Proof_Context.init_global thy)) + fun conv_attrs thy = (("properties",pos),"[@{termrepr ''"^conv_2_holstring thy prop ^" ''}]") + ::doc_attrs + fun conv_attrs' thy = map (fn ((lhs,pos),rhs) => (((lhs,pos),"+="),rhs)) (conv_attrs thy) + fun mks thy = case DOF_core.get_object_global_opt oid thy of + SOME NONE => (error("update of declared but not created doc_item:" ^ oid)) + | SOME _ => (update_instance_command (((oid,pos),cid_pos),conv_attrs' thy) thy) + | NONE => (create_and_check_docitem + {is_monitor = false} {is_inline = false} + oid pos cid_pos (conv_attrs thy) thy) + val check = (assert_cmd name_opt modes prop) o Proof_Context.init_global + in + (* Toplevel.keep (check o Toplevel.context_of) *) + Toplevel.theory (fn thy => (check thy; mks thy)) + end + +val attributes = attributes (* re-export *) + +end +val _ = + Outer_Syntax.command @{command_keyword "assert*"} + "evaluate and print term" + (attributes -- opt_evaluator -- opt_modes -- Parse.term >> assertion_cmd'); + +\ + +subsubsection*[ex_ass::example]\Example\ +text\Assertions allow for logical statements to be checked in the global context). \ +assert*[ass1::assertion, short_name = "\This is an assertion\"] \(3::int) < 4\ + subsection\Example Statements\ text\ \<^verbatim>\examples\ are currently considered \<^verbatim>\technical\. Is a main category to be refined @@ -347,7 +404,8 @@ doc_class tech_example = technical + subsection\Content in Engineering/Tech Papers \ - +text\This section is currently experimental and not supported by the documentation + generation backend.\ doc_class engineering_content = tc + short_name :: string <= "''''" diff --git a/src/tests/AssnsLemmaThmEtc.thy b/src/tests/AssnsLemmaThmEtc.thy index ab71072..064c8af 100755 --- a/src/tests/AssnsLemmaThmEtc.thy +++ b/src/tests/AssnsLemmaThmEtc.thy @@ -16,6 +16,7 @@ theory imports "Isabelle_DOF.Conceptual" "Isabelle_DOF.math_paper" + "Isabelle_DOF.scholarly_paper" (* for assert notation *) begin section\Elementary Creation of Doc-items and Access of their Attibutes\