(*  Title:      nominal_library.ML+
−
    Author:     Christian Urban+
−
+
−
  Basic function for nominal.+
−
*)+
−
+
−
signature NOMINAL_LIBRARY =+
−
sig+
−
  val mk_minus: term -> term+
−
  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 = +
−
 Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p+
−
+
−
fun mk_perm_ty ty p trm =+
−
  Const (@{const_name "permute"}, @{typ "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;+
−