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