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.15
1.16
1.17  subsection{*The @{text "\<le>"} Ordering*}
1.18 @@ -294,18 +297,15 @@
1.20  done
1.21
1.22 -lemma int_of_nat_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})"
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.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.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.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.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.156 +lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)"
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.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.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.197 -    "(w < z) = (\<exists>n. z = w + int_of_nat (Suc n))"
1.199 +    "(w < z) = (\<exists>n. z = w + int (Suc n))"
1.200  apply (cases z, cases w)
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.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.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.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.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.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.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.469 -val zless_int = @{thm zless_int};