From 3ba9454ac7c9088edf4af29dcb2a0ef2908a4d8b Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Sun, 25 Oct 2020 12:57:43 +0100 Subject: [PATCH] Slight improvements of the layout --- .../TR_MyCommentedIsabelle.thy | 93 ++++++++++--------- 1 file changed, 49 insertions(+), 44 deletions(-) diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy index abc5d5e..2a74292 100755 --- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -53,7 +53,8 @@ text*[abs::abstract, chapter*[intro::introduction]\ Introduction \ -text\ While Isabelle @{cite "DBLP:books/sp/NipkowPW02"} is mostly known as part of Isabelle/HOL +text\ \<^vs>\-0.5cm\ + While Isabelle @{cite "DBLP:books/sp/NipkowPW02"} is mostly known as part of Isabelle/HOL (an interactive theorem prover), it actually provides a system framework for developing a wide spectrum of applications. A particular strength of the Isabelle framework is the combination of text editing, formal verification, and code generation. This is a programming-tutorial of @@ -67,18 +68,17 @@ text\ While Isabelle @{cite "DBLP:books/sp/NipkowPW02"} is mostly known as types, intermediate results of computations and checks can be repeated by the reader who is invited to interact with this document. Moreover, the textual parts have been enriched with a maximum of formal content which makes this text re-checkable at each load and easier - maintainable.\ + maintainable. \ -figure*[architecture::figure,relative_width="80",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). \ +figure*[architecture::figure,relative_width="70",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). \ text\This programming roughly follows the Isabelle system architecture shown in \<^figure>\architecture\, and, to be more precise, more or less in the bottom-up order. We start from the basic underlying SML platform over the Kernels to the tactical layer - and end with a discussion over the front-end technologies. + and end with a discussion over the front-end technologies. \<^vs>\-1.0cm\ \ chapter*[t1::technical]\ SML and Fundamental SML libraries \ @@ -91,7 +91,8 @@ text\Isabelle is written in SML, the "Standard Meta-Language", which is is of Isabelle directly. In the example, a mutable variable X is declared, initialized to 0 and updated; and finally re-evaluated leading to output: \ -ML\ val X = Unsynchronized.ref 0; +ML\ + val X = Unsynchronized.ref 0; X:= !X + 1; X \ @@ -102,11 +103,13 @@ text\However, since Isabelle is a platform involving parallel execution, c code-base @{cite "DBLP:conf/mkm/BarrasGHRTWW13"}. The preferred programming style is purely functional: \ -ML\ fun fac x = if x = 0 then 1 else x * fac(x-1) ; +ML\ + fun fac x = if x = 0 then 1 else x * fac(x-1) ; fac 10; \ text\or:\ -ML\ type state = { a : int, b : string} +ML\ + type state = { a : int, b : string} fun incr_state ({a, b}:state) = {a=a+1, b=b} \ @@ -130,18 +133,18 @@ text\So: the text command for:\ text\\<^emph>\This is a text.\\ -text\... is represented in an \<^verbatim>\.thy\ file by:\ +text\... is represented in the integrated source (the \<^verbatim>\.thy\ file) by:\ -text\\verb+text\\<^emph>\This is a text.\\+\ +text\ *\\\This is a text.\\\\ -text\and desplayed in the Isabelle/jedit front-end at the sceen by:\ +text\and displayed in the Isabelle/jedit front-end at the sceen by:\ -figure*[fig2::figure, relative_width="100",src="''figures/text-element''"] +figure*[fig2::figure, relative_width="60", placement="pl_h", src="''figures/text-element''"] \A text-element as presented in Isabelle/jedit.\ -text\ text-commands, ML- commands (and in principle any other command) can be seen as +text\The text-commands, ML- commands (and in principle any other command) can be seen as \<^emph>\quotations\ over the underlying SML environment (similar to OCaml or Haskell). - Linking these different sorts of quotations with each other and the underlying SML-envirnment + Linking these different sorts of quotations with each other and the underlying SML-environment is supported via \<^emph>\antiquotations\'s. Generally speaking, antiquotations are a kind of semantic macro whose arguments were checked, interpreted and expanded using the underlying system state. This paves the way for a programming technique to specify expressions or patterns in an @@ -149,8 +152,9 @@ text\ text-commands, ML- commands (and in principle any other command) can Anti-quotations as "semantic macros" can produce a value for the surrounding context (ML, text, HOL, whatever) depending on local arguments and the underlying logical context. - The way an antiquotation is specified depends on the quotation expander: typically, this is a specific - character and an identifier, or specific parentheses and a complete expression or pattern.\ + The way an antiquotation is specified depends on the quotation expander: typically, this is a + specific character and an identifier, or specific parentheses and a complete expression or + pattern.\ text\ In Isabelle documentations, antiquotation's were heavily used to enrich literate explanations and documentations by "formal content", i.e. machine-checked, typed references @@ -162,7 +166,7 @@ text\ In Isabelle documentations, antiquotation's were heavily used to enr \<^item> \<^theory_text>\text\@{footnote \sdf\}, @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"}\\ \<^item> @{theory_text [display] \ val x = @{thm refl}; - val y = @{term "A \ B"} + val _ = @{term "A \ B"} val y = @{typ "'a list"} \ } @@ -170,13 +174,14 @@ text\ In Isabelle documentations, antiquotation's were heavily used to enr (*<*) (* example to execute: *) text\ @{footnote \sdf\}, @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"}\ -ML\ val x = @{thm refl}; - val y = @{term "A \ B"} +ML\ + val x = @{thm refl}; + val _ = @{term "A \ B"} val y = @{typ "'a list"} \ (*>*) -text\... which we will describe in more detail later. \ +text\\<^vs>\-1,0cm\... which we will describe in more detail later. \ text\In a way, anti-quotations implement a kind of literate specification style in text, models, code, proofs, etc., which become alltogether @@ -478,28 +483,28 @@ text\Note, furthermore, that there is a programming API for the HOL-instan operators of the HOL logic specific constructors and destructors:\ text*[T2::technical]\ -\<^enum> \<^ML>\HOLogic.boolT : typ\ -\<^enum> \<^ML>\HOLogic.mk_Trueprop : term -> term\, the embedder of bool to prop fundamental for HOL -\<^enum> \<^ML>\HOLogic.dest_Trueprop : term -> term\ -\<^enum> \<^ML>\HOLogic.Trueprop_conv : conv -> conv\ -\<^enum> \<^ML>\HOLogic.mk_setT : typ -> typ\, the ML level type constructor set -\<^enum> \<^ML>\HOLogic.dest_setT : typ -> typ\, the ML level type destructor for set -\<^enum> \<^ML>\HOLogic.Collect_const : typ -> term\ -\<^enum> \<^ML>\HOLogic.mk_Collect : string * typ * term -> term\ -\<^enum> \<^ML>\HOLogic.mk_mem : term * term -> term\ -\<^enum> \<^ML>\HOLogic.dest_mem : term -> term * term\ -\<^enum> \<^ML>\HOLogic.mk_set : typ -> term list -> term\ -\<^enum> \<^ML>\HOLogic.conj_intr : Proof.context -> thm -> thm -> thm\, some HOL-level derived-inferences -\<^enum> \<^ML>\HOLogic.conj_elim : Proof.context -> thm -> thm * thm\ -\<^enum> \<^ML>\HOLogic.conj_elims : Proof.context -> thm -> thm list\ -\<^enum> \<^ML>\HOLogic.conj : term\ , some ML level logical constructors -\<^enum> \<^ML>\HOLogic.disj : term\ -\<^enum> \<^ML>\HOLogic.imp : term\ -\<^enum> \<^ML>\HOLogic.Not : term\ -\<^enum> \<^ML>\HOLogic.mk_not : term -> term\ -\<^enum> \<^ML>\HOLogic.mk_conj : term * term -> term\ -\<^enum> \<^ML>\HOLogic.dest_conj : term -> term list\ -\<^enum> \<^ML>\HOLogic.conjuncts : term -> term list\ +\<^enum> \<^ML>\HOLogic.boolT : typ\ \<^vs>\-0,2cm\ +\<^enum> \<^ML>\HOLogic.mk_Trueprop : term -> term\, the embedder of bool to prop fundamental for HOL \<^vs>\-0,2cm\ +\<^enum> \<^ML>\HOLogic.dest_Trueprop : term -> term\ \<^vs>\-0,2cm\ +\<^enum> \<^ML>\HOLogic.Trueprop_conv : conv -> conv\ \<^vs>\-0,2cm\ +\<^enum> \<^ML>\HOLogic.mk_setT : typ -> typ\, the ML level type constructor set \<^vs>\-0,2cm\ +\<^enum> \<^ML>\HOLogic.dest_setT : typ -> typ\, the ML level type destructor for set \<^vs>\-0,2cm\ +\<^enum> \<^ML>\HOLogic.Collect_const : typ -> term\ \<^vs>\-0,2cm\ +\<^enum> \<^ML>\HOLogic.mk_Collect : string * typ * term -> term\ \<^vs>\-0,2cm\ +\<^enum> \<^ML>\HOLogic.mk_mem : term * term -> term\ \<^vs>\-0,2cm\ +\<^enum> \<^ML>\HOLogic.dest_mem : term -> term * term\ \<^vs>\-0,2cm\ +\<^enum> \<^ML>\HOLogic.mk_set : typ -> term list -> term\ \<^vs>\-0,2cm\ +\<^enum> \<^ML>\HOLogic.conj_intr : Proof.context -> thm -> thm -> thm\, some HOL-level derived-inferences \<^vs>\-0,2cm\ +\<^enum> \<^ML>\HOLogic.conj_elim : Proof.context -> thm -> thm * thm\ \<^vs>\-0,2cm\ +\<^enum> \<^ML>\HOLogic.conj_elims : Proof.context -> thm -> thm list\ \<^vs>\-0,2cm\ +\<^enum> \<^ML>\HOLogic.conj : term\ , some ML level logical constructors \<^vs>\-0,2cm\ +\<^enum> \<^ML>\HOLogic.disj : term\ \<^vs>\-0,2cm\ +\<^enum> \<^ML>\HOLogic.imp : term\ \<^vs>\-0,2cm\ +\<^enum> \<^ML>\HOLogic.Not : term\ \<^vs>\-0,2cm\ +\<^enum> \<^ML>\HOLogic.mk_not : term -> term\ \<^vs>\-0,2cm\ +\<^enum> \<^ML>\HOLogic.mk_conj : term * term -> term\ \<^vs>\-0,2cm\ +\<^enum> \<^ML>\HOLogic.dest_conj : term -> term list\ \<^vs>\-0,2cm\ +\<^enum> \<^ML>\HOLogic.conjuncts : term -> term list\ \<^vs>\-0,2cm\ \<^enum> ... \