(* Title: HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Author: Nik Sultana, Cambridge University Computer Laboratory
Reconstructs TPTP proofs in Isabelle/HOL. Specialised to work with proofs produced by LEO-II.
TODO - Proof transformation to remove "copy" steps, and perhaps other dud inferences.
*)
signature TPTP_RECONSTRUCT = sig (* Interface used by TPTP_Reconstruct.thy, to define LEO-II proof reconstruction. *)
datatype formula_kind =
Conjunctive ofbooloption
| Disjunctive ofbooloption
| Biimplicational ofbooloption
| Negative ofbooloption
| Existential ofbooloption * typ
| Universal ofbooloption * typ
| Equational ofbooloption * typ
| Atomic ofbooloption
| Implicational ofbooloption type formula_meaning =
(string *
{role : TPTP_Syntax.role,
fmla : term,
source_inf_opt : TPTP_Proof.source_info option}) type proof_annotation =
{problem_name : TPTP_Problem_Name.problem_name,
skolem_defs : ((*skolem const name*)string * Binding.binding) list,
defs : ((*node name*)string * Binding.binding) list,
axs : ((*node name*)string * Binding.binding) list, (*info for each node (for all lines in the TPTP proof)*)
meta : formula_meaning list} type rule_info =
{inference_name : string, (*name of calculus rule*)
inference_fmla : term, (*the inference as a term*)
parents : stringlist}
exception UNPOLARISED of term
val remove_polarity : bool -> term -> term * bool val interpret_bindings :
TPTP_Problem_Name.problem_name -> theory -> TPTP_Proof.parent_detail list -> (string * term) list -> (string * term) list val diff_and_instantiate : Proof.context -> thm -> term -> term -> thm (*FIXME from library*) val strip_top_all_vars : (string * typ) list -> term -> (string * typ) list * term val strip_top_All_vars : term -> (string * typ) list * term val strip_top_All_var : term -> (string * typ) * term val new_consts_between : term -> term -> term list val get_pannot_of_prob : theory -> TPTP_Problem_Name.problem_name -> proof_annotation val inference_at_node : 'a -> TPTP_Problem_Name.problem_name -> formula_meaning list -> string -> rule_info option val node_info : (string * 'a) list -> ('a -> 'b) -> string -> 'b
type step_id = string datatype rolling_stock =
Step of step_id
| Assumed
| Unconjoin
| Split of step_id (*where split occurs*) *
step_id (*where split ends*) *
step_id list(*children of the split*)
| Synth_step of step_id (*A step which doesn't necessarily appear in the original proof, or which has been modified slightly for better
handling by Isabelle*)
| Annotated_step of step_id * string(*Same interpretation as "Step", except that additional information is attached. This is currently used for debugging: Steps are mapped to Annotated_steps
and their rule names are included as strings*)
| Definition of step_id (*Mirrors TPTP role*)
| Axiom of step_id (*Mirrors TPTP role*)
| Caboose
(* Interface for using the proof reconstruction. *)
val import_thm : bool -> Path.T list -> Path.T -> (proof_annotation -> theory -> proof_annotation * theory) -> theory -> theory val get_fmlas_of_prob : theory -> TPTP_Problem_Name.problem_name -> TPTP_Interpret.tptp_formula_meaning list val structure_fmla_meaning : 'a * 'b * 'c * 'd -> 'a * {fmla: 'c, role: 'b, source_inf_opt: 'd} val make_skeleton : Proof.context -> proof_annotation -> rolling_stock list val naive_reconstruct_tacs :
(Proof.context -> TPTP_Problem_Name.problem_name -> step_id -> thm) ->
TPTP_Problem_Name.problem_name -> Proof.context -> (rolling_stock * term option * (thm * tactic) option) list val naive_reconstruct_tac :
Proof.context -> (Proof.context -> TPTP_Problem_Name.problem_name -> step_id -> thm) -> TPTP_Problem_Name.problem_name -> tactic val reconstruct : Proof.context -> (TPTP_Problem_Name.problem_name -> tactic) -> TPTP_Problem_Name.problem_name -> thm end
(*FIXME move to more general struct*) (*Extract the formulas of an imported TPTP problem -- these formulas
may make up a proof*) fun get_fmlas_of_prob thy prob_name : TPTP_Interpret.tptp_formula_meaning list =
AList.lookup (op =) (TPTP_Interpret.get_manifests thy) prob_name
|> the |> #3 (*get formulas*);
(** General **)
(* Proof annotations *)
(*FIXME modify TPTP_Interpret.tptp_formula_meaning into this type*) type formula_meaning =
(string *
{role : TPTP_Syntax.role,
fmla : term,
source_inf_opt : TPTP_Proof.source_info option})
fun apply_to_parent_info f
(n, {role, fmla, source_inf_opt}) = let val source_inf_opt' = case source_inf_opt of
NONE => NONE
| SOME (TPTP_Proof.Inference (inf_name, sinfos, pinfos)) =>
SOME (TPTP_Proof.Inference (inf_name, sinfos, f pinfos)) in
(n, {role = role, fmla = fmla, source_inf_opt = source_inf_opt'}) end
type proof_annotation =
{problem_name : TPTP_Problem_Name.problem_name,
skolem_defs : ((*skolem const name*)string * Binding.binding) list,
defs : ((*node name*)string * Binding.binding) list,
axs : ((*node name*)string * Binding.binding) list, (*info for each node (for all lines in the TPTP proof)*)
meta : formula_meaning list}
fun empty_pannot prob_name =
{problem_name = prob_name,
skolem_defs = [],
defs = [],
axs = [],
meta = []}
(* Storage of proof data *)
exception MANIFEST of TPTP_Problem_Name.problem_name * string(*FIXME move to TPTP_Interpret?*)
type manifest = TPTP_Problem_Name.problem_name * proof_annotation
(*manifest equality simply depends on problem name*) fun manifest_eq ((prob_name1, _), (prob_name2, _)) = prob_name1 = prob_name2
structure TPTP_Reconstruction_Data = Theory_Data
( type T = manifest list val empty = [] fun merge data : T = Library.merge manifest_eq data
) val get_manifests : theory -> manifest list = TPTP_Reconstruction_Data.get
fun update_manifest prob_name pannot thy = let val idx =
find_index
(fn (n, _) => n = prob_name)
(get_manifests thy) val transf = (fn _ =>
(prob_name, pannot)) in
TPTP_Reconstruction_Data.map
(nth_map idx transf)
thy end
(*similar to get_fmlas_of_prob but for proofs*) fun get_pannot_of_prob thy prob_name : proof_annotation = case AList.lookup (op =) (get_manifests thy) prob_name of
SOME pa => pa
| NONE => raise (MANIFEST (prob_name, "Could not find proof annotation"))
(* Constants *)
(*Prefix used for naming inferences which were added during proof transformation. (e.g., this is used to name "bind"-inference nodes
described below)*) val inode_prefixK = "inode"
(*New inference rule name, which is added to indicate that some variable has been instantiated. Additional proof metadata will
indicate which variable, and how it was instantiated*) val bindK = "bind"
(*New inference rule name, which is added to indicate that some (validity-preserving) preprocessing has been done to a (singleton)
clause prior to it being split.*) val split_preprocessingK = "split_preprocessing"
(* Storage of internal values *)
type tptp_reconstruction_state = {next_int : int} structure TPTP_Reconstruction_Internal_Data = Theory_Data
( type T = tptp_reconstruction_state val empty = {next_int = 0} fun merge data : T = snd data
)
(*increment internal counter, and obtain the current next value*) fun get_next_int thy : int * theory = let val state = TPTP_Reconstruction_Internal_Data.get thy val state' = {next_int = 1 + #next_int state} in
(#next_int state,
TPTP_Reconstruction_Internal_Data.put state' thy) end
(*FIXME in some applications (e.g. where the name is used for an inference node) need to check that the name is fresh, to avoid
collisions with other bits of the proof*) val get_next_name =
get_next_int
#> apfst (fn i => inode_prefixK ^ Int.toString i)
(* Building the index *)
(*thrown when we're expecting a TPTP_Proof.Bind annotation but find something else*)
exception NON_BINDING (*given a list of pairs consisting of a variable name and TPTP formula, returns the list consisting of the original variable name and the interpreted HOL formula. Needs the problem name to ensure use of correct interpretations for
constants and types.*) fun interpret_bindings (prob_name : TPTP_Problem_Name.problem_name) thy bindings acc = if null bindings then acc else case hd bindings of
TPTP_Proof.Bind (v, fmla) => let val (type_map, const_map) = case AList.lookup (op =) (TPTP_Interpret.get_manifests thy) prob_name of
NONE => raise (MANIFEST (prob_name, "Problem details not found in interpretation manifest"))
| SOME (type_map, const_map, _) => (type_map, const_map)
(*FIXME get config from the envir or make it parameter*) val config =
{cautious = true,
problem_name = SOME prob_name} val result =
(v,
TPTP_Interpret.interpret_formula
config TPTP_Syntax.THF
const_map [] type_map fmla thy
|> fst) in
interpret_bindings prob_name thy (tl bindings) (result :: acc) end
| _ => raise NON_BINDING
type rule_info =
{inference_name : string, (*name of calculus rule*)
inference_fmla : term, (*the inference as a term*)
parents : stringlist}
(*Instantiates a binding in orig_parent_fmla. Used in a proof
transformation to factor out instantiations from inferences.*) fun apply_binding thy prob_name orig_parent_fmla target_fmla bindings = let val bindings' = interpret_bindings prob_name thy bindings []
(*capture selected free variables. these variables, and their
intended de Bruijn index, are included in "var_ctxt"*) fun bind_free_vars var_ctxt t = case t of Const _ => t
| Var _ => t
| Bound _ => t
| Abs (x, ty, t') => Abs (x, ty, bind_free_vars (x :: var_ctxt) t')
| Free (x, ty) => let val idx = find_index (fn y => y = x) var_ctxt in if idx > ~1 andalso
ty = dummyT (*this check not really needed*) then
Bound idx else t end
| t1 $ t2 => bind_free_vars var_ctxt t1 $ bind_free_vars var_ctxt t2
(*Instantiate specific quantified variables: Look for subterms of form (! (% x. M)) where "x" appears as a "bound_var", then replace "x" for "body" in "M". Should only be applied at formula top level -- i.e., once past the quantifier prefix we needn't bother with looking for bound_vars. "var"_ctxt is used to keep track of lambda-bindings we encounter, to capture free variables in "body" correctly (i.e., replace Free with Bound having the
right index)*) fun instantiate_bound (binding as (bound_var, body)) (initial as (var_ctxt, t)) = case t of Const _ => initial
| Free _ => initial
| Var _ => initial
| Bound _ => initial
| Abs _ => initial
| t1 $ (t2 as Abs (x, ty, t')) => if is_Const t1 then (*Could be fooled by shadowing, but if order matters then should still be able to handle formulas like
(! X, X. F).*) if x = bound_var andalso
dest_Const_name t1 = \<^const_name>\<open>All\<close> then (*Body might contain free variables, so bind them using "var_ctxt". this involves replacing instances of Free with instances of Bound
at the right index.*) letval body' = bind_free_vars var_ctxt body in
(var_ctxt,
betapply (t2, body')) end else let val (var_ctxt', rest) = instantiate_bound binding (x :: var_ctxt, t') in
(var_ctxt',
t1 $ Abs (x, ty, rest)) end else initial
| t1 $ t2 => let val (var_ctxt', rest) = instantiate_bound binding (var_ctxt, t2) in
(var_ctxt', t1 $ rest) end
(*Here we preempt the following problem: if have (! X1, X2, X3. body), and X1 is instantiated to "c X2 X3", then the current code will yield (! X2, X3, X2a, X3a. body'). To avoid this, we must first push X1 in, before calling instantiate_bound, to make sure that bound variables don't
get free.*) fun safe_instantiate_bound (binding as (bound_var, body)) (var_ctxt, t) =
instantiate_bound binding
(var_ctxt, push_allvar_in bound_var t)
(*return true if one of the types is polymorphic*) fun is_polymorphic tys = if null tys thenfalse else case hd tys of Type (_, tys') => is_polymorphic (tl tys @ tys')
| TFree _ => true
| TVar _ => true
(*find the type of a quantified variable, at the "topmost" binding
occurrence*)
local fun type_of_quantified_var' s ts = if null ts then NONE else case hd ts of Const _ => type_of_quantified_var' s (tl ts)
| Free _ => type_of_quantified_var' s (tl ts)
| Var _ => type_of_quantified_var' s (tl ts)
| Bound _ => type_of_quantified_var' s (tl ts)
| Abs (s', ty, t') => if s = s' then SOME ty else type_of_quantified_var' s (t' :: tl ts)
| t1 $ t2 => type_of_quantified_var' s (t1 :: t2 :: tl ts) in fun type_of_quantified_var s =
single #> type_of_quantified_var' s end
(*Form the universal closure of "t".
NOTE remark above "val frees" about ordering of quantified variables*) fun close_formula t = let (*The ordering of Frees in this list affects the order in which variables appear in the quantification prefix. Currently this is assumed not to matter. This consists of a list of pairs: the first element consists of the "original" free variable, and the latter consists of the monomorphised equivalent. The two elements are identical if the original is already monomorphic. This monomorphisation is needed since, owing to TPTP's lack of type annotations, variables might not be constrained by type info. This results in them being
interpreted as polymorphic. E.g., this issue comes up in CSR148^1*) val frees_monomorphised =
fold_aterms
(fn t => fn rest => if is_Free t then let val (s, ty) = dest_Free t val ty' = if ty = dummyT orelse is_polymorphic [ty] then
the (type_of_quantified_var s target_fmla) else ty in insert (op =) (t, Free (s, ty')) rest end else rest)
t [] in
Term.subst_free frees_monomorphised t
|> fold (fn (s, ty) => fn t =>
HOLogic.mk_all (s, ty, t))
(map (snd #> dest_Free) frees_monomorphised) end
(*FIXME currently assuming that we're only ever given a single binding each time this is called*) val _ = \<^assert> (length bindings' = 1)
in
fold safe_instantiate_bound bindings' ([], HOLogic.dest_Trueprop orig_parent_fmla)
|> snd (*discard var typing context*)
|> close_formula
|> singleton (Type_Infer_Context.infer_types (Context.proof_of (Context.Theory thy)))
|> HOLogic.mk_Trueprop
|> rpair bindings' end
exception RECONSTRUCT ofstring
(*Some of these may be redundant wrt the original aims of this datatype, but it's useful to have a datatype to classify formulas
for use by other functions as well.*) datatype formula_kind =
Conjunctive ofbooloption
| Disjunctive ofbooloption
| Biimplicational ofbooloption
| Negative ofbooloption
| Existential ofbooloption * typ
| Universal ofbooloption * typ
| Equational ofbooloption * typ
| Atomic ofbooloption
| Implicational ofbooloption
exception UNPOLARISED of term (*Remove "= $true" or "= $false$ from the edge of a formula. Use "try" in case formula is not
polarised.*) fun remove_polarity strict formula = casetry HOLogic.dest_eq formula of
NONE => if strict thenraise (UNPOLARISED formula) else (formula, true)
| SOME (x, p as \<^term>\<open>True\<close>) => (x, true)
| SOME (x, p as \<^term>\<open>False\<close>) => (x, false)
| SOME (x, _) => if strict thenraise (UNPOLARISED formula) else (formula, true)
(*flattens a formula wrt associative operators*) fun flatten formula_kind formula = let fun is_conj (Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _) = true
| is_conj _ = false fun is_disj (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _) = true
| is_disj _ = false fun is_iff (Const (\<^const_name>\<open>HOL.eq\<close>, ty) $ _ $ _) =
ty = ([HOLogic.boolT, HOLogic.boolT] ---> HOLogic.boolT)
| is_iff _ = false
fun flatten' formula acc = case formula of Const (\<^const_name>\<open>HOL.conj\<close>, _) $ t1 $ t2 =>
(case formula_kind of
Conjunctive _ => let val left = if is_conj t1 then flatten' t1 acc else (t1 :: acc) in if is_conj t2 then flatten' t2 left else (t2 :: left) end
| _ => formula :: acc)
| Const (\<^const_name>\<open>HOL.disj\<close>, _) $ t1 $ t2 =>
(case formula_kind of
Disjunctive _ => let val left = if is_disj t1 then flatten' t1 acc else (t1 :: acc) in if is_disj t2 then flatten' t2 left else (t2 :: left) end
| _ => formula :: acc)
| Const (\<^const_name>\<open>HOL.eq\<close>, ty) $ t1 $ t2 => if ty = ([HOLogic.boolT, HOLogic.boolT] ---> HOLogic.boolT) then case formula_kind of
Biimplicational _ => let val left = if is_iff t1 then flatten' t1 acc else (t1 :: acc) in if is_iff t2 then flatten' t2 left else (t2 :: left) end
| _ => formula :: acc else formula :: acc
| _ => [formula]
val formula' = try_dest_Trueprop formula in case formula_kind of
Conjunctive (SOME _) =>
remove_polarity false formula'
|> fst
|> (fn t => flatten' t [])
| Disjunctive (SOME _) =>
remove_polarity false formula'
|> fst
|> (fn t => flatten' t [])
| Biimplicational (SOME _) =>
remove_polarity false formula'
|> fst
|> (fn t => flatten' t [])
| _ => flatten' formula' [] end
fun node_info fms projector node_name = case AList.lookup (op =) fms node_name of
NONE => raise (RECONSTRUCT ("node " ^ node_name ^ " doesn't exist"))
| SOME info => projector info
(*Given a list of parent infos, extract the parent node names and the additional info (e.g., if there was an instantiation in addition to the inference).
if "filtered"=true then exclude axiom and definition parents*) fun dest_parent_infos filtered fms parent_infos : {name : string, details : TPTP_Proof.parent_detail list} list = let (*Removes "definition" dependencies since these play no logical role -- i.e. they just give the expansions of constants. Removes "axiom" dependencies since these do not need to be derived; the reconstruction handler in "leo2_tac" can pick up the relevant axioms (using the info in the proof annotation) and use them in its reconstruction.
*) val filter_deps = filter (fn {name, ...} => let val role = node_info fms #role name in role <> TPTP_Syntax.Role_Definition andalso
role <> TPTP_Syntax.Role_Axiom end) val parent_nodelist =
parent_infos
|> map (fn n => case n of
TPTP_Proof.Parent parent => {name = parent, details = []}
| TPTP_Proof.ParentWithDetails (parent, details) =>
{name = parent, details = details}) in
parent_nodelist
|> filtered ? filter_deps end
fun parents_of_node fms n = case node_info fms #source_inf_opt n of
NONE => []
| SOME (TPTP_Proof.File _) => []
| SOME (TPTP_Proof.Inference (_, _ : TPTP_Proof.useful_info_as list, parent_infos)) =>
dest_parent_infos false fms parent_infos
|> map #name
exception FIND_ANCESTOR_USING_RULE ofstring (*BFS for an ancestor inference involving a specific rule*) fun find_ancestor_using_rule pannot inference_rule (fringe : stringlist) : string = if null fringe then raise (FIND_ANCESTOR_USING_RULE inference_rule) else case node_info (#meta pannot) #source_inf_opt (hd fringe) of
NONE => find_ancestor_using_rule pannot inference_rule (tl fringe)
| SOME (TPTP_Proof.File _) => find_ancestor_using_rule pannot inference_rule (tl fringe)
| SOME (TPTP_Proof.Inference (rule_name, _ : TPTP_Proof.useful_info_as list, parent_infos)) => if rule_name = inference_rule then hd fringe else
find_ancestor_using_rule pannot inference_rule
(tl fringe @ map #name (dest_parent_infos true (#meta pannot) parent_infos))
(*Given a node in the proof, produce the term representing the inference that took place in that step, the inference rule used, and which other (non-axiom and non-definition) nodes participated in the
inference*) fun inference_at_node thy (prob_name : TPTP_Problem_Name.problem_name)
(fms : formula_meaning list) from : rule_info option = let
exception INFERENCE_AT_NODE ofstring
(*lookup formula associated with a node*) val fmla_of_node =
node_info fms #fmla
#> try_dest_Trueprop
fun build_inference_info rule_name parent_infos = let val _ = \<^assert> (not (null parent_infos))
(*hypothesis formulas (with bindings already instantiated during the proof-transformation applied when loading the proof),
including any axioms or definitions*) val parent_nodes =
dest_parent_infos false fms parent_infos
|> map #name
val parent_fmlas = map fmla_of_node (rev(*FIXME can do away with this? it matters because of order of conjunction. is there a matching rev elsewhere?*) parent_nodes)
val inference_term = if null parent_fmlas then
fmla_of_node from
|> HOLogic.mk_Trueprop else
Logic.mk_implies
(fold
(curry HOLogic.mk_conj)
(tl parent_fmlas)
(hd parent_fmlas)
|> HOLogic.mk_Trueprop,
fmla_of_node from |> HOLogic.mk_Trueprop) in
SOME {inference_name = rule_name,
inference_fmla = inference_term,
parents = parent_nodes} end in (*examine node's "source" annotation: we're only interested
if it's an inference*) case node_info fms #source_inf_opt from of
NONE => NONE
| SOME (TPTP_Proof.File _) => NONE
| SOME (TPTP_Proof.Inference (rule_name, _ : TPTP_Proof.useful_info_as list, parent_infos)) => ifList.null parent_infos then raise (INFERENCE_AT_NODE
("empty parent list for node " ^
from ^ ": check proof format")) else
build_inference_info rule_name parent_infos end
where major_prem is a disjunction of prem1,...,premn.
*) fun make_elimination_rule_t ctxt major_prem prems_and_concs conclusion = let val thy = Proof_Context.theory_of ctxt val minor_prems = map (fn (v, conc) =>
Logic.mk_implies (v, HOLogic.mk_Trueprop conc))
prems_and_concs in
(Logic.list_implies
(major_prem :: minor_prems,
conclusion)) end
(*In summary, we emulate an n-way splitting rule via an n-way disjunction elimination.
Given a split formula and conclusion, we prove a rule which simulates the split. The conclusion is assumed to be a conjunction of conclusions for each branch of the split. The "minor_prem_assumptions" are the assumptions discharged in each branch; they're passed to the function to make sure that the generated rule is compatible with the skeleton (since the skeleton fixes the "order" of the reconstruction, based on the proof's structure).
Concretely, if P is "(_ & _) = $false" or "(_ | _) = $true" then splitting behaves as follows:
(A <=> B) = $false ------------------------------------------ (A => B) = $false (B => A) = $false ... ... R1 R2 ------------------------------------------ R1 & R2
*) fun simulate_split ctxt split_fmla minor_prem_assumptions conclusion = let val prems_and_concs =
ListPair.zip (minor_prem_assumptions, flatten (Conjunctive NONE) conclusion)
val rule_t = make_elimination_rule_t ctxt split_fmla prems_and_concs conclusion
(*these are replaced by fresh variables in the abstract term*) val abstraction_subterms =
(map (try_dest_Trueprop #> remove_polarity true #> fst)
minor_prem_assumptions)
(*generate an abstract rule as a term...*) val abs_rule_t =
abstract
abstraction_subterms
rule_t
|> snd (*ignore mapping info. this is a bit wasteful*) (*FIXME optimisation: instead on relying on diff
to regenerate this info, could use it directly*)
(*...and validate the abstract rule*) val abs_rule_thm =
Goal.prove ctxt [] [] abs_rule_t
(fn pdata => HEADGOAL (blast_tac (#context pdata)))
|> Drule.export_without_context in (*Instantiate the abstract rule based on the contents of the
required instance*)
diff_and_instantiate ctxt abs_rule_thm (Thm.prop_of abs_rule_thm) rule_t end
(* Building the skeleton *)
type step_id = string datatype rolling_stock =
Step of step_id
| Assumed
| Unconjoin
| Split of step_id (*where split occurs*) *
step_id (*where split ends*) *
step_id list(*children of the split*)
| Synth_step of step_id (*A step which doesn't necessarily appear in the original proof, or which has been modified slightly for better
handling by Isabelle*)
| Annotated_step of step_id * string(*Same interpretation as "Step", except that additional information is attached. This is currently used for debugging: Steps are mapped to Annotated_steps
and their rule names are included as strings*)
| Definition of step_id (*Mirrors TPTP role*)
| Axiom of step_id (*Mirrors TPTP role*) (* | Derived of step_id -- to be used by memoization*)
| Caboose
fun stock_to_string (Step n) = n
| stock_to_string (Annotated_step (n, anno)) = n ^ "(" ^ anno ^ ")"
| stock_to_string _ = error "Stock is not a step"(*FIXME more meaningful message*)
fun filter_by_role tptp_role = filter
(fn (_, info) =>
#role info = tptp_role)
fun filter_by_name node_name = filter
(fn (n, _) =>
n = node_name)
exception NO_MARKER_NODE (*We fall back on node "1" in case the proof is not that of a theorem*) fun proof_beginning_node fms = let val result =
cascaded_filter_single true
[filter_by_role TPTP_Syntax.Role_Conjecture,
filter_by_name "1"] (*FIXME const*)
fms in case result of
SOME x => fst x (*get the node name*)
| NONE => raise NO_MARKER_NODE end
(*Get the name of the node where the proof ends*) fun proof_end_node fms = (*FIXME this isn't very nice: we assume that the last line in the proof file is the closing line of the proof. It would be nicer if such a line is specially marked (with a role), since there is no obvious ordering on names, since they can be strings. Another way would be to run an analysis on the graph to find this node, since it has properties which should make it unique
in a graph*)
fms
|> hd (*since proof has been reversed prior*)
|> fst (*get node name*)
(*Generate list of (possibly reconstructed) inferences which can be
composed together to reconstruct the whole proof.*) fun make_skeleton ctxt (pannot : proof_annotation) : rolling_stock list = let val thy = Proof_Context.theory_of ctxt
fun stock_of n = case node_info (#meta pannot) #role n of
TPTP_Syntax.Role_Definition => (true, Definition n)
| TPTP_Syntax.Role_Axiom => (true, Axiom n)
| _ => (false, Step n)
fun n_is_split_conjecture (inference_info : rule_info option) = case inference_info of
NONE => false
| SOME inference_info => #inference_name inference_info = "split_conjecture"
(*Different kinds of inference sequences: - Linear: (just add a step to the skeleton) ---...---
- Fan-in: (treat each in-path as conjoined with the others. Linearise all the paths, and concatenate them.) /---... ------< \---...
- Real split: Instead of treating as a conjunction, as in normal fan-ins, we need to treat specially by looking at the location where the split occurs, and turn the split inference into a validity-preserving subproof. As with fan-ins, we handle each fan-in path, and concatenate. /---...---\ ------< >------ \---...---/
- Fake split: (treat like linear, since there isn't a split-node) ------<---...----------
Different kinds of sequences endings: - "Stop before": Non-decreasing list of nodes where should terminate. This starts off with the end node, and the split_nodes will be added dynamically as the skeleton is built. - Axiom/Definition
*)
(*The following functions build the skeleton for the reconstruction starting
from the node labelled "n" and stopping just before an element in stop_just_befores*) (*FIXME could throw exception if none of stop_just_befores is ever encountered*)
(*This approach below is naive because it linearises the proof DAG, and this would
duplicate some effort if the DAG isn't already linear.*)
exception SKELETON
fun check_parents stop_just_befores n = let val parents = parents_of_node (#meta pannot) n in if length parents = 1 then
AList.lookup (op =) stop_just_befores (the_single parents) else
NONE end
fun naive_skeleton' stop_just_befores n = case check_parents stop_just_befores n of
SOME skel => skel
| NONE => let val inference_info = inference_at_node thy (#problem_name pannot) (#meta pannot) n in if is_none inference_info then (*this is the case for the conjecture, definitions and axioms*) if node_info (#meta pannot) #role n = TPTP_Syntax.Role_Definition then
[(Definition n), Assumed] elseif node_info (#meta pannot) #role n = TPTP_Syntax.Role_Axiom then
[Axiom n] elseraise SKELETON else let val inference_info = the inference_info val parents = #parents inference_info in (*FIXME memoize antecedent_steps?*) if #inference_name inference_info = "solved_all_splits" andalso length parents > 1 then (*splitting involves fanning out then in; this is to be
treated different than other fan-out-ins.*) let (*find where the proofs fanned-out: pick some antecedent,
then find ancestor to use a "split_conjecture" inference.*) (*NOTE we assume that splits can't be nested*) val split_node =
find_ancestor_using_rule pannot "split_conjecture" [hd parents]
|> parents_of_node (#meta pannot)
|> the_single
(*compute the skeletons starting at parents to either the split_node if the antecedent is descended from the split_node, or the
stop_just_before otherwise*) val skeletons_up = map (naive_skeleton' ((split_node, [Assumed]) :: stop_just_befores)) parents in (*point to the split node, so that custom rule can be built later on*)
Step n :: (Split (split_node, n, parents)) :: (*this will create the elimination rule*)
naive_skeleton' stop_just_befores split_node @ (*this will discharge the major premise*)
flat skeletons_up @ [Assumed] (*this will discharge the minor premises*) end elseif length parents > 1 then (*Handle fan-in nodes which aren't split-sinks by
enclosing each branch but one in conjI-assumption invocations*) let val skeletons_up = map (naive_skeleton' stop_just_befores) parents in
Step n :: concat_between skeletons_up (SOME Unconjoin, NONE) @ [Assumed] end else
Step n :: naive_skeleton' stop_just_befores (the_single parents) end end in ifList.null (#meta pannot) then [] (*in case "proof" file is empty*) else
naive_skeleton'
[(proof_beginning_node (#meta pannot), [Assumed])]
(proof_end_node (#meta pannot)) (*make last step the Caboose*)
|> rev |> tl |> cons Caboose |> rev (*FIXME hacky*) end
(* Using the skeleton *)
exception SKELETON
local (*Change the negated assumption (which is output by the contradiction rule) into
a form familiar to Leo2*) val neg_eq_false =
@{lemma "!! P. (~ P) ==> (P = False)" by auto}
(*FIXME this is just a dummy thm to annotate the assumption tac "atac"*) val solved_all_splits =
@{lemma "False = True ==> False" by auto}
fun skel_to_naive_tactic ctxt prover_tac prob_name skel memo = fn st => let val thy = Proof_Context.theory_of ctxt val pannot = get_pannot_of_prob thy prob_name fun tac_and_memo node memo = case AList.lookup (op =) memo node of
NONE => let val tac = (*FIXME formula_sizelimit not being
checked here*)
prover_tac ctxt prob_name node in (tac, (node, tac) :: memo) end
| SOME tac => (tac, memo) fun rest skel' memo =
skel_to_naive_tactic ctxt prover_tac prob_name skel' memo
val tactic = if null skel then raise SKELETON (*FIXME or classify it as a Caboose: TRY (HEADGOAL atac) *) else case hd skel of
Assumed => TRY (HEADGOAL (assume_tac ctxt)) THEN rest (tl skel) memo
| Caboose => TRY (HEADGOAL (assume_tac ctxt))
| Unconjoin => resolve_tac ctxt @{thms conjI} 1 THEN rest (tl skel) memo
| Split (split_node, solved_node, antes) => let val split_fmla = node_info (#meta pannot) #fmla split_node val conclusion =
(inference_at_node thy prob_name (#meta pannot) solved_node
|> the
|> #inference_fmla)
|> Logic.dest_implies (*FIXME there might be !!-variables?*)
|> #1 val minor_prems_assumps = map (fn ante => find_ancestor_using_rule pannot "split_conjecture" [ante]) antes
|> map (node_info (#meta pannot) #fmla) val split_thm =
simulate_split ctxt split_fmla minor_prems_assumps conclusion in
resolve_tac ctxt [split_thm] 1 THEN rest (tl skel) memo end
| Step s => let val (th, memo') = tac_and_memo s memo in
resolve_tac ctxt [th] 1 THEN rest (tl skel) memo' end
| Definition n => let val def_thm = case AList.lookup (op =) (#defs pannot) n of
NONE => error ("Did not find definition: " ^ n)
| SOME binding => Global_Theory.get_thm thy (Binding.name_of binding) in
resolve_tac ctxt [def_thm] 1 THEN rest (tl skel) memo end
| Axiom n => let val ax_thm = case AList.lookup (op =) (#axs pannot) n of
NONE => error ("Did not find axiom: " ^ n)
| SOME binding => Global_Theory.get_thm thy (Binding.name_of binding) in
resolve_tac ctxt [ax_thm] 1 THEN rest (tl skel) memo end
| _ => raise SKELETON in tactic st end (*FIXME fuse these*) (*As above, but creates debug-friendly tactic.
This is also used for "partial proof reconstruction"*) fun skel_to_naive_tactic_dbg prover_tac ctxt prob_name skel (memo : (string * (thm * tactic) option) list) = let val thy = Proof_Context.theory_of ctxt val pannot = get_pannot_of_prob thy prob_name
(* FIXME !???! fun rtac_wrap thm_f i = fn st => let val thy = Thm.theory_of_thm st in rtac (thm_f thy) i st end
*)
(*Some nodes don't have an inference name, such as the conjecture, definitions and axioms. Such nodes shouldn't appear in the
skeleton.*) fun inference_name_of_node node = case AList.lookup (op =) (#meta pannot) node of
NONE => (warning "Inference step lacks an inference name"; "(Shouldn't be here)")
| SOME info => case #source_inf_opt info of
SOME (TPTP_Proof.Inference (infname, _, _)) =>
infname
| _ => (warning "Inference step lacks an inference name"; "(Shouldn't be here)")
fun inference_fmla node = case inference_at_node thy prob_name (#meta pannot) node of
NONE => NONE
| SOME {inference_fmla, ...} => SOME inference_fmla
fun rest memo' ctxt' = skel_to_naive_tactic_dbg prover_tac ctxt' prob_name (tl skel) memo' (*reconstruct the inference. also set timeout in case
tactic takes too long*) val try_make_step = (*FIXME const timeout*) (* Timeout.apply (Time.fromSeconds 5) *)
(fn ctxt' => let fun thm ctxt'' = prover_tac ctxt'' prob_name (hd skel |> stock_to_string) val reconstructed_inference = thm ctxt' fun rec_inf_tac st = HEADGOAL (resolve_tac ctxt' [thm ctxt']) st in (reconstructed_inference,
rec_inf_tac) end) fun ignore_interpretation_exn f x = SOME (f x) handle INTERPRET_INFERENCE => NONE in ifList.null skel then raise SKELETON (*FIXME or classify it as follows: [(Caboose, Thm.prop_of @{thm asm_rl} |> SOME, SOME (@{thm asm_rl}, TRY (HEADGOAL atac)))]
*) else case hd skel of
Assumed =>
(hd skel,
Thm.prop_of @{thm asm_rl}
|> SOME,
SOME (@{thm asm_rl}, TRY (HEADGOAL (assume_tac ctxt)))) :: rest memo ctxt
| Caboose =>
[(Caboose,
Thm.prop_of @{thm asm_rl}
|> SOME,
SOME (@{thm asm_rl}, TRY (HEADGOAL (assume_tac ctxt))))]
| Unconjoin =>
(hd skel,
Thm.prop_of @{thm conjI}
|> SOME,
SOME (@{thm conjI}, resolve_tac ctxt @{thms conjI} 1)) :: rest memo ctxt
| Split (split_node, solved_node, antes) => let val split_fmla = node_info (#meta pannot) #fmla split_node val conclusion =
(inference_at_node thy prob_name (#meta pannot) solved_node
|> the
|> #inference_fmla)
|> Logic.dest_implies (*FIXME there might be !!-variables?*)
|> #1 val minor_prems_assumps = map (fn ante => find_ancestor_using_rule pannot "split_conjecture" [ante]) antes
|> map (node_info (#meta pannot) #fmla) val split_thm =
simulate_split ctxt split_fmla minor_prems_assumps conclusion in
(hd skel,
Thm.prop_of split_thm
|> SOME,
SOME (split_thm, resolve_tac ctxt [split_thm] 1)) :: rest memo ctxt end
| Step node => let val inference_name = inference_name_of_node node val inference_fmla = inference_fmla node
(*FIXME debugging code val _ = if Config.get ctxt tptp_trace_reconstruction then (tracing ("handling node " ^ node); tracing ("inference " ^ inference_name); if is_some inference_fmla then tracing ("formula size " ^ Int.toString (Term.size_of_term (the inference_fmla))) else ()(*;
tracing ("formula " ^ @{make_string inference_fmla}) *) else ()*)
val (inference_instance_thm, memo', ctxt') = case AList.lookup (op =) memo node of
NONE => let val (thm, ctxt') = (*Instead of NONE could have another value indicating that the formula was too big*) if is_some inference_fmla andalso (*FIXME could have different inference rules have different sizelimits*)
exceeds_tptp_max_term_size ctxt (Term.size_of_term (the inference_fmla)) then
(
warning ("Gave up on node " ^ node ^ " because of fmla size " ^
Int.toString (Term.size_of_term (the inference_fmla)));
(NONE, ctxt)
) else let val maybe_thm = ignore_interpretation_exn try_make_step ctxt (* FIXME !???! val ctxt' = if is_some maybe_thm then the maybe_thm |> #1 |> Thm.theory_of_thm |> Proof_Context.init_global else ctxt
*) in
(maybe_thm, ctxt) end in (thm, (node, thm) :: memo, ctxt') end
| SOME maybe_thm => (maybe_thm, memo, ctxt) in
(Annotated_step (node, inference_name),
inference_fmla,
inference_instance_thm) :: rest memo' ctxt' end
| Definition n => let fun def_thm thy = case AList.lookup (op =) (#defs pannot) n of
NONE => error ("Did not find definition: " ^ n)
| SOME binding => Global_Theory.get_thm thy (Binding.name_of binding) in
(hd skel,
Thm.prop_of (def_thm thy)
|> SOME,
SOME (def_thm thy, HEADGOAL (resolve_tac ctxt [def_thm thy]))) :: rest memo ctxt end
| Axiom n => let val ax_thm = case AList.lookup (op =) (#axs pannot) n of
NONE => error ("Did not find axiom: " ^ n)
| SOME binding => Global_Theory.get_thm thy (Binding.name_of binding) in
(hd skel,
Thm.prop_of ax_thm
|> SOME,
SOME (ax_thm, resolve_tac ctxt [ax_thm] 1)) :: rest memo ctxt end end
(*The next function handles cases where Leo2 doesn't include the solved_all_splits step at the end (e.g. because there wouldn't be a split -- the proof
would be linear*) fun sas_if_needed_tac ctxt prob_name = let val thy = Proof_Context.theory_of ctxt val pannot = get_pannot_of_prob thy prob_name val last_inference_info_opt =
find_first
(fn (_, info) => #role info = TPTP_Syntax.Role_Plain)
(#meta pannot) val last_inference_info = case last_inference_info_opt of
NONE => NONE
| SOME (_, info) => #source_inf_opt info in if is_some last_inference_info andalso
TPTP_Proof.is_inference_called "solved_all_splits"
(the last_inference_info) then (@{thm asm_rl}, all_tac) else (solved_all_splits, TRY (resolve_tac ctxt [solved_all_splits] 1)) end in (*Build a tactic from a skeleton. This is naive because it uses the naive skeleton. The inference interpretation ("prover_tac") is a parameter -- it would usually be
different for different provers.*) fun naive_reconstruct_tac ctxt prover_tac prob_name = let val thy = Proof_Context.theory_of ctxt in
resolve_tac ctxt @{thms ccontr} 1 THEN dresolve_tac ctxt [neg_eq_false] 1 THEN (sas_if_needed_tac ctxt prob_name |> #2) THEN skel_to_naive_tactic ctxt prover_tac prob_name
(make_skeleton ctxt
(get_pannot_of_prob thy prob_name)) [] end
(*As above, but generates a list of tactics. This is useful for debugging, to apply
the tactics one by one manually.*) fun naive_reconstruct_tacs prover_tac prob_name ctxt = let val thy = Proof_Context.theory_of ctxt in
(Synth_step "ccontr", Thm.prop_of @{thm ccontr} |> SOME,
SOME (@{thm ccontr}, resolve_tac ctxt @{thms ccontr} 1)) ::
(Synth_step "neg_eq_false", Thm.prop_of neg_eq_false |> SOME,
SOME (neg_eq_false, dresolve_tac ctxt [neg_eq_false] 1)) ::
(Synth_step "sas_if_needed_tac", Thm.prop_of @{thm asm_rl} (*FIXME *) |> SOME,
SOME (sas_if_needed_tac ctxt prob_name)) ::
skel_to_naive_tactic_dbg prover_tac ctxt prob_name
(make_skeleton ctxt
(get_pannot_of_prob thy prob_name)) [] end end
(*Produces a theorem given a tactic and a parsed proof. This function is handy to test reconstruction, since it automates the interpretation and proving of the
parsed proof's goal.*) fun reconstruct ctxt tactic prob_name = let val thy = Proof_Context.theory_of ctxt val pannot = get_pannot_of_prob thy prob_name val goal =
#meta pannot
|> filter (fn (_, info) =>
#role info = TPTP_Syntax.Role_Conjecture) in if null (#meta pannot) then (*since the proof is empty, return a trivial result.*)
@{thm TrueI} elseif null goal then raise (RECONSTRUCT "Proof lacks conjecture") else
the_single goal
|> snd |> #fmla
|> (fn fmla => Goal.prove ctxt [] [] fmla (fn _ => tactic prob_name)) end
(** Skolemisation setup **)
(*Ignore these constants if they appear in the conclusion but not the hypothesis*) (*FIXME possibly incomplete*) val ignore_consts =
[HOLogic.conj, HOLogic.disj, HOLogic.imp, HOLogic.Not]
(*Difference between the constants appearing between two terms, minus "ignore_consts"*) fun new_consts_between t1 t2 = filter
(fn n => not (exists (fn n' => n' = n) ignore_consts))
(list_diff (consts_in t2) (consts_in t1))
(*Generate definition binding for an equation*) fun mk_bind_eq prob_name params ((n, ty), t) = let val bnd =
Binding.name (Long_Name.base_name n ^ "_def")
|> Binding.qualify false (TPTP_Problem_Name.mangle_problem_name prob_name) val t' =
Term.list_comb (Const (n, ty), params)
|> rpair t
|> HOLogic.mk_eq
|> HOLogic.mk_Trueprop
|> fold Logic.all params in
(bnd, t') end
(*Generate binding for an axiom. Similar to "mk_bind_eq"*) fun mk_bind_ax prob_name node t = let val bnd =
Binding.name node (*FIXME add suffix? e.g. ^ "_ax"*)
|> Binding.qualify false (TPTP_Problem_Name.mangle_problem_name prob_name) in
(bnd, t) end
(*Extract the constant name, type, and its definition*) fun get_defn_components
(Const (\<^const_name>\<open>HOL.Trueprop\<close>, _) $
(Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Const (name, ty) $ t)) = ((name, ty), t)
(*** Proof transformations ***)
(*Transforms a proof_annotation value.
Argument "f" is the proof transformer*) fun transf_pannot f (pannot : proof_annotation) : (theory * proof_annotation) = let val (thy', fms') = f (#meta pannot) in
(thy',
{problem_name = #problem_name pannot,
skolem_defs = #skolem_defs pannot,
defs = #defs pannot,
axs = #axs pannot,
meta = fms'}) end
(** Proof transformer to add virtual inference steps
encoding "bind" annotations in Leo-II proofs **)
where "bind" is an inference rule (distinct from any rule name used by Leo2) to indicate such inferences. This transformation is used to factor out instantiations, thus allowing the reconstruction to focus on (Rule name) rather than "(Rule name) + instantiations".
*) fun interpolate_binds prob_name thy fms : theory * formula_meaning list = let fun factor_out_bind target_node pinfo intermediate_thy = case pinfo of
TPTP_Proof.ParentWithDetails (n, pdetails) => (*create new node which contains the "bind" inference,
to be added to graph*) let val (new_node_name, thy') = get_next_name intermediate_thy val orig_fmla = node_info fms #fmla n val target_fmla = node_info fms #fmla target_node val new_node =
(new_node_name,
{role = TPTP_Syntax.Role_Plain,
fmla = apply_binding thy' prob_name orig_fmla target_fmla pdetails |> fst,
source_inf_opt =
SOME (TPTP_Proof.Inference (bindK, [], [pinfo]))}) in
((TPTP_Proof.Parent new_node_name, SOME new_node), thy') end
| _ => ((pinfo, NONE), intermediate_thy) fun process_nodes (step as (n, data)) (intermediate_thy, rest) = case #source_inf_opt data of
SOME (TPTP_Proof.Inference (inf_name, sinfos, pinfos)) => let val ((pinfos', parent_nodes), thy') =
fold_map (factor_out_bind n) pinfos intermediate_thy
|> apfst ListPair.unzip val step' =
(n, {role = #role data, fmla = #fmla data,
source_inf_opt = SOME (TPTP_Proof.Inference (inf_name, sinfos, pinfos'))}) in (thy', fold_options parent_nodes @ step' :: rest) end
| _ => (intermediate_thy, step :: rest) in
fold process_nodes fms (thy, []) (*new_nodes must come at the beginning, since we assume that the last line in a proof is the closing line*)
|> apsnd rev end
(** Proof transformer to add virtual inference steps encoding any transformation done immediately prior
to a splitting step **)
where "%" is either an "and" or an "iff" connective. This transformation is used to clarify the clause structure, to make it immediately "obvious" how splitting is taking place (by factoring out the other syntactic transformations -- e.g. related to quantifiers -- performed by Leo2). Having the clause in this "clearer" form makes the inference amenable to handling using the "abstraction" technique, which allows us to validate large inferences.
*)
exception PREPROCESS_SPLITS fun preprocess_splits prob_name thy fms : theory * formula_meaning list = let (*Simulate the transformation done by Leo2's preprocessing step during splitting. NOTE: we assume that the clause is a singleton
This transformation does the following: - miniscopes !-quantifiers (and recurs) - removes redundant ?-quantifiers (and recurs) - eliminates double negation (and recurs) - breaks up conjunction (and recurs)
- expands iff (and doesn't recur)*) fun transform_fmla i fmla_t = case fmla_t of Const (\<^const_name>\<open>HOL.All\<close>, ty) $ Abs (s, ty', t') => let val (i', fmla_ts) = transform_fmla i t' in if i' > i then
(i' + 1, map (fn t => Const (\<^const_name>\<open>HOL.All\<close>, ty) $ Abs (s, ty', t))
fmla_ts) else (i, [fmla_t]) end
| Const (\<^const_name>\<open>HOL.Ex\<close>, ty) $ Abs (s, ty', t') => if loose_bvar (t', 0) then
(i, [fmla_t]) else transform_fmla (i + 1) t'
| \<^term>\<open>HOL.Not\<close> $ (\<^term>\<open>HOL.Not\<close> $ t') =>
transform_fmla (i + 1) t'
| \<^term>\<open>HOL.conj\<close> $ t1 $ t2 => let val (i1, fmla_t1s) = transform_fmla (i + 1) t1 val (i2, fmla_t2s) = transform_fmla (i + 1) t2 in
(i1 + i2 - i, fmla_t1s @ fmla_t2s) end
| Const (\<^const_name>\<open>HOL.eq\<close>, ty) $ t1 $ t2 => let val (T1, (T2, res)) =
dest_funT ty
|> apsnd dest_funT in if T1 = HOLogic.boolT andalso T2 = HOLogic.boolT andalso
res = HOLogic.boolT then
(i + 1,
[HOLogic.mk_imp (t1, t2),
HOLogic.mk_imp (t2, t1)]) else (i, [fmla_t]) end
| _ => (i, [fmla_t])
fun preprocess_split thy split_node_name fmla_t = (*create new node which contains the new inference,
to be added to graph*) let val (node_name, thy') = get_next_name thy val (changes, fmla_conjs) =
transform_fmla 0 fmla_t
|> apsnd rev (*otherwise we run into problems because
of commutativity of conjunction*) val target_fmla =
fold (curry HOLogic.mk_conj) (tl fmla_conjs) (hd fmla_conjs) val new_node =
(node_name,
{role = TPTP_Syntax.Role_Plain,
fmla =
HOLogic.mk_eq (target_fmla, \<^term>\<open>False\<close>) (*polarise*)
|> HOLogic.mk_Trueprop,
source_inf_opt =
SOME (TPTP_Proof.Inference (split_preprocessingK, [], [TPTP_Proof.Parent split_node_name]))}) in if changes = 0 then NONE else SOME (TPTP_Proof.Parent node_name, new_node, thy') end in
fold
(fn step as (n, data) => fn (intermediate_thy, redirections, rest) => case #source_inf_opt data of
SOME (TPTP_Proof.Inference
(inf_name, sinfos, pinfos)) => if inf_name <> "split_conjecture"then
(intermediate_thy, redirections, step :: rest) else let (* NOTE: here we assume that the node only has one parent, and that there is no additional parent info.
*) val split_node_name = case pinfos of
[TPTP_Proof.Parent n] => n
| _ => raise PREPROCESS_SPLITS (*check if we've already handled that already node*) in case AList.lookup (op =) redirections split_node_name of
SOME preprocessed_split_node_name => let val step' =
apply_to_parent_info (fn _ => [TPTP_Proof.Parent preprocessed_split_node_name]) step in (intermediate_thy, redirections, step' :: rest) end
| NONE => let (*we know the polarity to be $false, from knowing Leo2*) val split_fmla =
try_dest_Trueprop (node_info fms #fmla split_node_name)
|> remove_polarity true
|> fst
val preprocess_result =
preprocess_split intermediate_thy
split_node_name
split_fmla in if is_none preprocess_result then (*no preprocessing done by Leo2, so no need to introduce a virtual inference. cache this result by
redirecting the split_node to itself*)
(intermediate_thy,
(split_node_name, split_node_name) :: redirections,
step :: rest) else let val (new_parent_info, new_parent_node, thy') = the preprocess_result val step' =
(n, {role = #role data, fmla = #fmla data,
source_inf_opt = SOME (TPTP_Proof.Inference (inf_name, sinfos, [new_parent_info]))}) in
(thy',
(split_node_name, fst new_parent_node) :: redirections,
step' :: new_parent_node :: rest) end end end
| _ => (intermediate_thy, redirections, step :: rest))
(rev fms) (*this allows us to put new inferences before other inferences which use them*)
(thy, [], [])
|> (fn (x, _, z) => (x, z)) (*discard redirection info*) end
(** Proof transformer to remove repeated quantification **)
exception DROP_REPEATED_QUANTIFICATION fun drop_repeated_quantification thy (fms : formula_meaning list) : theory * formula_meaning list = let (*In case of repeated quantification, removes outer quantification. Only need to look at top-level, since the repeated quantification
generally occurs at clause level*) fun remove_repeated_quantification seen t = case t of (*NOTE we're assuming that variables having the same name, have the same type throughout*) Const (\<^const_name>\<open>HOL.All\<close>, ty) $ Abs (s, ty', t') => let val (seen_so_far, seen') = case AList.lookup (op =) seen s of
NONE => (0, (s, 0) :: seen)
| SOME n => (n + 1, AList.update (op =) (s, n + 1) seen) val (pre_final_t, final_seen) = remove_repeated_quantification seen' t' val final_t = case AList.lookup (op =) final_seen s of
NONE => raise DROP_REPEATED_QUANTIFICATION
| SOME n => if n > seen_so_far then pre_final_t elseConst (\<^const_name>\<open>HOL.All\<close>, ty) $ Abs (s, ty', pre_final_t) in (final_t, final_seen) end
| _ => (t, seen)
(** Proof transformer to detect a redundant splitting and remove
the redundant branch. **)
fun node_is_inference fms rule_name node_name = case node_info fms #source_inf_opt node_name of
NONE => false
| SOME (TPTP_Proof.File _) => false
| SOME (TPTP_Proof.Inference (rule_name', _, _)) => rule_name' = rule_name
(*In this analysis we're interested if there exists a split-free path between the end of the proof and the negated conjecture. If so, then this path (or the shortest such path) could be
retained, and the rest of the proof erased.*) datatype branch_info =
Split_free (*Path is not part of a split. This is only used when path reaches the negated conjecture.*)
| Split_present (*Path is one of a number of splits. Such paths are excluded.*)
| Coinconsistent of int (*Path leads to a clause which is inconsistent with nodes concluded by other paths. Therefore this path should be kept if the others are kept
(i.e., unless one of them results from a split)*)
| No_info (*Analysis hasn't come across anything definite yet, though it still hasn't completed.*) (*A "paths" value consist of every way of reaching the destination,
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.34 Sekunden
(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.
