--- a/Nominal-General/Atoms.thy	Sat Sep 04 06:48:14 2010 +0800
+++ b/Nominal-General/Atoms.thy	Sat Sep 04 07:28:35 2010 +0800
@@ -4,9 +4,41 @@
     Instantiations of concrete atoms 
 *)
 theory Atoms
-imports Nominal2_Atoms
+imports Nominal2_Base
 begin
 
+
+
+section {* @{const nat_of} is an example of a function 
+  without finite support *}
+
+
+lemma not_fresh_nat_of:
+  shows "\<not> a \<sharp> nat_of"
+unfolding fresh_def supp_def
+proof (clarsimp)
+  assume "finite {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"
+  hence "finite ({a} \<union> {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of})"
+    by simp
+  then obtain b where
+    b1: "b \<noteq> a" and
+    b2: "sort_of b = sort_of a" and
+    b3: "(a \<rightleftharpoons> b) \<bullet> nat_of = nat_of"
+    by (rule obtain_atom) auto
+  have "nat_of a = (a \<rightleftharpoons> b) \<bullet> (nat_of a)" by (simp add: permute_nat_def)
+  also have "\<dots> = ((a \<rightleftharpoons> b) \<bullet> nat_of) ((a \<rightleftharpoons> b) \<bullet> a)" by (simp add: permute_fun_app_eq)
+  also have "\<dots> = nat_of ((a \<rightleftharpoons> b) \<bullet> a)" using b3 by simp
+  also have "\<dots> = nat_of b" using b2 by simp
+  finally have "nat_of a = nat_of b" by simp
+  with b2 have "a = b" by (simp add: atom_components_eq_iff)
+  with b1 show "False" by simp
+qed
+
+lemma supp_nat_of:
+  shows "supp nat_of = UNIV"
+  using not_fresh_nat_of [unfolded fresh_def] by auto
+
+
 section {* Manual instantiation of class @{text at}. *}
 
 typedef (open) name = "{a. sort_of a = Sort ''name'' []}"