(* Title: nominal_basic.ML Author: Christian Urban Basic functions for nominal.*)infix 1 ||>>> |>>>signature NOMINAL_BASIC =sig val trace: bool Unsynchronized.ref val trace_msg: (unit -> string) -> unit val |>>> : 'a * ('a -> 'b * 'c) -> 'b list * 'c val ||>>> : ('a list * 'b) * ('b -> 'a * 'b) -> 'a list * 'b val last2: 'a list -> 'a * 'a val split_triples: ('a * 'b * 'c) list -> ('a list * 'b list * 'c list) 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 * termendstructure Nominal_Basic: NOMINAL_BASIC =structval trace = Unsynchronized.ref falsefun trace_msg msg = if ! trace then tracing (msg ()) else ()infix 1 ||>>> |>>>fun (x |>>> f) = let val (x', y') = f x in ([x'], y') endfun (([], y) ||>>> f) = ([], y) | ((xs, y) ||>>> f) = let val (x', y') = f y in (xs @ [x'], y') end(* 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 xsfun split_triples xs = fold (fn (a, b, c) => fn (axs, bxs, cxs) => (a :: axs, b :: bxs, c :: cxs)) xs ([], [], [])fun last2 [] = raise Empty | last2 [_] = raise Empty | last2 [x, y] = (x, y) | last2 (_ :: xs) = last2 xsfun split_last2 xs = let val (xs', x) = split_last xs val (xs'', y) = split_last xs' in (xs'', y, x) endfun map4 _ [] [] [] [] = [] | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs usfun 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) zfun 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) $ trmfun mk_all (a, T) t = Logic.all_const 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"} $ pfun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ qfun perm_ty ty = @{typ "perm"} --> ty --> tyfun perm_const ty = Const (@{const_name "permute"}, perm_ty ty)fun mk_perm_ty ty p trm = perm_const ty $ p $ trmfun mk_perm p trm = mk_perm_ty (fastype_of trm) p trmfun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) | dest_perm t = raise TERM ("dest_perm", [t]);end (* structure *)open Nominal_Basic;