src/HOL/IntDiv.thy
 changeset 29651 16a19466bf81 parent 29410 97916a925a69 child 29668 33ba3faeaa0e
```     1.1 --- a/src/HOL/IntDiv.thy	Tue Jan 27 19:56:26 2009 +0100
1.2 +++ b/src/HOL/IntDiv.thy	Wed Jan 28 11:02:11 2009 +0100
1.3 @@ -1,82 +1,69 @@
1.4  (*  Title:      HOL/IntDiv.thy
1.5 -    ID:         \$Id\$
1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.7      Copyright   1999  University of Cambridge
1.8
1.9  *)
1.10
1.11 -header{*The Division Operators div and mod; the Divides Relation dvd*}
1.12 +header{* The Division Operators div and mod *}
1.13
1.14  theory IntDiv
1.15  imports Int Divides FunDef
1.16  begin
1.17
1.18 -constdefs
1.19 -  quorem :: "(int*int) * (int*int) => bool"
1.20 +definition divmod_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where
1.21      --{*definition of quotient and remainder*}
1.22 -    [code]: "quorem == %((a,b), (q,r)).
1.23 -                      a = b*q + r &
1.24 -                      (if 0 < b then 0\<le>r & r<b else b<r & r \<le> 0)"
1.25 +    [code]: "divmod_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
1.26 +               (if 0 < b then 0 \<le> r \<and> r < b else b < r \<and> r \<le> 0))"
1.27
1.28 -  adjust :: "[int, int*int] => int*int"
1.29 +definition adjust :: "int \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int" where
1.30      --{*for the division algorithm*}
1.31 -    [code]: "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
1.32 -                         else (2*q, r)"
1.33 +    [code]: "adjust b = (\<lambda>(q, r). if 0 \<le> r - b then (2 * q + 1, r - b)
1.34 +                         else (2 * q, r))"
1.35
1.36  text{*algorithm for the case @{text "a\<ge>0, b>0"}*}
1.37 -function
1.38 -  posDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int"
1.39 -where
1.40 -  "posDivAlg a b =
1.41 -     (if (a<b | b\<le>0) then (0,a)
1.42 -        else adjust b (posDivAlg a (2*b)))"
1.43 +function posDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
1.44 +  "posDivAlg a b = (if a < b \<or>  b \<le> 0 then (0, a)
1.45 +     else adjust b (posDivAlg a (2 * b)))"
1.46  by auto
1.47 -termination by (relation "measure (%(a,b). nat(a - b + 1))") auto
1.48 +termination by (relation "measure (\<lambda>(a, b). nat (a - b + 1))") auto
1.49
1.50  text{*algorithm for the case @{text "a<0, b>0"}*}
1.51 -function
1.52 -  negDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int"
1.53 -where
1.54 -  "negDivAlg a b  =
1.55 -     (if (0\<le>a+b | b\<le>0) then (-1,a+b)
1.56 -      else adjust b (negDivAlg a (2*b)))"
1.57 +function negDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
1.58 +  "negDivAlg a b = (if 0 \<le>a + b \<or> b \<le> 0  then (-1, a + b)
1.59 +     else adjust b (negDivAlg a (2 * b)))"
1.60  by auto
1.61 -termination by (relation "measure (%(a,b). nat(- a - b))") auto
1.62 +termination by (relation "measure (\<lambda>(a, b). nat (- a - b))") auto
1.63
1.64  text{*algorithm for the general case @{term "b\<noteq>0"}*}
1.65 -constdefs
1.66 -  negateSnd :: "int*int => int*int"
1.67 -    [code]: "negateSnd == %(q,r). (q,-r)"
1.68 +definition negateSnd :: "int \<times> int \<Rightarrow> int \<times> int" where
1.69 +  [code inline]: "negateSnd = apsnd uminus"
1.70
1.71 -definition
1.72 -  divAlg :: "int \<times> int \<Rightarrow> int \<times> int"
1.73 +definition divmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
1.74      --{*The full division algorithm considers all possible signs for a, b
1.75         including the special case @{text "a=0, b<0"} because
1.76         @{term negDivAlg} requires @{term "a<0"}.*}
1.77 -where
1.78 -  "divAlg = (\<lambda>(a, b). (if 0\<le>a then
1.79 -                  if 0\<le>b then posDivAlg a b
1.80 -                  else if a=0 then (0, 0)
1.81 +  "divmod a b = (if 0 \<le> a then if 0 \<le> b then posDivAlg a b
1.82 +                  else if a = 0 then (0, 0)
1.83                         else negateSnd (negDivAlg (-a) (-b))
1.84                 else
1.85 -                  if 0<b then negDivAlg a b
1.86 -                  else negateSnd (posDivAlg (-a) (-b))))"
1.87 +                  if 0 < b then negDivAlg a b
1.88 +                  else negateSnd (posDivAlg (-a) (-b)))"
1.89
1.90  instantiation int :: Divides.div
1.91  begin
1.92
1.93  definition
1.94 -  div_def: "a div b = fst (divAlg (a, b))"
1.95 +  div_def: "a div b = fst (divmod a b)"
1.96
1.97  definition
1.98 -  mod_def: "a mod b = snd (divAlg (a, b))"
1.99 +  mod_def: "a mod b = snd (divmod a b)"
1.100
1.101  instance ..
1.102
1.103  end
1.104
1.105 -lemma divAlg_mod_div:
1.106 -  "divAlg (p, q) = (p div q, p mod q)"
1.107 +lemma divmod_mod_div:
1.108 +  "divmod p q = (p div q, p mod q)"
1.109    by (auto simp add: div_def mod_def)
1.110
1.111  text{*
1.112 @@ -97,7 +84,7 @@
1.113
1.114      fun negateSnd (q,r:int) = (q,~r);
1.115
1.116 -    fun divAlg (a,b) = if 0\<le>a then
1.117 +    fun divmod (a,b) = if 0\<le>a then
1.118  			  if b>0 then posDivAlg (a,b)
1.119  			   else if a=0 then (0,0)
1.120  				else negateSnd (negDivAlg (~a,~b))
1.121 @@ -131,9 +118,9 @@
1.122      auto)
1.123
1.124  lemma unique_quotient:
1.125 -     "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  b \<noteq> 0 |]
1.126 +     "[| divmod_rel a b (q, r); divmod_rel a b (q', r');  b \<noteq> 0 |]
1.127        ==> q = q'"
1.128 -apply (simp add: quorem_def linorder_neq_iff split: split_if_asm)
1.129 +apply (simp add: divmod_rel_def linorder_neq_iff split: split_if_asm)
1.130  apply (blast intro: order_antisym
1.131               dest: order_eq_refl [THEN unique_quotient_lemma]
1.132               order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
1.133 @@ -141,10 +128,10 @@
1.134
1.135
1.136  lemma unique_remainder:
1.137 -     "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  b \<noteq> 0 |]
1.138 +     "[| divmod_rel a b (q, r); divmod_rel a b (q', r');  b \<noteq> 0 |]
1.139        ==> r = r'"
1.140  apply (subgoal_tac "q = q'")
1.141 - apply (simp add: quorem_def)
1.142 + apply (simp add: divmod_rel_def)
1.143  apply (blast intro: unique_quotient)
1.144  done
1.145
1.146 @@ -171,10 +158,10 @@
1.147  text{*Correctness of @{term posDivAlg}: it computes quotients correctly*}
1.148  theorem posDivAlg_correct:
1.149    assumes "0 \<le> a" and "0 < b"
1.150 -  shows "quorem ((a, b), posDivAlg a b)"
1.151 +  shows "divmod_rel a b (posDivAlg a b)"
1.152  using prems apply (induct a b rule: posDivAlg.induct)
1.153  apply auto
1.156  apply (subst posDivAlg_eqn, simp add: right_distrib)
1.157  apply (case_tac "a < b")
1.158  apply simp_all
1.159 @@ -200,10 +187,10 @@
1.160    It doesn't work if a=0 because the 0/b equals 0, not -1*)
1.161  lemma negDivAlg_correct:
1.162    assumes "a < 0" and "b > 0"
1.163 -  shows "quorem ((a, b), negDivAlg a b)"
1.164 +  shows "divmod_rel a b (negDivAlg a b)"
1.165  using prems apply (induct a b rule: negDivAlg.induct)
1.166  apply (auto simp add: linorder_not_le)
1.169  apply (subst negDivAlg_eqn, assumption)
1.170  apply (case_tac "a + b < (0\<Colon>int)")
1.171  apply simp_all
1.172 @@ -215,8 +202,8 @@
1.173  subsection{*Existence Shown by Proving the Division Algorithm to be Correct*}
1.174
1.175  (*the case a=0*)
1.176 -lemma quorem_0: "b \<noteq> 0 ==> quorem ((0,b), (0,0))"
1.177 -by (auto simp add: quorem_def linorder_neq_iff)
1.178 +lemma divmod_rel_0: "b \<noteq> 0 ==> divmod_rel 0 b (0, 0)"
1.179 +by (auto simp add: divmod_rel_def linorder_neq_iff)
1.180
1.181  lemma posDivAlg_0 [simp]: "posDivAlg 0 b = (0, 0)"
1.182  by (subst posDivAlg.simps, auto)
1.183 @@ -227,26 +214,26 @@
1.184  lemma negateSnd_eq [simp]: "negateSnd(q,r) = (q,-r)"
1.186
1.187 -lemma quorem_neg: "quorem ((-a,-b), qr) ==> quorem ((a,b), negateSnd qr)"
1.188 -by (auto simp add: split_ifs quorem_def)
1.189 +lemma divmod_rel_neg: "divmod_rel (-a) (-b) qr ==> divmod_rel a b (negateSnd qr)"
1.190 +by (auto simp add: split_ifs divmod_rel_def)
1.191
1.192 -lemma divAlg_correct: "b \<noteq> 0 ==> quorem ((a,b), divAlg (a, b))"
1.193 -by (force simp add: linorder_neq_iff quorem_0 divAlg_def quorem_neg
1.194 +lemma divmod_correct: "b \<noteq> 0 ==> divmod_rel a b (divmod a b)"
1.195 +by (force simp add: linorder_neq_iff divmod_rel_0 divmod_def divmod_rel_neg
1.196                      posDivAlg_correct negDivAlg_correct)
1.197
1.198  text{*Arbitrary definitions for division by zero.  Useful to simplify
1.199      certain equations.*}
1.200
1.201  lemma DIVISION_BY_ZERO [simp]: "a div (0::int) = 0 & a mod (0::int) = a"
1.202 -by (simp add: div_def mod_def divAlg_def posDivAlg.simps)
1.203 +by (simp add: div_def mod_def divmod_def posDivAlg.simps)
1.204
1.205
1.206  text{*Basic laws about division and remainder*}
1.207
1.208  lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
1.209  apply (case_tac "b = 0", simp)
1.210 -apply (cut_tac a = a and b = b in divAlg_correct)
1.211 -apply (auto simp add: quorem_def div_def mod_def)
1.212 +apply (cut_tac a = a and b = b in divmod_correct)
1.213 +apply (auto simp add: divmod_rel_def div_def mod_def)
1.214  done
1.215
1.216  lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k"
1.217 @@ -288,16 +275,16 @@
1.218  *}
1.219
1.220  lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b"
1.221 -apply (cut_tac a = a and b = b in divAlg_correct)
1.222 -apply (auto simp add: quorem_def mod_def)
1.223 +apply (cut_tac a = a and b = b in divmod_correct)
1.224 +apply (auto simp add: divmod_rel_def mod_def)
1.225  done
1.226
1.227  lemmas pos_mod_sign  [simp] = pos_mod_conj [THEN conjunct1, standard]
1.228     and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2, standard]
1.229
1.230  lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b"
1.231 -apply (cut_tac a = a and b = b in divAlg_correct)
1.232 -apply (auto simp add: quorem_def div_def mod_def)
1.233 +apply (cut_tac a = a and b = b in divmod_correct)
1.234 +apply (auto simp add: divmod_rel_def div_def mod_def)
1.235  done
1.236
1.237  lemmas neg_mod_sign  [simp] = neg_mod_conj [THEN conjunct1, standard]
1.238 @@ -307,47 +294,47 @@
1.239
1.240  subsection{*General Properties of div and mod*}
1.241
1.242 -lemma quorem_div_mod: "b \<noteq> 0 ==> quorem ((a, b), (a div b, a mod b))"
1.243 +lemma divmod_rel_div_mod: "b \<noteq> 0 ==> divmod_rel a b (a div b, a mod b)"
1.244  apply (cut_tac a = a and b = b in zmod_zdiv_equality)
1.245 -apply (force simp add: quorem_def linorder_neq_iff)
1.246 +apply (force simp add: divmod_rel_def linorder_neq_iff)
1.247  done
1.248
1.249 -lemma quorem_div: "[| quorem((a,b),(q,r));  b \<noteq> 0 |] ==> a div b = q"
1.250 -by (simp add: quorem_div_mod [THEN unique_quotient])
1.251 +lemma divmod_rel_div: "[| divmod_rel a b (q, r);  b \<noteq> 0 |] ==> a div b = q"
1.252 +by (simp add: divmod_rel_div_mod [THEN unique_quotient])
1.253
1.254 -lemma quorem_mod: "[| quorem((a,b),(q,r));  b \<noteq> 0 |] ==> a mod b = r"
1.255 -by (simp add: quorem_div_mod [THEN unique_remainder])
1.256 +lemma divmod_rel_mod: "[| divmod_rel a b (q, r);  b \<noteq> 0 |] ==> a mod b = r"
1.257 +by (simp add: divmod_rel_div_mod [THEN unique_remainder])
1.258
1.259  lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
1.260 -apply (rule quorem_div)
1.261 -apply (auto simp add: quorem_def)
1.262 +apply (rule divmod_rel_div)
1.263 +apply (auto simp add: divmod_rel_def)
1.264  done
1.265
1.266  lemma div_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a div b = 0"
1.267 -apply (rule quorem_div)
1.268 -apply (auto simp add: quorem_def)
1.269 +apply (rule divmod_rel_div)
1.270 +apply (auto simp add: divmod_rel_def)
1.271  done
1.272
1.273  lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"
1.274 -apply (rule quorem_div)
1.275 -apply (auto simp add: quorem_def)
1.276 +apply (rule divmod_rel_div)
1.277 +apply (auto simp add: divmod_rel_def)
1.278  done
1.279
1.280  (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
1.281
1.282  lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
1.283 -apply (rule_tac q = 0 in quorem_mod)
1.284 -apply (auto simp add: quorem_def)
1.285 +apply (rule_tac q = 0 in divmod_rel_mod)
1.286 +apply (auto simp add: divmod_rel_def)
1.287  done
1.288
1.289  lemma mod_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a mod b = a"
1.290 -apply (rule_tac q = 0 in quorem_mod)
1.291 -apply (auto simp add: quorem_def)
1.292 +apply (rule_tac q = 0 in divmod_rel_mod)
1.293 +apply (auto simp add: divmod_rel_def)
1.294  done
1.295
1.296  lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
1.297 -apply (rule_tac q = "-1" in quorem_mod)
1.298 -apply (auto simp add: quorem_def)
1.299 +apply (rule_tac q = "-1" in divmod_rel_mod)
1.300 +apply (auto simp add: divmod_rel_def)
1.301  done
1.302
1.303  text{*There is no @{text mod_neg_pos_trivial}.*}
1.304 @@ -356,15 +343,15 @@
1.305  (*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*)
1.306  lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)"
1.307  apply (case_tac "b = 0", simp)
1.308 -apply (simp add: quorem_div_mod [THEN quorem_neg, simplified,
1.309 -                                 THEN quorem_div, THEN sym])
1.310 +apply (simp add: divmod_rel_div_mod [THEN divmod_rel_neg, simplified,
1.311 +                                 THEN divmod_rel_div, THEN sym])
1.312
1.313  done
1.314
1.315  (*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*)
1.316  lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))"
1.317  apply (case_tac "b = 0", simp)
1.318 -apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_mod],
1.319 +apply (subst divmod_rel_div_mod [THEN divmod_rel_neg, simplified, THEN divmod_rel_mod],
1.320         auto)
1.321  done
1.322
1.323 @@ -372,22 +359,22 @@
1.324  subsection{*Laws for div and mod with Unary Minus*}
1.325
1.326  lemma zminus1_lemma:
1.327 -     "quorem((a,b),(q,r))
1.328 -      ==> quorem ((-a,b), (if r=0 then -q else -q - 1),
1.329 -                          (if r=0 then 0 else b-r))"
1.330 -by (force simp add: split_ifs quorem_def linorder_neq_iff right_diff_distrib)
1.331 +     "divmod_rel a b (q, r)
1.332 +      ==> divmod_rel (-a) b (if r=0 then -q else -q - 1,
1.333 +                          if r=0 then 0 else b-r)"
1.334 +by (force simp add: split_ifs divmod_rel_def linorder_neq_iff right_diff_distrib)
1.335
1.336
1.337  lemma zdiv_zminus1_eq_if:
1.338       "b \<noteq> (0::int)
1.339        ==> (-a) div b =
1.340            (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
1.341 -by (blast intro: quorem_div_mod [THEN zminus1_lemma, THEN quorem_div])
1.342 +by (blast intro: divmod_rel_div_mod [THEN zminus1_lemma, THEN divmod_rel_div])
1.343
1.344  lemma zmod_zminus1_eq_if:
1.345       "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
1.346  apply (case_tac "b = 0", simp)
1.347 -apply (blast intro: quorem_div_mod [THEN zminus1_lemma, THEN quorem_mod])
1.348 +apply (blast intro: divmod_rel_div_mod [THEN zminus1_lemma, THEN divmod_rel_mod])
1.349  done
1.350
1.351  lemma zdiv_zminus2: "a div (-b) = (-a::int) div b"
1.352 @@ -420,91 +407,91 @@
1.354  done
1.355
1.356 -lemma self_quotient: "[| quorem((a,a),(q,r));  a \<noteq> (0::int) |] ==> q = 1"
1.357 -apply (simp add: split_ifs quorem_def linorder_neq_iff)
1.358 +lemma self_quotient: "[| divmod_rel a a (q, r);  a \<noteq> (0::int) |] ==> q = 1"
1.359 +apply (simp add: split_ifs divmod_rel_def linorder_neq_iff)
1.360  apply (rule order_antisym, safe, simp_all)
1.361  apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1)
1.362  apply (rule_tac a = "-a" and r = "-r" in self_quotient_aux2)
1.364  done
1.365
1.366 -lemma self_remainder: "[| quorem((a,a),(q,r));  a \<noteq> (0::int) |] ==> r = 0"
1.367 +lemma self_remainder: "[| divmod_rel a a (q, r);  a \<noteq> (0::int) |] ==> r = 0"
1.368  apply (frule self_quotient, assumption)
1.371  done
1.372
1.373  lemma zdiv_self [simp]: "a \<noteq> 0 ==> a div a = (1::int)"
1.374 -by (simp add: quorem_div_mod [THEN self_quotient])
1.375 +by (simp add: divmod_rel_div_mod [THEN self_quotient])
1.376
1.377  (*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *)
1.378  lemma zmod_self [simp]: "a mod a = (0::int)"
1.379  apply (case_tac "a = 0", simp)
1.380 -apply (simp add: quorem_div_mod [THEN self_remainder])
1.381 +apply (simp add: divmod_rel_div_mod [THEN self_remainder])
1.382  done
1.383
1.384
1.385  subsection{*Computation of Division and Remainder*}
1.386
1.387  lemma zdiv_zero [simp]: "(0::int) div b = 0"
1.388 -by (simp add: div_def divAlg_def)
1.389 +by (simp add: div_def divmod_def)
1.390
1.391  lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
1.392 -by (simp add: div_def divAlg_def)
1.393 +by (simp add: div_def divmod_def)
1.394
1.395  lemma zmod_zero [simp]: "(0::int) mod b = 0"
1.396 -by (simp add: mod_def divAlg_def)
1.397 +by (simp add: mod_def divmod_def)
1.398
1.399  lemma zdiv_minus1: "(0::int) < b ==> -1 div b = -1"
1.400 -by (simp add: div_def divAlg_def)
1.401 +by (simp add: div_def divmod_def)
1.402
1.403  lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
1.404 -by (simp add: mod_def divAlg_def)
1.405 +by (simp add: mod_def divmod_def)
1.406
1.407  text{*a positive, b positive *}
1.408
1.409  lemma div_pos_pos: "[| 0 < a;  0 \<le> b |] ==> a div b = fst (posDivAlg a b)"
1.410 -by (simp add: div_def divAlg_def)
1.411 +by (simp add: div_def divmod_def)
1.412
1.413  lemma mod_pos_pos: "[| 0 < a;  0 \<le> b |] ==> a mod b = snd (posDivAlg a b)"
1.414 -by (simp add: mod_def divAlg_def)
1.415 +by (simp add: mod_def divmod_def)
1.416
1.417  text{*a negative, b positive *}
1.418
1.419  lemma div_neg_pos: "[| a < 0;  0 < b |] ==> a div b = fst (negDivAlg a b)"
1.420 -by (simp add: div_def divAlg_def)
1.421 +by (simp add: div_def divmod_def)
1.422
1.423  lemma mod_neg_pos: "[| a < 0;  0 < b |] ==> a mod b = snd (negDivAlg a b)"
1.424 -by (simp add: mod_def divAlg_def)
1.425 +by (simp add: mod_def divmod_def)
1.426
1.427  text{*a positive, b negative *}
1.428
1.429  lemma div_pos_neg:
1.430       "[| 0 < a;  b < 0 |] ==> a div b = fst (negateSnd (negDivAlg (-a) (-b)))"
1.431 -by (simp add: div_def divAlg_def)
1.432 +by (simp add: div_def divmod_def)
1.433
1.434  lemma mod_pos_neg:
1.435       "[| 0 < a;  b < 0 |] ==> a mod b = snd (negateSnd (negDivAlg (-a) (-b)))"
1.436 -by (simp add: mod_def divAlg_def)
1.437 +by (simp add: mod_def divmod_def)
1.438
1.439  text{*a negative, b negative *}
1.440
1.441  lemma div_neg_neg:
1.442       "[| a < 0;  b \<le> 0 |] ==> a div b = fst (negateSnd (posDivAlg (-a) (-b)))"
1.443 -by (simp add: div_def divAlg_def)
1.444 +by (simp add: div_def divmod_def)
1.445
1.446  lemma mod_neg_neg:
1.447       "[| a < 0;  b \<le> 0 |] ==> a mod b = snd (negateSnd (posDivAlg (-a) (-b)))"
1.448 -by (simp add: mod_def divAlg_def)
1.449 +by (simp add: mod_def divmod_def)
1.450
1.451  text {*Simplify expresions in which div and mod combine numerical constants*}
1.452
1.453 -lemma quoremI:
1.454 +lemma divmod_relI:
1.455    "\<lbrakk>a == b * q + r; if 0 < b then 0 \<le> r \<and> r < b else b < r \<and> r \<le> 0\<rbrakk>
1.456 -    \<Longrightarrow> quorem ((a, b), (q, r))"
1.457 -  unfolding quorem_def by simp
1.458 +    \<Longrightarrow> divmod_rel a b (q, r)"
1.459 +  unfolding divmod_rel_def by simp
1.460
1.461 -lemmas quorem_div_eq = quoremI [THEN quorem_div, THEN eq_reflection]
1.462 -lemmas quorem_mod_eq = quoremI [THEN quorem_mod, THEN eq_reflection]
1.463 +lemmas divmod_rel_div_eq = divmod_relI [THEN divmod_rel_div, THEN eq_reflection]
1.464 +lemmas divmod_rel_mod_eq = divmod_relI [THEN divmod_rel_mod, THEN eq_reflection]
1.465  lemmas arithmetic_simps =
1.466    arith_simps
1.468 @@ -548,10 +535,10 @@
1.469  *}
1.470
1.471  simproc_setup binary_int_div ("number_of m div number_of n :: int") =
1.472 -  {* K (divmod_proc (@{thm quorem_div_eq})) *}
1.473 +  {* K (divmod_proc (@{thm divmod_rel_div_eq})) *}
1.474
1.475  simproc_setup binary_int_mod ("number_of m mod number_of n :: int") =
1.476 -  {* K (divmod_proc (@{thm quorem_mod_eq})) *}
1.477 +  {* K (divmod_proc (@{thm divmod_rel_mod_eq})) *}
1.478
1.479  (* The following 8 lemmas are made unnecessary by the above simprocs: *)
1.480
1.481 @@ -718,18 +705,18 @@
1.482  text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *}
1.483
1.484  lemma zmult1_lemma:
1.485 -     "[| quorem((b,c),(q,r));  c \<noteq> 0 |]
1.486 -      ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"
1.487 -by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib)
1.488 +     "[| divmod_rel b c (q, r);  c \<noteq> 0 |]
1.489 +      ==> divmod_rel (a * b) c (a*q + a*r div c, a*r mod c)"
1.490 +by (force simp add: split_ifs divmod_rel_def linorder_neq_iff right_distrib)
1.491
1.492  lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
1.493  apply (case_tac "c = 0", simp)
1.494 -apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_div])
1.495 +apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_div])
1.496  done
1.497
1.498  lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)"
1.499  apply (case_tac "c = 0", simp)
1.500 -apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_mod])
1.501 +apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_mod])
1.502  done
1.503
1.504  lemma zmod_zmult1_eq': "(a*b) mod (c::int) = ((a mod c) * b) mod c"
1.505 @@ -760,20 +747,20 @@
1.506  text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
1.507
1.509 -     "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  c \<noteq> 0 |]
1.510 -      ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
1.511 -by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib)
1.512 +     "[| divmod_rel a c (aq, ar);  divmod_rel b c (bq, br);  c \<noteq> 0 |]
1.513 +      ==> divmod_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
1.514 +by (force simp add: split_ifs divmod_rel_def linorder_neq_iff right_distrib)
1.515
1.516  (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
1.518       "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
1.519  apply (case_tac "c = 0", simp)
1.520 -apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_div)
1.521 +apply (blast intro: zadd1_lemma [OF divmod_rel_div_mod divmod_rel_div_mod] divmod_rel_div)
1.522  done
1.523
1.524  lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c"
1.525  apply (case_tac "c = 0", simp)
1.526 -apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)
1.527 +apply (blast intro: zadd1_lemma [OF divmod_rel_div_mod divmod_rel_div_mod] divmod_rel_mod)
1.528  done
1.529
1.530  instance int :: ring_div
1.531 @@ -785,6 +772,33 @@
1.532        by (simp add: zmod_zmult1_eq zmod_zdiv_trivial)
1.533  qed auto
1.534
1.535 +lemma posDivAlg_div_mod:
1.536 +  assumes "k \<ge> 0"
1.537 +  and "l \<ge> 0"
1.538 +  shows "posDivAlg k l = (k div l, k mod l)"
1.539 +proof (cases "l = 0")
1.540 +  case True then show ?thesis by (simp add: posDivAlg.simps)
1.541 +next
1.542 +  case False with assms posDivAlg_correct
1.543 +    have "divmod_rel k l (fst (posDivAlg k l), snd (posDivAlg k l))"
1.544 +    by simp
1.545 +  from divmod_rel_div [OF this `l \<noteq> 0`] divmod_rel_mod [OF this `l \<noteq> 0`]
1.546 +  show ?thesis by simp
1.547 +qed
1.548 +
1.549 +lemma negDivAlg_div_mod:
1.550 +  assumes "k < 0"
1.551 +  and "l > 0"
1.552 +  shows "negDivAlg k l = (k div l, k mod l)"
1.553 +proof -
1.554 +  from assms have "l \<noteq> 0" by simp
1.555 +  from assms negDivAlg_correct
1.556 +    have "divmod_rel k l (fst (negDivAlg k l), snd (negDivAlg k l))"
1.557 +    by simp
1.558 +  from divmod_rel_div [OF this `l \<noteq> 0`] divmod_rel_mod [OF this `l \<noteq> 0`]
1.559 +  show ?thesis by simp
1.560 +qed
1.561 +
1.562  lemma zdiv_zadd_self1: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
1.564
1.565 @@ -862,21 +876,21 @@
1.567  done
1.568
1.569 -lemma zmult2_lemma: "[| quorem ((a,b), (q,r));  b \<noteq> 0;  0 < c |]
1.570 -      ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"
1.571 -by (auto simp add: mult_ac quorem_def linorder_neq_iff
1.572 +lemma zmult2_lemma: "[| divmod_rel a b (q, r);  b \<noteq> 0;  0 < c |]
1.573 +      ==> divmod_rel a (b * c) (q div c, b*(q mod c) + r)"
1.574 +by (auto simp add: mult_ac divmod_rel_def linorder_neq_iff
1.575                     zero_less_mult_iff right_distrib [symmetric]
1.576                     zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4)
1.577
1.578  lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"
1.579  apply (case_tac "b = 0", simp)
1.580 -apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_div])
1.581 +apply (force simp add: divmod_rel_div_mod [THEN zmult2_lemma, THEN divmod_rel_div])
1.582  done
1.583
1.584  lemma zmod_zmult2_eq:
1.585       "(0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b"
1.586  apply (case_tac "b = 0", simp)
1.587 -apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_mod])
1.588 +apply (force simp add: divmod_rel_div_mod [THEN zmult2_lemma, THEN divmod_rel_mod])
1.589  done
1.590
1.591
1.592 @@ -1360,7 +1374,7 @@
1.593  apply (subst split_div, auto)
1.594  apply (subst split_zdiv, auto)
1.595  apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient)
1.596 -apply (auto simp add: IntDiv.quorem_def of_nat_mult)
1.597 +apply (auto simp add: IntDiv.divmod_rel_def of_nat_mult)
1.598  done
1.599
1.600  lemma zmod_int: "int (a mod b) = (int a) mod (int b)"
1.601 @@ -1368,7 +1382,7 @@
1.602  apply (subst split_zmod, auto)
1.603  apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia
1.604         in unique_remainder)
1.605 -apply (auto simp add: IntDiv.quorem_def of_nat_mult)
1.606 +apply (auto simp add: IntDiv.divmod_rel_def of_nat_mult)
1.607  done
1.608
1.609  text{*Suggested by Matthias Daum*}
1.610 @@ -1429,7 +1443,7 @@
1.611  lemma of_int_num [code]:
1.612    "of_int k = (if k = 0 then 0 else if k < 0 then
1.613       - of_int (- k) else let
1.614 -       (l, m) = divAlg (k, 2);
1.615 +       (l, m) = divmod k 2;
1.616         l' = of_int l
1.617       in if m = 0 then l' + l' else l' + l' + 1)"
1.618  proof -
1.619 @@ -1457,7 +1471,7 @@
1.620      show "x * of_int 2 = x + x"
1.621      unfolding int2 of_int_add right_distrib by simp
1.622    qed
1.623 -  from aux1 show ?thesis by (auto simp add: divAlg_mod_div Let_def aux2 aux3)
1.624 +  from aux1 show ?thesis by (auto simp add: divmod_mod_div Let_def aux2 aux3)
1.625  qed
1.626
1.627  end
```