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