--- a/src/HOL/SMT.thy Thu Jul 27 15:22:35 2017 +0100
+++ b/src/HOL/SMT.thy Fri Jul 28 15:36:32 2017 +0100
@@ -119,6 +119,26 @@
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
+
+lemmas nat_zero_as_int = transfer_nat_int_numerals(1)
+lemmas nat_one_as_int = transfer_nat_int_numerals(2)
+lemma nat_numeral_as_int: "numeral = (\<lambda>i. nat (numeral i))" by simp
+lemma nat_less_as_int: "op < = (\<lambda>a b. int a < int b)" by simp
+lemma nat_leq_as_int: "op \<le> = (\<lambda>a b. int a \<le> int b)" by simp
+lemma Suc_as_int: "Suc = (\<lambda>a. nat (int a + 1))" by (rule ext) simp
+lemma nat_plus_as_int: "op + = (\<lambda>a b. nat (int a + int b))" by (rule ext)+ simp
+lemma nat_minus_as_int: "op - = (\<lambda>a b. nat (int a - int b))" by (rule ext)+ simp
+lemma nat_times_as_int: "op * = (\<lambda>a b. nat (int a * int b))" by (simp add: nat_mult_distrib)
+lemma nat_div_as_int: "op div = (\<lambda>a b. nat (int a div int b))" by (simp add: nat_div_distrib)
+lemma nat_mod_as_int: "op mod = (\<lambda>a b. nat (int a mod int b))" by (simp add: nat_mod_distrib)
+
+lemma int_Suc: "int (Suc n) = int n + 1" by simp
+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
+
subsection \<open>Integer division and modulo for Z3\<close>