(* 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;+ −