From 9c21b7a89ac431e0110fcef7bc7a7c7710b7b67f Mon Sep 17 00:00:00 2001 From: bu Date: Fri, 12 Jul 2019 16:32:19 +0200 Subject: [PATCH] restructuring intro --- .../MyCommentedIsabelle.thy | 39 +++++++++++++++---- 1 file changed, 31 insertions(+), 8 deletions(-) diff --git a/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy index 5f74ff1..60e2d12 100644 --- a/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy @@ -39,13 +39,40 @@ which makes this text re-checkable at each load and easier maintainable. chapter*[intro::introduction]\ Introduction \ +text\ +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. +This is a programming-tutorial of Isabelle and Isabelle/HOL, 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 not only to consider +the generated .pdf, but also consult the loadable version in Isabelle/jedit in order to make +experiments on the running code. This text is written itself in Isabelle/Isar using a specific +document ontology for technical reports. It is intended to be a "living document", i.e. it is not +only used for generating a static, conventional .pdf, but also for direct interactive exploration +in Isabelle/jedit. This way, 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.\ + +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). \ + +text\This cookbook 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. +\ chapter*[t1::technical]\ SML and Fundamental SML libraries \ 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. +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: \ @@ -140,12 +167,8 @@ text\It is instructive to study the fundamental bootstrapping sequence of command key in Isabelle/jedit and activating it) allows the Isabelle IDE to support hyperlinking \<^emph>\inside\ the Isabelle source.\ -text\The bootstrapping sequence is also reflected in the following diagram: \ - -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). \ +text\The bootstrapping sequence is also reflected in the following diagram +@{figure "architecture"}. \ section*[t12::technical] "Elements of the SML library";