--- a/Nominal/nominal_library.ML	Fri Dec 10 19:01:44 2010 +0000
+++ b/Nominal/nominal_library.ML	Sun Dec 12 00:10:40 2010 +0000
@@ -12,6 +12,7 @@
   val is_true: term -> bool
  
   val dest_listT: typ -> typ
+  val dest_fsetT: typ -> typ
 
   val mk_id: term -> term
 
@@ -34,6 +35,28 @@
   val mk_atom_ty: typ -> term -> term
   val mk_atom: term -> term
 
+  val mk_atom_set_ty: typ -> term -> term
+  val mk_atom_set: term -> term
+  val mk_atom_fset_ty: typ -> term -> term
+  val mk_atom_fset: term -> term
+  val mk_atom_list_ty: typ -> term -> term
+  val mk_atom_list: term -> term
+
+  val is_atom: Proof.context -> typ -> bool
+  val is_atom_set: Proof.context -> typ -> bool
+  val is_atom_fset: Proof.context -> typ -> bool
+  val is_atom_list: Proof.context -> typ -> bool
+
+  val setify_ty: Proof.context -> typ -> term -> term
+  val setify: Proof.context -> term -> term
+  val listify_ty: Proof.context -> typ -> term -> term
+  val listify: Proof.context -> term -> term
+
+  val fresh_ty: typ -> typ -> typ
+  val fresh_star_const: typ -> typ -> term
+  val mk_fresh_star_ty: typ -> typ -> term -> term -> term
+  val mk_fresh_star: term -> term -> term
+
   val supp_ty: typ -> typ
   val supp_const: typ -> term
   val mk_supp_ty: typ -> term -> term
@@ -110,6 +133,10 @@
 fun dest_listT (Type (@{type_name list}, [T])) = T
   | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])
 
+fun dest_fsetT (Type (@{type_name fset}, [T])) = T
+  | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
+
+
 fun mk_id trm =
   let 
     val ty = fastype_of trm
@@ -150,6 +177,79 @@
 fun mk_atom_ty ty t = atom_const ty $ t;
 fun mk_atom t = mk_atom_ty (fastype_of t) t;
 
+fun mk_atom_set_ty ty t =
+  let
+    val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"};
+    val img_ty = atom_ty --> ty --> @{typ "atom set"};
+  in
+    Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t
+  end
+
+fun mk_atom_fset_ty ty t =
+  let
+    val atom_ty = dest_fsetT ty
+    val fmap_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom fset"};
+    val fset = @{term "fset :: atom fset => atom set"}
+  in
+    fset $ (Const (@{const_name map_fset}, fmap_ty) $ (atom_const atom_ty) $ t)
+  end
+
+fun mk_atom_list_ty ty t =
+  let
+    val atom_ty = dest_listT ty
+    val map_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom list"}
+  in
+    Const (@{const_name map}, map_ty) $ (atom_const atom_ty) $ t
+  end
+
+fun mk_atom_set t = mk_atom_set_ty (fastype_of t) t
+fun mk_atom_fset t = mk_atom_fset_ty (fastype_of t) t
+fun mk_atom_list t = mk_atom_list_ty (fastype_of t) t
+
+
+
+(* testing for concrete atom types *)
+fun is_atom ctxt ty =
+  Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
+
+fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t
+  | is_atom_set _ _ = false;
+
+fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t
+  | is_atom_fset _ _ = false;
+
+fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t
+  | is_atom_list _ _ = false
+
+
+(* functions that coerces singletons, sets and fsets of concrete atoms
+   into sets of general atoms *)
+fun setify_ty ctxt ty t =
+  if is_atom ctxt ty
+    then  HOLogic.mk_set @{typ atom} [mk_atom_ty ty t]
+  else if is_atom_set ctxt ty
+    then mk_atom_set_ty ty t
+  else if is_atom_fset ctxt ty
+    then mk_atom_fset_ty ty t
+  else raise TERM ("setify", [t])
+
+(* functions that coerces singletons and lists of concrete atoms
+   into lists of general atoms  *)
+fun listify_ty ctxt ty t =
+  if is_atom ctxt ty
+    then HOLogic.mk_list @{typ atom} [mk_atom_ty ty t]
+  else if is_atom_list ctxt ty
+    then mk_atom_list_ty ty t
+  else raise TERM ("listify", [t])
+
+fun setify ctxt t = setify_ty ctxt (fastype_of t) t
+fun listify ctxt t = listify_ty ctxt (fastype_of t) t
+
+fun fresh_ty ty1 ty2 = [ty1, ty2] ---> @{typ bool}
+fun fresh_star_const ty1 ty2 = Const (@{const_name fresh_star}, fresh_ty ty1 ty2)
+fun mk_fresh_star_ty ty1 ty2 t1 t2 = fresh_star_const ty1 ty2 $ t1 $ t2
+fun mk_fresh_star t1 t2 = mk_fresh_star_ty (fastype_of t1) (fastype_of t2) t1 t2
+
 fun supp_ty ty = ty --> @{typ "atom set"};
 fun supp_const ty = Const (@{const_name supp}, supp_ty ty)
 fun mk_supp_ty ty t = supp_const ty $ t