--- a/Nominal/Abs.thy	Mon Jun 07 11:46:26 2010 +0200
+++ b/Nominal/Abs.thy	Wed Jun 09 15:14:16 2010 +0200
@@ -88,22 +88,17 @@
   and     b: "p \<bullet> R = R"
   shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)" 
   and   "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)" 
-  and   "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)" 
-proof -
-  { assume "R (p \<bullet> x) y"
-    then have "R y (p \<bullet> x)" using a by simp
-    then have "R (- p \<bullet> y) x"
-      apply(rule_tac p="p" in permute_boolE)
-      apply(perm_simp add: permute_minus_cancel b)
-      apply(assumption)
-      done
-  }
-  then show "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)" 
-    and     "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)" 
-    and     "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)" 
-    unfolding alphas fresh_star_def
-    by (auto simp add:  fresh_minus_perm)
-qed
+  and   "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
+apply(auto intro!: alpha_gen_sym)
+apply(drule_tac [!] a)
+apply(rule_tac [!] p="p" in permute_boolE)
+apply(perm_simp add: permute_minus_cancel b)
+apply(assumption)
+apply(perm_simp add: permute_minus_cancel b)
+apply(assumption)
+apply(perm_simp add: permute_minus_cancel b)
+apply(assumption)
+done
 
 lemma alpha_gen_trans:
   assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
@@ -115,6 +110,74 @@
   by (simp_all add: fresh_plus_perm)
 
 
+lemma alpha_gen_trans_eqvt:
+  assumes b: "(cs, y) \<approx>gen R f q (ds, z)"
+  and     a: "(bs, x) \<approx>gen R f p (cs, y)" 
+  and     d: "q \<bullet> R = R"
+  and     c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
+  shows "(bs, x) \<approx>gen R f (q + p) (ds, z)"
+apply(rule alpha_gen_trans)
+defer
+apply(rule a)
+apply(rule b)
+apply(drule c)
+apply(rule_tac p="q" in permute_boolE)
+apply(perm_simp add: permute_minus_cancel d)
+apply(assumption)
+apply(rotate_tac -1)
+apply(drule_tac p="q" in permute_boolI)
+apply(perm_simp add: permute_minus_cancel d)
+apply(simp add: permute_eqvt[symmetric])
+done
+
+lemma alpha_res_trans_eqvt:
+  assumes  b: "(cs, y) \<approx>res R f q (ds, z)"
+  and     a: "(bs, x) \<approx>res R f p (cs, y)" 
+  and     d: "q \<bullet> R = R"
+  and     c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
+  shows "(bs, x) \<approx>res R f (q + p) (ds, z)"
+apply(rule alpha_gen_trans)
+defer
+apply(rule a)
+apply(rule b)
+apply(drule c)
+apply(rule_tac p="q" in permute_boolE)
+apply(perm_simp add: permute_minus_cancel d)
+apply(assumption)
+apply(rotate_tac -1)
+apply(drule_tac p="q" in permute_boolI)
+apply(perm_simp add: permute_minus_cancel d)
+apply(simp add: permute_eqvt[symmetric])
+done
+
+lemma alpha_lst_trans_eqvt:
+  assumes b: "(cs, y) \<approx>lst R f q (ds, z)"
+  and     a: "(bs, x) \<approx>lst R f p (cs, y)" 
+  and     d: "q \<bullet> R = R"
+  and     c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
+  shows "(bs, x) \<approx>lst R f (q + p) (ds, z)"
+apply(rule alpha_gen_trans)
+defer
+apply(rule a)
+apply(rule b)
+apply(drule c)
+apply(rule_tac p="q" in permute_boolE)
+apply(perm_simp add: permute_minus_cancel d)
+apply(assumption)
+apply(rotate_tac -1)
+apply(drule_tac p="q" in permute_boolI)
+apply(perm_simp add: permute_minus_cancel d)
+apply(simp add: permute_eqvt[symmetric])
+done
+
+lemmas alpha_trans_eqvt = alpha_gen_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
+
+lemma test:
+  shows "(as, t) \<approx>gen R f pi (bs, s) \<Longrightarrow> R (pi \<bullet> t) s"
+  and   "(as, t) \<approx>res R f pi (bs, s) \<Longrightarrow> R (pi \<bullet> t) s"
+  and   "(cs, t) \<approx>lst R f pi (ds, s) \<Longrightarrow> R (pi \<bullet> t) s"
+  by (simp_all add: alphas)
+
 
 section {* General Abstractions *}