--- a/Nominal/Abs.thy	Thu Jun 03 15:02:52 2010 +0200
+++ b/Nominal/Abs.thy	Mon Jun 07 11:43:01 2010 +0200
@@ -51,6 +51,73 @@
   by (case_tac [!] bs, case_tac [!] cs) 
      (auto simp add: le_fun_def le_bool_def alphas)
 
+(* equivariance *)
+lemma alpha_gen_eqvt[eqvt]:
+  shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
+  and   "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
+  and   "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> es, p \<bullet> y)" 
+  unfolding alphas
+  unfolding permute_eqvt[symmetric]
+  unfolding set_eqvt[symmetric]
+  unfolding permute_fun_app_eq[symmetric]
+  unfolding Diff_eqvt[symmetric]
+  by (auto simp add: permute_bool_def fresh_star_permute_iff)
+
+(* equivalence *)
+lemma alpha_gen_refl:
+  assumes a: "R x x"
+  shows "(bs, x) \<approx>gen R f 0 (bs, x)"
+  and   "(bs, x) \<approx>res R f 0 (bs, x)"
+  and   "(cs, x) \<approx>lst R f 0 (cs, x)"
+  using a 
+  unfolding alphas
+  unfolding fresh_star_def
+  by (simp_all add: fresh_zero_perm)
+
+lemma alpha_gen_sym:
+  assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
+  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)"
+  unfolding alphas fresh_star_def
+  using a
+  by (auto simp add:  fresh_minus_perm)
+
+lemma alpha_gen_sym_eqvt:
+  assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)" 
+  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
+
+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"
+  shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)"
+  and   "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)"
+  and   "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>lst R f (q + p) (hs, z)"
+  using a
+  unfolding alphas fresh_star_def
+  by (simp_all add: fresh_plus_perm)
+
+
+
+section {* General Abstractions *}
+
 fun
   alpha_abs 
 where
@@ -731,45 +798,7 @@
 
 lemmas alphas_compose_trans2 = alpha_gen_compose_trans2 alpha_res_compose_trans2 alpha_lst_compose_trans2
 
-lemma alpha_gen_refl:
-  assumes a: "R x x"
-  shows "(bs, x) \<approx>gen R f 0 (bs, x)"
-  and   "(bs, x) \<approx>res R f 0 (bs, x)"
-  and   "(cs, x) \<approx>lst R f 0 (cs, x)"
-  using a 
-  unfolding alphas
-  unfolding fresh_star_def
-  by (simp_all add: fresh_zero_perm)
 
-lemma alpha_gen_sym:
-  assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
-  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)"
-  unfolding alphas fresh_star_def
-  using a
-  by (auto simp add:  fresh_minus_perm)
-
-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"
-  shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)"
-  and   "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)"
-  and   "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>lst R f (q + p) (hs, z)"
-  using a
-  unfolding alphas fresh_star_def
-  by (simp_all add: fresh_plus_perm)
-
-
-lemma alpha_gen_eqvt[eqvt]:
-  shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
-  and   "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
-  and   "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> es, p \<bullet> y)" 
-  unfolding alphas
-  unfolding permute_eqvt[symmetric]
-  unfolding set_eqvt[symmetric]
-  unfolding permute_fun_app_eq[symmetric]
-  unfolding Diff_eqvt[symmetric]
-  by (auto simp add: permute_bool_def fresh_star_permute_iff)
 
 lemma alpha_gen_simpler:
   assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"