--- a/Quot/Nominal/Nominal2_Atoms.thy	Sat Feb 06 12:58:56 2010 +0100
+++ b/Quot/Nominal/Nominal2_Atoms.thy	Sun Feb 07 10:16:21 2010 +0100
@@ -5,7 +5,7 @@
 *)
 theory Nominal2_Atoms
 imports Nominal2_Base
-uses ("atom_decl.ML")
+uses ("nominal_atoms.ML")
 begin
 
 section {* Concrete atom types *}
@@ -30,14 +30,13 @@
   shows "supp a = {atom a}"
   by (simp add: supp_atom [symmetric] supp_def atom_eqvt)
 
-lemma fresh_at: 
+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
@@ -157,20 +156,24 @@
   New atom types are defined as subtypes of @{typ atom}.
 *}
 
-lemma exists_eq_sort: 
+lemma exists_eq_simple_sort: 
   shows "\<exists>a. a \<in> {a. sort_of a = s}"
   by (rule_tac x="Atom s 0" in exI, simp)
 
+lemma exists_eq_sort: 
+  shows "\<exists>a. a \<in> {a. sort_of a \<in> range sort_fun}"
+  by (rule_tac x="Atom (sort_fun x) y" in exI, simp)
+
 lemma at_base_class:
-  fixes s :: atom_sort
+  fixes sort_fun :: "'b \<Rightarrow>atom_sort"
   fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
-  assumes type: "type_definition Rep Abs {a. P (sort_of a)}"
+  assumes type: "type_definition Rep Abs {a. sort_of a \<in> range sort_fun}"
   assumes atom_def: "\<And>a. atom a = Rep a"
   assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"
   shows "OFCLASS('a, at_base_class)"
 proof
-  interpret type_definition Rep Abs "{a. P (sort_of a)}" by (rule type)
-  have sort_of_Rep: "\<And>a. P (sort_of (Rep a))" using Rep by simp
+  interpret type_definition Rep Abs "{a. sort_of a \<in> range sort_fun}" by (rule type)
+  have sort_of_Rep: "\<And>a. sort_of (Rep a) \<in> range sort_fun" using Rep by simp
   fix a b :: 'a and p p1 p2 :: perm
   show "0 \<bullet> a = a"
     unfolding permute_def by (simp add: Rep_inverse)
@@ -182,6 +185,31 @@
     unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)
 qed
 
+(*
+lemma at_class:
+  fixes s :: atom_sort
+  fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
+  assumes type: "type_definition Rep Abs {a. sort_of a \<in> range (\<lambda>x::unit. s)}"
+  assumes atom_def: "\<And>a. atom a = Rep a"
+  assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"
+  shows "OFCLASS('a, at_class)"
+proof
+  interpret type_definition Rep Abs "{a. sort_of a \<in> range (\<lambda>x::unit. s)}" by (rule type)
+  have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by (simp add: image_def)
+  fix a b :: 'a and p p1 p2 :: perm
+  show "0 \<bullet> a = a"
+    unfolding permute_def by (simp add: Rep_inverse)
+  show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"
+    unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)
+  show "sort_of (atom a) = sort_of (atom b)"
+    unfolding atom_def by (simp add: sort_of_Rep)
+  show "atom a = atom b \<longleftrightarrow> a = b"
+    unfolding atom_def by (simp add: Rep_inject)
+  show "p \<bullet> atom a = atom (p \<bullet> a)"
+    unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)
+qed
+*)
+
 lemma at_class:
   fixes s :: atom_sort
   fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
@@ -191,7 +219,7 @@
   shows "OFCLASS('a, at_class)"
 proof
   interpret type_definition Rep Abs "{a. sort_of a = s}" by (rule type)
-  have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by simp
+  have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by (simp add: image_def)
   fix a b :: 'a and p p1 p2 :: perm
   show "0 \<bullet> a = a"
     unfolding permute_def by (simp add: Rep_inverse)
@@ -215,7 +243,9 @@
 
 text {* at the moment only single-sort concrete atoms are supported *}
 
-use "atom_decl.ML"
+use "nominal_atoms.ML"
+
+
 
 
 end