src/HOL/Divides.thy
 changeset 60758 d8d85a8172b5 parent 60690 a9e45c9588c3 child 60867 86e7560e07d0
     1.1 --- a/src/HOL/Divides.thy	Sat Jul 18 21:44:18 2015 +0200
1.2 +++ b/src/HOL/Divides.thy	Sat Jul 18 22:58:50 2015 +0200
1.3 @@ -3,13 +3,13 @@
1.4      Copyright   1999  University of Cambridge
1.5  *)
1.6
1.7 -section {* The division operators div and mod *}
1.8 +section \<open>The division operators div and mod\<close>
1.9
1.10  theory Divides
1.11  imports Parity
1.12  begin
1.13
1.14 -subsection {* Abstract division in commutative semirings. *}
1.15 +subsection \<open>Abstract division in commutative semirings.\<close>
1.16
1.17  class div = dvd + divide +
1.18    fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "mod" 70)
1.19 @@ -38,7 +38,7 @@
1.20    "n \<noteq> 0 \<Longrightarrow> a ^ n = 0 \<longleftrightarrow> a = 0"
1.21    using power_not_zero [of a n] by (auto simp add: zero_power)
1.22
1.23 -text {* @{const divide} and @{const mod} *}
1.24 +text \<open>@{const divide} and @{const mod}\<close>
1.25
1.26  lemma mod_div_equality2: "b * (a div b) + a mod b = a"
1.27    unfolding mult.commute [of b]
1.28 @@ -232,7 +232,7 @@
1.29    then show ?thesis by (simp add: mod_div_equality)
1.30  qed
1.31
1.32 -text {* Addition respects modular equivalence. *}
1.33 +text \<open>Addition respects modular equivalence.\<close>
1.34
1.35  lemma mod_add_left_eq: "(a + b) mod c = (a mod c + b) mod c"
1.36  proof -
1.37 @@ -274,7 +274,7 @@
1.38    \<Longrightarrow> (x + y) div z = x div z + y div z"
1.39  by (cases "z = 0", simp, unfold dvd_def, auto simp add: algebra_simps)
1.40
1.41 -text {* Multiplication respects modular equivalence. *}
1.42 +text \<open>Multiplication respects modular equivalence.\<close>
1.43
1.44  lemma mod_mult_left_eq: "(a * b) mod c = ((a mod c) * b) mod c"
1.45  proof -
1.46 @@ -312,7 +312,7 @@
1.47      by (simp only: mod_mult_eq [symmetric])
1.48  qed
1.49
1.50 -text {* Exponentiation respects modular equivalence. *}
1.51 +text \<open>Exponentiation respects modular equivalence.\<close>
1.52
1.53  lemma power_mod: "(a mod b)^n mod b = a^n mod b"
1.54  apply (induct n, simp_all)
1.55 @@ -325,10 +325,10 @@
1.56    assumes "c dvd b"
1.57    shows "a mod b mod c = a mod c"
1.58  proof -
1.59 -  from c dvd b obtain k where "b = c * k"
1.60 +  from \<open>c dvd b\<close> obtain k where "b = c * k"
1.61      by (rule dvdE)
1.62    have "a mod b mod c = a mod (c * k) mod c"
1.63 -    by (simp only: b = c * k)
1.64 +    by (simp only: \<open>b = c * k\<close>)
1.65    also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
1.66      by (simp only: mod_mult_self1)
1.67    also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
1.68 @@ -400,7 +400,7 @@
1.69  next
1.70    assume "b div a = c"
1.71    then have "b div a * a = c * a" by simp
1.72 -  moreover from a dvd b have "b div a * a = b" by simp
1.73 +  moreover from \<open>a dvd b\<close> have "b div a * a = b" by simp
1.74    ultimately show "b = c * a" by simp
1.75  qed
1.76
1.77 @@ -416,7 +416,7 @@
1.78
1.79  subclass idom_divide ..
1.80
1.81 -text {* Negation respects modular equivalence. *}
1.82 +text \<open>Negation respects modular equivalence.\<close>
1.83
1.84  lemma mod_minus_eq: "(- a) mod b = (- (a mod b)) mod b"
1.85  proof -
1.86 @@ -439,7 +439,7 @@
1.87      by (simp only: mod_minus_eq [symmetric])
1.88  qed
1.89
1.90 -text {* Subtraction respects modular equivalence. *}
1.91 +text \<open>Subtraction respects modular equivalence.\<close>
1.92
1.93  lemma mod_diff_left_eq:
1.94    "(a - b) mod c = (a mod c - b) mod c"
1.95 @@ -512,7 +512,7 @@
1.96  end
1.97
1.98
1.99 -subsubsection {* Parity and division *}
1.100 +subsubsection \<open>Parity and division\<close>
1.101
1.102  class semiring_div_parity = semiring_div + comm_semiring_1_cancel + numeral +
1.103    assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
1.104 @@ -594,15 +594,15 @@
1.105  end
1.106
1.107
1.108 -subsection {* Generic numeral division with a pragmatic type class *}
1.109 -
1.110 -text {*
1.111 +subsection \<open>Generic numeral division with a pragmatic type class\<close>
1.112 +
1.113 +text \<open>
1.114    The following type class contains everything necessary to formulate
1.115    a division algorithm in ring structures with numerals, restricted
1.116    to its positive segments.  This is its primary motiviation, and it
1.117    could surely be formulated using a more fine-grained, more algebraic
1.118    and less technical class hierarchy.
1.119 -*}
1.120 +\<close>
1.121
1.122  class semiring_numeral_div = semiring_div + comm_semiring_1_cancel + linordered_semidom +
1.123    assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
1.124 @@ -636,11 +636,11 @@
1.125      then have "a mod 2 \<noteq> 0" and "a mod 2 \<noteq> 1" by simp_all
1.126      have "0 < 2" by simp
1.127      with pos_mod_bound pos_mod_sign have "0 \<le> a mod 2" "a mod 2 < 2" by simp_all
1.128 -    with a mod 2 \<noteq> 0 have "0 < a mod 2" by simp
1.129 +    with \<open>a mod 2 \<noteq> 0\<close> have "0 < a mod 2" by simp
1.130      with discrete have "1 \<le> a mod 2" by simp
1.131 -    with a mod 2 \<noteq> 1 have "1 < a mod 2" by simp
1.132 +    with \<open>a mod 2 \<noteq> 1\<close> have "1 < a mod 2" by simp
1.133      with discrete have "2 \<le> a mod 2" by simp
1.134 -    with a mod 2 < 2 show False by simp
1.135 +    with \<open>a mod 2 < 2\<close> show False by simp
1.136    qed
1.137  next
1.138    show "1 mod 2 = 1"
1.139 @@ -657,9 +657,9 @@
1.140  proof -
1.141    from assms mod_less_eq_dividend [of a "2 * b"] have "b \<le> a"
1.142      by (auto intro: trans)
1.143 -  with 0 < b have "0 < a div b" by (auto intro: div_positive)
1.144 +  with \<open>0 < b\<close> have "0 < a div b" by (auto intro: div_positive)
1.145    then have [simp]: "1 \<le> a div b" by (simp add: discrete)
1.146 -  with 0 < b have mod_less: "a mod b < b" by (simp add: pos_mod_bound)
1.147 +  with \<open>0 < b\<close> have mod_less: "a mod b < b" by (simp add: pos_mod_bound)
1.148    def w \<equiv> "a div b mod 2" with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
1.149    have mod_w: "a mod (2 * b) = a mod b + b * w"
1.150      by (simp add: w_def mod_mult2_eq ac_simps)
1.151 @@ -668,7 +668,7 @@
1.152    with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp
1.153    have "2 * (a div (2 * b)) = a div b - w"
1.154      by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)
1.155 -  with w = 1 have div: "2 * (a div (2 * b)) = a div b - 1" by simp
1.156 +  with \<open>w = 1\<close> have div: "2 * (a div (2 * b)) = a div b - 1" by simp
1.157    then show ?P and ?Q
1.159  qed
1.160 @@ -683,7 +683,7 @@
1.161      by (simp add: w_def mod_mult2_eq ac_simps)
1.162    moreover have "b \<le> a mod b + b"
1.163    proof -
1.164 -    from 0 < b pos_mod_sign have "0 \<le> a mod b" by blast
1.165 +    from \<open>0 < b\<close> pos_mod_sign have "0 \<le> a mod b" by blast
1.166      then have "0 + b \<le> a mod b + b" by (rule add_right_mono)
1.167      then show ?thesis by simp
1.168    qed
1.169 @@ -692,7 +692,7 @@
1.170    with mod_w have mod: "a mod (2 * b) = a mod b" by simp
1.171    have "2 * (a div (2 * b)) = a div b - w"
1.172      by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)
1.173 -  with w = 0 have div: "2 * (a div (2 * b)) = a div b" by simp
1.174 +  with \<open>w = 0\<close> have div: "2 * (a div (2 * b)) = a div b" by simp
1.175    then show ?P and ?Q
1.176      by (simp_all add: div mod)
1.177  qed
1.178 @@ -715,12 +715,12 @@
1.179      in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
1.180      else (2 * q, r))"
1.181
1.182 -text {*
1.183 +text \<open>
1.184    This is a formulation of one step (referring to one digit position)
1.185    in school-method division: compare the dividend at the current
1.186    digit position with the remainder from previous division steps
1.187    and evaluate accordingly.
1.188 -*}
1.189 +\<close>
1.190
1.191  lemma divmod_step_eq [code]:
1.192    "divmod_step l (q, r) = (if numeral l \<le> r
1.193 @@ -732,13 +732,13 @@
1.194    "numeral l \<le> r \<Longrightarrow> divmod_step l (q, r) = (2 * q + 1, r - numeral l)"
1.195    by (auto simp add: divmod_step_eq not_le)
1.196
1.197 -text {*
1.198 +text \<open>
1.199    This is a formulation of school-method division.
1.200    If the divisor is smaller than the dividend, terminate.
1.201    If not, shift the dividend to the right until termination
1.202    occurs and then reiterate single division steps in the
1.203    opposite direction.
1.204 -*}
1.205 +\<close>
1.206
1.207  lemma divmod_divmod_step [code]:
1.208    "divmod m n = (if m < n then (0, numeral m)
1.209 @@ -803,7 +803,7 @@
1.210        div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2] add.commute del: numeral_times_numeral)
1.211  qed
1.212
1.213 -text {* Special case: divisibility *}
1.214 +text \<open>Special case: divisibility\<close>
1.215
1.216  definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"
1.217  where
1.218 @@ -820,21 +820,21 @@
1.219  end
1.220
1.221
1.222 -subsection {* Division on @{typ nat} *}
1.223 -
1.224 -text {*
1.225 +subsection \<open>Division on @{typ nat}\<close>
1.226 +
1.227 +text \<open>
1.228    We define @{const divide} and @{const mod} on @{typ nat} by means
1.229    of a characteristic relation with two input arguments
1.230    @{term "m\<Colon>nat"}, @{term "n\<Colon>nat"} and two output arguments
1.231    @{term "q\<Colon>nat"}(uotient) and @{term "r\<Colon>nat"}(emainder).
1.232 -*}
1.233 +\<close>
1.234
1.235  definition divmod_nat_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
1.236    "divmod_nat_rel m n qr \<longleftrightarrow>
1.237      m = fst qr * n + snd qr \<and>
1.238        (if n = 0 then fst qr = 0 else if n > 0 then 0 \<le> snd qr \<and> snd qr < n else n < snd qr \<and> snd qr \<le> 0)"
1.239
1.240 -text {* @{const divmod_nat_rel} is total: *}
1.241 +text \<open>@{const divmod_nat_rel} is total:\<close>
1.242
1.243  lemma divmod_nat_rel_ex:
1.244    obtains q r where "divmod_nat_rel m n (q, r)"
1.245 @@ -845,7 +845,7 @@
1.246    case False
1.247    have "\<exists>q r. m = q * n + r \<and> r < n"
1.248    proof (induct m)
1.249 -    case 0 with n \<noteq> 0
1.250 +    case 0 with \<open>n \<noteq> 0\<close>
1.251      have "(0\<Colon>nat) = 0 * n + 0 \<and> 0 < n" by simp
1.252      then show ?case by blast
1.253    next
1.254 @@ -860,14 +860,14 @@
1.255        moreover from n have "Suc r' \<le> n" by auto
1.256        ultimately have "n = Suc r'" by auto
1.257        with m have "Suc m = Suc q' * n + 0" by simp
1.258 -      with n \<noteq> 0 show ?thesis by blast
1.259 +      with \<open>n \<noteq> 0\<close> show ?thesis by blast
1.260      qed
1.261    qed
1.262    with that show thesis
1.263 -    using n \<noteq> 0 by (auto simp add: divmod_nat_rel_def)
1.264 +    using \<open>n \<noteq> 0\<close> by (auto simp add: divmod_nat_rel_def)
1.265  qed
1.266
1.267 -text {* @{const divmod_nat_rel} is injective: *}
1.268 +text \<open>@{const divmod_nat_rel} is injective:\<close>
1.269
1.270  lemma divmod_nat_rel_unique:
1.271    assumes "divmod_nat_rel m n qr"
1.272 @@ -884,17 +884,17 @@
1.275    done
1.276 -  from n \<noteq> 0 assms have *: "fst qr = fst qr'"
1.277 +  from \<open>n \<noteq> 0\<close> assms have *: "fst qr = fst qr'"
1.278      by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym)
1.279    with assms have "snd qr = snd qr'"
1.281    with * show ?thesis by (cases qr, cases qr') simp
1.282  qed
1.283
1.284 -text {*
1.285 +text \<open>
1.286    We instantiate divisibility on the natural numbers by
1.287    means of @{const divmod_nat_rel}:
1.288 -*}
1.289 +\<close>
1.290
1.291  definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
1.292    "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
1.293 @@ -966,7 +966,7 @@
1.294      unfolding divmod_nat_rel_def using assms by auto
1.295  qed
1.296
1.297 -text {* The ''recursion'' equations for @{const divide} and @{const mod} *}
1.298 +text \<open>The ''recursion'' equations for @{const divide} and @{const mod}\<close>
1.299
1.300  lemma div_less [simp]:
1.301    fixes m n :: nat
1.302 @@ -1043,11 +1043,11 @@
1.303    let (q, r) = divmod_nat (m - n) n in (Suc q, r))"
1.304    by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
1.305
1.306 -text {* Simproc for cancelling @{const divide} and @{const mod} *}
1.307 +text \<open>Simproc for cancelling @{const divide} and @{const mod}\<close>
1.308
1.309  ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
1.310
1.311 -ML {*
1.312 +ML \<open>
1.313  structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
1.314  (
1.315    val div_name = @{const_name divide};
1.316 @@ -1073,12 +1073,12 @@
1.317    val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
1.319  )
1.320 -*}
1.321 -
1.322 -simproc_setup cancel_div_mod_nat ("(m::nat) + n") = {* K Cancel_Div_Mod_Nat.proc *}
1.323 -
1.324 -
1.325 -subsubsection {* Quotient *}
1.326 +\<close>
1.327 +
1.328 +simproc_setup cancel_div_mod_nat ("(m::nat) + n") = \<open>K Cancel_Div_Mod_Nat.proc\<close>
1.329 +
1.330 +
1.331 +subsubsection \<open>Quotient\<close>
1.332
1.333  lemma div_geq: "0 < n \<Longrightarrow>  \<not> m < n \<Longrightarrow> m div n = Suc ((m - n) div n)"
1.334  by (simp add: le_div_geq linorder_not_less)
1.335 @@ -1098,15 +1098,15 @@
1.336    assumes "m \<ge> n"
1.337    shows "m div n > 0"
1.338  proof -
1.339 -  from m \<ge> n obtain q where "m = n + q"
1.340 +  from \<open>m \<ge> n\<close> obtain q where "m = n + q"
1.342 -  with n > 0 show ?thesis by simp
1.343 +  with \<open>n > 0\<close> show ?thesis by simp
1.344  qed
1.345
1.346  lemma div_eq_0_iff: "(a div b::nat) = 0 \<longleftrightarrow> a < b \<or> b = 0"
1.347    by (metis div_less div_positive div_by_0 gr0I less_numeral_extra(3) not_less)
1.348
1.349 -subsubsection {* Remainder *}
1.350 +subsubsection \<open>Remainder\<close>
1.351
1.352  lemma mod_less_divisor [simp]:
1.353    fixes m n :: nat
1.354 @@ -1144,7 +1144,7 @@
1.355    apply simp
1.356    done
1.357
1.358 -subsubsection {* Quotient and Remainder *}
1.359 +subsubsection \<open>Quotient and Remainder\<close>
1.360
1.361  lemma divmod_nat_rel_mult1_eq:
1.362    "divmod_nat_rel b c (q, r)
1.363 @@ -1192,7 +1192,7 @@
1.364    by intro_classes (auto intro: div_positive simp add: mult_div_cancel mod_mult2_eq div_mult2_eq)
1.365
1.366
1.367 -subsubsection {* Further Facts about Quotient and Remainder *}
1.368 +subsubsection \<open>Further Facts about Quotient and Remainder\<close>
1.369
1.370  lemma div_1 [simp]:
1.371    "m div Suc 0 = m"
1.372 @@ -1254,7 +1254,7 @@
1.373    apply (simp_all)
1.374  done
1.375
1.376 -text{*A fact for the mutilated chess board*}
1.377 +text\<open>A fact for the mutilated chess board\<close>
1.378  lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
1.379  apply (case_tac "n=0", simp)
1.380  apply (induct "m" rule: nat_less_induct)
1.381 @@ -1400,7 +1400,7 @@
1.382    done
1.383
1.384
1.385 -subsubsection {* An induction'' law for modulus arithmetic. *}
1.386 +subsubsection \<open>An induction'' law for modulus arithmetic.\<close>
1.387
1.388  lemma mod_induct_0:
1.389    assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
1.390 @@ -1505,9 +1505,9 @@
1.391    then show ?thesis by auto
1.392  qed
1.393
1.394 -text{*These lemmas collapse some needless occurrences of Suc:
1.395 +text\<open>These lemmas collapse some needless occurrences of Suc:
1.396      at least three Sucs, since two and fewer are rewritten back to Suc again!
1.397 -    We already have some rules to simplify operands smaller than 3.*}
1.398 +    We already have some rules to simplify operands smaller than 3.\<close>
1.399
1.400  lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
1.402 @@ -1611,27 +1611,27 @@
1.403  qed
1.404
1.405
1.406 -subsection {* Division on @{typ int} *}
1.407 +subsection \<open>Division on @{typ int}\<close>
1.408
1.409  definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where
1.410 -    --{*definition of quotient and remainder*}
1.411 +    --\<open>definition of quotient and remainder\<close>
1.412    "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
1.413      (if 0 < b then 0 \<le> r \<and> r < b else if b < 0 then b < r \<and> r \<le> 0 else q = 0))"
1.414
1.415 -text {*
1.416 +text \<open>
1.417    The following algorithmic devlopment actually echos what has already
1.418    been developed in class @{class semiring_numeral_div}.  In the long
1.419    run it seems better to derive division on @{typ int} just from
1.420    division on @{typ nat} and instantiate @{class semiring_numeral_div}
1.421    accordingly.
1.422 -*}
1.423 +\<close>
1.424
1.425  definition adjust :: "int \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int" where
1.426 -    --{*for the division algorithm*}
1.427 +    --\<open>for the division algorithm\<close>
1.428      "adjust b = (\<lambda>(q, r). if 0 \<le> r - b then (2 * q + 1, r - b)
1.429                           else (2 * q, r))"
1.430
1.431 -text{*algorithm for the case @{text "a\<ge>0, b>0"}*}
1.432 +text\<open>algorithm for the case @{text "a\<ge>0, b>0"}\<close>
1.433  function posDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
1.434    "posDivAlg a b = (if a < b \<or>  b \<le> 0 then (0, a)
1.435       else adjust b (posDivAlg a (2 * b)))"
1.436 @@ -1639,7 +1639,7 @@
1.437  termination by (relation "measure (\<lambda>(a, b). nat (a - b + 1))")
1.439
1.440 -text{*algorithm for the case @{text "a<0, b>0"}*}
1.441 +text\<open>algorithm for the case @{text "a<0, b>0"}\<close>
1.442  function negDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
1.443    "negDivAlg a b = (if 0 \<le>a + b \<or> b \<le> 0  then (-1, a + b)
1.444       else adjust b (negDivAlg a (2 * b)))"
1.445 @@ -1647,12 +1647,12 @@
1.446  termination by (relation "measure (\<lambda>(a, b). nat (- a - b))")
1.448
1.449 -text{*algorithm for the general case @{term "b\<noteq>0"}*}
1.450 +text\<open>algorithm for the general case @{term "b\<noteq>0"}\<close>
1.451
1.452  definition divmod_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
1.453 -    --{*The full division algorithm considers all possible signs for a, b
1.454 +    --\<open>The full division algorithm considers all possible signs for a, b
1.455         including the special case @{text "a=0, b<0"} because
1.456 -       @{term negDivAlg} requires @{term "a<0"}.*}
1.457 +       @{term negDivAlg} requires @{term "a<0"}.\<close>
1.458    "divmod_int a b = (if 0 \<le> a then if 0 \<le> b then posDivAlg a b
1.459                    else if a = 0 then (0, 0)
1.460                         else apsnd uminus (negDivAlg (-a) (-b))
1.461 @@ -1681,7 +1681,7 @@
1.462    "divmod_int p q = (p div q, p mod q)"
1.464
1.465 -text{*
1.466 +text\<open>
1.467  Here is the division algorithm in ML:
1.468
1.469  \begin{verbatim}
1.470 @@ -1707,10 +1707,10 @@
1.471                            if 0<b then negDivAlg (a,b)
1.472                            else        negateSnd (posDivAlg (~a,~b));
1.473  \end{verbatim}
1.474 -*}
1.475 -
1.476 -
1.477 -subsubsection {* Uniqueness and Monotonicity of Quotients and Remainders *}
1.478 +\<close>
1.479 +
1.480 +
1.481 +subsubsection \<open>Uniqueness and Monotonicity of Quotients and Remainders\<close>
1.482
1.483  lemma unique_quotient_lemma:
1.484       "[| b*q' + r'  \<le> b*q + r;  0 \<le> r';  r' < b;  r < b |]
1.485 @@ -1750,9 +1750,9 @@
1.486  done
1.487
1.488
1.489 -subsubsection {* Correctness of @{term posDivAlg}, the Algorithm for Non-Negative Dividends *}
1.490 -
1.491 -text{*And positive divisors*}
1.492 +subsubsection \<open>Correctness of @{term posDivAlg}, the Algorithm for Non-Negative Dividends\<close>
1.493 +
1.494 +text\<open>And positive divisors\<close>
1.495
1.497       "adjust b (q, r) =
1.498 @@ -1763,13 +1763,13 @@
1.499
1.500  declare posDivAlg.simps [simp del]
1.501
1.502 -text{*use with a simproc to avoid repeatedly proving the premise*}
1.503 +text\<open>use with a simproc to avoid repeatedly proving the premise\<close>
1.504  lemma posDivAlg_eqn:
1.505       "0 < b ==>
1.506        posDivAlg a b = (if a<b then (0,a) else adjust b (posDivAlg a (2*b)))"
1.507  by (rule posDivAlg.simps [THEN trans], simp)
1.508
1.509 -text{*Correctness of @{term posDivAlg}: it computes quotients correctly*}
1.510 +text\<open>Correctness of @{term posDivAlg}: it computes quotients correctly\<close>
1.511  theorem posDivAlg_correct:
1.512    assumes "0 \<le> a" and "0 < b"
1.513    shows "divmod_int_rel a b (posDivAlg a b)"
1.514 @@ -1785,13 +1785,13 @@
1.515    done
1.516
1.517
1.518 -subsubsection {* Correctness of @{term negDivAlg}, the Algorithm for Negative Dividends *}
1.519 -
1.520 -text{*And positive divisors*}
1.521 +subsubsection \<open>Correctness of @{term negDivAlg}, the Algorithm for Negative Dividends\<close>
1.522 +
1.523 +text\<open>And positive divisors\<close>
1.524
1.525  declare negDivAlg.simps [simp del]
1.526
1.527 -text{*use with a simproc to avoid repeatedly proving the premise*}
1.528 +text\<open>use with a simproc to avoid repeatedly proving the premise\<close>
1.529  lemma negDivAlg_eqn:
1.530       "0 < b ==>
1.531        negDivAlg a b =
1.532 @@ -1815,7 +1815,7 @@
1.533    done
1.534
1.535
1.536 -subsubsection {* Existence Shown by Proving the Division Algorithm to be Correct *}
1.537 +subsubsection \<open>Existence Shown by Proving the Division Algorithm to be Correct\<close>
1.538
1.539  (*the case a=0*)
1.540  lemma divmod_int_rel_0: "divmod_int_rel 0 b (0, 0)"
1.541 @@ -1916,14 +1916,14 @@
1.542
1.543  end
1.544
1.545 -text{*Basic laws about division and remainder*}
1.546 +text\<open>Basic laws about division and remainder\<close>
1.547
1.548  lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
1.549    by (fact mod_div_equality2 [symmetric])
1.550
1.551 -text {* Tool setup *}
1.552 -
1.553 -ML {*
1.554 +text \<open>Tool setup\<close>
1.555 +
1.556 +ML \<open>
1.557  structure Cancel_Div_Mod_Int = Cancel_Div_Mod
1.558  (
1.559    val div_name = @{const_name Rings.divide};
1.560 @@ -1937,9 +1937,9 @@
1.561    val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
1.563  )
1.564 -*}
1.565 -
1.566 -simproc_setup cancel_div_mod_int ("(k::int) + l") = {* K Cancel_Div_Mod_Int.proc *}
1.567 +\<close>
1.568 +
1.569 +simproc_setup cancel_div_mod_int ("(k::int) + l") = \<open>K Cancel_Div_Mod_Int.proc\<close>
1.570
1.571  lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
1.572    using divmod_int_correct [of a b]
1.573 @@ -1956,7 +1956,7 @@
1.574     and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
1.575
1.576
1.577 -subsubsection {* General Properties of div and mod *}
1.578 +subsubsection \<open>General Properties of div and mod\<close>
1.579
1.580  lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
1.581  apply (rule div_int_unique)
1.582 @@ -1990,10 +1990,10 @@
1.583  apply (auto simp add: divmod_int_rel_def)
1.584  done
1.585
1.586 -text{*There is no @{text mod_neg_pos_trivial}.*}
1.587 -
1.588 -
1.589 -subsubsection {* Laws for div and mod with Unary Minus *}
1.590 +text\<open>There is no @{text mod_neg_pos_trivial}.\<close>
1.591 +
1.592 +
1.593 +subsubsection \<open>Laws for div and mod with Unary Minus\<close>
1.594
1.595  lemma zminus1_lemma:
1.596       "divmod_int_rel a b (q, r) ==> b \<noteq> 0
1.597 @@ -2035,7 +2035,7 @@
1.598    unfolding zmod_zminus2_eq_if by auto
1.599
1.600
1.601 -subsubsection {* Computation of Division and Remainder *}
1.602 +subsubsection \<open>Computation of Division and Remainder\<close>
1.603
1.604  lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
1.605  by (simp add: div_int_def divmod_int_def)
1.606 @@ -2043,7 +2043,7 @@
1.607  lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
1.608  by (simp add: mod_int_def divmod_int_def)
1.609
1.610 -text{*a positive, b positive *}
1.611 +text\<open>a positive, b positive\<close>
1.612
1.613  lemma div_pos_pos: "[| 0 < a;  0 \<le> b |] ==> a div b = fst (posDivAlg a b)"
1.614  by (simp add: div_int_def divmod_int_def)
1.615 @@ -2051,7 +2051,7 @@
1.616  lemma mod_pos_pos: "[| 0 < a;  0 \<le> b |] ==> a mod b = snd (posDivAlg a b)"
1.617  by (simp add: mod_int_def divmod_int_def)
1.618
1.619 -text{*a negative, b positive *}
1.620 +text\<open>a negative, b positive\<close>
1.621
1.622  lemma div_neg_pos: "[| a < 0;  0 < b |] ==> a div b = fst (negDivAlg a b)"
1.623  by (simp add: div_int_def divmod_int_def)
1.624 @@ -2059,7 +2059,7 @@
1.625  lemma mod_neg_pos: "[| a < 0;  0 < b |] ==> a mod b = snd (negDivAlg a b)"
1.626  by (simp add: mod_int_def divmod_int_def)
1.627
1.628 -text{*a positive, b negative *}
1.629 +text\<open>a positive, b negative\<close>
1.630
1.631  lemma div_pos_neg:
1.632       "[| 0 < a;  b < 0 |] ==> a div b = fst (apsnd uminus (negDivAlg (-a) (-b)))"
1.633 @@ -2069,7 +2069,7 @@
1.634       "[| 0 < a;  b < 0 |] ==> a mod b = snd (apsnd uminus (negDivAlg (-a) (-b)))"
1.635  by (simp add: mod_int_def divmod_int_def)
1.636
1.637 -text{*a negative, b negative *}
1.638 +text\<open>a negative, b negative\<close>
1.639
1.640  lemma div_neg_neg:
1.641       "[| a < 0;  b \<le> 0 |] ==> a div b = fst (apsnd uminus (posDivAlg (-a) (-b)))"
1.642 @@ -2079,7 +2079,7 @@
1.643       "[| a < 0;  b \<le> 0 |] ==> a mod b = snd (apsnd uminus (posDivAlg (-a) (-b)))"
1.644  by (simp add: mod_int_def divmod_int_def)
1.645
1.646 -text {*Simplify expresions in which div and mod combine numerical constants*}
1.647 +text \<open>Simplify expresions in which div and mod combine numerical constants\<close>
1.648
1.649  lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
1.650    by (rule div_int_unique [of a b q r]) (simp add: divmod_int_rel_def)
1.651 @@ -2096,12 +2096,12 @@
1.652    by (rule mod_int_unique [of a b q r],
1.654
1.655 -text {*
1.656 +text \<open>
1.657    numeral simprocs -- high chance that these can be replaced
1.658    by divmod algorithm from @{class semiring_numeral_div}
1.659 -*}
1.660 -
1.661 -ML {*
1.662 +\<close>
1.663 +
1.664 +ML \<open>
1.665  local
1.666    val mk_number = HOLogic.mk_number HOLogic.intT
1.667    val plus = @{term "plus :: int \<Rightarrow> int \<Rightarrow> int"}
1.668 @@ -2133,21 +2133,21 @@
1.669              else (le $r$ zero, less $u$ r, negrule RS eq_reflection)
1.670          in SOME (rule OF map (prove ctxt) [goal1, goal2, goal3]) end)
1.671  end
1.672 -*}
1.673 +\<close>
1.674
1.675  simproc_setup binary_int_div
1.676    ("numeral m div numeral n :: int" |
1.677     "numeral m div - numeral n :: int" |
1.678     "- numeral m div numeral n :: int" |
1.679     "- numeral m div - numeral n :: int") =
1.680 -  {* K (divmod_proc @{thm int_div_pos_eq} @{thm int_div_neg_eq}) *}
1.681 +  \<open>K (divmod_proc @{thm int_div_pos_eq} @{thm int_div_neg_eq})\<close>
1.682
1.683  simproc_setup binary_int_mod
1.684    ("numeral m mod numeral n :: int" |
1.685     "numeral m mod - numeral n :: int" |
1.686     "- numeral m mod numeral n :: int" |
1.687     "- numeral m mod - numeral n :: int") =
1.688 -  {* K (divmod_proc @{thm int_mod_pos_eq} @{thm int_mod_neg_eq}) *}
1.689 +  \<open>K (divmod_proc @{thm int_mod_pos_eq} @{thm int_mod_neg_eq})\<close>
1.690
1.691  lemmas posDivAlg_eqn_numeral [simp] =
1.692      posDivAlg_eqn [of "numeral v" "numeral w", OF zero_less_numeral] for v w
1.693 @@ -2156,7 +2156,7 @@
1.694      negDivAlg_eqn [of "numeral v" "- numeral w", OF zero_less_numeral] for v w
1.695
1.696
1.697 -text {* Special-case simplification: @{text "\<plusminus>1 div z"} and @{text "\<plusminus>1 mod z"} *}
1.698 +text \<open>Special-case simplification: @{text "\<plusminus>1 div z"} and @{text "\<plusminus>1 mod z"}\<close>
1.699
1.700  lemma [simp]:
1.701    shows div_one_bit0: "1 div numeral (Num.Bit0 v) = (0 :: int)"
1.702 @@ -2178,7 +2178,7 @@
1.703    by (simp_all add: div_eq_minus1 zmod_minus1)
1.704
1.705
1.706 -subsubsection {* Monotonicity in the First Argument (Dividend) *}
1.707 +subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
1.708
1.709  lemma zdiv_mono1: "[| a \<le> a';  0 < (b::int) |] ==> a div b \<le> a' div b"
1.710  apply (cut_tac a = a and b = b in zmod_zdiv_equality)
1.711 @@ -2197,7 +2197,7 @@
1.712  done
1.713
1.714
1.715 -subsubsection {* Monotonicity in the Second Argument (Divisor) *}
1.716 +subsubsection \<open>Monotonicity in the Second Argument (Divisor)\<close>
1.717
1.718  lemma q_pos_lemma:
1.719       "[| 0 \<le> b'*q' + r'; r' < b';  0 < b' |] ==> 0 \<le> (q'::int)"
1.720 @@ -2259,9 +2259,9 @@
1.721  done
1.722
1.723
1.724 -subsubsection {* More Algebraic Laws for div and mod *}
1.725 -
1.726 -text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *}
1.727 +subsubsection \<open>More Algebraic Laws for div and mod\<close>
1.728 +
1.729 +text\<open>proving (a*b) div c = a * (b div c) + a * (b mod c)\<close>
1.730
1.731  lemma zmult1_lemma:
1.732       "[| divmod_int_rel b c (q, r) |]
1.733 @@ -2273,7 +2273,7 @@
1.734  apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN div_int_unique])
1.735  done
1.736
1.737 -text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
1.738 +text\<open>proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c)\<close>
1.739
1.741       "[| divmod_int_rel a c (aq, ar);  divmod_int_rel b c (bq, br) |]
1.742 @@ -2325,13 +2325,13 @@
1.743    using mod_div_equality [of m n] by arith
1.744
1.745
1.746 -subsubsection {* Proving  @{term "a div (b * c) = (a div b) div c"} *}
1.747 +subsubsection \<open>Proving  @{term "a div (b * c) = (a div b) div c"}\<close>
1.748
1.749  (*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but
1.750    7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems
1.751    to cause particular problems.*)
1.752
1.753 -text{*first, four lemmas to bound the remainder for the cases b<0 and b>0 *}
1.754 +text\<open>first, four lemmas to bound the remainder for the cases b<0 and b>0\<close>
1.755
1.756  lemma zmult2_lemma_aux1: "[| (0::int) < c;  b < r;  r \<le> 0 |] ==> b * c < b * (q mod c) + r"
1.757  apply (subgoal_tac "b * (c - q mod c) < r * 1")
1.758 @@ -2409,9 +2409,9 @@
1.759  qed
1.760
1.761
1.762 -subsubsection {* Splitting Rules for div and mod *}
1.763 -
1.764 -text{*The proofs of the two lemmas below are essentially identical*}
1.765 +subsubsection \<open>Splitting Rules for div and mod\<close>
1.766 +
1.767 +text\<open>The proofs of the two lemmas below are essentially identical\<close>
1.768
1.769  lemma split_pos_lemma:
1.770   "0<k ==>
1.771 @@ -2421,7 +2421,7 @@
1.774   apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)
1.775 -txt{*converse direction*}
1.776 +txt\<open>converse direction\<close>
1.777  apply (drule_tac x = "n div k" in spec)
1.778  apply (drule_tac x = "n mod k" in spec, simp)
1.779  done
1.780 @@ -2434,7 +2434,7 @@
1.783   apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)
1.784 -txt{*converse direction*}
1.785 +txt\<open>converse direction\<close>
1.786  apply (drule_tac x = "n div k" in spec)
1.787  apply (drule_tac x = "n mod k" in spec, simp)
1.788  done
1.789 @@ -2463,14 +2463,14 @@
1.790                        split_neg_lemma [of concl: "%x y. P y"])
1.791  done
1.792
1.793 -text {* Enable (lin)arith to deal with @{const divide} and @{const mod}
1.794 +text \<open>Enable (lin)arith to deal with @{const divide} and @{const mod}
1.795    when these are applied to some constant that is of the form
1.796 -  @{term "numeral k"}: *}
1.797 +  @{term "numeral k"}:\<close>
1.798  declare split_zdiv [of _ _ "numeral k", arith_split] for k
1.799  declare split_zmod [of _ _ "numeral k", arith_split] for k
1.800
1.801
1.802 -subsubsection {* Computing @{text "div"} and @{text "mod"} with shifting *}
1.803 +subsubsection \<open>Computing @{text "div"} and @{text "mod"} with shifting\<close>
1.804
1.805  lemma pos_divmod_int_rel_mult_2:
1.806    assumes "0 \<le> b"
1.807 @@ -2478,7 +2478,7 @@
1.808    shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"
1.809    using assms unfolding divmod_int_rel_def by auto
1.810
1.811 -declaration {* K (Lin_Arith.add_simps @{thms uminus_numeral_One}) *}
1.812 +declaration \<open>K (Lin_Arith.add_simps @{thms uminus_numeral_One})\<close>
1.813
1.814  lemma neg_divmod_int_rel_mult_2:
1.815    assumes "b \<le> 0"
1.816 @@ -2486,7 +2486,7 @@
1.817    shows "divmod_int_rel (1 + 2*a) (2*b) (q, 2*r - 1)"
1.818    using assms unfolding divmod_int_rel_def by auto
1.819
1.820 -text{*computing div by shifting *}
1.821 +text\<open>computing div by shifting\<close>
1.822
1.823  lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
1.824    using pos_divmod_int_rel_mult_2 [OF _ divmod_int_rel_div_mod]
1.825 @@ -2544,14 +2544,14 @@
1.826  proof
1.827    assume ?L
1.828    have "?L \<longrightarrow> ?R" by (rule split_zdiv[THEN iffD2]) simp
1.829 -  with ?L show ?R by blast
1.830 +  with \<open>?L\<close> show ?R by blast
1.831  next
1.832    assume ?R thus ?L
1.833      by(auto simp: div_pos_pos_trivial div_neg_neg_trivial)
1.834  qed
1.835
1.836
1.837 -subsubsection {* Quotients of Signs *}
1.838 +subsubsection \<open>Quotients of Signs\<close>
1.839
1.840  lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"
1.841  apply (subgoal_tac "a div b \<le> -1", force)
1.842 @@ -2566,9 +2566,9 @@
1.843  lemma div_nonpos_pos_le0: "[| (a::int) \<le> 0; b > 0 |] ==> a div b \<le> 0"
1.844  by (drule zdiv_mono1, auto)
1.845
1.846 -text{* Now for some equivalences of the form @{text"a div b >=< 0 \<longleftrightarrow> \<dots>"}
1.847 +text\<open>Now for some equivalences of the form @{text"a div b >=< 0 \<longleftrightarrow> \<dots>"}
1.848  conditional upon the sign of @{text a} or @{text b}. There are many more.
1.849 -They should all be simp rules unless that causes too much search. *}
1.850 +They should all be simp rules unless that causes too much search.\<close>
1.851
1.852  lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"
1.853  apply auto
1.854 @@ -2613,14 +2613,14 @@
1.855  done
1.856
1.857
1.858 -subsubsection {* The Divides Relation *}
1.859 +subsubsection \<open>The Divides Relation\<close>
1.860
1.861  lemma dvd_eq_mod_eq_0_numeral:
1.862    "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semiring_div)"
1.863    by (fact dvd_eq_mod_eq_0)
1.864
1.865
1.866 -subsubsection {* Further properties *}
1.867 +subsubsection \<open>Further properties\<close>
1.868
1.869  lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
1.870    using zmod_zdiv_equality[where a="m" and b="n"]
1.871 @@ -2650,7 +2650,7 @@
1.872  lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"
1.873  by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
1.874
1.875 -text{*Suggested by Matthias Daum*}
1.876 +text\<open>Suggested by Matthias Daum\<close>
1.877  lemma int_power_div_base:
1.878       "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
1.879  apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)")
1.880 @@ -2659,7 +2659,7 @@
1.881   apply simp_all
1.882  done
1.883
1.884 -text {* by Brian Huffman *}
1.885 +text \<open>by Brian Huffman\<close>
1.886  lemma zminus_zmod: "- ((x::int) mod m) mod m = - x mod m"
1.887  by (rule mod_minus_eq [symmetric])
1.888
1.889 @@ -2677,7 +2677,7 @@
1.890    power_mod
1.891    zminus_zmod zdiff_zmod_left zdiff_zmod_right
1.892
1.893 -text {* Distributive laws for function @{text nat}. *}
1.894 +text \<open>Distributive laws for function @{text nat}.\<close>
1.895
1.896  lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"
1.897  apply (rule linorder_cases [of y 0])
1.898 @@ -2693,7 +2693,7 @@
1.899  apply (simp add: nat_eq_iff zmod_int)
1.900  done
1.901
1.902 -text  {* transfer setup *}
1.903 +text  \<open>transfer setup\<close>
1.904
1.905  lemma transfer_nat_int_functions:
1.906      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
1.907 @@ -2729,7 +2729,7 @@
1.908    transfer_int_nat_function_closures
1.909  ]
1.910
1.911 -text{*Suggested by Matthias Daum*}
1.912 +text\<open>Suggested by Matthias Daum\<close>
1.913  lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
1.914  apply (subgoal_tac "nat x div nat k < nat x")
1.915   apply (simp add: nat_div_distrib [symmetric])
1.916 @@ -2781,11 +2781,11 @@
1.917    thus  ?lhs by simp
1.918  qed
1.919
1.920 -text {*
1.921 +text \<open>
1.922    This re-embedding of natural division on integers goes back to the
1.923    time when numerals had been signed numerals.  It should
1.924    now be replaced by the algorithm developed in @{class semiring_numeral_div}.
1.925 -*}
1.926 +\<close>
1.927
1.928  lemma div_nat_numeral [simp]:
1.929    "(numeral v :: nat) div numeral v' = nat (numeral v div numeral v')"
1.930 @@ -2804,14 +2804,14 @@
1.931    by (subst nat_mod_distrib) simp_all
1.932
1.933
1.934 -subsubsection {* Tools setup *}
1.935 -
1.936 -text {* Nitpick *}
1.937 +subsubsection \<open>Tools setup\<close>
1.938 +
1.939 +text \<open>Nitpick\<close>
1.940
1.941  lemmas [nitpick_unfold] = dvd_eq_mod_eq_0 mod_div_equality' zmod_zdiv_equality'
1.942
1.943
1.944 -subsubsection {* Code generation *}
1.945 +subsubsection \<open>Code generation\<close>
1.946
1.947  definition divmod_abs :: "int \<Rightarrow> int \<Rightarrow> int \<times> int"
1.948  where