--- a/Quot/Nominal/LamEx2.thy	Tue Feb 02 09:51:39 2010 +0100
+++ b/Quot/Nominal/LamEx2.thy	Tue Feb 02 10:20:54 2010 +0100
@@ -4,42 +4,6 @@
 
 
 (* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)
-lemma in_permute_iff:
-  shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
-apply(unfold mem_def permute_fun_def)[1]
-apply(simp add: permute_bool_def) 
-done
-
-lemma fresh_star_permute_iff:
-  shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"
-apply(simp add: fresh_star_def)
-apply(auto)
-apply(drule_tac x="p \<bullet> xa" in bspec)
-apply(unfold mem_def permute_fun_def)[1] 
-apply(simp add: eqvts)
-apply(simp add: fresh_permute_iff)
-apply(rule_tac ?p1="- p" in fresh_permute_iff[THEN iffD1])
-apply(simp)
-apply(drule_tac x="- p \<bullet> xa" in bspec)
-apply(rule_tac ?p1="p" in in_permute_iff[THEN iffD1])
-apply(simp)
-apply(simp)
-done
-
-lemma fresh_plus:
-  fixes p q::perm
-  shows "\<lbrakk>a \<sharp> p;  a \<sharp> q\<rbrakk> \<Longrightarrow> a \<sharp> (p + q)"
-unfolding fresh_def
-using supp_plus_perm
-apply(auto)
-done
-
-lemma fresh_star_plus:
-  fixes p q::perm
-  shows "\<lbrakk>a \<sharp>* p;  a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"
-unfolding fresh_star_def
-by (simp add: fresh_plus)
-
 lemma supp_finite_set:
   fixes S::"atom set"
   assumes "finite S"
@@ -191,29 +155,6 @@
 apply(assumption)
 done
 
-lemma fresh_minus_perm:
-  fixes p::perm
-  shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p"
-  apply(simp add: fresh_def)
-  apply(simp only: supp_minus_perm)
-  done
-
-lemma alpha_gen_atom_sym:
-  assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "\<exists>pi. ({atom a}, t) \<approx>gen \<lambda>x1 x2. R x1 x2 \<and> R x2 x1 f pi ({atom b}, s) \<Longrightarrow>
-       \<exists>pi. ({atom b}, s) \<approx>gen R f pi ({atom a}, t)"
-  apply(erule exE)
-  apply(rule_tac x="- pi" in exI)
-  apply(simp add: alpha_gen.simps)
-  apply(erule conjE)+
-  apply(rule conjI)
-  apply(simp add: fresh_star_def fresh_minus_perm)
-  apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
-  apply simp
-  apply(rule a)
-  apply assumption
-  done
-
 lemma alpha_sym:
   shows "t \<approx> s \<Longrightarrow> s \<approx> t"
   apply(induct rule: alpha.induct)
@@ -238,20 +179,9 @@
 apply(erule alpha.cases)
 apply(simp_all)
 apply(rule a3)
-apply(simp add: alpha_gen.simps)
-apply(erule conjE)+
-apply(erule exE)+
-apply(erule conjE)+
-apply(rule_tac x="pia + pi" in exI)
-apply(simp add: fresh_star_plus)
-apply(drule_tac x="- pia \<bullet> sa" in spec)
-apply(drule mp)
-apply(rotate_tac 7)
-apply(drule_tac pi="- pia" in alpha_eqvt)
-apply(simp)
-apply(rotate_tac 9)
-apply(drule_tac pi="pia" in alpha_eqvt)
-apply(simp)
+apply(rule alpha_gen_atom_trans)
+apply(rule alpha_eqvt)
+apply(assumption)+
 done
 
 lemma alpha_equivp: