src/HOL/IntDef.thy
changeset 23303 6091e530ff77
parent 23299 292b1cbd05dc
child 23307 2fe3345035c7
     1.1 --- a/src/HOL/IntDef.thy	Sun Jun 10 23:48:27 2007 +0200
     1.2 +++ b/src/HOL/IntDef.thy	Mon Jun 11 00:53:18 2007 +0200
     1.3 @@ -22,11 +22,6 @@
     1.4    int = "UNIV//intrel"
     1.5    by (auto simp add: quotient_def)
     1.6  
     1.7 -definition
     1.8 -  int :: "nat \<Rightarrow> int"
     1.9 -where
    1.10 -  [code func del]: "int m = Abs_Integ (intrel `` {(m, 0)})"
    1.11 -
    1.12  instance int :: zero
    1.13    Zero_int_def: "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})" ..
    1.14  
    1.15 @@ -223,6 +218,11 @@
    1.16    show "0 \<noteq> (1::int)" by (simp add: Zero_int_def One_int_def)
    1.17  qed
    1.18  
    1.19 +abbreviation
    1.20 +  int_of_nat :: "nat \<Rightarrow> int"
    1.21 +where
    1.22 +  "int_of_nat \<equiv> of_nat"
    1.23 +
    1.24  
    1.25  subsection{*The @{text "\<le>"} Ordering*}
    1.26  
    1.27 @@ -337,60 +337,6 @@
    1.28  done
    1.29  
    1.30  
    1.31 -subsection{*@{term int}: Embedding the Naturals into the Integers*}
    1.32 -
    1.33 -lemma inj_int: "inj int"
    1.34 -by (simp add: inj_on_def int_def)
    1.35 -
    1.36 -lemma int_int_eq [iff]: "(int m = int n) = (m = n)"
    1.37 -by (fast elim!: inj_int [THEN injD])
    1.38 -
    1.39 -lemma zadd_int: "(int m) + (int n) = int (m + n)"
    1.40 -  by (simp add: int_def add)
    1.41 -
    1.42 -lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z"
    1.43 -  by (simp add: zadd_int zadd_assoc [symmetric])
    1.44 -
    1.45 -lemma int_mult: "int (m * n) = (int m) * (int n)"
    1.46 -by (simp add: int_def mult)
    1.47 -
    1.48 -text{*Compatibility binding*}
    1.49 -lemmas zmult_int = int_mult [symmetric]
    1.50 -
    1.51 -lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)"
    1.52 -by (simp add: Zero_int_def [folded int_def])
    1.53 -
    1.54 -lemma zless_int [simp]: "(int m < int n) = (m<n)"
    1.55 -by (simp add: le add int_def linorder_not_le [symmetric]) 
    1.56 -
    1.57 -lemma int_less_0_conv [simp]: "~ (int k < 0)"
    1.58 -by (simp add: Zero_int_def [folded int_def])
    1.59 -
    1.60 -lemma zero_less_int_conv [simp]: "(0 < int n) = (0 < n)"
    1.61 -by (simp add: Zero_int_def [folded int_def])
    1.62 -
    1.63 -lemma zle_int [simp]: "(int m \<le> int n) = (m\<le>n)"
    1.64 -by (simp add: linorder_not_less [symmetric])
    1.65 -
    1.66 -lemma zero_zle_int [simp]: "(0 \<le> int n)"
    1.67 -by (simp add: Zero_int_def [folded int_def])
    1.68 -
    1.69 -lemma int_le_0_conv [simp]: "(int n \<le> 0) = (n = 0)"
    1.70 -by (simp add: Zero_int_def [folded int_def])
    1.71 -
    1.72 -lemma int_0 [simp]: "int 0 = (0::int)"
    1.73 -by (simp add: Zero_int_def [folded int_def])
    1.74 -
    1.75 -lemma int_1 [simp]: "int 1 = 1"
    1.76 -by (simp add: One_int_def [folded int_def])
    1.77 -
    1.78 -lemma int_Suc0_eq_1: "int (Suc 0) = 1"
    1.79 -by (simp add: One_int_def [folded int_def])
    1.80 -
    1.81 -lemma int_Suc: "int (Suc m) = 1 + (int m)"
    1.82 -by (simp add: One_int_def [folded int_def] zadd_int)
    1.83 -
    1.84 -
    1.85  subsection{*Magnitude of an Integer, as a Natural Number: @{term nat}*}
    1.86  
    1.87  definition
    1.88 @@ -406,24 +352,24 @@
    1.89      by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
    1.90  qed
    1.91  
    1.92 -lemma nat_int [simp]: "nat(int n) = n"
    1.93 -by (simp add: nat int_def) 
    1.94 +lemma nat_int_of_nat [simp]: "nat (int_of_nat n) = n"
    1.95 +by (simp add: nat int_of_nat_def)
    1.96  
    1.97  lemma nat_zero [simp]: "nat 0 = 0"
    1.98 -by (simp only: Zero_int_def [folded int_def] nat_int)
    1.99 +by (simp add: Zero_int_def nat)
   1.100  
   1.101 -lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
   1.102 -by (cases z, simp add: nat le int_def Zero_int_def)
   1.103 +lemma int_of_nat_nat_eq [simp]: "int_of_nat (nat z) = (if 0 \<le> z then z else 0)"
   1.104 +by (cases z, simp add: nat le int_of_nat_def Zero_int_def)
   1.105  
   1.106 -corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
   1.107 +corollary nat_0_le': "0 \<le> z ==> int_of_nat (nat z) = z"
   1.108  by simp
   1.109  
   1.110  lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
   1.111 -by (cases z, simp add: nat le int_def Zero_int_def)
   1.112 +by (cases z, simp add: nat le Zero_int_def)
   1.113  
   1.114  lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
   1.115  apply (cases w, cases z) 
   1.116 -apply (simp add: nat le linorder_not_le [symmetric] int_def Zero_int_def, arith)
   1.117 +apply (simp add: nat le linorder_not_le [symmetric] Zero_int_def, arith)
   1.118  done
   1.119  
   1.120  text{*An alternative condition is @{term "0 \<le> w"} *}
   1.121 @@ -435,74 +381,74 @@
   1.122  
   1.123  lemma zless_nat_conj: "(nat w < nat z) = (0 < z & w < z)"
   1.124  apply (cases w, cases z) 
   1.125 -apply (simp add: nat le int_def Zero_int_def linorder_not_le [symmetric], arith)
   1.126 +apply (simp add: nat le Zero_int_def linorder_not_le [symmetric], arith)
   1.127  done
   1.128  
   1.129 -lemma nonneg_eq_int: "[| 0 \<le> z;  !!m. z = int m ==> P |] ==> P"
   1.130 -by (blast dest: nat_0_le sym)
   1.131 +lemma nonneg_eq_int_of_nat: "[| 0 \<le> z;  !!m. z = int_of_nat m ==> P |] ==> P"
   1.132 +by (blast dest: nat_0_le' sym)
   1.133  
   1.134 -lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
   1.135 -by (cases w, simp add: nat le int_def Zero_int_def, arith)
   1.136 +lemma nat_eq_iff': "(nat w = m) = (if 0 \<le> w then w = int_of_nat m else m=0)"
   1.137 +by (cases w, simp add: nat le int_of_nat_def Zero_int_def, arith)
   1.138  
   1.139 -corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
   1.140 -by (simp only: eq_commute [of m] nat_eq_iff) 
   1.141 +corollary nat_eq_iff2': "(m = nat w) = (if 0 \<le> w then w = int_of_nat m else m=0)"
   1.142 +by (simp only: eq_commute [of m] nat_eq_iff')
   1.143  
   1.144 -lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < int m)"
   1.145 +lemma nat_less_iff': "0 \<le> w ==> (nat w < m) = (w < int_of_nat m)"
   1.146  apply (cases w)
   1.147 -apply (simp add: nat le int_def Zero_int_def linorder_not_le [symmetric], arith)
   1.148 +apply (simp add: nat le int_of_nat_def Zero_int_def linorder_not_le [symmetric], arith)
   1.149  done
   1.150  
   1.151 -lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \<le> z)"
   1.152 -by (auto simp add: nat_eq_iff2)
   1.153 +lemma int_of_nat_eq_iff: "(int_of_nat m = z) = (m = nat z & 0 \<le> z)"
   1.154 +by (auto simp add: nat_eq_iff2')
   1.155  
   1.156  lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
   1.157  by (insert zless_nat_conj [of 0], auto)
   1.158  
   1.159  lemma nat_add_distrib:
   1.160       "[| (0::int) \<le> z;  0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
   1.161 -by (cases z, cases z', simp add: nat add le int_def Zero_int_def)
   1.162 +by (cases z, cases z', simp add: nat add le Zero_int_def)
   1.163  
   1.164  lemma nat_diff_distrib:
   1.165       "[| (0::int) \<le> z';  z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
   1.166  by (cases z, cases z', 
   1.167 -    simp add: nat add minus diff_minus le int_def Zero_int_def)
   1.168 -
   1.169 +    simp add: nat add minus diff_minus le Zero_int_def)
   1.170  
   1.171 -lemma nat_zminus_int [simp]: "nat (- (int n)) = 0"
   1.172 -by (simp add: int_def minus nat Zero_int_def) 
   1.173 +lemma nat_zminus_int_of_nat [simp]: "nat (- (int_of_nat n)) = 0"
   1.174 +by (simp add: int_of_nat_def minus nat Zero_int_def) 
   1.175  
   1.176 -lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
   1.177 -by (cases z, simp add: nat le int_def  linorder_not_le [symmetric], arith)
   1.178 +lemma zless_nat_eq_int_zless: "(m < nat z) = (int_of_nat m < z)"
   1.179 +by (cases z, simp add: nat less int_of_nat_def, arith)
   1.180  
   1.181  
   1.182  subsection{*Lemmas about the Function @{term int} and Orderings*}
   1.183  
   1.184 -lemma negative_zless_0: "- (int (Suc n)) < 0"
   1.185 -by (simp add: order_less_le)
   1.186 +lemma negative_zless_0': "- (int_of_nat (Suc n)) < 0"
   1.187 +by (simp add: order_less_le del: of_nat_Suc)
   1.188  
   1.189 -lemma negative_zless [iff]: "- (int (Suc n)) < int m"
   1.190 -by (rule negative_zless_0 [THEN order_less_le_trans], simp)
   1.191 +lemma negative_zless' [iff]: "- (int_of_nat (Suc n)) < int_of_nat m"
   1.192 +by (rule negative_zless_0' [THEN order_less_le_trans], simp)
   1.193  
   1.194 -lemma negative_zle_0: "- int n \<le> 0"
   1.195 +lemma negative_zle_0': "- int_of_nat n \<le> 0"
   1.196  by (simp add: minus_le_iff)
   1.197  
   1.198 -lemma negative_zle [iff]: "- int n \<le> int m"
   1.199 -by (rule order_trans [OF negative_zle_0 zero_zle_int])
   1.200 +lemma negative_zle' [iff]: "- int_of_nat n \<le> int_of_nat m"
   1.201 +by (rule order_trans [OF negative_zle_0' of_nat_0_le_iff])
   1.202  
   1.203 -lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
   1.204 -by (subst le_minus_iff, simp)
   1.205 +lemma not_zle_0_negative' [simp]: "~ (0 \<le> - (int_of_nat (Suc n)))"
   1.206 +by (subst le_minus_iff, simp del: of_nat_Suc)
   1.207  
   1.208 -lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
   1.209 -by (simp add: int_def le minus Zero_int_def) 
   1.210 +lemma int_zle_neg': "(int_of_nat n \<le> - int_of_nat m) = (n = 0 & m = 0)"
   1.211 +by (simp add: int_of_nat_def le minus Zero_int_def)
   1.212  
   1.213 -lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
   1.214 +lemma not_int_zless_negative' [simp]: "~ (int_of_nat n < - int_of_nat m)"
   1.215  by (simp add: linorder_not_less)
   1.216  
   1.217 -lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)"
   1.218 -by (force simp add: order_eq_iff [of "- int n"] int_zle_neg)
   1.219 +lemma negative_eq_positive' [simp]:
   1.220 +  "(- int_of_nat n = int_of_nat m) = (n = 0 & m = 0)"
   1.221 +by (force simp add: order_eq_iff [of "- int_of_nat n"] int_zle_neg')
   1.222  
   1.223 -lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)"
   1.224 -proof (cases w, cases z, simp add: le add int_def)
   1.225 +lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int_of_nat n)"
   1.226 +proof (cases w, cases z, simp add: le add int_of_nat_def)
   1.227    fix a b c d
   1.228    assume "w = Abs_Integ (intrel `` {(a,b)})" "z = Abs_Integ (intrel `` {(c,d)})"
   1.229    show "(a+d \<le> c+b) = (\<exists>n. c+b = a+n+d)"
   1.230 @@ -517,8 +463,8 @@
   1.231    qed
   1.232  qed
   1.233  
   1.234 -lemma abs_int_eq [simp]: "abs (int m) = int m"
   1.235 -by (simp add: abs_if)
   1.236 +lemma abs_of_nat [simp]: "\<bar>of_nat n::'a::ordered_idom\<bar> = of_nat n"
   1.237 +by (rule  of_nat_0_le_iff [THEN abs_of_nonneg]) (* belongs in Nat.thy *)
   1.238  
   1.239  text{*This version is proved for all ordered rings, not just integers!
   1.240        It is proved here because attribute @{text arith_split} is not available
   1.241 @@ -541,11 +487,11 @@
   1.242  where
   1.243    "iszero z \<longleftrightarrow> z = 0"
   1.244  
   1.245 -lemma not_neg_int [simp]: "~ neg(int n)"
   1.246 +lemma not_neg_int_of_nat [simp]: "~ neg (int_of_nat n)"
   1.247  by (simp add: neg_def)
   1.248  
   1.249 -lemma neg_zminus_int [simp]: "neg(- (int (Suc n)))"
   1.250 -by (simp add: neg_def neg_less_0_iff_less)
   1.251 +lemma neg_zminus_int_of_nat [simp]: "neg (- (int_of_nat (Suc n)))"
   1.252 +by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
   1.253  
   1.254  lemmas neg_eq_less_0 = neg_def
   1.255  
   1.256 @@ -570,7 +516,7 @@
   1.257  lemma neg_nat: "neg z ==> nat z = 0"
   1.258  by (simp add: neg_def order_less_imp_le) 
   1.259  
   1.260 -lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
   1.261 +lemma not_neg_nat': "~ neg z ==> int_of_nat (nat z) = z"
   1.262  by (simp add: linorder_not_less neg_def)
   1.263  
   1.264  
   1.265 @@ -610,18 +556,11 @@
   1.266  apply (rule of_nat_mult [symmetric])
   1.267  done
   1.268  
   1.269 -text{*Agreement with the specific embedding for the integers*}
   1.270 -lemma int_eq_of_nat: "int = (of_nat :: nat => int)"
   1.271 -proof
   1.272 -  fix n
   1.273 -  show "int n = of_nat n"  by (induct n, simp_all add: int_Suc add_ac)
   1.274 -qed
   1.275 -
   1.276  lemma of_nat_eq_id [simp]: "of_nat = (id :: nat => nat)"
   1.277  proof
   1.278    fix n
   1.279    show "of_nat n = id n"  by (induct n, simp_all)
   1.280 -qed
   1.281 +qed (* belongs in Nat.thy *)
   1.282  
   1.283  
   1.284  subsection{*Embedding of the Integers into any @{text ring_1}:
   1.285 @@ -642,10 +581,10 @@
   1.286  qed
   1.287  
   1.288  lemma of_int_0 [simp]: "of_int 0 = 0"
   1.289 -by (simp add: of_int Zero_int_def int_def)
   1.290 +by (simp add: of_int Zero_int_def)
   1.291  
   1.292  lemma of_int_1 [simp]: "of_int 1 = 1"
   1.293 -by (simp add: of_int One_int_def int_def)
   1.294 +by (simp add: of_int One_int_def)
   1.295  
   1.296  lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z"
   1.297  by (cases w, cases z, simp add: compare_rls of_int add)
   1.298 @@ -706,7 +645,7 @@
   1.299    fix z
   1.300    show "of_int z = id z"
   1.301      by (cases z)
   1.302 -      (simp add: of_int add minus int_eq_of_nat [symmetric] int_def diff_minus)
   1.303 +      (simp add: of_int add minus int_of_nat_def diff_minus)
   1.304  qed
   1.305  
   1.306  
   1.307 @@ -759,9 +698,6 @@
   1.308  lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
   1.309  by (induct n, auto)
   1.310  
   1.311 -lemma of_int_int_eq [simp]: "of_int (int n) = of_nat n"
   1.312 -by (simp add: int_eq_of_nat)
   1.313 -
   1.314  lemma Ints_cases [cases set: Ints]:
   1.315    assumes "q \<in> \<int>"
   1.316    obtains (of_int) z where "q = of_int z"
   1.317 @@ -796,9 +732,6 @@
   1.318    apply (erule finite_induct, auto)
   1.319    done
   1.320  
   1.321 -lemma int_setsum: "int (setsum f A) = (\<Sum>x\<in>A. int(f x))"
   1.322 -  by (simp add: int_eq_of_nat of_nat_setsum)
   1.323 -
   1.324  lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
   1.325    apply (cases "finite A")
   1.326    apply (erule finite_induct, auto)
   1.327 @@ -809,9 +742,6 @@
   1.328    apply (erule finite_induct, auto)
   1.329    done
   1.330  
   1.331 -lemma int_setprod: "int (setprod f A) = (\<Prod>x\<in>A. int(f x))"
   1.332 -  by (simp add: int_eq_of_nat of_nat_setprod)
   1.333 -
   1.334  lemma setprod_nonzero_nat:
   1.335      "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
   1.336    by (rule setprod_nonzero, auto)
   1.337 @@ -834,6 +764,207 @@
   1.338  text{*Now we replace the case analysis rule by a more conventional one:
   1.339  whether an integer is negative or not.*}
   1.340  
   1.341 +lemma zless_iff_Suc_zadd':
   1.342 +    "(w < z) = (\<exists>n. z = w + int_of_nat (Suc n))"
   1.343 +apply (cases z, cases w)
   1.344 +apply (auto simp add: le add int_of_nat_def linorder_not_le [symmetric]) 
   1.345 +apply (rename_tac a b c d) 
   1.346 +apply (rule_tac x="a+d - Suc(c+b)" in exI) 
   1.347 +apply arith
   1.348 +done
   1.349 +
   1.350 +lemma negD': "x<0 ==> \<exists>n. x = - (int_of_nat (Suc n))"
   1.351 +apply (cases x)
   1.352 +apply (auto simp add: le minus Zero_int_def int_of_nat_def order_less_le)
   1.353 +apply (rule_tac x="y - Suc x" in exI, arith)
   1.354 +done
   1.355 +
   1.356 +theorem int_cases':
   1.357 +     "[|!! n. z = int_of_nat n ==> P;  !! n. z =  - (int_of_nat (Suc n)) ==> P |] ==> P"
   1.358 +apply (cases "z < 0", blast dest!: negD')
   1.359 +apply (simp add: linorder_not_less del: of_nat_Suc)
   1.360 +apply (blast dest: nat_0_le' [THEN sym])
   1.361 +done
   1.362 +
   1.363 +theorem int_induct':
   1.364 +     "[|!! n. P (int_of_nat n);  !!n. P (- (int_of_nat (Suc n))) |] ==> P z"
   1.365 +  by (cases z rule: int_cases') auto
   1.366 +
   1.367 +text{*Contributed by Brian Huffman*}
   1.368 +theorem int_diff_cases' [case_names diff]:
   1.369 +assumes prem: "!!m n. z = int_of_nat m - int_of_nat n ==> P" shows "P"
   1.370 +apply (cases z rule: eq_Abs_Integ)
   1.371 +apply (rule_tac m=x and n=y in prem)
   1.372 +apply (simp add: int_of_nat_def diff_def minus add)
   1.373 +done
   1.374 +
   1.375 +lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z"
   1.376 +by (cases z, simp add: nat le of_int Zero_int_def)
   1.377 +
   1.378 +lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
   1.379 +
   1.380 +
   1.381 +subsection{*@{term int}: Embedding the Naturals into the Integers*}
   1.382 +
   1.383 +definition
   1.384 +  int :: "nat \<Rightarrow> int"
   1.385 +where
   1.386 +  [code func del]: "int m = Abs_Integ (intrel `` {(m, 0)})"
   1.387 +
   1.388 +lemma inj_int: "inj int"
   1.389 +by (simp add: inj_on_def int_def)
   1.390 +
   1.391 +lemma int_int_eq [iff]: "(int m = int n) = (m = n)"
   1.392 +by (fast elim!: inj_int [THEN injD])
   1.393 +
   1.394 +lemma zadd_int: "(int m) + (int n) = int (m + n)"
   1.395 +  by (simp add: int_def add)
   1.396 +
   1.397 +lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z"
   1.398 +  by (simp add: zadd_int zadd_assoc [symmetric])
   1.399 +
   1.400 +lemma int_mult: "int (m * n) = (int m) * (int n)"
   1.401 +by (simp add: int_def mult)
   1.402 +
   1.403 +text{*Compatibility binding*}
   1.404 +lemmas zmult_int = int_mult [symmetric]
   1.405 +
   1.406 +lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)"
   1.407 +by (simp add: Zero_int_def [folded int_def])
   1.408 +
   1.409 +lemma zless_int [simp]: "(int m < int n) = (m<n)"
   1.410 +by (simp add: le add int_def linorder_not_le [symmetric]) 
   1.411 +
   1.412 +lemma int_less_0_conv [simp]: "~ (int k < 0)"
   1.413 +by (simp add: Zero_int_def [folded int_def])
   1.414 +
   1.415 +lemma zero_less_int_conv [simp]: "(0 < int n) = (0 < n)"
   1.416 +by (simp add: Zero_int_def [folded int_def])
   1.417 +
   1.418 +lemma zle_int [simp]: "(int m \<le> int n) = (m\<le>n)"
   1.419 +by (simp add: linorder_not_less [symmetric])
   1.420 +
   1.421 +lemma zero_zle_int [simp]: "(0 \<le> int n)"
   1.422 +by (simp add: Zero_int_def [folded int_def])
   1.423 +
   1.424 +lemma int_le_0_conv [simp]: "(int n \<le> 0) = (n = 0)"
   1.425 +by (simp add: Zero_int_def [folded int_def])
   1.426 +
   1.427 +lemma int_0 [simp]: "int 0 = (0::int)"
   1.428 +by (simp add: Zero_int_def [folded int_def])
   1.429 +
   1.430 +lemma int_1 [simp]: "int 1 = 1"
   1.431 +by (simp add: One_int_def [folded int_def])
   1.432 +
   1.433 +lemma int_Suc0_eq_1: "int (Suc 0) = 1"
   1.434 +by (simp add: One_int_def [folded int_def])
   1.435 +
   1.436 +lemma int_Suc: "int (Suc m) = 1 + (int m)"
   1.437 +by (simp add: One_int_def [folded int_def] zadd_int)
   1.438 +
   1.439 +lemma nat_int [simp]: "nat(int n) = n"
   1.440 +by (simp add: nat int_def) 
   1.441 +
   1.442 +lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
   1.443 +by (cases z, simp add: nat le int_def Zero_int_def)
   1.444 +
   1.445 +corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
   1.446 +by simp
   1.447 +
   1.448 +lemma nonneg_eq_int: "[| 0 \<le> z;  !!m. z = int m ==> P |] ==> P"
   1.449 +by (blast dest: nat_0_le sym)
   1.450 +
   1.451 +lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
   1.452 +by (cases w, simp add: nat le int_def Zero_int_def, arith)
   1.453 +
   1.454 +corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
   1.455 +by (simp only: eq_commute [of m] nat_eq_iff) 
   1.456 +
   1.457 +lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < int m)"
   1.458 +apply (cases w)
   1.459 +apply (simp add: nat le int_def Zero_int_def linorder_not_le [symmetric], arith)
   1.460 +done
   1.461 +
   1.462 +lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \<le> z)"
   1.463 +by (auto simp add: nat_eq_iff2)
   1.464 +
   1.465 +lemma nat_zminus_int [simp]: "nat (- (int n)) = 0"
   1.466 +by (simp add: int_def minus nat Zero_int_def) 
   1.467 +
   1.468 +lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
   1.469 +by (cases z, simp add: nat le int_def  linorder_not_le [symmetric], arith)
   1.470 +
   1.471 +lemma negative_zless_0: "- (int (Suc n)) < 0"
   1.472 +by (simp add: order_less_le)
   1.473 +
   1.474 +lemma negative_zless [iff]: "- (int (Suc n)) < int m"
   1.475 +by (rule negative_zless_0 [THEN order_less_le_trans], simp)
   1.476 +
   1.477 +lemma negative_zle_0: "- int n \<le> 0"
   1.478 +by (simp add: minus_le_iff)
   1.479 +
   1.480 +lemma negative_zle [iff]: "- int n \<le> int m"
   1.481 +by (rule order_trans [OF negative_zle_0 zero_zle_int])
   1.482 +
   1.483 +lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
   1.484 +by (subst le_minus_iff, simp)
   1.485 +
   1.486 +lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
   1.487 +by (simp add: int_def le minus Zero_int_def) 
   1.488 +
   1.489 +lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
   1.490 +by (simp add: linorder_not_less)
   1.491 +
   1.492 +lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)"
   1.493 +by (force simp add: order_eq_iff [of "- int n"] int_zle_neg)
   1.494 +
   1.495 +lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)"
   1.496 +proof (cases w, cases z, simp add: le add int_def)
   1.497 +  fix a b c d
   1.498 +  assume "w = Abs_Integ (intrel `` {(a,b)})" "z = Abs_Integ (intrel `` {(c,d)})"
   1.499 +  show "(a+d \<le> c+b) = (\<exists>n. c+b = a+n+d)"
   1.500 +  proof
   1.501 +    assume "a + d \<le> c + b" 
   1.502 +    thus "\<exists>n. c + b = a + n + d" 
   1.503 +      by (auto intro!: exI [where x="c+b - (a+d)"])
   1.504 +  next    
   1.505 +    assume "\<exists>n. c + b = a + n + d" 
   1.506 +    then obtain n where "c + b = a + n + d" ..
   1.507 +    thus "a + d \<le> c + b" by arith
   1.508 +  qed
   1.509 +qed
   1.510 +
   1.511 +lemma abs_int_eq [simp]: "abs (int m) = int m"
   1.512 +by (simp add: abs_if)
   1.513 +
   1.514 +lemma not_neg_int [simp]: "~ neg(int n)"
   1.515 +by (simp add: neg_def)
   1.516 +
   1.517 +lemma neg_zminus_int [simp]: "neg(- (int (Suc n)))"
   1.518 +by (simp add: neg_def neg_less_0_iff_less)
   1.519 +
   1.520 +lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
   1.521 +by (simp add: linorder_not_less neg_def)
   1.522 +
   1.523 +text{*Agreement with the specific embedding for the integers*}
   1.524 +lemma int_eq_of_nat: "int = (of_nat :: nat => int)"
   1.525 +proof
   1.526 +  fix n
   1.527 +  show "int n = of_nat n"  by (induct n, simp_all add: int_Suc add_ac)
   1.528 +qed
   1.529 +
   1.530 +lemma of_int_int_eq [simp]: "of_int (int n) = of_nat n"
   1.531 +by (simp add: int_eq_of_nat)
   1.532 +
   1.533 +lemma int_setsum: "int (setsum f A) = (\<Sum>x\<in>A. int(f x))"
   1.534 +  by (simp add: int_eq_of_nat of_nat_setsum)
   1.535 +
   1.536 +lemma int_setprod: "int (setprod f A) = (\<Prod>x\<in>A. int(f x))"
   1.537 +  by (simp add: int_eq_of_nat of_nat_setprod)
   1.538 +
   1.539 +text{*Now we replace the case analysis rule by a more conventional one:
   1.540 +whether an integer is negative or not.*}
   1.541 +
   1.542  lemma zless_iff_Suc_zadd:
   1.543      "(w < z) = (\<exists>n. z = w + int(Suc n))"
   1.544  apply (cases z, cases w)
   1.545 @@ -868,11 +999,6 @@
   1.546   apply (rule_tac m=0 and n="Suc n" in prem, simp)
   1.547  done
   1.548  
   1.549 -lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z"
   1.550 -apply (cases z)
   1.551 -apply (simp_all add: not_zle_0_negative del: int_Suc)
   1.552 -done
   1.553 -
   1.554  lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
   1.555  
   1.556  lemmas [simp] = int_Suc