--- a/FSet.thy	Fri Oct 30 18:31:06 2009 +0100
+++ b/FSet.thy	Fri Oct 30 19:03:53 2009 +0100
@@ -322,28 +322,24 @@
 thm list.recs(2)
 thm list.cases
 
-
-ML {* val ind_r_a = atomize_thm @{thm m2} *}
-prove {* build_regularize_goal ind_r_a rty rel @{context}  *}
-  ML_prf {*  fun tac ctxt =
+ML {* val ind_r_a = atomize_thm @{thm list.induct} *}
+(* prove {* build_regularize_goal ind_r_a rty rel @{context}  *}
+ ML_prf {*  fun tac ctxt =
      (FIRST' [
       rtac rel_refl,
       atac,
-      (rtac @{thm  allI} THEN' dtac @{thm spec}),
+      rtac @{thm get_rid},
+      rtac @{thm get_rid2},
       (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
         [(@{thm equiv_res_forall} OF [rel_eqv]),
          (@{thm equiv_res_exists} OF [rel_eqv])]) i)),
-      MetisTools.metis_tac ctxt [],
-      rtac (@{thm eq_rr} OF [rel_refl]),
-      ((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]))
+      (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl),
+      (rtac @{thm RIGHT_RES_FORALL_REGULAR})
     ]);
  *}
-  apply (tactic {* tac @{context} 1 *}) 
-  apply (tactic {* tac @{context} 1 *}) 
-  apply (tactic {* tac @{context} 1 *}) 
-
-
-ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv @{context} *}
+  apply (atomize(full))
+  apply (tactic {* tac @{context} 1 *}) *)
+ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv rel_refl @{context} *}
 ML {*
   val rt = build_repabs_term @{context} ind_r_r consts rty qty
   val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt);

--- a/LamEx.thy	Fri Oct 30 18:31:06 2009 +0100
+++ b/LamEx.thy	Fri Oct 30 19:03:53 2009 +0100
@@ -107,7 +107,7 @@
 
 lemma fv_lam:
   shows "fv (Lam a t) = (fv t) - {a}"
-sorry 
+sorry
 
 lemma real_alpha:
   assumes "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s"
@@ -179,16 +179,20 @@
 ML {* val a2 = lift_thm_lam @{context} @{thm a1} *}
 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *}
 
+ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *}
+
 local_setup {*
   Quotient.note (@{binding "pi_var"}, pi_var) #> snd #>
   Quotient.note (@{binding "pi_app"}, pi_app) #> snd #>
   Quotient.note (@{binding "pi_lam"}, pi_lam) #> snd #>
   Quotient.note (@{binding "a1"}, a1) #> snd #>
   Quotient.note (@{binding "a2"}, a2) #> snd #>
-  Quotient.note (@{binding "a3"}, a3) #> snd
+  Quotient.note (@{binding "a3"}, a3) #> snd #>
+  Quotient.note (@{binding "alpha_cases"}, alpha_cases) #> snd
 *}
 
 thm alpha.cases
+thm alpha_cases
 
 thm rlam.inject
 thm pi_var
@@ -217,114 +221,17 @@
 
 
 
-
-lemma get_rid: "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))"
-apply (auto)
-done
-
-lemma get_rid2: "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
-apply (auto)
-done
-
 ML {* val t_a = atomize_thm @{thm alpha.cases} *}
-prove {* build_regularize_goal t_a rty rel @{context}  *}
-  ML_prf {*  fun tac ctxt =
-     (FIRST' [
-      rtac rel_refl,
-      atac,
-      rtac @{thm get_rid},
-      rtac @{thm get_rid2},
-      (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
-        [(@{thm equiv_res_forall} OF [rel_eqv]),
-         (@{thm equiv_res_exists} OF [rel_eqv])]) i)),
-      (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl)
-    ]);
- *}
-  apply (atomize(full))
-  apply (tactic {* tac @{context} 1 *})
-  apply (rule get_rid)
-  apply (rule get_rid)
-  apply (rule get_rid2)
-  apply (simp)
-  apply (rule get_rid)
-  apply (rule get_rid2)
-  apply (rule get_rid)
-  apply (rule get_rid2)
-  apply (rule impI)
-  apply (simp)
-  apply (tactic {* tac @{context} 1 *})
-  apply (rule get_rid2)
-  apply (rule impI)
-  apply (simp)
-  apply (tactic {* tac @{context} 1 *})
-  apply (simp)
-  apply (rule get_rid2)
-  apply (rule get_rid)
-  apply (rule get_rid)
-  apply (rule get_rid)
-  apply (rule get_rid2)
-  apply (rule impI)
-  apply (simp)
-  apply (tactic {* tac @{context} 1 *})
-  apply (rule get_rid)
-  apply (rule get_rid2)
-
-
-  apply (tactic {* compose_tac (false, @{thm get_rid}, 1) 1 *})
-ML_prf {*
-fun focus_compose t = Subgoal.FOCUS (fn {concl, ...} =>
-  rtac t 1)
-*}
-thm spec[of _ "x"]
-  apply (rule allI)
-  apply (drule_tac x="a2" in spec)
-  apply (rule impI)
-  apply (erule impE)
-  apply (assumption)
-  apply (rule allI)
-  apply (drule_tac x="P" in spec)
-  apply (atomize(full))
-  apply (rule allI)
-  apply (rule allI)
-  apply (rule allI)
-  apply (rule impI)
-  apply (rule get_rid2)
-
-  thm get_rid2
-  apply (tactic {* compose_tac (false, @{thm get_rid2}, 0) 1 *})
-
-  thm spec
-
-  ML_prf {* val t = snd (Subgoal.focus @{context} 1 (Isar.goal ())) *}
-ML_prf {* Seq.pull (compose_tac (false, @{thm get_rid}, 2) 1 t) *}
-
-
-  thm get_rid
-  apply (rule allI)
-  apply (drule spec)
-
-  thm spec
-  apply (tactic {* compose_tac (false, @{thm get_rid}, 1) 1 *})
-
-  apply (tactic {* tac @{context} 1 *})
-  apply (tactic {* tac @{context} 1 *})
-  apply (rule impI)
-  apply (erule impE)
-  apply (assumption)
-  apply (tactic {* tac @{context} 1 *})
-  apply (rule impI)
-  apply (erule impE)
-  apply (tactic {* tac @{context} 1 *})
-  apply (tactic {* tac @{context} 1 *})
-  apply (tactic {* tac @{context} 1 *})
-  apply (tactic {* tac @{context} 1 *})
-
 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
+ML {* val abs = findabs rty (prop_of t_a); *}
+ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *}
 ML {* val t_a = simp_allex_prs @{context} quot t_l *}
-ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym
-
+ML {* val defs_sym = add_lower_defs @{context} defs; *}
+ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_a *}
+ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *}
+ML {* ObjectLogic.rulify t_r *}
 
 
 
@@ -358,127 +265,3 @@
   (* Simp starts hanging so don't know how to continue *)
   sorry
 
-(* Not sure if it make sense or if it will be needed *)
-lemma abs_fun_rsp: "(op = ===> alpha ===> op = ===> op =) abs_fun abs_fun"
-sorry
-
-(* Should not be needed *)
-lemma eq_rsp2: "((op = ===> op =) ===> (op = ===> op =) ===> op =) op = op ="
-apply auto
-apply (rule ext)
-apply auto
-apply (rule ext)
-apply auto
-done
-
-(* Should not be needed *)
-lemma perm_rsp_eq: "(op = ===> (op = ===> op =) ===> op = ===> op =) op \<bullet> op \<bullet>"
-apply auto
-thm arg_cong2
-apply (rule_tac f="perm x" in arg_cong2)
-apply (auto)
-apply (rule ext)
-apply (auto)
-done
-
-(* Should not be needed *)
-lemma fresh_rsp_eq: "(op = ===> (op = ===> op =) ===> op =) fresh fresh"
-apply (simp add: FUN_REL.simps)
-apply (metis ext)
-done
-
-(* It is just a test, it doesn't seem true... *)
-lemma quotient_cheat: "QUOTIENT op = (option_map ABS_lam) (option_map REP_lam)"
-sorry
-
-ML {* val rsp_thms = @{thms abs_fun_rsp OPT_QUOTIENT eq_rsp2 quotient_cheat perm_rsp_eq fresh_rsp_eq} @ rsp_thms *}
-ML {* fun lift_thm_lam lthy t = lift_thm lthy qty "lam" rsp_thms defs t *}
-
-thm a3
-ML {* Toplevel.program (fn () => lift_thm_lam @{context} @{thm a3}) *}
-thm a3
-ML {* val t_u1 = eqsubst_thm @{context} @{thms abs_fresh(1)} (atomize_thm @{thm a3}) *}
-ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} t_u1 *}
-
-(* T_U *)
-
-ML {* val t_a = atomize_thm @{thm rfv_var} *}
-ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *}
-ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
-
-ML {* fun r_mk_comb_tac_lam ctxt =
-  r_mk_comb_tac ctxt rty quot rel_refl trans2 rsp_thms
-*}
-
-instance lam :: fs_name
-apply(intro_classes)
-sorry
-
-prove asdf: {* Logic.mk_implies (concl_of t_r, (@{term "Trueprop (\<forall>t\<Colon>rlam\<in>Respects
-          alpha.
-         \<forall>(a\<Colon>name) b\<Colon>name.
-            \<forall>s\<Colon>rlam\<in>Respects
-                alpha.
-               t \<approx> ([(a,
-                 b)] \<bullet> s) \<longrightarrow>
-               a = b \<or>
-               a
-               \<notin> {a\<Colon>name.
-                infinite
-                 {b\<Colon>name. Not
-                  (([(a, b)] \<bullet>
-                  s) \<approx>
-                  s)}} \<longrightarrow>
-               rLam a
-                t \<approx> rLam
-                 b s)"})) *}
-apply (tactic {* full_simp_tac ((Simplifier.context @{context} HOL_ss) addsimps
-        [(@{thm equiv_res_forall} OF [rel_eqv]),
-         (@{thm equiv_res_exists} OF [rel_eqv])]) 1 *})
-apply (rule allI)
-apply (drule_tac x="t" in spec)
-apply (rule allI)
-apply (drule_tac x="a" in spec)
-apply (rule allI)
-apply (drule_tac x="b" in spec)
-apply (rule allI)
-apply (drule_tac x="s" in spec)
-apply (rule impI)
-apply (drule_tac mp)
-apply (simp)
-apply (simp)
-apply (rule impI)
-apply (rule a3)
-apply (simp)
-apply (simp add: abs_fresh(1))
-apply (case_tac "a = b")
-apply (simp)
-apply (simp)
-apply (auto)
-apply (unfold fresh_def)
-apply (unfold supp_def)
-apply (simp)
-prefer 2
-apply (simp)
-sorry
-
-ML {* val abs = findabs rty (prop_of t_a) *}
-ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
-ML {* val t_defs_sym = add_lower_defs @{context} defs *}
-
-ML {* val t_r' = @{thm asdf} OF [t_r] *}
-ML {* val t_t = repabs @{context} t_r' consts rty qty quot rel_refl trans2 rsp_thms *}
-ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *}
-ML {* val t_a = simp_allex_prs @{context} quot t_l *}
-ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_a *}
-ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *}
-ML {* val tt = MetaSimplifier.rewrite_rule [symmetric @{thm supp_def}, symmetric @{thm fresh_def}] t_r *}
-ML {* val rr = @{thm sym} OF @{thms abs_fresh(1)} *}
-ML {* val ttt = eqsubst_thm @{context} [rr] tt *}
-ML {* ObjectLogic.rulify ttt *}
-
-lemma
-  assumes a: "a \<notin> {a\<Colon>name. infinite {b\<Colon>name. \<not> ([(a, b)] \<bullet> s) \<approx> s}}"
-  shows "a \<notin> {a\<Colon>name. infinite {b\<Colon>name. [(a, b)] \<bullet> s \<noteq> s}}"
-  using a apply simp
-  sorry (* Not true... *)

--- a/QuotMain.thy	Fri Oct 30 18:31:06 2009 +0100
+++ b/QuotMain.thy	Fri Oct 30 19:03:53 2009 +0100
@@ -517,25 +517,31 @@
        (my_reg lthy rel rty (prop_of thm)))
 *}
 
-lemma eq_rr: "(\<And>x. R x x) \<Longrightarrow> a = b \<Longrightarrow> R a b"
-by (auto)
+lemma universal_twice: "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))"
+apply (auto)
+done
+
+lemma implication_twice: "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
+apply (auto)
+done
 
 ML {*
 fun regularize thm rty rel rel_eqv rel_refl lthy =
   let
     val g = build_regularize_goal thm rty rel lthy;
     fun tac ctxt =
+      (ObjectLogic.full_atomize_tac) THEN'
      REPEAT_ALL_NEW (FIRST' [
       rtac rel_refl,
       atac,
-      (rtac @{thm  allI} THEN' dtac @{thm spec}),
+      rtac @{thm universal_twice},
+      rtac @{thm implication_twice},
       (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
         [(@{thm equiv_res_forall} OF [rel_eqv]),
          (@{thm equiv_res_exists} OF [rel_eqv])]) i)),
-      MetisTools.metis_tac ctxt [],
-      rtac (@{thm eq_rr} OF [rel_refl]),
-      ((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]))
-    ]);
+      (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl),
+      (rtac @{thm RIGHT_RES_FORALL_REGULAR})
+     ]);
     val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1);
   in
     cthm OF [thm]

--- a/QuotScript.thy	Fri Oct 30 18:31:06 2009 +0100
+++ b/QuotScript.thy	Fri Oct 30 19:03:53 2009 +0100
@@ -461,8 +461,8 @@
   done
 
 lemma RIGHT_RES_FORALL_REGULAR:
-  assumes a: "!x :: 'a. (R x --> P x --> Q x)"
-  shows "All P ==> Ball R Q"
+  assumes a: "\<And>x :: 'a. (R x \<Longrightarrow> P x \<longrightarrow> Q x)"
+  shows "All P \<longrightarrow> Ball R Q"
   using a
   apply (metis COMBC_def Collect_def Collect_mem_eq a)
   done