src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
author blanchet
Mon, 15 Sep 2014 12:30:06 +0200
changeset 58341 6c8b30b9f583
parent 58142 d6a2e3567f95
child 58342 9a82544fd29f
permissions -rw-r--r--
removed accidental '@{print}'
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
55296
1d3dadda13a1 tuned behavior of 'smt' option
blanchet
parents: 55294
diff changeset
    22
  val proof_text : Proof.context -> bool -> bool option -> bool option -> (unit -> isar_params) ->
1d3dadda13a1 tuned behavior of 'smt' option
blanchet
parents: 55294
diff changeset
    23
    int -> 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
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    31
open ATP_Proof
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    32
open ATP_Proof_Reconstruct
49918
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49917
diff changeset
    33
open Sledgehammer_Util
55287
ffa306239316 renamed ML file
blanchet
parents: 55286
diff changeset
    34
open Sledgehammer_Proof_Methods
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55194
diff changeset
    35
open Sledgehammer_Isar_Proof
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55194
diff changeset
    36
open Sledgehammer_Isar_Preplay
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55194
diff changeset
    37
open Sledgehammer_Isar_Compress
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55194
diff changeset
    38
open Sledgehammer_Isar_Minimize
49914
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
    39
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
    40
structure String_Redirect = ATP_Proof_Redirect(
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53052
diff changeset
    41
  type key = atp_step_name
49914
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
    42
  val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s')
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
    43
  val string_of = fst)
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
    44
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    45
open String_Redirect
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    46
55222
a4ef6eb1fc20 added a 'trace' option
blanchet
parents: 55220
diff changeset
    47
val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false)
a4ef6eb1fc20 added a 'trace' option
blanchet
parents: 55220
diff changeset
    48
57785
0388026060d1 deal with E definitions
blanchet
parents: 57783
diff changeset
    49
val e_definition_rule = "definition"
57654
f89c0749533d 'shift_quantors' is not an E skolemization rule (cf. 3ab503b04bdb)
blanchet
parents: 57288
diff changeset
    50
val e_skolemize_rule = "skolemize"
57759
d7454ee84f34 more precise handling of LEO-II skolemization
blanchet
parents: 57758
diff changeset
    51
val leo2_extcnf_forall_neg_rule = "extcnf_forall_neg"
57709
9cda0c64c37a imported patch hilbert_choice_support
fleury
parents: 57708
diff changeset
    52
val satallax_skolemize_rule = "tab_ex"
54836
47857a79bdad recognize datatype reasoning in SPASS-Pirate
blanchet
parents: 54831
diff changeset
    53
val spass_pirate_datatype_rule = "DT"
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"
57761
blanchet
parents: 57759
diff changeset
    57
val veriT_tmp_ite_elim_rule = "tmp_ite_elim"
blanchet
parents: 57759
diff changeset
    58
val veriT_tmp_skolemize_rule = "tmp_skolemize"
58142
d6a2e3567f95 Some work on the new waldmeister integration
steckerm
parents: 58092
diff changeset
    59
val waldmeister_skolemize_rule = ATP_Waldmeister.waldmeister_skolemize_rule
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57792
diff changeset
    60
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
    61
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
    62
val zipperposition_cnf_rule = "cnf"
54746
6db5fbc02436 better handling of Z3 proof blocks
blanchet
parents: 54716
diff changeset
    63
54772
f5fd4a34b0e8 handle Skolems gracefully for SPASS as well
blanchet
parents: 54771
diff changeset
    64
val skolemize_rules =
57785
0388026060d1 deal with E definitions
blanchet
parents: 57783
diff changeset
    65
  [e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule,
0388026060d1 deal with E definitions
blanchet
parents: 57783
diff changeset
    66
   spass_skolemize_rule, vampire_skolemisation_rule, veriT_tmp_ite_elim_rule,
58142
d6a2e3567f95 Some work on the new waldmeister integration
steckerm
parents: 58092
diff changeset
    67
   veriT_tmp_skolemize_rule, waldmeister_skolemize_rule, z3_skolemize_rule, zipperposition_cnf_rule]
54746
6db5fbc02436 better handling of Z3 proof blocks
blanchet
parents: 54716
diff changeset
    68
54769
3d6ac2f68bf3 correcly recognize E skolemization steps that are wrapped in a 'shift_quantors' inference
blanchet
parents: 54768
diff changeset
    69
val is_skolemize_rule = member (op =) skolemize_rules
57761
blanchet
parents: 57759
diff changeset
    70
fun is_arith_rule rule =
57762
blanchet
parents: 57761
diff changeset
    71
  String.isPrefix z3_th_lemma_rule_prefix rule orelse rule = veriT_simp_arith_rule orelse
57761
blanchet
parents: 57759
diff changeset
    72
  rule = veriT_la_generic_rule
54836
47857a79bdad recognize datatype reasoning in SPASS-Pirate
blanchet
parents: 54831
diff changeset
    73
val is_datatype_rule = String.isPrefix spass_pirate_datatype_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
54505
d023838eb252 more refactoring to accommodate SMT proofs
blanchet
parents: 54503
diff changeset
    80
fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss)
d023838eb252 more refactoring to accommodate SMT proofs
blanchet
parents: 54503
diff changeset
    81
  | add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names))
49914
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
    82
54799
blanchet
parents: 54772
diff changeset
    83
fun add_line_pass1 (line as (name, role, t, rule, [])) lines =
54770
0e354ef1b167 reverse Skolem function arguments
blanchet
parents: 54769
diff changeset
    84
    (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or
0e354ef1b167 reverse Skolem function arguments
blanchet
parents: 54769
diff changeset
    85
       definitions. *)
57708
4b52c1b319ce veriT changes for lifted terms, and ite_elim rules.
fleury
parents: 57705
diff changeset
    86
    if role = Conjecture orelse role = Negated_Conjecture then
4b52c1b319ce veriT changes for lifted terms, and ite_elim rules.
fleury
parents: 57705
diff changeset
    87
      line :: lines
4b52c1b319ce veriT changes for lifted terms, and ite_elim rules.
fleury
parents: 57705
diff changeset
    88
    else if t aconv @{prop True} then
4b52c1b319ce veriT changes for lifted terms, and ite_elim rules.
fleury
parents: 57705
diff changeset
    89
      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
    90
    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
    91
      line :: lines
4b52c1b319ce veriT changes for lifted terms, and ite_elim rules.
fleury
parents: 57705
diff changeset
    92
    else if role = Axiom then
4b52c1b319ce veriT changes for lifted terms, and ite_elim rules.
fleury
parents: 57705
diff changeset
    93
      lines (* axioms (facts) need no proof lines *)
57768
a63f14f1214c fine-tuned Isar reconstruction, esp. boolean simplifications
blanchet
parents: 57767
diff changeset
    94
    else
a63f14f1214c fine-tuned Isar reconstruction, esp. boolean simplifications
blanchet
parents: 57767
diff changeset
    95
      map (replace_dependencies_in_line (name, [])) lines
54755
2eb43ddde491 use 'arith' when appropriate in Z3 proofs
blanchet
parents: 54754
diff changeset
    96
  | add_line_pass1 line lines = line :: lines
49914
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
    97
57771
0265ccdb9e6f better duplicate detection
blanchet
parents: 57770
diff changeset
    98
fun add_lines_pass2 res [] = rev res
0265ccdb9e6f better duplicate detection
blanchet
parents: 57770
diff changeset
    99
  | 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
   100
    let
57791
blanchet
parents: 57787
diff changeset
   101
      fun normalize role =
blanchet
parents: 57787
diff changeset
   102
        role = Conjecture ? (HOLogic.dest_Trueprop #> s_not #> HOLogic.mk_Trueprop)
blanchet
parents: 57787
diff changeset
   103
57771
0265ccdb9e6f better duplicate detection
blanchet
parents: 57770
diff changeset
   104
      val norm_t = normalize role t
0265ccdb9e6f better duplicate detection
blanchet
parents: 57770
diff changeset
   105
      val is_duplicate =
0265ccdb9e6f better duplicate detection
blanchet
parents: 57770
diff changeset
   106
        exists (fn (prev_name, prev_role, prev_t, _, _) =>
0265ccdb9e6f better duplicate detection
blanchet
parents: 57770
diff changeset
   107
            member (op =) deps prev_name andalso
0265ccdb9e6f better duplicate detection
blanchet
parents: 57770
diff changeset
   108
            Term.aconv_untyped (normalize prev_role prev_t, norm_t))
0265ccdb9e6f better duplicate detection
blanchet
parents: 57770
diff changeset
   109
          res
57770
6c4ab6f0a6fc normalize conjectures vs. negated conjectures when comparing terms
blanchet
parents: 57769
diff changeset
   110
57787
blanchet
parents: 57785
diff changeset
   111
      fun looks_boring () = t aconv @{prop False} 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
   112
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
   113
      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
   114
        is_skolemize_rule rule' andalso member (op =) deps' name
57770
6c4ab6f0a6fc normalize conjectures vs. negated conjectures when comparing terms
blanchet
parents: 57769
diff changeset
   115
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
   116
      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
   117
    in
57771
0265ccdb9e6f better duplicate detection
blanchet
parents: 57770
diff changeset
   118
      if is_duplicate orelse
57770
6c4ab6f0a6fc normalize conjectures vs. negated conjectures when comparing terms
blanchet
parents: 57769
diff changeset
   119
          (role = Plain andalso not (is_skolemize_rule rule) andalso
6c4ab6f0a6fc normalize conjectures vs. negated conjectures when comparing terms
blanchet
parents: 57769
diff changeset
   120
           not (is_arith_rule rule) andalso not (is_datatype_rule rule) andalso
6c4ab6f0a6fc normalize conjectures vs. negated conjectures when comparing terms
blanchet
parents: 57769
diff changeset
   121
           not (null lines) andalso looks_boring () andalso not (is_before_skolemize_rule ())) then
57771
0265ccdb9e6f better duplicate detection
blanchet
parents: 57770
diff changeset
   122
        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
   123
      else
57771
0265ccdb9e6f better duplicate detection
blanchet
parents: 57770
diff changeset
   124
        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
   125
    end
49914
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
   126
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
   127
type isar_params =
57783
2bf99b3f62e1 cleaner 'compress' option
blanchet
parents: 57780
diff changeset
   128
  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
   129
  * (term, string) atp_step list * thm
49914
23e36a4d28f1 refactor code
blanchet
parents: 49913
diff changeset
   130
56852
b38c5b9cf590 added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0')
blanchet
parents: 56130
diff changeset
   131
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
   132
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
   133
val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method]
55311
2bb02ba5d4b7 rationalized lists of methods
blanchet
parents: 55310
diff changeset
   134
57744
a68b8db8691d added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents: 57741
diff changeset
   135
val arith_methods = basic_arith_methods @ basic_simp_based_methods @ basic_systematic_methods
55311
2bb02ba5d4b7 rationalized lists of methods
blanchet
parents: 55310
diff changeset
   136
val datatype_methods = [Simp_Method, Simp_Size_Method]
57744
a68b8db8691d added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents: 57741
diff changeset
   137
val systematic_methods =
a68b8db8691d added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents: 57741
diff changeset
   138
  basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @
57699
a6cf197c1f1e also try 'metis' with 'full_types'
blanchet
parents: 57657
diff changeset
   139
  [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
   140
val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods
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
   141
fun skolem_methods_of z3 = basic_systematic_methods |> z3 ? cons Moura_Method
54766
6ac273f176cd store alternative proof methods in Isar data structure
blanchet
parents: 54765
diff changeset
   142
55297
1dfcd49f5dcb renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents: 55296
diff changeset
   143
fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
57739
blanchet
parents: 57735
diff changeset
   144
    (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) =
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   145
  let
56097
blanchet
parents: 56093
diff changeset
   146
    val _ = if debug then Output.urgent_message "Constructing Isar proof..." else ()
blanchet
parents: 56093
diff changeset
   147
57287
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   148
    fun generate_proof_text () =
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   149
      let
57791
blanchet
parents: 57787
diff changeset
   150
        val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof0, goal) =
57245
f6bf6d5341ee renamed Sledgehammer options
blanchet
parents: 57154
diff changeset
   151
          isar_params ()
55257
abfd7b90bba2 rationalized threading of 'metis' arguments
blanchet
parents: 55256
diff changeset
   152
57744
a68b8db8691d added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents: 57741
diff changeset
   153
        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
   154
55311
2bb02ba5d4b7 rationalized lists of methods
blanchet
parents: 55310
diff changeset
   155
        fun massage_methods (meths as meth :: _) =
57245
f6bf6d5341ee renamed Sledgehammer options
blanchet
parents: 57154
diff changeset
   156
          if not try0 then [meth]
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57792
diff changeset
   157
          else if smt_proofs = SOME true then SMT_Method :: meths
55297
1dfcd49f5dcb renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents: 55296
diff changeset
   158
          else meths
55273
e887c0743614 implemented new 'try0_isar' semantics
blanchet
parents: 55267
diff changeset
   159
55168
948e8b7ea82f correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents: 54838
diff changeset
   160
        val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
55264
43473497fb65 centralize preplaying
blanchet
parents: 55263
diff changeset
   161
        val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
43473497fb65 centralize preplaying
blanchet
parents: 55263
diff changeset
   162
        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
   163
948e8b7ea82f correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents: 54838
diff changeset
   164
        val do_preplay = preplay_timeout <> Time.zeroTime
57783
2bf99b3f62e1 cleaner 'compress' option
blanchet
parents: 57780
diff changeset
   165
        val compress =
2bf99b3f62e1 cleaner 'compress' option
blanchet
parents: 57780
diff changeset
   166
          (case compress of
2bf99b3f62e1 cleaner 'compress' option
blanchet
parents: 57780
diff changeset
   167
            NONE => if isar_proofs = NONE andalso do_preplay then 1000.0 else 10.0
2bf99b3f62e1 cleaner 'compress' option
blanchet
parents: 57780
diff changeset
   168
          | SOME n => n)
55168
948e8b7ea82f correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents: 54838
diff changeset
   169
57288
ffd928316c75 supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents: 57287
diff changeset
   170
        fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem
58341
6c8b30b9f583 removed accidental '@{print}'
blanchet
parents: 58142
diff changeset
   171
        fun skolems_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev
55168
948e8b7ea82f correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents: 54838
diff changeset
   172
948e8b7ea82f correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents: 54838
diff changeset
   173
        fun get_role keep_role ((num, _), role, t, rule, _) =
948e8b7ea82f correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents: 54838
diff changeset
   174
          if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
948e8b7ea82f correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents: 54838
diff changeset
   175
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   176
        val atp_proof =
57791
blanchet
parents: 57787
diff changeset
   177
          fold_rev add_line_pass1 atp_proof0 []
57771
0265ccdb9e6f better duplicate detection
blanchet
parents: 57770
diff changeset
   178
          |> add_lines_pass2 []
54700
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   179
54535
59737a43e044 support Negated_Conjecture as a TPTP role as well (e.g. for SMT proofs)
blanchet
parents: 54507
diff changeset
   180
        val conjs =
54700
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   181
          map_filter (fn (name, role, _, _, _) =>
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   182
              if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE)
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   183
            atp_proof
54751
9b93f9117f8b implemented Z3 skolemization
blanchet
parents: 54750
diff changeset
   184
        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
   185
ffd928316c75 supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents: 57287
diff changeset
   186
        fun add_lemma ((l, t), rule) ctxt =
ffd928316c75 supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents: 57287
diff changeset
   187
          let
ffd928316c75 supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents: 57287
diff changeset
   188
            val (skos, meths) =
58077
f050a297c9c3 try 'skolem' method first for Z3
blanchet
parents: 58073
diff changeset
   189
              (if is_skolemize_rule rule then
f050a297c9c3 try 'skolem' method first for Z3
blanchet
parents: 58073
diff changeset
   190
                 (skolems_of ctxt t, skolem_methods_of (rule = z3_skolemize_rule))
f050a297c9c3 try 'skolem' method first for Z3
blanchet
parents: 58073
diff changeset
   191
               else if is_arith_rule rule then
f050a297c9c3 try 'skolem' method first for Z3
blanchet
parents: 58073
diff changeset
   192
                 ([], arith_methods)
f050a297c9c3 try 'skolem' method first for Z3
blanchet
parents: 58073
diff changeset
   193
               else
f050a297c9c3 try 'skolem' method first for Z3
blanchet
parents: 58073
diff changeset
   194
                 ([], rewrite_methods))
57288
ffd928316c75 supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents: 57287
diff changeset
   195
              ||> massage_methods
ffd928316c75 supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents: 57287
diff changeset
   196
          in
ffd928316c75 supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents: 57287
diff changeset
   197
            (Prove ([], skos, l, t, [], ([], []), meths, ""),
ffd928316c75 supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents: 57287
diff changeset
   198
             ctxt |> not (null skos) ? (Variable.add_fixes (map fst skos) #> snd))
ffd928316c75 supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents: 57287
diff changeset
   199
          end
ffd928316c75 supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents: 57287
diff changeset
   200
ffd928316c75 supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents: 57287
diff changeset
   201
        val (lems, _) =
ffd928316c75 supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents: 57287
diff changeset
   202
          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
   203
57791
blanchet
parents: 57787
diff changeset
   204
        val bot = #1 (List.last atp_proof)
54700
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   205
51145
280ece22765b tuned code
blanchet
parents: 51130
diff changeset
   206
        val refute_graph =
51212
2bbcc9cc12b4 ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents: 51208
diff changeset
   207
          atp_proof
2bbcc9cc12b4 ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents: 51208
diff changeset
   208
          |> map (fn (name, _, _, _, from) => (from, name))
2bbcc9cc12b4 ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents: 51208
diff changeset
   209
          |> make_refute_graph bot
2bbcc9cc12b4 ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents: 51208
diff changeset
   210
          |> fold (Atom_Graph.default_node o rpair ()) conjs
54700
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   211
51145
280ece22765b tuned code
blanchet
parents: 51130
diff changeset
   212
        val axioms = axioms_of_refute_graph refute_graph conjs
54700
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   213
51145
280ece22765b tuned code
blanchet
parents: 51130
diff changeset
   214
        val tainted = tainted_atoms_of_refute_graph refute_graph conjs
51156
cbb640c3d203 made check for conjecture skolemization sound
blanchet
parents: 51149
diff changeset
   215
        val is_clause_tainted = exists (member (op =) tainted)
50676
83b8a5a39709 generate "obtain" steps corresponding to skolemization inferences
blanchet
parents: 50675
diff changeset
   216
        val steps =
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   217
          Symtab.empty
51201
f176855a1ee2 tuning (removed redundant datatype)
blanchet
parents: 51200
diff changeset
   218
          |> fold (fn (name as (s, _), role, t, rule, _) =>
54758
ba488d89614a simplify generated propositions
blanchet
parents: 54757
diff changeset
   219
              Symtab.update_new (s, (rule, t
ba488d89614a simplify generated propositions
blanchet
parents: 54757
diff changeset
   220
                |> (if is_clause_tainted [name] then
54768
ee0881a54c72 fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
blanchet
parents: 54767
diff changeset
   221
                      HOLogic.dest_Trueprop
ee0881a54c72 fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
blanchet
parents: 54767
diff changeset
   222
                      #> role <> Conjecture ? s_not
54758
ba488d89614a simplify generated propositions
blanchet
parents: 54757
diff changeset
   223
                      #> fold exists_of (map Var (Term.add_vars t []))
54768
ee0881a54c72 fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
blanchet
parents: 54767
diff changeset
   224
                      #> HOLogic.mk_Trueprop
54758
ba488d89614a simplify generated propositions
blanchet
parents: 54757
diff changeset
   225
                    else
ba488d89614a simplify generated propositions
blanchet
parents: 54757
diff changeset
   226
                      I))))
ba488d89614a simplify generated propositions
blanchet
parents: 54757
diff changeset
   227
            atp_proof
54700
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   228
54755
2eb43ddde491 use 'arith' when appropriate in Z3 proofs
blanchet
parents: 54754
diff changeset
   229
        val rule_of_clause_id = fst o the o Symtab.lookup steps o fst
54700
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   230
57768
a63f14f1214c fine-tuned Isar reconstruction, esp. boolean simplifications
blanchet
parents: 57767
diff changeset
   231
        val finish_off = close_form #> rename_bound_vars
57765
f1108245ba11 better handling of variable names
blanchet
parents: 57763
diff changeset
   232
57767
5bc204ca27ce centralized boolean simplification so that e.g. LEO-II benefits from it
blanchet
parents: 57765
diff changeset
   233
        fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> finish_off
50016
0ae5328ded8c fixed more "Trueprop" issues
blanchet
parents: 50015
diff changeset
   234
          | prop_of_clause names =
50676
83b8a5a39709 generate "obtain" steps corresponding to skolemization inferences
blanchet
parents: 50675
diff changeset
   235
            let
57765
f1108245ba11 better handling of variable names
blanchet
parents: 57763
diff changeset
   236
              val lits =
f1108245ba11 better handling of variable names
blanchet
parents: 57763
diff changeset
   237
                map (HOLogic.dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names)
50676
83b8a5a39709 generate "obtain" steps corresponding to skolemization inferences
blanchet
parents: 50675
diff changeset
   238
            in
54754
6b0ca7f79e93 robustness in degenerate case + tuning
blanchet
parents: 54753
diff changeset
   239
              (case List.partition (can HOLogic.dest_not) lits of
50018
4ea26c74d7ea use implications rather than disjunctions to improve readability
blanchet
parents: 50017
diff changeset
   240
                (negs as _ :: _, pos as _ :: _) =>
54507
d983a020489d whitespace tuning
blanchet
parents: 54505
diff changeset
   241
                s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos)
54754
6b0ca7f79e93 robustness in degenerate case + tuning
blanchet
parents: 54753
diff changeset
   242
              | _ => fold (curry s_disj) lits @{term False})
50018
4ea26c74d7ea use implications rather than disjunctions to improve readability
blanchet
parents: 50017
diff changeset
   243
            end
57767
5bc204ca27ce centralized boolean simplification so that e.g. LEO-II benefits from it
blanchet
parents: 57765
diff changeset
   244
            |> HOLogic.mk_Trueprop |> finish_off
54700
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   245
58083
ca7ec8728348 removed show stuttering
blanchet
parents: 58077
diff changeset
   246
        fun maybe_show outer c = if outer andalso eq_set (op =) (c, conjs) then [Show] else []
54700
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   247
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   248
        fun isar_steps outer predecessor accum [] =
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   249
            accum
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   250
            |> (if tainted = [] then
58083
ca7ec8728348 removed show stuttering
blanchet
parents: 58077
diff changeset
   251
                  (* e.g., trivial, empty proof by Z3 *)
54700
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   252
                  cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
57776
1111a9a328fe rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents: 57771
diff changeset
   253
                    sort_facts (the_list predecessor, []), massage_methods systematic_methods', ""))
54700
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   254
                else
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   255
                  I)
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   256
            |> rev
54755
2eb43ddde491 use 'arith' when appropriate in Z3 proofs
blanchet
parents: 54754
diff changeset
   257
          | isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) =
54700
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   258
            let
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   259
              val l = label_of_clause c
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   260
              val t = prop_of_clause c
54755
2eb43ddde491 use 'arith' when appropriate in Z3 proofs
blanchet
parents: 54754
diff changeset
   261
              val rule = rule_of_clause_id id
2eb43ddde491 use 'arith' when appropriate in Z3 proofs
blanchet
parents: 54754
diff changeset
   262
              val skolem = is_skolemize_rule rule
2eb43ddde491 use 'arith' when appropriate in Z3 proofs
blanchet
parents: 54754
diff changeset
   263
57776
1111a9a328fe rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents: 57771
diff changeset
   264
              val deps = ([], [])
1111a9a328fe rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents: 57771
diff changeset
   265
                |> fold add_fact_of_dependencies gamma
1111a9a328fe rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents: 57771
diff changeset
   266
                |> sort_facts
55244
12e1a5d8ee48 simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents: 55223
diff changeset
   267
              val meths =
58077
f050a297c9c3 try 'skolem' method first for Z3
blanchet
parents: 58073
diff changeset
   268
                (if skolem then skolem_methods_of (rule = z3_skolemize_rule)
55273
e887c0743614 implemented new 'try0_isar' semantics
blanchet
parents: 55267
diff changeset
   269
                 else if is_arith_rule rule then arith_methods
e887c0743614 implemented new 'try0_isar' semantics
blanchet
parents: 55267
diff changeset
   270
                 else if is_datatype_rule rule then datatype_methods
57744
a68b8db8691d added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents: 57741
diff changeset
   271
                 else systematic_methods')
55311
2bb02ba5d4b7 rationalized lists of methods
blanchet
parents: 55310
diff changeset
   272
                |> massage_methods
55280
f0187a12b8f2 tuned data structure
blanchet
parents: 55279
diff changeset
   273
58083
ca7ec8728348 removed show stuttering
blanchet
parents: 58077
diff changeset
   274
              fun prove sub facts = Prove (maybe_show outer c, [], l, t, sub, facts, meths, "")
55280
f0187a12b8f2 tuned data structure
blanchet
parents: 55279
diff changeset
   275
              fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs
54700
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   276
            in
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   277
              if is_clause_tainted c then
54712
cbebe2cf77f1 more work on Z3 Isar proofs
blanchet
parents: 54700
diff changeset
   278
                (case gamma of
54700
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   279
                  [g] =>
54755
2eb43ddde491 use 'arith' when appropriate in Z3 proofs
blanchet
parents: 54754
diff changeset
   280
                  if skolem andalso is_clause_tainted g then
57758
b2e6166bf487 beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents: 57744
diff changeset
   281
                    (case skolems_of ctxt (prop_of_clause g) of
b2e6166bf487 beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents: 57744
diff changeset
   282
                      [] => steps_of_rest (prove [] deps)
b2e6166bf487 beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents: 57744
diff changeset
   283
                    | skos =>
b2e6166bf487 beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents: 57744
diff changeset
   284
                      let val subproof = Proof (skos, [], rev accum) in
b2e6166bf487 beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents: 57744
diff changeset
   285
                        isar_steps outer (SOME l) [prove [subproof] ([], [])] infs
b2e6166bf487 beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents: 57744
diff changeset
   286
                      end)
51148
2246a2e17f92 tuning -- refactoring in preparation for handling skolemization of conjecture
blanchet
parents: 51147
diff changeset
   287
                  else
55280
f0187a12b8f2 tuned data structure
blanchet
parents: 55279
diff changeset
   288
                    steps_of_rest (prove [] deps)
f0187a12b8f2 tuned data structure
blanchet
parents: 55279
diff changeset
   289
                | _ => steps_of_rest (prove [] deps))
54700
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   290
              else
57288
ffd928316c75 supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents: 57287
diff changeset
   291
                steps_of_rest
57758
b2e6166bf487 beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents: 57744
diff changeset
   292
                  (if skolem then
b2e6166bf487 beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents: 57744
diff changeset
   293
                     (case skolems_of ctxt t of
b2e6166bf487 beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents: 57744
diff changeset
   294
                       [] => prove [] deps
b2e6166bf487 beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents: 57744
diff changeset
   295
                     | skos => Prove ([], skos, l, t, [], deps, meths, ""))
b2e6166bf487 beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents: 57744
diff changeset
   296
                   else
b2e6166bf487 beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents: 57744
diff changeset
   297
                     prove [] deps)
54700
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   298
            end
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   299
          | isar_steps outer predecessor accum (Cases cases :: infs) =
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   300
            let
55186
fafdf2424c57 don't forget the last inference(s) after conjecture skolemization
blanchet
parents: 55184
diff changeset
   301
              fun isar_case (c, subinfs) =
fafdf2424c57 don't forget the last inference(s) after conjecture skolemization
blanchet
parents: 55184
diff changeset
   302
                isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs
54700
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   303
              val c = succedent_of_cases cases
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   304
              val l = label_of_clause c
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   305
              val t = prop_of_clause c
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   306
              val step =
58083
ca7ec8728348 removed show stuttering
blanchet
parents: 58077
diff changeset
   307
                Prove (maybe_show outer c, [], l, t,
54760
a1ac3eaa0d11 generate proper succedent for cases with trivial branches
blanchet
parents: 54759
diff changeset
   308
                  map isar_case (filter_out (null o snd) cases),
57776
1111a9a328fe rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents: 57771
diff changeset
   309
                  sort_facts (the_list predecessor, []), massage_methods systematic_methods', "")
54700
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   310
            in
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   311
              isar_steps outer (SOME l) (step :: accum) infs
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   312
            end
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   313
        and isar_proof outer fix assms lems infs =
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   314
          Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
64177ce0a7bd adapted code for Z3 proof reconstruction
blanchet
parents: 54699
diff changeset
   315
55222
a4ef6eb1fc20 added a 'trace' option
blanchet
parents: 55220
diff changeset
   316
        val trace = Config.get ctxt trace
55214
48a347b40629 better tracing + syntactically correct 'metis' calls
blanchet
parents: 55213
diff changeset
   317
55256
6c317e374614 refactored data structure (step 3)
blanchet
parents: 55253
diff changeset
   318
        val canonical_isar_proof =
51145
280ece22765b tuned code
blanchet
parents: 51130
diff changeset
   319
          refute_graph
55214
48a347b40629 better tracing + syntactically correct 'metis' calls
blanchet
parents: 55213
diff changeset
   320
          |> trace ? tap (tracing o prefix "Refute graph: " o string_of_refute_graph)
51031
63d71b247323 more robustness in Isar proof reconstruction (cf. bug report by Ondrej)
blanchet
parents: 51026
diff changeset
   321
          |> redirect_graph axioms tainted bot
55214
48a347b40629 better tracing + syntactically correct 'metis' calls
blanchet
parents: 55213
diff changeset
   322
          |> trace ? tap (tracing o prefix "Direct proof: " o string_of_direct_proof)
54754
6b0ca7f79e93 robustness in degenerate case + tuning
blanchet
parents: 54753
diff changeset
   323
          |> isar_proof true params assms lems
58083
ca7ec8728348 removed show stuttering
blanchet
parents: 58077
diff changeset
   324
          |> postprocess_isar_proof_remove_show_stuttering
55213
dcb36a2540bc tuned ML function names
blanchet
parents: 55212
diff changeset
   325
          |> postprocess_isar_proof_remove_unreferenced_steps I
dcb36a2540bc tuned ML function names
blanchet
parents: 55212
diff changeset
   326
          |> relabel_isar_proof_canonically
55214
48a347b40629 better tracing + syntactically correct 'metis' calls
blanchet
parents: 55213
diff changeset
   327
55286
blanchet
parents: 55285
diff changeset
   328
        val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof
55256
6c317e374614 refactored data structure (step 3)
blanchet
parents: 55253
diff changeset
   329
55260
ada3ae6458d4 more data structure rationalization
blanchet
parents: 55258
diff changeset
   330
        val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
ada3ae6458d4 more data structure rationalization
blanchet
parents: 55258
diff changeset
   331
55264
43473497fb65 centralize preplaying
blanchet
parents: 55263
diff changeset
   332
        val _ = fold_isar_steps (fn meth =>
57054
blanchet
parents: 56985
diff changeset
   333
            K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth []))
55260
ada3ae6458d4 more data structure rationalization
blanchet
parents: 55258
diff changeset
   334
          (steps_of_isar_proof canonical_isar_proof) ()
55214
48a347b40629 better tracing + syntactically correct 'metis' calls
blanchet
parents: 55213
diff changeset
   335
55223
3c593bad6b31 generalized preplaying infrastructure to store various results for various methods
blanchet
parents: 55222
diff changeset
   336
        fun str_of_preplay_outcome outcome =
3c593bad6b31 generalized preplaying infrastructure to store various results for various methods
blanchet
parents: 55222
diff changeset
   337
          if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
3c593bad6b31 generalized preplaying infrastructure to store various results for various methods
blanchet
parents: 55222
diff changeset
   338
        fun str_of_meth l meth =
56985
82c83978fbd9 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents: 56983
diff changeset
   339
          string_of_proof_method ctxt [] meth ^ " " ^
55266
d9d31354834e centralize more preplaying
blanchet
parents: 55264
diff changeset
   340
          str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)
55244
12e1a5d8ee48 simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents: 55223
diff changeset
   341
        fun comment_of l = map (str_of_meth l) #> commas
55222
a4ef6eb1fc20 added a 'trace' option
blanchet
parents: 55220
diff changeset
   342
55214
48a347b40629 better tracing + syntactically correct 'metis' calls
blanchet
parents: 55213
diff changeset
   343
        fun trace_isar_proof label proof =
48a347b40629 better tracing + syntactically correct 'metis' calls
blanchet
parents: 55213
diff changeset
   344
          if trace then
55299
c3bb1cffce26 generate comments in Isar proofs
blanchet
parents: 55297
diff changeset
   345
            tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^
56097
blanchet
parents: 56093
diff changeset
   346
              string_of_isar_proof ctxt subgoal subgoal_count
blanchet
parents: 56093
diff changeset
   347
                (comment_isar_proof comment_of proof) ^ "\n")
55214
48a347b40629 better tracing + syntactically correct 'metis' calls
blanchet
parents: 55213
diff changeset
   348
          else
48a347b40629 better tracing + syntactically correct 'metis' calls
blanchet
parents: 55213
diff changeset
   349
            ()
54754
6b0ca7f79e93 robustness in degenerate case + tuning
blanchet
parents: 54753
diff changeset
   350
55299
c3bb1cffce26 generate comments in Isar proofs
blanchet
parents: 55297
diff changeset
   351
        fun comment_of l (meth :: _) =
c3bb1cffce26 generate comments in Isar proofs
blanchet
parents: 55297
diff changeset
   352
          (case (verbose,
c3bb1cffce26 generate comments in Isar proofs
blanchet
parents: 55297
diff changeset
   353
              Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)) of
c3bb1cffce26 generate comments in Isar proofs
blanchet
parents: 55297
diff changeset
   354
            (false, Played _) => ""
c3bb1cffce26 generate comments in Isar proofs
blanchet
parents: 55297
diff changeset
   355
          | (_, outcome) => string_of_play_outcome outcome)
c3bb1cffce26 generate comments in Isar proofs
blanchet
parents: 55297
diff changeset
   356
54828
b2271ad695db don't do 'isar_try0' if preplaying is off
blanchet
parents: 54827
diff changeset
   357
        val (play_outcome, isar_proof) =
55256
6c317e374614 refactored data structure (step 3)
blanchet
parents: 55253
diff changeset
   358
          canonical_isar_proof
55214
48a347b40629 better tracing + syntactically correct 'metis' calls
blanchet
parents: 55213
diff changeset
   359
          |> tap (trace_isar_proof "Original")
57245
f6bf6d5341ee renamed Sledgehammer options
blanchet
parents: 57154
diff changeset
   360
          |> compress_isar_proof ctxt compress preplay_timeout preplay_data
55214
48a347b40629 better tracing + syntactically correct 'metis' calls
blanchet
parents: 55213
diff changeset
   361
          |> tap (trace_isar_proof "Compressed")
55213
dcb36a2540bc tuned ML function names
blanchet
parents: 55212
diff changeset
   362
          |> postprocess_isar_proof_remove_unreferenced_steps
55266
d9d31354834e centralize more preplaying
blanchet
parents: 55264
diff changeset
   363
               (keep_fastest_method_of_isar_step (!preplay_data)
57054
blanchet
parents: 56985
diff changeset
   364
                #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
55214
48a347b40629 better tracing + syntactically correct 'metis' calls
blanchet
parents: 55213
diff changeset
   365
          |> tap (trace_isar_proof "Minimized")
55260
ada3ae6458d4 more data structure rationalization
blanchet
parents: 55258
diff changeset
   366
          |> `(preplay_outcome_of_isar_proof (!preplay_data))
55325
462ffd3b7065 tuned code
blanchet
parents: 55323
diff changeset
   367
          ||> (comment_isar_proof comment_of
462ffd3b7065 tuned code
blanchet
parents: 55323
diff changeset
   368
               #> chain_isar_proof
462ffd3b7065 tuned code
blanchet
parents: 55323
diff changeset
   369
               #> kill_useless_labels_in_isar_proof
57792
9cb24c835284 rationalize Skolem names
blanchet
parents: 57791
diff changeset
   370
               #> relabel_isar_proof_nicely
9cb24c835284 rationalize Skolem names
blanchet
parents: 57791
diff changeset
   371
               #> rationalize_obtains_in_isar_proofs ctxt)
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   372
      in
57287
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   373
        (case add_isar_steps (steps_of_isar_proof isar_proof) 0 of
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   374
          1 =>
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   375
          one_line_proof_text ctxt 0
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   376
            (if play_outcome_ord (play_outcome, one_line_play) = LESS then
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   377
               (case isar_proof of
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   378
                 Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) =>
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   379
                 let val used_facts' = filter (member (op =) gfs o fst) used_facts in
57739
blanchet
parents: 57735
diff changeset
   380
                   ((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count)
57287
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   381
                 end)
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   382
             else
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   383
               one_line_params) ^
57780
e1a3d025552d tuned terminology (cf. 'isar_proofs' option)
blanchet
parents: 57776
diff changeset
   384
          (if isar_proofs = SOME true then "\n(No Isar proof available.)"
57287
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   385
           else "")
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   386
        | num_steps =>
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   387
          let
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   388
            val msg =
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   389
              (if verbose then [string_of_int num_steps ^ " step" ^ plural_s num_steps] else []) @
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   390
              (if do_preplay then [string_of_play_outcome play_outcome] else [])
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   391
          in
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   392
            one_line_proof_text ctxt 0 one_line_params ^
57780
e1a3d025552d tuned terminology (cf. 'isar_proofs' option)
blanchet
parents: 57776
diff changeset
   393
            "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
57287
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   394
            Active.sendback_markup [Markup.padding_command]
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   395
              (string_of_isar_proof ctxt subgoal subgoal_count isar_proof)
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   396
          end)
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   397
      end
57056
8b2283566f6e properly reconstruct helpers in Z3 proofs
blanchet
parents: 57054
diff changeset
   398
  in
57287
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   399
    if debug then
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   400
      generate_proof_text ()
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   401
    else
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   402
      (case try generate_proof_text () of
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   403
        SOME s => s
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   404
      | NONE =>
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   405
        one_line_proof_text ctxt 0 one_line_params ^
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57286
diff changeset
   406
        (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
   407
  end
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   408
55297
1dfcd49f5dcb renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents: 55296
diff changeset
   409
fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =
54824
4e58a38b330b refactored preplaying outcome data structure
blanchet
parents: 54823
diff changeset
   410
  (case play of
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57792
diff changeset
   411
    Played _ => meth = SMT_Method andalso smt_proofs <> SOME true
56093
4eeb73a1feec simplified preplaying information
blanchet
parents: 56081
diff changeset
   412
  | Play_Timed_Out time => Time.> (time, Time.zeroTime)
4eeb73a1feec simplified preplaying information
blanchet
parents: 56081
diff changeset
   413
  | 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
   414
55297
1dfcd49f5dcb renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents: 55296
diff changeset
   415
fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
57739
blanchet
parents: 57735
diff changeset
   416
    (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
   417
  (if isar_proofs = SOME true orelse
55297
1dfcd49f5dcb renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents: 55296
diff changeset
   418
      (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt_proofs preplay) then
1dfcd49f5dcb renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents: 55296
diff changeset
   419
     isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   420
   else
56985
82c83978fbd9 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents: 56983
diff changeset
   421
     one_line_proof_text ctxt num_chained) one_line_params
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   422
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   423
end;