(*  Title:      nominal_library.ML

    Author:     Christian Urban

  Basic functions for nominal.

*)

signature NOMINAL_LIBRARY =

sig

  val mk_minus: term -> term

  val mk_plus: term -> term -> term

  val perm_ty: typ -> typ 

  val mk_perm_ty: typ -> term -> term -> term

  val mk_perm: term -> term -> term

  val dest_perm: term -> term * term

  val mk_sort_of: term -> term

  val atom_ty: typ -> typ

  val mk_atom_ty: typ -> term -> term

  val mk_atom: term -> term

  val supp_ty: typ -> typ

  val mk_supp_ty: typ -> term -> term

  val mk_supp: term -> term

  val mk_equiv: thm -> thm

  val safe_mk_equiv: thm -> thm

end

structure Nominal_Library: NOMINAL_LIBRARY =

struct

fun mk_minus p = @{term "uminus::perm => perm"} $ p;

fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q;

fun perm_ty ty = @{typ "perm"} --> ty --> ty; 

fun mk_perm_ty ty p trm = Const (@{const_name "permute"}, perm_ty ty) $ p $ trm;

fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm;

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 atom_ty ty = ty --> @{typ "atom"};

fun mk_atom_ty ty t = Const (@{const_name "atom"}, atom_ty ty) $ t;

fun mk_atom t = mk_atom_ty (fastype_of t) t;

fun supp_ty ty = ty --> @{typ "atom set"};

fun mk_supp_ty ty t = Const (@{const_name "supp"}, supp_ty ty) $ t;

fun mk_supp t = mk_supp_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;