--- a/src/HOL/SMT_Examples/SMT_Examples.certs Fri Dec 04 14:39:31 2015 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs Fri Dec 04 14:39:39 2015 +0100
@@ -6020,3 +6020,40 @@
785615f585a02b3e6ed8608ecc9660ba5c4025e2 2 0
sat
(error "line 9 column 10: proof is not available")
+c4e20de399740e8f0c9a87abad030298d74bc47b 12 0
+unsat
+((set-logic AUFLIA)
+(proof
+(let ((?x31 (p$ true)))
+(let (($x29 (< 2 3)))
+(let ((?x30 (p$ $x29)))
+(let (($x32 (= ?x30 ?x31)))
+(let ((@x42 (monotonicity (monotonicity (rewrite (= $x29 true)) $x32) (= $x32 (= ?x31 ?x31)))))
+(let ((@x49 (monotonicity (trans @x42 (rewrite (= (= ?x31 ?x31) true)) (= $x32 true)) (= (not $x32) (not true)))))
+(let ((@x53 (trans @x49 (rewrite (= (not true) false)) (= (not $x32) false))))
+(mp (asserted (not $x32)) @x53 false))))))))))
+
+23f5eb3b530a4577da2f8947333286ff70ed557f 11 0
+unsat
+((set-logic AUFLIA)
+(proof
+(let (($x29 (exists ((?v0 A$) )(! (g$ ?v0) :qid k!7))
+))
+(let (($x30 (f$ $x29)))
+(let (($x31 (=> $x30 true)))
+(let (($x32 (not $x31)))
+(let ((@x42 (trans (monotonicity (rewrite (= $x31 true)) (= $x32 (not true))) (rewrite (= (not true) false)) (= $x32 false))))
+(mp (asserted $x32) @x42 false))))))))
+
+60f1b32e9c6a2229b64c85dcfb0bde9c2bd5433a 11 0
+unsat
+((set-logic AUFLIA)
+(proof
+(let (($x29 (forall ((?v0 A$) )(! (g$ ?v0) :qid k!7))
+))
+(let (($x30 (f$ $x29)))
+(let (($x31 (=> $x30 true)))
+(let (($x32 (not $x31)))
+(let ((@x42 (trans (monotonicity (rewrite (= $x31 true)) (= $x32 (not true))) (rewrite (= (not true) false)) (= $x32 false))))
+(mp (asserted $x32) @x42 false))))))))
+
--- a/src/HOL/SMT_Examples/SMT_Word_Examples.certs Fri Dec 04 14:39:31 2015 +0100
+++ b/src/HOL/SMT_Examples/SMT_Word_Examples.certs Fri Dec 04 14:39:39 2015 +0100
@@ -367,3 +367,16 @@
(let ((@x46 (monotonicity @x43 (= $x34 (not (= (p$ $x29) ?x32))))))
(mp (asserted $x34) (trans @x46 @x63 (= $x34 false)) false))))))))))))))
+6182523304a5597432fa1bb8dd16e804ddd8d7ee 12 0
+unsat
+((set-logic <null>)
+(proof
+(let ((?x31 (p$ true)))
+(let (($x29 (bvule (_ bv0 4) a$)))
+(let ((?x30 (p$ $x29)))
+(let (($x32 (= ?x30 ?x31)))
+(let ((@x42 (monotonicity (monotonicity (rewrite (= $x29 true)) $x32) (= $x32 (= ?x31 ?x31)))))
+(let ((@x49 (monotonicity (trans @x42 (rewrite (= (= ?x31 ?x31) true)) (= $x32 true)) (= (not $x32) (not true)))))
+(let ((@x53 (trans @x49 (rewrite (= (not true) false)) (= (not $x32) false))))
+(mp (asserted (not $x32)) @x53 false))))))))))
+
--- a/src/HOL/Tools/SMT/smt_translate.ML Fri Dec 04 14:39:31 2015 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML Fri Dec 04 14:39:39 2015 +0100
@@ -319,14 +319,10 @@
val fol_rules = [
Let_def,
- @{lemma "P = True == P" by (rule eq_reflection) simp},
- @{lemma "if P then True else False == P" by (rule eq_reflection) simp}]
+ @{lemma "P = True == P" by (rule eq_reflection) simp}]
exception BAD_PATTERN of unit
- fun wrap_in_if pat t =
- if pat then raise BAD_PATTERN () else @{const If (bool)} $ t $ @{const True} $ @{const False}
-
fun is_builtin_conn_or_pred ctxt c ts =
is_some (SMT_Builtin.dest_builtin_conn ctxt c ts) orelse
is_some (SMT_Builtin.dest_builtin_pred ctxt c ts)
@@ -343,9 +339,10 @@
| (u as Const (@{const_name If}, _), [t1, t2, t3]) =>
if pat then raise BAD_PATTERN () else u $ in_form t1 $ in_term pat t2 $ in_term pat t3
| (Const (c as (n, _)), ts) =>
- if is_builtin_conn_or_pred ctxt c ts then wrap_in_if pat (in_form t)
- else if is_quant n then wrap_in_if pat (in_form t)
- else Term.list_comb (Const c, map (in_term pat) ts)
+ if is_builtin_conn_or_pred ctxt c ts orelse is_quant n then
+ if pat then raise BAD_PATTERN () else in_form t
+ else
+ Term.list_comb (Const c, map (in_term pat) ts)
| (Free c, ts) => Term.list_comb (Free c, map (in_term pat) ts)
| _ => t)