(* Title: nominal_basic.ML+ −
Author: Christian Urban+ −
+ −
Basic functions for nominal.+ −
*)+ −
+ −
signature NOMINAL_BASIC =+ −
sig+ −
val trace: bool Unsynchronized.ref+ −
val trace_msg: (unit -> string) -> unit+ −
+ −
val last2: 'a list -> 'a * 'a+ −
val split_last2: 'a list -> 'a list * 'a * 'a+ −
val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list+ −
val order_default: ('a * 'a -> bool) -> 'b -> 'a list -> ('a * 'b) list -> 'b list+ −
val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list+ −
val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list+ −
val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list+ −
val fold_left: ('a * 'a -> 'a) -> 'a list -> 'a -> 'a+ −
+ −
val is_true: term -> bool+ −
+ −
val dest_listT: typ -> typ+ −
val dest_fsetT: typ -> typ+ −
+ −
val mk_id: term -> term+ −
val mk_all: (string * typ) -> term -> term+ −
val mk_All: (string * typ) -> term -> term+ −
val mk_exists: (string * typ) -> term -> term+ −
+ −
val sum_case_const: typ -> typ -> typ -> term+ −
val mk_sum_case: term -> term -> term+ −
+ −
val mk_equiv: thm -> thm+ −
val safe_mk_equiv: thm -> thm+ −
+ −
val mk_minus: term -> term+ −
val mk_plus: term -> term -> term+ −
+ −
val perm_ty: typ -> typ + −
val perm_const: typ -> term+ −
val mk_perm_ty: typ -> term -> term -> term+ −
val mk_perm: term -> term -> term+ −
val dest_perm: term -> term * term+ −
+ −
end+ −
+ −
+ −
structure Nominal_Basic: NOMINAL_BASIC =+ −
struct+ −
+ −
val trace = Unsynchronized.ref false+ −
fun trace_msg msg = if ! trace then tracing (msg ()) else ()+ −
+ −
+ −
(* orders an AList according to keys - every key needs to be there *)+ −
fun order eq keys list = + −
map (the o AList.lookup eq list) keys+ −
+ −
(* orders an AList according to keys - returns default for non-existing keys *)+ −
fun order_default eq default keys list = + −
map (the_default default o AList.lookup eq list) keys+ −
+ −
(* remove duplicates *)+ −
fun remove_dups eq [] = []+ −
| remove_dups eq (x :: xs) = + −
if member eq xs x + −
then remove_dups eq xs + −
else x :: remove_dups eq xs+ −
+ −
fun last2 [] = raise Empty+ −
| last2 [_] = raise Empty+ −
| last2 [x, y] = (x, y)+ −
| last2 (_ :: xs) = last2 xs+ −
+ −
fun split_last2 xs = + −
let+ −
val (xs', x) = split_last xs+ −
val (xs'', y) = split_last xs'+ −
in+ −
(xs'', y, x)+ −
end+ −
+ −
fun map4 _ [] [] [] [] = []+ −
| map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us+ −
+ −
fun split_filter f [] = ([], [])+ −
| split_filter f (x :: xs) =+ −
let + −
val (r, l) = split_filter f xs + −
in + −
if f x + −
then (x :: r, l) + −
else (r, x :: l) + −
end+ −
+ −
(* to be used with left-infix binop-operations *)+ −
fun fold_left f [] z = z+ −
| fold_left f [x] z = x+ −
| fold_left f (x :: y :: xs) z = fold_left f (f (x, y) :: xs) z+ −
+ −
+ −
+ −
fun is_true @{term "Trueprop True"} = true+ −
| is_true _ = false + −
+ −
fun dest_listT (Type (@{type_name list}, [T])) = T+ −
| dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])+ −
+ −
fun dest_fsetT (Type (@{type_name fset}, [T])) = T+ −
| dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);+ −
+ −
+ −
fun mk_id trm = HOLogic.id_const (fastype_of trm) $ trm+ −
+ −
fun mk_all (a, T) t = Term.all T $ Abs (a, T, t)+ −
+ −
fun mk_All (a, T) t = HOLogic.all_const T $ Abs (a, T, t)+ −
+ −
fun mk_exists (a, T) t = HOLogic.exists_const T $ Abs (a, T, t)+ −
+ −
fun sum_case_const ty1 ty2 ty3 = + −
Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3)+ −
+ −
fun mk_sum_case trm1 trm2 =+ −
let+ −
val ([ty1], ty3) = strip_type (fastype_of trm1)+ −
val ty2 = domain_type (fastype_of trm2)+ −
in+ −
sum_case_const ty1 ty2 ty3 $ trm1 $ trm2+ −
end + −
+ −
+ −
fun mk_equiv r = r RS @{thm eq_reflection};+ −
fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;+ −
+ −
+ −
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 perm_const ty = Const (@{const_name "permute"}, perm_ty ty)+ −
fun mk_perm_ty ty p trm = perm_const 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]);+ −
+ −
end (* structure *)+ −
+ −
open Nominal_Basic;+ −