1 (*  Title:      nominal_library.ML

     2     Author:     Christian Urban

     3 

     4   Basic function for nominal.

     5 *)

     6 

     7 signature NOMINAL_LIBRARY =

     8 sig

     9   val mk_minus: term -> term

    10   val mk_perm: term -> term -> term

    11   val dest_perm: term -> term * term

    12 

    13   val mk_equiv: thm -> thm

    14   val safe_mk_equiv: thm -> thm

    15 end

    16 

    17 

    18 structure Nominal_Library: NOMINAL_LIBRARY =

    19 struct

    20 

    21 fun mk_minus p = 

    22  Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p

    23 

    24 fun mk_perm p trm =

    25 let

    26   val ty = fastype_of trm

    27 in

    28   Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm

    29 end

    30 

    31 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)

    32   | dest_perm t = raise TERM ("dest_perm", [t])

    33 

    34 fun mk_equiv r = r RS @{thm eq_reflection};

    35 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;

    36 

    37 end (* structure *)

    38 

    39 open Nominal_Library;