(* Title: HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Author: Nik Sultana, Cambridge University Computer Laboratory Collection of general functions used in the reconstruction module.
*)
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 listlist val permute : ''a list -> ''a listlist 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 dist_all_and_tac : Proof.context -> int -> tactic *)(*FIXME unused*) 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
(*zip as much as possible*) 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);
(*Pair a list up with the position number of each element,
starting from n*) 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 repeat_until_fixpoint f x = let val x' = f x in if x = x' then x else repeat_until_fixpoint f x' end
(*compute all permutations of a list*) 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 (* permute [1,2,3]; permute ["A", "B"]
*)
(*this exception is raised when the pair we wish to displace
isn't found in the association list*)
exception DISPLACE_KV; (*move a key-value pair, determined by the k, to the beginning of an association list. it moves the first occurrence of a pair
keyed by "k"*)
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 (*"k" is the key value of the pair we wish to displace*) 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 elseraise DISPLACE_KV end end
(*Given two lists, it generates a new list where the intersection of the lists forms the prefix
of the new list.*)
local fun prefix_intersection_list' (acc_pre, acc_pro) l1 l2 = if null l1 then List.rev acc_pre @ List.rev acc_pro elseif null l2 then List.rev acc_pre @ l1 @ List.rev acc_pro else letval 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,2,3,4,5]);
val _ = \<^assert>
(prefix_intersection_list [] [1,3,5] = [])
fun switch f y x = f x y
(*Given a value of type "'a option list", produce a value of type "'a list" by dropping the NONE elements
and projecting the SOME elements.*) 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)
exception MULTI_ELEMENT_LIST (*Try a number of predicates, in order, to find a single element. Predicates are expected to either return an empty list or a singleton list. If strict=true and list has more than one element,
then raise an exception. Otherwise try a new predicate.*) 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 thenraise MULTI_ELEMENT_LIST else cascaded_filter_single strict ps l
(*concat but with optional before-and-after delimiters*) 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
(*Given a list, find an element satisfying pred, and return
a pair consisting of that element and the list minus the element.*) fun find_and_remove pred l =
find_index pred l
|> switch chop l
|> apsnd break_list
|> (fn (xs, (y, ys)) => (y, xs @ ys))
(*Extract the forall-prefix of a term, and return a pair consisting of the prefix
and the body*)
local (*Strip off HOL's All combinator if it's at the toplevel*) fun try_dest_All (Const (\<^const_name>\<open>HOL.All\<close>, _) $ t) = t
| try_dest_All (Const (\<^const_name>\<open>HOL.Trueprop\<close>, _) $ t) = try_dest_All t
| try_dest_All t = t
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>\<open>'a\)],
HOLogic.all_const \<^typ>\<open>'a\ $
(HOLogic.eq_const \<^typ>\<open>'a\ $
Free ("x", \<^typ>\<open>'a\))) in
\<^assert>
((\<^term>\<open>\<forall>x. All ((=) x)\<close>
|> strip_top_All_vars)
= answer) end
(*like strip_top_All_vars, but peels a single variable off, instead of all of them*) fun strip_top_All_var t =
strip_top_All_vars' true [] t
|> apfst the_single end
(*like strip_top_All_vars but for "Pure.all" instead of "HOL.All"*) fun strip_top_all_vars acc t = if Logic.is_all t then let val (v, t') = Logic.dest_all_global t (*bound instances in t' are replaced with free vars*) in
strip_top_all_vars (v :: acc) t' end else (acc, (*variables are returned in FILO order*)
t)
(*given a term "t" ! X Y Z. t' then then "push_allvar_in "X" t" will give ! Y Z X. 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
(*Lists all consts in a term, uniquely*) 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 (*This carries out naive form of matching. It "diffs" two formulas, to create a function which maps (schematic or non-schematic) variables to terms. The first argument is the more "general" term. The second argument is used to find the "image" for the variables in the first argument which don't appear in the second argument.
Note that the list that is returned might have duplicate entries. It's not checked to see if the same variable maps to different
values -- that should be regarded as an error.*) 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)
and diff_probs acc ts = case ts of
[] => acc
| (pair :: ts') => diff' acc pair ts' in
diff_probs ([], []) [initial] end
(*Abstracts occurrences of "t_sub" in "t", returning a list of abstractions of "t" with a Var at each occurrence of "t_sub". If "strong=true" then it uses strong abstraction (i.e., replaces all occurrnces of "t_sub"), otherwise it uses weak abstraction (i.e., replaces the occurrences one at a time). NOTE there are many more possibilities between strong and week. These can be enumerated by abstracting based on the powerset of occurrences (minus the null element, which would correspond to "t").
*) 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
(*Carries out strong abstraction of a term guided by a list of other terms. In case some of the latter terms happen to be the same, it only abstracts them once. It returns the abstracted term, together with a map from
the fresh names to the terms.*) 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' = (* list_diff vs (list_diff (Term.add_frees t' []) 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)
(*Instantiate type variables in a term, based on a type environment*) 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
(*Take a "diff" between an (abstract) thm's term, and another term (the latter is an instance of the form), then instantiate the abstract theorem. This is a way of turning the latter term into a theorem, but without exposing the proof-search functions to complex terms. In addition to the abstract thm ("scheme_thm"), this function is also supplied with the (sub)term of the abstract thm ("scheme_t") we want to use in the diff, in case only part of "scheme_t"
might be needed (not the whole "Thm.prop_of scheme_thm")*) 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)
(*valuation of type variables*) 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) (*valuation of term variables*) 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
(*FIXME this is bad form?*) val try_dest_Trueprop = perhaps (try HOLogic.dest_Trueprop)
(** Some tacticals **)
(*Lift COND to be parametrised by subgoal number*) fun COND' sat' tac'1 tac'2 i =
COND (sat' i) (tac'1 i) (tac'2 i)
(*Apply simplification ("wittler") as few times as possible before being able to apply a tactic ("tac"). This is like a lazy version of REPEAT, since it attempts to REPEAT a tactic the smallest number times as possible,
to make some other tactic succeed subsequently.*) 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 (Thm.no_prems (fst (the pulled_tac_result))) in if tac_failed then (wittler THEN' ASAP wittler tac) i st else tac_result end
(** Some tactics **)
fun break_hypotheses_tac ctxt =
CHANGED o
((REPEAT_DETERM o eresolve_tac ctxt @{thms conjE}) THEN'
(REPEAT_DETERM o eresolve_tac ctxt @{thms disjE}))
(*Prove subgoals of form A ==> B1 | ... | A | ... | Bn*) fun clause_breaker_tac ctxt =
(REPEAT o resolve_tac ctxt @{thms disjI1 disjI2 conjI}) THEN'
assume_tac ctxt
(* Refines a subgoal have the form: A1 ... An ==> B1 | ... | Aj | ... | Bi | ... | Ak | ... into multiple subgoals of the form: A'1 ==> B1 | ... | Aj | ... | Bi | ... | Ak | ... : A'm ==> B1 | ... | Aj | ... | Bi | ... | Ak | ... where {A'1 .. A'm} is disjoint from {B1, ..., Aj, ..., Bi, ..., Ak, ...} (and solves the subgoal completely if the first set is empty)
*) fun batter_tac ctxt i =
break_hypotheses_tac ctxt i THEN
ALLGOALS (TRY o clause_breaker_tac ctxt)
(*Same idiom as ex_expander_tac*) 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} (*FIXME duplicates @{thm simp_meta(3)}*)
(Simplifier.empty_simpset ctxt))
#> CHANGED
#> REPEAT_DETERM
(** Subgoal analysis **)
(*Given an inference C ----- D This function returns "SOME X" if C = "! X. C'".
If C has no quantification prefix, then returns NONE.*) 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
(** Builders for goal analysers or transformers **)
(*Lifts function over terms to apply it to subgoals. "fun_over_terms" has type (term list * term -> 'a), where (term list * term) will be the term representations of the hypotheses and conclusion. if i_opt=SOME i then applies fun_over_terms to that subgoal and returns singleton result. otherwise applies fun_over_terms to all subgoals and return
list of results.*) 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
(*Applies a predicate to subgoal(s) conclusion(s)*) 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 (*discard hypotheses*)
#> map hyp_pred_over_terms) i_opt st val conc_results =
TERMFUN (snd (*discard hypotheses*)
#> conc_pred_over_terms) i_opt st val _ = \<^assert> (length hyp_results = length conc_results) in if null hyp_results thentrue 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
(** Tracing **) (*If "tac i st" succeeds then msg is printed to "trace" channel*) 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
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.16Bemerkung:
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
