--- a/ProgTutorial/Essential.thy	Mon Jun 20 13:59:58 2011 +0100
+++ b/ProgTutorial/Essential.thy	Tue Jun 21 12:53:16 2011 +0100
@@ -73,6 +73,32 @@
   only as ``comments''.  Application in Isabelle is realised with the
   term-constructor @{ML $}.
 
+  Be careful if you pretty-print terms. Consider pretty-printing the abstraction
+  term shown above:
+
+  @{ML_response_fake [display, gray]
+"@{term \"\<lambda>x y. x y\"}
+  |> pretty_term @{context}
+  |> pwriteln"
+  "\<lambda>x. x"}
+
+  This is one common source for puzzlement in Isabelle, which has 
+  tacitly eta-contracted the output. You obtain a similar result 
+  with beta-redexes
+
+  @{ML_response_fake [display, gray]
+"@{term \"(\<lambda>x y. x) 1 2\"}
+  |> pretty_term @{context}
+  |> pwriteln"
+  "1"}
+
+  There is a configuration value to switch off the tacit eta-contraction (see
+  \ref{sec:printing}), but none for beta-contraction. So in certain cases you
+  might have to inspect the internal representation of a term, instead of
+  pretty printing it. Because of the alluded puzzlement that might arise from
+  this feature of Isabelle, it is certainly an acrane fact that you should
+  keep in mind about pretty-printing terms.
+
   Isabelle makes a distinction between \emph{free} variables (term-constructor
   @{ML Free} and written on the user level in blue colour) and
   \emph{schematic} variables (term-constructor @{ML Var} and written with a
@@ -189,7 +215,6 @@
   @{ML_response [display, gray]
   "@{typ \"bool\"}"
   "bool"}
-
   which is the pretty printed version of @{text "bool"}. However, in PolyML
   (version @{text "\<ge>"}5.3) it is easy to install your own pretty printer. With the
   function below we mimic the behaviour of the usual pretty printer for
@@ -393,7 +418,7 @@
 
   Similarly the function @{ML_ind subst_bounds in Term}, 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.
+  function that strips off the outermost forall quantifiers in a term.
 *}
 
 ML{*fun strip_alls t =
@@ -401,7 +426,7 @@
   fun aux (x, T, t) = strip_alls t |>> cons (Free (x, T))
 in
   case t of
-    Const ("All", _) $ Abs body => aux body
+    Const (@{const_name All}, _) $ Abs body => aux body
   | _ => ([], t)
 end*}
 
@@ -414,9 +439,20 @@
 "([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")],
   Const (\"op =\", \<dots>) $ Bound 1 $ Bound 0)"}
 
-  After calling @{ML strip_alls}, you obtain a term with lose bound variables. With
-  the function @{ML subst_bounds}, you can replace these lose @{ML_ind 
-  Bound in Term}s with the stripped off variables.
+  Note that we produced in the body two dangling de Bruijn indices. 
+  Later on we will also use the inverse function that
+  builds the quantification from a body and a list of (free) variables.
+*}
+  
+ML{*fun build_alls ([], t) = t
+  | build_alls (Free (x, T) :: vs, t) = 
+      Const (@{const_name "All"}, (T --> @{typ bool}) --> @{typ bool}) 
+        $ Abs (x, T, build_alls (vs, t))*}
+
+text {*
+  As said above, after calling @{ML strip_alls}, you obtain a term with loose
+  bound variables. With the function @{ML subst_bounds}, you can replace these
+  loose @{ML_ind Bound in Term}s with the stripped off variables.
 
   @{ML_response_fake [display, gray, linenos]
   "let
@@ -437,7 +473,7 @@
   substitute just a variable with the name recorded in an abstraction. This
   name is by no means unique. If clashes need to be avoided, then we should
   use the function @{ML_ind dest_abs in Term}, which returns the body where
-  the lose de Bruijn index is replaced by a unique free variable. For example
+  the loose de Bruijn index is replaced by a unique free variable. For example
 
 
   @{ML_response_fake [display,gray]
@@ -448,6 +484,39 @@
 end"
   "(\"xa\", Free (\"xa\", \"Nat.nat \<Rightarrow> bool\") $ Free (\"x\", \"Nat.nat\"))"}
 
+  Sometimes it is necessary to manipulate de Bruijn indices in terms directly.
+  There are many functions to do this. We describe only two. The first,
+  @{ML_ind incr_boundvars in Term}, increases by an integer the indices 
+  of the loose bound variables in a term. In the code below
+
+@{ML_response_fake [display,gray]
+"@{term \"\<forall>x y z u. z = u\"}
+  |> strip_alls
+  ||> incr_boundvars 2
+  |> build_alls
+  |> pretty_term @{context}
+  |> pwriteln"
+  "\<forall>x y z u. x = y"}
+
+  we first strip off the forall-quantified variables (thus creating two loose
+  bound variables in the body); then we increase the indices of the loose
+  bound variables by @{ML 2} and finally re-quantify the variables. As a
+  result of @{ML incr_boundvars}, we obtain now a term that has the equation
+  between the first two quantified variables.
+
+  The second function, @{ML_ind loose_bvar1 in Text}, tests whether a term
+  contains a loose bound of a certain index. For example
+
+  @{ML_response_fake [gray,display]
+"let
+  val body = snd (strip_alls @{term \"\<forall>x y. x = (y::bool)\"})
+in
+  [loose_bvar1 (body, 0),
+   loose_bvar1 (body, 1),
+   loose_bvar1 (body, 2)]
+end"
+  "[true, true, false]"}
+
   There are also many convenient functions that construct specific HOL-terms
   in the structure @{ML_struct HOLogic}. For example @{ML_ind mk_eq in
   HOLogic} constructs an equality out of two terms.  The types needed in this
@@ -632,6 +701,14 @@
   number representing their sum.
   \end{exercise}
 
+  \begin{exercise}\label{fun:killqnt}
+  Write a function that removes trivial forall and exists quantifiers that do not
+  quantify over any variables.  For example the term @{term "\<forall>x y z. P x = P
+  z"} should be transformed to @{term "\<forall>x z. P x = P z"}, deleting the
+  quantification @{term "y"}. Hint: use the functions @{ML incr_boundvars}
+  and @{ML loose_bvar1}.
+  \end{exercise}
+
   \begin{exercise}\label{fun:makelist}
   Write a function that takes an integer @{text i} and
   produces an Isabelle integer list from @{text 1} upto @{text i},