src/HOL/Divides.thy
 author paulson Tue Apr 25 16:39:54 2017 +0100 (2017-04-25) changeset 65578 e4997c181cce parent 65556 fcd599570afa child 66630 034cabc4fda5 permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
 paulson@3366 ` 1` ```(* Title: HOL/Divides.thy ``` paulson@3366 ` 2` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` paulson@6865 ` 3` ``` Copyright 1999 University of Cambridge ``` huffman@18154 ` 4` ```*) ``` paulson@3366 ` 5` haftmann@64785 ` 6` ```section \More on quotient and remainder\ ``` paulson@3366 ` 7` nipkow@15131 ` 8` ```theory Divides ``` haftmann@58778 ` 9` ```imports Parity ``` nipkow@15131 ` 10` ```begin ``` paulson@3366 ` 11` haftmann@64592 ` 12` ```subsection \Quotient and remainder in integral domains with additional properties\ ``` haftmann@64592 ` 13` haftmann@64592 ` 14` ```class semiring_div = semidom_modulo + ``` haftmann@64592 ` 15` ``` assumes div_mult_self1 [simp]: "b \ 0 \ (a + c * b) div b = c + a div b" ``` haftmann@30930 ` 16` ``` and div_mult_mult1 [simp]: "c \ 0 \ (c * a) div (c * b) = a div b" ``` haftmann@25942 ` 17` ```begin ``` haftmann@25942 ` 18` haftmann@27651 ` 19` ```lemma div_mult_self2 [simp]: ``` haftmann@27651 ` 20` ``` assumes "b \ 0" ``` haftmann@27651 ` 21` ``` shows "(a + b * c) div b = c + a div b" ``` haftmann@57512 ` 22` ``` using assms div_mult_self1 [of b a c] by (simp add: mult.commute) ``` haftmann@26100 ` 23` haftmann@54221 ` 24` ```lemma div_mult_self3 [simp]: ``` haftmann@54221 ` 25` ``` assumes "b \ 0" ``` haftmann@54221 ` 26` ``` shows "(c * b + a) div b = c + a div b" ``` haftmann@54221 ` 27` ``` using assms by (simp add: add.commute) ``` haftmann@54221 ` 28` haftmann@54221 ` 29` ```lemma div_mult_self4 [simp]: ``` haftmann@54221 ` 30` ``` assumes "b \ 0" ``` haftmann@54221 ` 31` ``` shows "(b * c + a) div b = c + a div b" ``` haftmann@54221 ` 32` ``` using assms by (simp add: add.commute) ``` haftmann@54221 ` 33` haftmann@27651 ` 34` ```lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b" ``` haftmann@27651 ` 35` ```proof (cases "b = 0") ``` haftmann@27651 ` 36` ``` case True then show ?thesis by simp ``` haftmann@27651 ` 37` ```next ``` haftmann@27651 ` 38` ``` case False ``` haftmann@27651 ` 39` ``` have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b" ``` haftmann@64242 ` 40` ``` by (simp add: div_mult_mod_eq) ``` haftmann@27651 ` 41` ``` also from False div_mult_self1 [of b a c] have ``` haftmann@27651 ` 42` ``` "\ = (c + a div b) * b + (a + c * b) mod b" ``` nipkow@29667 ` 43` ``` by (simp add: algebra_simps) ``` haftmann@27651 ` 44` ``` finally have "a = a div b * b + (a + c * b) mod b" ``` haftmann@57512 ` 45` ``` by (simp add: add.commute [of a] add.assoc distrib_right) ``` haftmann@27651 ` 46` ``` then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b" ``` haftmann@64242 ` 47` ``` by (simp add: div_mult_mod_eq) ``` haftmann@27651 ` 48` ``` then show ?thesis by simp ``` haftmann@27651 ` 49` ```qed ``` haftmann@27651 ` 50` lp15@60562 ` 51` ```lemma mod_mult_self2 [simp]: ``` haftmann@54221 ` 52` ``` "(a + b * c) mod b = a mod b" ``` haftmann@57512 ` 53` ``` by (simp add: mult.commute [of b]) ``` haftmann@27651 ` 54` haftmann@54221 ` 55` ```lemma mod_mult_self3 [simp]: ``` haftmann@54221 ` 56` ``` "(c * b + a) mod b = a mod b" ``` haftmann@54221 ` 57` ``` by (simp add: add.commute) ``` haftmann@54221 ` 58` haftmann@54221 ` 59` ```lemma mod_mult_self4 [simp]: ``` haftmann@54221 ` 60` ``` "(b * c + a) mod b = a mod b" ``` haftmann@54221 ` 61` ``` by (simp add: add.commute) ``` haftmann@54221 ` 62` haftmann@60867 ` 63` ```lemma mod_mult_self1_is_0 [simp]: ``` haftmann@60867 ` 64` ``` "b * a mod b = 0" ``` haftmann@27651 ` 65` ``` using mod_mult_self2 [of 0 b a] by simp ``` haftmann@27651 ` 66` haftmann@60867 ` 67` ```lemma mod_mult_self2_is_0 [simp]: ``` haftmann@60867 ` 68` ``` "a * b mod b = 0" ``` haftmann@27651 ` 69` ``` using mod_mult_self1 [of 0 a b] by simp ``` haftmann@26062 ` 70` eberlm@63499 ` 71` ```lemma div_add_self1: ``` haftmann@27651 ` 72` ``` assumes "b \ 0" ``` haftmann@27651 ` 73` ``` shows "(b + a) div b = a div b + 1" ``` haftmann@57512 ` 74` ``` using assms div_mult_self1 [of b a 1] by (simp add: add.commute) ``` haftmann@26062 ` 75` eberlm@63499 ` 76` ```lemma div_add_self2: ``` haftmann@27651 ` 77` ``` assumes "b \ 0" ``` haftmann@27651 ` 78` ``` shows "(a + b) div b = a div b + 1" ``` haftmann@57512 ` 79` ``` using assms div_add_self1 [of b a] by (simp add: add.commute) ``` haftmann@27651 ` 80` haftmann@27676 ` 81` ```lemma mod_add_self1 [simp]: ``` haftmann@27651 ` 82` ``` "(b + a) mod b = a mod b" ``` haftmann@57512 ` 83` ``` using mod_mult_self1 [of a 1 b] by (simp add: add.commute) ``` haftmann@27651 ` 84` haftmann@27676 ` 85` ```lemma mod_add_self2 [simp]: ``` haftmann@27651 ` 86` ``` "(a + b) mod b = a mod b" ``` haftmann@27651 ` 87` ``` using mod_mult_self1 [of a 1 b] by simp ``` haftmann@27651 ` 88` haftmann@58911 ` 89` ```lemma mod_div_trivial [simp]: ``` haftmann@58911 ` 90` ``` "a mod b div b = 0" ``` huffman@29403 ` 91` ```proof (cases "b = 0") ``` huffman@29403 ` 92` ``` assume "b = 0" ``` huffman@29403 ` 93` ``` thus ?thesis by simp ``` huffman@29403 ` 94` ```next ``` huffman@29403 ` 95` ``` assume "b \ 0" ``` huffman@29403 ` 96` ``` hence "a div b + a mod b div b = (a mod b + a div b * b) div b" ``` huffman@29403 ` 97` ``` by (rule div_mult_self1 [symmetric]) ``` huffman@29403 ` 98` ``` also have "\ = a div b" ``` haftmann@64242 ` 99` ``` by (simp only: mod_div_mult_eq) ``` huffman@29403 ` 100` ``` also have "\ = a div b + 0" ``` huffman@29403 ` 101` ``` by simp ``` huffman@29403 ` 102` ``` finally show ?thesis ``` huffman@29403 ` 103` ``` by (rule add_left_imp_eq) ``` huffman@29403 ` 104` ```qed ``` huffman@29403 ` 105` haftmann@58911 ` 106` ```lemma mod_mod_trivial [simp]: ``` haftmann@58911 ` 107` ``` "a mod b mod b = a mod b" ``` huffman@29403 ` 108` ```proof - ``` huffman@29403 ` 109` ``` have "a mod b mod b = (a mod b + a div b * b) mod b" ``` huffman@29403 ` 110` ``` by (simp only: mod_mult_self1) ``` huffman@29403 ` 111` ``` also have "\ = a mod b" ``` haftmann@64242 ` 112` ``` by (simp only: mod_div_mult_eq) ``` huffman@29403 ` 113` ``` finally show ?thesis . ``` huffman@29403 ` 114` ```qed ``` huffman@29403 ` 115` huffman@29404 ` 116` ```lemma mod_mod_cancel: ``` huffman@29404 ` 117` ``` assumes "c dvd b" ``` huffman@29404 ` 118` ``` shows "a mod b mod c = a mod c" ``` huffman@29404 ` 119` ```proof - ``` wenzelm@60758 ` 120` ``` from \c dvd b\ obtain k where "b = c * k" ``` huffman@29404 ` 121` ``` by (rule dvdE) ``` huffman@29404 ` 122` ``` have "a mod b mod c = a mod (c * k) mod c" ``` wenzelm@60758 ` 123` ``` by (simp only: \b = c * k\) ``` huffman@29404 ` 124` ``` also have "\ = (a mod (c * k) + a div (c * k) * k * c) mod c" ``` huffman@29404 ` 125` ``` by (simp only: mod_mult_self1) ``` huffman@29404 ` 126` ``` also have "\ = (a div (c * k) * (c * k) + a mod (c * k)) mod c" ``` haftmann@58786 ` 127` ``` by (simp only: ac_simps) ``` huffman@29404 ` 128` ``` also have "\ = a mod c" ``` haftmann@64242 ` 129` ``` by (simp only: div_mult_mod_eq) ``` huffman@29404 ` 130` ``` finally show ?thesis . ``` huffman@29404 ` 131` ```qed ``` huffman@29404 ` 132` haftmann@30930 ` 133` ```lemma div_mult_mult2 [simp]: ``` haftmann@30930 ` 134` ``` "c \ 0 \ (a * c) div (b * c) = a div b" ``` haftmann@57512 ` 135` ``` by (drule div_mult_mult1) (simp add: mult.commute) ``` haftmann@30930 ` 136` haftmann@30930 ` 137` ```lemma div_mult_mult1_if [simp]: ``` haftmann@30930 ` 138` ``` "(c * a) div (c * b) = (if c = 0 then 0 else a div b)" ``` haftmann@30930 ` 139` ``` by simp_all ``` nipkow@30476 ` 140` haftmann@30930 ` 141` ```lemma mod_mult_mult1: ``` haftmann@30930 ` 142` ``` "(c * a) mod (c * b) = c * (a mod b)" ``` haftmann@30930 ` 143` ```proof (cases "c = 0") ``` haftmann@30930 ` 144` ``` case True then show ?thesis by simp ``` haftmann@30930 ` 145` ```next ``` haftmann@30930 ` 146` ``` case False ``` haftmann@64242 ` 147` ``` from div_mult_mod_eq ``` haftmann@30930 ` 148` ``` have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" . ``` haftmann@30930 ` 149` ``` with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b) ``` haftmann@30930 ` 150` ``` = c * a + c * (a mod b)" by (simp add: algebra_simps) ``` haftmann@64242 ` 151` ``` with div_mult_mod_eq show ?thesis by simp ``` haftmann@30930 ` 152` ```qed ``` lp15@60562 ` 153` haftmann@30930 ` 154` ```lemma mod_mult_mult2: ``` haftmann@30930 ` 155` ``` "(a * c) mod (b * c) = (a mod b) * c" ``` haftmann@57512 ` 156` ``` using mod_mult_mult1 [of c a b] by (simp add: mult.commute) ``` haftmann@30930 ` 157` huffman@47159 ` 158` ```lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)" ``` huffman@47159 ` 159` ``` by (fact mod_mult_mult2 [symmetric]) ``` huffman@47159 ` 160` huffman@47159 ` 161` ```lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)" ``` huffman@47159 ` 162` ``` by (fact mod_mult_mult1 [symmetric]) ``` huffman@47159 ` 163` huffman@31662 ` 164` ```lemma dvd_mod: "k dvd m \ k dvd n \ k dvd (m mod n)" ``` huffman@31662 ` 165` ``` unfolding dvd_def by (auto simp add: mod_mult_mult1) ``` huffman@31662 ` 166` haftmann@65556 ` 167` ```lemma div_plus_div_distrib_dvd_left: ``` haftmann@65556 ` 168` ``` "c dvd a \ (a + b) div c = a div c + b div c" ``` haftmann@65556 ` 169` ``` by (cases "c = 0") (auto elim: dvdE) ``` haftmann@65556 ` 170` haftmann@65556 ` 171` ```lemma div_plus_div_distrib_dvd_right: ``` haftmann@65556 ` 172` ``` "c dvd b \ (a + b) div c = a div c + b div c" ``` haftmann@65556 ` 173` ``` using div_plus_div_distrib_dvd_left [of c b a] ``` haftmann@65556 ` 174` ``` by (simp add: ac_simps) ``` haftmann@65556 ` 175` haftmann@64593 ` 176` ```named_theorems mod_simps ``` haftmann@64593 ` 177` haftmann@64593 ` 178` ```text \Addition respects modular equivalence.\ ``` haftmann@64593 ` 179` haftmann@64593 ` 180` ```lemma mod_add_left_eq [mod_simps]: ``` haftmann@64593 ` 181` ``` "(a mod c + b) mod c = (a + b) mod c" ``` haftmann@64593 ` 182` ```proof - ``` haftmann@64593 ` 183` ``` have "(a + b) mod c = (a div c * c + a mod c + b) mod c" ``` haftmann@64593 ` 184` ``` by (simp only: div_mult_mod_eq) ``` haftmann@64593 ` 185` ``` also have "\ = (a mod c + b + a div c * c) mod c" ``` haftmann@64593 ` 186` ``` by (simp only: ac_simps) ``` haftmann@64593 ` 187` ``` also have "\ = (a mod c + b) mod c" ``` haftmann@64593 ` 188` ``` by (rule mod_mult_self1) ``` haftmann@64593 ` 189` ``` finally show ?thesis ``` haftmann@64593 ` 190` ``` by (rule sym) ``` haftmann@64593 ` 191` ```qed ``` haftmann@64593 ` 192` haftmann@64593 ` 193` ```lemma mod_add_right_eq [mod_simps]: ``` haftmann@64593 ` 194` ``` "(a + b mod c) mod c = (a + b) mod c" ``` haftmann@64593 ` 195` ``` using mod_add_left_eq [of b c a] by (simp add: ac_simps) ``` haftmann@64593 ` 196` haftmann@64593 ` 197` ```lemma mod_add_eq: ``` haftmann@64593 ` 198` ``` "(a mod c + b mod c) mod c = (a + b) mod c" ``` haftmann@64593 ` 199` ``` by (simp add: mod_add_left_eq mod_add_right_eq) ``` haftmann@64593 ` 200` haftmann@64593 ` 201` ```lemma mod_sum_eq [mod_simps]: ``` haftmann@64593 ` 202` ``` "(\i\A. f i mod a) mod a = sum f A mod a" ``` haftmann@64593 ` 203` ```proof (induct A rule: infinite_finite_induct) ``` haftmann@64593 ` 204` ``` case (insert i A) ``` haftmann@64593 ` 205` ``` then have "(\i\insert i A. f i mod a) mod a ``` haftmann@64593 ` 206` ``` = (f i mod a + (\i\A. f i mod a)) mod a" ``` haftmann@64593 ` 207` ``` by simp ``` haftmann@64593 ` 208` ``` also have "\ = (f i + (\i\A. f i mod a) mod a) mod a" ``` haftmann@64593 ` 209` ``` by (simp add: mod_simps) ``` haftmann@64593 ` 210` ``` also have "\ = (f i + (\i\A. f i) mod a) mod a" ``` haftmann@64593 ` 211` ``` by (simp add: insert.hyps) ``` haftmann@64593 ` 212` ``` finally show ?case ``` haftmann@64593 ` 213` ``` by (simp add: insert.hyps mod_simps) ``` haftmann@64593 ` 214` ```qed simp_all ``` haftmann@64593 ` 215` haftmann@64593 ` 216` ```lemma mod_add_cong: ``` haftmann@64593 ` 217` ``` assumes "a mod c = a' mod c" ``` haftmann@64593 ` 218` ``` assumes "b mod c = b' mod c" ``` haftmann@64593 ` 219` ``` shows "(a + b) mod c = (a' + b') mod c" ``` haftmann@64593 ` 220` ```proof - ``` haftmann@64593 ` 221` ``` have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c" ``` haftmann@64593 ` 222` ``` unfolding assms .. ``` haftmann@64593 ` 223` ``` then show ?thesis ``` haftmann@64593 ` 224` ``` by (simp add: mod_add_eq) ``` haftmann@64593 ` 225` ```qed ``` haftmann@64593 ` 226` haftmann@64593 ` 227` ```text \Multiplication respects modular equivalence.\ ``` haftmann@64593 ` 228` haftmann@64593 ` 229` ```lemma mod_mult_left_eq [mod_simps]: ``` haftmann@64593 ` 230` ``` "((a mod c) * b) mod c = (a * b) mod c" ``` haftmann@64593 ` 231` ```proof - ``` haftmann@64593 ` 232` ``` have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c" ``` haftmann@64593 ` 233` ``` by (simp only: div_mult_mod_eq) ``` haftmann@64593 ` 234` ``` also have "\ = (a mod c * b + a div c * b * c) mod c" ``` haftmann@64593 ` 235` ``` by (simp only: algebra_simps) ``` haftmann@64593 ` 236` ``` also have "\ = (a mod c * b) mod c" ``` haftmann@64593 ` 237` ``` by (rule mod_mult_self1) ``` haftmann@64593 ` 238` ``` finally show ?thesis ``` haftmann@64593 ` 239` ``` by (rule sym) ``` haftmann@64593 ` 240` ```qed ``` haftmann@64593 ` 241` haftmann@64593 ` 242` ```lemma mod_mult_right_eq [mod_simps]: ``` haftmann@64593 ` 243` ``` "(a * (b mod c)) mod c = (a * b) mod c" ``` haftmann@64593 ` 244` ``` using mod_mult_left_eq [of b c a] by (simp add: ac_simps) ``` haftmann@64593 ` 245` haftmann@64593 ` 246` ```lemma mod_mult_eq: ``` haftmann@64593 ` 247` ``` "((a mod c) * (b mod c)) mod c = (a * b) mod c" ``` haftmann@64593 ` 248` ``` by (simp add: mod_mult_left_eq mod_mult_right_eq) ``` haftmann@64593 ` 249` haftmann@64593 ` 250` ```lemma mod_prod_eq [mod_simps]: ``` haftmann@64593 ` 251` ``` "(\i\A. f i mod a) mod a = prod f A mod a" ``` haftmann@64593 ` 252` ```proof (induct A rule: infinite_finite_induct) ``` haftmann@64593 ` 253` ``` case (insert i A) ``` haftmann@64593 ` 254` ``` then have "(\i\insert i A. f i mod a) mod a ``` haftmann@64593 ` 255` ``` = (f i mod a * (\i\A. f i mod a)) mod a" ``` haftmann@64593 ` 256` ``` by simp ``` haftmann@64593 ` 257` ``` also have "\ = (f i * ((\i\A. f i mod a) mod a)) mod a" ``` haftmann@64593 ` 258` ``` by (simp add: mod_simps) ``` haftmann@64593 ` 259` ``` also have "\ = (f i * ((\i\A. f i) mod a)) mod a" ``` haftmann@64593 ` 260` ``` by (simp add: insert.hyps) ``` haftmann@64593 ` 261` ``` finally show ?case ``` haftmann@64593 ` 262` ``` by (simp add: insert.hyps mod_simps) ``` haftmann@64593 ` 263` ```qed simp_all ``` haftmann@64593 ` 264` haftmann@64593 ` 265` ```lemma mod_mult_cong: ``` haftmann@64593 ` 266` ``` assumes "a mod c = a' mod c" ``` haftmann@64593 ` 267` ``` assumes "b mod c = b' mod c" ``` haftmann@64593 ` 268` ``` shows "(a * b) mod c = (a' * b') mod c" ``` haftmann@64593 ` 269` ```proof - ``` haftmann@64593 ` 270` ``` have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c" ``` haftmann@64593 ` 271` ``` unfolding assms .. ``` haftmann@64593 ` 272` ``` then show ?thesis ``` haftmann@64593 ` 273` ``` by (simp add: mod_mult_eq) ``` haftmann@64593 ` 274` ```qed ``` haftmann@64593 ` 275` haftmann@64593 ` 276` ```text \Exponentiation respects modular equivalence.\ ``` haftmann@64593 ` 277` haftmann@64593 ` 278` ```lemma power_mod [mod_simps]: ``` haftmann@64593 ` 279` ``` "((a mod b) ^ n) mod b = (a ^ n) mod b" ``` haftmann@64593 ` 280` ```proof (induct n) ``` haftmann@64593 ` 281` ``` case 0 ``` haftmann@64593 ` 282` ``` then show ?case by simp ``` haftmann@64593 ` 283` ```next ``` haftmann@64593 ` 284` ``` case (Suc n) ``` haftmann@64593 ` 285` ``` have "(a mod b) ^ Suc n mod b = (a mod b) * ((a mod b) ^ n mod b) mod b" ``` haftmann@64593 ` 286` ``` by (simp add: mod_mult_right_eq) ``` haftmann@64593 ` 287` ``` with Suc show ?case ``` haftmann@64593 ` 288` ``` by (simp add: mod_mult_left_eq mod_mult_right_eq) ``` haftmann@64593 ` 289` ```qed ``` haftmann@64593 ` 290` huffman@31661 ` 291` ```end ``` huffman@31661 ` 292` haftmann@59833 ` 293` ```class ring_div = comm_ring_1 + semiring_div ``` huffman@29405 ` 294` ```begin ``` huffman@29405 ` 295` haftmann@60353 ` 296` ```subclass idom_divide .. ``` haftmann@36634 ` 297` haftmann@64593 ` 298` ```lemma div_minus_minus [simp]: "(- a) div (- b) = a div b" ``` haftmann@64593 ` 299` ``` using div_mult_mult1 [of "- 1" a b] by simp ``` haftmann@64593 ` 300` haftmann@64593 ` 301` ```lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)" ``` haftmann@64593 ` 302` ``` using mod_mult_mult1 [of "- 1" a b] by simp ``` haftmann@64593 ` 303` haftmann@64593 ` 304` ```lemma div_minus_right: "a div (- b) = (- a) div b" ``` haftmann@64593 ` 305` ``` using div_minus_minus [of "- a" b] by simp ``` haftmann@64593 ` 306` haftmann@64593 ` 307` ```lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)" ``` haftmann@64593 ` 308` ``` using mod_minus_minus [of "- a" b] by simp ``` haftmann@64593 ` 309` haftmann@64593 ` 310` ```lemma div_minus1_right [simp]: "a div (- 1) = - a" ``` haftmann@64593 ` 311` ``` using div_minus_right [of a 1] by simp ``` haftmann@64593 ` 312` haftmann@64593 ` 313` ```lemma mod_minus1_right [simp]: "a mod (- 1) = 0" ``` haftmann@64593 ` 314` ``` using mod_minus_right [of a 1] by simp ``` haftmann@64593 ` 315` wenzelm@60758 ` 316` ```text \Negation respects modular equivalence.\ ``` huffman@29405 ` 317` haftmann@64593 ` 318` ```lemma mod_minus_eq [mod_simps]: ``` haftmann@64593 ` 319` ``` "(- (a mod b)) mod b = (- a) mod b" ``` huffman@29405 ` 320` ```proof - ``` huffman@29405 ` 321` ``` have "(- a) mod b = (- (a div b * b + a mod b)) mod b" ``` haftmann@64242 ` 322` ``` by (simp only: div_mult_mod_eq) ``` huffman@29405 ` 323` ``` also have "\ = (- (a mod b) + - (a div b) * b) mod b" ``` haftmann@57514 ` 324` ``` by (simp add: ac_simps) ``` huffman@29405 ` 325` ``` also have "\ = (- (a mod b)) mod b" ``` huffman@29405 ` 326` ``` by (rule mod_mult_self1) ``` haftmann@64593 ` 327` ``` finally show ?thesis ``` haftmann@64593 ` 328` ``` by (rule sym) ``` huffman@29405 ` 329` ```qed ``` huffman@29405 ` 330` huffman@29405 ` 331` ```lemma mod_minus_cong: ``` huffman@29405 ` 332` ``` assumes "a mod b = a' mod b" ``` huffman@29405 ` 333` ``` shows "(- a) mod b = (- a') mod b" ``` huffman@29405 ` 334` ```proof - ``` huffman@29405 ` 335` ``` have "(- (a mod b)) mod b = (- (a' mod b)) mod b" ``` huffman@29405 ` 336` ``` unfolding assms .. ``` haftmann@64593 ` 337` ``` then show ?thesis ``` haftmann@64593 ` 338` ``` by (simp add: mod_minus_eq) ``` huffman@29405 ` 339` ```qed ``` huffman@29405 ` 340` wenzelm@60758 ` 341` ```text \Subtraction respects modular equivalence.\ ``` huffman@29405 ` 342` haftmann@64593 ` 343` ```lemma mod_diff_left_eq [mod_simps]: ``` haftmann@64593 ` 344` ``` "(a mod c - b) mod c = (a - b) mod c" ``` haftmann@64593 ` 345` ``` using mod_add_cong [of a c "a mod c" "- b" "- b"] ``` haftmann@64593 ` 346` ``` by simp ``` haftmann@64593 ` 347` haftmann@64593 ` 348` ```lemma mod_diff_right_eq [mod_simps]: ``` haftmann@64593 ` 349` ``` "(a - b mod c) mod c = (a - b) mod c" ``` haftmann@64593 ` 350` ``` using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] ``` haftmann@64593 ` 351` ``` by simp ``` haftmann@54230 ` 352` haftmann@54230 ` 353` ```lemma mod_diff_eq: ``` haftmann@64593 ` 354` ``` "(a mod c - b mod c) mod c = (a - b) mod c" ``` haftmann@64593 ` 355` ``` using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] ``` haftmann@64593 ` 356` ``` by simp ``` huffman@29405 ` 357` huffman@29405 ` 358` ```lemma mod_diff_cong: ``` huffman@29405 ` 359` ``` assumes "a mod c = a' mod c" ``` huffman@29405 ` 360` ``` assumes "b mod c = b' mod c" ``` huffman@29405 ` 361` ``` shows "(a - b) mod c = (a' - b') mod c" ``` haftmann@64593 ` 362` ``` using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"] ``` haftmann@64593 ` 363` ``` by simp ``` huffman@47160 ` 364` lp15@60562 ` 365` ```lemma minus_mod_self2 [simp]: ``` haftmann@54221 ` 366` ``` "(a - b) mod b = a mod b" ``` haftmann@64593 ` 367` ``` using mod_diff_right_eq [of a b b] ``` haftmann@54221 ` 368` ``` by (simp add: mod_diff_right_eq) ``` haftmann@54221 ` 369` lp15@60562 ` 370` ```lemma minus_mod_self1 [simp]: ``` haftmann@54221 ` 371` ``` "(b - a) mod b = - a mod b" ``` haftmann@54230 ` 372` ``` using mod_add_self2 [of "- a" b] by simp ``` haftmann@54221 ` 373` huffman@29405 ` 374` ```end ``` huffman@29405 ` 375` haftmann@64785 ` 376` ``` ``` haftmann@64785 ` 377` ```subsection \Euclidean (semi)rings with cancel rules\ ``` haftmann@64785 ` 378` haftmann@64785 ` 379` ```class euclidean_semiring_cancel = euclidean_semiring + semiring_div ``` haftmann@64785 ` 380` haftmann@64785 ` 381` ```class euclidean_ring_cancel = euclidean_ring + ring_div ``` haftmann@64785 ` 382` haftmann@64785 ` 383` ```context unique_euclidean_semiring ``` haftmann@64785 ` 384` ```begin ``` haftmann@64785 ` 385` haftmann@64785 ` 386` ```subclass euclidean_semiring_cancel ``` haftmann@64785 ` 387` ```proof ``` haftmann@64785 ` 388` ``` show "(a + c * b) div b = c + a div b" if "b \ 0" for a b c ``` haftmann@64785 ` 389` ``` proof (cases a b rule: divmod_cases) ``` haftmann@64785 ` 390` ``` case by0 ``` haftmann@64785 ` 391` ``` with \b \ 0\ show ?thesis ``` haftmann@64785 ` 392` ``` by simp ``` haftmann@64785 ` 393` ``` next ``` haftmann@64785 ` 394` ``` case (divides q) ``` haftmann@64785 ` 395` ``` then show ?thesis ``` haftmann@64785 ` 396` ``` by (simp add: ac_simps) ``` haftmann@64785 ` 397` ``` next ``` haftmann@64785 ` 398` ``` case (remainder q r) ``` haftmann@64785 ` 399` ``` then show ?thesis ``` haftmann@64785 ` 400` ``` by (auto intro: div_eqI simp add: algebra_simps) ``` haftmann@64785 ` 401` ``` qed ``` haftmann@64785 ` 402` ```next ``` haftmann@64785 ` 403` ``` show"(c * a) div (c * b) = a div b" if "c \ 0" for a b c ``` haftmann@64785 ` 404` ``` proof (cases a b rule: divmod_cases) ``` haftmann@64785 ` 405` ``` case by0 ``` haftmann@64785 ` 406` ``` then show ?thesis ``` haftmann@64785 ` 407` ``` by simp ``` haftmann@64785 ` 408` ``` next ``` haftmann@64785 ` 409` ``` case (divides q) ``` haftmann@64785 ` 410` ``` with \c \ 0\ show ?thesis ``` haftmann@64785 ` 411` ``` by (simp add: mult.left_commute [of c]) ``` haftmann@64785 ` 412` ``` next ``` haftmann@64785 ` 413` ``` case (remainder q r) ``` haftmann@64785 ` 414` ``` from \b \ 0\ \c \ 0\ have "b * c \ 0" ``` haftmann@64785 ` 415` ``` by simp ``` haftmann@64785 ` 416` ``` from remainder \c \ 0\ ``` haftmann@64785 ` 417` ``` have "uniqueness_constraint (r * c) (b * c)" ``` haftmann@64785 ` 418` ``` and "euclidean_size (r * c) < euclidean_size (b * c)" ``` haftmann@64785 ` 419` ``` by (simp_all add: uniqueness_constraint_mono_mult uniqueness_constraint_mod size_mono_mult) ``` haftmann@64785 ` 420` ``` with remainder show ?thesis ``` haftmann@64785 ` 421` ``` by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps) ``` haftmann@64785 ` 422` ``` (use \b * c \ 0\ in simp) ``` haftmann@64785 ` 423` ``` qed ``` haftmann@64785 ` 424` ```qed ``` haftmann@64785 ` 425` haftmann@64785 ` 426` ```end ``` haftmann@64785 ` 427` haftmann@64785 ` 428` ```context unique_euclidean_ring ``` haftmann@64785 ` 429` ```begin ``` haftmann@64785 ` 430` haftmann@64785 ` 431` ```subclass euclidean_ring_cancel .. ``` haftmann@64785 ` 432` haftmann@64785 ` 433` ```end ``` haftmann@64785 ` 434` haftmann@58778 ` 435` haftmann@64592 ` 436` ```subsection \Parity\ ``` haftmann@58778 ` 437` lp15@60562 ` 438` ```class semiring_div_parity = semiring_div + comm_semiring_1_cancel + numeral + ``` haftmann@54226 ` 439` ``` assumes parity: "a mod 2 = 0 \ a mod 2 = 1" ``` haftmann@58786 ` 440` ``` assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1" ``` haftmann@58710 ` 441` ``` assumes zero_not_eq_two: "0 \ 2" ``` haftmann@54226 ` 442` ```begin ``` haftmann@54226 ` 443` haftmann@54226 ` 444` ```lemma parity_cases [case_names even odd]: ``` haftmann@54226 ` 445` ``` assumes "a mod 2 = 0 \ P" ``` haftmann@54226 ` 446` ``` assumes "a mod 2 = 1 \ P" ``` haftmann@54226 ` 447` ``` shows P ``` haftmann@54226 ` 448` ``` using assms parity by blast ``` haftmann@54226 ` 449` haftmann@58786 ` 450` ```lemma one_div_two_eq_zero [simp]: ``` haftmann@58778 ` 451` ``` "1 div 2 = 0" ``` haftmann@58778 ` 452` ```proof (cases "2 = 0") ``` haftmann@58778 ` 453` ``` case True then show ?thesis by simp ``` haftmann@58778 ` 454` ```next ``` haftmann@58778 ` 455` ``` case False ``` haftmann@64242 ` 456` ``` from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" . ``` haftmann@58778 ` 457` ``` with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp ``` haftmann@58953 ` 458` ``` then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff) ``` haftmann@58953 ` 459` ``` then have "1 div 2 = 0 \ 2 = 0" by simp ``` haftmann@58778 ` 460` ``` with False show ?thesis by auto ``` haftmann@58778 ` 461` ```qed ``` haftmann@58778 ` 462` haftmann@58786 ` 463` ```lemma not_mod_2_eq_0_eq_1 [simp]: ``` haftmann@58786 ` 464` ``` "a mod 2 \ 0 \ a mod 2 = 1" ``` haftmann@58786 ` 465` ``` by (cases a rule: parity_cases) simp_all ``` haftmann@58786 ` 466` haftmann@58786 ` 467` ```lemma not_mod_2_eq_1_eq_0 [simp]: ``` haftmann@58786 ` 468` ``` "a mod 2 \ 1 \ a mod 2 = 0" ``` haftmann@58786 ` 469` ``` by (cases a rule: parity_cases) simp_all ``` haftmann@58786 ` 470` haftmann@58778 ` 471` ```subclass semiring_parity ``` haftmann@58778 ` 472` ```proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1) ``` haftmann@58778 ` 473` ``` show "1 mod 2 = 1" ``` haftmann@58778 ` 474` ``` by (fact one_mod_two_eq_one) ``` haftmann@58778 ` 475` ```next ``` haftmann@58778 ` 476` ``` fix a b ``` haftmann@58778 ` 477` ``` assume "a mod 2 = 1" ``` haftmann@58778 ` 478` ``` moreover assume "b mod 2 = 1" ``` haftmann@58778 ` 479` ``` ultimately show "(a + b) mod 2 = 0" ``` haftmann@64593 ` 480` ``` using mod_add_eq [of a 2 b] by simp ``` haftmann@58778 ` 481` ```next ``` haftmann@58778 ` 482` ``` fix a b ``` haftmann@58778 ` 483` ``` assume "(a * b) mod 2 = 0" ``` haftmann@64593 ` 484` ``` then have "(a mod 2) * (b mod 2) mod 2 = 0" ``` haftmann@64593 ` 485` ``` by (simp add: mod_mult_eq) ``` haftmann@58778 ` 486` ``` then have "(a mod 2) * (b mod 2) = 0" ``` haftmann@64593 ` 487` ``` by (cases "a mod 2 = 0") simp_all ``` haftmann@58778 ` 488` ``` then show "a mod 2 = 0 \ b mod 2 = 0" ``` haftmann@58778 ` 489` ``` by (rule divisors_zero) ``` haftmann@58778 ` 490` ```next ``` haftmann@58778 ` 491` ``` fix a ``` haftmann@58778 ` 492` ``` assume "a mod 2 = 1" ``` haftmann@64593 ` 493` ``` then have "a = a div 2 * 2 + 1" ``` haftmann@64593 ` 494` ``` using div_mult_mod_eq [of a 2] by simp ``` haftmann@58778 ` 495` ``` then show "\b. a = b + 1" .. ``` haftmann@58778 ` 496` ```qed ``` haftmann@58778 ` 497` haftmann@58778 ` 498` ```lemma even_iff_mod_2_eq_zero: ``` haftmann@58778 ` 499` ``` "even a \ a mod 2 = 0" ``` haftmann@58778 ` 500` ``` by (fact dvd_eq_mod_eq_0) ``` haftmann@58778 ` 501` haftmann@64014 ` 502` ```lemma odd_iff_mod_2_eq_one: ``` haftmann@64014 ` 503` ``` "odd a \ a mod 2 = 1" ``` haftmann@64014 ` 504` ``` by (auto simp add: even_iff_mod_2_eq_zero) ``` haftmann@64014 ` 505` haftmann@58778 ` 506` ```lemma even_succ_div_two [simp]: ``` haftmann@58778 ` 507` ``` "even a \ (a + 1) div 2 = a div 2" ``` haftmann@58778 ` 508` ``` by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero) ``` haftmann@58778 ` 509` haftmann@58778 ` 510` ```lemma odd_succ_div_two [simp]: ``` haftmann@58778 ` 511` ``` "odd a \ (a + 1) div 2 = a div 2 + 1" ``` haftmann@58778 ` 512` ``` by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc) ``` haftmann@58778 ` 513` haftmann@58778 ` 514` ```lemma even_two_times_div_two: ``` haftmann@58778 ` 515` ``` "even a \ 2 * (a div 2) = a" ``` haftmann@58778 ` 516` ``` by (fact dvd_mult_div_cancel) ``` haftmann@58778 ` 517` haftmann@58834 ` 518` ```lemma odd_two_times_div_two_succ [simp]: ``` haftmann@58778 ` 519` ``` "odd a \ 2 * (a div 2) + 1 = a" ``` haftmann@64242 ` 520` ``` using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero) ``` haftmann@60868 ` 521` ``` ``` haftmann@54226 ` 522` ```end ``` haftmann@54226 ` 523` haftmann@25942 ` 524` haftmann@64592 ` 525` ```subsection \Numeral division with a pragmatic type class\ ``` wenzelm@60758 ` 526` wenzelm@60758 ` 527` ```text \ ``` haftmann@53067 ` 528` ``` The following type class contains everything necessary to formulate ``` haftmann@53067 ` 529` ``` a division algorithm in ring structures with numerals, restricted ``` haftmann@53067 ` 530` ``` to its positive segments. This is its primary motiviation, and it ``` haftmann@53067 ` 531` ``` could surely be formulated using a more fine-grained, more algebraic ``` haftmann@53067 ` 532` ``` and less technical class hierarchy. ``` wenzelm@60758 ` 533` ```\ ``` haftmann@53067 ` 534` lp15@60562 ` 535` ```class semiring_numeral_div = semiring_div + comm_semiring_1_cancel + linordered_semidom + ``` haftmann@59816 ` 536` ``` assumes div_less: "0 \ a \ a < b \ a div b = 0" ``` haftmann@53067 ` 537` ``` and mod_less: " 0 \ a \ a < b \ a mod b = a" ``` haftmann@53067 ` 538` ``` and div_positive: "0 < b \ b \ a \ a div b > 0" ``` haftmann@53067 ` 539` ``` and mod_less_eq_dividend: "0 \ a \ a mod b \ a" ``` haftmann@53067 ` 540` ``` and pos_mod_bound: "0 < b \ a mod b < b" ``` haftmann@53067 ` 541` ``` and pos_mod_sign: "0 < b \ 0 \ a mod b" ``` haftmann@53067 ` 542` ``` and mod_mult2_eq: "0 \ c \ a mod (b * c) = b * (a div b mod c) + a mod b" ``` haftmann@53067 ` 543` ``` and div_mult2_eq: "0 \ c \ a div (b * c) = a div b div c" ``` haftmann@53067 ` 544` ``` assumes discrete: "a < b \ a + 1 \ b" ``` haftmann@61275 ` 545` ``` fixes divmod :: "num \ num \ 'a \ 'a" ``` haftmann@61275 ` 546` ``` and divmod_step :: "num \ 'a \ 'a \ 'a \ 'a" ``` haftmann@61275 ` 547` ``` assumes divmod_def: "divmod m n = (numeral m div numeral n, numeral m mod numeral n)" ``` haftmann@61275 ` 548` ``` and divmod_step_def: "divmod_step l qr = (let (q, r) = qr ``` haftmann@61275 ` 549` ``` in if r \ numeral l then (2 * q + 1, r - numeral l) ``` haftmann@61275 ` 550` ``` else (2 * q, r))" ``` wenzelm@61799 ` 551` ``` \ \These are conceptually definitions but force generated code ``` haftmann@61275 ` 552` ``` to be monomorphic wrt. particular instances of this class which ``` haftmann@61275 ` 553` ``` yields a significant speedup.\ ``` haftmann@61275 ` 554` haftmann@53067 ` 555` ```begin ``` haftmann@53067 ` 556` haftmann@54226 ` 557` ```subclass semiring_div_parity ``` haftmann@54226 ` 558` ```proof ``` haftmann@54226 ` 559` ``` fix a ``` haftmann@54226 ` 560` ``` show "a mod 2 = 0 \ a mod 2 = 1" ``` haftmann@54226 ` 561` ``` proof (rule ccontr) ``` haftmann@54226 ` 562` ``` assume "\ (a mod 2 = 0 \ a mod 2 = 1)" ``` haftmann@54226 ` 563` ``` then have "a mod 2 \ 0" and "a mod 2 \ 1" by simp_all ``` haftmann@54226 ` 564` ``` have "0 < 2" by simp ``` haftmann@54226 ` 565` ``` with pos_mod_bound pos_mod_sign have "0 \ a mod 2" "a mod 2 < 2" by simp_all ``` wenzelm@60758 ` 566` ``` with \a mod 2 \ 0\ have "0 < a mod 2" by simp ``` haftmann@54226 ` 567` ``` with discrete have "1 \ a mod 2" by simp ``` wenzelm@60758 ` 568` ``` with \a mod 2 \ 1\ have "1 < a mod 2" by simp ``` haftmann@54226 ` 569` ``` with discrete have "2 \ a mod 2" by simp ``` wenzelm@60758 ` 570` ``` with \a mod 2 < 2\ show False by simp ``` haftmann@54226 ` 571` ``` qed ``` haftmann@58646 ` 572` ```next ``` haftmann@58646 ` 573` ``` show "1 mod 2 = 1" ``` haftmann@58646 ` 574` ``` by (rule mod_less) simp_all ``` haftmann@58710 ` 575` ```next ``` haftmann@58710 ` 576` ``` show "0 \ 2" ``` haftmann@58710 ` 577` ``` by simp ``` haftmann@53067 ` 578` ```qed ``` haftmann@53067 ` 579` haftmann@53067 ` 580` ```lemma divmod_digit_1: ``` haftmann@53067 ` 581` ``` assumes "0 \ a" "0 < b" and "b \ a mod (2 * b)" ``` haftmann@53067 ` 582` ``` shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P") ``` haftmann@53067 ` 583` ``` and "a mod (2 * b) - b = a mod b" (is "?Q") ``` haftmann@53067 ` 584` ```proof - ``` haftmann@53067 ` 585` ``` from assms mod_less_eq_dividend [of a "2 * b"] have "b \ a" ``` haftmann@53067 ` 586` ``` by (auto intro: trans) ``` wenzelm@60758 ` 587` ``` with \0 < b\ have "0 < a div b" by (auto intro: div_positive) ``` haftmann@53067 ` 588` ``` then have [simp]: "1 \ a div b" by (simp add: discrete) ``` wenzelm@60758 ` 589` ``` with \0 < b\ have mod_less: "a mod b < b" by (simp add: pos_mod_bound) ``` wenzelm@63040 ` 590` ``` define w where "w = a div b mod 2" ``` wenzelm@63040 ` 591` ``` with parity have w_exhaust: "w = 0 \ w = 1" by auto ``` haftmann@53067 ` 592` ``` have mod_w: "a mod (2 * b) = a mod b + b * w" ``` haftmann@53067 ` 593` ``` by (simp add: w_def mod_mult2_eq ac_simps) ``` haftmann@53067 ` 594` ``` from assms w_exhaust have "w = 1" ``` haftmann@53067 ` 595` ``` by (auto simp add: mod_w) (insert mod_less, auto) ``` haftmann@53067 ` 596` ``` with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp ``` haftmann@53067 ` 597` ``` have "2 * (a div (2 * b)) = a div b - w" ``` haftmann@64246 ` 598` ``` by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps) ``` wenzelm@60758 ` 599` ``` with \w = 1\ have div: "2 * (a div (2 * b)) = a div b - 1" by simp ``` haftmann@53067 ` 600` ``` then show ?P and ?Q ``` haftmann@60867 ` 601` ``` by (simp_all add: div mod add_implies_diff [symmetric]) ``` haftmann@53067 ` 602` ```qed ``` haftmann@53067 ` 603` haftmann@53067 ` 604` ```lemma divmod_digit_0: ``` haftmann@53067 ` 605` ``` assumes "0 < b" and "a mod (2 * b) < b" ``` haftmann@53067 ` 606` ``` shows "2 * (a div (2 * b)) = a div b" (is "?P") ``` haftmann@53067 ` 607` ``` and "a mod (2 * b) = a mod b" (is "?Q") ``` haftmann@53067 ` 608` ```proof - ``` wenzelm@63040 ` 609` ``` define w where "w = a div b mod 2" ``` wenzelm@63040 ` 610` ``` with parity have w_exhaust: "w = 0 \ w = 1" by auto ``` haftmann@53067 ` 611` ``` have mod_w: "a mod (2 * b) = a mod b + b * w" ``` haftmann@53067 ` 612` ``` by (simp add: w_def mod_mult2_eq ac_simps) ``` haftmann@53067 ` 613` ``` moreover have "b \ a mod b + b" ``` haftmann@53067 ` 614` ``` proof - ``` wenzelm@60758 ` 615` ``` from \0 < b\ pos_mod_sign have "0 \ a mod b" by blast ``` haftmann@53067 ` 616` ``` then have "0 + b \ a mod b + b" by (rule add_right_mono) ``` haftmann@53067 ` 617` ``` then show ?thesis by simp ``` haftmann@53067 ` 618` ``` qed ``` haftmann@53067 ` 619` ``` moreover note assms w_exhaust ``` haftmann@53067 ` 620` ``` ultimately have "w = 0" by auto ``` haftmann@53067 ` 621` ``` with mod_w have mod: "a mod (2 * b) = a mod b" by simp ``` haftmann@53067 ` 622` ``` have "2 * (a div (2 * b)) = a div b - w" ``` haftmann@64246 ` 623` ``` by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps) ``` wenzelm@60758 ` 624` ``` with \w = 0\ have div: "2 * (a div (2 * b)) = a div b" by simp ``` haftmann@53067 ` 625` ``` then show ?P and ?Q ``` haftmann@53067 ` 626` ``` by (simp_all add: div mod) ``` haftmann@53067 ` 627` ```qed ``` haftmann@53067 ` 628` haftmann@60867 ` 629` ```lemma fst_divmod: ``` haftmann@53067 ` 630` ``` "fst (divmod m n) = numeral m div numeral n" ``` haftmann@53067 ` 631` ``` by (simp add: divmod_def) ``` haftmann@53067 ` 632` haftmann@60867 ` 633` ```lemma snd_divmod: ``` haftmann@53067 ` 634` ``` "snd (divmod m n) = numeral m mod numeral n" ``` haftmann@53067 ` 635` ``` by (simp add: divmod_def) ``` haftmann@53067 ` 636` wenzelm@60758 ` 637` ```text \ ``` haftmann@53067 ` 638` ``` This is a formulation of one step (referring to one digit position) ``` haftmann@53067 ` 639` ``` in school-method division: compare the dividend at the current ``` haftmann@53070 ` 640` ``` digit position with the remainder from previous division steps ``` haftmann@53067 ` 641` ``` and evaluate accordingly. ``` wenzelm@60758 ` 642` ```\ ``` haftmann@53067 ` 643` haftmann@61275 ` 644` ```lemma divmod_step_eq [simp]: ``` haftmann@53067 ` 645` ``` "divmod_step l (q, r) = (if numeral l \ r ``` haftmann@53067 ` 646` ``` then (2 * q + 1, r - numeral l) else (2 * q, r))" ``` haftmann@53067 ` 647` ``` by (simp add: divmod_step_def) ``` haftmann@53067 ` 648` wenzelm@60758 ` 649` ```text \ ``` haftmann@53067 ` 650` ``` This is a formulation of school-method division. ``` haftmann@53067 ` 651` ``` If the divisor is smaller than the dividend, terminate. ``` haftmann@53067 ` 652` ``` If not, shift the dividend to the right until termination ``` haftmann@53067 ` 653` ``` occurs and then reiterate single division steps in the ``` haftmann@53067 ` 654` ``` opposite direction. ``` wenzelm@60758 ` 655` ```\ ``` haftmann@53067 ` 656` haftmann@60867 ` 657` ```lemma divmod_divmod_step: ``` haftmann@53067 ` 658` ``` "divmod m n = (if m < n then (0, numeral m) ``` haftmann@53067 ` 659` ``` else divmod_step n (divmod m (Num.Bit0 n)))" ``` haftmann@53067 ` 660` ```proof (cases "m < n") ``` haftmann@53067 ` 661` ``` case True then have "numeral m < numeral n" by simp ``` haftmann@53067 ` 662` ``` then show ?thesis ``` haftmann@60867 ` 663` ``` by (simp add: prod_eq_iff div_less mod_less fst_divmod snd_divmod) ``` haftmann@53067 ` 664` ```next ``` haftmann@53067 ` 665` ``` case False ``` haftmann@53067 ` 666` ``` have "divmod m n = ``` haftmann@53067 ` 667` ``` divmod_step n (numeral m div (2 * numeral n), ``` haftmann@53067 ` 668` ``` numeral m mod (2 * numeral n))" ``` haftmann@53067 ` 669` ``` proof (cases "numeral n \ numeral m mod (2 * numeral n)") ``` haftmann@53067 ` 670` ``` case True ``` haftmann@60867 ` 671` ``` with divmod_step_eq ``` haftmann@53067 ` 672` ``` have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) = ``` haftmann@53067 ` 673` ``` (2 * (numeral m div (2 * numeral n)) + 1, numeral m mod (2 * numeral n) - numeral n)" ``` haftmann@60867 ` 674` ``` by simp ``` haftmann@53067 ` 675` ``` moreover from True divmod_digit_1 [of "numeral m" "numeral n"] ``` haftmann@53067 ` 676` ``` have "2 * (numeral m div (2 * numeral n)) + 1 = numeral m div numeral n" ``` haftmann@53067 ` 677` ``` and "numeral m mod (2 * numeral n) - numeral n = numeral m mod numeral n" ``` haftmann@53067 ` 678` ``` by simp_all ``` haftmann@53067 ` 679` ``` ultimately show ?thesis by (simp only: divmod_def) ``` haftmann@53067 ` 680` ``` next ``` haftmann@53067 ` 681` ``` case False then have *: "numeral m mod (2 * numeral n) < numeral n" ``` haftmann@53067 ` 682` ``` by (simp add: not_le) ``` haftmann@60867 ` 683` ``` with divmod_step_eq ``` haftmann@53067 ` 684` ``` have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) = ``` haftmann@53067 ` 685` ``` (2 * (numeral m div (2 * numeral n)), numeral m mod (2 * numeral n))" ``` haftmann@60867 ` 686` ``` by auto ``` haftmann@53067 ` 687` ``` moreover from * divmod_digit_0 [of "numeral n" "numeral m"] ``` haftmann@53067 ` 688` ``` have "2 * (numeral m div (2 * numeral n)) = numeral m div numeral n" ``` haftmann@53067 ` 689` ``` and "numeral m mod (2 * numeral n) = numeral m mod numeral n" ``` haftmann@53067 ` 690` ``` by (simp_all only: zero_less_numeral) ``` haftmann@53067 ` 691` ``` ultimately show ?thesis by (simp only: divmod_def) ``` haftmann@53067 ` 692` ``` qed ``` haftmann@53067 ` 693` ``` then have "divmod m n = ``` haftmann@53067 ` 694` ``` divmod_step n (numeral m div numeral (Num.Bit0 n), ``` haftmann@53067 ` 695` ``` numeral m mod numeral (Num.Bit0 n))" ``` lp15@60562 ` 696` ``` by (simp only: numeral.simps distrib mult_1) ``` haftmann@53067 ` 697` ``` then have "divmod m n = divmod_step n (divmod m (Num.Bit0 n))" ``` haftmann@53067 ` 698` ``` by (simp add: divmod_def) ``` haftmann@53067 ` 699` ``` with False show ?thesis by simp ``` haftmann@53067 ` 700` ```qed ``` haftmann@53067 ` 701` wenzelm@61799 ` 702` ```text \The division rewrite proper -- first, trivial results involving \1\\ ``` haftmann@60867 ` 703` haftmann@61275 ` 704` ```lemma divmod_trivial [simp]: ``` haftmann@60867 ` 705` ``` "divmod Num.One Num.One = (numeral Num.One, 0)" ``` haftmann@60867 ` 706` ``` "divmod (Num.Bit0 m) Num.One = (numeral (Num.Bit0 m), 0)" ``` haftmann@60867 ` 707` ``` "divmod (Num.Bit1 m) Num.One = (numeral (Num.Bit1 m), 0)" ``` haftmann@60867 ` 708` ``` "divmod num.One (num.Bit0 n) = (0, Numeral1)" ``` haftmann@60867 ` 709` ``` "divmod num.One (num.Bit1 n) = (0, Numeral1)" ``` haftmann@60867 ` 710` ``` using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def) ``` haftmann@60867 ` 711` haftmann@60867 ` 712` ```text \Division by an even number is a right-shift\ ``` haftmann@58953 ` 713` haftmann@61275 ` 714` ```lemma divmod_cancel [simp]: ``` haftmann@53069 ` 715` ``` "divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \ (q, 2 * r))" (is ?P) ``` haftmann@53069 ` 716` ``` "divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \ (q, 2 * r + 1))" (is ?Q) ``` haftmann@53069 ` 717` ```proof - ``` haftmann@53069 ` 718` ``` have *: "\q. numeral (Num.Bit0 q) = 2 * numeral q" ``` haftmann@53069 ` 719` ``` "\q. numeral (Num.Bit1 q) = 2 * numeral q + 1" ``` haftmann@53069 ` 720` ``` by (simp_all only: numeral_mult numeral.simps distrib) simp_all ``` haftmann@53069 ` 721` ``` have "1 div 2 = 0" "1 mod 2 = 1" by (auto intro: div_less mod_less) ``` haftmann@53069 ` 722` ``` then show ?P and ?Q ``` haftmann@60867 ` 723` ``` by (simp_all add: fst_divmod snd_divmod prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1 ``` haftmann@60867 ` 724` ``` div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2] ``` haftmann@60867 ` 725` ``` add.commute del: numeral_times_numeral) ``` haftmann@58953 ` 726` ```qed ``` haftmann@58953 ` 727` haftmann@60867 ` 728` ```text \The really hard work\ ``` haftmann@60867 ` 729` haftmann@61275 ` 730` ```lemma divmod_steps [simp]: ``` haftmann@60867 ` 731` ``` "divmod (num.Bit0 m) (num.Bit1 n) = ``` haftmann@60867 ` 732` ``` (if m \ n then (0, numeral (num.Bit0 m)) ``` haftmann@60867 ` 733` ``` else divmod_step (num.Bit1 n) ``` haftmann@60867 ` 734` ``` (divmod (num.Bit0 m) ``` haftmann@60867 ` 735` ``` (num.Bit0 (num.Bit1 n))))" ``` haftmann@60867 ` 736` ``` "divmod (num.Bit1 m) (num.Bit1 n) = ``` haftmann@60867 ` 737` ``` (if m < n then (0, numeral (num.Bit1 m)) ``` haftmann@60867 ` 738` ``` else divmod_step (num.Bit1 n) ``` haftmann@60867 ` 739` ``` (divmod (num.Bit1 m) ``` haftmann@60867 ` 740` ``` (num.Bit0 (num.Bit1 n))))" ``` haftmann@60867 ` 741` ``` by (simp_all add: divmod_divmod_step) ``` haftmann@60867 ` 742` haftmann@61275 ` 743` ```lemmas divmod_algorithm_code = divmod_step_eq divmod_trivial divmod_cancel divmod_steps ``` haftmann@61275 ` 744` wenzelm@60758 ` 745` ```text \Special case: divisibility\ ``` haftmann@58953 ` 746` haftmann@58953 ` 747` ```definition divides_aux :: "'a \ 'a \ bool" ``` haftmann@58953 ` 748` ```where ``` haftmann@58953 ` 749` ``` "divides_aux qr \ snd qr = 0" ``` haftmann@58953 ` 750` haftmann@58953 ` 751` ```lemma divides_aux_eq [simp]: ``` haftmann@58953 ` 752` ``` "divides_aux (q, r) \ r = 0" ``` haftmann@58953 ` 753` ``` by (simp add: divides_aux_def) ``` haftmann@58953 ` 754` haftmann@58953 ` 755` ```lemma dvd_numeral_simp [simp]: ``` haftmann@58953 ` 756` ``` "numeral m dvd numeral n \ divides_aux (divmod n m)" ``` haftmann@58953 ` 757` ``` by (simp add: divmod_def mod_eq_0_iff_dvd) ``` haftmann@53069 ` 758` haftmann@60867 ` 759` ```text \Generic computation of quotient and remainder\ ``` haftmann@60867 ` 760` haftmann@60867 ` 761` ```lemma numeral_div_numeral [simp]: ``` haftmann@60867 ` 762` ``` "numeral k div numeral l = fst (divmod k l)" ``` haftmann@60867 ` 763` ``` by (simp add: fst_divmod) ``` haftmann@60867 ` 764` haftmann@60867 ` 765` ```lemma numeral_mod_numeral [simp]: ``` haftmann@60867 ` 766` ``` "numeral k mod numeral l = snd (divmod k l)" ``` haftmann@60867 ` 767` ``` by (simp add: snd_divmod) ``` haftmann@60867 ` 768` haftmann@60867 ` 769` ```lemma one_div_numeral [simp]: ``` haftmann@60867 ` 770` ``` "1 div numeral n = fst (divmod num.One n)" ``` haftmann@60867 ` 771` ``` by (simp add: fst_divmod) ``` haftmann@60867 ` 772` haftmann@60867 ` 773` ```lemma one_mod_numeral [simp]: ``` haftmann@60867 ` 774` ``` "1 mod numeral n = snd (divmod num.One n)" ``` haftmann@60867 ` 775` ``` by (simp add: snd_divmod) ``` haftmann@64630 ` 776` haftmann@64630 ` 777` ```text \Computing congruences modulo \2 ^ q\\ ``` haftmann@64630 ` 778` haftmann@64630 ` 779` ```lemma cong_exp_iff_simps: ``` haftmann@64630 ` 780` ``` "numeral n mod numeral Num.One = 0 ``` haftmann@64630 ` 781` ``` \ True" ``` haftmann@64630 ` 782` ``` "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = 0 ``` haftmann@64630 ` 783` ``` \ numeral n mod numeral q = 0" ``` haftmann@64630 ` 784` ``` "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = 0 ``` haftmann@64630 ` 785` ``` \ False" ``` haftmann@64630 ` 786` ``` "numeral m mod numeral Num.One = (numeral n mod numeral Num.One) ``` haftmann@64630 ` 787` ``` \ True" ``` haftmann@64630 ` 788` ``` "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q)) ``` haftmann@64630 ` 789` ``` \ True" ``` haftmann@64630 ` 790` ``` "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q)) ``` haftmann@64630 ` 791` ``` \ False" ``` haftmann@64630 ` 792` ``` "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q)) ``` haftmann@64630 ` 793` ``` \ (numeral n mod numeral q) = 0" ``` haftmann@64630 ` 794` ``` "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q)) ``` haftmann@64630 ` 795` ``` \ False" ``` haftmann@64630 ` 796` ``` "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q)) ``` haftmann@64630 ` 797` ``` \ numeral m mod numeral q = (numeral n mod numeral q)" ``` haftmann@64630 ` 798` ``` "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q)) ``` haftmann@64630 ` 799` ``` \ False" ``` haftmann@64630 ` 800` ``` "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q)) ``` haftmann@64630 ` 801` ``` \ (numeral m mod numeral q) = 0" ``` haftmann@64630 ` 802` ``` "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q)) ``` haftmann@64630 ` 803` ``` \ False" ``` haftmann@64630 ` 804` ``` "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q)) ``` haftmann@64630 ` 805` ``` \ numeral m mod numeral q = (numeral n mod numeral q)" ``` haftmann@64630 ` 806` ``` by (auto simp add: case_prod_beta dest: arg_cong [of _ _ even]) ``` haftmann@64630 ` 807` haftmann@53067 ` 808` ```end ``` haftmann@53067 ` 809` lp15@60562 ` 810` wenzelm@60758 ` 811` ```subsection \Division on @{typ nat}\ ``` wenzelm@60758 ` 812` haftmann@61433 ` 813` ```context ``` haftmann@61433 ` 814` ```begin ``` haftmann@61433 ` 815` wenzelm@60758 ` 816` ```text \ ``` haftmann@63950 ` 817` ``` We define @{const divide} and @{const modulo} on @{typ nat} by means ``` haftmann@26100 ` 818` ``` of a characteristic relation with two input arguments ``` wenzelm@61076 ` 819` ``` @{term "m::nat"}, @{term "n::nat"} and two output arguments ``` wenzelm@61076 ` 820` ``` @{term "q::nat"}(uotient) and @{term "r::nat"}(emainder). ``` wenzelm@60758 ` 821` ```\ ``` haftmann@26100 ` 822` haftmann@64635 ` 823` ```inductive eucl_rel_nat :: "nat \ nat \ nat \ nat \ bool" ``` haftmann@64635 ` 824` ``` where eucl_rel_nat_by0: "eucl_rel_nat m 0 (0, m)" ``` haftmann@64635 ` 825` ``` | eucl_rel_natI: "r < n \ m = q * n + r \ eucl_rel_nat m n (q, r)" ``` haftmann@64635 ` 826` haftmann@64635 ` 827` ```text \@{const eucl_rel_nat} is total:\ ``` haftmann@64635 ` 828` haftmann@64635 ` 829` ```qualified lemma eucl_rel_nat_ex: ``` haftmann@64635 ` 830` ``` obtains q r where "eucl_rel_nat m n (q, r)" ``` haftmann@26100 ` 831` ```proof (cases "n = 0") ``` haftmann@64635 ` 832` ``` case True ``` haftmann@64635 ` 833` ``` with that eucl_rel_nat_by0 show thesis ``` haftmann@64635 ` 834` ``` by blast ``` haftmann@26100 ` 835` ```next ``` haftmann@26100 ` 836` ``` case False ``` haftmann@26100 ` 837` ``` have "\q r. m = q * n + r \ r < n" ``` haftmann@26100 ` 838` ``` proof (induct m) ``` wenzelm@60758 ` 839` ``` case 0 with \n \ 0\ ``` wenzelm@61076 ` 840` ``` have "(0::nat) = 0 * n + 0 \ 0 < n" by simp ``` haftmann@26100 ` 841` ``` then show ?case by blast ``` haftmann@26100 ` 842` ``` next ``` haftmann@26100 ` 843` ``` case (Suc m) then obtain q' r' ``` haftmann@26100 ` 844` ``` where m: "m = q' * n + r'" and n: "r' < n" by auto ``` haftmann@26100 ` 845` ``` then show ?case proof (cases "Suc r' < n") ``` haftmann@26100 ` 846` ``` case True ``` haftmann@26100 ` 847` ``` from m n have "Suc m = q' * n + Suc r'" by simp ``` haftmann@26100 ` 848` ``` with True show ?thesis by blast ``` haftmann@26100 ` 849` ``` next ``` haftmann@64592 ` 850` ``` case False then have "n \ Suc r'" ``` haftmann@64592 ` 851` ``` by (simp add: not_less) ``` haftmann@64592 ` 852` ``` moreover from n have "Suc r' \ n" ``` haftmann@64592 ` 853` ``` by (simp add: Suc_le_eq) ``` haftmann@26100 ` 854` ``` ultimately have "n = Suc r'" by auto ``` haftmann@26100 ` 855` ``` with m have "Suc m = Suc q' * n + 0" by simp ``` wenzelm@60758 ` 856` ``` with \n \ 0\ show ?thesis by blast ``` haftmann@26100 ` 857` ``` qed ``` haftmann@26100 ` 858` ``` qed ``` haftmann@64635 ` 859` ``` with that \n \ 0\ eucl_rel_natI show thesis ``` haftmann@64635 ` 860` ``` by blast ``` haftmann@26100 ` 861` ```qed ``` haftmann@26100 ` 862` haftmann@64635 ` 863` ```text \@{const eucl_rel_nat} is injective:\ ``` haftmann@64635 ` 864` haftmann@64635 ` 865` ```qualified lemma eucl_rel_nat_unique_div: ``` haftmann@64635 ` 866` ``` assumes "eucl_rel_nat m n (q, r)" ``` haftmann@64635 ` 867` ``` and "eucl_rel_nat m n (q', r')" ``` haftmann@64635 ` 868` ``` shows "q = q'" ``` haftmann@26100 ` 869` ```proof (cases "n = 0") ``` haftmann@26100 ` 870` ``` case True with assms show ?thesis ``` haftmann@64635 ` 871` ``` by (auto elim: eucl_rel_nat.cases) ``` haftmann@26100 ` 872` ```next ``` haftmann@26100 ` 873` ``` case False ``` haftmann@64635 ` 874` ``` have *: "q' \ q" if "q' * n + r' = q * n + r" "r < n" for q r q' r' :: nat ``` haftmann@64635 ` 875` ``` proof (rule ccontr) ``` haftmann@64635 ` 876` ``` assume "\ q' \ q" ``` haftmann@64635 ` 877` ``` then have "q < q'" ``` haftmann@64635 ` 878` ``` by (simp add: not_le) ``` haftmann@64635 ` 879` ``` with that show False ``` haftmann@64635 ` 880` ``` by (auto simp add: less_iff_Suc_add algebra_simps) ``` haftmann@64635 ` 881` ``` qed ``` haftmann@64635 ` 882` ``` from \n \ 0\ assms show ?thesis ``` haftmann@64635 ` 883` ``` by (auto intro: order_antisym elim: eucl_rel_nat.cases dest: * sym split: if_splits) ``` haftmann@64635 ` 884` ```qed ``` haftmann@64635 ` 885` haftmann@64635 ` 886` ```qualified lemma eucl_rel_nat_unique_mod: ``` haftmann@64635 ` 887` ``` assumes "eucl_rel_nat m n (q, r)" ``` haftmann@64635 ` 888` ``` and "eucl_rel_nat m n (q', r')" ``` haftmann@64635 ` 889` ``` shows "r = r'" ``` haftmann@64635 ` 890` ```proof - ``` haftmann@64635 ` 891` ``` from assms have "q' = q" ``` haftmann@64635 ` 892` ``` by (auto intro: eucl_rel_nat_unique_div) ``` haftmann@64635 ` 893` ``` with assms show ?thesis ``` haftmann@64635 ` 894` ``` by (auto elim!: eucl_rel_nat.cases) ``` haftmann@26100 ` 895` ```qed ``` haftmann@26100 ` 896` wenzelm@60758 ` 897` ```text \ ``` haftmann@26100 ` 898` ``` We instantiate divisibility on the natural numbers by ``` haftmann@64635 ` 899` ``` means of @{const eucl_rel_nat}: ``` wenzelm@60758 ` 900` ```\ ``` haftmann@25942 ` 901` haftmann@61433 ` 902` ```qualified definition divmod_nat :: "nat \ nat \ nat \ nat" where ``` haftmann@64635 ` 903` ``` "divmod_nat m n = (THE qr. eucl_rel_nat m n qr)" ``` haftmann@64635 ` 904` haftmann@64635 ` 905` ```qualified lemma eucl_rel_nat_divmod_nat: ``` haftmann@64635 ` 906` ``` "eucl_rel_nat m n (divmod_nat m n)" ``` haftmann@30923 ` 907` ```proof - ``` haftmann@64635 ` 908` ``` from eucl_rel_nat_ex ``` haftmann@64635 ` 909` ``` obtain q r where rel: "eucl_rel_nat m n (q, r)" . ``` haftmann@30923 ` 910` ``` then show ?thesis ``` haftmann@64635 ` 911` ``` by (auto simp add: divmod_nat_def intro: theI ``` haftmann@64635 ` 912` ``` elim: eucl_rel_nat_unique_div eucl_rel_nat_unique_mod) ``` haftmann@30923 ` 913` ```qed ``` haftmann@30923 ` 914` haftmann@61433 ` 915` ```qualified lemma divmod_nat_unique: ``` haftmann@64635 ` 916` ``` "divmod_nat m n = (q, r)" if "eucl_rel_nat m n (q, r)" ``` haftmann@64635 ` 917` ``` using that ``` haftmann@64635 ` 918` ``` by (auto simp add: divmod_nat_def intro: eucl_rel_nat_divmod_nat elim: eucl_rel_nat_unique_div eucl_rel_nat_unique_mod) ``` haftmann@64635 ` 919` haftmann@64635 ` 920` ```qualified lemma divmod_nat_zero: ``` haftmann@64635 ` 921` ``` "divmod_nat m 0 = (0, m)" ``` haftmann@64635 ` 922` ``` by (rule divmod_nat_unique) (fact eucl_rel_nat_by0) ``` haftmann@64635 ` 923` haftmann@64635 ` 924` ```qualified lemma divmod_nat_zero_left: ``` haftmann@64635 ` 925` ``` "divmod_nat 0 n = (0, 0)" ``` haftmann@64635 ` 926` ``` by (rule divmod_nat_unique) ``` haftmann@64635 ` 927` ``` (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI) ``` haftmann@64635 ` 928` haftmann@64635 ` 929` ```qualified lemma divmod_nat_base: ``` haftmann@64635 ` 930` ``` "m < n \ divmod_nat m n = (0, m)" ``` haftmann@64635 ` 931` ``` by (rule divmod_nat_unique) ``` haftmann@64635 ` 932` ``` (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI) ``` haftmann@61433 ` 933` haftmann@61433 ` 934` ```qualified lemma divmod_nat_step: ``` haftmann@61433 ` 935` ``` assumes "0 < n" and "n \ m" ``` haftmann@64635 ` 936` ``` shows "divmod_nat m n = ``` haftmann@64635 ` 937` ``` (Suc (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))" ``` haftmann@61433 ` 938` ```proof (rule divmod_nat_unique) ``` haftmann@64635 ` 939` ``` have "eucl_rel_nat (m - n) n (divmod_nat (m - n) n)" ``` haftmann@64635 ` 940` ``` by (fact eucl_rel_nat_divmod_nat) ``` haftmann@64635 ` 941` ``` then show "eucl_rel_nat m n (Suc ``` haftmann@64635 ` 942` ``` (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))" ``` haftmann@64635 ` 943` ``` using assms ``` haftmann@64635 ` 944` ``` by (auto split: if_splits intro: eucl_rel_natI elim!: eucl_rel_nat.cases simp add: algebra_simps) ``` haftmann@61433 ` 945` ```qed ``` haftmann@61433 ` 946` haftmann@61433 ` 947` ```end ``` haftmann@64592 ` 948` haftmann@64592 ` 949` ```instantiation nat :: "{semidom_modulo, normalization_semidom}" ``` haftmann@60352 ` 950` ```begin ``` haftmann@60352 ` 951` haftmann@64592 ` 952` ```definition normalize_nat :: "nat \ nat" ``` haftmann@64592 ` 953` ``` where [simp]: "normalize = (id :: nat \ nat)" ``` haftmann@64592 ` 954` haftmann@64592 ` 955` ```definition unit_factor_nat :: "nat \ nat" ``` haftmann@64592 ` 956` ``` where "unit_factor n = (if n = 0 then 0 else 1 :: nat)" ``` haftmann@64592 ` 957` haftmann@64592 ` 958` ```lemma unit_factor_simps [simp]: ``` haftmann@64592 ` 959` ``` "unit_factor 0 = (0::nat)" ``` haftmann@64592 ` 960` ``` "unit_factor (Suc n) = 1" ``` haftmann@64592 ` 961` ``` by (simp_all add: unit_factor_nat_def) ``` haftmann@64592 ` 962` haftmann@64592 ` 963` ```definition divide_nat :: "nat \ nat \ nat" ``` haftmann@64592 ` 964` ``` where div_nat_def: "m div n = fst (Divides.divmod_nat m n)" ``` haftmann@64592 ` 965` haftmann@64592 ` 966` ```definition modulo_nat :: "nat \ nat \ nat" ``` haftmann@64592 ` 967` ``` where mod_nat_def: "m mod n = snd (Divides.divmod_nat m n)" ``` huffman@46551 ` 968` huffman@46551 ` 969` ```lemma fst_divmod_nat [simp]: ``` haftmann@61433 ` 970` ``` "fst (Divides.divmod_nat m n) = m div n" ``` huffman@46551 ` 971` ``` by (simp add: div_nat_def) ``` huffman@46551 ` 972` huffman@46551 ` 973` ```lemma snd_divmod_nat [simp]: ``` haftmann@61433 ` 974` ``` "snd (Divides.divmod_nat m n) = m mod n" ``` huffman@46551 ` 975` ``` by (simp add: mod_nat_def) ``` huffman@46551 ` 976` haftmann@33340 ` 977` ```lemma divmod_nat_div_mod: ``` haftmann@61433 ` 978` ``` "Divides.divmod_nat m n = (m div n, m mod n)" ``` huffman@46551 ` 979` ``` by (simp add: prod_eq_iff) ``` haftmann@26100 ` 980` huffman@47135 ` 981` ```lemma div_nat_unique: ``` haftmann@64635 ` 982` ``` assumes "eucl_rel_nat m n (q, r)" ``` haftmann@26100 ` 983` ``` shows "m div n = q" ``` haftmann@64592 ` 984` ``` using assms ``` haftmann@64592 ` 985` ``` by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff) ``` huffman@47135 ` 986` huffman@47135 ` 987` ```lemma mod_nat_unique: ``` haftmann@64635 ` 988` ``` assumes "eucl_rel_nat m n (q, r)" ``` haftmann@26100 ` 989` ``` shows "m mod n = r" ``` haftmann@64592 ` 990` ``` using assms ``` haftmann@64592 ` 991` ``` by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff) ``` haftmann@25571 ` 992` haftmann@64635 ` 993` ```lemma eucl_rel_nat: "eucl_rel_nat m n (m div n, m mod n)" ``` haftmann@64635 ` 994` ``` using Divides.eucl_rel_nat_divmod_nat ``` haftmann@64592 ` 995` ``` by (simp add: divmod_nat_div_mod) ``` haftmann@25942 ` 996` haftmann@63950 ` 997` ```text \The ''recursion'' equations for @{const divide} and @{const modulo}\ ``` haftmann@26100 ` 998` haftmann@26100 ` 999` ```lemma div_less [simp]: ``` haftmann@26100 ` 1000` ``` fixes m n :: nat ``` haftmann@26100 ` 1001` ``` assumes "m < n" ``` haftmann@26100 ` 1002` ``` shows "m div n = 0" ``` haftmann@61433 ` 1003` ``` using assms Divides.divmod_nat_base by (simp add: prod_eq_iff) ``` haftmann@25942 ` 1004` haftmann@26100 ` 1005` ```lemma le_div_geq: ``` haftmann@26100 ` 1006` ``` fixes m n :: nat ``` haftmann@26100 ` 1007` ``` assumes "0 < n" and "n \ m" ``` haftmann@26100 ` 1008` ``` shows "m div n = Suc ((m - n) div n)" ``` haftmann@61433 ` 1009` ``` using assms Divides.divmod_nat_step by (simp add: prod_eq_iff) ``` paulson@14267 ` 1010` haftmann@26100 ` 1011` ```lemma mod_less [simp]: ``` haftmann@26100 ` 1012` ``` fixes m n :: nat ``` haftmann@26100 ` 1013` ``` assumes "m < n" ``` haftmann@26100 ` 1014` ``` shows "m mod n = m" ``` haftmann@61433 ` 1015` ``` using assms Divides.divmod_nat_base by (simp add: prod_eq_iff) ``` haftmann@26100 ` 1016` haftmann@26100 ` 1017` ```lemma le_mod_geq: ``` haftmann@26100 ` 1018` ``` fixes m n :: nat ``` haftmann@26100 ` 1019` ``` assumes "n \ m" ``` haftmann@26100 ` 1020` ``` shows "m mod n = (m - n) mod n" ``` haftmann@61433 ` 1021` ``` using assms Divides.divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff) ``` paulson@14267 ` 1022` haftmann@64592 ` 1023` ```lemma mod_less_divisor [simp]: ``` haftmann@64592 ` 1024` ``` fixes m n :: nat ``` haftmann@64592 ` 1025` ``` assumes "n > 0" ``` haftmann@64592 ` 1026` ``` shows "m mod n < n" ``` haftmann@64635 ` 1027` ``` using assms eucl_rel_nat [of m n] ``` haftmann@64635 ` 1028` ``` by (auto elim: eucl_rel_nat.cases) ``` haftmann@64592 ` 1029` haftmann@64592 ` 1030` ```lemma mod_le_divisor [simp]: ``` haftmann@64592 ` 1031` ``` fixes m n :: nat ``` haftmann@64592 ` 1032` ``` assumes "n > 0" ``` haftmann@64592 ` 1033` ``` shows "m mod n \ n" ``` haftmann@64635 ` 1034` ``` using assms eucl_rel_nat [of m n] ``` haftmann@64635 ` 1035` ``` by (auto elim: eucl_rel_nat.cases) ``` haftmann@64592 ` 1036` huffman@47136 ` 1037` ```instance proof ``` huffman@47136 ` 1038` ``` fix m n :: nat ``` huffman@47136 ` 1039` ``` show "m div n * n + m mod n = m" ``` haftmann@64635 ` 1040` ``` using eucl_rel_nat [of m n] ``` haftmann@64635 ` 1041` ``` by (auto elim: eucl_rel_nat.cases) ``` huffman@47136 ` 1042` ```next ``` haftmann@64592 ` 1043` ``` fix n :: nat show "n div 0 = 0" ``` haftmann@64592 ` 1044` ``` by (simp add: div_nat_def Divides.divmod_nat_zero) ``` haftmann@64592 ` 1045` ```next ``` haftmann@64592 ` 1046` ``` fix m n :: nat ``` haftmann@64592 ` 1047` ``` assume "n \ 0" ``` haftmann@64592 ` 1048` ``` then show "m * n div n = m" ``` haftmann@64635 ` 1049` ``` by (auto intro!: eucl_rel_natI div_nat_unique [of _ _ _ 0]) ``` haftmann@64592 ` 1050` ```qed (simp_all add: unit_factor_nat_def) ``` haftmann@64592 ` 1051` haftmann@64592 ` 1052` ```end ``` haftmann@64592 ` 1053` haftmann@64592 ` 1054` ```instance nat :: semiring_div ``` haftmann@64592 ` 1055` ```proof ``` huffman@47136 ` 1056` ``` fix m n q :: nat ``` huffman@47136 ` 1057` ``` assume "n \ 0" ``` huffman@47136 ` 1058` ``` then show "(q + m * n) div n = m + q div n" ``` huffman@47136 ` 1059` ``` by (induct m) (simp_all add: le_div_geq) ``` huffman@47136 ` 1060` ```next ``` huffman@47136 ` 1061` ``` fix m n q :: nat ``` huffman@47136 ` 1062` ``` assume "m \ 0" ``` haftmann@64635 ` 1063` ``` show "(m * n) div (m * q) = n div q" ``` haftmann@64635 ` 1064` ``` proof (cases "q = 0") ``` haftmann@64635 ` 1065` ``` case True ``` haftmann@64635 ` 1066` ``` then show ?thesis ``` haftmann@64635 ` 1067` ``` by simp ``` haftmann@64635 ` 1068` ``` next ``` haftmann@64635 ` 1069` ``` case False ``` haftmann@64635 ` 1070` ``` show ?thesis ``` haftmann@64635 ` 1071` ``` proof (rule div_nat_unique [of _ _ _ "m * (n mod q)"]) ``` haftmann@64635 ` 1072` ``` show "eucl_rel_nat (m * n) (m * q) (n div q, m * (n mod q))" ``` haftmann@64635 ` 1073` ``` by (rule eucl_rel_natI) ``` haftmann@64635 ` 1074` ``` (use \m \ 0\ \q \ 0\ div_mult_mod_eq [of n q] in \auto simp add: algebra_simps distrib_left [symmetric]\) ``` haftmann@64635 ` 1075` ``` qed ``` haftmann@64635 ` 1076` ``` qed ``` haftmann@25942 ` 1077` ```qed ``` haftmann@26100 ` 1078` haftmann@64592 ` 1079` ```lemma div_by_Suc_0 [simp]: ``` haftmann@64592 ` 1080` ``` "m div Suc 0 = m" ``` haftmann@64592 ` 1081` ``` using div_by_1 [of m] by simp ``` haftmann@64592 ` 1082` haftmann@64592 ` 1083` ```lemma mod_by_Suc_0 [simp]: ``` haftmann@64592 ` 1084` ``` "m mod Suc 0 = 0" ``` haftmann@64592 ` 1085` ``` using mod_by_1 [of m] by simp ``` haftmann@64592 ` 1086` haftmann@64592 ` 1087` ```lemma mod_greater_zero_iff_not_dvd: ``` haftmann@64592 ` 1088` ``` fixes m n :: nat ``` haftmann@64592 ` 1089` ``` shows "m mod n > 0 \ \ n dvd m" ``` haftmann@64592 ` 1090` ``` by (simp add: dvd_eq_mod_eq_0) ``` haftmann@33361 ` 1091` haftmann@64785 ` 1092` ```instantiation nat :: unique_euclidean_semiring ``` haftmann@64785 ` 1093` ```begin ``` haftmann@64785 ` 1094` haftmann@64785 ` 1095` ```definition [simp]: ``` haftmann@64785 ` 1096` ``` "euclidean_size_nat = (id :: nat \ nat)" ``` haftmann@64785 ` 1097` haftmann@64785 ` 1098` ```definition [simp]: ``` haftmann@64785 ` 1099` ``` "uniqueness_constraint_nat = (top :: nat \ nat \ bool)" ``` haftmann@64785 ` 1100` haftmann@64785 ` 1101` ```instance ``` haftmann@64785 ` 1102` ``` by standard (use mult_le_mono2 [of 1] in \simp_all add: unit_factor_nat_def mod_greater_zero_iff_not_dvd\) ``` haftmann@64785 ` 1103` haftmann@64785 ` 1104` ```end ``` haftmann@64785 ` 1105` haftmann@63950 ` 1106` ```text \Simproc for cancelling @{const divide} and @{const modulo}\ ``` haftmann@25942 ` 1107` haftmann@64592 ` 1108` ```lemma (in semiring_modulo) cancel_div_mod_rules: ``` haftmann@64592 ` 1109` ``` "((a div b) * b + a mod b) + c = a + c" ``` haftmann@64592 ` 1110` ``` "(b * (a div b) + a mod b) + c = a + c" ``` haftmann@64592 ` 1111` ``` by (simp_all add: div_mult_mod_eq mult_div_mod_eq) ``` haftmann@64592 ` 1112` wenzelm@51299 ` 1113` ```ML_file "~~/src/Provers/Arith/cancel_div_mod.ML" ``` wenzelm@51299 ` 1114` wenzelm@60758 ` 1115` ```ML \ ``` wenzelm@43594 ` 1116` ```structure Cancel_Div_Mod_Nat = Cancel_Div_Mod ``` wenzelm@41550 ` 1117` ```( ``` haftmann@60352 ` 1118` ``` val div_name = @{const_name divide}; ``` haftmann@63950 ` 1119` ``` val mod_name = @{const_name modulo}; ``` haftmann@30934 ` 1120` ``` val mk_binop = HOLogic.mk_binop; ``` huffman@48561 ` 1121` ``` val mk_plus = HOLogic.mk_binop @{const_name Groups.plus}; ``` huffman@48561 ` 1122` ``` val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT; ``` huffman@48561 ` 1123` ``` fun mk_sum [] = HOLogic.zero ``` huffman@48561 ` 1124` ``` | mk_sum [t] = t ``` huffman@48561 ` 1125` ``` | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); ``` huffman@48561 ` 1126` ``` fun dest_sum tm = ``` huffman@48561 ` 1127` ``` if HOLogic.is_zero tm then [] ``` huffman@48561 ` 1128` ``` else ``` huffman@48561 ` 1129` ``` (case try HOLogic.dest_Suc tm of ``` huffman@48561 ` 1130` ``` SOME t => HOLogic.Suc_zero :: dest_sum t ``` huffman@48561 ` 1131` ``` | NONE => ``` huffman@48561 ` 1132` ``` (case try dest_plus tm of ``` huffman@48561 ` 1133` ``` SOME (t, u) => dest_sum t @ dest_sum u ``` huffman@48561 ` 1134` ``` | NONE => [tm])); ``` haftmann@25942 ` 1135` haftmann@64250 ` 1136` ``` val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules}; ``` haftmann@64250 ` 1137` haftmann@64250 ` 1138` ``` val prove_eq_sums = Arith_Data.prove_conv2 all_tac ``` haftmann@64250 ` 1139` ``` (Arith_Data.simp_all_tac @{thms add_0_left add_0_right ac_simps}) ``` wenzelm@41550 ` 1140` ```) ``` wenzelm@60758 ` 1141` ```\ ``` wenzelm@60758 ` 1142` haftmann@64592 ` 1143` ```simproc_setup cancel_div_mod_nat ("(m::nat) + n") = ``` haftmann@64592 ` 1144` ``` \K Cancel_Div_Mod_Nat.proc\ ``` haftmann@64592 ` 1145` haftmann@64592 ` 1146` ```lemma divmod_nat_if [code]: ``` haftmann@64592 ` 1147` ``` "Divides.divmod_nat m n = (if n = 0 \ m < n then (0, m) else ``` haftmann@64592 ` 1148` ``` let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))" ``` haftmann@64592 ` 1149` ``` by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq) ``` wenzelm@60758 ` 1150` haftmann@64593 ` 1151` ```lemma mod_Suc_eq [mod_simps]: ``` haftmann@64593 ` 1152` ``` "Suc (m mod n) mod n = Suc m mod n" ``` haftmann@64593 ` 1153` ```proof - ``` haftmann@64593 ` 1154` ``` have "(m mod n + 1) mod n = (m + 1) mod n" ``` haftmann@64593 ` 1155` ``` by (simp only: mod_simps) ``` haftmann@64593 ` 1156` ``` then show ?thesis ``` haftmann@64593 ` 1157` ``` by simp ``` haftmann@64593 ` 1158` ```qed ``` haftmann@64593 ` 1159` haftmann@64593 ` 1160` ```lemma mod_Suc_Suc_eq [mod_simps]: ``` haftmann@64593 ` 1161` ``` "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n" ``` haftmann@64593 ` 1162` ```proof - ``` haftmann@64593 ` 1163` ``` have "(m mod n + 2) mod n = (m + 2) mod n" ``` haftmann@64593 ` 1164` ``` by (simp only: mod_simps) ``` haftmann@64593 ` 1165` ``` then show ?thesis ``` haftmann@64593 ` 1166` ``` by simp ``` haftmann@64593 ` 1167` ```qed ``` haftmann@64593 ` 1168` wenzelm@60758 ` 1169` wenzelm@60758 ` 1170` ```subsubsection \Quotient\ ``` haftmann@26100 ` 1171` haftmann@26100 ` 1172` ```lemma div_geq: "0 < n \ \ m < n \ m div n = Suc ((m - n) div n)" ``` nipkow@29667 ` 1173` ```by (simp add: le_div_geq linorder_not_less) ``` haftmann@26100 ` 1174` haftmann@26100 ` 1175` ```lemma div_if: "0 < n \ m div n = (if m < n then 0 else Suc ((m - n) div n))" ``` nipkow@29667 ` 1176` ```by (simp add: div_geq) ``` haftmann@26100 ` 1177` haftmann@26100 ` 1178` ```lemma div_mult_self_is_m [simp]: "0 (m*n) div n = (m::nat)" ``` nipkow@29667 ` 1179` ```by simp ``` haftmann@26100 ` 1180` haftmann@26100 ` 1181` ```lemma div_mult_self1_is_m [simp]: "0 (n*m) div n = (m::nat)" ``` nipkow@29667 ` 1182` ```by simp ``` haftmann@26100 ` 1183` haftmann@53066 ` 1184` ```lemma div_positive: ``` haftmann@53066 ` 1185` ``` fixes m n :: nat ``` haftmann@53066 ` 1186` ``` assumes "n > 0" ``` haftmann@53066 ` 1187` ``` assumes "m \ n" ``` haftmann@53066 ` 1188` ``` shows "m div n > 0" ``` haftmann@53066 ` 1189` ```proof - ``` wenzelm@60758 ` 1190` ``` from \m \ n\ obtain q where "m = n + q" ``` haftmann@53066 ` 1191` ``` by (auto simp add: le_iff_add) ``` eberlm@63499 ` 1192` ``` with \n > 0\ show ?thesis by (simp add: div_add_self1) ``` haftmann@53066 ` 1193` ```qed ``` haftmann@53066 ` 1194` hoelzl@59000 ` 1195` ```lemma div_eq_0_iff: "(a div b::nat) = 0 \ a < b \ b = 0" ``` haftmann@64592 ` 1196` ``` by auto (metis div_positive less_numeral_extra(3) not_less) ``` haftmann@64592 ` 1197` haftmann@25942 ` 1198` wenzelm@60758 ` 1199` ```subsubsection \Remainder\ ``` haftmann@25942 ` 1200` haftmann@51173 ` 1201` ```lemma mod_Suc_le_divisor [simp]: ``` haftmann@51173 ` 1202` ``` "m mod Suc n \ n" ``` haftmann@51173 ` 1203` ``` using mod_less_divisor [of "Suc n" m] by arith ``` haftmann@51173 ` 1204` haftmann@26100 ` 1205` ```lemma mod_less_eq_dividend [simp]: ``` haftmann@26100 ` 1206` ``` fixes m n :: nat ``` haftmann@26100 ` 1207` ``` shows "m mod n \ m" ``` haftmann@26100 ` 1208` ```proof (rule add_leD2) ``` haftmann@64242 ` 1209` ``` from div_mult_mod_eq have "m div n * n + m mod n = m" . ``` haftmann@26100 ` 1210` ``` then show "m div n * n + m mod n \ m" by auto ``` haftmann@26100 ` 1211` ```qed ``` haftmann@26100 ` 1212` wenzelm@61076 ` 1213` ```lemma mod_geq: "\ m < (n::nat) \ m mod n = (m - n) mod n" ``` nipkow@29667 ` 1214` ```by (simp add: le_mod_geq linorder_not_less) ``` paulson@14267 ` 1215` wenzelm@61076 ` 1216` ```lemma mod_if: "m mod (n::nat) = (if m < n then m else (m - n) mod n)" ``` nipkow@29667 ` 1217` ```by (simp add: le_mod_geq) ``` haftmann@26100 ` 1218` paulson@14267 ` 1219` wenzelm@60758 ` 1220` ```subsubsection \Quotient and Remainder\ ``` paulson@14267 ` 1221` haftmann@30923 ` 1222` ```lemma div_mult1_eq: ``` haftmann@30923 ` 1223` ``` "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)" ``` haftmann@64635 ` 1224` ``` by (cases "c = 0") ``` haftmann@64635 ` 1225` ``` (auto simp add: algebra_simps distrib_left [symmetric] ``` haftmann@64635 ` 1226` ``` intro!: div_nat_unique [of _ _ _ "(a * (b mod c)) mod c"] eucl_rel_natI) ``` haftmann@64635 ` 1227` haftmann@64635 ` 1228` ```lemma eucl_rel_nat_add1_eq: ``` haftmann@64635 ` 1229` ``` "eucl_rel_nat a c (aq, ar) \ eucl_rel_nat b c (bq, br) ``` haftmann@64635 ` 1230` ``` \ eucl_rel_nat (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)" ``` haftmann@64635 ` 1231` ``` by (auto simp add: split_ifs algebra_simps elim!: eucl_rel_nat.cases intro: eucl_rel_nat_by0 eucl_rel_natI) ``` paulson@14267 ` 1232` paulson@14267 ` 1233` ```(*NOT suitable for rewriting: the RHS has an instance of the LHS*) ``` paulson@14267 ` 1234` ```lemma div_add1_eq: ``` haftmann@64635 ` 1235` ``` "(a + b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)" ``` haftmann@64635 ` 1236` ```by (blast intro: eucl_rel_nat_add1_eq [THEN div_nat_unique] eucl_rel_nat) ``` haftmann@64635 ` 1237` haftmann@64635 ` 1238` ```lemma eucl_rel_nat_mult2_eq: ``` haftmann@64635 ` 1239` ``` assumes "eucl_rel_nat a b (q, r)" ``` haftmann@64635 ` 1240` ``` shows "eucl_rel_nat a (b * c) (q div c, b *(q mod c) + r)" ``` haftmann@64635 ` 1241` ```proof (cases "c = 0") ``` haftmann@64635 ` 1242` ``` case True ``` haftmann@64635 ` 1243` ``` with assms show ?thesis ``` haftmann@64635 ` 1244` ``` by (auto intro: eucl_rel_nat_by0 elim!: eucl_rel_nat.cases simp add: ac_simps) ``` haftmann@64635 ` 1245` ```next ``` haftmann@64635 ` 1246` ``` case False ``` haftmann@64635 ` 1247` ``` { assume "r < b" ``` haftmann@64635 ` 1248` ``` with False have "b * (q mod c) + r < b * c" ``` haftmann@60352 ` 1249` ``` apply (cut_tac m = q and n = c in mod_less_divisor) ``` haftmann@60352 ` 1250` ``` apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto) ``` haftmann@60352 ` 1251` ``` apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst) ``` haftmann@60352 ` 1252` ``` apply (simp add: add_mult_distrib2) ``` haftmann@60352 ` 1253` ``` done ``` haftmann@60352 ` 1254` ``` then have "r + b * (q mod c) < b * c" ``` haftmann@60352 ` 1255` ``` by (simp add: ac_simps) ``` haftmann@64635 ` 1256` ``` } with assms False show ?thesis ``` haftmann@64635 ` 1257` ``` by (auto simp add: algebra_simps add_mult_distrib2 [symmetric] elim!: eucl_rel_nat.cases intro: eucl_rel_nat.intros) ``` haftmann@60352 ` 1258` ```qed ``` lp15@60562 ` 1259` blanchet@55085 ` 1260` ```lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)" ``` haftmann@64635 ` 1261` ```by (force simp add: eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN div_nat_unique]) ``` paulson@14267 ` 1262` blanchet@55085 ` 1263` ```lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)" ``` haftmann@64635 ` 1264` ```by (auto simp add: mult.commute eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN mod_nat_unique]) ``` paulson@14267 ` 1265` haftmann@61275 ` 1266` ```instantiation nat :: semiring_numeral_div ``` haftmann@61275 ` 1267` ```begin ``` haftmann@61275 ` 1268` haftmann@61275 ` 1269` ```definition divmod_nat :: "num \ num \ nat \ nat" ``` haftmann@61275 ` 1270` ```where ``` haftmann@61275 ` 1271` ``` divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)" ``` haftmann@61275 ` 1272` haftmann@61275 ` 1273` ```definition divmod_step_nat :: "num \ nat \ nat \ nat \ nat" ``` haftmann@61275 ` 1274` ```where ``` haftmann@61275 ` 1275` ``` "divmod_step_nat l qr = (let (q, r) = qr ``` haftmann@61275 ` 1276` ``` in if r \ numeral l then (2 * q + 1, r - numeral l) ``` haftmann@61275 ` 1277` ``` else (2 * q, r))" ``` haftmann@61275 ` 1278` haftmann@61275 ` 1279` ```instance ``` haftmann@61275 ` 1280` ``` by standard (auto intro: div_positive simp add: divmod'_nat_def divmod_step_nat_def mod_mult2_eq div_mult2_eq) ``` haftmann@61275 ` 1281` haftmann@61275 ` 1282` ```end ``` haftmann@61275 ` 1283` haftmann@61275 ` 1284` ```declare divmod_algorithm_code [where ?'a = nat, code] ``` haftmann@61275 ` 1285` ``` ``` paulson@14267 ` 1286` wenzelm@60758 ` 1287` ```subsubsection \Further Facts about Quotient and Remainder\ ``` paulson@14267 ` 1288` haftmann@64592 ` 1289` ```lemma div_le_mono: ``` haftmann@64592 ` 1290` ``` fixes m n k :: nat ``` haftmann@64592 ` 1291` ``` assumes "m \ n" ``` haftmann@64592 ` 1292` ``` shows "m div k \ n div k" ``` haftmann@64592 ` 1293` ```proof - ``` haftmann@64592 ` 1294` ``` from assms obtain q where "n = m + q" ``` haftmann@64592 ` 1295` ``` by (auto simp add: le_iff_add) ``` haftmann@64592 ` 1296` ``` then show ?thesis ``` haftmann@64592 ` 1297` ``` by (simp add: div_add1_eq [of m q k]) ``` haftmann@64592 ` 1298` ```qed ``` paulson@14267 ` 1299` paulson@14267 ` 1300` ```(* Antimonotonicity of div in second argument *) ``` paulson@14267 ` 1301` ```lemma div_le_mono2: "!!m::nat. [| 0n |] ==> (k div n) \ (k div m)" ``` paulson@14267 ` 1302` ```apply (subgoal_tac "0 (k-m) div n") ``` paulson@14267 ` 1311` ``` prefer 2 ``` paulson@14267 ` 1312` ``` apply (blast intro: div_le_mono diff_le_mono2) ``` paulson@14267 ` 1313` ```apply (rule le_trans, simp) ``` nipkow@15439 ` 1314` ```apply (simp) ``` paulson@14267 ` 1315` ```done ``` paulson@14267 ` 1316` paulson@14267 ` 1317` ```lemma div_le_dividend [simp]: "m div n \ (m::nat)" ``` paulson@14267 ` 1318` ```apply (case_tac "n=0", simp) ``` paulson@14267 ` 1319` ```apply (subgoal_tac "m div n \ m div 1", simp) ``` paulson@14267 ` 1320` ```apply (rule div_le_mono2) ``` paulson@14267 ` 1321` ```apply (simp_all (no_asm_simp)) ``` paulson@14267 ` 1322` ```done ``` paulson@14267 ` 1323` wenzelm@22718 ` 1324` ```(* Similar for "less than" *) ``` huffman@47138 ` 1325` ```lemma div_less_dividend [simp]: ``` huffman@47138 ` 1326` ``` "\(1::nat) < n; 0 < m\ \ m div n < m" ``` huffman@47138 ` 1327` ```apply (induct m rule: nat_less_induct) ``` paulson@14267 ` 1328` ```apply (rename_tac "m") ``` paulson@14267 ` 1329` ```apply (case_tac "mA fact for the mutilated chess board\ ``` paulson@14267 ` 1341` ```lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))" ``` paulson@14267 ` 1342` ```apply (case_tac "n=0", simp) ``` paulson@15251 ` 1343` ```apply (induct "m" rule: nat_less_induct) ``` paulson@14267 ` 1344` ```apply (case_tac "Suc (na) Suc(na) *) ``` paulson@16796 ` 1348` ```apply (simp add: linorder_not_less le_Suc_eq mod_geq) ``` nipkow@15439 ` 1349` ```apply (auto simp add: Suc_diff_le le_mod_geq) ``` paulson@14267 ` 1350` ```done ``` paulson@14267 ` 1351` paulson@14267 ` 1352` ```lemma mod_eq_0_iff: "(m mod d = 0) = (\q::nat. m = d*q)" ``` nipkow@29667 ` 1353` ```by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def) ``` paulson@17084 ` 1354` wenzelm@22718 ` 1355` ```lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1] ``` paulson@14267 ` 1356` paulson@14267 ` 1357` ```(*Loses information, namely we also have rq. m = r + q * d" ``` haftmann@57514 ` 1362` ```proof - ``` haftmann@64242 ` 1363` ``` from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast ``` haftmann@57514 ` 1364` ``` with assms have "m = r + q * d" by simp ``` haftmann@57514 ` 1365` ``` then show ?thesis .. ``` haftmann@57514 ` 1366` ```qed ``` paulson@14267 ` 1367` nipkow@13152 ` 1368` ```lemma split_div: ``` nipkow@13189 ` 1369` ``` "P(n div k :: nat) = ``` nipkow@13189 ` 1370` ``` ((k = 0 \ P 0) \ (k \ 0 \ (!i. !j P i)))" ``` nipkow@13189 ` 1371` ``` (is "?P = ?Q" is "_ = (_ \ (_ \ ?R))") ``` nipkow@13189 ` 1372` ```proof ``` nipkow@13189 ` 1373` ``` assume P: ?P ``` nipkow@13189 ` 1374` ``` show ?Q ``` nipkow@13189 ` 1375` ``` proof (cases) ``` nipkow@13189 ` 1376` ``` assume "k = 0" ``` haftmann@27651 ` 1377` ``` with P show ?Q by simp ``` nipkow@13189 ` 1378` ``` next ``` nipkow@13189 ` 1379` ``` assume not0: "k \ 0" ``` nipkow@13189 ` 1380` ``` thus ?Q ``` nipkow@13189 ` 1381` ``` proof (simp, intro allI impI) ``` nipkow@13189 ` 1382` ``` fix i j ``` nipkow@13189 ` 1383` ``` assume n: "n = k*i + j" and j: "j < k" ``` nipkow@13189 ` 1384` ``` show "P i" ``` nipkow@13189 ` 1385` ``` proof (cases) ``` wenzelm@22718 ` 1386` ``` assume "i = 0" ``` wenzelm@22718 ` 1387` ``` with n j P show "P i" by simp ``` nipkow@13189 ` 1388` ``` next ``` wenzelm@22718 ` 1389` ``` assume "i \ 0" ``` haftmann@57514 ` 1390` ``` with not0 n j P show "P i" by(simp add:ac_simps) ``` nipkow@13189 ` 1391` ``` qed ``` nipkow@13189 ` 1392` ``` qed ``` nipkow@13189 ` 1393` ``` qed ``` nipkow@13189 ` 1394` ```next ``` nipkow@13189 ` 1395` ``` assume Q: ?Q ``` nipkow@13189 ` 1396` ``` show ?P ``` nipkow@13189 ` 1397` ``` proof (cases) ``` nipkow@13189 ` 1398` ``` assume "k = 0" ``` haftmann@27651 ` 1399` ``` with Q show ?P by simp ``` nipkow@13189 ` 1400` ``` next ``` nipkow@13189 ` 1401` ``` assume not0: "k \ 0" ``` nipkow@13189 ` 1402` ``` with Q have R: ?R by simp ``` nipkow@13189 ` 1403` ``` from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"] ``` nipkow@13517 ` 1404` ``` show ?P by simp ``` nipkow@13189 ` 1405` ``` qed ``` nipkow@13189 ` 1406` ```qed ``` nipkow@13189 ` 1407` berghofe@13882 ` 1408` ```lemma split_div_lemma: ``` haftmann@26100 ` 1409` ``` assumes "0 < n" ``` wenzelm@61076 ` 1410` ``` shows "n * q \ m \ m < n * Suc q \ q = ((m::nat) div n)" (is "?lhs \ ?rhs") ``` haftmann@26100 ` 1411` ```proof ``` haftmann@26100 ` 1412` ``` assume ?rhs ``` haftmann@64246 ` 1413` ``` with minus_mod_eq_mult_div [symmetric] have nq: "n * q = m - (m mod n)" by simp ``` haftmann@26100 ` 1414` ``` then have A: "n * q \ m" by simp ``` haftmann@26100 ` 1415` ``` have "n - (m mod n) > 0" using mod_less_divisor assms by auto ``` haftmann@26100 ` 1416` ``` then have "m < m + (n - (m mod n))" by simp ``` haftmann@26100 ` 1417` ``` then have "m < n + (m - (m mod n))" by simp ``` haftmann@26100 ` 1418` ``` with nq have "m < n + n * q" by simp ``` haftmann@26100 ` 1419` ``` then have B: "m < n * Suc q" by simp ``` haftmann@26100 ` 1420` ``` from A B show ?lhs .. ``` haftmann@26100 ` 1421` ```next ``` haftmann@26100 ` 1422` ``` assume P: ?lhs ``` haftmann@64635 ` 1423` ``` then have "eucl_rel_nat m n (q, m - n * q)" ``` haftmann@64635 ` 1424` ``` by (auto intro: eucl_rel_natI simp add: ac_simps) ``` haftmann@61433 ` 1425` ``` then have "m div n = q" ``` haftmann@61433 ` 1426` ``` by (rule div_nat_unique) ``` haftmann@30923 ` 1427` ``` then show ?rhs by simp ``` haftmann@26100 ` 1428` ```qed ``` berghofe@13882 ` 1429` berghofe@13882 ` 1430` ```theorem split_div': ``` berghofe@13882 ` 1431` ``` "P ((m::nat) div n) = ((n = 0 \ P 0) \ ``` paulson@14267 ` 1432` ``` (\q. (n * q \ m \ m < n * (Suc q)) \ P q))" ``` haftmann@61433 ` 1433` ``` apply (cases "0 < n") ``` berghofe@13882 ` 1434` ``` apply (simp only: add: split_div_lemma) ``` haftmann@27651 ` 1435` ``` apply simp_all ``` berghofe@13882 ` 1436` ``` done ``` berghofe@13882 ` 1437` nipkow@13189 ` 1438` ```lemma split_mod: ``` nipkow@13189 ` 1439` ``` "P(n mod k :: nat) = ``` nipkow@13189 ` 1440` ``` ((k = 0 \ P n) \ (k \ 0 \ (!i. !j P j)))" ``` nipkow@13189 ` 1441` ``` (is "?P = ?Q" is "_ = (_ \ (_ \ ?R))") ``` nipkow@13189 ` 1442` ```proof ``` nipkow@13189 ` 1443` ``` assume P: ?P ``` nipkow@13189 ` 1444` ``` show ?Q ``` nipkow@13189 ` 1445` ``` proof (cases) ``` nipkow@13189 ` 1446` ``` assume "k = 0" ``` haftmann@27651 ` 1447` ``` with P show ?Q by simp ``` nipkow@13189 ` 1448` ``` next ``` nipkow@13189 ` 1449` ``` assume not0: "k \ 0" ``` nipkow@13189 ` 1450` ``` thus ?Q ``` nipkow@13189 ` 1451` ``` proof (simp, intro allI impI) ``` nipkow@13189 ` 1452` ``` fix i j ``` nipkow@13189 ` 1453` ``` assume "n = k*i + j" "j < k" ``` haftmann@58786 ` 1454` ``` thus "P j" using not0 P by (simp add: ac_simps) ``` nipkow@13189 ` 1455` ``` qed ``` nipkow@13189 ` 1456` ``` qed ``` nipkow@13189 ` 1457` ```next ``` nipkow@13189 ` 1458` ``` assume Q: ?Q ``` nipkow@13189 ` 1459` ``` show ?P ``` nipkow@13189 ` 1460` ``` proof (cases) ``` nipkow@13189 ` 1461` ``` assume "k = 0" ``` haftmann@27651 ` 1462` ``` with Q show ?P by simp ``` nipkow@13189 ` 1463` ``` next ``` nipkow@13189 ` 1464` ``` assume not0: "k \ 0" ``` nipkow@13189 ` 1465` ``` with Q have R: ?R by simp ``` nipkow@13189 ` 1466` ``` from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"] ``` nipkow@13517 ` 1467` ``` show ?P by simp ``` nipkow@13189 ` 1468` ``` qed ``` nipkow@13189 ` 1469` ```qed ``` nipkow@13189 ` 1470` noschinl@52398 ` 1471` ```lemma div_eq_dividend_iff: "a \ 0 \ (a :: nat) div b = a \ b = 1" ``` noschinl@52398 ` 1472` ``` apply rule ``` noschinl@52398 ` 1473` ``` apply (cases "b = 0") ``` noschinl@52398 ` 1474` ``` apply simp_all ``` noschinl@52398 ` 1475` ``` apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3) ``` noschinl@52398 ` 1476` ``` done ``` noschinl@52398 ` 1477` haftmann@63417 ` 1478` ```lemma (in field_char_0) of_nat_div: ``` haftmann@63417 ` 1479` ``` "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)" ``` haftmann@63417 ` 1480` ```proof - ``` haftmann@63417 ` 1481` ``` have "of_nat (m div n) = ((of_nat (m div n * n + m mod n) - of_nat (m mod n)) / of_nat n :: 'a)" ``` haftmann@63417 ` 1482` ``` unfolding of_nat_add by (cases "n = 0") simp_all ``` haftmann@63417 ` 1483` ``` then show ?thesis ``` haftmann@63417 ` 1484` ``` by simp ``` haftmann@63417 ` 1485` ```qed ``` haftmann@63417 ` 1486` haftmann@22800 ` 1487` wenzelm@60758 ` 1488` ```subsubsection \An ``induction'' law for modulus arithmetic.\ ``` paulson@14640 ` 1489` paulson@14640 ` 1490` ```lemma mod_induct_0: ``` paulson@14640 ` 1491` ``` assumes step: "\i P ((Suc i) mod p)" ``` paulson@14640 ` 1492` ``` and base: "P i" and i: "i(P 0)" ``` paulson@14640 ` 1496` ``` from i have p: "0k. 0 \ P (p-k)" (is "\k. ?A k") ``` paulson@14640 ` 1498` ``` proof ``` paulson@14640 ` 1499` ``` fix k ``` paulson@14640 ` 1500` ``` show "?A k" ``` paulson@14640 ` 1501` ``` proof (induct k) ``` wenzelm@61799 ` 1502` ``` show "?A 0" by simp \ "by contradiction" ``` paulson@14640 ` 1503` ``` next ``` paulson@14640 ` 1504` ``` fix n ``` paulson@14640 ` 1505` ``` assume ih: "?A n" ``` paulson@14640 ` 1506` ``` show "?A (Suc n)" ``` paulson@14640 ` 1507` ``` proof (clarsimp) ``` wenzelm@22718 ` 1508` ``` assume y: "P (p - Suc n)" ``` wenzelm@22718 ` 1509` ``` have n: "Suc n < p" ``` wenzelm@22718 ` 1510` ``` proof (rule ccontr) ``` wenzelm@22718 ` 1511` ``` assume "\(Suc n < p)" ``` wenzelm@22718 ` 1512` ``` hence "p - Suc n = 0" ``` wenzelm@22718 ` 1513` ``` by simp ``` wenzelm@22718 ` 1514` ``` with y contra show "False" ``` wenzelm@22718 ` 1515` ``` by simp ``` wenzelm@22718 ` 1516` ``` qed ``` wenzelm@22718 ` 1517` ``` hence n2: "Suc (p - Suc n) = p-n" by arith ``` wenzelm@22718 ` 1518` ``` from p have "p - Suc n < p" by arith ``` wenzelm@22718 ` 1519` ``` with y step have z: "P ((Suc (p - Suc n)) mod p)" ``` wenzelm@22718 ` 1520` ``` by blast ``` wenzelm@22718 ` 1521` ``` show "False" ``` wenzelm@22718 ` 1522` ``` proof (cases "n=0") ``` wenzelm@22718 ` 1523` ``` case True ``` wenzelm@22718 ` 1524` ``` with z n2 contra show ?thesis by simp ``` wenzelm@22718 ` 1525` ``` next ``` wenzelm@22718 ` 1526` ``` case False ``` wenzelm@22718 ` 1527` ``` with p have "p-n < p" by arith ``` wenzelm@22718 ` 1528` ``` with z n2 False ih show ?thesis by simp ``` wenzelm@22718 ` 1529` ``` qed ``` paulson@14640 ` 1530` ``` qed ``` paulson@14640 ` 1531` ``` qed ``` paulson@14640 ` 1532` ``` qed ``` paulson@14640 ` 1533` ``` moreover ``` paulson@14640 ` 1534` ``` from i obtain k where "0 i+k=p" ``` paulson@14640 ` 1535` ``` by (blast dest: less_imp_add_positive) ``` paulson@14640 ` 1536` ``` hence "0 i=p-k" by auto ``` paulson@14640 ` 1537` ``` moreover ``` paulson@14640 ` 1538` ``` note base ``` paulson@14640 ` 1539` ``` ultimately ``` paulson@14640 ` 1540` ``` show "False" by blast ``` paulson@14640 ` 1541` ```qed ``` paulson@14640 ` 1542` paulson@14640 ` 1543` ```lemma mod_induct: ``` paulson@14640 ` 1544` ``` assumes step: "\i P ((Suc i) mod p)" ``` paulson@14640 ` 1545` ``` and base: "P i" and i: "ij P j" (is "?A j") ``` paulson@14640 ` 1552` ``` proof (induct j) ``` paulson@14640 ` 1553` ``` from step base i show "?A 0" ``` wenzelm@22718 ` 1554` ``` by (auto elim: mod_induct_0) ``` paulson@14640 ` 1555` ``` next ``` paulson@14640 ` 1556` ``` fix k ``` paulson@14640 ` 1557` ``` assume ih: "?A k" ``` paulson@14640 ` 1558` ``` show "?A (Suc k)" ``` paulson@14640 ` 1559` ``` proof ``` wenzelm@22718 ` 1560` ``` assume suc: "Suc k < p" ``` wenzelm@22718 ` 1561` ``` hence k: "k m mod 2 = 1" ``` haftmann@33296 ` 1586` ```proof - ``` boehmes@35815 ` 1587` ``` { fix n :: nat have "(n::nat) < 2 \ n = 0 \ n = 1" by (cases n) simp_all } ``` haftmann@33296 ` 1588` ``` moreover have "m mod 2 < 2" by simp ``` haftmann@33296 ` 1589` ``` ultimately have "m mod 2 = 0 \ m mod 2 = 1" . ``` haftmann@33296 ` 1590` ``` then show ?thesis by auto ``` haftmann@33296 ` 1591` ```qed ``` haftmann@33296 ` 1592` wenzelm@60758 ` 1593` ```text\These lemmas collapse some needless occurrences of Suc: ``` haftmann@33296 ` 1594` ``` at least three Sucs, since two and fewer are rewritten back to Suc again! ``` wenzelm@60758 ` 1595` ``` We already have some rules to simplify operands smaller than 3.\ ``` haftmann@33296 ` 1596` haftmann@33296 ` 1597` ```lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)" ``` haftmann@33296 ` 1598` ```by (simp add: Suc3_eq_add_3) ``` haftmann@33296 ` 1599` haftmann@33296 ` 1600` ```lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)" ``` haftmann@33296 ` 1601` ```by (simp add: Suc3_eq_add_3) ``` haftmann@33296 ` 1602` haftmann@33296 ` 1603` ```lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n" ``` haftmann@33296 ` 1604` ```by (simp add: Suc3_eq_add_3) ``` haftmann@33296 ` 1605` haftmann@33296 ` 1606` ```lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n" ``` haftmann@33296 ` 1607` ```by (simp add: Suc3_eq_add_3) ``` haftmann@33296 ` 1608` huffman@47108 ` 1609` ```lemmas Suc_div_eq_add3_div_numeral [simp] = Suc_div_eq_add3_div [of _ "numeral v"] for v ``` huffman@47108 ` 1610` ```lemmas Suc_mod_eq_add3_mod_numeral [simp] = Suc_mod_eq_add3_mod [of _ "numeral v"] for v ``` haftmann@33296 ` 1611` lp15@60562 ` 1612` ```lemma Suc_times_mod_eq: "1 Suc (k * m) mod k = 1" ``` haftmann@33361 ` 1613` ```apply (induct "m") ``` haftmann@33361 ` 1614` ```apply (simp_all add: mod_Suc) ``` haftmann@33361 ` 1615` ```done ``` haftmann@33361 ` 1616` huffman@47108 ` 1617` ```declare Suc_times_mod_eq [of "numeral w", simp] for w ``` haftmann@33361 ` 1618` huffman@47138 ` 1619` ```lemma Suc_div_le_mono [simp]: "n div k \ (Suc n) div k" ``` huffman@47138 ` 1620` ```by (simp add: div_le_mono) ``` haftmann@33361 ` 1621` haftmann@33361 ` 1622` ```lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2" ``` haftmann@33361 ` 1623` ```by (cases n) simp_all ``` haftmann@33361 ` 1624` boehmes@35815 ` 1625` ```lemma div_2_gt_zero [simp]: assumes A: "(1::nat) < n" shows "0 < n div 2" ``` boehmes@35815 ` 1626` ```proof - ``` boehmes@35815 ` 1627` ``` from A have B: "0 < n - 1" and C: "n - 1 + 1 = n" by simp_all ``` lp15@60562 ` 1628` ``` from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp ``` boehmes@35815 ` 1629` ```qed ``` haftmann@33361 ` 1630` haftmann@33361 ` 1631` ```lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n" ``` haftmann@33361 ` 1632` ```proof - ``` haftmann@33361 ` 1633` ``` have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp ``` lp15@60562 ` 1634` ``` also have "... = Suc m mod n" by (rule mod_mult_self3) ``` haftmann@33361 ` 1635` ``` finally show ?thesis . ``` haftmann@33361 ` 1636` ```qed ``` haftmann@33361 ` 1637` haftmann@33361 ` 1638` ```lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n" ``` lp15@60562 ` 1639` ```apply (subst mod_Suc [of m]) ``` lp15@60562 ` 1640` ```apply (subst mod_Suc [of "m mod n"], simp) ``` haftmann@33361 ` 1641` ```done ``` haftmann@33361 ` 1642` huffman@47108 ` 1643` ```lemma mod_2_not_eq_zero_eq_one_nat: ``` huffman@47108 ` 1644` ``` fixes n :: nat ``` huffman@47108 ` 1645` ``` shows "n mod 2 \ 0 \ n mod 2 = 1" ``` haftmann@58786 ` 1646` ``` by (fact not_mod_2_eq_0_eq_1) ``` lp15@60562 ` 1647` haftmann@58778 ` 1648` ```lemma even_Suc_div_two [simp]: ``` haftmann@58778 ` 1649` ``` "even n \ Suc n div 2 = n div 2" ``` haftmann@58778 ` 1650` ``` using even_succ_div_two [of n] by simp ``` lp15@60562 ` 1651` haftmann@58778 ` 1652` ```lemma odd_Suc_div_two [simp]: ``` haftmann@58778 ` 1653` ``` "odd n \ Suc n div 2 = Suc (n div 2)" ``` haftmann@58778 ` 1654` ``` using odd_succ_div_two [of n] by simp ``` haftmann@58778 ` 1655` haftmann@58834 ` 1656` ```lemma odd_two_times_div_two_nat [simp]: ``` haftmann@60352 ` 1657` ``` assumes "odd n" ``` haftmann@60352 ` 1658` ``` shows "2 * (n div 2) = n - (1 :: nat)" ``` haftmann@60352 ` 1659` ```proof - ``` haftmann@60352 ` 1660` ``` from assms have "2 * (n div 2) + 1 = n" ``` haftmann@60352 ` 1661` ``` by (rule odd_two_times_div_two_succ) ``` haftmann@60352 ` 1662` ``` then have "Suc (2 * (n div 2)) - 1 = n - 1" ``` haftmann@60352 ` 1663` ``` by simp ``` haftmann@60352 ` 1664` ``` then show ?thesis ``` haftmann@60352 ` 1665` ``` by simp ``` haftmann@60352 ` 1666` ```qed ``` haftmann@58778 ` 1667` haftmann@58778 ` 1668` ```lemma parity_induct [case_names zero even odd]: ``` haftmann@58778 ` 1669` ``` assumes zero: "P 0" ``` haftmann@58778 ` 1670` ``` assumes even: "\n. P n \ P (2 * n)" ``` haftmann@58778 ` 1671` ``` assumes odd: "\n. P n \ P (Suc (2 * n))" ``` haftmann@58778 ` 1672` ``` shows "P n" ``` haftmann@58778 ` 1673` ```proof (induct n rule: less_induct) ``` haftmann@58778 ` 1674` ``` case (less n) ``` haftmann@58778 ` 1675` ``` show "P n" ``` haftmann@58778 ` 1676` ``` proof (cases "n = 0") ``` haftmann@58778 ` 1677` ``` case True with zero show ?thesis by simp ``` haftmann@58778 ` 1678` ``` next ``` haftmann@58778 ` 1679` ``` case False ``` haftmann@58778 ` 1680` ``` with less have hyp: "P (n div 2)" by simp ``` haftmann@58778 ` 1681` ``` show ?thesis ``` haftmann@58778 ` 1682` ``` proof (cases "even n") ``` haftmann@58778 ` 1683` ``` case True ``` haftmann@58778 ` 1684` ``` with hyp even [of "n div 2"] show ?thesis ``` haftmann@58834 ` 1685` ``` by simp ``` haftmann@58778 ` 1686` ``` next ``` haftmann@58778 ` 1687` ``` case False ``` lp15@60562 ` 1688` ``` with hyp odd [of "n div 2"] show ?thesis ``` haftmann@58834 ` 1689` ``` by simp ``` haftmann@58778 ` 1690` ``` qed ``` haftmann@58778 ` 1691` ``` qed ``` haftmann@58778 ` 1692` ```qed ``` haftmann@58778 ` 1693` haftmann@60868 ` 1694` ```lemma Suc_0_div_numeral [simp]: ``` haftmann@60868 ` 1695` ``` fixes k l :: num ``` haftmann@60868 ` 1696` ``` shows "Suc 0 div numeral k = fst (divmod Num.One k)" ``` haftmann@60868 ` 1697` ``` by (simp_all add: fst_divmod) ``` haftmann@60868 ` 1698` haftmann@60868 ` 1699` ```lemma Suc_0_mod_numeral [simp]: ``` haftmann@60868 ` 1700` ``` fixes k l :: num ``` haftmann@60868 ` 1701` ``` shows "Suc 0 mod numeral k = snd (divmod Num.One k)" ``` haftmann@60868 ` 1702` ``` by (simp_all add: snd_divmod) ``` haftmann@60868 ` 1703` haftmann@33361 ` 1704` wenzelm@60758 ` 1705` ```subsection \Division on @{typ int}\ ``` haftmann@33361 ` 1706` haftmann@64592 ` 1707` ```context ``` haftmann@64592 ` 1708` ```begin ``` haftmann@64592 ` 1709` haftmann@64635 ` 1710` ```inductive eucl_rel_int :: "int \ int \ int \ int \ bool" ``` haftmann@64635 ` 1711` ``` where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)" ``` haftmann@64635 ` 1712` ``` | eucl_rel_int_dividesI: "l \ 0 \ k = q * l \ eucl_rel_int k l (q, 0)" ``` haftmann@64635 ` 1713` ``` | eucl_rel_int_remainderI: "sgn r = sgn l \ \r\ < \l\ ``` haftmann@64635 ` 1714` ``` \ k = q * l + r \ eucl_rel_int k l (q, r)" ``` haftmann@64635 ` 1715` haftmann@64635 ` 1716` ```lemma eucl_rel_int_iff: ``` haftmann@64635 ` 1717` ``` "eucl_rel_int k l (q, r) \ ``` haftmann@64635 ` 1718` ``` k = l * q + r \ ``` haftmann@64635 ` 1719` ``` (if 0 < l then 0 \ r \ r < l else if l < 0 then l < r \ r \ 0 else q = 0)" ``` haftmann@64635 ` 1720` ``` by (cases "r = 0") ``` haftmann@64635 ` 1721` ``` (auto elim!: eucl_rel_int.cases intro: eucl_rel_int_by0 eucl_rel_int_dividesI eucl_rel_int_remainderI ``` haftmann@64635 ` 1722` ``` simp add: ac_simps sgn_1_pos sgn_1_neg) ``` haftmann@33361 ` 1723` haftmann@33361 ` 1724` ```lemma unique_quotient_lemma: ``` haftmann@60868 ` 1725` ``` "b * q' + r' \ b * q + r \ 0 \ r' \ r' < b \ r < b \ q' \ (q::int)" ``` haftmann@33361 ` 1726` ```apply (subgoal_tac "r' + b * (q'-q) \ r") ``` haftmann@33361 ` 1727` ``` prefer 2 apply (simp add: right_diff_distrib) ``` haftmann@33361 ` 1728` ```apply (subgoal_tac "0 < b * (1 + q - q') ") ``` haftmann@33361 ` 1729` ```apply (erule_tac [2] order_le_less_trans) ``` webertj@49962 ` 1730` ``` prefer 2 apply (simp add: right_diff_distrib distrib_left) ``` haftmann@33361 ` 1731` ```apply (subgoal_tac "b * q' < b * (1 + q) ") ``` webertj@49962 ` 1732` ``` prefer 2 apply (simp add: right_diff_distrib distrib_left) ``` haftmann@33361 ` 1733` ```apply (simp add: mult_less_cancel_left) ``` haftmann@33361 ` 1734` ```done ``` haftmann@33361 ` 1735` haftmann@33361 ` 1736` ```lemma unique_quotient_lemma_neg: ``` haftmann@60868 ` 1737` ``` "b * q' + r' \ b*q + r \ r \ 0 \ b < r \ b < r' \ q \ (q'::int)" ``` haftmann@60868 ` 1738` ``` by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma) auto ``` haftmann@33361 ` 1739` haftmann@33361 ` 1740` ```lemma unique_quotient: ``` haftmann@64635 ` 1741` ``` "eucl_rel_int a b (q, r) \ eucl_rel_int a b (q', r') \ q = q'" ``` haftmann@64635 ` 1742` ``` apply (simp add: eucl_rel_int_iff linorder_neq_iff split: if_split_asm) ``` haftmann@64635 ` 1743` ``` apply (blast intro: order_antisym ``` haftmann@64635 ` 1744` ``` dest: order_eq_refl [THEN unique_quotient_lemma] ``` haftmann@64635 ` 1745` ``` order_eq_refl [THEN unique_quotient_lemma_neg] sym)+ ``` haftmann@64635 ` 1746` ``` done ``` haftmann@33361 ` 1747` haftmann@33361 ` 1748` ```lemma unique_remainder: ``` haftmann@64635 ` 1749` ``` "eucl_rel_int a b (q, r) \ eucl_rel_int a b (q', r') \ r = r'" ``` haftmann@33361 ` 1750` ```apply (subgoal_tac "q = q'") ``` haftmann@64635 ` 1751` ``` apply (simp add: eucl_rel_int_iff) ``` haftmann@33361 ` 1752` ```apply (blast intro: unique_quotient) ``` haftmann@33361 ` 1753` ```done ``` haftmann@33361 ` 1754` haftmann@64592 ` 1755` ```end ``` haftmann@64592 ` 1756` haftmann@64592 ` 1757` ```instantiation int :: "{idom_modulo, normalization_semidom}" ``` haftmann@60868 ` 1758` ```begin ``` haftmann@60868 ` 1759` haftmann@64592 ` 1760` ```definition normalize_int :: "int \ int" ``` haftmann@64592 ` 1761` ``` where [simp]: "normalize = (abs :: int \ int)" ``` haftmann@64592 ` 1762` haftmann@64592 ` 1763` ```definition unit_factor_int :: "int \ int" ``` haftmann@64592 ` 1764` ``` where [simp]: "unit_factor = (sgn :: int \ int)" ``` haftmann@64592 ` 1765` haftmann@64592 ` 1766` ```definition divide_int :: "int \ int \ int" ``` haftmann@60868 ` 1767` ``` where "k div l = (if l = 0 \ k = 0 then 0 ``` haftmann@60868 ` 1768` ``` else if k > 0 \ l > 0 \ k < 0 \ l < 0 ``` haftmann@60868 ` 1769` ``` then int (nat \k\ div nat \l\) ``` haftmann@60868 ` 1770` ``` else ``` haftmann@60868 ` 1771` ``` if l dvd k then - int (nat \k\ div nat \l\) ``` haftmann@60868 ` 1772` ``` else - int (Suc (nat \k\ div nat \l\)))" ``` haftmann@60868 ` 1773` haftmann@64592 ` 1774` ```definition modulo_int :: "int \ int \ int" ``` haftmann@60868 ` 1775` ``` where "k mod l = (if l = 0 then k else if l dvd k then 0 ``` haftmann@60868 ` 1776` ``` else if k > 0 \ l > 0 \ k < 0 \ l < 0 ``` haftmann@60868 ` 1777` ``` then sgn l * int (nat \k\ mod nat \l\) ``` haftmann@60868 ` 1778` ``` else sgn l * (\l\ - int (nat \k\ mod nat \l\)))" ``` haftmann@60868 ` 1779` haftmann@64635 ` 1780` ```lemma eucl_rel_int: ``` haftmann@64635 ` 1781` ``` "eucl_rel_int k l (k div l, k mod l)" ``` haftmann@64592 ` 1782` ```proof (cases k rule: int_cases3) ``` haftmann@64592 ` 1783` ``` case zero ``` haftmann@64592 ` 1784` ``` then show ?thesis ``` haftmann@64635 ` 1785` ``` by (simp add: eucl_rel_int_iff divide_int_def modulo_int_def) ``` haftmann@64592 ` 1786` ```next ``` haftmann@64592 ` 1787` ``` case (pos n) ``` haftmann@64592 ` 1788` ``` then show ?thesis ``` haftmann@64592 ` 1789` ``` using div_mult_mod_eq [of n] ``` haftmann@64592 ` 1790` ``` by (cases l rule: int_cases3) ``` haftmann@64592 ` 1791` ``` (auto simp del: of_nat_mult of_nat_add ``` haftmann@64592 ` 1792` ``` simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps ``` haftmann@64635 ` 1793` ``` eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff) ``` haftmann@64592 ` 1794` ```next ``` haftmann@64592 ` 1795` ``` case (neg n) ``` haftmann@64592 ` 1796` ``` then show ?thesis ``` haftmann@64592 ` 1797` ``` using div_mult_mod_eq [of n] ``` haftmann@64592 ` 1798` ``` by (cases l rule: int_cases3) ``` haftmann@64592 ` 1799` ``` (auto simp del: of_nat_mult of_nat_add ``` haftmann@64592 ` 1800` ``` simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps ``` haftmann@64635 ` 1801` ``` eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff) ``` haftmann@64592 ` 1802` ```qed ``` haftmann@33361 ` 1803` huffman@47141 ` 1804` ```lemma divmod_int_unique: ``` haftmann@64635 ` 1805` ``` assumes "eucl_rel_int k l (q, r)" ``` haftmann@60868 ` 1806` ``` shows div_int_unique: "k div l = q" and mod_int_unique: "k mod l = r" ``` haftmann@64635 ` 1807` ``` using assms eucl_rel_int [of k l] ``` haftmann@60868 ` 1808` ``` using unique_quotient [of k l] unique_remainder [of k l] ``` haftmann@60868 ` 1809` ``` by auto ``` haftmann@64592 ` 1810` haftmann@64592 ` 1811` ```instance proof ``` haftmann@64592 ` 1812` ``` fix k l :: int ``` haftmann@64592 ` 1813` ``` show "k div l * l + k mod l = k" ``` haftmann@64635 ` 1814` ``` using eucl_rel_int [of k l] ``` haftmann@64635 ` 1815` ``` unfolding eucl_rel_int_iff by (simp add: ac_simps) ``` huffman@47141 ` 1816` ```next ``` haftmann@64592 ` 1817` ``` fix k :: int show "k div 0 = 0" ``` haftmann@64635 ` 1818` ``` by (rule div_int_unique, simp add: eucl_rel_int_iff) ``` huffman@47141 ` 1819` ```next ``` haftmann@64592 ` 1820` ``` fix k l :: int ``` haftmann@64592 ` 1821` ``` assume "l \ 0" ``` haftmann@64592 ` 1822` ``` then show "k * l div l = k" ``` haftmann@64635 ` 1823` ``` by (auto simp add: eucl_rel_int_iff ac_simps intro: div_int_unique [of _ _ _ 0]) ``` haftmann@64848 ` 1824` ```qed (auto simp add: sgn_mult mult_sgn_abs abs_eq_iff') ``` huffman@47141 ` 1825` haftmann@60429 ` 1826` ```end ``` haftmann@60429 ` 1827` haftmann@60517 ` 1828` ```lemma is_unit_int: ``` haftmann@60517 ` 1829` ``` "is_unit (k::int) \ k = 1 \ k = - 1" ``` haftmann@60517 ` 1830` ``` by auto ``` haftmann@60517 ` 1831` haftmann@64715 ` 1832` ```lemma zdiv_int: ``` haftmann@64715 ` 1833` ``` "int (a div b) = int a div int b" ``` haftmann@64715 ` 1834` ``` by (simp add: divide_int_def) ``` haftmann@64715 ` 1835` haftmann@64715 ` 1836` ```lemma zmod_int: ``` haftmann@64715 ` 1837` ``` "int (a mod b) = int a mod int b" ``` haftmann@64715 ` 1838` ``` by (simp add: modulo_int_def int_dvd_iff) ``` haftmann@64715 ` 1839` haftmann@64715 ` 1840` ```lemma div_abs_eq_div_nat: ``` haftmann@64715 ` 1841` ``` "\k\ div \l\ = int (nat \k\ div nat \l\)" ``` haftmann@64715 ` 1842` ``` by (simp add: divide_int_def) ``` haftmann@64715 ` 1843` haftmann@64715 ` 1844` ```lemma mod_abs_eq_div_nat: ``` haftmann@64715 ` 1845` ``` "\k\ mod \l\ = int (nat \k\ mod nat \l\)" ``` haftmann@64715 ` 1846` ``` by (simp add: modulo_int_def dvd_int_unfold_dvd_nat) ``` haftmann@64715 ` 1847` haftmann@64715 ` 1848` ```lemma div_sgn_abs_cancel: ``` haftmann@64715 ` 1849` ``` fixes k l v :: int ``` haftmann@64715 ` 1850` ``` assumes "v \ 0" ``` haftmann@64715 ` 1851` ``` shows "(sgn v * \k\) div (sgn v * \l\) = \k\ div \l\" ``` haftmann@64715 ` 1852` ```proof - ``` haftmann@64715 ` 1853` ``` from assms have "sgn v = - 1 \ sgn v = 1" ``` haftmann@64715 ` 1854` ``` by (cases "v \ 0") auto ``` haftmann@64715 ` 1855` ``` then show ?thesis ``` haftmann@64715 ` 1856` ``` using assms unfolding divide_int_def [of "sgn v * \k\" "sgn v * \l\"] ``` haftmann@64715 ` 1857` ``` by (auto simp add: not_less div_abs_eq_div_nat) ``` haftmann@64715 ` 1858` ```qed ``` haftmann@64715 ` 1859` haftmann@64715 ` 1860` ```lemma div_eq_sgn_abs: ``` haftmann@64715 ` 1861` ``` fixes k l v :: int ``` haftmann@64715 ` 1862` ``` assumes "sgn k = sgn l" ``` haftmann@64715 ` 1863` ``` shows "k div l = \k\ div \l\" ``` haftmann@64715 ` 1864` ```proof (cases "l = 0") ``` haftmann@64715 ` 1865` ``` case True ``` haftmann@64715 ` 1866` ``` then show ?thesis ``` haftmann@64715 ` 1867` ``` by simp ``` haftmann@64715 ` 1868` ```next ``` haftmann@64715 ` 1869` ``` case False ``` haftmann@64715 ` 1870` ``` with assms have "(sgn k * \k\) div (sgn l * \l\) = \k\ div \l\" ``` haftmann@64715 ` 1871` ``` by (simp add: div_sgn_abs_cancel) ``` haftmann@64715 ` 1872` ``` then show ?thesis ``` haftmann@64715 ` 1873` ``` by (simp add: sgn_mult_abs) ``` haftmann@64715 ` 1874` ```qed ``` haftmann@64715 ` 1875` haftmann@64715 ` 1876` ```lemma div_dvd_sgn_abs: ``` haftmann@64715 ` 1877` ``` fixes k l :: int ``` haftmann@64715 ` 1878` ``` assumes "l dvd k" ``` haftmann@64715 ` 1879` ``` shows "k div l = (sgn k * sgn l) * (\k\ div \l\)" ``` haftmann@64715 ` 1880` ```proof (cases "k = 0") ``` haftmann@64715 ` 1881` ``` case True ``` haftmann@64715 ` 1882` ``` then show ?thesis ``` haftmann@64715 ` 1883` ``` by simp ``` haftmann@64715 ` 1884` ```next ``` haftmann@64715 ` 1885` ``` case False ``` haftmann@64715 ` 1886` ``` show ?thesis ``` haftmann@64715 ` 1887` ``` proof (cases "sgn l = sgn k") ``` haftmann@64715 ` 1888` ``` case True ``` haftmann@64715 ` 1889` ``` then show ?thesis ``` haftmann@64715 ` 1890` ``` by (simp add: div_eq_sgn_abs) ``` haftmann@64715 ` 1891` ``` next ``` haftmann@64715 ` 1892` ``` case False ``` haftmann@64715 ` 1893` ``` with \k \ 0\ assms show ?thesis ``` haftmann@64715 ` 1894` ``` unfolding divide_int_def [of k l] ``` haftmann@64715 ` 1895` ``` by (auto simp add: zdiv_int) ``` haftmann@64715 ` 1896` ``` qed ``` haftmann@64715 ` 1897` ```qed ``` haftmann@64715 ` 1898` haftmann@64715 ` 1899` ```lemma div_noneq_sgn_abs: ``` haftmann@64715 ` 1900` ``` fixes k l :: int ``` haftmann@64715 ` 1901` ``` assumes "l \ 0" ``` haftmann@64715 ` 1902` ``` assumes "sgn k \ sgn l" ``` haftmann@64715 ` 1903` ``` shows "k div l = - (\k\ div \l\) - of_bool (\ l dvd k)" ``` haftmann@64715 ` 1904` ``` using assms ``` haftmann@64715 ` 1905` ``` by (simp only: divide_int_def [of k l], auto simp add: not_less zdiv_int) ``` haftmann@64715 ` 1906` ``` ``` haftmann@64715 ` 1907` ```lemma sgn_mod: ``` haftmann@64715 ` 1908` ``` fixes k l :: int ``` haftmann@64715 ` 1909` ``` assumes "l \ 0" "\ l dvd k" ``` haftmann@64715 ` 1910` ``` shows "sgn (k mod l) = sgn l" ``` haftmann@64715 ` 1911` ```proof - ``` haftmann@64715 ` 1912` ``` from \\ l dvd k\ ``` haftmann@64715 ` 1913` ``` have "k mod l \ 0" ``` haftmann@64715 ` 1914` ``` by (simp add: dvd_eq_mod_eq_0) ``` haftmann@64715 ` 1915` ``` show ?thesis ``` haftmann@64715 ` 1916` ``` using \l \ 0\ \\ l dvd k\ ``` haftmann@64715 ` 1917` ``` unfolding modulo_int_def [of k l] ``` haftmann@64715 ` 1918` ``` by (auto simp add: sgn_1_pos sgn_1_neg mod_greater_zero_iff_not_dvd nat_dvd_iff not_less ``` haftmann@64715 ` 1919` ``` zless_nat_eq_int_zless [symmetric] elim: nonpos_int_cases) ``` haftmann@64715 ` 1920` ```qed ``` haftmann@64715 ` 1921` haftmann@64715 ` 1922` ```lemma abs_mod_less: ``` haftmann@64715 ` 1923` ``` fixes k l :: int ``` haftmann@64715 ` 1924` ``` assumes "l \ 0" ``` haftmann@64715 ` 1925` ``` shows "\k mod l\ < \l\" ``` haftmann@64715 ` 1926` ``` using assms unfolding modulo_int_def [of k l] ``` haftmann@64715 ` 1927` ``` by (auto simp add: not_less int_dvd_iff mod_greater_zero_iff_not_dvd elim: pos_int_cases neg_int_cases nonneg_int_cases nonpos_int_cases) ``` haftmann@64715 ` 1928` haftmann@64592 ` 1929` ```instance int :: ring_div ``` haftmann@60685 ` 1930` ```proof ``` haftmann@64592 ` 1931` ``` fix k l s :: int ``` haftmann@64592 ` 1932` ``` assume "l \ 0" ``` haftmann@64635 ` 1933` ``` then have "eucl_rel_int (k + s * l) l (s + k div l, k mod l)" ``` haftmann@64635 ` 1934` ``` using eucl_rel_int [of k l] ``` haftmann@64635 ` 1935` ``` unfolding eucl_rel_int_iff by (auto simp: algebra_simps) ``` haftmann@64592 ` 1936` ``` then show "(k + s * l) div l = s + k div l" ``` haftmann@64592 ` 1937` ``` by (rule div_int_unique) ``` haftmann@64592 ` 1938` ```next ``` haftmann@64592 ` 1939` ``` fix k l s :: int ``` haftmann@64592 ` 1940` ``` assume "s \ 0" ``` haftmann@64635 ` 1941` ``` have "\q r. eucl_rel_int k l (q, r) ``` haftmann@64635 ` 1942` ``` \ eucl_rel_int (s * k) (s * l) (q, s * r)" ``` haftmann@64635 ` 1943` ``` unfolding eucl_rel_int_iff ``` haftmann@64592 ` 1944` ``` by (rule linorder_cases [of 0 l]) ``` haftmann@64592 ` 1945` ``` (use \s \ 0\ in \auto simp: algebra_simps ``` haftmann@64592 ` 1946` ``` mult_less_0_iff zero_less_mult_iff mult_strict_right_mono ``` haftmann@64592 ` 1947` ``` mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff\) ``` haftmann@64635 ` 1948` ``` then have "eucl_rel_int (s * k) (s * l) (k div l, s * (k mod l))" ``` haftmann@64635 ` 1949` ``` using eucl_rel_int [of k l] . ``` haftmann@64592 ` 1950` ``` then show "(s * k) div (s * l) = k div l" ``` haftmann@64592 ` 1951` ``` by (rule div_int_unique) ``` haftmann@64592 ` 1952` ```qed ``` wenzelm@60758 ` 1953` wenzelm@60758 ` 1954` ```ML \ ``` wenzelm@43594 ` 1955` ```structure Cancel_Div_Mod_Int = Cancel_Div_Mod ``` wenzelm@41550 ` 1956` ```( ``` haftmann@63950 ` 1957` ``` val div_name = @{const_name divide}; ``` haftmann@63950 ` 1958` ``` val mod_name = @{const_name modulo}; ``` haftmann@33361 ` 1959` ``` val mk_binop = HOLogic.mk_binop; ``` haftmann@33361 ` 1960` ``` val mk_sum = Arith_Data.mk_sum HOLogic.intT; ``` haftmann@33361 ` 1961` ``` val dest_sum = Arith_Data.dest_sum; ``` haftmann@33361 ` 1962` haftmann@64250 ` 1963` ``` val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules}; ``` haftmann@64250 ` 1964` haftmann@64592 ` 1965` ``` val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac ``` haftmann@64592 ` 1966` ``` @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps}) ``` wenzelm@41550 ` 1967` ```) ``` wenzelm@60758 ` 1968` ```\ ``` wenzelm@60758 ` 1969` haftmann@64592 ` 1970` ```simproc_setup cancel_div_mod_int ("(k::int) + l") = ``` haftmann@64592 ` 1971` ``` \K Cancel_Div_Mod_Int.proc\ ``` haftmann@64592 ` 1972` haftmann@64592 ` 1973` haftmann@64592 ` 1974` ```text\Basic laws about division and remainder\ ``` haftmann@64592 ` 1975` huffman@47141 ` 1976` ```lemma pos_mod_conj: "(0::int) < b \ 0 \ a mod b \ a mod b < b" ``` haftmann@64635 ` 1977` ``` using eucl_rel_int [of a b] ``` haftmann@64635 ` 1978` ``` by (auto simp add: eucl_rel_int_iff prod_eq_iff) ``` haftmann@33361 ` 1979` wenzelm@45607 ` 1980` ```lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1] ``` wenzelm@45607 ` 1981` ``` and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2] ``` haftmann@33361 ` 1982` huffman@47141 ` 1983` ```lemma neg_mod_conj: "b < (0::int) \ a mod b \ 0 \ b < a mod b" ``` haftmann@64635 ` 1984` ``` using eucl_rel_int [of a b] ``` haftmann@64635 ` 1985` ``` by (auto simp add: eucl_rel_int_iff prod_eq_iff) ``` haftmann@33361 ` 1986` wenzelm@45607 ` 1987` ```lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1] ``` wenzelm@45607 ` 1988` ``` and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2] ``` haftmann@33361 ` 1989` haftmann@33361 ` 1990` wenzelm@60758 ` 1991` ```subsubsection \General Properties of div and mod\ ``` haftmann@33361 ` 1992` haftmann@33361 ` 1993` ```lemma div_pos_pos_trivial: "[| (0::int) \ a; a < b |] ==> a div b = 0" ``` huffman@47140 ` 1994` ```apply (rule div_int_unique) ``` haftmann@64635 ` 1995` ```apply (auto simp add: eucl_rel_int_iff) ``` haftmann@33361 ` 1996` ```done ``` haftmann@33361 ` 1997` haftmann@33361 ` 1998` ```lemma div_neg_neg_trivial: "[| a \ (0::int); b < a |] ==> a div b = 0" ``` huffman@47140 ` 1999` ```apply (rule div_int_unique) ``` haftmann@64635 ` 2000` ```apply (auto simp add: eucl_rel_int_iff) ``` haftmann@33361 ` 2001` ```done ``` haftmann@33361 ` 2002` haftmann@33361 ` 2003` ```lemma div_pos_neg_trivial: "[| (0::int) < a; a+b \ 0 |] ==> a div b = -1" ``` huffman@47140 ` 2004` ```apply (rule div_int_unique) ``` haftmann@64635 ` 2005` ```apply (auto simp add: eucl_rel_int_iff) ``` haftmann@33361 ` 2006` ```done ``` haftmann@33361 ` 2007` haftmann@33361 ` 2008` ```(*There is no div_neg_pos_trivial because 0 div b = 0 would supersede it*) ``` haftmann@33361 ` 2009` haftmann@33361 ` 2010` ```lemma mod_pos_pos_trivial: "[| (0::int) \ a; a < b |] ==> a mod b = a" ``` huffman@47140 ` 2011` ```apply (rule_tac q = 0 in mod_int_unique) ``` haftmann@64635 ` 2012` ```apply (auto simp add: eucl_rel_int_iff) ``` haftmann@33361 ` 2013` ```done ``` haftmann@33361 ` 2014` haftmann@33361 ` 2015` ```lemma mod_neg_neg_trivial: "[| a \ (0::int); b < a |] ==> a mod b = a" ``` huffman@47140 ` 2016` ```apply (rule_tac q = 0 in mod_int_unique) ``` haftmann@64635 ` 2017` ```apply (auto simp add: eucl_rel_int_iff) ``` haftmann@33361 ` 2018` ```done ``` haftmann@33361 ` 2019` haftmann@33361 ` 2020` ```lemma mod_pos_neg_trivial: "[| (0::int) < a; a+b \ 0 |] ==> a mod b = a+b" ``` huffman@47140 ` 2021` ```apply (rule_tac q = "-1" in mod_int_unique) ``` haftmann@64635 ` 2022` ```apply (auto simp add: eucl_rel_int_iff) ``` haftmann@33361 ` 2023` ```done ``` haftmann@33361 ` 2024` wenzelm@61799 ` 2025` ```text\There is no \mod_neg_pos_trivial\.\ ``` wenzelm@60758 ` 2026` wenzelm@60758 ` 2027` wenzelm@60758 ` 2028` ```subsubsection \Laws for div and mod with Unary Minus\ ``` haftmann@33361 ` 2029` haftmann@33361 ` 2030` ```lemma zminus1_lemma: ``` haftmann@64635 ` 2031` ``` "eucl_rel_int a b (q, r) ==> b \ 0 ``` haftmann@64635 ` 2032` ``` ==> eucl_rel_int (-a) b (if r=0 then -q else -q - 1, ``` haftmann@33361 ` 2033` ``` if r=0 then 0 else b-r)" ``` haftmann@64635 ` 2034` ```by (force simp add: split_ifs eucl_rel_int_iff linorder_neq_iff right_diff_distrib) ``` haftmann@33361 ` 2035` haftmann@33361 ` 2036` haftmann@33361 ` 2037` ```lemma zdiv_zminus1_eq_if: ``` lp15@60562 ` 2038` ``` "b \ (0::int) ``` lp15@60562 ` 2039` ``` ==> (-a) div b = ``` haftmann@33361 ` 2040` ``` (if a mod b = 0 then - (a div b) else - (a div b) - 1)" ``` haftmann@64635 ` 2041` ```by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN div_int_unique]) ``` haftmann@33361 ` 2042` haftmann@33361 ` 2043` ```lemma zmod_zminus1_eq_if: ``` haftmann@33361 ` 2044` ``` "(-a::int) mod b = (if a mod b = 0 then 0 else b - (a mod b))" ``` haftmann@33361 ` 2045` ```apply (case_tac "b = 0", simp) ``` haftmann@64635 ` 2046` ```apply (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN mod_int_unique]) ``` haftmann@33361 ` 2047` ```done ``` haftmann@33361 ` 2048` haftmann@64593 ` 2049` ```lemma zmod_zminus1_not_zero: ``` haftmann@33361 ` 2050` ``` fixes k l :: int ``` haftmann@33361 ` 2051` ``` shows "- k mod l \ 0 \ k mod l \ 0" ``` haftmann@64592 ` 2052` ``` by (simp add: mod_eq_0_iff_dvd) ``` haftmann@64592 ` 2053` haftmann@64593 ` 2054` ```lemma zmod_zminus2_not_zero: ``` haftmann@64592 ` 2055` ``` fixes k l :: int ``` haftmann@64592 ` 2056` ``` shows "k mod - l \ 0 \ k mod l \ 0" ``` haftmann@64592 ` 2057` ``` by (simp add: mod_eq_0_iff_dvd) ``` haftmann@33361 ` 2058` haftmann@33361 ` 2059` ```lemma zdiv_zminus2_eq_if: ``` lp15@60562 ` 2060` ``` "b \ (0::int) ``` lp15@60562 ` 2061` ``` ==> a div (-b) = ``` haftmann@33361 ` 2062` ``` (if a mod b = 0 then - (a div b) else - (a div b) - 1)" ``` huffman@47159 ` 2063` ```by (simp add: zdiv_zminus1_eq_if div_minus_right) ``` haftmann@33361 ` 2064` haftmann@33361 ` 2065` ```lemma zmod_zminus2_eq_if: ``` haftmann@33361 ` 2066` ``` "a mod (-b::int) = (if a mod b = 0 then 0 else (a mod b) - b)" ``` huffman@47159 ` 2067` ```by (simp add: zmod_zminus1_eq_if mod_minus_right) ``` haftmann@33361 ` 2068` haftmann@33361 ` 2069` wenzelm@60758 ` 2070` ```subsubsection \Monotonicity in the First Argument (Dividend)\ ``` haftmann@33361 ` 2071` haftmann@33361 ` 2072` ```lemma zdiv_mono1: "[| a \ a'; 0 < (b::int) |] ==> a div b \ a' div b" ``` haftmann@64246 ` 2073` ```using mult_div_mod_eq [symmetric, of a b] ``` haftmann@64246 ` 2074` ```using mult_div_mod_eq [symmetric, of a' b] ``` haftmann@64246 ` 2075` ```apply - ``` haftmann@33361 ` 2076` ```apply (rule unique_quotient_lemma) ``` haftmann@33361 ` 2077` ```apply (erule subst) ``` haftmann@33361 ` 2078` ```apply (erule subst, simp_all) ``` haftmann@33361 ` 2079` ```done ``` haftmann@33361 ` 2080` haftmann@33361 ` 2081` ```lemma zdiv_mono1_neg: "[| a \ a'; (b::int) < 0 |] ==> a' div b \ a div b" ``` haftmann@64246 ` 2082` ```using mult_div_mod_eq [symmetric, of a b] ``` haftmann@64246 ` 2083` ```using mult_div_mod_eq [symmetric, of a' b] ``` haftmann@64246 ` 2084` ```apply - ``` haftmann@33361 ` 2085` ```apply (rule unique_quotient_lemma_neg) ``` haftmann@33361 ` 2086` ```apply (erule subst) ``` haftmann@33361 ` 2087` ```apply (erule subst, simp_all) ``` haftmann@33361 ` 2088` ```done ``` haftmann@33361 ` 2089` haftmann@33361 ` 2090` wenzelm@60758 ` 2091` ```subsubsection \Monotonicity in the Second Argument (Divisor)\ ``` haftmann@33361 ` 2092` haftmann@33361 ` 2093` ```lemma q_pos_lemma: ``` haftmann@33361 ` 2094` ``` "[| 0 \ b'*q' + r'; r' < b'; 0 < b' |] ==> 0 \ (q'::int)" ``` haftmann@33361 ` 2095` ```apply (subgoal_tac "0 < b'* (q' + 1) ") ``` haftmann@33361 ` 2096` ``` apply (simp add: zero_less_mult_iff) ``` webertj@49962 ` 2097` ```apply (simp add: distrib_left) ``` haftmann@33361 ` 2098` ```done ``` haftmann@33361 ` 2099` haftmann@33361 ` 2100` ```lemma zdiv_mono2_lemma: ``` lp15@60562 ` 2101` ``` "[| b*q + r = b'*q' + r'; 0 \ b'*q' + r'; ``` lp15@60562 ` 2102` ``` r' < b'; 0 \ r; 0 < b'; b' \ b |] ``` haftmann@33361 ` 2103` ``` ==> q \ (q'::int)" ``` lp15@60562 ` 2104` ```apply (frule q_pos_lemma, assumption+) ``` haftmann@33361 ` 2105` ```apply (subgoal_tac "b*q < b* (q' + 1) ") ``` haftmann@33361 ` 2106` ``` apply (simp add: mult_less_cancel_left) ``` haftmann@33361 ` 2107` ```apply (subgoal_tac "b*q = r' - r + b'*q'") ``` haftmann@33361 ` 2108` ``` prefer 2 apply simp ``` webertj@49962 ` 2109` ```apply (simp (no_asm_simp) add: distrib_left) ``` haftmann@57512 ` 2110` ```apply (subst add.commute, rule add_less_le_mono, arith) ``` haftmann@33361 ` 2111` ```apply (rule mult_right_mono, auto) ``` haftmann@33361 ` 2112` ```done ``` haftmann@33361 ` 2113` haftmann@33361 ` 2114` ```lemma zdiv_mono2: ``` haftmann@33361 ` 2115` ``` "[| (0::int) \ a; 0 < b'; b' \ b |] ==> a div b \ a div b'" ``` haftmann@33361 ` 2116` ```apply (subgoal_tac "b \ 0") ``` haftmann@64246 ` 2117` ``` prefer 2 apply arith ``` haftmann@64246 ` 2118` ```using mult_div_mod_eq [symmetric, of a b] ``` haftmann@64246 ` 2119` ```using mult_div_mod_eq [symmetric, of a b'] ``` haftmann@64246 ` 2120` ```apply - ``` haftmann@33361 ` 2121` ```apply (rule zdiv_mono2_lemma) ``` haftmann@33361 ` 2122` ```apply (erule subst) ``` haftmann@33361 ` 2123` ```apply (erule subst, simp_all) ``` haftmann@33361 ` 2124` ```done ``` haftmann@33361 ` 2125` haftmann@33361 ` 2126` ```lemma q_neg_lemma: ``` haftmann@33361 ` 2127` ``` "[| b'*q' + r' < 0; 0 \ r'; 0 < b' |] ==> q' \ (0::int)" ``` haftmann@33361 ` 2128` ```apply (subgoal_tac "b'*q' < 0") ``` haftmann@33361 ` 2129` ``` apply (simp add: mult_less_0_iff, arith) ``` haftmann@33361 ` 2130` ```done ``` haftmann@33361 ` 2131` haftmann@33361 ` 2132` ```lemma zdiv_mono2_neg_lemma: ``` lp15@60562 ` 2133` ``` "[| b*q + r = b'*q' + r'; b'*q' + r' < 0; ``` lp15@60562 ` 2134` ``` r < b; 0 \ r'; 0 < b'; b' \ b |] ``` haftmann@33361 ` 2135` ``` ==> q' \ (q::int)" ``` lp15@60562 ` 2136` ```apply (frule q_neg_lemma, assumption+) ``` haftmann@33361 ` 2137` ```apply (subgoal_tac "b*q' < b* (q + 1) ") ``` haftmann@33361 ` 2138` ``` apply (simp add: mult_less_cancel_left) ``` webertj@49962 ` 2139` ```apply (simp add: distrib_left) ``` haftmann@33361 ` 2140` ```apply (subgoal_tac "b*q' \ b'*q'") ``` haftmann@33361 ` 2141` ``` prefer 2 apply (simp add: mult_right_mono_neg, arith) ``` haftmann@33361 ` 2142` ```done ``` haftmann@33361 ` 2143` haftmann@33361 ` 2144` ```lemma zdiv_mono2_neg: ``` haftmann@33361 ` 2145` ``` "[| a < (0::int); 0 < b'; b' \ b |] ==> a div b' \ a div b" ``` haftmann@64246 ` 2146` ```using mult_div_mod_eq [symmetric, of a b] ``` haftmann@64246 ` 2147` ```using mult_div_mod_eq [symmetric, of a b'] ``` haftmann@64246 ` 2148` ```apply - ``` haftmann@33361 ` 2149` ```apply (rule zdiv_mono2_neg_lemma) ``` haftmann@33361 ` 2150` ```apply (erule subst) ``` haftmann@33361 ` 2151` ```apply (erule subst, simp_all) ``` haftmann@33361 ` 2152` ```done ``` haftmann@33361 ` 2153` haftmann@33361 ` 2154` wenzelm@60758 ` 2155` ```subsubsection \More Algebraic Laws for div and mod\ ``` wenzelm@60758 ` 2156` wenzelm@60758 ` 2157` ```text\proving (a*b) div c = a * (b div c) + a * (b mod c)\ ``` haftmann@33361 ` 2158` haftmann@33361 ` 2159` ```lemma zmult1_lemma: ``` haftmann@64635 ` 2160` ``` "[| eucl_rel_int b c (q, r) |] ``` haftmann@64635 ` 2161` ``` ==> eucl_rel_int (a * b) c (a*q + a*r div c, a*r mod c)" ``` haftmann@64635 ` 2162` ```by (auto simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left ac_simps) ``` haftmann@33361 ` 2163` haftmann@33361 ` 2164` ```lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)" ``` haftmann@33361 ` 2165` ```apply (case_tac "c = 0", simp) ``` haftmann@64635 ` 2166` ```apply (blast intro: eucl_rel_int [THEN zmult1_lemma, THEN div_int_unique]) ``` haftmann@33361 ` 2167` ```done ``` haftmann@33361 ` 2168` wenzelm@60758 ` 2169` ```text\proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c)\ ``` haftmann@33361 ` 2170` haftmann@33361 ` 2171` ```lemma zadd1_lemma: ``` haftmann@64635 ` 2172` ``` "[| eucl_rel_int a c (aq, ar); eucl_rel_int b c (bq, br) |] ``` haftmann@64635 ` 2173` ``` ==> eucl_rel_int (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)" ``` haftmann@64635 ` 2174` ```by (force simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left) ``` haftmann@33361 ` 2175` haftmann@33361 ` 2176` ```(*NOT suitable for rewriting: the RHS has an instance of the LHS*) ``` haftmann@33361 ` 2177` ```lemma zdiv_zadd1_eq: ``` haftmann@33361 ` 2178` ``` "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)" ``` haftmann@33361 ` 2179` ```apply (case_tac "c = 0", simp) ``` haftmann@64635 ` 2180` ```apply (blast intro: zadd1_lemma [OF eucl_rel_int eucl_rel_int] div_int_unique) ``` haftmann@33361 ` 2181` ```done ``` haftmann@33361 ` 2182` haftmann@33361 ` 2183` ```lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)" ``` haftmann@33361 ` 2184` ```by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def) ``` haftmann@33361 ` 2185` haftmann@33361 ` 2186` ```(* REVISIT: should this be generalized to all semiring_div types? *) ``` haftmann@33361 ` 2187` ```lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1] ``` haftmann@33361 ` 2188` haftmann@33361 ` 2189` wenzelm@60758 ` 2190` ```subsubsection \Proving @{term "a div (b * c) = (a div b) div c"}\ ``` haftmann@33361 ` 2191` haftmann@33361 ` 2192` ```(*The condition c>0 seems necessary. Consider that 7 div ~6 = ~2 but ``` haftmann@33361 ` 2193` ``` 7 div 2 div ~3 = 3 div ~3 = ~1. The subcase (a div b) mod c = 0 seems ``` haftmann@33361 ` 2194` ``` to cause particular problems.*) ``` haftmann@33361 ` 2195` wenzelm@60758 ` 2196` ```text\first, four lemmas to bound the remainder for the cases b<0 and b>0\ ``` haftmann@33361 ` 2197` blanchet@55085 ` 2198` ```lemma zmult2_lemma_aux1: "[| (0::int) < c; b < r; r \ 0 |] ==> b * c < b * (q mod c) + r" ``` haftmann@33361 ` 2199` ```apply (subgoal_tac "b * (c - q mod c) < r * 1") ``` haftmann@33361 ` 2200` ``` apply (simp add: algebra_simps) ``` haftmann@33361 ` 2201` ```apply (rule order_le_less_trans) ``` haftmann@33361 ` 2202` ``` apply (erule_tac [2] mult_strict_right_mono) ``` haftmann@33361 ` 2203` ``` apply (rule mult_left_mono_neg) ``` huffman@35216 ` 2204` ``` using add1_zle_eq[of "q mod c"]apply(simp add: algebra_simps) ``` haftmann@33361 ` 2205` ``` apply (simp) ``` haftmann@33361 ` 2206` ```apply (simp) ``` haftmann@33361 ` 2207` ```done ``` haftmann@33361 ` 2208` haftmann@33361 ` 2209` ```lemma zmult2_lemma_aux2: ``` haftmann@33361 ` 2210` ``` "[| (0::int) < c; b < r; r \ 0 |] ==> b * (q mod c) + r \ 0" ``` haftmann@33361 ` 2211` ```apply (subgoal_tac "b * (q mod c) \ 0") ``` haftmann@33361 ` 2212` ``` apply arith ``` haftmann@33361 ` 2213` ```apply (simp add: mult_le_0_iff) ``` haftmann@33361 ` 2214` ```done ``` haftmann@33361 ` 2215` haftmann@33361 ` 2216` ```lemma zmult2_lemma_aux3: "[| (0::int) < c; 0 \ r; r < b |] ==> 0 \ b * (q mod c) + r" ``` haftmann@33361 ` 2217` ```apply (subgoal_tac "0 \ b * (q mod c) ") ``` haftmann@33361 ` 2218` ```apply arith ``` haftmann@33361 ` 2219` ```apply (simp add: zero_le_mult_iff) ``` haftmann@33361 ` 2220` ```done ``` haftmann@33361 ` 2221` haftmann@33361 ` 2222` ```lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 \ r; r < b |] ==> b * (q mod c) + r < b * c" ``` haftmann@33361 ` 2223` ```apply (subgoal_tac "r * 1 < b * (c - q mod c) ") ``` haftmann@33361 ` 2224` ``` apply (simp add: right_diff_distrib) ``` haftmann@33361 ` 2225` ```apply (rule order_less_le_trans) ``` haftmann@33361 ` 2226` ``` apply (erule mult_strict_right_mono) ``` haftmann@33361 ` 2227` ``` apply (rule_tac [2] mult_left_mono) ``` haftmann@33361 ` 2228` ``` apply simp ``` huffman@35216 ` 2229` ``` using add1_zle_eq[of "q mod c"] apply (simp add: algebra_simps) ``` haftmann@33361 ` 2230` ```apply simp ``` haftmann@33361 ` 2231` ```done ``` haftmann@33361 ` 2232` haftmann@64635 ` 2233` ```lemma zmult2_lemma: "[| eucl_rel_int a b (q, r); 0 < c |] ``` haftmann@64635 ` 2234` ``` ==> eucl_rel_int a (b * c) (q div c, b*(q mod c) + r)" ``` haftmann@64635 ` 2235` ```by (auto simp add: mult.assoc eucl_rel_int_iff linorder_neq_iff ``` lp15@60562 ` 2236` ``` zero_less_mult_iff distrib_left [symmetric] ``` nipkow@62390 ` 2237` ``` zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: if_split_asm) ``` haftmann@33361 ` 2238` haftmann@53068 ` 2239` ```lemma zdiv_zmult2_eq: ``` haftmann@53068 ` 2240` ``` fixes a b c :: int ``` haftmann@53068 ` 2241` ``` shows "0 \ c \ a div (b * c) = (a div b) div c" ``` haftmann@33361 ` 2242` ```apply (case_tac "b = 0", simp) ``` haftmann@64635 ` 2243` ```apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN div_int_unique]) ``` haftmann@33361 ` 2244` ```done ``` haftmann@33361 ` 2245` haftmann@33361 ` 2246` ```lemma zmod_zmult2_eq: ``` haftmann@53068 ` 2247` ``` fixes a b c :: int ``` haftmann@53068 ` 2248` ``` shows "0 \ c \ a mod (b * c) = b * (a div b mod c) + a mod b" ``` haftmann@33361 ` 2249` ```apply (case_tac "b = 0", simp) ``` haftmann@64635 ` 2250` ```apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN mod_int_unique]) ``` haftmann@33361 ` 2251` ```done ``` haftmann@33361 ` 2252` huffman@47108 ` 2253` ```lemma div_pos_geq: ``` huffman@47108 ` 2254` ``` fixes k l :: int ``` huffman@47108 ` 2255` ``` assumes "0 < l" and "l \ k" ``` huffman@47108 ` 2256` ``` shows "k div l = (k - l) div l + 1" ``` huffman@47108 ` 2257` ```proof - ``` huffman@47108 ` 2258` ``` have "k = (k - l) + l" by simp ``` huffman@47108 ` 2259` ``` then obtain j where k: "k = j + l" .. ``` eberlm@63499 ` 2260` ``` with assms show ?thesis by (simp add: div_add_self2) ``` huffman@47108 ` 2261` ```qed ``` huffman@47108 ` 2262` huffman@47108 ` 2263` ```lemma mod_pos_geq: ``` huffman@47108 ` 2264` ``` fixes k l :: int ``` huffman@47108 ` 2265` ``` assumes "0 < l" and "l \ k" ``` huffman@47108 ` 2266` ``` shows "k mod l = (k - l) mod l" ``` huffman@47108 ` 2267` ```proof - ``` huffman@47108 ` 2268` ``` have "k = (k - l) + l" by simp ``` huffman@47108 ` 2269` ``` then obtain j where k: "k = j + l" .. ``` huffman@47108 ` 2270` ``` with assms show ?thesis by simp ``` huffman@47108 ` 2271` ```qed ``` huffman@47108 ` 2272` haftmann@33361 ` 2273` wenzelm@60758 ` 2274` ```subsubsection \Splitting Rules for div and mod\ ``` wenzelm@60758 ` 2275` wenzelm@60758 ` 2276` ```text\The proofs of the two lemmas below are essentially identical\ ``` haftmann@33361 ` 2277` haftmann@33361 ` 2278` ```lemma split_pos_lemma: ``` lp15@60562 ` 2279` ``` "0 ``` haftmann@33361 ` 2280` ``` P(n div k :: int)(n mod k) = (\i j. 0\j & j P i j)" ``` haftmann@33361 ` 2281` ```apply (rule iffI, clarify) ``` lp15@60562 ` 2282` ``` apply (erule_tac P="P x y" for x y in rev_mp) ``` haftmann@64593 ` 2283` ``` apply (subst mod_add_eq [symmetric]) ``` lp15@60562 ` 2284` ``` apply (subst zdiv_zadd1_eq) ``` lp15@60562 ` 2285` ``` apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial) ``` wenzelm@60758 ` 2286` ```txt\converse direction\ ``` lp15@60562 ` 2287` ```apply (drule_tac x = "n div k" in spec) ``` haftmann@33361 ` 2288` ```apply (drule_tac x = "n mod k" in spec, simp) ``` haftmann@33361 ` 2289` ```done ``` haftmann@33361 ` 2290` haftmann@33361 ` 2291` ```lemma split_neg_lemma: ``` haftmann@33361 ` 2292` ``` "k<0 ==> ``` haftmann@33361 ` 2293` ``` P(n div k :: int)(n mod k) = (\i j. k0 & n = k*i + j --> P i j)" ``` haftmann@33361 ` 2294` ```apply (rule iffI, clarify) ``` lp15@60562 ` 2295` ``` apply (erule_tac P="P x y" for x y in rev_mp) ``` haftmann@64593 ` 2296` ``` apply (subst mod_add_eq [symmetric]) ``` lp15@60562 ` 2297` ``` apply (subst zdiv_zadd1_eq) ``` lp15@60562 ` 2298` ``` apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial) ``` wenzelm@60758 ` 2299` ```txt\converse direction\ ``` lp15@60562 ` 2300` ```apply (drule_tac x = "n div k" in spec) ``` haftmann@33361 ` 2301` ```apply (drule_tac x = "n mod k" in spec, simp) ``` haftmann@33361 ` 2302` ```done ``` haftmann@33361 ` 2303` haftmann@33361 ` 2304` ```lemma split_zdiv: ``` haftmann@33361 ` 2305` ``` "P(n div k :: int) = ``` lp15@60562 ` 2306` ``` ((k = 0 --> P 0) & ``` lp15@60562 ` 2307` ``` (0 (\i j. 0\j & j P i)) & ``` haftmann@33361 ` 2308` ``` (k<0 --> (\i j. k0 & n = k*i + j --> P i)))" ``` haftmann@33361 ` 2309` ```apply (case_tac "k=0", simp) ``` haftmann@33361 ` 2310` ```apply (simp only: linorder_neq_iff) ``` lp15@60562 ` 2311` ```apply (erule disjE) ``` lp15@60562 ` 2312` ``` apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"] ``` haftmann@33361 ` 2313` ``` split_neg_lemma [of concl: "%x y. P x"]) ``` haftmann@33361 ` 2314` ```done ``` haftmann@33361 ` 2315` haftmann@33361 ` 2316` ```lemma split_zmod: ``` haftmann@33361 ` 2317` ``` "P(n mod k :: int) = ``` lp15@60562 ` 2318` ``` ((k = 0 --> P n) & ``` lp15@60562 ` 2319` ``` (0 (\i j. 0\j & j P j)) & ``` haftmann@33361 ` 2320` ``` (k<0 --> (\i j. k0 & n = k*i + j --> P j)))" ``` haftmann@33361 ` 2321` ```apply (case_tac "k=0", simp) ``` haftmann@33361 ` 2322` ```apply (simp only: linorder_neq_iff) ``` lp15@60562 ` 2323` ```apply (erule disjE) ``` lp15@60562 ` 2324` ``` apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"] ``` haftmann@33361 ` 2325` ``` split_neg_lemma [of concl: "%x y. P y"]) ``` haftmann@33361 ` 2326` ```done ``` haftmann@33361 ` 2327` haftmann@63950 ` 2328` ```text \Enable (lin)arith to deal with @{const divide} and @{const modulo} ``` webertj@33730 ` 2329` ``` when these are applied to some constant that is of the form ``` wenzelm@60758 ` 2330` ``` @{term "numeral k"}:\ ``` huffman@47108 ` 2331` ```declare split_zdiv [of _ _ "numeral k", arith_split] for k ``` huffman@47108 ` 2332` ```declare split_zmod [of _ _ "numeral k", arith_split] for k ``` haftmann@33361 ` 2333` haftmann@33361 ` 2334` wenzelm@61799 ` 2335` ```subsubsection \Computing \div\ and \mod\ with shifting\ ``` huffman@47166 ` 2336` haftmann@64635 ` 2337` ```lemma pos_eucl_rel_int_mult_2: ``` huffman@47166 ` 2338` ``` assumes "0 \ b" ``` haftmann@64635 ` 2339` ``` assumes "eucl_rel_int a b (q, r)" ``` haftmann@64635 ` 2340` ``` shows "eucl_rel_int (1 + 2*a) (2*b) (q, 1 + 2*r)" ``` haftmann@64635 ` 2341` ``` using assms unfolding eucl_rel_int_iff by auto ``` haftmann@64635 ` 2342` haftmann@64635 ` 2343` ```lemma neg_eucl_rel_int_mult_2: ``` huffman@47166 ` 2344` ``` assumes "b \ 0" ``` haftmann@64635 ` 2345` ``` assumes "eucl_rel_int (a + 1) b (q, r)" ``` haftmann@64635 ` 2346` ``` shows "eucl_rel_int (1 + 2*a) (2*b) (q, 2*r - 1)" ``` haftmann@64635 ` 2347` ``` using assms unfolding eucl_rel_int_iff by auto ``` haftmann@33361 ` 2348` wenzelm@60758 ` 2349` ```text\computing div by shifting\ ``` haftmann@33361 ` 2350` haftmann@33361 ` 2351` ```lemma pos_zdiv_mult_2: "(0::int) \ a ==> (1 + 2*b) div (2*a) = b div a" ``` haftmann@64635 ` 2352` ``` using pos_eucl_rel_int_mult_2 [OF _ eucl_rel_int] ``` huffman@47166 ` 2353` ``` by (rule div_int_unique) ``` haftmann@33361 ` 2354` lp15@60562 ` 2355` ```lemma neg_zdiv_mult_2: ``` boehmes@35815 ` 2356` ``` assumes A: "a \ (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a" ``` haftmann@64635 ` 2357` ``` using neg_eucl_rel_int_mult_2 [OF A eucl_rel_int] ``` huffman@47166 ` 2358` ``` by (rule div_int_unique) ``` haftmann@33361 ` 2359` huffman@47108 ` 2360` ```(* FIXME: add rules for negative numerals *) ``` huffman@47108 ` 2361` ```lemma zdiv_numeral_Bit0 [simp]: ``` huffman@47108 ` 2362` ``` "numeral (Num.Bit0 v) div numeral (Num.Bit0 w) = ``` huffman@47108 ` 2363` ``` numeral v div (numeral w :: int)" ``` huffman@47108 ` 2364` ``` unfolding numeral.simps unfolding mult_2 [symmetric] ``` huffman@47108 ` 2365` ``` by (rule div_mult_mult1, simp) ``` huffman@47108 ` 2366` huffman@47108 ` 2367` ```lemma zdiv_numeral_Bit1 [simp]: ``` lp15@60562 ` 2368` ``` "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) = ``` huffman@47108 ` 2369` ``` (numeral v div (numeral w :: int))" ``` huffman@47108 ` 2370` ``` unfolding numeral.simps ``` haftmann@57512 ` 2371` ``` unfolding mult_2 [symmetric] add.commute [of _ 1] ``` huffman@47108 ` 2372` ``` by (rule pos_zdiv_mult_2, simp) ``` haftmann@33361 ` 2373` haftmann@33361 ` 2374` ```lemma pos_zmod_mult_2: ``` haftmann@33361 ` 2375` ``` fixes a b :: int ``` haftmann@33361 ` 2376` ``` assumes "0 \ a" ``` haftmann@33361 ` 2377` ``` shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)" ``` haftmann@64635 ` 2378` ``` using pos_eucl_rel_int_mult_2 [OF assms eucl_rel_int] ``` huffman@47166 ` 2379` ``` by (rule mod_int_unique) ``` haftmann@33361 ` 2380` haftmann@33361 ` 2381` ```lemma neg_zmod_mult_2: ``` haftmann@33361 ` 2382` ``` fixes a b :: int ``` haftmann@33361 ` 2383` ``` assumes "a \ 0" ``` haftmann@33361 ` 2384` ``` shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1" ``` haftmann@64635 ` 2385` ``` using neg_eucl_rel_int_mult_2 [OF assms eucl_rel_int] ``` huffman@47166 ` 2386` ``` by (rule mod_int_unique) ``` haftmann@33361 ` 2387` huffman@47108 ` 2388` ```(* FIXME: add rules for negative numerals *) ``` huffman@47108 ` 2389` ```lemma zmod_numeral_Bit0 [simp]: ``` lp15@60562 ` 2390` ``` "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) = ``` huffman@47108 ` 2391` ``` (2::int) * (numeral v mod numeral w)" ``` huffman@47108 ` 2392` ``` unfolding numeral_Bit0 [of v] numeral_Bit0 [of w] ``` huffman@47108 ` 2393` ``` unfolding mult_2 [symmetric] by (rule mod_mult_mult1) ``` huffman@47108 ` 2394` huffman@47108 ` 2395` ```lemma zmod_numeral_Bit1 [simp]: ``` huffman@47108 ` 2396` ``` "numeral (Num.Bit1 v) mod numeral (Num.Bit0 w) = ``` huffman@47108 ` 2397` ``` 2 * (numeral v mod numeral w) + (1::int)" ``` huffman@47108 ` 2398` ``` unfolding numeral_Bit1 [of v] numeral_Bit0 [of w] ``` haftmann@57512 ` 2399` ``` unfolding mult_2 [symmetric] add.commute [of _ 1] ``` huffman@47108 ` 2400` ``` by (rule pos_zmod_mult_2, simp) ``` haftmann@33361 ` 2401` nipkow@39489 ` 2402` ```lemma zdiv_eq_0_iff: ``` nipkow@39489 ` 2403` ``` "(i::int) div k = 0 \ k=0 \ 0\i \ i i\0 \ k ?R" by (rule split_zdiv[THEN iffD2]) simp ``` wenzelm@60758 ` 2407` ``` with \?L\ show ?R by blast ``` nipkow@39489 ` 2408` ```next ``` nipkow@39489 ` 2409` ``` assume ?R thus ?L ``` nipkow@39489 ` 2410` ``` by(auto simp: div_pos_pos_trivial div_neg_neg_trivial) ``` nipkow@39489 ` 2411` ```qed ``` nipkow@39489 ` 2412` haftmann@63947 ` 2413` ```lemma zmod_trival_iff: ``` haftmann@63947 ` 2414` ``` fixes i k :: int ``` haftmann@63947 ` 2415` ``` shows "i mod k = i \ k = 0 \ 0 \ i \ i < k \ i \ 0 \ k < i" ``` haftmann@63947 ` 2416` ```proof - ``` haftmann@63947 ` 2417` ``` have "i mod k = i \ i div k = 0" ``` haftmann@64242 ` 2418` ``` by safe (insert div_mult_mod_eq [of i k], auto) ``` haftmann@63947 ` 2419` ``` with zdiv_eq_0_iff ``` haftmann@63947 ` 2420` ``` show ?thesis ``` haftmann@63947 ` 2421` ``` by simp ``` haftmann@63947 ` 2422` ```qed ``` nipkow@39489 ` 2423` haftmann@64785 ` 2424` ```instantiation int :: unique_euclidean_ring ``` haftmann@64785 ` 2425` ```begin ``` haftmann@64785 ` 2426` haftmann@64785 ` 2427` ```definition [simp]: ``` haftmann@64785 ` 2428` ``` "euclidean_size_int = (nat \ abs :: int \ nat)" ``` haftmann@64785 ` 2429` haftmann@64785 ` 2430` ```definition [simp]: ``` haftmann@64785 ` 2431` ``` "uniqueness_constraint_int (k :: int) l \ unit_factor k = unit_factor l" ``` haftmann@64785 ` 2432` ``` ``` haftmann@64785 ` 2433` ```instance ``` haftmann@64785 ` 2434` ``` by standard ``` haftmann@64785 ` 2435` ``` (use mult_le_mono2 [of 1] in \auto simp add: abs_mult nat_mult_distrib sgn_mod zdiv_eq_0_iff sgn_1_pos sgn_mult split: abs_split\) ``` haftmann@64785 ` 2436` haftmann@64785 ` 2437` ```end ``` haftmann@64785 ` 2438` haftmann@64785 ` 2439` ``` ``` wenzelm@60758 ` 2440` ```subsubsection \Quotients of Signs\ ``` haftmann@33361 ` 2441` haftmann@60868 ` 2442` ```lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1" ``` haftmann@60868 ` 2443` ```by (simp add: divide_int_def) ``` haftmann@60868 ` 2444` haftmann@60868 ` 2445` ```lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1" ``` haftmann@63950 ` 2446` ```by (simp add: modulo_int_def) ``` haftmann@60868 ` 2447` haftmann@33361 ` 2448` ```lemma div_neg_pos_less0: "[| a < (0::int); 0 < b |] ==> a div b < 0" ``` haftmann@33361 ` 2449` ```apply (subgoal_tac "a div b \ -1", force) ``` haftmann@33361 ` 2450` ```apply (rule order_trans) ``` haftmann@33361 ` 2451` ```apply (rule_tac a' = "-1" in zdiv_mono1) ``` haftmann@33361 ` 2452` ```apply (auto simp add: div_eq_minus1) ``` haftmann@33361 ` 2453` ```done ``` haftmann@33361 ` 2454` haftmann@33361 ` 2455` ```lemma div_nonneg_neg_le0: "[| (0::int) \ a; b < 0 |] ==> a div b \ 0" ``` haftmann@33361 ` 2456` ```by (drule zdiv_mono1_neg, auto) ``` haftmann@33361 ` 2457` haftmann@33361 ` 2458` ```lemma div_nonpos_pos_le0: "[| (a::int) \ 0; b > 0 |] ==> a div b \ 0" ``` haftmann@33361 ` 2459` ```by (drule zdiv_mono1, auto) ``` haftmann@33361 ` 2460` wenzelm@61799 ` 2461` ```text\Now for some equivalences of the form \a div b >=< 0 \ \\ ``` wenzelm@61799 ` 2462` ```conditional upon the sign of \a\ or \b\. There are many more. ``` wenzelm@60758 ` 2463` ```They should all be simp rules unless that causes too much search.\ ``` nipkow@33804 ` 2464` haftmann@33361 ` 2465` ```lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \ a div b) = (0 \ a)" ``` haftmann@33361 ` 2466` ```apply auto ``` haftmann@33361 ` 2467` ```apply (drule_tac [2] zdiv_mono1) ``` haftmann@33361 ` 2468` ```apply (auto simp add: linorder_neq_iff) ``` haftmann@33361 ` 2469` ```apply (simp (no_asm_use) add: linorder_not_less [symmetric]) ``` haftmann@33361 ` 2470` ```apply (blast intro: div_neg_pos_less0) ``` haftmann@33361 ` 2471` ```done ``` haftmann@33361 ` 2472` haftmann@60868 ` 2473` ```lemma pos_imp_zdiv_pos_iff: ``` haftmann@60868 ` 2474` ``` "0 0 < (i::int) div k \ k \ i" ``` haftmann@60868 ` 2475` ```using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k] ``` haftmann@60868 ` 2476` ```by arith ``` haftmann@60868 ` 2477` haftmann@33361 ` 2478` ```lemma neg_imp_zdiv_nonneg_iff: ``` nipkow@33804 ` 2479` ``` "b < (0::int) ==> (0 \ a div b) = (a \ (0::int))" ``` huffman@47159 ` 2480` ```apply (subst div_minus_minus [symmetric]) ``` haftmann@33361 ` 2481` ```apply (subst pos_imp_zdiv_nonneg_iff, auto) ``` haftmann@33361 ` 2482` ```done ``` haftmann@33361 ` 2483` haftmann@33361 ` 2484` ```(*But not (a div b \ 0 iff a\0); consider a=1, b=2 when a div b = 0.*) ``` haftmann@33361 ` 2485` ```lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)" ``` haftmann@33361 ` 2486` ```by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff) ``` haftmann@33361 ` 2487` haftmann@33361 ` 2488` ```(*Again the law fails for \: consider a = -1, b = -2 when a div b = 0*) ``` haftmann@33361 ` 2489` ```lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)" ``` haftmann@33361 ` 2490` ```by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff) ``` haftmann@33361 ` 2491` nipkow@33804 ` 2492` ```lemma nonneg1_imp_zdiv_pos_iff: ``` nipkow@33804 ` 2493` ``` "(0::int) <= a \ (a div b > 0) = (a >= b & b>0)" ``` nipkow@33804 ` 2494` ```apply rule ``` nipkow@33804 ` 2495` ``` apply rule ``` nipkow@33804 ` 2496` ``` using div_pos_pos_trivial[of a b]apply arith ``` nipkow@33804 ` 2497` ``` apply(cases "b=0")apply simp ``` nipkow@33804 ` 2498` ``` using div_nonneg_neg_le0[of a b]apply arith ``` nipkow@33804 ` 2499` ```using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b]apply simp ``` nipkow@33804 ` 2500` ```done ``` nipkow@33804 ` 2501` nipkow@39489 ` 2502` ```lemma zmod_le_nonneg_dividend: "(m::int) \ 0 ==> m mod k \ m" ``` nipkow@39489 ` 2503` ```apply (rule split_zmod[THEN iffD2]) ``` nipkow@44890 ` 2504` ```apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le) ``` nipkow@39489 ` 2505` ```done ``` nipkow@39489 ` 2506` haftmann@60868 ` 2507` haftmann@60868 ` 2508` ```subsubsection \Computation of Division and Remainder\ ``` haftmann@60868 ` 2509` haftmann@61275 ` 2510` ```instantiation int :: semiring_numeral_div ``` haftmann@61275 ` 2511` ```begin ``` haftmann@61275 ` 2512` haftmann@61275 ` 2513` ```definition divmod_int :: "num \ num \ int \ int" ``` haftmann@61275 ` 2514` ```where ``` haftmann@61275 ` 2515` ``` "divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)" ``` haftmann@61275 ` 2516` haftmann@61275 ` 2517` ```definition divmod_step_int :: "num \ int \ int \ int \ int" ``` haftmann@61275 ` 2518` ```where ``` haftmann@61275 ` 2519` ``` "divmod_step_int l qr = (let (q, r) = qr ``` haftmann@61275 ` 2520` ``` in if r \ numeral l then (2 * q + 1, r - numeral l) ``` haftmann@61275 ` 2521` ``` else (2 * q, r))" ``` haftmann@61275 ` 2522` haftmann@61275 ` 2523` ```instance ``` haftmann@61275 ` 2524` ``` by standard (auto intro: zmod_le_nonneg_dividend simp add: divmod_int_def divmod_step_int_def ``` haftmann@61275 ` 2525` ``` pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial zmod_zmult2_eq zdiv_zmult2_eq) ``` haftmann@61275 ` 2526` haftmann@61275 ` 2527` ```end ``` haftmann@61275 ` 2528` haftmann@61275 ` 2529` ```declare divmod_algorithm_code [where ?'a = int, code] ``` lp15@60562 ` 2530` haftmann@60930 ` 2531` ```context ``` haftmann@60930 ` 2532` ```begin ``` haftmann@60930 ` 2533` ``` ``` haftmann@60930 ` 2534` ```qualified definition adjust_div :: "int \ int \ int" ``` haftmann@60868 ` 2535` ```where ``` haftmann@60868 ` 2536` ``` "adjust_div qr = (let (q, r) = qr in q + of_bool (r \ 0))" ``` haftmann@60868 ` 2537` haftmann@60930 ` 2538` ```qualified lemma adjust_div_eq [simp, code]: ``` haftmann@60868 ` 2539` ``` "adjust_div (q, r) = q + of_bool (r \ 0)" ``` haftmann@60868 ` 2540` ``` by (simp add: adjust_div_def) ``` haftmann@60868 ` 2541` haftmann@60930 ` 2542` ```qualified definition adjust_mod :: "int \ int \ int" ``` haftmann@60868 ` 2543` ```where ``` haftmann@60868 ` 2544` ``` [simp]: "adjust_mod l r = (if r = 0 then 0 else l - r)" ``` haftmann@60868 ` 2545` haftmann@60868 ` 2546` ```lemma minus_numeral_div_numeral [simp]: ``` haftmann@60868 ` 2547` ``` "- numeral m div numeral n = - (adjust_div (divmod m n) :: int)" ``` haftmann@60868 ` 2548` ```proof - ``` haftmann@60868 ` 2549` ``` have "int (fst (divmod m n)) = fst (divmod m n)" ``` haftmann@60868 ` 2550` ``` by (simp only: fst_divmod divide_int_def) auto ``` haftmann@60868 ` 2551` ``` then show ?thesis ``` haftmann@60868 ` 2552` ``` by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def) ``` haftmann@60868 ` 2553` ```qed ```