src/HOL/SMT.thy
changeset 66298 5ff9fe3fee66
parent 61799 4cf66f21b764
child 66323 c41642bc1ebb
     1.1 --- a/src/HOL/SMT.thy	Thu Jul 27 15:22:35 2017 +0100
     1.2 +++ b/src/HOL/SMT.thy	Fri Jul 28 15:36:32 2017 +0100
     1.3 @@ -119,6 +119,26 @@
     1.4  lemmas min_def_raw = min_def[abs_def]
     1.5  lemmas max_def_raw = max_def[abs_def]
     1.6  
     1.7 +lemma nat_int': "\<forall>n. nat (int n) = n" by simp
     1.8 +lemma int_nat_nneg: "\<forall>i. i \<ge> 0 \<longrightarrow> int (nat i) = i" by simp
     1.9 +lemma int_nat_neg: "\<forall>i. i < 0 \<longrightarrow> int (nat i) = 0" by simp
    1.10 +
    1.11 +lemmas nat_zero_as_int = transfer_nat_int_numerals(1)
    1.12 +lemmas nat_one_as_int = transfer_nat_int_numerals(2)
    1.13 +lemma nat_numeral_as_int: "numeral = (\<lambda>i. nat (numeral i))" by simp
    1.14 +lemma nat_less_as_int: "op < = (\<lambda>a b. int a < int b)" by simp
    1.15 +lemma nat_leq_as_int: "op \<le> = (\<lambda>a b. int a \<le> int b)" by simp
    1.16 +lemma Suc_as_int: "Suc = (\<lambda>a. nat (int a + 1))" by (rule ext) simp
    1.17 +lemma nat_plus_as_int: "op + = (\<lambda>a b. nat (int a + int b))" by (rule ext)+ simp
    1.18 +lemma nat_minus_as_int: "op - = (\<lambda>a b. nat (int a - int b))" by (rule ext)+ simp
    1.19 +lemma nat_times_as_int: "op * = (\<lambda>a b. nat (int a * int b))" by (simp add: nat_mult_distrib)
    1.20 +lemma nat_div_as_int: "op div = (\<lambda>a b. nat (int a div int b))" by (simp add: nat_div_distrib)
    1.21 +lemma nat_mod_as_int: "op mod = (\<lambda>a b. nat (int a mod int b))" by (simp add: nat_mod_distrib)
    1.22 +
    1.23 +lemma int_Suc: "int (Suc n) = int n + 1" by simp
    1.24 +lemma int_plus: "int (n + m) = int n + int m" by (rule of_nat_add)
    1.25 +lemma int_minus: "int (n - m) = int (nat (int n - int m))" by auto
    1.26 +
    1.27  
    1.28  subsection \<open>Integer division and modulo for Z3\<close>
    1.29