diff -r d425bdf419f5 -r 5ff9fe3fee66 src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Thu Jul 27 15:22:35 2017 +0100
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Fri Jul 28 15:36:32 2017 +0100
@@ -222,6 +222,123 @@
   by smt+
 
 
+section {* Natural numbers *}
+
+declare [[smt_nat_as_int]]
+
+lemma
+  "(0::nat) = 0"
+  "(1::nat) = 1"
+  "(0::nat) < 1"
+  "(0::nat) \<le> 1"
+  "(123456789::nat) < 2345678901"
+  by smt+
+
+lemma
+  "Suc 0 = 1"
+  "Suc x = x + 1"
+  "x < Suc x"
+  "(Suc x = Suc y) = (x = y)"
+  "Suc (x + y) < Suc x + Suc y"
+  by smt+
+
+lemma
+  "(x::nat) + 0 = x"
+  "0 + x = x"
+  "x + y = y + x"
+  "x + (y + z) = (x + y) + z"
+  "(x + y = 0) = (x = 0 \<and> y = 0)"
+  by smt+
+
+lemma
+  "(x::nat) - 0 = x"
+  "x < y \<longrightarrow> x - y = 0"
+  "x - y = 0 \<or> y - x = 0"
+  "(x - y) + y = (if x < y then y else x)"
+  "x - y - z = x - (y + z)"
+  by smt+
+
+lemma
+  "(x::nat) * 0 = 0"
+  "0 * x = 0"
+  "x * 1 = x"
+  "1 * x = x"
+  "3 * x = x * 3"
+  by smt+
+
+lemma
+  "(0::nat) div 0 = 0"
+  "(x::nat) div 0 = 0"
+  "(0::nat) div 1 = 0"
+  "(1::nat) div 1 = 1"
+  "(3::nat) div 1 = 3"
+  "(x::nat) div 1 = x"
+  "(0::nat) div 3 = 0"
+  "(1::nat) div 3 = 0"
+  "(3::nat) div 3 = 1"
+  "(x::nat) div 3 \<le> x"
+  "(x div 3 = x) = (x = 0)"
+  using [[z3_extensions]]
+  by smt+
+
+lemma
+  "(0::nat) mod 0 = 0"
+  "(x::nat) mod 0 = x"
+  "(0::nat) mod 1 = 0"
+  "(1::nat) mod 1 = 0"
+  "(3::nat) mod 1 = 0"
+  "(x::nat) mod 1 = 0"
+  "(0::nat) mod 3 = 0"
+  "(1::nat) mod 3 = 1"
+  "(3::nat) mod 3 = 0"
+  "x mod 3 < 3"
+  "(x mod 3 = x) = (x < 3)"
+  using [[z3_extensions]]
+  by smt+
+
+lemma
+  "(x::nat) = x div 1 * 1 + x mod 1"
+  "x = x div 3 * 3 + x mod 3"
+  using [[z3_extensions]]
+  by smt+
+
+lemma
+  "min (x::nat) y \<le> x"
+  "min x y \<le> y"
+  "min x y \<le> x + y"
+  "z < x \<and> z < y \<longrightarrow> z < min x y"
+  "min x y = min y x"
+  "min x 0 = 0"
+  by smt+
+
+lemma
+  "max (x::nat) y \<ge> x"
+  "max x y \<ge> y"
+  "max x y \<ge> (x - y) + (y - x)"
+  "z > x \<and> z > y \<longrightarrow> z > max x y"
+  "max x y = max y x"
+  "max x 0 = x"
+  by smt+
+
+lemma
+  "0 \<le> (x::nat)"
+  "0 < x \<and> x \<le> 1 \<longrightarrow> x = 1"
+  "x \<le> x"
+  "x \<le> y \<longrightarrow> 3 * x \<le> 3 * y"
+  "x < y \<longrightarrow> 3 * x < 3 * y"
+  "x < y \<longrightarrow> x \<le> y"
+  "(x < y) = (x + 1 \<le> y)"
+  "\<not> (x < x)"
+  "x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
+  "x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
+  "x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z"
+  "x < y \<longrightarrow> y < z \<longrightarrow> x < z"
+  "x < y \<and> y < z \<longrightarrow> \<not> (z < x)"
+  by smt+
+
+declare [[smt_nat_as_int = false]]
+
+
 section \<open>Integers\<close>
 
 lemma