diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index ff8b79c..9d382cf 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -87,7 +87,7 @@ subsubsection*[isadof::technical]\Installing \<^isadof>\ text\ In the following, we assume that you already downloaded the \<^isadof> distribution (\href{\isadofarchiveurl}{\isadofarchiven}) from the \<^isadof> web site. The main steps for - installing are extracting the \<^isadof> distribution and calling its \inlinebash|install| script. + installing are extracting the \<^isadof> distribution and calling its \<^boxed_bash>\install\ script. We start by extracting the \<^isadof> archive: @{boxed_bash [display]\ë\prompt{}ë tar xf ë\href{\isadofarchiveurl}{\isadofarchiven}ë\} This will create a directory \texttt{\isadofdirn} containing \<^isadof> distribution. @@ -144,8 +144,8 @@ Isabelle/DOF Installer /usr/local/Isabelleë\isabelleversion/bin/isabelleë build -D . \} After the successful installation, you can now explore the examples (in the sub-directory -\inlinebash|examples| or create your own project. On the first start, the session -\inlinebash|Isabelle_DOF| will be built automatically. If you want to pre-build this +\<^boxed_bash>\examples\ or create your own project. On the first start, the session +\<^boxed_bash>\Isabelle_DOF\ will be built automatically. If you want to pre-build this session and all example documents, execute: @{boxed_bash [display]\ë\prompt{\isadofdirn}ë isabelle build -D . \} @@ -154,7 +154,7 @@ session and all example documents, execute: subsection*[first_project::technical]\Creating an \<^isadof> Project\ text\ \<^isadof> provides its own variant of Isabelle's - \inlinebash|mkroot| tool, called \inlinebash|mkroot_DOF|:\index{mkroot\_DOF} + \<^boxed_bash>\mkroot\ tool, called \<^boxed_bash>\mkroot_DOF\:\index{mkroot\_DOF} @{boxed_bash [display]\ë\prompt{}ë isabelle mkroot_DOF -h @@ -182,14 +182,14 @@ Usage: isabelle mkroot_DOF [OPTIONS] [DIR] \<^item> which ontologies (\<^eg>, scholarly\_paper) are required and \<^item> which document template (layout)\index{document template} should be used (\<^eg>, scrartcl\index{scrartcl}). Some templates (\<^eg>, lncs) require that the users manually - obtains and adds the necessary \<^LaTeX> class file (\<^eg>, \inlinebash|llncs.cls|. + obtains and adds the necessary \<^LaTeX> class file (\<^eg>, \<^boxed_bash>\llncs.cls\. This is due to licensing restrictions). \ text\ If you are happy with the defaults, \ie, using the ontology for writing academic papers (scholarly\_paper) using a report layout based on the article class (\inlineltx|scrartcl|) of the KOMA-Script bundle~@{cite "kohm:koma-script:2019"}, you can create your first project - \inlinebash|myproject| as follows: + \<^boxed_bash>\myproject\ as follows: @{boxed_bash [display]\ë\prompt{}ë isabelle mkroot_DOF myproject @@ -200,13 +200,13 @@ Preparing session "myproject" iëën "myproject" Now use the following coëëmmand line to build the session: isabelle build -D myproject \} - This creates a directory \inlinebash|myproject| containing the \<^isadof>-setup for your + This creates a directory \<^boxed_bash>\myproject\ containing the \<^isadof>-setup for your new document. To check the document formally, including the generation of the document in PDF, you only need to execute @{boxed_bash [display]\ë\prompt{}ë isabelle build -d . myproject \} -This will create the directory \inlinebash|myproject|: +This will create the directory \<^boxed_bash>\myproject\: \begin{center} \begin{minipage}{.9\textwidth} \dirtree{% @@ -220,9 +220,9 @@ This will create the directory \inlinebash|myproject|: } \end{minipage} \end{center} -The \<^isadof> configuration (\inlinebash|isadof.cfg|) specifies the required +The \<^isadof> configuration (\<^boxed_bash>\isadof.cfg\) specifies the required ontologies and the document template using a YAML syntax.\<^footnote>\Isabelle power users will recognize that -\<^isadof>'s document setup does not make use of a file \inlinebash|root.tex|: this file is +\<^isadof>'s document setup does not make use of a file \<^boxed_bash>\root.tex\: this file is replaced by built-in document templates.\ The main two configuration files for users are: \<^item> The file \<^boxed_bash>\ROOT\\<^index>\ROOT\, which defines the Isabelle session. New theory files as well as new @@ -453,42 +453,6 @@ figure*[fig02::figure,spawn_columns=False,relative_width="95",src="''figures/def text\The corresponding output of this snippet in the integrated source is shown in\<^figure>\fig02\. \ subsection*[scholar_pide::example]\More Freeform Elements, and Resulting Navigation\ -(* -figure*[fig1::figure,spawn_columns=False,relative_width="95",src="''figures/Dogfood-Intro''"] - \ Ouroboros I: This paper from inside \ldots \ - -text\ - @{docitem \fig1\} shows the corresponding view in the Isabelle/jedit of the start of an academic - paper. The text uses \<^isadof>'s own text-commands containing the meta-information provided by the - underlying ontology. We proceed by a definition of \<^boxed_theory_text>\introduction\'s, which we define - as the extension of \<^boxed_theory_text>\text_section\ which is intended to capture common infrastructure: - -@{boxed_theory_text [display]\ -doc_class introduction = text_section + - comment :: string -\} - - As a consequence of the definition as extension, the \<^boxed_theory_text>\introduction\ class - inherits the attributes \<^boxed_theory_text>\main_author\ and \<^boxed_theory_text>\todo_list\ - together with the corresponding default values. - - We proceed more or less conventionally by the subsequent sections: - -@{boxed_theory_text [display]\ -doc_class technical = text_section + - definition_list :: "string list" <= "[]" - -doc_class example = text_section + - comment :: string - -doc_class conclusion = text_section + - main_author :: "author option" <= None - -doc_class related_work = conclusion + - main_author :: "author option" <= None - -\} -*) text\ In the following, we present some other text-elements provided by the Common Ontology Library in @{theory "Isabelle_DOF.Isa_COL"}. It provides a document class for figures: @@ -559,12 +523,8 @@ text\ meta-information. Clicking on a document class identifier permits to hyperlink into the corresponding class definition (\autoref{fig:Dogfood-IV-jumpInDocCLass}); hovering over an attribute-definition (which is qualified in order to disambiguate; - \autoref{fig:Dogfood-V-attribute}). - % TODO for Burkhart Wolff. - % The last phrase should be completed to make it clearer: - % In this part "hovering over an...in order to disambiguate", something is missing. + \autoref{fig:Dogfood-V-attribute}) shows its type. \ -(* Bu : This autoref stuff could be avoided if we would finally have monitors over figures... *) figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-V-attribute''"] \ Exploring an attribute (hyperlinked to the class). \ @@ -716,124 +676,6 @@ safety-related condition; however, this happens in a context where general \<^em are listed. \<^isadof>'s checks establish that this is legal in the given ontology. \ -(* -section*[math_exam::example]\Writing Exams (math\_exam)\ -subsection\The Math Exam Example\ -text\ - The ontology ``math\_exam''\index{ontology!math\_exam} is an experimental ontology modeling - the process of writing exams at higher education institution in the United Kingdom, where exams - undergo both an internal and external review process. The \<^isadof> distribution contains a tiny - example using the ontology ``math\_exam'' in the directory - \nolinkurl{examples/math_exam/MathExam/}. You can inspect/edit the example - in Isabelle's IDE, by either - \<^item> starting Isabelle/jedit using your graphical user interface (\<^eg>, by clicking on the - Isabelle-Icon provided by the Isabelle installation) and loading the file - \nolinkurl{examples/math_exam/MathExam/MathExam.thy}. - \<^item> starting Isabelle/jedit from the command line by calling: -@{boxed_bash [display]\ë\prompt{\isadofdirn}ë - isabelle jedit examples/math_exam/MathExam/MathExam.thy \} -\ -text\ - You can build the PDF-document by calling: -@{boxed_bash [display]\ë\prompt{}ë isabelle build MathExam\} -\ - -subsection\Modeling Exams\ -text\ - The math-exam scenario is an application with mixed formal and semi-formal content. It addresses - applications where the author of the exam is not present during the exam and the preparation - requires a very rigorous process. - - We assume that the content has four different types of addressees, which have a different - \<^emph>\view\ on the integrated document: - \<^item> the \<^emph>\setter\, \ie, the author of the exam, - \<^item> the \<^emph>\checker\, \ie, an internal person that checks - the exam for feasibility and non-ambiguity, - \<^item> the \<^emph>\external\, \ie, an external person that checks - the exam for feasibility and non-ambiguity, and - \<^item> the \<^emph>\student\, \ie, the addressee of the exam. -\ -text\ - The latter quality assurance mechanism is used in many universities, - where for organizational reasons the execution of an exam takes place in facilities - where the author of the exam is not expected to be physically present. - Furthermore, we assume a simple grade system (thus, some calculation is required). We - can model this as follows: - -@{boxed_theory_text [display]\ -doc_class Author = ... -datatype Subject = algebra | geometry | statistical -datatype Grade = A1 | A2 | A3 -doc_class Header = examTitle :: string - examSubject :: Subject - date :: string - timeAllowed :: int -- minutes -datatype ContentClass = setter - | checker - | external_examiner - | student -doc_class Exam_item = concerns :: "ContentClass set" -doc_class Exam_item = concerns :: "ContentClass set" - -type_synonym SubQuestion = string -\} - - The heart of this ontology is an alternation of questions and answers, where the answers can - consist of simple yes-no answers or lists of formulas. Since we do not assume familiarity of - the students with Isabelle (\<^boxed_theory_text>\term\ would assume that this is a parse-able and - type-checkable entity), we basically model a derivation as a sequence of strings: - -@{boxed_theory_text [display]\ -doc_class Answer_Formal_Step = Exam_item + - justification :: string - "term" :: "string" - -doc_class Answer_YesNo = Exam_item + - step_label :: string - yes_no :: bool -- \for checkboxes\ - -datatype Question_Type = - formal | informal | mixed - -doc_class Task = Exam_item + - level :: Level - type :: Question_Type - subitems :: "(SubQuestion * - (Answer_Formal_Step list + Answer_YesNo) list) list" - concerns :: "ContentClass set" <= "UNIV" - mark :: int -doc_class Exercise = Exam_item + - type :: Question_Type - content :: "(Task) list" - concerns :: "ContentClass set" <= "UNIV" - mark :: int -\} - -In many institutions, having a rigorous process of validation for exam subjects makes sense: is -the initial question correct? Is a proof in the sense of the question possible? We model the -possibility that the @{term examiner} validates a question by a sample proof validated by Isabelle: - -@{boxed_theory_text [display]\ -doc_class Validation = - tests :: "term list" <="[]" - proofs :: "thm list" <="[]" - -doc_class Solution = Exam_item + - content :: "Exercise list" - valids :: "Validation list" - concerns :: "ContentClass set" <= "{setter,checker,external_examiner}" - -doc_class MathExam= - content :: "(Header + Author + Exercise) list" - global_grade :: Grade - where "\Author\$^+$ ~~ Header ~~ \Exercise ~~ Solution\$^+$ " -\} - -In our scenario this sample proofs are completely \<^emph>\intern\, \ie, not exposed to the -students but just additional material for the internal review process of the exam. -\ - -*) section*[tech_onto::example]\Writing Technical Reports in \<^boxed_theory_text>\technical_report\\ text\While it is perfectly possible to write documents in the @@ -882,22 +724,6 @@ So its value is that readers can just reuse some of these snippets and adapt the purposes. \ -(* -@{boxed_theory_text [display] \ -text\Finally, a number of commonly used "squigglish" combinators is listed: - -\<^item> @{ML "op ! : 'a Unsynchronized.ref->'a"}, access operation on a program variable -\<^item> @{ML "op := : ('a Unsynchronized.ref * 'a)->unit"}, update operation on a program variable -\<^item> @{ML "op #> : ('a->'b) * ('b->'c)->'a->'c"}, a reversed function composition -\<^item> @{ML "op o : (('b->'c) * ('a->'b))->'a->'c"}, function composition -\<^item> @{ML "op || : ('a->'b) * ('a->'b) -> 'a -> 'b"}, parse alternative -\<^item> @{ML "op -- : ('a->'b*'c) * ('c->'d*'e)->'a->('b*'d)*'e"}, parse pair -\<^item> @{ML "op ? : bool * ('a->'a)->'a->'a"}, if then else -\<^item> @{ML "I : 'a -> 'a"}, the I combinator -\<^item> @{ML "K : 'a -> 'b -> 'a"}, the K combinator \ -\} -*) - figure*[strict_SS::figure, relative_width="95", src="''figures/MyCommentedIsabelle.png''"] \A table with a number of SML functions, together with their type.\