--- a/ProgTutorial/Tactical.thy	Mon Oct 05 11:45:49 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Tue Oct 06 11:35:00 2009 +0200
@@ -1873,7 +1873,6 @@
 section {* Conversions\label{sec:conversion} *}
 
 text {*
-
   Conversions are a thin layer on top of Isabelle's inference kernel, and 
   can be viewed as a controllable, bare-bone version of Isabelle's simplifier.
   One difference between conversions and the simplifier is that the former
@@ -2193,6 +2192,78 @@
   As you can see, the premises are rewritten according to @{ML if_true1_conv}, while
   the conclusion according to @{ML all_true1_conv}.
 
+  Conversions can also be helpful for constructing meta-equality theorems.
+  Such theorems are often definitions. As an example consider the following
+  two ways of defining the identity function in Isabelle. 
+*}
+
+definition id1::"'a \<Rightarrow> 'a" 
+where "id1 x \<equiv> x"
+
+definition id2::"'a \<Rightarrow> 'a"
+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}.
+
+  @{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.
+*}
+
+ML %linenosgray{*fun unabs_def ctxt def =
+let
+  val (lhs, rhs) = Thm.dest_equals (cprop_of def)
+  val xs = strip_abs_vars (term_of rhs)
+  val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt
+  
+  val thy = ProofContext.theory_of ctxt'
+  val cxs = map (cterm_of thy o Free) xs
+  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)
+in
+  get_conv xs new_lhs |>  
+  singleton (ProofContext.export ctxt' ctxt)
+end*}
+
+text {*
+  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
+
+
+  @{ML_response_fake [display, gray]
+  "unabs_def @{context} @{thm id2_def}"
+  "id2 ?x1 \<equiv> ?x1"}
+*}
+
+text {*
   To sum up this section, conversions are more general than the simplifier
   or simprocs, but you have to do more work yourself. Also conversions are
   often much less efficient than the simplifier. The advantage of conversions, 

Binary file progtutorial.pdf has changed