File ‹Utils.ML›
signature Utils =
sig
val &&& : ('a -> 'b) * ('a -> 'c) -> 'a -> 'b * 'c
val *** : ('a -> 'b) * ('c -> 'd) -> 'a * 'c -> 'b * 'd
val @@ : ''a list * ''a list -> ''a list
val --- : ''a list * ''a list -> ''a list
val binop : term -> term -> term -> term
val add_: term -> term -> term
val add_to_context : string -> Proof.context -> Proof.context
val app_: term -> term -> term
val concat_: term -> term -> term
val dest_apply: term -> term * term
val dest_abs : string * typ * term -> string * term
val dest_iff_lhs: term -> term
val dest_iff_rhs: term -> term
val dest_iff_tms: term -> term * term
val dest_lhs_def: term -> term
val dest_rhs_def: term -> term
val dest_satisfies_tms: term -> term * term
val dest_satisfies_frm: term -> term
val dest_eq_tms: term -> term * term
val dest_mem_tms: term -> term * term
val dest_sats_frm: term -> (term * term) * term
val dest_eq_tms': term -> term * term
val dest_trueprop: term -> term
val print_theorem: Position.T -> (string * thm list) * Proof.context -> Proof.context
val eq_: term -> term -> term
val fix_vars: thm -> string list -> Proof.context -> thm
val flat : ''a list list -> ''a list
val formula_: term
val freeName: term -> string
val frees : term -> term list
val length_: term -> term
val list_: term -> term
val lt_: term -> term -> term
val map_option : ('a -> 'b) -> 'a option -> 'b option
val mem_: term -> term -> term
val mk_FinSet: term list -> term
val mk_Pair: term -> term -> term
val mk_ZFlist: ('a -> term) -> 'a list -> term
val mk_ZFnat: int -> term
val nat_: term
val nth_: term -> term -> term
val reachable : (''a -> ''a -> bool) -> ''a list -> ''a list -> ''a list
val subset_: term -> term -> term
val thm_concl_tm : Proof.context -> xstring -> (Vars.key * cterm) list * term * Proof.context
val to_ML_list: term -> term list
val tp: term -> term
val var_i : string -> term
val zip_with : ('a * 'b -> 'c) -> 'a list -> 'b list -> 'c list
end
structure Utils : Utils =
struct
fun binop h t u = h $ t $ u
val mk_Pair = binop @{const Pair}
fun mk_FinSet nil = @{const zero}
| mk_FinSet (e :: es) = @{const cons} $ e $ mk_FinSet es
fun mk_ZFnat 0 = @{const zero}
| mk_ZFnat n = @{const succ} $ mk_ZFnat (n-1)
fun mk_ZFlist _ nil = @{const "Nil"}
| mk_ZFlist f (t :: ts) = @{const "Cons"} $ f t $ mk_ZFlist f ts
fun to_ML_list (@{const Nil}) = nil
| to_ML_list (@{const Cons} $ t $ ts) = t :: to_ML_list ts
| to_ML_list _ = nil
fun freeName (Free (n,_)) = n
| freeName _ = error "Not a free variable"
val app_ = binop @{const apply}
fun tp x = @{const Trueprop} $ x
fun length_ env = @{const length} $ env
val nth_ = binop @{const nth}
val add_ = binop @{const add}
val mem_ = binop @{const mem}
val subset_ = binop @{const Subset}
val lt_ = binop @{const lt}
val concat_ = binop @{const app}
val eq_ = binop @{const IFOL.eq(i)}
fun list_ set = @{const list} $ set
val nat_ = @{const nat}
val formula_ = @{const formula}
fun dest_eq_tms (Const (@{const_name IFOL.eq},_) $ t $ u) = (t, u)
| dest_eq_tms t = raise TERM ("dest_eq_tms", [t])
fun dest_mem_tms (@{const mem} $ t $ u) = (t, u)
| dest_mem_tms t = raise TERM ("dest_mem_tms", [t])
fun dest_eq_tms' (Const (@{const_name Pure.eq},_) $ t $ u) = (t, u)
| dest_eq_tms' t = raise TERM ("dest_eq_tms", [t])
val dest_lhs_def = #1 o dest_eq_tms'
val dest_rhs_def = #2 o dest_eq_tms'
fun dest_apply (@{const apply} $ t $ u) = (t,u)
| dest_apply t = raise TERM ("dest_applies_op", [t])
fun dest_satisfies_tms (@{const Formula.satisfies} $ A $ f) = (A,f)
| dest_satisfies_tms t = raise TERM ("dest_satisfies_tms", [t]);
val dest_satisfies_frm = #2 o dest_satisfies_tms
fun dest_sats_frm t = t |> dest_eq_tms |> #1 |> dest_apply |>> dest_satisfies_tms ;
fun dest_trueprop (@{const IFOL.Trueprop} $ t) = t
| dest_trueprop t = t
fun dest_iff_tms (@{const IFOL.iff} $ t $ u) = (t, u)
| dest_iff_tms t = raise TERM ("dest_iff_tms", [t])
val dest_iff_lhs = #1 o dest_iff_tms
val dest_iff_rhs = #2 o dest_iff_tms
fun thm_concl_tm ctxt thm_ref =
let
val thm = Proof_Context.get_thm ctxt thm_ref
val thm_vars = rev (Term.add_vars (Thm.full_prop_of thm) [])
val (((_,inst),thm_tms),ctxt1) = Variable.import true [thm] ctxt
val vars = map (fn v => (v, the (Vars.lookup inst v))) thm_vars
in
(vars, thm_tms |> hd |> Thm.concl_of, ctxt1)
end
fun fix_vars thm vars ctxt = let
val (_, ctxt1) = Variable.add_fixes vars ctxt
in singleton (Proof_Context.export ctxt1 ctxt) thm
end
fun print_theorem pos (thms, lthy) =
(Proof_Display.print_theorem pos lthy thms; lthy)
infix 6 @@
fun op @@ (xs, ys) = union (op =) ys xs
fun flat xss = fold (curry op @@) xss []
infix 6 ---
fun op --- (xs, ys) = subtract (op =) ys xs
infix 6 &&&
fun op &&& (f, g) = fn x => (f x, g x)
infix 6 ***
fun op *** (f, g) = fn (x, y) => (f x, g y)
fun add_to_context v c = if Variable.is_fixed c v then c else #2 (Variable.add_fixes [v] c)
fun frees t = fold_aterms (fn t => if is_Free t then cons t else I) t []
fun reachable p u xs =
let
val step = map (fn x => filter (p x) (u --- xs)) xs |> flat
val acc = if null step then [] else reachable p (u --- xs) step
in
xs @@ acc
end
fun zip_with _ [] _ = []
| zip_with _ _ [] = []
| zip_with f (x :: xs) (y :: ys) = f (x, y) :: zip_with f xs ys
fun var_i s = Free (s, @{typ "i"})
fun map_option f (SOME a) = SOME (f a)
| map_option _ NONE = NONE
fun dest_abs (v, ty, t) = (v, Term.subst_bound ((Free (v, ty)), t))
end