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.28    by transfer (clarsimp simp add: le_imp_diff_is_add)
    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.82    thus ?thesis by (simp add: linorder_not_less add.assoc add_increasing
    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.95 -    by (auto simp add: add.assoc) 
    1.96 +    by (auto simp add: add.assoc)
    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.103 -      by (simp add: le_imp_0_less add_increasing) 
   1.104 -    also have "... = - (1 + z + z)" 
   1.105 -      by (simp add: neg add.assoc [symmetric]) 
   1.106 -    also have "... = 0" by (simp add: eq) 
   1.107 +      by (simp add: le_imp_0_less add_increasing)
   1.108 +    also have "... = - (1 + z + z)"
   1.109 +      by (simp add: neg add.assoc [symmetric])
   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.216        by (simp add: abs_mult)
   1.217      also have "... = 1"
   1.218        by (simp add: mn)
   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.259    using dvd_add_times_triv_right_iff [of k n m] by (simp add: ac_simps)
   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