summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | desharna |

Wed, 21 Oct 2020 17:46:51 +0200 | |

changeset 72583 | e728d3a3d383 |

parent 72582 | b69a3a7655f2 |

child 72584 | 4ea19e5dc67e |

Tuned isar_proofs constructions

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Oct 21 17:31:15 2020 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Oct 21 17:46:51 2020 +0200 @@ -268,10 +268,8 @@ insert_lemma_in_step lem step @ steps else step :: insert_lemma_in_steps lem steps - and insert_lemma_in_proof lem (Proof {fixes, assumptions, steps}) = - let val steps' = insert_lemma_in_steps lem steps in - Proof {fixes = fixes, assumptions = assumptions, steps = steps'} - end + and insert_lemma_in_proof lem (proof as Proof {steps, ...}) = + isar_proof_with_steps proof (insert_lemma_in_steps lem steps) val rule_of_clause_id = fst o the o Symtab.lookup steps o fst

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Wed Oct 21 17:31:15 2020 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Wed Oct 21 17:46:51 2020 +0200 @@ -64,9 +64,9 @@ | update_subproofs (proof :: subproofs) updates = update_proof proof (update_subproofs subproofs updates) and update_proof proof (proofs, []) = (proof :: proofs, []) - | update_proof (Proof {fixes, assumptions, steps}) (proofs, updates) = + | update_proof (proof as Proof {steps, ...}) (proofs, updates) = let val (steps', updates') = update_steps steps updates in - (Proof {fixes = fixes, assumptions = assumptions, steps = steps'} :: proofs, updates') + (isar_proof_with_steps proof steps' :: proofs, updates') end in fst (update_steps steps (rev updates)) @@ -273,9 +273,9 @@ can be eliminated. In the best case, this once again leads to a proof whose proof steps do not have subproofs. Applying this approach recursively will result in a flat proof in the best cast. *) - fun compress_proof (proof as (Proof {fixes, assumptions, steps})) = + fun compress_proof (proof as (Proof {steps, ...})) = if compress_further () then - Proof {fixes = fixes, assumptions = assumptions, steps = compress_steps steps} + isar_proof_with_steps proof (compress_steps steps) else proof and compress_steps steps =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Wed Oct 21 17:31:15 2020 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Wed Oct 21 17:46:51 2020 +0200 @@ -74,7 +74,7 @@ | _ => step (* don't touch steps that time out or fail *)) | minimize_isar_step_dependencies _ _ step = step -fun postprocess_isar_proof_remove_show_stuttering (Proof {fixes, assumptions, steps}) = +fun postprocess_isar_proof_remove_show_stuttering (proof as Proof {steps, ...}) = let fun process_steps [] = [] | process_steps (steps as [Prove ([], [], _, t1, subs1, facts1, meths1, comment1), @@ -83,14 +83,13 @@ else steps | process_steps (step :: steps) = step :: process_steps steps in - Proof {fixes = fixes, assumptions = assumptions, steps = process_steps steps} + isar_proof_with_steps proof (process_steps steps) end fun postprocess_isar_proof_remove_unreferenced_steps postproc_step = let - fun process_proof (Proof {fixes, assumptions, steps}) = - process_steps steps - ||> (fn steps' => Proof {fixes = fixes, assumptions = assumptions, steps = steps'}) + fun process_proof (proof as Proof {steps, ...}) = + process_steps steps ||> isar_proof_with_steps proof and process_steps [] = ([], []) | process_steps steps = (* the last step is always implicitly referenced *)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Wed Oct 21 17:31:15 2020 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Wed Oct 21 17:46:51 2020 +0200 @@ -33,6 +33,7 @@ val sort_facts : facts -> facts val steps_of_isar_proof : isar_proof -> isar_step list + val isar_proof_with_steps : isar_proof -> isar_step list -> isar_proof val label_of_isar_step : isar_step -> label option val facts_of_isar_step : isar_step -> facts val proof_methods_of_isar_step : isar_step -> proof_method list @@ -103,6 +104,8 @@ fun sort_facts (lfs, gfs) = (sort (label_ord o swap) lfs, sort string_ord gfs) fun steps_of_isar_proof (Proof {steps, ...}) = steps +fun isar_proof_with_steps (Proof {fixes, assumptions, ...}) steps = + Proof {fixes = fixes, assumptions = assumptions, steps = steps} fun label_of_isar_step (Prove (_, _, l, _, _, _, _, _)) = SOME l | label_of_isar_step _ = NONE @@ -122,8 +125,7 @@ fun map_isar_steps f = let - fun map_proof (Proof {fixes, assumptions, steps}) = - Proof {fixes = fixes, assumptions = assumptions, steps = map map_step steps} + fun map_proof (proof as Proof {steps, ...}) = isar_proof_with_steps proof (map map_step steps) and map_step (step as Let _) = f step | map_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) = f (Prove (qs, xs, l, t, map map_proof subs, facts, meths, comment)) @@ -155,10 +157,8 @@ and chain_isar_steps _ [] = [] | chain_isar_steps prev (i :: is) = chain_isar_step prev i :: chain_isar_steps (label_of_isar_step i) is -and chain_isar_proof (Proof {fixes, assumptions, steps}) = - let val steps' = chain_isar_steps (try (List.last #> fst) assumptions) steps in - Proof {fixes = fixes, assumptions = assumptions, steps = steps'} - end +and chain_isar_proof (proof as Proof {assumptions, steps, ...}) = + isar_proof_with_steps proof (chain_isar_steps (try (List.last #> fst) assumptions) steps) fun kill_useless_labels_in_isar_proof proof = let