src/HOL/Divides.thy
changeset 60562 24af00b010cf
parent 60517 f16e4fb20652
child 60685 cb21b7022b00
     1.1 --- a/src/HOL/Divides.thy	Mon Jun 22 23:19:48 2015 +0200
     1.2 +++ b/src/HOL/Divides.thy	Tue Jun 23 16:55:28 2015 +0100
     1.3 @@ -92,7 +92,7 @@
     1.4    then show ?thesis by simp
     1.5  qed
     1.6  
     1.7 -lemma mod_mult_self2 [simp]: 
     1.8 +lemma mod_mult_self2 [simp]:
     1.9    "(a + b * c) mod b = a mod b"
    1.10    by (simp add: mult.commute [of b])
    1.11  
    1.12 @@ -365,9 +365,9 @@
    1.13    have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
    1.14    with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
    1.15      = c * a + c * (a mod b)" by (simp add: algebra_simps)
    1.16 -  with mod_div_equality show ?thesis by simp 
    1.17 +  with mod_div_equality show ?thesis by simp
    1.18  qed
    1.19 -  
    1.20 +
    1.21  lemma mod_mult_mult2:
    1.22    "(a * c) mod (b * c) = (a mod b) * c"
    1.23    using mod_mult_mult1 [of c a b] by (simp add: mult.commute)
    1.24 @@ -406,7 +406,7 @@
    1.25  done
    1.26  
    1.27  lemma dvd_div_eq_mult:
    1.28 -  assumes "a \<noteq> 0" and "a dvd b"  
    1.29 +  assumes "a \<noteq> 0" and "a dvd b"
    1.30    shows "b div a = c \<longleftrightarrow> b = c * a"
    1.31  proof
    1.32    assume "b = c * a"
    1.33 @@ -417,7 +417,7 @@
    1.34    moreover from `a dvd b` have "b div a * a = b" by simp
    1.35    ultimately show "b = c * a" by simp
    1.36  qed
    1.37 -   
    1.38 +
    1.39  lemma dvd_div_div_eq_mult:
    1.40    assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"
    1.41    shows "b div a = d div c \<longleftrightarrow> b * c = a * d"
    1.42 @@ -515,11 +515,11 @@
    1.43  lemma mod_minus1_right [simp]: "a mod (-1) = 0"
    1.44    using mod_minus_right [of a 1] by simp
    1.45  
    1.46 -lemma minus_mod_self2 [simp]: 
    1.47 +lemma minus_mod_self2 [simp]:
    1.48    "(a - b) mod b = a mod b"
    1.49    by (simp add: mod_diff_right_eq)
    1.50  
    1.51 -lemma minus_mod_self1 [simp]: 
    1.52 +lemma minus_mod_self1 [simp]:
    1.53    "(b - a) mod b = - a mod b"
    1.54    using mod_add_self2 [of "- a" b] by simp
    1.55  
    1.56 @@ -528,7 +528,7 @@
    1.57  
    1.58  subsubsection {* Parity and division *}
    1.59  
    1.60 -class semiring_div_parity = semiring_div + comm_semiring_1_diff_distrib + numeral + 
    1.61 +class semiring_div_parity = semiring_div + comm_semiring_1_cancel + numeral +
    1.62    assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
    1.63    assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
    1.64    assumes zero_not_eq_two: "0 \<noteq> 2"
    1.65 @@ -618,8 +618,7 @@
    1.66    and less technical class hierarchy.
    1.67  *}
    1.68  
    1.69 -class semiring_numeral_div = semiring_div + comm_semiring_1_diff_distrib + linordered_semidom +
    1.70 -  assumes le_add_diff_inverse2: "b \<le> a \<Longrightarrow> a - b + b = a"
    1.71 +class semiring_numeral_div = semiring_div + comm_semiring_1_cancel + linordered_semidom +
    1.72    assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
    1.73      and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
    1.74      and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
    1.75 @@ -794,7 +793,7 @@
    1.76    then have "divmod m n =
    1.77      divmod_step n (numeral m div numeral (Num.Bit0 n),
    1.78        numeral m mod numeral (Num.Bit0 n))"
    1.79 -    by (simp only: numeral.simps distrib mult_1) 
    1.80 +    by (simp only: numeral.simps distrib mult_1)
    1.81    then have "divmod m n = divmod_step n (divmod m (Num.Bit0 n))"
    1.82      by (simp add: divmod_def)
    1.83    with False show ?thesis by simp
    1.84 @@ -834,10 +833,7 @@
    1.85  
    1.86  end
    1.87  
    1.88 -hide_fact (open) le_add_diff_inverse2
    1.89 -  -- {* restore simple accesses for more general variants of theorems *}
    1.90 -
    1.91 -  
    1.92 +
    1.93  subsection {* Division on @{typ nat} *}
    1.94  
    1.95  text {*
    1.96 @@ -927,7 +923,7 @@
    1.97  qed
    1.98  
    1.99  lemma divmod_nat_unique:
   1.100 -  assumes "divmod_nat_rel m n qr" 
   1.101 +  assumes "divmod_nat_rel m n qr"
   1.102    shows "divmod_nat m n = qr"
   1.103    using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
   1.104  
   1.105 @@ -953,12 +949,12 @@
   1.106    by (simp add: prod_eq_iff)
   1.107  
   1.108  lemma div_nat_unique:
   1.109 -  assumes "divmod_nat_rel m n (q, r)" 
   1.110 +  assumes "divmod_nat_rel m n (q, r)"
   1.111    shows "m div n = q"
   1.112    using assms by (auto dest!: divmod_nat_unique simp add: prod_eq_iff)
   1.113  
   1.114  lemma mod_nat_unique:
   1.115 -  assumes "divmod_nat_rel m n (q, r)" 
   1.116 +  assumes "divmod_nat_rel m n (q, r)"
   1.117    shows "m mod n = r"
   1.118    using assms by (auto dest!: divmod_nat_unique simp add: prod_eq_iff)
   1.119  
   1.120 @@ -1168,7 +1164,7 @@
   1.121    assumes "divmod_nat_rel a b (q, r)"
   1.122    shows "divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
   1.123  proof -
   1.124 -  { assume "r < b" and "0 < c" 
   1.125 +  { assume "r < b" and "0 < c"
   1.126      then have "b * (q mod c) + r < b * c"
   1.127        apply (cut_tac m = q and n = c in mod_less_divisor)
   1.128        apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
   1.129 @@ -1180,7 +1176,7 @@
   1.130    } with assms show ?thesis
   1.131      by (auto simp add: divmod_nat_rel_def algebra_simps add_mult_distrib2 [symmetric])
   1.132  qed
   1.133 -    
   1.134 +
   1.135  lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
   1.136  by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
   1.137  
   1.138 @@ -1523,7 +1519,7 @@
   1.139  lemmas Suc_div_eq_add3_div_numeral [simp] = Suc_div_eq_add3_div [of _ "numeral v"] for v
   1.140  lemmas Suc_mod_eq_add3_mod_numeral [simp] = Suc_mod_eq_add3_mod [of _ "numeral v"] for v
   1.141  
   1.142 -lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" 
   1.143 +lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1"
   1.144  apply (induct "m")
   1.145  apply (simp_all add: mod_Suc)
   1.146  done
   1.147 @@ -1539,30 +1535,30 @@
   1.148  lemma div_2_gt_zero [simp]: assumes A: "(1::nat) < n" shows "0 < n div 2"
   1.149  proof -
   1.150    from A have B: "0 < n - 1" and C: "n - 1 + 1 = n" by simp_all
   1.151 -  from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp 
   1.152 +  from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp
   1.153  qed
   1.154  
   1.155  lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n"
   1.156  proof -
   1.157    have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp
   1.158 -  also have "... = Suc m mod n" by (rule mod_mult_self3) 
   1.159 +  also have "... = Suc m mod n" by (rule mod_mult_self3)
   1.160    finally show ?thesis .
   1.161  qed
   1.162  
   1.163  lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
   1.164 -apply (subst mod_Suc [of m]) 
   1.165 -apply (subst mod_Suc [of "m mod n"], simp) 
   1.166 +apply (subst mod_Suc [of m])
   1.167 +apply (subst mod_Suc [of "m mod n"], simp)
   1.168  done
   1.169  
   1.170  lemma mod_2_not_eq_zero_eq_one_nat:
   1.171    fixes n :: nat
   1.172    shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
   1.173    by (fact not_mod_2_eq_0_eq_1)
   1.174 -  
   1.175 +
   1.176  lemma even_Suc_div_two [simp]:
   1.177    "even n \<Longrightarrow> Suc n div 2 = n div 2"
   1.178    using even_succ_div_two [of n] by simp
   1.179 -  
   1.180 +
   1.181  lemma odd_Suc_div_two [simp]:
   1.182    "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
   1.183    using odd_succ_div_two [of n] by simp
   1.184 @@ -1603,7 +1599,7 @@
   1.185          by simp
   1.186      next
   1.187        case False
   1.188 -      with hyp odd [of "n div 2"] show ?thesis 
   1.189 +      with hyp odd [of "n div 2"] show ?thesis
   1.190          by simp
   1.191      qed
   1.192    qed
   1.193 @@ -1650,12 +1646,12 @@
   1.194  
   1.195  definition divmod_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
   1.196      --{*The full division algorithm considers all possible signs for a, b
   1.197 -       including the special case @{text "a=0, b<0"} because 
   1.198 +       including the special case @{text "a=0, b<0"} because
   1.199         @{term negDivAlg} requires @{term "a<0"}.*}
   1.200    "divmod_int a b = (if 0 \<le> a then if 0 \<le> b then posDivAlg a b
   1.201                    else if a = 0 then (0, 0)
   1.202                         else apsnd uminus (negDivAlg (-a) (-b))
   1.203 -               else 
   1.204 +               else
   1.205                    if 0 < b then negDivAlg a b
   1.206                    else apsnd uminus (posDivAlg (-a) (-b)))"
   1.207  
   1.208 @@ -1698,11 +1694,11 @@
   1.209  
   1.210      fun negateSnd (q,r:int) = (q,~r);
   1.211  
   1.212 -    fun divmod (a,b) = if 0\<le>a then 
   1.213 -                          if b>0 then posDivAlg (a,b) 
   1.214 +    fun divmod (a,b) = if 0\<le>a then
   1.215 +                          if b>0 then posDivAlg (a,b)
   1.216                             else if a=0 then (0,0)
   1.217                                  else negateSnd (negDivAlg (~a,~b))
   1.218 -                       else 
   1.219 +                       else
   1.220                            if 0<b then negDivAlg (a,b)
   1.221                            else        negateSnd (posDivAlg (~a,~b));
   1.222  \end{verbatim}
   1.223 @@ -1712,7 +1708,7 @@
   1.224  subsubsection {* Uniqueness and Monotonicity of Quotients and Remainders *}
   1.225  
   1.226  lemma unique_quotient_lemma:
   1.227 -     "[| b*q' + r'  \<le> b*q + r;  0 \<le> r';  r' < b;  r < b |]  
   1.228 +     "[| b*q' + r'  \<le> b*q + r;  0 \<le> r';  r' < b;  r < b |]
   1.229        ==> q' \<le> (q::int)"
   1.230  apply (subgoal_tac "r' + b * (q'-q) \<le> r")
   1.231   prefer 2 apply (simp add: right_diff_distrib)
   1.232 @@ -1725,23 +1721,23 @@
   1.233  done
   1.234  
   1.235  lemma unique_quotient_lemma_neg:
   1.236 -     "[| b*q' + r' \<le> b*q + r;  r \<le> 0;  b < r;  b < r' |]  
   1.237 +     "[| b*q' + r' \<le> b*q + r;  r \<le> 0;  b < r;  b < r' |]
   1.238        ==> q \<le> (q'::int)"
   1.239 -by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma, 
   1.240 +by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma,
   1.241      auto)
   1.242  
   1.243  lemma unique_quotient:
   1.244 -     "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r') |]  
   1.245 +     "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r') |]
   1.246        ==> q = q'"
   1.247  apply (simp add: divmod_int_rel_def linorder_neq_iff split: split_if_asm)
   1.248  apply (blast intro: order_antisym
   1.249 -             dest: order_eq_refl [THEN unique_quotient_lemma] 
   1.250 +             dest: order_eq_refl [THEN unique_quotient_lemma]
   1.251               order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
   1.252  done
   1.253  
   1.254  
   1.255  lemma unique_remainder:
   1.256 -     "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r') |]  
   1.257 +     "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r') |]
   1.258        ==> r = r'"
   1.259  apply (subgoal_tac "q = q'")
   1.260   apply (simp add: divmod_int_rel_def)
   1.261 @@ -1754,9 +1750,9 @@
   1.262  text{*And positive divisors*}
   1.263  
   1.264  lemma adjust_eq [simp]:
   1.265 -     "adjust b (q, r) = 
   1.266 -      (let diff = r - b in  
   1.267 -        if 0 \<le> diff then (2 * q + 1, diff)   
   1.268 +     "adjust b (q, r) =
   1.269 +      (let diff = r - b in
   1.270 +        if 0 \<le> diff then (2 * q + 1, diff)
   1.271                       else (2*q, r))"
   1.272    by (simp add: Let_def adjust_def)
   1.273  
   1.274 @@ -1764,7 +1760,7 @@
   1.275  
   1.276  text{*use with a simproc to avoid repeatedly proving the premise*}
   1.277  lemma posDivAlg_eqn:
   1.278 -     "0 < b ==>  
   1.279 +     "0 < b ==>
   1.280        posDivAlg a b = (if a<b then (0,a) else adjust b (posDivAlg a (2*b)))"
   1.281  by (rule posDivAlg.simps [THEN trans], simp)
   1.282  
   1.283 @@ -1792,8 +1788,8 @@
   1.284  
   1.285  text{*use with a simproc to avoid repeatedly proving the premise*}
   1.286  lemma negDivAlg_eqn:
   1.287 -     "0 < b ==>  
   1.288 -      negDivAlg a b =       
   1.289 +     "0 < b ==>
   1.290 +      negDivAlg a b =
   1.291         (if 0\<le>a+b then (-1,a+b) else adjust b (negDivAlg a (2*b)))"
   1.292  by (rule negDivAlg.simps [THEN trans], simp)
   1.293  
   1.294 @@ -1838,7 +1834,7 @@
   1.295                      posDivAlg_correct negDivAlg_correct)
   1.296  
   1.297  lemma divmod_int_unique:
   1.298 -  assumes "divmod_int_rel a b qr" 
   1.299 +  assumes "divmod_int_rel a b qr"
   1.300    shows "divmod_int a b = qr"
   1.301    using assms divmod_int_correct [of a b]
   1.302    using unique_quotient [of a b] unique_remainder [of a b]
   1.303 @@ -1912,7 +1908,7 @@
   1.304  
   1.305    val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
   1.306  
   1.307 -  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac 
   1.308 +  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
   1.309      (@{thm diff_conv_add_uminus} :: @{thms add_0_left add_0_right} @ @{thms ac_simps}))
   1.310  )
   1.311  *}
   1.312 @@ -1975,14 +1971,14 @@
   1.313  
   1.314  lemma zminus1_lemma:
   1.315       "divmod_int_rel a b (q, r) ==> b \<noteq> 0
   1.316 -      ==> divmod_int_rel (-a) b (if r=0 then -q else -q - 1,  
   1.317 +      ==> divmod_int_rel (-a) b (if r=0 then -q else -q - 1,
   1.318                            if r=0 then 0 else b-r)"
   1.319  by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_diff_distrib)
   1.320  
   1.321  
   1.322  lemma zdiv_zminus1_eq_if:
   1.323 -     "b \<noteq> (0::int)  
   1.324 -      ==> (-a) div b =  
   1.325 +     "b \<noteq> (0::int)
   1.326 +      ==> (-a) div b =
   1.327            (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
   1.328  by (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN div_int_unique])
   1.329  
   1.330 @@ -1998,8 +1994,8 @@
   1.331    unfolding zmod_zminus1_eq_if by auto
   1.332  
   1.333  lemma zdiv_zminus2_eq_if:
   1.334 -     "b \<noteq> (0::int)  
   1.335 -      ==> a div (-b) =  
   1.336 +     "b \<noteq> (0::int)
   1.337 +      ==> a div (-b) =
   1.338            (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
   1.339  by (simp add: zdiv_zminus1_eq_if div_minus_right)
   1.340  
   1.341 @@ -2010,7 +2006,7 @@
   1.342  lemma zmod_zminus2_not_zero:
   1.343    fixes k l :: int
   1.344    shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
   1.345 -  unfolding zmod_zminus2_eq_if by auto 
   1.346 +  unfolding zmod_zminus2_eq_if by auto
   1.347  
   1.348  
   1.349  subsubsection {* Computation of Division and Remainder *}
   1.350 @@ -2185,10 +2181,10 @@
   1.351  done
   1.352  
   1.353  lemma zdiv_mono2_lemma:
   1.354 -     "[| b*q + r = b'*q' + r';  0 \<le> b'*q' + r';   
   1.355 -         r' < b';  0 \<le> r;  0 < b';  b' \<le> b |]   
   1.356 +     "[| b*q + r = b'*q' + r';  0 \<le> b'*q' + r';
   1.357 +         r' < b';  0 \<le> r;  0 < b';  b' \<le> b |]
   1.358        ==> q \<le> (q'::int)"
   1.359 -apply (frule q_pos_lemma, assumption+) 
   1.360 +apply (frule q_pos_lemma, assumption+)
   1.361  apply (subgoal_tac "b*q < b* (q' + 1) ")
   1.362   apply (simp add: mult_less_cancel_left)
   1.363  apply (subgoal_tac "b*q = r' - r + b'*q'")
   1.364 @@ -2216,10 +2212,10 @@
   1.365  done
   1.366  
   1.367  lemma zdiv_mono2_neg_lemma:
   1.368 -     "[| b*q + r = b'*q' + r';  b'*q' + r' < 0;   
   1.369 -         r < b;  0 \<le> r';  0 < b';  b' \<le> b |]   
   1.370 +     "[| b*q + r = b'*q' + r';  b'*q' + r' < 0;
   1.371 +         r < b;  0 \<le> r';  0 < b';  b' \<le> b |]
   1.372        ==> q' \<le> (q::int)"
   1.373 -apply (frule q_neg_lemma, assumption+) 
   1.374 +apply (frule q_neg_lemma, assumption+)
   1.375  apply (subgoal_tac "b*q' < b* (q + 1) ")
   1.376   apply (simp add: mult_less_cancel_left)
   1.377  apply (simp add: distrib_left)
   1.378 @@ -2242,7 +2238,7 @@
   1.379  text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *}
   1.380  
   1.381  lemma zmult1_lemma:
   1.382 -     "[| divmod_int_rel b c (q, r) |]  
   1.383 +     "[| divmod_int_rel b c (q, r) |]
   1.384        ==> divmod_int_rel (a * b) c (a*q + a*r div c, a*r mod c)"
   1.385  by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left ac_simps)
   1.386  
   1.387 @@ -2254,7 +2250,7 @@
   1.388  text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
   1.389  
   1.390  lemma zadd1_lemma:
   1.391 -     "[| divmod_int_rel a c (aq, ar);  divmod_int_rel b c (bq, br) |]  
   1.392 +     "[| divmod_int_rel a c (aq, ar);  divmod_int_rel b c (bq, br) |]
   1.393        ==> divmod_int_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
   1.394  by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left)
   1.395  
   1.396 @@ -2346,10 +2342,10 @@
   1.397  apply simp
   1.398  done
   1.399  
   1.400 -lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); 0 < c |]  
   1.401 +lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); 0 < c |]
   1.402        ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
   1.403  by (auto simp add: mult.assoc divmod_int_rel_def linorder_neq_iff
   1.404 -                   zero_less_mult_iff distrib_left [symmetric] 
   1.405 +                   zero_less_mult_iff distrib_left [symmetric]
   1.406                     zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm)
   1.407  
   1.408  lemma zdiv_zmult2_eq:
   1.409 @@ -2392,15 +2388,15 @@
   1.410  text{*The proofs of the two lemmas below are essentially identical*}
   1.411  
   1.412  lemma split_pos_lemma:
   1.413 - "0<k ==> 
   1.414 + "0<k ==>
   1.415      P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
   1.416  apply (rule iffI, clarify)
   1.417 - apply (erule_tac P="P x y" for x y in rev_mp)  
   1.418 - apply (subst mod_add_eq) 
   1.419 - apply (subst zdiv_zadd1_eq) 
   1.420 - apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)  
   1.421 + apply (erule_tac P="P x y" for x y in rev_mp)
   1.422 + apply (subst mod_add_eq)
   1.423 + apply (subst zdiv_zadd1_eq)
   1.424 + apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)
   1.425  txt{*converse direction*}
   1.426 -apply (drule_tac x = "n div k" in spec) 
   1.427 +apply (drule_tac x = "n div k" in spec)
   1.428  apply (drule_tac x = "n mod k" in spec, simp)
   1.429  done
   1.430  
   1.431 @@ -2408,36 +2404,36 @@
   1.432   "k<0 ==>
   1.433      P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
   1.434  apply (rule iffI, clarify)
   1.435 - apply (erule_tac P="P x y" for x y in rev_mp)  
   1.436 - apply (subst mod_add_eq) 
   1.437 - apply (subst zdiv_zadd1_eq) 
   1.438 - apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)  
   1.439 + apply (erule_tac P="P x y" for x y in rev_mp)
   1.440 + apply (subst mod_add_eq)
   1.441 + apply (subst zdiv_zadd1_eq)
   1.442 + apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)
   1.443  txt{*converse direction*}
   1.444 -apply (drule_tac x = "n div k" in spec) 
   1.445 +apply (drule_tac x = "n div k" in spec)
   1.446  apply (drule_tac x = "n mod k" in spec, simp)
   1.447  done
   1.448  
   1.449  lemma split_zdiv:
   1.450   "P(n div k :: int) =
   1.451 -  ((k = 0 --> P 0) & 
   1.452 -   (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) & 
   1.453 +  ((k = 0 --> P 0) &
   1.454 +   (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) &
   1.455     (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))"
   1.456  apply (case_tac "k=0", simp)
   1.457  apply (simp only: linorder_neq_iff)
   1.458 -apply (erule disjE) 
   1.459 - apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"] 
   1.460 +apply (erule disjE)
   1.461 + apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"]
   1.462                        split_neg_lemma [of concl: "%x y. P x"])
   1.463  done
   1.464  
   1.465  lemma split_zmod:
   1.466   "P(n mod k :: int) =
   1.467 -  ((k = 0 --> P n) & 
   1.468 -   (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) & 
   1.469 +  ((k = 0 --> P n) &
   1.470 +   (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) &
   1.471     (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P j)))"
   1.472  apply (case_tac "k=0", simp)
   1.473  apply (simp only: linorder_neq_iff)
   1.474 -apply (erule disjE) 
   1.475 - apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"] 
   1.476 +apply (erule disjE)
   1.477 + apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"]
   1.478                        split_neg_lemma [of concl: "%x y. P y"])
   1.479  done
   1.480  
   1.481 @@ -2470,7 +2466,7 @@
   1.482    using pos_divmod_int_rel_mult_2 [OF _ divmod_int_rel_div_mod]
   1.483    by (rule div_int_unique)
   1.484  
   1.485 -lemma neg_zdiv_mult_2: 
   1.486 +lemma neg_zdiv_mult_2:
   1.487    assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
   1.488    using neg_divmod_int_rel_mult_2 [OF A divmod_int_rel_div_mod]
   1.489    by (rule div_int_unique)
   1.490 @@ -2483,7 +2479,7 @@
   1.491    by (rule div_mult_mult1, simp)
   1.492  
   1.493  lemma zdiv_numeral_Bit1 [simp]:
   1.494 -  "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =  
   1.495 +  "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =
   1.496      (numeral v div (numeral w :: int))"
   1.497    unfolding numeral.simps
   1.498    unfolding mult_2 [symmetric] add.commute [of _ 1]
   1.499 @@ -2505,7 +2501,7 @@
   1.500  
   1.501  (* FIXME: add rules for negative numerals *)
   1.502  lemma zmod_numeral_Bit0 [simp]:
   1.503 -  "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =  
   1.504 +  "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =
   1.505      (2::int) * (numeral v mod numeral w)"
   1.506    unfolding numeral_Bit0 [of v] numeral_Bit0 [of w]
   1.507    unfolding mult_2 [symmetric] by (rule mod_mult_mult1)
   1.508 @@ -2609,7 +2605,7 @@
   1.509      simp add: zmult_div_cancel
   1.510      pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial
   1.511      zmod_zmult2_eq zdiv_zmult2_eq)
   1.512 -  
   1.513 +
   1.514  lemma zdiv_int: "int (a div b) = (int a) div (int b)"
   1.515  apply (subst split_div, auto)
   1.516  apply (subst split_zdiv, auto)
   1.517 @@ -2620,7 +2616,7 @@
   1.518  lemma zmod_int: "int (a mod b) = (int a) mod (int b)"
   1.519  apply (subst split_mod, auto)
   1.520  apply (subst split_zmod, auto)
   1.521 -apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia 
   1.522 +apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia
   1.523         in unique_remainder)
   1.524  apply (auto simp add: divmod_int_rel_def of_nat_mult)
   1.525  done
   1.526 @@ -2718,7 +2714,7 @@
   1.527  proof
   1.528    assume H: "x mod n = y mod n"
   1.529    hence "x mod n - y mod n = 0" by simp
   1.530 -  hence "(x mod n - y mod n) mod n = 0" by simp 
   1.531 +  hence "(x mod n - y mod n) mod n = 0" by simp
   1.532    hence "(x - y) mod n = 0" by (simp add: mod_diff_eq[symmetric])
   1.533    thus "n dvd x - y" by (simp add: dvd_eq_mod_eq_0)
   1.534  next
   1.535 @@ -2732,27 +2728,27 @@
   1.536  lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y  mod n" and xy:"y \<le> x"
   1.537    shows "\<exists>q. x = y + n * q"
   1.538  proof-
   1.539 -  from xy have th: "int x - int y = int (x - y)" by simp 
   1.540 -  from xyn have "int x mod int n = int y mod int n" 
   1.541 +  from xy have th: "int x - int y = int (x - y)" by simp
   1.542 +  from xyn have "int x mod int n = int y mod int n"
   1.543      by (simp add: zmod_int [symmetric])
   1.544 -  hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric]) 
   1.545 +  hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric])
   1.546    hence "n dvd x - y" by (simp add: th zdvd_int)
   1.547    then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
   1.548  qed
   1.549  
   1.550 -lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)" 
   1.551 +lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"
   1.552    (is "?lhs = ?rhs")
   1.553  proof
   1.554    assume H: "x mod n = y mod n"
   1.555    {assume xy: "x \<le> y"
   1.556      from H have th: "y mod n = x mod n" by simp
   1.557 -    from nat_mod_eq_lemma[OF th xy] have ?rhs 
   1.558 +    from nat_mod_eq_lemma[OF th xy] have ?rhs
   1.559        apply clarify  apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}
   1.560    moreover
   1.561    {assume xy: "y \<le> x"
   1.562 -    from nat_mod_eq_lemma[OF H xy] have ?rhs 
   1.563 +    from nat_mod_eq_lemma[OF H xy] have ?rhs
   1.564        apply clarify  apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}
   1.565 -  ultimately  show ?rhs using linear[of x y] by blast  
   1.566 +  ultimately  show ?rhs using linear[of x y] by blast
   1.567  next
   1.568    assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast
   1.569    hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp
   1.570 @@ -2762,7 +2758,7 @@
   1.571  text {*
   1.572    This re-embedding of natural division on integers goes back to the
   1.573    time when numerals had been signed numerals.  It should
   1.574 -  now be replaced by the algorithm developed in @{class semiring_numeral_div}.  
   1.575 +  now be replaced by the algorithm developed in @{class semiring_numeral_div}.
   1.576  *}
   1.577  
   1.578  lemma div_nat_numeral [simp]: