221 (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ |
219 (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ |
222 do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^ |
220 do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^ |
223 (if n <> 1 then "next" else "qed") |
221 (if n <> 1 then "next" else "qed") |
224 in do_proof end |
222 in do_proof end |
225 |
223 |
226 fun min_local ctxt type_enc lam_trans proof = |
224 fun minimize_locally ctxt type_enc lam_trans proof = |
227 let |
225 let |
228 (* Merging spots, greedy algorithm *) |
226 (* Merging spots, greedy algorithm *) |
229 fun cost (Prove (_, _ , t, _)) = Term.size_of_term t |
227 fun cost (Prove (_, _ , t, _)) = Term.size_of_term t |
230 | cost _ = ~1 |
228 | cost _ = ~1 |
231 fun can_merge (Prove (_, lbl, _, By_Metis _)) (Prove (_, _, _, By_Metis _)) = |
229 fun can_merge (Prove (_, lbl, _, By_Metis _)) |
232 (lbl = no_label) |
230 (Prove (_, _, _, By_Metis _)) = |
|
231 (lbl = no_label) |
233 | can_merge _ _ = false |
232 | can_merge _ _ = false |
234 val merge_spots = |
233 val merge_spots = |
235 fold_index |
234 fold_index (fn (i, s2) => fn (s1, pile) => |
236 (fn (i, s2) => fn (s1, pile) => (s2, pile |> can_merge s1 s2 ? cons (i, cost s1))) |
235 (s2, pile |> can_merge s1 s2 ? cons (i, cost s1))) |
237 (tl proof) (hd proof, []) |
236 (tl proof) (hd proof, []) |
238 |> snd |> sort (rev_order o int_ord o pairself snd) |> map fst |
237 |> snd |> sort (rev_order o int_ord o pairself snd) |> map fst |
239 |
238 |
240 (* Enrich context with facts *) |
239 (* Enrich context with facts *) |
241 val thy = Proof_Context.theory_of ctxt |
240 val thy = Proof_Context.theory_of ctxt |
242 fun sorry t = Skip_Proof.make_thm thy (HOLogic.mk_Trueprop t) (* FIXME: mk_Trueprop always ok? *) |
241 fun sorry t = Skip_Proof.make_thm thy (HOLogic.mk_Trueprop t) (* FIXME: mk_Trueprop always ok? *) |
243 fun enrich_ctxt' (Prove (_, lbl, t, _)) ctxt = |
242 fun enrich_ctxt' (Prove (_, lbl, t, _)) ctxt = |
244 if lbl = no_label then ctxt |
243 ctxt |> lbl <> no_label |
245 else Proof_Context.put_thms false (string_for_label lbl, SOME [sorry t]) ctxt |
244 ? Proof_Context.put_thms false (string_for_label lbl, SOME [sorry t]) |
246 | enrich_ctxt' _ ctxt = ctxt |
245 | enrich_ctxt' _ ctxt = ctxt |
247 val rich_ctxt = fold enrich_ctxt' proof ctxt |
246 val rich_ctxt = fold enrich_ctxt' proof ctxt |
248 |
247 |
249 (* Timing *) |
248 (* Timing *) |
250 fun take_time tac arg = |
249 fun take_time tac arg = |
254 (tac arg ; Timing.result t_start |> #cpu) |
253 (tac arg ; Timing.result t_start |> #cpu) |
255 end |
254 end |
256 fun try_metis (Prove (qs, _, t, By_Metis fact_names)) s0 = |
255 fun try_metis (Prove (qs, _, t, By_Metis fact_names)) s0 = |
257 let |
256 let |
258 fun thmify (Prove (_, _, t, _)) = sorry t |
257 fun thmify (Prove (_, _, t, _)) = sorry t |
259 val facts = fact_names |>> map string_for_label |
258 val facts = |
260 |> op@ |
259 fact_names |
261 |> map (Proof_Context.get_thm rich_ctxt) |
260 |>> map string_for_label |
262 |> (if member op= qs Then |
261 |> op @ |
263 then cons (the s0 |> thmify) |
262 |> map (Proof_Context.get_thm rich_ctxt) |
264 else I) |
263 |> (if member (op =) qs Then then cons (the s0 |> thmify) else I) |
265 val goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop t) (* FIXME: mk_Trueprop always ok? *) |
264 val goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop t) (* FIXME: mk_Trueprop always ok? *) |
266 fun tac {context = ctxt, prems = _} = |
265 fun tac {context = ctxt, prems = _} = |
267 Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 |
266 Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 |
268 in |
267 in |
269 take_time (fn () => goal tac) |
268 take_time (fn () => goal tac) |
271 |
270 |
272 (* Merging *) |
271 (* Merging *) |
273 fun merge (Prove (qs1, _, _, By_Metis (ls1, ss1))) |
272 fun merge (Prove (qs1, _, _, By_Metis (ls1, ss1))) |
274 (Prove (qs2, lbl , t, By_Metis (ls2, ss2))) = |
273 (Prove (qs2, lbl , t, By_Metis (ls2, ss2))) = |
275 let |
274 let |
276 val qs = (inter op= qs1 qs2) (* FIXME: Is this correct? *) |
275 val qs = |
277 |> member op= (union op= qs1 qs2) Ultimately ? cons Ultimately |
276 inter (op =) qs1 qs2 (* FIXME: Is this correct? *) |
278 |> member op= qs2 Show ? cons Show |
277 |> member (op =) (union (op =) qs1 qs2) Ultimately ? cons Ultimately |
279 in Prove (qs, lbl, t, By_Metis (ls1@ls2, ss1@ss2)) end |
278 |> member (op =) qs2 Show ? cons Show |
|
279 in Prove (qs, lbl, t, By_Metis (ls1 @ ls2, ss1 @ ss2)) end |
280 fun try_merge proof i = |
280 fun try_merge proof i = |
281 let |
281 let |
282 val (front, s0, s1, s2, tail) = |
282 val (front, s0, s1, s2, tail) = |
283 case (proof, i) of |
283 case (proof, i) of |
284 ((s1::s2::proof), 0) => ([], NONE, s1, s2, proof) |
284 ((s1 :: s2 :: proof), 0) => ([], NONE, s1, s2, proof) |
285 | _ => let val (front, s0::s1::s2::tail) = chop (i-1) proof |
285 | _ => |
286 in (front, SOME s0, s1, s2, tail) end |
286 let val (front, s0 :: s1 :: s2 :: tail) = chop (i - 1) proof in |
|
287 (front, SOME s0, s1, s2, tail) |
|
288 end |
287 val s12 = merge s1 s2 |
289 val s12 = merge s1 s2 |
288 val t1 = try_metis s1 s0 () |
290 val t1 = try_metis s1 s0 () |
289 val t2 = try_metis s2 (SOME s1) () |
291 val t2 = try_metis s2 (SOME s1) () |
290 val tlimit = t1 + t2 |> Time.toReal |> curry Real.* 1.2 |> Time.fromReal |
292 val tlimit = t1 + t2 |> Time.toReal |> curry Real.* 1.2 |> Time.fromReal |
291 in |
293 in |
292 (TimeLimit.timeLimit tlimit (try_metis s12 s0) (); |
294 (TimeLimit.timeLimit tlimit (try_metis s12 s0) (); |
293 SOME (front @ (case s0 of NONE => s12::tail | SOME s => s::s12::tail))) |
295 SOME (front @ (case s0 of |
|
296 NONE => s12 :: tail |
|
297 | SOME s => s :: s12 :: tail))) |
294 handle _ => NONE |
298 handle _ => NONE |
295 end |
299 end |
296 fun merge_steps proof [] = proof |
300 fun merge_steps proof [] = proof |
297 | merge_steps proof (i::is) = |
301 | merge_steps proof (i :: is) = |
298 case try_merge proof i of |
302 case try_merge proof i of |
299 NONE => merge_steps proof is |
303 NONE => merge_steps proof is |
300 | SOME proof' => merge_steps proof' (map (fn j => if j>i then j-1 else j) is) |
304 | SOME proof' => |
|
305 merge_steps proof' (map (fn j => if j > i then j - 1 else j) is) |
301 in merge_steps proof merge_spots end |
306 in merge_steps proof merge_spots end |
302 |
307 |
303 fun isar_proof_text ctxt isar_proof_requested |
308 fun isar_proof_text ctxt isar_proof_requested |
304 (debug, isar_shrink_factor, pool, fact_names, sym_tab, atp_proof, goal) |
309 (debug, isar_shrink_factor, pool, fact_names, sym_tab, atp_proof, goal) |
305 (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = |
310 (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = |