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@56629
|
14 |
type one_line_params = Sledgehammer_Proof_Methods.one_line_params
|
blanchet@50929
|
15 |
|
blanchet@56564
|
16 |
val trace : bool Config.T
|
blanchet@56564
|
17 |
|
blanchet@50929
|
18 |
type isar_params =
|
blanchet@56638
|
19 |
bool * (string option * string option) * Time.time * real * bool * bool
|
blanchet@56630
|
20 |
* (term, string) atp_step list * thm
|
blanchet@50929
|
21 |
|
blanchet@56638
|
22 |
val proof_text : Proof.context -> bool -> bool option -> bool option -> (unit -> isar_params) ->
|
blanchet@56638
|
23 |
int -> 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
|
blanchet@56629
|
34 |
open Sledgehammer_Proof_Methods
|
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@57468
|
71 |
fun is_True_prop t = t aconv @{prop True}
|
blanchet@56100
|
72 |
|
blanchet@56141
|
73 |
fun add_line_pass1 (line as (name, role, t, rule, [])) lines =
|
blanchet@56112
|
74 |
(* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or
|
blanchet@56112
|
75 |
definitions. *)
|
blanchet@58398
|
76 |
if role = Conjecture orelse role = Negated_Conjecture then line :: lines
|
blanchet@58398
|
77 |
else if is_True_prop t then map (replace_dependencies_in_line (name, [])) lines
|
blanchet@58398
|
78 |
else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then line :: lines
|
blanchet@58398
|
79 |
else if role = Axiom then lines (* axioms (facts) need no proof lines *)
|
blanchet@58398
|
80 |
else map (replace_dependencies_in_line (name, [])) lines
|
blanchet@56097
|
81 |
| add_line_pass1 line lines = line :: lines
|
blanchet@50929
|
82 |
|
blanchet@57472
|
83 |
fun add_lines_pass2 res _ [] = rev res
|
blanchet@57472
|
84 |
| add_lines_pass2 res prev_t ((line as (name, role, t, rule, deps)) :: lines) =
|
blanchet@56526
|
85 |
let
|
blanchet@56526
|
86 |
val is_last_line = null lines
|
blanchet@56526
|
87 |
|
blanchet@56526
|
88 |
fun looks_interesting () =
|
blanchet@57472
|
89 |
not (is_True_prop t) andalso not (t aconv prev_t) andalso null (Term.add_tvars t []) andalso
|
blanchet@57472
|
90 |
length deps >= 2 andalso not (can the_single lines)
|
blanchet@56526
|
91 |
|
blanchet@56526
|
92 |
fun is_skolemizing_line (_, _, _, rule', deps') =
|
blanchet@56526
|
93 |
is_skolemize_rule rule' andalso member (op =) deps' name
|
blanchet@56526
|
94 |
fun is_before_skolemize_rule () = exists is_skolemizing_line lines
|
blanchet@56526
|
95 |
in
|
blanchet@56526
|
96 |
if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse
|
blanchet@56526
|
97 |
is_datatype_rule rule orelse is_last_line orelse looks_interesting () orelse
|
blanchet@56526
|
98 |
is_before_skolemize_rule () then
|
blanchet@57472
|
99 |
add_lines_pass2 (line :: res) t lines
|
blanchet@56526
|
100 |
else
|
blanchet@57472
|
101 |
add_lines_pass2 res t (map (replace_dependencies_in_line (name, deps)) lines)
|
blanchet@56526
|
102 |
end
|
blanchet@50929
|
103 |
|
blanchet@50929
|
104 |
type isar_params =
|
blanchet@56638
|
105 |
bool * (string option * string option) * Time.time * real * bool * bool
|
blanchet@56630
|
106 |
* (term, string) atp_step list * thm
|
blanchet@50929
|
107 |
|
blanchet@58194
|
108 |
val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method]
|
blanchet@57439
|
109 |
val simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method]
|
blanchet@56665
|
110 |
val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method]
|
blanchet@56653
|
111 |
|
blanchet@56653
|
112 |
val arith_methods = basic_arith_methods @ simp_based_methods @ basic_systematic_methods
|
blanchet@56653
|
113 |
val datatype_methods = [Simp_Method, Simp_Size_Method]
|
blanchet@56653
|
114 |
val systematic_methods0 = basic_systematic_methods @ basic_arith_methods @ simp_based_methods @
|
blanchet@56653
|
115 |
[Metis_Method (SOME no_typesN, NONE)]
|
blanchet@56653
|
116 |
val rewrite_methods = simp_based_methods @ basic_systematic_methods @ basic_arith_methods
|
blanchet@56653
|
117 |
val skolem_methods = basic_systematic_methods
|
blanchet@56108
|
118 |
|
blanchet@56639
|
119 |
fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
|
blanchet@58629
|
120 |
(one_line_params as ((_, one_line_play), banner, used_facts, minimize_command, subgoal,
|
blanchet@58629
|
121 |
subgoal_count)) =
|
blanchet@50898
|
122 |
let
|
blanchet@57439
|
123 |
val _ = if debug then Output.urgent_message "Constructing Isar proof..." else ()
|
blanchet@57439
|
124 |
|
blanchet@58629
|
125 |
fun generate_proof_text () =
|
blanchet@50898
|
126 |
let
|
blanchet@58587
|
127 |
val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof, goal) =
|
blanchet@58587
|
128 |
isar_params ()
|
blanchet@56599
|
129 |
|
blanchet@56653
|
130 |
val systematic_methods = insert (op =) (Metis_Method alt_metis_args) systematic_methods0
|
blanchet@56510
|
131 |
|
blanchet@56653
|
132 |
fun massage_methods (meths as meth :: _) =
|
blanchet@58587
|
133 |
if not try0 then [meth]
|
blanchet@57423
|
134 |
else if smt_proofs = SOME true then SMT2_Method :: meths
|
blanchet@56639
|
135 |
else meths
|
blanchet@56615
|
136 |
|
blanchet@56510
|
137 |
val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
|
blanchet@56606
|
138 |
val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
|
blanchet@56606
|
139 |
val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
|
blanchet@56510
|
140 |
|
blanchet@56510
|
141 |
val do_preplay = preplay_timeout <> Time.zeroTime
|
blanchet@58587
|
142 |
val compress = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress
|
blanchet@56510
|
143 |
|
wenzelm@57290
|
144 |
val is_fixed = Variable.is_declared ctxt orf Name.is_skolem
|
blanchet@56510
|
145 |
fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
|
blanchet@56510
|
146 |
|
blanchet@56510
|
147 |
fun get_role keep_role ((num, _), role, t, rule, _) =
|
blanchet@56510
|
148 |
if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
|
blanchet@56510
|
149 |
|
blanchet@50898
|
150 |
val atp_proof =
|
blanchet@50898
|
151 |
atp_proof
|
blanchet@56097
|
152 |
|> rpair [] |-> fold_rev add_line_pass1
|
blanchet@57472
|
153 |
|> add_lines_pass2 [] Term.dummy
|
blanchet@56042
|
154 |
|
blanchet@55908
|
155 |
val conjs =
|
blanchet@56042
|
156 |
map_filter (fn (name, role, _, _, _) =>
|
blanchet@56042
|
157 |
if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE)
|
blanchet@56042
|
158 |
atp_proof
|
blanchet@56093
|
159 |
val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof
|
blanchet@56042
|
160 |
val lems =
|
blanchet@56042
|
161 |
map_filter (get_role (curry (op =) Lemma)) atp_proof
|
blanchet@56093
|
162 |
|> map (fn ((l, t), rule) =>
|
blanchet@56095
|
163 |
let
|
blanchet@56586
|
164 |
val (skos, meths) =
|
blanchet@56615
|
165 |
(if is_skolemize_rule rule then (skolems_of t, skolem_methods)
|
blanchet@56615
|
166 |
else if is_arith_rule rule then ([], arith_methods)
|
blanchet@56615
|
167 |
else ([], rewrite_methods))
|
blanchet@56653
|
168 |
||> massage_methods
|
blanchet@56095
|
169 |
in
|
blanchet@56641
|
170 |
Prove ([], skos, l, t, [], ([], []), meths, "")
|
blanchet@56095
|
171 |
end)
|
blanchet@56042
|
172 |
|
blanchet@52349
|
173 |
val bot = atp_proof |> List.last |> #1
|
blanchet@56042
|
174 |
|
blanchet@52282
|
175 |
val refute_graph =
|
blanchet@52349
|
176 |
atp_proof
|
blanchet@52349
|
177 |
|> map (fn (name, _, _, _, from) => (from, name))
|
blanchet@52349
|
178 |
|> make_refute_graph bot
|
blanchet@52349
|
179 |
|> fold (Atom_Graph.default_node o rpair ()) conjs
|
blanchet@56042
|
180 |
|
blanchet@52282
|
181 |
val axioms = axioms_of_refute_graph refute_graph conjs
|
blanchet@56042
|
182 |
|
blanchet@52282
|
183 |
val tainted = tainted_atoms_of_refute_graph refute_graph conjs
|
blanchet@52293
|
184 |
val is_clause_tainted = exists (member (op =) tainted)
|
blanchet@51691
|
185 |
val steps =
|
blanchet@50898
|
186 |
Symtab.empty
|
blanchet@52338
|
187 |
|> fold (fn (name as (s, _), role, t, rule, _) =>
|
blanchet@56100
|
188 |
Symtab.update_new (s, (rule, t
|
blanchet@56100
|
189 |
|> (if is_clause_tainted [name] then
|
blanchet@56110
|
190 |
HOLogic.dest_Trueprop
|
blanchet@56110
|
191 |
#> role <> Conjecture ? s_not
|
blanchet@56100
|
192 |
#> fold exists_of (map Var (Term.add_vars t []))
|
blanchet@56110
|
193 |
#> HOLogic.mk_Trueprop
|
blanchet@56100
|
194 |
else
|
blanchet@56100
|
195 |
I))))
|
blanchet@56100
|
196 |
atp_proof
|
blanchet@56042
|
197 |
|
blanchet@56097
|
198 |
val rule_of_clause_id = fst o the o Symtab.lookup steps o fst
|
blanchet@56042
|
199 |
|
blanchet@56099
|
200 |
fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> close_form
|
blanchet@51031
|
201 |
| prop_of_clause names =
|
blanchet@51691
|
202 |
let
|
blanchet@56100
|
203 |
val lits = map (HOLogic.dest_Trueprop o snd)
|
blanchet@56100
|
204 |
(map_filter (Symtab.lookup steps o fst) names)
|
blanchet@51691
|
205 |
in
|
blanchet@56096
|
206 |
(case List.partition (can HOLogic.dest_not) lits of
|
blanchet@51033
|
207 |
(negs as _ :: _, pos as _ :: _) =>
|
blanchet@55880
|
208 |
s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos)
|
blanchet@56096
|
209 |
| _ => fold (curry s_disj) lits @{term False})
|
blanchet@51033
|
210 |
end
|
blanchet@51031
|
211 |
|> HOLogic.mk_Trueprop |> close_form
|
blanchet@56042
|
212 |
|
blanchet@56511
|
213 |
fun maybe_show outer c = (outer andalso eq_set (op =) (c, conjs)) ? cons Show
|
blanchet@56042
|
214 |
|
blanchet@56042
|
215 |
fun isar_steps outer predecessor accum [] =
|
blanchet@56042
|
216 |
accum
|
blanchet@56042
|
217 |
|> (if tainted = [] then
|
blanchet@56042
|
218 |
cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
|
blanchet@56653
|
219 |
(the_list predecessor, []), massage_methods systematic_methods, ""))
|
blanchet@56042
|
220 |
else
|
blanchet@56042
|
221 |
I)
|
blanchet@56042
|
222 |
|> rev
|
blanchet@56097
|
223 |
| isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) =
|
blanchet@56042
|
224 |
let
|
blanchet@56042
|
225 |
val l = label_of_clause c
|
blanchet@56042
|
226 |
val t = prop_of_clause c
|
blanchet@56097
|
227 |
val rule = rule_of_clause_id id
|
blanchet@56097
|
228 |
val skolem = is_skolemize_rule rule
|
blanchet@56097
|
229 |
|
blanchet@56621
|
230 |
val deps = fold add_fact_of_dependencies gamma ([], [])
|
blanchet@56586
|
231 |
val meths =
|
blanchet@56615
|
232 |
(if skolem then skolem_methods
|
blanchet@56615
|
233 |
else if is_arith_rule rule then arith_methods
|
blanchet@56615
|
234 |
else if is_datatype_rule rule then datatype_methods
|
blanchet@56653
|
235 |
else systematic_methods)
|
blanchet@56653
|
236 |
|> massage_methods
|
blanchet@56622
|
237 |
|
blanchet@56641
|
238 |
fun prove sub facts = Prove (maybe_show outer c [], [], l, t, sub, facts, meths, "")
|
blanchet@56622
|
239 |
fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs
|
blanchet@56042
|
240 |
in
|
blanchet@56042
|
241 |
if is_clause_tainted c then
|
blanchet@56054
|
242 |
(case gamma of
|
blanchet@56042
|
243 |
[g] =>
|
blanchet@56097
|
244 |
if skolem andalso is_clause_tainted g then
|
blanchet@56093
|
245 |
let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in
|
blanchet@56622
|
246 |
isar_steps outer (SOME l) [prove [subproof] ([], [])] infs
|
blanchet@56042
|
247 |
end
|
blanchet@52285
|
248 |
else
|
blanchet@56622
|
249 |
steps_of_rest (prove [] deps)
|
blanchet@56622
|
250 |
| _ => steps_of_rest (prove [] deps))
|
blanchet@56042
|
251 |
else
|
blanchet@56641
|
252 |
steps_of_rest (if skolem then Prove ([], skolems_of t, l, t, [], deps, meths, "")
|
blanchet@56622
|
253 |
else prove [] deps)
|
blanchet@56042
|
254 |
end
|
blanchet@56042
|
255 |
| isar_steps outer predecessor accum (Cases cases :: infs) =
|
blanchet@56042
|
256 |
let
|
blanchet@56528
|
257 |
fun isar_case (c, subinfs) =
|
blanchet@56528
|
258 |
isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs
|
blanchet@56042
|
259 |
val c = succedent_of_cases cases
|
blanchet@56042
|
260 |
val l = label_of_clause c
|
blanchet@56042
|
261 |
val t = prop_of_clause c
|
blanchet@56042
|
262 |
val step =
|
blanchet@56102
|
263 |
Prove (maybe_show outer c [], [], l, t,
|
blanchet@56102
|
264 |
map isar_case (filter_out (null o snd) cases),
|
blanchet@56653
|
265 |
(the_list predecessor, []), massage_methods systematic_methods, "")
|
blanchet@56042
|
266 |
in
|
blanchet@56042
|
267 |
isar_steps outer (SOME l) (step :: accum) infs
|
blanchet@56042
|
268 |
end
|
blanchet@56042
|
269 |
and isar_proof outer fix assms lems infs =
|
blanchet@56042
|
270 |
Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
|
blanchet@56042
|
271 |
|
blanchet@56564
|
272 |
val trace = Config.get ctxt trace
|
blanchet@56556
|
273 |
|
blanchet@56598
|
274 |
val canonical_isar_proof =
|
blanchet@52282
|
275 |
refute_graph
|
blanchet@56556
|
276 |
|> trace ? tap (tracing o prefix "Refute graph: " o string_of_refute_graph)
|
blanchet@52213
|
277 |
|> redirect_graph axioms tainted bot
|
blanchet@56556
|
278 |
|> trace ? tap (tracing o prefix "Direct proof: " o string_of_direct_proof)
|
blanchet@56096
|
279 |
|> isar_proof true params assms lems
|
blanchet@56555
|
280 |
|> postprocess_isar_proof_remove_unreferenced_steps I
|
blanchet@56555
|
281 |
|> relabel_isar_proof_canonically
|
blanchet@56556
|
282 |
|
blanchet@56628
|
283 |
val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof
|
blanchet@56598
|
284 |
|
blanchet@56602
|
285 |
val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
|
blanchet@56602
|
286 |
|
blanchet@56606
|
287 |
val _ = fold_isar_steps (fn meth =>
|
blanchet@58396
|
288 |
K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth []))
|
blanchet@56602
|
289 |
(steps_of_isar_proof canonical_isar_proof) ()
|
blanchet@56556
|
290 |
|
blanchet@56565
|
291 |
fun str_of_preplay_outcome outcome =
|
blanchet@56565
|
292 |
if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
|
blanchet@56565
|
293 |
fun str_of_meth l meth =
|
blanchet@58327
|
294 |
string_of_proof_method ctxt [] meth ^ " " ^
|
blanchet@56608
|
295 |
str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)
|
blanchet@56586
|
296 |
fun comment_of l = map (str_of_meth l) #> commas
|
blanchet@56564
|
297 |
|
blanchet@56556
|
298 |
fun trace_isar_proof label proof =
|
blanchet@56556
|
299 |
if trace then
|
blanchet@56641
|
300 |
tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^
|
blanchet@57439
|
301 |
string_of_isar_proof ctxt subgoal subgoal_count
|
blanchet@57439
|
302 |
(comment_isar_proof comment_of proof) ^ "\n")
|
blanchet@56556
|
303 |
else
|
blanchet@56556
|
304 |
()
|
blanchet@56096
|
305 |
|
blanchet@56641
|
306 |
fun comment_of l (meth :: _) =
|
blanchet@56641
|
307 |
(case (verbose,
|
blanchet@56641
|
308 |
Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)) of
|
blanchet@56641
|
309 |
(false, Played _) => ""
|
blanchet@56641
|
310 |
| (_, outcome) => string_of_play_outcome outcome)
|
blanchet@56641
|
311 |
|
blanchet@56170
|
312 |
val (play_outcome, isar_proof) =
|
blanchet@56598
|
313 |
canonical_isar_proof
|
blanchet@56556
|
314 |
|> tap (trace_isar_proof "Original")
|
blanchet@58587
|
315 |
|> compress_isar_proof ctxt compress preplay_timeout 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@58396
|
319 |
#> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
|
blanchet@56556
|
320 |
|> tap (trace_isar_proof "Minimized")
|
blanchet@58587
|
321 |
(* It's not clear whether this is worth the trouble (and if so, "compress" has an
|
blanchet@56671
|
322 |
unnatural semantics): *)
|
blanchet@56671
|
323 |
(*
|
blanchet@56669
|
324 |
|> minimize
|
blanchet@58587
|
325 |
? (compress_isar_proof ctxt compress preplay_timeout preplay_data
|
blanchet@56669
|
326 |
#> tap (trace_isar_proof "Compressed again"))
|
blanchet@56671
|
327 |
*)
|
blanchet@56602
|
328 |
|> `(preplay_outcome_of_isar_proof (!preplay_data))
|
blanchet@56667
|
329 |
||> (comment_isar_proof comment_of
|
blanchet@56667
|
330 |
#> chain_isar_proof
|
blanchet@56667
|
331 |
#> kill_useless_labels_in_isar_proof
|
blanchet@56667
|
332 |
#> relabel_isar_proof_nicely)
|
blanchet@50898
|
333 |
in
|
blanchet@58629
|
334 |
(case add_isar_steps (steps_of_isar_proof isar_proof) 0 of
|
blanchet@58629
|
335 |
1 =>
|
blanchet@58629
|
336 |
one_line_proof_text ctxt 0
|
blanchet@58629
|
337 |
(if play_outcome_ord (play_outcome, one_line_play) = LESS then
|
blanchet@58629
|
338 |
(case isar_proof of
|
blanchet@58629
|
339 |
Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) =>
|
blanchet@58629
|
340 |
let val used_facts' = filter (member (op =) gfs o fst) used_facts in
|
blanchet@58629
|
341 |
((meth, play_outcome), banner, used_facts', minimize_command, subgoal,
|
blanchet@58629
|
342 |
subgoal_count)
|
blanchet@58629
|
343 |
end)
|
blanchet@58629
|
344 |
else
|
blanchet@58629
|
345 |
one_line_params) ^
|
blanchet@58629
|
346 |
(if isar_proofs = SOME true then "\n(No structured proof available -- proof too simple.)"
|
blanchet@58629
|
347 |
else "")
|
blanchet@58629
|
348 |
| num_steps =>
|
blanchet@58629
|
349 |
let
|
blanchet@58629
|
350 |
val msg =
|
blanchet@58629
|
351 |
(if verbose then [string_of_int num_steps ^ " step" ^ plural_s num_steps] else []) @
|
blanchet@58629
|
352 |
(if do_preplay then [string_of_play_outcome play_outcome] else [])
|
blanchet@58629
|
353 |
in
|
blanchet@58629
|
354 |
one_line_proof_text ctxt 0 one_line_params ^
|
blanchet@58629
|
355 |
"\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
|
blanchet@58629
|
356 |
Active.sendback_markup [Markup.padding_command]
|
blanchet@58629
|
357 |
(string_of_isar_proof ctxt subgoal subgoal_count isar_proof)
|
blanchet@58629
|
358 |
end)
|
blanchet@50898
|
359 |
end
|
blanchet@58398
|
360 |
in
|
blanchet@58629
|
361 |
if debug then
|
blanchet@58629
|
362 |
generate_proof_text ()
|
blanchet@58629
|
363 |
else
|
blanchet@58629
|
364 |
(case try generate_proof_text () of
|
blanchet@58629
|
365 |
SOME s => s
|
blanchet@58629
|
366 |
| NONE =>
|
blanchet@58629
|
367 |
one_line_proof_text ctxt 0 one_line_params ^
|
blanchet@58629
|
368 |
(if isar_proofs = SOME true then "\nWarning: Isar proof construction failed." else ""))
|
blanchet@58398
|
369 |
end
|
blanchet@50898
|
370 |
|
blanchet@56639
|
371 |
fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =
|
blanchet@56166
|
372 |
(case play of
|
blanchet@57423
|
373 |
Played _ => meth = SMT2_Method andalso smt_proofs <> SOME true
|
blanchet@57435
|
374 |
| Play_Timed_Out time => Time.> (time, Time.zeroTime)
|
blanchet@57435
|
375 |
| Play_Failed => true)
|
blanchet@52324
|
376 |
|
blanchet@56639
|
377 |
fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
|
blanchet@56598
|
378 |
(one_line_params as (preplay, _, _, _, _, _)) =
|
blanchet@52327
|
379 |
(if isar_proofs = SOME true orelse
|
blanchet@56639
|
380 |
(isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt_proofs preplay) then
|
blanchet@56639
|
381 |
isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
|
blanchet@50898
|
382 |
else
|
blanchet@58327
|
383 |
one_line_proof_text ctxt num_chained) one_line_params
|
blanchet@50898
|
384 |
|
blanchet@50898
|
385 |
end;
|