introduce abbreviation 'int' earlier in Int.thy
authorhuffman
Sun Sep 04 07:15:13 2011 -0700 (2011-09-04)
changeset 4470979f10d9e63c1
parent 44708 37ce74ff4203
child 44710 9caf6883f1f4
introduce abbreviation 'int' earlier in Int.thy
src/HOL/Int.thy
     1.1 --- a/src/HOL/Int.thy	Sun Sep 04 06:56:10 2011 -0700
     1.2 +++ b/src/HOL/Int.thy	Sun Sep 04 07:15:13 2011 -0700
     1.3 @@ -162,7 +162,10 @@
     1.4      by (simp add: Zero_int_def One_int_def)
     1.5  qed
     1.6  
     1.7 -lemma int_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})"
     1.8 +abbreviation int :: "nat \<Rightarrow> int" where
     1.9 +  "int \<equiv> of_nat"
    1.10 +
    1.11 +lemma int_def: "int m = Abs_Integ (intrel `` {(m, 0)})"
    1.12  by (induct m) (simp_all add: Zero_int_def One_int_def add)
    1.13  
    1.14  
    1.15 @@ -218,7 +221,7 @@
    1.16  
    1.17  text{*strict, in 1st argument; proof is by induction on k>0*}
    1.18  lemma zmult_zless_mono2_lemma:
    1.19 -     "(i::int)<j ==> 0<k ==> of_nat k * i < of_nat k * j"
    1.20 +     "(i::int)<j ==> 0<k ==> int k * i < int k * j"
    1.21  apply (induct k)
    1.22  apply simp
    1.23  apply (simp add: left_distrib)
    1.24 @@ -226,13 +229,13 @@
    1.25  apply (simp_all add: add_strict_mono)
    1.26  done
    1.27  
    1.28 -lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = of_nat n"
    1.29 +lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = int n"
    1.30  apply (cases k)
    1.31  apply (auto simp add: le add int_def Zero_int_def)
    1.32  apply (rule_tac x="x-y" in exI, simp)
    1.33  done
    1.34  
    1.35 -lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = of_nat n"
    1.36 +lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = int n"
    1.37  apply (cases k)
    1.38  apply (simp add: less int_def Zero_int_def)
    1.39  apply (rule_tac x="x-y" in exI, simp)
    1.40 @@ -261,7 +264,7 @@
    1.41  done
    1.42  
    1.43  lemma zless_iff_Suc_zadd:
    1.44 -  "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + of_nat (Suc n))"
    1.45 +  "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + int (Suc n))"
    1.46  apply (cases z, cases w)
    1.47  apply (auto simp add: less add int_def)
    1.48  apply (rename_tac a b c d) 
    1.49 @@ -314,7 +317,7 @@
    1.50  done
    1.51  
    1.52  text{*Collapse nested embeddings*}
    1.53 -lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
    1.54 +lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n"
    1.55  by (induct n) auto
    1.56  
    1.57  lemma of_int_power:
    1.58 @@ -400,13 +403,13 @@
    1.59      by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
    1.60  qed
    1.61  
    1.62 -lemma nat_int [simp]: "nat (of_nat n) = n"
    1.63 +lemma nat_int [simp]: "nat (int n) = n"
    1.64  by (simp add: nat int_def)
    1.65  
    1.66 -lemma int_nat_eq [simp]: "of_nat (nat z) = (if 0 \<le> z then z else 0)"
    1.67 +lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
    1.68  by (cases z) (simp add: nat le int_def Zero_int_def)
    1.69  
    1.70 -corollary nat_0_le: "0 \<le> z ==> of_nat (nat z) = z"
    1.71 +corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
    1.72  by simp
    1.73  
    1.74  lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
    1.75 @@ -431,14 +434,14 @@
    1.76  
    1.77  lemma nonneg_eq_int:
    1.78    fixes z :: int
    1.79 -  assumes "0 \<le> z" and "\<And>m. z = of_nat m \<Longrightarrow> P"
    1.80 +  assumes "0 \<le> z" and "\<And>m. z = int m \<Longrightarrow> P"
    1.81    shows P
    1.82    using assms by (blast dest: nat_0_le sym)
    1.83  
    1.84 -lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = of_nat m else m=0)"
    1.85 +lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
    1.86  by (cases w) (simp add: nat le int_def Zero_int_def, arith)
    1.87  
    1.88 -corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = of_nat m else m=0)"
    1.89 +corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
    1.90  by (simp only: eq_commute [of m] nat_eq_iff)
    1.91  
    1.92  lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
    1.93 @@ -446,7 +449,7 @@
    1.94  apply (simp add: nat le int_def Zero_int_def linorder_not_le[symmetric], arith)
    1.95  done
    1.96  
    1.97 -lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> of_nat n"
    1.98 +lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n"
    1.99    by (cases x, simp add: nat le int_def le_diff_conv)
   1.100  
   1.101  lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y"
   1.102 @@ -470,10 +473,10 @@
   1.103  by (cases z, cases z')
   1.104    (simp add: nat add minus diff_minus le Zero_int_def)
   1.105  
   1.106 -lemma nat_zminus_int [simp]: "nat (- (of_nat n)) = 0"
   1.107 +lemma nat_zminus_int [simp]: "nat (- int n) = 0"
   1.108  by (simp add: int_def minus nat Zero_int_def) 
   1.109  
   1.110 -lemma zless_nat_eq_int_zless: "(m < nat z) = (of_nat m < z)"
   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  context ring_1
   1.115 @@ -491,31 +494,31 @@
   1.116  
   1.117  subsection{*Lemmas about the Function @{term of_nat} and Orderings*}
   1.118  
   1.119 -lemma negative_zless_0: "- (of_nat (Suc n)) < (0 \<Colon> int)"
   1.120 +lemma negative_zless_0: "- (int (Suc n)) < (0 \<Colon> int)"
   1.121  by (simp add: order_less_le del: of_nat_Suc)
   1.122  
   1.123 -lemma negative_zless [iff]: "- (of_nat (Suc n)) < (of_nat m \<Colon> int)"
   1.124 +lemma negative_zless [iff]: "- (int (Suc n)) < int m"
   1.125  by (rule negative_zless_0 [THEN order_less_le_trans], simp)
   1.126  
   1.127 -lemma negative_zle_0: "- of_nat n \<le> (0 \<Colon> int)"
   1.128 +lemma negative_zle_0: "- int n \<le> 0"
   1.129  by (simp add: minus_le_iff)
   1.130  
   1.131 -lemma negative_zle [iff]: "- of_nat n \<le> (of_nat m \<Colon> int)"
   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> - (of_nat (Suc n) \<Colon> int))"
   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: "((of_nat n \<Colon> int) \<le> - of_nat m) = (n = 0 & m = 0)"
   1.140 +lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
   1.141  by (simp add: int_def le minus Zero_int_def)
   1.142  
   1.143 -lemma not_int_zless_negative [simp]: "~ ((of_nat n \<Colon> int) < - of_nat m)"
   1.144 +lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
   1.145  by (simp add: linorder_not_less)
   1.146  
   1.147 -lemma negative_eq_positive [simp]: "((- of_nat n \<Colon> int) = of_nat m) = (n = 0 & m = 0)"
   1.148 +lemma negative_eq_positive [simp]: "(- int n = of_nat m) = (n = 0 & m = 0)"
   1.149  by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
   1.150  
   1.151 -lemma zle_iff_zadd: "(w\<Colon>int) \<le> z \<longleftrightarrow> (\<exists>n. z = w + of_nat n)"
   1.152 +lemma zle_iff_zadd: "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)"
   1.153  proof -
   1.154    have "(w \<le> z) = (0 \<le> z - w)"
   1.155      by (simp only: le_diff_eq add_0_left)
   1.156 @@ -526,10 +529,10 @@
   1.157    finally show ?thesis .
   1.158  qed
   1.159  
   1.160 -lemma zadd_int_left: "of_nat m + (of_nat n + z) = of_nat (m + n) + (z\<Colon>int)"
   1.161 +lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z"
   1.162  by simp
   1.163  
   1.164 -lemma int_Suc0_eq_1: "of_nat (Suc 0) = (1\<Colon>int)"
   1.165 +lemma int_Suc0_eq_1: "int (Suc 0) = 1"
   1.166  by simp
   1.167  
   1.168  text{*This version is proved for all ordered rings, not just integers!
   1.169 @@ -540,7 +543,7 @@
   1.170       "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
   1.171  by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
   1.172  
   1.173 -lemma negD: "(x \<Colon> int) < 0 \<Longrightarrow> \<exists>n. x = - (of_nat (Suc n))"
   1.174 +lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x = - (int (Suc n))"
   1.175  apply (cases x)
   1.176  apply (auto simp add: le minus Zero_int_def int_def order_less_le)
   1.177  apply (rule_tac x="y - Suc x" in exI, arith)
   1.178 @@ -553,7 +556,7 @@
   1.179  whether an integer is negative or not.*}
   1.180  
   1.181  theorem int_cases [case_names nonneg neg, cases type: int]:
   1.182 -  "[|!! n. (z \<Colon> int) = of_nat n ==> P;  !! n. z =  - (of_nat (Suc n)) ==> P |] ==> P"
   1.183 +  "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
   1.184  apply (cases "z < 0")
   1.185  apply (blast dest!: negD)
   1.186  apply (simp add: linorder_not_less del: of_nat_Suc)
   1.187 @@ -562,12 +565,12 @@
   1.188  done
   1.189  
   1.190  theorem int_of_nat_induct [case_names nonneg neg, induct type: int]:
   1.191 -     "[|!! n. P (of_nat n \<Colon> int);  !!n. P (- (of_nat (Suc n))) |] ==> P z"
   1.192 +     "[|!! n. P (int n);  !!n. P (- (int (Suc n))) |] ==> P z"
   1.193    by (cases z) auto
   1.194  
   1.195  text{*Contributed by Brian Huffman*}
   1.196  theorem int_diff_cases:
   1.197 -  obtains (diff) m n where "(z\<Colon>int) = of_nat m - of_nat n"
   1.198 +  obtains (diff) m n where "z = int m - int n"
   1.199  apply (cases z rule: eq_Abs_Integ)
   1.200  apply (rule_tac m=x and n=y in diff)
   1.201  apply (simp add: int_def minus add diff_minus)
   1.202 @@ -944,11 +947,11 @@
   1.203    assumes number_of_eq: "number_of k = of_int k"
   1.204  
   1.205  class number_semiring = number + comm_semiring_1 +
   1.206 -  assumes number_of_int: "number_of (of_nat n) = of_nat n"
   1.207 +  assumes number_of_int: "number_of (int n) = of_nat n"
   1.208  
   1.209  instance number_ring \<subseteq> number_semiring
   1.210  proof
   1.211 -  fix n show "number_of (of_nat n) = (of_nat n :: 'a)"
   1.212 +  fix n show "number_of (int n) = (of_nat n :: 'a)"
   1.213      unfolding number_of_eq by (rule of_int_of_nat_eq)
   1.214  qed
   1.215  
   1.216 @@ -1124,7 +1127,7 @@
   1.217    show ?thesis
   1.218    proof
   1.219      assume eq: "1 + z + z = 0"
   1.220 -    have "(0::int) < 1 + (of_nat n + of_nat n)"
   1.221 +    have "(0::int) < 1 + (int n + int n)"
   1.222        by (simp add: le_imp_0_less add_increasing) 
   1.223      also have "... = - (1 + z + z)" 
   1.224        by (simp add: neg add_assoc [symmetric]) 
   1.225 @@ -1644,7 +1647,7 @@
   1.226  lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard]
   1.227  
   1.228  lemma split_nat [arith_split]:
   1.229 -  "P(nat(i::int)) = ((\<forall>n. i = of_nat n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
   1.230 +  "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
   1.231    (is "?P = (?L & ?R)")
   1.232  proof (cases "i < 0")
   1.233    case True thus ?thesis by auto
   1.234 @@ -1737,11 +1740,6 @@
   1.235      by (rule wf_subset [OF wf_measure]) 
   1.236  qed
   1.237  
   1.238 -abbreviation
   1.239 -  int :: "nat \<Rightarrow> int"
   1.240 -where
   1.241 -  "int \<equiv> of_nat"
   1.242 -
   1.243  (* `set:int': dummy construction *)
   1.244  theorem int_ge_induct [case_names base step, induct set: int]:
   1.245    fixes i :: int