2209   Both definitions define the same function. Indeed, the

  2209   Both definitions define the same function, although the theorems @{thm

  2210   function @{ML_ind abs_def in Drule} can automatically

  2210   [source] id1_def} and @{thm [source] id2_def} are different. However it is

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

  2211   easy to transform one theorem into the other. The function @{ML_ind abs_def

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

  2212   in Drule} can automatically transform theorem @{thm [source] id1_def}

  2213   into @{thm [source] id2_def} by abstracting all variables on the 

  2214   left-hand side in the right-hand side.

  2218   There is however no function inIsabelle that transforms 

  2220   Unfortunately, Isabelle has no build-in function that transforms the

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

  2221   theorems in the other direction. We can conveniently implement one using

  2220   using conversions. The feature of conversions we are

  2222   conversions. The feature of conversions we are using is that if we apply a

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

  2223   @{ML_type cterm} to a conversion we obtain a meta-equality theorem (recall

  2222   conversion we obtain a meta-equality theorem. The

  2224   that the type of conversions is an abbreviation for 

  2223   code of the transformation is below.

  2225   @{ML_type "cterm -> thm"}). The code of the transformation is below.

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

  2239     | get_conv (_::xs) = Conv.fun_conv (get_conv xs)

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

  2249   abstraction. We compute the possibly empty list of abstracted variables in

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

  2250   Line 4 using the function @{ML_ind strip_abs_vars}. For this we have to

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

  2251   transform the @{ML_type cterm} into a @{ML_type term}. In Line 5 we

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

  2252   importing these variables into the context @{ML_text ctxt'}, in order to

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

  2253   export them again in Line 15.  In Line 8 we certify the list of variables,

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

  2254   which in turn we apply to the @{ML_text lhs} of the definition using the

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

  2255   function @{ML_ind list_comb in Drule}. In Line 11 and 12 we generate the

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

  2256   conversion according to the length of the list of (abstracted) variables. If

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

  2257   there are none, then we just return the conversion corresponding to the

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

  2258   original definition. If there are variables, then we have to prefix this

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

  2259   conversion with @{ML_ind fun_conv in Conv}. Now in Line 14 we only have to

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

  2260   apply the new left-hand side to the generated conversion and obtain the the

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

  2261   theorem we want to construct. As mentioned above, in Line 15 we only have to

  2260   for the theorem.  For example

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

  2261 

  2263   the theorem.  An example is as follows.