--- a/ProgTutorial/Intro.thy Tue May 14 17:45:13 2019 +0200
+++ b/ProgTutorial/Intro.thy Thu May 16 19:56:12 2019 +0200
@@ -4,7 +4,6 @@
chapter \<open>Introduction\<close>
-
text \<open>
\begin{flushright}
{\em
@@ -16,7 +15,7 @@
\end{flushright}
\medskip
- If your next project requires you to program on the ML-level of Isabelle,
+ If your next project requires you to program Isabelle with ML,
then this tutorial is for you. It will guide you through the first steps of
Isabelle programming, and also explain ``tricks of the trade''. We also hope
the tutorial will encourage students and researchers to play with Isabelle
@@ -27,7 +26,7 @@
Isabelle interface with the Jedit GUI. Explanation of this part is beyond
this tutorial.
- The best way to get to know the ML-level of Isabelle is by experimenting
+ The best way to get to know the Isabelle/ML is by experimenting
with the many code examples included in the tutorial. The code is as far as
possible checked against the Isabelle
distribution.%%\footnote{\input{version.tex}}
@@ -47,11 +46,51 @@
the functional programming language ML, the language in which most of
Isabelle is implemented. If you are unfamiliar with either of these two
subjects, then you should first work through the Isabelle/HOL tutorial
- \cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}. Recently,
+ @{cite "isa-tutorial"} or Paulson's book on ML @{cite "paulson-ml2"}. Recently,
Isabelle has adopted a sizable amount of Scala code for a slick GUI
based on jEdit. This part of the code is beyond the interest of this
tutorial, since it mostly does not concern the regular Isabelle
developer.
+
+ The rich Isabelle infrastructure can be categorized by various aspects @{cite "wenzel-technology"}:
+
+ @{emph \<open>@{bold \<open>Logic\<close>}\<close>}
+ \begin{description}
+ \item[Isabelle/Pure] is the logical Framework and bootstrap environment. The Pure logic
+ is used to represent rules for Higher-Order Natural Deduction declaratively. This allows
+ the implementation and definition of object logics like HOL using the Pure logic and
+ framework.
+ \item[Isabelle/HOL] is the main library of theories and tools for applications that is used
+ throughout this tutorial.
+ \end{description}
+
+ @{emph \<open>@{bold\<open>Programming\<close>}\<close>}
+ \begin{description}
+ \item[Isabelle/ML] is the Isabelle tool implementation and extension language. It is based
+ on Poly/ML\footnote{@{url \<open>http://polyml.org\<close>}}. Both Isabelle/Pure and Isabelle/ML emerge
+ from the same bootstrap process: the result is a meta-language for programming the logic
+ that is intertwined with it from a technological viewpoint, but logic and programming
+ remain formally separated.
+ \item[Isabelle/Scala] is the Isabelle system programming language. It connects the logical
+ environment with the outside world. Most notably resulting in the Prover IDE Isabelle/jEdit
+ and the command line tools.
+ \end{description}
+
+ @{emph \<open>@{bold\<open>Proof\<close>}\<close>}
+ \begin{description}
+ \item[Isabelle/Isar] is the structured proof language of the Isabelle framework. Isar
+ means, Intelligible semi-automated reasoning.
+ \item[Document language] for HTML output and \LaTeX type-setting of proof text. A proof
+ document combines formal and informal text to describe what has been proven to a general
+ audience.
+ \end{description}
+
+ @{emph \<open>@{bold\<open>IDE\<close>}\<close>}
+ \begin{description}
+ \item[Isabelle/jEdit] is the IDE for proof and tool development. It provides a rich interactive
+ frontend to the Isabelle framework in which logic and proof development, document creation as
+ well as ML programming are seamlessly integrated.
+ \end{description}
\<close>
section \<open>Existing Documentation\<close>
@@ -61,18 +100,23 @@
part of the distribution of Isabelle):
\begin{description}
- \item[The Isabelle/Isar Implementation Manual] describes Isabelle
- from a high-level perspective, documenting some of the underlying
- concepts and interfaces.
+ \item[The Isabelle/Isar Reference Manual] provides a top level view on the Isabelle system,
+ explaining general concepts and specification material (like grammars,
+ examples and so on) about Isabelle, Isar, Pure, HOL and the document language.
- \item[The Isabelle Reference Manual] is an older document that used
+ \item[The Isabelle/Isar Implementation Manual] describes Isabelle
+ implementation from a high-level perspective, documenting the major
+ underlying concepts and interfaces.
+
+ \item[Isabelle/jEdit] describes the IDE.
+
+ \item[The Old Introduction to Isabelle] is an older document that used
to be the main reference of Isabelle at a time when all proof scripts
- were written on the ML-level. Many parts of this manual are outdated
+ were written with ML. Many parts of this manual are outdated
now, but some parts, particularly the chapters on tactics, are still
useful.
- \item[The Isar Reference Manual] provides specification material (like grammars,
- examples and so on) about Isar and its implementation.
+
\end{description}
Then of course there are:
@@ -86,9 +130,12 @@
parts, it is often good to look at code that does similar things as you
want to do and learn from it.
This tutorial contains frequently pointers to the
- Isabelle sources. Still, the UNIX command \mbox{\<open>grep -R\<close>} is
- often your best friend while programming with Isabelle.\footnote{Or
- hypersearch if you work with jEdit.} To understand the sources,
+ Isabelle sources. The best way is to interactively explore the sources
+ within the IDE provided by Isabelle/jEdit. By loading @{ML_file "Pure/ROOT.ML"}
+ into Isabelle/jEdit the sources of Pure are annotated with markup and you can
+ interactively follow the structure.
+ Moreover, the UNIX command \mbox{\<open>grep -R\<close>} or hypersearch within Isabelle/jEdit is
+ often your best friend while programming with Isabelle. To understand the sources,
it is often also necessary to track the change history of a file or
files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}}
for Isabelle provides convenient interfaces to query the history of
@@ -122,7 +169,7 @@
generates when evaluated. This response is prefixed with a
@{text [quotes] ">"}, like:
- @{ML_response [display,gray] "3 + 4" "7"}
+ @{ML_matchresult [display,gray] "3 + 4" "7"}
The user-level commands of Isabelle (i.e., the non-ML code) are written
in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply},
@@ -155,7 +202,7 @@
understand code written by somebody else. This is aggravated in Isabelle by
the fact that many parts of the code contain none or only few
comments. There is one strategy that might be helpful to navigate your way:
- ML is an interactive programming environment, which means you can evaluate
+ ML and Isabelle/jEdit is an interactive programming environment, which means you can evaluate
code on the fly (for example inside an \isacommand{ML}~\<open>\<verbopen>\<dots>\<verbclose>\<close> section). So you can copy (self-contained)
chunks of existing code into a separate theory file and then study it
alongside with examples. You can also install ``probes'' inside the copied
@@ -284,7 +331,7 @@
\item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}
and exercise \ref{fun:killqnt}.
- \item {\bf Sascha B�hme} contributed the recipes in \ref{rec:timeout},
+ \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout},
\ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion}
and helped with recipe \ref{rec:timing}. Parts of section \ref{sec:storing}
are by him.
@@ -305,12 +352,15 @@
in section \ref{sec:theorems}.
\item {\bf Alexander Krauss} wrote a very early version of the ``first-steps''
- chapter and also contributed the material on @{ML_funct Named_Thms}.
+ chapter and also contributed the material on @{ML_functor Named_Thms}.
%%\item {\bf Tobias Nipkow} contributed recipe \ref{rec:callml}.
\item {\bf Michael Norrish} proofread parts of the text.
+ \item {\bf Norbert Schirmer} updated the document to work with Isabelle 2018 and
+ later.
+
\item {\bf Andreas Schropp} improved and corrected section \ref{sec:univ} and
contributed towards section \ref{sec:sorts}.