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