--- a/ProgTutorial/FirstSteps.thy Thu Aug 13 21:32:10 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy Sun Aug 16 21:54:47 2009 +0200
@@ -194,11 +194,13 @@
*)
text {*
- Most often you want to inspect data of type @{ML_type term}, @{ML_type cterm}
- or @{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 far too unwieldy. One way to transform
- a term into a string is to use the function @{ML [index] string_of_term in Syntax}.
+ Most often you want to inspect data of Isabelle's most basic datastructures,
+ namely @{ML_type term}, @{ML_type cterm} or @{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 far too
+ unwieldy. One way to transform a term into a string is to use the function
+ @{ML [index] string_of_term in Syntax}.
+
@{ML_response_fake [display,gray]
"Syntax.string_of_term @{context} @{term \"1::nat\"}"
@@ -206,17 +208,23 @@
This produces a string with some additional information encoded in it. The string
can be properly printed by using either the function @{ML [index] writeln} or
- @{ML [index] tracing}.
+ @{ML [index] tracing}:
@{ML_response_fake [display,gray]
"writeln (Syntax.string_of_term @{context} @{term \"1::nat\"})"
"\"1\""}
+ or
+
+ @{ML_response_fake [display,gray]
+ "tracing (Syntax.string_of_term @{context} @{term \"1::nat\"})"
+ "\"1\""}
+
A @{ML_type cterm} can be transformed into a string by the following function.
*}
ML{*fun string_of_cterm ctxt t =
- Syntax.string_of_term ctxt (term_of t)*}
+ Syntax.string_of_term ctxt (term_of t)*}
text {*
In this example the function @{ML [index] term_of} extracts the @{ML_type term} from
@@ -225,7 +233,7 @@
*}
ML{*fun string_of_cterms ctxt ts =
- commas (map (string_of_cterm ctxt) ts)*}
+ commas (map (string_of_cterm ctxt) ts)*}
text {*
The easiest way to get the string of a theorem is to transform it
@@ -245,7 +253,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}.
+ function @{ML [index] import in Variable}. This is similar
+ to the attribute @{text "[no_vars]"} from Isabelle's user-level.
*}
ML{*fun no_vars ctxt thm =
@@ -495,6 +504,39 @@
ML{*fun (x, y) ||> f = (x, f y)*}
text {*
+ 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])"}. You
+ can implement this function more concisely as
+*}
+
+ML{*fun separate i [] = ([], [])
+ | separate i (x::xs) =
+ let
+ val (los, grs) = separate i xs
+ in
+ if i <= x then (los, x::grs) else (x::los, grs)
+ end*}
+
+text {*
+ where however the return value of the recursive
+ call is bound explicitly to the pair @{ML "(los, grs)" for los grs}.
+ This function can equally be written as
+*}
+
+ML{*fun separate i [] = ([], [])
+ | separate i (x::xs) =
+ if i <= x
+ then separate i xs ||> cons x
+ else separate i xs |>> cons x*}
+
+text {*
+ where no explicit @{text "let"} is needed. While in this example the gain is
+ only small, in more complicated situations the benefit of avoiding @{text "lets"}
+ can be substantial.
+
With the combinator @{ML [index] "|->"} you can re-combine the elements from a pair.
This combinator is defined as
*}
@@ -569,6 +611,8 @@
\end{readmore}
(FIXME: say something about calling conventions)
+
+ (FIXME: say something about singleton)
*}
@@ -685,7 +729,7 @@
code also difficult to read. In the next section we will see how the (build in)
antiquotation @{text "@{term \<dots>}"} can be used to construct terms.
A restriction of this antiquotation is that it does not allow you to
- use schematic variables. If you want an antiquotation that does not
+ use schematic variables. If you want to have an antiquotation that does not
have this restriction, you can implement your own using the
function @{ML [index] ML_Antiquote.inline}. The code is as follows.
*}
@@ -698,11 +742,11 @@
|> ML_Syntax.atomic))*}
text {*
- We call the new antiquotation @{text "term_pat"} (Line 1); the parser in Line
- 2 provides us with a context and a string; this string is transformed into a
- term using the function @{ML [index] read_term_pattern in ProofContext} (Line 4);
- the next two lines print the term so that the ML-system can understand
- them. An example of this antiquotation is as follows.
+ The parser in Line 2 provides us with a context and a string; this string is
+ transformed into a term using the function @{ML [index] read_term_pattern in
+ ProofContext} (Line 4); the next two lines print the term so that the
+ ML-system can understand them. An example of this antiquotation is as
+ follows.
@{ML_response_fake [display,gray]
"@{term_pat \"Suc (?x::nat)\"}"
@@ -774,10 +818,12 @@
@{ML $}.
- Isabelle makes a distinction between \emph{free} variables (term-constructor @{ML Free})
- and variables (term-constructor @{ML Var}). The latter correspond to the schematic
- variables that when printed show up with a question mark in front of them. Consider
- the following two examples
+ Isabelle makes a distinction between \emph{free} variables (term-constructor
+ @{ML Free} and written in blue colour) and \emph{schematic} variables
+ (term-constructor @{ML Var} and written with a leading question mark). The
+ latter correspond to the schematic variables that when printed show up with
+ a question mark in front of them. Consider the following two examples
+
@{ML_response_fake [display, gray]
"let
@@ -986,10 +1032,10 @@
of Church-style typing, where variables with the same name still differ, if they
have different type.
- There is also the function @{ML [index] subst_free} with which terms can
- be replaced by other terms. For example below, we will replace in
- @{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0 x"}
- the subterm @{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0"} by @{term y}, and @{term x} by @{term True}.
+ There is also the function @{ML [index] subst_free} with which terms can be
+ replaced by other terms. For example below, we will replace in @{term
+ "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0 x"} the subterm @{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0"} by
+ @{term y}, and @{term x} by @{term True}.
@{ML_response_fake [display,gray]
"let
@@ -1013,6 +1059,48 @@
end"
"Free (\"x\", \"nat\")"}
+ Similarly the function @{ML [index] subst_bounds}, replaces lose bound
+ variables with terms. To see how this function works, let us implement a
+ function that strips off the outermost quantifiers in a term.
+*}
+
+ML {*
+subst_bounds ([Free ("x", @{typ nat}), Free ("y", @{typ bool})],
+ (Bound 1 $ Bound 0))
+*}
+
+
+ML{*fun strip_alls (Const ("All", _) $ Abs (n, T, t)) =
+ strip_alls t |>> cons (Free (n, T))
+ | strip_alls t = ([], t) *}
+
+text {*
+ The function returns a pair consisting of the stripped off variables and
+ the body of the universal quantifications. For example
+
+ @{ML_response_fake [display, gray]
+ "strip_alls @{term \"\<forall>x y. x = (y::bool)\"}"
+"([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")],
+ Const (\"op =\", \<dots>) $ Bound 1 $ Bound 0)"}
+
+ With the function @{ML subst_bounds}, you can replace the lose
+ @{ML [index] Bound}s with the stripped off variables.
+
+ @{ML_response_fake [display, gray, linenos]
+ "let
+ val (vrs, trm) = strip_alls @{term \"\<forall>x y. x = (y::bool)\"}
+in
+ subst_bounds (rev vrs, trm)
+ |> Syntax.string_of_term @{context}
+ |> tracing
+end"
+ "x = y"}
+
+ Note that in Line 4 we had to reverse the list of variables that @{ML strip_alls}
+ returned. The reason is that the head of the list the function @{ML subst_bounds}
+ takes is the replacement for @{ML "Bound 0"}, the next element for @{ML "Bound 1"}
+ and so on.
+
There are many convenient functions that construct specific HOL-terms. For
example @{ML [index] mk_eq in HOLogic} constructs an equality out of two terms.
The types needed in this equality are calculated from the type of the