--- a/Nominal/Abs.thy	Wed Aug 25 22:55:42 2010 +0800
+++ b/Nominal/Abs.thy	Wed Aug 25 23:16:42 2010 +0800
@@ -560,29 +560,9 @@
   by (perm_simp) (rule refl)
 
 
-
-
-section {* BELOW is stuff that may or may not be needed *}
+(* Below seems to be not needed *)
 
-lemma supp_atom_image:
-  fixes as::"'a::at_base set"
-  shows "supp (atom ` as) = supp as"
-apply(simp add: supp_def)
-apply(simp add: image_eqvt)
-apply(simp add: eqvts_raw)
-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"
-  apply (simp add: fresh_def)
-  apply (simp add: supp_atom_image)
-  apply (fold fresh_def)
-  apply (simp add: swap_fresh_fresh)
-  done
-
-(* TODO: The following lemmas can be moved somewhere... *)
-
+(*
 lemma Abs_eq_iff:
   shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
   and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
@@ -598,23 +578,7 @@
   and q2: "Quotient R2 Abs2 Rep2"
   shows "((Abs1 ---> Abs2 ---> prod_fun Abs1 Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> prod_fun Rep1 Rep2 ---> id) split = split"
   by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
-
-lemma alphas2:
-  "(bs, x1, x2) \<approx>gen (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) =
-  (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2
-  \<and> pi \<bullet> bs = cs)"
-  "(bs, x1, x2) \<approx>res (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) =
-  (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2)"
-  "(bsl, x1, x2) \<approx>lst (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (csl, y1, y2) =
-  (f1 x1 \<union> f2 x2 - set bsl = f1 y1 \<union> f2 y2 - set csl \<and> (f1 x1 \<union> f2 x2 - set bsl) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2
-  \<and> pi \<bullet> bsl = csl)"
-by (simp_all add: alphas)
-
-lemma alphas3:
-  "(bsl, x1, x2, x3) \<approx>lst (\<lambda>(x1, y1, z1) (x2, y2, z2). R1 x1 x2 \<and> R2 y1 y2 \<and> R3 z1 z2) (\<lambda>(a, b, c). f1 a \<union> (f2 b \<union> f3 c)) pi (csl, y1, y2, y3) = (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl = f1 y1 \<union> (f2 y2 \<union> f3 y3) - set csl \<and>
-     (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl) \<sharp>* pi \<and>
-     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)
+*)
 
 
 end