--- a/LamEx.thy	Wed Dec 02 17:16:44 2009 +0100
+++ b/LamEx.thy	Wed Dec 02 20:54:59 2009 +0100
@@ -299,3 +299,55 @@
   (* Simp starts hanging so don't know how to continue *)
   sorry
 
+lemma real_alpha_pre:
+  assumes a: "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s"
+  shows "rLam a t \<approx> rLam b s"
+sorry
+
+lemma perm_prs : "(id ---> option_map ABS_lam) ([b].REP_lam s) = [b].s"
+sorry
+
+lemma perm_prs2: "(id ---> option_map ABS_lam) ((id ---> option_map REP_lam) ([b].(s::lam))) = [b].s"
+sorry
+
+lemma real_alpha:
+  "\<lbrakk>t = [(a, b)] \<bullet> s; a \<sharp> [b].s\<rbrakk> \<Longrightarrow> Lam a t = Lam b s"
+apply (tactic {* procedure_tac @{context} @{thm real_alpha_pre} 1 *})
+prefer 2
+apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+apply (simp only: perm_prs)
+prefer 2
+apply (tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+prefer 3
+apply (tactic {* clean_tac @{context} [quot] defs 1 *})
+
+thm all_prs
+thm REP_ABS_RSP
+thm ball_reg_eqv_range
+
+
+thm perm_lam_def
+apply (simp only: perm_prs)
+
+apply (tactic {* regularize_tac @{context} [quot] 1 *})
+
+done
+

--- a/QuotMain.thy	Wed Dec 02 17:16:44 2009 +0100
+++ b/QuotMain.thy	Wed Dec 02 20:54:59 2009 +0100
@@ -604,16 +604,15 @@
       (let
         val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2;
         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
-        val _ = tracing (Syntax.string_of_term ctxt glc);
+(*        val _ = tracing (Syntax.string_of_term ctxt glc);*)
         val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
         val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]);
         val R1c = cterm_of thy R1;
         val thmi = Drule.instantiate' [] [SOME R1c] thm;
-(*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *)
+(*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi));*)
         val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
-        val _ = tracing "AAA";
         val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
-        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));
+(*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); *)
       in
         SOME thm2
       end
@@ -636,16 +635,15 @@
       (let
         val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2;
         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
-        val _ = tracing (Syntax.string_of_term ctxt glc);
+(*        val _ = tracing (Syntax.string_of_term ctxt glc); *)
         val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
         val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv_range} OF [eqv]]);
         val R1c = cterm_of thy R1;
         val thmi = Drule.instantiate' [] [SOME R1c] thm;
 (*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *)
         val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
-        val _ = tracing "AAA";
         val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
-        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));
+(*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));*)
       in
         SOME thm2
       end