10 use "nominal_dt_rawperm.ML"

    11 use "nominal_dt_rawfuns.ML"

    13 ML {*

    14 open Nominal_Dt_RawPerm

    15 open Nominal_Dt_RawFuns

    16 *}

    17 

    18 ML {*

    19 fun is_atom ctxt ty =

    20   Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})

    21 

    22 fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t

    23   | is_atom_set _ _ = false;

    24 

    25 fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t

    26   | is_atom_fset _ _ = false;

    27 

    28 fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t

    29   | is_atom_list _ _ = false

    30 

    31 

    32 (* functions for producing sets, fsets and lists of general atom type

    33    out from concrete atom types *)

    34 fun mk_atom_set t =

    35 let

    36   val ty = fastype_of t;

    37   val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"};

    38   val img_ty = atom_ty --> ty --> @{typ "atom set"};

    39 in

    40   Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t

    41 end

    42 

    43 fun mk_atom_fset t =

    44 let

    45   val ty = fastype_of t;

    46   val atom_ty = dest_fsetT ty --> @{typ "atom"};

    47   val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};

    48   val fset_to_set = @{term "fset_to_set :: atom fset => atom set"}

    49 in

    50   fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)

    51 end

    52 *}