--- a/LFex.thy	Sat Nov 28 03:06:22 2009 +0100
+++ b/LFex.thy	Sat Nov 28 03:07:38 2009 +0100
@@ -303,20 +303,19 @@
 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
 prefer 2
 ML_prf {* val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} *}
-apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
-apply (tactic {* lambda_prs_tac @{context} quot 1 *})
-ML_prf {* val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot *}
-ML_prf {* val aps_thms = map (applic_prs @{context} absrep) aps *}
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *})
-ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *}
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *})
-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}
+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 {*
@@ -338,15 +337,15 @@
     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 _ = 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)));*)
+    val _ = rrr2 := tl;*)
+    val (insp, inst) = make_inst (term_of tl) (term_of ctrm);
+    val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts;
+(*    val _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)
   in
-    Conv.all_conv ctrm
-(*    Conv.rewr_conv ti ctrm *)
+(*    Conv.all_conv ctrm*)
+    Conv.rewr_conv ti ctrm
   end
 (* TODO: We can add a proper error message... *)
   handle Bind => Conv.all_conv ctrm
@@ -374,51 +373,36 @@
           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 {* val lower = flat (map (add_lower_defs @{context}) defs) *}
+ML_prf {* val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower *}
+ML_prf {* val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot *}
+ML_prf {* val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same *}
+apply (tactic {* simp_tac ((Simplifier.context @{context} empty_ss) addsimps (meta_reps_same @ meta_lower)) 1 *})
+thm FORALL_PRS[symmetric]
 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;
+fun allex_prs_tac lthy quot =
+  (EqSubst.eqsubst_tac lthy [1] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
+  THEN' (quotient_tac quot);
 *}
+apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
+ML_prf {* val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot *}
+ML_prf {* val aps_thms = map (applic_prs @{context} absrep) aps *}
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
+apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *})
+apply (rule refl)
 
-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 {*  *}
+
+
 print_quotients
 apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl [trans2] [] 1*})