316 

   316 ML_prf {*

   317 val rrr1 = ref @{cterm "0"}

   318 val rrr2 = ref @{cterm "0"}

   319 val rrrt = ref @{thm refl}

   320 *}

   321 

   322 ML_prf {*

   323 fun lambda_prs_conv1 ctxt quot_thms ctrm =

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

   325   let

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

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

   328     val thy = ProofContext.theory_of ctxt;

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

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

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

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

   333     val tac =

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

   335       (quotient_tac quot_thms);

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

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

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

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

   340     val tl = Thm.lhs_of ts;

   341     val _ = rrrt := ts;

   342     val _ = rrr1 := ctrm;

   343     val _ = rrr2 := tl;

   344 (*    val insts = matching_prs (ProofContext.theory_of ctxt) (term_of tl) (term_of ctrm);

   345     val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts);

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

   347   in

   348     Conv.all_conv ctrm

   349 (*    Conv.rewr_conv ti ctrm *)

   350   end

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

   352   handle Bind => Conv.all_conv ctrm

   353 

   354 *}

   355 

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

   357 (* could be potentially all of them       *)

   358 ML_prf {*

   359 fun lambda_prs_conv ctxt quot ctrm =

   360   case (term_of ctrm) of

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

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

   363       then_conv (lambda_prs_conv1 ctxt quot)) ctrm

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

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

   366   | _ => Conv.all_conv ctrm

   367 *}

   368 

   369 ML_prf {*

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

   371   CONVERSION

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

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

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

   375 *}

   376 apply (tactic {* lambda_prs_tac @{context} quot 1 *})

   377 ML_prf {* !rrr1 *}

   378 ML_prf {* val rrr1' = @{cterm "((ABS_KIND ---> ABS_KIND ---> Fun.id) ---> Fun.id)

   379      (\<lambda>P1\<Colon>kind \<Rightarrow> kind \<Rightarrow> bool.

   380          All (((ABS_TY ---> ABS_TY ---> Fun.id) ---> Fun.id)

   381                (\<lambda>P2\<Colon>ty \<Rightarrow> ty \<Rightarrow> bool.

   382                    \<forall>(a\<Colon>TRM \<Rightarrow> TRM \<Rightarrow> bool) (b\<Colon>KIND) (c\<Colon>KIND) (d\<Colon>TY) (e\<Colon>TY) (f\<Colon>TRM) g\<Colon>TRM.

   383                       (REP_KIND ---> REP_KIND ---> Fun.id) P1 TYP TYP \<longrightarrow>

   384                       (\<forall>a\<Colon>TY. (REP_TY ---> REP_TY ---> Fun.id) P2 a a \<longrightarrow>

   385                               (\<forall>x\<Colon>KIND.

   386                                   (REP_KIND ---> REP_KIND ---> Fun.id) P1 x x \<longrightarrow>

   387                                   (\<forall>xa\<Colon>name. (REP_KIND ---> REP_KIND ---> Fun.id) P1 (KPI a xa x) (KPI a xa x)))) \<longrightarrow>

   388                       (\<forall>a\<Colon>TY. (REP_TY ---> REP_TY ---> Fun.id) P2 a a \<longrightarrow>

   389                               (\<forall>(x\<Colon>name) (x'\<Colon>name) xa\<Colon>KIND.

   390                                   (REP_KIND ---> REP_KIND ---> Fun.id) P1 ([(x, x')] \<bullet> xa) ([(x, x')] \<bullet> xa) \<longrightarrow>

   391                                   x \<notin> FV_ty a \<longrightarrow>

   392                                   x \<notin> FV_kind xa - {x'} \<longrightarrow>

   393                                   (REP_KIND ---> REP_KIND ---> Fun.id) P1 (KPI a x ([(x, x')] \<bullet> xa)) (KPI a x' xa))) \<longrightarrow>

   394                       (b = c \<longrightarrow> (REP_KIND ---> REP_KIND ---> Fun.id) P1 c c) \<and>

   395                       (d = e \<longrightarrow> (REP_TY ---> REP_TY ---> Fun.id) P2 e e) \<and> (f = g \<longrightarrow> a g g))))"} *}

   396 ML_prf {* (!rrrt); rrr1'; (!rrr1) *}

   397 

   398 ML_prf {*

   399 fun make_inst lhs t =

   400   let

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

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

   403     fun mk_abs i t =

   404       if incr_boundvars i u aconv t then Bound i

   405       else (case t of

   406         t1 $ t2 => mk_abs i t1 $ mk_abs i t2

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

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

   409       | _ => t);

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

   411 *}

   412 

   413 ML_prf {* cterm_of @{theory} (snd (make_inst (term_of (!rrr2)) (term_of (!rrr1)))) *}

   414 ML_prf {* val betaeta = Conv.fconv_rule Drule.beta_eta_conversion *}

   415 ML_prf {* val rr = betaeta (Drule.instantiate' [] [SOME it] (!rrrt)) *}

   416 ML_prf {* (term_of (Thm.lhs_of rr)) aconv (term_of (!rrr1)) *}

   417 ML_prf {* matching_prs @{theory} (term_of (!rrr2)) (term_of (rrr1')) *}

   418 ML_prf {* matching_prs @{theory} (term_of (!rrr2)) (term_of (!rrr1)) *}