--- a/src/HOL/SMT_Examples/SMT_Tests.thy Mon Jul 28 11:03:28 2014 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy Sun Jul 27 21:20:11 2014 +0200
@@ -223,119 +223,6 @@
by smt2+
-section {* Natural numbers *}
-
-lemma
- "(0::nat) = 0"
- "(1::nat) = 1"
- "(0::nat) < 1"
- "(0::nat) \<le> 1"
- "(123456789::nat) < 2345678901"
- by smt2+
-
-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 smt2+
-
-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 smt2+
-
-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 smt2+
-
-lemma
- "(x::nat) * 0 = 0"
- "0 * x = 0"
- "x * 1 = x"
- "1 * x = x"
- "3 * x = x * 3"
- by smt2+
-
-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_new_extensions]]
- by smt2+
-
-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_new_extensions]]
- by smt2+
-
-lemma
- "(x::nat) = x div 1 * 1 + x mod 1"
- "x = x div 3 * 3 + x mod 3"
- using [[z3_new_extensions]]
- by smt2+
-
-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 smt2+
-
-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 smt2+
-
-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 smt2+
-
-
section {* Integers *}
lemma