author | wenzelm |
Fri, 04 Jan 2019 23:22:53 +0100 | |
changeset 69593 | 3dda49e08b9d |
parent 63692 | 1bc4bc2c9fd1 |
child 70586 | 57df8a85317a |
permissions | -rw-r--r-- |
55287 | 1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML |
52555 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
3 |
Author: Steffen Juilf Smolka, TU Muenchen |
|
4 |
||
5 |
Reconstructors. |
|
6 |
*) |
|
7 |
||
55287 | 8 |
signature SLEDGEHAMMER_PROOF_METHODS = |
52555 | 9 |
sig |
10 |
type stature = ATP_Problem_Generate.stature |
|
11 |
||
55285 | 12 |
datatype proof_method = |
13 |
Metis_Method of string option * string option | |
|
14 |
Meson_Method | |
|
58061 | 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 | 18 |
Simp_Method | |
19 |
Simp_Size_Method | |
|
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 | 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 | 26 |
Algebra_Method |
52555 | 27 |
|
54824 | 28 |
datatype play_outcome = |
29 |
Played of Time.time | |
|
30 |
Play_Timed_Out of Time.time | |
|
56093 | 31 |
Play_Failed |
52555 | 32 |
|
54824 | 33 |
type one_line_params = |
57739 | 34 |
((string * stature) list * (proof_method * play_outcome)) * string * int * int |
52555 | 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 | 39 |
val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic |
55211 | 40 |
val string_of_play_outcome : play_outcome -> string |
55269 | 41 |
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
|
42 |
val one_line_proof_text : Proof.context -> int -> one_line_params -> string |
54495 | 43 |
end; |
52555 | 44 |
|
55287 | 45 |
structure Sledgehammer_Proof_Methods : SLEDGEHAMMER_PROOF_METHODS = |
52555 | 46 |
struct |
47 |
||
54828 | 48 |
open ATP_Util |
52555 | 49 |
open ATP_Problem_Generate |
55211 | 50 |
open ATP_Proof_Reconstruct |
52555 | 51 |
|
55285 | 52 |
datatype proof_method = |
53 |
Metis_Method of string option * string option | |
|
54 |
Meson_Method | |
|
58061 | 55 |
SMT_Method | |
56852
b38c5b9cf590
added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0')
blanchet
parents:
56093
diff
changeset
|
56 |
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
|
57 |
Blast_Method | |
55285 | 58 |
Simp_Method | |
59 |
Simp_Size_Method | |
|
60 |
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
|
61 |
Fastforce_Method | |
55285 | 62 |
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
|
63 |
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
|
64 |
Linarith_Method | |
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
65 |
Presburger_Method | |
55285 | 66 |
Algebra_Method |
52555 | 67 |
|
54824 | 68 |
datatype play_outcome = |
69 |
Played of Time.time | |
|
70 |
Play_Timed_Out of Time.time | |
|
56093 | 71 |
Play_Failed |
52555 | 72 |
|
57739 | 73 |
type one_line_params = |
74 |
((string * stature) list * (proof_method * play_outcome)) * string * int * int |
|
55211 | 75 |
|
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
76 |
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
|
77 |
| is_proof_method_direct Meson_Method = true |
58061 | 78 |
| 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
|
79 |
| is_proof_method_direct Simp_Method = true |
57465 | 80 |
| 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
|
81 |
| is_proof_method_direct _ = false |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
82 |
|
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
|
83 |
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
|
84 |
| 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
|
85 |
| 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
|
86 |
|
58499
094efe6ac459
don't affect other subgoals with 'auto' in one-liner proofs
blanchet
parents:
58092
diff
changeset
|
87 |
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
|
88 |
| is_proof_method_multi_goal _ = false |
094efe6ac459
don't affect other subgoals with 'auto' in one-liner proofs
blanchet
parents:
58092
diff
changeset
|
89 |
|
56983
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
90 |
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
|
91 |
|
56985
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset
|
92 |
fun string_of_proof_method ctxt ss meth = |
56983
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
93 |
let |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
94 |
val meth_s = |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
95 |
(case meth of |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
96 |
Metis_Method (NONE, NONE) => "metis" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
97 |
| Metis_Method (type_enc_opt, lam_trans_opt) => |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
98 |
"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
|
99 |
| Meson_Method => "meson" |
58061 | 100 |
| SMT_Method => "smt" |
56983
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
101 |
| SATx_Method => "satx" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
102 |
| Blast_Method => "blast" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
103 |
| 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
|
104 |
| 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
|
105 |
| 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
|
106 |
| Fastforce_Method => "fastforce" |
56983
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
107 |
| 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
|
108 |
| Moura_Method => "moura" |
56983
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
109 |
| Linarith_Method => "linarith" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
110 |
| Presburger_Method => "presburger" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
111 |
| Algebra_Method => "algebra") |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
112 |
in |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
113 |
maybe_paren (space_implode " " (meth_s :: ss)) |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
114 |
end |
55285 | 115 |
|
57054 | 116 |
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
|
117 |
(case meth of |
222f46a4dbec
new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents:
56951
diff
changeset
|
118 |
Metis_Method (type_enc_opt, lam_trans_opt) => |
61330
20af2ad9261e
further improved fine point w.r.t. replaying in the presence of chained facts and a non-empty meta-quantifier prefix + avoid printing internal names in backquotes
blanchet
parents:
60350
diff
changeset
|
119 |
let |
20af2ad9261e
further improved fine point w.r.t. replaying in the presence of chained facts and a non-empty meta-quantifier prefix + avoid printing internal names in backquotes
blanchet
parents:
60350
diff
changeset
|
120 |
val ctxt = ctxt |
20af2ad9261e
further improved fine point w.r.t. replaying in the presence of chained facts and a non-empty meta-quantifier prefix + avoid printing internal names in backquotes
blanchet
parents:
60350
diff
changeset
|
121 |
|> Config.put Metis_Tactic.verbose false |
20af2ad9261e
further improved fine point w.r.t. replaying in the presence of chained facts and a non-empty meta-quantifier prefix + avoid printing internal names in backquotes
blanchet
parents:
60350
diff
changeset
|
122 |
|> Config.put Metis_Tactic.trace false |
20af2ad9261e
further improved fine point w.r.t. replaying in the presence of chained facts and a non-empty meta-quantifier prefix + avoid printing internal names in backquotes
blanchet
parents:
60350
diff
changeset
|
123 |
in |
62219
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61841
diff
changeset
|
124 |
SELECT_GOAL (Metis_Tactic.metis_method ((Option.map single type_enc_opt, lam_trans_opt), |
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61841
diff
changeset
|
125 |
global_facts) ctxt local_facts) |
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
|
126 |
end |
62219
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61841
diff
changeset
|
127 |
| SMT_Method => SMT_Solver.smt_tac ctxt (local_facts @ global_facts) |
56965
222f46a4dbec
new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents:
56951
diff
changeset
|
128 |
| _ => |
62219
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61841
diff
changeset
|
129 |
Method.insert_tac ctxt local_facts THEN' |
55285 | 130 |
(case meth of |
62219
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61841
diff
changeset
|
131 |
Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts |
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61841
diff
changeset
|
132 |
| Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts) |
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61841
diff
changeset
|
133 |
| Simp_Size_Method => |
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61841
diff
changeset
|
134 |
Simplifier.asm_full_simp_tac (ctxt addsimps (@{thm size_ne_size_imp_ne} :: global_facts)) |
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61841
diff
changeset
|
135 |
| _ => |
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61841
diff
changeset
|
136 |
Method.insert_tac ctxt global_facts THEN' |
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61841
diff
changeset
|
137 |
(case meth of |
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61841
diff
changeset
|
138 |
SATx_Method => SAT.satx_tac ctxt |
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61841
diff
changeset
|
139 |
| Blast_Method => blast_tac ctxt |
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61841
diff
changeset
|
140 |
| Auto_Method => SELECT_GOAL (Clasimp.auto_tac ctxt) |
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61841
diff
changeset
|
141 |
| Fastforce_Method => Clasimp.fast_force_tac ctxt |
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61841
diff
changeset
|
142 |
| Force_Method => Clasimp.force_tac ctxt |
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61841
diff
changeset
|
143 |
| Moura_Method => moura_tac ctxt |
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61841
diff
changeset
|
144 |
| Linarith_Method => Lin_Arith.tac ctxt |
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61841
diff
changeset
|
145 |
| Presburger_Method => Cooper.tac true [] [] ctxt |
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61841
diff
changeset
|
146 |
| Algebra_Method => Groebner.algebra_tac [] [] ctxt))) |
55211 | 147 |
|
54828 | 148 |
fun string_of_play_outcome (Played time) = string_of_ext_time (false, time) |
56093 | 149 |
| string_of_play_outcome (Play_Timed_Out time) = |
150 |
if time = Time.zeroTime then "" else string_of_ext_time (true, time) ^ ", timed out" |
|
54828 | 151 |
| string_of_play_outcome Play_Failed = "failed" |
152 |
||
55269 | 153 |
fun play_outcome_ord (Played time1, Played time2) = |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58499
diff
changeset
|
154 |
int_ord (apply2 Time.toMilliseconds (time1, time2)) |
55269 | 155 |
| play_outcome_ord (Played _, _) = LESS |
156 |
| play_outcome_ord (_, Played _) = GREATER |
|
157 |
| 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
|
158 |
int_ord (apply2 Time.toMilliseconds (time1, time2)) |
55269 | 159 |
| play_outcome_ord (Play_Timed_Out _, _) = LESS |
160 |
| play_outcome_ord (_, Play_Timed_Out _) = GREATER |
|
161 |
| play_outcome_ord (Play_Failed, Play_Failed) = EQUAL |
|
162 |
||
55211 | 163 |
fun apply_on_subgoal _ 1 = "by " |
164 |
| apply_on_subgoal 1 _ = "apply " |
|
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
165 |
| apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n |
55211 | 166 |
|
55285 | 167 |
(* 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
|
168 |
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
|
169 |
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
|
170 |
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
|
171 |
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
|
172 |
([], 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
|
173 |
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
|
174 |
(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
|
175 |
in |
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
176 |
(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
|
177 |
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
|
178 |
(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
|
179 |
end |
55211 | 180 |
|
56093 | 181 |
fun try_command_line banner play command = |
182 |
let val s = string_of_play_outcome play in |
|
63518 | 183 |
banner ^ ": " ^ Active.sendback_markup_command command ^ |
63692 | 184 |
(s |> s <> "" ? enclose " (" ")") |
56093 | 185 |
end |
52555 | 186 |
|
56985
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset
|
187 |
fun one_line_proof_text ctxt num_chained |
57739 | 188 |
((used_facts, (meth, play)), banner, subgoal, subgoal_count) = |
57777 | 189 |
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
|
190 |
map fst extra |
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57720
diff
changeset
|
191 |
|> proof_method_command ctxt meth subgoal subgoal_count (map fst chained) num_chained |
63692 | 192 |
|> (if play = Play_Failed then prefix "One-line proof reconstruction failed: " |
57735
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57720
diff
changeset
|
193 |
else try_command_line banner play) |
55211 | 194 |
end |
52555 | 195 |
|
54495 | 196 |
end; |