src/HOL/Divides.thy
changeset 22718 936f7580937d
parent 22473 753123c89d72
child 22744 5cbe966d67a2
     1.1 --- a/src/HOL/Divides.thy	Mon Apr 16 16:11:03 2007 +0200
     1.2 +++ b/src/HOL/Divides.thy	Tue Apr 17 00:30:44 2007 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4  instance nat :: "Divides.div"
     1.5    mod_def: "m mod n == wfrec (pred_nat^+)
     1.6                            (%f j. if j<n | n=0 then j else f (j-n)) m"
     1.7 -  div_def:   "m div n == wfrec (pred_nat^+) 
     1.8 +  div_def:   "m div n == wfrec (pred_nat^+)
     1.9                            (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m" ..
    1.10  
    1.11  definition
    1.12 @@ -42,13 +42,11 @@
    1.13    dvd  :: "'a::times \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where
    1.14    dvd_def: "m dvd n \<longleftrightarrow> (\<exists>k. n = m*k)"
    1.15  
    1.16 -consts
    1.17 -  quorem :: "(nat*nat) * (nat*nat) => bool"
    1.18 -
    1.19 -defs
    1.20 +definition
    1.21 +  quorem :: "(nat*nat) * (nat*nat) => bool" where
    1.22    (*This definition helps prove the harder properties of div and mod.
    1.23      It is copied from IntDiv.thy; should it be overloaded?*)
    1.24 -  quorem_def: "quorem \<equiv> (%((a,b), (q,r)).
    1.25 +  "quorem = (%((a,b), (q,r)).
    1.26                      a = b*q + r &
    1.27                      (if 0<b then 0\<le>r & r<b else b<r & r \<le>0))"
    1.28  
    1.29 @@ -56,161 +54,150 @@
    1.30  
    1.31  subsection{*Initial Lemmas*}
    1.32  
    1.33 -lemmas wf_less_trans = 
    1.34 +lemmas wf_less_trans =
    1.35         def_wfrec [THEN trans, OF eq_reflection wf_pred_nat [THEN wf_trancl],
    1.36                    standard]
    1.37  
    1.38 -lemma mod_eq: "(%m. m mod n) = 
    1.39 +lemma mod_eq: "(%m. m mod n) =
    1.40                wfrec (pred_nat^+) (%f j. if j<n | n=0 then j else f (j-n))"
    1.41  by (simp add: mod_def)
    1.42  
    1.43 -lemma div_eq: "(%m. m div n) = wfrec (pred_nat^+)  
    1.44 +lemma div_eq: "(%m. m div n) = wfrec (pred_nat^+)
    1.45                 (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))"
    1.46  by (simp add: div_def)
    1.47  
    1.48  
    1.49 -(** Aribtrary definitions for division by zero.  Useful to simplify 
    1.50 +(** Aribtrary definitions for division by zero.  Useful to simplify
    1.51      certain equations **)
    1.52  
    1.53  lemma DIVISION_BY_ZERO_DIV [simp]: "a div 0 = (0::nat)"
    1.54 -by (rule div_eq [THEN wf_less_trans], simp)
    1.55 +  by (rule div_eq [THEN wf_less_trans], simp)
    1.56  
    1.57  lemma DIVISION_BY_ZERO_MOD [simp]: "a mod 0 = (a::nat)"
    1.58 -by (rule mod_eq [THEN wf_less_trans], simp)
    1.59 +  by (rule mod_eq [THEN wf_less_trans], simp)
    1.60  
    1.61  
    1.62  subsection{*Remainder*}
    1.63  
    1.64  lemma mod_less [simp]: "m<n ==> m mod n = (m::nat)"
    1.65 -by (rule mod_eq [THEN wf_less_trans], simp)
    1.66 +  by (rule mod_eq [THEN wf_less_trans]) simp
    1.67  
    1.68  lemma mod_geq: "~ m < (n::nat) ==> m mod n = (m-n) mod n"
    1.69 -apply (case_tac "n=0", simp) 
    1.70 -apply (rule mod_eq [THEN wf_less_trans])
    1.71 -apply (simp add: cut_apply less_eq)
    1.72 -done
    1.73 +  apply (cases "n=0")
    1.74 +   apply simp
    1.75 +  apply (rule mod_eq [THEN wf_less_trans])
    1.76 +  apply (simp add: cut_apply less_eq)
    1.77 +  done
    1.78  
    1.79  (*Avoids the ugly ~m<n above*)
    1.80  lemma le_mod_geq: "(n::nat) \<le> m ==> m mod n = (m-n) mod n"
    1.81 -by (simp add: mod_geq linorder_not_less)
    1.82 +  by (simp add: mod_geq linorder_not_less)
    1.83  
    1.84  lemma mod_if: "m mod (n::nat) = (if m<n then m else (m-n) mod n)"
    1.85 -by (simp add: mod_geq)
    1.86 +  by (simp add: mod_geq)
    1.87  
    1.88  lemma mod_1 [simp]: "m mod Suc 0 = 0"
    1.89 -apply (induct "m")
    1.90 -apply (simp_all (no_asm_simp) add: mod_geq)
    1.91 -done
    1.92 +  by (induct m) (simp_all add: mod_geq)
    1.93  
    1.94  lemma mod_self [simp]: "n mod n = (0::nat)"
    1.95 -apply (case_tac "n=0")
    1.96 -apply (simp_all add: mod_geq)
    1.97 -done
    1.98 +  by (cases "n = 0") (simp_all add: mod_geq)
    1.99  
   1.100  lemma mod_add_self2 [simp]: "(m+n) mod n = m mod (n::nat)"
   1.101 -apply (subgoal_tac "(n + m) mod n = (n+m-n) mod n") 
   1.102 -apply (simp add: add_commute)
   1.103 -apply (subst mod_geq [symmetric], simp_all)
   1.104 -done
   1.105 +  apply (subgoal_tac "(n + m) mod n = (n+m-n) mod n")
   1.106 +   apply (simp add: add_commute)
   1.107 +  apply (subst mod_geq [symmetric], simp_all)
   1.108 +  done
   1.109  
   1.110  lemma mod_add_self1 [simp]: "(n+m) mod n = m mod (n::nat)"
   1.111 -by (simp add: add_commute mod_add_self2)
   1.112 +  by (simp add: add_commute mod_add_self2)
   1.113  
   1.114  lemma mod_mult_self1 [simp]: "(m + k*n) mod n = m mod (n::nat)"
   1.115 -apply (induct "k")
   1.116 -apply (simp_all add: add_left_commute [of _ n])
   1.117 -done
   1.118 +  by (induct k) (simp_all add: add_left_commute [of _ n])
   1.119  
   1.120  lemma mod_mult_self2 [simp]: "(m + n*k) mod n = m mod (n::nat)"
   1.121 -by (simp add: mult_commute mod_mult_self1)
   1.122 +  by (simp add: mult_commute mod_mult_self1)
   1.123  
   1.124  lemma mod_mult_distrib: "(m mod n) * (k::nat) = (m*k) mod (n*k)"
   1.125 -apply (case_tac "n=0", simp)
   1.126 -apply (case_tac "k=0", simp)
   1.127 -apply (induct "m" rule: nat_less_induct)
   1.128 -apply (subst mod_if, simp)
   1.129 -apply (simp add: mod_geq diff_mult_distrib)
   1.130 -done
   1.131 +  apply (cases "n = 0", simp)
   1.132 +  apply (cases "k = 0", simp)
   1.133 +  apply (induct m rule: nat_less_induct)
   1.134 +  apply (subst mod_if, simp)
   1.135 +  apply (simp add: mod_geq diff_mult_distrib)
   1.136 +  done
   1.137  
   1.138  lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)"
   1.139 -by (simp add: mult_commute [of k] mod_mult_distrib)
   1.140 +  by (simp add: mult_commute [of k] mod_mult_distrib)
   1.141  
   1.142  lemma mod_mult_self_is_0 [simp]: "(m*n) mod n = (0::nat)"
   1.143 -apply (case_tac "n=0", simp)
   1.144 -apply (induct "m", simp)
   1.145 -apply (rename_tac "k")
   1.146 -apply (cut_tac m = "k*n" and n = n in mod_add_self2)
   1.147 -apply (simp add: add_commute)
   1.148 -done
   1.149 +  apply (cases "n = 0", simp)
   1.150 +  apply (induct m, simp)
   1.151 +  apply (rename_tac k)
   1.152 +  apply (cut_tac m = "k * n" and n = n in mod_add_self2)
   1.153 +  apply (simp add: add_commute)
   1.154 +  done
   1.155  
   1.156  lemma mod_mult_self1_is_0 [simp]: "(n*m) mod n = (0::nat)"
   1.157 -by (simp add: mult_commute mod_mult_self_is_0)
   1.158 +  by (simp add: mult_commute mod_mult_self_is_0)
   1.159  
   1.160  
   1.161  subsection{*Quotient*}
   1.162  
   1.163  lemma div_less [simp]: "m<n ==> m div n = (0::nat)"
   1.164 -by (rule div_eq [THEN wf_less_trans], simp)
   1.165 +  by (rule div_eq [THEN wf_less_trans], simp)
   1.166  
   1.167  lemma div_geq: "[| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)"
   1.168 -apply (rule div_eq [THEN wf_less_trans])
   1.169 -apply (simp add: cut_apply less_eq)
   1.170 -done
   1.171 +  apply (rule div_eq [THEN wf_less_trans])
   1.172 +  apply (simp add: cut_apply less_eq)
   1.173 +  done
   1.174  
   1.175  (*Avoids the ugly ~m<n above*)
   1.176  lemma le_div_geq: "[| 0<n;  n\<le>m |] ==> m div n = Suc((m-n) div n)"
   1.177 -by (simp add: div_geq linorder_not_less)
   1.178 +  by (simp add: div_geq linorder_not_less)
   1.179  
   1.180  lemma div_if: "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))"
   1.181 -by (simp add: div_geq)
   1.182 +  by (simp add: div_geq)
   1.183  
   1.184  
   1.185  (*Main Result about quotient and remainder.*)
   1.186  lemma mod_div_equality: "(m div n)*n + m mod n = (m::nat)"
   1.187 -apply (case_tac "n=0", simp)
   1.188 -apply (induct "m" rule: nat_less_induct)
   1.189 -apply (subst mod_if)
   1.190 -apply (simp_all (no_asm_simp) add: add_assoc div_geq add_diff_inverse)
   1.191 -done
   1.192 +  apply (cases "n = 0", simp)
   1.193 +  apply (induct m rule: nat_less_induct)
   1.194 +  apply (subst mod_if)
   1.195 +  apply (simp_all add: add_assoc div_geq add_diff_inverse)
   1.196 +  done
   1.197  
   1.198  lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"
   1.199 -apply(cut_tac m = m and n = n in mod_div_equality)
   1.200 -apply(simp add: mult_commute)
   1.201 -done
   1.202 +  apply (cut_tac m = m and n = n in mod_div_equality)
   1.203 +  apply (simp add: mult_commute)
   1.204 +  done
   1.205  
   1.206  subsection{*Simproc for Cancelling Div and Mod*}
   1.207  
   1.208  lemma div_mod_equality: "((m div n)*n + m mod n) + k = (m::nat) + k"
   1.209 -apply(simp add: mod_div_equality)
   1.210 -done
   1.211 +  by (simp add: mod_div_equality)
   1.212  
   1.213  lemma div_mod_equality2: "(n*(m div n) + m mod n) + k = (m::nat) + k"
   1.214 -apply(simp add: mod_div_equality2)
   1.215 -done
   1.216 +  by (simp add: mod_div_equality2)
   1.217  
   1.218  ML
   1.219  {*
   1.220 -val div_mod_equality = thm "div_mod_equality";
   1.221 -val div_mod_equality2 = thm "div_mod_equality2";
   1.222 -
   1.223 -
   1.224  structure CancelDivModData =
   1.225  struct
   1.226  
   1.227 -val div_name = "Divides.div";
   1.228 -val mod_name = "Divides.mod";
   1.229 +val div_name = @{const_name Divides.div};
   1.230 +val mod_name = @{const_name Divides.mod};
   1.231  val mk_binop = HOLogic.mk_binop;
   1.232  val mk_sum = NatArithUtils.mk_sum;
   1.233  val dest_sum = NatArithUtils.dest_sum;
   1.234  
   1.235  (*logic*)
   1.236  
   1.237 -val div_mod_eqs = map mk_meta_eq [div_mod_equality,div_mod_equality2]
   1.238 +val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}]
   1.239  
   1.240  val trans = trans
   1.241  
   1.242  val prove_eq_sums =
   1.243 -  let val simps = add_0 :: add_0_right :: add_ac
   1.244 +  let val simps = @{thm add_0} :: @{thm add_0_right} :: @{thms add_ac}
   1.245    in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
   1.246  
   1.247  end;
   1.248 @@ -226,25 +213,26 @@
   1.249  
   1.250  (* a simple rearrangement of mod_div_equality: *)
   1.251  lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
   1.252 -by (cut_tac m = m and n = n in mod_div_equality2, arith)
   1.253 +  by (cut_tac m = m and n = n in mod_div_equality2, arith)
   1.254  
   1.255  lemma mod_less_divisor [simp]: "0<n ==> m mod n < (n::nat)"
   1.256 -apply (induct "m" rule: nat_less_induct)
   1.257 -apply (case_tac "na<n", simp) 
   1.258 -txt{*case @{term "n \<le> na"}*}
   1.259 -apply (simp add: mod_geq)
   1.260 -done
   1.261 +  apply (induct m rule: nat_less_induct)
   1.262 +  apply (rename_tac m)
   1.263 +  apply (case_tac "m<n", simp)
   1.264 +  txt{*case @{term "n \<le> m"}*}
   1.265 +  apply (simp add: mod_geq)
   1.266 +  done
   1.267  
   1.268  lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
   1.269 -apply(drule mod_less_divisor[where m = m])
   1.270 -apply simp
   1.271 -done
   1.272 +  apply (drule mod_less_divisor [where m = m])
   1.273 +  apply simp
   1.274 +  done
   1.275  
   1.276  lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
   1.277 -by (cut_tac m = "m*n" and n = n in mod_div_equality, auto)
   1.278 +  by (cut_tac m = "m*n" and n = n in mod_div_equality, auto)
   1.279  
   1.280  lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
   1.281 -by (simp add: mult_commute div_mult_self_is_m)
   1.282 +  by (simp add: mult_commute div_mult_self_is_m)
   1.283  
   1.284  (*mod_mult_distrib2 above is the counterpart for remainder*)
   1.285  
   1.286 @@ -252,95 +240,93 @@
   1.287  subsection{*Proving facts about Quotient and Remainder*}
   1.288  
   1.289  lemma unique_quotient_lemma:
   1.290 -     "[| b*q' + r'  \<le> b*q + r;  x < b;  r < b |]  
   1.291 +     "[| b*q' + r'  \<le> b*q + r;  x < b;  r < b |]
   1.292        ==> q' \<le> (q::nat)"
   1.293 -apply (rule leI)
   1.294 -apply (subst less_iff_Suc_add)
   1.295 -apply (auto simp add: add_mult_distrib2)
   1.296 -done
   1.297 +  apply (rule leI)
   1.298 +  apply (subst less_iff_Suc_add)
   1.299 +  apply (auto simp add: add_mult_distrib2)
   1.300 +  done
   1.301  
   1.302  lemma unique_quotient:
   1.303 -     "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |]  
   1.304 +     "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |]
   1.305        ==> q = q'"
   1.306 -apply (simp add: split_ifs quorem_def)
   1.307 -apply (blast intro: order_antisym 
   1.308 -             dest: order_eq_refl [THEN unique_quotient_lemma] sym)
   1.309 -done
   1.310 +  apply (simp add: split_ifs quorem_def)
   1.311 +  apply (blast intro: order_antisym
   1.312 +    dest: order_eq_refl [THEN unique_quotient_lemma] sym)
   1.313 +  done
   1.314  
   1.315  lemma unique_remainder:
   1.316 -     "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |]  
   1.317 +     "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |]
   1.318        ==> r = r'"
   1.319 -apply (subgoal_tac "q = q'")
   1.320 -prefer 2 apply (blast intro: unique_quotient)
   1.321 -apply (simp add: quorem_def)
   1.322 -done
   1.323 +  apply (subgoal_tac "q = q'")
   1.324 +   prefer 2 apply (blast intro: unique_quotient)
   1.325 +  apply (simp add: quorem_def)
   1.326 +  done
   1.327  
   1.328  lemma quorem_div_mod: "0 < b ==> quorem ((a, b), (a div b, a mod b))"
   1.329 -  unfolding quorem_def by simp 
   1.330 +  unfolding quorem_def by simp
   1.331  
   1.332  lemma quorem_div: "[| quorem((a,b),(q,r));  0 < b |] ==> a div b = q"
   1.333 -by (simp add: quorem_div_mod [THEN unique_quotient])
   1.334 +  by (simp add: quorem_div_mod [THEN unique_quotient])
   1.335  
   1.336  lemma quorem_mod: "[| quorem((a,b),(q,r));  0 < b |] ==> a mod b = r"
   1.337 -by (simp add: quorem_div_mod [THEN unique_remainder])
   1.338 +  by (simp add: quorem_div_mod [THEN unique_remainder])
   1.339  
   1.340  (** A dividend of zero **)
   1.341  
   1.342  lemma div_0 [simp]: "0 div m = (0::nat)"
   1.343 -by (case_tac "m=0", simp_all)
   1.344 +  by (cases "m = 0") simp_all
   1.345  
   1.346  lemma mod_0 [simp]: "0 mod m = (0::nat)"
   1.347 -by (case_tac "m=0", simp_all)
   1.348 +  by (cases "m = 0") simp_all
   1.349  
   1.350  (** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
   1.351  
   1.352  lemma quorem_mult1_eq:
   1.353 -     "[| quorem((b,c),(q,r));  0 < c |]  
   1.354 +     "[| quorem((b,c),(q,r));  0 < c |]
   1.355        ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"
   1.356 -apply (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
   1.357 -done
   1.358 +  by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
   1.359  
   1.360  lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"
   1.361 -apply (case_tac "c = 0", simp)
   1.362 -apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_div])
   1.363 -done
   1.364 +  apply (cases "c = 0", simp)
   1.365 +  apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_div])
   1.366 +  done
   1.367  
   1.368  lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"
   1.369 -apply (case_tac "c = 0", simp)
   1.370 -apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_mod])
   1.371 -done
   1.372 +  apply (cases "c = 0", simp)
   1.373 +  apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_mod])
   1.374 +  done
   1.375  
   1.376  lemma mod_mult1_eq': "(a*b) mod (c::nat) = ((a mod c) * b) mod c"
   1.377 -apply (rule trans)
   1.378 -apply (rule_tac s = "b*a mod c" in trans)
   1.379 -apply (rule_tac [2] mod_mult1_eq)
   1.380 -apply (simp_all (no_asm) add: mult_commute)
   1.381 -done
   1.382 +  apply (rule trans)
   1.383 +   apply (rule_tac s = "b*a mod c" in trans)
   1.384 +    apply (rule_tac [2] mod_mult1_eq)
   1.385 +   apply (simp_all add: mult_commute)
   1.386 +  done
   1.387  
   1.388  lemma mod_mult_distrib_mod: "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"
   1.389 -apply (rule mod_mult1_eq' [THEN trans])
   1.390 -apply (rule mod_mult1_eq)
   1.391 -done
   1.392 +  apply (rule mod_mult1_eq' [THEN trans])
   1.393 +  apply (rule mod_mult1_eq)
   1.394 +  done
   1.395  
   1.396  (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
   1.397  
   1.398  lemma quorem_add1_eq:
   1.399 -     "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  0 < c |]  
   1.400 +     "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  0 < c |]
   1.401        ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
   1.402 -by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
   1.403 +  by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
   1.404  
   1.405  (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
   1.406  lemma div_add1_eq:
   1.407       "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
   1.408 -apply (case_tac "c = 0", simp)
   1.409 -apply (blast intro: quorem_add1_eq [THEN quorem_div] quorem_div_mod quorem_div_mod)
   1.410 -done
   1.411 +  apply (cases "c = 0", simp)
   1.412 +  apply (blast intro: quorem_add1_eq [THEN quorem_div] quorem_div_mod quorem_div_mod)
   1.413 +  done
   1.414  
   1.415  lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
   1.416 -apply (case_tac "c = 0", simp)
   1.417 -apply (blast intro: quorem_div_mod quorem_div_mod
   1.418 -                    quorem_add1_eq [THEN quorem_mod])
   1.419 -done
   1.420 +  apply (cases "c = 0", simp)
   1.421 +  apply (blast intro: quorem_div_mod quorem_div_mod quorem_add1_eq [THEN quorem_mod])
   1.422 +  done
   1.423  
   1.424  
   1.425  subsection{*Proving @{term "a div (b*c) = (a div b) div c"}*}
   1.426 @@ -348,45 +334,44 @@
   1.427  (** first, a lemma to bound the remainder **)
   1.428  
   1.429  lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
   1.430 -apply (cut_tac m = q and n = c in mod_less_divisor)
   1.431 -apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
   1.432 -apply (erule_tac P = "%x. ?lhs < ?rhs x" in ssubst)
   1.433 -apply (simp add: add_mult_distrib2)
   1.434 -done
   1.435 +  apply (cut_tac m = q and n = c in mod_less_divisor)
   1.436 +  apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
   1.437 +  apply (erule_tac P = "%x. ?lhs < ?rhs x" in ssubst)
   1.438 +  apply (simp add: add_mult_distrib2)
   1.439 +  done
   1.440  
   1.441 -lemma quorem_mult2_eq: "[| quorem ((a,b), (q,r));  0 < b;  0 < c |]  
   1.442 +lemma quorem_mult2_eq: "[| quorem ((a,b), (q,r));  0 < b;  0 < c |]
   1.443        ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"
   1.444 -apply (auto simp add: mult_ac quorem_def add_mult_distrib2 [symmetric] mod_lemma)
   1.445 -done
   1.446 +  by (auto simp add: mult_ac quorem_def add_mult_distrib2 [symmetric] mod_lemma)
   1.447  
   1.448  lemma div_mult2_eq: "a div (b*c) = (a div b) div (c::nat)"
   1.449 -apply (case_tac "b=0", simp)
   1.450 -apply (case_tac "c=0", simp)
   1.451 -apply (force simp add: quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_div])
   1.452 -done
   1.453 +  apply (cases "b = 0", simp)
   1.454 +  apply (cases "c = 0", simp)
   1.455 +  apply (force simp add: quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_div])
   1.456 +  done
   1.457  
   1.458  lemma mod_mult2_eq: "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)"
   1.459 -apply (case_tac "b=0", simp)
   1.460 -apply (case_tac "c=0", simp)
   1.461 -apply (auto simp add: mult_commute quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_mod])
   1.462 -done
   1.463 +  apply (cases "b = 0", simp)
   1.464 +  apply (cases "c = 0", simp)
   1.465 +  apply (auto simp add: mult_commute quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_mod])
   1.466 +  done
   1.467  
   1.468  
   1.469  subsection{*Cancellation of Common Factors in Division*}
   1.470  
   1.471  lemma div_mult_mult_lemma:
   1.472 -     "[| (0::nat) < b;  0 < c |] ==> (c*a) div (c*b) = a div b"
   1.473 -by (auto simp add: div_mult2_eq)
   1.474 +    "[| (0::nat) < b;  0 < c |] ==> (c*a) div (c*b) = a div b"
   1.475 +  by (auto simp add: div_mult2_eq)
   1.476  
   1.477  lemma div_mult_mult1 [simp]: "(0::nat) < c ==> (c*a) div (c*b) = a div b"
   1.478 -apply (case_tac "b = 0")
   1.479 -apply (auto simp add: linorder_neq_iff [of b] div_mult_mult_lemma)
   1.480 -done
   1.481 +  apply (cases "b = 0")
   1.482 +  apply (auto simp add: linorder_neq_iff [of b] div_mult_mult_lemma)
   1.483 +  done
   1.484  
   1.485  lemma div_mult_mult2 [simp]: "(0::nat) < c ==> (a*c) div (b*c) = a div b"
   1.486 -apply (drule div_mult_mult1)
   1.487 -apply (auto simp add: mult_commute)
   1.488 -done
   1.489 +  apply (drule div_mult_mult1)
   1.490 +  apply (auto simp add: mult_commute)
   1.491 +  done
   1.492  
   1.493  
   1.494  (*Distribution of Factors over Remainders:
   1.495 @@ -404,34 +389,32 @@
   1.496  subsection{*Further Facts about Quotient and Remainder*}
   1.497  
   1.498  lemma div_1 [simp]: "m div Suc 0 = m"
   1.499 -apply (induct "m")
   1.500 -apply (simp_all (no_asm_simp) add: div_geq)
   1.501 -done
   1.502 +  by (induct m) (simp_all add: div_geq)
   1.503  
   1.504  lemma div_self [simp]: "0<n ==> n div n = (1::nat)"
   1.505 -by (simp add: div_geq)
   1.506 +  by (simp add: div_geq)
   1.507  
   1.508  lemma div_add_self2: "0<n ==> (m+n) div n = Suc (m div n)"
   1.509 -apply (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n) ")
   1.510 -apply (simp add: add_commute)
   1.511 -apply (subst div_geq [symmetric], simp_all)
   1.512 -done
   1.513 +  apply (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n) ")
   1.514 +   apply (simp add: add_commute)
   1.515 +  apply (subst div_geq [symmetric], simp_all)
   1.516 +  done
   1.517  
   1.518  lemma div_add_self1: "0<n ==> (n+m) div n = Suc (m div n)"
   1.519 -by (simp add: add_commute div_add_self2)
   1.520 +  by (simp add: add_commute div_add_self2)
   1.521  
   1.522  lemma div_mult_self1 [simp]: "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n"
   1.523 -apply (subst div_add1_eq)
   1.524 -apply (subst div_mult1_eq, simp)
   1.525 -done
   1.526 +  apply (subst div_add1_eq)
   1.527 +  apply (subst div_mult1_eq, simp)
   1.528 +  done
   1.529  
   1.530  lemma div_mult_self2 [simp]: "0<n ==> (m + n*k) div n = k + m div (n::nat)"
   1.531 -by (simp add: mult_commute div_mult_self1)
   1.532 +  by (simp add: mult_commute div_mult_self1)
   1.533  
   1.534  
   1.535  (* Monotonicity of div in first argument *)
   1.536  lemma div_le_mono [rule_format (no_asm)]:
   1.537 -     "\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
   1.538 +    "\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
   1.539  apply (case_tac "k=0", simp)
   1.540  apply (induct "n" rule: nat_less_induct, clarify)
   1.541  apply (case_tac "n<k")
   1.542 @@ -448,12 +431,12 @@
   1.543  (* Antimonotonicity of div in second argument *)
   1.544  lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
   1.545  apply (subgoal_tac "0<n")
   1.546 - prefer 2 apply simp 
   1.547 + prefer 2 apply simp
   1.548  apply (induct_tac k rule: nat_less_induct)
   1.549  apply (rename_tac "k")
   1.550  apply (case_tac "k<n", simp)
   1.551  apply (subgoal_tac "~ (k<m) ")
   1.552 - prefer 2 apply simp 
   1.553 + prefer 2 apply simp
   1.554  apply (simp add: div_geq)
   1.555  apply (subgoal_tac "(k-n) div n \<le> (k-m) div n")
   1.556   prefer 2
   1.557 @@ -469,14 +452,14 @@
   1.558  apply (simp_all (no_asm_simp))
   1.559  done
   1.560  
   1.561 -(* Similar for "less than" *) 
   1.562 +(* Similar for "less than" *)
   1.563  lemma div_less_dividend [rule_format]:
   1.564       "!!n::nat. 1<n ==> 0 < m --> m div n < m"
   1.565  apply (induct_tac m rule: nat_less_induct)
   1.566  apply (rename_tac "m")
   1.567  apply (case_tac "m<n", simp)
   1.568  apply (subgoal_tac "0<n")
   1.569 - prefer 2 apply simp 
   1.570 + prefer 2 apply simp
   1.571  apply (simp add: div_geq)
   1.572  apply (case_tac "n<m")
   1.573   apply (subgoal_tac "(m-n) div n < (m-n) ")
   1.574 @@ -500,199 +483,187 @@
   1.575  done
   1.576  
   1.577  lemma nat_mod_div_trivial [simp]: "m mod n div n = (0 :: nat)"
   1.578 -by (case_tac "n=0", auto)
   1.579 +  by (cases "n = 0") auto
   1.580  
   1.581  lemma nat_mod_mod_trivial [simp]: "m mod n mod n = (m mod n :: nat)"
   1.582 -by (case_tac "n=0", auto)
   1.583 +  by (cases "n = 0") auto
   1.584  
   1.585  
   1.586  subsection{*The Divides Relation*}
   1.587  
   1.588  lemma dvdI [intro?]: "n = m * k ==> m dvd n"
   1.589 -by (unfold dvd_def, blast)
   1.590 +  unfolding dvd_def by blast
   1.591  
   1.592  lemma dvdE [elim?]: "!!P. [|m dvd n;  !!k. n = m*k ==> P|] ==> P"
   1.593 -by (unfold dvd_def, blast)
   1.594 +  unfolding dvd_def by blast
   1.595  
   1.596  lemma dvd_0_right [iff]: "m dvd (0::nat)"
   1.597 -apply (unfold dvd_def)
   1.598 -apply (blast intro: mult_0_right [symmetric])
   1.599 -done
   1.600 +  unfolding dvd_def by (blast intro: mult_0_right [symmetric])
   1.601  
   1.602  lemma dvd_0_left: "0 dvd m ==> m = (0::nat)"
   1.603 -by (force simp add: dvd_def)
   1.604 +  by (force simp add: dvd_def)
   1.605  
   1.606  lemma dvd_0_left_iff [iff]: "(0 dvd (m::nat)) = (m = 0)"
   1.607 -by (blast intro: dvd_0_left)
   1.608 +  by (blast intro: dvd_0_left)
   1.609  
   1.610  lemma dvd_1_left [iff]: "Suc 0 dvd k"
   1.611 -by (unfold dvd_def, simp)
   1.612 +  unfolding dvd_def by simp
   1.613  
   1.614  lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"
   1.615 -by (simp add: dvd_def)
   1.616 +  by (simp add: dvd_def)
   1.617  
   1.618  lemma dvd_refl [simp]: "m dvd (m::nat)"
   1.619 -apply (unfold dvd_def)
   1.620 -apply (blast intro: mult_1_right [symmetric])
   1.621 -done
   1.622 +  unfolding dvd_def by (blast intro: mult_1_right [symmetric])
   1.623  
   1.624  lemma dvd_trans [trans]: "[| m dvd n; n dvd p |] ==> m dvd (p::nat)"
   1.625 -apply (unfold dvd_def)
   1.626 -apply (blast intro: mult_assoc)
   1.627 -done
   1.628 +  unfolding dvd_def by (blast intro: mult_assoc)
   1.629  
   1.630  lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
   1.631 -apply (unfold dvd_def)
   1.632 -apply (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
   1.633 -done
   1.634 +  unfolding dvd_def
   1.635 +  by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
   1.636  
   1.637  lemma dvd_add: "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)"
   1.638 -apply (unfold dvd_def)
   1.639 -apply (blast intro: add_mult_distrib2 [symmetric])
   1.640 -done
   1.641 +  unfolding dvd_def
   1.642 +  by (blast intro: add_mult_distrib2 [symmetric])
   1.643  
   1.644  lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
   1.645 -apply (unfold dvd_def)
   1.646 -apply (blast intro: diff_mult_distrib2 [symmetric])
   1.647 -done
   1.648 +  unfolding dvd_def
   1.649 +  by (blast intro: diff_mult_distrib2 [symmetric])
   1.650  
   1.651  lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\<le>m |] ==> k dvd (m::nat)"
   1.652 -apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
   1.653 -apply (blast intro: dvd_add)
   1.654 -done
   1.655 +  apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
   1.656 +  apply (blast intro: dvd_add)
   1.657 +  done
   1.658  
   1.659  lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\<le>m |] ==> k dvd (n::nat)"
   1.660 -by (drule_tac m = m in dvd_diff, auto)
   1.661 +  by (drule_tac m = m in dvd_diff, auto)
   1.662  
   1.663  lemma dvd_mult: "k dvd n ==> k dvd (m*n :: nat)"
   1.664 -apply (unfold dvd_def)
   1.665 -apply (blast intro: mult_left_commute)
   1.666 -done
   1.667 +  unfolding dvd_def by (blast intro: mult_left_commute)
   1.668  
   1.669  lemma dvd_mult2: "k dvd m ==> k dvd (m*n :: nat)"
   1.670 -apply (subst mult_commute)
   1.671 -apply (erule dvd_mult)
   1.672 -done
   1.673 +  apply (subst mult_commute)
   1.674 +  apply (erule dvd_mult)
   1.675 +  done
   1.676  
   1.677  lemma dvd_triv_right [iff]: "k dvd (m*k :: nat)"
   1.678 -by (rule dvd_refl [THEN dvd_mult])
   1.679 +  by (rule dvd_refl [THEN dvd_mult])
   1.680  
   1.681  lemma dvd_triv_left [iff]: "k dvd (k*m :: nat)"
   1.682 -by (rule dvd_refl [THEN dvd_mult2])
   1.683 +  by (rule dvd_refl [THEN dvd_mult2])
   1.684  
   1.685  lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
   1.686 -apply (rule iffI)
   1.687 -apply (erule_tac [2] dvd_add)
   1.688 -apply (rule_tac [2] dvd_refl)
   1.689 -apply (subgoal_tac "n = (n+k) -k")
   1.690 - prefer 2 apply simp 
   1.691 -apply (erule ssubst)
   1.692 -apply (erule dvd_diff)
   1.693 -apply (rule dvd_refl)
   1.694 -done
   1.695 +  apply (rule iffI)
   1.696 +   apply (erule_tac [2] dvd_add)
   1.697 +   apply (rule_tac [2] dvd_refl)
   1.698 +  apply (subgoal_tac "n = (n+k) -k")
   1.699 +   prefer 2 apply simp
   1.700 +  apply (erule ssubst)
   1.701 +  apply (erule dvd_diff)
   1.702 +  apply (rule dvd_refl)
   1.703 +  done
   1.704  
   1.705  lemma dvd_mod: "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n"
   1.706 -apply (unfold dvd_def)
   1.707 -apply (case_tac "n=0", auto)
   1.708 -apply (blast intro: mod_mult_distrib2 [symmetric])
   1.709 -done
   1.710 +  unfolding dvd_def
   1.711 +  apply (case_tac "n = 0", auto)
   1.712 +  apply (blast intro: mod_mult_distrib2 [symmetric])
   1.713 +  done
   1.714  
   1.715  lemma dvd_mod_imp_dvd: "[| (k::nat) dvd m mod n;  k dvd n |] ==> k dvd m"
   1.716 -apply (subgoal_tac "k dvd (m div n) *n + m mod n")
   1.717 - apply (simp add: mod_div_equality)
   1.718 -apply (simp only: dvd_add dvd_mult)
   1.719 -done
   1.720 +  apply (subgoal_tac "k dvd (m div n) *n + m mod n")
   1.721 +   apply (simp add: mod_div_equality)
   1.722 +  apply (simp only: dvd_add dvd_mult)
   1.723 +  done
   1.724  
   1.725  lemma dvd_mod_iff: "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)"
   1.726 -by (blast intro: dvd_mod_imp_dvd dvd_mod)
   1.727 +  by (blast intro: dvd_mod_imp_dvd dvd_mod)
   1.728  
   1.729  lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"
   1.730 -apply (unfold dvd_def)
   1.731 -apply (erule exE)
   1.732 -apply (simp add: mult_ac)
   1.733 -done
   1.734 +  unfolding dvd_def
   1.735 +  apply (erule exE)
   1.736 +  apply (simp add: mult_ac)
   1.737 +  done
   1.738  
   1.739  lemma dvd_mult_cancel1: "0<m ==> (m*n dvd m) = (n = (1::nat))"
   1.740 -apply auto
   1.741 -apply (subgoal_tac "m*n dvd m*1")
   1.742 -apply (drule dvd_mult_cancel, auto)
   1.743 -done
   1.744 +  apply auto
   1.745 +   apply (subgoal_tac "m*n dvd m*1")
   1.746 +   apply (drule dvd_mult_cancel, auto)
   1.747 +  done
   1.748  
   1.749  lemma dvd_mult_cancel2: "0<m ==> (n*m dvd m) = (n = (1::nat))"
   1.750 -apply (subst mult_commute)
   1.751 -apply (erule dvd_mult_cancel1)
   1.752 -done
   1.753 +  apply (subst mult_commute)
   1.754 +  apply (erule dvd_mult_cancel1)
   1.755 +  done
   1.756  
   1.757  lemma mult_dvd_mono: "[| i dvd m; j dvd n|] ==> i*j dvd (m*n :: nat)"
   1.758 -apply (unfold dvd_def, clarify)
   1.759 -apply (rule_tac x = "k*ka" in exI)
   1.760 -apply (simp add: mult_ac)
   1.761 -done
   1.762 +  apply (unfold dvd_def, clarify)
   1.763 +  apply (rule_tac x = "k*ka" in exI)
   1.764 +  apply (simp add: mult_ac)
   1.765 +  done
   1.766  
   1.767  lemma dvd_mult_left: "(i*j :: nat) dvd k ==> i dvd k"
   1.768 -by (simp add: dvd_def mult_assoc, blast)
   1.769 +  by (simp add: dvd_def mult_assoc, blast)
   1.770  
   1.771  lemma dvd_mult_right: "(i*j :: nat) dvd k ==> j dvd k"
   1.772 -apply (unfold dvd_def, clarify)
   1.773 -apply (rule_tac x = "i*k" in exI)
   1.774 -apply (simp add: mult_ac)
   1.775 -done
   1.776 +  apply (unfold dvd_def, clarify)
   1.777 +  apply (rule_tac x = "i*k" in exI)
   1.778 +  apply (simp add: mult_ac)
   1.779 +  done
   1.780  
   1.781  lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \<le> (n::nat)"
   1.782 -apply (unfold dvd_def, clarify)
   1.783 -apply (simp_all (no_asm_use) add: zero_less_mult_iff)
   1.784 -apply (erule conjE)
   1.785 -apply (rule le_trans)
   1.786 -apply (rule_tac [2] le_refl [THEN mult_le_mono])
   1.787 -apply (erule_tac [2] Suc_leI, simp)
   1.788 -done
   1.789 +  apply (unfold dvd_def, clarify)
   1.790 +  apply (simp_all (no_asm_use) add: zero_less_mult_iff)
   1.791 +  apply (erule conjE)
   1.792 +  apply (rule le_trans)
   1.793 +   apply (rule_tac [2] le_refl [THEN mult_le_mono])
   1.794 +   apply (erule_tac [2] Suc_leI, simp)
   1.795 +  done
   1.796  
   1.797  lemma dvd_eq_mod_eq_0: "!!k::nat. (k dvd n) = (n mod k = 0)"
   1.798 -apply (unfold dvd_def)
   1.799 -apply (case_tac "k=0", simp, safe)
   1.800 -apply (simp add: mult_commute)
   1.801 -apply (rule_tac t = n and n1 = k in mod_div_equality [THEN subst])
   1.802 -apply (subst mult_commute, simp)
   1.803 -done
   1.804 +  apply (unfold dvd_def)
   1.805 +  apply (case_tac "k=0", simp, safe)
   1.806 +   apply (simp add: mult_commute)
   1.807 +  apply (rule_tac t = n and n1 = k in mod_div_equality [THEN subst])
   1.808 +  apply (subst mult_commute, simp)
   1.809 +  done
   1.810  
   1.811  lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
   1.812 -apply (subgoal_tac "m mod n = 0")
   1.813 - apply (simp add: mult_div_cancel)
   1.814 -apply (simp only: dvd_eq_mod_eq_0)
   1.815 -done
   1.816 +  apply (subgoal_tac "m mod n = 0")
   1.817 +   apply (simp add: mult_div_cancel)
   1.818 +  apply (simp only: dvd_eq_mod_eq_0)
   1.819 +  done
   1.820  
   1.821  lemma le_imp_power_dvd: "!!i::nat. m \<le> n ==> i^m dvd i^n"
   1.822 -apply (unfold dvd_def)
   1.823 -apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
   1.824 -apply (simp add: power_add)
   1.825 -done
   1.826 +  apply (unfold dvd_def)
   1.827 +  apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
   1.828 +  apply (simp add: power_add)
   1.829 +  done
   1.830  
   1.831  lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"
   1.832 -by (induct "n", auto)
   1.833 +  by (induct n) auto
   1.834  
   1.835  lemma power_le_dvd [rule_format]: "k^j dvd n --> i\<le>j --> k^i dvd (n::nat)"
   1.836 -apply (induct "j")
   1.837 -apply (simp_all add: le_Suc_eq)
   1.838 -apply (blast dest!: dvd_mult_right)
   1.839 -done
   1.840 +  apply (induct j)
   1.841 +   apply (simp_all add: le_Suc_eq)
   1.842 +  apply (blast dest!: dvd_mult_right)
   1.843 +  done
   1.844  
   1.845  lemma power_dvd_imp_le: "[|i^m dvd i^n;  (1::nat) < i|] ==> m \<le> n"
   1.846 -apply (rule power_le_imp_le_exp, assumption)
   1.847 -apply (erule dvd_imp_le, simp)
   1.848 -done
   1.849 +  apply (rule power_le_imp_le_exp, assumption)
   1.850 +  apply (erule dvd_imp_le, simp)
   1.851 +  done
   1.852  
   1.853  lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
   1.854 -by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
   1.855 +  by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
   1.856  
   1.857 -lemmas mod_eq_0D = mod_eq_0_iff [THEN iffD1]
   1.858 -declare mod_eq_0D [dest!]
   1.859 +lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
   1.860  
   1.861  (*Loses information, namely we also have r<d provided d is nonzero*)
   1.862  lemma mod_eqD: "(m mod d = r) ==> \<exists>q::nat. m = r + q*d"
   1.863 -apply (cut_tac m = m in mod_div_equality)
   1.864 -apply (simp only: add_ac)
   1.865 -apply (blast intro: sym)
   1.866 -done
   1.867 +  apply (cut_tac m = m in mod_div_equality)
   1.868 +  apply (simp only: add_ac)
   1.869 +  apply (blast intro: sym)
   1.870 +  done
   1.871  
   1.872  
   1.873  lemma split_div:
   1.874 @@ -713,11 +684,11 @@
   1.875        assume n: "n = k*i + j" and j: "j < k"
   1.876        show "P i"
   1.877        proof (cases)
   1.878 -	assume "i = 0"
   1.879 -	with n j P show "P i" by simp
   1.880 +        assume "i = 0"
   1.881 +        with n j P show "P i" by simp
   1.882        next
   1.883 -	assume "i \<noteq> 0"
   1.884 -	with not0 n j P show "P i" by(simp add:add_ac)
   1.885 +        assume "i \<noteq> 0"
   1.886 +        with not0 n j P show "P i" by(simp add:add_ac)
   1.887        qed
   1.888      qed
   1.889    qed
   1.890 @@ -818,28 +789,28 @@
   1.891        assume ih: "?A n"
   1.892        show "?A (Suc n)"
   1.893        proof (clarsimp)
   1.894 -	assume y: "P (p - Suc n)"
   1.895 -	have n: "Suc n < p"
   1.896 -	proof (rule ccontr)
   1.897 -	  assume "\<not>(Suc n < p)"
   1.898 -	  hence "p - Suc n = 0"
   1.899 -	    by simp
   1.900 -	  with y contra show "False"
   1.901 -	    by simp
   1.902 -	qed
   1.903 -	hence n2: "Suc (p - Suc n) = p-n" by arith
   1.904 -	from p have "p - Suc n < p" by arith
   1.905 -	with y step have z: "P ((Suc (p - Suc n)) mod p)"
   1.906 -	  by blast
   1.907 -	show "False"
   1.908 -	proof (cases "n=0")
   1.909 -	  case True
   1.910 -	  with z n2 contra show ?thesis by simp
   1.911 -	next
   1.912 -	  case False
   1.913 -	  with p have "p-n < p" by arith
   1.914 -	  with z n2 False ih show ?thesis by simp
   1.915 -	qed
   1.916 +        assume y: "P (p - Suc n)"
   1.917 +        have n: "Suc n < p"
   1.918 +        proof (rule ccontr)
   1.919 +          assume "\<not>(Suc n < p)"
   1.920 +          hence "p - Suc n = 0"
   1.921 +            by simp
   1.922 +          with y contra show "False"
   1.923 +            by simp
   1.924 +        qed
   1.925 +        hence n2: "Suc (p - Suc n) = p-n" by arith
   1.926 +        from p have "p - Suc n < p" by arith
   1.927 +        with y step have z: "P ((Suc (p - Suc n)) mod p)"
   1.928 +          by blast
   1.929 +        show "False"
   1.930 +        proof (cases "n=0")
   1.931 +          case True
   1.932 +          with z n2 contra show ?thesis by simp
   1.933 +        next
   1.934 +          case False
   1.935 +          with p have "p-n < p" by arith
   1.936 +          with z n2 False ih show ?thesis by simp
   1.937 +        qed
   1.938        qed
   1.939      qed
   1.940    qed
   1.941 @@ -864,22 +835,22 @@
   1.942      show "j<p \<longrightarrow> P j" (is "?A j")
   1.943      proof (induct j)
   1.944        from step base i show "?A 0"
   1.945 -	by (auto elim: mod_induct_0)
   1.946 +        by (auto elim: mod_induct_0)
   1.947      next
   1.948        fix k
   1.949        assume ih: "?A k"
   1.950        show "?A (Suc k)"
   1.951        proof
   1.952 -	assume suc: "Suc k < p"
   1.953 -	hence k: "k<p" by simp
   1.954 -	with ih have "P k" ..
   1.955 -	with step k have "P (Suc k mod p)"
   1.956 -	  by blast
   1.957 -	moreover
   1.958 -	from suc have "Suc k mod p = Suc k"
   1.959 -	  by simp
   1.960 -	ultimately
   1.961 -	show "P (Suc k)" by simp
   1.962 +        assume suc: "Suc k < p"
   1.963 +        hence k: "k<p" by simp
   1.964 +        with ih have "P k" ..
   1.965 +        with step k have "P (Suc k mod p)"
   1.966 +          by blast
   1.967 +        moreover
   1.968 +        from suc have "Suc k mod p = Suc k"
   1.969 +          by simp
   1.970 +        ultimately
   1.971 +        show "P (Suc k)" by simp
   1.972        qed
   1.973      qed
   1.974    qed
   1.975 @@ -889,15 +860,15 @@
   1.976  
   1.977  lemma mod_add_left_eq: "((a::nat) + b) mod c = (a mod c + b) mod c"
   1.978    apply (rule trans [symmetric])
   1.979 -  apply (rule mod_add1_eq, simp)
   1.980 +   apply (rule mod_add1_eq, simp)
   1.981    apply (rule mod_add1_eq [symmetric])
   1.982    done
   1.983  
   1.984  lemma mod_add_right_eq: "(a+b) mod (c::nat) = (a + (b mod c)) mod c"
   1.985 -apply (rule trans [symmetric])
   1.986 -apply (rule mod_add1_eq, simp)
   1.987 -apply (rule mod_add1_eq [symmetric])
   1.988 -done
   1.989 +  apply (rule trans [symmetric])
   1.990 +   apply (rule mod_add1_eq, simp)
   1.991 +  apply (rule mod_add1_eq [symmetric])
   1.992 +  done
   1.993  
   1.994  
   1.995  subsection {* Code generation for div and mod *}
   1.996 @@ -905,25 +876,21 @@
   1.997  definition
   1.998    "divmod (m\<Colon>nat) n = (m div n, m mod n)"
   1.999  
  1.1000 -lemma divmod_zero [code]:
  1.1001 -  "divmod m 0 = (0, m)"
  1.1002 +lemma divmod_zero [code]: "divmod m 0 = (0, m)"
  1.1003    unfolding divmod_def by simp
  1.1004  
  1.1005  lemma divmod_succ [code]:
  1.1006    "divmod m (Suc k) = (if m < Suc k then (0, m) else
  1.1007      let
  1.1008        (p, q) = divmod (m - Suc k) (Suc k)
  1.1009 -    in (Suc p, q)
  1.1010 -  )"
  1.1011 +    in (Suc p, q))"
  1.1012    unfolding divmod_def Let_def split_def
  1.1013    by (auto intro: div_geq mod_geq)
  1.1014  
  1.1015 -lemma div_divmod [code]:
  1.1016 -  "m div n = fst (divmod m n)"
  1.1017 +lemma div_divmod [code]: "m div n = fst (divmod m n)"
  1.1018    unfolding divmod_def by simp
  1.1019  
  1.1020 -lemma mod_divmod [code]:
  1.1021 -  "m mod n = snd (divmod m n)"
  1.1022 +lemma mod_divmod [code]: "m mod n = snd (divmod m n)"
  1.1023    unfolding divmod_def by simp
  1.1024  
  1.1025  code_modulename SML
  1.1026 @@ -934,7 +901,6 @@
  1.1027  
  1.1028  hide (open) const divmod
  1.1029  
  1.1030 -
  1.1031  subsection {* Legacy bindings *}
  1.1032  
  1.1033  ML
  1.1034 @@ -1038,7 +1004,6 @@
  1.1035  val mod_eqD = thm "mod_eqD";
  1.1036  *}
  1.1037  
  1.1038 -
  1.1039  (*
  1.1040  lemma split_div:
  1.1041  assumes m: "m \<noteq> 0"