src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML
author paulson <lp15@cam.ac.uk>
Fri, 08 Aug 2025 16:46:03 +0100
changeset 82969 dedd9d13c79c
parent 80667 b167ec56056f
permissions -rw-r--r--
Generalised a theorem about Lebesgue integration
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
     1
(*  Title:      HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
     2
    Author:     Nik Sultana, Cambridge University Computer Laboratory
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
     3
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
     4
Reconstructs TPTP proofs in Isabelle/HOL.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
     5
Specialised to work with proofs produced by LEO-II.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
     6
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
     7
TODO
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
     8
 - Proof transformation to remove "copy" steps, and perhaps other dud inferences.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
     9
*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    10
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    11
signature TPTP_RECONSTRUCT =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    12
sig
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    13
  (* Interface used by TPTP_Reconstruct.thy, to define LEO-II proof reconstruction. *)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    14
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    15
  datatype formula_kind =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    16
      Conjunctive of bool option
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    17
    | Disjunctive of bool option
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    18
    | Biimplicational of bool option
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    19
    | Negative of bool option
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    20
    | Existential of bool option * typ
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    21
    | Universal of bool option * typ
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    22
    | Equational of bool option * typ
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    23
    | Atomic of bool option
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    24
    | Implicational of bool option
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    25
  type formula_meaning =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    26
    (string *
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    27
     {role : TPTP_Syntax.role,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    28
      fmla : term,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    29
      source_inf_opt : TPTP_Proof.source_info option})
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    30
  type proof_annotation =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    31
    {problem_name : TPTP_Problem_Name.problem_name,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    32
     skolem_defs : ((*skolem const name*)string * Binding.binding) list,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    33
     defs : ((*node name*)string * Binding.binding) list,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    34
     axs : ((*node name*)string * Binding.binding) list,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    35
     (*info for each node (for all lines in the TPTP proof)*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    36
     meta : formula_meaning list}
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    37
  type rule_info =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    38
    {inference_name : string, (*name of calculus rule*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    39
     inference_fmla : term, (*the inference as a term*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    40
     parents : string list}
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    41
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    42
  exception UNPOLARISED of term
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    43
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    44
  val remove_polarity : bool -> term -> term * bool
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    45
  val interpret_bindings :
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    46
     TPTP_Problem_Name.problem_name -> theory -> TPTP_Proof.parent_detail list -> (string * term) list -> (string * term) list
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    47
  val diff_and_instantiate : Proof.context -> thm -> term -> term -> thm (*FIXME from library*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    48
  val strip_top_all_vars : (string * typ) list -> term -> (string * typ) list * term
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    49
  val strip_top_All_vars : term -> (string * typ) list * term
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    50
  val strip_top_All_var : term -> (string * typ) * term
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    51
  val new_consts_between : term -> term -> term list
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    52
  val get_pannot_of_prob : theory -> TPTP_Problem_Name.problem_name -> proof_annotation
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    53
  val inference_at_node : 'a -> TPTP_Problem_Name.problem_name -> formula_meaning list -> string -> rule_info option
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    54
  val node_info : (string * 'a) list -> ('a -> 'b) -> string -> 'b
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    55
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    56
  type step_id = string
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    57
  datatype rolling_stock =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    58
      Step of step_id
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    59
    | Assumed
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    60
    | Unconjoin
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    61
    | Split of step_id (*where split occurs*) *
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    62
               step_id (*where split ends*) *
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    63
               step_id list (*children of the split*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    64
    | Synth_step of step_id (*A step which doesn't necessarily appear in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    65
      the original proof, or which has been modified slightly for better
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    66
      handling by Isabelle*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    67
    | Annotated_step of step_id * string (*Same interpretation as
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    68
      "Step", except that additional information is attached. This is
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    69
      currently used for debugging: Steps are mapped to Annotated_steps
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    70
      and their rule names are included as strings*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    71
    | Definition of step_id (*Mirrors TPTP role*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    72
    | Axiom of step_id (*Mirrors TPTP role*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    73
    | Caboose
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    74
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    75
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    76
  (* Interface for using the proof reconstruction. *)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    77
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    78
  val import_thm : bool -> Path.T list -> Path.T -> (proof_annotation -> theory -> proof_annotation * theory) -> theory -> theory
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    79
  val get_fmlas_of_prob : theory -> TPTP_Problem_Name.problem_name -> TPTP_Interpret.tptp_formula_meaning list
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    80
  val structure_fmla_meaning : 'a * 'b * 'c * 'd -> 'a * {fmla: 'c, role: 'b, source_inf_opt: 'd}
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    81
  val make_skeleton : Proof.context -> proof_annotation -> rolling_stock list
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    82
  val naive_reconstruct_tacs :
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    83
     (Proof.context -> TPTP_Problem_Name.problem_name -> step_id -> thm) ->
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    84
     TPTP_Problem_Name.problem_name -> Proof.context -> (rolling_stock * term option * (thm * tactic) option) list
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    85
  val naive_reconstruct_tac :
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    86
     Proof.context -> (Proof.context -> TPTP_Problem_Name.problem_name -> step_id -> thm) -> TPTP_Problem_Name.problem_name -> tactic
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    87
  val reconstruct : Proof.context -> (TPTP_Problem_Name.problem_name -> tactic) -> TPTP_Problem_Name.problem_name -> thm
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    88
end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    89
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    90
structure TPTP_Reconstruct : TPTP_RECONSTRUCT =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    91
struct
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    92
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    93
open TPTP_Reconstruct_Library
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    94
open TPTP_Syntax
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    95
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    96
(*FIXME move to more general struct*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    97
(*Extract the formulas of an imported TPTP problem -- these formulas
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    98
  may make up a proof*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
    99
fun get_fmlas_of_prob thy prob_name : TPTP_Interpret.tptp_formula_meaning list =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   100
  AList.lookup (op =) (TPTP_Interpret.get_manifests thy) prob_name
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   101
  |> the |> #3 (*get formulas*);
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   102
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   103
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   104
(** General **)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   105
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   106
(* Proof annotations *)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   107
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   108
(*FIXME modify TPTP_Interpret.tptp_formula_meaning into this type*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   109
type formula_meaning =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   110
  (string *
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   111
   {role : TPTP_Syntax.role,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   112
    fmla : term,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   113
    source_inf_opt : TPTP_Proof.source_info option})
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   114
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   115
fun apply_to_parent_info f
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   116
   (n, {role, fmla, source_inf_opt}) =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   117
  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   118
    val source_inf_opt' =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   119
      case source_inf_opt of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   120
          NONE => NONE
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   121
        | SOME (TPTP_Proof.Inference (inf_name, sinfos, pinfos)) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   122
            SOME (TPTP_Proof.Inference (inf_name, sinfos, f pinfos))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   123
  in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   124
   (n, {role = role, fmla = fmla, source_inf_opt = source_inf_opt'})
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   125
  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   126
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   127
fun structure_fmla_meaning (s, r, t, info) =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   128
  (s, {role = r, fmla = t, source_inf_opt = info})
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   129
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   130
type proof_annotation =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   131
  {problem_name : TPTP_Problem_Name.problem_name,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   132
   skolem_defs : ((*skolem const name*)string * Binding.binding) list,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   133
   defs : ((*node name*)string * Binding.binding) list,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   134
   axs : ((*node name*)string * Binding.binding) list,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   135
   (*info for each node (for all lines in the TPTP proof)*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   136
   meta : formula_meaning list}
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   137
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   138
fun empty_pannot prob_name =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   139
  {problem_name = prob_name,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   140
   skolem_defs = [],
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   141
   defs = [],
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   142
   axs = [],
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   143
   meta = []}
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   144
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   145
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   146
(* Storage of proof data *)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   147
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   148
exception MANIFEST of TPTP_Problem_Name.problem_name * string (*FIXME move to TPTP_Interpret?*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   149
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   150
type manifest = TPTP_Problem_Name.problem_name * proof_annotation
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   151
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   152
(*manifest equality simply depends on problem name*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   153
fun manifest_eq ((prob_name1, _), (prob_name2, _)) = prob_name1 = prob_name2
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   154
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   155
structure TPTP_Reconstruction_Data = Theory_Data
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   156
(
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   157
  type T = manifest list
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   158
  val empty = []
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   159
  fun merge data : T = Library.merge manifest_eq data
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   160
)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   161
val get_manifests : theory -> manifest list = TPTP_Reconstruction_Data.get
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   162
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   163
fun update_manifest prob_name pannot thy =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   164
  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   165
    val idx =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   166
      find_index
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   167
        (fn (n, _) => n = prob_name)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   168
        (get_manifests thy)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   169
    val transf = (fn _ =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   170
      (prob_name, pannot))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   171
  in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   172
    TPTP_Reconstruction_Data.map
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   173
      (nth_map idx transf)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   174
      thy
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   175
  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   176
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   177
(*similar to get_fmlas_of_prob but for proofs*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   178
fun get_pannot_of_prob thy prob_name : proof_annotation =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   179
  case AList.lookup (op =) (get_manifests thy) prob_name of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   180
      SOME pa => pa
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   181
    | NONE => raise (MANIFEST (prob_name, "Could not find proof annotation"))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   182
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   183
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   184
(* Constants *)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   185
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   186
(*Prefix used for naming inferences which were added during proof
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   187
transformation. (e.g., this is used to name "bind"-inference nodes
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   188
described below)*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   189
val inode_prefixK = "inode"
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   190
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   191
(*New inference rule name, which is added to indicate that some
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   192
variable has been instantiated. Additional proof metadata will
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   193
indicate which variable, and how it was instantiated*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   194
val bindK = "bind"
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   195
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   196
(*New inference rule name, which is added to indicate that some
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   197
(validity-preserving) preprocessing has been done to a (singleton)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   198
clause prior to it being split.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   199
val split_preprocessingK = "split_preprocessing"
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   200
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   201
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   202
(* Storage of internal values *)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   203
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   204
type tptp_reconstruction_state = {next_int : int}
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   205
structure TPTP_Reconstruction_Internal_Data = Theory_Data
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   206
(
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   207
  type T = tptp_reconstruction_state
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   208
  val empty = {next_int = 0}
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   209
  fun merge data : T = snd data
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   210
)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   211
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   212
(*increment internal counter, and obtain the current next value*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   213
fun get_next_int thy : int * theory =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   214
  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   215
    val state = TPTP_Reconstruction_Internal_Data.get thy
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   216
    val state' = {next_int = 1 + #next_int state}
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   217
  in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   218
    (#next_int state,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   219
     TPTP_Reconstruction_Internal_Data.put state' thy)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   220
  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   221
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   222
(*FIXME in some applications (e.g. where the name is used for an
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   223
   inference node) need to check that the name is fresh, to avoid
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   224
   collisions with other bits of the proof*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   225
val get_next_name =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   226
  get_next_int
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   227
  #> apfst (fn i => inode_prefixK ^ Int.toString i)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   228
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   229
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   230
(* Building the index *)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   231
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   232
(*thrown when we're expecting a TPTP_Proof.Bind annotation but find something else*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   233
exception NON_BINDING
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   234
(*given a list of pairs consisting of a variable name and
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   235
  TPTP formula, returns the list consisting of the original
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   236
  variable name and the interpreted HOL formula. Needs the
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   237
  problem name to ensure use of correct interpretations for
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   238
  constants and types.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   239
fun interpret_bindings (prob_name : TPTP_Problem_Name.problem_name) thy bindings acc =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   240
  if null bindings then acc
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   241
  else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   242
    case hd bindings of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   243
        TPTP_Proof.Bind (v, fmla) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   244
          let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   245
            val (type_map, const_map) =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   246
                case AList.lookup (op =) (TPTP_Interpret.get_manifests thy) prob_name of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   247
                    NONE => raise (MANIFEST (prob_name, "Problem details not found in interpretation manifest"))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   248
                  | SOME (type_map, const_map, _) => (type_map, const_map)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   249
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   250
            (*FIXME get config from the envir or make it parameter*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   251
            val config =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   252
              {cautious = true,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   253
               problem_name = SOME prob_name}
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   254
            val result =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   255
              (v,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   256
               TPTP_Interpret.interpret_formula
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   257
                config TPTP_Syntax.THF
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   258
                const_map [] type_map fmla thy
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   259
               |> fst)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   260
          in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   261
            interpret_bindings prob_name thy (tl bindings) (result :: acc)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   262
          end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   263
      | _ => raise NON_BINDING
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   264
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   265
type rule_info =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   266
  {inference_name : string, (*name of calculus rule*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   267
   inference_fmla : term, (*the inference as a term*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   268
   parents : string list}
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   269
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   270
(*Instantiates a binding in orig_parent_fmla. Used in a proof
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   271
  transformation to factor out instantiations from inferences.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   272
fun apply_binding thy prob_name orig_parent_fmla target_fmla bindings =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   273
  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   274
    val bindings' = interpret_bindings prob_name thy bindings []
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   275
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   276
    (*capture selected free variables. these variables, and their
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   277
      intended de Bruijn index, are included in "var_ctxt"*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   278
    fun bind_free_vars var_ctxt t =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   279
      case t of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   280
          Const _ => t
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   281
        | Var _ => t
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   282
        | Bound _ => t
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   283
        | Abs (x, ty, t') => Abs (x, ty, bind_free_vars (x :: var_ctxt) t')
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   284
        | Free (x, ty) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   285
            let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   286
              val idx = find_index (fn y => y = x) var_ctxt
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   287
            in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   288
              if idx > ~1 andalso
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   289
                 ty = dummyT (*this check not really needed*) then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   290
                  Bound idx
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   291
              else t
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   292
            end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   293
        | t1 $ t2 => bind_free_vars var_ctxt t1 $ bind_free_vars var_ctxt t2
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   294
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   295
    (*Instantiate specific quantified variables:
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   296
      Look for subterms of form (! (% x. M)) where "x" appears as a "bound_var",
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   297
      then replace "x" for "body" in "M".
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   298
      Should only be applied at formula top level -- i.e., once past the quantifier
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   299
      prefix we needn't bother with looking for bound_vars.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   300
      "var"_ctxt is used to keep track of lambda-bindings we encounter, to capture
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   301
      free variables in "body" correctly (i.e., replace Free with Bound having the
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   302
      right index)*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   303
    fun instantiate_bound (binding as (bound_var, body)) (initial as (var_ctxt, t))  =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   304
      case t of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   305
          Const _ => initial
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   306
        | Free _ => initial
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   307
        | Var _ => initial
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   308
        | Bound _ => initial
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   309
        | Abs _ => initial
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   310
        | t1 $ (t2 as Abs (x, ty, t')) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   311
            if is_Const t1 then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   312
              (*Could be fooled by shadowing, but if order matters
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   313
                then should still be able to handle formulas like
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   314
                (! X, X. F).*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   315
              if x = bound_var andalso
80636
4041e7c8059d tuned: more explicit dest_Const_name and dest_Const_type;
wenzelm
parents: 74561
diff changeset
   316
                 dest_Const_name t1 = \<^const_name>\<open>All\<close> then
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   317
                  (*Body might contain free variables, so bind them using "var_ctxt".
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   318
                    this involves replacing instances of Free with instances of Bound
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   319
                    at the right index.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   320
                  let val body' = bind_free_vars var_ctxt body
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   321
                  in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   322
                    (var_ctxt,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   323
                     betapply (t2, body'))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   324
                  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   325
              else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   326
                  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   327
                    val (var_ctxt', rest) = instantiate_bound binding (x :: var_ctxt, t')
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   328
                  in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   329
                    (var_ctxt',
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   330
                     t1 $ Abs (x, ty, rest))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   331
                  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   332
            else initial
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   333
        | t1 $ t2 =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   334
            let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   335
              val (var_ctxt', rest) = instantiate_bound binding (var_ctxt, t2)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   336
            in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   337
              (var_ctxt', t1 $ rest)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   338
            end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   339
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   340
    (*Here we preempt the following problem:
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   341
     if have (! X1, X2, X3. body), and X1 is instantiated to
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   342
     "c X2 X3", then the current code will yield
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   343
     (! X2, X3, X2a, X3a. body').
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   344
     To avoid this, we must first push X1 in, before calling
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   345
     instantiate_bound, to make sure that bound variables don't
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   346
     get free.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   347
    fun safe_instantiate_bound (binding as (bound_var, body)) (var_ctxt, t) =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   348
       instantiate_bound binding
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   349
         (var_ctxt, push_allvar_in bound_var t)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   350
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   351
    (*return true if one of the types is polymorphic*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   352
    fun is_polymorphic tys =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   353
      if null tys then false
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   354
      else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   355
        case hd tys of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   356
            Type (_, tys') => is_polymorphic (tl tys @ tys')
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   357
          | TFree _ => true
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   358
          | TVar _ => true
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   359
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   360
    (*find the type of a quantified variable, at the "topmost" binding
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   361
      occurrence*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   362
    local
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   363
      fun type_of_quantified_var' s ts =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   364
        if null ts then NONE
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   365
        else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   366
          case hd ts of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   367
              Const _ => type_of_quantified_var' s (tl ts)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   368
            | Free _ => type_of_quantified_var' s (tl ts)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   369
            | Var _ => type_of_quantified_var' s (tl ts)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   370
            | Bound _ => type_of_quantified_var' s (tl ts)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   371
            | Abs (s', ty, t') =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   372
                if s = s' then SOME ty
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   373
                else type_of_quantified_var' s (t' :: tl ts)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   374
            | t1 $ t2 => type_of_quantified_var' s (t1 :: t2 :: tl ts)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   375
    in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   376
      fun type_of_quantified_var s =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   377
        single #> type_of_quantified_var' s
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   378
    end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   379
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   380
    (*Form the universal closure of "t".
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   381
      NOTE remark above "val frees" about ordering of quantified variables*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   382
    fun close_formula t =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   383
      let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   384
          (*The ordering of Frees in this list affects the order in which variables appear
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   385
            in the quantification prefix. Currently this is assumed not to matter.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   386
            This consists of a list of pairs: the first element consists of the "original"
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   387
            free variable, and the latter consists of the monomorphised equivalent. The
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   388
            two elements are identical if the original is already monomorphic.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   389
            This monomorphisation is needed since, owing to TPTP's lack of type annotations,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   390
            variables might not be constrained by type info. This results in them being
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   391
            interpreted as polymorphic. E.g., this issue comes up in CSR148^1*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   392
          val frees_monomorphised =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   393
            fold_aterms
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   394
              (fn t => fn rest =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   395
                 if is_Free t then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   396
                   let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   397
                     val (s, ty) = dest_Free t
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   398
                     val ty' =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   399
                       if ty = dummyT orelse is_polymorphic [ty] then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   400
                         the (type_of_quantified_var s target_fmla)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   401
                       else ty
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   402
                   in insert (op =) (t, Free (s, ty')) rest
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   403
                   end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   404
                 else rest)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   405
              t []
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   406
      in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   407
        Term.subst_free frees_monomorphised t
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   408
        |> fold (fn (s, ty) => fn t =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   409
                    HOLogic.mk_all (s, ty, t))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   410
              (map (snd #> dest_Free) frees_monomorphised)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   411
      end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   412
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   413
    (*FIXME currently assuming that we're only ever given a single binding each time this is called*)
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69366
diff changeset
   414
    val _ = \<^assert> (length bindings' = 1)
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   415
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   416
  in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   417
    fold safe_instantiate_bound bindings' ([], HOLogic.dest_Trueprop orig_parent_fmla)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   418
    |> snd (*discard var typing context*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   419
    |> close_formula
80667
wenzelm
parents: 80636
diff changeset
   420
    |> singleton (Type_Infer_Context.infer_types (Context.proof_of (Context.Theory thy)))
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   421
    |> HOLogic.mk_Trueprop
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   422
    |> rpair bindings'
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   423
  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   424
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   425
exception RECONSTRUCT of string
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   426
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   427
(*Some of these may be redundant wrt the original aims of this
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   428
  datatype, but it's useful to have a datatype to classify formulas
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   429
  for use by other functions as well.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   430
datatype formula_kind =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   431
    Conjunctive of bool option
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   432
  | Disjunctive of bool option
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   433
  | Biimplicational of bool option
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   434
  | Negative of bool option
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   435
  | Existential of bool option * typ
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   436
  | Universal of bool option * typ
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   437
  | Equational of bool option * typ
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   438
  | Atomic of bool option
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   439
  | Implicational of bool option
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   440
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   441
exception UNPOLARISED of term
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   442
(*Remove "= $true" or "= $false$ from the edge
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   443
  of a formula. Use "try" in case formula is not
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   444
  polarised.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   445
fun remove_polarity strict formula =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   446
  case try HOLogic.dest_eq formula of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   447
      NONE => if strict then raise (UNPOLARISED formula)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   448
              else (formula, true)
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69366
diff changeset
   449
    | SOME (x, p as \<^term>\<open>True\<close>) => (x, true)
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69366
diff changeset
   450
    | SOME (x, p as \<^term>\<open>False\<close>) => (x, false)
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   451
    | SOME (x, _) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   452
        if strict then raise (UNPOLARISED formula)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   453
        else (formula, true)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   454
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   455
(*flattens a formula wrt associative operators*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   456
fun flatten formula_kind formula =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   457
  let
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69366
diff changeset
   458
    fun is_conj (Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _) = true
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   459
      | is_conj _ = false
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69366
diff changeset
   460
    fun is_disj (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _) = true
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   461
      | is_disj _ = false
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69366
diff changeset
   462
    fun is_iff (Const (\<^const_name>\<open>HOL.eq\<close>, ty) $ _ $ _) =
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   463
          ty = ([HOLogic.boolT, HOLogic.boolT] ---> HOLogic.boolT)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   464
      | is_iff _ = false
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   465
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   466
    fun flatten' formula acc =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   467
      case formula of
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69366
diff changeset
   468
          Const (\<^const_name>\<open>HOL.conj\<close>, _) $ t1 $ t2 =>
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   469
            (case formula_kind of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   470
                 Conjunctive _ =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   471
                   let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   472
                     val left =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   473
                       if is_conj t1 then flatten' t1 acc else (t1 :: acc)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   474
                   in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   475
                       if is_conj t2 then flatten' t2 left else (t2 :: left)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   476
                   end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   477
               | _ => formula :: acc)
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69366
diff changeset
   478
        | Const (\<^const_name>\<open>HOL.disj\<close>, _) $ t1 $ t2 =>
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   479
            (case formula_kind of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   480
                 Disjunctive _ =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   481
                   let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   482
                     val left =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   483
                       if is_disj t1 then flatten' t1 acc else (t1 :: acc)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   484
                   in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   485
                       if is_disj t2 then flatten' t2 left else (t2 :: left)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   486
                   end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   487
               | _ => formula :: acc)
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69366
diff changeset
   488
        | Const (\<^const_name>\<open>HOL.eq\<close>, ty) $ t1 $ t2 =>
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   489
            if ty = ([HOLogic.boolT, HOLogic.boolT] ---> HOLogic.boolT) then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   490
              case formula_kind of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   491
                   Biimplicational _ =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   492
                     let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   493
                       val left =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   494
                         if is_iff t1 then flatten' t1 acc else (t1 :: acc)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   495
                     in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   496
                         if is_iff t2 then flatten' t2 left else (t2 :: left)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   497
                     end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   498
                 | _ => formula :: acc
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   499
            else formula :: acc
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   500
        | _ => [formula]
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   501
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   502
    val formula' = try_dest_Trueprop formula
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   503
  in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   504
    case formula_kind of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   505
        Conjunctive (SOME _) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   506
          remove_polarity false formula'
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   507
          |> fst
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   508
          |> (fn t => flatten' t [])
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   509
      | Disjunctive (SOME _) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   510
          remove_polarity false formula'
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   511
          |> fst
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   512
          |> (fn t => flatten' t [])
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   513
      | Biimplicational (SOME _) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   514
          remove_polarity false formula'
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   515
          |> fst
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   516
          |> (fn t => flatten' t [])
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   517
      | _ => flatten' formula' []
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   518
  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   519
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   520
fun node_info fms projector node_name =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   521
  case AList.lookup (op =) fms node_name of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   522
      NONE =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   523
        raise (RECONSTRUCT ("node " ^ node_name ^
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   524
                            " doesn't exist"))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   525
    | SOME info => projector info
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   526
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   527
(*Given a list of parent infos, extract the parent node names
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   528
  and the additional info (e.g., if there was an instantiation
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   529
  in addition to the inference).
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   530
  if "filtered"=true then exclude axiom and definition parents*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   531
fun dest_parent_infos filtered fms parent_infos : {name : string, details : TPTP_Proof.parent_detail list} list =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   532
  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   533
    (*Removes "definition" dependencies since these play no
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   534
      logical role -- i.e. they just give the expansions of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   535
      constants.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   536
      Removes "axiom" dependencies since these do not need to
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   537
      be derived; the reconstruction handler in "leo2_tac" can
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   538
      pick up the relevant axioms (using the info in the proof
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   539
      annotation) and use them in its reconstruction.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   540
    *)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   541
    val filter_deps =
58412
f65f11f4854c more standard Isabelle/ML operations;
wenzelm
parents: 58411
diff changeset
   542
      filter (fn {name, ...} =>
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   543
        let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   544
          val role = node_info fms #role name
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   545
        in role <> TPTP_Syntax.Role_Definition andalso
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   546
            role <> TPTP_Syntax.Role_Axiom
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   547
        end)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   548
    val parent_nodelist =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   549
      parent_infos
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   550
      |> map (fn n =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   551
                 case n of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   552
                     TPTP_Proof.Parent parent => {name = parent, details = []}
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   553
                   | TPTP_Proof.ParentWithDetails (parent, details) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   554
                     {name = parent, details = details})
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   555
  in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   556
    parent_nodelist
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   557
    |> filtered ? filter_deps
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   558
  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   559
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   560
fun parents_of_node fms n =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   561
  case node_info fms #source_inf_opt n of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   562
      NONE => []
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   563
    | SOME (TPTP_Proof.File _) => []
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   564
    | SOME (TPTP_Proof.Inference (_, _ : TPTP_Proof.useful_info_as list, parent_infos)) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   565
        dest_parent_infos false fms parent_infos
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   566
        |> map #name
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   567
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   568
exception FIND_ANCESTOR_USING_RULE of string
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   569
(*BFS for an ancestor inference involving a specific rule*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   570
fun find_ancestor_using_rule pannot inference_rule (fringe : string list) : string =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   571
  if null fringe then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   572
    raise (FIND_ANCESTOR_USING_RULE inference_rule)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   573
  else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   574
    case node_info (#meta pannot) #source_inf_opt (hd fringe) of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   575
        NONE => find_ancestor_using_rule pannot inference_rule (tl fringe)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   576
      | SOME (TPTP_Proof.File _) => find_ancestor_using_rule pannot inference_rule (tl fringe)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   577
      | SOME (TPTP_Proof.Inference (rule_name, _ : TPTP_Proof.useful_info_as list, parent_infos)) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   578
          if rule_name = inference_rule then hd fringe
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   579
          else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   580
            find_ancestor_using_rule pannot inference_rule
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   581
             (tl fringe @
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   582
              map #name (dest_parent_infos true (#meta pannot) parent_infos))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   583
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   584
(*Given a node in the proof, produce the term representing the inference
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   585
  that took place in that step, the inference rule used, and which
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   586
  other (non-axiom and non-definition) nodes participated in the
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   587
  inference*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   588
fun inference_at_node thy (prob_name : TPTP_Problem_Name.problem_name)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   589
     (fms : formula_meaning list) from : rule_info option =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   590
    let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   591
      exception INFERENCE_AT_NODE of string
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   592
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   593
      (*lookup formula associated with a node*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   594
      val fmla_of_node =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   595
          node_info fms #fmla
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   596
          #> try_dest_Trueprop
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   597
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   598
      fun build_inference_info rule_name parent_infos =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   599
        let
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69366
diff changeset
   600
          val _ = \<^assert> (not (null parent_infos))
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   601
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   602
          (*hypothesis formulas (with bindings already
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   603
            instantiated during the proof-transformation
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   604
            applied when loading the proof),
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   605
            including any axioms or definitions*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   606
          val parent_nodes =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   607
            dest_parent_infos false fms parent_infos
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   608
            |> map #name
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   609
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   610
          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)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   611
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   612
          val inference_term =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   613
            if null parent_fmlas then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   614
                fmla_of_node from
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   615
                |> HOLogic.mk_Trueprop
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   616
            else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   617
                Logic.mk_implies
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   618
                 (fold
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   619
                    (curry HOLogic.mk_conj)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   620
                    (tl parent_fmlas)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   621
                    (hd parent_fmlas)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   622
                  |> HOLogic.mk_Trueprop,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   623
                  fmla_of_node from |> HOLogic.mk_Trueprop)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   624
        in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   625
          SOME {inference_name = rule_name,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   626
                inference_fmla = inference_term,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   627
                parents = parent_nodes}
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   628
        end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   629
    in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   630
      (*examine node's "source" annotation: we're only interested
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   631
        if it's an inference*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   632
      case node_info fms #source_inf_opt from of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   633
                NONE => NONE
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   634
              | SOME (TPTP_Proof.File _) => NONE
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   635
              | SOME (TPTP_Proof.Inference (rule_name, _ : TPTP_Proof.useful_info_as list, parent_infos)) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   636
                  if List.null parent_infos then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   637
                    raise (INFERENCE_AT_NODE
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   638
                            ("empty parent list for node " ^
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   639
                             from ^ ": check proof format"))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   640
                  else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   641
                    build_inference_info rule_name parent_infos
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   642
    end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   643
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   644
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   645
(** Proof skeleton **)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   646
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   647
(* Emulating skeleton steps *)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   648
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   649
(*
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   650
Builds a rule (thm) of the following form:
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   651
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   652
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   653
                  prem1                   premn
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   654
                   ...         ...         ...
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   655
   major_prem     conc1                   concn
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   656
  -----------------------------------------------
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   657
                    conclusion
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   658
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   659
where major_prem is a disjunction of prem1,...,premn.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   660
*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   661
fun make_elimination_rule_t ctxt major_prem prems_and_concs conclusion =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   662
  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   663
    val thy = Proof_Context.theory_of ctxt
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   664
    val minor_prems =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   665
      map (fn (v, conc) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   666
        Logic.mk_implies (v, HOLogic.mk_Trueprop conc))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   667
        prems_and_concs
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   668
  in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   669
    (Logic.list_implies
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   670
     (major_prem :: minor_prems,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   671
     conclusion))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   672
  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   673
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   674
(*In summary, we emulate an n-way splitting rule via an n-way
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   675
  disjunction elimination.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   676
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   677
  Given a split formula and conclusion, we prove a rule which
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   678
  simulates the split. The conclusion is assumed to be a conjunction
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   679
  of conclusions for each branch of the split. The
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   680
  "minor_prem_assumptions" are the assumptions discharged in each
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   681
  branch; they're passed to the function to make sure that the
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   682
  generated rule is compatible with the skeleton (since the skeleton
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   683
  fixes the "order" of the reconstruction, based on the proof's
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   684
  structure).
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   685
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   686
  Concretely, if P is "(_ & _) = $false" or "(_ | _) = $true" then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   687
  splitting behaves as follows:
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   688
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   689
                     P
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   690
      -------------------------------
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   691
       _ = $false         _ = $false
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   692
          ...       ...       ...
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   693
           R1                  Rn
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   694
      -------------------------------
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   695
               R1 & ... & Rn
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   696
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   697
  Splitting (binary) iffs works as follows:
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   698
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   699
                  (A <=> B) = $false
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   700
      ------------------------------------------
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   701
       (A => B) = $false      (B => A) = $false
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   702
             ...                     ...
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   703
              R1                      R2
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   704
      ------------------------------------------
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   705
                        R1 & R2
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   706
*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   707
fun simulate_split ctxt split_fmla minor_prem_assumptions conclusion =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   708
  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   709
    val prems_and_concs =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   710
      ListPair.zip (minor_prem_assumptions, flatten (Conjunctive NONE) conclusion)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   711
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   712
    val rule_t = make_elimination_rule_t ctxt split_fmla prems_and_concs conclusion
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   713
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   714
    (*these are replaced by fresh variables in the abstract term*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   715
    val abstraction_subterms =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   716
      (map (try_dest_Trueprop #> remove_polarity true #> fst)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   717
              minor_prem_assumptions)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   718
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   719
    (*generate an abstract rule as a term...*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   720
    val abs_rule_t =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   721
      abstract
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   722
        abstraction_subterms
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   723
        rule_t
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   724
      |> snd (*ignore mapping info. this is a bit wasteful*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   725
             (*FIXME optimisation: instead on relying on diff
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   726
                to regenerate this info, could use it directly*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   727
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   728
    (*...and validate the abstract rule*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   729
    val abs_rule_thm =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   730
      Goal.prove ctxt [] [] abs_rule_t
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   731
       (fn pdata => HEADGOAL (blast_tac (#context pdata)))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   732
      |> Drule.export_without_context
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   733
  in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   734
    (*Instantiate the abstract rule based on the contents of the
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   735
      required instance*)
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 58893
diff changeset
   736
    diff_and_instantiate ctxt abs_rule_thm (Thm.prop_of abs_rule_thm) rule_t
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   737
  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   738
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   739
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   740
(* Building the skeleton *)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   741
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   742
type step_id = string
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   743
datatype rolling_stock =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   744
    Step of step_id
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   745
  | Assumed
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   746
  | Unconjoin
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   747
  | Split of step_id (*where split occurs*) *
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   748
             step_id (*where split ends*) *
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   749
             step_id list (*children of the split*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   750
  | Synth_step of step_id (*A step which doesn't necessarily appear in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   751
    the original proof, or which has been modified slightly for better
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   752
    handling by Isabelle*) (*FIXME "inodes" should be made into Synth_steps*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   753
  | Annotated_step of step_id * string (*Same interpretation as
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   754
    "Step", except that additional information is attached. This is
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   755
    currently used for debugging: Steps are mapped to Annotated_steps
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   756
    and their rule names are included as strings*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   757
  | Definition of step_id (*Mirrors TPTP role*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   758
  | Axiom of step_id (*Mirrors TPTP role*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   759
(*  | Derived of step_id -- to be used by memoization*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   760
  | Caboose
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   761
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   762
fun stock_to_string (Step n) = n
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   763
  | stock_to_string (Annotated_step (n, anno)) = n ^ "(" ^ anno ^ ")"
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   764
  | stock_to_string _ = error "Stock is not a step" (*FIXME more meaningful message*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   765
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   766
fun filter_by_role tptp_role =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   767
  filter
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   768
   (fn (_, info) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   769
       #role info = tptp_role)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   770
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   771
fun filter_by_name node_name =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   772
  filter
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   773
   (fn (n, _) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   774
       n = node_name)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   775
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   776
exception NO_MARKER_NODE
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   777
(*We fall back on node "1" in case the proof is not that of a theorem*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   778
fun proof_beginning_node fms =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   779
  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   780
    val result =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   781
      cascaded_filter_single true
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   782
       [filter_by_role TPTP_Syntax.Role_Conjecture,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   783
        filter_by_name "1"] (*FIXME const*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   784
       fms
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   785
  in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   786
    case result of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   787
        SOME x => fst x (*get the node name*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   788
      | NONE => raise NO_MARKER_NODE
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   789
  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   790
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   791
(*Get the name of the node where the proof ends*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   792
fun proof_end_node fms =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   793
  (*FIXME this isn't very nice: we assume that the last line in the
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   794
    proof file is the closing line of the proof. It would be nicer if
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   795
    such a line is specially marked (with a role), since there is no
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   796
    obvious ordering on names, since they can be strings.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   797
    Another way would be to run an analysis on the graph to find
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   798
    this node, since it has properties which should make it unique
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   799
    in a graph*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   800
  fms
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   801
  |> hd (*since proof has been reversed prior*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   802
  |> fst (*get node name*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   803
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   804
(*Generate list of (possibly reconstructed) inferences which can be
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   805
  composed together to reconstruct the whole proof.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   806
fun make_skeleton ctxt (pannot : proof_annotation) : rolling_stock list =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   807
  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   808
    val thy = Proof_Context.theory_of ctxt
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   809
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   810
    fun stock_is_ax_or_def (Axiom _) = true
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   811
      | stock_is_ax_or_def (Definition _) = true
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   812
      | stock_is_ax_or_def _ = false
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   813
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   814
    fun stock_of n =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   815
      case node_info (#meta pannot) #role n of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   816
          TPTP_Syntax.Role_Definition => (true, Definition n)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   817
        | TPTP_Syntax.Role_Axiom => (true, Axiom n)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   818
        | _ => (false, Step n)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   819
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   820
    fun n_is_split_conjecture (inference_info : rule_info option) =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   821
      case inference_info of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   822
          NONE => false
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   823
        | SOME inference_info => #inference_name inference_info = "split_conjecture"
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   824
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   825
    (*Different kinds of inference sequences:
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   826
        - Linear: (just add a step to the skeleton)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   827
           ---...---
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   828
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   829
        - Fan-in: (treat each in-path as conjoined with the others. Linearise all the paths, and concatenate them.)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   830
                  /---...
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   831
           ------<
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   832
                  \---...
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   833
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   834
        - Real split: Instead of treating as a conjunction, as in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   835
           normal fan-ins, we need to treat specially by looking
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   836
           at the location where the split occurs, and turn the
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   837
           split inference into a validity-preserving subproof.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   838
           As with fan-ins, we handle each fan-in path, and
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   839
           concatenate.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   840
                  /---...---\
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   841
           ------<           >------
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   842
                  \---...---/
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   843
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   844
        - Fake split: (treat like linear, since there isn't a split-node)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   845
           ------<---...----------
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   846
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   847
      Different kinds of sequences endings:
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   848
        - "Stop before": Non-decreasing list of nodes where should terminate.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   849
                         This starts off with the end node, and the split_nodes
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   850
                         will be added dynamically as the skeleton is built.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   851
        - Axiom/Definition
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   852
     *)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   853
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   854
    (*The following functions build the skeleton for the reconstruction starting
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   855
      from the node labelled "n" and stopping just before an element in stop_just_befores*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   856
    (*FIXME could throw exception if none of stop_just_befores is ever encountered*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   857
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   858
    (*This approach below is naive because it linearises the proof DAG, and this would
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   859
      duplicate some effort if the DAG isn't already linear.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   860
    exception SKELETON
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   861
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   862
    fun check_parents stop_just_befores n =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   863
      let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   864
        val parents = parents_of_node (#meta pannot) n
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   865
      in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   866
        if length parents = 1 then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   867
          AList.lookup (op =) stop_just_befores (the_single parents)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   868
        else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   869
          NONE
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   870
      end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   871
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   872
    fun naive_skeleton' stop_just_befores n =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   873
      case check_parents stop_just_befores n of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   874
          SOME skel => skel
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   875
        | NONE =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   876
            let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   877
              val inference_info = inference_at_node thy (#problem_name pannot) (#meta pannot) n
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   878
            in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   879
                if is_none inference_info then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   880
                  (*this is the case for the conjecture, definitions and axioms*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   881
                    if node_info (#meta pannot) #role n = TPTP_Syntax.Role_Definition then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   882
                      [(Definition n), Assumed]
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   883
                    else if node_info (#meta pannot) #role n = TPTP_Syntax.Role_Axiom then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   884
                      [Axiom n]
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   885
                    else raise SKELETON
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   886
                else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   887
                  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   888
                    val inference_info = the inference_info
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   889
                    val parents = #parents inference_info
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   890
                  in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   891
                    (*FIXME memoize antecedent_steps?*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   892
                    if #inference_name inference_info = "solved_all_splits" andalso length parents > 1 then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   893
                      (*splitting involves fanning out then in; this is to be
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   894
                        treated different than other fan-out-ins.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   895
                      let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   896
                        (*find where the proofs fanned-out: pick some antecedent,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   897
                          then find ancestor to use a "split_conjecture" inference.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   898
                        (*NOTE we assume that splits can't be nested*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   899
                        val split_node =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   900
                          find_ancestor_using_rule pannot "split_conjecture" [hd parents]
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   901
                          |> parents_of_node (#meta pannot)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   902
                          |> the_single
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   903
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   904
                        (*compute the skeletons starting at parents to either the split_node
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   905
                          if the antecedent is descended from the split_node, or the
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   906
                          stop_just_before otherwise*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   907
                        val skeletons_up =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   908
                          map (naive_skeleton' ((split_node, [Assumed]) :: stop_just_befores)) parents
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   909
                      in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   910
                        (*point to the split node, so that custom rule can be built later on*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   911
                        Step n :: (Split (split_node, n, parents)) :: (*this will create the elimination rule*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   912
                         naive_skeleton' stop_just_befores split_node @ (*this will discharge the major premise*)
58411
wenzelm
parents: 56220
diff changeset
   913
                         flat skeletons_up @ [Assumed] (*this will discharge the minor premises*)
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   914
                      end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   915
                    else if length parents > 1 then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   916
                      (*Handle fan-in nodes which aren't split-sinks by
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   917
                        enclosing each branch but one in conjI-assumption invocations*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   918
                        let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   919
                          val skeletons_up =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   920
                            map (naive_skeleton' stop_just_befores) parents
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   921
                        in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   922
                          Step n :: concat_between skeletons_up (SOME Unconjoin, NONE) @ [Assumed]
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   923
                        end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   924
                    else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   925
                      Step n :: naive_skeleton' stop_just_befores (the_single parents)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   926
                  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   927
            end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   928
  in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   929
    if List.null (#meta pannot) then [] (*in case "proof" file is empty*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   930
    else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   931
      naive_skeleton'
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   932
       [(proof_beginning_node (#meta pannot), [Assumed])]
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   933
       (proof_end_node (#meta pannot))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   934
      (*make last step the Caboose*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   935
      |> rev |> tl |> cons Caboose |> rev (*FIXME hacky*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   936
  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   937
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   938
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   939
(* Using the skeleton *)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   940
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   941
exception SKELETON
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   942
local
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   943
    (*Change the negated assumption (which is output by the contradiction rule) into
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   944
      a form familiar to Leo2*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   945
    val neg_eq_false =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   946
      @{lemma "!! P. (~ P) ==> (P = False)" by auto}
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   947
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   948
    (*FIXME this is just a dummy thm to annotate the assumption tac "atac"*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   949
    val solved_all_splits =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   950
      @{lemma "False = True ==> False" by auto}
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   951
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   952
    fun skel_to_naive_tactic ctxt prover_tac prob_name skel memo = fn st =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   953
      let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   954
        val thy = Proof_Context.theory_of ctxt
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   955
        val pannot = get_pannot_of_prob thy prob_name
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   956
        fun tac_and_memo node memo =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   957
          case AList.lookup (op =) memo node of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   958
              NONE =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   959
                let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   960
                  val tac =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   961
                    (*FIXME formula_sizelimit not being
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   962
                            checked here*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   963
                    prover_tac ctxt prob_name node
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   964
                in (tac, (node, tac) :: memo) end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   965
            | SOME tac => (tac, memo)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   966
        fun rest skel' memo =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   967
          skel_to_naive_tactic ctxt prover_tac prob_name skel' memo
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   968
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   969
        val tactic =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   970
          if null skel then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   971
            raise SKELETON (*FIXME or classify it as a Caboose: TRY (HEADGOAL atac) *)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   972
          else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   973
            case hd skel of
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 60649
diff changeset
   974
                Assumed => TRY (HEADGOAL (assume_tac ctxt)) THEN rest (tl skel) memo
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 60649
diff changeset
   975
              | Caboose => TRY (HEADGOAL (assume_tac ctxt))
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 60649
diff changeset
   976
              | Unconjoin => resolve_tac ctxt @{thms conjI} 1 THEN rest (tl skel) memo
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   977
              | Split (split_node, solved_node, antes) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   978
                  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   979
                    val split_fmla = node_info (#meta pannot) #fmla split_node
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   980
                    val conclusion =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   981
                      (inference_at_node thy prob_name (#meta pannot) solved_node
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   982
                       |> the
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   983
                       |> #inference_fmla)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   984
                      |> Logic.dest_implies (*FIXME there might be !!-variables?*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   985
                      |> #1
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   986
                    val minor_prems_assumps =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   987
                      map (fn ante => find_ancestor_using_rule pannot "split_conjecture" [ante]) antes
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   988
                      |> map (node_info (#meta pannot) #fmla)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   989
                    val split_thm =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   990
                      simulate_split ctxt split_fmla minor_prems_assumps conclusion
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   991
                  in
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 60649
diff changeset
   992
                    resolve_tac ctxt [split_thm] 1 THEN rest (tl skel) memo
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   993
                  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   994
              | Step s =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   995
                  let
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 60649
diff changeset
   996
                    val (th, memo') = tac_and_memo s memo
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   997
                  in
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 60649
diff changeset
   998
                    resolve_tac ctxt [th] 1 THEN rest (tl skel) memo'
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
   999
                  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1000
              | Definition n =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1001
                  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1002
                    val def_thm =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1003
                      case AList.lookup (op =) (#defs pannot) n of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1004
                          NONE => error ("Did not find definition: " ^ n)
59858
890b68e1e8b6 support for strictly private name space entries;
wenzelm
parents: 59582
diff changeset
  1005
                        | SOME binding => Global_Theory.get_thm thy (Binding.name_of binding)
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1006
                  in
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 60649
diff changeset
  1007
                    resolve_tac ctxt [def_thm] 1 THEN rest (tl skel) memo
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1008
                  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1009
              | Axiom n =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1010
                  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1011
                    val ax_thm =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1012
                      case AList.lookup (op =) (#axs pannot) n of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1013
                          NONE => error ("Did not find axiom: " ^ n)
59858
890b68e1e8b6 support for strictly private name space entries;
wenzelm
parents: 59582
diff changeset
  1014
                        | SOME binding => Global_Theory.get_thm thy (Binding.name_of binding)
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1015
                  in
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 60649
diff changeset
  1016
                    resolve_tac ctxt [ax_thm] 1 THEN rest (tl skel) memo
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1017
                  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1018
              | _ => raise SKELETON
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1019
      in tactic st end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1020
(*FIXME fuse these*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1021
    (*As above, but creates debug-friendly tactic.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1022
      This is also used for "partial proof reconstruction"*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1023
    fun skel_to_naive_tactic_dbg prover_tac ctxt prob_name skel (memo : (string * (thm * tactic) option) list) =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1024
      let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1025
        val thy = Proof_Context.theory_of ctxt
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1026
        val pannot = get_pannot_of_prob thy prob_name
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1027
60649
e007aa6a8aa2 more explicit use of context and elimination of Thm.theory_of_thm, although unclear (and untested?) situations remain;
wenzelm
parents: 59936
diff changeset
  1028
(* FIXME !???!
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1029
        fun rtac_wrap thm_f i = fn st =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1030
          let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1031
            val thy = Thm.theory_of_thm st
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1032
          in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1033
            rtac (thm_f thy) i st
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1034
          end
60649
e007aa6a8aa2 more explicit use of context and elimination of Thm.theory_of_thm, although unclear (and untested?) situations remain;
wenzelm
parents: 59936
diff changeset
  1035
*)
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1036
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1037
        (*Some nodes don't have an inference name, such as the conjecture,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1038
          definitions and axioms. Such nodes shouldn't appear in the
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1039
          skeleton.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1040
        fun inference_name_of_node node =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1041
           case AList.lookup (op =) (#meta pannot) node of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1042
               NONE => (warning "Inference step lacks an inference name"; "(Shouldn't be here)")
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1043
             | SOME info =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1044
                 case #source_inf_opt info of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1045
                     SOME (TPTP_Proof.Inference (infname, _, _)) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1046
                       infname
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1047
                   | _ => (warning "Inference step lacks an inference name"; "(Shouldn't be here)")
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1048
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1049
        fun inference_fmla node =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1050
          case inference_at_node thy prob_name (#meta pannot) node of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1051
              NONE => NONE
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1052
            | SOME {inference_fmla, ...} => SOME inference_fmla
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1053
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1054
        fun rest memo' ctxt' = skel_to_naive_tactic_dbg prover_tac ctxt' prob_name (tl skel) memo'
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1055
        (*reconstruct the inference. also set timeout in case
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1056
          tactic takes too long*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1057
        val try_make_step =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1058
          (*FIXME const timeout*)
62519
a564458f94db tuned signature -- clarified modules;
wenzelm
parents: 62243
diff changeset
  1059
          (* Timeout.apply (Time.fromSeconds 5) *)
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1060
          (fn ctxt' =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1061
             let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1062
               fun thm ctxt'' = prover_tac ctxt'' prob_name (hd skel |> stock_to_string)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1063
               val reconstructed_inference = thm ctxt'
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 60649
diff changeset
  1064
               fun rec_inf_tac st = HEADGOAL (resolve_tac ctxt' [thm ctxt']) st
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1065
             in (reconstructed_inference,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1066
                 rec_inf_tac)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1067
             end)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1068
        fun ignore_interpretation_exn f x = SOME (f x)
62243
dd22d2423047 clarified exception handling;
wenzelm
parents: 60754
diff changeset
  1069
          handle INTERPRET_INFERENCE => NONE
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1070
      in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1071
        if List.null skel then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1072
          raise SKELETON
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1073
        (*FIXME or classify it as follows:
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1074
          [(Caboose,
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 58893
diff changeset
  1075
            Thm.prop_of @{thm asm_rl}
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1076
            |> SOME,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1077
            SOME (@{thm asm_rl}, TRY (HEADGOAL atac)))]
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1078
         *)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1079
        else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1080
          case hd skel of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1081
              Assumed =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1082
                (hd skel,
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 58893
diff changeset
  1083
                 Thm.prop_of @{thm asm_rl}
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1084
                 |> SOME,
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 60649
diff changeset
  1085
                 SOME (@{thm asm_rl}, TRY (HEADGOAL (assume_tac ctxt)))) :: rest memo ctxt
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1086
            | Caboose =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1087
                [(Caboose,
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 58893
diff changeset
  1088
                  Thm.prop_of @{thm asm_rl}
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1089
                  |> SOME,
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 60649
diff changeset
  1090
                  SOME (@{thm asm_rl}, TRY (HEADGOAL (assume_tac ctxt))))]
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1091
            | Unconjoin =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1092
                (hd skel,
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 58893
diff changeset
  1093
                 Thm.prop_of @{thm conjI}
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1094
                 |> SOME,
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 60649
diff changeset
  1095
                 SOME (@{thm conjI}, resolve_tac ctxt @{thms conjI} 1)) :: rest memo ctxt
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1096
            | Split (split_node, solved_node, antes) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1097
                let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1098
                  val split_fmla = node_info (#meta pannot) #fmla split_node
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1099
                  val conclusion =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1100
                        (inference_at_node thy prob_name (#meta pannot) solved_node
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1101
                         |> the
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1102
                         |> #inference_fmla)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1103
                        |> Logic.dest_implies (*FIXME there might be !!-variables?*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1104
                        |> #1
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1105
                  val minor_prems_assumps =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1106
                      map (fn ante => find_ancestor_using_rule pannot "split_conjecture" [ante]) antes
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1107
                      |> map (node_info (#meta pannot) #fmla)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1108
                  val split_thm =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1109
                      simulate_split ctxt split_fmla minor_prems_assumps conclusion
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1110
                in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1111
                  (hd skel,
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 58893
diff changeset
  1112
                   Thm.prop_of split_thm
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1113
                   |> SOME,
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 60649
diff changeset
  1114
                   SOME (split_thm, resolve_tac ctxt [split_thm] 1)) :: rest memo ctxt
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1115
                end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1116
            | Step node =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1117
                let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1118
                  val inference_name = inference_name_of_node node
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1119
                  val inference_fmla = inference_fmla node
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1120
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1121
                  (*FIXME debugging code
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1122
                  val _ =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1123
                    if Config.get ctxt tptp_trace_reconstruction then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1124
                       (tracing ("handling node " ^ node);
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1125
                        tracing ("inference " ^ inference_name);
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1126
                        if is_some inference_fmla then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1127
                          tracing ("formula size " ^ Int.toString (Term.size_of_term (the inference_fmla)))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1128
                        else ()(*;
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1129
                        tracing ("formula " ^ @{make_string inference_fmla}) *))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1130
                    else ()*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1131
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1132
                  val (inference_instance_thm, memo', ctxt') =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1133
                    case AList.lookup (op =) memo node of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1134
                        NONE =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1135
                          let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1136
                            val (thm, ctxt') =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1137
                              (*Instead of NONE could have another value indicating that the formula was too big*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1138
                                if is_some inference_fmla andalso
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1139
                                   (*FIXME could have different inference rules have different sizelimits*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1140
                                   exceeds_tptp_max_term_size ctxt (Term.size_of_term (the inference_fmla)) then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1141
                                    (
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1142
                                     warning ("Gave up on node " ^ node ^ " because of fmla size " ^
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1143
                                              Int.toString (Term.size_of_term (the inference_fmla)));
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1144
                                     (NONE, ctxt)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1145
                                    )
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1146
                                else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1147
                                  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1148
                                    val maybe_thm = ignore_interpretation_exn try_make_step ctxt
60649
e007aa6a8aa2 more explicit use of context and elimination of Thm.theory_of_thm, although unclear (and untested?) situations remain;
wenzelm
parents: 59936
diff changeset
  1149
(* FIXME !???!
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1150
                                    val ctxt' =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1151
                                      if is_some maybe_thm then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1152
                                        the maybe_thm
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1153
                                        |> #1
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1154
                                        |> Thm.theory_of_thm |> Proof_Context.init_global
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1155
                                      else ctxt
60649
e007aa6a8aa2 more explicit use of context and elimination of Thm.theory_of_thm, although unclear (and untested?) situations remain;
wenzelm
parents: 59936
diff changeset
  1156
*)
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1157
                                  in
60649
e007aa6a8aa2 more explicit use of context and elimination of Thm.theory_of_thm, although unclear (and untested?) situations remain;
wenzelm
parents: 59936
diff changeset
  1158
                                    (maybe_thm, ctxt)
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1159
                                  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1160
                          in (thm, (node, thm) :: memo, ctxt') end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1161
                      | SOME maybe_thm => (maybe_thm, memo, ctxt)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1162
                in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1163
                  (Annotated_step (node, inference_name),
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1164
                   inference_fmla,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1165
                   inference_instance_thm) :: rest memo' ctxt'
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1166
                end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1167
            | Definition n =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1168
                let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1169
                  fun def_thm thy =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1170
                    case AList.lookup (op =) (#defs pannot) n of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1171
                        NONE => error ("Did not find definition: " ^ n)
59858
890b68e1e8b6 support for strictly private name space entries;
wenzelm
parents: 59582
diff changeset
  1172
                      | SOME binding => Global_Theory.get_thm thy (Binding.name_of binding)
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1173
                in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1174
                  (hd skel,
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 58893
diff changeset
  1175
                   Thm.prop_of (def_thm thy)
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1176
                   |> SOME,
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 60649
diff changeset
  1177
                   SOME (def_thm thy, HEADGOAL (resolve_tac ctxt [def_thm thy]))) :: rest memo ctxt
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1178
                end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1179
            | Axiom n =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1180
                let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1181
                  val ax_thm =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1182
                    case AList.lookup (op =) (#axs pannot) n of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1183
                        NONE => error ("Did not find axiom: " ^ n)
59858
890b68e1e8b6 support for strictly private name space entries;
wenzelm
parents: 59582
diff changeset
  1184
                      | SOME binding => Global_Theory.get_thm thy (Binding.name_of binding)
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1185
                in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1186
                  (hd skel,
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 58893
diff changeset
  1187
                   Thm.prop_of ax_thm
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1188
                   |> SOME,
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 60649
diff changeset
  1189
                   SOME (ax_thm, resolve_tac ctxt [ax_thm] 1)) :: rest memo ctxt
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1190
                end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1191
      end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1192
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1193
    (*The next function handles cases where Leo2 doesn't include the solved_all_splits
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1194
      step at the end (e.g. because there wouldn't be a split -- the proof
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1195
      would be linear*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1196
    fun sas_if_needed_tac ctxt prob_name =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1197
      let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1198
        val thy = Proof_Context.theory_of ctxt
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1199
        val pannot = get_pannot_of_prob thy prob_name
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1200
        val last_inference_info_opt =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1201
          find_first
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1202
           (fn (_, info) => #role info = TPTP_Syntax.Role_Plain)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1203
           (#meta pannot)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1204
        val last_inference_info =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1205
          case last_inference_info_opt of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1206
              NONE => NONE
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1207
            | SOME (_, info) => #source_inf_opt info
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1208
      in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1209
        if is_some last_inference_info andalso
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1210
         TPTP_Proof.is_inference_called "solved_all_splits"
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1211
          (the last_inference_info)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1212
        then (@{thm asm_rl}, all_tac)
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 60649
diff changeset
  1213
        else (solved_all_splits, TRY (resolve_tac ctxt [solved_all_splits] 1))
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1214
      end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1215
in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1216
  (*Build a tactic from a skeleton. This is naive because it uses the naive skeleton.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1217
    The inference interpretation ("prover_tac") is a parameter -- it would usually be
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1218
    different for different provers.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1219
  fun naive_reconstruct_tac ctxt prover_tac prob_name =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1220
    let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1221
      val thy = Proof_Context.theory_of ctxt
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1222
    in
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 60649
diff changeset
  1223
      resolve_tac ctxt @{thms ccontr} 1
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 60649
diff changeset
  1224
      THEN dresolve_tac ctxt [neg_eq_false] 1
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1225
      THEN (sas_if_needed_tac ctxt prob_name |> #2)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1226
      THEN skel_to_naive_tactic ctxt prover_tac prob_name
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1227
       (make_skeleton ctxt
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1228
        (get_pannot_of_prob thy prob_name)) []
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1229
    end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1230
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1231
  (*As above, but generates a list of tactics. This is useful for debugging, to apply
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1232
    the tactics one by one manually.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1233
  fun naive_reconstruct_tacs prover_tac prob_name ctxt =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1234
    let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1235
      val thy = Proof_Context.theory_of ctxt
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1236
    in
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 58893
diff changeset
  1237
      (Synth_step "ccontr", Thm.prop_of @{thm ccontr} |> SOME,
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 60649
diff changeset
  1238
       SOME (@{thm ccontr}, resolve_tac ctxt @{thms ccontr} 1)) ::
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 58893
diff changeset
  1239
      (Synth_step "neg_eq_false", Thm.prop_of neg_eq_false |> SOME,
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 60649
diff changeset
  1240
       SOME (neg_eq_false, dresolve_tac ctxt [neg_eq_false] 1)) ::
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 58893
diff changeset
  1241
      (Synth_step "sas_if_needed_tac", Thm.prop_of @{thm asm_rl} (*FIXME *) |> SOME,
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1242
       SOME (sas_if_needed_tac ctxt prob_name)) ::
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1243
      skel_to_naive_tactic_dbg prover_tac ctxt prob_name
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1244
       (make_skeleton ctxt
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1245
        (get_pannot_of_prob thy prob_name)) []
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1246
    end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1247
end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1248
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1249
(*Produces a theorem given a tactic and a parsed proof. This function is handy
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1250
to test reconstruction, since it automates the interpretation and proving of the
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1251
parsed proof's goal.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1252
fun reconstruct ctxt tactic prob_name =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1253
  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1254
    val thy = Proof_Context.theory_of ctxt
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1255
    val pannot = get_pannot_of_prob thy prob_name
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1256
    val goal =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1257
      #meta pannot
58412
f65f11f4854c more standard Isabelle/ML operations;
wenzelm
parents: 58411
diff changeset
  1258
      |> filter (fn (_, info) =>
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1259
          #role info = TPTP_Syntax.Role_Conjecture)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1260
  in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1261
    if null (#meta pannot) then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1262
      (*since the proof is empty, return a trivial result.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1263
      @{thm TrueI}
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1264
    else if null goal then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1265
      raise (RECONSTRUCT "Proof lacks conjecture")
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1266
    else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1267
      the_single goal
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1268
      |> snd |> #fmla
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1269
      |> (fn fmla => Goal.prove ctxt [] [] fmla (fn _ => tactic prob_name))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1270
  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1271
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1272
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1273
(** Skolemisation setup **)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1274
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1275
(*Ignore these constants if they appear in the conclusion but not the hypothesis*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1276
(*FIXME possibly incomplete*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1277
val ignore_consts =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1278
  [HOLogic.conj, HOLogic.disj, HOLogic.imp, HOLogic.Not]
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1279
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1280
(*Difference between the constants appearing between two terms, minus "ignore_consts"*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1281
fun new_consts_between t1 t2 =
58412
f65f11f4854c more standard Isabelle/ML operations;
wenzelm
parents: 58411
diff changeset
  1282
  filter
f65f11f4854c more standard Isabelle/ML operations;
wenzelm
parents: 58411
diff changeset
  1283
   (fn n => not (exists (fn n' => n' = n) ignore_consts))
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1284
   (list_diff (consts_in t2) (consts_in t1))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1285
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1286
(*Generate definition binding for an equation*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1287
fun mk_bind_eq prob_name params ((n, ty), t) =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1288
  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1289
    val bnd =
56220
4c43a2881b25 more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
wenzelm
parents: 55596
diff changeset
  1290
      Binding.name (Long_Name.base_name n ^ "_def")
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1291
      |> Binding.qualify false (TPTP_Problem_Name.mangle_problem_name prob_name)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1292
    val t' =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1293
      Term.list_comb (Const (n, ty), params)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1294
      |> rpair t
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1295
      |> HOLogic.mk_eq
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1296
      |> HOLogic.mk_Trueprop
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1297
      |> fold Logic.all params
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1298
  in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1299
    (bnd, t')
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1300
  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1301
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1302
(*Generate binding for an axiom. Similar to "mk_bind_eq"*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1303
fun mk_bind_ax prob_name node t =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1304
  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1305
    val bnd =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1306
      Binding.name node
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1307
      (*FIXME add suffix? e.g. ^ "_ax"*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1308
      |> Binding.qualify false (TPTP_Problem_Name.mangle_problem_name prob_name)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1309
  in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1310
    (bnd, t)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1311
  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1312
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1313
(*Extract the constant name, type, and its definition*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1314
fun get_defn_components
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69366
diff changeset
  1315
  (Const (\<^const_name>\<open>HOL.Trueprop\<close>, _) $
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69366
diff changeset
  1316
    (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1317
      Const (name, ty) $ t)) = ((name, ty), t)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1318
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1319
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1320
(*** Proof transformations ***)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1321
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1322
(*Transforms a proof_annotation value.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1323
  Argument "f" is the proof transformer*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1324
fun transf_pannot f (pannot : proof_annotation) : (theory * proof_annotation) =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1325
  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1326
    val (thy', fms') = f (#meta pannot)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1327
  in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1328
    (thy',
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1329
     {problem_name = #problem_name pannot,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1330
      skolem_defs = #skolem_defs pannot,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1331
      defs = #defs pannot,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1332
      axs = #axs pannot,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1333
      meta = fms'})
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1334
  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1335
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1336
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1337
(** Proof transformer to add virtual inference steps
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1338
    encoding "bind" annotations in Leo-II proofs **)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1339
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1340
(*
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1341
Involves finding an inference of this form:
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1342
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1343
       (!x1 ... xn. F)   ...   Cn
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1344
  ------------------------------------ (Rule name)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1345
          G[t1/x1, ..., tn/xn]
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1346
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1347
and turn it into this:
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1348
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1349
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1350
     (!x1 ... xn. F)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1351
  ---------------------- bind
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1352
   F[t1/x1, ..., tn/xn]           ...   Cn
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1353
  -------------------------------------------- (Rule name)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1354
                    G
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1355
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1356
where "bind" is an inference rule (distinct from any rule name used
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1357
by Leo2) to indicate such inferences.  This transformation is used
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1358
to factor out instantiations, thus allowing the reconstruction to
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1359
focus on (Rule name) rather than "(Rule name) + instantiations".
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1360
*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1361
fun interpolate_binds prob_name thy fms : theory * formula_meaning list =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1362
  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1363
    fun factor_out_bind target_node pinfo intermediate_thy =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1364
      case pinfo of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1365
         TPTP_Proof.ParentWithDetails (n, pdetails) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1366
           (*create new node which contains the "bind" inference,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1367
             to be added to graph*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1368
           let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1369
             val (new_node_name, thy') = get_next_name intermediate_thy
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1370
             val orig_fmla = node_info fms #fmla n
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1371
             val target_fmla = node_info fms #fmla target_node
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1372
             val new_node =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1373
              (new_node_name,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1374
               {role = TPTP_Syntax.Role_Plain,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1375
                fmla = apply_binding thy' prob_name orig_fmla target_fmla pdetails |> fst,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1376
                source_inf_opt =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1377
                  SOME (TPTP_Proof.Inference (bindK, [], [pinfo]))})
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1378
           in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1379
             ((TPTP_Proof.Parent new_node_name, SOME new_node), thy')
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1380
           end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1381
       | _ => ((pinfo, NONE), intermediate_thy)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1382
    fun process_nodes (step as (n, data)) (intermediate_thy, rest) =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1383
      case #source_inf_opt data of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1384
          SOME (TPTP_Proof.Inference (inf_name, sinfos, pinfos)) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1385
            let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1386
              val ((pinfos', parent_nodes), thy') =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1387
                fold_map (factor_out_bind n) pinfos intermediate_thy
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1388
                |> apfst ListPair.unzip
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1389
              val step' =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1390
                (n, {role = #role data, fmla = #fmla data,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1391
                 source_inf_opt = SOME (TPTP_Proof.Inference (inf_name, sinfos, pinfos'))})
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1392
            in (thy', fold_options parent_nodes @ step' :: rest) end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1393
        | _ => (intermediate_thy, step :: rest)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1394
  in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1395
    fold process_nodes fms (thy, [])
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1396
    (*new_nodes must come at the beginning, since we assume that the last line in a proof is the closing line*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1397
    |> apsnd rev
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1398
  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1399
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1400
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1401
(** Proof transformer to add virtual inference steps
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1402
    encoding any transformation done immediately prior
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1403
    to a splitting step **)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1404
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1405
(*
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1406
Involves finding an inference of this form:
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1407
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1408
                   F = $false
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1409
  ----------------------------------- split_conjecture
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1410
    (F1 = $false) ... (Fn = $false)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1411
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1412
where F doesn't have an "and" or "iff" at the top level,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1413
and turn it into this:
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1414
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1415
                   F = $false
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1416
  ----------------------------------- split_preprocessing
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1417
            (F1 % ... % Fn) = $false
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1418
  ----------------------------------- split_conjecture
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1419
    (F1 = $false) ... (Fn = $false)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1420
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1421
where "%" is either an "and" or an "iff" connective.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1422
This transformation is used to clarify the clause structure, to
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1423
make it immediately "obvious" how splitting is taking place
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1424
(by factoring out the other syntactic transformations -- e.g.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1425
related to quantifiers -- performed by Leo2). Having the clause
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1426
in this "clearer" form makes the inference amenable to handling
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1427
using the "abstraction" technique, which allows us to validate
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1428
large inferences.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1429
*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1430
exception PREPROCESS_SPLITS
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1431
fun preprocess_splits prob_name thy fms : theory * formula_meaning list =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1432
  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1433
    (*Simulate the transformation done by Leo2's preprocessing
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1434
      step during splitting.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1435
      NOTE: we assume that the clause is a singleton
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1436
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1437
      This transformation does the following:
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1438
       - miniscopes !-quantifiers (and recurs)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1439
       - removes redundant ?-quantifiers (and recurs)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1440
       - eliminates double negation (and recurs)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1441
       - breaks up conjunction (and recurs)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1442
       - expands iff (and doesn't recur)*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1443
    fun transform_fmla i fmla_t =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1444
      case fmla_t of
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69366
diff changeset
  1445
          Const (\<^const_name>\<open>HOL.All\<close>, ty) $ Abs (s, ty', t') =>
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1446
            let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1447
              val (i', fmla_ts) = transform_fmla i t'
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1448
            in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1449
              if i' > i then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1450
                (i' + 1,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1451
                 map (fn t =>
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69366
diff changeset
  1452
                  Const (\<^const_name>\<open>HOL.All\<close>, ty) $ Abs (s, ty', t))
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1453
                fmla_ts)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1454
              else (i, [fmla_t])
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1455
            end
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69366
diff changeset
  1456
        | Const (\<^const_name>\<open>HOL.Ex\<close>, ty) $ Abs (s, ty', t') =>
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1457
            if loose_bvar (t', 0) then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1458
              (i, [fmla_t])
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1459
            else transform_fmla (i + 1) t'
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69366
diff changeset
  1460
        | \<^term>\<open>HOL.Not\<close> $ (\<^term>\<open>HOL.Not\<close> $ t') =>
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1461
            transform_fmla (i + 1) t'
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69366
diff changeset
  1462
        | \<^term>\<open>HOL.conj\<close> $ t1 $ t2 =>
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1463
            let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1464
              val (i1, fmla_t1s) = transform_fmla (i + 1) t1
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1465
              val (i2, fmla_t2s) = transform_fmla (i + 1) t2
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1466
            in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1467
              (i1 + i2 - i, fmla_t1s @ fmla_t2s)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1468
            end
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69366
diff changeset
  1469
        | Const (\<^const_name>\<open>HOL.eq\<close>, ty) $ t1 $ t2 =>
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1470
            let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1471
              val (T1, (T2, res)) =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1472
                dest_funT ty
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1473
                |> apsnd dest_funT
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1474
            in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1475
              if T1 = HOLogic.boolT andalso T2 = HOLogic.boolT andalso
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1476
                 res = HOLogic.boolT then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1477
                (i + 1,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1478
                  [HOLogic.mk_imp (t1, t2),
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1479
                   HOLogic.mk_imp (t2, t1)])
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1480
              else (i, [fmla_t])
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1481
            end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1482
        | _ => (i, [fmla_t])
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1483
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1484
    fun preprocess_split thy split_node_name fmla_t =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1485
      (*create new node which contains the new inference,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1486
        to be added to graph*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1487
      let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1488
        val (node_name, thy') = get_next_name thy
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1489
        val (changes, fmla_conjs) =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1490
          transform_fmla 0 fmla_t
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1491
          |> apsnd rev (*otherwise we run into problems because
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1492
                         of commutativity of conjunction*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1493
        val target_fmla =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1494
          fold (curry HOLogic.mk_conj) (tl fmla_conjs) (hd fmla_conjs)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1495
        val new_node =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1496
         (node_name,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1497
          {role = TPTP_Syntax.Role_Plain,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1498
           fmla =
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69366
diff changeset
  1499
             HOLogic.mk_eq (target_fmla, \<^term>\<open>False\<close>) (*polarise*)
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1500
             |> HOLogic.mk_Trueprop,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1501
           source_inf_opt =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1502
             SOME (TPTP_Proof.Inference (split_preprocessingK, [], [TPTP_Proof.Parent split_node_name]))})
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1503
      in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1504
        if changes = 0 then NONE
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1505
        else SOME (TPTP_Proof.Parent node_name, new_node, thy')
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1506
      end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1507
  in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1508
    fold
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1509
     (fn step as (n, data) => fn (intermediate_thy, redirections, rest) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1510
       case #source_inf_opt data of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1511
            SOME (TPTP_Proof.Inference
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1512
                   (inf_name, sinfos, pinfos)) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1513
              if inf_name <> "split_conjecture" then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1514
                (intermediate_thy, redirections, step :: rest)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1515
              else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1516
                let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1517
                  (*
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1518
                   NOTE: here we assume that the node only has one
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1519
                         parent, and that there is no additional
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1520
                         parent info.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1521
                   *)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1522
                  val split_node_name =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1523
                    case pinfos of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1524
                        [TPTP_Proof.Parent n] => n
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1525
                      | _ => raise PREPROCESS_SPLITS
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1526
                (*check if we've already handled that already node*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1527
                in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1528
                  case AList.lookup (op =) redirections split_node_name of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1529
                      SOME preprocessed_split_node_name =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1530
                        let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1531
                          val step' =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1532
                            apply_to_parent_info (fn _ => [TPTP_Proof.Parent preprocessed_split_node_name]) step
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1533
                        in (intermediate_thy, redirections, step' :: rest) end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1534
                    | NONE =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1535
                        let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1536
                          (*we know the polarity to be $false, from knowing Leo2*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1537
                          val split_fmla =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1538
                            try_dest_Trueprop (node_info fms #fmla split_node_name)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1539
                            |> remove_polarity true
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1540
                            |> fst
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1541
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1542
                          val preprocess_result =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1543
                            preprocess_split intermediate_thy
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1544
                              split_node_name
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1545
                              split_fmla
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1546
                        in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1547
                          if is_none preprocess_result then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1548
                            (*no preprocessing done by Leo2, so no need to introduce
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1549
                              a virtual inference. cache this result by
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1550
                              redirecting the split_node to itself*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1551
                            (intermediate_thy,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1552
                             (split_node_name, split_node_name) :: redirections,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1553
                             step :: rest)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1554
                          else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1555
                            let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1556
                              val (new_parent_info, new_parent_node, thy') = the preprocess_result
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1557
                              val step' =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1558
                                (n, {role = #role data, fmla = #fmla data,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1559
                                 source_inf_opt = SOME (TPTP_Proof.Inference (inf_name, sinfos, [new_parent_info]))})
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1560
                            in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1561
                              (thy',
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1562
                               (split_node_name, fst new_parent_node) :: redirections,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1563
                               step' :: new_parent_node :: rest)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1564
                            end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1565
                        end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1566
                end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1567
          | _ => (intermediate_thy, redirections, step :: rest))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1568
     (rev fms) (*this allows us to put new inferences before other inferences which use them*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1569
     (thy, [], [])
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1570
    |> (fn (x, _, z) => (x, z)) (*discard redirection info*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1571
  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1572
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1573
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1574
(** Proof transformer to remove repeated quantification **)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1575
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1576
exception DROP_REPEATED_QUANTIFICATION
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1577
fun drop_repeated_quantification thy (fms : formula_meaning list) : theory * formula_meaning list =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1578
  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1579
    (*In case of repeated quantification, removes outer quantification.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1580
      Only need to look at top-level, since the repeated quantification
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1581
      generally occurs at clause level*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1582
    fun remove_repeated_quantification seen t =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1583
      case t of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1584
          (*NOTE we're assuming that variables having the same name, have the same type throughout*)
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69366
diff changeset
  1585
          Const (\<^const_name>\<open>HOL.All\<close>, ty) $ Abs (s, ty', t') =>
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1586
            let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1587
              val (seen_so_far, seen') =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1588
                case AList.lookup (op =) seen s of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1589
                    NONE => (0, (s, 0) :: seen)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1590
                  | SOME n => (n + 1, AList.update (op =) (s, n + 1) seen)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1591
              val (pre_final_t, final_seen) = remove_repeated_quantification seen' t'
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1592
              val final_t =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1593
                case AList.lookup (op =) final_seen s of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1594
                    NONE => raise DROP_REPEATED_QUANTIFICATION
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1595
                  | SOME n =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1596
                      if n > seen_so_far then pre_final_t
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69366
diff changeset
  1597
                      else Const (\<^const_name>\<open>HOL.All\<close>, ty) $ Abs (s, ty', pre_final_t)
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1598
            in (final_t, final_seen) end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1599
        | _ => (t, seen)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1600
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1601
    fun remove_repeated_quantification' (n, {role, fmla, source_inf_opt}) =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1602
      (n,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1603
       {role = role,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1604
        fmla =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1605
          try_dest_Trueprop fmla
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1606
          |> remove_repeated_quantification []
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1607
          |> fst
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1608
          |> HOLogic.mk_Trueprop,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1609
        source_inf_opt = source_inf_opt})
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1610
  in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1611
    (thy, map remove_repeated_quantification' fms)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1612
  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1613
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1614
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1615
(** Proof transformer to detect a redundant splitting and remove
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1616
    the redundant branch. **)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1617
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1618
fun node_is_inference fms rule_name node_name =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1619
  case node_info fms #source_inf_opt node_name of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1620
      NONE => false
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1621
    | SOME (TPTP_Proof.File _) => false
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1622
    | SOME (TPTP_Proof.Inference (rule_name', _, _)) => rule_name' = rule_name
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1623
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1624
(*In this analysis we're interested if there exists a split-free
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1625
  path between the end of the proof and the negated conjecture.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1626
  If so, then this path (or the shortest such path) could be
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1627
  retained, and the rest of the proof erased.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1628
datatype branch_info =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1629
    Split_free (*Path is not part of a split. This is only used when path reaches the negated conjecture.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1630
  | Split_present (*Path is one of a number of splits. Such paths are excluded.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1631
  | Coinconsistent of int (*Path leads to a clause which is inconsistent with nodes concluded by other paths.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1632
                            Therefore this path should be kept if the others are kept
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1633
                            (i.e., unless one of them results from a split)*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1634
  | No_info (*Analysis hasn't come across anything definite yet, though it still hasn't completed.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1635
(*A "paths" value consist of every way of reaching the destination,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1636
  including information come across it so far. Taking the head of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1637
  each way gives the fringe. All paths should share the same source
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1638
  and sink.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1639
type path = (branch_info * string list)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1640
exception PRUNE_REDUNDANT_SPLITS
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1641
fun prune_redundant_splits prob_name thy fms : theory * formula_meaning list =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1642
  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1643
    (*All paths start at the contradiction*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1644
    val initial_path = (No_info, [proof_end_node fms])
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1645
    (*All paths should end at the proof's beginning*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1646
    val end_node = proof_beginning_node fms
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1647
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1648
    fun compute_path (path as ((info,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1649
                       (n :: ns)) : path))(*i.e. node list can't be empty*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1650
        intermediate_thy =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1651
      case info of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1652
          Split_free => (([path], []), intermediate_thy)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1653
        | Coinconsistent branch_id =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1654
            (*If this branch has a split_conjecture parent then all "sibling" branches get erased.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1655
            (*This branch can't lead to yet another coinconsistent branch (in the case of Leo2).*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1656
            let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1657
              val parent_nodes = parents_of_node fms n
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1658
            in
58412
f65f11f4854c more standard Isabelle/ML operations;
wenzelm
parents: 58411
diff changeset
  1659
              if exists (node_is_inference fms "split_conjecture") parent_nodes then
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1660
                (([], [branch_id]), intermediate_thy) (*all related branches are to be deleted*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1661
              else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1662
                list_prod [] parent_nodes (n :: ns)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1663
                |> map (fn ns' => (Coinconsistent branch_id, ns'))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1664
                |> (fn x => ((x, []), intermediate_thy))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1665
            end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1666
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1667
        | No_info =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1668
            let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1669
              val parent_nodes = parents_of_node fms n
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1670
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1671
              (*if this node is a consistency checking node then parent nodes will be marked as coinconsistent*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1672
              val (thy', new_branch_info) =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1673
                if node_is_inference fms "fo_atp_e" n orelse
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1674
                   node_is_inference fms "res" n then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1675
                  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1676
                    val (i', intermediate_thy') = get_next_int intermediate_thy
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1677
                  in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1678
                    (intermediate_thy', SOME (Coinconsistent i'))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1679
                  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1680
                else (intermediate_thy, NONE)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1681
            in
58412
f65f11f4854c more standard Isabelle/ML operations;
wenzelm
parents: 58411
diff changeset
  1682
              if exists (node_is_inference fms "split_conjecture") parent_nodes then
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1683
                (([], []), thy')
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1684
              else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1685
                list_prod [] parent_nodes (n :: ns)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1686
                |> map (fn ns' =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1687
                          let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1688
                            val info =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1689
                              if is_some new_branch_info then the new_branch_info
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1690
                              else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1691
                                if hd ns' = end_node then Split_free else No_info
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1692
                          in (info, ns') end)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1693
                |> (fn x => ((x, []), thy'))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1694
            end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1695
        | _ => raise PRUNE_REDUNDANT_SPLITS
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1696
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1697
    fun compute_paths intermediate_thy (paths : path list) =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1698
      if filter (fn (_, ns) => ns <> [] andalso hd ns = end_node) paths = paths then
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1699
        (*fixpoint reached when all paths are at the head position*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1700
        (intermediate_thy, paths)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1701
      else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1702
        let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1703
          val filtered_paths = filter (fn (info, _) : path => info <> Split_present) paths (*not interested in paths containing a split*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1704
          val (paths', thy') =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1705
            fold_map compute_path filtered_paths intermediate_thy
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1706
        in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1707
          paths'
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1708
          |> ListPair.unzip (*we get a list of pairs of lists. we want a pair of lists*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1709
          |> (fn (paths, branch_ids) =>
58411
wenzelm
parents: 56220
diff changeset
  1710
               (flat paths,
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1711
                (*remove duplicate branch_ids*)
58411
wenzelm
parents: 56220
diff changeset
  1712
                fold (Library.insert (op =)) (flat branch_ids) []))
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1713
          (*filter paths having branch_ids appearing in the second list*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1714
          |> (fn (paths, branch_ids) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1715
              filter (fn (info, _) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1716
                        case info of
58412
f65f11f4854c more standard Isabelle/ML operations;
wenzelm
parents: 58411
diff changeset
  1717
                            Coinconsistent branch_id => exists (fn x => x = branch_id) branch_ids
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1718
                          | _ => true) paths)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1719
          |> compute_paths thy'
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1720
        end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1721
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1722
    val (thy', paths) =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1723
      compute_paths thy [initial_path]
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1724
      |> apsnd
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1725
          (filter (fn (branch_info, _) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1726
                  case branch_info of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1727
                      Split_free => true
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1728
                    | Coinconsistent _ => true
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1729
                    | _ => false))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1730
    (*Extract subset of fms which is used in a path.
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1731
      Also, remove references (in parent info annotations) to erased nodes.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1732
    fun path_to_fms ((_, nodes) : path) =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1733
      fold
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1734
       (fn n => fn fms' =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1735
          case AList.lookup (op =) fms' n of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1736
              SOME _ => fms'
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1737
            | NONE =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1738
               let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1739
                 val node_info = the (AList.lookup (op =) fms n)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1740
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1741
                 val source_info' =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1742
                   case #source_inf_opt node_info of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1743
                       NONE => error "Only the conjecture is an orphan"
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1744
                     | SOME (source_info as TPTP_Proof.File _) => source_info
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1745
                     | SOME (source_info as
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1746
                             TPTP_Proof.Inference (inference_name,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1747
                                                   useful_infos : TPTP_Proof.useful_info_as list,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1748
                                                   parent_infos)) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1749
                         let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1750
                           fun is_node_in_fms' parent_info =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1751
                             let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1752
                               val parent_nodename =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1753
                                 case parent_info of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1754
                                     TPTP_Proof.Parent n => n
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1755
                                   | TPTP_Proof.ParentWithDetails (n, _) => n
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1756
                             in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1757
                               case AList.lookup (op =) fms' parent_nodename of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1758
                                   NONE => false
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1759
                                 | SOME _ => true
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1760
                             end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1761
                         in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1762
                           TPTP_Proof.Inference (inference_name,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1763
                                                 useful_infos,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1764
                                                 filter is_node_in_fms' parent_infos)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1765
                         end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1766
               in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1767
                   (n,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1768
                    {role = #role node_info,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1769
                     fmla = #fmla node_info,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1770
                     source_inf_opt = SOME source_info'}) :: fms'
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1771
               end)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1772
       nodes
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1773
       []
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1774
  in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1775
    if null paths then (thy', fms) else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1776
      (thy',
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1777
       hd(*FIXME could pick path based on length, or some notion of "difficulty"*) paths
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1778
       |> path_to_fms)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1779
  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1780
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1781
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1782
(*** Main functions ***)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1783
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1784
(*interpret proof*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1785
fun import_thm cautious path_prefixes file_name
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1786
 (on_load : proof_annotation -> theory -> (proof_annotation * theory)) thy =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1787
  let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1788
    val prob_name =
69366
b6dacf6eabe3 clarified signature;
wenzelm
parents: 65999
diff changeset
  1789
      Path.file_name file_name
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1790
      |> TPTP_Problem_Name.parse_problem_name
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1791
    val thy1 = TPTP_Interpret.import_file cautious path_prefixes file_name [] [] thy
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1792
    val fms = get_fmlas_of_prob thy1 prob_name
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1793
  in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1794
    if List.null fms then
62552
53603d1aad5f proper Path.print for user messages;
wenzelm
parents: 62519
diff changeset
  1795
      (warning ("File " ^ Path.print file_name ^ " appears empty!");
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1796
       TPTP_Reconstruction_Data.map (cons ((prob_name, empty_pannot prob_name))) thy1)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1797
    else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1798
      let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1799
        val defn_equations =
58412
f65f11f4854c more standard Isabelle/ML operations;
wenzelm
parents: 58411
diff changeset
  1800
          filter (fn (_, role, _, _) => role = TPTP_Syntax.Role_Definition) fms
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1801
          |> map (fn (node, _, t, _) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1802
               (node,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1803
                get_defn_components t
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1804
                |> mk_bind_eq prob_name []))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1805
        val axioms =
58412
f65f11f4854c more standard Isabelle/ML operations;
wenzelm
parents: 58411
diff changeset
  1806
          filter (fn (_, role, _, _) => role = TPTP_Syntax.Role_Axiom) fms
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1807
          |> map (fn (node, _, t, _) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1808
               (node,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1809
                mk_bind_ax prob_name node t))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1810
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1811
        (*add definitions and axioms to the theory*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1812
        val thy2 =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1813
          fold
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1814
           (fn bnd => fn thy =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1815
              let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1816
                val ((name, thm), thy') = Thm.add_axiom_global bnd thy
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1817
              in Global_Theory.add_thm ((#1 bnd, thm), []) thy' |> #2 end)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1818
           (map snd defn_equations @ map snd axioms)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1819
          thy1
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1820
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1821
        (*apply global proof transformations*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1822
        val (thy3, pre_pannot) : theory * proof_annotation =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1823
          transf_pannot
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1824
           (prune_redundant_splits prob_name thy2
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1825
            #-> interpolate_binds prob_name
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1826
            #-> preprocess_splits prob_name
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1827
            #-> drop_repeated_quantification)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1828
           {problem_name = prob_name,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1829
            skolem_defs = [],
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1830
            defs = map (apsnd fst) defn_equations,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1831
            axs = map (apsnd fst) axioms,
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1832
            meta = map (fn (n, r, t, info) => (n, {role=r, fmla=t, source_inf_opt=info})) fms}
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1833
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1834
        (*store pannot*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1835
        val thy4 = TPTP_Reconstruction_Data.map (cons ((prob_name, pre_pannot))) thy3
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1836
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1837
        (*run hook, which might result in changed pannot and theory*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1838
        val (pannot, thy5) = on_load pre_pannot thy4
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1839
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1840
      (*store the most recent pannot*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1841
      in TPTP_Reconstruction_Data.map (cons ((prob_name, pannot))) thy5 end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1842
  end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1843
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1844
(*This has been disabled since it requires a hook to be specified to use "import_thm"
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1845
val _ =
59936
b8ffc3dc9e24 @{command_spec} is superseded by @{command_keyword};
wenzelm
parents: 59858
diff changeset
  1846
  Outer_Syntax.command @{command_keyword import_leo2_proof} "import TPTP proof"
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1847
    (Parse.path >> (fn name =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1848
      Toplevel.theory (fn thy =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1849
       let val path = Path.explode name
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1850
       in import_thm true [Path.dir path, Path.explode "$TPTP"] path (*FIXME hook needs to be given here*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1851
thy end)))
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1852
*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1853
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1854
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1855
(** Archive **)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1856
(*FIXME move elsewhere*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1857
(*This contains currently unused, but possibly useful, functions written
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1858
  during experimentation, in case they are useful later on*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1859
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1860
(*given a list of rules and a node, return
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1861
  SOME (rule name) if that node's rule name
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1862
  belongs to the list of rules*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1863
fun match_rules_of_current (pannot : proof_annotation) rules n =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1864
  case node_info (#meta pannot) #source_inf_opt n of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1865
      NONE => NONE
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1866
    | SOME (TPTP_Proof.File _) => NONE
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1867
    | SOME (TPTP_Proof.Inference (rule_name, _ : TPTP_Proof.useful_info_as list, _)) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1868
        if member (op =) rules rule_name then SOME rule_name else NONE
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1869
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1870
(*given a node and a list of rules, determine
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1871
  whether all the rules can be matched to
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1872
  parent nodes. If nonstrict then there may be
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1873
  more parents than given rules.*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1874
fun match_rules_of_immediate_previous (pannot : proof_annotation) strict rules n =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1875
  case node_info (#meta pannot) #source_inf_opt n of
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1876
      NONE => null rules
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1877
    | SOME (TPTP_Proof.File _) => null rules
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1878
    | SOME (TPTP_Proof.Inference (rule_name, _ : TPTP_Proof.useful_info_as list, parent_infos)) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1879
        let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1880
          val matched_rules : string option list =
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1881
            map (match_rules_of_current pannot rules)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1882
                (dest_parent_infos true (#meta pannot) parent_infos |> map #name)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1883
        in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1884
          if strict andalso member (op =) matched_rules NONE then false
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1885
          else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1886
            (*check that all the rules were matched*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1887
            fold
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1888
              (fn (rule : string) => fn (st, matches : string option list) =>
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1889
                 if not st then (st, matches)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1890
                 else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1891
                   let
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1892
                     val idx = find_index (fn match => SOME rule = match) matches
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1893
                   in
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1894
                     if idx < 0 then (false, matches)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1895
                     else
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1896
                       (st, nth_drop idx matches)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1897
                   end)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1898
             rules
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1899
             (true, matched_rules)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1900
            |> #1 (*discard the other info*)
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1901
        end
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
diff changeset
  1902
end