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