blanchet@56544
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar.ML
|
blanchet@50898
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
blanchet@50898
|
3 |
Author: Steffen Juilf Smolka, TU Muenchen
|
blanchet@50898
|
4 |
|
blanchet@50929
|
5 |
Isar proof reconstruction from ATP proofs.
|
blanchet@50898
|
6 |
*)
|
blanchet@50898
|
7 |
|
blanchet@56544
|
8 |
signature SLEDGEHAMMER_ISAR =
|
blanchet@50898
|
9 |
sig
|
blanchet@56113
|
10 |
type atp_step_name = ATP_Proof.atp_step_name
|
blanchet@55868
|
11 |
type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
|
blanchet@54723
|
12 |
type 'a atp_proof = 'a ATP_Proof.atp_proof
|
blanchet@50929
|
13 |
type stature = ATP_Problem_Generate.stature
|
blanchet@55868
|
14 |
type one_line_params = Sledgehammer_Reconstructor.one_line_params
|
blanchet@50929
|
15 |
|
blanchet@56564
|
16 |
val trace : bool Config.T
|
blanchet@56564
|
17 |
|
blanchet@50929
|
18 |
type isar_params =
|
blanchet@56609
|
19 |
bool * (string option * string option) * Time.time * real * bool * bool
|
blanchet@56599
|
20 |
* (term, string) atp_step list * thm
|
blanchet@50929
|
21 |
|
blanchet@56510
|
22 |
val proof_text : Proof.context -> bool -> bool option -> (unit -> isar_params) -> int ->
|
blanchet@56102
|
23 |
one_line_params -> string
|
blanchet@50898
|
24 |
end;
|
blanchet@50898
|
25 |
|
blanchet@56544
|
26 |
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
|
blanchet@50898
|
27 |
struct
|
blanchet@50898
|
28 |
|
blanchet@50898
|
29 |
open ATP_Util
|
blanchet@50929
|
30 |
open ATP_Problem
|
blanchet@50898
|
31 |
open ATP_Proof
|
blanchet@50898
|
32 |
open ATP_Proof_Reconstruct
|
blanchet@50933
|
33 |
open Sledgehammer_Util
|
smolkas@53692
|
34 |
open Sledgehammer_Reconstructor
|
blanchet@56544
|
35 |
open Sledgehammer_Isar_Proof
|
blanchet@56544
|
36 |
open Sledgehammer_Isar_Preplay
|
blanchet@56544
|
37 |
open Sledgehammer_Isar_Compress
|
blanchet@56544
|
38 |
open Sledgehammer_Isar_Minimize
|
blanchet@50929
|
39 |
|
blanchet@50929
|
40 |
structure String_Redirect = ATP_Proof_Redirect(
|
blanchet@54723
|
41 |
type key = atp_step_name
|
blanchet@50929
|
42 |
val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s')
|
blanchet@50929
|
43 |
val string_of = fst)
|
blanchet@50929
|
44 |
|
blanchet@50898
|
45 |
open String_Redirect
|
blanchet@50898
|
46 |
|
blanchet@56564
|
47 |
val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false)
|
blanchet@56564
|
48 |
|
blanchet@56111
|
49 |
val e_skolemize_rules = ["skolemize", "shift_quantors"]
|
blanchet@56178
|
50 |
val spass_pirate_datatype_rule = "DT"
|
blanchet@56088
|
51 |
val vampire_skolemisation_rule = "skolemisation"
|
blanchet@56088
|
52 |
(* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *)
|
blanchet@56093
|
53 |
val z3_skolemize_rule = "sk"
|
blanchet@56095
|
54 |
val z3_th_lemma_rule = "th-lemma"
|
blanchet@56088
|
55 |
|
blanchet@56114
|
56 |
val skolemize_rules =
|
blanchet@56114
|
57 |
e_skolemize_rules @ [spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule]
|
blanchet@56088
|
58 |
|
blanchet@56111
|
59 |
val is_skolemize_rule = member (op =) skolemize_rules
|
blanchet@56097
|
60 |
val is_arith_rule = String.isPrefix z3_th_lemma_rule
|
blanchet@56178
|
61 |
val is_datatype_rule = String.isPrefix spass_pirate_datatype_rule
|
blanchet@56097
|
62 |
|
blanchet@55874
|
63 |
fun raw_label_of_num num = (num, 0)
|
blanchet@50929
|
64 |
|
blanchet@55874
|
65 |
fun label_of_clause [(num, _)] = raw_label_of_num num
|
blanchet@55874
|
66 |
| label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0)
|
blanchet@51020
|
67 |
|
blanchet@55878
|
68 |
fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss)
|
blanchet@55878
|
69 |
| add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names))
|
blanchet@50929
|
70 |
|
blanchet@56100
|
71 |
(* No "real" literals means only type information (tfree_tcs, clsrel, or clsarity). *)
|
blanchet@56100
|
72 |
fun is_only_type_information t = t aconv @{prop True}
|
blanchet@56100
|
73 |
|
blanchet@56100
|
74 |
(* Discard facts; consolidate adjacent lines that prove the same formula, since they differ only in
|
blanchet@56101
|
75 |
type information. *)
|
blanchet@56141
|
76 |
fun add_line_pass1 (line as (name, role, t, rule, [])) lines =
|
blanchet@56112
|
77 |
(* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or
|
blanchet@56112
|
78 |
definitions. *)
|
blanchet@56042
|
79 |
if role = Lemma orelse role = Conjecture orelse role = Negated_Conjecture orelse
|
blanchet@56097
|
80 |
role = Hypothesis orelse is_arith_rule rule then
|
blanchet@56088
|
81 |
line :: lines
|
blanchet@55878
|
82 |
else if role = Axiom then
|
blanchet@50929
|
83 |
(* Facts are not proof lines. *)
|
blanchet@55880
|
84 |
lines |> is_only_type_information t ? map (replace_dependencies_in_line (name, []))
|
blanchet@50929
|
85 |
else
|
blanchet@50929
|
86 |
map (replace_dependencies_in_line (name, [])) lines
|
blanchet@56097
|
87 |
| add_line_pass1 line lines = line :: lines
|
blanchet@50929
|
88 |
|
blanchet@56533
|
89 |
fun add_lines_pass2 res [] = rev res
|
blanchet@56533
|
90 |
| add_lines_pass2 res ((name, role, t, rule, deps) :: lines) =
|
blanchet@56526
|
91 |
let
|
blanchet@56526
|
92 |
val is_last_line = null lines
|
blanchet@56526
|
93 |
|
blanchet@56526
|
94 |
fun looks_interesting () =
|
blanchet@56526
|
95 |
not (is_only_type_information t) andalso null (Term.add_tvars t [])
|
blanchet@56526
|
96 |
andalso length deps >= 2 andalso not (can the_single lines)
|
blanchet@56526
|
97 |
|
blanchet@56526
|
98 |
fun is_skolemizing_line (_, _, _, rule', deps') =
|
blanchet@56526
|
99 |
is_skolemize_rule rule' andalso member (op =) deps' name
|
blanchet@56526
|
100 |
fun is_before_skolemize_rule () = exists is_skolemizing_line lines
|
blanchet@56526
|
101 |
in
|
blanchet@56526
|
102 |
if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse
|
blanchet@56526
|
103 |
is_datatype_rule rule orelse is_last_line orelse looks_interesting () orelse
|
blanchet@56526
|
104 |
is_before_skolemize_rule () then
|
blanchet@56533
|
105 |
add_lines_pass2 ((name, role, t, rule, deps) :: res) lines
|
blanchet@56526
|
106 |
else
|
blanchet@56533
|
107 |
add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines)
|
blanchet@56526
|
108 |
end
|
blanchet@50929
|
109 |
|
blanchet@50929
|
110 |
type isar_params =
|
blanchet@56609
|
111 |
bool * (string option * string option) * Time.time * real * bool * bool
|
blanchet@56609
|
112 |
* (term, string) atp_step list * thm
|
blanchet@50929
|
113 |
|
blanchet@56586
|
114 |
val arith_methods =
|
blanchet@56586
|
115 |
[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
|
blanchet@56599
|
116 |
Algebra_Method, Metis_Method (NONE, NONE), Meson_Method]
|
blanchet@56586
|
117 |
val datatype_methods = [Simp_Method, Simp_Size_Method]
|
blanchet@56599
|
118 |
val metislike_methods0 =
|
blanchet@56599
|
119 |
[Metis_Method (NONE, NONE), Simp_Method, Auto_Method, Arith_Method, Blast_Method,
|
blanchet@56616
|
120 |
Fastforce_Method, Force_Method, Algebra_Method, Meson_Method,
|
blanchet@56616
|
121 |
Metis_Method (SOME no_typesN, NONE)]
|
blanchet@56586
|
122 |
val rewrite_methods =
|
blanchet@56599
|
123 |
[Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method (NONE, NONE),
|
blanchet@56599
|
124 |
Meson_Method]
|
blanchet@56599
|
125 |
val skolem_methods = [Metis_Method (NONE, NONE), Blast_Method, Meson_Method]
|
blanchet@56108
|
126 |
|
blanchet@56510
|
127 |
fun isar_proof_text ctxt debug isar_proofs isar_params
|
blanchet@50933
|
128 |
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
|
blanchet@50898
|
129 |
let
|
blanchet@50898
|
130 |
fun isar_proof_of () =
|
blanchet@50898
|
131 |
let
|
blanchet@56609
|
132 |
val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, minimize,
|
blanchet@56609
|
133 |
atp_proof, goal) = try isar_params ()
|
blanchet@56599
|
134 |
|
blanchet@56599
|
135 |
val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0
|
blanchet@56510
|
136 |
|
blanchet@56615
|
137 |
val massage_meths = not try0_isar ? single o hd
|
blanchet@56615
|
138 |
|
blanchet@56510
|
139 |
val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
|
blanchet@56606
|
140 |
val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
|
blanchet@56606
|
141 |
val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
|
blanchet@56510
|
142 |
|
blanchet@56510
|
143 |
val do_preplay = preplay_timeout <> Time.zeroTime
|
blanchet@56595
|
144 |
val compress_isar = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress_isar
|
blanchet@56510
|
145 |
|
blanchet@56510
|
146 |
val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
|
blanchet@56510
|
147 |
fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
|
blanchet@56510
|
148 |
|
blanchet@56510
|
149 |
fun get_role keep_role ((num, _), role, t, rule, _) =
|
blanchet@56510
|
150 |
if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
|
blanchet@56510
|
151 |
|
blanchet@50898
|
152 |
val atp_proof =
|
blanchet@50898
|
153 |
atp_proof
|
blanchet@56097
|
154 |
|> rpair [] |-> fold_rev add_line_pass1
|
blanchet@56533
|
155 |
|> add_lines_pass2 []
|
blanchet@56042
|
156 |
|
blanchet@55908
|
157 |
val conjs =
|
blanchet@56042
|
158 |
map_filter (fn (name, role, _, _, _) =>
|
blanchet@56042
|
159 |
if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE)
|
blanchet@56042
|
160 |
atp_proof
|
blanchet@56093
|
161 |
val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof
|
blanchet@56042
|
162 |
val lems =
|
blanchet@56042
|
163 |
map_filter (get_role (curry (op =) Lemma)) atp_proof
|
blanchet@56093
|
164 |
|> map (fn ((l, t), rule) =>
|
blanchet@56095
|
165 |
let
|
blanchet@56586
|
166 |
val (skos, meths) =
|
blanchet@56615
|
167 |
(if is_skolemize_rule rule then (skolems_of t, skolem_methods)
|
blanchet@56615
|
168 |
else if is_arith_rule rule then ([], arith_methods)
|
blanchet@56615
|
169 |
else ([], rewrite_methods))
|
blanchet@56615
|
170 |
||> massage_meths
|
blanchet@56095
|
171 |
in
|
blanchet@56622
|
172 |
Prove ([], skos, l, t, [], ([], []), meths)
|
blanchet@56095
|
173 |
end)
|
blanchet@56042
|
174 |
|
blanchet@52349
|
175 |
val bot = atp_proof |> List.last |> #1
|
blanchet@56042
|
176 |
|
blanchet@52282
|
177 |
val refute_graph =
|
blanchet@52349
|
178 |
atp_proof
|
blanchet@52349
|
179 |
|> map (fn (name, _, _, _, from) => (from, name))
|
blanchet@52349
|
180 |
|> make_refute_graph bot
|
blanchet@52349
|
181 |
|> fold (Atom_Graph.default_node o rpair ()) conjs
|
blanchet@56042
|
182 |
|
blanchet@52282
|
183 |
val axioms = axioms_of_refute_graph refute_graph conjs
|
blanchet@56042
|
184 |
|
blanchet@52282
|
185 |
val tainted = tainted_atoms_of_refute_graph refute_graph conjs
|
blanchet@52293
|
186 |
val is_clause_tainted = exists (member (op =) tainted)
|
blanchet@51691
|
187 |
val steps =
|
blanchet@50898
|
188 |
Symtab.empty
|
blanchet@52338
|
189 |
|> fold (fn (name as (s, _), role, t, rule, _) =>
|
blanchet@56100
|
190 |
Symtab.update_new (s, (rule, t
|
blanchet@56100
|
191 |
|> (if is_clause_tainted [name] then
|
blanchet@56110
|
192 |
HOLogic.dest_Trueprop
|
blanchet@56110
|
193 |
#> role <> Conjecture ? s_not
|
blanchet@56100
|
194 |
#> fold exists_of (map Var (Term.add_vars t []))
|
blanchet@56110
|
195 |
#> HOLogic.mk_Trueprop
|
blanchet@56100
|
196 |
else
|
blanchet@56100
|
197 |
I))))
|
blanchet@56100
|
198 |
atp_proof
|
blanchet@56042
|
199 |
|
blanchet@56097
|
200 |
val rule_of_clause_id = fst o the o Symtab.lookup steps o fst
|
blanchet@56042
|
201 |
|
blanchet@56099
|
202 |
fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> close_form
|
blanchet@51031
|
203 |
| prop_of_clause names =
|
blanchet@51691
|
204 |
let
|
blanchet@56100
|
205 |
val lits = map (HOLogic.dest_Trueprop o snd)
|
blanchet@56100
|
206 |
(map_filter (Symtab.lookup steps o fst) names)
|
blanchet@51691
|
207 |
in
|
blanchet@56096
|
208 |
(case List.partition (can HOLogic.dest_not) lits of
|
blanchet@51033
|
209 |
(negs as _ :: _, pos as _ :: _) =>
|
blanchet@55880
|
210 |
s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos)
|
blanchet@56096
|
211 |
| _ => fold (curry s_disj) lits @{term False})
|
blanchet@51033
|
212 |
end
|
blanchet@51031
|
213 |
|> HOLogic.mk_Trueprop |> close_form
|
blanchet@56042
|
214 |
|
blanchet@56511
|
215 |
fun maybe_show outer c = (outer andalso eq_set (op =) (c, conjs)) ? cons Show
|
blanchet@56042
|
216 |
|
blanchet@56042
|
217 |
fun isar_steps outer predecessor accum [] =
|
blanchet@56042
|
218 |
accum
|
blanchet@56042
|
219 |
|> (if tainted = [] then
|
blanchet@56042
|
220 |
cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
|
blanchet@56622
|
221 |
(the_list predecessor, []), massage_meths metislike_methods))
|
blanchet@56042
|
222 |
else
|
blanchet@56042
|
223 |
I)
|
blanchet@56042
|
224 |
|> rev
|
blanchet@56097
|
225 |
| isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) =
|
blanchet@56042
|
226 |
let
|
blanchet@56042
|
227 |
val l = label_of_clause c
|
blanchet@56042
|
228 |
val t = prop_of_clause c
|
blanchet@56097
|
229 |
val rule = rule_of_clause_id id
|
blanchet@56097
|
230 |
val skolem = is_skolemize_rule rule
|
blanchet@56097
|
231 |
|
blanchet@56621
|
232 |
val deps = fold add_fact_of_dependencies gamma ([], [])
|
blanchet@56586
|
233 |
val meths =
|
blanchet@56615
|
234 |
(if skolem then skolem_methods
|
blanchet@56615
|
235 |
else if is_arith_rule rule then arith_methods
|
blanchet@56615
|
236 |
else if is_datatype_rule rule then datatype_methods
|
blanchet@56615
|
237 |
else metislike_methods)
|
blanchet@56615
|
238 |
|> massage_meths
|
blanchet@56622
|
239 |
|
blanchet@56622
|
240 |
fun prove sub facts = Prove (maybe_show outer c [], [], l, t, sub, facts, meths)
|
blanchet@56622
|
241 |
fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs
|
blanchet@56042
|
242 |
in
|
blanchet@56042
|
243 |
if is_clause_tainted c then
|
blanchet@56054
|
244 |
(case gamma of
|
blanchet@56042
|
245 |
[g] =>
|
blanchet@56097
|
246 |
if skolem andalso is_clause_tainted g then
|
blanchet@56093
|
247 |
let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in
|
blanchet@56622
|
248 |
isar_steps outer (SOME l) [prove [subproof] ([], [])] infs
|
blanchet@56042
|
249 |
end
|
blanchet@52285
|
250 |
else
|
blanchet@56622
|
251 |
steps_of_rest (prove [] deps)
|
blanchet@56622
|
252 |
| _ => steps_of_rest (prove [] deps))
|
blanchet@56042
|
253 |
else
|
blanchet@56622
|
254 |
steps_of_rest (if skolem then Prove ([], skolems_of t, l, t, [], deps, meths)
|
blanchet@56622
|
255 |
else prove [] deps)
|
blanchet@56042
|
256 |
end
|
blanchet@56042
|
257 |
| isar_steps outer predecessor accum (Cases cases :: infs) =
|
blanchet@56042
|
258 |
let
|
blanchet@56528
|
259 |
fun isar_case (c, subinfs) =
|
blanchet@56528
|
260 |
isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs
|
blanchet@56042
|
261 |
val c = succedent_of_cases cases
|
blanchet@56042
|
262 |
val l = label_of_clause c
|
blanchet@56042
|
263 |
val t = prop_of_clause c
|
blanchet@56042
|
264 |
val step =
|
blanchet@56102
|
265 |
Prove (maybe_show outer c [], [], l, t,
|
blanchet@56102
|
266 |
map isar_case (filter_out (null o snd) cases),
|
blanchet@56622
|
267 |
(the_list predecessor, []), massage_meths metislike_methods)
|
blanchet@56042
|
268 |
in
|
blanchet@56042
|
269 |
isar_steps outer (SOME l) (step :: accum) infs
|
blanchet@56042
|
270 |
end
|
blanchet@56042
|
271 |
and isar_proof outer fix assms lems infs =
|
blanchet@56042
|
272 |
Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
|
blanchet@56042
|
273 |
|
blanchet@56599
|
274 |
val string_of_isar_proof = string_of_isar_proof ctxt subgoal subgoal_count
|
blanchet@56556
|
275 |
|
blanchet@56564
|
276 |
val trace = Config.get ctxt trace
|
blanchet@56556
|
277 |
|
blanchet@56598
|
278 |
val canonical_isar_proof =
|
blanchet@52282
|
279 |
refute_graph
|
blanchet@56556
|
280 |
|> trace ? tap (tracing o prefix "Refute graph: " o string_of_refute_graph)
|
blanchet@52213
|
281 |
|> redirect_graph axioms tainted bot
|
blanchet@56556
|
282 |
|> trace ? tap (tracing o prefix "Direct proof: " o string_of_direct_proof)
|
blanchet@56096
|
283 |
|> isar_proof true params assms lems
|
blanchet@56555
|
284 |
|> postprocess_isar_proof_remove_unreferenced_steps I
|
blanchet@56555
|
285 |
|> relabel_isar_proof_canonically
|
blanchet@56556
|
286 |
|
blanchet@56606
|
287 |
val ctxt = ctxt
|
blanchet@56598
|
288 |
|> enrich_context_with_local_facts canonical_isar_proof
|
blanchet@56598
|
289 |
|> silence_reconstructors debug
|
blanchet@56598
|
290 |
|
blanchet@56602
|
291 |
val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
|
blanchet@56602
|
292 |
|
blanchet@56606
|
293 |
val _ = fold_isar_steps (fn meth =>
|
blanchet@56606
|
294 |
K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth []))
|
blanchet@56602
|
295 |
(steps_of_isar_proof canonical_isar_proof) ()
|
blanchet@56556
|
296 |
|
blanchet@56565
|
297 |
fun str_of_preplay_outcome outcome =
|
blanchet@56565
|
298 |
if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
|
blanchet@56565
|
299 |
|
blanchet@56565
|
300 |
fun str_of_meth l meth =
|
blanchet@56602
|
301 |
string_of_proof_method meth ^ " " ^
|
blanchet@56608
|
302 |
str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)
|
blanchet@56586
|
303 |
fun comment_of l = map (str_of_meth l) #> commas
|
blanchet@56564
|
304 |
|
blanchet@56556
|
305 |
fun trace_isar_proof label proof =
|
blanchet@56556
|
306 |
if trace then
|
blanchet@56564
|
307 |
tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof comment_of proof ^
|
blanchet@56564
|
308 |
"\n")
|
blanchet@56556
|
309 |
else
|
blanchet@56556
|
310 |
()
|
blanchet@56096
|
311 |
|
blanchet@56170
|
312 |
val (play_outcome, isar_proof) =
|
blanchet@56598
|
313 |
canonical_isar_proof
|
blanchet@56556
|
314 |
|> tap (trace_isar_proof "Original")
|
blanchet@56606
|
315 |
|> compress_isar_proof ctxt compress_isar preplay_data
|
blanchet@56556
|
316 |
|> tap (trace_isar_proof "Compressed")
|
blanchet@56555
|
317 |
|> postprocess_isar_proof_remove_unreferenced_steps
|
blanchet@56608
|
318 |
(keep_fastest_method_of_isar_step (!preplay_data)
|
blanchet@56609
|
319 |
#> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
|
blanchet@56556
|
320 |
|> tap (trace_isar_proof "Minimized")
|
blanchet@56602
|
321 |
|> `(preplay_outcome_of_isar_proof (!preplay_data))
|
blanchet@56562
|
322 |
||> chain_isar_proof
|
blanchet@56562
|
323 |
||> kill_useless_labels_in_isar_proof
|
blanchet@56562
|
324 |
||> relabel_isar_proof_finally
|
blanchet@50898
|
325 |
in
|
blanchet@56564
|
326 |
(case string_of_isar_proof (K (K "")) isar_proof of
|
blanchet@50898
|
327 |
"" =>
|
blanchet@56555
|
328 |
if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)."
|
blanchet@56555
|
329 |
else ""
|
blanchet@56556
|
330 |
| isar_text =>
|
blanchet@51685
|
331 |
let
|
blanchet@51685
|
332 |
val msg =
|
blanchet@52340
|
333 |
(if verbose then
|
blanchet@56602
|
334 |
let val num_steps = add_isar_steps (steps_of_isar_proof isar_proof) 0 in
|
blanchet@56555
|
335 |
[string_of_int num_steps ^ " step" ^ plural_s num_steps]
|
blanchet@56555
|
336 |
end
|
blanchet@52340
|
337 |
else
|
blanchet@52340
|
338 |
[]) @
|
blanchet@56170
|
339 |
(if do_preplay then [string_of_play_outcome play_outcome] else [])
|
smolkas@51292
|
340 |
in
|
blanchet@55880
|
341 |
"\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
|
blanchet@55880
|
342 |
Active.sendback_markup [Markup.padding_command] isar_text
|
blanchet@56096
|
343 |
end)
|
blanchet@50898
|
344 |
end
|
blanchet@56102
|
345 |
|
blanchet@56510
|
346 |
val one_line_proof = one_line_proof_text 0 one_line_params
|
blanchet@50898
|
347 |
val isar_proof =
|
blanchet@50898
|
348 |
if debug then
|
blanchet@50898
|
349 |
isar_proof_of ()
|
blanchet@56096
|
350 |
else
|
blanchet@56096
|
351 |
(case try isar_proof_of () of
|
blanchet@56096
|
352 |
SOME s => s
|
blanchet@56096
|
353 |
| NONE =>
|
blanchet@56096
|
354 |
if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "")
|
blanchet@50898
|
355 |
in one_line_proof ^ isar_proof end
|
blanchet@50898
|
356 |
|
blanchet@56166
|
357 |
fun isar_proof_would_be_a_good_idea (reconstr, play) =
|
blanchet@56166
|
358 |
(case play of
|
blanchet@56166
|
359 |
Played _ => reconstr = SMT
|
blanchet@56165
|
360 |
| Play_Timed_Out _ => true
|
blanchet@56166
|
361 |
| Play_Failed => true
|
blanchet@56166
|
362 |
| Not_Played => false)
|
blanchet@52324
|
363 |
|
blanchet@56510
|
364 |
fun proof_text ctxt debug isar_proofs isar_params num_chained
|
blanchet@56598
|
365 |
(one_line_params as (preplay, _, _, _, _, _)) =
|
blanchet@52327
|
366 |
(if isar_proofs = SOME true orelse
|
blanchet@52327
|
367 |
(isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
|
blanchet@56510
|
368 |
isar_proof_text ctxt debug isar_proofs isar_params
|
blanchet@50898
|
369 |
else
|
wenzelm@54189
|
370 |
one_line_proof_text num_chained) one_line_params
|
blanchet@50898
|
371 |
|
blanchet@50898
|
372 |
end;
|