--- 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}, 

--- a/ProgTutorial/Intro.thy	Mon Jun 20 13:59:58 2011 +0100
+++ b/ProgTutorial/Intro.thy	Tue Jun 21 12:53:16 2011 +0100
@@ -252,7 +252,8 @@
   \ref{chp:package} describing this package and has been helpful \emph{beyond
   measure} with answering questions about Isabelle.
 
-  \item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}.
+  \item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}
+  and exercise \ref{fun:killqnt}.
 
   \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, 
   \ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion} 

--- a/ProgTutorial/Solutions.thy	Mon Jun 20 13:59:58 2011 +0100
+++ b/ProgTutorial/Solutions.thy	Tue Jun 21 12:53:16 2011 +0100
@@ -35,6 +35,43 @@
 ML{*fun make_sum t1 t2 =
   HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *}
 
+text {* \solution{fun:killqnt} *}
+
+ML %linenosgray{*val quantifiers = [@{const_name All}, @{const_name Ex}]
+
+fun kill_trivial_quantifiers trm =
+let
+  fun aux t =
+    case t of
+      Const (s1, T1) $ Abs (x, T2, t2) =>
+        if member (op =) quantifiers s1 andalso not (loose_bvar1 (t2, 0)) 
+        then incr_boundvars ~1 (aux t2)
+        else Const (s1, T1) $ Abs (x, T2, aux t2)
+    | t1 $ t2 => aux t1 $ aux t2
+    | Abs (s, T, t') => Abs (s, T, aux t')
+    | _ => t
+in 
+  aux trm
+end*}
+
+text {*
+  In line 7 we traverse the term, by first checking whether a term is an
+  application of a constant with an abstraction. If the constant stands for
+  a listed quantifier (see Line 1) and the bound variable does not occur
+  as a loose bound variable in the body, then we delete the quantifier. 
+  For this we have to increase all other dangling de Bruijn indices by
+  @{text "-1"} to account for the deleted quantifier. An example is 
+  as follows:
+
+  @{ML_response_fake [display,gray]
+  "@{prop \"\<forall>x y z. P x = P z\"}
+  |> kill_trivial_quantifiers
+  |> pretty_term @{context} 
+  |> pwriteln"
+  "\<forall>x z. P x = P z"}
+*}
+
+
 
 text {* \solution{fun:makelist} *}
 

Binary file progtutorial.pdf has changed