2195   Conversions can also be helpful for constructing meta-equality theorems.

  2196   Such theorems are often definitions. As an example consider the following

  2197   two ways of defining the identity function in Isabelle. 

  2198 *}

  2199 

  2200 definition id1::"'a \<Rightarrow> 'a" 

  2201 where "id1 x \<equiv> x"

  2202 

  2203 definition id2::"'a \<Rightarrow> 'a"

  2204 where "id2 \<equiv> \<lambda>x. x"

  2205 

  2206 text {*

  2207   Both definitions define the same function. Indeed, the

  2208   function @{ML_ind abs_def in Drule} can automatically

  2209   transform the theorem @{thm [source] id1_def} into

  2210   the theorem @{thm [source] id2_def}.

  2211 

  2212   @{ML_response_fake [display,gray]

  2213   "Drule.abs_def @{thm id1_def}"

  2214   "id1 \<equiv> \<lambda>x. x"}

  2215 

  2216   There is however no function inIsabelle that transforms 

  2217   the theorems in the other direction. We can implement one

  2218   using conversions. The feature of conversions we are

  2219   using is that if we apply a @{ML_type cterm} to a 

  2220   conversion we obtain a meta-equality theorem. The

  2221   code of the transformation is below.

  2222 *}

  2223 

  2224 ML %linenosgray{*fun unabs_def ctxt def =

  2225 let

  2226   val (lhs, rhs) = Thm.dest_equals (cprop_of def)

  2227   val xs = strip_abs_vars (term_of rhs)

  2228   val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt

  2229   

  2230   val thy = ProofContext.theory_of ctxt'

  2231   val cxs = map (cterm_of thy o Free) xs

  2232   val new_lhs = Drule.list_comb (lhs, cxs)

  2233 

  2234   fun get_conv [] = Conv.rewr_conv def

  2235     | get_conv (x::xs) = Conv.fun_conv (get_conv xs)

  2236 in

  2237   get_conv xs new_lhs |>  

  2238   singleton (ProofContext.export ctxt' ctxt)

  2239 end*}

  2240 

  2241 text {*

  2242   In Line 3 we destruct the meta-equality into the @{ML_type cterm}s

  2243   corresponding to the left-hand and right-hand side of the meta-equality. The

  2244   assumption in @{ML unabs_def} is that the right-hand side is an

  2245   abstraction. We compute the list of abstracted variables in Line 4 using the

  2246   function @{ML_ind strip_abs_vars}. For this we have to transform the

  2247   @{ML_type cterm} into @{ML_type term}. In Line 5 we importing these

  2248   variables into the context @{ML_text ctxt'}, in order to export them again

  2249   in Line 15.  In Line 8 we certify the list of variables, which in turn we

  2250   apply to the @{ML_text lhs} of the definition using the function @{ML_ind

  2251   list_comb in Drule}. In Line 11 and 12 generate the conversion according to

  2252   the length of the list of variables. If there are none, we just return the

  2253   conversion corresponding to the original definition. If there are variables,

  2254   we have to prefix this conversion with @{ML_ind fun_conv in Conv}. Now in

  2255   Line 14 we only have to apply the new left-hand side to the generated

  2256   conversion and obtain the the theorem we are after. In Line 15 we only have

  2257   to export the context @{ML_text ctxt'} in order to produce meta-variables

  2258   for the theorem.  For example

  2259 

  2260 

  2261   @{ML_response_fake [display, gray]

  2262   "unabs_def @{context} @{thm id2_def}"

  2263   "id2 ?x1 \<equiv> ?x1"}

  2264 *}

  2265 

  2266 text {*