src/HOL/Int.thy
 changeset 60162 645058aa9d6f parent 59667 651ea265d568 child 60570 7ed2cde6806d
```     1.1 --- a/src/HOL/Int.thy	Wed Apr 29 14:04:22 2015 +0100
1.2 +++ b/src/HOL/Int.thy	Thu Apr 30 15:28:01 2015 +0100
1.3 @@ -3,7 +3,7 @@
1.4      Author:     Tobias Nipkow, Florian Haftmann, TU Muenchen
1.5  *)
1.6
1.7 -section {* The Integers as Equivalence Classes over Pairs of Natural Numbers *}
1.8 +section {* The Integers as Equivalence Classes over Pairs of Natural Numbers *}
1.9
1.10  theory Int
1.11  imports Equiv_Relations Power Quotient Fun_Def
1.12 @@ -338,10 +338,10 @@
1.13
1.14  text{*An alternative condition is @{term "0 \<le> w"} *}
1.15  corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
1.16 -by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
1.17 +by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
1.18
1.19  corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
1.20 -by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
1.21 +by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
1.22
1.23  lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
1.24    by transfer (clarsimp, arith)
1.25 @@ -355,7 +355,7 @@
1.26  lemma nat_eq_iff:
1.27    "nat w = m \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)"
1.29 -
1.30 +
1.31  corollary nat_eq_iff2:
1.32    "m = nat w \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)"
1.33    using nat_eq_iff [of w m] by auto
1.34 @@ -378,7 +378,7 @@
1.35
1.36  lemma nat_2: "nat 2 = Suc (Suc 0)"
1.37    by simp
1.38 -
1.39 +
1.40  lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
1.41    by transfer (clarsimp, arith)
1.42
1.43 @@ -404,7 +404,7 @@
1.44  lemma nat_diff_distrib':
1.45    "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> nat (x - y) = nat x - nat y"
1.46    by transfer clarsimp
1.47 -
1.48 +
1.49  lemma nat_diff_distrib:
1.50    "0 \<le> z' \<Longrightarrow> z' \<le> z \<Longrightarrow> nat (z - z') = nat z - nat z'"
1.51    by (rule nat_diff_distrib') auto
1.52 @@ -415,7 +415,7 @@
1.53  lemma le_nat_iff:
1.54    "k \<ge> 0 \<Longrightarrow> n \<le> nat k \<longleftrightarrow> int n \<le> k"
1.55    by transfer auto
1.56 -
1.57 +
1.58  lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
1.59    by transfer (clarsimp simp add: less_diff_conv)
1.60
1.61 @@ -427,7 +427,7 @@
1.62
1.63  end
1.64
1.65 -lemma diff_nat_numeral [simp]:
1.66 +lemma diff_nat_numeral [simp]:
1.67    "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
1.68    by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
1.69
1.70 @@ -550,7 +550,7 @@
1.71
1.72  text {* Preliminaries *}
1.73
1.74 -lemma le_imp_0_less:
1.75 +lemma le_imp_0_less:
1.76    assumes le: "0 \<le> z"
1.77    shows "(0::int) < 1 + z"
1.78  proof -
1.79 @@ -565,7 +565,7 @@
1.80  proof (cases z)
1.81    case (nonneg n)
1.83 -                             le_imp_0_less [THEN order_less_imp_le])
1.84 +                             le_imp_0_less [THEN order_less_imp_le])
1.85  next
1.86    case (neg n)
1.87    thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
1.88 @@ -580,19 +580,19 @@
1.89    "1 + z + z \<noteq> (0::int)"
1.90  proof (cases z)
1.91    case (nonneg n)
1.92 -  have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
1.93 +  have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
1.94    thus ?thesis using  le_imp_0_less [OF le]
1.97  next
1.98    case (neg n)
1.99    show ?thesis
1.100    proof
1.101      assume eq: "1 + z + z = 0"
1.102      have "(0::int) < 1 + (int n + int n)"
1.104 -    also have "... = - (1 + z + z)"
1.106 -    also have "... = 0" by (simp add: eq)
1.108 +    also have "... = - (1 + z + z)"
1.110 +    also have "... = 0" by (simp add: eq)
1.111      finally have "0<0" ..
1.112      thus False by blast
1.113    qed
1.114 @@ -699,12 +699,12 @@
1.115      hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
1.116      with odd_nonzero show False by blast
1.117    qed
1.118 -qed
1.119 +qed
1.120
1.121  lemma Nats_numeral [simp]: "numeral w \<in> Nats"
1.122    using of_nat_in_Nats [of "numeral w"] by simp
1.123
1.124 -lemma Ints_odd_less_0:
1.125 +lemma Ints_odd_less_0:
1.126    assumes in_Ints: "a \<in> Ints"
1.127    shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))"
1.128  proof -
1.129 @@ -787,9 +787,7 @@
1.130  text{*Simplify the term @{term "w + - z"}*}
1.131
1.132  lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
1.133 -apply (insert zless_nat_conj [of 1 z])
1.134 -apply auto
1.135 -done
1.136 +  using zless_nat_conj [of 1 z] by auto
1.137
1.138  text{*This simplifies expressions of the form @{term "int n = z"} where
1.139        z is an integer literal.*}
1.140 @@ -857,7 +855,7 @@
1.141
1.142  lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
1.143  apply (cases "z=0 | w=0")
1.144 -apply (auto simp add: abs_if nat_mult_distrib [symmetric]
1.145 +apply (auto simp add: abs_if nat_mult_distrib [symmetric]
1.146                        nat_mult_distrib_neg [symmetric] mult_less_0_iff)
1.147  done
1.148
1.149 @@ -867,9 +865,9 @@
1.150  done
1.151
1.152  lemma diff_nat_eq_if:
1.153 -     "nat z - nat z' =
1.154 -        (if z' < 0 then nat z
1.155 -         else let d = z-z' in
1.156 +     "nat z - nat z' =
1.157 +        (if z' < 0 then nat z
1.158 +         else let d = z-z' in
1.159                if d < 0 then 0 else nat d)"
1.160  by (simp add: Let_def nat_diff_distrib [symmetric])
1.161
1.162 @@ -891,8 +889,8 @@
1.163  proof -
1.164    have "int_ge_less_than d \<subseteq> measure (%z. nat (z-d))"
1.165      by (auto simp add: int_ge_less_than_def)
1.166 -  thus ?thesis
1.167 -    by (rule wf_subset [OF wf_measure])
1.168 +  thus ?thesis
1.169 +    by (rule wf_subset [OF wf_measure])
1.170  qed
1.171
1.172  text{*This variant looks odd, but is typical of the relations suggested
1.173 @@ -905,10 +903,10 @@
1.174
1.175  theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
1.176  proof -
1.177 -  have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))"
1.178 +  have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))"
1.179      by (auto simp add: int_ge_less_than2_def)
1.180 -  thus ?thesis
1.181 -    by (rule wf_subset [OF wf_measure])
1.182 +  thus ?thesis
1.183 +    by (rule wf_subset [OF wf_measure])
1.184  qed
1.185
1.186  (* `set:int': dummy construction *)
1.187 @@ -1009,7 +1007,7 @@
1.188  subsection{*Intermediate value theorems*}
1.189
1.190  lemma int_val_lemma:
1.191 -     "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->
1.192 +     "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->
1.193        f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
1.194  unfolding One_nat_def
1.195  apply (induct n)
1.196 @@ -1027,9 +1025,9 @@
1.197  lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
1.198
1.199  lemma nat_intermed_int_val:
1.200 -     "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;
1.201 +     "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;
1.202           f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
1.203 -apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
1.204 +apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
1.205         in int_val_lemma)
1.206  unfolding One_nat_def
1.207  apply simp
1.208 @@ -1053,8 +1051,8 @@
1.209    proof
1.210      assume "2 \<le> \<bar>m\<bar>"
1.211      hence "2*\<bar>n\<bar> \<le> \<bar>m\<bar>*\<bar>n\<bar>"
1.212 -      by (simp add: mult_mono 0)
1.213 -    also have "... = \<bar>m*n\<bar>"
1.214 +      by (simp add: mult_mono 0)
1.215 +    also have "... = \<bar>m*n\<bar>"
1.217      also have "... = 1"
1.219 @@ -1077,10 +1075,10 @@
1.220  qed
1.221
1.222  lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
1.223 -apply (rule iffI)
1.224 +apply (rule iffI)
1.225   apply (frule pos_zmult_eq_1_iff_lemma)
1.226 - apply (simp add: mult.commute [of m])
1.227 - apply (frule pos_zmult_eq_1_iff_lemma, auto)
1.228 + apply (simp add: mult.commute [of m])
1.229 + apply (frule pos_zmult_eq_1_iff_lemma, auto)
1.230  done
1.231
1.232  lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)"
1.233 @@ -1226,14 +1224,14 @@
1.234    apply (auto simp add: mult.assoc zero_le_mult_iff zmult_eq_1_iff)
1.235    done
1.236
1.237 -lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a"
1.238 +lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a"
1.239    shows "\<bar>a\<bar> = \<bar>b\<bar>"
1.240  proof cases
1.241    assume "a = 0" with assms show ?thesis by simp
1.242  next
1.243    assume "a \<noteq> 0"
1.244 -  from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast
1.245 -  from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast
1.246 +  from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast
1.247 +  from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast
1.248    from k k' have "a = a*k*k'" by simp
1.249    with mult_cancel_left1[where c="a" and b="k*k'"]
1.250    have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult.assoc)
1.251 @@ -1242,7 +1240,7 @@
1.252  qed
1.253
1.254  lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
1.255 -  using dvd_add_right_iff [of k "- n" m] by simp
1.256 +  using dvd_add_right_iff [of k "- n" m] by simp
1.257
1.258  lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
1.260 @@ -1317,10 +1315,10 @@
1.261    then show "x dvd 1" by (auto intro: dvdI)
1.262  qed
1.263
1.264 -lemma zdvd_mult_cancel1:
1.265 +lemma zdvd_mult_cancel1:
1.266    assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
1.267  proof
1.268 -  assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m"
1.269 +  assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m"
1.270      by (cases "n >0") (auto simp add: minus_equation_iff)
1.271  next
1.272    assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
```