removed constant int :: nat => int;
authorhuffman
Wed Jun 13 03:31:11 2007 +0200 (2007-06-13)
changeset 23365f31794033ae1
parent 23364 1f3b832c90c1
child 23366 a1e61b5c000f
removed constant int :: nat => int;
int is now an abbreviation for of_nat :: nat => int
src/HOL/IntArith.thy
src/HOL/IntDef.thy
src/HOL/IntDiv.thy
src/HOL/Library/EfficientNat.thy
src/HOL/Library/GCD.thy
src/HOL/Library/Word.thy
src/HOL/NatBin.thy
src/HOL/NumberTheory/Fib.thy
src/HOL/NumberTheory/Quadratic_Reciprocity.thy
src/HOL/Numeral.thy
src/HOL/Presburger.thy
src/HOL/Real/Float.thy
src/HOL/Real/Rational.thy
src/HOL/arith_data.ML
src/HOL/int_arith1.ML
     1.1 --- a/src/HOL/IntArith.thy	Wed Jun 13 03:28:21 2007 +0200
     1.2 +++ b/src/HOL/IntArith.thy	Wed Jun 13 03:31:11 2007 +0200
     1.3 @@ -196,25 +196,6 @@
     1.4        z is an integer literal.*}
     1.5  lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard]
     1.6  
     1.7 -lemmas int_of_nat_eq_iff_number_of [simp] =
     1.8 -  int_of_nat_eq_iff [of _ "number_of v", standard]
     1.9 -
    1.10 -lemma split_nat':
    1.11 -  "P(nat(i::int)) = ((\<forall>n. i = int_of_nat n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
    1.12 -  (is "?P = (?L & ?R)")
    1.13 -proof (cases "i < 0")
    1.14 -  case True thus ?thesis by simp
    1.15 -next
    1.16 -  case False
    1.17 -  have "?P = ?L"
    1.18 -  proof
    1.19 -    assume ?P thus ?L using False by clarsimp
    1.20 -  next
    1.21 -    assume ?L thus ?P using False by simp
    1.22 -  qed
    1.23 -  with False show ?thesis by simp
    1.24 -qed
    1.25 -
    1.26  lemma split_nat [arith_split]:
    1.27    "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
    1.28    (is "?P = (?L & ?R)")
    1.29 @@ -232,10 +213,6 @@
    1.30  qed
    1.31  
    1.32  
    1.33 -(*Analogous to zadd_int*)
    1.34 -lemma zdiff_int: "n \<le> m ==> int m - int n = int (m-n)" 
    1.35 -by (induct m n rule: diff_induct, simp_all)
    1.36 -
    1.37  lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
    1.38  apply (cases "0 \<le> z'")
    1.39  apply (rule inj_int [THEN injD])
     2.1 --- a/src/HOL/IntDef.thy	Wed Jun 13 03:28:21 2007 +0200
     2.2 +++ b/src/HOL/IntDef.thy	Wed Jun 13 03:31:11 2007 +0200
     2.3 @@ -219,9 +219,12 @@
     2.4  qed
     2.5  
     2.6  abbreviation
     2.7 -  int_of_nat :: "nat \<Rightarrow> int"
     2.8 +  int :: "nat \<Rightarrow> int"
     2.9  where
    2.10 -  "int_of_nat \<equiv> of_nat"
    2.11 +  "int \<equiv> of_nat"
    2.12 +
    2.13 +lemma int_def: "int m = Abs_Integ (intrel `` {(m, 0)})"
    2.14 +by (induct m, simp_all add: Zero_int_def One_int_def add)
    2.15  
    2.16  
    2.17  subsection{*The @{text "\<le>"} Ordering*}
    2.18 @@ -294,18 +297,15 @@
    2.19  apply (simp_all add: add_strict_mono)
    2.20  done
    2.21  
    2.22 -lemma int_of_nat_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})"
    2.23 -by (induct m, simp_all add: Zero_int_def One_int_def add)
    2.24 -
    2.25  lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = of_nat n"
    2.26  apply (cases k)
    2.27 -apply (auto simp add: le add int_of_nat_def Zero_int_def)
    2.28 +apply (auto simp add: le add int_def Zero_int_def)
    2.29  apply (rule_tac x="x-y" in exI, simp)
    2.30  done
    2.31  
    2.32  lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = of_nat n"
    2.33  apply (cases k)
    2.34 -apply (simp add: less int_of_nat_def Zero_int_def)
    2.35 +apply (simp add: less int_def Zero_int_def)
    2.36  apply (rule_tac x="x-y" in exI, simp)
    2.37  done
    2.38  
    2.39 @@ -352,16 +352,16 @@
    2.40      by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
    2.41  qed
    2.42  
    2.43 -lemma nat_int_of_nat [simp]: "nat (int_of_nat n) = n"
    2.44 -by (simp add: nat int_of_nat_def)
    2.45 +lemma nat_int [simp]: "nat (int n) = n"
    2.46 +by (simp add: nat int_def)
    2.47  
    2.48  lemma nat_zero [simp]: "nat 0 = 0"
    2.49  by (simp add: Zero_int_def nat)
    2.50  
    2.51 -lemma int_of_nat_nat_eq [simp]: "int_of_nat (nat z) = (if 0 \<le> z then z else 0)"
    2.52 -by (cases z, simp add: nat le int_of_nat_def Zero_int_def)
    2.53 +lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
    2.54 +by (cases z, simp add: nat le int_def Zero_int_def)
    2.55  
    2.56 -corollary nat_0_le': "0 \<le> z ==> int_of_nat (nat z) = z"
    2.57 +corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
    2.58  by simp
    2.59  
    2.60  lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
    2.61 @@ -379,27 +379,27 @@
    2.62  corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
    2.63  by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
    2.64  
    2.65 -lemma zless_nat_conj: "(nat w < nat z) = (0 < z & w < z)"
    2.66 +lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
    2.67  apply (cases w, cases z) 
    2.68  apply (simp add: nat le Zero_int_def linorder_not_le [symmetric], arith)
    2.69  done
    2.70  
    2.71 -lemma nonneg_eq_int_of_nat: "[| 0 \<le> z;  !!m. z = int_of_nat m ==> P |] ==> P"
    2.72 -by (blast dest: nat_0_le' sym)
    2.73 +lemma nonneg_eq_int: "[| 0 \<le> z;  !!m. z = int m ==> P |] ==> P"
    2.74 +by (blast dest: nat_0_le sym)
    2.75  
    2.76 -lemma nat_eq_iff': "(nat w = m) = (if 0 \<le> w then w = int_of_nat m else m=0)"
    2.77 -by (cases w, simp add: nat le int_of_nat_def Zero_int_def, arith)
    2.78 +lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
    2.79 +by (cases w, simp add: nat le int_def Zero_int_def, arith)
    2.80  
    2.81 -corollary nat_eq_iff2': "(m = nat w) = (if 0 \<le> w then w = int_of_nat m else m=0)"
    2.82 -by (simp only: eq_commute [of m] nat_eq_iff')
    2.83 +corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
    2.84 +by (simp only: eq_commute [of m] nat_eq_iff)
    2.85  
    2.86 -lemma nat_less_iff': "0 \<le> w ==> (nat w < m) = (w < int_of_nat m)"
    2.87 +lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < int m)"
    2.88  apply (cases w)
    2.89 -apply (simp add: nat le int_of_nat_def Zero_int_def linorder_not_le [symmetric], arith)
    2.90 +apply (simp add: nat le int_def Zero_int_def linorder_not_le [symmetric], arith)
    2.91  done
    2.92  
    2.93 -lemma int_of_nat_eq_iff: "(int_of_nat m = z) = (m = nat z & 0 \<le> z)"
    2.94 -by (auto simp add: nat_eq_iff2')
    2.95 +lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \<le> z)"
    2.96 +by (auto simp add: nat_eq_iff2)
    2.97  
    2.98  lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
    2.99  by (insert zless_nat_conj [of 0], auto)
   2.100 @@ -413,42 +413,41 @@
   2.101  by (cases z, cases z', 
   2.102      simp add: nat add minus diff_minus le Zero_int_def)
   2.103  
   2.104 -lemma nat_zminus_int_of_nat [simp]: "nat (- (int_of_nat n)) = 0"
   2.105 -by (simp add: int_of_nat_def minus nat Zero_int_def) 
   2.106 +lemma nat_zminus_int [simp]: "nat (- (int n)) = 0"
   2.107 +by (simp add: int_def minus nat Zero_int_def) 
   2.108  
   2.109 -lemma zless_nat_eq_int_zless': "(m < nat z) = (int_of_nat m < z)"
   2.110 -by (cases z, simp add: nat less int_of_nat_def, arith)
   2.111 +lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
   2.112 +by (cases z, simp add: nat less int_def, arith)
   2.113  
   2.114  
   2.115  subsection{*Lemmas about the Function @{term int} and Orderings*}
   2.116  
   2.117 -lemma negative_zless_0': "- (int_of_nat (Suc n)) < 0"
   2.118 +lemma negative_zless_0: "- (int (Suc n)) < 0"
   2.119  by (simp add: order_less_le del: of_nat_Suc)
   2.120  
   2.121 -lemma negative_zless' [iff]: "- (int_of_nat (Suc n)) < int_of_nat m"
   2.122 -by (rule negative_zless_0' [THEN order_less_le_trans], simp)
   2.123 +lemma negative_zless [iff]: "- (int (Suc n)) < int m"
   2.124 +by (rule negative_zless_0 [THEN order_less_le_trans], simp)
   2.125  
   2.126 -lemma negative_zle_0': "- int_of_nat n \<le> 0"
   2.127 +lemma negative_zle_0: "- int n \<le> 0"
   2.128  by (simp add: minus_le_iff)
   2.129  
   2.130 -lemma negative_zle' [iff]: "- int_of_nat n \<le> int_of_nat m"
   2.131 -by (rule order_trans [OF negative_zle_0' of_nat_0_le_iff])
   2.132 +lemma negative_zle [iff]: "- int n \<le> int m"
   2.133 +by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
   2.134  
   2.135 -lemma not_zle_0_negative' [simp]: "~ (0 \<le> - (int_of_nat (Suc n)))"
   2.136 +lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
   2.137  by (subst le_minus_iff, simp del: of_nat_Suc)
   2.138  
   2.139 -lemma int_zle_neg': "(int_of_nat n \<le> - int_of_nat m) = (n = 0 & m = 0)"
   2.140 -by (simp add: int_of_nat_def le minus Zero_int_def)
   2.141 +lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
   2.142 +by (simp add: int_def le minus Zero_int_def)
   2.143  
   2.144 -lemma not_int_zless_negative' [simp]: "~ (int_of_nat n < - int_of_nat m)"
   2.145 +lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
   2.146  by (simp add: linorder_not_less)
   2.147  
   2.148 -lemma negative_eq_positive' [simp]:
   2.149 -  "(- int_of_nat n = int_of_nat m) = (n = 0 & m = 0)"
   2.150 -by (force simp add: order_eq_iff [of "- int_of_nat n"] int_zle_neg')
   2.151 +lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)"
   2.152 +by (force simp add: order_eq_iff [of "- int n"] int_zle_neg)
   2.153  
   2.154 -lemma zle_iff_zadd': "(w \<le> z) = (\<exists>n. z = w + int_of_nat n)"
   2.155 -proof (cases w, cases z, simp add: le add int_of_nat_def)
   2.156 +lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)"
   2.157 +proof (cases w, cases z, simp add: le add int_def)
   2.158    fix a b c d
   2.159    assume "w = Abs_Integ (intrel `` {(a,b)})" "z = Abs_Integ (intrel `` {(c,d)})"
   2.160    show "(a+d \<le> c+b) = (\<exists>n. c+b = a+n+d)"
   2.161 @@ -487,10 +486,10 @@
   2.162  where
   2.163    "iszero z \<longleftrightarrow> z = 0"
   2.164  
   2.165 -lemma not_neg_int_of_nat [simp]: "~ neg (int_of_nat n)"
   2.166 +lemma not_neg_int [simp]: "~ neg (int n)"
   2.167  by (simp add: neg_def)
   2.168  
   2.169 -lemma neg_zminus_int_of_nat [simp]: "neg (- (int_of_nat (Suc n)))"
   2.170 +lemma neg_zminus_int [simp]: "neg (- (int (Suc n)))"
   2.171  by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
   2.172  
   2.173  lemmas neg_eq_less_0 = neg_def
   2.174 @@ -516,7 +515,7 @@
   2.175  lemma neg_nat: "neg z ==> nat z = 0"
   2.176  by (simp add: neg_def order_less_imp_le) 
   2.177  
   2.178 -lemma not_neg_nat': "~ neg z ==> int_of_nat (nat z) = z"
   2.179 +lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
   2.180  by (simp add: linorder_not_less neg_def)
   2.181  
   2.182  
   2.183 @@ -645,7 +644,7 @@
   2.184    fix z
   2.185    show "of_int z = id z"
   2.186      by (cases z)
   2.187 -      (simp add: of_int add minus int_of_nat_def diff_minus)
   2.188 +      (simp add: of_int add minus int_def diff_minus)
   2.189  qed
   2.190  
   2.191  
   2.192 @@ -764,245 +763,80 @@
   2.193  text{*Now we replace the case analysis rule by a more conventional one:
   2.194  whether an integer is negative or not.*}
   2.195  
   2.196 -lemma zless_iff_Suc_zadd':
   2.197 -    "(w < z) = (\<exists>n. z = w + int_of_nat (Suc n))"
   2.198 +lemma zless_iff_Suc_zadd:
   2.199 +    "(w < z) = (\<exists>n. z = w + int (Suc n))"
   2.200  apply (cases z, cases w)
   2.201 -apply (auto simp add: le add int_of_nat_def linorder_not_le [symmetric]) 
   2.202 +apply (auto simp add: le add int_def linorder_not_le [symmetric]) 
   2.203  apply (rename_tac a b c d) 
   2.204  apply (rule_tac x="a+d - Suc(c+b)" in exI) 
   2.205  apply arith
   2.206  done
   2.207  
   2.208 -lemma negD': "x<0 ==> \<exists>n. x = - (int_of_nat (Suc n))"
   2.209 +lemma negD: "x<0 ==> \<exists>n. x = - (int (Suc n))"
   2.210  apply (cases x)
   2.211 -apply (auto simp add: le minus Zero_int_def int_of_nat_def order_less_le)
   2.212 +apply (auto simp add: le minus Zero_int_def int_def order_less_le)
   2.213  apply (rule_tac x="y - Suc x" in exI, arith)
   2.214  done
   2.215  
   2.216 -theorem int_cases' [cases type: int, case_names nonneg neg]:
   2.217 -     "[|!! n. z = int_of_nat n ==> P;  !! n. z =  - (int_of_nat (Suc n)) ==> P |] ==> P"
   2.218 -apply (cases "z < 0", blast dest!: negD')
   2.219 +theorem int_cases [cases type: int, case_names nonneg neg]:
   2.220 +     "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
   2.221 +apply (cases "z < 0", blast dest!: negD)
   2.222  apply (simp add: linorder_not_less del: of_nat_Suc)
   2.223 -apply (blast dest: nat_0_le' [THEN sym])
   2.224 +apply (blast dest: nat_0_le [THEN sym])
   2.225  done
   2.226  
   2.227 -theorem int_induct' [induct type: int, case_names nonneg neg]:
   2.228 -     "[|!! n. P (int_of_nat n);  !!n. P (- (int_of_nat (Suc n))) |] ==> P z"
   2.229 -  by (cases z rule: int_cases') auto
   2.230 +theorem int_induct'[induct type: int, case_names nonneg neg]:
   2.231 +     "[|!! n. P (int n);  !!n. P (- (int (Suc n))) |] ==> P z"
   2.232 +  by (cases z rule: int_cases) auto
   2.233  
   2.234  text{*Contributed by Brian Huffman*}
   2.235 -theorem int_diff_cases' [case_names diff]:
   2.236 -assumes prem: "!!m n. z = int_of_nat m - int_of_nat n ==> P" shows "P"
   2.237 +theorem int_diff_cases [case_names diff]:
   2.238 +assumes prem: "!!m n. z = int m - int n ==> P" shows "P"
   2.239  apply (cases z rule: eq_Abs_Integ)
   2.240  apply (rule_tac m=x and n=y in prem)
   2.241 -apply (simp add: int_of_nat_def diff_def minus add)
   2.242 +apply (simp add: int_def diff_def minus add)
   2.243  done
   2.244  
   2.245  lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z"
   2.246  by (cases z rule: eq_Abs_Integ, simp add: nat le of_int Zero_int_def)
   2.247  
   2.248 -lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
   2.249  
   2.250 -
   2.251 -subsection{*@{term int}: Embedding the Naturals into the Integers*}
   2.252 -
   2.253 -definition
   2.254 -  int :: "nat \<Rightarrow> int"
   2.255 -where
   2.256 -  [code func del]: "int m = Abs_Integ (intrel `` {(m, 0)})"
   2.257 -
   2.258 -text{*Agreement with the specific embedding for the integers*}
   2.259 -lemma int_eq_of_nat: "int = (of_nat :: nat => int)"
   2.260 -by (simp add: expand_fun_eq int_of_nat_def int_def)
   2.261 -
   2.262 -lemma inj_int: "inj int"
   2.263 -by (simp add: inj_on_def int_def)
   2.264 -
   2.265 -lemma int_int_eq [iff]: "(int m = int n) = (m = n)"
   2.266 -unfolding int_eq_of_nat by (rule of_nat_eq_iff)
   2.267 -
   2.268 -lemma zadd_int: "(int m) + (int n) = int (m + n)"
   2.269 -unfolding int_eq_of_nat by (rule of_nat_add [symmetric])
   2.270 +subsection {* Legacy theorems *}
   2.271  
   2.272  lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z"
   2.273 -unfolding int_eq_of_nat by simp
   2.274 -
   2.275 -lemma int_mult: "int (m * n) = (int m) * (int n)"
   2.276 -unfolding int_eq_of_nat by (rule of_nat_mult)
   2.277 -
   2.278 -text{*Compatibility binding*}
   2.279 -lemmas zmult_int = int_mult [symmetric]
   2.280 -
   2.281 -lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)"
   2.282 -unfolding int_eq_of_nat by (rule of_nat_eq_0_iff)
   2.283 -
   2.284 -lemma zless_int [simp]: "(int m < int n) = (m<n)"
   2.285 -unfolding int_eq_of_nat by (rule of_nat_less_iff)
   2.286 -
   2.287 -lemma int_less_0_conv [simp]: "~ (int k < 0)"
   2.288 -unfolding int_eq_of_nat by (rule of_nat_less_0_iff)
   2.289 -
   2.290 -lemma zero_less_int_conv [simp]: "(0 < int n) = (0 < n)"
   2.291 -unfolding int_eq_of_nat by (rule of_nat_0_less_iff)
   2.292 -
   2.293 -lemma zle_int [simp]: "(int m \<le> int n) = (m\<le>n)"
   2.294 -unfolding int_eq_of_nat by (rule of_nat_le_iff)
   2.295 -
   2.296 -lemma zero_zle_int [simp]: "(0 \<le> int n)"
   2.297 -unfolding int_eq_of_nat by (rule of_nat_0_le_iff)
   2.298 -
   2.299 -lemma int_le_0_conv [simp]: "(int n \<le> 0) = (n = 0)"
   2.300 -unfolding int_eq_of_nat by (rule of_nat_le_0_iff)
   2.301 -
   2.302 -lemma int_0 [simp]: "int 0 = (0::int)"
   2.303 -unfolding int_eq_of_nat by (rule of_nat_0)
   2.304 -
   2.305 -lemma int_1 [simp]: "int 1 = 1"
   2.306 -unfolding int_eq_of_nat by (rule of_nat_1)
   2.307 -
   2.308 -lemma int_Suc0_eq_1: "int (Suc 0) = 1"
   2.309 -unfolding int_eq_of_nat by simp
   2.310 +by simp
   2.311  
   2.312  lemma int_Suc: "int (Suc m) = 1 + (int m)"
   2.313 -unfolding int_eq_of_nat by simp
   2.314 -
   2.315 -lemma nat_int [simp]: "nat(int n) = n"
   2.316 -unfolding int_eq_of_nat by (rule nat_int_of_nat)
   2.317 -
   2.318 -lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
   2.319 -unfolding int_eq_of_nat by (rule int_of_nat_nat_eq)
   2.320 -
   2.321 -corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
   2.322 -unfolding int_eq_of_nat by (rule nat_0_le')
   2.323 -
   2.324 -lemma nonneg_eq_int: "[| 0 \<le> z;  !!m. z = int m ==> P |] ==> P"
   2.325 -unfolding int_eq_of_nat by (blast elim: nonneg_eq_int_of_nat)
   2.326 -
   2.327 -lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
   2.328 -unfolding int_eq_of_nat by (rule nat_eq_iff')
   2.329 -
   2.330 -corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
   2.331 -unfolding int_eq_of_nat by (rule nat_eq_iff2')
   2.332 -
   2.333 -lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < int m)"
   2.334 -unfolding int_eq_of_nat by (rule nat_less_iff')
   2.335 -
   2.336 -lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \<le> z)"
   2.337 -unfolding int_eq_of_nat by (rule int_of_nat_eq_iff)
   2.338 -
   2.339 -lemma nat_zminus_int [simp]: "nat (- (int n)) = 0"
   2.340 -unfolding int_eq_of_nat by (rule nat_zminus_int_of_nat)
   2.341 -
   2.342 -lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
   2.343 -unfolding int_eq_of_nat by (rule zless_nat_eq_int_zless')
   2.344 +by simp
   2.345  
   2.346 -lemma negative_zless_0: "- (int (Suc n)) < 0"
   2.347 -unfolding int_eq_of_nat by (rule negative_zless_0')
   2.348 -
   2.349 -lemma negative_zless [iff]: "- (int (Suc n)) < int m"
   2.350 -unfolding int_eq_of_nat by (rule negative_zless')
   2.351 -
   2.352 -lemma negative_zle_0: "- int n \<le> 0"
   2.353 -unfolding int_eq_of_nat by (rule negative_zle_0')
   2.354 -
   2.355 -lemma negative_zle [iff]: "- int n \<le> int m"
   2.356 -unfolding int_eq_of_nat by (rule negative_zle')
   2.357 -
   2.358 -lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
   2.359 -unfolding int_eq_of_nat by (rule not_zle_0_negative')
   2.360 -
   2.361 -lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
   2.362 -unfolding int_eq_of_nat by (rule int_zle_neg')
   2.363 -
   2.364 -lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
   2.365 -unfolding int_eq_of_nat by (rule not_int_zless_negative')
   2.366 -
   2.367 -lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)"
   2.368 -unfolding int_eq_of_nat by (rule negative_eq_positive')
   2.369 -
   2.370 -lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)"
   2.371 -unfolding int_eq_of_nat by (rule zle_iff_zadd')
   2.372 -
   2.373 -lemma abs_int_eq [simp]: "abs (int m) = int m"
   2.374 -unfolding int_eq_of_nat by (rule abs_of_nat)
   2.375 -
   2.376 -lemma not_neg_int [simp]: "~ neg(int n)"
   2.377 -unfolding int_eq_of_nat by (rule not_neg_int_of_nat)
   2.378 -
   2.379 -lemma neg_zminus_int [simp]: "neg(- (int (Suc n)))"
   2.380 -unfolding int_eq_of_nat by (rule neg_zminus_int_of_nat)
   2.381 +lemma int_Suc0_eq_1: "int (Suc 0) = 1"
   2.382 +by simp
   2.383  
   2.384 -lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
   2.385 -unfolding int_eq_of_nat by (rule not_neg_nat')
   2.386 -
   2.387 -lemma of_int_int_eq [simp]: "of_int (int n) = of_nat n"
   2.388 -unfolding int_eq_of_nat by (rule of_int_of_nat_eq)
   2.389 -
   2.390 -lemma int_setsum: "int (setsum f A) = (\<Sum>x\<in>A. int(f x))"
   2.391 -unfolding int_eq_of_nat by (rule of_nat_setsum)
   2.392 -
   2.393 -lemma int_setprod: "int (setprod f A) = (\<Prod>x\<in>A. int(f x))"
   2.394 -unfolding int_eq_of_nat by (rule of_nat_setprod)
   2.395 -
   2.396 -text{*Now we replace the case analysis rule by a more conventional one:
   2.397 -whether an integer is negative or not.*}
   2.398 -
   2.399 -lemma zless_iff_Suc_zadd:
   2.400 -    "(w < z) = (\<exists>n. z = w + int(Suc n))"
   2.401 -unfolding int_eq_of_nat by (rule zless_iff_Suc_zadd')
   2.402 -
   2.403 -lemma negD: "x<0 ==> \<exists>n. x = - (int (Suc n))"
   2.404 -unfolding int_eq_of_nat by (rule negD')
   2.405 -
   2.406 -theorem int_cases [cases type: int, case_names nonneg neg]:
   2.407 -     "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
   2.408 -unfolding int_eq_of_nat
   2.409 -apply (cases "z < 0", blast dest!: negD')
   2.410 -apply (simp add: linorder_not_less)
   2.411 -apply (blast dest: nat_0_le' [THEN sym])
   2.412 -done
   2.413 -
   2.414 -theorem int_induct [induct type: int, case_names nonneg neg]:
   2.415 -     "[|!! n. P (int n);  !!n. P (- (int (Suc n))) |] ==> P z"
   2.416 -  by (cases z) auto
   2.417 +lemmas inj_int = inj_of_nat [where 'a=int]
   2.418 +lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
   2.419 +lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
   2.420 +lemmas int_mult = of_nat_mult [where 'a=int]
   2.421 +lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
   2.422 +lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int]
   2.423 +lemmas zless_int = of_nat_less_iff [where 'a=int]
   2.424 +lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int]
   2.425 +lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
   2.426 +lemmas zle_int = of_nat_le_iff [where 'a=int]
   2.427 +lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
   2.428 +lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int]
   2.429 +lemmas int_0 = of_nat_0 [where ?'a_1.0=int]
   2.430 +lemmas int_1 = of_nat_1 [where 'a=int]
   2.431 +lemmas abs_int_eq = abs_of_nat [where 'a=int]
   2.432 +lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
   2.433 +lemmas int_setsum = of_nat_setsum [where 'a=int]
   2.434 +lemmas int_setprod = of_nat_setprod [where 'a=int]
   2.435 +lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
   2.436 +lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
   2.437 +lemmas int_eq_of_nat = TrueI
   2.438  
   2.439 -text{*Contributed by Brian Huffman*}
   2.440 -theorem int_diff_cases [case_names diff]:
   2.441 -assumes prem: "!!m n. z = int m - int n ==> P" shows "P"
   2.442 - apply (rule_tac z=z in int_cases)
   2.443 -  apply (rule_tac m=n and n=0 in prem, simp)
   2.444 - apply (rule_tac m=0 and n="Suc n" in prem, simp)
   2.445 -done
   2.446 -
   2.447 -lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
   2.448 -
   2.449 -lemmas [simp] = int_Suc
   2.450 -
   2.451 -
   2.452 -subsection {* Legacy ML bindings *}
   2.453 -
   2.454 -ML {*
   2.455 -val of_nat_0 = @{thm of_nat_0};
   2.456 -val of_nat_1 = @{thm of_nat_1};
   2.457 -val of_nat_Suc = @{thm of_nat_Suc};
   2.458 -val of_nat_add = @{thm of_nat_add};
   2.459 -val of_nat_mult = @{thm of_nat_mult};
   2.460 -val of_int_0 = @{thm of_int_0};
   2.461 -val of_int_1 = @{thm of_int_1};
   2.462 -val of_int_add = @{thm of_int_add};
   2.463 -val of_int_mult = @{thm of_int_mult};
   2.464 -val int_eq_of_nat = @{thm int_eq_of_nat};
   2.465 -val zle_int = @{thm zle_int};
   2.466 -val int_int_eq = @{thm int_int_eq};
   2.467 -val diff_int_def = @{thm diff_int_def};
   2.468 -val zadd_ac = @{thms zadd_ac};
   2.469 -val zless_int = @{thm zless_int};
   2.470 -val zadd_int = @{thm zadd_int};
   2.471 -val zmult_int = @{thm zmult_int};
   2.472 -val nat_0_le = @{thm nat_0_le};
   2.473 -val int_0 = @{thm int_0};
   2.474 -val int_1 = @{thm int_1};
   2.475 -val abs_split = @{thm abs_split};
   2.476 -*}
   2.477 +abbreviation
   2.478 +  int_of_nat :: "nat \<Rightarrow> int"
   2.479 +where
   2.480 +  "int_of_nat \<equiv> of_nat"
   2.481  
   2.482  end
     3.1 --- a/src/HOL/IntDiv.thy	Wed Jun 13 03:28:21 2007 +0200
     3.2 +++ b/src/HOL/IntDiv.thy	Wed Jun 13 03:31:11 2007 +0200
     3.3 @@ -11,8 +11,6 @@
     3.4  imports IntArith Divides FunDef
     3.5  begin
     3.6  
     3.7 -declare zless_nat_conj [simp]
     3.8 -
     3.9  constdefs
    3.10    quorem :: "(int*int) * (int*int) => bool"
    3.11      --{*definition of quotient and remainder*}
    3.12 @@ -266,7 +264,7 @@
    3.13    val trans = trans;
    3.14    val prove_eq_sums =
    3.15      let
    3.16 -      val simps = diff_int_def :: Int_Numeral_Simprocs.add_0s @ zadd_ac
    3.17 +      val simps = @{thm diff_int_def} :: Int_Numeral_Simprocs.add_0s @ @{thms zadd_ac}
    3.18      in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
    3.19  end)
    3.20  
    3.21 @@ -1238,9 +1236,9 @@
    3.22    apply simp
    3.23    done
    3.24  
    3.25 -theorem zdvd_int_of_nat: "(x dvd y) = (int_of_nat x dvd int_of_nat y)"
    3.26 +theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
    3.27    unfolding dvd_def
    3.28 -  apply (rule_tac s="\<exists>k. int_of_nat y = int_of_nat x * int_of_nat k" in trans)
    3.29 +  apply (rule_tac s="\<exists>k. int y = int x * int k" in trans)
    3.30    apply (simp only: of_nat_mult [symmetric] of_nat_eq_iff)
    3.31    apply (simp add: ex_nat cong add: conj_cong)
    3.32    apply (rule iffI)
    3.33 @@ -1257,9 +1255,6 @@
    3.34    apply (simp add: mult_ac)
    3.35    done
    3.36  
    3.37 -theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
    3.38 -  unfolding int_eq_of_nat by (rule zdvd_int_of_nat)
    3.39 -
    3.40  lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
    3.41  proof
    3.42    assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by (simp add: zdvd_abs1)
    3.43 @@ -1280,40 +1275,31 @@
    3.44    from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
    3.45  qed
    3.46  
    3.47 -lemma int_of_nat_dvd_iff: "(int_of_nat m dvd z) = (m dvd nat (abs z))"
    3.48 +lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
    3.49    apply (auto simp add: dvd_def nat_abs_mult_distrib)
    3.50 -  apply (auto simp add: nat_eq_iff' abs_if split add: split_if_asm)
    3.51 -   apply (rule_tac x = "-(int_of_nat k)" in exI)
    3.52 +  apply (auto simp add: nat_eq_iff abs_if split add: split_if_asm)
    3.53 +   apply (rule_tac x = "-(int k)" in exI)
    3.54    apply auto
    3.55    done
    3.56  
    3.57 -lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
    3.58 -  unfolding int_eq_of_nat by (rule int_of_nat_dvd_iff)
    3.59 -
    3.60 -lemma dvd_int_of_nat_iff: "(z dvd int_of_nat m) = (nat (abs z) dvd m)"
    3.61 +lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
    3.62    apply (auto simp add: dvd_def abs_if)
    3.63      apply (rule_tac [3] x = "nat k" in exI)
    3.64 -    apply (rule_tac [2] x = "-(int_of_nat k)" in exI)
    3.65 +    apply (rule_tac [2] x = "-(int k)" in exI)
    3.66      apply (rule_tac x = "nat (-k)" in exI)
    3.67 -    apply (cut_tac [3] m = m and 'a=int in of_nat_less_0_iff)
    3.68 -    apply (cut_tac m = m and 'a=int in of_nat_less_0_iff)
    3.69 +    apply (cut_tac [3] m = m in int_less_0_conv)
    3.70 +    apply (cut_tac m = m in int_less_0_conv)
    3.71      apply (auto simp add: zero_le_mult_iff mult_less_0_iff
    3.72 -      nat_mult_distrib [symmetric] nat_eq_iff2')
    3.73 -  done
    3.74 -
    3.75 -lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
    3.76 -  unfolding int_eq_of_nat by (rule dvd_int_of_nat_iff)
    3.77 -
    3.78 -lemma nat_dvd_iff': "(nat z dvd m) = (if 0 \<le> z then (z dvd int_of_nat m) else m = 0)"
    3.79 -  apply (auto simp add: dvd_def)
    3.80 -  apply (rule_tac x = "nat k" in exI)
    3.81 -  apply (cut_tac m = m and 'a=int in of_nat_less_0_iff)
    3.82 -  apply (auto simp add: zero_le_mult_iff mult_less_0_iff
    3.83 -    nat_mult_distrib [symmetric] nat_eq_iff2')
    3.84 +      nat_mult_distrib [symmetric] nat_eq_iff2)
    3.85    done
    3.86  
    3.87  lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
    3.88 -  unfolding int_eq_of_nat by (rule nat_dvd_iff')
    3.89 +  apply (auto simp add: dvd_def)
    3.90 +  apply (rule_tac x = "nat k" in exI)
    3.91 +  apply (cut_tac m = m in int_less_0_conv)
    3.92 +  apply (auto simp add: zero_le_mult_iff mult_less_0_iff
    3.93 +    nat_mult_distrib [symmetric] nat_eq_iff2)
    3.94 +  done
    3.95  
    3.96  lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))"
    3.97    apply (auto simp add: dvd_def)
    3.98 @@ -1327,9 +1313,9 @@
    3.99    done
   3.100  
   3.101  lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
   3.102 -  apply (rule_tac z=n in int_cases')
   3.103 -  apply (auto simp add: dvd_int_of_nat_iff)
   3.104 -  apply (rule_tac z=z in int_cases')
   3.105 +  apply (rule_tac z=n in int_cases)
   3.106 +  apply (auto simp add: dvd_int_iff)
   3.107 +  apply (rule_tac z=z in int_cases)
   3.108    apply (auto simp add: dvd_imp_le)
   3.109    done
   3.110  
   3.111 @@ -1377,33 +1363,25 @@
   3.112  done
   3.113  
   3.114  lemma int_power: "int (m^n) = (int m) ^ n"
   3.115 -  by (induct n, simp_all add: int_mult)
   3.116 +  by (rule of_nat_power)
   3.117  
   3.118  text{*Compatibility binding*}
   3.119  lemmas zpower_int = int_power [symmetric]
   3.120  
   3.121 -lemma int_of_nat_div:
   3.122 -  "int_of_nat (a div b) = (int_of_nat a) div (int_of_nat b)"
   3.123 +lemma zdiv_int: "int (a div b) = (int a) div (int b)"
   3.124  apply (subst split_div, auto)
   3.125  apply (subst split_zdiv, auto)
   3.126 -apply (rule_tac a="int_of_nat (b * i) + int_of_nat j" and b="int_of_nat b" and r="int_of_nat j" and r'=ja in IntDiv.unique_quotient)
   3.127 -apply (auto simp add: IntDiv.quorem_def)
   3.128 -done
   3.129 -
   3.130 -lemma zdiv_int: "int (a div b) = (int a) div (int b)"
   3.131 -  unfolding int_eq_of_nat by (rule int_of_nat_div)
   3.132 -
   3.133 -lemma int_of_nat_mod:
   3.134 -  "int_of_nat (a mod b) = (int_of_nat a) mod (int_of_nat b)"
   3.135 -apply (subst split_mod, auto)
   3.136 -apply (subst split_zmod, auto)
   3.137 -apply (rule_tac a="int_of_nat (b * i) + int_of_nat j" and b="int_of_nat b" and q="int_of_nat i" and q'=ia 
   3.138 -       in unique_remainder)
   3.139 +apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient)
   3.140  apply (auto simp add: IntDiv.quorem_def)
   3.141  done
   3.142  
   3.143  lemma zmod_int: "int (a mod b) = (int a) mod (int b)"
   3.144 -  unfolding int_eq_of_nat by (rule int_of_nat_mod)
   3.145 +apply (subst split_mod, auto)
   3.146 +apply (subst split_zmod, auto)
   3.147 +apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia 
   3.148 +       in unique_remainder)
   3.149 +apply (auto simp add: IntDiv.quorem_def)
   3.150 +done
   3.151  
   3.152  text{*Suggested by Matthias Daum*}
   3.153  lemma int_power_div_base:
     4.1 --- a/src/HOL/Library/EfficientNat.thy	Wed Jun 13 03:28:21 2007 +0200
     4.2 +++ b/src/HOL/Library/EfficientNat.thy	Wed Jun 13 03:31:11 2007 +0200
     4.3 @@ -31,6 +31,19 @@
     4.4    nat_of_int :: "int \<Rightarrow> nat" where
     4.5    "k \<ge> 0 \<Longrightarrow> nat_of_int k = nat k"
     4.6  
     4.7 +definition
     4.8 +  int' :: "nat \<Rightarrow> int" where
     4.9 +  "int' n = of_nat n"
    4.10 +
    4.11 +lemma int'_Suc [simp]: "int' (Suc n) = 1 + int' n"
    4.12 +unfolding int'_def by simp
    4.13 +
    4.14 +lemma int'_add: "int' (m + n) = int' m + int' n"
    4.15 +unfolding int'_def by (rule of_nat_add)
    4.16 +
    4.17 +lemma int'_mult: "int' (m * n) = int' m * int' n"
    4.18 +unfolding int'_def by (rule of_nat_mult)
    4.19 +
    4.20  lemma nat_of_int_of_number_of:
    4.21    fixes k
    4.22    assumes "k \<ge> 0"
    4.23 @@ -44,8 +57,11 @@
    4.24    using prems unfolding Pls_def by simp
    4.25  
    4.26  lemma nat_of_int_int:
    4.27 -  "nat_of_int (int n) = n"
    4.28 -  using zero_zle_int nat_of_int_def by simp
    4.29 +  "nat_of_int (int' n) = n"
    4.30 +  using nat_of_int_def int'_def by simp
    4.31 +
    4.32 +lemma eq_nat_of_int: "int' n = x \<Longrightarrow> n = nat_of_int x"
    4.33 +by (erule subst, simp only: nat_of_int_int)
    4.34  
    4.35  text {*
    4.36    Case analysis on natural numbers is rephrased using a conditional
    4.37 @@ -66,10 +82,10 @@
    4.38  qed
    4.39  
    4.40  lemma [code inline]:
    4.41 -  "nat_case = (\<lambda>f g n. if n = 0 then f else g (nat_of_int (int n - 1)))"
    4.42 +  "nat_case = (\<lambda>f g n. if n = 0 then f else g (nat_of_int (int' n - 1)))"
    4.43  proof (rule ext)+
    4.44    fix f g n
    4.45 -  show "nat_case f g n = (if n = 0 then f else g (nat_of_int (int n - 1)))"
    4.46 +  show "nat_case f g n = (if n = 0 then f else g (nat_of_int (int' n - 1)))"
    4.47    by (cases n) (simp_all add: nat_of_int_int)
    4.48  qed
    4.49  
    4.50 @@ -82,43 +98,33 @@
    4.51    by (simp add: nat_of_int_def)
    4.52  lemma [code func, code inline]:  "1 = nat_of_int 1"
    4.53    by (simp add: nat_of_int_def)
    4.54 -lemma [code func]: "Suc n = nat_of_int (int n + 1)"
    4.55 -  by (simp add: nat_of_int_def)
    4.56 -lemma [code]: "m + n = nat (int m + int n)"
    4.57 -  by arith
    4.58 -lemma [code func, code inline]: "m + n = nat_of_int (int m + int n)"
    4.59 -  by (simp add: nat_of_int_def)
    4.60 -lemma [code, code inline]: "m - n = nat (int m - int n)"
    4.61 -  by arith
    4.62 -lemma [code]: "m * n = nat (int m * int n)"
    4.63 -  unfolding zmult_int by simp
    4.64 -lemma [code func, code inline]: "m * n = nat_of_int (int m * int n)"
    4.65 -proof -
    4.66 -  have "int (m * n) = int m * int n"
    4.67 -    by (induct m) (simp_all add: zadd_zmult_distrib)
    4.68 -  then have "m * n = nat (int m * int n)" by auto
    4.69 -  also have "\<dots> = nat_of_int (int m * int n)"
    4.70 -  proof -
    4.71 -    have "int m \<ge> 0" and "int n \<ge> 0" by auto
    4.72 -    have "int m * int n \<ge> 0" by (rule split_mult_pos_le) auto
    4.73 -    with nat_of_int_def show ?thesis by auto
    4.74 -  qed
    4.75 -  finally show ?thesis .
    4.76 -qed  
    4.77 -lemma [code]: "m div n = nat (int m div int n)"
    4.78 -  unfolding zdiv_int [symmetric] by simp
    4.79 +lemma [code func]: "Suc n = nat_of_int (int' n + 1)"
    4.80 +  by (simp add: eq_nat_of_int)
    4.81 +lemma [code]: "m + n = nat (int' m + int' n)"
    4.82 +  by (simp add: int'_def nat_eq_iff2)
    4.83 +lemma [code func, code inline]: "m + n = nat_of_int (int' m + int' n)"
    4.84 +  by (simp add: eq_nat_of_int int'_add)
    4.85 +lemma [code, code inline]: "m - n = nat (int' m - int' n)"
    4.86 +  by (simp add: int'_def nat_eq_iff2)
    4.87 +lemma [code]: "m * n = nat (int' m * int' n)"
    4.88 +  unfolding int'_def
    4.89 +  by (simp add: of_nat_mult [symmetric] del: of_nat_mult)
    4.90 +lemma [code func, code inline]: "m * n = nat_of_int (int' m * int' n)"
    4.91 +  by (simp add: eq_nat_of_int int'_mult)
    4.92 +lemma [code]: "m div n = nat (int' m div int' n)"
    4.93 +  unfolding int'_def zdiv_int [symmetric] by simp
    4.94  lemma [code func]: "m div n = fst (Divides.divmod m n)"
    4.95    unfolding divmod_def by simp
    4.96 -lemma [code]: "m mod n = nat (int m mod int n)"
    4.97 -  unfolding zmod_int [symmetric] by simp
    4.98 +lemma [code]: "m mod n = nat (int' m mod int' n)"
    4.99 +  unfolding int'_def zmod_int [symmetric] by simp
   4.100  lemma [code func]: "m mod n = snd (Divides.divmod m n)"
   4.101    unfolding divmod_def by simp
   4.102 -lemma [code, code inline]: "(m < n) \<longleftrightarrow> (int m < int n)"
   4.103 -  by simp
   4.104 -lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int m \<le> int n)"
   4.105 -  by simp
   4.106 -lemma [code func, code inline]: "m = n \<longleftrightarrow> int m = int n"
   4.107 -  by simp
   4.108 +lemma [code, code inline]: "(m < n) \<longleftrightarrow> (int' m < int' n)"
   4.109 +  unfolding int'_def by simp
   4.110 +lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int' m \<le> int' n)"
   4.111 +  unfolding int'_def by simp
   4.112 +lemma [code func, code inline]: "m = n \<longleftrightarrow> int' m = int' n"
   4.113 +  unfolding int'_def by simp
   4.114  lemma [code func]: "nat k = (if k < 0 then 0 else nat_of_int k)"
   4.115  proof (cases "k < 0")
   4.116    case True then show ?thesis by simp
   4.117 @@ -126,26 +132,27 @@
   4.118    case False then show ?thesis by (simp add: nat_of_int_def)
   4.119  qed
   4.120  lemma [code func]:
   4.121 -  "int_aux i n = (if int n = 0 then i else int_aux (i + 1) (nat_of_int (int n - 1)))"
   4.122 +  "int_aux i n = (if int' n = 0 then i else int_aux (i + 1) (nat_of_int (int' n - 1)))"
   4.123  proof -
   4.124 -  have "0 < n \<Longrightarrow> int n = 1 + int (nat_of_int (int n - 1))"
   4.125 +  have "0 < n \<Longrightarrow> int' n = 1 + int' (nat_of_int (int' n - 1))"
   4.126    proof -
   4.127      assume prem: "n > 0"
   4.128 -    then have "int n - 1 \<ge> 0" by auto
   4.129 -    then have "nat_of_int (int n - 1) = nat (int n - 1)" by (simp add: nat_of_int_def)
   4.130 -    with prem show "int n = 1 + int (nat_of_int (int n - 1))" by simp
   4.131 +    then have "int' n - 1 \<ge> 0" unfolding int'_def by auto
   4.132 +    then have "nat_of_int (int' n - 1) = nat (int' n - 1)" by (simp add: nat_of_int_def)
   4.133 +    with prem show "int' n = 1 + int' (nat_of_int (int' n - 1))" unfolding int'_def by simp
   4.134    qed
   4.135 -  then show ?thesis unfolding int_aux_def by simp
   4.136 +  then show ?thesis unfolding int_aux_def int'_def by simp
   4.137  qed
   4.138  
   4.139  lemma div_nat_code [code func]:
   4.140 -  "m div k = nat_of_int (fst (divAlg (int m, int k)))"
   4.141 -  unfolding div_def [symmetric] zdiv_int [symmetric] nat_of_int_int ..
   4.142 +  "m div k = nat_of_int (fst (divAlg (int' m, int' k)))"
   4.143 +  unfolding div_def [symmetric] int'_def zdiv_int [symmetric]
   4.144 +  unfolding int'_def [symmetric] nat_of_int_int ..
   4.145  
   4.146  lemma mod_nat_code [code func]:
   4.147 -  "m mod k = nat_of_int (snd (divAlg (int m, int k)))"
   4.148 -  unfolding mod_def [symmetric] zmod_int [symmetric] nat_of_int_int ..
   4.149 -
   4.150 +  "m mod k = nat_of_int (snd (divAlg (int' m, int' k)))"
   4.151 +  unfolding mod_def [symmetric] int'_def zmod_int [symmetric]
   4.152 +  unfolding int'_def [symmetric] nat_of_int_int ..
   4.153  
   4.154  subsection {* Code generator setup for basic functions *}
   4.155  
   4.156 @@ -185,13 +192,13 @@
   4.157  *}
   4.158  
   4.159  consts_code
   4.160 -  int ("(_)")
   4.161 +  int' ("(_)")
   4.162    nat ("\<module>nat")
   4.163  attach {*
   4.164  fun nat i = if i < 0 then 0 else i;
   4.165  *}
   4.166  
   4.167 -code_const int
   4.168 +code_const int'
   4.169    (SML "_")
   4.170    (OCaml "_")
   4.171    (Haskell "_")
   4.172 @@ -392,6 +399,6 @@
   4.173    Nat Integer
   4.174    EfficientNat Integer
   4.175  
   4.176 -hide const nat_of_int
   4.177 +hide const nat_of_int int'
   4.178  
   4.179  end
     5.1 --- a/src/HOL/Library/GCD.thy	Wed Jun 13 03:28:21 2007 +0200
     5.2 +++ b/src/HOL/Library/GCD.thy	Wed Jun 13 03:31:11 2007 +0200
     5.3 @@ -265,7 +265,7 @@
     5.4    from relprime_dvd_mult [OF g th] obtain h' where h': "nat \<bar>k\<bar> = nat \<bar>i\<bar> * h'"
     5.5      unfolding dvd_def by blast
     5.6    from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp
     5.7 -  then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
     5.8 +  then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by simp
     5.9    then show ?thesis
    5.10      apply (subst zdvd_abs1 [symmetric])
    5.11      apply (subst zdvd_abs2 [symmetric])
     6.1 --- a/src/HOL/Library/Word.thy	Wed Jun 13 03:28:21 2007 +0200
     6.2 +++ b/src/HOL/Library/Word.thy	Wed Jun 13 03:31:11 2007 +0200
     6.3 @@ -989,12 +989,12 @@
     6.4  next
     6.5    fix xs
     6.6    assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs"
     6.7 -  show "bv_to_int (norm_signed (\<one>#xs)) = -1 - int (bv_to_nat (bv_not xs))"
     6.8 +  show "bv_to_int (norm_signed (\<one>#xs)) = - int (bv_to_nat (bv_not xs)) + -1"
     6.9    proof (rule bit_list_cases [of xs],simp_all)
    6.10      fix ys
    6.11      assume [simp]: "xs = \<one>#ys"
    6.12      from ind
    6.13 -    show "bv_to_int (norm_signed (\<one>#ys)) = -1 - int (bv_to_nat (bv_not ys))"
    6.14 +    show "bv_to_int (norm_signed (\<one>#ys)) = - int (bv_to_nat (bv_not ys)) + -1"
    6.15        by simp
    6.16    qed
    6.17  qed
    6.18 @@ -1007,11 +1007,11 @@
    6.19      by (simp add: int_nat_two_exp)
    6.20  next
    6.21    fix bs
    6.22 -  have "-1 - int (bv_to_nat (bv_not bs)) \<le> 0"
    6.23 +  have "- int (bv_to_nat (bv_not bs)) + -1 \<le> 0"
    6.24      by simp
    6.25    also have "... < 2 ^ length bs"
    6.26      by (induct bs,simp_all)
    6.27 -  finally show "-1 - int (bv_to_nat (bv_not bs)) < 2 ^ length bs"
    6.28 +  finally show "- int (bv_to_nat (bv_not bs)) + -1 < 2 ^ length bs"
    6.29      .
    6.30  qed
    6.31  
    6.32 @@ -1027,7 +1027,7 @@
    6.33  next
    6.34    fix bs
    6.35    from bv_to_nat_upper_range [of "bv_not bs"]
    6.36 -  show "- (2 ^ length bs) \<le> -1 - int (bv_to_nat (bv_not bs))"
    6.37 +  show "- (2 ^ length bs) \<le> - int (bv_to_nat (bv_not bs)) + -1"
    6.38      by (simp add: int_nat_two_exp)
    6.39  qed
    6.40  
     7.1 --- a/src/HOL/NatBin.thy	Wed Jun 13 03:28:21 2007 +0200
     7.2 +++ b/src/HOL/NatBin.thy	Wed Jun 13 03:31:11 2007 +0200
     7.3 @@ -58,14 +58,14 @@
     7.4  apply (case_tac "0 <= z'")
     7.5  apply (auto simp add: div_nonneg_neg_le0 DIVISION_BY_ZERO_DIV)
     7.6  apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO)
     7.7 -apply (auto elim!: nonneg_eq_int_of_nat)
     7.8 +apply (auto elim!: nonneg_eq_int)
     7.9  apply (rename_tac m m')
    7.10 -apply (subgoal_tac "0 <= int_of_nat m div int_of_nat m'")
    7.11 +apply (subgoal_tac "0 <= int m div int m'")
    7.12   prefer 2 apply (simp add: nat_numeral_0_eq_0 pos_imp_zdiv_nonneg_iff) 
    7.13  apply (rule of_nat_eq_iff [where 'a=int, THEN iffD1], simp)
    7.14 -apply (rule_tac r = "int_of_nat (m mod m') " in quorem_div)
    7.15 +apply (rule_tac r = "int (m mod m') " in quorem_div)
    7.16   prefer 2 apply force
    7.17 -apply (simp add: nat_less_iff' [symmetric] quorem_def nat_numeral_0_eq_0
    7.18 +apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0
    7.19                   of_nat_add [symmetric] of_nat_mult [symmetric]
    7.20              del: of_nat_add of_nat_mult)
    7.21  done
    7.22 @@ -74,14 +74,14 @@
    7.23  lemma nat_mod_distrib:
    7.24       "[| (0::int) <= z;  0 <= z' |] ==> nat (z mod z') = nat z mod nat z'"
    7.25  apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO)
    7.26 -apply (auto elim!: nonneg_eq_int_of_nat)
    7.27 +apply (auto elim!: nonneg_eq_int)
    7.28  apply (rename_tac m m')
    7.29 -apply (subgoal_tac "0 <= int_of_nat m mod int_of_nat m'")
    7.30 - prefer 2 apply (simp add: nat_less_iff nat_numeral_0_eq_0 pos_mod_sign) 
    7.31 -apply (rule of_nat_eq_iff [where 'a=int, THEN iffD1], simp)
    7.32 -apply (rule_tac q = "int_of_nat (m div m') " in quorem_mod)
    7.33 +apply (subgoal_tac "0 <= int m mod int m'")
    7.34 + prefer 2 apply (simp add: nat_less_iff nat_numeral_0_eq_0 pos_mod_sign)
    7.35 +apply (rule int_int_eq [THEN iffD1], simp)
    7.36 +apply (rule_tac q = "int (m div m') " in quorem_mod)
    7.37   prefer 2 apply force
    7.38 -apply (simp add: nat_less_iff' [symmetric] quorem_def nat_numeral_0_eq_0
    7.39 +apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0
    7.40                   of_nat_add [symmetric] of_nat_mult [symmetric]
    7.41              del: of_nat_add of_nat_mult)
    7.42  done
    7.43 @@ -97,14 +97,7 @@
    7.44  
    7.45  (*"neg" is used in rewrite rules for binary comparisons*)
    7.46  lemma int_nat_number_of [simp]:
    7.47 -     "int (number_of v :: nat) =  
    7.48 -         (if neg (number_of v :: int) then 0  
    7.49 -          else (number_of v :: int))"
    7.50 -by (simp del: nat_number_of
    7.51 -	 add: neg_nat nat_number_of_def not_neg_nat add_assoc)
    7.52 -
    7.53 -lemma int_of_nat_number_of [simp]:
    7.54 -     "int_of_nat (number_of v) =  
    7.55 +     "int (number_of v) =  
    7.56           (if neg (number_of v :: int) then 0  
    7.57            else (number_of v :: int))"
    7.58  by (simp del: nat_number_of
    7.59 @@ -520,9 +513,6 @@
    7.60  by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
    7.61  
    7.62  
    7.63 -(* Push int(.) inwards: *)
    7.64 -declare zadd_int [symmetric, simp]
    7.65 -
    7.66  lemma lemma1: "(m+m = n+n) = (m = (n::int))"
    7.67  by auto
    7.68  
     8.1 --- a/src/HOL/NumberTheory/Fib.thy	Wed Jun 13 03:28:21 2007 +0200
     8.2 +++ b/src/HOL/NumberTheory/Fib.thy	Wed Jun 13 03:31:11 2007 +0200
     8.3 @@ -85,7 +85,7 @@
     8.4    (if n mod 2 = 0 then fib (Suc n) * fib (Suc n) - 1
     8.5     else fib (Suc n) * fib (Suc n) + 1)"
     8.6    apply (rule int_int_eq [THEN iffD1]) 
     8.7 -  apply (simp add: fib_Cassini_int) 
     8.8 +  apply (simp add: fib_Cassini_int del: of_nat_mult) 
     8.9    apply (subst zdiff_int [symmetric]) 
    8.10     apply (insert fib_Suc_gr_0 [of n], simp_all)
    8.11    done
     9.1 --- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed Jun 13 03:28:21 2007 +0200
     9.2 +++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed Jun 13 03:31:11 2007 +0200
     9.3 @@ -281,7 +281,7 @@
     9.4  
     9.5  lemma S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
     9.6    using P_set_card Q_set_card P_set_finite Q_set_finite
     9.7 -  by (auto simp add: S_def zmult_int setsum_constant)
     9.8 +  by (auto simp add: S_def setsum_constant)
     9.9  
    9.10  lemma S1_Int_S2_prop: "S1 \<inter> S2 = {}"
    9.11    by (auto simp add: S1_def S2_def)
    10.1 --- a/src/HOL/Numeral.thy	Wed Jun 13 03:28:21 2007 +0200
    10.2 +++ b/src/HOL/Numeral.thy	Wed Jun 13 03:31:11 2007 +0200
    10.3 @@ -457,7 +457,7 @@
    10.4  
    10.5  lemma odd_less_0:
    10.6    "(1 + z + z < 0) = (z < (0::int))";
    10.7 -proof (cases z rule: int_cases')
    10.8 +proof (cases z rule: int_cases)
    10.9    case (nonneg n)
   10.10    thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
   10.11                               le_imp_0_less [THEN order_less_imp_le])  
   10.12 @@ -593,7 +593,7 @@
   10.13    "int_aux i (Suc n) = int_aux (i + 1) n" -- {* tail recursive *}
   10.14    by (simp add: int_aux_def)+
   10.15  
   10.16 -lemma [code]:
   10.17 +lemma [code unfold]:
   10.18    "int n = int_aux 0 n"
   10.19    by (simp add: int_aux_def)
   10.20  
    11.1 --- a/src/HOL/Presburger.thy	Wed Jun 13 03:28:21 2007 +0200
    11.2 +++ b/src/HOL/Presburger.thy	Wed Jun 13 03:31:11 2007 +0200
    11.3 @@ -383,29 +383,14 @@
    11.4    by (simp split add: split_nat)
    11.5  
    11.6  lemma ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
    11.7 -  by (auto split add: split_nat) 
    11.8 -(rule_tac x = "nat x" in exI,erule_tac x = "nat x" in allE, simp)
    11.9 +  apply (auto split add: split_nat)
   11.10 +  apply (rule_tac x="int x" in exI, simp)
   11.11 +  apply (rule_tac x = "nat x" in exI,erule_tac x = "nat x" in allE, simp)
   11.12 +  done
   11.13  
   11.14  lemma zdiff_int_split: "P (int (x - y)) =
   11.15    ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
   11.16 -  by (case_tac "y \<le> x",simp_all add: zdiff_int)
   11.17 -
   11.18 -lemma zdvd_int: "(x dvd y) = (int x dvd int y)"
   11.19 -  apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
   11.20 -    nat_0_le cong add: conj_cong)
   11.21 -  apply (rule iffI)
   11.22 -  apply iprover
   11.23 -  apply (erule exE)
   11.24 -  apply (case_tac "x=0")
   11.25 -  apply (rule_tac x=0 in exI)
   11.26 -  apply simp
   11.27 -  apply (case_tac "0 \<le> k")
   11.28 -  apply iprover
   11.29 -  apply (simp add: linorder_not_le)
   11.30 -  apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
   11.31 -  apply assumption
   11.32 -  apply (simp add: mult_ac)
   11.33 -  done
   11.34 +  by (case_tac "y \<le> x", simp_all)
   11.35  
   11.36  lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)" by simp
   11.37  lemma number_of2: "(0::int) <= Numeral0" by simp
   11.38 @@ -670,4 +655,4 @@
   11.39    less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
   11.40    less_number_of
   11.41  
   11.42 -end
   11.43 \ No newline at end of file
   11.44 +end
    12.1 --- a/src/HOL/Real/Float.thy	Wed Jun 13 03:28:21 2007 +0200
    12.2 +++ b/src/HOL/Real/Float.thy	Wed Jun 13 03:31:11 2007 +0200
    12.3 @@ -35,7 +35,8 @@
    12.4      apply (auto, induct_tac n)
    12.5      apply (simp_all add: pow2_def)
    12.6      apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
    12.7 -    by (auto simp add: h)
    12.8 +    apply (auto simp add: h)
    12.9 +    by (simp add: add_commute)
   12.10    show ?thesis
   12.11    proof (induct a)
   12.12      case (1 n)
   12.13 @@ -45,7 +46,7 @@
   12.14      show ?case
   12.15        apply (auto)
   12.16        apply (subst pow2_neg[of "- int n"])
   12.17 -      apply (subst pow2_neg[of "-1 - int n"])
   12.18 +      apply (subst pow2_neg[of "- int n + -1"])
   12.19        apply (auto simp add: g pos)
   12.20        done
   12.21    qed
    13.1 --- a/src/HOL/Real/Rational.thy	Wed Jun 13 03:28:21 2007 +0200
    13.2 +++ b/src/HOL/Real/Rational.thy	Wed Jun 13 03:31:11 2007 +0200
    13.3 @@ -565,7 +565,7 @@
    13.4  by (induct n) (simp_all add: of_rat_add)
    13.5  
    13.6  lemma of_rat_of_int_eq [simp]: "of_rat (of_int z) = of_int z"
    13.7 -by (cases z rule: int_diff_cases', simp add: of_rat_diff)
    13.8 +by (cases z rule: int_diff_cases, simp add: of_rat_diff)
    13.9  
   13.10  lemma of_rat_number_of_eq [simp]:
   13.11    "of_rat (number_of w) = (number_of w :: 'a::{number_ring,field_char_0})"
    14.1 --- a/src/HOL/arith_data.ML	Wed Jun 13 03:28:21 2007 +0200
    14.2 +++ b/src/HOL/arith_data.ML	Wed Jun 13 03:31:11 2007 +0200
    14.3 @@ -601,7 +601,7 @@
    14.4          val terms2      = map (subst_term [(split_term, zero_nat)]) rev_terms
    14.5          val t1'         = incr_boundvars 1 t1
    14.6          val t1_eq_int_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
    14.7 -                            (Const ("IntDef.int", HOLogic.natT --> HOLogic.intT) $ n)
    14.8 +                            (Const ("Nat.of_nat", HOLogic.natT --> HOLogic.intT) $ n)
    14.9          val t1_lt_zero  = Const (@{const_name Orderings.less},
   14.10                              HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
   14.11          val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
    15.1 --- a/src/HOL/int_arith1.ML	Wed Jun 13 03:28:21 2007 +0200
    15.2 +++ b/src/HOL/int_arith1.ML	Wed Jun 13 03:31:11 2007 +0200
    15.3 @@ -573,10 +573,11 @@
    15.4       @{thm mult_zero_left}, @{thm mult_zero_right}, @{thm mult_num1}, @{thm mult_1_right},
    15.5       @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym,
    15.6       @{thm minus_add_distrib}, @{thm minus_minus}, @{thm mult_assoc},
    15.7 -     of_nat_0, of_nat_1, of_nat_Suc, of_nat_add, of_nat_mult,
    15.8 -     of_int_0, of_int_1, of_int_add, of_int_mult, int_eq_of_nat]
    15.9 +     @{thm of_nat_0}, @{thm of_nat_1}, @{thm of_nat_Suc}, @{thm of_nat_add},
   15.10 +     @{thm of_nat_mult}, @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add},
   15.11 +     @{thm of_int_mult}]
   15.12  
   15.13 -val nat_inj_thms = [zle_int RS iffD2, int_int_eq RS iffD2]
   15.14 +val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
   15.15  
   15.16  val Int_Numeral_Base_Simprocs = assoc_fold_simproc
   15.17    :: Int_Numeral_Simprocs.combine_numerals
   15.18 @@ -595,7 +596,6 @@
   15.19                        addsimprocs Int_Numeral_Base_Simprocs
   15.20                        addcongs [if_weak_cong]}) #>
   15.21    arith_inj_const ("Nat.of_nat", HOLogic.natT --> HOLogic.intT) #>
   15.22 -  arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT) #>
   15.23    arith_discrete "IntDef.int"
   15.24  
   15.25  end;