--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Wed Feb 19 15:57:02 2014 +0000
@@ -0,0 +1,1925 @@
+(* 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 of bool option
+ | Disjunctive of bool option
+ | Biimplicational of bool option
+ | Negative of bool option
+ | Existential of bool option * typ
+ | Universal of bool option * typ
+ | Equational of bool option * typ
+ | Atomic of bool option
+ | Implicational of bool option
+ 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 : string list}
+
+ 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
+
+structure TPTP_Reconstruct : TPTP_RECONSTRUCT =
+struct
+
+open TPTP_Reconstruct_Library
+open TPTP_Syntax
+
+(*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
+
+fun structure_fmla_meaning (s, r, t, info) =
+ (s, {role = r, fmla = t, source_inf_opt = info})
+
+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 = []
+ val extend = I
+ 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}
+ val extend = I
+ 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 : string list}
+
+(*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
+ fst (dest_Const t1) = @{const_name All} 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.*)
+ let val 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 then false
+ 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
+ |> single
+ |> Type_Infer_Context.infer_types (Context.proof_of (Context.Theory thy))
+ |> the_single
+ |> HOLogic.mk_Trueprop
+ |> rpair bindings'
+ end
+
+exception RECONSTRUCT of string
+
+(*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 of bool option
+ | Disjunctive of bool option
+ | Biimplicational of bool option
+ | Negative of bool option
+ | Existential of bool option * typ
+ | Universal of bool option * typ
+ | Equational of bool option * typ
+ | Atomic of bool option
+ | Implicational of bool option
+
+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 =
+ case try HOLogic.dest_eq formula of
+ NONE => if strict then raise (UNPOLARISED formula)
+ else (formula, true)
+ | SOME (x, p as @{term True}) => (x, true)
+ | SOME (x, p as @{term False}) => (x, false)
+ | SOME (x, _) =>
+ if strict then raise (UNPOLARISED formula)
+ else (formula, true)
+
+(*flattens a formula wrt associative operators*)
+fun flatten formula_kind formula =
+ let
+ fun is_conj (Const (@{const_name HOL.conj}, _) $ _ $ _) = true
+ | is_conj _ = false
+ fun is_disj (Const (@{const_name HOL.disj}, _) $ _ $ _) = true
+ | is_disj _ = false
+ fun is_iff (Const (@{const_name HOL.eq}, ty) $ _ $ _) =
+ ty = ([HOLogic.boolT, HOLogic.boolT] ---> HOLogic.boolT)
+ | is_iff _ = false
+
+ fun flatten' formula acc =
+ case formula of
+ Const (@{const_name HOL.conj}, _) $ 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 HOL.disj}, _) $ 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 HOL.eq}, 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 =
+ List.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 of string
+(*BFS for an ancestor inference involving a specific rule*)
+fun find_ancestor_using_rule pannot inference_rule (fringe : string list) : 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 of string
+
+ (*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)) =>
+ if List.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
+
+
+(** Proof skeleton **)
+
+(* Emulating skeleton steps *)
+
+(*
+Builds a rule (thm) of the following form:
+
+
+ prem1 premn
+ ... ... ...
+ major_prem conc1 concn
+ -----------------------------------------------
+ conclusion
+
+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:
+
+ P
+ -------------------------------
+ _ = $false _ = $false
+ ... ... ...
+ R1 Rn
+ -------------------------------
+ R1 & ... & Rn
+
+ Splitting (binary) iffs works 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 (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*) (*FIXME "inodes" should be made into Synth_steps*)
+ | 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_is_ax_or_def (Axiom _) = true
+ | stock_is_ax_or_def (Definition _) = true
+ | stock_is_ax_or_def _ = false
+
+ 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]
+ else if node_info (#meta pannot) #role n = TPTP_Syntax.Role_Axiom then
+ [Axiom n]
+ else raise 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*)
+ List.concat skeletons_up @ [Assumed] (*this will discharge the minor premises*)
+ end
+ else if 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
+ if List.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 atac) THEN rest (tl skel) memo
+ | Caboose => TRY (HEADGOAL atac)
+ | Unconjoin => rtac @{thm 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
+ rtac split_thm 1 THEN rest (tl skel) memo
+ end
+ | Step s =>
+ let
+ val (tac, memo') = tac_and_memo s memo
+ in
+ rtac tac 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 =>
+ Binding.dest binding
+ |> #3
+ |> Global_Theory.get_thm thy
+ in
+ rtac 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 =>
+ Binding.dest binding
+ |> #3
+ |> Global_Theory.get_thm thy
+ in
+ rtac 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
+
+ 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*)
+ (* TimeLimit.timeLimit (Time.fromSeconds 5) *)
+ (fn ctxt' =>
+ let
+ fun thm ctxt'' = prover_tac ctxt'' prob_name (hd skel |> stock_to_string)
+ val reconstructed_inference = thm ctxt'
+ val rec_inf_tac = fn st =>
+ let
+ val ctxt =
+ Thm.theory_of_thm st
+ |> Proof_Context.init_global
+ in
+ HEADGOAL (rtac (thm ctxt)) st
+ end
+ in (reconstructed_inference,
+ rec_inf_tac)
+ end)
+ fun ignore_interpretation_exn f x = SOME (f x)
+ handle
+ INTERPRET_INFERENCE => NONE
+ | exn => reraise exn
+ in
+ if List.null skel then
+ raise SKELETON
+ (*FIXME or classify it as follows:
+ [(Caboose,
+ prop_of @{thm asm_rl}
+ |> SOME,
+ SOME (@{thm asm_rl}, TRY (HEADGOAL atac)))]
+ *)
+ else
+ case hd skel of
+ Assumed =>
+ (hd skel,
+ prop_of @{thm asm_rl}
+ |> SOME,
+ SOME (@{thm asm_rl}, TRY (HEADGOAL atac))) :: rest memo ctxt
+ | Caboose =>
+ [(Caboose,
+ prop_of @{thm asm_rl}
+ |> SOME,
+ SOME (@{thm asm_rl}, TRY (HEADGOAL atac)))]
+ | Unconjoin =>
+ (hd skel,
+ prop_of @{thm conjI}
+ |> SOME,
+ SOME (@{thm conjI}, rtac @{thm 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,
+ prop_of split_thm
+ |> SOME,
+ SOME (split_thm, rtac 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
+ 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 =>
+ Binding.dest binding
+ |> #3
+ |> Global_Theory.get_thm thy
+ in
+ (hd skel,
+ prop_of (def_thm thy)
+ |> SOME,
+ SOME (def_thm thy,
+ HEADGOAL (rtac_wrap def_thm))) :: 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 =>
+ Binding.dest binding
+ |> #3
+ |> Global_Theory.get_thm thy
+ in
+ (hd skel,
+ prop_of ax_thm
+ |> SOME,
+ SOME (ax_thm, rtac 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 (rtac 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
+ rtac @{thm ccontr} 1
+ THEN dtac 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", prop_of @{thm ccontr} |> SOME,
+ SOME (@{thm ccontr}, rtac @{thm ccontr} 1)) ::
+ (Synth_step "neg_eq_false", prop_of neg_eq_false |> SOME,
+ SOME (neg_eq_false, dtac neg_eq_false 1)) ::
+ (Synth_step "sas_if_needed_tac", 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
+ |> List.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}
+ else if 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 =
+ List.filter
+ (fn n => not (List.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 (List.last (space_explode "." 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 HOL.Trueprop}, _) $
+ (Const (@{const_name HOL.eq}, _) $
+ 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 **)
+
+(*
+Involves finding an inference of this form:
+
+ (!x1 ... xn. F) ... Cn
+ ------------------------------------ (Rule name)
+ G[t1/x1, ..., tn/xn]
+
+and turn it into this:
+
+
+ (!x1 ... xn. F)
+ ---------------------- bind
+ F[t1/x1, ..., tn/xn] ... Cn
+ -------------------------------------------- (Rule name)
+ G
+
+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 **)
+
+(*
+Involves finding an inference of this form:
+
+ F = $false
+ ----------------------------------- split_conjecture
+ (F1 = $false) ... (Fn = $false)
+
+where F doesn't have an "and" or "iff" at the top level,
+and turn it into this:
+
+ F = $false
+ ----------------------------------- split_preprocessing
+ (F1 % ... % Fn) = $false
+ ----------------------------------- split_conjecture
+ (F1 = $false) ... (Fn = $false)
+
+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 "HOL.All"}, 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 "HOL.All"}, ty) $ Abs (s, ty', t))
+ fmla_ts)
+ else (i, [fmla_t])
+ end
+ | Const (@{const_name "HOL.Ex"}, ty) $ Abs (s, ty', t') =>
+ if loose_bvar (t', 0) then
+ (i, [fmla_t])
+ else transform_fmla (i + 1) t'
+ | @{term HOL.Not} $ (@{term HOL.Not} $ t') =>
+ transform_fmla (i + 1) t'
+ | @{term HOL.conj} $ 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 HOL.eq}, 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 False}) (*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 "HOL.All"}, 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
+ else Const (@{const_name "HOL.All"}, ty) $ Abs (s, ty', pre_final_t)
+ in (final_t, final_seen) end
+ | _ => (t, seen)
+
+ fun remove_repeated_quantification' (n, {role, fmla, source_inf_opt}) =
+ (n,
+ {role = role,
+ fmla =
+ try_dest_Trueprop fmla
+ |> remove_repeated_quantification []
+ |> fst
+ |> HOLogic.mk_Trueprop,
+ source_inf_opt = source_inf_opt})
+ in
+ (thy, map remove_repeated_quantification' fms)
+ end
+
+
+(** 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,
+ including information come across it so far. Taking the head of
+ each way gives the fringe. All paths should share the same source
+ and sink.*)
+type path = (branch_info * string list)
+exception PRUNE_REDUNDANT_SPLITS
+fun prune_redundant_splits prob_name thy fms : theory * formula_meaning list =
+ let
+ (*All paths start at the contradiction*)
+ val initial_path = (No_info, [proof_end_node fms])
+ (*All paths should end at the proof's beginning*)
+ val end_node = proof_beginning_node fms
+
+ fun compute_path (path as ((info,
+ (n :: ns)) : path))(*i.e. node list can't be empty*)
+ intermediate_thy =
+ case info of
+ Split_free => (([path], []), intermediate_thy)
+ | Coinconsistent branch_id =>
+ (*If this branch has a split_conjecture parent then all "sibling" branches get erased.*)
+ (*This branch can't lead to yet another coinconsistent branch (in the case of Leo2).*)
+ let
+ val parent_nodes = parents_of_node fms n
+ in
+ if List.exists (node_is_inference fms "split_conjecture") parent_nodes then
+ (([], [branch_id]), intermediate_thy) (*all related branches are to be deleted*)
+ else
+ list_prod [] parent_nodes (n :: ns)
+ |> map (fn ns' => (Coinconsistent branch_id, ns'))
+ |> (fn x => ((x, []), intermediate_thy))
+ end
+
+ | No_info =>
+ let
+ val parent_nodes = parents_of_node fms n
+
+ (*if this node is a consistency checking node then parent nodes will be marked as coinconsistent*)
+ val (thy', new_branch_info) =
+ if node_is_inference fms "fo_atp_e" n orelse
+ node_is_inference fms "res" n then
+ let
+ val (i', intermediate_thy') = get_next_int intermediate_thy
+ in
+ (intermediate_thy', SOME (Coinconsistent i'))
+ end
+ else (intermediate_thy, NONE)
+ in
+ if List.exists (node_is_inference fms "split_conjecture") parent_nodes then
+ (([], []), thy')
+ else
+ list_prod [] parent_nodes (n :: ns)
+ |> map (fn ns' =>
+ let
+ val info =
+ if is_some new_branch_info then the new_branch_info
+ else
+ if hd ns' = end_node then Split_free else No_info
+ in (info, ns') end)
+ |> (fn x => ((x, []), thy'))
+ end
+ | _ => raise PRUNE_REDUNDANT_SPLITS
+
+ fun compute_paths intermediate_thy (paths : path list) =
+ if filter (fn (_, ns) => ns <> [] andalso hd ns = end_node) paths = paths then
+ (*fixpoint reached when all paths are at the head position*)
+ (intermediate_thy, paths)
+ else
+ let
+ val filtered_paths = filter (fn (info, _) : path => info <> Split_present) paths (*not interested in paths containing a split*)
+ val (paths', thy') =
+ fold_map compute_path filtered_paths intermediate_thy
+ in
+ paths'
+ |> ListPair.unzip (*we get a list of pairs of lists. we want a pair of lists*)
+ |> (fn (paths, branch_ids) =>
+ (List.concat paths,
+ (*remove duplicate branch_ids*)
+ fold (Library.insert (op =)) (List.concat branch_ids) []))
+ (*filter paths having branch_ids appearing in the second list*)
+ |> (fn (paths, branch_ids) =>
+ filter (fn (info, _) =>
+ case info of
+ Coinconsistent branch_id => List.exists (fn x => x = branch_id) branch_ids
+ | _ => true) paths)
+ |> compute_paths thy'
+ end
+
+ val (thy', paths) =
+ compute_paths thy [initial_path]
+ |> apsnd
+ (filter (fn (branch_info, _) =>
+ case branch_info of
+ Split_free => true
+ | Coinconsistent _ => true
+ | _ => false))
+ (*Extract subset of fms which is used in a path.
+ Also, remove references (in parent info annotations) to erased nodes.*)
+ fun path_to_fms ((_, nodes) : path) =
+ fold
+ (fn n => fn fms' =>
+ case AList.lookup (op =) fms' n of
+ SOME _ => fms'
+ | NONE =>
+ let
+ val node_info = the (AList.lookup (op =) fms n)
+
+ val source_info' =
+ case #source_inf_opt node_info of
+ NONE => error "Only the conjecture is an orphan"
+ | SOME (source_info as TPTP_Proof.File _) => source_info
+ | SOME (source_info as
+ TPTP_Proof.Inference (inference_name,
+ useful_infos : TPTP_Proof.useful_info_as list,
+ parent_infos)) =>
+ let
+ fun is_node_in_fms' parent_info =
+ let
+ val parent_nodename =
+ case parent_info of
+ TPTP_Proof.Parent n => n
+ | TPTP_Proof.ParentWithDetails (n, _) => n
+ in
+ case AList.lookup (op =) fms' parent_nodename of
+ NONE => false
+ | SOME _ => true
+ end
+ in
+ TPTP_Proof.Inference (inference_name,
+ useful_infos,
+ filter is_node_in_fms' parent_infos)
+ end
+ in
+ (n,
+ {role = #role node_info,
+ fmla = #fmla node_info,
+ source_inf_opt = SOME source_info'}) :: fms'
+ end)
+ nodes
+ []
+ in
+ if null paths then (thy', fms) else
+ (thy',
+ hd(*FIXME could pick path based on length, or some notion of "difficulty"*) paths
+ |> path_to_fms)
+ end
+
+
+(*** Main functions ***)
+
+(*interpret proof*)
+fun import_thm cautious path_prefixes file_name
+ (on_load : proof_annotation -> theory -> (proof_annotation * theory)) thy =
+ let
+ val prob_name =
+ Path.base file_name
+ |> Path.implode
+ |> TPTP_Problem_Name.parse_problem_name
+ val thy1 = TPTP_Interpret.import_file cautious path_prefixes file_name [] [] thy
+ val fms = get_fmlas_of_prob thy1 prob_name
+ in
+ if List.null fms then
+ (warning ("File " ^ Path.implode file_name ^ " appears empty!");
+ TPTP_Reconstruction_Data.map (cons ((prob_name, empty_pannot prob_name))) thy1)
+ else
+ let
+ val defn_equations =
+ List.filter (fn (_, role, _, _) => role = TPTP_Syntax.Role_Definition) fms
+ |> map (fn (node, _, t, _) =>
+ (node,
+ get_defn_components t
+ |> mk_bind_eq prob_name []))
+ val axioms =
+ List.filter (fn (_, role, _, _) => role = TPTP_Syntax.Role_Axiom) fms
+ |> map (fn (node, _, t, _) =>
+ (node,
+ mk_bind_ax prob_name node t))
+
+ (*add definitions and axioms to the theory*)
+ val thy2 =
+ fold
+ (fn bnd => fn thy =>
+ let
+ val ((name, thm), thy') = Thm.add_axiom_global bnd thy
+ in Global_Theory.add_thm ((#1 bnd, thm), []) thy' |> #2 end)
+ (map snd defn_equations @ map snd axioms)
+ thy1
+
+ (*apply global proof transformations*)
+ val (thy3, pre_pannot) : theory * proof_annotation =
+ transf_pannot
+ (prune_redundant_splits prob_name thy2
+ #-> interpolate_binds prob_name
+ #-> preprocess_splits prob_name
+ #-> drop_repeated_quantification)
+ {problem_name = prob_name,
+ skolem_defs = [],
+ defs = map (apsnd fst) defn_equations,
+ axs = map (apsnd fst) axioms,
+ meta = map (fn (n, r, t, info) => (n, {role=r, fmla=t, source_inf_opt=info})) fms}
+
+ (*store pannot*)
+ val thy4 = TPTP_Reconstruction_Data.map (cons ((prob_name, pre_pannot))) thy3
+
+ (*run hook, which might result in changed pannot and theory*)
+ val (pannot, thy5) = on_load pre_pannot thy4
+
+ (*store the most recent pannot*)
+ in TPTP_Reconstruction_Data.map (cons ((prob_name, pannot))) thy5 end
+ end
+
+(*This has been disabled since it requires a hook to be specified to use "import_thm"
+val _ =
+ Outer_Syntax.improper_command @{command_spec "import_leo2_proof"} "import TPTP proof"
+ (Parse.path >> (fn name =>
+ Toplevel.theory (fn thy =>
+ let val path = Path.explode name
+ in import_thm true [Path.dir path, Path.explode "$TPTP"] path (*FIXME hook needs to be given here*)
+thy end)))
+*)
+
+
+(** Archive **)
+(*FIXME move elsewhere*)
+(*This contains currently unused, but possibly useful, functions written
+ during experimentation, in case they are useful later on*)
+
+(*given a list of rules and a node, return
+ SOME (rule name) if that node's rule name
+ belongs to the list of rules*)
+fun match_rules_of_current (pannot : proof_annotation) rules n =
+ case node_info (#meta pannot) #source_inf_opt n of
+ NONE => NONE
+ | SOME (TPTP_Proof.File _) => NONE
+ | SOME (TPTP_Proof.Inference (rule_name, _ : TPTP_Proof.useful_info_as list, _)) =>
+ if member (op =) rules rule_name then SOME rule_name else NONE
+
+(*given a node and a list of rules, determine
+ whether all the rules can be matched to
+ parent nodes. If nonstrict then there may be
+ more parents than given rules.*)
+fun match_rules_of_immediate_previous (pannot : proof_annotation) strict rules n =
+ case node_info (#meta pannot) #source_inf_opt n of
+ NONE => null rules
+ | SOME (TPTP_Proof.File _) => null rules
+ | SOME (TPTP_Proof.Inference (rule_name, _ : TPTP_Proof.useful_info_as list, parent_infos)) =>
+ let
+ val matched_rules : string option list =
+ map (match_rules_of_current pannot rules)
+ (dest_parent_infos true (#meta pannot) parent_infos |> map #name)
+ in
+ if strict andalso member (op =) matched_rules NONE then false
+ else
+ (*check that all the rules were matched*)
+ fold
+ (fn (rule : string) => fn (st, matches : string option list) =>
+ if not st then (st, matches)
+ else
+ let
+ val idx = find_index (fn match => SOME rule = match) matches
+ in
+ if idx < 0 then (false, matches)
+ else
+ (st, nth_drop idx matches)
+ end)
+ rules
+ (true, matched_rules)
+ |> #1 (*discard the other info*)
+ end
+end