--- a/Nominal/Abs.thy	Fri Mar 26 18:44:47 2010 +0100
+++ b/Nominal/Abs.thy	Fri Mar 26 22:02:59 2010 +0100
@@ -204,6 +204,14 @@
               prod.induct[where 'a="atom set" and 'b="'a"]
               prod.induct[where 'a="atom list" and 'b="'a"])
 
+lemma abs_eq_iff:
+  shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)"
+  and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)"
+  and   "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)"
+  apply(simp_all)
+  apply(lifting alphas_abs)
+  done
+
 instantiation abs_gen :: (pt) pt
 begin
 
@@ -269,6 +277,42 @@
 
 lemmas permute_abs = permute_Abs permute_Abs_res permute_Abs_lst
 
+lemma abs_swap1:
+  assumes a1: "a \<notin> (supp x) - bs"
+  and     a2: "b \<notin> (supp x) - bs"
+  shows "Abs bs x = Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
+  and   "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
+  unfolding abs_eq_iff
+  unfolding alphas_abs
+  unfolding alphas
+  unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] 
+  unfolding fresh_star_def fresh_def
+  unfolding swap_set_not_in[OF a1 a2] 
+  using a1 a2
+  by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
+     (auto simp add: supp_perm swap_atom)
+
+lemma abs_swap2:
+  assumes a1: "a \<notin> (supp x) - (set bs)"
+  and     a2: "b \<notin> (supp x) - (set bs)"
+  shows "Abs_lst bs x = Abs_lst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
+  unfolding abs_eq_iff
+  unfolding alphas_abs
+  unfolding alphas
+  unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric]
+  unfolding fresh_star_def fresh_def
+  unfolding swap_set_not_in[OF a1 a2]
+  using a1 a2
+  by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
+     (auto simp add: supp_perm swap_atom)
+
+lemma abs_supports:
+  shows "((supp x) - as) supports (Abs as x)"
+  and   "((supp x) - as) supports (Abs_res as x)"
+  and   "((supp x) - (set bs)) supports (Abs_lst bs x)"
+  unfolding supports_def
+  unfolding permute_abs
+  by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
 
 quotient_definition
   "supp_gen :: ('a::pt) abs_gen \<Rightarrow> atom set"
@@ -311,51 +355,6 @@
   apply(simp_all add: eqvts_raw)
   done
 
-lemma abs_eq_iff:
-  shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)"
-  and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)"
-  and   "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)"
-  apply(simp_all)
-  apply(lifting alphas_abs)
-  done
-
-lemma abs_swap1:
-  assumes a1: "a \<notin> (supp x) - bs"
-  and     a2: "b \<notin> (supp x) - bs"
-  shows "Abs bs x = Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
-  and   "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
-  unfolding abs_eq_iff
-  unfolding alphas_abs
-  unfolding alphas
-  unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] 
-  unfolding fresh_star_def fresh_def
-  unfolding swap_set_not_in[OF a1 a2] 
-  using a1 a2
-  by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
-     (auto simp add: supp_perm swap_atom)
-
-lemma abs_swap2:
-  assumes a1: "a \<notin> (supp x) - (set bs)"
-  and     a2: "b \<notin> (supp x) - (set bs)"
-  shows "Abs_lst bs x = Abs_lst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
-  unfolding abs_eq_iff
-  unfolding alphas_abs
-  unfolding alphas
-  unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric]
-  unfolding fresh_star_def fresh_def
-  unfolding swap_set_not_in[OF a1 a2]
-  using a1 a2
-  by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
-     (auto simp add: supp_perm swap_atom)
-
-lemma abs_supports:
-  shows "((supp x) - as) supports (Abs as x)"
-  and   "((supp x) - as) supports (Abs_res as x)"
-  and   "((supp x) - (set bs)) supports (Abs_lst bs x)"
-  unfolding supports_def
-  unfolding permute_abs
-  by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
-
 lemma supp_abs_subset1:
   assumes a: "finite (supp x)"
   shows "(supp x) - as \<subseteq> supp (Abs as x)"