diff -r aa999d263b10 -r d00dd828f7af Nominal/Abs.thy
--- a/Nominal/Abs.thy	Fri Mar 26 22:22:41 2010 +0100
+++ b/Nominal/Abs.thy	Fri Mar 26 22:23:22 2010 +0100
@@ -117,33 +117,6 @@
   apply(rule_tac [!] x="p \<bullet> pa" in exI)
   by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric])
 
-lemma alphas_abs_swap1:
-  assumes a1: "a \<notin> (supp x) - bs"
-  and     a2: "b \<notin> (supp x) - bs"
-  shows "(bs, x) \<approx>abs ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
-  and   "(bs, x) \<approx>abs_res ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
-  using a1 a2
-  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] 
-  by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
-     (auto simp add: supp_perm swap_atom)
-
-lemma alphas_abs_swap2:
-  assumes a1: "a \<notin> (supp x) - (set bs)"
-  and     a2: "b \<notin> (supp x) - (set bs)"
-  shows "(bs, x) \<approx>abs_lst ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
-  using a1 a2
-  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] 
-  by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
-     (auto simp add: supp_perm swap_atom)
-
 fun
   aux_set 
 where
@@ -227,9 +200,16 @@
   shows "(\<And>as (x::'a::pt). P1 (Abs as x)) \<Longrightarrow> P1 x1"
   and   "(\<And>as (x::'a::pt). P2 (Abs_res as x)) \<Longrightarrow> P2 x2"
   and   "(\<And>as (x::'a::pt). P3 (Abs_lst as x)) \<Longrightarrow> P3 x3"
-  apply(lifting prod.induct[where 'a="atom set" and 'b="'a"])
-  apply(lifting prod.induct[where 'a="atom set" and 'b="'a"])
-  apply(lifting prod.induct[where 'a="atom list" and 'b="'a"])
+  by (lifting prod.induct[where 'a="atom set" and 'b="'a"]
+              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
@@ -297,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"
@@ -317,10 +333,7 @@
   shows "supp_gen (Abs bs x) = (supp x) - bs"
   and   "supp_res (Abs_res bs x) = (supp x) - bs"
   and   "supp_lst (Abs_lst cs x) = (supp x) - (set cs)"
-  apply(lifting aux_set.simps)
-  apply(lifting aux_set.simps)
-  apply(lifting aux_list.simps)
-  done
+  by (lifting aux_set.simps aux_set.simps aux_list.simps)
 
 lemma aux_supp_eqvt[eqvt]:
   shows "(p \<bullet> supp_gen x) = supp_gen (p \<bullet> x)"
@@ -342,30 +355,6 @@
   apply(simp_all add: eqvts_raw)
   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)"
-  using a1 a2 
-  apply(lifting alphas_abs_swap1(1))
-  apply(lifting alphas_abs_swap1(2))
-  done
-
-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)"
-  using a1 a2 by (lifting alphas_abs_swap2)
-
-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)"
@@ -430,14 +419,6 @@
   unfolding supp_abs
   by auto
 
-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
-
 
 section {* BELOW is stuff that may or may not be needed *}