src/HOL/IntDef.thy
changeset 23365 f31794033ae1
parent 23308 95a01ddfb024
child 23372 0035be079bee
     1.1 --- a/src/HOL/IntDef.thy	Wed Jun 13 03:28:21 2007 +0200
     1.2 +++ b/src/HOL/IntDef.thy	Wed Jun 13 03:31:11 2007 +0200
     1.3 @@ -219,9 +219,12 @@
     1.4  qed
     1.5  
     1.6  abbreviation
     1.7 -  int_of_nat :: "nat \<Rightarrow> int"
     1.8 +  int :: "nat \<Rightarrow> int"
     1.9  where
    1.10 -  "int_of_nat \<equiv> of_nat"
    1.11 +  "int \<equiv> of_nat"
    1.12 +
    1.13 +lemma int_def: "int m = Abs_Integ (intrel `` {(m, 0)})"
    1.14 +by (induct m, simp_all add: Zero_int_def One_int_def add)
    1.15  
    1.16  
    1.17  subsection{*The @{text "\<le>"} Ordering*}
    1.18 @@ -294,18 +297,15 @@
    1.19  apply (simp_all add: add_strict_mono)
    1.20  done
    1.21  
    1.22 -lemma int_of_nat_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})"
    1.23 -by (induct m, simp_all add: Zero_int_def One_int_def add)
    1.24 -
    1.25  lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = of_nat n"
    1.26  apply (cases k)
    1.27 -apply (auto simp add: le add int_of_nat_def Zero_int_def)
    1.28 +apply (auto simp add: le add int_def Zero_int_def)
    1.29  apply (rule_tac x="x-y" in exI, simp)
    1.30  done
    1.31  
    1.32  lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = of_nat n"
    1.33  apply (cases k)
    1.34 -apply (simp add: less int_of_nat_def Zero_int_def)
    1.35 +apply (simp add: less int_def Zero_int_def)
    1.36  apply (rule_tac x="x-y" in exI, simp)
    1.37  done
    1.38  
    1.39 @@ -352,16 +352,16 @@
    1.40      by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
    1.41  qed
    1.42  
    1.43 -lemma nat_int_of_nat [simp]: "nat (int_of_nat n) = n"
    1.44 -by (simp add: nat int_of_nat_def)
    1.45 +lemma nat_int [simp]: "nat (int n) = n"
    1.46 +by (simp add: nat int_def)
    1.47  
    1.48  lemma nat_zero [simp]: "nat 0 = 0"
    1.49  by (simp add: Zero_int_def nat)
    1.50  
    1.51 -lemma int_of_nat_nat_eq [simp]: "int_of_nat (nat z) = (if 0 \<le> z then z else 0)"
    1.52 -by (cases z, simp add: nat le int_of_nat_def Zero_int_def)
    1.53 +lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
    1.54 +by (cases z, simp add: nat le int_def Zero_int_def)
    1.55  
    1.56 -corollary nat_0_le': "0 \<le> z ==> int_of_nat (nat z) = z"
    1.57 +corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
    1.58  by simp
    1.59  
    1.60  lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
    1.61 @@ -379,27 +379,27 @@
    1.62  corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
    1.63  by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
    1.64  
    1.65 -lemma zless_nat_conj: "(nat w < nat z) = (0 < z & w < z)"
    1.66 +lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
    1.67  apply (cases w, cases z) 
    1.68  apply (simp add: nat le Zero_int_def linorder_not_le [symmetric], arith)
    1.69  done
    1.70  
    1.71 -lemma nonneg_eq_int_of_nat: "[| 0 \<le> z;  !!m. z = int_of_nat m ==> P |] ==> P"
    1.72 -by (blast dest: nat_0_le' sym)
    1.73 +lemma nonneg_eq_int: "[| 0 \<le> z;  !!m. z = int m ==> P |] ==> P"
    1.74 +by (blast dest: nat_0_le sym)
    1.75  
    1.76 -lemma nat_eq_iff': "(nat w = m) = (if 0 \<le> w then w = int_of_nat m else m=0)"
    1.77 -by (cases w, simp add: nat le int_of_nat_def Zero_int_def, arith)
    1.78 +lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
    1.79 +by (cases w, simp add: nat le int_def Zero_int_def, arith)
    1.80  
    1.81 -corollary nat_eq_iff2': "(m = nat w) = (if 0 \<le> w then w = int_of_nat m else m=0)"
    1.82 -by (simp only: eq_commute [of m] nat_eq_iff')
    1.83 +corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
    1.84 +by (simp only: eq_commute [of m] nat_eq_iff)
    1.85  
    1.86 -lemma nat_less_iff': "0 \<le> w ==> (nat w < m) = (w < int_of_nat m)"
    1.87 +lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < int m)"
    1.88  apply (cases w)
    1.89 -apply (simp add: nat le int_of_nat_def Zero_int_def linorder_not_le [symmetric], arith)
    1.90 +apply (simp add: nat le int_def Zero_int_def linorder_not_le [symmetric], arith)
    1.91  done
    1.92  
    1.93 -lemma int_of_nat_eq_iff: "(int_of_nat m = z) = (m = nat z & 0 \<le> z)"
    1.94 -by (auto simp add: nat_eq_iff2')
    1.95 +lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \<le> z)"
    1.96 +by (auto simp add: nat_eq_iff2)
    1.97  
    1.98  lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
    1.99  by (insert zless_nat_conj [of 0], auto)
   1.100 @@ -413,42 +413,41 @@
   1.101  by (cases z, cases z', 
   1.102      simp add: nat add minus diff_minus le Zero_int_def)
   1.103  
   1.104 -lemma nat_zminus_int_of_nat [simp]: "nat (- (int_of_nat n)) = 0"
   1.105 -by (simp add: int_of_nat_def minus nat Zero_int_def) 
   1.106 +lemma nat_zminus_int [simp]: "nat (- (int n)) = 0"
   1.107 +by (simp add: int_def minus nat Zero_int_def) 
   1.108  
   1.109 -lemma zless_nat_eq_int_zless': "(m < nat z) = (int_of_nat m < z)"
   1.110 -by (cases z, simp add: nat less int_of_nat_def, arith)
   1.111 +lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
   1.112 +by (cases z, simp add: nat less int_def, arith)
   1.113  
   1.114  
   1.115  subsection{*Lemmas about the Function @{term int} and Orderings*}
   1.116  
   1.117 -lemma negative_zless_0': "- (int_of_nat (Suc n)) < 0"
   1.118 +lemma negative_zless_0: "- (int (Suc n)) < 0"
   1.119  by (simp add: order_less_le del: of_nat_Suc)
   1.120  
   1.121 -lemma negative_zless' [iff]: "- (int_of_nat (Suc n)) < int_of_nat m"
   1.122 -by (rule negative_zless_0' [THEN order_less_le_trans], simp)
   1.123 +lemma negative_zless [iff]: "- (int (Suc n)) < int m"
   1.124 +by (rule negative_zless_0 [THEN order_less_le_trans], simp)
   1.125  
   1.126 -lemma negative_zle_0': "- int_of_nat n \<le> 0"
   1.127 +lemma negative_zle_0: "- int n \<le> 0"
   1.128  by (simp add: minus_le_iff)
   1.129  
   1.130 -lemma negative_zle' [iff]: "- int_of_nat n \<le> int_of_nat m"
   1.131 -by (rule order_trans [OF negative_zle_0' of_nat_0_le_iff])
   1.132 +lemma negative_zle [iff]: "- int n \<le> int m"
   1.133 +by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
   1.134  
   1.135 -lemma not_zle_0_negative' [simp]: "~ (0 \<le> - (int_of_nat (Suc n)))"
   1.136 +lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
   1.137  by (subst le_minus_iff, simp del: of_nat_Suc)
   1.138  
   1.139 -lemma int_zle_neg': "(int_of_nat n \<le> - int_of_nat m) = (n = 0 & m = 0)"
   1.140 -by (simp add: int_of_nat_def le minus Zero_int_def)
   1.141 +lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
   1.142 +by (simp add: int_def le minus Zero_int_def)
   1.143  
   1.144 -lemma not_int_zless_negative' [simp]: "~ (int_of_nat n < - int_of_nat m)"
   1.145 +lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
   1.146  by (simp add: linorder_not_less)
   1.147  
   1.148 -lemma negative_eq_positive' [simp]:
   1.149 -  "(- int_of_nat n = int_of_nat m) = (n = 0 & m = 0)"
   1.150 -by (force simp add: order_eq_iff [of "- int_of_nat n"] int_zle_neg')
   1.151 +lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)"
   1.152 +by (force simp add: order_eq_iff [of "- int n"] int_zle_neg)
   1.153  
   1.154 -lemma zle_iff_zadd': "(w \<le> z) = (\<exists>n. z = w + int_of_nat n)"
   1.155 -proof (cases w, cases z, simp add: le add int_of_nat_def)
   1.156 +lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)"
   1.157 +proof (cases w, cases z, simp add: le add int_def)
   1.158    fix a b c d
   1.159    assume "w = Abs_Integ (intrel `` {(a,b)})" "z = Abs_Integ (intrel `` {(c,d)})"
   1.160    show "(a+d \<le> c+b) = (\<exists>n. c+b = a+n+d)"
   1.161 @@ -487,10 +486,10 @@
   1.162  where
   1.163    "iszero z \<longleftrightarrow> z = 0"
   1.164  
   1.165 -lemma not_neg_int_of_nat [simp]: "~ neg (int_of_nat n)"
   1.166 +lemma not_neg_int [simp]: "~ neg (int n)"
   1.167  by (simp add: neg_def)
   1.168  
   1.169 -lemma neg_zminus_int_of_nat [simp]: "neg (- (int_of_nat (Suc n)))"
   1.170 +lemma neg_zminus_int [simp]: "neg (- (int (Suc n)))"
   1.171  by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
   1.172  
   1.173  lemmas neg_eq_less_0 = neg_def
   1.174 @@ -516,7 +515,7 @@
   1.175  lemma neg_nat: "neg z ==> nat z = 0"
   1.176  by (simp add: neg_def order_less_imp_le) 
   1.177  
   1.178 -lemma not_neg_nat': "~ neg z ==> int_of_nat (nat z) = z"
   1.179 +lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
   1.180  by (simp add: linorder_not_less neg_def)
   1.181  
   1.182  
   1.183 @@ -645,7 +644,7 @@
   1.184    fix z
   1.185    show "of_int z = id z"
   1.186      by (cases z)
   1.187 -      (simp add: of_int add minus int_of_nat_def diff_minus)
   1.188 +      (simp add: of_int add minus int_def diff_minus)
   1.189  qed
   1.190  
   1.191  
   1.192 @@ -764,245 +763,80 @@
   1.193  text{*Now we replace the case analysis rule by a more conventional one:
   1.194  whether an integer is negative or not.*}
   1.195  
   1.196 -lemma zless_iff_Suc_zadd':
   1.197 -    "(w < z) = (\<exists>n. z = w + int_of_nat (Suc n))"
   1.198 +lemma zless_iff_Suc_zadd:
   1.199 +    "(w < z) = (\<exists>n. z = w + int (Suc n))"
   1.200  apply (cases z, cases w)
   1.201 -apply (auto simp add: le add int_of_nat_def linorder_not_le [symmetric]) 
   1.202 +apply (auto simp add: le add int_def linorder_not_le [symmetric]) 
   1.203  apply (rename_tac a b c d) 
   1.204  apply (rule_tac x="a+d - Suc(c+b)" in exI) 
   1.205  apply arith
   1.206  done
   1.207  
   1.208 -lemma negD': "x<0 ==> \<exists>n. x = - (int_of_nat (Suc n))"
   1.209 +lemma negD: "x<0 ==> \<exists>n. x = - (int (Suc n))"
   1.210  apply (cases x)
   1.211 -apply (auto simp add: le minus Zero_int_def int_of_nat_def order_less_le)
   1.212 +apply (auto simp add: le minus Zero_int_def int_def order_less_le)
   1.213  apply (rule_tac x="y - Suc x" in exI, arith)
   1.214  done
   1.215  
   1.216 -theorem int_cases' [cases type: int, case_names nonneg neg]:
   1.217 -     "[|!! n. z = int_of_nat n ==> P;  !! n. z =  - (int_of_nat (Suc n)) ==> P |] ==> P"
   1.218 -apply (cases "z < 0", blast dest!: negD')
   1.219 +theorem int_cases [cases type: int, case_names nonneg neg]:
   1.220 +     "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
   1.221 +apply (cases "z < 0", blast dest!: negD)
   1.222  apply (simp add: linorder_not_less del: of_nat_Suc)
   1.223 -apply (blast dest: nat_0_le' [THEN sym])
   1.224 +apply (blast dest: nat_0_le [THEN sym])
   1.225  done
   1.226  
   1.227 -theorem int_induct' [induct type: int, case_names nonneg neg]:
   1.228 -     "[|!! n. P (int_of_nat n);  !!n. P (- (int_of_nat (Suc n))) |] ==> P z"
   1.229 -  by (cases z rule: int_cases') auto
   1.230 +theorem int_induct'[induct type: int, case_names nonneg neg]:
   1.231 +     "[|!! n. P (int n);  !!n. P (- (int (Suc n))) |] ==> P z"
   1.232 +  by (cases z rule: int_cases) auto
   1.233  
   1.234  text{*Contributed by Brian Huffman*}
   1.235 -theorem int_diff_cases' [case_names diff]:
   1.236 -assumes prem: "!!m n. z = int_of_nat m - int_of_nat n ==> P" shows "P"
   1.237 +theorem int_diff_cases [case_names diff]:
   1.238 +assumes prem: "!!m n. z = int m - int n ==> P" shows "P"
   1.239  apply (cases z rule: eq_Abs_Integ)
   1.240  apply (rule_tac m=x and n=y in prem)
   1.241 -apply (simp add: int_of_nat_def diff_def minus add)
   1.242 +apply (simp add: int_def diff_def minus add)
   1.243  done
   1.244  
   1.245  lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z"
   1.246  by (cases z rule: eq_Abs_Integ, simp add: nat le of_int Zero_int_def)
   1.247  
   1.248 -lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
   1.249  
   1.250 -
   1.251 -subsection{*@{term int}: Embedding the Naturals into the Integers*}
   1.252 -
   1.253 -definition
   1.254 -  int :: "nat \<Rightarrow> int"
   1.255 -where
   1.256 -  [code func del]: "int m = Abs_Integ (intrel `` {(m, 0)})"
   1.257 -
   1.258 -text{*Agreement with the specific embedding for the integers*}
   1.259 -lemma int_eq_of_nat: "int = (of_nat :: nat => int)"
   1.260 -by (simp add: expand_fun_eq int_of_nat_def int_def)
   1.261 -
   1.262 -lemma inj_int: "inj int"
   1.263 -by (simp add: inj_on_def int_def)
   1.264 -
   1.265 -lemma int_int_eq [iff]: "(int m = int n) = (m = n)"
   1.266 -unfolding int_eq_of_nat by (rule of_nat_eq_iff)
   1.267 -
   1.268 -lemma zadd_int: "(int m) + (int n) = int (m + n)"
   1.269 -unfolding int_eq_of_nat by (rule of_nat_add [symmetric])
   1.270 +subsection {* Legacy theorems *}
   1.271  
   1.272  lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z"
   1.273 -unfolding int_eq_of_nat by simp
   1.274 -
   1.275 -lemma int_mult: "int (m * n) = (int m) * (int n)"
   1.276 -unfolding int_eq_of_nat by (rule of_nat_mult)
   1.277 -
   1.278 -text{*Compatibility binding*}
   1.279 -lemmas zmult_int = int_mult [symmetric]
   1.280 -
   1.281 -lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)"
   1.282 -unfolding int_eq_of_nat by (rule of_nat_eq_0_iff)
   1.283 -
   1.284 -lemma zless_int [simp]: "(int m < int n) = (m<n)"
   1.285 -unfolding int_eq_of_nat by (rule of_nat_less_iff)
   1.286 -
   1.287 -lemma int_less_0_conv [simp]: "~ (int k < 0)"
   1.288 -unfolding int_eq_of_nat by (rule of_nat_less_0_iff)
   1.289 -
   1.290 -lemma zero_less_int_conv [simp]: "(0 < int n) = (0 < n)"
   1.291 -unfolding int_eq_of_nat by (rule of_nat_0_less_iff)
   1.292 -
   1.293 -lemma zle_int [simp]: "(int m \<le> int n) = (m\<le>n)"
   1.294 -unfolding int_eq_of_nat by (rule of_nat_le_iff)
   1.295 -
   1.296 -lemma zero_zle_int [simp]: "(0 \<le> int n)"
   1.297 -unfolding int_eq_of_nat by (rule of_nat_0_le_iff)
   1.298 -
   1.299 -lemma int_le_0_conv [simp]: "(int n \<le> 0) = (n = 0)"
   1.300 -unfolding int_eq_of_nat by (rule of_nat_le_0_iff)
   1.301 -
   1.302 -lemma int_0 [simp]: "int 0 = (0::int)"
   1.303 -unfolding int_eq_of_nat by (rule of_nat_0)
   1.304 -
   1.305 -lemma int_1 [simp]: "int 1 = 1"
   1.306 -unfolding int_eq_of_nat by (rule of_nat_1)
   1.307 -
   1.308 -lemma int_Suc0_eq_1: "int (Suc 0) = 1"
   1.309 -unfolding int_eq_of_nat by simp
   1.310 +by simp
   1.311  
   1.312  lemma int_Suc: "int (Suc m) = 1 + (int m)"
   1.313 -unfolding int_eq_of_nat by simp
   1.314 -
   1.315 -lemma nat_int [simp]: "nat(int n) = n"
   1.316 -unfolding int_eq_of_nat by (rule nat_int_of_nat)
   1.317 -
   1.318 -lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
   1.319 -unfolding int_eq_of_nat by (rule int_of_nat_nat_eq)
   1.320 -
   1.321 -corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
   1.322 -unfolding int_eq_of_nat by (rule nat_0_le')
   1.323 -
   1.324 -lemma nonneg_eq_int: "[| 0 \<le> z;  !!m. z = int m ==> P |] ==> P"
   1.325 -unfolding int_eq_of_nat by (blast elim: nonneg_eq_int_of_nat)
   1.326 -
   1.327 -lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
   1.328 -unfolding int_eq_of_nat by (rule nat_eq_iff')
   1.329 -
   1.330 -corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
   1.331 -unfolding int_eq_of_nat by (rule nat_eq_iff2')
   1.332 -
   1.333 -lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < int m)"
   1.334 -unfolding int_eq_of_nat by (rule nat_less_iff')
   1.335 -
   1.336 -lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \<le> z)"
   1.337 -unfolding int_eq_of_nat by (rule int_of_nat_eq_iff)
   1.338 -
   1.339 -lemma nat_zminus_int [simp]: "nat (- (int n)) = 0"
   1.340 -unfolding int_eq_of_nat by (rule nat_zminus_int_of_nat)
   1.341 -
   1.342 -lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
   1.343 -unfolding int_eq_of_nat by (rule zless_nat_eq_int_zless')
   1.344 +by simp
   1.345  
   1.346 -lemma negative_zless_0: "- (int (Suc n)) < 0"
   1.347 -unfolding int_eq_of_nat by (rule negative_zless_0')
   1.348 -
   1.349 -lemma negative_zless [iff]: "- (int (Suc n)) < int m"
   1.350 -unfolding int_eq_of_nat by (rule negative_zless')
   1.351 -
   1.352 -lemma negative_zle_0: "- int n \<le> 0"
   1.353 -unfolding int_eq_of_nat by (rule negative_zle_0')
   1.354 -
   1.355 -lemma negative_zle [iff]: "- int n \<le> int m"
   1.356 -unfolding int_eq_of_nat by (rule negative_zle')
   1.357 -
   1.358 -lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
   1.359 -unfolding int_eq_of_nat by (rule not_zle_0_negative')
   1.360 -
   1.361 -lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
   1.362 -unfolding int_eq_of_nat by (rule int_zle_neg')
   1.363 -
   1.364 -lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
   1.365 -unfolding int_eq_of_nat by (rule not_int_zless_negative')
   1.366 -
   1.367 -lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)"
   1.368 -unfolding int_eq_of_nat by (rule negative_eq_positive')
   1.369 -
   1.370 -lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)"
   1.371 -unfolding int_eq_of_nat by (rule zle_iff_zadd')
   1.372 -
   1.373 -lemma abs_int_eq [simp]: "abs (int m) = int m"
   1.374 -unfolding int_eq_of_nat by (rule abs_of_nat)
   1.375 -
   1.376 -lemma not_neg_int [simp]: "~ neg(int n)"
   1.377 -unfolding int_eq_of_nat by (rule not_neg_int_of_nat)
   1.378 -
   1.379 -lemma neg_zminus_int [simp]: "neg(- (int (Suc n)))"
   1.380 -unfolding int_eq_of_nat by (rule neg_zminus_int_of_nat)
   1.381 +lemma int_Suc0_eq_1: "int (Suc 0) = 1"
   1.382 +by simp
   1.383  
   1.384 -lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
   1.385 -unfolding int_eq_of_nat by (rule not_neg_nat')
   1.386 -
   1.387 -lemma of_int_int_eq [simp]: "of_int (int n) = of_nat n"
   1.388 -unfolding int_eq_of_nat by (rule of_int_of_nat_eq)
   1.389 -
   1.390 -lemma int_setsum: "int (setsum f A) = (\<Sum>x\<in>A. int(f x))"
   1.391 -unfolding int_eq_of_nat by (rule of_nat_setsum)
   1.392 -
   1.393 -lemma int_setprod: "int (setprod f A) = (\<Prod>x\<in>A. int(f x))"
   1.394 -unfolding int_eq_of_nat by (rule of_nat_setprod)
   1.395 -
   1.396 -text{*Now we replace the case analysis rule by a more conventional one:
   1.397 -whether an integer is negative or not.*}
   1.398 -
   1.399 -lemma zless_iff_Suc_zadd:
   1.400 -    "(w < z) = (\<exists>n. z = w + int(Suc n))"
   1.401 -unfolding int_eq_of_nat by (rule zless_iff_Suc_zadd')
   1.402 -
   1.403 -lemma negD: "x<0 ==> \<exists>n. x = - (int (Suc n))"
   1.404 -unfolding int_eq_of_nat by (rule negD')
   1.405 -
   1.406 -theorem int_cases [cases type: int, case_names nonneg neg]:
   1.407 -     "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
   1.408 -unfolding int_eq_of_nat
   1.409 -apply (cases "z < 0", blast dest!: negD')
   1.410 -apply (simp add: linorder_not_less)
   1.411 -apply (blast dest: nat_0_le' [THEN sym])
   1.412 -done
   1.413 -
   1.414 -theorem int_induct [induct type: int, case_names nonneg neg]:
   1.415 -     "[|!! n. P (int n);  !!n. P (- (int (Suc n))) |] ==> P z"
   1.416 -  by (cases z) auto
   1.417 +lemmas inj_int = inj_of_nat [where 'a=int]
   1.418 +lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
   1.419 +lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
   1.420 +lemmas int_mult = of_nat_mult [where 'a=int]
   1.421 +lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
   1.422 +lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int]
   1.423 +lemmas zless_int = of_nat_less_iff [where 'a=int]
   1.424 +lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int]
   1.425 +lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
   1.426 +lemmas zle_int = of_nat_le_iff [where 'a=int]
   1.427 +lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
   1.428 +lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int]
   1.429 +lemmas int_0 = of_nat_0 [where ?'a_1.0=int]
   1.430 +lemmas int_1 = of_nat_1 [where 'a=int]
   1.431 +lemmas abs_int_eq = abs_of_nat [where 'a=int]
   1.432 +lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
   1.433 +lemmas int_setsum = of_nat_setsum [where 'a=int]
   1.434 +lemmas int_setprod = of_nat_setprod [where 'a=int]
   1.435 +lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
   1.436 +lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
   1.437 +lemmas int_eq_of_nat = TrueI
   1.438  
   1.439 -text{*Contributed by Brian Huffman*}
   1.440 -theorem int_diff_cases [case_names diff]:
   1.441 -assumes prem: "!!m n. z = int m - int n ==> P" shows "P"
   1.442 - apply (rule_tac z=z in int_cases)
   1.443 -  apply (rule_tac m=n and n=0 in prem, simp)
   1.444 - apply (rule_tac m=0 and n="Suc n" in prem, simp)
   1.445 -done
   1.446 -
   1.447 -lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
   1.448 -
   1.449 -lemmas [simp] = int_Suc
   1.450 -
   1.451 -
   1.452 -subsection {* Legacy ML bindings *}
   1.453 -
   1.454 -ML {*
   1.455 -val of_nat_0 = @{thm of_nat_0};
   1.456 -val of_nat_1 = @{thm of_nat_1};
   1.457 -val of_nat_Suc = @{thm of_nat_Suc};
   1.458 -val of_nat_add = @{thm of_nat_add};
   1.459 -val of_nat_mult = @{thm of_nat_mult};
   1.460 -val of_int_0 = @{thm of_int_0};
   1.461 -val of_int_1 = @{thm of_int_1};
   1.462 -val of_int_add = @{thm of_int_add};
   1.463 -val of_int_mult = @{thm of_int_mult};
   1.464 -val int_eq_of_nat = @{thm int_eq_of_nat};
   1.465 -val zle_int = @{thm zle_int};
   1.466 -val int_int_eq = @{thm int_int_eq};
   1.467 -val diff_int_def = @{thm diff_int_def};
   1.468 -val zadd_ac = @{thms zadd_ac};
   1.469 -val zless_int = @{thm zless_int};
   1.470 -val zadd_int = @{thm zadd_int};
   1.471 -val zmult_int = @{thm zmult_int};
   1.472 -val nat_0_le = @{thm nat_0_le};
   1.473 -val int_0 = @{thm int_0};
   1.474 -val int_1 = @{thm int_1};
   1.475 -val abs_split = @{thm abs_split};
   1.476 -*}
   1.477 +abbreviation
   1.478 +  int_of_nat :: "nat \<Rightarrow> int"
   1.479 +where
   1.480 +  "int_of_nat \<equiv> of_nat"
   1.481  
   1.482  end