src/HOL/Euclidean_Division.thy
 author haftmann Sun Oct 08 22:28:21 2017 +0200 (20 months ago) changeset 66808 1907167b6038 parent 66807 c3631f32dfeb child 66810 cc2b490f9dc4 permissions -rw-r--r--
elementary definition of division on natural numbers
 haftmann@64785 ` 1` ```(* Title: HOL/Euclidean_Division.thy ``` haftmann@64785 ` 2` ``` Author: Manuel Eberl, TU Muenchen ``` haftmann@64785 ` 3` ``` Author: Florian Haftmann, TU Muenchen ``` haftmann@64785 ` 4` ```*) ``` haftmann@64785 ` 5` haftmann@64785 ` 6` ```section \Uniquely determined division in euclidean (semi)rings\ ``` haftmann@64785 ` 7` haftmann@64785 ` 8` ```theory Euclidean_Division ``` haftmann@66808 ` 9` ``` imports Nat_Transfer Lattices_Big ``` haftmann@64785 ` 10` ```begin ``` haftmann@64785 ` 11` haftmann@66808 ` 12` ```subsection \Prelude: simproc for cancelling @{const divide} and @{const modulo}\ ``` haftmann@66808 ` 13` haftmann@66808 ` 14` ```lemma (in semiring_modulo) cancel_div_mod_rules: ``` haftmann@66808 ` 15` ``` "((a div b) * b + a mod b) + c = a + c" ``` haftmann@66808 ` 16` ``` "(b * (a div b) + a mod b) + c = a + c" ``` haftmann@66808 ` 17` ``` by (simp_all add: div_mult_mod_eq mult_div_mod_eq) ``` haftmann@66808 ` 18` haftmann@66808 ` 19` ```ML_file "~~/src/Provers/Arith/cancel_div_mod.ML" ``` haftmann@66808 ` 20` haftmann@66808 ` 21` haftmann@64785 ` 22` ```subsection \Euclidean (semi)rings with explicit division and remainder\ ``` haftmann@64785 ` 23` ``` ``` haftmann@64785 ` 24` ```class euclidean_semiring = semidom_modulo + normalization_semidom + ``` haftmann@64785 ` 25` ``` fixes euclidean_size :: "'a \ nat" ``` haftmann@64785 ` 26` ``` assumes size_0 [simp]: "euclidean_size 0 = 0" ``` haftmann@64785 ` 27` ``` assumes mod_size_less: ``` haftmann@64785 ` 28` ``` "b \ 0 \ euclidean_size (a mod b) < euclidean_size b" ``` haftmann@64785 ` 29` ``` assumes size_mult_mono: ``` haftmann@64785 ` 30` ``` "b \ 0 \ euclidean_size a \ euclidean_size (a * b)" ``` haftmann@64785 ` 31` ```begin ``` haftmann@64785 ` 32` haftmann@64785 ` 33` ```lemma size_mult_mono': "b \ 0 \ euclidean_size a \ euclidean_size (b * a)" ``` haftmann@64785 ` 34` ``` by (subst mult.commute) (rule size_mult_mono) ``` haftmann@64785 ` 35` haftmann@64785 ` 36` ```lemma euclidean_size_normalize [simp]: ``` haftmann@64785 ` 37` ``` "euclidean_size (normalize a) = euclidean_size a" ``` haftmann@64785 ` 38` ```proof (cases "a = 0") ``` haftmann@64785 ` 39` ``` case True ``` haftmann@64785 ` 40` ``` then show ?thesis ``` haftmann@64785 ` 41` ``` by simp ``` haftmann@64785 ` 42` ```next ``` haftmann@64785 ` 43` ``` case [simp]: False ``` haftmann@64785 ` 44` ``` have "euclidean_size (normalize a) \ euclidean_size (normalize a * unit_factor a)" ``` haftmann@64785 ` 45` ``` by (rule size_mult_mono) simp ``` haftmann@64785 ` 46` ``` moreover have "euclidean_size a \ euclidean_size (a * (1 div unit_factor a))" ``` haftmann@64785 ` 47` ``` by (rule size_mult_mono) simp ``` haftmann@64785 ` 48` ``` ultimately show ?thesis ``` haftmann@64785 ` 49` ``` by simp ``` haftmann@64785 ` 50` ```qed ``` haftmann@64785 ` 51` haftmann@64785 ` 52` ```lemma dvd_euclidean_size_eq_imp_dvd: ``` haftmann@64785 ` 53` ``` assumes "a \ 0" and "euclidean_size a = euclidean_size b" ``` haftmann@64785 ` 54` ``` and "b dvd a" ``` haftmann@64785 ` 55` ``` shows "a dvd b" ``` haftmann@64785 ` 56` ```proof (rule ccontr) ``` haftmann@64785 ` 57` ``` assume "\ a dvd b" ``` haftmann@64785 ` 58` ``` hence "b mod a \ 0" using mod_0_imp_dvd [of b a] by blast ``` haftmann@64785 ` 59` ``` then have "b mod a \ 0" by (simp add: mod_eq_0_iff_dvd) ``` haftmann@64785 ` 60` ``` from \b dvd a\ have "b dvd b mod a" by (simp add: dvd_mod_iff) ``` haftmann@64785 ` 61` ``` then obtain c where "b mod a = b * c" unfolding dvd_def by blast ``` haftmann@64785 ` 62` ``` with \b mod a \ 0\ have "c \ 0" by auto ``` haftmann@64785 ` 63` ``` with \b mod a = b * c\ have "euclidean_size (b mod a) \ euclidean_size b" ``` haftmann@64785 ` 64` ``` using size_mult_mono by force ``` haftmann@64785 ` 65` ``` moreover from \\ a dvd b\ and \a \ 0\ ``` haftmann@64785 ` 66` ``` have "euclidean_size (b mod a) < euclidean_size a" ``` haftmann@64785 ` 67` ``` using mod_size_less by blast ``` haftmann@64785 ` 68` ``` ultimately show False using \euclidean_size a = euclidean_size b\ ``` haftmann@64785 ` 69` ``` by simp ``` haftmann@64785 ` 70` ```qed ``` haftmann@64785 ` 71` haftmann@64785 ` 72` ```lemma euclidean_size_times_unit: ``` haftmann@64785 ` 73` ``` assumes "is_unit a" ``` haftmann@64785 ` 74` ``` shows "euclidean_size (a * b) = euclidean_size b" ``` haftmann@64785 ` 75` ```proof (rule antisym) ``` haftmann@64785 ` 76` ``` from assms have [simp]: "a \ 0" by auto ``` haftmann@64785 ` 77` ``` thus "euclidean_size (a * b) \ euclidean_size b" by (rule size_mult_mono') ``` haftmann@64785 ` 78` ``` from assms have "is_unit (1 div a)" by simp ``` haftmann@64785 ` 79` ``` hence "1 div a \ 0" by (intro notI) simp_all ``` haftmann@64785 ` 80` ``` hence "euclidean_size (a * b) \ euclidean_size ((1 div a) * (a * b))" ``` haftmann@64785 ` 81` ``` by (rule size_mult_mono') ``` haftmann@64785 ` 82` ``` also from assms have "(1 div a) * (a * b) = b" ``` haftmann@64785 ` 83` ``` by (simp add: algebra_simps unit_div_mult_swap) ``` haftmann@64785 ` 84` ``` finally show "euclidean_size (a * b) \ euclidean_size b" . ``` haftmann@64785 ` 85` ```qed ``` haftmann@64785 ` 86` haftmann@64785 ` 87` ```lemma euclidean_size_unit: ``` haftmann@64785 ` 88` ``` "is_unit a \ euclidean_size a = euclidean_size 1" ``` haftmann@64785 ` 89` ``` using euclidean_size_times_unit [of a 1] by simp ``` haftmann@64785 ` 90` haftmann@64785 ` 91` ```lemma unit_iff_euclidean_size: ``` haftmann@64785 ` 92` ``` "is_unit a \ euclidean_size a = euclidean_size 1 \ a \ 0" ``` haftmann@64785 ` 93` ```proof safe ``` haftmann@64785 ` 94` ``` assume A: "a \ 0" and B: "euclidean_size a = euclidean_size 1" ``` haftmann@64785 ` 95` ``` show "is_unit a" ``` haftmann@64785 ` 96` ``` by (rule dvd_euclidean_size_eq_imp_dvd [OF A B]) simp_all ``` haftmann@64785 ` 97` ```qed (auto intro: euclidean_size_unit) ``` haftmann@64785 ` 98` haftmann@64785 ` 99` ```lemma euclidean_size_times_nonunit: ``` haftmann@64785 ` 100` ``` assumes "a \ 0" "b \ 0" "\ is_unit a" ``` haftmann@64785 ` 101` ``` shows "euclidean_size b < euclidean_size (a * b)" ``` haftmann@64785 ` 102` ```proof (rule ccontr) ``` haftmann@64785 ` 103` ``` assume "\euclidean_size b < euclidean_size (a * b)" ``` haftmann@64785 ` 104` ``` with size_mult_mono'[OF assms(1), of b] ``` haftmann@64785 ` 105` ``` have eq: "euclidean_size (a * b) = euclidean_size b" by simp ``` haftmann@64785 ` 106` ``` have "a * b dvd b" ``` haftmann@64785 ` 107` ``` by (rule dvd_euclidean_size_eq_imp_dvd [OF _ eq]) (insert assms, simp_all) ``` haftmann@64785 ` 108` ``` hence "a * b dvd 1 * b" by simp ``` haftmann@64785 ` 109` ``` with \b \ 0\ have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff) ``` haftmann@64785 ` 110` ``` with assms(3) show False by contradiction ``` haftmann@64785 ` 111` ```qed ``` haftmann@64785 ` 112` haftmann@64785 ` 113` ```lemma dvd_imp_size_le: ``` haftmann@64785 ` 114` ``` assumes "a dvd b" "b \ 0" ``` haftmann@64785 ` 115` ``` shows "euclidean_size a \ euclidean_size b" ``` haftmann@64785 ` 116` ``` using assms by (auto elim!: dvdE simp: size_mult_mono) ``` haftmann@64785 ` 117` haftmann@64785 ` 118` ```lemma dvd_proper_imp_size_less: ``` haftmann@64785 ` 119` ``` assumes "a dvd b" "\ b dvd a" "b \ 0" ``` haftmann@64785 ` 120` ``` shows "euclidean_size a < euclidean_size b" ``` haftmann@64785 ` 121` ```proof - ``` haftmann@64785 ` 122` ``` from assms(1) obtain c where "b = a * c" by (erule dvdE) ``` haftmann@64785 ` 123` ``` hence z: "b = c * a" by (simp add: mult.commute) ``` haftmann@64785 ` 124` ``` from z assms have "\is_unit c" by (auto simp: mult.commute mult_unit_dvd_iff) ``` haftmann@64785 ` 125` ``` with z assms show ?thesis ``` haftmann@64785 ` 126` ``` by (auto intro!: euclidean_size_times_nonunit) ``` haftmann@64785 ` 127` ```qed ``` haftmann@64785 ` 128` haftmann@66798 ` 129` ```lemma unit_imp_mod_eq_0: ``` haftmann@66798 ` 130` ``` "a mod b = 0" if "is_unit b" ``` haftmann@66798 ` 131` ``` using that by (simp add: mod_eq_0_iff_dvd unit_imp_dvd) ``` haftmann@66798 ` 132` haftmann@64785 ` 133` ```end ``` haftmann@64785 ` 134` haftmann@64785 ` 135` ```class euclidean_ring = idom_modulo + euclidean_semiring ``` haftmann@64785 ` 136` haftmann@64785 ` 137` ``` ``` haftmann@66806 ` 138` ```subsection \Euclidean (semi)rings with cancel rules\ ``` haftmann@66806 ` 139` haftmann@66806 ` 140` ```class euclidean_semiring_cancel = euclidean_semiring + ``` haftmann@66806 ` 141` ``` assumes div_mult_self1 [simp]: "b \ 0 \ (a + c * b) div b = c + a div b" ``` haftmann@66806 ` 142` ``` and div_mult_mult1 [simp]: "c \ 0 \ (c * a) div (c * b) = a div b" ``` haftmann@66806 ` 143` ```begin ``` haftmann@66806 ` 144` haftmann@66806 ` 145` ```lemma div_mult_self2 [simp]: ``` haftmann@66806 ` 146` ``` assumes "b \ 0" ``` haftmann@66806 ` 147` ``` shows "(a + b * c) div b = c + a div b" ``` haftmann@66806 ` 148` ``` using assms div_mult_self1 [of b a c] by (simp add: mult.commute) ``` haftmann@66806 ` 149` haftmann@66806 ` 150` ```lemma div_mult_self3 [simp]: ``` haftmann@66806 ` 151` ``` assumes "b \ 0" ``` haftmann@66806 ` 152` ``` shows "(c * b + a) div b = c + a div b" ``` haftmann@66806 ` 153` ``` using assms by (simp add: add.commute) ``` haftmann@66806 ` 154` haftmann@66806 ` 155` ```lemma div_mult_self4 [simp]: ``` haftmann@66806 ` 156` ``` assumes "b \ 0" ``` haftmann@66806 ` 157` ``` shows "(b * c + a) div b = c + a div b" ``` haftmann@66806 ` 158` ``` using assms by (simp add: add.commute) ``` haftmann@66806 ` 159` haftmann@66806 ` 160` ```lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b" ``` haftmann@66806 ` 161` ```proof (cases "b = 0") ``` haftmann@66806 ` 162` ``` case True then show ?thesis by simp ``` haftmann@66806 ` 163` ```next ``` haftmann@66806 ` 164` ``` case False ``` haftmann@66806 ` 165` ``` have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b" ``` haftmann@66806 ` 166` ``` by (simp add: div_mult_mod_eq) ``` haftmann@66806 ` 167` ``` also from False div_mult_self1 [of b a c] have ``` haftmann@66806 ` 168` ``` "\ = (c + a div b) * b + (a + c * b) mod b" ``` haftmann@66806 ` 169` ``` by (simp add: algebra_simps) ``` haftmann@66806 ` 170` ``` finally have "a = a div b * b + (a + c * b) mod b" ``` haftmann@66806 ` 171` ``` by (simp add: add.commute [of a] add.assoc distrib_right) ``` haftmann@66806 ` 172` ``` then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b" ``` haftmann@66806 ` 173` ``` by (simp add: div_mult_mod_eq) ``` haftmann@66806 ` 174` ``` then show ?thesis by simp ``` haftmann@66806 ` 175` ```qed ``` haftmann@66806 ` 176` haftmann@66806 ` 177` ```lemma mod_mult_self2 [simp]: ``` haftmann@66806 ` 178` ``` "(a + b * c) mod b = a mod b" ``` haftmann@66806 ` 179` ``` by (simp add: mult.commute [of b]) ``` haftmann@66806 ` 180` haftmann@66806 ` 181` ```lemma mod_mult_self3 [simp]: ``` haftmann@66806 ` 182` ``` "(c * b + a) mod b = a mod b" ``` haftmann@66806 ` 183` ``` by (simp add: add.commute) ``` haftmann@66806 ` 184` haftmann@66806 ` 185` ```lemma mod_mult_self4 [simp]: ``` haftmann@66806 ` 186` ``` "(b * c + a) mod b = a mod b" ``` haftmann@66806 ` 187` ``` by (simp add: add.commute) ``` haftmann@66806 ` 188` haftmann@66806 ` 189` ```lemma mod_mult_self1_is_0 [simp]: ``` haftmann@66806 ` 190` ``` "b * a mod b = 0" ``` haftmann@66806 ` 191` ``` using mod_mult_self2 [of 0 b a] by simp ``` haftmann@66806 ` 192` haftmann@66806 ` 193` ```lemma mod_mult_self2_is_0 [simp]: ``` haftmann@66806 ` 194` ``` "a * b mod b = 0" ``` haftmann@66806 ` 195` ``` using mod_mult_self1 [of 0 a b] by simp ``` haftmann@66806 ` 196` haftmann@66806 ` 197` ```lemma div_add_self1: ``` haftmann@66806 ` 198` ``` assumes "b \ 0" ``` haftmann@66806 ` 199` ``` shows "(b + a) div b = a div b + 1" ``` haftmann@66806 ` 200` ``` using assms div_mult_self1 [of b a 1] by (simp add: add.commute) ``` haftmann@66806 ` 201` haftmann@66806 ` 202` ```lemma div_add_self2: ``` haftmann@66806 ` 203` ``` assumes "b \ 0" ``` haftmann@66806 ` 204` ``` shows "(a + b) div b = a div b + 1" ``` haftmann@66806 ` 205` ``` using assms div_add_self1 [of b a] by (simp add: add.commute) ``` haftmann@66806 ` 206` haftmann@66806 ` 207` ```lemma mod_add_self1 [simp]: ``` haftmann@66806 ` 208` ``` "(b + a) mod b = a mod b" ``` haftmann@66806 ` 209` ``` using mod_mult_self1 [of a 1 b] by (simp add: add.commute) ``` haftmann@66806 ` 210` haftmann@66806 ` 211` ```lemma mod_add_self2 [simp]: ``` haftmann@66806 ` 212` ``` "(a + b) mod b = a mod b" ``` haftmann@66806 ` 213` ``` using mod_mult_self1 [of a 1 b] by simp ``` haftmann@66806 ` 214` haftmann@66806 ` 215` ```lemma mod_div_trivial [simp]: ``` haftmann@66806 ` 216` ``` "a mod b div b = 0" ``` haftmann@66806 ` 217` ```proof (cases "b = 0") ``` haftmann@66806 ` 218` ``` assume "b = 0" ``` haftmann@66806 ` 219` ``` thus ?thesis by simp ``` haftmann@66806 ` 220` ```next ``` haftmann@66806 ` 221` ``` assume "b \ 0" ``` haftmann@66806 ` 222` ``` hence "a div b + a mod b div b = (a mod b + a div b * b) div b" ``` haftmann@66806 ` 223` ``` by (rule div_mult_self1 [symmetric]) ``` haftmann@66806 ` 224` ``` also have "\ = a div b" ``` haftmann@66806 ` 225` ``` by (simp only: mod_div_mult_eq) ``` haftmann@66806 ` 226` ``` also have "\ = a div b + 0" ``` haftmann@66806 ` 227` ``` by simp ``` haftmann@66806 ` 228` ``` finally show ?thesis ``` haftmann@66806 ` 229` ``` by (rule add_left_imp_eq) ``` haftmann@66806 ` 230` ```qed ``` haftmann@66806 ` 231` haftmann@66806 ` 232` ```lemma mod_mod_trivial [simp]: ``` haftmann@66806 ` 233` ``` "a mod b mod b = a mod b" ``` haftmann@66806 ` 234` ```proof - ``` haftmann@66806 ` 235` ``` have "a mod b mod b = (a mod b + a div b * b) mod b" ``` haftmann@66806 ` 236` ``` by (simp only: mod_mult_self1) ``` haftmann@66806 ` 237` ``` also have "\ = a mod b" ``` haftmann@66806 ` 238` ``` by (simp only: mod_div_mult_eq) ``` haftmann@66806 ` 239` ``` finally show ?thesis . ``` haftmann@66806 ` 240` ```qed ``` haftmann@66806 ` 241` haftmann@66806 ` 242` ```lemma mod_mod_cancel: ``` haftmann@66806 ` 243` ``` assumes "c dvd b" ``` haftmann@66806 ` 244` ``` shows "a mod b mod c = a mod c" ``` haftmann@66806 ` 245` ```proof - ``` haftmann@66806 ` 246` ``` from \c dvd b\ obtain k where "b = c * k" ``` haftmann@66806 ` 247` ``` by (rule dvdE) ``` haftmann@66806 ` 248` ``` have "a mod b mod c = a mod (c * k) mod c" ``` haftmann@66806 ` 249` ``` by (simp only: \b = c * k\) ``` haftmann@66806 ` 250` ``` also have "\ = (a mod (c * k) + a div (c * k) * k * c) mod c" ``` haftmann@66806 ` 251` ``` by (simp only: mod_mult_self1) ``` haftmann@66806 ` 252` ``` also have "\ = (a div (c * k) * (c * k) + a mod (c * k)) mod c" ``` haftmann@66806 ` 253` ``` by (simp only: ac_simps) ``` haftmann@66806 ` 254` ``` also have "\ = a mod c" ``` haftmann@66806 ` 255` ``` by (simp only: div_mult_mod_eq) ``` haftmann@66806 ` 256` ``` finally show ?thesis . ``` haftmann@66806 ` 257` ```qed ``` haftmann@66806 ` 258` haftmann@66806 ` 259` ```lemma div_mult_mult2 [simp]: ``` haftmann@66806 ` 260` ``` "c \ 0 \ (a * c) div (b * c) = a div b" ``` haftmann@66806 ` 261` ``` by (drule div_mult_mult1) (simp add: mult.commute) ``` haftmann@66806 ` 262` haftmann@66806 ` 263` ```lemma div_mult_mult1_if [simp]: ``` haftmann@66806 ` 264` ``` "(c * a) div (c * b) = (if c = 0 then 0 else a div b)" ``` haftmann@66806 ` 265` ``` by simp_all ``` haftmann@66806 ` 266` haftmann@66806 ` 267` ```lemma mod_mult_mult1: ``` haftmann@66806 ` 268` ``` "(c * a) mod (c * b) = c * (a mod b)" ``` haftmann@66806 ` 269` ```proof (cases "c = 0") ``` haftmann@66806 ` 270` ``` case True then show ?thesis by simp ``` haftmann@66806 ` 271` ```next ``` haftmann@66806 ` 272` ``` case False ``` haftmann@66806 ` 273` ``` from div_mult_mod_eq ``` haftmann@66806 ` 274` ``` have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" . ``` haftmann@66806 ` 275` ``` with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b) ``` haftmann@66806 ` 276` ``` = c * a + c * (a mod b)" by (simp add: algebra_simps) ``` haftmann@66806 ` 277` ``` with div_mult_mod_eq show ?thesis by simp ``` haftmann@66806 ` 278` ```qed ``` haftmann@66806 ` 279` haftmann@66806 ` 280` ```lemma mod_mult_mult2: ``` haftmann@66806 ` 281` ``` "(a * c) mod (b * c) = (a mod b) * c" ``` haftmann@66806 ` 282` ``` using mod_mult_mult1 [of c a b] by (simp add: mult.commute) ``` haftmann@66806 ` 283` haftmann@66806 ` 284` ```lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)" ``` haftmann@66806 ` 285` ``` by (fact mod_mult_mult2 [symmetric]) ``` haftmann@66806 ` 286` haftmann@66806 ` 287` ```lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)" ``` haftmann@66806 ` 288` ``` by (fact mod_mult_mult1 [symmetric]) ``` haftmann@66806 ` 289` haftmann@66806 ` 290` ```lemma dvd_mod: "k dvd m \ k dvd n \ k dvd (m mod n)" ``` haftmann@66806 ` 291` ``` unfolding dvd_def by (auto simp add: mod_mult_mult1) ``` haftmann@66806 ` 292` haftmann@66806 ` 293` ```lemma div_plus_div_distrib_dvd_left: ``` haftmann@66806 ` 294` ``` "c dvd a \ (a + b) div c = a div c + b div c" ``` haftmann@66806 ` 295` ``` by (cases "c = 0") (auto elim: dvdE) ``` haftmann@66806 ` 296` haftmann@66806 ` 297` ```lemma div_plus_div_distrib_dvd_right: ``` haftmann@66806 ` 298` ``` "c dvd b \ (a + b) div c = a div c + b div c" ``` haftmann@66806 ` 299` ``` using div_plus_div_distrib_dvd_left [of c b a] ``` haftmann@66806 ` 300` ``` by (simp add: ac_simps) ``` haftmann@66806 ` 301` haftmann@66806 ` 302` ```named_theorems mod_simps ``` haftmann@66806 ` 303` haftmann@66806 ` 304` ```text \Addition respects modular equivalence.\ ``` haftmann@66806 ` 305` haftmann@66806 ` 306` ```lemma mod_add_left_eq [mod_simps]: ``` haftmann@66806 ` 307` ``` "(a mod c + b) mod c = (a + b) mod c" ``` haftmann@66806 ` 308` ```proof - ``` haftmann@66806 ` 309` ``` have "(a + b) mod c = (a div c * c + a mod c + b) mod c" ``` haftmann@66806 ` 310` ``` by (simp only: div_mult_mod_eq) ``` haftmann@66806 ` 311` ``` also have "\ = (a mod c + b + a div c * c) mod c" ``` haftmann@66806 ` 312` ``` by (simp only: ac_simps) ``` haftmann@66806 ` 313` ``` also have "\ = (a mod c + b) mod c" ``` haftmann@66806 ` 314` ``` by (rule mod_mult_self1) ``` haftmann@66806 ` 315` ``` finally show ?thesis ``` haftmann@66806 ` 316` ``` by (rule sym) ``` haftmann@66806 ` 317` ```qed ``` haftmann@66806 ` 318` haftmann@66806 ` 319` ```lemma mod_add_right_eq [mod_simps]: ``` haftmann@66806 ` 320` ``` "(a + b mod c) mod c = (a + b) mod c" ``` haftmann@66806 ` 321` ``` using mod_add_left_eq [of b c a] by (simp add: ac_simps) ``` haftmann@66806 ` 322` haftmann@66806 ` 323` ```lemma mod_add_eq: ``` haftmann@66806 ` 324` ``` "(a mod c + b mod c) mod c = (a + b) mod c" ``` haftmann@66806 ` 325` ``` by (simp add: mod_add_left_eq mod_add_right_eq) ``` haftmann@66806 ` 326` haftmann@66806 ` 327` ```lemma mod_sum_eq [mod_simps]: ``` haftmann@66806 ` 328` ``` "(\i\A. f i mod a) mod a = sum f A mod a" ``` haftmann@66806 ` 329` ```proof (induct A rule: infinite_finite_induct) ``` haftmann@66806 ` 330` ``` case (insert i A) ``` haftmann@66806 ` 331` ``` then have "(\i\insert i A. f i mod a) mod a ``` haftmann@66806 ` 332` ``` = (f i mod a + (\i\A. f i mod a)) mod a" ``` haftmann@66806 ` 333` ``` by simp ``` haftmann@66806 ` 334` ``` also have "\ = (f i + (\i\A. f i mod a) mod a) mod a" ``` haftmann@66806 ` 335` ``` by (simp add: mod_simps) ``` haftmann@66806 ` 336` ``` also have "\ = (f i + (\i\A. f i) mod a) mod a" ``` haftmann@66806 ` 337` ``` by (simp add: insert.hyps) ``` haftmann@66806 ` 338` ``` finally show ?case ``` haftmann@66806 ` 339` ``` by (simp add: insert.hyps mod_simps) ``` haftmann@66806 ` 340` ```qed simp_all ``` haftmann@66806 ` 341` haftmann@66806 ` 342` ```lemma mod_add_cong: ``` haftmann@66806 ` 343` ``` assumes "a mod c = a' mod c" ``` haftmann@66806 ` 344` ``` assumes "b mod c = b' mod c" ``` haftmann@66806 ` 345` ``` shows "(a + b) mod c = (a' + b') mod c" ``` haftmann@66806 ` 346` ```proof - ``` haftmann@66806 ` 347` ``` have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c" ``` haftmann@66806 ` 348` ``` unfolding assms .. ``` haftmann@66806 ` 349` ``` then show ?thesis ``` haftmann@66806 ` 350` ``` by (simp add: mod_add_eq) ``` haftmann@66806 ` 351` ```qed ``` haftmann@66806 ` 352` haftmann@66806 ` 353` ```text \Multiplication respects modular equivalence.\ ``` haftmann@66806 ` 354` haftmann@66806 ` 355` ```lemma mod_mult_left_eq [mod_simps]: ``` haftmann@66806 ` 356` ``` "((a mod c) * b) mod c = (a * b) mod c" ``` haftmann@66806 ` 357` ```proof - ``` haftmann@66806 ` 358` ``` have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c" ``` haftmann@66806 ` 359` ``` by (simp only: div_mult_mod_eq) ``` haftmann@66806 ` 360` ``` also have "\ = (a mod c * b + a div c * b * c) mod c" ``` haftmann@66806 ` 361` ``` by (simp only: algebra_simps) ``` haftmann@66806 ` 362` ``` also have "\ = (a mod c * b) mod c" ``` haftmann@66806 ` 363` ``` by (rule mod_mult_self1) ``` haftmann@66806 ` 364` ``` finally show ?thesis ``` haftmann@66806 ` 365` ``` by (rule sym) ``` haftmann@66806 ` 366` ```qed ``` haftmann@66806 ` 367` haftmann@66806 ` 368` ```lemma mod_mult_right_eq [mod_simps]: ``` haftmann@66806 ` 369` ``` "(a * (b mod c)) mod c = (a * b) mod c" ``` haftmann@66806 ` 370` ``` using mod_mult_left_eq [of b c a] by (simp add: ac_simps) ``` haftmann@66806 ` 371` haftmann@66806 ` 372` ```lemma mod_mult_eq: ``` haftmann@66806 ` 373` ``` "((a mod c) * (b mod c)) mod c = (a * b) mod c" ``` haftmann@66806 ` 374` ``` by (simp add: mod_mult_left_eq mod_mult_right_eq) ``` haftmann@66806 ` 375` haftmann@66806 ` 376` ```lemma mod_prod_eq [mod_simps]: ``` haftmann@66806 ` 377` ``` "(\i\A. f i mod a) mod a = prod f A mod a" ``` haftmann@66806 ` 378` ```proof (induct A rule: infinite_finite_induct) ``` haftmann@66806 ` 379` ``` case (insert i A) ``` haftmann@66806 ` 380` ``` then have "(\i\insert i A. f i mod a) mod a ``` haftmann@66806 ` 381` ``` = (f i mod a * (\i\A. f i mod a)) mod a" ``` haftmann@66806 ` 382` ``` by simp ``` haftmann@66806 ` 383` ``` also have "\ = (f i * ((\i\A. f i mod a) mod a)) mod a" ``` haftmann@66806 ` 384` ``` by (simp add: mod_simps) ``` haftmann@66806 ` 385` ``` also have "\ = (f i * ((\i\A. f i) mod a)) mod a" ``` haftmann@66806 ` 386` ``` by (simp add: insert.hyps) ``` haftmann@66806 ` 387` ``` finally show ?case ``` haftmann@66806 ` 388` ``` by (simp add: insert.hyps mod_simps) ``` haftmann@66806 ` 389` ```qed simp_all ``` haftmann@66806 ` 390` haftmann@66806 ` 391` ```lemma mod_mult_cong: ``` haftmann@66806 ` 392` ``` assumes "a mod c = a' mod c" ``` haftmann@66806 ` 393` ``` assumes "b mod c = b' mod c" ``` haftmann@66806 ` 394` ``` shows "(a * b) mod c = (a' * b') mod c" ``` haftmann@66806 ` 395` ```proof - ``` haftmann@66806 ` 396` ``` have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c" ``` haftmann@66806 ` 397` ``` unfolding assms .. ``` haftmann@66806 ` 398` ``` then show ?thesis ``` haftmann@66806 ` 399` ``` by (simp add: mod_mult_eq) ``` haftmann@66806 ` 400` ```qed ``` haftmann@66806 ` 401` haftmann@66806 ` 402` ```text \Exponentiation respects modular equivalence.\ ``` haftmann@66806 ` 403` haftmann@66806 ` 404` ```lemma power_mod [mod_simps]: ``` haftmann@66806 ` 405` ``` "((a mod b) ^ n) mod b = (a ^ n) mod b" ``` haftmann@66806 ` 406` ```proof (induct n) ``` haftmann@66806 ` 407` ``` case 0 ``` haftmann@66806 ` 408` ``` then show ?case by simp ``` haftmann@66806 ` 409` ```next ``` haftmann@66806 ` 410` ``` case (Suc n) ``` haftmann@66806 ` 411` ``` have "(a mod b) ^ Suc n mod b = (a mod b) * ((a mod b) ^ n mod b) mod b" ``` haftmann@66806 ` 412` ``` by (simp add: mod_mult_right_eq) ``` haftmann@66806 ` 413` ``` with Suc show ?case ``` haftmann@66806 ` 414` ``` by (simp add: mod_mult_left_eq mod_mult_right_eq) ``` haftmann@66806 ` 415` ```qed ``` haftmann@66806 ` 416` haftmann@66806 ` 417` ```end ``` haftmann@66806 ` 418` haftmann@66806 ` 419` haftmann@66806 ` 420` ```class euclidean_ring_cancel = euclidean_ring + euclidean_semiring_cancel ``` haftmann@66806 ` 421` ```begin ``` haftmann@66806 ` 422` haftmann@66806 ` 423` ```subclass idom_divide .. ``` haftmann@66806 ` 424` haftmann@66806 ` 425` ```lemma div_minus_minus [simp]: "(- a) div (- b) = a div b" ``` haftmann@66806 ` 426` ``` using div_mult_mult1 [of "- 1" a b] by simp ``` haftmann@66806 ` 427` haftmann@66806 ` 428` ```lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)" ``` haftmann@66806 ` 429` ``` using mod_mult_mult1 [of "- 1" a b] by simp ``` haftmann@66806 ` 430` haftmann@66806 ` 431` ```lemma div_minus_right: "a div (- b) = (- a) div b" ``` haftmann@66806 ` 432` ``` using div_minus_minus [of "- a" b] by simp ``` haftmann@66806 ` 433` haftmann@66806 ` 434` ```lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)" ``` haftmann@66806 ` 435` ``` using mod_minus_minus [of "- a" b] by simp ``` haftmann@66806 ` 436` haftmann@66806 ` 437` ```lemma div_minus1_right [simp]: "a div (- 1) = - a" ``` haftmann@66806 ` 438` ``` using div_minus_right [of a 1] by simp ``` haftmann@66806 ` 439` haftmann@66806 ` 440` ```lemma mod_minus1_right [simp]: "a mod (- 1) = 0" ``` haftmann@66806 ` 441` ``` using mod_minus_right [of a 1] by simp ``` haftmann@66806 ` 442` haftmann@66806 ` 443` ```text \Negation respects modular equivalence.\ ``` haftmann@66806 ` 444` haftmann@66806 ` 445` ```lemma mod_minus_eq [mod_simps]: ``` haftmann@66806 ` 446` ``` "(- (a mod b)) mod b = (- a) mod b" ``` haftmann@66806 ` 447` ```proof - ``` haftmann@66806 ` 448` ``` have "(- a) mod b = (- (a div b * b + a mod b)) mod b" ``` haftmann@66806 ` 449` ``` by (simp only: div_mult_mod_eq) ``` haftmann@66806 ` 450` ``` also have "\ = (- (a mod b) + - (a div b) * b) mod b" ``` haftmann@66806 ` 451` ``` by (simp add: ac_simps) ``` haftmann@66806 ` 452` ``` also have "\ = (- (a mod b)) mod b" ``` haftmann@66806 ` 453` ``` by (rule mod_mult_self1) ``` haftmann@66806 ` 454` ``` finally show ?thesis ``` haftmann@66806 ` 455` ``` by (rule sym) ``` haftmann@66806 ` 456` ```qed ``` haftmann@66806 ` 457` haftmann@66806 ` 458` ```lemma mod_minus_cong: ``` haftmann@66806 ` 459` ``` assumes "a mod b = a' mod b" ``` haftmann@66806 ` 460` ``` shows "(- a) mod b = (- a') mod b" ``` haftmann@66806 ` 461` ```proof - ``` haftmann@66806 ` 462` ``` have "(- (a mod b)) mod b = (- (a' mod b)) mod b" ``` haftmann@66806 ` 463` ``` unfolding assms .. ``` haftmann@66806 ` 464` ``` then show ?thesis ``` haftmann@66806 ` 465` ``` by (simp add: mod_minus_eq) ``` haftmann@66806 ` 466` ```qed ``` haftmann@66806 ` 467` haftmann@66806 ` 468` ```text \Subtraction respects modular equivalence.\ ``` haftmann@66806 ` 469` haftmann@66806 ` 470` ```lemma mod_diff_left_eq [mod_simps]: ``` haftmann@66806 ` 471` ``` "(a mod c - b) mod c = (a - b) mod c" ``` haftmann@66806 ` 472` ``` using mod_add_cong [of a c "a mod c" "- b" "- b"] ``` haftmann@66806 ` 473` ``` by simp ``` haftmann@66806 ` 474` haftmann@66806 ` 475` ```lemma mod_diff_right_eq [mod_simps]: ``` haftmann@66806 ` 476` ``` "(a - b mod c) mod c = (a - b) mod c" ``` haftmann@66806 ` 477` ``` using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] ``` haftmann@66806 ` 478` ``` by simp ``` haftmann@66806 ` 479` haftmann@66806 ` 480` ```lemma mod_diff_eq: ``` haftmann@66806 ` 481` ``` "(a mod c - b mod c) mod c = (a - b) mod c" ``` haftmann@66806 ` 482` ``` using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] ``` haftmann@66806 ` 483` ``` by simp ``` haftmann@66806 ` 484` haftmann@66806 ` 485` ```lemma mod_diff_cong: ``` haftmann@66806 ` 486` ``` assumes "a mod c = a' mod c" ``` haftmann@66806 ` 487` ``` assumes "b mod c = b' mod c" ``` haftmann@66806 ` 488` ``` shows "(a - b) mod c = (a' - b') mod c" ``` haftmann@66806 ` 489` ``` using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"] ``` haftmann@66806 ` 490` ``` by simp ``` haftmann@66806 ` 491` haftmann@66806 ` 492` ```lemma minus_mod_self2 [simp]: ``` haftmann@66806 ` 493` ``` "(a - b) mod b = a mod b" ``` haftmann@66806 ` 494` ``` using mod_diff_right_eq [of a b b] ``` haftmann@66806 ` 495` ``` by (simp add: mod_diff_right_eq) ``` haftmann@66806 ` 496` haftmann@66806 ` 497` ```lemma minus_mod_self1 [simp]: ``` haftmann@66806 ` 498` ``` "(b - a) mod b = - a mod b" ``` haftmann@66806 ` 499` ``` using mod_add_self2 [of "- a" b] by simp ``` haftmann@66806 ` 500` haftmann@66806 ` 501` ```lemma mod_eq_dvd_iff: ``` haftmann@66806 ` 502` ``` "a mod c = b mod c \ c dvd a - b" (is "?P \ ?Q") ``` haftmann@66806 ` 503` ```proof ``` haftmann@66806 ` 504` ``` assume ?P ``` haftmann@66806 ` 505` ``` then have "(a mod c - b mod c) mod c = 0" ``` haftmann@66806 ` 506` ``` by simp ``` haftmann@66806 ` 507` ``` then show ?Q ``` haftmann@66806 ` 508` ``` by (simp add: dvd_eq_mod_eq_0 mod_simps) ``` haftmann@66806 ` 509` ```next ``` haftmann@66806 ` 510` ``` assume ?Q ``` haftmann@66806 ` 511` ``` then obtain d where d: "a - b = c * d" .. ``` haftmann@66806 ` 512` ``` then have "a = c * d + b" ``` haftmann@66806 ` 513` ``` by (simp add: algebra_simps) ``` haftmann@66806 ` 514` ``` then show ?P by simp ``` haftmann@66806 ` 515` ```qed ``` haftmann@66806 ` 516` haftmann@66806 ` 517` ```end ``` haftmann@66806 ` 518` haftmann@66806 ` 519` ``` ``` haftmann@64785 ` 520` ```subsection \Uniquely determined division\ ``` haftmann@64785 ` 521` ``` ``` haftmann@64785 ` 522` ```class unique_euclidean_semiring = euclidean_semiring + ``` haftmann@64785 ` 523` ``` fixes uniqueness_constraint :: "'a \ 'a \ bool" ``` haftmann@64785 ` 524` ``` assumes size_mono_mult: ``` haftmann@64785 ` 525` ``` "b \ 0 \ euclidean_size a < euclidean_size c ``` haftmann@64785 ` 526` ``` \ euclidean_size (a * b) < euclidean_size (c * b)" ``` haftmann@64785 ` 527` ``` -- \FIXME justify\ ``` haftmann@64785 ` 528` ``` assumes uniqueness_constraint_mono_mult: ``` haftmann@64785 ` 529` ``` "uniqueness_constraint a b \ uniqueness_constraint (a * c) (b * c)" ``` haftmann@64785 ` 530` ``` assumes uniqueness_constraint_mod: ``` haftmann@64785 ` 531` ``` "b \ 0 \ \ b dvd a \ uniqueness_constraint (a mod b) b" ``` haftmann@64785 ` 532` ``` assumes div_bounded: ``` haftmann@64785 ` 533` ``` "b \ 0 \ uniqueness_constraint r b ``` haftmann@64785 ` 534` ``` \ euclidean_size r < euclidean_size b ``` haftmann@64785 ` 535` ``` \ (q * b + r) div b = q" ``` haftmann@64785 ` 536` ```begin ``` haftmann@64785 ` 537` haftmann@64785 ` 538` ```lemma divmod_cases [case_names divides remainder by0]: ``` haftmann@64785 ` 539` ``` obtains ``` haftmann@64785 ` 540` ``` (divides) q where "b \ 0" ``` haftmann@64785 ` 541` ``` and "a div b = q" ``` haftmann@64785 ` 542` ``` and "a mod b = 0" ``` haftmann@64785 ` 543` ``` and "a = q * b" ``` haftmann@64785 ` 544` ``` | (remainder) q r where "b \ 0" and "r \ 0" ``` haftmann@64785 ` 545` ``` and "uniqueness_constraint r b" ``` haftmann@64785 ` 546` ``` and "euclidean_size r < euclidean_size b" ``` haftmann@64785 ` 547` ``` and "a div b = q" ``` haftmann@64785 ` 548` ``` and "a mod b = r" ``` haftmann@64785 ` 549` ``` and "a = q * b + r" ``` haftmann@64785 ` 550` ``` | (by0) "b = 0" ``` haftmann@64785 ` 551` ```proof (cases "b = 0") ``` haftmann@64785 ` 552` ``` case True ``` haftmann@64785 ` 553` ``` then show thesis ``` haftmann@64785 ` 554` ``` by (rule by0) ``` haftmann@64785 ` 555` ```next ``` haftmann@64785 ` 556` ``` case False ``` haftmann@64785 ` 557` ``` show thesis ``` haftmann@64785 ` 558` ``` proof (cases "b dvd a") ``` haftmann@64785 ` 559` ``` case True ``` haftmann@64785 ` 560` ``` then obtain q where "a = b * q" .. ``` haftmann@64785 ` 561` ``` with \b \ 0\ divides ``` haftmann@64785 ` 562` ``` show thesis ``` haftmann@64785 ` 563` ``` by (simp add: ac_simps) ``` haftmann@64785 ` 564` ``` next ``` haftmann@64785 ` 565` ``` case False ``` haftmann@64785 ` 566` ``` then have "a mod b \ 0" ``` haftmann@64785 ` 567` ``` by (simp add: mod_eq_0_iff_dvd) ``` haftmann@64785 ` 568` ``` moreover from \b \ 0\ \\ b dvd a\ have "uniqueness_constraint (a mod b) b" ``` haftmann@64785 ` 569` ``` by (rule uniqueness_constraint_mod) ``` haftmann@64785 ` 570` ``` moreover have "euclidean_size (a mod b) < euclidean_size b" ``` haftmann@64785 ` 571` ``` using \b \ 0\ by (rule mod_size_less) ``` haftmann@64785 ` 572` ``` moreover have "a = a div b * b + a mod b" ``` haftmann@64785 ` 573` ``` by (simp add: div_mult_mod_eq) ``` haftmann@64785 ` 574` ``` ultimately show thesis ``` haftmann@64785 ` 575` ``` using \b \ 0\ by (blast intro: remainder) ``` haftmann@64785 ` 576` ``` qed ``` haftmann@64785 ` 577` ```qed ``` haftmann@64785 ` 578` haftmann@64785 ` 579` ```lemma div_eqI: ``` haftmann@64785 ` 580` ``` "a div b = q" if "b \ 0" "uniqueness_constraint r b" ``` haftmann@64785 ` 581` ``` "euclidean_size r < euclidean_size b" "q * b + r = a" ``` haftmann@64785 ` 582` ```proof - ``` haftmann@64785 ` 583` ``` from that have "(q * b + r) div b = q" ``` haftmann@64785 ` 584` ``` by (auto intro: div_bounded) ``` haftmann@64785 ` 585` ``` with that show ?thesis ``` haftmann@64785 ` 586` ``` by simp ``` haftmann@64785 ` 587` ```qed ``` haftmann@64785 ` 588` haftmann@64785 ` 589` ```lemma mod_eqI: ``` haftmann@64785 ` 590` ``` "a mod b = r" if "b \ 0" "uniqueness_constraint r b" ``` haftmann@64785 ` 591` ``` "euclidean_size r < euclidean_size b" "q * b + r = a" ``` haftmann@64785 ` 592` ```proof - ``` haftmann@64785 ` 593` ``` from that have "a div b = q" ``` haftmann@64785 ` 594` ``` by (rule div_eqI) ``` haftmann@64785 ` 595` ``` moreover have "a div b * b + a mod b = a" ``` haftmann@64785 ` 596` ``` by (fact div_mult_mod_eq) ``` haftmann@64785 ` 597` ``` ultimately have "a div b * b + a mod b = a div b * b + r" ``` haftmann@64785 ` 598` ``` using \q * b + r = a\ by simp ``` haftmann@64785 ` 599` ``` then show ?thesis ``` haftmann@64785 ` 600` ``` by simp ``` haftmann@64785 ` 601` ```qed ``` haftmann@64785 ` 602` haftmann@66806 ` 603` ```subclass euclidean_semiring_cancel ``` haftmann@66806 ` 604` ```proof ``` haftmann@66806 ` 605` ``` show "(a + c * b) div b = c + a div b" if "b \ 0" for a b c ``` haftmann@66806 ` 606` ``` proof (cases a b rule: divmod_cases) ``` haftmann@66806 ` 607` ``` case by0 ``` haftmann@66806 ` 608` ``` with \b \ 0\ show ?thesis ``` haftmann@66806 ` 609` ``` by simp ``` haftmann@66806 ` 610` ``` next ``` haftmann@66806 ` 611` ``` case (divides q) ``` haftmann@66806 ` 612` ``` then show ?thesis ``` haftmann@66806 ` 613` ``` by (simp add: ac_simps) ``` haftmann@66806 ` 614` ``` next ``` haftmann@66806 ` 615` ``` case (remainder q r) ``` haftmann@66806 ` 616` ``` then show ?thesis ``` haftmann@66806 ` 617` ``` by (auto intro: div_eqI simp add: algebra_simps) ``` haftmann@66806 ` 618` ``` qed ``` haftmann@66806 ` 619` ```next ``` haftmann@66806 ` 620` ``` show"(c * a) div (c * b) = a div b" if "c \ 0" for a b c ``` haftmann@66806 ` 621` ``` proof (cases a b rule: divmod_cases) ``` haftmann@66806 ` 622` ``` case by0 ``` haftmann@66806 ` 623` ``` then show ?thesis ``` haftmann@66806 ` 624` ``` by simp ``` haftmann@66806 ` 625` ``` next ``` haftmann@66806 ` 626` ``` case (divides q) ``` haftmann@66806 ` 627` ``` with \c \ 0\ show ?thesis ``` haftmann@66806 ` 628` ``` by (simp add: mult.left_commute [of c]) ``` haftmann@66806 ` 629` ``` next ``` haftmann@66806 ` 630` ``` case (remainder q r) ``` haftmann@66806 ` 631` ``` from \b \ 0\ \c \ 0\ have "b * c \ 0" ``` haftmann@66806 ` 632` ``` by simp ``` haftmann@66806 ` 633` ``` from remainder \c \ 0\ ``` haftmann@66806 ` 634` ``` have "uniqueness_constraint (r * c) (b * c)" ``` haftmann@66806 ` 635` ``` and "euclidean_size (r * c) < euclidean_size (b * c)" ``` haftmann@66806 ` 636` ``` by (simp_all add: uniqueness_constraint_mono_mult uniqueness_constraint_mod size_mono_mult) ``` haftmann@66806 ` 637` ``` with remainder show ?thesis ``` haftmann@66806 ` 638` ``` by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps) ``` haftmann@66806 ` 639` ``` (use \b * c \ 0\ in simp) ``` haftmann@66806 ` 640` ``` qed ``` haftmann@66806 ` 641` ```qed ``` haftmann@66806 ` 642` haftmann@64785 ` 643` ```end ``` haftmann@64785 ` 644` haftmann@64785 ` 645` ```class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring ``` haftmann@66806 ` 646` ```begin ``` haftmann@66806 ` 647` ``` ``` haftmann@66806 ` 648` ```subclass euclidean_ring_cancel .. ``` haftmann@64785 ` 649` haftmann@64785 ` 650` ```end ``` haftmann@66806 ` 651` haftmann@66808 ` 652` haftmann@66808 ` 653` ```subsection \Euclidean division on @{typ nat}\ ``` haftmann@66808 ` 654` haftmann@66808 ` 655` ```instantiation nat :: unique_euclidean_semiring ``` haftmann@66808 ` 656` ```begin ``` haftmann@66808 ` 657` haftmann@66808 ` 658` ```definition normalize_nat :: "nat \ nat" ``` haftmann@66808 ` 659` ``` where [simp]: "normalize = (id :: nat \ nat)" ``` haftmann@66808 ` 660` haftmann@66808 ` 661` ```definition unit_factor_nat :: "nat \ nat" ``` haftmann@66808 ` 662` ``` where "unit_factor n = (if n = 0 then 0 else 1 :: nat)" ``` haftmann@66808 ` 663` haftmann@66808 ` 664` ```lemma unit_factor_simps [simp]: ``` haftmann@66808 ` 665` ``` "unit_factor 0 = (0::nat)" ``` haftmann@66808 ` 666` ``` "unit_factor (Suc n) = 1" ``` haftmann@66808 ` 667` ``` by (simp_all add: unit_factor_nat_def) ``` haftmann@66808 ` 668` haftmann@66808 ` 669` ```definition euclidean_size_nat :: "nat \ nat" ``` haftmann@66808 ` 670` ``` where [simp]: "euclidean_size_nat = id" ``` haftmann@66808 ` 671` haftmann@66808 ` 672` ```definition uniqueness_constraint_nat :: "nat \ nat \ bool" ``` haftmann@66808 ` 673` ``` where [simp]: "uniqueness_constraint_nat = \" ``` haftmann@66808 ` 674` haftmann@66808 ` 675` ```definition divide_nat :: "nat \ nat \ nat" ``` haftmann@66808 ` 676` ``` where "m div n = (if n = 0 then 0 else Max {k::nat. k * n \ m})" ``` haftmann@66808 ` 677` haftmann@66808 ` 678` ```definition modulo_nat :: "nat \ nat \ nat" ``` haftmann@66808 ` 679` ``` where "m mod n = m - (m div n * (n::nat))" ``` haftmann@66808 ` 680` haftmann@66808 ` 681` ```instance proof ``` haftmann@66808 ` 682` ``` fix m n :: nat ``` haftmann@66808 ` 683` ``` have ex: "\k. k * n \ l" for l :: nat ``` haftmann@66808 ` 684` ``` by (rule exI [of _ 0]) simp ``` haftmann@66808 ` 685` ``` have fin: "finite {k. k * n \ l}" if "n > 0" for l ``` haftmann@66808 ` 686` ``` proof - ``` haftmann@66808 ` 687` ``` from that have "{k. k * n \ l} \ {k. k \ l}" ``` haftmann@66808 ` 688` ``` by (cases n) auto ``` haftmann@66808 ` 689` ``` then show ?thesis ``` haftmann@66808 ` 690` ``` by (rule finite_subset) simp ``` haftmann@66808 ` 691` ``` qed ``` haftmann@66808 ` 692` ``` have mult_div_unfold: "n * (m div n) = Max {l. l \ m \ n dvd l}" ``` haftmann@66808 ` 693` ``` proof (cases "n = 0") ``` haftmann@66808 ` 694` ``` case True ``` haftmann@66808 ` 695` ``` moreover have "{l. l = 0 \ l \ m} = {0::nat}" ``` haftmann@66808 ` 696` ``` by auto ``` haftmann@66808 ` 697` ``` ultimately show ?thesis ``` haftmann@66808 ` 698` ``` by simp ``` haftmann@66808 ` 699` ``` next ``` haftmann@66808 ` 700` ``` case False ``` haftmann@66808 ` 701` ``` with ex [of m] fin have "n * Max {k. k * n \ m} = Max (times n ` {k. k * n \ m})" ``` haftmann@66808 ` 702` ``` by (auto simp add: nat_mult_max_right intro: hom_Max_commute) ``` haftmann@66808 ` 703` ``` also have "times n ` {k. k * n \ m} = {l. l \ m \ n dvd l}" ``` haftmann@66808 ` 704` ``` by (auto simp add: ac_simps elim!: dvdE) ``` haftmann@66808 ` 705` ``` finally show ?thesis ``` haftmann@66808 ` 706` ``` using False by (simp add: divide_nat_def ac_simps) ``` haftmann@66808 ` 707` ``` qed ``` haftmann@66808 ` 708` ``` show "n div 0 = 0" ``` haftmann@66808 ` 709` ``` by (simp add: divide_nat_def) ``` haftmann@66808 ` 710` ``` have less_eq: "m div n * n \ m" ``` haftmann@66808 ` 711` ``` by (auto simp add: mult_div_unfold ac_simps intro: Max.boundedI) ``` haftmann@66808 ` 712` ``` then show "m div n * n + m mod n = m" ``` haftmann@66808 ` 713` ``` by (simp add: modulo_nat_def) ``` haftmann@66808 ` 714` ``` assume "n \ 0" ``` haftmann@66808 ` 715` ``` show "m * n div n = m" ``` haftmann@66808 ` 716` ``` using \n \ 0\ by (auto simp add: divide_nat_def ac_simps intro: Max_eqI) ``` haftmann@66808 ` 717` ``` show "euclidean_size (m mod n) < euclidean_size n" ``` haftmann@66808 ` 718` ``` proof - ``` haftmann@66808 ` 719` ``` have "m < Suc (m div n) * n" ``` haftmann@66808 ` 720` ``` proof (rule ccontr) ``` haftmann@66808 ` 721` ``` assume "\ m < Suc (m div n) * n" ``` haftmann@66808 ` 722` ``` then have "Suc (m div n) * n \ m" ``` haftmann@66808 ` 723` ``` by (simp add: not_less) ``` haftmann@66808 ` 724` ``` moreover from \n \ 0\ have "Max {k. k * n \ m} < Suc (m div n)" ``` haftmann@66808 ` 725` ``` by (simp add: divide_nat_def) ``` haftmann@66808 ` 726` ``` with \n \ 0\ ex fin have "\k. k * n \ m \ k < Suc (m div n)" ``` haftmann@66808 ` 727` ``` by auto ``` haftmann@66808 ` 728` ``` ultimately have "Suc (m div n) < Suc (m div n)" ``` haftmann@66808 ` 729` ``` by blast ``` haftmann@66808 ` 730` ``` then show False ``` haftmann@66808 ` 731` ``` by simp ``` haftmann@66808 ` 732` ``` qed ``` haftmann@66808 ` 733` ``` with \n \ 0\ show ?thesis ``` haftmann@66808 ` 734` ``` by (simp add: modulo_nat_def) ``` haftmann@66808 ` 735` ``` qed ``` haftmann@66808 ` 736` ``` show "euclidean_size m \ euclidean_size (m * n)" ``` haftmann@66808 ` 737` ``` using \n \ 0\ by (cases n) simp_all ``` haftmann@66808 ` 738` ``` fix q r :: nat ``` haftmann@66808 ` 739` ``` show "(q * n + r) div n = q" if "euclidean_size r < euclidean_size n" ``` haftmann@66808 ` 740` ``` proof - ``` haftmann@66808 ` 741` ``` from that have "r < n" ``` haftmann@66808 ` 742` ``` by simp ``` haftmann@66808 ` 743` ``` have "k \ q" if "k * n \ q * n + r" for k ``` haftmann@66808 ` 744` ``` proof (rule ccontr) ``` haftmann@66808 ` 745` ``` assume "\ k \ q" ``` haftmann@66808 ` 746` ``` then have "q < k" ``` haftmann@66808 ` 747` ``` by simp ``` haftmann@66808 ` 748` ``` then obtain l where "k = Suc (q + l)" ``` haftmann@66808 ` 749` ``` by (auto simp add: less_iff_Suc_add) ``` haftmann@66808 ` 750` ``` with \r < n\ that show False ``` haftmann@66808 ` 751` ``` by (simp add: algebra_simps) ``` haftmann@66808 ` 752` ``` qed ``` haftmann@66808 ` 753` ``` with \n \ 0\ ex fin show ?thesis ``` haftmann@66808 ` 754` ``` by (auto simp add: divide_nat_def Max_eq_iff) ``` haftmann@66808 ` 755` ``` qed ``` haftmann@66808 ` 756` ```qed (simp_all add: unit_factor_nat_def) ``` haftmann@66808 ` 757` haftmann@66806 ` 758` ```end ``` haftmann@66808 ` 759` haftmann@66808 ` 760` ```text \Tool support\ ``` haftmann@66808 ` 761` haftmann@66808 ` 762` ```ML \ ``` haftmann@66808 ` 763` ```structure Cancel_Div_Mod_Nat = Cancel_Div_Mod ``` haftmann@66808 ` 764` ```( ``` haftmann@66808 ` 765` ``` val div_name = @{const_name divide}; ``` haftmann@66808 ` 766` ``` val mod_name = @{const_name modulo}; ``` haftmann@66808 ` 767` ``` val mk_binop = HOLogic.mk_binop; ``` haftmann@66808 ` 768` ``` val mk_plus = HOLogic.mk_binop @{const_name Groups.plus}; ``` haftmann@66808 ` 769` ``` val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT; ``` haftmann@66808 ` 770` ``` fun mk_sum [] = HOLogic.zero ``` haftmann@66808 ` 771` ``` | mk_sum [t] = t ``` haftmann@66808 ` 772` ``` | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); ``` haftmann@66808 ` 773` ``` fun dest_sum tm = ``` haftmann@66808 ` 774` ``` if HOLogic.is_zero tm then [] ``` haftmann@66808 ` 775` ``` else ``` haftmann@66808 ` 776` ``` (case try HOLogic.dest_Suc tm of ``` haftmann@66808 ` 777` ``` SOME t => HOLogic.Suc_zero :: dest_sum t ``` haftmann@66808 ` 778` ``` | NONE => ``` haftmann@66808 ` 779` ``` (case try dest_plus tm of ``` haftmann@66808 ` 780` ``` SOME (t, u) => dest_sum t @ dest_sum u ``` haftmann@66808 ` 781` ``` | NONE => [tm])); ``` haftmann@66808 ` 782` haftmann@66808 ` 783` ``` val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules}; ``` haftmann@66808 ` 784` haftmann@66808 ` 785` ``` val prove_eq_sums = Arith_Data.prove_conv2 all_tac ``` haftmann@66808 ` 786` ``` (Arith_Data.simp_all_tac @{thms add_0_left add_0_right ac_simps}) ``` haftmann@66808 ` 787` ```) ``` haftmann@66808 ` 788` ```\ ``` haftmann@66808 ` 789` haftmann@66808 ` 790` ```simproc_setup cancel_div_mod_nat ("(m::nat) + n") = ``` haftmann@66808 ` 791` ``` \K Cancel_Div_Mod_Nat.proc\ ``` haftmann@66808 ` 792` haftmann@66808 ` 793` ```lemma div_nat_eqI: ``` haftmann@66808 ` 794` ``` "m div n = q" if "n * q \ m" and "m < n * Suc q" for m n q :: nat ``` haftmann@66808 ` 795` ``` by (rule div_eqI [of _ "m - n * q"]) (use that in \simp_all add: algebra_simps\) ``` haftmann@66808 ` 796` haftmann@66808 ` 797` ```lemma mod_nat_eqI: ``` haftmann@66808 ` 798` ``` "m mod n = r" if "r < n" and "r \ m" and "n dvd m - r" for m n r :: nat ``` haftmann@66808 ` 799` ``` by (rule mod_eqI [of _ _ "(m - r) div n"]) (use that in \simp_all add: algebra_simps\) ``` haftmann@66808 ` 800` haftmann@66808 ` 801` ```lemma div_mult_self_is_m [simp]: ``` haftmann@66808 ` 802` ``` "m * n div n = m" if "n > 0" for m n :: nat ``` haftmann@66808 ` 803` ``` using that by simp ``` haftmann@66808 ` 804` haftmann@66808 ` 805` ```lemma div_mult_self1_is_m [simp]: ``` haftmann@66808 ` 806` ``` "n * m div n = m" if "n > 0" for m n :: nat ``` haftmann@66808 ` 807` ``` using that by simp ``` haftmann@66808 ` 808` haftmann@66808 ` 809` ```lemma mod_less_divisor [simp]: ``` haftmann@66808 ` 810` ``` "m mod n < n" if "n > 0" for m n :: nat ``` haftmann@66808 ` 811` ``` using mod_size_less [of n m] that by simp ``` haftmann@66808 ` 812` haftmann@66808 ` 813` ```lemma mod_le_divisor [simp]: ``` haftmann@66808 ` 814` ``` "m mod n \ n" if "n > 0" for m n :: nat ``` haftmann@66808 ` 815` ``` using that by (auto simp add: le_less) ``` haftmann@66808 ` 816` haftmann@66808 ` 817` ```lemma div_times_less_eq_dividend [simp]: ``` haftmann@66808 ` 818` ``` "m div n * n \ m" for m n :: nat ``` haftmann@66808 ` 819` ``` by (simp add: minus_mod_eq_div_mult [symmetric]) ``` haftmann@66808 ` 820` haftmann@66808 ` 821` ```lemma times_div_less_eq_dividend [simp]: ``` haftmann@66808 ` 822` ``` "n * (m div n) \ m" for m n :: nat ``` haftmann@66808 ` 823` ``` using div_times_less_eq_dividend [of m n] ``` haftmann@66808 ` 824` ``` by (simp add: ac_simps) ``` haftmann@66808 ` 825` haftmann@66808 ` 826` ```lemma dividend_less_div_times: ``` haftmann@66808 ` 827` ``` "m < n + (m div n) * n" if "0 < n" for m n :: nat ``` haftmann@66808 ` 828` ```proof - ``` haftmann@66808 ` 829` ``` from that have "m mod n < n" ``` haftmann@66808 ` 830` ``` by simp ``` haftmann@66808 ` 831` ``` then show ?thesis ``` haftmann@66808 ` 832` ``` by (simp add: minus_mod_eq_div_mult [symmetric]) ``` haftmann@66808 ` 833` ```qed ``` haftmann@66808 ` 834` haftmann@66808 ` 835` ```lemma dividend_less_times_div: ``` haftmann@66808 ` 836` ``` "m < n + n * (m div n)" if "0 < n" for m n :: nat ``` haftmann@66808 ` 837` ``` using dividend_less_div_times [of n m] that ``` haftmann@66808 ` 838` ``` by (simp add: ac_simps) ``` haftmann@66808 ` 839` haftmann@66808 ` 840` ```lemma mod_Suc_le_divisor [simp]: ``` haftmann@66808 ` 841` ``` "m mod Suc n \ n" ``` haftmann@66808 ` 842` ``` using mod_less_divisor [of "Suc n" m] by arith ``` haftmann@66808 ` 843` haftmann@66808 ` 844` ```lemma mod_less_eq_dividend [simp]: ``` haftmann@66808 ` 845` ``` "m mod n \ m" for m n :: nat ``` haftmann@66808 ` 846` ```proof (rule add_leD2) ``` haftmann@66808 ` 847` ``` from div_mult_mod_eq have "m div n * n + m mod n = m" . ``` haftmann@66808 ` 848` ``` then show "m div n * n + m mod n \ m" by auto ``` haftmann@66808 ` 849` ```qed ``` haftmann@66808 ` 850` haftmann@66808 ` 851` ```lemma ``` haftmann@66808 ` 852` ``` div_less [simp]: "m div n = 0" ``` haftmann@66808 ` 853` ``` and mod_less [simp]: "m mod n = m" ``` haftmann@66808 ` 854` ``` if "m < n" for m n :: nat ``` haftmann@66808 ` 855` ``` using that by (auto intro: div_eqI mod_eqI) ``` haftmann@66808 ` 856` haftmann@66808 ` 857` ```lemma le_div_geq: ``` haftmann@66808 ` 858` ``` "m div n = Suc ((m - n) div n)" if "0 < n" and "n \ m" for m n :: nat ``` haftmann@66808 ` 859` ```proof - ``` haftmann@66808 ` 860` ``` from \n \ m\ obtain q where "m = n + q" ``` haftmann@66808 ` 861` ``` by (auto simp add: le_iff_add) ``` haftmann@66808 ` 862` ``` with \0 < n\ show ?thesis ``` haftmann@66808 ` 863` ``` by (simp add: div_add_self1) ``` haftmann@66808 ` 864` ```qed ``` haftmann@66808 ` 865` haftmann@66808 ` 866` ```lemma le_mod_geq: ``` haftmann@66808 ` 867` ``` "m mod n = (m - n) mod n" if "n \ m" for m n :: nat ``` haftmann@66808 ` 868` ```proof - ``` haftmann@66808 ` 869` ``` from \n \ m\ obtain q where "m = n + q" ``` haftmann@66808 ` 870` ``` by (auto simp add: le_iff_add) ``` haftmann@66808 ` 871` ``` then show ?thesis ``` haftmann@66808 ` 872` ``` by simp ``` haftmann@66808 ` 873` ```qed ``` haftmann@66808 ` 874` haftmann@66808 ` 875` ```lemma div_if: ``` haftmann@66808 ` 876` ``` "m div n = (if m < n \ n = 0 then 0 else Suc ((m - n) div n))" ``` haftmann@66808 ` 877` ``` by (simp add: le_div_geq) ``` haftmann@66808 ` 878` haftmann@66808 ` 879` ```lemma mod_if: ``` haftmann@66808 ` 880` ``` "m mod n = (if m < n then m else (m - n) mod n)" for m n :: nat ``` haftmann@66808 ` 881` ``` by (simp add: le_mod_geq) ``` haftmann@66808 ` 882` haftmann@66808 ` 883` ```lemma div_eq_0_iff: ``` haftmann@66808 ` 884` ``` "m div n = 0 \ m < n \ n = 0" for m n :: nat ``` haftmann@66808 ` 885` ``` by (simp add: div_if) ``` haftmann@66808 ` 886` haftmann@66808 ` 887` ```lemma div_greater_zero_iff: ``` haftmann@66808 ` 888` ``` "m div n > 0 \ n \ m \ n > 0" for m n :: nat ``` haftmann@66808 ` 889` ``` using div_eq_0_iff [of m n] by auto ``` haftmann@66808 ` 890` haftmann@66808 ` 891` ```lemma mod_greater_zero_iff_not_dvd: ``` haftmann@66808 ` 892` ``` "m mod n > 0 \ \ n dvd m" for m n :: nat ``` haftmann@66808 ` 893` ``` by (simp add: dvd_eq_mod_eq_0) ``` haftmann@66808 ` 894` haftmann@66808 ` 895` ```lemma div_by_Suc_0 [simp]: ``` haftmann@66808 ` 896` ``` "m div Suc 0 = m" ``` haftmann@66808 ` 897` ``` using div_by_1 [of m] by simp ``` haftmann@66808 ` 898` haftmann@66808 ` 899` ```lemma mod_by_Suc_0 [simp]: ``` haftmann@66808 ` 900` ``` "m mod Suc 0 = 0" ``` haftmann@66808 ` 901` ``` using mod_by_1 [of m] by simp ``` haftmann@66808 ` 902` haftmann@66808 ` 903` ```lemma div2_Suc_Suc [simp]: ``` haftmann@66808 ` 904` ``` "Suc (Suc m) div 2 = Suc (m div 2)" ``` haftmann@66808 ` 905` ``` by (simp add: numeral_2_eq_2 le_div_geq) ``` haftmann@66808 ` 906` haftmann@66808 ` 907` ```lemma Suc_n_div_2_gt_zero [simp]: ``` haftmann@66808 ` 908` ``` "0 < Suc n div 2" if "n > 0" for n :: nat ``` haftmann@66808 ` 909` ``` using that by (cases n) simp_all ``` haftmann@66808 ` 910` haftmann@66808 ` 911` ```lemma div_2_gt_zero [simp]: ``` haftmann@66808 ` 912` ``` "0 < n div 2" if "Suc 0 < n" for n :: nat ``` haftmann@66808 ` 913` ``` using that Suc_n_div_2_gt_zero [of "n - 1"] by simp ``` haftmann@66808 ` 914` haftmann@66808 ` 915` ```lemma mod2_Suc_Suc [simp]: ``` haftmann@66808 ` 916` ``` "Suc (Suc m) mod 2 = m mod 2" ``` haftmann@66808 ` 917` ``` by (simp add: numeral_2_eq_2 le_mod_geq) ``` haftmann@66808 ` 918` haftmann@66808 ` 919` ```lemma add_self_div_2 [simp]: ``` haftmann@66808 ` 920` ``` "(m + m) div 2 = m" for m :: nat ``` haftmann@66808 ` 921` ``` by (simp add: mult_2 [symmetric]) ``` haftmann@66808 ` 922` haftmann@66808 ` 923` ```lemma add_self_mod_2 [simp]: ``` haftmann@66808 ` 924` ``` "(m + m) mod 2 = 0" for m :: nat ``` haftmann@66808 ` 925` ``` by (simp add: mult_2 [symmetric]) ``` haftmann@66808 ` 926` haftmann@66808 ` 927` ```lemma mod2_gr_0 [simp]: ``` haftmann@66808 ` 928` ``` "0 < m mod 2 \ m mod 2 = 1" for m :: nat ``` haftmann@66808 ` 929` ```proof - ``` haftmann@66808 ` 930` ``` have "m mod 2 < 2" ``` haftmann@66808 ` 931` ``` by (rule mod_less_divisor) simp ``` haftmann@66808 ` 932` ``` then have "m mod 2 = 0 \ m mod 2 = 1" ``` haftmann@66808 ` 933` ``` by arith ``` haftmann@66808 ` 934` ``` then show ?thesis ``` haftmann@66808 ` 935` ``` by auto ``` haftmann@66808 ` 936` ```qed ``` haftmann@66808 ` 937` haftmann@66808 ` 938` ```lemma mod_Suc_eq [mod_simps]: ``` haftmann@66808 ` 939` ``` "Suc (m mod n) mod n = Suc m mod n" ``` haftmann@66808 ` 940` ```proof - ``` haftmann@66808 ` 941` ``` have "(m mod n + 1) mod n = (m + 1) mod n" ``` haftmann@66808 ` 942` ``` by (simp only: mod_simps) ``` haftmann@66808 ` 943` ``` then show ?thesis ``` haftmann@66808 ` 944` ``` by simp ``` haftmann@66808 ` 945` ```qed ``` haftmann@66808 ` 946` haftmann@66808 ` 947` ```lemma mod_Suc_Suc_eq [mod_simps]: ``` haftmann@66808 ` 948` ``` "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n" ``` haftmann@66808 ` 949` ```proof - ``` haftmann@66808 ` 950` ``` have "(m mod n + 2) mod n = (m + 2) mod n" ``` haftmann@66808 ` 951` ``` by (simp only: mod_simps) ``` haftmann@66808 ` 952` ``` then show ?thesis ``` haftmann@66808 ` 953` ``` by simp ``` haftmann@66808 ` 954` ```qed ``` haftmann@66808 ` 955` haftmann@66808 ` 956` ```lemma ``` haftmann@66808 ` 957` ``` Suc_mod_mult_self1 [simp]: "Suc (m + k * n) mod n = Suc m mod n" ``` haftmann@66808 ` 958` ``` and Suc_mod_mult_self2 [simp]: "Suc (m + n * k) mod n = Suc m mod n" ``` haftmann@66808 ` 959` ``` and Suc_mod_mult_self3 [simp]: "Suc (k * n + m) mod n = Suc m mod n" ``` haftmann@66808 ` 960` ``` and Suc_mod_mult_self4 [simp]: "Suc (n * k + m) mod n = Suc m mod n" ``` haftmann@66808 ` 961` ``` by (subst mod_Suc_eq [symmetric], simp add: mod_simps)+ ``` haftmann@66808 ` 962` haftmann@66808 ` 963` ```lemma div_mult1_eq: -- \TODO: Generalization candidate\ ``` haftmann@66808 ` 964` ``` "(a * b) div c = a * (b div c) + a * (b mod c) div c" for a b c :: nat ``` haftmann@66808 ` 965` ``` apply (cases "c = 0") ``` haftmann@66808 ` 966` ``` apply simp ``` haftmann@66808 ` 967` ``` apply (rule div_eqI [of _ "(a * (b mod c)) mod c"]) ``` haftmann@66808 ` 968` ``` apply (auto simp add: algebra_simps distrib_left [symmetric]) ``` haftmann@66808 ` 969` ``` done ``` haftmann@66808 ` 970` haftmann@66808 ` 971` ```lemma div_add1_eq: -- \NOT suitable for rewriting: the RHS has an instance of the LHS\ ``` haftmann@66808 ` 972` ``` -- \TODO: Generalization candidate\ ``` haftmann@66808 ` 973` ``` "(a + b) div c = a div c + b div c + ((a mod c + b mod c) div c)" for a b c :: nat ``` haftmann@66808 ` 974` ``` apply (cases "c = 0") ``` haftmann@66808 ` 975` ``` apply simp ``` haftmann@66808 ` 976` ``` apply (rule div_eqI [of _ "(a mod c + b mod c) mod c"]) ``` haftmann@66808 ` 977` ``` apply (auto simp add: algebra_simps) ``` haftmann@66808 ` 978` ``` done ``` haftmann@66808 ` 979` haftmann@66808 ` 980` ```context ``` haftmann@66808 ` 981` ``` fixes m n q :: nat ``` haftmann@66808 ` 982` ```begin ``` haftmann@66808 ` 983` haftmann@66808 ` 984` ```private lemma eucl_rel_mult2: ``` haftmann@66808 ` 985` ``` "m mod n + n * (m div n mod q) < n * q" ``` haftmann@66808 ` 986` ``` if "n > 0" and "q > 0" ``` haftmann@66808 ` 987` ```proof - ``` haftmann@66808 ` 988` ``` from \n > 0\ have "m mod n < n" ``` haftmann@66808 ` 989` ``` by (rule mod_less_divisor) ``` haftmann@66808 ` 990` ``` from \q > 0\ have "m div n mod q < q" ``` haftmann@66808 ` 991` ``` by (rule mod_less_divisor) ``` haftmann@66808 ` 992` ``` then obtain s where "q = Suc (m div n mod q + s)" ``` haftmann@66808 ` 993` ``` by (blast dest: less_imp_Suc_add) ``` haftmann@66808 ` 994` ``` moreover have "m mod n + n * (m div n mod q) < n * Suc (m div n mod q + s)" ``` haftmann@66808 ` 995` ``` using \m mod n < n\ by (simp add: add_mult_distrib2) ``` haftmann@66808 ` 996` ``` ultimately show ?thesis ``` haftmann@66808 ` 997` ``` by simp ``` haftmann@66808 ` 998` ```qed ``` haftmann@66808 ` 999` haftmann@66808 ` 1000` ```lemma div_mult2_eq: ``` haftmann@66808 ` 1001` ``` "m div (n * q) = (m div n) div q" ``` haftmann@66808 ` 1002` ```proof (cases "n = 0 \ q = 0") ``` haftmann@66808 ` 1003` ``` case True ``` haftmann@66808 ` 1004` ``` then show ?thesis ``` haftmann@66808 ` 1005` ``` by auto ``` haftmann@66808 ` 1006` ```next ``` haftmann@66808 ` 1007` ``` case False ``` haftmann@66808 ` 1008` ``` with eucl_rel_mult2 show ?thesis ``` haftmann@66808 ` 1009` ``` by (auto intro: div_eqI [of _ "n * (m div n mod q) + m mod n"] ``` haftmann@66808 ` 1010` ``` simp add: algebra_simps add_mult_distrib2 [symmetric]) ``` haftmann@66808 ` 1011` ```qed ``` haftmann@66808 ` 1012` haftmann@66808 ` 1013` ```lemma mod_mult2_eq: ``` haftmann@66808 ` 1014` ``` "m mod (n * q) = n * (m div n mod q) + m mod n" ``` haftmann@66808 ` 1015` ```proof (cases "n = 0 \ q = 0") ``` haftmann@66808 ` 1016` ``` case True ``` haftmann@66808 ` 1017` ``` then show ?thesis ``` haftmann@66808 ` 1018` ``` by auto ``` haftmann@66808 ` 1019` ```next ``` haftmann@66808 ` 1020` ``` case False ``` haftmann@66808 ` 1021` ``` with eucl_rel_mult2 show ?thesis ``` haftmann@66808 ` 1022` ``` by (auto intro: mod_eqI [of _ _ "(m div n) div q"] ``` haftmann@66808 ` 1023` ``` simp add: algebra_simps add_mult_distrib2 [symmetric]) ``` haftmann@66808 ` 1024` ```qed ``` haftmann@66808 ` 1025` haftmann@66808 ` 1026` ```end ``` haftmann@66808 ` 1027` haftmann@66808 ` 1028` ```lemma div_le_mono: ``` haftmann@66808 ` 1029` ``` "m div k \ n div k" if "m \ n" for m n k :: nat ``` haftmann@66808 ` 1030` ```proof - ``` haftmann@66808 ` 1031` ``` from that obtain q where "n = m + q" ``` haftmann@66808 ` 1032` ``` by (auto simp add: le_iff_add) ``` haftmann@66808 ` 1033` ``` then show ?thesis ``` haftmann@66808 ` 1034` ``` by (simp add: div_add1_eq [of m q k]) ``` haftmann@66808 ` 1035` ```qed ``` haftmann@66808 ` 1036` haftmann@66808 ` 1037` ```text \Antimonotonicity of @{const divide} in second argument\ ``` haftmann@66808 ` 1038` haftmann@66808 ` 1039` ```lemma div_le_mono2: ``` haftmann@66808 ` 1040` ``` "k div n \ k div m" if "0 < m" and "m \ n" for m n k :: nat ``` haftmann@66808 ` 1041` ```using that proof (induct k arbitrary: m rule: less_induct) ``` haftmann@66808 ` 1042` ``` case (less k) ``` haftmann@66808 ` 1043` ``` show ?case ``` haftmann@66808 ` 1044` ``` proof (cases "n \ k") ``` haftmann@66808 ` 1045` ``` case False ``` haftmann@66808 ` 1046` ``` then show ?thesis ``` haftmann@66808 ` 1047` ``` by simp ``` haftmann@66808 ` 1048` ``` next ``` haftmann@66808 ` 1049` ``` case True ``` haftmann@66808 ` 1050` ``` have "(k - n) div n \ (k - m) div n" ``` haftmann@66808 ` 1051` ``` using less.prems ``` haftmann@66808 ` 1052` ``` by (blast intro: div_le_mono diff_le_mono2) ``` haftmann@66808 ` 1053` ``` also have "\ \ (k - m) div m" ``` haftmann@66808 ` 1054` ``` using \n \ k\ less.prems less.hyps [of "k - m" m] ``` haftmann@66808 ` 1055` ``` by simp ``` haftmann@66808 ` 1056` ``` finally show ?thesis ``` haftmann@66808 ` 1057` ``` using \n \ k\ less.prems ``` haftmann@66808 ` 1058` ``` by (simp add: le_div_geq) ``` haftmann@66808 ` 1059` ``` qed ``` haftmann@66808 ` 1060` ```qed ``` haftmann@66808 ` 1061` haftmann@66808 ` 1062` ```lemma div_le_dividend [simp]: ``` haftmann@66808 ` 1063` ``` "m div n \ m" for m n :: nat ``` haftmann@66808 ` 1064` ``` using div_le_mono2 [of 1 n m] by (cases "n = 0") simp_all ``` haftmann@66808 ` 1065` haftmann@66808 ` 1066` ```lemma div_less_dividend [simp]: ``` haftmann@66808 ` 1067` ``` "m div n < m" if "1 < n" and "0 < m" for m n :: nat ``` haftmann@66808 ` 1068` ```using that proof (induct m rule: less_induct) ``` haftmann@66808 ` 1069` ``` case (less m) ``` haftmann@66808 ` 1070` ``` show ?case ``` haftmann@66808 ` 1071` ``` proof (cases "n < m") ``` haftmann@66808 ` 1072` ``` case False ``` haftmann@66808 ` 1073` ``` with less show ?thesis ``` haftmann@66808 ` 1074` ``` by (cases "n = m") simp_all ``` haftmann@66808 ` 1075` ``` next ``` haftmann@66808 ` 1076` ``` case True ``` haftmann@66808 ` 1077` ``` then show ?thesis ``` haftmann@66808 ` 1078` ``` using less.hyps [of "m - n"] less.prems ``` haftmann@66808 ` 1079` ``` by (simp add: le_div_geq) ``` haftmann@66808 ` 1080` ``` qed ``` haftmann@66808 ` 1081` ```qed ``` haftmann@66808 ` 1082` haftmann@66808 ` 1083` ```lemma div_eq_dividend_iff: ``` haftmann@66808 ` 1084` ``` "m div n = m \ n = 1" if "m > 0" for m n :: nat ``` haftmann@66808 ` 1085` ```proof ``` haftmann@66808 ` 1086` ``` assume "n = 1" ``` haftmann@66808 ` 1087` ``` then show "m div n = m" ``` haftmann@66808 ` 1088` ``` by simp ``` haftmann@66808 ` 1089` ```next ``` haftmann@66808 ` 1090` ``` assume P: "m div n = m" ``` haftmann@66808 ` 1091` ``` show "n = 1" ``` haftmann@66808 ` 1092` ``` proof (rule ccontr) ``` haftmann@66808 ` 1093` ``` have "n \ 0" ``` haftmann@66808 ` 1094` ``` by (rule ccontr) (use that P in auto) ``` haftmann@66808 ` 1095` ``` moreover assume "n \ 1" ``` haftmann@66808 ` 1096` ``` ultimately have "n > 1" ``` haftmann@66808 ` 1097` ``` by simp ``` haftmann@66808 ` 1098` ``` with that have "m div n < m" ``` haftmann@66808 ` 1099` ``` by simp ``` haftmann@66808 ` 1100` ``` with P show False ``` haftmann@66808 ` 1101` ``` by simp ``` haftmann@66808 ` 1102` ``` qed ``` haftmann@66808 ` 1103` ```qed ``` haftmann@66808 ` 1104` haftmann@66808 ` 1105` ```lemma less_mult_imp_div_less: ``` haftmann@66808 ` 1106` ``` "m div n < i" if "m < i * n" for m n i :: nat ``` haftmann@66808 ` 1107` ```proof - ``` haftmann@66808 ` 1108` ``` from that have "i * n > 0" ``` haftmann@66808 ` 1109` ``` by (cases "i * n = 0") simp_all ``` haftmann@66808 ` 1110` ``` then have "i > 0" and "n > 0" ``` haftmann@66808 ` 1111` ``` by simp_all ``` haftmann@66808 ` 1112` ``` have "m div n * n \ m" ``` haftmann@66808 ` 1113` ``` by simp ``` haftmann@66808 ` 1114` ``` then have "m div n * n < i * n" ``` haftmann@66808 ` 1115` ``` using that by (rule le_less_trans) ``` haftmann@66808 ` 1116` ``` with \n > 0\ show ?thesis ``` haftmann@66808 ` 1117` ``` by simp ``` haftmann@66808 ` 1118` ```qed ``` haftmann@66808 ` 1119` haftmann@66808 ` 1120` ```text \A fact for the mutilated chess board\ ``` haftmann@66808 ` 1121` haftmann@66808 ` 1122` ```lemma mod_Suc: ``` haftmann@66808 ` 1123` ``` "Suc m mod n = (if Suc (m mod n) = n then 0 else Suc (m mod n))" (is "_ = ?rhs") ``` haftmann@66808 ` 1124` ```proof (cases "n = 0") ``` haftmann@66808 ` 1125` ``` case True ``` haftmann@66808 ` 1126` ``` then show ?thesis ``` haftmann@66808 ` 1127` ``` by simp ``` haftmann@66808 ` 1128` ```next ``` haftmann@66808 ` 1129` ``` case False ``` haftmann@66808 ` 1130` ``` have "Suc m mod n = Suc (m mod n) mod n" ``` haftmann@66808 ` 1131` ``` by (simp add: mod_simps) ``` haftmann@66808 ` 1132` ``` also have "\ = ?rhs" ``` haftmann@66808 ` 1133` ``` using False by (auto intro!: mod_nat_eqI intro: neq_le_trans simp add: Suc_le_eq) ``` haftmann@66808 ` 1134` ``` finally show ?thesis . ``` haftmann@66808 ` 1135` ```qed ``` haftmann@66808 ` 1136` haftmann@66808 ` 1137` ```lemma Suc_times_mod_eq: ``` haftmann@66808 ` 1138` ``` "Suc (m * n) mod m = 1" if "Suc 0 < m" ``` haftmann@66808 ` 1139` ``` using that by (simp add: mod_Suc) ``` haftmann@66808 ` 1140` haftmann@66808 ` 1141` ```lemma Suc_times_numeral_mod_eq [simp]: ``` haftmann@66808 ` 1142` ``` "Suc (numeral k * n) mod numeral k = 1" if "numeral k \ (1::nat)" ``` haftmann@66808 ` 1143` ``` by (rule Suc_times_mod_eq) (use that in simp) ``` haftmann@66808 ` 1144` haftmann@66808 ` 1145` ```lemma Suc_div_le_mono [simp]: ``` haftmann@66808 ` 1146` ``` "m div n \ Suc m div n" ``` haftmann@66808 ` 1147` ``` by (simp add: div_le_mono) ``` haftmann@66808 ` 1148` haftmann@66808 ` 1149` ```text \These lemmas collapse some needless occurrences of Suc: ``` haftmann@66808 ` 1150` ``` at least three Sucs, since two and fewer are rewritten back to Suc again! ``` haftmann@66808 ` 1151` ``` We already have some rules to simplify operands smaller than 3.\ ``` haftmann@66808 ` 1152` haftmann@66808 ` 1153` ```lemma div_Suc_eq_div_add3 [simp]: ``` haftmann@66808 ` 1154` ``` "m div Suc (Suc (Suc n)) = m div (3 + n)" ``` haftmann@66808 ` 1155` ``` by (simp add: Suc3_eq_add_3) ``` haftmann@66808 ` 1156` haftmann@66808 ` 1157` ```lemma mod_Suc_eq_mod_add3 [simp]: ``` haftmann@66808 ` 1158` ``` "m mod Suc (Suc (Suc n)) = m mod (3 + n)" ``` haftmann@66808 ` 1159` ``` by (simp add: Suc3_eq_add_3) ``` haftmann@66808 ` 1160` haftmann@66808 ` 1161` ```lemma Suc_div_eq_add3_div: ``` haftmann@66808 ` 1162` ``` "Suc (Suc (Suc m)) div n = (3 + m) div n" ``` haftmann@66808 ` 1163` ``` by (simp add: Suc3_eq_add_3) ``` haftmann@66808 ` 1164` haftmann@66808 ` 1165` ```lemma Suc_mod_eq_add3_mod: ``` haftmann@66808 ` 1166` ``` "Suc (Suc (Suc m)) mod n = (3 + m) mod n" ``` haftmann@66808 ` 1167` ``` by (simp add: Suc3_eq_add_3) ``` haftmann@66808 ` 1168` haftmann@66808 ` 1169` ```lemmas Suc_div_eq_add3_div_numeral [simp] = ``` haftmann@66808 ` 1170` ``` Suc_div_eq_add3_div [of _ "numeral v"] for v ``` haftmann@66808 ` 1171` haftmann@66808 ` 1172` ```lemmas Suc_mod_eq_add3_mod_numeral [simp] = ``` haftmann@66808 ` 1173` ``` Suc_mod_eq_add3_mod [of _ "numeral v"] for v ``` haftmann@66808 ` 1174` haftmann@66808 ` 1175` ```lemma (in field_char_0) of_nat_div: ``` haftmann@66808 ` 1176` ``` "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)" ``` haftmann@66808 ` 1177` ```proof - ``` haftmann@66808 ` 1178` ``` 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@66808 ` 1179` ``` unfolding of_nat_add by (cases "n = 0") simp_all ``` haftmann@66808 ` 1180` ``` then show ?thesis ``` haftmann@66808 ` 1181` ``` by simp ``` haftmann@66808 ` 1182` ```qed ``` haftmann@66808 ` 1183` haftmann@66808 ` 1184` ```text \An ``induction'' law for modulus arithmetic.\ ``` haftmann@66808 ` 1185` haftmann@66808 ` 1186` ```lemma mod_induct [consumes 3, case_names step]: ``` haftmann@66808 ` 1187` ``` "P m" if "P n" and "n < p" and "m < p" ``` haftmann@66808 ` 1188` ``` and step: "\n. n < p \ P n \ P (Suc n mod p)" ``` haftmann@66808 ` 1189` ```using \m < p\ proof (induct m) ``` haftmann@66808 ` 1190` ``` case 0 ``` haftmann@66808 ` 1191` ``` show ?case ``` haftmann@66808 ` 1192` ``` proof (rule ccontr) ``` haftmann@66808 ` 1193` ``` assume "\ P 0" ``` haftmann@66808 ` 1194` ``` from \n < p\ have "0 < p" ``` haftmann@66808 ` 1195` ``` by simp ``` haftmann@66808 ` 1196` ``` from \n < p\ obtain m where "0 < m" and "p = n + m" ``` haftmann@66808 ` 1197` ``` by (blast dest: less_imp_add_positive) ``` haftmann@66808 ` 1198` ``` with \P n\ have "P (p - m)" ``` haftmann@66808 ` 1199` ``` by simp ``` haftmann@66808 ` 1200` ``` moreover have "\ P (p - m)" ``` haftmann@66808 ` 1201` ``` using \0 < m\ proof (induct m) ``` haftmann@66808 ` 1202` ``` case 0 ``` haftmann@66808 ` 1203` ``` then show ?case ``` haftmann@66808 ` 1204` ``` by simp ``` haftmann@66808 ` 1205` ``` next ``` haftmann@66808 ` 1206` ``` case (Suc m) ``` haftmann@66808 ` 1207` ``` show ?case ``` haftmann@66808 ` 1208` ``` proof ``` haftmann@66808 ` 1209` ``` assume P: "P (p - Suc m)" ``` haftmann@66808 ` 1210` ``` with \\ P 0\ have "Suc m < p" ``` haftmann@66808 ` 1211` ``` by (auto intro: ccontr) ``` haftmann@66808 ` 1212` ``` then have "Suc (p - Suc m) = p - m" ``` haftmann@66808 ` 1213` ``` by arith ``` haftmann@66808 ` 1214` ``` moreover from \0 < p\ have "p - Suc m < p" ``` haftmann@66808 ` 1215` ``` by arith ``` haftmann@66808 ` 1216` ``` with P step have "P ((Suc (p - Suc m)) mod p)" ``` haftmann@66808 ` 1217` ``` by blast ``` haftmann@66808 ` 1218` ``` ultimately show False ``` haftmann@66808 ` 1219` ``` using \\ P 0\ Suc.hyps by (cases "m = 0") simp_all ``` haftmann@66808 ` 1220` ``` qed ``` haftmann@66808 ` 1221` ``` qed ``` haftmann@66808 ` 1222` ``` ultimately show False ``` haftmann@66808 ` 1223` ``` by blast ``` haftmann@66808 ` 1224` ``` qed ``` haftmann@66808 ` 1225` ```next ``` haftmann@66808 ` 1226` ``` case (Suc m) ``` haftmann@66808 ` 1227` ``` then have "m < p" and mod: "Suc m mod p = Suc m" ``` haftmann@66808 ` 1228` ``` by simp_all ``` haftmann@66808 ` 1229` ``` from \m < p\ have "P m" ``` haftmann@66808 ` 1230` ``` by (rule Suc.hyps) ``` haftmann@66808 ` 1231` ``` with \m < p\ have "P (Suc m mod p)" ``` haftmann@66808 ` 1232` ``` by (rule step) ``` haftmann@66808 ` 1233` ``` with mod show ?case ``` haftmann@66808 ` 1234` ``` by simp ``` haftmann@66808 ` 1235` ```qed ``` haftmann@66808 ` 1236` haftmann@66808 ` 1237` ```lemma split_div: ``` haftmann@66808 ` 1238` ``` "P (m div n) \ (n = 0 \ P 0) \ (n \ 0 \ ``` haftmann@66808 ` 1239` ``` (\i j. j < n \ m = n * i + j \ P i))" ``` haftmann@66808 ` 1240` ``` (is "?P = ?Q") for m n :: nat ``` haftmann@66808 ` 1241` ```proof (cases "n = 0") ``` haftmann@66808 ` 1242` ``` case True ``` haftmann@66808 ` 1243` ``` then show ?thesis ``` haftmann@66808 ` 1244` ``` by simp ``` haftmann@66808 ` 1245` ```next ``` haftmann@66808 ` 1246` ``` case False ``` haftmann@66808 ` 1247` ``` show ?thesis ``` haftmann@66808 ` 1248` ``` proof ``` haftmann@66808 ` 1249` ``` assume ?P ``` haftmann@66808 ` 1250` ``` with False show ?Q ``` haftmann@66808 ` 1251` ``` by auto ``` haftmann@66808 ` 1252` ``` next ``` haftmann@66808 ` 1253` ``` assume ?Q ``` haftmann@66808 ` 1254` ``` with False have *: "\i j. j < n \ m = n * i + j \ P i" ``` haftmann@66808 ` 1255` ``` by simp ``` haftmann@66808 ` 1256` ``` with False show ?P ``` haftmann@66808 ` 1257` ``` by (auto intro: * [of "m mod n"]) ``` haftmann@66808 ` 1258` ``` qed ``` haftmann@66808 ` 1259` ```qed ``` haftmann@66808 ` 1260` haftmann@66808 ` 1261` ```lemma split_div': ``` haftmann@66808 ` 1262` ``` "P (m div n) \ n = 0 \ P 0 \ (\q. (n * q \ m \ m < n * Suc q) \ P q)" ``` haftmann@66808 ` 1263` ```proof (cases "n = 0") ``` haftmann@66808 ` 1264` ``` case True ``` haftmann@66808 ` 1265` ``` then show ?thesis ``` haftmann@66808 ` 1266` ``` by simp ``` haftmann@66808 ` 1267` ```next ``` haftmann@66808 ` 1268` ``` case False ``` haftmann@66808 ` 1269` ``` then have "n * q \ m \ m < n * Suc q \ m div n = q" for q ``` haftmann@66808 ` 1270` ``` by (auto intro: div_nat_eqI dividend_less_times_div) ``` haftmann@66808 ` 1271` ``` then show ?thesis ``` haftmann@66808 ` 1272` ``` by auto ``` haftmann@66808 ` 1273` ```qed ``` haftmann@66808 ` 1274` haftmann@66808 ` 1275` ```lemma split_mod: ``` haftmann@66808 ` 1276` ``` "P (m mod n) \ (n = 0 \ P m) \ (n \ 0 \ ``` haftmann@66808 ` 1277` ``` (\i j. j < n \ m = n * i + j \ P j))" ``` haftmann@66808 ` 1278` ``` (is "?P \ ?Q") for m n :: nat ``` haftmann@66808 ` 1279` ```proof (cases "n = 0") ``` haftmann@66808 ` 1280` ``` case True ``` haftmann@66808 ` 1281` ``` then show ?thesis ``` haftmann@66808 ` 1282` ``` by simp ``` haftmann@66808 ` 1283` ```next ``` haftmann@66808 ` 1284` ``` case False ``` haftmann@66808 ` 1285` ``` show ?thesis ``` haftmann@66808 ` 1286` ``` proof ``` haftmann@66808 ` 1287` ``` assume ?P ``` haftmann@66808 ` 1288` ``` with False show ?Q ``` haftmann@66808 ` 1289` ``` by auto ``` haftmann@66808 ` 1290` ``` next ``` haftmann@66808 ` 1291` ``` assume ?Q ``` haftmann@66808 ` 1292` ``` with False have *: "\i j. j < n \ m = n * i + j \ P j" ``` haftmann@66808 ` 1293` ``` by simp ``` haftmann@66808 ` 1294` ``` with False show ?P ``` haftmann@66808 ` 1295` ``` by (auto intro: * [of _ "m div n"]) ``` haftmann@66808 ` 1296` ``` qed ``` haftmann@66808 ` 1297` ```qed ``` haftmann@66808 ` 1298` haftmann@66808 ` 1299` haftmann@66808 ` 1300` ```subsection \Code generation\ ``` haftmann@66808 ` 1301` haftmann@66808 ` 1302` ```code_identifier ``` haftmann@66808 ` 1303` ``` code_module Euclidean_Division \ (SML) Arith and (OCaml) Arith and (Haskell) Arith ``` haftmann@66808 ` 1304` haftmann@66808 ` 1305` ```end ```