src/HOL/Number_Theory/Factorial_Ring.thy
 author haftmann Thu Mar 03 08:33:55 2016 +0100 (2016-03-03) changeset 62499 4a5b81ff5992 parent 62366 95c6cf433c91 child 63040 eb4ddd18d635 permissions -rw-r--r--
constructive formulation of factorization
 haftmann@60804 ` 1` ```(* Title: HOL/Number_Theory/Factorial_Ring.thy ``` haftmann@60804 ` 2` ``` Author: Florian Haftmann, TU Muenchen ``` haftmann@60804 ` 3` ```*) ``` haftmann@60804 ` 4` haftmann@60804 ` 5` ```section \Factorial (semi)rings\ ``` haftmann@60804 ` 6` haftmann@60804 ` 7` ```theory Factorial_Ring ``` haftmann@62499 ` 8` ```imports Main Primes "~~/src/HOL/Library/Multiset" ``` haftmann@62499 ` 9` ```begin ``` haftmann@62499 ` 10` haftmann@62499 ` 11` ```context algebraic_semidom ``` haftmann@60804 ` 12` ```begin ``` haftmann@60804 ` 13` haftmann@62499 ` 14` ```lemma dvd_mult_imp_div: ``` haftmann@62499 ` 15` ``` assumes "a * c dvd b" ``` haftmann@62499 ` 16` ``` shows "a dvd b div c" ``` haftmann@62499 ` 17` ```proof (cases "c = 0") ``` haftmann@62499 ` 18` ``` case True then show ?thesis by simp ``` haftmann@62499 ` 19` ```next ``` haftmann@62499 ` 20` ``` case False ``` haftmann@62499 ` 21` ``` from \a * c dvd b\ obtain d where "b = a * c * d" .. ``` haftmann@62499 ` 22` ``` with False show ?thesis by (simp add: mult.commute [of a] mult.assoc) ``` haftmann@62499 ` 23` ```qed ``` haftmann@62499 ` 24` haftmann@62499 ` 25` ```end ``` haftmann@62499 ` 26` haftmann@60804 ` 27` ```class factorial_semiring = normalization_semidom + ``` haftmann@60804 ` 28` ``` assumes finite_divisors: "a \ 0 \ finite {b. b dvd a \ normalize b = b}" ``` haftmann@60804 ` 29` ``` fixes is_prime :: "'a \ bool" ``` haftmann@60804 ` 30` ``` assumes not_is_prime_zero [simp]: "\ is_prime 0" ``` haftmann@60804 ` 31` ``` and is_prime_not_unit: "is_prime p \ \ is_unit p" ``` haftmann@62499 ` 32` ``` and no_prime_divisorsI2: "(\b. b dvd a \ \ is_prime b) \ is_unit a" ``` haftmann@60804 ` 33` ``` assumes is_primeI: "p \ 0 \ \ is_unit p \ (\a. a dvd p \ \ is_unit a \ p dvd a) \ is_prime p" ``` haftmann@60804 ` 34` ``` and is_primeD: "is_prime p \ p dvd a * b \ p dvd a \ p dvd b" ``` haftmann@60804 ` 35` ```begin ``` haftmann@60804 ` 36` haftmann@60804 ` 37` ```lemma not_is_prime_one [simp]: ``` haftmann@60804 ` 38` ``` "\ is_prime 1" ``` haftmann@60804 ` 39` ``` by (auto dest: is_prime_not_unit) ``` haftmann@60804 ` 40` haftmann@60804 ` 41` ```lemma is_prime_not_zeroI: ``` haftmann@60804 ` 42` ``` assumes "is_prime p" ``` haftmann@60804 ` 43` ``` shows "p \ 0" ``` haftmann@60804 ` 44` ``` using assms by (auto intro: ccontr) ``` haftmann@60804 ` 45` haftmann@60804 ` 46` ```lemma is_prime_multD: ``` haftmann@60804 ` 47` ``` assumes "is_prime (a * b)" ``` haftmann@60804 ` 48` ``` shows "is_unit a \ is_unit b" ``` haftmann@60804 ` 49` ```proof - ``` haftmann@60804 ` 50` ``` from assms have "a \ 0" "b \ 0" by auto ``` haftmann@60804 ` 51` ``` moreover from assms is_primeD [of "a * b"] have "a * b dvd a \ a * b dvd b" ``` haftmann@60804 ` 52` ``` by auto ``` haftmann@60804 ` 53` ``` ultimately show ?thesis ``` haftmann@60804 ` 54` ``` using dvd_times_left_cancel_iff [of a b 1] ``` haftmann@60804 ` 55` ``` dvd_times_right_cancel_iff [of b a 1] ``` haftmann@60804 ` 56` ``` by auto ``` haftmann@60804 ` 57` ```qed ``` haftmann@60804 ` 58` haftmann@60804 ` 59` ```lemma is_primeD2: ``` haftmann@60804 ` 60` ``` assumes "is_prime p" and "a dvd p" and "\ is_unit a" ``` haftmann@60804 ` 61` ``` shows "p dvd a" ``` haftmann@60804 ` 62` ```proof - ``` haftmann@60804 ` 63` ``` from \a dvd p\ obtain b where "p = a * b" .. ``` haftmann@60804 ` 64` ``` with \is_prime p\ is_prime_multD \\ is_unit a\ have "is_unit b" by auto ``` haftmann@60804 ` 65` ``` with \p = a * b\ show ?thesis ``` haftmann@60804 ` 66` ``` by (auto simp add: mult_unit_dvd_iff) ``` haftmann@60804 ` 67` ```qed ``` haftmann@60804 ` 68` haftmann@60804 ` 69` ```lemma is_prime_mult_unit_left: ``` haftmann@60804 ` 70` ``` assumes "is_prime p" ``` haftmann@60804 ` 71` ``` and "is_unit a" ``` haftmann@60804 ` 72` ``` shows "is_prime (a * p)" ``` haftmann@60804 ` 73` ```proof (rule is_primeI) ``` haftmann@60804 ` 74` ``` from assms show "a * p \ 0" "\ is_unit (a * p)" ``` haftmann@60804 ` 75` ``` by (auto simp add: is_unit_mult_iff is_prime_not_unit) ``` haftmann@60804 ` 76` ``` show "a * p dvd b" if "b dvd a * p" "\ is_unit b" for b ``` haftmann@60804 ` 77` ``` proof - ``` haftmann@60804 ` 78` ``` from that \is_unit a\ have "b dvd p" ``` haftmann@60804 ` 79` ``` using dvd_mult_unit_iff [of a b p] by (simp add: ac_simps) ``` haftmann@60804 ` 80` ``` with \is_prime p\ \\ is_unit b\ have "p dvd b" ``` haftmann@60804 ` 81` ``` using is_primeD2 [of p b] by auto ``` haftmann@60804 ` 82` ``` with \is_unit a\ show ?thesis ``` haftmann@60804 ` 83` ``` using mult_unit_dvd_iff [of a p b] by (simp add: ac_simps) ``` haftmann@60804 ` 84` ``` qed ``` haftmann@60804 ` 85` ```qed ``` haftmann@60804 ` 86` haftmann@60804 ` 87` ```lemma is_primeI2: ``` haftmann@60804 ` 88` ``` assumes "p \ 0" ``` haftmann@60804 ` 89` ``` assumes "\ is_unit p" ``` haftmann@60804 ` 90` ``` assumes P: "\a b. p dvd a * b \ p dvd a \ p dvd b" ``` haftmann@60804 ` 91` ``` shows "is_prime p" ``` haftmann@60804 ` 92` ```using \p \ 0\ \\ is_unit p\ proof (rule is_primeI) ``` haftmann@60804 ` 93` ``` fix a ``` haftmann@60804 ` 94` ``` assume "a dvd p" ``` haftmann@60804 ` 95` ``` then obtain b where "p = a * b" .. ``` haftmann@60804 ` 96` ``` with \p \ 0\ have "b \ 0" by simp ``` haftmann@60804 ` 97` ``` moreover from \p = a * b\ P have "p dvd a \ p dvd b" by auto ``` haftmann@60804 ` 98` ``` moreover assume "\ is_unit a" ``` haftmann@60804 ` 99` ``` ultimately show "p dvd a" ``` haftmann@60804 ` 100` ``` using dvd_times_right_cancel_iff [of b a 1] \p = a * b\ by auto ``` haftmann@60804 ` 101` ```qed ``` haftmann@60804 ` 102` haftmann@60804 ` 103` ```lemma not_is_prime_divisorE: ``` haftmann@60804 ` 104` ``` assumes "a \ 0" and "\ is_unit a" and "\ is_prime a" ``` haftmann@60804 ` 105` ``` obtains b where "b dvd a" and "\ is_unit b" and "\ a dvd b" ``` haftmann@60804 ` 106` ```proof - ``` haftmann@60804 ` 107` ``` from assms have "\b. b dvd a \ \ is_unit b \ \ a dvd b" ``` haftmann@60804 ` 108` ``` by (auto intro: is_primeI) ``` haftmann@60804 ` 109` ``` with that show thesis by blast ``` haftmann@60804 ` 110` ```qed ``` haftmann@60804 ` 111` haftmann@60804 ` 112` ```lemma is_prime_normalize_iff [simp]: ``` haftmann@60804 ` 113` ``` "is_prime (normalize p) \ is_prime p" (is "?P \ ?Q") ``` haftmann@60804 ` 114` ```proof ``` haftmann@60804 ` 115` ``` assume ?Q show ?P ``` haftmann@60804 ` 116` ``` by (rule is_primeI) (insert \?Q\, simp_all add: is_prime_not_zeroI is_prime_not_unit is_primeD2) ``` haftmann@60804 ` 117` ```next ``` haftmann@60804 ` 118` ``` assume ?P show ?Q ``` haftmann@60804 ` 119` ``` by (rule is_primeI) ``` haftmann@60804 ` 120` ``` (insert is_prime_not_zeroI [of "normalize p"] is_prime_not_unit [of "normalize p"] is_primeD2 [of "normalize p"] \?P\, simp_all) ``` haftmann@60804 ` 121` ```qed ``` haftmann@60804 ` 122` haftmann@62499 ` 123` ```lemma no_prime_divisorsI: ``` haftmann@62499 ` 124` ``` assumes "\b. b dvd a \ normalize b = b \ \ is_prime b" ``` haftmann@62499 ` 125` ``` shows "is_unit a" ``` haftmann@62499 ` 126` ```proof (rule no_prime_divisorsI2) ``` haftmann@62499 ` 127` ``` fix b ``` haftmann@62499 ` 128` ``` assume "b dvd a" ``` haftmann@62499 ` 129` ``` then have "normalize b dvd a" ``` haftmann@62499 ` 130` ``` by simp ``` haftmann@62499 ` 131` ``` moreover have "normalize (normalize b) = normalize b" ``` haftmann@62499 ` 132` ``` by simp ``` haftmann@62499 ` 133` ``` ultimately have "\ is_prime (normalize b)" ``` haftmann@62499 ` 134` ``` by (rule assms) ``` haftmann@62499 ` 135` ``` then show "\ is_prime b" ``` haftmann@62499 ` 136` ``` by simp ``` haftmann@62499 ` 137` ```qed ``` haftmann@62499 ` 138` haftmann@62499 ` 139` ```lemma prime_divisorE: ``` haftmann@62499 ` 140` ``` assumes "a \ 0" and "\ is_unit a" ``` haftmann@62499 ` 141` ``` obtains p where "is_prime p" and "p dvd a" ``` haftmann@62499 ` 142` ``` using assms no_prime_divisorsI [of a] by blast ``` haftmann@62499 ` 143` haftmann@62499 ` 144` ```lemma is_prime_associated: ``` haftmann@62499 ` 145` ``` assumes "is_prime p" and "is_prime q" and "q dvd p" ``` haftmann@62499 ` 146` ``` shows "normalize q = normalize p" ``` haftmann@62499 ` 147` ```using \q dvd p\ proof (rule associatedI) ``` haftmann@62499 ` 148` ``` from \is_prime q\ have "\ is_unit q" ``` haftmann@62499 ` 149` ``` by (simp add: is_prime_not_unit) ``` haftmann@62499 ` 150` ``` with \is_prime p\ \q dvd p\ show "p dvd q" ``` haftmann@62499 ` 151` ``` by (blast intro: is_primeD2) ``` haftmann@62499 ` 152` ```qed ``` haftmann@62499 ` 153` haftmann@62499 ` 154` ```lemma prime_dvd_mult_iff: ``` haftmann@62499 ` 155` ``` assumes "is_prime p" ``` haftmann@62499 ` 156` ``` shows "p dvd a * b \ p dvd a \ p dvd b" ``` haftmann@62499 ` 157` ``` using assms by (auto dest: is_primeD) ``` haftmann@62499 ` 158` haftmann@62499 ` 159` ```lemma prime_dvd_msetprod: ``` haftmann@62499 ` 160` ``` assumes "is_prime p" ``` haftmann@62499 ` 161` ``` assumes dvd: "p dvd msetprod A" ``` haftmann@62499 ` 162` ``` obtains a where "a \# A" and "p dvd a" ``` haftmann@62499 ` 163` ```proof - ``` haftmann@62499 ` 164` ``` from dvd have "\a. a \# A \ p dvd a" ``` haftmann@62499 ` 165` ``` proof (induct A) ``` haftmann@62499 ` 166` ``` case empty then show ?case ``` haftmann@62499 ` 167` ``` using \is_prime p\ by (simp add: is_prime_not_unit) ``` haftmann@62499 ` 168` ``` next ``` haftmann@62499 ` 169` ``` case (add A a) ``` haftmann@62499 ` 170` ``` then have "p dvd msetprod A * a" by simp ``` haftmann@62499 ` 171` ``` with \is_prime p\ consider (A) "p dvd msetprod A" | (B) "p dvd a" ``` haftmann@62499 ` 172` ``` by (blast dest: is_primeD) ``` haftmann@62499 ` 173` ``` then show ?case proof cases ``` haftmann@62499 ` 174` ``` case B then show ?thesis by auto ``` haftmann@62499 ` 175` ``` next ``` haftmann@62499 ` 176` ``` case A ``` haftmann@62499 ` 177` ``` with add.hyps obtain b where "b \# A" "p dvd b" ``` haftmann@62499 ` 178` ``` by auto ``` haftmann@62499 ` 179` ``` then show ?thesis by auto ``` haftmann@62499 ` 180` ``` qed ``` haftmann@62499 ` 181` ``` qed ``` haftmann@62499 ` 182` ``` with that show thesis by blast ``` haftmann@62499 ` 183` ```qed ``` haftmann@62499 ` 184` haftmann@62499 ` 185` ```lemma msetprod_eq_iff: ``` haftmann@62499 ` 186` ``` assumes "\p\set_mset P. is_prime p \ normalize p = p" and "\p\set_mset Q. is_prime p \ normalize p = p" ``` haftmann@62499 ` 187` ``` shows "msetprod P = msetprod Q \ P = Q" (is "?R \ ?S") ``` haftmann@62499 ` 188` ```proof ``` haftmann@62499 ` 189` ``` assume ?S then show ?R by simp ``` haftmann@62499 ` 190` ```next ``` haftmann@62499 ` 191` ``` assume ?R then show ?S using assms proof (induct P arbitrary: Q) ``` haftmann@62499 ` 192` ``` case empty then have Q: "msetprod Q = 1" by simp ``` haftmann@62499 ` 193` ``` have "Q = {#}" ``` haftmann@62499 ` 194` ``` proof (rule ccontr) ``` haftmann@62499 ` 195` ``` assume "Q \ {#}" ``` haftmann@62499 ` 196` ``` then obtain r R where "Q = R + {#r#}" ``` haftmann@62499 ` 197` ``` using multi_nonempty_split by blast ``` haftmann@62499 ` 198` ``` moreover with empty have "is_prime r" by simp ``` haftmann@62499 ` 199` ``` ultimately have "msetprod Q = msetprod R * r" ``` haftmann@62499 ` 200` ``` by simp ``` haftmann@62499 ` 201` ``` with Q have "msetprod R * r = 1" ``` haftmann@62499 ` 202` ``` by simp ``` haftmann@62499 ` 203` ``` then have "is_unit r" ``` haftmann@62499 ` 204` ``` by (metis local.dvd_triv_right) ``` haftmann@62499 ` 205` ``` with \is_prime r\ show False by (simp add: is_prime_not_unit) ``` haftmann@62499 ` 206` ``` qed ``` haftmann@62499 ` 207` ``` then show ?case by simp ``` haftmann@62499 ` 208` ``` next ``` haftmann@62499 ` 209` ``` case (add P p) ``` haftmann@62499 ` 210` ``` then have "is_prime p" and "normalize p = p" ``` haftmann@62499 ` 211` ``` and "msetprod Q = msetprod P * p" and "p dvd msetprod Q" ``` haftmann@62499 ` 212` ``` by auto (metis local.dvd_triv_right) ``` haftmann@62499 ` 213` ``` with prime_dvd_msetprod ``` haftmann@62499 ` 214` ``` obtain q where "q \# Q" and "p dvd q" ``` haftmann@62499 ` 215` ``` by blast ``` haftmann@62499 ` 216` ``` with add.prems have "is_prime q" and "normalize q = q" ``` haftmann@62499 ` 217` ``` by simp_all ``` haftmann@62499 ` 218` ``` from \is_prime p\ have "p \ 0" ``` haftmann@62499 ` 219` ``` by auto ``` haftmann@62499 ` 220` ``` from \is_prime q\ \is_prime p\ \p dvd q\ ``` haftmann@62499 ` 221` ``` have "normalize p = normalize q" ``` haftmann@62499 ` 222` ``` by (rule is_prime_associated) ``` haftmann@62499 ` 223` ``` from \normalize p = p\ \normalize q = q\ have "p = q" ``` haftmann@62499 ` 224` ``` unfolding \normalize p = normalize q\ by simp ``` haftmann@62499 ` 225` ``` with \q \# Q\ have "p \# Q" by simp ``` haftmann@62499 ` 226` ``` have "msetprod P = msetprod (Q - {#p#})" ``` haftmann@62499 ` 227` ``` using \p \# Q\ \p \ 0\ \msetprod Q = msetprod P * p\ ``` haftmann@62499 ` 228` ``` by (simp add: msetprod_minus) ``` haftmann@62499 ` 229` ``` then have "P = Q - {#p#}" ``` haftmann@62499 ` 230` ``` using add.prems(2-3) ``` haftmann@62499 ` 231` ``` by (auto intro: add.hyps dest: in_diffD) ``` haftmann@62499 ` 232` ``` with \p \# Q\ show ?case by simp ``` haftmann@62499 ` 233` ``` qed ``` haftmann@62499 ` 234` ```qed ``` haftmann@62499 ` 235` haftmann@62499 ` 236` ```lemma prime_dvd_power_iff: ``` haftmann@62499 ` 237` ``` assumes "is_prime p" ``` haftmann@62499 ` 238` ``` shows "p dvd a ^ n \ p dvd a \ n > 0" ``` haftmann@62499 ` 239` ``` using assms by (induct n) (auto dest: is_prime_not_unit is_primeD) ``` haftmann@62499 ` 240` haftmann@62499 ` 241` ```lemma prime_power_dvd_multD: ``` haftmann@62499 ` 242` ``` assumes "is_prime p" ``` haftmann@62499 ` 243` ``` assumes "p ^ n dvd a * b" and "n > 0" and "\ p dvd a" ``` haftmann@62499 ` 244` ``` shows "p ^ n dvd b" ``` haftmann@62499 ` 245` ```using \p ^ n dvd a * b\ and \n > 0\ proof (induct n arbitrary: b) ``` haftmann@62499 ` 246` ``` case 0 then show ?case by simp ``` haftmann@62499 ` 247` ```next ``` haftmann@62499 ` 248` ``` case (Suc n) show ?case ``` haftmann@62499 ` 249` ``` proof (cases "n = 0") ``` haftmann@62499 ` 250` ``` case True with Suc \is_prime p\ \\ p dvd a\ show ?thesis ``` haftmann@62499 ` 251` ``` by (simp add: prime_dvd_mult_iff) ``` haftmann@62499 ` 252` ``` next ``` haftmann@62499 ` 253` ``` case False then have "n > 0" by simp ``` haftmann@62499 ` 254` ``` from \is_prime p\ have "p \ 0" by auto ``` haftmann@62499 ` 255` ``` from Suc.prems have *: "p * p ^ n dvd a * b" ``` haftmann@62499 ` 256` ``` by simp ``` haftmann@62499 ` 257` ``` then have "p dvd a * b" ``` haftmann@62499 ` 258` ``` by (rule dvd_mult_left) ``` haftmann@62499 ` 259` ``` with Suc \is_prime p\ \\ p dvd a\ have "p dvd b" ``` haftmann@62499 ` 260` ``` by (simp add: prime_dvd_mult_iff) ``` haftmann@62499 ` 261` ``` moreover def c \ "b div p" ``` haftmann@62499 ` 262` ``` ultimately have b: "b = p * c" by simp ``` haftmann@62499 ` 263` ``` with * have "p * p ^ n dvd p * (a * c)" ``` haftmann@62499 ` 264` ``` by (simp add: ac_simps) ``` haftmann@62499 ` 265` ``` with \p \ 0\ have "p ^ n dvd a * c" ``` haftmann@62499 ` 266` ``` by simp ``` haftmann@62499 ` 267` ``` with Suc.hyps \n > 0\ have "p ^ n dvd c" ``` haftmann@62499 ` 268` ``` by blast ``` haftmann@62499 ` 269` ``` with \p \ 0\ show ?thesis ``` haftmann@62499 ` 270` ``` by (simp add: b) ``` haftmann@62499 ` 271` ``` qed ``` haftmann@62499 ` 272` ```qed ``` haftmann@62499 ` 273` haftmann@60804 ` 274` ```lemma is_prime_inj_power: ``` haftmann@60804 ` 275` ``` assumes "is_prime p" ``` haftmann@60804 ` 276` ``` shows "inj (op ^ p)" ``` haftmann@60804 ` 277` ```proof (rule injI, rule ccontr) ``` haftmann@60804 ` 278` ``` fix m n :: nat ``` haftmann@60804 ` 279` ``` have [simp]: "p ^ q = 1 \ q = 0" (is "?P \ ?Q") for q ``` haftmann@60804 ` 280` ``` proof ``` haftmann@60804 ` 281` ``` assume ?Q then show ?P by simp ``` haftmann@60804 ` 282` ``` next ``` haftmann@60804 ` 283` ``` assume ?P then have "is_unit (p ^ q)" by simp ``` haftmann@60804 ` 284` ``` with assms show ?Q by (auto simp add: is_unit_power_iff is_prime_not_unit) ``` haftmann@60804 ` 285` ``` qed ``` haftmann@60804 ` 286` ``` have *: False if "p ^ m = p ^ n" and "m > n" for m n ``` haftmann@60804 ` 287` ``` proof - ``` haftmann@60804 ` 288` ``` from assms have "p \ 0" ``` haftmann@60804 ` 289` ``` by (rule is_prime_not_zeroI) ``` haftmann@60804 ` 290` ``` then have "p ^ n \ 0" ``` haftmann@60804 ` 291` ``` by (induct n) simp_all ``` haftmann@60804 ` 292` ``` from that have "m = n + (m - n)" and "m - n > 0" by arith+ ``` haftmann@60804 ` 293` ``` then obtain q where "m = n + q" and "q > 0" .. ``` haftmann@60804 ` 294` ``` with that have "p ^ n * p ^ q = p ^ n * 1" by (simp add: power_add) ``` haftmann@60804 ` 295` ``` with \p ^ n \ 0\ have "p ^ q = 1" ``` haftmann@60804 ` 296` ``` using mult_left_cancel [of "p ^ n" "p ^ q" 1] by simp ``` haftmann@60804 ` 297` ``` with \q > 0\ show ?thesis by simp ``` haftmann@60804 ` 298` ``` qed ``` haftmann@60804 ` 299` ``` assume "m \ n" ``` haftmann@60804 ` 300` ``` then have "m > n \ m < n" by arith ``` haftmann@60804 ` 301` ``` moreover assume "p ^ m = p ^ n" ``` haftmann@60804 ` 302` ``` ultimately show False using * [of m n] * [of n m] by auto ``` haftmann@60804 ` 303` ```qed ``` haftmann@60804 ` 304` haftmann@62499 ` 305` ```definition factorization :: "'a \ 'a multiset option" ``` haftmann@62499 ` 306` ``` where "factorization a = (if a = 0 then None ``` haftmann@62499 ` 307` ``` else Some (setsum (\p. replicate_mset (Max {n. p ^ n dvd a}) p) ``` haftmann@62499 ` 308` ``` {p. p dvd a \ is_prime p \ normalize p = p}))" ``` haftmann@62499 ` 309` haftmann@62499 ` 310` ```lemma factorization_normalize [simp]: ``` haftmann@62499 ` 311` ``` "factorization (normalize a) = factorization a" ``` haftmann@62499 ` 312` ``` by (simp add: factorization_def) ``` haftmann@62499 ` 313` haftmann@62499 ` 314` ```lemma factorization_0 [simp]: ``` haftmann@62499 ` 315` ``` "factorization 0 = None" ``` haftmann@62499 ` 316` ``` by (simp add: factorization_def) ``` haftmann@62499 ` 317` haftmann@62499 ` 318` ```lemma factorization_eq_None_iff [simp]: ``` haftmann@62499 ` 319` ``` "factorization a = None \ a = 0" ``` haftmann@62499 ` 320` ``` by (simp add: factorization_def) ``` haftmann@60804 ` 321` haftmann@62499 ` 322` ```lemma factorization_eq_Some_iff: ``` haftmann@62499 ` 323` ``` "factorization a = Some P \ ``` haftmann@62499 ` 324` ``` normalize a = msetprod P \ 0 \# P \ (\p \ set_mset P. is_prime p \ normalize p = p)" ``` haftmann@62499 ` 325` ```proof (cases "a = 0") ``` haftmann@62499 ` 326` ``` have [simp]: "0 = msetprod P \ 0 \# P" ``` haftmann@62499 ` 327` ``` using msetprod_zero_iff [of P] by blast ``` haftmann@62499 ` 328` ``` case True ``` haftmann@62499 ` 329` ``` then show ?thesis by auto ``` haftmann@62499 ` 330` ```next ``` haftmann@62499 ` 331` ``` case False ``` haftmann@60804 ` 332` ``` let ?prime_factors = "\a. {p. p dvd a \ is_prime p \ normalize p = p}" ``` haftmann@62499 ` 333` ``` have "?prime_factors a \ {b. b dvd a \ normalize b = b}" ``` haftmann@62499 ` 334` ``` by auto ``` haftmann@62499 ` 335` ``` moreover from \a \ 0\ have "finite {b. b dvd a \ normalize b = b}" ``` haftmann@60804 ` 336` ``` by (rule finite_divisors) ``` haftmann@62499 ` 337` ``` ultimately have "finite (?prime_factors a)" ``` haftmann@62499 ` 338` ``` by (rule finite_subset) ``` haftmann@62499 ` 339` ``` then show ?thesis using \a \ 0\ ``` haftmann@62499 ` 340` ``` proof (induct "?prime_factors a" arbitrary: a P) ``` haftmann@60804 ` 341` ``` case empty then have ``` haftmann@62499 ` 342` ``` *: "{p. p dvd a \ is_prime p \ normalize p = p} = {}" ``` haftmann@62499 ` 343` ``` and "a \ 0" ``` haftmann@60804 ` 344` ``` by auto ``` haftmann@62499 ` 345` ``` from \a \ 0\ have "factorization a = Some {#}" ``` haftmann@62499 ` 346` ``` by (simp only: factorization_def *) simp ``` haftmann@62499 ` 347` ``` from * have "normalize a = 1" ``` haftmann@62499 ` 348` ``` by (auto intro: is_unit_normalize no_prime_divisorsI) ``` haftmann@62499 ` 349` ``` show ?case (is "?lhs \ ?rhs") proof ``` haftmann@62499 ` 350` ``` assume ?lhs with \factorization a = Some {#}\ \normalize a = 1\ ``` haftmann@62499 ` 351` ``` show ?rhs by simp ``` haftmann@62499 ` 352` ``` next ``` haftmann@62499 ` 353` ``` assume ?rhs have "P = {#}" ``` haftmann@62499 ` 354` ``` proof (rule ccontr) ``` haftmann@62499 ` 355` ``` assume "P \ {#}" ``` haftmann@62499 ` 356` ``` then obtain q Q where "P = Q + {#q#}" ``` haftmann@62499 ` 357` ``` using multi_nonempty_split by blast ``` haftmann@62499 ` 358` ``` with \?rhs\ \normalize a = 1\ ``` haftmann@62499 ` 359` ``` have "1 = q * msetprod Q" and "is_prime q" ``` haftmann@62499 ` 360` ``` by (simp_all add: ac_simps) ``` haftmann@62499 ` 361` ``` then have "is_unit q" by (auto intro: dvdI) ``` haftmann@62499 ` 362` ``` with \is_prime q\ show False ``` haftmann@62499 ` 363` ``` using is_prime_not_unit by blast ``` haftmann@62499 ` 364` ``` qed ``` haftmann@62499 ` 365` ``` with \factorization a = Some {#}\ show ?lhs by simp ``` haftmann@60804 ` 366` ``` qed ``` haftmann@60804 ` 367` ``` next ``` haftmann@62499 ` 368` ``` case (insert p F) ``` haftmann@62499 ` 369` ``` from \insert p F = ?prime_factors a\ ``` haftmann@62499 ` 370` ``` have "?prime_factors a = insert p F" ``` haftmann@62499 ` 371` ``` by simp ``` haftmann@62499 ` 372` ``` then have "p dvd a" and "is_prime p" and "normalize p = p" and "p \ 0" ``` haftmann@62499 ` 373` ``` by (auto intro!: is_prime_not_zeroI) ``` haftmann@62499 ` 374` ``` def n \ "Max {n. p ^ n dvd a}" ``` haftmann@62499 ` 375` ``` then have "n > 0" and "p ^ n dvd a" and "\ p ^ Suc n dvd a" ``` haftmann@62499 ` 376` ``` proof - ``` haftmann@60804 ` 377` ``` def N \ "{n. p ^ n dvd a}" ``` haftmann@62499 ` 378` ``` then have n_M: "n = Max N" by (simp add: n_def) ``` haftmann@60804 ` 379` ``` from is_prime_inj_power \is_prime p\ have "inj (op ^ p)" . ``` haftmann@60804 ` 380` ``` then have "inj_on (op ^ p) U" for U ``` haftmann@60804 ` 381` ``` by (rule subset_inj_on) simp ``` haftmann@60804 ` 382` ``` moreover have "op ^ p ` N \ {b. b dvd a \ normalize b = b}" ``` haftmann@60804 ` 383` ``` by (auto simp add: normalize_power \normalize p = p\ N_def) ``` haftmann@60804 ` 384` ``` ultimately have "finite N" ``` haftmann@60804 ` 385` ``` by (rule inj_on_finite) (simp add: finite_divisors \a \ 0\) ``` haftmann@60804 ` 386` ``` from N_def \a \ 0\ have "0 \ N" by (simp add: N_def) ``` haftmann@60804 ` 387` ``` then have "N \ {}" by blast ``` haftmann@60804 ` 388` ``` note * = \finite N\ \N \ {}\ ``` haftmann@60804 ` 389` ``` from N_def \p dvd a\ have "1 \ N" by simp ``` haftmann@62499 ` 390` ``` with * have "Max N > 0" ``` haftmann@60804 ` 391` ``` by (auto simp add: Max_gr_iff) ``` haftmann@62499 ` 392` ``` then show "n > 0" by (simp add: n_M) ``` haftmann@60804 ` 393` ``` from * have "Max N \ N" by (rule Max_in) ``` haftmann@62499 ` 394` ``` then have "p ^ Max N dvd a" by (simp add: N_def) ``` haftmann@62499 ` 395` ``` then show "p ^ n dvd a" by (simp add: n_M) ``` haftmann@60804 ` 396` ``` from * have "\n\N. n \ Max N" ``` haftmann@60804 ` 397` ``` by (simp add: Max_le_iff [symmetric]) ``` haftmann@60804 ` 398` ``` then have "p ^ Suc (Max N) dvd a \ Suc (Max N) \ Max N" ``` haftmann@60804 ` 399` ``` by (rule bspec) (simp add: N_def) ``` haftmann@62499 ` 400` ``` then have "\ p ^ Suc (Max N) dvd a" ``` haftmann@60804 ` 401` ``` by auto ``` haftmann@62499 ` 402` ``` then show "\ p ^ Suc n dvd a" ``` haftmann@62499 ` 403` ``` by (simp add: n_M) ``` haftmann@60804 ` 404` ``` qed ``` haftmann@62499 ` 405` ``` def b \ "a div p ^ n" ``` haftmann@62499 ` 406` ``` with \p ^ n dvd a\ have a: "a = p ^ n * b" ``` haftmann@62499 ` 407` ``` by simp ``` haftmann@62499 ` 408` ``` with \\ p ^ Suc n dvd a\ have "\ p dvd b" and "b \ 0" ``` haftmann@60804 ` 409` ``` by (auto elim: dvdE simp add: ac_simps) ``` haftmann@62499 ` 410` ``` have "?prime_factors a = insert p (?prime_factors b)" ``` haftmann@60804 ` 411` ``` proof (rule set_eqI) ``` haftmann@60804 ` 412` ``` fix q ``` haftmann@62499 ` 413` ``` show "q \ ?prime_factors a \ q \ insert p (?prime_factors b)" ``` haftmann@62499 ` 414` ``` using \is_prime p\ \normalize p = p\ \n > 0\ ``` haftmann@62499 ` 415` ``` by (auto simp add: a prime_dvd_mult_iff prime_dvd_power_iff) ``` haftmann@62499 ` 416` ``` (auto dest: is_prime_associated) ``` haftmann@60804 ` 417` ``` qed ``` haftmann@62499 ` 418` ``` with \\ p dvd b\ have "?prime_factors a - {p} = ?prime_factors b" ``` haftmann@62499 ` 419` ``` by auto ``` haftmann@62499 ` 420` ``` with insert.hyps have "F = ?prime_factors b" ``` haftmann@60804 ` 421` ``` by auto ``` haftmann@62499 ` 422` ``` then have "?prime_factors b = F" ``` haftmann@62499 ` 423` ``` by simp ``` haftmann@62499 ` 424` ``` with \?prime_factors a = insert p (?prime_factors b)\ have "?prime_factors a = insert p F" ``` haftmann@60804 ` 425` ``` by simp ``` haftmann@62499 ` 426` ``` have equiv: "(\p\F. replicate_mset (Max {n. p ^ n dvd a}) p) = ``` haftmann@62499 ` 427` ``` (\p\F. replicate_mset (Max {n. p ^ n dvd b}) p)" ``` haftmann@62499 ` 428` ``` using refl proof (rule Groups_Big.setsum.cong) ``` haftmann@62499 ` 429` ``` fix q ``` haftmann@62499 ` 430` ``` assume "q \ F" ``` haftmann@62499 ` 431` ``` have "{n. q ^ n dvd a} = {n. q ^ n dvd b}" ``` haftmann@62499 ` 432` ``` proof - ``` haftmann@62499 ` 433` ``` have "q ^ m dvd a \ q ^ m dvd b" (is "?R \ ?S") ``` haftmann@62499 ` 434` ``` for m ``` haftmann@62499 ` 435` ``` proof (cases "m = 0") ``` haftmann@62499 ` 436` ``` case True then show ?thesis by simp ``` haftmann@62499 ` 437` ``` next ``` haftmann@62499 ` 438` ``` case False then have "m > 0" by simp ``` haftmann@62499 ` 439` ``` show ?thesis ``` haftmann@62499 ` 440` ``` proof ``` haftmann@62499 ` 441` ``` assume ?S then show ?R by (simp add: a) ``` haftmann@62499 ` 442` ``` next ``` haftmann@62499 ` 443` ``` assume ?R ``` haftmann@62499 ` 444` ``` then have *: "q ^ m dvd p ^ n * b" by (simp add: a) ``` haftmann@62499 ` 445` ``` from insert.hyps \q \ F\ ``` haftmann@62499 ` 446` ``` have "is_prime q" "normalize q = q" "p \ q" "q dvd p ^ n * b" ``` haftmann@62499 ` 447` ``` by (auto simp add: a) ``` haftmann@62499 ` 448` ``` from \is_prime q\ * \m > 0\ show ?S ``` haftmann@62499 ` 449` ``` proof (rule prime_power_dvd_multD) ``` haftmann@62499 ` 450` ``` have "\ q dvd p" ``` haftmann@62499 ` 451` ``` proof ``` haftmann@62499 ` 452` ``` assume "q dvd p" ``` haftmann@62499 ` 453` ``` with \is_prime q\ \is_prime p\ have "normalize q = normalize p" ``` haftmann@62499 ` 454` ``` by (blast intro: is_prime_associated) ``` haftmann@62499 ` 455` ``` with \normalize p = p\ \normalize q = q\ \p \ q\ show False ``` haftmann@62499 ` 456` ``` by simp ``` haftmann@62499 ` 457` ``` qed ``` haftmann@62499 ` 458` ``` with \is_prime q\ show "\ q dvd p ^ n" ``` haftmann@62499 ` 459` ``` by (simp add: prime_dvd_power_iff) ``` haftmann@62499 ` 460` ``` qed ``` haftmann@62499 ` 461` ``` qed ``` haftmann@62499 ` 462` ``` qed ``` haftmann@62499 ` 463` ``` then show ?thesis by auto ``` haftmann@62499 ` 464` ``` qed ``` haftmann@62499 ` 465` ``` then show ``` haftmann@62499 ` 466` ``` "replicate_mset (Max {n. q ^ n dvd a}) q = replicate_mset (Max {n. q ^ n dvd b}) q" ``` haftmann@62499 ` 467` ``` by simp ``` haftmann@62499 ` 468` ``` qed ``` haftmann@62499 ` 469` ``` def Q \ "the (factorization b)" ``` haftmann@62499 ` 470` ``` with \b \ 0\ have [simp]: "factorization b = Some Q" ``` haftmann@62499 ` 471` ``` by simp ``` haftmann@62499 ` 472` ``` from \a \ 0\ have "factorization a = ``` haftmann@62499 ` 473` ``` Some (\p\?prime_factors a. replicate_mset (Max {n. p ^ n dvd a}) p)" ``` haftmann@62499 ` 474` ``` by (simp add: factorization_def) ``` haftmann@62499 ` 475` ``` also have "\ = ``` haftmann@62499 ` 476` ``` Some (\p\insert p F. replicate_mset (Max {n. p ^ n dvd a}) p)" ``` haftmann@62499 ` 477` ``` by (simp add: \?prime_factors a = insert p F\) ``` haftmann@62499 ` 478` ``` also have "\ = ``` haftmann@62499 ` 479` ``` Some (replicate_mset n p + (\p\F. replicate_mset (Max {n. p ^ n dvd a}) p))" ``` haftmann@62499 ` 480` ``` using \finite F\ \p \ F\ n_def by simp ``` haftmann@62499 ` 481` ``` also have "\ = ``` haftmann@62499 ` 482` ``` Some (replicate_mset n p + (\p\F. replicate_mset (Max {n. p ^ n dvd b}) p))" ``` haftmann@62499 ` 483` ``` using equiv by simp ``` haftmann@62499 ` 484` ``` also have "\ = Some (replicate_mset n p + the (factorization b))" ``` haftmann@62499 ` 485` ``` using \b \ 0\ by (simp add: factorization_def \?prime_factors a = insert p F\ \?prime_factors b = F\) ``` haftmann@62499 ` 486` ``` finally have fact_a: "factorization a = ``` haftmann@62499 ` 487` ``` Some (replicate_mset n p + Q)" ``` haftmann@62499 ` 488` ``` by simp ``` haftmann@62499 ` 489` ``` moreover have "factorization b = Some Q \ ``` haftmann@62499 ` 490` ``` normalize b = msetprod Q \ ``` haftmann@62499 ` 491` ``` 0 \# Q \ ``` haftmann@62499 ` 492` ``` (\p\#Q. is_prime p \ normalize p = p)" ``` haftmann@62499 ` 493` ``` using \F = ?prime_factors b\ \b \ 0\ by (rule insert.hyps) ``` haftmann@62499 ` 494` ``` ultimately have ``` haftmann@62499 ` 495` ``` norm_a: "normalize a = msetprod (replicate_mset n p + Q)" and ``` haftmann@62499 ` 496` ``` prime_Q: "\p\set_mset Q. is_prime p \ normalize p = p" ``` haftmann@62499 ` 497` ``` by (simp_all add: a normalize_mult normalize_power \normalize p = p\) ``` haftmann@62499 ` 498` ``` show ?case (is "?lhs \ ?rhs") proof ``` haftmann@62499 ` 499` ``` assume ?lhs with fact_a ``` haftmann@62499 ` 500` ``` have "P = replicate_mset n p + Q" by simp ``` haftmann@62499 ` 501` ``` with \n > 0\ \is_prime p\ \normalize p = p\ prime_Q ``` haftmann@62499 ` 502` ``` show ?rhs by (auto simp add: norm_a dest: is_prime_not_zeroI) ``` haftmann@62499 ` 503` ``` next ``` haftmann@62499 ` 504` ``` assume ?rhs ``` haftmann@62499 ` 505` ``` with \n > 0\ \is_prime p\ \normalize p = p\ \n > 0\ prime_Q ``` haftmann@62499 ` 506` ``` have "msetprod P = msetprod (replicate_mset n p + Q)" ``` haftmann@62499 ` 507` ``` and "\p\set_mset P. is_prime p \ normalize p = p" ``` haftmann@62499 ` 508` ``` and "\p\set_mset (replicate_mset n p + Q). is_prime p \ normalize p = p" ``` haftmann@62499 ` 509` ``` by (simp_all add: norm_a) ``` haftmann@62499 ` 510` ``` then have "P = replicate_mset n p + Q" ``` haftmann@62499 ` 511` ``` by (simp only: msetprod_eq_iff) ``` haftmann@62499 ` 512` ``` then show ?lhs ``` haftmann@62499 ` 513` ``` by (simp add: fact_a) ``` haftmann@62499 ` 514` ``` qed ``` haftmann@60804 ` 515` ``` qed ``` haftmann@60804 ` 516` ```qed ``` haftmann@62499 ` 517` haftmann@62499 ` 518` ```lemma factorization_cases [case_names 0 factorization]: ``` haftmann@62499 ` 519` ``` assumes "0": "a = 0 \ P" ``` haftmann@62499 ` 520` ``` assumes factorization: "\A. a \ 0 \ factorization a = Some A \ msetprod A = normalize a ``` haftmann@62499 ` 521` ``` \ 0 \# A \ (\p. p \# A \ normalize p = p) \ (\p. p \# A \ is_prime p) \ P" ``` haftmann@62499 ` 522` ``` shows P ``` haftmann@62499 ` 523` ```proof (cases "a = 0") ``` haftmann@62499 ` 524` ``` case True with 0 show P . ``` haftmann@62499 ` 525` ```next ``` haftmann@62499 ` 526` ``` case False ``` haftmann@62499 ` 527` ``` then have "factorization a \ None" by simp ``` haftmann@62499 ` 528` ``` then obtain A where "factorization a = Some A" by blast ``` haftmann@62499 ` 529` ``` moreover from this have "msetprod A = normalize a" ``` haftmann@62499 ` 530` ``` "0 \# A" "\p. p \# A \ normalize p = p" "\p. p \# A \ is_prime p" ``` haftmann@62499 ` 531` ``` by (auto simp add: factorization_eq_Some_iff) ``` haftmann@62499 ` 532` ``` ultimately show P using \a \ 0\ factorization by blast ``` haftmann@62499 ` 533` ```qed ``` haftmann@62499 ` 534` haftmann@62499 ` 535` ```lemma factorizationE: ``` haftmann@62499 ` 536` ``` assumes "a \ 0" ``` haftmann@62499 ` 537` ``` obtains A u where "factorization a = Some A" "normalize a = msetprod A" ``` haftmann@62499 ` 538` ``` "0 \# A" "\p. p \# A \ is_prime p" "\p. p \# A \ normalize p = p" ``` haftmann@62499 ` 539` ``` using assms by (cases a rule: factorization_cases) simp_all ``` haftmann@62499 ` 540` haftmann@62499 ` 541` ```lemma prime_dvd_mset_prod_iff: ``` haftmann@62499 ` 542` ``` assumes "is_prime p" "normalize p = p" "\p. p \# A \ is_prime p" "\p. p \# A \ normalize p = p" ``` haftmann@62499 ` 543` ``` shows "p dvd msetprod A \ p \# A" ``` haftmann@62499 ` 544` ```using assms proof (induct A) ``` haftmann@62499 ` 545` ``` case empty then show ?case by (auto dest: is_prime_not_unit) ``` haftmann@62499 ` 546` ```next ``` haftmann@62499 ` 547` ``` case (add A q) then show ?case ``` haftmann@62499 ` 548` ``` using is_prime_associated [of q p] ``` haftmann@62499 ` 549` ``` by (simp_all add: prime_dvd_mult_iff, safe, simp_all) ``` haftmann@62499 ` 550` ```qed ``` haftmann@62499 ` 551` haftmann@62499 ` 552` ```end ``` haftmann@62499 ` 553` haftmann@62499 ` 554` ```class factorial_semiring_gcd = factorial_semiring + gcd + ``` haftmann@62499 ` 555` ``` assumes gcd_unfold: "gcd a b = ``` haftmann@62499 ` 556` ``` (if a = 0 then normalize b ``` haftmann@62499 ` 557` ``` else if b = 0 then normalize a ``` haftmann@62499 ` 558` ``` else msetprod (the (factorization a) #\ the (factorization b)))" ``` haftmann@62499 ` 559` ``` and lcm_unfold: "lcm a b = ``` haftmann@62499 ` 560` ``` (if a = 0 \ b = 0 then 0 ``` haftmann@62499 ` 561` ``` else msetprod (the (factorization a) #\ the (factorization b)))" ``` haftmann@62499 ` 562` ```begin ``` haftmann@62499 ` 563` haftmann@62499 ` 564` ```subclass semiring_gcd ``` haftmann@62499 ` 565` ```proof ``` haftmann@62499 ` 566` ``` fix a b ``` haftmann@62499 ` 567` ``` have comm: "gcd a b = gcd b a" for a b ``` haftmann@62499 ` 568` ``` by (simp add: gcd_unfold ac_simps) ``` haftmann@62499 ` 569` ``` have "gcd a b dvd a" for a b ``` haftmann@62499 ` 570` ``` proof (cases a rule: factorization_cases) ``` haftmann@62499 ` 571` ``` case 0 then show ?thesis by simp ``` haftmann@62499 ` 572` ``` next ``` haftmann@62499 ` 573` ``` case (factorization A) note fact_A = this ``` haftmann@62499 ` 574` ``` then have non_zero: "\p. p \#A \ p \ 0" ``` haftmann@62499 ` 575` ``` using normalize_0 not_is_prime_zero by blast ``` haftmann@62499 ` 576` ``` show ?thesis ``` haftmann@62499 ` 577` ``` proof (cases b rule: factorization_cases) ``` haftmann@62499 ` 578` ``` case 0 then show ?thesis by (simp add: gcd_unfold) ``` haftmann@62499 ` 579` ``` next ``` haftmann@62499 ` 580` ``` case (factorization B) note fact_B = this ``` haftmann@62499 ` 581` ``` have "msetprod (A #\ B) dvd msetprod A" ``` haftmann@62499 ` 582` ``` using non_zero proof (induct B arbitrary: A) ``` haftmann@62499 ` 583` ``` case empty show ?case by simp ``` haftmann@62499 ` 584` ``` next ``` haftmann@62499 ` 585` ``` case (add B p) show ?case ``` haftmann@62499 ` 586` ``` proof (cases "p \# A") ``` haftmann@62499 ` 587` ``` case True then obtain C where "A = C + {#p#}" ``` haftmann@62499 ` 588` ``` by (metis insert_DiffM2) ``` haftmann@62499 ` 589` ``` moreover with True add have "p \ 0" and "\p. p \# C \ p \ 0" ``` haftmann@62499 ` 590` ``` by auto ``` haftmann@62499 ` 591` ``` ultimately show ?thesis ``` haftmann@62499 ` 592` ``` using True add.hyps [of C] ``` haftmann@62499 ` 593` ``` by (simp add: inter_union_distrib_left [symmetric]) ``` haftmann@62499 ` 594` ``` next ``` haftmann@62499 ` 595` ``` case False with add.prems add.hyps [of A] show ?thesis ``` haftmann@62499 ` 596` ``` by (simp add: inter_add_right1) ``` haftmann@62499 ` 597` ``` qed ``` haftmann@62499 ` 598` ``` qed ``` haftmann@62499 ` 599` ``` with fact_A fact_B show ?thesis by (simp add: gcd_unfold) ``` haftmann@62499 ` 600` ``` qed ``` haftmann@62499 ` 601` ``` qed ``` haftmann@62499 ` 602` ``` then have "gcd a b dvd a" and "gcd b a dvd b" ``` haftmann@62499 ` 603` ``` by simp_all ``` haftmann@62499 ` 604` ``` then show "gcd a b dvd a" and "gcd a b dvd b" ``` haftmann@62499 ` 605` ``` by (simp_all add: comm) ``` haftmann@62499 ` 606` ``` show "c dvd gcd a b" if "c dvd a" and "c dvd b" for c ``` haftmann@62499 ` 607` ``` proof (cases "a = 0 \ b = 0 \ c = 0") ``` haftmann@62499 ` 608` ``` case True with that show ?thesis by (auto simp add: gcd_unfold) ``` haftmann@62499 ` 609` ``` next ``` haftmann@62499 ` 610` ``` case False then have "a \ 0" and "b \ 0" and "c \ 0" ``` haftmann@62499 ` 611` ``` by simp_all ``` haftmann@62499 ` 612` ``` then obtain A B C where fact: ``` haftmann@62499 ` 613` ``` "factorization a = Some A" "factorization b = Some B" "factorization c = Some C" ``` haftmann@62499 ` 614` ``` and norm: "normalize a = msetprod A" "normalize b = msetprod B" "normalize c = msetprod C" ``` haftmann@62499 ` 615` ``` and A: "0 \# A" "\p. p \# A \ normalize p = p" "\p. p \# A \ is_prime p" ``` haftmann@62499 ` 616` ``` and B: "0 \# B" "\p. p \# B \ normalize p = p" "\p. p \# B \ is_prime p" ``` haftmann@62499 ` 617` ``` and C: "0 \# C" "\p. p \# C \ normalize p = p" "\p. p \# C \ is_prime p" ``` haftmann@62499 ` 618` ``` by (blast elim!: factorizationE) ``` haftmann@62499 ` 619` ``` moreover from that have "normalize c dvd normalize a" and "normalize c dvd normalize b" ``` haftmann@62499 ` 620` ``` by simp_all ``` haftmann@62499 ` 621` ``` ultimately have "msetprod C dvd msetprod A" and "msetprod C dvd msetprod B" ``` haftmann@62499 ` 622` ``` by simp_all ``` haftmann@62499 ` 623` ``` with A B C have "msetprod C dvd msetprod (A #\ B)" ``` haftmann@62499 ` 624` ``` proof (induct C arbitrary: A B) ``` haftmann@62499 ` 625` ``` case empty then show ?case by simp ``` haftmann@62499 ` 626` ``` next ``` haftmann@62499 ` 627` ``` case add: (add C p) ``` haftmann@62499 ` 628` ``` from add.prems ``` haftmann@62499 ` 629` ``` have p: "p \ 0" "is_prime p" "normalize p = p" by auto ``` haftmann@62499 ` 630` ``` from add.prems have prems: "msetprod C * p dvd msetprod A" "msetprod C * p dvd msetprod B" ``` haftmann@62499 ` 631` ``` by simp_all ``` haftmann@62499 ` 632` ``` then have "p dvd msetprod A" "p dvd msetprod B" ``` haftmann@62499 ` 633` ``` by (auto dest: dvd_mult_imp_div dvd_mult_right) ``` haftmann@62499 ` 634` ``` with p add.prems have "p \# A" "p \# B" ``` haftmann@62499 ` 635` ``` by (simp_all add: prime_dvd_mset_prod_iff) ``` haftmann@62499 ` 636` ``` then obtain A' B' where ABp: "A = {#p#} + A'" "B = {#p#} + B'" ``` haftmann@62499 ` 637` ``` by (auto dest!: multi_member_split simp add: ac_simps) ``` haftmann@62499 ` 638` ``` with add.prems prems p have "msetprod C dvd msetprod (A' #\ B')" ``` haftmann@62499 ` 639` ``` by (auto intro: add.hyps simp add: ac_simps) ``` haftmann@62499 ` 640` ``` with p have "msetprod ({#p#} + C) dvd msetprod (({#p#} + A') #\ ({#p#} + B'))" ``` haftmann@62499 ` 641` ``` by (simp add: inter_union_distrib_right [symmetric]) ``` haftmann@62499 ` 642` ``` then show ?case by (simp add: ABp ac_simps) ``` haftmann@62499 ` 643` ``` qed ``` haftmann@62499 ` 644` ``` with \a \ 0\ \b \ 0\ that fact have "normalize c dvd gcd a b" ``` haftmann@62499 ` 645` ``` by (simp add: norm [symmetric] gcd_unfold fact) ``` haftmann@62499 ` 646` ``` then show ?thesis by simp ``` haftmann@62499 ` 647` ``` qed ``` haftmann@62499 ` 648` ``` show "normalize (gcd a b) = gcd a b" ``` haftmann@62499 ` 649` ``` apply (simp add: gcd_unfold) ``` haftmann@62499 ` 650` ``` apply safe ``` haftmann@62499 ` 651` ``` apply (rule normalized_msetprodI) ``` haftmann@62499 ` 652` ``` apply (auto elim: factorizationE) ``` haftmann@62499 ` 653` ``` done ``` haftmann@62499 ` 654` ``` show "lcm a b = normalize (a * b) div gcd a b" ``` haftmann@62499 ` 655` ``` by (auto elim!: factorizationE simp add: gcd_unfold lcm_unfold normalize_mult ``` haftmann@62499 ` 656` ``` union_diff_inter_eq_sup [symmetric] msetprod_diff inter_subset_eq_union) ``` haftmann@62499 ` 657` ```qed ``` haftmann@62499 ` 658` haftmann@60804 ` 659` ```end ``` haftmann@60804 ` 660` haftmann@60804 ` 661` ```instantiation nat :: factorial_semiring ``` haftmann@60804 ` 662` ```begin ``` haftmann@60804 ` 663` haftmann@60804 ` 664` ```definition is_prime_nat :: "nat \ bool" ``` haftmann@60804 ` 665` ```where ``` haftmann@60804 ` 666` ``` "is_prime_nat p \ (1 < p \ (\n. n dvd p \ n = 1 \ n = p))" ``` haftmann@60804 ` 667` haftmann@60804 ` 668` ```lemma is_prime_eq_prime: ``` haftmann@60804 ` 669` ``` "is_prime = prime" ``` haftmann@60804 ` 670` ``` by (simp add: fun_eq_iff prime_def is_prime_nat_def) ``` haftmann@60804 ` 671` haftmann@60804 ` 672` ```instance proof ``` haftmann@60804 ` 673` ``` show "\ is_prime (0::nat)" by (simp add: is_prime_nat_def) ``` haftmann@60804 ` 674` ``` show "\ is_unit p" if "is_prime p" for p :: nat ``` haftmann@60804 ` 675` ``` using that by (simp add: is_prime_nat_def) ``` haftmann@60804 ` 676` ```next ``` haftmann@60804 ` 677` ``` fix p :: nat ``` haftmann@60804 ` 678` ``` assume "p \ 0" and "\ is_unit p" ``` haftmann@60804 ` 679` ``` then have "p > 1" by simp ``` haftmann@60804 ` 680` ``` assume P: "\n. n dvd p \ \ is_unit n \ p dvd n" ``` haftmann@60804 ` 681` ``` have "n = 1" if "n dvd p" "n \ p" for n ``` haftmann@60804 ` 682` ``` proof (rule ccontr) ``` haftmann@60804 ` 683` ``` assume "n \ 1" ``` haftmann@60804 ` 684` ``` with that P have "p dvd n" by auto ``` haftmann@60804 ` 685` ``` with \n dvd p\ have "n = p" by (rule dvd_antisym) ``` haftmann@60804 ` 686` ``` with that show False by simp ``` haftmann@60804 ` 687` ``` qed ``` haftmann@60804 ` 688` ``` with \p > 1\ show "is_prime p" by (auto simp add: is_prime_nat_def) ``` haftmann@60804 ` 689` ```next ``` haftmann@60804 ` 690` ``` fix p m n :: nat ``` haftmann@60804 ` 691` ``` assume "is_prime p" ``` haftmann@60804 ` 692` ``` then have "prime p" by (simp add: is_prime_eq_prime) ``` haftmann@60804 ` 693` ``` moreover assume "p dvd m * n" ``` haftmann@60804 ` 694` ``` ultimately show "p dvd m \ p dvd n" ``` haftmann@60804 ` 695` ``` by (rule prime_dvd_mult_nat) ``` haftmann@60804 ` 696` ```next ``` haftmann@60804 ` 697` ``` fix n :: nat ``` haftmann@60804 ` 698` ``` show "is_unit n" if "\m. m dvd n \ \ is_prime m" ``` haftmann@60804 ` 699` ``` using that prime_factor_nat by (auto simp add: is_prime_eq_prime) ``` haftmann@60804 ` 700` ```qed simp ``` haftmann@60804 ` 701` haftmann@60804 ` 702` ```end ``` haftmann@60804 ` 703` haftmann@60804 ` 704` ```instantiation int :: factorial_semiring ``` haftmann@60804 ` 705` ```begin ``` haftmann@60804 ` 706` haftmann@60804 ` 707` ```definition is_prime_int :: "int \ bool" ``` haftmann@60804 ` 708` ```where ``` haftmann@60804 ` 709` ``` "is_prime_int p \ is_prime (nat \p\)" ``` haftmann@60804 ` 710` haftmann@60804 ` 711` ```lemma is_prime_int_iff [simp]: ``` haftmann@60804 ` 712` ``` "is_prime (int n) \ is_prime n" ``` haftmann@60804 ` 713` ``` by (simp add: is_prime_int_def) ``` haftmann@60804 ` 714` haftmann@60804 ` 715` ```lemma is_prime_nat_abs_iff [simp]: ``` haftmann@60804 ` 716` ``` "is_prime (nat \k\) \ is_prime k" ``` haftmann@60804 ` 717` ``` by (simp add: is_prime_int_def) ``` haftmann@60804 ` 718` haftmann@60804 ` 719` ```instance proof ``` haftmann@60804 ` 720` ``` show "\ is_prime (0::int)" by (simp add: is_prime_int_def) ``` haftmann@60804 ` 721` ``` show "\ is_unit p" if "is_prime p" for p :: int ``` haftmann@60804 ` 722` ``` using that is_prime_not_unit [of "nat \p\"] by simp ``` haftmann@60804 ` 723` ```next ``` haftmann@60804 ` 724` ``` fix p :: int ``` haftmann@60804 ` 725` ``` assume P: "\k. k dvd p \ \ is_unit k \ p dvd k" ``` haftmann@60804 ` 726` ``` have "nat \p\ dvd n" if "n dvd nat \p\" and "n \ Suc 0" for n :: nat ``` haftmann@60804 ` 727` ``` proof - ``` haftmann@60804 ` 728` ``` from that have "int n dvd p" by (simp add: int_dvd_iff) ``` haftmann@60804 ` 729` ``` moreover from that have "\ is_unit (int n)" by simp ``` haftmann@60804 ` 730` ``` ultimately have "p dvd int n" by (rule P) ``` haftmann@60804 ` 731` ``` with that have "p dvd int n" by auto ``` haftmann@60804 ` 732` ``` then show ?thesis by (simp add: dvd_int_iff) ``` haftmann@60804 ` 733` ``` qed ``` haftmann@60804 ` 734` ``` moreover assume "p \ 0" and "\ is_unit p" ``` haftmann@60804 ` 735` ``` ultimately have "is_prime (nat \p\)" by (intro is_primeI) auto ``` haftmann@60804 ` 736` ``` then show "is_prime p" by simp ``` haftmann@60804 ` 737` ```next ``` haftmann@60804 ` 738` ``` fix p k l :: int ``` haftmann@60804 ` 739` ``` assume "is_prime p" ``` haftmann@60804 ` 740` ``` then have *: "is_prime (nat \p\)" by simp ``` haftmann@60804 ` 741` ``` assume "p dvd k * l" ``` haftmann@60804 ` 742` ``` then have "nat \p\ dvd nat \k * l\" ``` haftmann@62348 ` 743` ``` by (simp add: dvd_int_unfold_dvd_nat) ``` haftmann@60804 ` 744` ``` then have "nat \p\ dvd nat \k\ * nat \l\" ``` haftmann@60804 ` 745` ``` by (simp add: abs_mult nat_mult_distrib) ``` haftmann@60804 ` 746` ``` with * have "nat \p\ dvd nat \k\ \ nat \p\ dvd nat \l\" ``` haftmann@60804 ` 747` ``` using is_primeD [of "nat \p\"] by auto ``` haftmann@60804 ` 748` ``` then show "p dvd k \ p dvd l" ``` haftmann@62348 ` 749` ``` by (simp add: dvd_int_unfold_dvd_nat) ``` haftmann@60804 ` 750` ```next ``` haftmann@60804 ` 751` ``` fix k :: int ``` haftmann@60804 ` 752` ``` assume P: "\l. l dvd k \ \ is_prime l" ``` haftmann@60804 ` 753` ``` have "is_unit (nat \k\)" ``` haftmann@60804 ` 754` ``` proof (rule no_prime_divisorsI) ``` haftmann@60804 ` 755` ``` fix m ``` haftmann@60804 ` 756` ``` assume "m dvd nat \k\" ``` haftmann@60804 ` 757` ``` then have "int m dvd k" by (simp add: int_dvd_iff) ``` haftmann@60804 ` 758` ``` then have "\ is_prime (int m)" by (rule P) ``` haftmann@60804 ` 759` ``` then show "\ is_prime m" by simp ``` haftmann@60804 ` 760` ``` qed ``` haftmann@60804 ` 761` ``` then show "is_unit k" by simp ``` haftmann@60804 ` 762` ```qed simp ``` haftmann@60804 ` 763` haftmann@60804 ` 764` ```end ``` haftmann@60804 ` 765` haftmann@60804 ` 766` ```end ```