src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
author blanchet
Sun, 03 May 2015 22:15:29 +0200
changeset 60252 2c468c062589
parent 59058 a78612c67ec0
child 60305 7d278b0617d3
permissions -rw-r--r--
improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55287
ffa306239316 renamed ML file
blanchet
parents: 55286
diff changeset
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
52555
6811291d1869 moved code -> easier debugging
smolkas
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
6811291d1869 moved code -> easier debugging
smolkas
parents:
diff changeset
     3
    Author:     Steffen Juilf Smolka, TU Muenchen
6811291d1869 moved code -> easier debugging
smolkas
parents:
diff changeset
     4
6811291d1869 moved code -> easier debugging
smolkas
parents:
diff changeset
     5
Reconstructors.
6811291d1869 moved code -> easier debugging
smolkas
parents:
diff changeset
     6
*)
6811291d1869 moved code -> easier debugging
smolkas
parents:
diff changeset
     7
55287
ffa306239316 renamed ML file
blanchet
parents: 55286
diff changeset
     8
signature SLEDGEHAMMER_PROOF_METHODS =
52555
6811291d1869 moved code -> easier debugging
smolkas
parents:
diff changeset
     9
sig
6811291d1869 moved code -> easier debugging
smolkas
parents:
diff changeset
    10
  type stature = ATP_Problem_Generate.stature
6811291d1869 moved code -> easier debugging
smolkas
parents:
diff changeset
    11
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55269
diff changeset
    12
  datatype proof_method =
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55269
diff changeset
    13
    Metis_Method of string option * string option |
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55269
diff changeset
    14
    Meson_Method |
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57948
diff changeset
    15
    SMT_Method |
56852
b38c5b9cf590 added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0')
blanchet
parents: 56093
diff changeset
    16
    SATx_Method |
55323
253a029335a2 split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents: 55315
diff changeset
    17
    Blast_Method |
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55269
diff changeset
    18
    Simp_Method |
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55269
diff changeset
    19
    Simp_Size_Method |
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55269
diff changeset
    20
    Auto_Method |
58092
4ae52c60603a renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents: 58075
diff changeset
    21
    Fastforce_Method |
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55269
diff changeset
    22
    Force_Method |
58092
4ae52c60603a renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents: 58075
diff changeset
    23
    Moura_Method |
55323
253a029335a2 split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents: 55315
diff changeset
    24
    Linarith_Method |
253a029335a2 split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents: 55315
diff changeset
    25
    Presburger_Method |
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55269
diff changeset
    26
    Algebra_Method
52555
6811291d1869 moved code -> easier debugging
smolkas
parents:
diff changeset
    27
54824
4e58a38b330b refactored preplaying outcome data structure
blanchet
parents: 54823
diff changeset
    28
  datatype play_outcome =
4e58a38b330b refactored preplaying outcome data structure
blanchet
parents: 54823
diff changeset
    29
    Played of Time.time |
4e58a38b330b refactored preplaying outcome data structure
blanchet
parents: 54823
diff changeset
    30
    Play_Timed_Out of Time.time |
56093
4eeb73a1feec simplified preplaying information
blanchet
parents: 56081
diff changeset
    31
    Play_Failed
52555
6811291d1869 moved code -> easier debugging
smolkas
parents:
diff changeset
    32
54824
4e58a38b330b refactored preplaying outcome data structure
blanchet
parents: 54823
diff changeset
    33
  type one_line_params =
57739
blanchet
parents: 57735
diff changeset
    34
    ((string * stature) list * (proof_method * play_outcome)) * string * int * int
52555
6811291d1869 moved code -> easier debugging
smolkas
parents:
diff changeset
    35
57287
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57054
diff changeset
    36
  val is_proof_method_direct : proof_method -> bool
60252
2c468c062589 improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents: 59058
diff changeset
    37
  val proof_method_distinguishes_chained_and_direct : proof_method -> bool
56985
82c83978fbd9 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents: 56983
diff changeset
    38
  val string_of_proof_method : Proof.context -> string list -> proof_method -> string
57054
blanchet
parents: 56985
diff changeset
    39
  val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
57720
9df2757f5bec tuned ML function name
blanchet
parents: 57675
diff changeset
    40
  val thms_influence_proof_method : Proof.context -> proof_method -> thm list -> bool
55211
5d027af93a08 moved ML code around
blanchet
parents: 55180
diff changeset
    41
  val string_of_play_outcome : play_outcome -> string
55269
aae87746f412 more thorough, hybrid compression
blanchet
parents: 55212
diff changeset
    42
  val play_outcome_ord : play_outcome * play_outcome -> order
56985
82c83978fbd9 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents: 56983
diff changeset
    43
  val one_line_proof_text : Proof.context -> int -> one_line_params -> string
54495
237d5be57277 refactored
blanchet
parents: 52590
diff changeset
    44
end;
52555
6811291d1869 moved code -> easier debugging
smolkas
parents:
diff changeset
    45
55287
ffa306239316 renamed ML file
blanchet
parents: 55286
diff changeset
    46
structure Sledgehammer_Proof_Methods : SLEDGEHAMMER_PROOF_METHODS =
52555
6811291d1869 moved code -> easier debugging
smolkas
parents:
diff changeset
    47
struct
6811291d1869 moved code -> easier debugging
smolkas
parents:
diff changeset
    48
54828
b2271ad695db don't do 'isar_try0' if preplaying is off
blanchet
parents: 54824
diff changeset
    49
open ATP_Util
52555
6811291d1869 moved code -> easier debugging
smolkas
parents:
diff changeset
    50
open ATP_Problem_Generate
55211
5d027af93a08 moved ML code around
blanchet
parents: 55180
diff changeset
    51
open ATP_Proof_Reconstruct
52555
6811291d1869 moved code -> easier debugging
smolkas
parents:
diff changeset
    52
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55269
diff changeset
    53
datatype proof_method =
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55269
diff changeset
    54
  Metis_Method of string option * string option |
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55269
diff changeset
    55
  Meson_Method |
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57948
diff changeset
    56
  SMT_Method |
56852
b38c5b9cf590 added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0')
blanchet
parents: 56093
diff changeset
    57
  SATx_Method |
55323
253a029335a2 split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents: 55315
diff changeset
    58
  Blast_Method |
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55269
diff changeset
    59
  Simp_Method |
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55269
diff changeset
    60
  Simp_Size_Method |
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55269
diff changeset
    61
  Auto_Method |
58092
4ae52c60603a renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents: 58075
diff changeset
    62
  Fastforce_Method |
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55269
diff changeset
    63
  Force_Method |
58092
4ae52c60603a renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents: 58075
diff changeset
    64
  Moura_Method |
55323
253a029335a2 split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents: 55315
diff changeset
    65
  Linarith_Method |
253a029335a2 split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents: 55315
diff changeset
    66
  Presburger_Method |
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55269
diff changeset
    67
  Algebra_Method
52555
6811291d1869 moved code -> easier debugging
smolkas
parents:
diff changeset
    68
54824
4e58a38b330b refactored preplaying outcome data structure
blanchet
parents: 54823
diff changeset
    69
datatype play_outcome =
4e58a38b330b refactored preplaying outcome data structure
blanchet
parents: 54823
diff changeset
    70
  Played of Time.time |
4e58a38b330b refactored preplaying outcome data structure
blanchet
parents: 54823
diff changeset
    71
  Play_Timed_Out of Time.time |
56093
4eeb73a1feec simplified preplaying information
blanchet
parents: 56081
diff changeset
    72
  Play_Failed
52555
6811291d1869 moved code -> easier debugging
smolkas
parents:
diff changeset
    73
57739
blanchet
parents: 57735
diff changeset
    74
type one_line_params =
blanchet
parents: 57735
diff changeset
    75
  ((string * stature) list * (proof_method * play_outcome)) * string * int * int
55211
5d027af93a08 moved ML code around
blanchet
parents: 55180
diff changeset
    76
57287
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57054
diff changeset
    77
fun is_proof_method_direct (Metis_Method _) = true
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57054
diff changeset
    78
  | is_proof_method_direct Meson_Method = true
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57948
diff changeset
    79
  | is_proof_method_direct SMT_Method = true
57287
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57054
diff changeset
    80
  | is_proof_method_direct Simp_Method = true
57465
ed826e2053c9 fine-tuned methods
blanchet
parents: 57290
diff changeset
    81
  | is_proof_method_direct Simp_Size_Method = true
57287
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57054
diff changeset
    82
  | is_proof_method_direct _ = false
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57054
diff changeset
    83
60252
2c468c062589 improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents: 59058
diff changeset
    84
fun proof_method_distinguishes_chained_and_direct Simp_Method = true
2c468c062589 improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents: 59058
diff changeset
    85
  | proof_method_distinguishes_chained_and_direct Simp_Size_Method = true
2c468c062589 improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents: 59058
diff changeset
    86
  | proof_method_distinguishes_chained_and_direct _ = false
2c468c062589 improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents: 59058
diff changeset
    87
58499
094efe6ac459 don't affect other subgoals with 'auto' in one-liner proofs
blanchet
parents: 58092
diff changeset
    88
fun is_proof_method_multi_goal Auto_Method = true
094efe6ac459 don't affect other subgoals with 'auto' in one-liner proofs
blanchet
parents: 58092
diff changeset
    89
  | is_proof_method_multi_goal _ = false
094efe6ac459 don't affect other subgoals with 'auto' in one-liner proofs
blanchet
parents: 58092
diff changeset
    90
56983
132142089ea6 use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents: 56965
diff changeset
    91
fun maybe_paren s = s |> not (Symbol_Pos.is_identifier s) ? enclose "(" ")"
132142089ea6 use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents: 56965
diff changeset
    92
56985
82c83978fbd9 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents: 56983
diff changeset
    93
fun string_of_proof_method ctxt ss meth =
56983
132142089ea6 use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents: 56965
diff changeset
    94
  let
132142089ea6 use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents: 56965
diff changeset
    95
    val meth_s =
132142089ea6 use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents: 56965
diff changeset
    96
      (case meth of
132142089ea6 use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents: 56965
diff changeset
    97
        Metis_Method (NONE, NONE) => "metis"
132142089ea6 use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents: 56965
diff changeset
    98
      | Metis_Method (type_enc_opt, lam_trans_opt) =>
132142089ea6 use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents: 56965
diff changeset
    99
        "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
132142089ea6 use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents: 56965
diff changeset
   100
      | Meson_Method => "meson"
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57948
diff changeset
   101
      | SMT_Method => "smt"
56983
132142089ea6 use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents: 56965
diff changeset
   102
      | SATx_Method => "satx"
132142089ea6 use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents: 56965
diff changeset
   103
      | Blast_Method => "blast"
132142089ea6 use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents: 56965
diff changeset
   104
      | Simp_Method => if null ss then "simp" else "simp add:"
56985
82c83978fbd9 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents: 56983
diff changeset
   105
      | Simp_Size_Method => "simp add: " ^ short_thm_name ctxt @{thm size_ne_size_imp_ne}
56983
132142089ea6 use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents: 56965
diff changeset
   106
      | Auto_Method => "auto"
58092
4ae52c60603a renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents: 58075
diff changeset
   107
      | Fastforce_Method => "fastforce"
56983
132142089ea6 use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents: 56965
diff changeset
   108
      | Force_Method => "force"
58092
4ae52c60603a renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents: 58075
diff changeset
   109
      | Moura_Method => "moura"
56983
132142089ea6 use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents: 56965
diff changeset
   110
      | Linarith_Method => "linarith"
132142089ea6 use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents: 56965
diff changeset
   111
      | Presburger_Method => "presburger"
132142089ea6 use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents: 56965
diff changeset
   112
      | Algebra_Method => "algebra")
132142089ea6 use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents: 56965
diff changeset
   113
  in
132142089ea6 use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents: 56965
diff changeset
   114
    maybe_paren (space_implode " " (meth_s :: ss))
132142089ea6 use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents: 56965
diff changeset
   115
  end
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55269
diff changeset
   116
57054
blanchet
parents: 56985
diff changeset
   117
fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
56965
222f46a4dbec new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents: 56951
diff changeset
   118
  Method.insert_tac local_facts THEN'
222f46a4dbec new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents: 56951
diff changeset
   119
  (case meth of
222f46a4dbec new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents: 56951
diff changeset
   120
    Metis_Method (type_enc_opt, lam_trans_opt) =>
57290
bc06471cb7b7 move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents: 57287
diff changeset
   121
    let val ctxt = Config.put Metis_Tactic.verbose false ctxt in
bc06471cb7b7 move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents: 57287
diff changeset
   122
      Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)]
bc06471cb7b7 move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents: 57287
diff changeset
   123
        (lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts
bc06471cb7b7 move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents: 57287
diff changeset
   124
    end
58075
95bab16eac45 going back to bc06471cb7b7 for silencing -- the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
blanchet
parents: 58074
diff changeset
   125
  | Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts
95bab16eac45 going back to bc06471cb7b7 for silencing -- the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
blanchet
parents: 58074
diff changeset
   126
  | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
95bab16eac45 going back to bc06471cb7b7 for silencing -- the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
blanchet
parents: 58074
diff changeset
   127
  | Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts)
57465
ed826e2053c9 fine-tuned methods
blanchet
parents: 57290
diff changeset
   128
  | Simp_Size_Method =>
58075
95bab16eac45 going back to bc06471cb7b7 for silencing -- the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
blanchet
parents: 58074
diff changeset
   129
    Simplifier.asm_full_simp_tac (ctxt addsimps (@{thm size_ne_size_imp_ne} :: global_facts))
56965
222f46a4dbec new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents: 56951
diff changeset
   130
  | _ =>
222f46a4dbec new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents: 56951
diff changeset
   131
    Method.insert_tac global_facts THEN'
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55269
diff changeset
   132
    (case meth of
56965
222f46a4dbec new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents: 56951
diff changeset
   133
      SATx_Method => SAT.satx_tac ctxt
222f46a4dbec new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents: 56951
diff changeset
   134
    | Blast_Method => blast_tac ctxt
58075
95bab16eac45 going back to bc06471cb7b7 for silencing -- the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
blanchet
parents: 58074
diff changeset
   135
    | Auto_Method => SELECT_GOAL (Clasimp.auto_tac ctxt)
58092
4ae52c60603a renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents: 58075
diff changeset
   136
    | Fastforce_Method => Clasimp.fast_force_tac ctxt
58075
95bab16eac45 going back to bc06471cb7b7 for silencing -- the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
blanchet
parents: 58074
diff changeset
   137
    | Force_Method => Clasimp.force_tac ctxt
58092
4ae52c60603a renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents: 58075
diff changeset
   138
    | Moura_Method => moura_tac ctxt
57290
bc06471cb7b7 move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents: 57287
diff changeset
   139
    | Linarith_Method =>
bc06471cb7b7 move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents: 57287
diff changeset
   140
      let val ctxt = Config.put Lin_Arith.verbose false ctxt in Lin_Arith.tac ctxt end
56965
222f46a4dbec new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents: 56951
diff changeset
   141
    | Presburger_Method => Cooper.tac true [] [] ctxt
222f46a4dbec new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents: 56951
diff changeset
   142
    | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
55211
5d027af93a08 moved ML code around
blanchet
parents: 55180
diff changeset
   143
58092
4ae52c60603a renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents: 58075
diff changeset
   144
val simp_based_methods = [Simp_Method, Simp_Size_Method, Auto_Method, Force_Method, Moura_Method]
57675
47336af5d2b2 faster minimization by not adding facts that are already in the simpset
blanchet
parents: 57674
diff changeset
   145
57720
9df2757f5bec tuned ML function name
blanchet
parents: 57675
diff changeset
   146
fun thms_influence_proof_method ctxt meth ths =
57675
47336af5d2b2 faster minimization by not adding facts that are already in the simpset
blanchet
parents: 57674
diff changeset
   147
  not (member (op =) simp_based_methods meth) orelse
58075
95bab16eac45 going back to bc06471cb7b7 for silencing -- the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
blanchet
parents: 58074
diff changeset
   148
  (* unfortunate pointer comparison -- but it's always safe to consider a theorem useful *)
95bab16eac45 going back to bc06471cb7b7 for silencing -- the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
blanchet
parents: 58074
diff changeset
   149
  not (pointer_eq (ctxt addsimps ths, ctxt))
57675
47336af5d2b2 faster minimization by not adding facts that are already in the simpset
blanchet
parents: 57674
diff changeset
   150
54828
b2271ad695db don't do 'isar_try0' if preplaying is off
blanchet
parents: 54824
diff changeset
   151
fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
56093
4eeb73a1feec simplified preplaying information
blanchet
parents: 56081
diff changeset
   152
  | string_of_play_outcome (Play_Timed_Out time) =
4eeb73a1feec simplified preplaying information
blanchet
parents: 56081
diff changeset
   153
    if time = Time.zeroTime then "" else string_of_ext_time (true, time) ^ ", timed out"
54828
b2271ad695db don't do 'isar_try0' if preplaying is off
blanchet
parents: 54824
diff changeset
   154
  | string_of_play_outcome Play_Failed = "failed"
b2271ad695db don't do 'isar_try0' if preplaying is off
blanchet
parents: 54824
diff changeset
   155
55269
aae87746f412 more thorough, hybrid compression
blanchet
parents: 55212
diff changeset
   156
fun play_outcome_ord (Played time1, Played time2) =
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58499
diff changeset
   157
    int_ord (apply2 Time.toMilliseconds (time1, time2))
55269
aae87746f412 more thorough, hybrid compression
blanchet
parents: 55212
diff changeset
   158
  | play_outcome_ord (Played _, _) = LESS
aae87746f412 more thorough, hybrid compression
blanchet
parents: 55212
diff changeset
   159
  | play_outcome_ord (_, Played _) = GREATER
aae87746f412 more thorough, hybrid compression
blanchet
parents: 55212
diff changeset
   160
  | play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) =
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58499
diff changeset
   161
    int_ord (apply2 Time.toMilliseconds (time1, time2))
55269
aae87746f412 more thorough, hybrid compression
blanchet
parents: 55212
diff changeset
   162
  | play_outcome_ord (Play_Timed_Out _, _) = LESS
aae87746f412 more thorough, hybrid compression
blanchet
parents: 55212
diff changeset
   163
  | play_outcome_ord (_, Play_Timed_Out _) = GREATER
aae87746f412 more thorough, hybrid compression
blanchet
parents: 55212
diff changeset
   164
  | play_outcome_ord (Play_Failed, Play_Failed) = EQUAL
aae87746f412 more thorough, hybrid compression
blanchet
parents: 55212
diff changeset
   165
55211
5d027af93a08 moved ML code around
blanchet
parents: 55180
diff changeset
   166
fun apply_on_subgoal _ 1 = "by "
5d027af93a08 moved ML code around
blanchet
parents: 55180
diff changeset
   167
  | apply_on_subgoal 1 _ = "apply "
57287
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57054
diff changeset
   168
  | apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
55211
5d027af93a08 moved ML code around
blanchet
parents: 55180
diff changeset
   169
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55269
diff changeset
   170
(* FIXME *)
60252
2c468c062589 improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents: 59058
diff changeset
   171
fun proof_method_command ctxt meth i n used_chaineds _(*num_chained*) extras =
2c468c062589 improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents: 59058
diff changeset
   172
  let
2c468c062589 improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents: 59058
diff changeset
   173
    val (indirect_ss, direct_ss) =
2c468c062589 improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents: 59058
diff changeset
   174
      if is_proof_method_direct meth then
2c468c062589 improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents: 59058
diff changeset
   175
        ([], extras |> proof_method_distinguishes_chained_and_direct meth ? append used_chaineds)
2c468c062589 improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents: 59058
diff changeset
   176
      else
2c468c062589 improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents: 59058
diff changeset
   177
        (extras, [])
2c468c062589 improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents: 59058
diff changeset
   178
  in
57287
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57054
diff changeset
   179
    (if null indirect_ss then "" else "using " ^ space_implode " " indirect_ss ^ " ") ^
58499
094efe6ac459 don't affect other subgoals with 'auto' in one-liner proofs
blanchet
parents: 58092
diff changeset
   180
    apply_on_subgoal i n ^ string_of_proof_method ctxt direct_ss meth ^
094efe6ac459 don't affect other subgoals with 'auto' in one-liner proofs
blanchet
parents: 58092
diff changeset
   181
    (if is_proof_method_multi_goal meth andalso n <> 1 then "[1]" else "")
57287
68aa585269ac given two one-liners, only show the best of the two
blanchet
parents: 57054
diff changeset
   182
  end
55211
5d027af93a08 moved ML code around
blanchet
parents: 55180
diff changeset
   183
56093
4eeb73a1feec simplified preplaying information
blanchet
parents: 56081
diff changeset
   184
fun try_command_line banner play command =
4eeb73a1feec simplified preplaying information
blanchet
parents: 56081
diff changeset
   185
  let val s = string_of_play_outcome play in
4eeb73a1feec simplified preplaying information
blanchet
parents: 56081
diff changeset
   186
    banner ^ ": " ^ Active.sendback_markup [Markup.padding_command] command ^
4eeb73a1feec simplified preplaying information
blanchet
parents: 56081
diff changeset
   187
    (s |> s <> "" ? enclose " (" ")") ^ "."
4eeb73a1feec simplified preplaying information
blanchet
parents: 56081
diff changeset
   188
  end
52555
6811291d1869 moved code -> easier debugging
smolkas
parents:
diff changeset
   189
56985
82c83978fbd9 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents: 56983
diff changeset
   190
fun one_line_proof_text ctxt num_chained
57739
blanchet
parents: 57735
diff changeset
   191
    ((used_facts, (meth, play)), banner, subgoal, subgoal_count) =
57777
563df8185d98 more informative preplay failures
blanchet
parents: 57776
diff changeset
   192
  let val (chained, extra) = List.partition (fn (_, (sc, _)) => sc = Chained) used_facts in
57735
056a55b44ec7 eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents: 57720
diff changeset
   193
    map fst extra
056a55b44ec7 eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents: 57720
diff changeset
   194
    |> proof_method_command ctxt meth subgoal subgoal_count (map fst chained) num_chained
056a55b44ec7 eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents: 57720
diff changeset
   195
    |> (if play = Play_Failed then enclose "One-line proof reconstruction failed: " "."
056a55b44ec7 eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents: 57720
diff changeset
   196
        else try_command_line banner play)
55211
5d027af93a08 moved ML code around
blanchet
parents: 55180
diff changeset
   197
  end
52555
6811291d1869 moved code -> easier debugging
smolkas
parents:
diff changeset
   198
54495
237d5be57277 refactored
blanchet
parents: 52590
diff changeset
   199
end;