diff --git a/examples/scholarly_paper/2020-iFM-CSP/paper.thy b/examples/scholarly_paper/2020-iFM-CSP/paper.thy index 2d4e2d1..3559565 100644 --- a/examples/scholarly_paper/2020-iFM-CSP/paper.thy +++ b/examples/scholarly_paper/2020-iFM-CSP/paper.thy @@ -616,7 +616,7 @@ be deadlocked after any non-terminating trace. \<^vs>\-0.2cm\\ Theorem*[T1, short_name="\DF definition captures deadlock-freeness\"] -\ \hfill \break \deadlock_free P \ (\s\\ P. tickFree s \ (s, {\}\events_of P) \ \ P)\ \<^vs>\-0.4cm\\ +\ \<^hf> \<^br> \deadlock_free P \ (\s\\ P. tickFree s \ (s, {\}\events_of P) \ \ P)\ \<^vs>\-0.4cm\\ Definition*[X11]\ \livelock\<^sub>-free P \ \ P = {} \ \<^vs>\-0.2cm\\ @@ -634,7 +634,7 @@ Finally, we proved the following theorem that confirms the relationship between properties:\<^vs>\-0.3cm\ \ Theorem*[T2, short_name="''DF implies LF''"] - \ \hspace{0.5cm} \deadlock_free P \ livelock_free P\ \<^vs>\-0.3cm\\ + \ \<^hs>\0.5cm\ \deadlock_free P \ livelock_free P\ \<^vs>\-0.3cm\\ text\ This is totally natural, at a first glance, but surprising as the proof of deadlock-freeness only diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index 79bae4a..aee20d0 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -16,6 +16,7 @@ theory "03_GuidedTour" imports "02_Background" + "Isabelle_DOF.technical_report" "Isabelle_DOF.CENELEC_50128" begin (*>*) diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index 88b3327..c922c26 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -508,45 +508,83 @@ ML\writeln (DOF_core.print_doc_class_tree orelse String.isPrefix "Isa_COL" l) toLaTeX)\ (*>*) -text\The \<^verbatim>\scholarly_paper\ ontology extends \<^verbatim>\COL\ by the following concepts: +text\ The \<^verbatim>\scholarly_paper\ ontology is oriented towards the classical domains in science: +\<^enum> mathematics +\<^enum> informatics +\<^enum> natural sciences +\<^enum> technology and/or engineering + +It extends \<^verbatim>\COL\ by the following concepts: \begin{center} \begin{minipage}{.9\textwidth} \dirtree{% .0 . .1 scholarly\_paper.title. .1 scholarly\_paper.subtitle. -.1 scholarly\_paper.author{An Author Entity Declaration}. +.1 scholarly\_paper.author\DTcomment{An Author Entity Declaration}. .1 scholarly\_paper.abstract. .1 Isa\_COL.text\_element. -.2 scholarly\_paper.text\_section{A Subclass for Major Paper Text-Elements}. -.3 scholarly\_paper.introduction{...}. -.3 scholarly\_paper.conclusion{...}. -.4 scholarly\_paper.related\_work{...}. -.3 scholarly\_paper.bibliography{...}. -.3 scholarly\_paper.annex{...}. -.3 scholarly\_paper.example{...}. -.3 scholarly\_paper.technical{Freeform Class for Technical Content}. -.4 scholarly\_paper.math\_content{...}. -.5 scholarly\_paper.definition{Freeform}. -.5 scholarly\_paper.lemma{Freeform}. -.5 scholarly\_paper.theorem{Freeform}. -.5 scholarly\_paper.corollary{Freeform}. -.5 scholarly\_paper.math\_example{...}. -.5 scholarly\_paper.math\_semiformal{...}. -.4 scholarly\_paper.tech\_example{...}. -.4 scholarly\_paper.math\_motivation{...}. -.4 scholarly\_paper.math\_explanation{...}. -.4 scholarly\_paper.engineering\_content{...}. -.5 scholarly\_paper.data{...}. -.5 scholarly\_paper.evaluation{...}. -.5 scholarly\_paper.experiment{...}. +.2 scholarly\_paper.text\_section\DTcomment{Major Paper Text-Elements}. +.3 scholarly\_paper.introduction\DTcomment{...}. +.3 scholarly\_paper.conclusion\DTcomment{...}. +.4 scholarly\_paper.related\_work\DTcomment{...}. +.3 scholarly\_paper.bibliography\DTcomment{...}. +.3 scholarly\_paper.annex\DTcomment{...}. +.3 scholarly\_paper.example\DTcomment{Example in General Sense}. +.3 scholarly\_paper.technical\DTcomment{Root for Technical Content}. +.4 scholarly\_paper.math\_content\DTcomment{...}. +.5 scholarly\_paper.definition\DTcomment{Freeform}. +.5 scholarly\_paper.lemma\DTcomment{Freeform}. +.5 scholarly\_paper.theorem\DTcomment{Freeform}. +.5 scholarly\_paper.corollary\DTcomment{Freeform}. +.5 scholarly\_paper.math\_example\DTcomment{Freeform}. +.5 scholarly\_paper.math\_semiformal\DTcomment{Freeform}. +.4 scholarly\_paper.tech\_example\DTcomment{...}. +.4 scholarly\_paper.math\_motivation\DTcomment{...}. +.4 scholarly\_paper.math\_explanation\DTcomment{...}. +.4 scholarly\_paper.engineering\_content\DTcomment{...}. +.5 scholarly\_paper.data. +.5 scholarly\_paper.evaluation. +.5 scholarly\_paper.experiment. .4 ... .1 ... -.1 scholarly\_paper.article{The Paper Monitor}. +.1 scholarly\_paper.article\DTcomment{The Paper Monitor}. .1 \ldots. } \end{minipage} \end{center} + +\ + +text\A pivotal abstract class in the hierarchy is: +@{boxed_theory_text [display] +\ +doc_class text_section = text_element + + main_author :: "author option" <= None + fixme_list :: "string list" <= "[]" + level :: "int option" <= "None" +\} + +Besides attributes of more practical considerations like a fixme-list, that can be modified during +the editing process but is only visible in the integrated source but usually ignored in the +\<^LaTeX>, this class also introduces the possibility to assign an "ownership" or "responsibility" of +a text-element to a specific author. Note that this is possible since \<^isadof> assigns to each +document class also a class-type which is declared in the HOL environment.\ + +(*<*) +declare_reference*["text-elements-expls"::example] +(*>*) +text*[s23::example, main_author = "Some(@{docitem \bu\}::author)"]\ +Recall that concrete authors can be denoted by term-antiquotations generated by \<^isadof>; for example, +this may be for a text fragment like +@{boxed_theory_text [display] +\text*[\::example, main_author = "Some(@{docitem ''bu''}::author)"] \\\ \ \\\\} +or +@{boxed_theory_text [display] +\text*[\::example, main_author = "Some(@{docitem \bu\}::author)"] \\\ \ \\\\} + +where \<^boxed_theory_text>\"''bu''"\ is a string presentation of the reference to the author +text element (see below in @{docitem (unchecked) \text-elements-expls\}). \ text\Some of these concepts were supported as command-abbreviations leading to the extension @@ -564,7 +602,19 @@ of the \<^isadof> language: \ \ -subsubsection*["text-elements-expls"::technical]\Examples\ +text\Usually, command macros for text elements will assign to the default class corresponding for this +class. For pragmatic reasons, \<^theory_text>\Definition*\, \<^theory_text>\Lemma*\ and \<^theory_text>\Theorem*\ represent an exception +of this rule and are set up such that the default class is the super class @{typ \math_content\} +(rather than to the class @{typ \definition\}). +This way, it is possible to use these macros for several different sorts of the very generic +concept "definition", which can be used as a freeform mathematical definition but also for a +freeform terminological definition as used in certification standards. Moreover, new subclasses +of @{typ \math_content\} might be introduced in a derived ontology with an own specific layout +definition. +\ + + +subsubsection*["text-elements-expls"::example]\Examples\ text\ While the default user interface for class definitions via the @@ -572,7 +622,6 @@ text\ class, \<^isadof> provides short-hands for certain, widely-used, concepts such as \<^boxed_theory_text>\title*\ ... \\ or \<^boxed_theory_text>\section*\ ... \\, \<^eg>: - @{boxed_theory_text [display]\ title*[title::title]\Isabelle/DOF\ subtitle*[subtitle::subtitle]\User and Implementation Manual\ @@ -583,54 +632,29 @@ text\ affiliation = "\Université Paris-Saclay, LRI, Paris, France\"]\Burkhart Wolff\ \} -In general, all standard text-elements from the Isabelle document model such -as \<^theory_text>\chapter\, \<^theory_text>\section\, \<^theory_text>\text\, have in the \<^isadof> -implementation their counterparts in the family of text-elements that are ontology-aware, -\<^ie>, they dispose on a meta-argument list that allows to define that a test-element -that has an identity as a text-object labelled as \obj_id\, belongs to a document class -\class_id\ that has been defined earlier, and has its class-attributes set with particular -values (which are denotable in Isabelle/HOL mathematical term syntax). -\<^item> \annotated_text_element\ : -\<^rail>\ - ( ( @@{command "title*"} - | @@{command "subtitle*"} - | @@{command "author*"} - | @@{command "abstract*"}) - \ - '[' meta_args ']' '\' text '\' - ) - \ +\ + +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\}. +However, in order to avoid the somewhat tedious consequence: +@{boxed_theory_text [display] +\Theorem*[T1::"theorem", short_name="\DF definition captures deadlock-freeness\"] \\\ \ \\\\} + +the choice of the default class can be influenced by setting globally an attribute such as +@{boxed_theory_text [display] +\declare[[ Definition_default_class = "definition"]] + declare[[ Theorem_default_class = "theorem"]] +\} + +which allows the above example be shortened to: +@{boxed_theory_text [display] +\Theorem*[T1, short_name="\DF definition captures deadlock-freeness\"] \\\ \ \\\ +\} \ -text\\<^isadof> uses the concept of implicit abstract classes (or: \<^emph>\shadow classes\). -These refer to the set of possible \<^boxed_theory_text>\doc_class\ declarations that posses a number -of attributes with their types in common. Shadow classes represent an implicit requirement -(or pre-condition) on a given class to posses these attributes in order to work properly -for certain \<^isadof> commands. - -shadow classes will find concrete instances in COL, but \<^isadof> text elements do not \<^emph>\depend\ -on our COL definitions: Ontology developers are free to build own class instances for these -shadow classes, with own attributes and, last not least, own definitions of invariants independent -from ours. - -In particular, these shadow classes are used at present in \<^isadof>: -@{boxed_theory_text [display]\ -DOCUMENT_ALIKES = - level :: "int option" <= "None" - -ASSERTION_ALIKES = - properties :: "term list" - -FORMAL_STATEMENT_ALIKE = - properties :: "thm list" -\} - -These shadow-classes correspond to semantic macros - \<^ML>\Onto_Macros.enriched_document_cmd_exp\, - \<^ML>\Onto_Macros.assertion_cmd'\, and - \<^ML>\Onto_Macros.enriched_formal_statement_command\.\ - +subsection\ASSERTIONS : NEED TO BE INTEGRATED. TODO.\ text\ Similarly, we provide "minimal" instances of the \<^boxed_theory_text>\ASSERTION_ALIKES\ @@ -642,12 +666,41 @@ doc_class assertions = 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) + toLaTeX)\ +(*>*) +text\ The \<^verbatim>\technical_report\ ontology extends \<^verbatim>\scholarly_paper\ by concepts needed +for larger reports in the domain of mathematics and engineering. + +% +\begin{center} +\begin{minipage}{.9\textwidth} +\dirtree{% +.0 . +.1 technical\_report.front\_matter\DTcomment{...}. +.1 technical\_report.table\_of\_contents\DTcomment{...}. +.1 technical\_report.index\DTcomment{...}. +.1 ... +.1 technical\_report.report\DTcomment{...}. +} +\end{minipage} +\end{center} +\ + subsection\A Domain-Specific Ontology: \<^theory>\Isabelle_DOF.CENELEC_50128\\ + + subsubsection\Example: Text Elemens with Levels\ text\ The category ``exported constraint (EC)'' is, in the file diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index 4a92f6e..eab2540 100755 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -521,7 +521,8 @@ define_macro* hs2 \ \\hspace{\ _ \}\*) define_shortcut* clearpage \ \\clearpage{}\ - + hf \ \\hfill\ + br \ \\break\ end diff --git a/src/ontologies/technical_report/technical_report.thy b/src/ontologies/technical_report/technical_report.thy index 014235b..731d48b 100755 --- a/src/ontologies/technical_report/technical_report.thy +++ b/src/ontologies/technical_report/technical_report.thy @@ -35,7 +35,7 @@ doc_class index = section\Code Statement Elements\ doc_class "code" = technical + - checked :: bool <= "False" + checked :: bool <= "False" caption :: "string" <= "''''" @@ -79,251 +79,3 @@ doc_class report = end - -(* -===================================== -docclass: Isa_COL.thms - name: "thms" - origin: Isa_COL - attrs: "properties" - invs: -docclass: Isa_COL.figure - name: "figure" - origin: Isa_COL - attrs: "relative_width", "src", "placement", "spawn_columns"(True) - invs: -docclass: Isa_COL.chapter = Isa_COL.text_element + - name: "chapter" - origin: Isa_COL - attrs: "level"(Some 0) - invs: -docclass: Isa_COL.concept - name: "concept" - origin: Isa_COL - attrs: "tag"([]), "properties"([]) - invs: -docclass: Isa_COL.section = Isa_COL.text_element + - name: "section" - origin: Isa_COL - attrs: "level"(Some 1) - invs: -docclass: Isa_COL.assertions - name: "assertions" - origin: Isa_COL - attrs: "properties" - invs: -docclass: Isa_COL.subsection = Isa_COL.text_element + - name: "subsection" - origin: Isa_COL - attrs: "level"(Some 2) - invs: -docclass: Isa_COL.definitions - name: "definitions" - origin: Isa_COL - attrs: "requires", "establishes" - invs: -docclass: Isa_COL.formal_item - name: "formal_item" - origin: Isa_COL - attrs: "item" - invs: -docclass: Isa_COL.figure_group - name: "figure_group" - origin: Isa_COL - attrs: "trace"([]), "caption" - invs: -docclass: Isa_COL.text_element - name: "text_element" - origin: Isa_COL - attrs: "level"(None), "referentiable"(False), "variants"({STR ''outline'', STR ''document''}) - invs: -docclass: scholarly_paper.data = scholarly_paper.engineering_content + - name: "data" - origin: scholarly_paper - attrs: "tag"([]) - invs: -docclass: technical_report.SML = technical_report.code + - name: "SML" - origin: technical_report - attrs: "checked"(False) - invs: -docclass: Isa_COL.subsubsection = Isa_COL.text_element + - name: "subsubsection" - origin: Isa_COL - attrs: "level"(Some 3) - invs: -docclass: scholarly_paper.annex = scholarly_paper.text_section + - name: "annex" - origin: scholarly_paper - attrs: "main_author"(None) - invs: -docclass: scholarly_paper.lemma = scholarly_paper.math_content + - name: "lemma" - origin: scholarly_paper - attrs: "referentiable"(True), "mcc"(lem) - invs: d3::\\. lemma.mcc \ = lem -docclass: scholarly_paper.title - name: "title" - origin: scholarly_paper - attrs: "short_title"(None) - invs: -docclass: technical_report.ISAR = technical_report.code + - name: "ISAR" - origin: technical_report - attrs: "checked"(False) - invs: -docclass: technical_report.code = scholarly_paper.technical + - name: "code" - origin: technical_report - attrs: "checked"(False), "label"([]) - invs: -docclass: Isa_COL.formal_content - name: "formal_content" - origin: Isa_COL - attrs: "trace"([]), "style" - invs: -docclass: scholarly_paper.author - name: "author" - origin: scholarly_paper - attrs: "email"([]), "http_site"([]), "orcid"([]), "affiliation" - invs: -docclass: technical_report.LATEX = technical_report.code + - name: "LATEX" - origin: technical_report - attrs: "checked"(False) - invs: -docclass: technical_report.index - name: "index" - origin: technical_report - attrs: "kind", "level" - invs: -docclass: scholarly_paper.article - name: "article" - origin: scholarly_paper - attrs: "trace"([]), "style_id"(''LNCS''), "version"((0, 0, 0)) - invs: -docclass: scholarly_paper.example = scholarly_paper.text_section + - name: "example" - origin: scholarly_paper - attrs: "referentiable"(True), "status"(description), "short_name"([]) - invs: -docclass: scholarly_paper.theorem = scholarly_paper.math_content + - name: "theorem" - origin: scholarly_paper - attrs: "referentiable"(True), "mcc"(thm) - invs: d2::\\. theorem.mcc \ = thm -docclass: scholarly_paper.abstract - name: "abstract" - origin: scholarly_paper - attrs: "keywordlist"([]), "principal_theorems" - invs: -docclass: scholarly_paper.subtitle - name: "subtitle" - origin: scholarly_paper - attrs: "abbrev"(None) - invs: -docclass: scholarly_paper.corollary = scholarly_paper.math_content + - name: "corollary" - origin: scholarly_paper - attrs: "referentiable"(True), "mcc"(cor) - invs: d4::\\. corollary.mcc \ = thm -docclass: scholarly_paper.technical = scholarly_paper.text_section + - name: "technical" - origin: scholarly_paper - attrs: "definition_list"([]), "status"(description), "formal_results" - invs: L1::\\. 0 < the (text_section.level \) -docclass: scholarly_paper.conclusion = scholarly_paper.text_section + - name: "conclusion" - origin: scholarly_paper - attrs: "main_author"(None) - invs: -docclass: scholarly_paper.definition = scholarly_paper.math_content + - name: "definition" - origin: scholarly_paper - attrs: "referentiable"(True), "mcc"(defn) - invs: d1::\\. definition.mcc \ = defn -docclass: scholarly_paper.evaluation = scholarly_paper.engineering_content + - name: "evaluation" - origin: scholarly_paper - attrs: "tag"([]) - invs: -docclass: scholarly_paper.experiment = scholarly_paper.engineering_content + - name: "experiment" - origin: scholarly_paper - attrs: "tag"([]) - invs: -docclass: Isa_COL.side_by_side_figure = Isa_COL.figure + - name: "side_by_side_figure" - origin: Isa_COL - attrs: "anchor", "caption", "relative_width2", "src2", "anchor2", "caption2" - invs: -docclass: scholarly_paper.bibliography = scholarly_paper.text_section + - name: "bibliography" - origin: scholarly_paper - attrs: "style"(Some ''LNCS'') - invs: -docclass: scholarly_paper.introduction = scholarly_paper.text_section + - name: "introduction" - origin: scholarly_paper - attrs: "comment", "claims" - invs: -docclass: scholarly_paper.math_content = scholarly_paper.technical + - name: "math_content" - origin: scholarly_paper - attrs: "referentiable"(True), "short_name"([]), "status"(semiformal), "mcc"(thm) - invs: s1::\\. \ math_content.referentiable \ \ - math_content.short_name \ = [], s2::\\. math_content.status \ = semiformal -docclass: scholarly_paper.math_example = scholarly_paper.math_content + - name: "math_example" - origin: scholarly_paper - attrs: "referentiable"(True), "mcc"(expl) - invs: d5::\\. math_example.mcc \ = expl -docclass: scholarly_paper.related_work = scholarly_paper.conclusion + - name: "related_work" - origin: scholarly_paper - attrs: "main_author"(None) - invs: -docclass: scholarly_paper.tech_example = scholarly_paper.technical + - name: "tech_example" - origin: scholarly_paper - attrs: "referentiable"(True), "tag"([]) - invs: -docclass: scholarly_paper.text_section = Isa_COL.text_element + - name: "text_section" - origin: scholarly_paper - attrs: "main_author"(None), "fixme_list"([]), "level"(None) - invs: -docclass: technical_report.front_matter - name: "front_matter" - origin: technical_report - attrs: "front_matter_style" - invs: -docclass: scholarly_paper.math_motivation = scholarly_paper.technical + - name: "math_motivation" - origin: scholarly_paper - attrs: "referentiable"(False) - invs: -docclass: scholarly_paper.math_semiformal = scholarly_paper.math_content + - name: "math_semiformal" - origin: scholarly_paper - attrs: "referentiable"(True) - invs: -docclass: scholarly_paper.math_explanation = scholarly_paper.technical + - name: "math_explanation" - origin: scholarly_paper - attrs: "referentiable"(False) - invs: -docclass: technical_report.table_of_contents - name: "table_of_contents" - origin: technical_report - attrs: "bookmark_depth"(3), "depth"(3) - invs: -docclass: scholarly_paper.engineering_content = scholarly_paper.technical + - name: "engineering_content" - origin: scholarly_paper - attrs: "short_name"([]), "status" - invs: -===================================== - - -*) diff --git a/src/tests/ROOT b/src/tests/ROOT index f429670..759e0bd 100755 --- a/src/tests/ROOT +++ b/src/tests/ROOT @@ -4,5 +4,5 @@ session "Isabelle_DOF-tests" = "Isabelle_DOF" + "AssnsLemmaThmEtc" "Concept_ExampleInvariant" "Concept_Example" - "InnerSyntaxAntiquotations" + "TermAntiquotations" "Attributes" diff --git a/src/tests/InnerSyntaxAntiquotations.thy b/src/tests/TermAntiquotations.thy similarity index 95% rename from src/tests/InnerSyntaxAntiquotations.thy rename to src/tests/TermAntiquotations.thy index 164be01..ee8a72f 100755 --- a/src/tests/InnerSyntaxAntiquotations.thy +++ b/src/tests/TermAntiquotations.thy @@ -18,7 +18,7 @@ For historical reasons, \<^emph>\term antiquotations\ are called th "Inner Syntax Antiquotations". \ theory - InnerSyntaxAntiquotations + TermAntiquotations imports "Isabelle_DOF.Conceptual" begin @@ -50,7 +50,7 @@ text\Some sample lemma:\ lemma murks : "Example=Example" by simp text\Example for a meta-attribute of ODL-type @{typ "file"} with an appropriate ISA for the - file @{file "InnerSyntaxAntiquotations.thy"}\ + file @{file "TermAntiquotations.thy"}\ (* not working: text*[xcv::F, u="@{file ''InnerSyntaxAntiquotations.thy''}"]\Lorem ipsum ...\ *) @@ -65,7 +65,7 @@ text*[xcv2::C, g="@{thm ''HOL.refl''}"]\Lorem ipsum ...\ text\Major sample: test-item of doc-class \F\ with a relational link between class instances, and links to formal Isabelle items like \typ\, \term\ and \thm\. \ text*[xcv4::F, r="[@{thm ''HOL.refl''}, - @{thm \InnerSyntaxAntiquotations.murks\}]", (* long names required *) + @{thm \TermAntiquotations.murks\}]", (* long names required *) b="{(@{docitem ''xcv1''},@{docitem \xcv2\})}", (* notations \...\ vs. ''...'' *) s="[@{typ \int list\}]", properties = "[@{term \H \ H\}]" (* notation \...\ required for UTF8*)