# HG changeset patch # User blanchet # Date 1409237907 -7200 # Node ID ca7ec8728348849ee049696f42f1db0d4c2a1f48 # Parent 6842fb6365695eb4a1e180b4c53fbf3ccd17a909 removed show stuttering diff -r 6842fb636569 -r ca7ec8728348 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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 diff -r 6842fb636569 -r ca7ec8728348 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML --- 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) =