From 85d94848b6a52f8e3e68418f8453b3de5631a05b Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 6 Feb 2021 12:08:18 +0000 Subject: [PATCH] Revised Chapter 3. --- .../Isabelle_DOF-Manual/03_GuidedTour.thy | 58 +++++++------------ 1 file changed, 20 insertions(+), 38 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index 044e7c2..338b662 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -391,22 +391,6 @@ standard inductive \<^theory_text>\datatype\ definition mechanism i for attibute declarations. Vice-versa, document class definitions imply a corresponding HOL type definition. \ -(* For Achim zum spielen... -text\For example, this allows the following presentation in the source: -@{boxed_theory_text [display] \ -text*[X2::"definition"]\\RUN A \ \ X. \ x \ A \ X\ \<^vs>\-0.7cm\\ -text*[X3::"definition"]\\CHAOS A \ \ X. (STOP \ (\ x \ A \ X))\ \<^vs>\-0.7cm\\ -text*[X4::"definition"]\\CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \ \ X. (SKIP \ STOP \ (\ x \ A \ X))\\<^vs>\-0.7cm\\ - -text\ The \RUN\-process defined @{definition X2} represents the process that accepts all -events, but never stops nor deadlocks. The \CHAOS\-process comes in two variants shown in -@{definition X3} and @{definition X4}: the process that non-deterministically stops or -accepts any offered event, wheras \CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P\ can additionaly terminate.\ -\} -\ -*) - -(* alternative *) figure*[fig01::figure,spawn_columns=False,relative_width="95",src="''figures/definition-use-CSP.png''"] \ A screenshot of the integrated source with definitions ...\ text\An example for a sequence of (Isabelle-formula-) texts, their ontological declarations as @@ -436,6 +420,9 @@ We refrain ourselves here to briefly describe three freeform antiquotations used \<^item> the freeform antiquotations for verbatim, emphasized, bold, or footnote text elements. \ +figure*[fig02::figure,spawn_columns=False,relative_width="95",src="''figures/definition-use-CSP-pdf.png''"] + \ ... and the corresponding pdf-oputput.\ + text\ \<^isadof> text-elements such as \<^theory_text>\text*\ allow to have such standard term-antiquotations inside their text, permitting to give the whole text entity a formal, referentiable status with typed meta- @@ -443,8 +430,6 @@ information attached to it that may be used for presentation issues, search, or purposes. The corresponding output of this snippet in the integrated source is shown in \<^figure>\fig02\. \ -figure*[fig02::figure,spawn_columns=False,relative_width="95",src="''figures/definition-use-CSP-pdf.png''"] - \ ... and the corresponding pdf-oputput.\ subsection*[scholar_pide::example]\More Freeform Elements, and Resulting Navigation\ text\ In the following, we present some other text-elements provided by the Common Ontology Library @@ -479,11 +464,12 @@ text\ where "(title ~~ \subtitle\ ~~ \author\$^+$+ ~~ abstract ~~ introduction ~~ \technical || example\$^+$ ~~ conclusion ~~ bibliography)" - % TODO: - % Update to the new implementation. - % where is deprecated and the new implementation uses accepts and rejects. - \} + \}\ + (* % TODO: + % Update to the new implementation. + % where is deprecated and the new implementation uses accepts and rejects. *) +text\ In a integrated document source, the body of the content can be paranthesized into: @{boxed_theory_text [display]\ @@ -564,9 +550,7 @@ text\ processes. Making the link-structure machine-checkable, be it between requirements, assumptions, their implementation and their discharge by evidence (be it tests, proofs, or authoritative arguments), has the potential in our view to decrease the cost of software developments - targeting certifications. Note that continuously checking the links between the formal and the - semi-formal parts of such documents is particularly valuable during the development, - which is usually a collaborative effort. + targeting certifications. As in many other cases, formal certification documents come with an own terminology and pragmatics of what has to be demonstrated and where, and how the traceability of requirements through @@ -581,11 +565,11 @@ doc_class requirement = long_name :: "string option" doc_class requirement_analysis = no :: "nat" where "requirement_item +" - +(* % TODO: % Update to the new implementation. -% where is deprecated and the new implementation uses accepts and rejects. - +% where is deprecated and the new implementation uses accepts and rejects. +*) doc_class hypothesis = requirement + hyp_type :: hyp_type <= physical (* default *) @@ -695,17 +679,15 @@ We still mention a few of these document antiquotations here: \<^item> \<^theory_text>\@{value \term\ }\ performs the evaluation of \term\, \<^item> \<^theory_text>\@{ML \ml-term\ }\ parses and type-checks \ml-term\, \<^item> \<^theory_text>\@{ML_file \ml-file\ }\ parses the path for \ml-file\ and - verifies its existance in the (Isabelle-virtual) file-system, -\<^item> ... - -Note that there are options to display sub-parts of formulas etc., but it is a consequence + verifies its existance in the (Isabelle-virtual) file-system. +\ +text\There are options to display sub-parts of formulas etc., but it is a consequence of tight-checking that the information must be given complete and exactly in the syntax of Isabelle. This may be over-precise and a burden to readers not familiar with Isabelle, which may motivate authors to choose the aforementioned freeform-style. \ -subsection\A \<^verbatim>\technical_report\ in tight-checking-style: \TR_MyCommentedIsabelle\ - Programming Manual \ - +subsection\A Technical Report with Tight Checking\ text\An example of tight checking is a small programming manual developed by the second author in order to document programming trick discoveries while implementing in Isabelle. While not necessarily a meeting standards of a scientific text, it appears to us that this information @@ -734,12 +716,12 @@ In the pdf output, these text-fragments were displayed verbatim. section\Style Guide\ text\ - The document generation process of \<^isadof> is based on Isabelle's document generation framework, + The document generation of \<^isadof> is based on Isabelle's document generation framework, using \<^LaTeX>{} as the underlying back-end. As Isabelle's document generation framework, it is possible to embed (nearly) arbitrary \<^LaTeX>-commands in text-commands, \<^eg>: @{boxed_theory_text [display]\ -text\ This is \emph{emphasized} a$$nd this is a +text\ This is \emph{emphasized} and this is a citation~\cite{brucker.ea:isabelle-ontologies:2018}\ \} @@ -747,8 +729,8 @@ text\ This is \emph{emphasized} a$$nd this is a Isabelle) provided alternatives: @{boxed_theory_text [display]\ -text\ This is *\emphasized\ a$$nd this is a - citation <@>{cite "brucker.ea:isabelle-ontologies:2018"}.\ +text\ This is *\emphasized\ and this is a + citation @{cite "brucker.ea:isabelle-ontologies:2018"}.\ \} Clearly, this is not always possible and, in fact, often \<^isadof> documents will contain