slightly adapted towards more uniformity with div/mod on nat
authorhaftmann
Wed Jan 28 11:02:11 2009 +0100 (2009-01-28)
changeset 2965116a19466bf81
parent 29647 12070638fe29
child 29652 f4c6e546b7fe
slightly adapted towards more uniformity with div/mod on nat
src/HOL/IntDiv.thy
     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.154 -apply (simp add: quorem_def)
   1.155 +apply (simp add: divmod_rel_def)
   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.167 -apply (simp add: quorem_def)
   1.168 +apply (simp add: divmod_rel_def)
   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.185  by (simp add: negateSnd_def)
   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.353  apply (simp add: right_diff_distrib)
   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.363  apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: add_commute)+
   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.369 -apply (simp add: quorem_def)
   1.370 +apply (simp add: divmod_rel_def)
   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.467    add_special
   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.508  lemma zadd1_lemma:
   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.517  lemma zdiv_zadd1_eq:
   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.563  by (rule div_add_self1) (* already declared [simp] *)
   1.564  
   1.565 @@ -862,21 +876,21 @@
   1.566                        add1_zle_eq pos_mod_bound)
   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