
diff -r f4fa6540e280 -r c90f4ec30d43 ProgTutorial/FirstSteps.thy
--- 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




