9   val trace: bool Unsynchronized.ref

    10   val trace_msg: (unit -> string) -> unit

    11 

    12   val last2: 'a list -> 'a * 'a

    13   val split_last2: 'a list -> 'a list * 'a * 'a

    14   val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list

    15   val order_default: ('a * 'a -> bool) -> 'b -> 'a list -> ('a * 'b) list -> 'b list

    16   val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list

    17   val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list

    18   val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list

    19   val fold_left: ('a * 'a -> 'a) -> 'a list -> 'a -> 'a

    20   

    21   val is_true: term -> bool

    22  

    23   val dest_listT: typ -> typ

    24   val dest_fsetT: typ -> typ

    25 

    26   val mk_id: term -> term

    27   val mk_all: (string * typ) -> term -> term

    28   val mk_All: (string * typ) -> term -> term

    29   val mk_exists: (string * typ) -> term -> term

    30 

    31   val sum_case_const: typ -> typ -> typ -> term

    32   val mk_sum_case: term -> term -> term

    33  

    34   val mk_minus: term -> term

    35   val mk_plus: term -> term -> term

    36 

    37   val perm_ty: typ -> typ 

    38   val perm_const: typ -> term

    39   val mk_perm_ty: typ -> term -> term -> term

    40   val mk_perm: term -> term -> term

    41   val dest_perm: term -> term * term

    42 

    94   val mk_equiv: thm -> thm

    95   val safe_mk_equiv: thm -> thm

    96 

   146 

   147 val trace = Unsynchronized.ref false

   148 fun trace_msg msg = if ! trace then tracing (msg ()) else ()

   149 

   150 

   151 (* orders an AList according to keys - every key needs to be there *)

   152 fun order eq keys list = 

   153   map (the o AList.lookup eq list) keys

   154 

   155 (* orders an AList according to keys - returns default for non-existing keys *)

   156 fun order_default eq default keys list = 

   157   map (the_default default o AList.lookup eq list) keys

   158 

   159 (* remove duplicates *)

   160 fun remove_dups eq [] = []

   161   | remove_dups eq (x :: xs) = 

   162       if member eq xs x 

   163       then remove_dups eq xs 

   164       else x :: remove_dups eq xs

   165 

   166 fun last2 [] = raise Empty

   167   | last2 [_] = raise Empty

   168   | last2 [x, y] = (x, y)

   169   | last2 (_ :: xs) = last2 xs

   170 

   171 fun split_last2 xs = 

   172   let

   173     val (xs', x) = split_last xs

   174     val (xs'', y) = split_last xs'

   175   in

   176     (xs'', y, x)

   177   end

   178 

   179 fun map4 _ [] [] [] [] = []

   180   | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us

   181 

   182 fun split_filter f [] = ([], [])

   183   | split_filter f (x :: xs) =

   184       let 

   185         val (r, l) = split_filter f xs 

   186       in 

   187         if f x 

   188         then (x :: r, l) 

   189         else (r, x :: l) 

   190       end

   191 

   192 (* to be used with left-infix binop-operations *)

   193 fun fold_left f [] z = z

   194   | fold_left f [x] z = x

   195   | fold_left f (x :: y :: xs) z = fold_left f (f (x, y) :: xs) z

   196 

   197 

   198 

   199 fun is_true @{term "Trueprop True"} = true

   200   | is_true _ = false 

   201 

   202 fun dest_listT (Type (@{type_name list}, [T])) = T

   203   | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])

   204 

   205 fun dest_fsetT (Type (@{type_name fset}, [T])) = T

   206   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);

   207 

   208 

   209 fun mk_id trm = HOLogic.id_const (fastype_of trm) $ trm

   210 

   211 fun mk_all (a, T) t =  Term.all T $ Abs (a, T, t)

   212 

   213 fun mk_All (a, T) t =  HOLogic.all_const T $ Abs (a, T, t)

   214 

   215 fun mk_exists (a, T) t =  HOLogic.exists_const T $ Abs (a, T, t)

   216 

   217 fun sum_case_const ty1 ty2 ty3 = 

   218   Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3)

   219 

   220 fun mk_sum_case trm1 trm2 =

   221   let

   222     val ([ty1], ty3) = strip_type (fastype_of trm1)

   223     val ty2 = domain_type (fastype_of trm2)

   224   in

   225     sum_case_const ty1 ty2 ty3 $ trm1 $ trm2

   226   end 

   227 

   228 

   229 

   230 fun mk_minus p = @{term "uminus::perm => perm"} $ p

   231 

   232 fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q

   233 

   234 fun perm_ty ty = @{typ "perm"} --> ty --> ty

   235 fun perm_const ty  = Const (@{const_name "permute"}, perm_ty ty)

   236 fun mk_perm_ty ty p trm = perm_const ty $ p $ trm

   237 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm

   238 

   239 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)

   240   | dest_perm t = raise TERM ("dest_perm", [t]);

   359 

   360 

   361 fun mk_equiv r = r RS @{thm eq_reflection};

   362 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;