(*  Title:      nominal_library.ML
    Author:     Christian Urban

  Basic function 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_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_equiv r = r RS @{thm eq_reflection};
fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;

end (* structure *)

open Nominal_Library;