src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
author desharna
Thu, 12 Nov 2020 11:00:34 +0100
changeset 72585 18eb7ec2720f
parent 72584 4ea19e5dc67e
child 72798 e732c98b02e6
permissions -rw-r--r--
Tuned indentation
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55194
diff changeset
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar.ML
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
     3
    Author:     Steffen Juilf Smolka, TU Muenchen
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
     4
49914
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
     5
Isar proof reconstruction from ATP proofs.
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
     6
*)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
     7
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55194
diff changeset
     8
signature SLEDGEHAMMER_ISAR =
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
     9
sig
54771
85879aa61334 move some Z3 specifics out (and into private repository with the rest of the Z3-specific code)
blanchet
parents: 54770
diff changeset
    10
  type atp_step_name = ATP_Proof.atp_step_name
54495
237d5be57277 refactored
blanchet
parents: 54093
diff changeset
    11
  type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53052
diff changeset
    12
  type 'a atp_proof = 'a ATP_Proof.atp_proof
49914
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
    13
  type stature = ATP_Problem_Generate.stature
55287
ffa306239316 renamed ML file
blanchet
parents: 55286
diff changeset
    14
  type one_line_params = Sledgehammer_Proof_Methods.one_line_params
49914
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
    15
55222
a4ef6eb1fc20 added a 'trace' option
blanchet
parents: 55220
diff changeset
    16
  val trace : bool Config.T
a4ef6eb1fc20 added a 'trace' option
blanchet
parents: 55220
diff changeset
    17
49914
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
    18
  type isar_params =
57783
2bf99b3f62e1 cleaner 'compress' option
blanchet
parents: 57780
diff changeset
    19
    bool * (string option * string option) * Time.time * real option * bool * bool
55288
1a4358d14ce2 added 'smt' option to control generation of 'by smt' proofs
blanchet
parents: 55287
diff changeset
    20
    * (term, string) atp_step list * thm
49914
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
    21
71931
0c8a9c028304 simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)
blanchet
parents: 70931
diff changeset
    22
  val proof_text : Proof.context -> bool -> bool option -> bool -> (unit -> isar_params) -> int ->
0c8a9c028304 simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)
blanchet
parents: 70931
diff changeset
    23
    one_line_params -> string
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    24
end;
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    25
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55194
diff changeset
    26
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    27
struct
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    28
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    29
open ATP_Util
49914
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
    30
open ATP_Problem
70931
1d2b2cc792f1 removed experimental encoding for Waldmeister
blanchet
parents: 69593
diff changeset
    31
open ATP_Problem_Generate
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    32
open ATP_Proof
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    33
open ATP_Proof_Reconstruct
49918
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49917
diff changeset
    34
open Sledgehammer_Util
55287
ffa306239316 renamed ML file
blanchet
parents: 55286
diff changeset
    35
open Sledgehammer_Proof_Methods
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55194
diff changeset
    36
open Sledgehammer_Isar_Proof
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55194
diff changeset
    37
open Sledgehammer_Isar_Preplay
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55194
diff changeset
    38
open Sledgehammer_Isar_Compress
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55194
diff changeset
    39
open Sledgehammer_Isar_Minimize
49914
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
    40
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
    41
structure String_Redirect = ATP_Proof_Redirect(
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53052
diff changeset
    42
  type key = atp_step_name
49914
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
    43
  val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s')
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
    44
  val string_of = fst)
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
    45
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    46
open String_Redirect
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    47
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69205
diff changeset
    48
val trace = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_isar_trace\<close> (K false)
55222
a4ef6eb1fc20 added a 'trace' option
blanchet
parents: 55220
diff changeset
    49
57785
0388026060d1 deal with E definitions
blanchet
parents: 57783
diff changeset
    50
val e_definition_rule = "definition"
57654
f89c0749533d 'shift_quantors' is not an E skolemization rule (cf. 3ab503b04bdb)
blanchet
parents: 57288
diff changeset
    51
val e_skolemize_rule = "skolemize"
57759
d7454ee84f34 more precise handling of LEO-II skolemization
blanchet
parents: 57758
diff changeset
    52
val leo2_extcnf_forall_neg_rule = "extcnf_forall_neg"
57709
9cda0c64c37a imported patch hilbert_choice_support
fleury
parents: 57708
diff changeset
    53
val satallax_skolemize_rule = "tab_ex"
54746
6db5fbc02436 better handling of Z3 proof blocks
blanchet
parents: 54716
diff changeset
    54
val vampire_skolemisation_rule = "skolemisation"
57761
blanchet
parents: 57759
diff changeset
    55
val veriT_la_generic_rule = "la_generic"
57708
4b52c1b319ce veriT changes for lifted terms, and ite_elim rules.
fleury
parents: 57705
diff changeset
    56
val veriT_simp_arith_rule = "simp_arith"
72513
75f5c63f6cfa better handling of skolemization for Isar reconstruction in Sledgehammer for veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 72401
diff changeset
    57
val veriT_skolemize_rules = Verit_Proof.skolemization_steps
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57792
diff changeset
    58
val z3_skolemize_rule = Z3_Proof.string_of_rule Z3_Proof.Skolemize
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57792
diff changeset
    59
val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "")
57702
dfc834e39c1f Skolemization support for leo-II and Zipperposition.
fleury
parents: 57699
diff changeset
    60
val zipperposition_cnf_rule = "cnf"
54746
6db5fbc02436 better handling of Z3 proof blocks
blanchet
parents: 54716
diff changeset
    61
54772
f5fd4a34b0e8 handle Skolems gracefully for SPASS as well
blanchet
parents: 54771
diff changeset
    62
val skolemize_rules =
57785
0388026060d1 deal with E definitions
blanchet
parents: 57783
diff changeset
    63
  [e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule,
72513
75f5c63f6cfa better handling of skolemization for Isar reconstruction in Sledgehammer for veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 72401
diff changeset
    64
   spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule,
75f5c63f6cfa better handling of skolemization for Isar reconstruction in Sledgehammer for veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 72401
diff changeset
    65
   zipperposition_cnf_rule] @ veriT_skolemize_rules
54746
6db5fbc02436 better handling of Z3 proof blocks
blanchet
parents: 54716
diff changeset
    66
58653
4b44c227c0e0 improved handling of extensionality in Isar proofs generated from LEO-II and Satallax
blanchet
parents: 58517
diff changeset
    67
fun is_ext_rule rule = (rule = leo2_extcnf_equal_neg_rule)
4b44c227c0e0 improved handling of extensionality in Isar proofs generated from LEO-II and Satallax
blanchet
parents: 58517
diff changeset
    68
val is_maybe_ext_rule = is_ext_rule orf String.isPrefix satallax_tab_rule_prefix
4b44c227c0e0 improved handling of extensionality in Isar proofs generated from LEO-II and Satallax
blanchet
parents: 58517
diff changeset
    69
54769
3d6ac2f68bf3 correcly recognize E skolemization steps that are wrapped in a 'shift_quantors' inference
blanchet
parents: 54768
diff changeset
    70
val is_skolemize_rule = member (op =) skolemize_rules
57761
blanchet
parents: 57759
diff changeset
    71
fun is_arith_rule rule =
57762
blanchet
parents: 57761
diff changeset
    72
  String.isPrefix z3_th_lemma_rule_prefix rule orelse rule = veriT_simp_arith_rule orelse
57761
blanchet
parents: 57759
diff changeset
    73
  rule = veriT_la_generic_rule
54755
2eb43ddde491 use 'arith' when appropriate in Z3 proofs
blanchet
parents: 54754
diff changeset
    74
54501
77c9460e01b0 simplified old code
blanchet
parents: 54500
diff changeset
    75
fun raw_label_of_num num = (num, 0)
49914
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
    76
54501
77c9460e01b0 simplified old code
blanchet
parents: 54500
diff changeset
    77
fun label_of_clause [(num, _)] = raw_label_of_num num
77c9460e01b0 simplified old code
blanchet
parents: 54500
diff changeset
    78
  | label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0)
50005
e9a9bff107da handle non-unit clauses gracefully
blanchet
parents: 50004
diff changeset
    79
58653
4b44c227c0e0 improved handling of extensionality in Isar proofs generated from LEO-II and Satallax
blanchet
parents: 58517
diff changeset
    80
fun add_global_fact ss = apsnd (union (op =) ss)
4b44c227c0e0 improved handling of extensionality in Isar proofs generated from LEO-II and Satallax
blanchet
parents: 58517
diff changeset
    81
4b44c227c0e0 improved handling of extensionality in Isar proofs generated from LEO-II and Satallax
blanchet
parents: 58517
diff changeset
    82
fun add_fact_of_dependency [(_, ss as _ :: _)] = add_global_fact ss
4b44c227c0e0 improved handling of extensionality in Isar proofs generated from LEO-II and Satallax
blanchet
parents: 58517
diff changeset
    83
  | add_fact_of_dependency names = apfst (insert (op =) (label_of_clause names))
49914
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
    84
54799
blanchet
parents: 54772
diff changeset
    85
fun add_line_pass1 (line as (name, role, t, rule, [])) lines =
54770
0e354ef1b167 reverse Skolem function arguments
blanchet
parents: 54769
diff changeset
    86
    (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or
0e354ef1b167 reverse Skolem function arguments
blanchet
parents: 54769
diff changeset
    87
       definitions. *)
57708
4b52c1b319ce veriT changes for lifted terms, and ite_elim rules.
fleury
parents: 57705
diff changeset
    88
    if role = Conjecture orelse role = Negated_Conjecture then
4b52c1b319ce veriT changes for lifted terms, and ite_elim rules.
fleury
parents: 57705
diff changeset
    89
      line :: lines
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69205
diff changeset
    90
    else if t aconv \<^prop>\<open>True\<close> then
57708
4b52c1b319ce veriT changes for lifted terms, and ite_elim rules.
fleury
parents: 57705
diff changeset
    91
      map (replace_dependencies_in_line (name, [])) lines
57714
4856a7b8b9c3 Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents: 57713
diff changeset
    92
    else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then
57708
4b52c1b319ce veriT changes for lifted terms, and ite_elim rules.
fleury
parents: 57705
diff changeset
    93
      line :: lines
4b52c1b319ce veriT changes for lifted terms, and ite_elim rules.
fleury
parents: 57705
diff changeset
    94
    else if role = Axiom then
4b52c1b319ce veriT changes for lifted terms, and ite_elim rules.
fleury
parents: 57705
diff changeset
    95
      lines (* axioms (facts) need no proof lines *)
57768
a63f14f1214c fine-tuned Isar reconstruction, esp. boolean simplifications
blanchet
parents: 57767
diff changeset
    96
    else
a63f14f1214c fine-tuned Isar reconstruction, esp. boolean simplifications
blanchet
parents: 57767
diff changeset
    97
      map (replace_dependencies_in_line (name, [])) lines
54755
2eb43ddde491 use 'arith' when appropriate in Z3 proofs
blanchet
parents: 54754
diff changeset
    98
  | add_line_pass1 line lines = line :: lines
49914
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
    99
57771
0265ccdb9e6f better duplicate detection
blanchet
parents: 57770
diff changeset
   100
fun add_lines_pass2 res [] = rev res
0265ccdb9e6f better duplicate detection
blanchet
parents: 57770
diff changeset
   101
  | add_lines_pass2 res ((line as (name, role, t, rule, deps)) :: lines) =
55184
6e2295db4cf8 keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents: 55183
diff changeset
   102
    let
57791
blanchet
parents: 57787
diff changeset
   103
      fun normalize role =
blanchet
parents: 57787
diff changeset
   104
        role = Conjecture ? (HOLogic.dest_Trueprop #> s_not #> HOLogic.mk_Trueprop)
blanchet
parents: 57787
diff changeset
   105
57771
0265ccdb9e6f better duplicate detection
blanchet
parents: 57770
diff changeset
   106
      val norm_t = normalize role t
0265ccdb9e6f better duplicate detection
blanchet
parents: 57770
diff changeset
   107
      val is_duplicate =
0265ccdb9e6f better duplicate detection
blanchet
parents: 57770
diff changeset
   108
        exists (fn (prev_name, prev_role, prev_t, _, _) =>
58514
1fc93ea5136b eliminate duplicate hypotheses (which can arise due to (un)clausification)
blanchet
parents: 58506
diff changeset
   109
            (prev_role = Hypothesis andalso prev_t aconv t) orelse
1fc93ea5136b eliminate duplicate hypotheses (which can arise due to (un)clausification)
blanchet
parents: 58506
diff changeset
   110
            (member (op =) deps prev_name andalso
1fc93ea5136b eliminate duplicate hypotheses (which can arise due to (un)clausification)
blanchet
parents: 58506
diff changeset
   111
             Term.aconv_untyped (normalize prev_role prev_t, norm_t)))
57771
0265ccdb9e6f better duplicate detection
blanchet
parents: 57770
diff changeset
   112
          res
57770
6c4ab6f0a6fc normalize conjectures vs. negated conjectures when comparing terms
blanchet
parents: 57769
diff changeset
   113
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69205
diff changeset
   114
      fun looks_boring () = t aconv \<^prop>\<open>False\<close> orelse length deps < 2
55184
6e2295db4cf8 keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents: 55183
diff changeset
   115
6e2295db4cf8 keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents: 55183
diff changeset
   116
      fun is_skolemizing_line (_, _, _, rule', deps') =
6e2295db4cf8 keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents: 55183
diff changeset
   117
        is_skolemize_rule rule' andalso member (op =) deps' name
57770
6c4ab6f0a6fc normalize conjectures vs. negated conjectures when comparing terms
blanchet
parents: 57769
diff changeset
   118
55184
6e2295db4cf8 keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents: 55183
diff changeset
   119
      fun is_before_skolemize_rule () = exists is_skolemizing_line lines
6e2295db4cf8 keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents: 55183
diff changeset
   120
    in
57771
0265ccdb9e6f better duplicate detection
blanchet
parents: 57770
diff changeset
   121
      if is_duplicate orelse
57770
6c4ab6f0a6fc normalize conjectures vs. negated conjectures when comparing terms
blanchet
parents: 57769
diff changeset
   122
          (role = Plain andalso not (is_skolemize_rule rule) andalso
58653
4b44c227c0e0 improved handling of extensionality in Isar proofs generated from LEO-II and Satallax
blanchet
parents: 58517
diff changeset
   123
           not (is_ext_rule rule) andalso not (is_arith_rule rule) andalso
72401
2783779b7dd3 removed obsolete unmaintained experimental prover Pirate
blanchet
parents: 72355
diff changeset
   124
           not (null lines) andalso looks_boring () andalso not (is_before_skolemize_rule ())) then
57771
0265ccdb9e6f better duplicate detection
blanchet
parents: 57770
diff changeset
   125
        add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines)
55184
6e2295db4cf8 keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents: 55183
diff changeset
   126
      else
57771
0265ccdb9e6f better duplicate detection
blanchet
parents: 57770
diff changeset
   127
        add_lines_pass2 (line :: res) lines
55184
6e2295db4cf8 keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents: 55183
diff changeset
   128
    end
49914
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
   129
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
   130
type isar_params =
57783
2bf99b3f62e1 cleaner 'compress' option
blanchet
parents: 57780
diff changeset
   131
  bool * (string option * string option) * Time.time * real option * bool * bool
55288
1a4358d14ce2 added 'smt' option to control generation of 'by smt' proofs
blanchet
parents: 55287
diff changeset
   132
  * (term, string) atp_step list * thm
49914
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
   133
56852
b38c5b9cf590 added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0')
blanchet
parents: 56130
diff changeset
   134
val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method]
58092
4ae52c60603a renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents: 58083
diff changeset
   135
val basic_simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method]
55323
253a029335a2 split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents: 55311
diff changeset
   136
val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method]
55311
2bb02ba5d4b7 rationalized lists of methods
blanchet
parents: 55310
diff changeset
   137
57744
a68b8db8691d added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents: 57741
diff changeset
   138
val arith_methods = basic_arith_methods @ basic_simp_based_methods @ basic_systematic_methods
a68b8db8691d added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents: 57741
diff changeset
   139
val systematic_methods =
a68b8db8691d added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents: 57741
diff changeset
   140
  basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @
57699
a6cf197c1f1e also try 'metis' with 'full_types'
blanchet
parents: 57657
diff changeset
   141
  [Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)]
57744
a68b8db8691d added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents: 57741
diff changeset
   142
val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods
58517
64f6b4bd52a7 more precise lemma insertion
blanchet
parents: 58516
diff changeset
   143
val skolem_methods = Moura_Method :: systematic_methods
54766
6ac273f176cd store alternative proof methods in Isar data structure
blanchet
parents: 54765
diff changeset
   144
60612
79d71bfea310 removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents: 59577
diff changeset
   145
fun isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params
57739
blanchet
parents: 57735
diff changeset
   146
    (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) =
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   147
  let
58843
521cea5fa777 discontinued obsolete Output.urgent_message;
wenzelm
parents: 58653
diff changeset
   148
    val _ = if debug then writeln "Constructing Isar proof..." else ()
56097
blanchet
parents: 56093
diff changeset
   149
57287
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   150
    fun generate_proof_text () =
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   151
      let
57791
blanchet
parents: 57787
diff changeset
   152
        val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof0, goal) =
57245
f6bf6d5341ee renamed Sledgehammer options
blanchet
parents: 57154
diff changeset
   153
          isar_params ()
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   154
      in
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   155
        if null atp_proof0 then
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   156
          one_line_proof_text ctxt 0 one_line_params
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   157
        else
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   158
          let
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   159
            val systematic_methods' = insert (op =) (Metis_Method alt_metis_args) systematic_methods
55168
948e8b7ea82f correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents: 54838
diff changeset
   160
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   161
            fun massage_methods (meths as meth :: _) =
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   162
              if not try0 then [meth]
72518
4be6ae020fc4 Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents: 72513
diff changeset
   163
              else if smt_proofs then SMT_Method SMT_Default :: meths
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   164
              else meths
55168
948e8b7ea82f correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents: 54838
diff changeset
   165
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   166
            val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   167
            val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   168
            val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
55168
948e8b7ea82f correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents: 54838
diff changeset
   169
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   170
            val do_preplay = preplay_timeout <> Time.zeroTime
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   171
            val compress =
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   172
              (case compress of
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   173
                NONE => if isar_proofs = NONE andalso do_preplay then 1000.0 else 10.0
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   174
              | SOME n => n)
55168
948e8b7ea82f correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents: 54838
diff changeset
   175
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   176
            fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   177
            fun skolems_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev
54700
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   178
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   179
            fun get_role keep_role ((num, _), role, t, rule, _) =
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   180
              if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   181
72355
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 71931
diff changeset
   182
            val trace = Config.get ctxt trace
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 71931
diff changeset
   183
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 71931
diff changeset
   184
            val string_of_atp_steps =
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 71931
diff changeset
   185
              let val to_string = ATP_Proof.string_of_atp_step (Syntax.string_of_term ctxt) I in
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 71931
diff changeset
   186
                enclose "[\n" "\n]" o cat_lines o map (enclose "  " "," o to_string)
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 71931
diff changeset
   187
              end
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 71931
diff changeset
   188
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 71931
diff changeset
   189
            val atp_proof = atp_proof0
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 71931
diff changeset
   190
              |> trace ? tap (tracing o prefix "atp_proof0 = " o string_of_atp_steps)
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 71931
diff changeset
   191
              |> (fn x => fold_rev add_line_pass1 x [])
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   192
              |> add_lines_pass2 []
72355
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 71931
diff changeset
   193
              |> trace ? tap (tracing o prefix "atp_proof = " o string_of_atp_steps)
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   194
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   195
            val conjs =
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   196
              map_filter (fn (name, role, _, _, _) =>
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   197
                  if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE)
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   198
                atp_proof
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   199
            val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof
57288
ffd928316c75 supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents: 57287
diff changeset
   200
72584
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   201
            fun add_lemma ((label, goal), rule) ctxt =
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   202
              let
72584
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   203
                val (skos, proof_methods) =
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   204
                  (if is_skolemize_rule rule then (skolems_of ctxt goal, skolem_methods)
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   205
                   else if is_arith_rule rule then ([], arith_methods)
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   206
                   else ([], rewrite_methods))
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   207
                  ||> massage_methods
72584
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   208
                val prove = Prove {
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   209
                  qualifiers = [],
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   210
                  obtains = skos,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   211
                  label = label,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   212
                  goal = goal,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   213
                  subproofs = [],
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   214
                  facts = ([], []),
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   215
                  proof_methods = proof_methods,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   216
                  comment = ""}
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   217
              in
72584
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   218
                (prove, ctxt |> not (null skos) ? (Variable.add_fixes (map fst skos) #> snd))
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   219
              end
57288
ffd928316c75 supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents: 57287
diff changeset
   220
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   221
            val (lems, _) =
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   222
              fold_map add_lemma (map_filter (get_role (curry (op =) Lemma)) atp_proof) ctxt
54700
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   223
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   224
            val bot = #1 (List.last atp_proof)
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   225
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   226
            val refute_graph =
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   227
              atp_proof
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   228
              |> map (fn (name, _, _, _, from) => (from, name))
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   229
              |> make_refute_graph bot
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   230
              |> fold (Atom_Graph.default_node o rpair ()) conjs
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   231
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   232
            val axioms = axioms_of_refute_graph refute_graph conjs
54700
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   233
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   234
            val tainted = tainted_atoms_of_refute_graph refute_graph conjs
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   235
            val is_clause_tainted = exists (member (op =) tainted)
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   236
            val steps =
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   237
              Symtab.empty
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   238
              |> fold (fn (name as (s, _), role, t, rule, _) =>
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   239
                  Symtab.update_new (s, (rule, t
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   240
                    |> (if is_clause_tainted [name] then
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   241
                          HOLogic.dest_Trueprop
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   242
                          #> role <> Conjecture ? s_not
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   243
                          #> fold exists_of (map Var (Term.add_vars t []))
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   244
                          #> HOLogic.mk_Trueprop
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   245
                        else
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   246
                          I))))
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   247
                atp_proof
58516
1edba0152491 insert lemmas closer to where they are needed, both for esthetics and (primarily) for correctness in case the lemma refers to a skolem
blanchet
parents: 58514
diff changeset
   248
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   249
            fun is_referenced_in_step _ (Let _) = false
72584
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   250
              | is_referenced_in_step l (Prove {subproofs, facts = (ls, _), ...}) =
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   251
                member (op =) ls l orelse exists (is_referenced_in_proof l) subproofs
72582
b69a3a7655f2 Tuned isar_proof datatype
desharna
parents: 72518
diff changeset
   252
            and is_referenced_in_proof l (Proof {steps, ...}) =
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   253
              exists (is_referenced_in_step l) steps
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   254
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   255
            fun insert_lemma_in_step lem
72584
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   256
                  (step as Prove {qualifiers, obtains, label, goal, subproofs, facts = (ls, gs),
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   257
                  proof_methods, comment}) =
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   258
              let val l' = the (label_of_isar_step lem) in
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   259
                if member (op =) ls l' then
58517
64f6b4bd52a7 more precise lemma insertion
blanchet
parents: 58516
diff changeset
   260
                  [lem, step]
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   261
                else
72584
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   262
                  let val refs = map (is_referenced_in_proof l') subproofs in
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   263
                    if length (filter I refs) = 1 then
72584
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   264
                      [Prove {
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   265
                        qualifiers = qualifiers,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   266
                        obtains = obtains,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   267
                        label = label,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   268
                        goal = goal,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   269
                        subproofs =
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   270
                          map2 (fn false => I | true => insert_lemma_in_proof lem) refs subproofs,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   271
                        facts = (ls, gs),
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   272
                        proof_methods = proof_methods,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   273
                        comment = comment}]
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   274
                    else
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   275
                      [lem, step]
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   276
                  end
58517
64f6b4bd52a7 more precise lemma insertion
blanchet
parents: 58516
diff changeset
   277
              end
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   278
            and insert_lemma_in_steps lem [] = [lem]
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   279
              | insert_lemma_in_steps lem (step :: steps) =
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   280
                if is_referenced_in_step (the (label_of_isar_step lem)) step then
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   281
                  insert_lemma_in_step lem step @ steps
54700
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   282
                else
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   283
                  step :: insert_lemma_in_steps lem steps
72583
e728d3a3d383 Tuned isar_proofs constructions
desharna
parents: 72582
diff changeset
   284
            and insert_lemma_in_proof lem (proof as Proof {steps, ...}) =
72585
18eb7ec2720f Tuned indentation
desharna
parents: 72584
diff changeset
   285
              isar_proof_with_steps proof (insert_lemma_in_steps lem steps)
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   286
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   287
            val rule_of_clause_id = fst o the o Symtab.lookup steps o fst
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   288
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   289
            val finish_off = close_form #> rename_bound_vars
54755
2eb43ddde491 use 'arith' when appropriate in Z3 proofs
blanchet
parents: 54754
diff changeset
   290
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   291
            fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> finish_off
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   292
              | prop_of_clause names =
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   293
                let
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   294
                  val lits =
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   295
                    map (HOLogic.dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names)
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   296
                in
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   297
                  (case List.partition (can HOLogic.dest_not) lits of
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   298
                    (negs as _ :: _, pos as _ :: _) =>
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   299
                    s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs),
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   300
                      Library.foldr1 s_disj pos)
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69205
diff changeset
   301
                  | _ => fold (curry s_disj) lits \<^term>\<open>False\<close>)
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   302
                end
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   303
                |> HOLogic.mk_Trueprop |> finish_off
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   304
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   305
            fun maybe_show outer c = if outer andalso eq_set (op =) (c, conjs) then [Show] else []
55280
f0187a12b8f2 tuned data structure
blanchet
parents: 55279
diff changeset
   306
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   307
            fun isar_steps outer predecessor accum [] =
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   308
                accum
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   309
                |> (if tainted = [] then
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   310
                      (* e.g., trivial, empty proof by Z3 *)
72584
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   311
                      cons (Prove {
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   312
                        qualifiers = if outer then [Show] else [],
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   313
                        obtains = [],
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   314
                        label = no_label,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   315
                        goal = concl_t,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   316
                        subproofs = [],
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   317
                        facts = sort_facts (the_list predecessor, []),
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   318
                        proof_methods = massage_methods systematic_methods',
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   319
                        comment = ""})
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   320
                    else
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   321
                      I)
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   322
                |> rev
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   323
              | isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) =
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   324
                let
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   325
                  val l = label_of_clause c
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   326
                  val t = prop_of_clause c
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   327
                  val rule = rule_of_clause_id id
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   328
                  val skolem = is_skolemize_rule rule
54700
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   329
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   330
                  val deps = ([], [])
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   331
                    |> fold add_fact_of_dependency gamma
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   332
                    |> is_maybe_ext_rule rule ? add_global_fact [short_thm_name ctxt ext]
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   333
                    |> sort_facts
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   334
                  val meths =
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   335
                    (if skolem then skolem_methods
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   336
                     else if is_arith_rule rule then arith_methods
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   337
                     else systematic_methods')
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   338
                    |> massage_methods
55214
48a347b40629 better tracing + syntactically correct 'metis' calls
blanchet
parents: 55213
diff changeset
   339
72584
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   340
                  fun prove subproofs facts = Prove {
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   341
                    qualifiers = maybe_show outer c,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   342
                    obtains = [],
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   343
                    label = l,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   344
                    goal = t,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   345
                    subproofs = subproofs,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   346
                    facts = facts,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   347
                    proof_methods = meths,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   348
                    comment = ""}
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   349
                  fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   350
                in
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   351
                  if is_clause_tainted c then
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   352
                    (case gamma of
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   353
                      [g] =>
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   354
                      if skolem andalso is_clause_tainted g then
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   355
                        let
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   356
                          val skos = skolems_of ctxt (prop_of_clause g)
72582
b69a3a7655f2 Tuned isar_proof datatype
desharna
parents: 72518
diff changeset
   357
                          val subproof = Proof {fixes = skos, assumptions = [], steps = rev accum}
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   358
                        in
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   359
                          isar_steps outer (SOME l) [prove [subproof] ([], [])] infs
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   360
                        end
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   361
                      else
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   362
                        steps_of_rest (prove [] deps)
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   363
                    | _ => steps_of_rest (prove [] deps))
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   364
                  else
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   365
                    steps_of_rest
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   366
                      (if skolem then
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   367
                         (case skolems_of ctxt t of
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   368
                           [] => prove [] deps
72584
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   369
                         | skos => Prove {
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   370
                             qualifiers = [],
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   371
                             obtains = skos,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   372
                             label = l,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   373
                             goal = t,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   374
                             subproofs = [],
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   375
                             facts = deps,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   376
                             proof_methods = meths,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   377
                             comment = ""})
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   378
                       else
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   379
                         prove [] deps)
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   380
                end
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   381
              | isar_steps outer predecessor accum (Cases cases :: infs) =
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   382
                let
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   383
                  fun isar_case (c, subinfs) =
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   384
                    isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   385
                  val c = succedent_of_cases cases
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   386
                  val l = label_of_clause c
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   387
                  val t = prop_of_clause c
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   388
                  val step =
72584
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   389
                    Prove {
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   390
                      qualifiers = maybe_show outer c,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   391
                      obtains = [],
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   392
                      label = l,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   393
                      goal = t,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   394
                      subproofs = map isar_case (filter_out (null o snd) cases),
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   395
                      facts = sort_facts (the_list predecessor, []),
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   396
                      proof_methods = massage_methods systematic_methods',
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   397
                      comment = ""}
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   398
                in
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   399
                  isar_steps outer (SOME l) (step :: accum) infs
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   400
                end
72582
b69a3a7655f2 Tuned isar_proof datatype
desharna
parents: 72518
diff changeset
   401
            and isar_proof outer fixes assumptions lems infs =
b69a3a7655f2 Tuned isar_proof datatype
desharna
parents: 72518
diff changeset
   402
              let val steps = fold_rev insert_lemma_in_steps lems (isar_steps outer NONE [] infs) in
b69a3a7655f2 Tuned isar_proof datatype
desharna
parents: 72518
diff changeset
   403
                Proof {fixes = fixes, assumptions = assumptions, steps = steps}
b69a3a7655f2 Tuned isar_proof datatype
desharna
parents: 72518
diff changeset
   404
              end
55214
48a347b40629 better tracing + syntactically correct 'metis' calls
blanchet
parents: 55213
diff changeset
   405
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   406
            val canonical_isar_proof =
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   407
              refute_graph
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   408
              |> trace ? tap (tracing o prefix "Refute graph:\n" o string_of_refute_graph)
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   409
              |> redirect_graph axioms tainted bot
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   410
              |> trace ? tap (tracing o prefix "Direct proof:\n" o string_of_direct_proof)
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   411
              |> isar_proof true params assms lems
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   412
              |> postprocess_isar_proof_remove_show_stuttering
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   413
              |> postprocess_isar_proof_remove_unreferenced_steps I
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   414
              |> relabel_isar_proof_canonically
54754
6b0ca7f79e93 robustness in degenerate case + tuning
blanchet
parents: 54753
diff changeset
   415
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   416
            val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   417
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   418
            val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   419
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   420
            val _ = fold_isar_steps (fn meth =>
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   421
                K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth []))
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   422
              (steps_of_isar_proof canonical_isar_proof) ()
55299
c3bb1cffce26 generate comments in Isar proofs
blanchet
parents: 55297
diff changeset
   423
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   424
            fun str_of_preplay_outcome outcome =
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   425
              if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   426
            fun str_of_meth l meth =
72401
2783779b7dd3 removed obsolete unmaintained experimental prover Pirate
blanchet
parents: 72355
diff changeset
   427
              string_of_proof_method [] meth ^ " " ^
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   428
              str_of_preplay_outcome
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   429
                (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   430
            fun comment_of l = map (str_of_meth l) #> commas
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   431
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   432
            fun trace_isar_proof label proof =
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   433
              if trace then
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   434
                tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   435
                  string_of_isar_proof ctxt subgoal subgoal_count
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   436
                    (comment_isar_proof comment_of proof) ^ "\n")
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   437
              else
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   438
                ()
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   439
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   440
            fun comment_of l (meth :: _) =
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   441
              (case (verbose,
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   442
                  Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)) of
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   443
                (false, Played _) => ""
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   444
              | (_, outcome) => string_of_play_outcome outcome)
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   445
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   446
            val (play_outcome, isar_proof) =
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   447
              canonical_isar_proof
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   448
              |> tap (trace_isar_proof "Original")
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   449
              |> compress_isar_proof ctxt compress preplay_timeout preplay_data
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   450
              |> tap (trace_isar_proof "Compressed")
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   451
              |> postprocess_isar_proof_remove_unreferenced_steps
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   452
                   (keep_fastest_method_of_isar_step (!preplay_data)
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   453
                    #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   454
              |> tap (trace_isar_proof "Minimized")
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   455
              |> `(preplay_outcome_of_isar_proof (!preplay_data))
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   456
              ||> (comment_isar_proof comment_of
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   457
                   #> chain_isar_proof
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   458
                   #> kill_useless_labels_in_isar_proof
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   459
                   #> relabel_isar_proof_nicely
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   460
                   #> rationalize_obtains_in_isar_proofs ctxt)
57287
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   461
          in
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   462
            (case (num_chained, add_isar_steps (steps_of_isar_proof isar_proof) 0) of
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   463
              (0, 1) =>
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   464
              one_line_proof_text ctxt 0
67560
0fa87bd86566 tuned signature: more operations;
wenzelm
parents: 63692
diff changeset
   465
                (if is_less (play_outcome_ord (play_outcome, one_line_play)) then
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   466
                   (case isar_proof of
72584
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   467
                     Proof {steps = [Prove {facts = (_, gfs), proof_methods = meth :: _, ...}],
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 72583
diff changeset
   468
                     ...} =>
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   469
                     let
68668
c9570658e8f1 don't lose facts that were introduced to deal with a theory or some preprocessing in the prover (e.g. the definition of 'abs' in an SMT proof)
blanchet
parents: 67560
diff changeset
   470
                       val used_facts' =
c9570658e8f1 don't lose facts that were introduced to deal with a theory or some preprocessing in the prover (e.g. the definition of 'abs' in an SMT proof)
blanchet
parents: 67560
diff changeset
   471
                         map_filter (fn s =>
c9570658e8f1 don't lose facts that were introduced to deal with a theory or some preprocessing in the prover (e.g. the definition of 'abs' in an SMT proof)
blanchet
parents: 67560
diff changeset
   472
                            if exists (fn (s', (sc, _)) => s' = s andalso sc = Chained)
c9570658e8f1 don't lose facts that were introduced to deal with a theory or some preprocessing in the prover (e.g. the definition of 'abs' in an SMT proof)
blanchet
parents: 67560
diff changeset
   473
                                used_facts then
c9570658e8f1 don't lose facts that were introduced to deal with a theory or some preprocessing in the prover (e.g. the definition of 'abs' in an SMT proof)
blanchet
parents: 67560
diff changeset
   474
                              NONE
c9570658e8f1 don't lose facts that were introduced to deal with a theory or some preprocessing in the prover (e.g. the definition of 'abs' in an SMT proof)
blanchet
parents: 67560
diff changeset
   475
                            else
c9570658e8f1 don't lose facts that were introduced to deal with a theory or some preprocessing in the prover (e.g. the definition of 'abs' in an SMT proof)
blanchet
parents: 67560
diff changeset
   476
                              SOME (s, (Global, General))) gfs
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   477
                     in
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   478
                       ((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count)
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   479
                     end)
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   480
                 else
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   481
                   one_line_params) ^
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   482
              (if isar_proofs = SOME true then "\n(No Isar proof available.)" else "")
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   483
            | (_, num_steps) =>
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   484
              let
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   485
                val msg =
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   486
                  (if verbose then [string_of_int num_steps ^ " step" ^ plural_s num_steps]
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   487
                   else []) @
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   488
                  (if do_preplay then [string_of_play_outcome play_outcome] else [])
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   489
              in
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   490
                one_line_proof_text ctxt 0 one_line_params ^
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   491
                "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
63518
ae8fd6fe63a1 tuned signature;
wenzelm
parents: 62826
diff changeset
   492
                Active.sendback_markup_command
62220
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   493
                  (string_of_isar_proof ctxt subgoal subgoal_count isar_proof)
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   494
              end)
0e17a97234bd avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents: 60612
diff changeset
   495
          end
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   496
      end
57056
8b2283566f6e properly reconstruct helpers in Z3 proofs
blanchet
parents: 57054
diff changeset
   497
  in
57287
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   498
    if debug then
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   499
      generate_proof_text ()
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   500
    else
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   501
      (case try generate_proof_text () of
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   502
        SOME s => s
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   503
      | NONE =>
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   504
        one_line_proof_text ctxt 0 one_line_params ^
63692
1bc4bc2c9fd1 killed final stops in Sledgehammer and friends
blanchet
parents: 63518
diff changeset
   505
        (if isar_proofs = SOME true then "\nWarning: Isar proof construction failed" else ""))
57056
8b2283566f6e properly reconstruct helpers in Z3 proofs
blanchet
parents: 57054
diff changeset
   506
  end
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   507
72355
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 71931
diff changeset
   508
fun isar_proof_would_be_a_good_idea (_, play) =
54824
4e58a38b330b refactored preplaying outcome data structure
blanchet
parents: 54823
diff changeset
   509
  (case play of
71931
0c8a9c028304 simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)
blanchet
parents: 70931
diff changeset
   510
    Played _ => false
62826
eb94e570c1a4 prefer infix operations;
wenzelm
parents: 62220
diff changeset
   511
  | Play_Timed_Out time => time > Time.zeroTime
56093
4eeb73a1feec simplified preplaying information
blanchet
parents: 56081
diff changeset
   512
  | Play_Failed => true)
51187
c344cf148e8f avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs
blanchet
parents: 51179
diff changeset
   513
55297
1dfcd49f5dcb renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents: 55296
diff changeset
   514
fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
57739
blanchet
parents: 57735
diff changeset
   515
    (one_line_params as ((_, preplay), _, _, _)) =
51190
2654b3965c8d made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents: 51187
diff changeset
   516
  (if isar_proofs = SOME true orelse
71931
0c8a9c028304 simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)
blanchet
parents: 70931
diff changeset
   517
      (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
60612
79d71bfea310 removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents: 59577
diff changeset
   518
     isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   519
   else
56985
82c83978fbd9 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents: 56983
diff changeset
   520
     one_line_proof_text ctxt num_chained) one_line_params
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   521
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   522
end;