src/HOL/SMT_Examples/SMT_Tests.thy

   "(p \<or> q) \<and> \<not> p \<Longrightarrow> q"
   "(a \<and> b) \<or> (c \<and> d) \<Longrightarrow> (a \<and> b) \<or> (c \<and> d)"
   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
   "(0::int) = 0"
   "(0::int) = (- 0)"