--- a/Nominal/Rsp.thy	Wed Mar 17 09:57:54 2010 +0100
+++ b/Nominal/Rsp.thy	Wed Mar 17 11:11:25 2010 +0100
@@ -186,7 +186,7 @@
   (split_conjs THEN_ALL_NEW TRY o resolve_tac
     @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]})
   THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps (@{thms permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt))
+  asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt))
 *}
 
 ML {*

--- a/Nominal/Term5.thy	Wed Mar 17 09:57:54 2010 +0100
+++ b/Nominal/Term5.thy	Wed Mar 17 11:11:25 2010 +0100
@@ -50,7 +50,7 @@
 (*lemma alpha5_eqvt:
   "(xa \<approx>5 y \<longrightarrow> (p \<bullet> xa) \<approx>5 (p \<bullet> y)) \<and>
   (xb \<approx>l ya \<longrightarrow> (p \<bullet> xb) \<approx>l (p \<bullet> ya)) \<and>
-  (alpha_rbv5 a b c \<longrightarrow> alpha_rbv5 (p \<bullet> a) (p \<bullet> b) (p \<bullet> c))"
+  (alpha_rbv5 b c \<longrightarrow> alpha_rbv5 (p \<bullet> b) (p \<bullet> c))"
 apply (tactic {* alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} @{context} 1 *})
 done*)
 
@@ -75,10 +75,21 @@
 apply (simp_all add: alpha5_inj)
 apply (erule exE)
 apply (rule_tac x="- pi" in exI)
+apply (simp add: alpha_gen)
+  apply(simp add: fresh_star_def fresh_minus_perm)
 apply clarify
 apply (rule conjI)
-apply (erule_tac [!] alpha_gen_compose_sym)
-apply (simp_all add: alpha5_eqvt)
+apply (rotate_tac 3)
+apply (frule_tac p="- pi" in alpha5_eqvt(2))
+apply simp
+apply (rule conjI)
+apply (rotate_tac 5)
+apply (frule_tac p="- pi" in alpha5_eqvt(1))
+apply simp
+apply (rotate_tac 6)
+apply simp
+apply (drule_tac p1="- pi" in permute_eq_iff[symmetric,THEN iffD1])
+apply (simp)
 done
 
 lemma alpha5_transp:
@@ -94,19 +105,29 @@
 apply (simp_all add: alpha5_inj)
 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
 apply (simp_all add: alpha5_inj)
-apply (tactic {* eetac @{thm exi_sum} @{context} 1 *})
-apply clarify
-apply (rule conjI)
-apply (erule alpha_gen_compose_trans)
-apply (assumption)
-apply (simp add: alpha5_eqvt)
-apply (erule alpha_gen_compose_trans)
-apply (assumption)
-apply (simp add: alpha5_eqvt)
+defer
 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
 apply (simp_all add: alpha5_inj)
 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
 apply (simp_all add: alpha5_inj)
+apply (tactic {* eetac @{thm exi_sum} @{context} 1 *})
+apply (simp add: alpha_gen)
+apply clarify
+apply(simp add: fresh_star_plus)
+apply (rule conjI)
+apply (erule_tac x="- pi \<bullet> rltsaa" in allE)
+apply (rotate_tac 5)
+apply (drule_tac p="- pi" in alpha5_eqvt(2))
+apply simp
+apply (drule_tac p="pi" in alpha5_eqvt(2))
+apply simp
+apply (erule_tac x="- pi \<bullet> rtrm5aa" in allE)
+apply (rotate_tac 7)
+apply (drule_tac p="- pi" in alpha5_eqvt(1))
+apply simp
+apply (rotate_tac 3)
+apply (drule_tac p="pi" in alpha5_eqvt(1))
+apply simp
 done
 
 lemma alpha5_equivp:
@@ -146,7 +167,7 @@
   apply(simp_all add: eqvts)
   apply(simp add: alpha_gen)
   apply(clarify)
-  apply(simp)
+  apply blast
 done
 
 lemma bv_list_rsp:
@@ -234,20 +255,25 @@
 lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
 lemmas bv5[simp] = rbv5.simps[quot_lifted]
 lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted]
-lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen2, unfolded alpha_gen, quot_lifted, folded alpha_gen2, folded alpha_gen]
 lemmas alpha5_DIS = alpha_dis[quot_lifted]
 
+(* why is this not in Isabelle? *)
+lemma set_sub: "{a, b} - {b} = {a} - {b}"
+by auto
+
 lemma lets_bla:
   "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \<noteq> (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))"
-apply (simp only: alpha5_INJ)
-apply (simp only: bv5)
+apply (simp only: alpha5_INJ bv5)
 apply simp
 apply (rule allI)
 apply (simp_all add: alpha_gen)
 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ eqvts)
 apply (rule impI)
 apply (rule impI)
-sorry (* The assumption is false, so it is true *)
+apply (rule impI)
+apply (simp add: set_sub)
+done
 
 lemma lets_ok:
   "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
@@ -256,6 +282,7 @@
 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: eqvts)
 done
 
 lemma lets_ok3:

--- 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: