--- a/ProgTutorial/FirstSteps.thy Mon Aug 17 20:57:32 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy Tue Aug 18 01:05:56 2009 +0200
@@ -8,8 +8,8 @@
chapter {* First Steps *}
text {*
- Isabelle programming is done in ML. Just like lemmas and proofs, ML-code
- for Isabelle must be part of a theory. If you want to follow the code given in
+ Isabelle programming is done in ML. Just like lemmas and proofs, ML-code for
+ Isabelle must be part of a theory. If you want to follow the code given in
this chapter, we assume you are working inside the theory starting with
\begin{quote}
@@ -28,22 +28,22 @@
section {* Including ML-Code *}
text {*
- The easiest and quickest way to include code in a theory is
- by using the \isacommand{ML}-command. For example:
-
-\begin{isabelle}
-\begin{graybox}
-\isacommand{ML}~@{text "\<verbopen>"}\isanewline
-\hspace{5mm}@{ML "3 + 4"}\isanewline
-@{text "\<verbclose>"}\isanewline
-@{text "> 7"}\smallskip
-\end{graybox}
-\end{isabelle}
-
- 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
+ The easiest and quickest way to include code in a theory is by using the
+ \isacommand{ML}-command. For example:
+
+ \begin{isabelle}
+ \begin{graybox}
+ \isacommand{ML}~@{text "\<verbopen>"}\isanewline
+ \hspace{5mm}@{ML "3 + 4"}\isanewline
+ @{text "\<verbclose>"}\isanewline
+ @{text "> 7"}\smallskip
+ \end{graybox}
+ \end{isabelle}
+
+ 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
*}
ML %gray {*
@@ -52,16 +52,15 @@
*}
text {*
- and even those can be undone when the proof
- script is retracted. As mentioned in the Introduction, we will drop the
- \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we
- show code. The lines prefixed with @{text [quotes] ">"} are not part of the
- code, rather they indicate what the response is when the code is evaluated.
- There are also the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for
- including ML-code. The first evaluates the given code, but any effect on the
- theory, in which the code is embedded, is suppressed. The second needs to
- be used if ML-code is defined
- inside a proof. For example
+ and even those can be undone when the proof script is retracted. As
+ mentioned in the Introduction, we will drop the \isacommand{ML}~@{text
+ "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we show code. The lines
+ prefixed with @{text [quotes] ">"} are not part of the code, rather they
+ indicate what the response is when the code is evaluated. There are also
+ the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for including
+ ML-code. The first evaluates the given code, but any effect on the theory,
+ in which the code is embedded, is suppressed. The second needs to be used if
+ ML-code is defined inside a proof. For example
\begin{quote}
\begin{isabelle}
@@ -72,8 +71,8 @@
\end{isabelle}
\end{quote}
- However, both commands will only play minor roles in this tutorial (we will always
- arrange that the ML-code is defined outside of proofs, for example).
+ However, both commands will only play minor roles in this tutorial (we will
+ always arrange that the ML-code is defined outside of proofs, for example).
Once a portion of code is relatively stable, you usually want to export it
to a separate ML-file. Such files can then be included somewhere inside a
@@ -105,44 +104,44 @@
\end{tabular}
\end{quote}
- Note that no parentheses are given this time. Note also that the
- included ML-file should not contain any
- \isacommand{use} itself. Otherwise Isabelle is unable to record all
- file dependencies, which is a nuisance if you have to track down
- errors.
+ Note that no parentheses are given this time. Note also that the included
+ ML-file should not contain any \isacommand{use} itself. Otherwise Isabelle
+ is unable to record all file dependencies, which is a nuisance if you have
+ to track down errors.
*}
section {* Debugging and Printing\label{sec:printing} *}
text {*
-
- During development you might find it necessary to inspect some data
- in your code. This can be done in a ``quick-and-dirty'' fashion using
- the function @{ML [index] "writeln"}. For example
+ During development you might find it necessary to inspect some data in your
+ code. This can be done in a ``quick-and-dirty'' fashion using the function
+ @{ML [index] "writeln"}. For example
@{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""}
- will print out @{text [quotes] "any string"} inside the response buffer
- of Isabelle. This function expects a string as argument. If you develop under PolyML,
- then there is a convenient, though again ``quick-and-dirty'', method for
- converting values into strings, namely the function @{ML PolyML.makestring}:
+ will print out @{text [quotes] "any string"} inside the response buffer of
+ Isabelle. This function expects a string as argument. If you develop under
+ PolyML, then there is a convenient, though again ``quick-and-dirty'', method
+ for converting values into strings, namely the function
+ @{ML [index] makestring in PolyML}:
@{ML_response_fake [display,gray] "writeln (PolyML.makestring 1)" "\"1\""}
- However, @{ML [index] makestring in PolyML} only works if the type of what 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 [index] tracing} is more appropriate. This function writes all output into
- a separate tracing buffer. For example:
+ However, @{ML makestring in PolyML} only works if the type of what
+ 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 [index] tracing} is more appropriate. This function writes all
+ output into a separate tracing buffer. For example:
@{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
- It is also possible to redirect the ``channel'' where the string @{text "foo"} is
- printed to a separate file, e.g., to prevent ProofGeneral from choking on massive
- amounts of trace output. This redirection can be achieved with the code:
+ It is also possible to redirect the ``channel'' where the string @{text
+ "foo"} is printed to a separate file, e.g., to prevent ProofGeneral from
+ choking on massive amounts of trace output. This redirection can be achieved
+ with the code:
*}
ML{*val strip_specials =
@@ -198,7 +197,7 @@
text {*
Most often you want to inspect data of Isabelle's most basic data
- structures, namely @{ML_type term}, @{ML_type cterm} or @{ML_type
+ structures, namely @{ML_type term}, @{ML_type cterm} and @{ML_type
thm}. Isabelle contains elaborate pretty-printing functions for printing
them (see Section \ref{sec:pretty}), but for quick-and-dirty solutions they
are a bit unwieldy. One way to transform a term into a string is to use the
@@ -270,8 +269,8 @@
In order to improve the readability of theorems we convert these schematic
variables into free variables using the function @{ML [index] import in
- Variable}. This is similar to the theorem attribute @{text "[no_vars]"} from
- Isabelle's user-level.
+ Variable}. This is similar to statements like @{text "conjI[no_vars]"}
+ from Isabelle's user-level.
*}
ML{*fun no_vars ctxt thm =
@@ -524,9 +523,9 @@
These two functions can be used to avoid explicit @{text "lets"} for
intermediate values in functions that return pairs. Suppose for example you
want to separate a list of integers into two lists according to a
- treshold. For example if the treshold is @{ML "5"}, the list @{ML
- "[1,6,2,5,3,4]"} should be separated to @{ML "([1,2,3,4], [6,5])"}. This
- function can be implemented as
+ treshold. If the treshold is @{ML "5"}, the list @{ML "[1,6,2,5,3,4]"}
+ should be separated to @{ML "([1,2,3,4], [6,5])"}. This function can be
+ implemented as
*}
ML{*fun separate i [] = ([], [])
@@ -619,7 +618,7 @@
text {*
When using combinators for writing function in waterfall fashion, it is
- sometimes necessary to do some ``plumbing'' for fitting functions
+ sometimes necessary to do some ``plumbing'' in order to fit functions
together. We have already seen such plumbing in the function @{ML
apply_fresh_args}, where @{ML curry} is needed for making the function @{ML
list_comb} that works over pairs to fit with the combinator @{ML "|>"}. Such