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@56599
|
19 |
bool * (string option * string option) * Time.time * real * 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_Try0
|
blanchet@56544
|
39 |
open Sledgehammer_Isar_Minimize
|
blanchet@50929
|
40 |
|
blanchet@50929
|
41 |
structure String_Redirect = ATP_Proof_Redirect(
|
blanchet@54723
|
42 |
type key = atp_step_name
|
blanchet@50929
|
43 |
val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s')
|
blanchet@50929
|
44 |
val string_of = fst)
|
blanchet@50929
|
45 |
|
blanchet@50898
|
46 |
open String_Redirect
|
blanchet@50898
|
47 |
|
blanchet@56564
|
48 |
val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false)
|
blanchet@56564
|
49 |
|
blanchet@56111
|
50 |
val e_skolemize_rules = ["skolemize", "shift_quantors"]
|
blanchet@56178
|
51 |
val spass_pirate_datatype_rule = "DT"
|
blanchet@56088
|
52 |
val vampire_skolemisation_rule = "skolemisation"
|
blanchet@56088
|
53 |
(* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *)
|
blanchet@56093
|
54 |
val z3_skolemize_rule = "sk"
|
blanchet@56095
|
55 |
val z3_th_lemma_rule = "th-lemma"
|
blanchet@56088
|
56 |
|
blanchet@56114
|
57 |
val skolemize_rules =
|
blanchet@56114
|
58 |
e_skolemize_rules @ [spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule]
|
blanchet@56088
|
59 |
|
blanchet@56111
|
60 |
val is_skolemize_rule = member (op =) skolemize_rules
|
blanchet@56097
|
61 |
val is_arith_rule = String.isPrefix z3_th_lemma_rule
|
blanchet@56178
|
62 |
val is_datatype_rule = String.isPrefix spass_pirate_datatype_rule
|
blanchet@56097
|
63 |
|
blanchet@55874
|
64 |
fun raw_label_of_num num = (num, 0)
|
blanchet@50929
|
65 |
|
blanchet@55874
|
66 |
fun label_of_clause [(num, _)] = raw_label_of_num num
|
blanchet@55874
|
67 |
| label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0)
|
blanchet@51020
|
68 |
|
blanchet@55878
|
69 |
fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss)
|
blanchet@55878
|
70 |
| add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names))
|
blanchet@50929
|
71 |
|
blanchet@56100
|
72 |
(* No "real" literals means only type information (tfree_tcs, clsrel, or clsarity). *)
|
blanchet@56100
|
73 |
fun is_only_type_information t = t aconv @{prop True}
|
blanchet@56100
|
74 |
|
blanchet@56100
|
75 |
(* Discard facts; consolidate adjacent lines that prove the same formula, since they differ only in
|
blanchet@56101
|
76 |
type information. *)
|
blanchet@56141
|
77 |
fun add_line_pass1 (line as (name, role, t, rule, [])) lines =
|
blanchet@56112
|
78 |
(* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or
|
blanchet@56112
|
79 |
definitions. *)
|
blanchet@56042
|
80 |
if role = Lemma orelse role = Conjecture orelse role = Negated_Conjecture orelse
|
blanchet@56097
|
81 |
role = Hypothesis orelse is_arith_rule rule then
|
blanchet@56088
|
82 |
line :: lines
|
blanchet@55878
|
83 |
else if role = Axiom then
|
blanchet@50929
|
84 |
(* Facts are not proof lines. *)
|
blanchet@55880
|
85 |
lines |> is_only_type_information t ? map (replace_dependencies_in_line (name, []))
|
blanchet@50929
|
86 |
else
|
blanchet@50929
|
87 |
map (replace_dependencies_in_line (name, [])) lines
|
blanchet@56097
|
88 |
| add_line_pass1 line lines = line :: lines
|
blanchet@50929
|
89 |
|
blanchet@56533
|
90 |
fun add_lines_pass2 res [] = rev res
|
blanchet@56533
|
91 |
| add_lines_pass2 res ((name, role, t, rule, deps) :: lines) =
|
blanchet@56526
|
92 |
let
|
blanchet@56526
|
93 |
val is_last_line = null lines
|
blanchet@56526
|
94 |
|
blanchet@56526
|
95 |
fun looks_interesting () =
|
blanchet@56526
|
96 |
not (is_only_type_information t) andalso null (Term.add_tvars t [])
|
blanchet@56526
|
97 |
andalso length deps >= 2 andalso not (can the_single lines)
|
blanchet@56526
|
98 |
|
blanchet@56526
|
99 |
fun is_skolemizing_line (_, _, _, rule', deps') =
|
blanchet@56526
|
100 |
is_skolemize_rule rule' andalso member (op =) deps' name
|
blanchet@56526
|
101 |
fun is_before_skolemize_rule () = exists is_skolemizing_line lines
|
blanchet@56526
|
102 |
in
|
blanchet@56526
|
103 |
if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse
|
blanchet@56526
|
104 |
is_datatype_rule rule orelse is_last_line orelse looks_interesting () orelse
|
blanchet@56526
|
105 |
is_before_skolemize_rule () then
|
blanchet@56533
|
106 |
add_lines_pass2 ((name, role, t, rule, deps) :: res) lines
|
blanchet@56526
|
107 |
else
|
blanchet@56533
|
108 |
add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines)
|
blanchet@56526
|
109 |
end
|
blanchet@50929
|
110 |
|
blanchet@50929
|
111 |
type isar_params =
|
blanchet@56599
|
112 |
bool * (string option * string option) * Time.time * real * bool * (term, string) atp_step list
|
blanchet@56599
|
113 |
* thm
|
blanchet@50929
|
114 |
|
blanchet@56586
|
115 |
val arith_methods =
|
blanchet@56586
|
116 |
[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
|
blanchet@56599
|
117 |
Algebra_Method, Metis_Method (NONE, NONE), Meson_Method]
|
blanchet@56586
|
118 |
val datatype_methods = [Simp_Method, Simp_Size_Method]
|
blanchet@56599
|
119 |
val metislike_methods0 =
|
blanchet@56599
|
120 |
[Metis_Method (NONE, NONE), Simp_Method, Auto_Method, Arith_Method, Blast_Method,
|
blanchet@56599
|
121 |
Fastforce_Method, Force_Method, Algebra_Method, Meson_Method]
|
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@56599
|
132 |
val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, atp_proof,
|
blanchet@56599
|
133 |
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@56510
|
137 |
val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
|
blanchet@56510
|
138 |
val (_, ctxt) =
|
blanchet@56510
|
139 |
params
|
blanchet@56510
|
140 |
|> map (fn (s, T) => (Binding.name s, SOME T, NoSyn))
|
blanchet@56510
|
141 |
|> (fn fixes => ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes)
|
blanchet@56510
|
142 |
|
blanchet@56510
|
143 |
val do_preplay = preplay_timeout <> Time.zeroTime
|
blanchet@56525
|
144 |
val try0_isar = try0_isar andalso do_preplay
|
blanchet@56595
|
145 |
val compress_isar = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress_isar
|
blanchet@56510
|
146 |
|
blanchet@56510
|
147 |
val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
|
blanchet@56510
|
148 |
fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
|
blanchet@56510
|
149 |
|
blanchet@56510
|
150 |
fun get_role keep_role ((num, _), role, t, rule, _) =
|
blanchet@56510
|
151 |
if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
|
blanchet@56510
|
152 |
|
blanchet@50898
|
153 |
val atp_proof =
|
blanchet@50898
|
154 |
atp_proof
|
blanchet@56097
|
155 |
|> rpair [] |-> fold_rev add_line_pass1
|
blanchet@56533
|
156 |
|> add_lines_pass2 []
|
blanchet@56042
|
157 |
|
blanchet@55908
|
158 |
val conjs =
|
blanchet@56042
|
159 |
map_filter (fn (name, role, _, _, _) =>
|
blanchet@56042
|
160 |
if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE)
|
blanchet@56042
|
161 |
atp_proof
|
blanchet@56093
|
162 |
val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof
|
blanchet@56042
|
163 |
val lems =
|
blanchet@56042
|
164 |
map_filter (get_role (curry (op =) Lemma)) atp_proof
|
blanchet@56093
|
165 |
|> map (fn ((l, t), rule) =>
|
blanchet@56095
|
166 |
let
|
blanchet@56586
|
167 |
val (skos, meths) =
|
blanchet@56586
|
168 |
if is_skolemize_rule rule then (skolems_of t, skolem_methods)
|
blanchet@56586
|
169 |
else if is_arith_rule rule then ([], arith_methods)
|
blanchet@56586
|
170 |
else ([], rewrite_methods)
|
blanchet@56095
|
171 |
in
|
blanchet@56586
|
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@56586
|
221 |
((the_list predecessor, []), 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@56042
|
232 |
fun prove sub by = Prove (maybe_show outer c [], [], l, t, sub, by)
|
blanchet@56042
|
233 |
fun do_rest l step = isar_steps outer (SOME l) (step :: accum) infs
|
blanchet@56097
|
234 |
|
blanchet@56097
|
235 |
val deps = fold add_fact_of_dependencies gamma no_facts
|
blanchet@56586
|
236 |
val meths =
|
blanchet@56587
|
237 |
if skolem then skolem_methods
|
blanchet@56587
|
238 |
else if is_arith_rule rule then arith_methods
|
blanchet@56586
|
239 |
else if is_datatype_rule rule then datatype_methods
|
blanchet@56586
|
240 |
else metislike_methods
|
blanchet@56586
|
241 |
val by = (deps, meths)
|
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@56587
|
248 |
isar_steps outer (SOME l) [prove [subproof] (no_facts, meths)] infs
|
blanchet@56042
|
249 |
end
|
blanchet@52285
|
250 |
else
|
blanchet@56042
|
251 |
do_rest l (prove [] by)
|
blanchet@56054
|
252 |
| _ => do_rest l (prove [] by))
|
blanchet@56042
|
253 |
else
|
blanchet@56107
|
254 |
do_rest l (if skolem then Prove ([], skolems_of t, l, t, [], by) else prove [] by)
|
blanchet@56042
|
255 |
end
|
blanchet@56042
|
256 |
| isar_steps outer predecessor accum (Cases cases :: infs) =
|
blanchet@56042
|
257 |
let
|
blanchet@56528
|
258 |
fun isar_case (c, subinfs) =
|
blanchet@56528
|
259 |
isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs
|
blanchet@56042
|
260 |
val c = succedent_of_cases cases
|
blanchet@56042
|
261 |
val l = label_of_clause c
|
blanchet@56042
|
262 |
val t = prop_of_clause c
|
blanchet@56042
|
263 |
val step =
|
blanchet@56102
|
264 |
Prove (maybe_show outer c [], [], l, t,
|
blanchet@56102
|
265 |
map isar_case (filter_out (null o snd) cases),
|
blanchet@56586
|
266 |
((the_list predecessor, []), metislike_methods))
|
blanchet@56042
|
267 |
in
|
blanchet@56042
|
268 |
isar_steps outer (SOME l) (step :: accum) infs
|
blanchet@56042
|
269 |
end
|
blanchet@56042
|
270 |
and isar_proof outer fix assms lems infs =
|
blanchet@56042
|
271 |
Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
|
blanchet@56042
|
272 |
|
blanchet@56599
|
273 |
val string_of_isar_proof = string_of_isar_proof ctxt subgoal subgoal_count
|
blanchet@56556
|
274 |
|
blanchet@56564
|
275 |
val trace = Config.get ctxt trace
|
blanchet@56556
|
276 |
|
blanchet@56598
|
277 |
val canonical_isar_proof =
|
blanchet@52282
|
278 |
refute_graph
|
blanchet@56556
|
279 |
|> trace ? tap (tracing o prefix "Refute graph: " o string_of_refute_graph)
|
blanchet@52213
|
280 |
|> redirect_graph axioms tainted bot
|
blanchet@56556
|
281 |
|> trace ? tap (tracing o prefix "Direct proof: " o string_of_direct_proof)
|
blanchet@56096
|
282 |
|> isar_proof true params assms lems
|
blanchet@56555
|
283 |
|> postprocess_isar_proof_remove_unreferenced_steps I
|
blanchet@56555
|
284 |
|> relabel_isar_proof_canonically
|
blanchet@56556
|
285 |
|
blanchet@56598
|
286 |
val preplay_ctxt = ctxt
|
blanchet@56598
|
287 |
|> enrich_context_with_local_facts canonical_isar_proof
|
blanchet@56598
|
288 |
|> silence_reconstructors debug
|
blanchet@56598
|
289 |
|
blanchet@56602
|
290 |
val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
|
blanchet@56602
|
291 |
|
blanchet@56602
|
292 |
fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
|
blanchet@56602
|
293 |
set_preplay_outcomes_of_isar_step preplay_data l (map (fn meth => (meth,
|
blanchet@56602
|
294 |
Lazy.lazy (fn () => preplay_isar_step preplay_ctxt preplay_timeout meth step)))
|
blanchet@56602
|
295 |
meths)
|
blanchet@56602
|
296 |
| reset_preplay_outcomes _ = ()
|
blanchet@56602
|
297 |
|
blanchet@56602
|
298 |
val _ = fold_isar_steps (K o reset_preplay_outcomes)
|
blanchet@56602
|
299 |
(steps_of_isar_proof canonical_isar_proof) ()
|
blanchet@56556
|
300 |
|
blanchet@56565
|
301 |
fun str_of_preplay_outcome outcome =
|
blanchet@56565
|
302 |
if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
|
blanchet@56565
|
303 |
|
blanchet@56565
|
304 |
fun str_of_meth l meth =
|
blanchet@56602
|
305 |
string_of_proof_method meth ^ " " ^
|
blanchet@56602
|
306 |
str_of_preplay_outcome (preplay_outcome_of_isar_step (!preplay_data) l meth)
|
blanchet@56586
|
307 |
fun comment_of l = map (str_of_meth l) #> commas
|
blanchet@56564
|
308 |
|
blanchet@56556
|
309 |
fun trace_isar_proof label proof =
|
blanchet@56556
|
310 |
if trace then
|
blanchet@56564
|
311 |
tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof comment_of proof ^
|
blanchet@56564
|
312 |
"\n")
|
blanchet@56556
|
313 |
else
|
blanchet@56556
|
314 |
()
|
blanchet@56096
|
315 |
|
blanchet@56170
|
316 |
val (play_outcome, isar_proof) =
|
blanchet@56598
|
317 |
canonical_isar_proof
|
blanchet@56556
|
318 |
|> tap (trace_isar_proof "Original")
|
blanchet@56600
|
319 |
|> compress_isar_proof preplay_ctxt compress_isar preplay_data
|
blanchet@56556
|
320 |
|> tap (trace_isar_proof "Compressed")
|
blanchet@56600
|
321 |
|> try0_isar ? try0_isar_proof preplay_ctxt preplay_timeout preplay_data
|
blanchet@56556
|
322 |
|> tap (trace_isar_proof "Tried0")
|
blanchet@56555
|
323 |
|> postprocess_isar_proof_remove_unreferenced_steps
|
blanchet@56600
|
324 |
(try0_isar ? minimize_isar_step_dependencies preplay_ctxt preplay_data)
|
blanchet@56556
|
325 |
|> tap (trace_isar_proof "Minimized")
|
blanchet@56602
|
326 |
|> `(preplay_outcome_of_isar_proof (!preplay_data))
|
blanchet@56562
|
327 |
||> chain_isar_proof
|
blanchet@56562
|
328 |
||> kill_useless_labels_in_isar_proof
|
blanchet@56562
|
329 |
||> relabel_isar_proof_finally
|
blanchet@50898
|
330 |
in
|
blanchet@56564
|
331 |
(case string_of_isar_proof (K (K "")) isar_proof of
|
blanchet@50898
|
332 |
"" =>
|
blanchet@56555
|
333 |
if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)."
|
blanchet@56555
|
334 |
else ""
|
blanchet@56556
|
335 |
| isar_text =>
|
blanchet@51685
|
336 |
let
|
blanchet@51685
|
337 |
val msg =
|
blanchet@52340
|
338 |
(if verbose then
|
blanchet@56602
|
339 |
let val num_steps = add_isar_steps (steps_of_isar_proof isar_proof) 0 in
|
blanchet@56555
|
340 |
[string_of_int num_steps ^ " step" ^ plural_s num_steps]
|
blanchet@56555
|
341 |
end
|
blanchet@52340
|
342 |
else
|
blanchet@52340
|
343 |
[]) @
|
blanchet@56170
|
344 |
(if do_preplay then [string_of_play_outcome play_outcome] else [])
|
smolkas@51292
|
345 |
in
|
blanchet@55880
|
346 |
"\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
|
blanchet@55880
|
347 |
Active.sendback_markup [Markup.padding_command] isar_text
|
blanchet@56096
|
348 |
end)
|
blanchet@50898
|
349 |
end
|
blanchet@56102
|
350 |
|
blanchet@56510
|
351 |
val one_line_proof = one_line_proof_text 0 one_line_params
|
blanchet@50898
|
352 |
val isar_proof =
|
blanchet@50898
|
353 |
if debug then
|
blanchet@50898
|
354 |
isar_proof_of ()
|
blanchet@56096
|
355 |
else
|
blanchet@56096
|
356 |
(case try isar_proof_of () of
|
blanchet@56096
|
357 |
SOME s => s
|
blanchet@56096
|
358 |
| NONE =>
|
blanchet@56096
|
359 |
if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "")
|
blanchet@50898
|
360 |
in one_line_proof ^ isar_proof end
|
blanchet@50898
|
361 |
|
blanchet@56166
|
362 |
fun isar_proof_would_be_a_good_idea (reconstr, play) =
|
blanchet@56166
|
363 |
(case play of
|
blanchet@56166
|
364 |
Played _ => reconstr = SMT
|
blanchet@56165
|
365 |
| Play_Timed_Out _ => true
|
blanchet@56166
|
366 |
| Play_Failed => true
|
blanchet@56166
|
367 |
| Not_Played => false)
|
blanchet@52324
|
368 |
|
blanchet@56510
|
369 |
fun proof_text ctxt debug isar_proofs isar_params num_chained
|
blanchet@56598
|
370 |
(one_line_params as (preplay, _, _, _, _, _)) =
|
blanchet@52327
|
371 |
(if isar_proofs = SOME true orelse
|
blanchet@52327
|
372 |
(isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
|
blanchet@56510
|
373 |
isar_proof_text ctxt debug isar_proofs isar_params
|
blanchet@50898
|
374 |
else
|
wenzelm@54189
|
375 |
one_line_proof_text num_chained) one_line_params
|
blanchet@50898
|
376 |
|
blanchet@50898
|
377 |
end;
|