# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259343524 -3600
# Node ID 1f2c8be84be7fd31aaff32bd984cea4933d514d6
# Parent  2b64936f8fab293fdd0c5ad3802639c5d36ec751# Parent  dcfe009c98aa7da00d1520d18d7b228a282ea7d0
Merge

diff -r dcfe009c98aa -r 1f2c8be84be7 LFex.thy
--- a/LFex.thy	Fri Nov 27 13:59:52 2009 +0100
+++ b/LFex.thy	Fri Nov 27 18:38:44 2009 +0100
@@ -313,7 +313,109 @@
 ML_prf {* val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot *}
 apply (tactic {* simp_tac (HOL_ss addsimps reps_same) 1 *})
 apply (tactic {* lambda_prs_tac @{context} quot 1 *})
+ML_prf {*
+val rrr1 = ref @{cterm "0"}
+val rrr2 = ref @{cterm "0"}
+val rrrt = ref @{thm refl}
+*}
 
+ML_prf {*
+fun lambda_prs_conv1 ctxt quot_thms ctrm =
+  case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) =>
+  let
+    val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1);
+    val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2);
+    val thy = ProofContext.theory_of ctxt;
+    val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]
+    val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d];
+    val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
+    val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS};
+    val tac =
+      (compose_tac (false, lpi, 2)) THEN_ALL_NEW
+      (quotient_tac quot_thms);
+    val gc = Drule.strip_imp_concl (cprop_of lpi);
+    val t = Goal.prove_internal [] gc (fn _ => tac 1)
+    val te = @{thm eq_reflection} OF [t]
+    val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
+    val tl = Thm.lhs_of ts;
+    val _ = rrrt := ts;
+    val _ = rrr1 := ctrm;
+    val _ = rrr2 := tl;
+(*    val insts = matching_prs (ProofContext.theory_of ctxt) (term_of tl) (term_of ctrm);
+    val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts);
+    val _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)
+  in
+    Conv.all_conv ctrm
+(*    Conv.rewr_conv ti ctrm *)
+  end
+(* TODO: We can add a proper error message... *)
+  handle Bind => Conv.all_conv ctrm
+
+*}
+
+(* quot stands for the QUOTIENT theorems: *) 
+(* could be potentially all of them       *)
+ML_prf {*
+fun lambda_prs_conv ctxt quot ctrm =
+  case (term_of ctrm) of
+    (Const (@{const_name "fun_map"}, _) $ _ $ _) $ (Abs _) =>
+      (Conv.arg_conv (Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt)
+      then_conv (lambda_prs_conv1 ctxt quot)) ctrm
+  | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm
+  | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm
+  | _ => Conv.all_conv ctrm
+*}
+
+ML_prf {*
+fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) =>
+  CONVERSION
+    (Conv.params_conv ~1 (fn ctxt =>
+       (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv
+          Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)
+*}
+apply (tactic {* lambda_prs_tac @{context} quot 1 *})
+ML_prf {* !rrr1 *}
+ML_prf {* val rrr1' = @{cterm "((ABS_KIND ---> ABS_KIND ---> Fun.id) ---> Fun.id)
+     (\<lambda>P1\<Colon>kind \<Rightarrow> kind \<Rightarrow> bool.
+         All (((ABS_TY ---> ABS_TY ---> Fun.id) ---> Fun.id)
+               (\<lambda>P2\<Colon>ty \<Rightarrow> ty \<Rightarrow> bool.
+                   \<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.
+                      (REP_KIND ---> REP_KIND ---> Fun.id) P1 TYP TYP \<longrightarrow>
+                      (\<forall>a\<Colon>TY. (REP_TY ---> REP_TY ---> Fun.id) P2 a a \<longrightarrow>
+                              (\<forall>x\<Colon>KIND.
+                                  (REP_KIND ---> REP_KIND ---> Fun.id) P1 x x \<longrightarrow>
+                                  (\<forall>xa\<Colon>name. (REP_KIND ---> REP_KIND ---> Fun.id) P1 (KPI a xa x) (KPI a xa x)))) \<longrightarrow>
+                      (\<forall>a\<Colon>TY. (REP_TY ---> REP_TY ---> Fun.id) P2 a a \<longrightarrow>
+                              (\<forall>(x\<Colon>name) (x'\<Colon>name) xa\<Colon>KIND.
+                                  (REP_KIND ---> REP_KIND ---> Fun.id) P1 ([(x, x')] \<bullet> xa) ([(x, x')] \<bullet> xa) \<longrightarrow>
+                                  x \<notin> FV_ty a \<longrightarrow>
+                                  x \<notin> FV_kind xa - {x'} \<longrightarrow>
+                                  (REP_KIND ---> REP_KIND ---> Fun.id) P1 (KPI a x ([(x, x')] \<bullet> xa)) (KPI a x' xa))) \<longrightarrow>
+                      (b = c \<longrightarrow> (REP_KIND ---> REP_KIND ---> Fun.id) P1 c c) \<and>
+                      (d = e \<longrightarrow> (REP_TY ---> REP_TY ---> Fun.id) P2 e e) \<and> (f = g \<longrightarrow> a g g))))"} *}
+ML_prf {* (!rrrt); rrr1'; (!rrr1) *}
+
+ML_prf {*
+fun make_inst lhs t =
+  let
+    val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
+    val _ $ (Abs (_, _, g)) = t;
+    fun mk_abs i t =
+      if incr_boundvars i u aconv t then Bound i
+      else (case t of
+        t1 $ t2 => mk_abs i t1 $ mk_abs i t2
+      | Abs (s, T, t') => Abs (s, T, mk_abs (i+1) t')
+      | Bound j => if i = j then error "make_inst" else t
+      | _ => t);
+  in (f, Abs ("x", T, mk_abs 0 g)) end;
+*}
+
+ML_prf {* cterm_of @{theory} (snd (make_inst (term_of (!rrr2)) (term_of (!rrr1)))) *}
+ML_prf {* val betaeta = Conv.fconv_rule Drule.beta_eta_conversion *}
+ML_prf {* val rr = betaeta (Drule.instantiate' [] [SOME it] (!rrrt)) *}
+ML_prf {* (term_of (Thm.lhs_of rr)) aconv (term_of (!rrr1)) *}
+ML_prf {* matching_prs @{theory} (term_of (!rrr2)) (term_of (rrr1')) *}
+ML_prf {* matching_prs @{theory} (term_of (!rrr2)) (term_of (!rrr1)) *}
 
 apply (tactic {* clean_tac @{context}  defs aps 1 *})
 ML_prf {*  *}