229 ML_prf {*

   229 (*apply(tactic {* clean_tac @{context} quot defs aps 1 *}) *)

   230 fun make_inst lhs t =

   231   let

   232     val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;

   233     val _ $ (Abs (_, _, g)) = t;

   234     fun mk_abs i t =

   235       if incr_boundvars i u aconv t then Bound i

   236       else (case t of

   237         t1 $ t2 => mk_abs i t1 $ mk_abs i t2

   238       | Abs (s, T, t') => Abs (s, T, mk_abs (i+1) t')

   239       | Bound j => if i = j then error "make_inst" else t

   240       | _ => t);

   241   in (f, Abs ("x", T, mk_abs 0 g)) end;

   242 *}

   243 

   244 ML_prf {*

   245 fun lambda_prs_conv1 ctxt quot_thms ctrm =

   246   case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) =>

   247   let

   248     val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1);

   249     val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2);

   250     val thy = ProofContext.theory_of ctxt;

   251     val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]

   252     val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d];

   253     val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]

   254     val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS};

   255     val tac =

   256       (compose_tac (false, lpi, 2)) THEN_ALL_NEW

   257       (quotient_tac quot_thms);

   258     val gc = Drule.strip_imp_concl (cprop_of lpi);

   259     val t = Goal.prove_internal [] gc (fn _ => tac 1)

   260     val te = @{thm eq_reflection} OF [t]

   261     val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te

   262     val tl = Thm.lhs_of ts;

   263     val (insp, inst) = make_inst (term_of tl) (term_of ctrm);

   264     val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts;

   265 (*    val _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)

   266   in

   267 (*    Conv.all_conv ctrm*)

   268     Conv.rewr_conv ti ctrm

   269   end

   270 (* TODO: We can add a proper error message... *)

   271   handle Bind => Conv.all_conv ctrm

   272 

   273 *}

   274 

   275 (* quot stands for the QUOTIENT theorems: *) 

   276 (* could be potentially all of them       *)

   277 ML_prf {*

   278 fun lambda_prs_conv ctxt quot ctrm =

   279   case (term_of ctrm) of

   280     (Const (@{const_name "fun_map"}, _) $ _ $ _) $ (Abs _) =>

   281       (Conv.arg_conv (Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt)

   282       then_conv (lambda_prs_conv1 ctxt quot)) ctrm

   283   | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm

   284   | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm

   285   | _ => Conv.all_conv ctrm

   286 *}

   287 

   288 ML_prf {*

   289 fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) =>

   290   CONVERSION

   291     (Conv.params_conv ~1 (fn ctxt =>

   292        (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv

   293           Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)

   294 *}