--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML Sun Dec 15 18:01:38 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML Sun Dec 15 18:01:38 2013 +0100
@@ -76,9 +76,10 @@
let
fun add_edge to from =
Atom_Graph.default_node (from, ())
- #> Atom_Graph.default_node (to, ())
#> Atom_Graph.add_edge_acyclic (from, to)
- fun add_infer (froms, to) = fold (add_edge to) froms
+ fun add_infer (froms, to) =
+ Atom_Graph.default_node (to, ())
+ #> fold (add_edge to) froms
val graph = fold add_infer infers Atom_Graph.empty
val reachable = Atom_Graph.all_preds graph [bot]
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Sun Dec 15 18:01:38 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Sun Dec 15 18:01:38 2013 +0100
@@ -55,17 +55,18 @@
let val (refed, steps) = do_steps steps in
(refed, Proof (fix, assms, steps))
end
- and do_steps steps =
- let
- (* the last step is always implicitly referenced *)
- val (steps, (refed, concl)) =
- split_last steps
- ||> do_refed_step
- in
- fold_rev do_step steps (refed, [concl])
- end
+ and do_steps [] = ([], [])
+ | do_steps steps =
+ let
+ (* the last step is always implicitly referenced *)
+ val (steps, (refed, concl)) =
+ split_last steps
+ ||> do_refed_step
+ in
+ fold_rev do_step steps (refed, [concl])
+ end
and do_step step (refed, accu) =
- case label_of_step step of
+ (case label_of_step step of
NONE => (refed, step :: accu)
| SOME l =>
if Ord_List.member label_ord refed l then
@@ -73,7 +74,7 @@
|>> Ord_List.union label_ord refed
||> (fn x => x :: accu)
else
- (refed, accu)
+ (refed, accu))
and do_refed_step step = step |> postproc_step |> do_refed_step'
and do_refed_step' (Let _) = raise Fail "Sledgehammer_Minimize_Isar"
| do_refed_step' (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Sun Dec 15 18:01:38 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Sun Dec 15 18:01:38 2013 +0100
@@ -279,7 +279,8 @@
in
(* One-step Metis proofs are pointless; better use the one-liner directly. *)
(case proof of
- Proof ([], [], [Prove (_, [], _, _, [], (_, MetisM))]) => ""
+ Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *)
+ | Proof ([], [], [Prove (_, [], _, _, [], (_, MetisM))]) => ""
| _ =>
(if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sun Dec 15 18:01:38 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sun Dec 15 18:01:38 2013 +0100
@@ -323,10 +323,10 @@
val lits =
map (maybe_dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names)
in
- case List.partition (can HOLogic.dest_not) lits of
+ (case List.partition (can HOLogic.dest_not) lits of
(negs as _ :: _, pos as _ :: _) =>
s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos)
- | _ => fold (curry s_disj) lits @{term False}
+ | _ => fold (curry s_disj) lits @{term False})
end
|> HOLogic.mk_Trueprop |> close_form
@@ -380,15 +380,9 @@
and isar_proof outer fix assms lems infs =
Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
- val isar_proof_of_direct_proof = isar_proof true params assms lems
-
(* 60 seconds seems like a good interpreation of "no timeout" *)
val preplay_timeout = preplay_timeout |> the_default (seconds 60.0)
- val clean_up_labels_in_proof =
- chain_direct_proof
- #> kill_useless_labels_in_proof
- #> relabel_proof
val (preplay_interface as {overall_preplay_stats, ...}, isar_proof) =
refute_graph
(*
@@ -398,11 +392,12 @@
(*
|> tap (tracing o prefix "Direct proof: " o string_of_direct_proof)
*)
- |> isar_proof_of_direct_proof
+ |> isar_proof true params assms lems
|> postprocess_remove_unreferenced_steps I
|> relabel_proof_canonically
|> `(proof_preplay_interface debug ctxt metis_type_enc metis_lam_trans do_preplay
preplay_timeout)
+
val ((preplay_time, preplay_fail), isar_proof) =
isar_proof
|> compress_proof (if isar_proofs = SOME true then isar_compress else 1000.0)
@@ -410,11 +405,14 @@
|> isar_try0 ? try0 preplay_timeout preplay_interface
|> postprocess_remove_unreferenced_steps (isar_try0 ? min_deps_of_step preplay_interface)
|> `overall_preplay_stats
- ||> clean_up_labels_in_proof
+ ||> (chain_direct_proof
+ #> kill_useless_labels_in_proof
+ #> relabel_proof)
+
val isar_text =
string_of_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count isar_proof
in
- case isar_text of
+ (case isar_text of
"" =>
if isar_proofs = SOME true then
"\nNo structured proof available (proof too simple)."
@@ -437,24 +435,23 @@
in
"\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
Active.sendback_markup [Markup.padding_command] isar_text
- end
+ end)
end
val isar_proof =
if debug then
isar_proof_of ()
- else case try isar_proof_of () of
- SOME s => s
- | NONE => if isar_proofs = SOME true then
- "\nWarning: The Isar proof construction failed."
- else
- ""
+ else
+ (case try isar_proof_of () of
+ SOME s => s
+ | NONE =>
+ if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "")
in one_line_proof ^ isar_proof end
fun isar_proof_would_be_a_good_idea preplay =
- case preplay of
+ (case preplay of
Played (reconstr, _) => reconstr = SMT
| Trust_Playable _ => false
- | Failed_to_Play _ => true
+ | Failed_to_Play _ => true)
fun proof_text ctxt isar_proofs isar_params num_chained
(one_line_params as (preplay, _, _, _, _, _)) =