--- a/LFex.thy	Fri Dec 04 15:20:06 2009 +0100
+++ b/LFex.thy	Fri Dec 04 15:25:26 2009 +0100
@@ -67,18 +67,18 @@
   apply(auto intro: akind_aty_atrm.intros)
   done
 
-lemma alpha_EQUIVs:
-  shows "EQUIV akind"
-  and   "EQUIV aty"
-  and   "EQUIV atrm"
+lemma alpha_equivps:
+  shows "equivp akind"
+  and   "equivp aty"
+  and   "equivp atrm"
 sorry
 
 quotient KIND = kind / akind
-  by (rule alpha_EQUIVs)
+  by (rule alpha_equivps)
 
 quotient TY = ty / aty
    and   TRM = trm / atrm
-  by (auto intro: alpha_EQUIVs)
+  by (auto intro: alpha_equivps)
 
 print_quotients
 
@@ -217,10 +217,10 @@
 thm kind_ty_trm.induct
 
 ML {*
-  val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM}
-  val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs}
-  (*val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs}*)
-  val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot
+  val quot = @{thms Quotient_KIND Quotient_TY Quotient_TRM}
+  val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) @{thms alpha_equivps}
+  (*val trans2 = map (fn x => @{thm EQUALS_PRS} OF [x]) quot*)
+  val reps_same = map (fn x => @{thm Quotient_REL_REP} OF [x]) quot
   val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
 *}
 
@@ -258,8 +258,8 @@
          ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"
 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11
 apply - 
-apply(tactic {* lift_tac @{context} @{thm akind_aty_atrm.induct} @{thms alpha_EQUIVs} 1 *})
-(*apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
+apply(tactic {* lift_tac @{context} @{thm akind_aty_atrm.induct} @{thms alpha_equivps} 1 *})
+(*apply(tactic {* regularize_tac @{context} @{thms alpha_equivps} 1 *})
 apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})
 apply(tactic {* clean_tac @{context} 1 *})
 *)
@@ -268,7 +268,7 @@
 Profiling:
 ML_prf {* fun ith i =  (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *}
 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *}
-ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_EQUIVs} 1) (ith 1)) *}
+ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_equivps} 1) (ith 1)) *}
 ML_prf {* PolyML.profiling 1 *}
 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *}
 *)
@@ -298,7 +298,7 @@
   \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2);
   \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk>
   \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm"
-apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} @{thms alpha_EQUIVs} 1 *})
+apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} @{thms alpha_equivps} 1 *})
 done
 
 print_quotients

--- a/LamEx.thy	Fri Dec 04 15:20:06 2009 +0100
+++ b/LamEx.thy	Fri Dec 04 15:25:26 2009 +0100
@@ -46,12 +46,12 @@
   apply(simp)
   done
 
-lemma alpha_EQUIV:
-  shows "EQUIV alpha"
+lemma alpha_equivp:
+  shows "equivp alpha"
 sorry
 
 quotient lam = rlam / alpha
-  apply(rule alpha_EQUIV)
+  apply(rule alpha_equivp)
   done
 
 print_quotients
@@ -281,13 +281,13 @@
 lemma "option_map id = id"
 sorry
 
-lemma OPT_QUOTIENT:
-  assumes q: "QUOTIENT R Abs Rep"
-  shows "QUOTIENT (option_rel R) (option_map Abs) (option_map Rep)"
-  apply (unfold QUOTIENT_def)
+lemma option_Quotient:
+  assumes q: "Quotient R Abs Rep"
+  shows "Quotient (option_rel R) (option_map Abs) (option_map Rep)"
+  apply (unfold Quotient_def)
   apply (auto)
   using q
-  apply (unfold QUOTIENT_def)
+  apply (unfold Quotient_def)
   apply (case_tac "a :: 'b noption")
   apply (simp)
   apply (simp)
@@ -297,46 +297,3 @@
   (* 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_lift:
-  "\<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} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (simp only: perm_prs)
-prefer 2
-apply (tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-prefer 3
-apply (tactic {* clean_tac @{context} 1 *})
-apply (simp only: perm_prs)
-(*apply (tactic {* regularize_tac @{context} 1 *})*)
-sorry
-