--- a/Nominal/Perm.thy	Sun May 23 02:15:24 2010 +0100
+++ b/Nominal/Perm.thy	Mon May 24 20:02:37 2010 +0100
@@ -1,10 +1,55 @@
 theory Perm
 imports 
   "../Nominal-General/Nominal2_Base"
-  "../Nominal-General/Nominal2_Atoms"
+  "../Nominal-General/Nominal2_Atoms" 
+  "Nominal2_FSet"
+uses ("nominal_dt_rawperm.ML")
+     ("nominal_dt_rawfuns.ML")
 begin
 
+use "nominal_dt_rawperm.ML"
+use "nominal_dt_rawfuns.ML"
 
+ML {*
+open Nominal_Dt_RawPerm
+open Nominal_Dt_RawFuns
+*}
+
+ML {*
+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 for producing sets, fsets and lists of general atom type
+   out from concrete atom types *)
+fun mk_atom_set t =
+let
+  val ty = fastype_of t;
+  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 t =
+let
+  val ty = fastype_of t;
+  val atom_ty = dest_fsetT ty --> @{typ "atom"};
+  val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};
+  val fset_to_set = @{term "fset_to_set :: atom fset => atom set"}
+in
+  fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
+end
+*}
 (* permutations for quotient types *)
 
 ML {* Class_Target.prove_instantiation_exit_result *}