File ‹TPTP_Parser/tptp_reconstruct_library.ML›
signature TPTP_RECONSTRUCT_LIBRARY =
sig
exception BREAK_LIST
val break_list : 'a list -> 'a * 'a list
val break_seq : 'a Seq.seq -> 'a * 'a Seq.seq
exception MULTI_ELEMENT_LIST
val cascaded_filter_single : bool -> ('a list -> 'a list) list -> 'a list -> 'a option
val concat_between : 'a list list -> ('a option * 'a option) -> 'a list
exception DIFF_TYPE of typ * typ
exception DIFF of term * term
val diff :
theory ->
term * term -> (term * term) list * (typ * typ) list
exception DISPLACE_KV
val displace_kv : ''a -> (''a * 'b) list -> (''a * 'b) list
val enumerate : int -> 'a list -> (int * 'a) list
val fold_options : 'a option list -> 'a list
val find_and_remove : ('a -> bool) -> 'a list -> 'a * 'a list
val lift_option : ('a -> 'b) -> 'a option -> 'b option
val list_diff : ''a list -> ''a list -> ''a list
val list_prod : 'a list list -> 'a list -> 'a list -> 'a list list
val permute : ''a list -> ''a list list
val prefix_intersection_list :
''a list -> ''a list -> ''a list
val repeat_until_fixpoint : (''a -> ''a) -> ''a -> ''a
val switch : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
val zip_amap :
'a list ->
'b list ->
('a * 'b) list -> ('a * 'b) list * ('a list * 'b list)
val consts_in : term -> term list
val head_quantified_variable : Proof.context -> int -> thm -> (string * typ) option
val push_allvar_in : string -> term -> term
val strip_top_All_var : term -> (string * typ) * term
val strip_top_All_vars : term -> (string * typ) list * term
val strip_top_all_vars :
(string * typ) list -> term -> (string * typ) list * term
val trace_tac' : Proof.context -> string ->
('a -> thm -> 'b Seq.seq) -> 'a -> thm -> 'b Seq.seq
val try_dest_Trueprop : term -> term
val type_devar : typ TVars.table -> term -> term
val diff_and_instantiate : Proof.context -> thm -> term -> term -> thm
val batter_tac : Proof.context -> int -> tactic
val break_hypotheses_tac : Proof.context -> int -> tactic
val clause_breaker_tac : Proof.context -> int -> tactic
val reassociate_conjs_tac : Proof.context -> int -> tactic
val ASAP : (int -> tactic) -> (int -> tactic) -> int -> tactic
val COND' :
('a -> thm -> bool) ->
('a -> tactic) -> ('a -> tactic) -> 'a -> tactic
val TERMFUN :
(term list * term -> 'a) -> int option -> thm -> 'a list
val TERMPRED :
(term -> bool) ->
(term -> bool) -> int option -> thm -> bool
val guided_abstract :
bool -> term -> term -> ((string * typ) * term) * term list
val abstract :
term list -> term -> ((string * typ) * term) list * term
end
structure TPTP_Reconstruct_Library : TPTP_RECONSTRUCT_LIBRARY =
struct
fun zip_amap [] ys acc = (acc, ([], ys))
| zip_amap xs [] acc = (acc, (xs, []))
| zip_amap (x :: xs) (y :: ys) acc =
zip_amap xs ys ((x, y) :: acc);
fun enumerate n ls =
let
fun enumerate' [] _ acc = acc
| enumerate' (x :: xs) n acc = enumerate' xs (n + 1) ((n, x) :: acc)
in
enumerate' ls n []
|> rev
end
fun list_diff l1 l2 =
filter (fn x => forall (fn y => x <> y) l2) l1
val _ = \<^assert>
(list_diff [1,2,3] [2,4] = [1, 3])
fun list_prod acc [] _ = rev acc
| list_prod acc (x :: xs) ys = list_prod ((x :: ys) :: acc) xs ys
fun repeat_until_fixpoint f x =
let
val x' = f x
in
if x = x' then x else repeat_until_fixpoint f x'
end
fun permute l =
let
fun permute' (l, []) = [(l, [])]
| permute' (l, xs) =
map (fn x => (x :: l, filter (fn y => y <> x) xs)) xs
|> maps permute'
in
permute' ([], l)
|> map fst
end
exception DISPLACE_KV;
local
fun fold_fun k (kv as (k', v)) (l, buff) =
if is_some buff then (kv :: l, buff)
else
if k = k' then
(l, SOME kv)
else
(kv :: l, buff)
in
fun displace_kv k alist =
let
val (pre_alist, kv) = fold (fold_fun k) alist ([], NONE)
in
if is_some kv then
the kv :: rev pre_alist
else raise DISPLACE_KV
end
end
local
fun prefix_intersection_list' (acc_pre, acc_pro) l1 l2 =
if null l1 then
List.rev acc_pre @ List.rev acc_pro
else if null l2 then
List.rev acc_pre @ l1 @ List.rev acc_pro
else
let val l1_hd = hd l1
in
prefix_intersection_list'
(if member (op =) l2 l1_hd then
(l1_hd :: acc_pre, acc_pro)
else
(acc_pre, l1_hd :: acc_pro))
(tl l1) l2
end
in
fun prefix_intersection_list l1 l2 = prefix_intersection_list' ([], []) l1 l2
end;
val _ = \<^assert>
(prefix_intersection_list [1,2,3,4,5] [1,3,5] = [1, 3, 5, 2, 4]);
val _ = \<^assert>
(prefix_intersection_list [1,2,3,4,5] [] = [1,2,3,4,5]);
val _ = \<^assert>
(prefix_intersection_list [] [1,3,5] = [])
fun switch f y x = f x y
fun fold_options opt_list =
fold
(fn x => fn l => if is_some x then the x :: l else l)
opt_list
[];
val _ = \<^assert>
([2,0,1] =
fold_options [NONE, SOME 1, NONE, SOME 0, NONE, NONE, SOME 2]);
fun lift_option (f : 'a -> 'b) (x_opt : 'a option) : 'b option =
case x_opt of
NONE => NONE
| SOME x => SOME (f x)
fun break_seq x = (Seq.hd x, Seq.tl x)
exception BREAK_LIST
fun break_list (x :: xs) = (x, xs)
| break_list _ = raise BREAK_LIST
exception MULTI_ELEMENT_LIST
fun cascaded_filter_single strict preds l =
case preds of
[] => NONE
| (p :: ps) =>
case p l of
[] => cascaded_filter_single strict ps l
| [x] => SOME x
| l =>
if strict then raise MULTI_ELEMENT_LIST
else cascaded_filter_single strict ps l
fun concat_between [] _ = []
| concat_between [l] _ = l
| concat_between (l :: ls) (seps as (bef, aft)) =
let
val pre = if is_some bef then the bef :: l else l
val mid = if is_some aft then [the aft] else []
val post = concat_between ls seps
in
pre @ mid @ post
end
fun find_and_remove pred l =
find_index pred l
|> switch chop l
|> apsnd break_list
|> (fn (xs, (y, ys)) => (y, xs @ ys))
val _ = \<^assert> (find_and_remove (curry (op =) 3) [0,1,2,3,4,5] = (3, [0,1,2,4,5]))
local
fun try_dest_All (Const (\<^const_name>‹HOL.All›, _) $ t) = t
| try_dest_All (Const (\<^const_name>‹HOL.Trueprop›, _) $ t) = try_dest_All t
| try_dest_All t = t
val _ = \<^assert>
((\<^term>‹∀x. (∀y. P) = True›
|> try_dest_All
|> Term.strip_abs_vars)
= [("x", \<^typ>‹'a›)])
val _ = \<^assert>
((\<^prop>‹∀x. (∀y. P) = True›
|> try_dest_All
|> Term.strip_abs_vars)
= [("x", \<^typ>‹'a›)])
fun strip_top_All_vars' once acc t =
let
val t' = try_dest_All t
val var =
try (Term.strip_abs_vars #> hd) t'
fun strip v t =
(v, subst_bounds ([Free v], Term.strip_abs_body t))
in
if t' = t orelse is_none var then (acc, t)
else
let
val (v, t) = strip (the var) t'
val acc' = v :: acc
in
if once then (acc', t)
else strip_top_All_vars' once acc' t
end
end
in
fun strip_top_All_vars t = strip_top_All_vars' false [] t
val _ =
let
val answer =
([("x", \<^typ>‹'a›)],
HOLogic.all_const \<^typ>‹'a› $
(HOLogic.eq_const \<^typ>‹'a› $
Free ("x", \<^typ>‹'a›)))
in
\<^assert>
((\<^term>‹∀x. All ((=) x)›
|> strip_top_All_vars)
= answer)
end
fun strip_top_All_var t =
strip_top_All_vars' true [] t
|> apfst the_single
end
fun strip_top_all_vars acc t =
if Logic.is_all t then
let
val (v, t') = Logic.dest_all_global t
in
strip_top_all_vars (v :: acc) t'
end
else (acc,
t)
fun push_allvar_in v t =
let
val (vs, t') = strip_top_All_vars t
val vs' = displace_kv v vs
in
fold (fn (v, ty) => fn t =>
HOLogic.mk_all (v, ty, t)) vs' t'
end
fun consts_in (Const c) = [Const c]
| consts_in (Free _) = []
| consts_in (Var _) = []
| consts_in (Bound _) = []
| consts_in (Abs (_, _, t)) = consts_in t
| consts_in (t1 $ t2) = union (op =) (consts_in t1) (consts_in t2);
exception DIFF of term * term
exception DIFF_TYPE of typ * typ
fun diff thy (initial as (t_gen, t)) =
let
fun diff_ty acc [] = acc
| diff_ty acc ((pair as (ty_gen, ty)) :: ts) =
case pair of
(Type (s1, ty_gens1), Type (s2, ty_gens2)) =>
if s1 <> s2 orelse
length ty_gens1 <> length ty_gens2 then
raise (DIFF (t_gen, t))
else
diff_ty acc
(ts @ ListPair.zip (ty_gens1, ty_gens2))
| (TFree (s1, so1), TFree (s2, so2)) =>
if s1 <> s2 orelse
not (Sign.subsort thy (so2, so1)) then
raise (DIFF (t_gen, t))
else
diff_ty acc ts
| (TVar (idx1, so1), TVar (idx2, so2)) =>
if idx1 <> idx2 orelse
not (Sign.subsort thy (so2, so1)) then
raise (DIFF (t_gen, t))
else
diff_ty acc ts
| (TFree _, _) => diff_ty (pair :: acc) ts
| (TVar _, _) => diff_ty (pair :: acc) ts
| _ => raise (DIFF_TYPE pair)
fun diff' (acc as (acc_t, acc_ty)) (pair as (t_gen, t)) ts =
case pair of
(Const (s1, ty1), Const (s2, ty2)) =>
if s1 <> s2 orelse
not (Sign.typ_instance thy (ty2, ty1)) then
raise (DIFF (t_gen, t))
else
diff_probs acc ts
| (Free (s1, ty1), Free (s2, ty2)) =>
if s1 <> s2 orelse
not (Sign.typ_instance thy (ty2, ty1)) then
raise (DIFF (t_gen, t))
else
diff_probs acc ts
| (Var (idx1, ty1), Var (idx2, ty2)) =>
if idx1 <> idx2 orelse
not (Sign.typ_instance thy (ty2, ty1)) then
raise (DIFF (t_gen, t))
else
diff_probs acc ts
| (Bound i1, Bound i2) =>
if i1 <> i2 then
raise (DIFF (t_gen, t))
else
diff_probs acc ts
| (Abs (s1, ty1, t1), Abs (s2, ty2, t2)) =>
if s1 <> s2 orelse
not (Sign.typ_instance thy (ty2, ty1)) then
raise (DIFF (t_gen, t))
else
diff' acc (t1, t2) ts
| (ta1 $ ta2, tb1 $ tb2) =>
diff_probs acc ((ta1, tb1) :: (ta2, tb2) :: ts)
| (Free (_, ty), _) =>
diff_probs
(pair :: acc_t,
diff_ty acc_ty [(ty, Term.fastype_of t)])
ts
| (Var (_, ty), _) =>
diff_probs
(pair :: acc_t,
diff_ty acc_ty [(ty, Term.fastype_of t)])
ts
| _ => raise (DIFF (t_gen, t))
and diff_probs acc ts =
case ts of
[] => acc
| (pair :: ts') => diff' acc pair ts'
in
diff_probs ([], []) [initial]
end
fun guided_abstract strong t_sub t =
let
val varnames = Term.add_frees t [] |> map #1
val prefixK = "v"
val freshvar =
let
fun find_fresh i =
let
val varname = prefixK ^ Int.toString i
in
if member (op =) varnames varname then
find_fresh (i + 1)
else
(varname, fastype_of t_sub)
end
in
find_fresh 0
end
fun guided_abstract' t =
case t of
Abs (s, ty, t') =>
if t = t_sub then [Free freshvar]
else
(map (fn t' => Abs (s, ty, t'))
(guided_abstract' t'))
| t1 $ t2 =>
if t = t_sub then [Free freshvar]
else
(map (fn t' => t' $ t2)
(guided_abstract' t1)) @
(map (fn t' => t1 $ t')
(guided_abstract' t2))
| _ =>
if t = t_sub then [Free freshvar]
else [t]
fun guided_abstract_strong' t =
let
fun continue t = guided_abstract_strong' t
|> (fn x => if null x then t
else the_single x)
in
case t of
Abs (s, ty, t') =>
if t = t_sub then [Free freshvar]
else
[Abs (s, ty, continue t')]
| t1 $ t2 =>
if t = t_sub then [Free freshvar]
else
[continue t1 $ continue t2]
| _ =>
if t = t_sub then [Free freshvar]
else [t]
end
in
((freshvar, t_sub),
if strong then guided_abstract_strong' t
else guided_abstract' t)
end
fun abstract ts t =
fold_map (apsnd the_single oo (guided_abstract true)) ts t
|> (fn (v_and_ts, t') =>
let
val (vs, ts) = ListPair.unzip v_and_ts
val vs' =
Term.add_frees t' []
|> list_diff vs
|> list_diff vs
val v'_and_ts =
map (fn v =>
(v, AList.lookup (op =) v_and_ts v |> the))
vs'
in
(v'_and_ts, t')
end)
fun type_devar tyenv (t : term) : term =
case t of
Const (s, ty) => Const (s, Term_Subst.instantiateT tyenv ty)
| Free (s, ty) => Free (s, Term_Subst.instantiateT tyenv ty)
| Var (idx, ty) => Var (idx, Term_Subst.instantiateT tyenv ty)
| Bound _ => t
| Abs (s, ty, t') =>
Abs (s, Term_Subst.instantiateT tyenv ty, type_devar tyenv t')
| t1 $ t2 => type_devar tyenv t1 $ type_devar tyenv t2
fun diff_and_instantiate ctxt scheme_thm scheme_t instance_t =
let
val (term_pairing, type_pairing) =
diff (Proof_Context.theory_of ctxt) (scheme_t, instance_t)
val typeval = map (fn (v, T) => (dest_TVar v, Thm.ctyp_of ctxt T)) type_pairing
val typeval_env =
TVars.make (map (apfst dest_TVar) type_pairing)
val termval =
map (apfst (dest_Var o type_devar typeval_env)) term_pairing
|> map (apsnd (Thm.cterm_of ctxt))
in
Thm.instantiate (TVars.make typeval, Vars.make termval) scheme_thm
end
val try_dest_Trueprop = perhaps (try HOLogic.dest_Trueprop)
fun COND' sat' tac'1 tac'2 i =
COND (sat' i) (tac'1 i) (tac'2 i)
fun ASAP wittler (tac : int -> tactic) (i : int) = fn st =>
let
val tac_result = tac i st
val pulled_tac_result = Seq.pull tac_result
val tac_failed =
is_none pulled_tac_result orelse
not (has_fewer_prems 1 (fst (the pulled_tac_result)))
in
if tac_failed then (wittler THEN' ASAP wittler tac) i st
else tac_result
end
fun break_hypotheses_tac ctxt =
CHANGED o
((REPEAT_DETERM o eresolve_tac ctxt @{thms conjE}) THEN'
(REPEAT_DETERM o eresolve_tac ctxt @{thms disjE}))
fun clause_breaker_tac ctxt =
(REPEAT o resolve_tac ctxt @{thms disjI1 disjI2 conjI}) THEN'
assume_tac ctxt
fun batter_tac ctxt i =
break_hypotheses_tac ctxt i THEN
ALLGOALS (TRY o clause_breaker_tac ctxt)
fun dist_all_and_tac ctxt i =
let
val simpset =
empty_simpset ctxt
|> Simplifier.add_simp
@{lemma "∀x. P x ∧ Q x ≡ (∀x. P x) ∧ (∀x. Q x)"
by (rule eq_reflection, auto)}
in
CHANGED (asm_full_simp_tac simpset i)
end
fun reassociate_conjs_tac ctxt =
asm_full_simp_tac
(Simplifier.add_simp
@{lemma "(A & B) & C == A & B & C" by auto}
(Raw_Simplifier.empty_simpset ctxt))
#> CHANGED
#> REPEAT_DETERM
fun head_quantified_variable ctxt i = fn st =>
let
val gls =
Thm.prop_of st
|> Logic.strip_horn
|> fst
val hypos =
if null gls then []
else
rpair (i - 1) gls
|> uncurry nth
|> strip_top_all_vars []
|> snd
|> Logic.strip_horn
|> fst
fun foralls_of_hd_hypos () =
hd hypos
|> try_dest_Trueprop
|> strip_top_All_vars
|> #1
|> rev
val quantified_variables = foralls_of_hd_hypos ()
in
if null hypos orelse null quantified_variables then NONE
else SOME (hd quantified_variables)
end
fun TERMFUN
(fun_over_terms : term list * term -> 'a)
(i_opt : int option) : thm -> 'a list = fn st =>
let
val t_raws =
Thm.prop_of st
|> strip_top_all_vars []
|> snd
|> Logic.strip_horn
|> fst
in
if null t_raws then []
else
let
val ts =
let
val stripper =
strip_top_all_vars []
#> snd
#> Logic.strip_horn
#> apsnd try_dest_Trueprop
#> apfst (map try_dest_Trueprop)
in
map stripper t_raws
end
in
case i_opt of
NONE =>
map fun_over_terms ts
| SOME i =>
nth ts (i - 1)
|> fun_over_terms
|> single
end
end
fun TERMPRED
(hyp_pred_over_terms : term -> bool)
(conc_pred_over_terms : term -> bool)
(i_opt : int option) : thm -> bool = fn st =>
let
val hyp_results =
TERMFUN (fst
#> map hyp_pred_over_terms) i_opt st
val conc_results =
TERMFUN (snd
#> conc_pred_over_terms) i_opt st
val _ = \<^assert> (length hyp_results = length conc_results)
in
if null hyp_results then true
else
let
val hyps_conjoined =
fold (fn a => fn b =>
b andalso (forall (fn x => x) a)) hyp_results true
val concs_conjoined =
fold (fn a => fn b =>
b andalso a) conc_results true
in hyps_conjoined andalso concs_conjoined end
end
fun trace_tac' ctxt msg tac i st =
let
val result = tac i st
in
if Config.get ctxt tptp_trace_reconstruction andalso
not (is_none (Seq.pull result)) then
(tracing msg; result)
else result
end
end