adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

lib: notify if crunch generates side-conditions 

Signed-off-by: Corey Lewis <corey.lewis@unsw.edu.au>
This commit is contained in:
Corey Lewis 2021-11-10 13:12:34 +11:00 committed by Corey Lewis
parent 141d2f4b67
commit f28ce0b310
1 changed files with 4 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
lib/crunch-cmd.ML
View File

@ -752,6 +752,10 @@ fun crunch cfg pre extra stack const' thms =
(ms ~~ goals);
in fold (fn pre' => fn goal => collect_preconds pre' goal pre extra ctxt'') preconds goal end;
val goal' = if Instance.has_preconds then collect_preconds' pre else goal;
val _ =
if Instance.has_preconds andalso not (Term.aconv_untyped (get_precond goal, get_precond goal'))
then Output.information ("Lemma generated for " ^ Proof_Context.markup_const ctxt const ^ " has side-conditions.")
else ();
val goal_prop = HOLogic.mk_Trueprop goal';
val ctxt''' = ctxt'' |> Proof_Context.augment goal_prop