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 b305a8a..a2e5db4 100755 --- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -16,8 +16,7 @@ theory TR_MyCommentedIsabelle imports "Isabelle_DOF.technical_report" begin -setup \ DOF_lib.define_shortcut \<^binding>\csp\ "CSP" - #> DOF_lib.define_shortcut \<^binding>\isabelle\ "Isabelle/HOL"\ +setup \ DOF_lib.define_shortcut \<^binding>\isabelle\ "Isabelle/HOL"\ open_monitor*[this::report] (*>*) @@ -32,14 +31,14 @@ text*[bu::author, text*[abs::abstract, keywordlist="[''LCF-Architecture'',''Isabelle'',''SML'',''PIDE'',''Programming Guide'', ''Tactic Programming'']"]\ - While Isabelle 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. + While Isabelle is mostly known as "logical framework" underlying \<^isabelle> and thus commonly + understood as 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 document editing, formal verification, and code generation. - This is a programming-tutorial of Isabelle and Isabelle/HOL, a complementary + This is a programming-tutorial of \<^isabelle>, conceived as a complementary text to the unfortunately somewhat outdated "The Isabelle Cookbook" in - \url{https://nms.kcl.ac.uk/christian.urban/Cookbook/}. The reader is encouraged + \<^url>\https://nms.kcl.ac.uk/christian.urban/Cookbook/\. The reader is encouraged not only to consider the generated .pdf, but also consult the loadable version in Isabelle/jEdit @{cite "DBLP:journals/corr/Wenzel14"}in order to make experiments on the running code. @@ -75,7 +74,7 @@ figure*[architecture::figure,relative_width="80",src="''figures/isabelle-archite asynchronous communication between the Isabelle system and the IDE (right-hand side). \ -text\This cookbook roughly follows the Isabelle system architecture shown in +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 @@ -89,8 +88,8 @@ section*[t11::technical] "ML, Text and Antiquotations" text\Isabelle is written in SML, the "Standard Meta-Language", which is is an impure functional programming language allowing, in principle, mutable variables and side-effects. The following Isabelle/Isar commands allow for accessing the underlying SML interpreter - of Isabelle directly. In the example, a mutable variable X is declared, defined to 0 and updated; - and finally re-evaluated leading to output: \ + 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; X:= !X + 1; @@ -106,7 +105,7 @@ text\However, since Isabelle is a platform involving parallel execution, c ML\ fun fac x = if x = 0 then 1 else x * fac(x-1) ; fac 10; \ -(* or *) +text\or:\ ML\ type state = { a : int, b : string} fun incr_state ({a, b}:state) = {a=a+1, b=b} \ @@ -123,7 +122,7 @@ text\ The Isabelle/Isar interpreter (called \<^emph>\toplevel\ text\ Besides the ML-command used in the above examples, there are a number of commands - representing text-elements in Isabelle/Isar; text commands can be interleaved arbitraryly + representing text-elements in Isabelle/Isar; text commands can be interleaved arbitrarily with other commands. Text in text-commands may use LaTeX and is used for type-setting documentations in a kind of literate programming style. \ @@ -143,13 +142,14 @@ figure*[fig2::figure, relative_width="100",src="''figures/text-element''"] text\ 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 - is supported via \<^emph>\antiquotations\'s. Generally speaking, antiquotations are a programming - technique to specify expressions or patterns in a quotation, parsed in the context of the - enclosing expression or pattern where the quotation is. Another way to understand this concept: - anti-quotations are "semantic macros" that produce a value for the surrounding context + 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 + anti-quotation in various contexts, be it in an ML fragment or a documentation fragment. + 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 a specific + 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 @@ -157,19 +157,36 @@ text\ In Isabelle documentations, antiquotation's were heavily used to enr to all sorts of entities in the context of the interpreting environment. Formal content allows for coping with sources that rapidly evolve and were developed by distributed teams as is typical in open-source developments. - A paradigmatic example for antiquotation in Texts and Program snippets is here:\ -text\ @{footnote \sdf\}, @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"}\ + A paradigmatic example for antiquotation in documentation text snippets and program snippets is here: + \<^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 y = @{typ "'a list"} + \ + } + \ + +(*<*) (* example to execute: *) +text\ @{footnote \sdf\}, @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"}\ ML\ val x = @{thm refl}; val y = @{term "A \ B"} val y = @{typ "'a list"} \ +(*>*) text\... which we will describe in more detail later. \ -text\In a way, literate specification attempting to maximize its formal content is a way to - ensure "Agile Development" in a (theory)-document development, at least for its objectives, - albeit not for its popular methods and processes like SCRUM. \ +text\In a way, anti-quotations implement a kind of + literate specification style in text, models, code, proofs, etc., which become alltogether + elements of one global \<^emph>\integrated document\ in which mutual dependencies can be machine=checked + (i.e. \formal\ in this sense). + Attempting to maximize the \formal content\ is a way to ensure "Agile Development" (AD) of an + integrated document development, in the sense that it allows to give immediate feedback + with respect to changes which enable thus the popular AD-objective \<^emph>\embrace change\. + Note that while we adhere to this objective, we do not depend or encourage popular AD methods + and processes such as SCRUM. \ paragraph\ A maximum of formal content inside text documentation also ensures the @@ -188,7 +205,7 @@ text\The bootstrapping sequence is also reflected in the following diagram section*[t12::technical] "Elements of the SML library"; -text\Elements of the @{file "$ISABELLE_HOME/src/Pure/General/basics.ML"} SML library +text\Elements of the \<^file>\~~/src/Pure/General/basics.ML\ SML library are basic exceptions. Note that exceptions should be catched individually, uncatched exceptions except those generated by the specific "error" function are discouraged in Isabelle source programming since they might produce races in the internal Isabelle evaluation. @@ -1128,8 +1145,8 @@ text\ The extensibility of Isabelle as a system framework depends on a num \<^item> \<^ML>\Document.state : unit -> Document.state\, giving the state as a "collection of named nodes, each consisting of an editable list of commands, associated with asynchronous execution process, - \<^item> \<^ML>\Session.get_keywords : unit -> Keyword.keywords\, this looks to be really session global, - \<^item> \<^ML>\Thy_Header.get_keywords : theory -> Keyword.keywords\ + \<^item> \<^ML>\Session.get_keywords : unit -> Keyword.keywords\, this looks to be session global, + \<^item> \<^ML>\Thy_Header.get_keywords : theory -> Keyword.keywords\ this looks to be just theory global. \ @@ -1137,15 +1154,14 @@ text\ The extensibility of Isabelle as a system framework depends on a num subsubsection*[ex1137::example]\A paradigmatic example: \<^theory_text>\text\\ text\ @{ML [display]\ - Outer_Syntax.command ("text", @{here}) "formal comment (primary style)" (Parse.opt_target -- Parse.document_source >> Pure_Syn.document_command {markdown = true}) \} -\ +\ text\Here are a few queries relevant for the global config of the isar engine:\ ML\ Document.state();\ -ML\ Session.get_keywords(); (* this looks to be really session global. *) \ +ML\ Session.get_keywords(); (* this looks to be session global. *) \ ML\ Thy_Header.get_keywords @{theory};(* this looks to be really theory global. *) \ @@ -1153,15 +1169,15 @@ ML\ Thy_Header.get_keywords @{theory};(* this looks to be really theory gl subsection*[transmgt::technical] \Transaction Management in the Isar-Engine : The Toplevel \ ML\Toplevel.exit: Toplevel.transition -> Toplevel.transition; - Toplevel.keep: (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; - Toplevel.keep': (bool -> Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; - Toplevel.ignored: Position.T -> Toplevel.transition; - Toplevel.generic_theory: (generic_theory -> generic_theory) -> Toplevel.transition -> Toplevel.transition; - Toplevel.theory': (bool -> theory -> theory) -> Toplevel.transition -> Toplevel.transition; - Toplevel.theory: (theory -> theory) -> Toplevel.transition -> Toplevel.transition; + Toplevel.keep: (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; + Toplevel.keep': (bool -> Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; + Toplevel.ignored: Position.T -> Toplevel.transition; + Toplevel.generic_theory: (generic_theory -> generic_theory) -> Toplevel.transition -> Toplevel.transition; + Toplevel.theory': (bool -> theory -> theory) -> Toplevel.transition -> Toplevel.transition; + Toplevel.theory: (theory -> theory) -> Toplevel.transition -> Toplevel.transition; - Toplevel.present_local_theory: - (xstring * Position.T) option -> + Toplevel.present_local_theory: + (xstring * Position.T) option -> (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; (* where text treatment and antiquotation parsing happens *) @@ -1324,10 +1340,10 @@ setup\HLDefinitionSample.define_test\ subsection*[ex212::example]\Proof Example (High-level)\ -text\The Isar-engine refers to a level of "specification constructs"; i.e. to a level with +text\The Isar-toplevel refers to a level of "specification constructs"; i.e. to a level with more high-level commands that represent internally quite complex theory transformations; with the exception of the axiomatization constructs, they are alltogether logically conservative. -The proof command interface bhind \lemma\ or \theorem\ uses a structure capturing the +The proof command interface behind \lemma\ or \theorem\ uses a structure capturing the syntactic @{ML_structure Element}'s of the \fix\, \assume\, \shows\ structuring. \