--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Aug 28 16:58:27 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Aug 28 16:58:27 2014 +0200
@@ -242,11 +242,12 @@
end
|> HOLogic.mk_Trueprop |> finish_off
- fun maybe_show outer c = (outer andalso eq_set (op =) (c, conjs)) ? cons Show
+ fun maybe_show outer c = if outer andalso eq_set (op =) (c, conjs) then [Show] else []
fun isar_steps outer predecessor accum [] =
accum
|> (if tainted = [] then
+ (* e.g., trivial, empty proof by Z3 *)
cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
sort_facts (the_list predecessor, []), massage_methods systematic_methods', ""))
else
@@ -269,7 +270,7 @@
else systematic_methods')
|> massage_methods
- fun prove sub facts = Prove (maybe_show outer c [], [], l, t, sub, facts, meths, "")
+ fun prove sub facts = Prove (maybe_show outer c, [], l, t, sub, facts, meths, "")
fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs
in
if is_clause_tainted c then
@@ -302,7 +303,7 @@
val l = label_of_clause c
val t = prop_of_clause c
val step =
- Prove (maybe_show outer c [], [], l, t,
+ Prove (maybe_show outer c, [], l, t,
map isar_case (filter_out (null o snd) cases),
sort_facts (the_list predecessor, []), massage_methods systematic_methods', "")
in
@@ -319,6 +320,7 @@
|> redirect_graph axioms tainted bot
|> trace ? tap (tracing o prefix "Direct proof: " o string_of_direct_proof)
|> isar_proof true params assms lems
+ |> postprocess_isar_proof_remove_show_stuttering
|> postprocess_isar_proof_remove_unreferenced_steps I
|> relabel_isar_proof_canonically
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Thu Aug 28 16:58:27 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Thu Aug 28 16:58:27 2014 +0200
@@ -15,6 +15,7 @@
val minimized_isar_step : Proof.context -> Time.time -> isar_step -> Time.time * isar_step
val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data Unsynchronized.ref ->
isar_step -> isar_step
+ val postprocess_isar_proof_remove_show_stuttering : isar_proof -> isar_proof
val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof ->
isar_proof
end;
@@ -74,6 +75,18 @@
| _ => step (* don't touch steps that time out or fail *))
| minimize_isar_step_dependencies _ _ step = step
+fun postprocess_isar_proof_remove_show_stuttering (Proof (fix, assms, steps)) =
+ let
+ fun process_steps [] = []
+ | process_steps (steps as [Prove ([], [], l1, t1, subs1, facts1, meths1, comment1),
+ Prove ([Show], [], l2, t2, _, _, _, comment2)]) =
+ if t1 aconv t2 then [Prove ([Show], [], l2, t2, subs1, facts1, meths1, comment1 ^ comment2)]
+ else steps
+ | process_steps (step :: steps) = step :: process_steps steps
+ in
+ Proof (fix, assms, process_steps steps)
+ end
+
fun postprocess_isar_proof_remove_unreferenced_steps postproc_step =
let
fun process_proof (Proof (fix, assms, steps)) =
@@ -92,7 +105,7 @@
process_used_step step |>> Ord_List.union label_ord used ||> (fn step => step :: accu)
else
(used, accu))
- and process_used_step step = step |> postproc_step |> process_used_step_subproofs
+ and process_used_step step = process_used_step_subproofs (postproc_step step)
and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)) =
let
val (used, subproofs) =