# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1254821700 -7200
# Node ID 6fba3a3e80a356477facd8082a791e5e4e68e143
# Parent  46100dc4a80839266aa874e55b51c469b058ed0d
added the function unabs_def in the conversions section

diff -r 46100dc4a808 -r 6fba3a3e80a3 ProgTutorial/Tactical.thy
--- 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, 
diff -r 46100dc4a808 -r 6fba3a3e80a3 progtutorial.pdf
Binary file progtutorial.pdf has changed