diff --git a/examples/conceptual/InnerSyntaxAntiquotations.thy b/examples/conceptual/InnerSyntaxAntiquotations.thy index 2af9e73..145882f 100644 --- a/examples/conceptual/InnerSyntaxAntiquotations.thy +++ b/examples/conceptual/InnerSyntaxAntiquotations.thy @@ -11,8 +11,8 @@ an own syntax for references to types, terms, theorems, etc. are necessary. Thes of Isabelle/Isar, so inside the \verb+" ... "+ parenthesis. They are the key-mechanism to denote -\<^item> Links, i.e. attributes refering to doc classes defined by the ontology -\<^item> Meta-Links, i.e. attributes referring to formal entities inside Isabelle (such as thm's) +\<^item> Ontological Links, i.e. attributes refering to document classes defined by the ontology +\<^item> Ontological F-Links, i.e. attributes referring to formal entities inside Isabelle (such as thm's) This file contains a number of examples resulting from the @{theory "Conceptual"} - ontology; the emphasis of this presentation is to present the expressivity of ODL on a paradigmatical example. @@ -43,9 +43,13 @@ text*[xcv4::F, r="[@{thm ''HOL.refl''}, b="{(@{docitem ''xcv1''},@{docitem ''xcv2''})}", s="[@{typ ''int list''}]"]\Lorem ipsum ...\ +text*[xcv5::G, g="@{thm ''HOL.sym''}"]\Lorem ipsum ...\ + text\... and here we add a relation between @{docitem \xcv3\} and @{docitem \xcv2\} -into the relation \verb+b+ of @{docitem_ref \xcv4\} \ -update_instance*[xcv4::F, b+="{(@{docitem ''xcv3''},@{docitem ''xcv2''})}"] +into the relation \verb+b+ of @{docitem_ref \xcv5\}. Note that in the link-relation, +a @{typ "C"}-type is required, but a @{typ "G"}-type is offered which is leagal in +\verb+Isa_DOF+ because of the sub-class relation between those classes: \ +update_instance*[xcv4::F, b+="{(@{docitem ''xcv3''},@{docitem ''xcv5''})}"] text\And here is the result on term level:\ ML\ @{docitem_attr b::xcv4} \ diff --git a/examples/scholarly/IsaDofApplications.thy b/examples/scholarly/IsaDofApplications.thy index c04852d..654b883 100644 --- a/examples/scholarly/IsaDofApplications.thy +++ b/examples/scholarly/IsaDofApplications.thy @@ -88,9 +88,8 @@ scenarios from the point of view of the ontology modeling. In @{docitem_ref (unc we discuss the user-interaction generated from the ontological definitions. Finally, we draw conclusions and discuss related work in @{docitem_ref (unchecked) \conclusion\}. \ -section*[bgrnd::text_section, - main_author="Some(@{docitem ''adb''}::author)"] - \ Background: The Isabelle System \ +section*[bgrnd::text_section,main_author="Some(@{docitem ''adb''}::author)"]\ + Background: The Isabelle System \ text\ While Isabelle is widely perceived as an interactive theorem prover for HOL (Higher-order Logic)~\cite{nipkow.ea:isabelle:2002}, we @@ -117,9 +116,7 @@ it is the \emph{Eclipse of Formal Methods Tools}. This refers to the \end{itemize} \ -figure*[architecture::figure,relative_width="''100''", - src="''figures/isabelle-architecture''"] - \ The system architecture of Isabelle (left-hand side) and the +figure*[architecture::figure,relative_width="''100''",src="''figures/isabelle-architecture''"]\ The system architecture of Isabelle (left-hand side) and the asynchronous communication between the Isabelle system and the IDE (right-hand side). \ @@ -161,9 +158,7 @@ displayed and can be used for calculations before actually being typeset. When e Isabelle's PIDE offers auto-completion and error-messages while typing the above \emph{semi-formal} content. \ -section*[isadof::text_section, - main_author="Some(@{docitem ''adb''}::author)"] - \ \isadof \ +section*[isadof::text_section,main_author="Some(@{docitem ''adb''}::author)"]\ \isadof \ text\ An \isadof document consists of three components: \begin{itemize} @@ -284,9 +279,7 @@ semantic links between concepts can be modeled this way. The translation of its content to, \eg, Springer's \LaTeX{} setup for the Lecture Notes in Computer Science Series, as required by many scientific conferences, is mostly straight-forward. \ -figure*[fig1::figure, spawn_columns=False,relative_width="''95''", - src="''figures/Dogfood-Intro''"] - \ Ouroboros I: This paper from inside \ldots \ +figure*[fig1::figure,spawn_columns=False,relative_width="''95''",src="''figures/Dogfood-Intro''"]\ Ouroboros I: This paper from inside \ldots \ text*[ctest2]\This is a crucial test : @{docitem_ref \fig1\} @{thm "refl"}\ @@ -386,9 +379,7 @@ use fractions or even mathematical reals. This must be counterbalanced by syntac and semantic convenience. Choosing the mathematical reals, \eg, would have the drawback that attribute evaluation could be substantially more complicated.\ -figure*[fig_figures::figure, spawn_columns=False,relative_width="''85''", - src="''figures/Dogfood-figures''"] - \ Ouroboros II: figures \ldots \ +figure*[fig_figures::figure,spawn_columns=False,relative_width="''85''",src="''figures/Dogfood-figures''"]\ Ouroboros II: figures \ldots \ text\ The document class \inlineisar+figure+ --- supported by the \isadof text command \inlineisar+figure*+ --- makes it possible to express the pictures and diagrams in this paper @@ -515,9 +506,7 @@ exam-sheets with multiple-choice and/or free-response elements help of the latter, it is possible that students write in a browser a formal mathematical derivation---as part of an algebra exercise, for example---which is submitted to the examiners electronically. \ -figure*[fig_qcm::figure, spawn_columns=False,relative_width="''90''", - src="''figures/InteractiveMathSheet''"] - \ A Generated QCM Fragment \ldots \ +figure*[fig_qcm::figure,spawn_columns=False,relative_width="''90''",src="''figures/InteractiveMathSheet''"]\ A Generated QCM Fragment \ldots \ subsection*[cenelec_onto::example]\ The Certification Scenario following CENELEC \ text\ Documents to be provided in formal certifications (such as CENELEC @@ -602,41 +591,16 @@ class definition (\autoref{fig:Dogfood-IV-jumpInDocCLass}); hovering over an att (which is qualified in order to disambiguate; \autoref{fig:Dogfood-V-attribute}). \ -side_by_side_figure*["text-elements"::side_by_side_figure, - anchor="''fig-Dogfood-II-bgnd1''" - ,caption="''Exploring a Reference of a Text-Element.''" - ,relative_width="''48''" - ,src="''figures/Dogfood-II-bgnd1''" - ,anchor2="''fig-bgnd-text_section''" - ,caption2="''Exploring the class of a text element.''" - ,relative_width2="''47''" - ,src2="''figures/Dogfood-III-bgnd-text_section''" -]\ Exploring text elements. \ +side_by_side_figure*["text-elements"::side_by_side_figure,anchor="''fig-Dogfood-II-bgnd1''",caption="''Exploring a Reference of a Text-Element.''",relative_width="''48''",src="''figures/Dogfood-II-bgnd1''",anchor2="''fig-bgnd-text_section''",caption2="''Exploring the class of a text element.''",relative_width2="''47''",src2="''figures/Dogfood-III-bgnd-text_section''"]\ Exploring text elements. \ -side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV-jumpInDocCLass''" - ,caption="''Hyperlink to Class-Definition.''" - ,relative_width="''48''" - ,src="''figures/Dogfood-IV-jumpInDocCLass''" - ,anchor2="''fig:Dogfood-V-attribute''" - ,caption2="''Exploring an attribute.''" - ,relative_width2="''47''" - ,src2="''figures/Dogfood-III-bgnd-text_section''" -]\ Hyperlinks.\ +side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV-jumpInDocCLass''",caption="''Hyperlink to Class-Definition.''",relative_width="''48''",src="''figures/Dogfood-IV-jumpInDocCLass''",anchor2="''fig:Dogfood-V-attribute''",caption2="''Exploring an attribute.''",relative_width2="''47''",src2="''figures/Dogfood-III-bgnd-text_section''"]\ Hyperlinks.\ declare_reference*["figDogfoodVIlinkappl"::figure] -text\ An ontological reference application in -\autoref{figDogfoodVIlinkappl}: the -ontology-dependant antiquotation \inlineisar|@ {example ...}| refers to the corresponding -text-elements. Hovering allows for inspection, clicking for jumping to the definition. -If the link does not exist or has a non-compatible type, the text is not validated. -\ +text\ An ontological reference application in \autoref{figDogfoodVIlinkappl}: the ontology-dependant antiquotation \inlineisar|@ {example ...}| refers to the corresponding text-elements. Hovering allows for inspection, clicking for jumping to the definition. If the link does not exist or has a non-compatible type, the text is not validated. \ -figure*[figDogfoodVIlinkappl::figure,relative_width="''80''", - src="''figures/Dogfood-V-attribute''"] - \ Exploring an attribute (hyperlinked to the class). \ - +figure*[figDogfoodVIlinkappl::figure,relative_width="''80''",src="''figures/Dogfood-V-attribute''"]\ Exploring an attribute (hyperlinked to the class). \ subsection*[cenelec_pide::example]\ CENELEC \ declare_reference*[figfig3::figure] text\ The corresponding view in @{docitem_ref (unchecked) @@ -645,9 +609,7 @@ coherent to the @{example \cenelec_onto\}. The first sample shows s \cite{wenzel:isabelle-isar:2017} into formal entities of a theory. This way, the informal parts of a document get ``formal content'' and become more robust under change. \ -figure*[figfig3::figure,relative_width="''80''", - src="''figures/antiquotations-PIDE''"] - \ Standard antiquotations referring to theory elements.\ +figure*[figfig3::figure,relative_width="''80''",src="''figures/antiquotations-PIDE''"]\ Standard antiquotations referring to theory elements.\ declare_reference*[figfig5::figure] text\ The subsequent sample in @{docitem_ref (unchecked) \figfig5\} shows the definition of an @@ -656,12 +618,8 @@ has the consequence that a certain calculation must be executed sufficiently fas device. This condition can not be established inside the formal theory but has to be checked by system integration tests.\ -figure*[figfig5::figure,relative_width="''80''", - src="''figures/srac-definition''"] - \ Defining a SRAC reference \ldots \ -figure*[figfig7::figure,relative_width="''80''", - src="''figures/srac-as-es-application''"] - \ Using a SRAC as EC document reference. \ +figure*[figfig5::figure,relative_width="''80''",src="''figures/srac-definition''"]\ Defining a SRAC reference \ldots \ +figure*[figfig7::figure,relative_width="''80''",src="''figures/srac-as-es-application''"]\ Using a SRAC as EC document reference. \ text\ Now we reference in @{docitem_ref (unchecked) \figfig7\} this safety-related condition; however, this happens in a context where general \emph{exported constraints} are listed. diff --git a/ontologies/Conceptual.thy b/ontologies/Conceptual.thy index 4e04148..75a2c55 100644 --- a/ontologies/Conceptual.thy +++ b/ontologies/Conceptual.thy @@ -32,7 +32,11 @@ doc_class F = r :: "thm list" u :: "file" s :: "typ list" - b :: "(A \ C) set" <= "{}" + b :: "(A \ C) set" <= "{}" (* This is a relation link, roughly corresponding + to an association class. It can be used to track + claims to result - relations, for example.*) +doc_class G = C + + g :: "thm" <= "@{thm ''HOL.refl''}" doc_class M = trace :: "(A + C + D + F) list"