diff -r 99706604c573 -r 9038c9549073 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Wed Jun 23 06:45:03 2010 +0100
+++ b/Nominal/Abs.thy	Wed Jun 23 06:54:48 2010 +0100
@@ -536,7 +536,8 @@
 apply(simp add: atom_image_cong)
 done
 
-lemma swap_atom_image_fresh: "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn"
+lemma swap_atom_image_fresh: 
+  "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn"
   apply (simp add: fresh_def)
   apply (simp add: supp_atom_image)
   apply (fold fresh_def)
@@ -578,291 +579,6 @@
      R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 \<and> R3 (pi \<bullet> x3) y3 \<and> pi \<bullet> bsl = csl)"
 by (simp add: alphas)
 
-lemma alpha_gen_compose_sym:
-  fixes pi
-  assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
-  and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "(ab, s) \<approx>gen R f (- pi) (aa, t)"
-  using b apply -
-  apply(simp add: alphas)
-  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(clarify)
-  apply(simp)
-  apply(rule a)
-  apply assumption
-  done
-
-lemma alpha_res_compose_sym:
-  fixes pi
-  assumes b: "(aa, t) \<approx>res (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
-  and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "(ab, s) \<approx>res R f (- pi) (aa, t)"
-  using b apply -
-  apply(simp add: alphas)
-  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_lst_compose_sym:
-  fixes pi
-  assumes b: "(aa, t) \<approx>lst (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
-  and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "(ab, s) \<approx>lst R f (- pi) (aa, t)"
-  using b apply -
-  apply(simp add: alphas)
-  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(clarify)
-  apply(simp)
-  apply(rule a)
-  apply assumption
-  done
-
-lemmas alphas_compose_sym = alpha_gen_compose_sym alpha_res_compose_sym alpha_lst_compose_sym
-
-lemma alpha_gen_compose_sym2:
-  assumes a: "(aa, t1, t2) \<approx>gen (\<lambda>(x11, x12) (x21, x22).
-  (R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)"
-  and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
-  and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
-  shows "(ab, s1, s2) \<approx>gen (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)"
-  using a
-  apply(simp add: alphas)
-  apply clarify
-  apply (rule conjI)
-  apply(simp add: fresh_star_def fresh_minus_perm)
-  apply (rule conjI)
-  apply (rotate_tac 3)
-  apply (drule_tac pi="- pi" in r1)
-  apply simp
-  apply (rule conjI)
-  apply (rotate_tac -1)
-  apply (drule_tac pi="- pi" in r2)
-  apply simp_all
-  done
-
-lemma alpha_res_compose_sym2:
-  assumes a: "(aa, t1, t2) \<approx>res (\<lambda>(x11, x12) (x21, x22).
-  (R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)"
-  and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
-  and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
-  shows "(ab, s1, s2) \<approx>res (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)"
-  using a
-  apply(simp add: alphas)
-  apply clarify
-  apply (rule conjI)
-  apply(simp add: fresh_star_def fresh_minus_perm)
-  apply (rule conjI)
-  apply (rotate_tac 3)
-  apply (drule_tac pi="- pi" in r1)
-  apply simp
-  apply (rotate_tac -1)
-  apply (drule_tac pi="- pi" in r2)
-  apply simp
-  done
-
-lemma alpha_lst_compose_sym2:
-  assumes a: "(aa, t1, t2) \<approx>lst (\<lambda>(x11, x12) (x21, x22).
-  (R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)"
-  and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
-  and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
-  shows "(ab, s1, s2) \<approx>lst (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)"
-  using a
-  apply(simp add: alphas)
-  apply clarify
-  apply (rule conjI)
-  apply(simp add: fresh_star_def fresh_minus_perm)
-  apply (rule conjI)
-  apply (rotate_tac 3)
-  apply (drule_tac pi="- pi" in r1)
-  apply simp
-  apply (rule conjI)
-  apply (rotate_tac -1)
-  apply (drule_tac pi="- pi" in r2)
-  apply simp_all
-  done
-
-lemmas alphas_compose_sym2 = alpha_gen_compose_sym2 alpha_res_compose_sym2 alpha_lst_compose_sym2
-
-lemma alpha_gen_compose_trans:
-  fixes pi pia
-  assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
-  and c: "(ab, ta) \<approx>gen R f pia (ac, sa)"
-  and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)"
-  using b c apply -
-  apply(simp add: alphas)
-  apply(erule conjE)+
-  apply(simp add: fresh_star_plus)
-  apply(drule_tac x="- pia \<bullet> sa" in spec)
-  apply(drule mp)
-  apply(rotate_tac 5)
-  apply(drule_tac pi="- pia" in a)
-  apply(simp)
-  apply(rotate_tac 7)
-  apply(drule_tac pi="pia" in a)
-  apply(simp)
-  done
-
-lemma alpha_res_compose_trans:
-  fixes pi pia
-  assumes b: "(aa, t) \<approx>res (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
-  and c: "(ab, ta) \<approx>res R f pia (ac, sa)"
-  and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "(aa, t) \<approx>res R f (pia + pi) (ac, sa)"
-  using b c apply -
-  apply(simp add: alphas)
-  apply(erule conjE)+
-  apply(simp add: fresh_star_plus)
-  apply(drule_tac x="- pia \<bullet> sa" in spec)
-  apply(drule mp)
-  apply(drule_tac pi="- pia" in a)
-  apply(simp)
-  apply(rotate_tac 6)
-  apply(drule_tac pi="pia" in a)
-  apply(simp)
-  done
-
-lemma alpha_lst_compose_trans:
-  fixes pi pia
-  assumes b: "(aa, t) \<approx>lst (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
-  and c: "(ab, ta) \<approx>lst R f pia (ac, sa)"
-  and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "(aa, t) \<approx>lst R f (pia + pi) (ac, sa)"
-  using b c apply -
-  apply(simp add: alphas)
-  apply(erule conjE)+
-  apply(simp add: fresh_star_plus)
-  apply(drule_tac x="- pia \<bullet> sa" in spec)
-  apply(drule mp)
-  apply(rotate_tac 5)
-  apply(drule_tac pi="- pia" in a)
-  apply(simp)
-  apply(rotate_tac 7)
-  apply(drule_tac pi="pia" in a)
-  apply(simp)
-  done
-
-lemmas alphas_compose_trans = alpha_gen_compose_trans alpha_res_compose_trans alpha_lst_compose_trans
-
-lemma alpha_gen_compose_trans2:
-  fixes pi pia
-  assumes b: "(aa, (t1, t2)) \<approx>gen
-    (\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z))
-    (\<lambda>(b, a). fv_a b \<union> fv_b a) pi (ab, (ta1, ta2))"
-  and c: "(ab, (ta1, ta2)) \<approx>gen (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
-    pia (ac, (sa1, sa2))"
-  and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
-  and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
-  shows "(aa, (t1, t2)) \<approx>gen (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
-    (pia + pi) (ac, (sa1, sa2))"
-  using b c apply -
-  apply(simp add: alphas2)
-  apply(simp add: alphas)
-  apply(erule conjE)+
-  apply(simp add: fresh_star_plus)
-  apply(drule_tac x="- pia \<bullet> sa1" in spec)
-  apply(drule mp)
-  apply(rotate_tac 5)
-  apply(drule_tac pi="- pia" in r1)
-  apply(simp)
-  apply(rotate_tac -1)
-  apply(drule_tac pi="pia" in r1)
-  apply(simp)
-  apply(drule_tac x="- pia \<bullet> sa2" in spec)
-  apply(drule mp)
-  apply(rotate_tac 6)
-  apply(drule_tac pi="- pia" in r2)
-  apply(simp)
-  apply(rotate_tac -1)
-  apply(drule_tac pi="pia" in r2)
-  apply(simp)
-  done
-
-lemma alpha_res_compose_trans2:
-  fixes pi pia
-  assumes b: "(aa, (t1, t2)) \<approx>res
-    (\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z))
-    (\<lambda>(b, a). fv_a b \<union> fv_b a) pi (ab, (ta1, ta2))"
-  and c: "(ab, (ta1, ta2)) \<approx>res (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
-    pia (ac, (sa1, sa2))"
-  and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
-  and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
-  shows "(aa, (t1, t2)) \<approx>res (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
-    (pia + pi) (ac, (sa1, sa2))"
-  using b c apply -
-  apply(simp add: alphas2)
-  apply(simp add: alphas)
-  apply(erule conjE)+
-  apply(simp add: fresh_star_plus)
-  apply(drule_tac x="- pia \<bullet> sa1" in spec)
-  apply(drule mp)
-  apply(rotate_tac 5)
-  apply(drule_tac pi="- pia" in r1)
-  apply(simp)
-  apply(rotate_tac -1)
-  apply(drule_tac pi="pia" in r1)
-  apply(simp)
-  apply(drule_tac x="- pia \<bullet> sa2" in spec)
-  apply(drule mp)
-  apply(rotate_tac 6)
-  apply(drule_tac pi="- pia" in r2)
-  apply(simp)
-  apply(rotate_tac -1)
-  apply(drule_tac pi="pia" in r2)
-  apply(simp)
-  done
-
-lemma alpha_lst_compose_trans2:
-  fixes pi pia
-  assumes b: "(aa, (t1, t2)) \<approx>lst
-    (\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z))
-    (\<lambda>(b, a). fv_a b \<union> fv_b a) pi (ab, (ta1, ta2))"
-  and c: "(ab, (ta1, ta2)) \<approx>lst (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
-    pia (ac, (sa1, sa2))"
-  and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
-  and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
-  shows "(aa, (t1, t2)) \<approx>lst (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
-    (pia + pi) (ac, (sa1, sa2))"
-  using b c apply -
-  apply(simp add: alphas2)
-  apply(simp add: alphas)
-  apply(erule conjE)+
-  apply(simp add: fresh_star_plus)
-  apply(drule_tac x="- pia \<bullet> sa1" in spec)
-  apply(drule mp)
-  apply(rotate_tac 5)
-  apply(drule_tac pi="- pia" in r1)
-  apply(simp)
-  apply(rotate_tac -1)
-  apply(drule_tac pi="pia" in r1)
-  apply(simp)
-  apply(drule_tac x="- pia \<bullet> sa2" in spec)
-  apply(drule mp)
-  apply(rotate_tac 6)
-  apply(drule_tac pi="- pia" in r2)
-  apply(simp)
-  apply(rotate_tac -1)
-  apply(drule_tac pi="pia" in r2)
-  apply(simp)
-  done
-
-lemmas alphas_compose_trans2 = alpha_gen_compose_trans2 alpha_res_compose_trans2 alpha_lst_compose_trans2
-
-
-
 lemma alpha_gen_simpler:
   assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"
   and fin_fv: "finite (f x)"