--- a/ProgTutorial/First_Steps.thy Tue Jun 14 22:09:40 2011 +0100
+++ b/ProgTutorial/First_Steps.thy Fri Jun 17 16:58:05 2011 +0100
@@ -57,7 +57,8 @@
\end{graybox}
\end{isabelle}
- Like normal Isabelle scripts, \isacommand{ML}-commands can be evaluated by
+ If you work with ProofGeneral then like normal Isabelle scripts
+ \isacommand{ML}-commands can be evaluated by
using the advance and undo buttons of your Isabelle environment. The code
inside the \isacommand{ML}-command can also contain value and function
bindings, for example
@@ -148,18 +149,10 @@
@{ML_response_fake [display,gray] "writeln (@{make_string} 1)" "\"1\""}
However, @{text "@{makes_tring}"} only works if the type of what
- is converted is monomorphic and not a function.
+ is converted is monomorphic and not a function.
- The function @{ML "writeln"} should only be used for testing purposes,
- because any output this function generates will be overwritten as soon as an
- error is raised. For printing anything more serious and elaborate, the
- function @{ML_ind tracing in Output} is more appropriate. This function writes all
- output into a separate tracing buffer. For example:
-
- @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
-
- You can print out error messages with the function @{ML_ind error in Library}; for
- example:
+ You can print out error messages with the function @{ML_ind error in Library};
+ for example:
@{ML_response_fake [display,gray]
"if 0=1 then true else (error \"foo\")"
@@ -168,40 +161,13 @@
This function raises the exception @{text ERROR}, which will then
be displayed by the infrastructure. Note that this exception is meant
- for ``user-level'' error messages seen by the ``end-user''.
-
+ for ``user-level'' error messages seen by the ``end-user''.
+
For messages where you want to indicate a genuine program error, then
use the exception @{text Fail}. Here the infrastructure indicates that this
is a low-level exception, and also prints the source position of the ML
raise statement.
-
- \footnote{\bf FIXME Mention how to work with @{ML_ind debug in Toplevel} and
- @{ML_ind profiling in Toplevel}.}
-
-*}
-
-(* FIXME*)
-(*
-ML {* reset Toplevel.debug *}
-
-ML {* fun dodgy_fun () = (raise TYPE ("",[],[]); 1) *}
-
-ML {* fun innocent () = dodgy_fun () *}
-ML {* exception_trace (fn () => cterm_of @{theory} (Bound 0)) *}
-ML {* exception_trace (fn () => innocent ()) *}
-
-ML {* Toplevel.program (fn () => cterm_of @{theory} (Bound 0)) *}
-
-ML {* Toplevel.program (fn () => innocent ()) *}
-*)
-
-text {*
- %Kernel exceptions TYPE, TERM, THM also have their place in situations
- %where kernel-like operations are involved. The printing is similar as for
- %Fail, although there is some special treatment when Toplevel.debug is
- %enabled.
-
Most often you want to inspect data of Isabelle's basic data structures,
namely @{ML_type term}, @{ML_type typ}, @{ML_type cterm}, @{ML_type ctyp}
and @{ML_type thm}. Isabelle contains elaborate pretty-printing functions,
@@ -252,13 +218,17 @@
text {*
@{ML_response_fake [display, gray]
- "pwriteln (pretty_term
- (Config.put show_all_types true @{context}) @{term \"(1::nat, x)\"})"
+ "let
+ val show_all_types_ctxt = Config.put show_all_types true @{context}
+in
+ pwriteln (pretty_term show_all_types_ctxt @{term \"(1::nat, x)\"})
+end"
"(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"}
- where @{term Pair} is the term-constructor for products.
- Other configuration values that influence printing of terms are
- @{ML_ind show_brackets in Syntax} and @{ML_ind show_sorts in Syntax}.
+ where now even @{term Pair} is written with its type (@{term Pair} is the
+ term-constructor for products). Other configuration values that influence
+ printing of terms are @{ML_ind show_brackets in Syntax} and @{ML_ind
+ show_sorts in Syntax}.
*}
text {*
@@ -297,21 +267,15 @@
"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
However, in order to improve the readability when printing theorems, we
- convert these schematic variables into free variables using the function
- @{ML_ind import in Variable}. This is similar to statements like @{text
- "conjI[no_vars]"} on Isabelle's user-level.
+ can switch off the question marks as follows:
*}
-ML{*fun no_vars ctxt thm =
-let
- val ((_, [thm']), _) = Variable.import true [thm] ctxt
+ML{*fun pretty_thm_no_vars ctxt thm =
+let
+ val ctxt' = Config.put show_question_marks false ctxt
in
- thm'
-end
-
-fun pretty_thm_no_vars ctxt thm =
- pretty_term ctxt (prop_of (no_vars ctxt thm))*}
-
+ pretty_term ctxt' (prop_of thm)
+end*}
text {*
With this function, theorem @{thm [source] conjI} is now printed as follows:
@@ -542,12 +506,12 @@
The remaining combinators we describe in this section add convenience for the
``waterfall method'' of writing functions. The combinator @{ML_ind tap in
Basics} allows you to get hold of an intermediate result (to do some
- side-calculations for instance). The function
+ side-calculations or print out an intermediate result, for instance). The function
*}
ML %linenosgray{*fun inc_by_three x =
x |> (fn x => x + 1)
- |> tap (fn x => tracing (PolyML.makestring x))
+ |> tap (fn x => writeln (@{make_string} x))
|> (fn x => x + 2)*}
text {*
--- a/ProgTutorial/Intro.thy Tue Jun 14 22:09:40 2011 +0100
+++ b/ProgTutorial/Intro.thy Fri Jun 17 16:58:05 2011 +0100
@@ -28,8 +28,8 @@
Isabelle programming, and also explain ``tricks of the trade''. We also hope
the tutorial will encourage students and researchers to play with Isabelle
and implement new ideas. The source code of Isabelle can look intimidating,
- but beginners can get by with knowledge of only a small number of functions
- and a few basic coding conventions.
+ but beginners can get by with knowledge of only a handful of concepts,
+ a small number of functions and a few basic coding conventions.
The best way to get to know the ML-level of Isabelle is by experimenting
@@ -51,7 +51,11 @@
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}.
+ \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.
*}
section {* Existing Documentation *}
@@ -80,9 +84,12 @@
\begin{description}
\item[The Isabelle sources.] They are the ultimate reference for how
things really work. Therefore you should not hesitate to look at the
- way things are actually implemented. More importantly, 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
+ way things are actually implemented. While much of the Isabelle
+ code is uncommented, some parts have very helpful comments---particularly
+ the code about theorems and terms. Despite the lack of comments in most
+ 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{@{text "grep -R"}} is
often your best friend while programming with Isabelle.\footnote{Or
hypersearch if you work with jEdit.} To understand the sources,
@@ -148,22 +155,23 @@
section {* How To Understand Isabelle Code *}
text {*
- One of the more difficult aspects of any kind of programming is to 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 code on the fly (for example inside an
- \isacommand{ML}~@{text "\<verbopen>\<dots>\<verbclose>"} 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 code without having to recompile the whole Isabelle distribution. Such
+ One of the more difficult aspects of any kind of programming is to
+ 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
+ code on the fly (for example inside an \isacommand{ML}~@{text
+ "\<verbopen>\<dots>\<verbclose>"} 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
+ code without having to recompile the whole Isabelle distribution. Such
probes might be messages or printouts of variables (see chapter
\ref{chp:firststeps}). Although PolyML also contains a debugger, it seems
probing the code with explicit print statements is the most effective method
- for understanding what some piece of code is doing. However do not expect quick
- results with this! Depending on the size of the code you are looking at,
- you will spend the better part of a quiet afternoon with it. And there
- seems to be no better way for understanding code in Isabelle.
+ for understanding what some piece of code is doing. However do not expect
+ quick results with this! It is painful. Depending on the size of the code
+ you are looking at, you will spend the better part of a quiet afternoon with
+ it. And there seems to be no better way for understanding code in Isabelle.
*}
--- a/ProgTutorial/Tactical.thy Tue Jun 14 22:09:40 2011 +0100
+++ b/ProgTutorial/Tactical.thy Fri Jun 17 16:58:05 2011 +0100
@@ -775,20 +775,12 @@
is similar to @{ML RS}, but takes an additional number as argument. This
number makes explicit which premise should be instantiated.
- To improve readability of the theorems we shall produce below, we will use the
- function @{ML no_vars} from Section~\ref{sec:printing}, which transforms
- schematic variables into free ones. Using this function for the first @{ML
- RS}-expression above produces the more readable result:
-
- @{ML_response_fake [display,gray]
- "no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> Q"}
-
If you want to instantiate more than one premise of a theorem, you can use
the function @{ML_ind MRS in Drule}:
@{ML_response_fake [display,gray]
- "no_vars @{context} ([@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI})"
- "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> (Pa \<or> Q)"}
+ "[@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI}"
+ "\<lbrakk>?P2; ?Q1\<rbrakk> \<Longrightarrow> (?P2 \<or> ?Q2) \<and> (?P1 \<or> ?Q1)"}
If you need to instantiate lists of theorems, you can use the
functions @{ML_ind RL in Drule} and @{ML_ind MRL in Drule}. For
@@ -800,12 +792,12 @@
val list1 = [@{thm impI}, @{thm disjI2}]
val list2 = [@{thm conjI}, @{thm disjI1}]
in
- map (no_vars @{context}) (list1 RL list2)
+ list1 RL list2
end"
-"[\<lbrakk>P \<Longrightarrow> Q; Qa\<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) \<and> Qa,
- \<lbrakk>Q; Qa\<rbrakk> \<Longrightarrow> (P \<or> Q) \<and> Qa,
- (P \<Longrightarrow> Q) \<Longrightarrow> (P \<longrightarrow> Q) \<or> Qa,
- Q \<Longrightarrow> (P \<or> Q) \<or> Qa]"}
+"[\<lbrakk>?P1 \<Longrightarrow> ?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<and> ?Q,
+ \<lbrakk>?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q,
+ (?P1 \<Longrightarrow> ?Q1) \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<or> ?Q,
+ ?Q1 \<Longrightarrow> (?P1 \<or> ?Q1) \<or> ?Q]"}
\begin{readmore}
The combinators for instantiating theorems with other theorems are
Binary file progtutorial.pdf has changed