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