src/HOL/IntDef.thy
 changeset 24196 f1dbfd7e3223 parent 23950 f54c0e339061 child 24286 7619080e49f0
```     1.1 --- a/src/HOL/IntDef.thy	Thu Aug 09 15:52:45 2007 +0200
1.2 +++ b/src/HOL/IntDef.thy	Thu Aug 09 15:52:47 2007 +0200
1.3 @@ -149,12 +149,7 @@
1.4      by (simp add: Zero_int_def One_int_def)
1.5  qed
1.6
1.7 -abbreviation
1.8 -  int :: "nat \<Rightarrow> int"
1.9 -where
1.10 -  "int \<equiv> of_nat"
1.11 -
1.12 -lemma int_def: "int m = Abs_Integ (intrel `` {(m, 0)})"
1.13 +lemma int_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})"
1.15
1.16
1.17 @@ -194,20 +189,20 @@
1.18
1.19  text{*strict, in 1st argument; proof is by induction on k>0*}
1.20  lemma zmult_zless_mono2_lemma:
1.21 -     "(i::int)<j ==> 0<k ==> int k * i < int k * j"
1.22 +     "(i::int)<j ==> 0<k ==> of_nat k * i < of_nat k * j"
1.23  apply (induct "k", simp)
1.25  apply (case_tac "k=0")
1.27  done
1.28
1.29 -lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = int n"
1.30 +lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = of_nat n"
1.31  apply (cases k)
1.33  apply (rule_tac x="x-y" in exI, simp)
1.34  done
1.35
1.36 -lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = int n"
1.37 +lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = of_nat n"
1.38  apply (cases k)
1.39  apply (simp add: less int_def Zero_int_def)
1.40  apply (rule_tac x="x-y" in exI, simp)
1.41 @@ -258,16 +253,16 @@
1.42      by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
1.43  qed
1.44
1.45 -lemma nat_int [simp]: "nat (int n) = n"
1.46 +lemma nat_int [simp]: "nat (of_nat n) = n"
1.47  by (simp add: nat int_def)
1.48
1.49  lemma nat_zero [simp]: "nat 0 = 0"
1.50  by (simp add: Zero_int_def nat)
1.51
1.52 -lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
1.53 +lemma int_nat_eq [simp]: "of_nat (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 (nat z) = z"
1.57 +corollary nat_0_le: "0 \<le> z ==> of_nat (nat z) = z"
1.58  by simp
1.59
1.60  lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
1.61 @@ -290,21 +285,24 @@
1.62  apply (simp add: nat le Zero_int_def linorder_not_le [symmetric], arith)
1.63  done
1.64
1.65 -lemma nonneg_eq_int: "[| 0 \<le> z;  !!m. z = int m ==> P |] ==> P"
1.66 -by (blast dest: nat_0_le sym)
1.67 +lemma nonneg_eq_int:
1.68 +  fixes z :: int
1.69 +  assumes "0 \<le> z" and "\<And>m. z = of_nat m \<Longrightarrow> P"
1.70 +  shows P
1.71 +  using assms by (blast dest: nat_0_le sym)
1.72
1.73 -lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
1.74 +lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = of_nat m else m=0)"
1.75  by (cases w, simp add: nat le int_def Zero_int_def, arith)
1.76
1.77 -corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
1.78 +corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = of_nat m else m=0)"
1.79  by (simp only: eq_commute [of m] nat_eq_iff)
1.80
1.81 -lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < int m)"
1.82 +lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
1.83  apply (cases w)
1.84  apply (simp add: nat le int_def Zero_int_def linorder_not_le [symmetric], arith)
1.85  done
1.86
1.87 -lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \<le> z)"
1.88 +lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)"
1.89  by (auto simp add: nat_eq_iff2)
1.90
1.91  lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
1.92 @@ -319,59 +317,56 @@
1.93  by (cases z, cases z',
1.95
1.96 -lemma nat_zminus_int [simp]: "nat (- (int n)) = 0"
1.97 +lemma nat_zminus_int [simp]: "nat (- (of_nat n)) = 0"
1.98  by (simp add: int_def minus nat Zero_int_def)
1.99
1.100 -lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
1.101 +lemma zless_nat_eq_int_zless: "(m < nat z) = (of_nat m < z)"
1.102  by (cases z, simp add: nat less int_def, arith)
1.103
1.104
1.105 -subsection{*Lemmas about the Function @{term int} and Orderings*}
1.106 +subsection{*Lemmas about the Function @{term of_nat} and Orderings*}
1.107
1.108 -lemma negative_zless_0: "- (int (Suc n)) < 0"
1.109 +lemma negative_zless_0: "- (of_nat (Suc n)) < (0 \<Colon> int)"
1.110  by (simp add: order_less_le del: of_nat_Suc)
1.111
1.112 -lemma negative_zless [iff]: "- (int (Suc n)) < int m"
1.113 +lemma negative_zless [iff]: "- (of_nat (Suc n)) < (of_nat m \<Colon> int)"
1.114  by (rule negative_zless_0 [THEN order_less_le_trans], simp)
1.115
1.116 -lemma negative_zle_0: "- int n \<le> 0"
1.117 +lemma negative_zle_0: "- of_nat n \<le> (0 \<Colon> int)"
1.119
1.120 -lemma negative_zle [iff]: "- int n \<le> int m"
1.121 +lemma negative_zle [iff]: "- of_nat n \<le> (of_nat m \<Colon> int)"
1.122  by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
1.123
1.124 -lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
1.125 +lemma not_zle_0_negative [simp]: "~ (0 \<le> - (of_nat (Suc n) \<Colon> int))"
1.126  by (subst le_minus_iff, simp del: of_nat_Suc)
1.127
1.128 -lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
1.129 +lemma int_zle_neg: "((of_nat n \<Colon> int) \<le> - of_nat m) = (n = 0 & m = 0)"
1.130  by (simp add: int_def le minus Zero_int_def)
1.131
1.132 -lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
1.133 +lemma not_int_zless_negative [simp]: "~ ((of_nat n \<Colon> int) < - of_nat m)"
1.135
1.136 -lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)"
1.137 -by (force simp add: order_eq_iff [of "- int n"] int_zle_neg)
1.138 +lemma negative_eq_positive [simp]: "((- of_nat n \<Colon> int) = of_nat m) = (n = 0 & m = 0)"
1.139 +by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
1.140
1.141 -lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)"
1.142 +lemma zle_iff_zadd: "(w\<Colon>int) \<le> z \<longleftrightarrow> (\<exists>n. z = w + of_nat n)"
1.143  proof -
1.144    have "(w \<le> z) = (0 \<le> z - w)"
1.145      by (simp only: le_diff_eq add_0_left)
1.146 -  also have "\<dots> = (\<exists>n. z - w = int n)"
1.147 +  also have "\<dots> = (\<exists>n. z - w = of_nat n)"
1.148      by (auto elim: zero_le_imp_eq_int)
1.149 -  also have "\<dots> = (\<exists>n. z = w + int n)"
1.150 +  also have "\<dots> = (\<exists>n. z = w + of_nat n)"
1.151      by (simp only: group_simps)
1.152    finally show ?thesis .
1.153  qed
1.154
1.155 -lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z"
1.156 +lemma zadd_int_left: "of_nat m + (of_nat n + z) = of_nat (m + n) + (z\<Colon>int)"
1.157  by simp
1.158
1.159 -lemma int_Suc0_eq_1: "int (Suc 0) = 1"
1.160 +lemma int_Suc0_eq_1: "of_nat (Suc 0) = (1\<Colon>int)"
1.161  by simp
1.162
1.163 -lemma abs_of_nat [simp]: "\<bar>of_nat n::'a::ordered_idom\<bar> = of_nat n"
1.164 -by (rule  of_nat_0_le_iff [THEN abs_of_nonneg]) (* belongs in Nat.thy *)
1.165 -
1.166  text{*This version is proved for all ordered rings, not just integers!
1.167        It is proved here because attribute @{text arith_split} is not available
1.168        in theory @{text Ring_and_Field}.
1.169 @@ -393,10 +388,10 @@
1.170  where
1.171    "iszero z \<longleftrightarrow> z = 0"
1.172
1.173 -lemma not_neg_int [simp]: "~ neg (int n)"
1.174 +lemma not_neg_int [simp]: "~ neg (of_nat n)"
1.176
1.177 -lemma neg_zminus_int [simp]: "neg (- (int (Suc n)))"
1.178 +lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))"
1.179  by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
1.180
1.181  lemmas neg_eq_less_0 = neg_def
1.182 @@ -422,7 +417,7 @@
1.183  lemma neg_nat: "neg z ==> nat z = 0"
1.184  by (simp add: neg_def order_less_imp_le)
1.185
1.186 -lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
1.187 +lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z"
1.188  by (simp add: linorder_not_less neg_def)
1.189
1.190
1.191 @@ -490,7 +485,7 @@
1.192  class ring_char_0 = ring_1 + semiring_char_0
1.193
1.194  lemma of_int_eq_iff [simp]:
1.195 -     "(of_int w = (of_int z::'a::ring_char_0)) = (w = z)"
1.196 +   "of_int w = (of_int z \<Colon> 'a\<Colon>ring_char_0) \<longleftrightarrow> w = z"
1.197  apply (cases w, cases z, simp add: of_int)
1.198  apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
1.199  apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
1.200 @@ -586,7 +581,7 @@
1.201  whether an integer is negative or not.*}
1.202
1.204 -    "(w < z) = (\<exists>n. z = w + int (Suc n))"
1.205 +  "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + of_nat (Suc n))"
1.206  apply (cases z, cases w)
1.208  apply (rename_tac a b c d)
1.209 @@ -594,26 +589,26 @@
1.210  apply arith
1.211  done
1.212
1.213 -lemma negD: "x<0 ==> \<exists>n. x = - (int (Suc n))"
1.214 +lemma negD: "(x \<Colon> int) < 0 \<Longrightarrow> \<exists>n. x = - (of_nat (Suc n))"
1.215  apply (cases x)
1.216  apply (auto simp add: le minus Zero_int_def int_def order_less_le)
1.217  apply (rule_tac x="y - Suc x" in exI, arith)
1.218  done
1.219
1.220  theorem int_cases [cases type: int, case_names nonneg neg]:
1.221 -     "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
1.222 +  "[|!! n. (z \<Colon> int) = of_nat n ==> P;  !! n. z =  - (of_nat (Suc n)) ==> P |] ==> P"
1.223  apply (cases "z < 0", blast dest!: negD)
1.224  apply (simp add: linorder_not_less del: of_nat_Suc)
1.225  apply (blast dest: nat_0_le [THEN sym])
1.226  done
1.227
1.228  theorem int_induct [induct type: int, case_names nonneg neg]:
1.229 -     "[|!! n. P (int n);  !!n. P (- (int (Suc n))) |] ==> P z"
1.230 +     "[|!! n. P (of_nat n \<Colon> int);  !!n. P (- (of_nat (Suc n))) |] ==> P z"
1.231    by (cases z rule: int_cases) auto
1.232
1.233  text{*Contributed by Brian Huffman*}
1.234  theorem int_diff_cases [case_names diff]:
1.235 -assumes prem: "!!m n. z = int m - int n ==> P" shows "P"
1.236 +assumes prem: "!!m n. (z\<Colon>int) = of_nat m - of_nat n ==> P" shows "P"
1.237  apply (cases z rule: eq_Abs_Integ)
1.238  apply (rule_tac m=x and n=y in prem)
1.240 @@ -673,9 +668,9 @@
1.241  lemmas zle_int = of_nat_le_iff [where 'a=int]
1.242  lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
1.243  lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="?n"]
1.244 -lemmas int_0 = of_nat_0 [where ?'a_1.0=int]
1.245 +lemmas int_0 = of_nat_0 [where 'a=int]
1.246  lemmas int_1 = of_nat_1 [where 'a=int]
1.247 -lemmas int_Suc = of_nat_Suc [where ?'a_1.0=int]
1.248 +lemmas int_Suc = of_nat_Suc [where 'a=int]
1.249  lemmas abs_int_eq = abs_of_nat [where 'a=int and n="?m"]
1.250  lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
1.251  lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
1.252 @@ -683,6 +678,11 @@
1.253  lemmas int_eq_of_nat = TrueI
1.254
1.255  abbreviation
1.256 +  int :: "nat \<Rightarrow> int"
1.257 +where
1.258 +  "int \<equiv> of_nat"
1.259 +
1.260 +abbreviation
1.261    int_of_nat :: "nat \<Rightarrow> int"
1.262  where
1.263    "int_of_nat \<equiv> of_nat"
```