author haftmann Wed, 28 Jan 2009 11:02:11 +0100 changeset 29651 16a19466bf81 parent 29647 12070638fe29 child 29652 f4c6e546b7fe
slightly adapted towards more uniformity with div/mod on nat
 src/HOL/IntDiv.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/IntDiv.thy	Tue Jan 27 19:56:26 2009 +0100
+++ b/src/HOL/IntDiv.thy	Wed Jan 28 11:02:11 2009 +0100
@@ -1,82 +1,69 @@
(*  Title:      HOL/IntDiv.thy
-    ID:         \$Id\$
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

*)

-header{*The Division Operators div and mod; the Divides Relation dvd*}
+header{* The Division Operators div and mod *}

theory IntDiv
imports Int Divides FunDef
begin

-constdefs
-  quorem :: "(int*int) * (int*int) => bool"
+definition divmod_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where
--{*definition of quotient and remainder*}
-    [code]: "quorem == %((a,b), (q,r)).
-                      a = b*q + r &
-                      (if 0 < b then 0\<le>r & r<b else b<r & r \<le> 0)"
+    [code]: "divmod_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
+               (if 0 < b then 0 \<le> r \<and> r < b else b < r \<and> r \<le> 0))"

-  adjust :: "[int, int*int] => int*int"
+definition adjust :: "int \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int" where
--{*for the division algorithm*}
-    [code]: "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
-                         else (2*q, r)"
+    [code]: "adjust b = (\<lambda>(q, r). if 0 \<le> r - b then (2 * q + 1, r - b)
+                         else (2 * q, r))"

text{*algorithm for the case @{text "a\<ge>0, b>0"}*}
-function
-  posDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int"
-where
-  "posDivAlg a b =
-     (if (a<b | b\<le>0) then (0,a)
-        else adjust b (posDivAlg a (2*b)))"
+function posDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
+  "posDivAlg a b = (if a < b \<or>  b \<le> 0 then (0, a)
+     else adjust b (posDivAlg a (2 * b)))"
by auto
-termination by (relation "measure (%(a,b). nat(a - b + 1))") auto
+termination by (relation "measure (\<lambda>(a, b). nat (a - b + 1))") auto

text{*algorithm for the case @{text "a<0, b>0"}*}
-function
-  negDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int"
-where
-  "negDivAlg a b  =
-     (if (0\<le>a+b | b\<le>0) then (-1,a+b)
-      else adjust b (negDivAlg a (2*b)))"
+function negDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
+  "negDivAlg a b = (if 0 \<le>a + b \<or> b \<le> 0  then (-1, a + b)
+     else adjust b (negDivAlg a (2 * b)))"
by auto
-termination by (relation "measure (%(a,b). nat(- a - b))") auto
+termination by (relation "measure (\<lambda>(a, b). nat (- a - b))") auto

text{*algorithm for the general case @{term "b\<noteq>0"}*}
-constdefs
-  negateSnd :: "int*int => int*int"
-    [code]: "negateSnd == %(q,r). (q,-r)"
+definition negateSnd :: "int \<times> int \<Rightarrow> int \<times> int" where
+  [code inline]: "negateSnd = apsnd uminus"

-definition
-  divAlg :: "int \<times> int \<Rightarrow> int \<times> int"
+definition divmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
--{*The full division algorithm considers all possible signs for a, b
including the special case @{text "a=0, b<0"} because
@{term negDivAlg} requires @{term "a<0"}.*}
-where
-  "divAlg = (\<lambda>(a, b). (if 0\<le>a then
-                  if 0\<le>b then posDivAlg a b
-                  else if a=0 then (0, 0)
+  "divmod a b = (if 0 \<le> a then if 0 \<le> b then posDivAlg a b
+                  else if a = 0 then (0, 0)
else negateSnd (negDivAlg (-a) (-b))
else
-                  if 0<b then negDivAlg a b
-                  else negateSnd (posDivAlg (-a) (-b))))"
+                  if 0 < b then negDivAlg a b
+                  else negateSnd (posDivAlg (-a) (-b)))"

instantiation int :: Divides.div
begin

definition
-  div_def: "a div b = fst (divAlg (a, b))"
+  div_def: "a div b = fst (divmod a b)"

definition
-  mod_def: "a mod b = snd (divAlg (a, b))"
+  mod_def: "a mod b = snd (divmod a b)"

instance ..

end

-lemma divAlg_mod_div:
-  "divAlg (p, q) = (p div q, p mod q)"
+lemma divmod_mod_div:
+  "divmod p q = (p div q, p mod q)"
by (auto simp add: div_def mod_def)

text{*
@@ -97,7 +84,7 @@

fun negateSnd (q,r:int) = (q,~r);

-    fun divAlg (a,b) = if 0\<le>a then
+    fun divmod (a,b) = if 0\<le>a then
if b>0 then posDivAlg (a,b)
else if a=0 then (0,0)
else negateSnd (negDivAlg (~a,~b))
@@ -131,9 +118,9 @@
auto)

lemma unique_quotient:
-     "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  b \<noteq> 0 |]
+     "[| divmod_rel a b (q, r); divmod_rel a b (q', r');  b \<noteq> 0 |]
==> q = q'"
-apply (simp add: quorem_def linorder_neq_iff split: split_if_asm)
+apply (simp add: divmod_rel_def linorder_neq_iff split: split_if_asm)
apply (blast intro: order_antisym
dest: order_eq_refl [THEN unique_quotient_lemma]
order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
@@ -141,10 +128,10 @@

lemma unique_remainder:
-     "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  b \<noteq> 0 |]
+     "[| divmod_rel a b (q, r); divmod_rel a b (q', r');  b \<noteq> 0 |]
==> r = r'"
apply (subgoal_tac "q = q'")
apply (blast intro: unique_quotient)
done

@@ -171,10 +158,10 @@
text{*Correctness of @{term posDivAlg}: it computes quotients correctly*}
theorem posDivAlg_correct:
assumes "0 \<le> a" and "0 < b"
-  shows "quorem ((a, b), posDivAlg a b)"
+  shows "divmod_rel a b (posDivAlg a b)"
using prems apply (induct a b rule: posDivAlg.induct)
apply auto
apply (subst posDivAlg_eqn, simp add: right_distrib)
apply (case_tac "a < b")
apply simp_all
@@ -200,10 +187,10 @@
It doesn't work if a=0 because the 0/b equals 0, not -1*)
lemma negDivAlg_correct:
assumes "a < 0" and "b > 0"
-  shows "quorem ((a, b), negDivAlg a b)"
+  shows "divmod_rel a b (negDivAlg a b)"
using prems apply (induct a b rule: negDivAlg.induct)
apply (subst negDivAlg_eqn, assumption)
apply (case_tac "a + b < (0\<Colon>int)")
apply simp_all
@@ -215,8 +202,8 @@
subsection{*Existence Shown by Proving the Division Algorithm to be Correct*}

(*the case a=0*)
-lemma quorem_0: "b \<noteq> 0 ==> quorem ((0,b), (0,0))"
-by (auto simp add: quorem_def linorder_neq_iff)
+lemma divmod_rel_0: "b \<noteq> 0 ==> divmod_rel 0 b (0, 0)"
+by (auto simp add: divmod_rel_def linorder_neq_iff)

lemma posDivAlg_0 [simp]: "posDivAlg 0 b = (0, 0)"
by (subst posDivAlg.simps, auto)
@@ -227,26 +214,26 @@
lemma negateSnd_eq [simp]: "negateSnd(q,r) = (q,-r)"

-lemma quorem_neg: "quorem ((-a,-b), qr) ==> quorem ((a,b), negateSnd qr)"
-by (auto simp add: split_ifs quorem_def)
+lemma divmod_rel_neg: "divmod_rel (-a) (-b) qr ==> divmod_rel a b (negateSnd qr)"
+by (auto simp add: split_ifs divmod_rel_def)

-lemma divAlg_correct: "b \<noteq> 0 ==> quorem ((a,b), divAlg (a, b))"
-by (force simp add: linorder_neq_iff quorem_0 divAlg_def quorem_neg
+lemma divmod_correct: "b \<noteq> 0 ==> divmod_rel a b (divmod a b)"
+by (force simp add: linorder_neq_iff divmod_rel_0 divmod_def divmod_rel_neg
posDivAlg_correct negDivAlg_correct)

text{*Arbitrary definitions for division by zero.  Useful to simplify
certain equations.*}

lemma DIVISION_BY_ZERO [simp]: "a div (0::int) = 0 & a mod (0::int) = a"
-by (simp add: div_def mod_def divAlg_def posDivAlg.simps)
+by (simp add: div_def mod_def divmod_def posDivAlg.simps)

text{*Basic laws about division and remainder*}

lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
apply (case_tac "b = 0", simp)
-apply (cut_tac a = a and b = b in divAlg_correct)
-apply (auto simp add: quorem_def div_def mod_def)
+apply (cut_tac a = a and b = b in divmod_correct)
+apply (auto simp add: divmod_rel_def div_def mod_def)
done

lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k"
@@ -288,16 +275,16 @@
*}

lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b"
-apply (cut_tac a = a and b = b in divAlg_correct)
-apply (auto simp add: quorem_def mod_def)
+apply (cut_tac a = a and b = b in divmod_correct)
+apply (auto simp add: divmod_rel_def mod_def)
done

lemmas pos_mod_sign  [simp] = pos_mod_conj [THEN conjunct1, standard]
and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2, standard]

lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b"
-apply (cut_tac a = a and b = b in divAlg_correct)
-apply (auto simp add: quorem_def div_def mod_def)
+apply (cut_tac a = a and b = b in divmod_correct)
+apply (auto simp add: divmod_rel_def div_def mod_def)
done

lemmas neg_mod_sign  [simp] = neg_mod_conj [THEN conjunct1, standard]
@@ -307,47 +294,47 @@

subsection{*General Properties of div and mod*}

-lemma quorem_div_mod: "b \<noteq> 0 ==> quorem ((a, b), (a div b, a mod b))"
+lemma divmod_rel_div_mod: "b \<noteq> 0 ==> divmod_rel a b (a div b, a mod b)"
apply (cut_tac a = a and b = b in zmod_zdiv_equality)
-apply (force simp add: quorem_def linorder_neq_iff)
+apply (force simp add: divmod_rel_def linorder_neq_iff)
done

-lemma quorem_div: "[| quorem((a,b),(q,r));  b \<noteq> 0 |] ==> a div b = q"
-by (simp add: quorem_div_mod [THEN unique_quotient])
+lemma divmod_rel_div: "[| divmod_rel a b (q, r);  b \<noteq> 0 |] ==> a div b = q"
+by (simp add: divmod_rel_div_mod [THEN unique_quotient])

-lemma quorem_mod: "[| quorem((a,b),(q,r));  b \<noteq> 0 |] ==> a mod b = r"
-by (simp add: quorem_div_mod [THEN unique_remainder])
+lemma divmod_rel_mod: "[| divmod_rel a b (q, r);  b \<noteq> 0 |] ==> a mod b = r"
+by (simp add: divmod_rel_div_mod [THEN unique_remainder])

lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
-apply (rule quorem_div)
+apply (rule divmod_rel_div)
done

lemma div_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a div b = 0"
-apply (rule quorem_div)
+apply (rule divmod_rel_div)
done

lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"
-apply (rule quorem_div)
+apply (rule divmod_rel_div)
done

(*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)

lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
-apply (rule_tac q = 0 in quorem_mod)
+apply (rule_tac q = 0 in divmod_rel_mod)
done

lemma mod_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a mod b = a"
-apply (rule_tac q = 0 in quorem_mod)
+apply (rule_tac q = 0 in divmod_rel_mod)
done

lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
-apply (rule_tac q = "-1" in quorem_mod)
+apply (rule_tac q = "-1" in divmod_rel_mod)
done

text{*There is no @{text mod_neg_pos_trivial}.*}
@@ -356,15 +343,15 @@
(*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*)
lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)"
apply (case_tac "b = 0", simp)
-apply (simp add: quorem_div_mod [THEN quorem_neg, simplified,
-                                 THEN quorem_div, THEN sym])
+apply (simp add: divmod_rel_div_mod [THEN divmod_rel_neg, simplified,
+                                 THEN divmod_rel_div, THEN sym])

done

(*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*)
lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))"
apply (case_tac "b = 0", simp)
-apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_mod],
+apply (subst divmod_rel_div_mod [THEN divmod_rel_neg, simplified, THEN divmod_rel_mod],
auto)
done

@@ -372,22 +359,22 @@
subsection{*Laws for div and mod with Unary Minus*}

lemma zminus1_lemma:
-     "quorem((a,b),(q,r))
-      ==> quorem ((-a,b), (if r=0 then -q else -q - 1),
-                          (if r=0 then 0 else b-r))"
-by (force simp add: split_ifs quorem_def linorder_neq_iff right_diff_distrib)
+     "divmod_rel a b (q, r)
+      ==> divmod_rel (-a) b (if r=0 then -q else -q - 1,
+                          if r=0 then 0 else b-r)"
+by (force simp add: split_ifs divmod_rel_def linorder_neq_iff right_diff_distrib)

lemma zdiv_zminus1_eq_if:
"b \<noteq> (0::int)
==> (-a) div b =
(if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
-by (blast intro: quorem_div_mod [THEN zminus1_lemma, THEN quorem_div])
+by (blast intro: divmod_rel_div_mod [THEN zminus1_lemma, THEN divmod_rel_div])

lemma zmod_zminus1_eq_if:
"(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
apply (case_tac "b = 0", simp)
-apply (blast intro: quorem_div_mod [THEN zminus1_lemma, THEN quorem_mod])
+apply (blast intro: divmod_rel_div_mod [THEN zminus1_lemma, THEN divmod_rel_mod])
done

lemma zdiv_zminus2: "a div (-b) = (-a::int) div b"
@@ -420,91 +407,91 @@
done

-lemma self_quotient: "[| quorem((a,a),(q,r));  a \<noteq> (0::int) |] ==> q = 1"
-apply (simp add: split_ifs quorem_def linorder_neq_iff)
+lemma self_quotient: "[| divmod_rel a a (q, r);  a \<noteq> (0::int) |] ==> q = 1"
+apply (simp add: split_ifs divmod_rel_def linorder_neq_iff)
apply (rule order_antisym, safe, simp_all)
apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1)
apply (rule_tac a = "-a" and r = "-r" in self_quotient_aux2)
done

-lemma self_remainder: "[| quorem((a,a),(q,r));  a \<noteq> (0::int) |] ==> r = 0"
+lemma self_remainder: "[| divmod_rel a a (q, r);  a \<noteq> (0::int) |] ==> r = 0"
apply (frule self_quotient, assumption)
done

lemma zdiv_self [simp]: "a \<noteq> 0 ==> a div a = (1::int)"
-by (simp add: quorem_div_mod [THEN self_quotient])
+by (simp add: divmod_rel_div_mod [THEN self_quotient])

(*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *)
lemma zmod_self [simp]: "a mod a = (0::int)"
apply (case_tac "a = 0", simp)
-apply (simp add: quorem_div_mod [THEN self_remainder])
+apply (simp add: divmod_rel_div_mod [THEN self_remainder])
done

subsection{*Computation of Division and Remainder*}

lemma zdiv_zero [simp]: "(0::int) div b = 0"

lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"

lemma zmod_zero [simp]: "(0::int) mod b = 0"

lemma zdiv_minus1: "(0::int) < b ==> -1 div b = -1"

lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"

text{*a positive, b positive *}

lemma div_pos_pos: "[| 0 < a;  0 \<le> b |] ==> a div b = fst (posDivAlg a b)"

lemma mod_pos_pos: "[| 0 < a;  0 \<le> b |] ==> a mod b = snd (posDivAlg a b)"

text{*a negative, b positive *}

lemma div_neg_pos: "[| a < 0;  0 < b |] ==> a div b = fst (negDivAlg a b)"

lemma mod_neg_pos: "[| a < 0;  0 < b |] ==> a mod b = snd (negDivAlg a b)"

text{*a positive, b negative *}

lemma div_pos_neg:
"[| 0 < a;  b < 0 |] ==> a div b = fst (negateSnd (negDivAlg (-a) (-b)))"

lemma mod_pos_neg:
"[| 0 < a;  b < 0 |] ==> a mod b = snd (negateSnd (negDivAlg (-a) (-b)))"

text{*a negative, b negative *}

lemma div_neg_neg:
"[| a < 0;  b \<le> 0 |] ==> a div b = fst (negateSnd (posDivAlg (-a) (-b)))"

lemma mod_neg_neg:
"[| a < 0;  b \<le> 0 |] ==> a mod b = snd (negateSnd (posDivAlg (-a) (-b)))"

text {*Simplify expresions in which div and mod combine numerical constants*}

-lemma quoremI:
+lemma divmod_relI:
"\<lbrakk>a == b * q + r; if 0 < b then 0 \<le> r \<and> r < b else b < r \<and> r \<le> 0\<rbrakk>
-    \<Longrightarrow> quorem ((a, b), (q, r))"
-  unfolding quorem_def by simp
+    \<Longrightarrow> divmod_rel a b (q, r)"
+  unfolding divmod_rel_def by simp

-lemmas quorem_div_eq = quoremI [THEN quorem_div, THEN eq_reflection]
-lemmas quorem_mod_eq = quoremI [THEN quorem_mod, THEN eq_reflection]
+lemmas divmod_rel_div_eq = divmod_relI [THEN divmod_rel_div, THEN eq_reflection]
+lemmas divmod_rel_mod_eq = divmod_relI [THEN divmod_rel_mod, THEN eq_reflection]
lemmas arithmetic_simps =
arith_simps
@@ -548,10 +535,10 @@
*}

simproc_setup binary_int_div ("number_of m div number_of n :: int") =
-  {* K (divmod_proc (@{thm quorem_div_eq})) *}
+  {* K (divmod_proc (@{thm divmod_rel_div_eq})) *}

simproc_setup binary_int_mod ("number_of m mod number_of n :: int") =
-  {* K (divmod_proc (@{thm quorem_mod_eq})) *}
+  {* K (divmod_proc (@{thm divmod_rel_mod_eq})) *}

(* The following 8 lemmas are made unnecessary by the above simprocs: *)

@@ -718,18 +705,18 @@
text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *}

lemma zmult1_lemma:
-     "[| quorem((b,c),(q,r));  c \<noteq> 0 |]
-      ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"
-by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib)
+     "[| divmod_rel b c (q, r);  c \<noteq> 0 |]
+      ==> divmod_rel (a * b) c (a*q + a*r div c, a*r mod c)"
+by (force simp add: split_ifs divmod_rel_def linorder_neq_iff right_distrib)

lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
apply (case_tac "c = 0", simp)
-apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_div])
+apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_div])
done

lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)"
apply (case_tac "c = 0", simp)
-apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_mod])
+apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_mod])
done

lemma zmod_zmult1_eq': "(a*b) mod (c::int) = ((a mod c) * b) mod c"
@@ -760,20 +747,20 @@
text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}

-     "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  c \<noteq> 0 |]
-      ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
-by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib)
+     "[| divmod_rel a c (aq, ar);  divmod_rel b c (bq, br);  c \<noteq> 0 |]
+      ==> divmod_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
+by (force simp add: split_ifs divmod_rel_def linorder_neq_iff right_distrib)

(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
"(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
apply (case_tac "c = 0", simp)
-apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_div)
+apply (blast intro: zadd1_lemma [OF divmod_rel_div_mod divmod_rel_div_mod] divmod_rel_div)
done

lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c"
apply (case_tac "c = 0", simp)
-apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)
+apply (blast intro: zadd1_lemma [OF divmod_rel_div_mod divmod_rel_div_mod] divmod_rel_mod)
done

instance int :: ring_div
@@ -785,6 +772,33 @@
qed auto

+lemma posDivAlg_div_mod:
+  assumes "k \<ge> 0"
+  and "l \<ge> 0"
+  shows "posDivAlg k l = (k div l, k mod l)"
+proof (cases "l = 0")
+  case True then show ?thesis by (simp add: posDivAlg.simps)
+next
+  case False with assms posDivAlg_correct
+    have "divmod_rel k l (fst (posDivAlg k l), snd (posDivAlg k l))"
+    by simp
+  from divmod_rel_div [OF this `l \<noteq> 0`] divmod_rel_mod [OF this `l \<noteq> 0`]
+  show ?thesis by simp
+qed
+
+lemma negDivAlg_div_mod:
+  assumes "k < 0"
+  and "l > 0"
+  shows "negDivAlg k l = (k div l, k mod l)"
+proof -
+  from assms have "l \<noteq> 0" by simp
+  from assms negDivAlg_correct
+    have "divmod_rel k l (fst (negDivAlg k l), snd (negDivAlg k l))"
+    by simp
+  from divmod_rel_div [OF this `l \<noteq> 0`] divmod_rel_mod [OF this `l \<noteq> 0`]
+  show ?thesis by simp
+qed
+
lemma zdiv_zadd_self1: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"

@@ -862,21 +876,21 @@
done

-lemma zmult2_lemma: "[| quorem ((a,b), (q,r));  b \<noteq> 0;  0 < c |]
-      ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"
-by (auto simp add: mult_ac quorem_def linorder_neq_iff
+lemma zmult2_lemma: "[| divmod_rel a b (q, r);  b \<noteq> 0;  0 < c |]
+      ==> divmod_rel a (b * c) (q div c, b*(q mod c) + r)"
+by (auto simp add: mult_ac divmod_rel_def linorder_neq_iff
zero_less_mult_iff right_distrib [symmetric]
zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4)

lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"
apply (case_tac "b = 0", simp)
-apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_div])
+apply (force simp add: divmod_rel_div_mod [THEN zmult2_lemma, THEN divmod_rel_div])
done

lemma zmod_zmult2_eq:
"(0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b"
apply (case_tac "b = 0", simp)
-apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_mod])
+apply (force simp add: divmod_rel_div_mod [THEN zmult2_lemma, THEN divmod_rel_mod])
done

@@ -1360,7 +1374,7 @@
apply (subst split_div, auto)
apply (subst split_zdiv, auto)
apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient)
-apply (auto simp add: IntDiv.quorem_def of_nat_mult)
+apply (auto simp add: IntDiv.divmod_rel_def of_nat_mult)
done

lemma zmod_int: "int (a mod b) = (int a) mod (int b)"
@@ -1368,7 +1382,7 @@
apply (subst split_zmod, auto)
apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia
in unique_remainder)
-apply (auto simp add: IntDiv.quorem_def of_nat_mult)
+apply (auto simp add: IntDiv.divmod_rel_def of_nat_mult)
done

text{*Suggested by Matthias Daum*}
@@ -1429,7 +1443,7 @@
lemma of_int_num [code]:
"of_int k = (if k = 0 then 0 else if k < 0 then
- of_int (- k) else let
-       (l, m) = divAlg (k, 2);
+       (l, m) = divmod k 2;
l' = of_int l
in if m = 0 then l' + l' else l' + l' + 1)"
proof -
@@ -1457,7 +1471,7 @@
show "x * of_int 2 = x + x"
unfolding int2 of_int_add right_distrib by simp
qed
-  from aux1 show ?thesis by (auto simp add: divAlg_mod_div Let_def aux2 aux3)
+  from aux1 show ?thesis by (auto simp add: divmod_mod_div Let_def aux2 aux3)
qed

end```