49883
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
|
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
|
3 |
Author: Steffen Juilf Smolka, TU Muenchen
|
|
4 |
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
|
|
8 |
sig
|
|
9 |
type isar_params = ATP_Proof_Reconstruct.isar_params
|
|
10 |
type one_line_params = ATP_Proof_Reconstruct.one_line_params
|
|
11 |
val isar_proof_text :
|
49913
|
12 |
Proof.context -> bool -> isar_params -> one_line_params -> string
|
49883
|
13 |
val proof_text :
|
49913
|
14 |
Proof.context -> bool -> isar_params -> int -> one_line_params -> string
|
49883
|
15 |
end;
|
|
16 |
|
|
17 |
structure Sledgehammer_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
|
|
18 |
struct
|
|
19 |
|
|
20 |
open ATP_Util
|
|
21 |
open ATP_Proof
|
|
22 |
open ATP_Problem_Generate
|
|
23 |
open ATP_Proof_Reconstruct
|
|
24 |
open String_Redirect
|
|
25 |
|
|
26 |
(** Type annotations **)
|
|
27 |
|
|
28 |
fun post_traverse_term_type' f _ (t as Const (_, T)) s = f t T s
|
|
29 |
| post_traverse_term_type' f _ (t as Free (_, T)) s = f t T s
|
|
30 |
| post_traverse_term_type' f _ (t as Var (_, T)) s = f t T s
|
|
31 |
| post_traverse_term_type' f env (t as Bound i) s = f t (nth env i) s
|
|
32 |
| post_traverse_term_type' f env (Abs (x, T1, b)) s =
|
|
33 |
let
|
|
34 |
val ((b', s'), T2) = post_traverse_term_type' f (T1 :: env) b s
|
|
35 |
in f (Abs (x, T1, b')) (T1 --> T2) s' end
|
|
36 |
| post_traverse_term_type' f env (u $ v) s =
|
|
37 |
let
|
|
38 |
val ((u', s'), Type (_, [_, T])) = post_traverse_term_type' f env u s
|
|
39 |
val ((v', s''), _) = post_traverse_term_type' f env v s'
|
|
40 |
in f (u' $ v') T s'' end
|
|
41 |
|
|
42 |
fun post_traverse_term_type f s t =
|
|
43 |
post_traverse_term_type' (fn t => fn T => fn s => (f t T s, T)) [] t s |> fst
|
|
44 |
fun post_fold_term_type f s t =
|
|
45 |
post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd
|
|
46 |
|
|
47 |
(* Data structures, orders *)
|
|
48 |
val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)
|
|
49 |
|
|
50 |
structure Var_Set_Tab = Table(
|
|
51 |
type key = indexname list
|
|
52 |
val ord = list_ord Term_Ord.fast_indexname_ord)
|
|
53 |
|
|
54 |
(* (1) Generalize Types *)
|
|
55 |
fun generalize_types ctxt t =
|
|
56 |
t |> map_types (fn _ => dummyT)
|
|
57 |
|> Syntax.check_term
|
|
58 |
(Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
|
|
59 |
|
|
60 |
(* (2) Typing-spot Table *)
|
|
61 |
local
|
|
62 |
fun key_of_atype (TVar (idxn, _)) =
|
|
63 |
Ord_List.insert Term_Ord.fast_indexname_ord idxn
|
|
64 |
| key_of_atype _ = I
|
|
65 |
fun key_of_type T = fold_atyps key_of_atype T []
|
|
66 |
fun update_tab t T (tab, pos) =
|
|
67 |
(case key_of_type T of
|
|
68 |
[] => tab
|
|
69 |
| key =>
|
|
70 |
let val cost = (size_of_typ T, (size_of_term t, pos)) in
|
|
71 |
case Var_Set_Tab.lookup tab key of
|
|
72 |
NONE => Var_Set_Tab.update_new (key, cost) tab
|
|
73 |
| SOME old_cost =>
|
|
74 |
(case cost_ord (cost, old_cost) of
|
|
75 |
LESS => Var_Set_Tab.update (key, cost) tab
|
|
76 |
| _ => tab)
|
|
77 |
end,
|
|
78 |
pos + 1)
|
|
79 |
in
|
|
80 |
val typing_spot_table =
|
|
81 |
post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst
|
|
82 |
end
|
|
83 |
|
|
84 |
(* (3) Reverse-Greedy *)
|
|
85 |
fun reverse_greedy typing_spot_tab =
|
|
86 |
let
|
|
87 |
fun update_count z =
|
|
88 |
fold (fn tvar => fn tab =>
|
|
89 |
let val c = Vartab.lookup tab tvar |> the_default 0 in
|
|
90 |
Vartab.update (tvar, c + z) tab
|
|
91 |
end)
|
|
92 |
fun superfluous tcount =
|
|
93 |
forall (fn tvar => the (Vartab.lookup tcount tvar) > 1)
|
|
94 |
fun drop_superfluous (tvars, (_, (_, spot))) (spots, tcount) =
|
|
95 |
if superfluous tcount tvars then (spots, update_count ~1 tvars tcount)
|
|
96 |
else (spot :: spots, tcount)
|
|
97 |
val (typing_spots, tvar_count_tab) =
|
|
98 |
Var_Set_Tab.fold
|
|
99 |
(fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k))
|
|
100 |
typing_spot_tab ([], Vartab.empty)
|
|
101 |
|>> sort_distinct (rev_order o cost_ord o pairself snd)
|
|
102 |
in fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst end
|
|
103 |
|
|
104 |
(* (4) Introduce Annotations *)
|
|
105 |
fun introduce_annotations thy spots t t' =
|
|
106 |
let
|
|
107 |
val get_types = post_fold_term_type (K cons) []
|
|
108 |
fun match_types tp =
|
|
109 |
fold (Sign.typ_match thy) (op ~~ (pairself get_types tp)) Vartab.empty
|
|
110 |
fun unica' b x [] = if b then [x] else []
|
|
111 |
| unica' b x (y :: ys) =
|
|
112 |
if x = y then unica' false x ys
|
|
113 |
else unica' true y ys |> b ? cons x
|
|
114 |
fun unica ord xs =
|
|
115 |
case sort ord xs of x :: ys => unica' true x ys | [] => []
|
|
116 |
val add_all_tfree_namesT = fold_atyps (fn TFree (x, _) => cons x | _ => I)
|
|
117 |
fun erase_unica_tfrees env =
|
|
118 |
let
|
|
119 |
val unica =
|
|
120 |
Vartab.fold (add_all_tfree_namesT o snd o snd) env []
|
|
121 |
|> unica fast_string_ord
|
|
122 |
val erase_unica = map_atyps
|
|
123 |
(fn T as TFree (s, _) =>
|
|
124 |
if Ord_List.member fast_string_ord unica s then dummyT else T
|
|
125 |
| T => T)
|
|
126 |
in Vartab.map (K (apsnd erase_unica)) env end
|
|
127 |
val env = match_types (t', t) |> erase_unica_tfrees
|
|
128 |
fun get_annot env (TFree _) = (false, (env, dummyT))
|
|
129 |
| get_annot env (T as TVar (v, S)) =
|
|
130 |
let val T' = Envir.subst_type env T in
|
|
131 |
if T' = dummyT then (false, (env, dummyT))
|
|
132 |
else (true, (Vartab.update (v, (S, dummyT)) env, T'))
|
|
133 |
end
|
|
134 |
| get_annot env (Type (S, Ts)) =
|
|
135 |
(case fold_rev (fn T => fn (b, (env, Ts)) =>
|
|
136 |
let
|
|
137 |
val (b', (env', T)) = get_annot env T
|
|
138 |
in (b orelse b', (env', T :: Ts)) end)
|
|
139 |
Ts (false, (env, [])) of
|
|
140 |
(true, (env', Ts)) => (true, (env', Type (S, Ts)))
|
|
141 |
| (false, (env', _)) => (false, (env', dummyT)))
|
|
142 |
fun post1 _ T (env, cp, ps as p :: ps', annots) =
|
|
143 |
if p <> cp then
|
|
144 |
(env, cp + 1, ps, annots)
|
|
145 |
else
|
|
146 |
let val (_, (env', T')) = get_annot env T in
|
|
147 |
(env', cp + 1, ps', (p, T') :: annots)
|
|
148 |
end
|
|
149 |
| post1 _ _ accum = accum
|
|
150 |
val (_, _, _, annots) = post_fold_term_type post1 (env, 0, spots, []) t'
|
|
151 |
fun post2 t _ (cp, annots as (p, T) :: annots') =
|
|
152 |
if p <> cp then (t, (cp + 1, annots))
|
|
153 |
else (Type.constraint T t, (cp + 1, annots'))
|
|
154 |
| post2 t _ x = (t, x)
|
|
155 |
in post_traverse_term_type post2 (0, rev annots) t |> fst end
|
|
156 |
|
|
157 |
(* (5) Annotate *)
|
|
158 |
fun annotate_types ctxt t =
|
|
159 |
let
|
|
160 |
val thy = Proof_Context.theory_of ctxt
|
|
161 |
val t' = generalize_types ctxt t
|
|
162 |
val typing_spots =
|
|
163 |
t' |> typing_spot_table
|
|
164 |
|> reverse_greedy
|
|
165 |
|> sort int_ord
|
|
166 |
in introduce_annotations thy typing_spots t t' end
|
|
167 |
|
|
168 |
fun string_for_proof ctxt type_enc lam_trans i n =
|
|
169 |
let
|
|
170 |
fun fix_print_mode f x =
|
|
171 |
Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
|
|
172 |
(print_mode_value ())) f x
|
|
173 |
fun do_indent ind = replicate_string (ind * indent_size) " "
|
|
174 |
fun do_free (s, T) =
|
|
175 |
maybe_quote s ^ " :: " ^
|
|
176 |
maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
|
|
177 |
fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
|
|
178 |
fun do_have qs =
|
|
179 |
(if member (op =) qs Moreover then "moreover " else "") ^
|
|
180 |
(if member (op =) qs Ultimately then "ultimately " else "") ^
|
|
181 |
(if member (op =) qs Then then
|
|
182 |
if member (op =) qs Show then "thus" else "hence"
|
|
183 |
else
|
|
184 |
if member (op =) qs Show then "show" else "have")
|
|
185 |
val do_term =
|
|
186 |
maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
|
|
187 |
o annotate_types ctxt
|
|
188 |
val reconstr = Metis (type_enc, lam_trans)
|
|
189 |
fun do_facts (ls, ss) =
|
|
190 |
reconstructor_command reconstr 1 1 [] 0
|
|
191 |
(ls |> sort_distinct (prod_ord string_ord int_ord),
|
|
192 |
ss |> sort_distinct string_ord)
|
|
193 |
and do_step ind (Fix xs) =
|
|
194 |
do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
|
|
195 |
| do_step ind (Let (t1, t2)) =
|
|
196 |
do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
|
|
197 |
| do_step ind (Assume (l, t)) =
|
|
198 |
do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
|
|
199 |
| do_step ind (Prove (qs, l, t, By_Metis facts)) =
|
|
200 |
do_indent ind ^ do_have qs ^ " " ^
|
|
201 |
do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
|
|
202 |
| do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) =
|
|
203 |
implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind)
|
|
204 |
proofs) ^
|
|
205 |
do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
|
|
206 |
do_facts facts ^ "\n"
|
|
207 |
and do_steps prefix suffix ind steps =
|
|
208 |
let val s = implode (map (do_step ind) steps) in
|
|
209 |
replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
|
|
210 |
String.extract (s, ind * indent_size,
|
|
211 |
SOME (size s - ind * indent_size - 1)) ^
|
|
212 |
suffix ^ "\n"
|
|
213 |
end
|
|
214 |
and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
|
|
215 |
(* One-step proofs are pointless; better use the Metis one-liner
|
|
216 |
directly. *)
|
|
217 |
and do_proof [Prove (_, _, _, By_Metis _)] = ""
|
|
218 |
| do_proof proof =
|
|
219 |
(if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
|
|
220 |
do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^
|
|
221 |
(if n <> 1 then "next" else "qed")
|
|
222 |
in do_proof end
|
|
223 |
|
49913
|
224 |
fun minimize_locally ctxt type_enc lam_trans proof =
|
49883
|
225 |
let
|
|
226 |
(* Merging spots, greedy algorithm *)
|
|
227 |
fun cost (Prove (_, _ , t, _)) = Term.size_of_term t
|
|
228 |
| cost _ = ~1
|
49913
|
229 |
fun can_merge (Prove (_, lbl, _, By_Metis _))
|
|
230 |
(Prove (_, _, _, By_Metis _)) =
|
|
231 |
(lbl = no_label)
|
49883
|
232 |
| can_merge _ _ = false
|
|
233 |
val merge_spots =
|
49913
|
234 |
fold_index (fn (i, s2) => fn (s1, pile) =>
|
|
235 |
(s2, pile |> can_merge s1 s2 ? cons (i, cost s1)))
|
49883
|
236 |
(tl proof) (hd proof, [])
|
|
237 |
|> snd |> sort (rev_order o int_ord o pairself snd) |> map fst
|
|
238 |
|
|
239 |
(* Enrich context with facts *)
|
|
240 |
val thy = Proof_Context.theory_of ctxt
|
|
241 |
fun sorry t = Skip_Proof.make_thm thy (HOLogic.mk_Trueprop t) (* FIXME: mk_Trueprop always ok? *)
|
|
242 |
fun enrich_ctxt' (Prove (_, lbl, t, _)) ctxt =
|
49913
|
243 |
ctxt |> lbl <> no_label
|
|
244 |
? Proof_Context.put_thms false (string_for_label lbl, SOME [sorry t])
|
49883
|
245 |
| enrich_ctxt' _ ctxt = ctxt
|
|
246 |
val rich_ctxt = fold enrich_ctxt' proof ctxt
|
|
247 |
|
|
248 |
(* Timing *)
|
|
249 |
fun take_time tac arg =
|
|
250 |
let
|
|
251 |
val t_start = Timing.start ()
|
|
252 |
in
|
|
253 |
(tac arg ; Timing.result t_start |> #cpu)
|
|
254 |
end
|
|
255 |
fun try_metis (Prove (qs, _, t, By_Metis fact_names)) s0 =
|
|
256 |
let
|
|
257 |
fun thmify (Prove (_, _, t, _)) = sorry t
|
49913
|
258 |
val facts =
|
|
259 |
fact_names
|
|
260 |
|>> map string_for_label
|
|
261 |
|> op @
|
|
262 |
|> map (Proof_Context.get_thm rich_ctxt)
|
|
263 |
|> (if member (op =) qs Then then cons (the s0 |> thmify) else I)
|
49883
|
264 |
val goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop t) (* FIXME: mk_Trueprop always ok? *)
|
|
265 |
fun tac {context = ctxt, prems = _} =
|
|
266 |
Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
|
|
267 |
in
|
|
268 |
take_time (fn () => goal tac)
|
|
269 |
end
|
|
270 |
|
|
271 |
(* Merging *)
|
|
272 |
fun merge (Prove (qs1, _, _, By_Metis (ls1, ss1)))
|
|
273 |
(Prove (qs2, lbl , t, By_Metis (ls2, ss2))) =
|
|
274 |
let
|
49913
|
275 |
val qs =
|
|
276 |
inter (op =) qs1 qs2 (* FIXME: Is this correct? *)
|
|
277 |
|> member (op =) (union (op =) qs1 qs2) Ultimately ? cons Ultimately
|
|
278 |
|> member (op =) qs2 Show ? cons Show
|
|
279 |
in Prove (qs, lbl, t, By_Metis (ls1 @ ls2, ss1 @ ss2)) end
|
49883
|
280 |
fun try_merge proof i =
|
|
281 |
let
|
|
282 |
val (front, s0, s1, s2, tail) =
|
|
283 |
case (proof, i) of
|
49913
|
284 |
((s1 :: s2 :: proof), 0) => ([], NONE, s1, s2, proof)
|
|
285 |
| _ =>
|
|
286 |
let val (front, s0 :: s1 :: s2 :: tail) = chop (i - 1) proof in
|
|
287 |
(front, SOME s0, s1, s2, tail)
|
|
288 |
end
|
49883
|
289 |
val s12 = merge s1 s2
|
|
290 |
val t1 = try_metis s1 s0 ()
|
|
291 |
val t2 = try_metis s2 (SOME s1) ()
|
|
292 |
val tlimit = t1 + t2 |> Time.toReal |> curry Real.* 1.2 |> Time.fromReal
|
|
293 |
in
|
|
294 |
(TimeLimit.timeLimit tlimit (try_metis s12 s0) ();
|
49913
|
295 |
SOME (front @ (case s0 of
|
|
296 |
NONE => s12 :: tail
|
|
297 |
| SOME s => s :: s12 :: tail)))
|
49883
|
298 |
handle _ => NONE
|
|
299 |
end
|
|
300 |
fun merge_steps proof [] = proof
|
49913
|
301 |
| merge_steps proof (i :: is) =
|
49883
|
302 |
case try_merge proof i of
|
|
303 |
NONE => merge_steps proof is
|
49913
|
304 |
| SOME proof' =>
|
|
305 |
merge_steps proof' (map (fn j => if j > i then j - 1 else j) is)
|
49883
|
306 |
in merge_steps proof merge_spots end
|
|
307 |
|
|
308 |
fun isar_proof_text ctxt isar_proof_requested
|
|
309 |
(debug, isar_shrink_factor, pool, fact_names, sym_tab, atp_proof, goal)
|
|
310 |
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
|
|
311 |
let
|
|
312 |
val isar_shrink_factor =
|
|
313 |
(if isar_proof_requested then 1 else 2) * isar_shrink_factor
|
|
314 |
val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
|
|
315 |
val frees = fold Term.add_frees (concl_t :: hyp_ts) []
|
|
316 |
val one_line_proof = one_line_proof_text 0 one_line_params
|
|
317 |
val type_enc =
|
|
318 |
if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
|
|
319 |
else partial_typesN
|
|
320 |
val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans
|
|
321 |
|
|
322 |
fun isar_proof_of () =
|
|
323 |
let
|
|
324 |
val atp_proof =
|
|
325 |
atp_proof
|
|
326 |
|> clean_up_atp_proof_dependencies
|
|
327 |
|> nasty_atp_proof pool
|
|
328 |
|> map_term_names_in_atp_proof repair_name
|
|
329 |
|> decode_lines ctxt sym_tab
|
|
330 |
|> rpair [] |-> fold_rev (add_line fact_names)
|
|
331 |
|> repair_waldmeister_endgame
|
|
332 |
|> rpair [] |-> fold_rev add_nontrivial_line
|
|
333 |
|> rpair (0, [])
|
|
334 |
|-> fold_rev (add_desired_line isar_shrink_factor fact_names frees)
|
|
335 |
|> snd
|
|
336 |
val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts)
|
|
337 |
val conjs =
|
|
338 |
atp_proof
|
|
339 |
|> map_filter (fn Inference_Step (name as (_, ss), _, _, []) =>
|
|
340 |
if member (op =) ss conj_name then SOME name else NONE
|
|
341 |
| _ => NONE)
|
|
342 |
fun dep_of_step (Definition_Step _) = NONE
|
|
343 |
| dep_of_step (Inference_Step (name, _, _, from)) = SOME (from, name)
|
|
344 |
val ref_graph = atp_proof |> map_filter dep_of_step |> make_ref_graph
|
|
345 |
val axioms = axioms_of_ref_graph ref_graph conjs
|
|
346 |
val tainted = tainted_atoms_of_ref_graph ref_graph conjs
|
|
347 |
val props =
|
|
348 |
Symtab.empty
|
|
349 |
|> fold (fn Definition_Step _ => I (* FIXME *)
|
|
350 |
| Inference_Step ((s, _), t, _, _) =>
|
|
351 |
Symtab.update_new (s,
|
|
352 |
t |> fold forall_of (map Var (Term.add_vars t []))
|
|
353 |
|> member (op = o apsnd fst) tainted s ? s_not))
|
|
354 |
atp_proof
|
|
355 |
fun prop_of_clause c =
|
|
356 |
fold (curry s_disj) (map_filter (Symtab.lookup props o fst) c)
|
|
357 |
@{term False}
|
|
358 |
fun label_of_clause [name] = raw_label_for_name name
|
|
359 |
| label_of_clause c = (space_implode "___" (map fst c), 0)
|
|
360 |
fun maybe_show outer c =
|
|
361 |
(outer andalso length c = 1 andalso subset (op =) (c, conjs))
|
|
362 |
? cons Show
|
|
363 |
fun do_have outer qs (gamma, c) =
|
|
364 |
Prove (maybe_show outer c qs, label_of_clause c, prop_of_clause c,
|
|
365 |
By_Metis (fold (add_fact_from_dependency fact_names
|
|
366 |
o the_single) gamma ([], [])))
|
|
367 |
fun do_inf outer (Have z) = do_have outer [] z
|
|
368 |
| do_inf outer (Hence z) = do_have outer [Then] z
|
|
369 |
| do_inf outer (Cases cases) =
|
|
370 |
let val c = succedent_of_cases cases in
|
|
371 |
Prove (maybe_show outer c [Ultimately], label_of_clause c,
|
|
372 |
prop_of_clause c,
|
|
373 |
Case_Split (map (do_case false) cases, ([], [])))
|
|
374 |
end
|
|
375 |
and do_case outer (c, infs) =
|
|
376 |
Assume (label_of_clause c, prop_of_clause c) ::
|
|
377 |
map (do_inf outer) infs
|
|
378 |
val isar_proof =
|
|
379 |
(if null params then [] else [Fix params]) @
|
|
380 |
(ref_graph
|
|
381 |
|> redirect_graph axioms tainted
|
|
382 |
|> chain_direct_proof
|
|
383 |
|> map (do_inf true)
|
|
384 |
|> kill_duplicate_assumptions_in_proof
|
|
385 |
|> kill_useless_labels_in_proof
|
|
386 |
|> relabel_proof
|
49913
|
387 |
|> minimize_locally ctxt type_enc lam_trans)
|
49883
|
388 |
|> string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
|
|
389 |
in
|
|
390 |
case isar_proof of
|
|
391 |
"" =>
|
|
392 |
if isar_proof_requested then
|
|
393 |
"\nNo structured proof available (proof too short)."
|
|
394 |
else
|
|
395 |
""
|
|
396 |
| _ =>
|
|
397 |
"\n\n" ^ (if isar_proof_requested then "Structured proof"
|
|
398 |
else "Perhaps this will work") ^
|
|
399 |
":\n" ^ Markup.markup Isabelle_Markup.sendback isar_proof
|
|
400 |
end
|
|
401 |
val isar_proof =
|
|
402 |
if debug then
|
|
403 |
isar_proof_of ()
|
|
404 |
else case try isar_proof_of () of
|
|
405 |
SOME s => s
|
|
406 |
| NONE => if isar_proof_requested then
|
|
407 |
"\nWarning: The Isar proof construction failed."
|
|
408 |
else
|
|
409 |
""
|
|
410 |
in one_line_proof ^ isar_proof end
|
|
411 |
|
|
412 |
fun proof_text ctxt isar_proof isar_params num_chained
|
|
413 |
(one_line_params as (preplay, _, _, _, _, _)) =
|
|
414 |
(if case preplay of Failed_to_Play _ => true | _ => isar_proof then
|
|
415 |
isar_proof_text ctxt isar_proof isar_params
|
|
416 |
else
|
|
417 |
one_line_proof_text num_chained) one_line_params
|
|
418 |
|
|
419 |
end;
|