#
026388c1 |
|
25-Nov-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added Tactical.PRED_ASSUM. It's similar to PAT_ASSUM but uses a predicate to pick the assumption. Added blastLib.FULL_BBLAST_TAC, which attempts to use "blastable" assumptions. Make blastLib.BBLAST_PROVE smarter with respect to counterexamples (existential goals). For example, > blastLib.BBLAST_PROVE ``?x y. x + y = 12w : word8``; val it = |- ?x y. x + y = 12w: thm is now possible, and we also have: > blastLib.BBLAST_PROVE ``x < y = x <=+ y : word8``; Found counterexample: y -> 255w and x -> 0w Exception- SAT_cex |- (0w < 255w <=> 0w <=+ 255w) <=> F raised The printing of counterexamples is controlled by the trace "print blast counterexamples".
|