--- a/Nominal/Term5n.thy	Wed Mar 17 09:57:54 2010 +0100
+++ b/Nominal/Term5n.thy	Wed Mar 17 11:11:25 2010 +0100
@@ -53,10 +53,34 @@
 build_alpha_eqvts [@{term alpha_rtrm5}, @{term alpha_rlts}, @{term alpha_rbv5}] (fn _ => alpha_eqvt_tac  @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} ctxt 1) ctxt) ctxt)) *}
 print_theorems
 
+lemma alpha5_reflp:
+"y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 x x)"
+apply (rule rtrm5_rlts.induct)
+apply (simp_all add: alpha5_inj)
+apply (rule_tac x="0::perm" in exI)
+apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm)
+done
+
+lemma alpha5_symp:
+"(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and>
+(x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>
+(alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)"
+sorry
+
+lemma alpha5_transp:
+"(a \<approx>5 b \<longrightarrow> (\<forall>c. b \<approx>5 c \<longrightarrow> a \<approx>5 c)) \<and>
+(x \<approx>l y \<longrightarrow> (\<forall>z. y \<approx>l z \<longrightarrow> x \<approx>l z)) \<and>
+(alpha_rbv5 k l \<longrightarrow> (\<forall>m. alpha_rbv5 l m \<longrightarrow> alpha_rbv5 k m))"
+sorry
+
 lemma alpha5_equivp:
   "equivp alpha_rtrm5"
   "equivp alpha_rlts"
-  sorry
+  unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
+  apply (simp_all only: alpha5_reflp)
+  apply (meson alpha5_symp alpha5_transp)
+  apply (meson alpha5_symp alpha5_transp)
+  done
 
 quotient_type
   trm5 = rtrm5 / alpha_rtrm5
@@ -96,14 +120,34 @@
   apply simp
   done
 
-lemma alpha_rbv5_rsp: "xa \<approx>l y \<Longrightarrow> xb \<approx>l ya \<Longrightarrow> alpha_rbv5 xa xb = alpha_rbv5 y ya"
+local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *}
+print_theorems
+
+lemma alpha_rbv_rsp_pre:
+  "x \<approx>l y \<Longrightarrow> \<forall>z. alpha_rbv5 x z = alpha_rbv5 y z"
   apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
-  apply (erule_tac[!] alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
-  apply (simp_all)
-  defer defer (* should follow from distinctness *)
+  apply (simp_all add: alpha_dis alpha5_inj)
+  apply clarify
+  apply (case_tac [!] z)
+  apply (simp_all add: alpha_dis alpha5_inj)
   apply clarify
-  apply (simp add: alpha5_inj)
-  sorry (* should be true? *)
+  apply auto
+  apply (meson alpha5_symp alpha5_transp)
+  apply (meson alpha5_symp alpha5_transp)
+  done
+
+lemma alpha_rbv_rsp_pre2:
+  "x \<approx>l y \<Longrightarrow> \<forall>z. alpha_rbv5 z x = alpha_rbv5 z y"
+  apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
+  apply (simp_all add: alpha_dis alpha5_inj)
+  apply clarify
+  apply (case_tac [!] z)
+  apply (simp_all add: alpha_dis alpha5_inj)
+  apply clarify
+  apply auto
+  apply (meson alpha5_symp alpha5_transp)
+  apply (meson alpha5_symp alpha5_transp)
+  done
 
 lemma [quot_respect]:
   "(alpha_rlts ===> op =) fv_rlts fv_rlts"
@@ -117,12 +161,8 @@
   "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute"
   "(op = ===> alpha_rlts ===> alpha_rlts) permute permute"
   "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5"
-  apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha_rbv5_rsp)
+  apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha_rbv_rsp_pre alpha_rbv_rsp_pre2 alpha5_reflp)
   apply (clarify)
-  apply (rule conjI)
-  apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
-  apply (simp_all add: alpha5_inj)
-  apply clarify
   apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
 done
 
@@ -168,7 +208,7 @@
 apply (simp add: alpha5_INJ)
 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
 apply (simp_all add: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
+apply (simp add: permute_trm5_lts fresh_star_def eqvts)
 done
 
 lemma lets_ok3:
@@ -185,6 +225,7 @@
 apply (simp add: alpha5_INJ alpha_gen)
 apply (rule_tac x="0::perm" in exI)
 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts)
+apply blast
 done
 
 lemma distinct_helper: