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