--- a/ProgTutorial/Tactical.thy	Tue Oct 06 16:40:37 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Wed Oct 07 09:54:01 2009 +0200
@@ -2206,21 +2206,23 @@
 where "id2 \<equiv> \<lambda>x. x"
 
 text {*
-  Both definitions define the same function. Indeed, the
-  function @{ML_ind abs_def in Drule} can automatically
-  transform the theorem @{thm [source] id1_def} into
-  the theorem @{thm [source] id2_def}.
+  Both definitions define the same function, although the theorems @{thm
+  [source] id1_def} and @{thm [source] id2_def} are different. However it is
+  easy to transform one theorem into the other. The function @{ML_ind abs_def
+  in Drule} can automatically transform theorem @{thm [source] id1_def}
+  into @{thm [source] id2_def} by abstracting all variables on the 
+  left-hand side in the right-hand side.
 
   @{ML_response_fake [display,gray]
   "Drule.abs_def @{thm id1_def}"
   "id1 \<equiv> \<lambda>x. x"}
 
-  There is however no function inIsabelle that transforms 
-  the theorems in the other direction. We can implement one
-  using conversions. The feature of conversions we are
-  using is that if we apply a @{ML_type cterm} to a 
-  conversion we obtain a meta-equality theorem. The
-  code of the transformation is below.
+  Unfortunately, Isabelle has no build-in function that transforms the
+  theorems in the other direction. We can conveniently implement one using
+  conversions. The feature of conversions we are using is that if we apply a
+  @{ML_type cterm} to a conversion we obtain a meta-equality theorem (recall
+  that the type of conversions is an abbreviation for 
+  @{ML_type "cterm -> thm"}). The code of the transformation is below.
 *}
 
 ML %linenosgray{*fun unabs_def ctxt def =
@@ -2234,7 +2236,7 @@
   val new_lhs = Drule.list_comb (lhs, cxs)
 
   fun get_conv [] = Conv.rewr_conv def
-    | get_conv (x::xs) = Conv.fun_conv (get_conv xs)
+    | get_conv (_::xs) = Conv.fun_conv (get_conv xs)
 in
   get_conv xs new_lhs |>  
   singleton (ProofContext.export ctxt' ctxt)
@@ -2244,21 +2246,21 @@
   In Line 3 we destruct the meta-equality into the @{ML_type cterm}s
   corresponding to the left-hand and right-hand side of the meta-equality. The
   assumption in @{ML unabs_def} is that the right-hand side is an
-  abstraction. We compute the list of abstracted variables in Line 4 using the
-  function @{ML_ind strip_abs_vars}. For this we have to transform the
-  @{ML_type cterm} into @{ML_type term}. In Line 5 we importing these
-  variables into the context @{ML_text ctxt'}, in order to export them again
-  in Line 15.  In Line 8 we certify the list of variables, which in turn we
-  apply to the @{ML_text lhs} of the definition using the function @{ML_ind
-  list_comb in Drule}. In Line 11 and 12 generate the conversion according to
-  the length of the list of variables. If there are none, we just return the
-  conversion corresponding to the original definition. If there are variables,
-  we have to prefix this conversion with @{ML_ind fun_conv in Conv}. Now in
-  Line 14 we only have to apply the new left-hand side to the generated
-  conversion and obtain the the theorem we are after. In Line 15 we only have
-  to export the context @{ML_text ctxt'} in order to produce meta-variables
-  for the theorem.  For example
-
+  abstraction. We compute the possibly empty list of abstracted variables in
+  Line 4 using the function @{ML_ind strip_abs_vars}. For this we have to
+  transform the @{ML_type cterm} into a @{ML_type term}. In Line 5 we
+  importing these variables into the context @{ML_text ctxt'}, in order to
+  export them again in Line 15.  In Line 8 we certify the list of variables,
+  which in turn we apply to the @{ML_text lhs} of the definition using the
+  function @{ML_ind list_comb in Drule}. In Line 11 and 12 we generate the
+  conversion according to the length of the list of (abstracted) variables. If
+  there are none, then we just return the conversion corresponding to the
+  original definition. If there are variables, then we have to prefix this
+  conversion with @{ML_ind fun_conv in Conv}. Now in Line 14 we only have to
+  apply the new left-hand side to the generated conversion and obtain the the
+  theorem we want to construct. As mentioned above, in Line 15 we only have to
+  export the context @{ML_text ctxt'} in order to produce meta-variables for
+  the theorem.  An example is as follows.
 
   @{ML_response_fake [display, gray]
   "unabs_def @{context} @{thm id2_def}"

Binary file progtutorial.pdf has changed