# HG changeset patch
# User boehmes
# Date 1523437153 -7200
# Node ID 959b0aed2ce5a417cd85cddf949925bca827c216
# Parent  e9f66b35d63603ccfb6947bd95d8143c1a31546e
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle

diff -r e9f66b35d636 -r 959b0aed2ce5 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Mon Apr 09 17:21:10 2018 +0100
+++ b/src/HOL/SMT.thy	Wed Apr 11 10:59:13 2018 +0200
@@ -120,10 +120,6 @@
 lemmas min_def_raw = min_def[abs_def]
 lemmas max_def_raw = max_def[abs_def]
 
-lemma nat_int': "\<forall>n. nat (int n) = n" by simp
-lemma int_nat_nneg: "\<forall>i. i \<ge> 0 \<longrightarrow> int (nat i) = i" by simp
-lemma int_nat_neg: "\<forall>i. i < 0 \<longrightarrow> int (nat i) = 0" by simp
-
 lemma nat_zero_as_int:
   "0 = nat 0"
   by simp
@@ -146,6 +142,31 @@
 lemma int_plus: "int (n + m) = int n + int m" by (rule of_nat_add)
 lemma int_minus: "int (n - m) = int (nat (int n - int m))" by auto
 
+lemma nat_int_comparison:
+  fixes a b :: nat
+  shows "(a = b) = (int a = int b)"
+    and "(a < b) = (int a < int b)"
+    and "(a \<le> b) = (int a \<le> int b)"
+  by simp_all
+
+lemma int_ops:
+  fixes a b :: nat
+  shows "int 0 = 0"
+    and "int 1 = 1"
+    and "int (numeral n) = numeral n"
+    and "int (Suc a) = int a + 1"
+    and "int (a + b) = int a + int b"
+    and "int (a - b) = (if int a < int b then 0 else int a - int b)"
+    and "int (a * b) = int a * int b"
+    and "int (a div b) = int a div int b"
+    and "int (a mod b) = int a mod int b"
+  by (auto intro: zdiv_int zmod_int)
+
+lemma int_if:
+  fixes a b :: nat
+  shows "int (if P then a else b) = (if P then int a else int b)"
+  by simp
+
 
 subsection \<open>Integer division and modulo for Z3\<close>
 
diff -r e9f66b35d636 -r 959b0aed2ce5 src/HOL/SMT_Examples/SMT_Examples.certs
--- a/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Apr 09 17:21:10 2018 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs	Wed Apr 11 10:59:13 2018 +0200
@@ -5658,3 +5658,431 @@
 (
 a0
 )
+60f0eb26fb928f5be2217521c55fd281c68657ab 12 0
+unsat
+((set-logic AUFLIA)
+(proof
+(let ((@x39 (rewrite (= (= (* 2 (of_nat$ x$)) 1) false))))
+(let ((?x29 (of_nat$ x$)))
+(let ((?x30 (* 2 ?x29)))
+(let (($x32 (= ?x30 1)))
+(let (($x33 (not $x32)))
+(let (($x34 (not $x33)))
+(let ((@x37 (rewrite (= $x34 $x32))))
+(mp (asserted $x34) (trans @x37 @x39 (= $x34 false)) false))))))))))
+
+8add3cdd73f5b10c545c377441668f38198ca42e 23 0
+unsat
+((set-logic AUFLIA)
+(proof
+(let ((?x28 (of_nat$ a$)))
+(let (($x57 (>= ?x28 4)))
+(let (($x47 (>= ?x28 3)))
+(let (($x61 (or $x47 (not $x57))))
+(let (($x64 (not $x61)))
+(let ((@x51 (monotonicity (rewrite (= (< ?x28 3) (not $x47))) (= (not (< ?x28 3)) (not (not $x47))))))
+(let ((@x55 (trans @x51 (rewrite (= (not (not $x47)) $x47)) (= (not (< ?x28 3)) $x47))))
+(let ((@x63 (monotonicity @x55 (rewrite (= (< (* 2 ?x28) 7) (not $x57))) (= (or (not (< ?x28 3)) (< (* 2 ?x28) 7)) $x61))))
+(let ((@x66 (monotonicity @x63 (= (not (or (not (< ?x28 3)) (< (* 2 ?x28) 7))) $x64))))
+(let (($x36 (not (=> (< ?x28 3) (< (* 2 ?x28) 7)))))
+(let (($x34 (< (* 2 ?x28) 7)))
+(let (($x30 (< ?x28 3)))
+(let (($x38 (not $x30)))
+(let (($x39 (or $x38 $x34)))
+(let ((@x44 (monotonicity (rewrite (= (=> $x30 $x34) $x39)) (= $x36 (not $x39)))))
+(let ((@x71 (not-or-elim (mp (asserted $x36) (trans @x44 @x66 (= $x36 $x64)) $x64) $x57)))
+(let (($x45 (not $x47)))
+(let ((@x70 (not-or-elim (mp (asserted $x36) (trans @x44 @x66 (= $x36 $x64)) $x64) $x45)))
+(unit-resolution ((_ th-lemma arith farkas 1 1) $x61) @x70 @x71 false)))))))))))))))))))))
+
+4c6f37a2909344bd2a4d64422c28ae3c0bb6baa4 22 0
+unsat
+((set-logic AUFLIA)
+(proof
+(let ((?x29 (of_nat$ y$)))
+(let ((?x30 (+ 1 ?x29)))
+(let ((?x33 (- ?x30 ?x29)))
+(let (($x32 (< ?x30 ?x29)))
+(let ((?x34 (ite $x32 0 ?x33)))
+(let ((?x31 (* 0 ?x30)))
+(let (($x35 (< ?x31 ?x34)))
+(let (($x36 (not $x35)))
+(let ((@x55 (monotonicity (rewrite (= $x32 false)) (= (ite $x32 0 1) (ite false 0 1)))))
+(let ((@x59 (trans @x55 (rewrite (= (ite false 0 1) 1)) (= (ite $x32 0 1) 1))))
+(let ((@x62 (monotonicity @x59 (= (< 0 (ite $x32 0 1)) (< 0 1)))))
+(let ((@x66 (trans @x62 (rewrite (= (< 0 1) true)) (= (< 0 (ite $x32 0 1)) true))))
+(let ((@x69 (monotonicity @x66 (= (not (< 0 (ite $x32 0 1))) (not true)))))
+(let ((@x73 (trans @x69 (rewrite (= (not true) false)) (= (not (< 0 (ite $x32 0 1))) false))))
+(let ((@x44 (monotonicity (rewrite (= ?x33 1)) (= ?x34 (ite $x32 0 1)))))
+(let ((@x47 (monotonicity (rewrite (= ?x31 0)) @x44 (= $x35 (< 0 (ite $x32 0 1))))))
+(let ((@x50 (monotonicity @x47 (= $x36 (not (< 0 (ite $x32 0 1)))))))
+(mp (asserted $x36) (trans @x50 @x73 (= $x36 false)) false))))))))))))))))))))
+
+b714679c599d34ff47961092cf8a68a58c263339 37 0
+unsat
+((set-logic AUFLIA)
+(proof
+(let ((?x29 (of_nat$ y$)))
+(let (($x91 (>= ?x29 0)))
+(let ((@x126 (mp (asserted (<= 0 ?x29)) (rewrite (= (<= 0 ?x29) $x91)) $x91)))
+(let (($x86 (<= ?x29 (- 1))))
+(let (($x111 (not (or (= (not $x86) (= (ite $x91 ?x29 0) ?x29)) (not $x86)))))
+(let (($x39 (=> (not (ite (< 0 (+ 1 ?x29)) true false)) false)))
+(let (($x36 (= (ite (< (+ 1 ?x29) 1) 0 (- (+ 1 ?x29) 1)) ?x29)))
+(let ((?x30 (+ 1 ?x29)))
+(let (($x31 (< 0 ?x30)))
+(let (($x32 (ite $x31 true false)))
+(let (($x37 (= $x32 $x36)))
+(let (($x41 (or false (or $x37 $x39))))
+(let (($x42 (not $x41)))
+(let (($x112 (= (not (or (= $x31 (= (ite (< ?x30 1) 0 ?x29) ?x29)) $x31)) $x111)))
+(let (($x33 (< ?x30 1)))
+(let ((?x48 (ite $x33 0 ?x29)))
+(let (($x51 (= ?x48 ?x29)))
+(let (($x57 (= $x31 $x51)))
+(let (($x72 (or $x57 $x31)))
+(let (($x109 (= $x72 (or (= (not $x86) (= (ite $x91 ?x29 0) ?x29)) (not $x86)))))
+(let ((@x96 (monotonicity (rewrite (= $x33 (not $x91))) (= ?x48 (ite (not $x91) 0 ?x29)))))
+(let ((@x101 (trans @x96 (rewrite (= (ite (not $x91) 0 ?x29) (ite $x91 ?x29 0))) (= ?x48 (ite $x91 ?x29 0)))))
+(let ((@x107 (monotonicity (rewrite (= $x31 (not $x86))) (monotonicity @x101 (= $x51 (= (ite $x91 ?x29 0) ?x29))) (= $x57 (= (not $x86) (= (ite $x91 ?x29 0) ?x29))))))
+(let ((@x113 (monotonicity (monotonicity @x107 (rewrite (= $x31 (not $x86))) $x109) $x112)))
+(let ((@x67 (monotonicity (monotonicity (rewrite (= $x32 $x31)) (= (not $x32) (not $x31))) (= $x39 (=> (not $x31) false)))))
+(let ((@x71 (trans @x67 (rewrite (= (=> (not $x31) false) $x31)) (= $x39 $x31))))
+(let ((@x50 (monotonicity (rewrite (= (- ?x30 1) ?x29)) (= (ite $x33 0 (- ?x30 1)) ?x48))))
+(let ((@x56 (monotonicity (rewrite (= $x32 $x31)) (monotonicity @x50 (= $x36 $x51)) (= $x37 (= $x31 $x51)))))
+(let ((@x74 (monotonicity (trans @x56 (rewrite (= (= $x31 $x51) $x57)) (= $x37 $x57)) @x71 (= (or $x37 $x39) $x72))))
+(let ((@x81 (trans (monotonicity @x74 (= $x41 (or false $x72))) (rewrite (= (or false $x72) $x72)) (= $x41 $x72))))
+(let ((@x115 (trans (monotonicity @x81 (= $x42 (not $x72))) @x113 (= $x42 $x111))))
+(let ((@x119 (not-or-elim (mp (asserted $x42) @x115 $x111) $x86)))
+(unit-resolution ((_ th-lemma arith farkas 1 1) (or (not $x86) (not $x91))) @x119 @x126 false)))))))))))))))))))))))))))))))))))
+
+37308e9e03de5831baac25fd010c0af7fb3ac06c 64 0
+unsat
+((set-logic AUFLIA)
+(proof
+(let ((?x58 (* (- 1) x$)))
+(let (($x76 (>= x$ 0)))
+(let ((?x83 (ite $x76 x$ ?x58)))
+(let ((?x536 (* (- 1) ?x83)))
+(let ((?x539 (+ ?x58 ?x536)))
+(let (($x237 (<= ?x539 0)))
+(let (($x229 (= ?x58 ?x83)))
+(let (($x77 (not $x76)))
+(let (($x143 (= x$ ?x83)))
+(let ((@x182 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x143) (<= (+ x$ ?x536) 0))) (unit-resolution (def-axiom (or $x77 $x143)) (hypothesis $x76) $x143) (<= (+ x$ ?x536) 0))))
+(let (($x232 (>= ?x83 0)))
+(let (($x337 (not $x232)))
+(let ((?x88 (nat$ ?x83)))
+(let ((?x91 (of_nat$ ?x88)))
+(let (($x233 (= ?x91 0)))
+(let (($x94 (= ?x91 ?x83)))
+(let (($x234 (ite $x232 $x94 $x233)))
+(let (($x560 (forall ((?v0 Int) )(! (let (($x39 (>= ?v0 0)))
+(ite $x39 (= (of_nat$ (nat$ ?v0)) ?v0) (= (of_nat$ (nat$ ?v0)) 0))) :pattern ( (nat$ ?v0) ) :qid k!8))
+))
+(let (($x139 (forall ((?v0 Int) )(! (let (($x39 (>= ?v0 0)))
+(ite $x39 (= (of_nat$ (nat$ ?v0)) ?v0) (= (of_nat$ (nat$ ?v0)) 0))) :qid k!8))
+))
+(let (($x39 (>= ?0 0)))
+(let (($x136 (ite $x39 (= (of_nat$ (nat$ ?0)) ?0) (= (of_nat$ (nat$ ?0)) 0))))
+(let (($x46 (forall ((?v0 Int) )(! (let ((?x29 (of_nat$ (nat$ ?v0))))
+(= ?x29 (ite (>= ?v0 0) ?v0 0))) :qid k!8))
+))
+(let ((@x141 (quant-intro (rewrite (= (= (of_nat$ (nat$ ?0)) (ite $x39 ?0 0)) $x136)) (= $x46 $x139))))
+(let ((?x29 (of_nat$ (nat$ ?0))))
+(let (($x43 (= ?x29 (ite $x39 ?0 0))))
+(let (($x33 (forall ((?v0 Int) )(! (let ((?x29 (of_nat$ (nat$ ?v0))))
+(= ?x29 (ite (<= 0 ?v0) ?v0 0))) :qid k!8))
+))
+(let ((@x42 (monotonicity (rewrite (= (<= 0 ?0) $x39)) (= (ite (<= 0 ?0) ?0 0) (ite $x39 ?0 0)))))
+(let ((@x45 (monotonicity @x42 (= (= ?x29 (ite (<= 0 ?0) ?0 0)) $x43))))
+(let ((@x122 (mp~ (mp (asserted $x33) (quant-intro @x45 (= $x33 $x46)) $x46) (nnf-pos (refl (~ $x43 $x43)) (~ $x46 $x46)) $x46)))
+(let ((@x565 (mp (mp @x122 @x141 $x139) (quant-intro (refl (= $x136 $x136)) (= $x139 $x560)) $x560)))
+(let (($x551 (or (not $x560) $x234)))
+(let ((@x552 ((_ quant-inst (ite $x76 x$ ?x58)) $x551)))
+(let (($x97 (not $x94)))
+(let (($x36 (< x$ 0)))
+(let ((?x51 (ite $x36 (- x$) x$)))
+(let (($x55 (not (= (of_nat$ (nat$ ?x51)) ?x51))))
+(let (($x98 (= (not (= (of_nat$ (nat$ (ite $x36 ?x58 x$))) (ite $x36 ?x58 x$))) $x97)))
+(let ((?x61 (ite $x36 ?x58 x$)))
+(let ((?x64 (nat$ ?x61)))
+(let ((?x67 (of_nat$ ?x64)))
+(let (($x70 (= ?x67 ?x61)))
+(let ((@x87 (trans (monotonicity (rewrite (= $x36 $x77)) (= ?x61 (ite $x77 ?x58 x$))) (rewrite (= (ite $x77 ?x58 x$) ?x83)) (= ?x61 ?x83))))
+(let ((@x96 (monotonicity (monotonicity (monotonicity @x87 (= ?x64 ?x88)) (= ?x67 ?x91)) @x87 (= $x70 $x94))))
+(let ((@x66 (monotonicity (monotonicity (rewrite (= (- x$) ?x58)) (= ?x51 ?x61)) (= (nat$ ?x51) ?x64))))
+(let ((@x72 (monotonicity (monotonicity @x66 (= (of_nat$ (nat$ ?x51)) ?x67)) (monotonicity (rewrite (= (- x$) ?x58)) (= ?x51 ?x61)) (= (= (of_nat$ (nat$ ?x51)) ?x51) $x70))))
+(let ((@x101 (trans (monotonicity @x72 (= $x55 (not $x70))) (monotonicity @x96 $x98) (= $x55 $x97))))
+(let ((@x102 (mp (asserted $x55) @x101 $x97)))
+(let ((@x545 (unit-resolution (def-axiom (or (not $x234) $x337 $x94)) @x102 (or (not $x234) $x337))))
+(let ((@x532 ((_ th-lemma arith farkas -1 1 1) (hypothesis $x76) (unit-resolution @x545 (unit-resolution @x552 @x565 $x234) $x337) @x182 false)))
+(let ((@x533 (lemma @x532 $x77)))
+(let ((@x526 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x229) $x237)) (unit-resolution (def-axiom (or $x76 $x229)) @x533 $x229) $x237)))
+((_ th-lemma arith farkas 1 1 1) (unit-resolution @x545 (unit-resolution @x552 @x565 $x234) $x337) @x533 @x526 false))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+ed82050c49ac6c4c1fb3e26f7f8f9a2dd0dd0173 264 0
+unsat
+((set-logic AUFLIA)
+(declare-fun ?v1!0 (Nat$) Nat$)
+(proof
+(let ((?x89 (of_nat$ m$)))
+(let ((?x90 (* 4 ?x89)))
+(let ((?x98 (+ 1 ?x90)))
+(let ((?x101 (nat$ ?x98)))
+(let ((?x276 (of_nat$ ?x101)))
+(let ((?x581 (* (- 1) ?x276)))
+(let ((?x582 (+ ?x90 ?x581)))
+(let (($x555 (>= ?x582 (- 1))))
+(let (($x580 (= ?x582 (- 1))))
+(let (($x574 (= ?x276 0)))
+(let (($x622 (>= ?x89 0)))
+(let (($x583 (ite $x622 $x580 $x574)))
+(let (($x737 (forall ((?v0 Int) )(! (let (($x160 (>= ?v0 0)))
+(ite $x160 (= (of_nat$ (nat$ ?v0)) ?v0) (= (of_nat$ (nat$ ?v0)) 0))) :pattern ( (nat$ ?v0) ) :qid k!14))
+))
+(let (($x271 (forall ((?v0 Int) )(! (let (($x160 (>= ?v0 0)))
+(ite $x160 (= (of_nat$ (nat$ ?v0)) ?v0) (= (of_nat$ (nat$ ?v0)) 0))) :qid k!14))
+))
+(let (($x160 (>= ?0 0)))
+(let (($x268 (ite $x160 (= (of_nat$ (nat$ ?0)) ?0) (= (of_nat$ (nat$ ?0)) 0))))
+(let (($x167 (forall ((?v0 Int) )(! (let ((?x149 (nat$ ?v0)))
+(let ((?x150 (of_nat$ ?x149)))
+(= ?x150 (ite (>= ?v0 0) ?v0 0)))) :qid k!14))
+))
+(let ((@x273 (quant-intro (rewrite (= (= (of_nat$ (nat$ ?0)) (ite $x160 ?0 0)) $x268)) (= $x167 $x271))))
+(let ((?x149 (nat$ ?0)))
+(let ((?x150 (of_nat$ ?x149)))
+(let (($x164 (= ?x150 (ite $x160 ?0 0))))
+(let (($x154 (forall ((?v0 Int) )(! (let ((?x149 (nat$ ?v0)))
+(let ((?x150 (of_nat$ ?x149)))
+(= ?x150 (ite (<= 0 ?v0) ?v0 0)))) :qid k!14))
+))
+(let ((@x163 (monotonicity (rewrite (= (<= 0 ?0) $x160)) (= (ite (<= 0 ?0) ?0 0) (ite $x160 ?0 0)))))
+(let ((@x166 (monotonicity @x163 (= (= ?x150 (ite (<= 0 ?0) ?0 0)) $x164))))
+(let ((@x243 (mp~ (mp (asserted $x154) (quant-intro @x166 (= $x154 $x167)) $x167) (nnf-pos (refl (~ $x164 $x164)) (~ $x167 $x167)) $x167)))
+(let ((@x742 (mp (mp @x243 @x273 $x271) (quant-intro (refl (= $x268 $x268)) (= $x271 $x737)) $x737)))
+(let (($x587 (or (not $x737) $x583)))
+(let ((@x585 (monotonicity (rewrite (= (>= ?x98 0) $x622)) (rewrite (= (= ?x276 ?x98) $x580)) (= (ite (>= ?x98 0) (= ?x276 ?x98) $x574) $x583))))
+(let ((@x568 (monotonicity @x585 (= (or (not $x737) (ite (>= ?x98 0) (= ?x276 ?x98) $x574)) $x587))))
+(let ((@x571 (trans @x568 (rewrite (= $x587 $x587)) (= (or (not $x737) (ite (>= ?x98 0) (= ?x276 ?x98) $x574)) $x587))))
+(let ((@x572 (mp ((_ quant-inst (+ 1 ?x90)) (or (not $x737) (ite (>= ?x98 0) (= ?x276 ?x98) $x574))) @x571 $x587)))
+(let (($x723 (forall ((?v0 Nat$) )(! (let ((?x30 (of_nat$ ?v0)))
+(>= ?x30 0)) :pattern ( (of_nat$ ?v0) ) :qid k!12))
+))
+(let (($x142 (forall ((?v0 Nat$) )(! (let ((?x30 (of_nat$ ?v0)))
+(>= ?x30 0)) :qid k!12))
+))
+(let ((@x727 (quant-intro (refl (= (>= (of_nat$ ?0) 0) (>= (of_nat$ ?0) 0))) (= $x142 $x723))))
+(let ((@x232 (nnf-pos (refl (~ (>= (of_nat$ ?0) 0) (>= (of_nat$ ?0) 0))) (~ $x142 $x142))))
+(let (($x135 (forall ((?v0 Nat$) )(! (let ((?x30 (of_nat$ ?v0)))
+(<= 0 ?x30)) :qid k!12))
+))
+(let ((@x144 (quant-intro (rewrite (= (<= 0 (of_nat$ ?0)) (>= (of_nat$ ?0) 0))) (= $x135 $x142))))
+(let ((@x728 (mp (mp~ (mp (asserted $x135) @x144 $x142) @x232 $x142) @x727 $x723)))
+(let (($x593 (or (not $x723) $x622)))
+(let ((@x594 ((_ quant-inst m$) $x593)))
+(let ((@x547 (unit-resolution (def-axiom (or (not $x583) (not $x622) $x580)) (unit-resolution @x594 @x728 $x622) (or (not $x583) $x580))))
+(let ((@x551 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x580) $x555)) (unit-resolution @x547 (unit-resolution @x572 @x742 $x583) $x580) $x555)))
+(let (($x361 (<= ?x276 1)))
+(let (($x668 (not $x361)))
+(let (($x346 (forall ((?v1 Nat$) )(! (let ((?x89 (of_nat$ m$)))
+(let ((?x90 (* 4 ?x89)))
+(let ((?x98 (+ 1 ?x90)))
+(let ((?x101 (nat$ ?x98)))
+(let ((?x276 (of_nat$ ?x101)))
+(let ((?x30 (of_nat$ ?v1)))
+(let (($x363 (= ?x30 ?x276)))
+(let (($x34 (= ?x30 1)))
+(let (($x362 (dvd$ ?v1 ?x101)))
+(let (($x352 (not $x362)))
+(or $x352 $x34 $x363))))))))))) :pattern ( (dvd$ ?v1 (nat$ (+ 1 (* 4 (of_nat$ m$))))) ) :pattern ( (of_nat$ ?v1) ) :qid k!10))
+))
+(let (($x682 (not $x346)))
+(let (($x683 (or $x361 $x682)))
+(let (($x338 (not $x683)))
+(let (($x104 (prime_nat$ ?x101)))
+(let (($x110 (not $x104)))
+(let (($x468 (or $x110 $x338)))
+(let ((?x351 (?v1!0 ?x101)))
+(let ((?x686 (of_nat$ ?x351)))
+(let (($x688 (= ?x686 ?x276)))
+(let (($x687 (= ?x686 1)))
+(let (($x684 (dvd$ ?x351 ?x101)))
+(let (($x685 (not $x684)))
+(let (($x689 (or $x685 $x687 $x688)))
+(let (($x679 (not $x689)))
+(let (($x344 (or $x104 $x361 $x679)))
+(let (($x681 (not $x344)))
+(let (($x678 (not $x468)))
+(let (($x323 (or $x678 $x681)))
+(let (($x665 (not $x323)))
+(let (($x719 (forall ((?v0 Nat$) )(! (let (($x191 (or (not (dvd$ (?v1!0 ?v0) ?v0)) (= (of_nat$ (?v1!0 ?v0)) 1) (= (of_nat$ (?v1!0 ?v0)) (of_nat$ ?v0)))))
+(let (($x192 (not $x191)))
+(let ((?x30 (of_nat$ ?v0)))
+(let (($x65 (<= ?x30 1)))
+(let (($x28 (prime_nat$ ?v0)))
+(let (($x217 (or $x28 $x65 $x192)))
+(let (($x692 (forall ((?v1 Nat$) )(! (let ((?x30 (of_nat$ ?v1)))
+(let (($x34 (= ?x30 1)))
+(or (not (dvd$ ?v1 ?v0)) $x34 (= ?x30 (of_nat$ ?v0))))) :pattern ( (dvd$ ?v1 ?v0) ) :pattern ( (of_nat$ ?v1) ) :qid k!10))
+))
+(let (($x177 (not $x28)))
+(not (or (not (or $x177 (not (or $x65 (not $x692))))) (not $x217))))))))))) :pattern ( (prime_nat$ ?v0) ) :pattern ( (of_nat$ ?v0) ) :qid k!10))
+))
+(let (($x262 (forall ((?v0 Nat$) )(! (let (($x191 (or (not (dvd$ (?v1!0 ?v0) ?v0)) (= (of_nat$ (?v1!0 ?v0)) 1) (= (of_nat$ (?v1!0 ?v0)) (of_nat$ ?v0)))))
+(let (($x192 (not $x191)))
+(let ((?x30 (of_nat$ ?v0)))
+(let (($x65 (<= ?x30 1)))
+(let (($x28 (prime_nat$ ?v0)))
+(let (($x217 (or $x28 $x65 $x192)))
+(let (($x72 (forall ((?v1 Nat$) )(! (let ((?x30 (of_nat$ ?v1)))
+(let (($x34 (= ?x30 1)))
+(or (not (dvd$ ?v1 ?v0)) $x34 (= ?x30 (of_nat$ ?v0))))) :qid k!10))
+))
+(let (($x193 (not $x72)))
+(let (($x245 (not (or $x65 $x193))))
+(let (($x177 (not $x28)))
+(let (($x248 (or $x177 $x245)))
+(not (or (not $x248) (not $x217)))))))))))))) :qid k!10))
+))
+(let (($x191 (or (not (dvd$ (?v1!0 ?0) ?0)) (= (of_nat$ (?v1!0 ?0)) 1) (= (of_nat$ (?v1!0 ?0)) (of_nat$ ?0)))))
+(let (($x192 (not $x191)))
+(let ((?x30 (of_nat$ ?0)))
+(let (($x65 (<= ?x30 1)))
+(let (($x28 (prime_nat$ ?0)))
+(let (($x217 (or $x28 $x65 $x192)))
+(let (($x692 (forall ((?v1 Nat$) )(! (let ((?x30 (of_nat$ ?v1)))
+(let (($x34 (= ?x30 1)))
+(or (not (dvd$ ?v1 ?0)) $x34 (= ?x30 (of_nat$ ?0))))) :pattern ( (dvd$ ?v1 ?0) ) :pattern ( (of_nat$ ?v1) ) :qid k!10))
+))
+(let (($x177 (not $x28)))
+(let (($x72 (forall ((?v1 Nat$) )(! (let ((?x30 (of_nat$ ?v1)))
+(let (($x34 (= ?x30 1)))
+(or (not (dvd$ ?v1 ?0)) $x34 (= ?x30 (of_nat$ ?0))))) :qid k!10))
+))
+(let (($x193 (not $x72)))
+(let (($x245 (not (or $x65 $x193))))
+(let (($x248 (or $x177 $x245)))
+(let (($x257 (not (or (not $x248) (not $x217)))))
+(let (($x716 (= $x257 (not (or (not (or $x177 (not (or $x65 (not $x692))))) (not $x217))))))
+(let (($x713 (= (or (not $x248) (not $x217)) (or (not (or $x177 (not (or $x65 (not $x692))))) (not $x217)))))
+(let (($x34 (= ?x30 1)))
+(let (($x69 (or (not (dvd$ ?0 ?1)) $x34 (= ?x30 (of_nat$ ?1)))))
+(let ((@x699 (monotonicity (quant-intro (refl (= $x69 $x69)) (= $x72 $x692)) (= $x193 (not $x692)))))
+(let ((@x705 (monotonicity (monotonicity @x699 (= (or $x65 $x193) (or $x65 (not $x692)))) (= $x245 (not (or $x65 (not $x692)))))))
+(let ((@x711 (monotonicity (monotonicity @x705 (= $x248 (or $x177 (not (or $x65 (not $x692)))))) (= (not $x248) (not (or $x177 (not (or $x65 (not $x692)))))))))
+(let ((@x721 (quant-intro (monotonicity (monotonicity @x711 $x713) $x716) (= $x262 $x719))))
+(let (($x225 (forall ((?v0 Nat$) )(! (let (($x191 (or (not (dvd$ (?v1!0 ?v0) ?v0)) (= (of_nat$ (?v1!0 ?v0)) 1) (= (of_nat$ (?v1!0 ?v0)) (of_nat$ ?v0)))))
+(let (($x192 (not $x191)))
+(let ((?x30 (of_nat$ ?v0)))
+(let (($x65 (<= ?x30 1)))
+(let (($x28 (prime_nat$ ?v0)))
+(let (($x217 (or $x28 $x65 $x192)))
+(let (($x72 (forall ((?v1 Nat$) )(! (let ((?x30 (of_nat$ ?v1)))
+(let (($x34 (= ?x30 1)))
+(or (not (dvd$ ?v1 ?v0)) $x34 (= ?x30 (of_nat$ ?v0))))) :qid k!10))
+))
+(let (($x66 (not $x65)))
+(let (($x75 (and $x66 $x72)))
+(let (($x177 (not $x28)))
+(let (($x201 (or $x177 $x75)))
+(and $x201 $x217)))))))))))) :qid k!10))
+))
+(let ((@x250 (monotonicity (rewrite (= (and (not $x65) $x72) $x245)) (= (or $x177 (and (not $x65) $x72)) $x248))))
+(let ((@x253 (monotonicity @x250 (= (and (or $x177 (and (not $x65) $x72)) $x217) (and $x248 $x217)))))
+(let ((@x261 (trans @x253 (rewrite (= (and $x248 $x217) $x257)) (= (and (or $x177 (and (not $x65) $x72)) $x217) $x257))))
+(let (($x205 (forall ((?v0 Nat$) )(! (let (($x191 (or (not (dvd$ (?v1!0 ?v0) ?v0)) (= (of_nat$ (?v1!0 ?v0)) 1) (= (of_nat$ (?v1!0 ?v0)) (of_nat$ ?v0)))))
+(let (($x192 (not $x191)))
+(let ((?x30 (of_nat$ ?v0)))
+(let (($x65 (<= ?x30 1)))
+(let (($x66 (not $x65)))
+(let (($x182 (not $x66)))
+(let (($x196 (or $x182 $x192)))
+(let (($x28 (prime_nat$ ?v0)))
+(let (($x200 (or $x28 $x196)))
+(let (($x72 (forall ((?v1 Nat$) )(! (let ((?x30 (of_nat$ ?v1)))
+(let (($x34 (= ?x30 1)))
+(or (not (dvd$ ?v1 ?v0)) $x34 (= ?x30 (of_nat$ ?v0))))) :qid k!10))
+))
+(let (($x75 (and $x66 $x72)))
+(let (($x177 (not $x28)))
+(let (($x201 (or $x177 $x75)))
+(and $x201 $x200)))))))))))))) :qid k!10))
+))
+(let (($x66 (not $x65)))
+(let (($x75 (and $x66 $x72)))
+(let (($x201 (or $x177 $x75)))
+(let (($x222 (and $x201 $x217)))
+(let (($x182 (not $x66)))
+(let (($x196 (or $x182 $x192)))
+(let (($x200 (or $x28 $x196)))
+(let (($x202 (and $x201 $x200)))
+(let ((@x216 (monotonicity (monotonicity (rewrite (= $x182 $x65)) (= $x196 (or $x65 $x192))) (= $x200 (or $x28 (or $x65 $x192))))))
+(let ((@x221 (trans @x216 (rewrite (= (or $x28 (or $x65 $x192)) $x217)) (= $x200 $x217))))
+(let (($x81 (forall ((?v0 Nat$) )(! (let (($x72 (forall ((?v1 Nat$) )(! (let ((?x30 (of_nat$ ?v1)))
+(let (($x34 (= ?x30 1)))
+(or (not (dvd$ ?v1 ?v0)) $x34 (= ?x30 (of_nat$ ?v0))))) :qid k!10))
+))
+(let ((?x30 (of_nat$ ?v0)))
+(let (($x65 (<= ?x30 1)))
+(let (($x66 (not $x65)))
+(let (($x75 (and $x66 $x72)))
+(let (($x28 (prime_nat$ ?v0)))
+(= $x28 $x75))))))) :qid k!10))
+))
+(let ((@x199 (nnf-neg (refl (~ $x182 $x182)) (sk (~ $x193 $x192)) (~ (not $x75) $x196))))
+(let ((@x181 (monotonicity (refl (~ $x66 $x66)) (nnf-pos (refl (~ $x69 $x69)) (~ $x72 $x72)) (~ $x75 $x75))))
+(let ((@x204 (nnf-pos (refl (~ $x28 $x28)) (refl (~ $x177 $x177)) @x181 @x199 (~ (= $x28 $x75) $x202))))
+(let (($x42 (forall ((?v0 Nat$) )(! (let (($x39 (forall ((?v1 Nat$) )(! (let (($x33 (dvd$ ?v1 ?v0)))
+(=> $x33 (or (= (of_nat$ ?v1) 1) (= (of_nat$ ?v1) (of_nat$ ?v0))))) :qid k!10))
+))
+(let ((?x30 (of_nat$ ?v0)))
+(let (($x31 (< 1 ?x30)))
+(let (($x28 (prime_nat$ ?v0)))
+(= $x28 (and $x31 $x39)))))) :qid k!10))
+))
+(let (($x62 (forall ((?v0 Nat$) )(! (let (($x48 (forall ((?v1 Nat$) )(! (or (not (dvd$ ?v1 ?v0)) (or (= (of_nat$ ?v1) 1) (= (of_nat$ ?v1) (of_nat$ ?v0)))) :qid k!10))
+))
+(let ((?x30 (of_nat$ ?v0)))
+(let (($x31 (< 1 ?x30)))
+(let (($x51 (and $x31 $x48)))
+(let (($x28 (prime_nat$ ?v0)))
+(= $x28 $x51)))))) :qid k!10))
+))
+(let (($x78 (= $x28 $x75)))
+(let (($x48 (forall ((?v1 Nat$) )(! (or (not (dvd$ ?v1 ?0)) (or (= (of_nat$ ?v1) 1) (= (of_nat$ ?v1) (of_nat$ ?0)))) :qid k!10))
+))
+(let (($x31 (< 1 ?x30)))
+(let (($x51 (and $x31 $x48)))
+(let (($x57 (= $x28 $x51)))
+(let (($x45 (or (not (dvd$ ?0 ?1)) (or $x34 (= ?x30 (of_nat$ ?1))))))
+(let ((@x77 (monotonicity (rewrite (= $x31 $x66)) (quant-intro (rewrite (= $x45 $x69)) (= $x48 $x72)) (= $x51 $x75))))
+(let (($x39 (forall ((?v1 Nat$) )(! (let (($x33 (dvd$ ?v1 ?0)))
+(=> $x33 (or (= (of_nat$ ?v1) 1) (= (of_nat$ ?v1) (of_nat$ ?0))))) :qid k!10))
+))
+(let (($x41 (= $x28 (and $x31 $x39))))
+(let ((@x47 (rewrite (= (=> (dvd$ ?0 ?1) (or $x34 (= ?x30 (of_nat$ ?1)))) $x45))))
+(let ((@x53 (monotonicity (quant-intro @x47 (= $x39 $x48)) (= (and $x31 $x39) $x51))))
+(let ((@x61 (trans (monotonicity @x53 (= $x41 (= $x28 $x51))) (rewrite (= (= $x28 $x51) $x57)) (= $x41 $x57))))
+(let ((@x85 (trans (quant-intro @x61 (= $x42 $x62)) (quant-intro (monotonicity @x77 (= $x57 $x78)) (= $x62 $x81)) (= $x42 $x81))))
+(let ((@x208 (mp~ (mp (asserted $x42) @x85 $x81) (nnf-pos @x204 (~ $x81 $x205)) $x205)))
+(let ((@x228 (mp @x208 (quant-intro (monotonicity @x221 (= $x202 $x222)) (= $x205 $x225)) $x225)))
+(let ((@x722 (mp (mp @x228 (quant-intro @x261 (= $x225 $x262)) $x262) @x721 $x719)))
+(let (($x329 (or (not $x719) $x665)))
+(let ((@x667 ((_ quant-inst (nat$ ?x98)) $x329)))
+(let ((@x553 (unit-resolution (def-axiom (or $x323 $x468)) (unit-resolution @x667 @x722 $x665) $x468)))
+(let (($x125 (not (or $x110 (>= ?x89 1)))))
+(let (($x94 (<= 1 ?x89)))
+(let (($x95 (=> (prime_nat$ (nat$ (+ ?x90 1))) $x94)))
+(let (($x96 (not $x95)))
+(let ((@x124 (monotonicity (rewrite (= $x94 (>= ?x89 1))) (= (or $x110 $x94) (or $x110 (>= ?x89 1))))))
+(let ((@x103 (monotonicity (rewrite (= (+ ?x90 1) ?x98)) (= (nat$ (+ ?x90 1)) ?x101))))
+(let ((@x109 (monotonicity (monotonicity @x103 (= (prime_nat$ (nat$ (+ ?x90 1))) $x104)) (= $x95 (=> $x104 $x94)))))
+(let ((@x115 (trans @x109 (rewrite (= (=> $x104 $x94) (or $x110 $x94))) (= $x95 (or $x110 $x94)))))
+(let ((@x129 (trans (monotonicity @x115 (= $x96 (not (or $x110 $x94)))) (monotonicity @x124 (= (not (or $x110 $x94)) $x125)) (= $x96 $x125))))
+(let ((@x131 (not-or-elim (mp (asserted $x96) @x129 $x125) $x104)))
+(let ((@x479 (unit-resolution (unit-resolution (def-axiom (or $x678 $x110 $x338)) @x131 (or $x678 $x338)) @x553 $x338)))
+(let ((@x133 (not-or-elim (mp (asserted $x96) @x129 $x125) (not (>= ?x89 1)))))
+((_ th-lemma arith farkas -4 1 1) @x133 (unit-resolution (def-axiom (or $x683 $x668)) @x479 $x668) @x551 false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
diff -r e9f66b35d636 -r 959b0aed2ce5 src/HOL/SMT_Examples/SMT_Examples.thy
--- a/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Apr 09 17:21:10 2018 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Wed Apr 11 10:59:13 2018 +0200
@@ -396,7 +396,7 @@
    False \<or> P = (x - 1 = y) \<or> (\<not>P \<longrightarrow> False)"
   by smt
 
-lemma "int (nat \<bar>x::int\<bar>) = \<bar>x\<bar>" by smt
+lemma "int (nat \<bar>x::int\<bar>) = \<bar>x\<bar>" by (smt int_nat_eq)
 
 definition prime_nat :: "nat \<Rightarrow> bool" where
   "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
diff -r e9f66b35d636 -r 959b0aed2ce5 src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Mon Apr 09 17:21:10 2018 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Apr 11 10:59:13 2018 +0200
@@ -330,78 +330,85 @@
 (** embedding of standard natural number operations into integer operations **)
 
 local
-  val nat_embedding = @{thms nat_int' int_nat_nneg int_nat_neg}
-
   val simple_nat_ops = [
-    @{const less (nat)}, @{const less_eq (nat)},
+    @{const HOL.eq (nat)}, @{const less (nat)}, @{const less_eq (nat)},
     \<^const>\<open>Suc\<close>, @{const plus (nat)}, @{const minus (nat)}]
 
-  val mult_nat_ops =
+  val nat_consts = simple_nat_ops @
+    [@{const numeral (nat)}, @{const zero_class.zero (nat)}, @{const one_class.one (nat)}] @
     [@{const times (nat)}, @{const divide (nat)}, @{const modulo (nat)}]
 
-  val nat_ops = simple_nat_ops @ mult_nat_ops
-
-  val nat_consts = nat_ops @ [@{const numeral (nat)},
-    @{const zero_class.zero (nat)}, @{const one_class.one (nat)}]
-
-  val nat_int_coercions = [@{const of_nat (int)}, \<^const>\<open>nat\<close>]
-
-  val builtin_nat_ops = nat_int_coercions @ simple_nat_ops
-
   val is_nat_const = member (op aconv) nat_consts
 
-  fun is_nat_const' @{const of_nat (int)} = true
-    | is_nat_const' t = is_nat_const t
+  val nat_int_thm = Thm.symmetric (mk_meta_eq @{thm nat_int})
+  val nat_int_comp_thms = map mk_meta_eq @{thms nat_int_comparison}
+  val int_ops_thms = map mk_meta_eq @{thms int_ops}
+  val int_if_thm = mk_meta_eq @{thm int_if}
 
-  val expands = map mk_meta_eq @{thms nat_zero_as_int nat_one_as_int nat_numeral_as_int
-    nat_less_as_int nat_leq_as_int Suc_as_int nat_plus_as_int nat_minus_as_int nat_times_as_int
-    nat_div_as_int nat_mod_as_int}
-
-  val ints = map mk_meta_eq @{thms of_nat_0 of_nat_1 int_Suc int_plus int_minus of_nat_mult zdiv_int
-    zmod_int}
-  val int_if = mk_meta_eq @{lemma "int (if P then n else m) = (if P then int n else int m)" by simp}
+  fun if_conv cv1 cv2 = Conv.combination_conv (Conv.combination_conv (Conv.arg_conv cv1) cv2) cv2
 
-  fun mk_number_eq ctxt i lhs =
-    let
-      val eq = SMT_Util.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
-      val ctxt' = put_simpset HOL_ss ctxt addsimps @{thms of_nat_numeral}
-      val tac = HEADGOAL (Simplifier.simp_tac ctxt')
-    in Goal.norm_result ctxt (Goal.prove_internal ctxt [] eq (K tac)) end
-
-  fun ite_conv cv1 cv2 =
-    Conv.combination_conv (Conv.combination_conv (Conv.arg_conv cv1) cv2) cv2
-
-  fun int_conv ctxt ct =
+  fun int_ops_conv cv ctxt ct =
     (case Thm.term_of ct of
-      @{const of_nat (int)} $ (n as (@{const numeral (nat)} $ _)) =>
-        Conv.rewr_conv (mk_number_eq ctxt (snd (HOLogic.dest_number n)) ct)
+      @{const of_nat (int)} $ (Const (@{const_name If}, _) $ _ $ _ $ _) =>
+        Conv.rewr_conv int_if_thm then_conv
+        if_conv (cv ctxt) (int_ops_conv cv ctxt)
     | @{const of_nat (int)} $ _ =>
-        (Conv.rewrs_conv ints then_conv Conv.sub_conv ints_conv ctxt) else_conv
-        (Conv.rewr_conv int_if then_conv
-          ite_conv (nat_conv ctxt) (int_conv ctxt)) else_conv
-        Conv.sub_conv (Conv.top_sweep_conv nat_conv) ctxt
+        (Conv.rewrs_conv int_ops_thms then_conv
+          Conv.top_sweep_conv (int_ops_conv cv) ctxt) else_conv
+        Conv.arg_conv (Conv.sub_conv cv ctxt)
     | _ => Conv.no_conv) ct
 
-  and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt
+  val unfold_nat_let_conv = Conv.rewr_conv @{lemma "Let (n::nat) f \<equiv> f n" by (rule Let_def)}
+  val drop_nat_int_conv = Conv.rewr_conv (Thm.symmetric nat_int_thm)
+
+  fun nat_to_int_conv ctxt ct = (
+    Conv.top_conv (K (Conv.try_conv unfold_nat_let_conv)) ctxt then_conv
+    Conv.top_sweep_conv nat_conv ctxt then_conv
+    Conv.top_conv (K (Conv.try_conv drop_nat_int_conv)) ctxt) ct
+
+  and nat_conv ctxt ct = (
+      Conv.rewrs_conv (nat_int_thm :: nat_int_comp_thms) then_conv
+      Conv.top_sweep_conv (int_ops_conv nat_to_int_conv) ctxt) ct
 
-  and expand_conv ctxt =
-    SMT_Util.if_conv (is_nat_const o Term.head_of)
-      (expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt) (int_conv ctxt)
+  fun add_int_of_nat vs ct cu (q, cts) =
+    (case Thm.term_of ct of
+      @{const of_nat(int)} =>
+        if Term.exists_subterm (member (op aconv) vs) (Thm.term_of cu) then (true, cts)
+        else (q, insert (op aconvc) cu cts)
+    | _ => (q, cts))
 
-  and nat_conv ctxt = SMT_Util.if_exists_conv is_nat_const' (Conv.top_sweep_conv expand_conv ctxt)
+  fun add_apps f vs ct = 
+    (case Thm.term_of ct of
+      _ $ _ =>
+        let val (cu1, cu2) = Thm.dest_comb ct
+        in f vs cu1 cu2 #> add_apps f vs cu1 #> add_apps f vs cu2 end
+    | Abs _ =>
+        let val (cv, cu) = Thm.dest_abs NONE ct
+        in add_apps f (Thm.term_of cv :: vs) cu end
+    | _ => I)
 
-  val uses_nat_int = Term.exists_subterm (member (op aconv) nat_int_coercions)
+  val int_thm = @{lemma "(0::int) <= int (n::nat)" by simp}
+  val nat_int_thms = @{lemma
+    "\<forall>n::nat. (0::int) <= int n"
+    "\<forall>n::nat. nat (int n) = n"
+    "\<forall>i::int. int (nat i) = (if 0 <= i then i else 0)"
+    by simp_all}
+  val var = Term.dest_Var (Thm.term_of (funpow 3 Thm.dest_arg (Thm.cprop_of int_thm)))
 in
 
-val nat_as_int_conv = nat_conv
+fun nat_as_int_conv ctxt = SMT_Util.if_exists_conv is_nat_const (nat_to_int_conv ctxt)
 
-fun add_nat_embedding thms =
-  if exists (uses_nat_int o Thm.prop_of) thms then (thms, nat_embedding) else (thms, [])
+fun add_int_of_nat_constraints thms =
+  let val (q, cts) = fold (add_apps add_int_of_nat [] o Thm.cprop_of) thms (false, [])
+  in
+    if q then (thms, nat_int_thms)
+    else (thms, map (fn ct => Thm.instantiate ([], [(var, ct)]) int_thm) cts)
+  end
 
 val setup_nat_as_int =
   SMT_Builtin.add_builtin_typ_ext (\<^typ>\<open>nat\<close>,
     fn ctxt => K (Config.get ctxt SMT_Config.nat_as_int)) #>
-  fold (SMT_Builtin.add_builtin_fun_ext' o Term.dest_Const) builtin_nat_ops
+  fold (SMT_Builtin.add_builtin_fun_ext' o Term.dest_Const) simple_nat_ops
 
 end
 
@@ -454,7 +461,7 @@
 fun unfold_polymorph ctxt = map (apsnd (Conv.fconv_rule (unfold_conv ctxt)))
 fun unfold_monomorph ctxt =
   map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt)))
-  #> Config.get ctxt SMT_Config.nat_as_int ? burrow_ids add_nat_embedding
+  #> Config.get ctxt SMT_Config.nat_as_int ? burrow_ids add_int_of_nat_constraints
 
 
 (* overall normalization *)