--- a/Nominal-General/Nominal2_Atoms.thy	Tue Apr 27 19:51:35 2010 +0200
+++ b/Nominal-General/Nominal2_Atoms.thy	Tue Apr 27 22:21:16 2010 +0200
@@ -16,68 +16,6 @@
   Class @{text at} only allows types with a single sort.
 *}
 
-class at_base = pt +
-  fixes atom :: "'a \<Rightarrow> atom"
-  assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b"
-  assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)"
-
-declare atom_eqvt[eqvt]
-
-class at = at_base +
-  assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)"
-
-lemma supp_at_base: 
-  fixes a::"'a::at_base"
-  shows "supp a = {atom a}"
-  by (simp add: supp_atom [symmetric] supp_def atom_eqvt)
-
-lemma fresh_at_base: 
-  shows "a \<sharp> b \<longleftrightarrow> a \<noteq> atom b"
-  unfolding fresh_def by (simp add: supp_at_base)
-
-instance at_base < fs
-proof qed (simp add: supp_at_base)
-
-lemma at_base_infinite [simp]:
-  shows "infinite (UNIV :: 'a::at_base set)" (is "infinite ?U")
-proof
-  obtain a :: 'a where "True" by auto
-  assume "finite ?U"
-  hence "finite (atom ` ?U)"
-    by (rule finite_imageI)
-  then obtain b where b: "b \<notin> atom ` ?U" "sort_of b = sort_of (atom a)"
-    by (rule obtain_atom)
-  from b(2) have "b = atom ((atom a \<rightleftharpoons> b) \<bullet> a)"
-    unfolding atom_eqvt [symmetric]
-    by (simp add: swap_atom)
-  hence "b \<in> atom ` ?U" by simp
-  with b(1) show "False" by simp
-qed
-
-lemma swap_at_base_simps [simp]:
-  fixes x y::"'a::at_base"
-  shows "sort_of (atom x) = sort_of (atom y) \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> x = y"
-  and   "sort_of (atom x) = sort_of (atom y) \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> y = x"
-  and   "atom x \<noteq> a \<Longrightarrow> atom x \<noteq> b \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x"
-  unfolding atom_eq_iff [symmetric]
-  unfolding atom_eqvt [symmetric]
-  by simp_all
-
-lemma obtain_at_base:
-  assumes X: "finite X"
-  obtains a::"'a::at_base" where "atom a \<notin> X"
-proof -
-  have "inj (atom :: 'a \<Rightarrow> atom)"
-    by (simp add: inj_on_def)
-  with X have "finite (atom -` X :: 'a set)"
-    by (rule finite_vimageI)
-  with at_base_infinite have "atom -` X \<noteq> (UNIV :: 'a set)"
-    by auto
-  then obtain a :: 'a where "atom a \<notin> X"
-    by auto
-  thus ?thesis ..
-qed
-
 lemma atom_image_cong:
   fixes X Y::"('a::at_base) set"
   shows "(atom ` X = atom ` Y) = (X = Y)"