--- 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