# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1272399676 -7200
# Node ID 84a13d1e251111980a865c6b07bbdcd7a5a84fc1
# Parent  774d631726ad831be051ef6ffe4343722959e706
moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base

diff -r 774d631726ad -r 84a13d1e2511 Nominal-General/Nominal2_Atoms.thy
--- 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)"
diff -r 774d631726ad -r 84a13d1e2511 Nominal-General/Nominal2_Base.thy
--- a/Nominal-General/Nominal2_Base.thy	Tue Apr 27 19:51:35 2010 +0200
+++ b/Nominal-General/Nominal2_Base.thy	Tue Apr 27 22:21:16 2010 +0200
@@ -1099,6 +1099,69 @@
     by auto
 qed
 
+
+section {* Concrete atoms types *}
+
+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)"
+
+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
+
 section {* library functions for the nominal infrastructure *}
 use "nominal_library.ML"
 
diff -r 774d631726ad -r 84a13d1e2511 Nominal-General/Nominal2_Eqvt.thy
--- a/Nominal-General/Nominal2_Eqvt.thy	Tue Apr 27 19:51:35 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Tue Apr 27 22:21:16 2010 +0200
@@ -251,7 +251,7 @@
   imp_eqvt [folded induct_implies_def]
 
   (* nominal *)
-  supp_eqvt fresh_eqvt add_perm_eqvt
+  supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt
 
   (* datatypes *)
   permute_prod.simps append_eqvt rev_eqvt set_eqvt
diff -r 774d631726ad -r 84a13d1e2511 Nominal-General/nominal_atoms.ML
--- a/Nominal-General/nominal_atoms.ML	Tue Apr 27 19:51:35 2010 +0200
+++ b/Nominal-General/nominal_atoms.ML	Tue Apr 27 22:21:16 2010 +0200
@@ -15,24 +15,13 @@
 structure Atom_Decl :> ATOM_DECL =
 struct
 
-val atomT = @{typ atom};
-val permT = @{typ perm};
-
-val sort_of_const = @{term sort_of};
-fun atom_const T = Const (@{const_name atom}, T --> atomT);
-fun permute_const T = Const (@{const_name permute}, permT --> T --> T);
-
-fun mk_sort_of t = sort_of_const $ t;
-fun mk_atom t = atom_const (fastype_of t) $ t;
-fun mk_permute (p, t) = permute_const (fastype_of t) $ p $ t;
-
 fun atom_decl_set (str : string) : term =
   let
-    val a = Free ("a", atomT);
+    val a = Free ("a", @{typ atom});
     val s = Const (@{const_name "Sort"}, @{typ "string => atom_sort list => atom_sort"})
               $ HOLogic.mk_string str $ HOLogic.nil_const @{typ "atom_sort"};
   in
-    HOLogic.mk_Collect ("a", atomT, HOLogic.mk_eq (mk_sort_of a, s))
+    HOLogic.mk_Collect ("a", @{typ atom}, HOLogic.mk_eq (mk_sort_of a, s))
   end
 
 fun add_atom_decl (name : binding, arg : binding option) (thy : theory) =
@@ -48,15 +37,15 @@
 
     (* definition of atom and permute *)
     val newT = #abs_type (fst info);
-    val RepC = Const (Rep_name, newT --> atomT);
-    val AbsC = Const (Abs_name, atomT --> newT);
+    val RepC = Const (Rep_name, newT --> @{typ atom});
+    val AbsC = Const (Abs_name, @{typ atom} --> newT);
     val a = Free ("a", newT);
-    val p = Free ("p", permT);
+    val p = Free ("p", @{typ perm});
     val atom_eqn =
       HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_atom a, RepC $ a));
     val permute_eqn =
       HOLogic.mk_Trueprop (HOLogic.mk_eq
-        (mk_permute (p, a), AbsC $ (mk_permute (p, RepC $ a))));
+        (mk_perm p a, AbsC $ (mk_perm p (RepC $ a))));
     val atom_def_name =
       Binding.prefix_name "atom_" (Binding.suffix_name "_def" name);
     val permute_def_name =
diff -r 774d631726ad -r 84a13d1e2511 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Tue Apr 27 19:51:35 2010 +0200
+++ b/Nominal-General/nominal_library.ML	Tue Apr 27 22:21:16 2010 +0200
@@ -6,6 +6,8 @@
 
 signature NOMINAL_LIBRARY =
 sig
+
+
   val mk_minus: term -> term
   val mk_plus: term -> term -> term
 
@@ -14,6 +16,10 @@
   val mk_perm: term -> term -> term
   val dest_perm: term -> term * term
 
+  val mk_sort_of: term -> term
+  val mk_atom_ty: typ -> term -> term
+  val mk_atom: term -> term
+
   val mk_equiv: thm -> thm
   val safe_mk_equiv: thm -> thm
 end
@@ -38,9 +44,16 @@
 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
   | dest_perm t = raise TERM ("dest_perm", [t])
 
+
+fun mk_sort_of t = @{term "sort_of"} $ t;
+
+fun mk_atom_ty T t = Const (@{const_name atom}, T --> @{typ atom}) $ t;
+fun mk_atom t = mk_atom_ty (fastype_of t) t;
+
 fun mk_equiv r = r RS @{thm eq_reflection};
 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
 
+
 end (* structure *)
 
 open Nominal_Library;
\ No newline at end of file
diff -r 774d631726ad -r 84a13d1e2511 Nominal/NewFv.thy
--- a/Nominal/NewFv.thy	Tue Apr 27 19:51:35 2010 +0200
+++ b/Nominal/NewFv.thy	Tue Apr 27 22:21:16 2010 +0200
@@ -13,9 +13,8 @@
 
 ML {*
   open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);
-  (* TODO: It is the same as one in 'nominal_atoms' *)
-  fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom});
-  fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x];
+
+  fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom x];
   val noatoms = @{term "{} :: atom set"};
   fun mk_union sets =
     fold (fn a => fn b =>