src/HOL/Algebra/Divisibility.thy
 author paulson Wed Jun 06 14:25:53 2018 +0100 (12 months ago) changeset 68399 0b71d08528f0 parent 68004 a8a20be7053a child 68470 7ddcce75c3ee permissions -rw-r--r--
resolution of name clashes in Algebra
 wenzelm@41959 ` 1` ```(* Title: HOL/Algebra/Divisibility.thy ``` wenzelm@41959 ` 2` ``` Author: Clemens Ballarin ``` wenzelm@41959 ` 3` ``` Author: Stephan Hohe ``` ballarin@27701 ` 4` ```*) ``` ballarin@27701 ` 5` wenzelm@61382 ` 6` ```section \Divisibility in monoids and rings\ ``` wenzelm@41959 ` 7` ballarin@27701 ` 8` ```theory Divisibility ``` ballarin@66579 ` 9` ``` imports "HOL-Library.Permutation" Coset Group ``` ballarin@27701 ` 10` ```begin ``` ballarin@27701 ` 11` wenzelm@61382 ` 12` ```section \Factorial Monoids\ ``` wenzelm@61382 ` 13` wenzelm@61382 ` 14` ```subsection \Monoids with Cancellation Law\ ``` ballarin@27701 ` 15` ballarin@27701 ` 16` ```locale monoid_cancel = monoid + ``` wenzelm@63832 ` 17` ``` assumes l_cancel: "\c \ a = c \ b; a \ carrier G; b \ carrier G; c \ carrier G\ \ a = b" ``` wenzelm@63832 ` 18` ``` and r_cancel: "\a \ c = b \ c; a \ carrier G; b \ carrier G; c \ carrier G\ \ a = b" ``` ballarin@27701 ` 19` ballarin@27701 ` 20` ```lemma (in monoid) monoid_cancelI: ``` wenzelm@63832 ` 21` ``` assumes l_cancel: "\a b c. \c \ a = c \ b; a \ carrier G; b \ carrier G; c \ carrier G\ \ a = b" ``` wenzelm@63832 ` 22` ``` and r_cancel: "\a b c. \a \ c = b \ c; a \ carrier G; b \ carrier G; c \ carrier G\ \ a = b" ``` ballarin@27701 ` 23` ``` shows "monoid_cancel G" ``` wenzelm@61169 ` 24` ``` by standard fact+ ``` ballarin@27701 ` 25` wenzelm@63832 ` 26` ```lemma (in monoid_cancel) is_monoid_cancel: "monoid_cancel G" .. ``` ballarin@27701 ` 27` ballarin@29237 ` 28` ```sublocale group \ monoid_cancel ``` wenzelm@61169 ` 29` ``` by standard simp_all ``` ballarin@27701 ` 30` ballarin@27701 ` 31` ballarin@27701 ` 32` ```locale comm_monoid_cancel = monoid_cancel + comm_monoid ``` ballarin@27701 ` 33` ballarin@27701 ` 34` ```lemma comm_monoid_cancelI: ``` ballarin@28599 ` 35` ``` fixes G (structure) ``` ballarin@28599 ` 36` ``` assumes "comm_monoid G" ``` wenzelm@63832 ` 37` ``` assumes cancel: "\a b c. \a \ c = b \ c; a \ carrier G; b \ carrier G; c \ carrier G\ \ a = b" ``` ballarin@27701 ` 38` ``` shows "comm_monoid_cancel G" ``` ballarin@28599 ` 39` ```proof - ``` ballarin@29237 ` 40` ``` interpret comm_monoid G by fact ``` ballarin@28599 ` 41` ``` show "comm_monoid_cancel G" ``` paulson@36278 ` 42` ``` by unfold_locales (metis assms(2) m_ac(2))+ ``` ballarin@28599 ` 43` ```qed ``` ballarin@27701 ` 44` wenzelm@63832 ` 45` ```lemma (in comm_monoid_cancel) is_comm_monoid_cancel: "comm_monoid_cancel G" ``` haftmann@28823 ` 46` ``` by intro_locales ``` ballarin@27701 ` 47` wenzelm@63832 ` 48` ```sublocale comm_group \ comm_monoid_cancel .. ``` ballarin@27701 ` 49` ballarin@27701 ` 50` wenzelm@61382 ` 51` ```subsection \Products of Units in Monoids\ ``` ballarin@27701 ` 52` ballarin@27701 ` 53` ```lemma (in monoid) prod_unit_l: ``` wenzelm@63832 ` 54` ``` assumes abunit[simp]: "a \ b \ Units G" ``` wenzelm@63832 ` 55` ``` and aunit[simp]: "a \ Units G" ``` ballarin@27701 ` 56` ``` and carr[simp]: "a \ carrier G" "b \ carrier G" ``` ballarin@27701 ` 57` ``` shows "b \ Units G" ``` ballarin@27701 ` 58` ```proof - ``` ballarin@27701 ` 59` ``` have c: "inv (a \ b) \ a \ carrier G" by simp ``` ballarin@27701 ` 60` wenzelm@63832 ` 61` ``` have "(inv (a \ b) \ a) \ b = inv (a \ b) \ (a \ b)" ``` wenzelm@63832 ` 62` ``` by (simp add: m_assoc) ``` wenzelm@57865 ` 63` ``` also have "\ = \" by simp ``` ballarin@27701 ` 64` ``` finally have li: "(inv (a \ b) \ a) \ b = \" . ``` ballarin@27701 ` 65` ballarin@27701 ` 66` ``` have "\ = inv a \ a" by (simp add: Units_l_inv[symmetric]) ``` ballarin@27701 ` 67` ``` also have "\ = inv a \ \ \ a" by simp ``` ballarin@27701 ` 68` ``` also have "\ = inv a \ ((a \ b) \ inv (a \ b)) \ a" ``` wenzelm@63832 ` 69` ``` by (simp add: Units_r_inv[OF abunit, symmetric] del: Units_r_inv) ``` ballarin@27701 ` 70` ``` also have "\ = ((inv a \ a) \ b) \ inv (a \ b) \ a" ``` ballarin@27701 ` 71` ``` by (simp add: m_assoc del: Units_l_inv) ``` wenzelm@57865 ` 72` ``` also have "\ = b \ inv (a \ b) \ a" by simp ``` ballarin@27701 ` 73` ``` also have "\ = b \ (inv (a \ b) \ a)" by (simp add: m_assoc) ``` ballarin@27701 ` 74` ``` finally have ri: "b \ (inv (a \ b) \ a) = \ " by simp ``` ballarin@27701 ` 75` wenzelm@63832 ` 76` ``` from c li ri show "b \ Units G" by (auto simp: Units_def) ``` ballarin@27701 ` 77` ```qed ``` ballarin@27701 ` 78` ballarin@27701 ` 79` ```lemma (in monoid) prod_unit_r: ``` wenzelm@63832 ` 80` ``` assumes abunit[simp]: "a \ b \ Units G" ``` wenzelm@63832 ` 81` ``` and bunit[simp]: "b \ Units G" ``` ballarin@27701 ` 82` ``` and carr[simp]: "a \ carrier G" "b \ carrier G" ``` ballarin@27701 ` 83` ``` shows "a \ Units G" ``` ballarin@27701 ` 84` ```proof - ``` ballarin@27701 ` 85` ``` have c: "b \ inv (a \ b) \ carrier G" by simp ``` ballarin@27701 ` 86` ballarin@27701 ` 87` ``` have "a \ (b \ inv (a \ b)) = (a \ b) \ inv (a \ b)" ``` ballarin@27701 ` 88` ``` by (simp add: m_assoc del: Units_r_inv) ``` ballarin@27701 ` 89` ``` also have "\ = \" by simp ``` ballarin@27701 ` 90` ``` finally have li: "a \ (b \ inv (a \ b)) = \" . ``` ballarin@27701 ` 91` ballarin@27701 ` 92` ``` have "\ = b \ inv b" by (simp add: Units_r_inv[symmetric]) ``` ballarin@27701 ` 93` ``` also have "\ = b \ \ \ inv b" by simp ``` wenzelm@63832 ` 94` ``` also have "\ = b \ (inv (a \ b) \ (a \ b)) \ inv b" ``` wenzelm@63832 ` 95` ``` by (simp add: Units_l_inv[OF abunit, symmetric] del: Units_l_inv) ``` ballarin@27701 ` 96` ``` also have "\ = (b \ inv (a \ b) \ a) \ (b \ inv b)" ``` ballarin@27701 ` 97` ``` by (simp add: m_assoc del: Units_l_inv) ``` ballarin@27701 ` 98` ``` also have "\ = b \ inv (a \ b) \ a" by simp ``` ballarin@27701 ` 99` ``` finally have ri: "(b \ inv (a \ b)) \ a = \ " by simp ``` ballarin@27701 ` 100` wenzelm@63832 ` 101` ``` from c li ri show "a \ Units G" by (auto simp: Units_def) ``` ballarin@27701 ` 102` ```qed ``` ballarin@27701 ` 103` ballarin@27701 ` 104` ```lemma (in comm_monoid) unit_factor: ``` ballarin@27701 ` 105` ``` assumes abunit: "a \ b \ Units G" ``` ballarin@27701 ` 106` ``` and [simp]: "a \ carrier G" "b \ carrier G" ``` ballarin@27701 ` 107` ``` shows "a \ Units G" ``` wenzelm@63832 ` 108` ``` using abunit[simplified Units_def] ``` ballarin@27701 ` 109` ```proof clarsimp ``` ballarin@27701 ` 110` ``` fix i ``` ballarin@27701 ` 111` ``` assume [simp]: "i \ carrier G" ``` ballarin@27701 ` 112` ballarin@27701 ` 113` ``` have carr': "b \ i \ carrier G" by simp ``` ballarin@27701 ` 114` ballarin@27701 ` 115` ``` have "(b \ i) \ a = (i \ b) \ a" by (simp add: m_comm) ``` ballarin@27701 ` 116` ``` also have "\ = i \ (b \ a)" by (simp add: m_assoc) ``` ballarin@27701 ` 117` ``` also have "\ = i \ (a \ b)" by (simp add: m_comm) ``` wenzelm@63832 ` 118` ``` also assume "i \ (a \ b) = \" ``` ballarin@27701 ` 119` ``` finally have li': "(b \ i) \ a = \" . ``` ballarin@27701 ` 120` ballarin@27701 ` 121` ``` have "a \ (b \ i) = a \ b \ i" by (simp add: m_assoc) ``` wenzelm@63832 ` 122` ``` also assume "a \ b \ i = \" ``` ballarin@27701 ` 123` ``` finally have ri': "a \ (b \ i) = \" . ``` ballarin@27701 ` 124` ballarin@27701 ` 125` ``` from carr' li' ri' ``` wenzelm@63832 ` 126` ``` show "a \ Units G" by (simp add: Units_def, fast) ``` ballarin@27701 ` 127` ```qed ``` ballarin@27701 ` 128` wenzelm@35849 ` 129` wenzelm@61382 ` 130` ```subsection \Divisibility and Association\ ``` wenzelm@61382 ` 131` wenzelm@61382 ` 132` ```subsubsection \Function definitions\ ``` ballarin@27701 ` 133` wenzelm@63832 ` 134` ```definition factor :: "[_, 'a, 'a] \ bool" (infix "divides\" 65) ``` wenzelm@35848 ` 135` ``` where "a divides\<^bsub>G\<^esub> b \ (\c\carrier G. b = a \\<^bsub>G\<^esub> c)" ``` wenzelm@35847 ` 136` wenzelm@63832 ` 137` ```definition associated :: "[_, 'a, 'a] \ bool" (infix "\\" 55) ``` wenzelm@35848 ` 138` ``` where "a \\<^bsub>G\<^esub> b \ a divides\<^bsub>G\<^esub> b \ b divides\<^bsub>G\<^esub> a" ``` ballarin@27701 ` 139` nipkow@67399 ` 140` ```abbreviation "division_rel G \ \carrier = carrier G, eq = (\\<^bsub>G\<^esub>), le = (divides\<^bsub>G\<^esub>)\" ``` wenzelm@63832 ` 141` wenzelm@63832 ` 142` ```definition properfactor :: "[_, 'a, 'a] \ bool" ``` wenzelm@35848 ` 143` ``` where "properfactor G a b \ a divides\<^bsub>G\<^esub> b \ \(b divides\<^bsub>G\<^esub> a)" ``` wenzelm@35847 ` 144` wenzelm@63832 ` 145` ```definition irreducible :: "[_, 'a] \ bool" ``` wenzelm@35848 ` 146` ``` where "irreducible G a \ a \ Units G \ (\b\carrier G. properfactor G b a \ b \ Units G)" ``` wenzelm@35847 ` 147` wenzelm@63832 ` 148` ```definition prime :: "[_, 'a] \ bool" ``` wenzelm@63832 ` 149` ``` where "prime G p \ ``` wenzelm@63832 ` 150` ``` p \ Units G \ ``` wenzelm@35847 ` 151` ``` (\a\carrier G. \b\carrier G. p divides\<^bsub>G\<^esub> (a \\<^bsub>G\<^esub> b) \ p divides\<^bsub>G\<^esub> a \ p divides\<^bsub>G\<^esub> b)" ``` ballarin@27701 ` 152` ballarin@27701 ` 153` wenzelm@61382 ` 154` ```subsubsection \Divisibility\ ``` ballarin@27701 ` 155` ballarin@27701 ` 156` ```lemma dividesI: ``` ballarin@27701 ` 157` ``` fixes G (structure) ``` ballarin@27701 ` 158` ``` assumes carr: "c \ carrier G" ``` ballarin@27701 ` 159` ``` and p: "b = a \ c" ``` ballarin@27701 ` 160` ``` shows "a divides b" ``` wenzelm@63832 ` 161` ``` unfolding factor_def using assms by fast ``` ballarin@27701 ` 162` ballarin@27701 ` 163` ```lemma dividesI' [intro]: ``` wenzelm@63832 ` 164` ``` fixes G (structure) ``` ballarin@27701 ` 165` ``` assumes p: "b = a \ c" ``` ballarin@27701 ` 166` ``` and carr: "c \ carrier G" ``` ballarin@27701 ` 167` ``` shows "a divides b" ``` wenzelm@63832 ` 168` ``` using assms by (fast intro: dividesI) ``` ballarin@27701 ` 169` ballarin@27701 ` 170` ```lemma dividesD: ``` ballarin@27701 ` 171` ``` fixes G (structure) ``` ballarin@27701 ` 172` ``` assumes "a divides b" ``` ballarin@27701 ` 173` ``` shows "\c\carrier G. b = a \ c" ``` wenzelm@63832 ` 174` ``` using assms unfolding factor_def by fast ``` ballarin@27701 ` 175` ballarin@27701 ` 176` ```lemma dividesE [elim]: ``` ballarin@27701 ` 177` ``` fixes G (structure) ``` ballarin@27701 ` 178` ``` assumes d: "a divides b" ``` ballarin@27701 ` 179` ``` and elim: "\c. \b = a \ c; c \ carrier G\ \ P" ``` ballarin@27701 ` 180` ``` shows "P" ``` ballarin@27701 ` 181` ```proof - ``` wenzelm@63846 ` 182` ``` from dividesD[OF d] obtain c where "c \ carrier G" and "b = a \ c" by auto ``` wenzelm@63832 ` 183` ``` then show P by (elim elim) ``` ballarin@27701 ` 184` ```qed ``` ballarin@27701 ` 185` ballarin@27701 ` 186` ```lemma (in monoid) divides_refl[simp, intro!]: ``` ballarin@27701 ` 187` ``` assumes carr: "a \ carrier G" ``` ballarin@27701 ` 188` ``` shows "a divides a" ``` wenzelm@63832 ` 189` ``` by (intro dividesI[of "\"]) (simp_all add: carr) ``` ballarin@27701 ` 190` ballarin@27701 ` 191` ```lemma (in monoid) divides_trans [trans]: ``` ballarin@27701 ` 192` ``` assumes dvds: "a divides b" "b divides c" ``` ballarin@27701 ` 193` ``` and acarr: "a \ carrier G" ``` ballarin@27701 ` 194` ``` shows "a divides c" ``` wenzelm@63832 ` 195` ``` using dvds[THEN dividesD] by (blast intro: dividesI m_assoc acarr) ``` ballarin@27701 ` 196` ballarin@27701 ` 197` ```lemma (in monoid) divides_mult_lI [intro]: ``` ballarin@27701 ` 198` ``` assumes ab: "a divides b" ``` ballarin@27701 ` 199` ``` and carr: "a \ carrier G" "b \ carrier G" "c \ carrier G" ``` ballarin@27701 ` 200` ``` shows "(c \ a) divides (c \ b)" ``` wenzelm@63832 ` 201` ``` using ab ``` wenzelm@63832 ` 202` ``` apply (elim dividesE) ``` wenzelm@63832 ` 203` ``` apply (simp add: m_assoc[symmetric] carr) ``` wenzelm@63832 ` 204` ``` apply (fast intro: dividesI) ``` wenzelm@63832 ` 205` ``` done ``` ballarin@27701 ` 206` ballarin@27701 ` 207` ```lemma (in monoid_cancel) divides_mult_l [simp]: ``` ballarin@27701 ` 208` ``` assumes carr: "a \ carrier G" "b \ carrier G" "c \ carrier G" ``` ballarin@27701 ` 209` ``` shows "(c \ a) divides (c \ b) = a divides b" ``` wenzelm@63832 ` 210` ``` apply safe ``` wenzelm@63832 ` 211` ``` apply (elim dividesE, intro dividesI, assumption) ``` wenzelm@63832 ` 212` ``` apply (rule l_cancel[of c]) ``` wenzelm@63832 ` 213` ``` apply (simp add: m_assoc carr)+ ``` wenzelm@63832 ` 214` ``` apply (fast intro: carr) ``` wenzelm@63832 ` 215` ``` done ``` ballarin@27701 ` 216` ballarin@27701 ` 217` ```lemma (in comm_monoid) divides_mult_rI [intro]: ``` ballarin@27701 ` 218` ``` assumes ab: "a divides b" ``` ballarin@27701 ` 219` ``` and carr: "a \ carrier G" "b \ carrier G" "c \ carrier G" ``` ballarin@27701 ` 220` ``` shows "(a \ c) divides (b \ c)" ``` wenzelm@63832 ` 221` ``` using carr ab ``` wenzelm@63832 ` 222` ``` apply (simp add: m_comm[of a c] m_comm[of b c]) ``` wenzelm@63832 ` 223` ``` apply (rule divides_mult_lI, assumption+) ``` wenzelm@63832 ` 224` ``` done ``` ballarin@27701 ` 225` ballarin@27701 ` 226` ```lemma (in comm_monoid_cancel) divides_mult_r [simp]: ``` ballarin@27701 ` 227` ``` assumes carr: "a \ carrier G" "b \ carrier G" "c \ carrier G" ``` ballarin@27701 ` 228` ``` shows "(a \ c) divides (b \ c) = a divides b" ``` wenzelm@63832 ` 229` ``` using carr by (simp add: m_comm[of a c] m_comm[of b c]) ``` ballarin@27701 ` 230` ballarin@27701 ` 231` ```lemma (in monoid) divides_prod_r: ``` ballarin@27701 ` 232` ``` assumes ab: "a divides b" ``` ballarin@27701 ` 233` ``` and carr: "a \ carrier G" "b \ carrier G" "c \ carrier G" ``` ballarin@27701 ` 234` ``` shows "a divides (b \ c)" ``` wenzelm@63832 ` 235` ``` using ab carr by (fast intro: m_assoc) ``` ballarin@27701 ` 236` ballarin@27701 ` 237` ```lemma (in comm_monoid) divides_prod_l: ``` ballarin@27701 ` 238` ``` assumes carr[intro]: "a \ carrier G" "b \ carrier G" "c \ carrier G" ``` ballarin@27701 ` 239` ``` and ab: "a divides b" ``` ballarin@27701 ` 240` ``` shows "a divides (c \ b)" ``` wenzelm@63832 ` 241` ``` using ab carr ``` wenzelm@63832 ` 242` ``` apply (simp add: m_comm[of c b]) ``` wenzelm@63832 ` 243` ``` apply (fast intro: divides_prod_r) ``` wenzelm@63832 ` 244` ``` done ``` ballarin@27701 ` 245` ballarin@27701 ` 246` ```lemma (in monoid) unit_divides: ``` ballarin@27701 ` 247` ``` assumes uunit: "u \ Units G" ``` wenzelm@63832 ` 248` ``` and acarr: "a \ carrier G" ``` ballarin@27701 ` 249` ``` shows "u divides a" ``` ballarin@27701 ` 250` ```proof (intro dividesI[of "(inv u) \ a"], fast intro: uunit acarr) ``` wenzelm@63832 ` 251` ``` from uunit acarr have xcarr: "inv u \ a \ carrier G" by fast ``` wenzelm@63832 ` 252` ``` from uunit acarr have "u \ (inv u \ a) = (u \ inv u) \ a" ``` wenzelm@63832 ` 253` ``` by (fast intro: m_assoc[symmetric]) ``` ballarin@27701 ` 254` ``` also have "\ = \ \ a" by (simp add: Units_r_inv[OF uunit]) ``` wenzelm@63832 ` 255` ``` also from acarr have "\ = a" by simp ``` wenzelm@63832 ` 256` ``` finally show "a = u \ (inv u \ a)" .. ``` ballarin@27701 ` 257` ```qed ``` ballarin@27701 ` 258` ballarin@27701 ` 259` ```lemma (in comm_monoid) divides_unit: ``` ballarin@27701 ` 260` ``` assumes udvd: "a divides u" ``` wenzelm@63832 ` 261` ``` and carr: "a \ carrier G" "u \ Units G" ``` ballarin@27701 ` 262` ``` shows "a \ Units G" ``` wenzelm@63832 ` 263` ``` using udvd carr by (blast intro: unit_factor) ``` ballarin@27701 ` 264` ballarin@27701 ` 265` ```lemma (in comm_monoid) Unit_eq_dividesone: ``` ballarin@27701 ` 266` ``` assumes ucarr: "u \ carrier G" ``` ballarin@27701 ` 267` ``` shows "u \ Units G = u divides \" ``` wenzelm@63832 ` 268` ``` using ucarr by (fast dest: divides_unit intro: unit_divides) ``` ballarin@27701 ` 269` ballarin@27701 ` 270` wenzelm@61382 ` 271` ```subsubsection \Association\ ``` ballarin@27701 ` 272` ballarin@27701 ` 273` ```lemma associatedI: ``` ballarin@27701 ` 274` ``` fixes G (structure) ``` ballarin@27701 ` 275` ``` assumes "a divides b" "b divides a" ``` ballarin@27701 ` 276` ``` shows "a \ b" ``` wenzelm@63832 ` 277` ``` using assms by (simp add: associated_def) ``` ballarin@27701 ` 278` ballarin@27701 ` 279` ```lemma (in monoid) associatedI2: ``` ballarin@27701 ` 280` ``` assumes uunit[simp]: "u \ Units G" ``` ballarin@27701 ` 281` ``` and a: "a = b \ u" ``` ballarin@27701 ` 282` ``` and bcarr[simp]: "b \ carrier G" ``` ballarin@27701 ` 283` ``` shows "a \ b" ``` wenzelm@63832 ` 284` ``` using uunit bcarr ``` wenzelm@63832 ` 285` ``` unfolding a ``` wenzelm@63832 ` 286` ``` apply (intro associatedI) ``` wenzelm@63832 ` 287` ``` apply (rule dividesI[of "inv u"], simp) ``` wenzelm@63832 ` 288` ``` apply (simp add: m_assoc Units_closed) ``` wenzelm@63832 ` 289` ``` apply fast ``` wenzelm@63832 ` 290` ``` done ``` ballarin@27701 ` 291` ballarin@27701 ` 292` ```lemma (in monoid) associatedI2': ``` wenzelm@63832 ` 293` ``` assumes "a = b \ u" ``` wenzelm@63832 ` 294` ``` and "u \ Units G" ``` wenzelm@63832 ` 295` ``` and "b \ carrier G" ``` ballarin@27701 ` 296` ``` shows "a \ b" ``` wenzelm@63832 ` 297` ``` using assms by (intro associatedI2) ``` ballarin@27701 ` 298` ballarin@27701 ` 299` ```lemma associatedD: ``` ballarin@27701 ` 300` ``` fixes G (structure) ``` ballarin@27701 ` 301` ``` assumes "a \ b" ``` ballarin@27701 ` 302` ``` shows "a divides b" ``` wenzelm@63832 ` 303` ``` using assms by (simp add: associated_def) ``` ballarin@27701 ` 304` ballarin@27701 ` 305` ```lemma (in monoid_cancel) associatedD2: ``` ballarin@27701 ` 306` ``` assumes assoc: "a \ b" ``` ballarin@27701 ` 307` ``` and carr: "a \ carrier G" "b \ carrier G" ``` ballarin@27701 ` 308` ``` shows "\u\Units G. a = b \ u" ``` wenzelm@63832 ` 309` ``` using assoc ``` wenzelm@63832 ` 310` ``` unfolding associated_def ``` ballarin@27701 ` 311` ```proof clarify ``` ballarin@27701 ` 312` ``` assume "b divides a" ``` wenzelm@63832 ` 313` ``` then obtain u where ucarr: "u \ carrier G" and a: "a = b \ u" ``` wenzelm@63846 ` 314` ``` by (rule dividesE) ``` ballarin@27701 ` 315` ballarin@27701 ` 316` ``` assume "a divides b" ``` wenzelm@63832 ` 317` ``` then obtain u' where u'carr: "u' \ carrier G" and b: "b = a \ u'" ``` wenzelm@63846 ` 318` ``` by (rule dividesE) ``` ballarin@27701 ` 319` ``` note carr = carr ucarr u'carr ``` ballarin@27701 ` 320` wenzelm@63832 ` 321` ``` from carr have "a \ \ = a" by simp ``` ballarin@27701 ` 322` ``` also have "\ = b \ u" by (simp add: a) ``` ballarin@27701 ` 323` ``` also have "\ = a \ u' \ u" by (simp add: b) ``` wenzelm@63832 ` 324` ``` also from carr have "\ = a \ (u' \ u)" by (simp add: m_assoc) ``` wenzelm@63832 ` 325` ``` finally have "a \ \ = a \ (u' \ u)" . ``` wenzelm@63832 ` 326` ``` with carr have u1: "\ = u' \ u" by (fast dest: l_cancel) ``` wenzelm@63832 ` 327` wenzelm@63832 ` 328` ``` from carr have "b \ \ = b" by simp ``` ballarin@27701 ` 329` ``` also have "\ = a \ u'" by (simp add: b) ``` ballarin@27701 ` 330` ``` also have "\ = b \ u \ u'" by (simp add: a) ``` wenzelm@63832 ` 331` ``` also from carr have "\ = b \ (u \ u')" by (simp add: m_assoc) ``` wenzelm@63832 ` 332` ``` finally have "b \ \ = b \ (u \ u')" . ``` wenzelm@63832 ` 333` ``` with carr have u2: "\ = u \ u'" by (fast dest: l_cancel) ``` wenzelm@63832 ` 334` wenzelm@63832 ` 335` ``` from u'carr u1[symmetric] u2[symmetric] have "\u'\carrier G. u' \ u = \ \ u \ u' = \" ``` wenzelm@63832 ` 336` ``` by fast ``` wenzelm@63832 ` 337` ``` then have "u \ Units G" ``` wenzelm@63832 ` 338` ``` by (simp add: Units_def ucarr) ``` wenzelm@63832 ` 339` ``` with ucarr a show "\u\Units G. a = b \ u" by fast ``` ballarin@27701 ` 340` ```qed ``` ballarin@27701 ` 341` ballarin@27701 ` 342` ```lemma associatedE: ``` ballarin@27701 ` 343` ``` fixes G (structure) ``` ballarin@27701 ` 344` ``` assumes assoc: "a \ b" ``` ballarin@27701 ` 345` ``` and e: "\a divides b; b divides a\ \ P" ``` ballarin@27701 ` 346` ``` shows "P" ``` ballarin@27701 ` 347` ```proof - ``` wenzelm@63832 ` 348` ``` from assoc have "a divides b" "b divides a" ``` wenzelm@63832 ` 349` ``` by (simp_all add: associated_def) ``` wenzelm@63832 ` 350` ``` then show P by (elim e) ``` ballarin@27701 ` 351` ```qed ``` ballarin@27701 ` 352` ballarin@27701 ` 353` ```lemma (in monoid_cancel) associatedE2: ``` ballarin@27701 ` 354` ``` assumes assoc: "a \ b" ``` ballarin@27701 ` 355` ``` and e: "\u. \a = b \ u; u \ Units G\ \ P" ``` ballarin@27701 ` 356` ``` and carr: "a \ carrier G" "b \ carrier G" ``` ballarin@27701 ` 357` ``` shows "P" ``` ballarin@27701 ` 358` ```proof - ``` wenzelm@63832 ` 359` ``` from assoc and carr have "\u\Units G. a = b \ u" ``` wenzelm@63832 ` 360` ``` by (rule associatedD2) ``` wenzelm@63832 ` 361` ``` then obtain u where "u \ Units G" "a = b \ u" ``` wenzelm@63832 ` 362` ``` by auto ``` wenzelm@63832 ` 363` ``` then show P by (elim e) ``` ballarin@27701 ` 364` ```qed ``` ballarin@27701 ` 365` ballarin@27701 ` 366` ```lemma (in monoid) associated_refl [simp, intro!]: ``` ballarin@27701 ` 367` ``` assumes "a \ carrier G" ``` ballarin@27701 ` 368` ``` shows "a \ a" ``` wenzelm@63832 ` 369` ``` using assms by (fast intro: associatedI) ``` ballarin@27701 ` 370` ballarin@27701 ` 371` ```lemma (in monoid) associated_sym [sym]: ``` ballarin@27701 ` 372` ``` assumes "a \ b" ``` ballarin@27701 ` 373` ``` and "a \ carrier G" "b \ carrier G" ``` ballarin@27701 ` 374` ``` shows "b \ a" ``` wenzelm@63832 ` 375` ``` using assms by (iprover intro: associatedI elim: associatedE) ``` ballarin@27701 ` 376` ballarin@27701 ` 377` ```lemma (in monoid) associated_trans [trans]: ``` ballarin@27701 ` 378` ``` assumes "a \ b" "b \ c" ``` ballarin@27701 ` 379` ``` and "a \ carrier G" "b \ carrier G" "c \ carrier G" ``` ballarin@27701 ` 380` ``` shows "a \ c" ``` wenzelm@63832 ` 381` ``` using assms by (iprover intro: associatedI divides_trans elim: associatedE) ``` wenzelm@63832 ` 382` wenzelm@63832 ` 383` ```lemma (in monoid) division_equiv [intro, simp]: "equivalence (division_rel G)" ``` ballarin@27701 ` 384` ``` apply unfold_locales ``` wenzelm@63832 ` 385` ``` apply simp_all ``` wenzelm@63832 ` 386` ``` apply (metis associated_def) ``` ballarin@27701 ` 387` ``` apply (iprover intro: associated_trans) ``` ballarin@27701 ` 388` ``` done ``` ballarin@27701 ` 389` ballarin@27701 ` 390` wenzelm@61382 ` 391` ```subsubsection \Division and associativity\ ``` ballarin@27701 ` 392` ballarin@27701 ` 393` ```lemma divides_antisym: ``` ballarin@27701 ` 394` ``` fixes G (structure) ``` ballarin@27701 ` 395` ``` assumes "a divides b" "b divides a" ``` ballarin@27701 ` 396` ``` and "a \ carrier G" "b \ carrier G" ``` ballarin@27701 ` 397` ``` shows "a \ b" ``` wenzelm@63832 ` 398` ``` using assms by (fast intro: associatedI) ``` ballarin@27701 ` 399` ballarin@27701 ` 400` ```lemma (in monoid) divides_cong_l [trans]: ``` wenzelm@63832 ` 401` ``` assumes "x \ x'" ``` wenzelm@63832 ` 402` ``` and "x' divides y" ``` wenzelm@63832 ` 403` ``` and [simp]: "x \ carrier G" "x' \ carrier G" "y \ carrier G" ``` ballarin@27701 ` 404` ``` shows "x divides y" ``` ballarin@27701 ` 405` ```proof - ``` wenzelm@63832 ` 406` ``` from assms(1) have "x divides x'" by (simp add: associatedD) ``` wenzelm@63832 ` 407` ``` also note assms(2) ``` wenzelm@63832 ` 408` ``` finally show "x divides y" by simp ``` ballarin@27701 ` 409` ```qed ``` ballarin@27701 ` 410` ballarin@27701 ` 411` ```lemma (in monoid) divides_cong_r [trans]: ``` wenzelm@63832 ` 412` ``` assumes "x divides y" ``` wenzelm@63832 ` 413` ``` and "y \ y'" ``` wenzelm@63832 ` 414` ``` and [simp]: "x \ carrier G" "y \ carrier G" "y' \ carrier G" ``` ballarin@27701 ` 415` ``` shows "x divides y'" ``` ballarin@27701 ` 416` ```proof - ``` wenzelm@63832 ` 417` ``` note assms(1) ``` wenzelm@63832 ` 418` ``` also from assms(2) have "y divides y'" by (simp add: associatedD) ``` wenzelm@63832 ` 419` ``` finally show "x divides y'" by simp ``` ballarin@27701 ` 420` ```qed ``` ballarin@27701 ` 421` ballarin@27713 ` 422` ```lemma (in monoid) division_weak_partial_order [simp, intro!]: ``` ballarin@27713 ` 423` ``` "weak_partial_order (division_rel G)" ``` ballarin@27701 ` 424` ``` apply unfold_locales ``` wenzelm@63832 ` 425` ``` apply simp_all ``` wenzelm@63832 ` 426` ``` apply (simp add: associated_sym) ``` wenzelm@63832 ` 427` ``` apply (blast intro: associated_trans) ``` wenzelm@63832 ` 428` ``` apply (simp add: divides_antisym) ``` wenzelm@63832 ` 429` ``` apply (blast intro: divides_trans) ``` ballarin@27701 ` 430` ``` apply (blast intro: divides_cong_l divides_cong_r associated_sym) ``` ballarin@27701 ` 431` ``` done ``` ballarin@27701 ` 432` wenzelm@63832 ` 433` wenzelm@61382 ` 434` ```subsubsection \Multiplication and associativity\ ``` ballarin@27701 ` 435` ballarin@27701 ` 436` ```lemma (in monoid_cancel) mult_cong_r: ``` ballarin@27701 ` 437` ``` assumes "b \ b'" ``` ballarin@27701 ` 438` ``` and carr: "a \ carrier G" "b \ carrier G" "b' \ carrier G" ``` ballarin@27701 ` 439` ``` shows "a \ b \ a \ b'" ``` wenzelm@63832 ` 440` ``` using assms ``` wenzelm@63832 ` 441` ``` apply (elim associatedE2, intro associatedI2) ``` wenzelm@63832 ` 442` ``` apply (auto intro: m_assoc[symmetric]) ``` wenzelm@63832 ` 443` ``` done ``` ballarin@27701 ` 444` ballarin@27701 ` 445` ```lemma (in comm_monoid_cancel) mult_cong_l: ``` ballarin@27701 ` 446` ``` assumes "a \ a'" ``` ballarin@27701 ` 447` ``` and carr: "a \ carrier G" "a' \ carrier G" "b \ carrier G" ``` ballarin@27701 ` 448` ``` shows "a \ b \ a' \ b" ``` wenzelm@63832 ` 449` ``` using assms ``` wenzelm@63832 ` 450` ``` apply (elim associatedE2, intro associatedI2) ``` wenzelm@63832 ` 451` ``` apply assumption ``` wenzelm@63832 ` 452` ``` apply (simp add: m_assoc Units_closed) ``` wenzelm@63832 ` 453` ``` apply (simp add: m_comm Units_closed) ``` wenzelm@63832 ` 454` ``` apply simp_all ``` wenzelm@63832 ` 455` ``` done ``` ballarin@27701 ` 456` ballarin@27701 ` 457` ```lemma (in monoid_cancel) assoc_l_cancel: ``` ballarin@27701 ` 458` ``` assumes carr: "a \ carrier G" "b \ carrier G" "b' \ carrier G" ``` ballarin@27701 ` 459` ``` and "a \ b \ a \ b'" ``` ballarin@27701 ` 460` ``` shows "b \ b'" ``` wenzelm@63832 ` 461` ``` using assms ``` wenzelm@63832 ` 462` ``` apply (elim associatedE2, intro associatedI2) ``` wenzelm@63832 ` 463` ``` apply assumption ``` wenzelm@63832 ` 464` ``` apply (rule l_cancel[of a]) ``` wenzelm@63832 ` 465` ``` apply (simp add: m_assoc Units_closed) ``` wenzelm@63832 ` 466` ``` apply fast+ ``` wenzelm@63832 ` 467` ``` done ``` ballarin@27701 ` 468` ballarin@27701 ` 469` ```lemma (in comm_monoid_cancel) assoc_r_cancel: ``` ballarin@27701 ` 470` ``` assumes "a \ b \ a' \ b" ``` ballarin@27701 ` 471` ``` and carr: "a \ carrier G" "a' \ carrier G" "b \ carrier G" ``` ballarin@27701 ` 472` ``` shows "a \ a'" ``` wenzelm@63832 ` 473` ``` using assms ``` wenzelm@63832 ` 474` ``` apply (elim associatedE2, intro associatedI2) ``` wenzelm@63832 ` 475` ``` apply assumption ``` wenzelm@63832 ` 476` ``` apply (rule r_cancel[of a b]) ``` wenzelm@63832 ` 477` ``` apply (metis Units_closed assms(3) assms(4) m_ac) ``` wenzelm@63832 ` 478` ``` apply fast+ ``` wenzelm@63832 ` 479` ``` done ``` ballarin@27701 ` 480` ballarin@27701 ` 481` wenzelm@61382 ` 482` ```subsubsection \Units\ ``` ballarin@27701 ` 483` ballarin@27701 ` 484` ```lemma (in monoid_cancel) assoc_unit_l [trans]: ``` wenzelm@63832 ` 485` ``` assumes "a \ b" ``` wenzelm@63832 ` 486` ``` and "b \ Units G" ``` wenzelm@63832 ` 487` ``` and "a \ carrier G" ``` ballarin@27701 ` 488` ``` shows "a \ Units G" ``` wenzelm@63832 ` 489` ``` using assms by (fast elim: associatedE2) ``` ballarin@27701 ` 490` ballarin@27701 ` 491` ```lemma (in monoid_cancel) assoc_unit_r [trans]: ``` wenzelm@63832 ` 492` ``` assumes aunit: "a \ Units G" ``` wenzelm@63832 ` 493` ``` and asc: "a \ b" ``` ballarin@27701 ` 494` ``` and bcarr: "b \ carrier G" ``` ballarin@27701 ` 495` ``` shows "b \ Units G" ``` wenzelm@63832 ` 496` ``` using aunit bcarr associated_sym[OF asc] by (blast intro: assoc_unit_l) ``` ballarin@27701 ` 497` ballarin@27701 ` 498` ```lemma (in comm_monoid) Units_cong: ``` ballarin@27701 ` 499` ``` assumes aunit: "a \ Units G" and asc: "a \ b" ``` ballarin@27701 ` 500` ``` and bcarr: "b \ carrier G" ``` ballarin@27701 ` 501` ``` shows "b \ Units G" ``` wenzelm@63832 ` 502` ``` using assms by (blast intro: divides_unit elim: associatedE) ``` ballarin@27701 ` 503` ballarin@27701 ` 504` ```lemma (in monoid) Units_assoc: ``` ballarin@27701 ` 505` ``` assumes units: "a \ Units G" "b \ Units G" ``` ballarin@27701 ` 506` ``` shows "a \ b" ``` wenzelm@63832 ` 507` ``` using units by (fast intro: associatedI unit_divides) ``` wenzelm@63832 ` 508` wenzelm@63832 ` 509` ```lemma (in monoid) Units_are_ones: "Units G {.=}\<^bsub>(division_rel G)\<^esub> {\}" ``` wenzelm@63832 ` 510` ``` apply (simp add: set_eq_def elem_def, rule, simp_all) ``` ballarin@27701 ` 511` ```proof clarsimp ``` ballarin@27701 ` 512` ``` fix a ``` ballarin@27701 ` 513` ``` assume aunit: "a \ Units G" ``` ballarin@27701 ` 514` ``` show "a \ \" ``` wenzelm@63832 ` 515` ``` apply (rule associatedI) ``` wenzelm@63832 ` 516` ``` apply (fast intro: dividesI[of "inv a"] aunit Units_r_inv[symmetric]) ``` wenzelm@63832 ` 517` ``` apply (fast intro: dividesI[of "a"] l_one[symmetric] Units_closed[OF aunit]) ``` wenzelm@63832 ` 518` ``` done ``` ballarin@27701 ` 519` ```next ``` ballarin@27701 ` 520` ``` have "\ \ Units G" by simp ``` ballarin@27701 ` 521` ``` moreover have "\ \ \" by simp ``` ballarin@27701 ` 522` ``` ultimately show "\a \ Units G. \ \ a" by fast ``` ballarin@27701 ` 523` ```qed ``` ballarin@27701 ` 524` wenzelm@63832 ` 525` ```lemma (in comm_monoid) Units_Lower: "Units G = Lower (division_rel G) (carrier G)" ``` wenzelm@63832 ` 526` ``` apply (simp add: Units_def Lower_def) ``` wenzelm@63832 ` 527` ``` apply (rule, rule) ``` wenzelm@63832 ` 528` ``` apply clarsimp ``` wenzelm@63832 ` 529` ``` apply (rule unit_divides) ``` wenzelm@63832 ` 530` ``` apply (unfold Units_def, fast) ``` wenzelm@63832 ` 531` ``` apply assumption ``` wenzelm@63832 ` 532` ``` apply clarsimp ``` wenzelm@63832 ` 533` ``` apply (metis Unit_eq_dividesone Units_r_inv_ex m_ac(2) one_closed) ``` wenzelm@63832 ` 534` ``` done ``` ballarin@27701 ` 535` ballarin@27701 ` 536` wenzelm@61382 ` 537` ```subsubsection \Proper factors\ ``` ballarin@27701 ` 538` ballarin@27701 ` 539` ```lemma properfactorI: ``` ballarin@27701 ` 540` ``` fixes G (structure) ``` ballarin@27701 ` 541` ``` assumes "a divides b" ``` ballarin@27701 ` 542` ``` and "\(b divides a)" ``` ballarin@27701 ` 543` ``` shows "properfactor G a b" ``` wenzelm@63832 ` 544` ``` using assms unfolding properfactor_def by simp ``` ballarin@27701 ` 545` ballarin@27701 ` 546` ```lemma properfactorI2: ``` ballarin@27701 ` 547` ``` fixes G (structure) ``` ballarin@27701 ` 548` ``` assumes advdb: "a divides b" ``` ballarin@27701 ` 549` ``` and neq: "\(a \ b)" ``` ballarin@27701 ` 550` ``` shows "properfactor G a b" ``` wenzelm@63846 ` 551` ```proof (rule properfactorI, rule advdb, rule notI) ``` ballarin@27701 ` 552` ``` assume "b divides a" ``` ballarin@27701 ` 553` ``` with advdb have "a \ b" by (rule associatedI) ``` ballarin@27701 ` 554` ``` with neq show "False" by fast ``` ballarin@27701 ` 555` ```qed ``` ballarin@27701 ` 556` ballarin@27701 ` 557` ```lemma (in comm_monoid_cancel) properfactorI3: ``` ballarin@27701 ` 558` ``` assumes p: "p = a \ b" ``` ballarin@27701 ` 559` ``` and nunit: "b \ Units G" ``` ballarin@27701 ` 560` ``` and carr: "a \ carrier G" "b \ carrier G" "p \ carrier G" ``` ballarin@27701 ` 561` ``` shows "properfactor G a p" ``` wenzelm@63832 ` 562` ``` unfolding p ``` wenzelm@63832 ` 563` ``` using carr ``` wenzelm@63832 ` 564` ``` apply (intro properfactorI, fast) ``` ballarin@27701 ` 565` ```proof (clarsimp, elim dividesE) ``` ballarin@27701 ` 566` ``` fix c ``` ballarin@27701 ` 567` ``` assume ccarr: "c \ carrier G" ``` ballarin@27701 ` 568` ``` note [simp] = carr ccarr ``` ballarin@27701 ` 569` ballarin@27701 ` 570` ``` have "a \ \ = a" by simp ``` ballarin@27701 ` 571` ``` also assume "a = a \ b \ c" ``` ballarin@27701 ` 572` ``` also have "\ = a \ (b \ c)" by (simp add: m_assoc) ``` ballarin@27701 ` 573` ``` finally have "a \ \ = a \ (b \ c)" . ``` ballarin@27701 ` 574` wenzelm@63832 ` 575` ``` then have rinv: "\ = b \ c" by (intro l_cancel[of "a" "\" "b \ c"], simp+) ``` ballarin@27701 ` 576` ``` also have "\ = c \ b" by (simp add: m_comm) ``` ballarin@27701 ` 577` ``` finally have linv: "\ = c \ b" . ``` ballarin@27701 ` 578` wenzelm@63832 ` 579` ``` from ccarr linv[symmetric] rinv[symmetric] have "b \ Units G" ``` wenzelm@63832 ` 580` ``` unfolding Units_def by fastforce ``` wenzelm@63832 ` 581` ``` with nunit show False .. ``` ballarin@27701 ` 582` ```qed ``` ballarin@27701 ` 583` ballarin@27701 ` 584` ```lemma properfactorE: ``` ballarin@27701 ` 585` ``` fixes G (structure) ``` ballarin@27701 ` 586` ``` assumes pf: "properfactor G a b" ``` ballarin@27701 ` 587` ``` and r: "\a divides b; \(b divides a)\ \ P" ``` ballarin@27701 ` 588` ``` shows "P" ``` wenzelm@63832 ` 589` ``` using pf unfolding properfactor_def by (fast intro: r) ``` ballarin@27701 ` 590` ballarin@27701 ` 591` ```lemma properfactorE2: ``` ballarin@27701 ` 592` ``` fixes G (structure) ``` ballarin@27701 ` 593` ``` assumes pf: "properfactor G a b" ``` ballarin@27701 ` 594` ``` and elim: "\a divides b; \(a \ b)\ \ P" ``` ballarin@27701 ` 595` ``` shows "P" ``` wenzelm@63832 ` 596` ``` using pf unfolding properfactor_def by (fast elim: elim associatedE) ``` ballarin@27701 ` 597` ballarin@27701 ` 598` ```lemma (in monoid) properfactor_unitE: ``` ballarin@27701 ` 599` ``` assumes uunit: "u \ Units G" ``` ballarin@27701 ` 600` ``` and pf: "properfactor G a u" ``` ballarin@27701 ` 601` ``` and acarr: "a \ carrier G" ``` ballarin@27701 ` 602` ``` shows "P" ``` wenzelm@63832 ` 603` ``` using pf unit_divides[OF uunit acarr] by (fast elim: properfactorE) ``` ballarin@27701 ` 604` ballarin@27701 ` 605` ```lemma (in monoid) properfactor_divides: ``` ballarin@27701 ` 606` ``` assumes pf: "properfactor G a b" ``` ballarin@27701 ` 607` ``` shows "a divides b" ``` wenzelm@63832 ` 608` ``` using pf by (elim properfactorE) ``` ballarin@27701 ` 609` ballarin@27701 ` 610` ```lemma (in monoid) properfactor_trans1 [trans]: ``` ballarin@27701 ` 611` ``` assumes dvds: "a divides b" "properfactor G b c" ``` ballarin@27701 ` 612` ``` and carr: "a \ carrier G" "b \ carrier G" "c \ carrier G" ``` ballarin@27701 ` 613` ``` shows "properfactor G a c" ``` wenzelm@63832 ` 614` ``` using dvds carr ``` wenzelm@63832 ` 615` ``` apply (elim properfactorE, intro properfactorI) ``` wenzelm@63832 ` 616` ``` apply (iprover intro: divides_trans)+ ``` wenzelm@63832 ` 617` ``` done ``` ballarin@27701 ` 618` ballarin@27701 ` 619` ```lemma (in monoid) properfactor_trans2 [trans]: ``` ballarin@27701 ` 620` ``` assumes dvds: "properfactor G a b" "b divides c" ``` ballarin@27701 ` 621` ``` and carr: "a \ carrier G" "b \ carrier G" "c \ carrier G" ``` ballarin@27701 ` 622` ``` shows "properfactor G a c" ``` wenzelm@63832 ` 623` ``` using dvds carr ``` wenzelm@63832 ` 624` ``` apply (elim properfactorE, intro properfactorI) ``` wenzelm@63832 ` 625` ``` apply (iprover intro: divides_trans)+ ``` wenzelm@63832 ` 626` ``` done ``` ballarin@27701 ` 627` ballarin@27713 ` 628` ```lemma properfactor_lless: ``` ballarin@27701 ` 629` ``` fixes G (structure) ``` ballarin@27713 ` 630` ``` shows "properfactor G = lless (division_rel G)" ``` wenzelm@63832 ` 631` ``` apply (rule ext) ``` wenzelm@63832 ` 632` ``` apply (rule ext) ``` wenzelm@63832 ` 633` ``` apply rule ``` wenzelm@63832 ` 634` ``` apply (fastforce elim: properfactorE2 intro: weak_llessI) ``` wenzelm@63832 ` 635` ``` apply (fastforce elim: weak_llessE intro: properfactorI2) ``` wenzelm@63832 ` 636` ``` done ``` ballarin@27701 ` 637` ballarin@27701 ` 638` ```lemma (in monoid) properfactor_cong_l [trans]: ``` ballarin@27701 ` 639` ``` assumes x'x: "x' \ x" ``` ballarin@27701 ` 640` ``` and pf: "properfactor G x y" ``` ballarin@27701 ` 641` ``` and carr: "x \ carrier G" "x' \ carrier G" "y \ carrier G" ``` ballarin@27701 ` 642` ``` shows "properfactor G x' y" ``` wenzelm@63832 ` 643` ``` using pf ``` wenzelm@63832 ` 644` ``` unfolding properfactor_lless ``` ballarin@27701 ` 645` ```proof - ``` ballarin@29237 ` 646` ``` interpret weak_partial_order "division_rel G" .. ``` wenzelm@63832 ` 647` ``` from x'x have "x' .=\<^bsub>division_rel G\<^esub> x" by simp ``` ballarin@27701 ` 648` ``` also assume "x \\<^bsub>division_rel G\<^esub> y" ``` wenzelm@63832 ` 649` ``` finally show "x' \\<^bsub>division_rel G\<^esub> y" by (simp add: carr) ``` ballarin@27701 ` 650` ```qed ``` ballarin@27701 ` 651` ballarin@27701 ` 652` ```lemma (in monoid) properfactor_cong_r [trans]: ``` ballarin@27701 ` 653` ``` assumes pf: "properfactor G x y" ``` ballarin@27701 ` 654` ``` and yy': "y \ y'" ``` ballarin@27701 ` 655` ``` and carr: "x \ carrier G" "y \ carrier G" "y' \ carrier G" ``` ballarin@27701 ` 656` ``` shows "properfactor G x y'" ``` wenzelm@63832 ` 657` ``` using pf ``` wenzelm@63832 ` 658` ``` unfolding properfactor_lless ``` ballarin@27701 ` 659` ```proof - ``` ballarin@29237 ` 660` ``` interpret weak_partial_order "division_rel G" .. ``` ballarin@27701 ` 661` ``` assume "x \\<^bsub>division_rel G\<^esub> y" ``` ballarin@27701 ` 662` ``` also from yy' ``` wenzelm@63832 ` 663` ``` have "y .=\<^bsub>division_rel G\<^esub> y'" by simp ``` wenzelm@63832 ` 664` ``` finally show "x \\<^bsub>division_rel G\<^esub> y'" by (simp add: carr) ``` ballarin@27701 ` 665` ```qed ``` ballarin@27701 ` 666` ballarin@27701 ` 667` ```lemma (in monoid_cancel) properfactor_mult_lI [intro]: ``` ballarin@27701 ` 668` ``` assumes ab: "properfactor G a b" ``` ballarin@27701 ` 669` ``` and carr: "a \ carrier G" "b \ carrier G" "c \ carrier G" ``` ballarin@27701 ` 670` ``` shows "properfactor G (c \ a) (c \ b)" ``` wenzelm@63832 ` 671` ``` using ab carr by (fastforce elim: properfactorE intro: properfactorI) ``` ballarin@27701 ` 672` ballarin@27701 ` 673` ```lemma (in monoid_cancel) properfactor_mult_l [simp]: ``` ballarin@27701 ` 674` ``` assumes carr: "a \ carrier G" "b \ carrier G" "c \ carrier G" ``` ballarin@27701 ` 675` ``` shows "properfactor G (c \ a) (c \ b) = properfactor G a b" ``` wenzelm@63832 ` 676` ``` using carr by (fastforce elim: properfactorE intro: properfactorI) ``` ballarin@27701 ` 677` ballarin@27701 ` 678` ```lemma (in comm_monoid_cancel) properfactor_mult_rI [intro]: ``` ballarin@27701 ` 679` ``` assumes ab: "properfactor G a b" ``` ballarin@27701 ` 680` ``` and carr: "a \ carrier G" "b \ carrier G" "c \ carrier G" ``` ballarin@27701 ` 681` ``` shows "properfactor G (a \ c) (b \ c)" ``` wenzelm@63832 ` 682` ``` using ab carr by (fastforce elim: properfactorE intro: properfactorI) ``` ballarin@27701 ` 683` ballarin@27701 ` 684` ```lemma (in comm_monoid_cancel) properfactor_mult_r [simp]: ``` ballarin@27701 ` 685` ``` assumes carr: "a \ carrier G" "b \ carrier G" "c \ carrier G" ``` ballarin@27701 ` 686` ``` shows "properfactor G (a \ c) (b \ c) = properfactor G a b" ``` wenzelm@63832 ` 687` ``` using carr by (fastforce elim: properfactorE intro: properfactorI) ``` ballarin@27701 ` 688` ballarin@27701 ` 689` ```lemma (in monoid) properfactor_prod_r: ``` ballarin@27701 ` 690` ``` assumes ab: "properfactor G a b" ``` ballarin@27701 ` 691` ``` and carr[simp]: "a \ carrier G" "b \ carrier G" "c \ carrier G" ``` ballarin@27701 ` 692` ``` shows "properfactor G a (b \ c)" ``` wenzelm@63832 ` 693` ``` by (intro properfactor_trans2[OF ab] divides_prod_r) simp_all ``` ballarin@27701 ` 694` ballarin@27701 ` 695` ```lemma (in comm_monoid) properfactor_prod_l: ``` ballarin@27701 ` 696` ``` assumes ab: "properfactor G a b" ``` ballarin@27701 ` 697` ``` and carr[simp]: "a \ carrier G" "b \ carrier G" "c \ carrier G" ``` ballarin@27701 ` 698` ``` shows "properfactor G a (c \ b)" ``` wenzelm@63832 ` 699` ``` by (intro properfactor_trans2[OF ab] divides_prod_l) simp_all ``` ballarin@27701 ` 700` ballarin@27701 ` 701` wenzelm@61382 ` 702` ```subsection \Irreducible Elements and Primes\ ``` wenzelm@61382 ` 703` wenzelm@61382 ` 704` ```subsubsection \Irreducible elements\ ``` ballarin@27701 ` 705` ballarin@27701 ` 706` ```lemma irreducibleI: ``` ballarin@27701 ` 707` ``` fixes G (structure) ``` ballarin@27701 ` 708` ``` assumes "a \ Units G" ``` ballarin@27701 ` 709` ``` and "\b. \b \ carrier G; properfactor G b a\ \ b \ Units G" ``` ballarin@27701 ` 710` ``` shows "irreducible G a" ``` wenzelm@63832 ` 711` ``` using assms unfolding irreducible_def by blast ``` ballarin@27701 ` 712` ballarin@27701 ` 713` ```lemma irreducibleE: ``` ballarin@27701 ` 714` ``` fixes G (structure) ``` ballarin@27701 ` 715` ``` assumes irr: "irreducible G a" ``` wenzelm@63832 ` 716` ``` and elim: "\a \ Units G; \b. b \ carrier G \ properfactor G b a \ b \ Units G\ \ P" ``` ballarin@27701 ` 717` ``` shows "P" ``` wenzelm@63832 ` 718` ``` using assms unfolding irreducible_def by blast ``` ballarin@27701 ` 719` ballarin@27701 ` 720` ```lemma irreducibleD: ``` ballarin@27701 ` 721` ``` fixes G (structure) ``` ballarin@27701 ` 722` ``` assumes irr: "irreducible G a" ``` wenzelm@63832 ` 723` ``` and pf: "properfactor G b a" ``` wenzelm@63832 ` 724` ``` and bcarr: "b \ carrier G" ``` ballarin@27701 ` 725` ``` shows "b \ Units G" ``` wenzelm@63832 ` 726` ``` using assms by (fast elim: irreducibleE) ``` ballarin@27701 ` 727` ballarin@27701 ` 728` ```lemma (in monoid_cancel) irreducible_cong [trans]: ``` ballarin@27701 ` 729` ``` assumes irred: "irreducible G a" ``` ballarin@27701 ` 730` ``` and aa': "a \ a'" ``` ballarin@27701 ` 731` ``` and carr[simp]: "a \ carrier G" "a' \ carrier G" ``` ballarin@27701 ` 732` ``` shows "irreducible G a'" ``` wenzelm@63832 ` 733` ``` using assms ``` wenzelm@63832 ` 734` ``` apply (elim irreducibleE, intro irreducibleI) ``` wenzelm@63832 ` 735` ``` apply simp_all ``` wenzelm@63832 ` 736` ``` apply (metis assms(2) assms(3) assoc_unit_l) ``` wenzelm@63832 ` 737` ``` apply (metis assms(2) assms(3) assms(4) associated_sym properfactor_cong_r) ``` wenzelm@63832 ` 738` ``` done ``` ballarin@27701 ` 739` ballarin@27701 ` 740` ```lemma (in monoid) irreducible_prod_rI: ``` ballarin@27701 ` 741` ``` assumes airr: "irreducible G a" ``` ballarin@27701 ` 742` ``` and bunit: "b \ Units G" ``` ballarin@27701 ` 743` ``` and carr[simp]: "a \ carrier G" "b \ carrier G" ``` ballarin@27701 ` 744` ``` shows "irreducible G (a \ b)" ``` wenzelm@63832 ` 745` ``` using airr carr bunit ``` wenzelm@63832 ` 746` ``` apply (elim irreducibleE, intro irreducibleI, clarify) ``` wenzelm@63832 ` 747` ``` apply (subgoal_tac "a \ Units G", simp) ``` wenzelm@63832 ` 748` ``` apply (intro prod_unit_r[of a b] carr bunit, assumption) ``` wenzelm@63847 ` 749` ``` apply (metis assms(2,3) associatedI2 m_closed properfactor_cong_r) ``` wenzelm@63832 ` 750` ``` done ``` ballarin@27701 ` 751` ballarin@27701 ` 752` ```lemma (in comm_monoid) irreducible_prod_lI: ``` ballarin@27701 ` 753` ``` assumes birr: "irreducible G b" ``` ballarin@27701 ` 754` ``` and aunit: "a \ Units G" ``` ballarin@27701 ` 755` ``` and carr [simp]: "a \ carrier G" "b \ carrier G" ``` ballarin@27701 ` 756` ``` shows "irreducible G (a \ b)" ``` wenzelm@63832 ` 757` ``` apply (subst m_comm, simp+) ``` wenzelm@63832 ` 758` ``` apply (intro irreducible_prod_rI assms) ``` wenzelm@63832 ` 759` ``` done ``` ballarin@27701 ` 760` ballarin@27701 ` 761` ```lemma (in comm_monoid_cancel) irreducible_prodE [elim]: ``` ballarin@27701 ` 762` ``` assumes irr: "irreducible G (a \ b)" ``` ballarin@27701 ` 763` ``` and carr[simp]: "a \ carrier G" "b \ carrier G" ``` ballarin@27701 ` 764` ``` and e1: "\irreducible G a; b \ Units G\ \ P" ``` ballarin@27701 ` 765` ``` and e2: "\a \ Units G; irreducible G b\ \ P" ``` wenzelm@63832 ` 766` ``` shows P ``` wenzelm@63832 ` 767` ``` using irr ``` ballarin@27701 ` 768` ```proof (elim irreducibleE) ``` ballarin@27701 ` 769` ``` assume abnunit: "a \ b \ Units G" ``` ballarin@27701 ` 770` ``` and isunit[rule_format]: "\ba. ba \ carrier G \ properfactor G ba (a \ b) \ ba \ Units G" ``` wenzelm@63832 ` 771` ``` show P ``` ballarin@27701 ` 772` ``` proof (cases "a \ Units G") ``` wenzelm@63832 ` 773` ``` case aunit: True ``` ballarin@27701 ` 774` ``` have "irreducible G b" ``` wenzelm@63846 ` 775` ``` proof (rule irreducibleI, rule notI) ``` ballarin@27701 ` 776` ``` assume "b \ Units G" ``` ballarin@27701 ` 777` ``` with aunit have "(a \ b) \ Units G" by fast ``` ballarin@27701 ` 778` ``` with abnunit show "False" .. ``` ballarin@27701 ` 779` ``` next ``` ballarin@27701 ` 780` ``` fix c ``` ballarin@27701 ` 781` ``` assume ccarr: "c \ carrier G" ``` ballarin@27701 ` 782` ``` and "properfactor G c b" ``` wenzelm@63832 ` 783` ``` then have "properfactor G c (a \ b)" by (simp add: properfactor_prod_l[of c b a]) ``` wenzelm@63832 ` 784` ``` with ccarr show "c \ Units G" by (fast intro: isunit) ``` ballarin@27701 ` 785` ``` qed ``` wenzelm@63832 ` 786` ``` with aunit show "P" by (rule e2) ``` ballarin@27701 ` 787` ``` next ``` wenzelm@63832 ` 788` ``` case anunit: False ``` ballarin@27701 ` 789` ``` with carr have "properfactor G b (b \ a)" by (fast intro: properfactorI3) ``` wenzelm@63832 ` 790` ``` then have bf: "properfactor G b (a \ b)" by (subst m_comm[of a b], simp+) ``` wenzelm@63832 ` 791` ``` then have bunit: "b \ Units G" by (intro isunit, simp) ``` ballarin@27701 ` 792` ballarin@27701 ` 793` ``` have "irreducible G a" ``` wenzelm@63846 ` 794` ``` proof (rule irreducibleI, rule notI) ``` ballarin@27701 ` 795` ``` assume "a \ Units G" ``` ballarin@27701 ` 796` ``` with bunit have "(a \ b) \ Units G" by fast ``` ballarin@27701 ` 797` ``` with abnunit show "False" .. ``` ballarin@27701 ` 798` ``` next ``` ballarin@27701 ` 799` ``` fix c ``` ballarin@27701 ` 800` ``` assume ccarr: "c \ carrier G" ``` ballarin@27701 ` 801` ``` and "properfactor G c a" ``` wenzelm@63832 ` 802` ``` then have "properfactor G c (a \ b)" ``` wenzelm@63832 ` 803` ``` by (simp add: properfactor_prod_r[of c a b]) ``` wenzelm@63832 ` 804` ``` with ccarr show "c \ Units G" by (fast intro: isunit) ``` ballarin@27701 ` 805` ``` qed ``` ballarin@27701 ` 806` ``` from this bunit show "P" by (rule e1) ``` ballarin@27701 ` 807` ``` qed ``` ballarin@27701 ` 808` ```qed ``` ballarin@27701 ` 809` ballarin@27701 ` 810` wenzelm@61382 ` 811` ```subsubsection \Prime elements\ ``` ballarin@27701 ` 812` ballarin@27701 ` 813` ```lemma primeI: ``` ballarin@27701 ` 814` ``` fixes G (structure) ``` ballarin@27701 ` 815` ``` assumes "p \ Units G" ``` ballarin@27701 ` 816` ``` and "\a b. \a \ carrier G; b \ carrier G; p divides (a \ b)\ \ p divides a \ p divides b" ``` ballarin@27701 ` 817` ``` shows "prime G p" ``` wenzelm@63832 ` 818` ``` using assms unfolding prime_def by blast ``` ballarin@27701 ` 819` ballarin@27701 ` 820` ```lemma primeE: ``` ballarin@27701 ` 821` ``` fixes G (structure) ``` ballarin@27701 ` 822` ``` assumes pprime: "prime G p" ``` ballarin@27701 ` 823` ``` and e: "\p \ Units G; \a\carrier G. \b\carrier G. ``` wenzelm@63832 ` 824` ``` p divides a \ b \ p divides a \ p divides b\ \ P" ``` ballarin@27701 ` 825` ``` shows "P" ``` wenzelm@63832 ` 826` ``` using pprime unfolding prime_def by (blast dest: e) ``` ballarin@27701 ` 827` ballarin@27701 ` 828` ```lemma (in comm_monoid_cancel) prime_divides: ``` ballarin@27701 ` 829` ``` assumes carr: "a \ carrier G" "b \ carrier G" ``` ballarin@27701 ` 830` ``` and pprime: "prime G p" ``` ballarin@27701 ` 831` ``` and pdvd: "p divides a \ b" ``` ballarin@27701 ` 832` ``` shows "p divides a \ p divides b" ``` wenzelm@63832 ` 833` ``` using assms by (blast elim: primeE) ``` ballarin@27701 ` 834` ballarin@27701 ` 835` ```lemma (in monoid_cancel) prime_cong [trans]: ``` ballarin@27701 ` 836` ``` assumes pprime: "prime G p" ``` ballarin@27701 ` 837` ``` and pp': "p \ p'" ``` ballarin@27701 ` 838` ``` and carr[simp]: "p \ carrier G" "p' \ carrier G" ``` ballarin@27701 ` 839` ``` shows "prime G p'" ``` wenzelm@63832 ` 840` ``` using pprime ``` wenzelm@63832 ` 841` ``` apply (elim primeE, intro primeI) ``` wenzelm@63832 ` 842` ``` apply (metis assms(2) assms(3) assoc_unit_l) ``` wenzelm@63832 ` 843` ``` apply (metis assms(2) assms(3) assms(4) associated_sym divides_cong_l m_closed) ``` wenzelm@63832 ` 844` ``` done ``` wenzelm@63832 ` 845` ballarin@27701 ` 846` wenzelm@61382 ` 847` ```subsection \Factorization and Factorial Monoids\ ``` wenzelm@61382 ` 848` wenzelm@61382 ` 849` ```subsubsection \Function definitions\ ``` ballarin@27701 ` 850` wenzelm@63832 ` 851` ```definition factors :: "[_, 'a list, 'a] \ bool" ``` nipkow@67399 ` 852` ``` where "factors G fs a \ (\x \ (set fs). irreducible G x) \ foldr (\\<^bsub>G\<^esub>) fs \\<^bsub>G\<^esub> = a" ``` wenzelm@35847 ` 853` wenzelm@63832 ` 854` ```definition wfactors ::"[_, 'a list, 'a] \ bool" ``` nipkow@67399 ` 855` ``` where "wfactors G fs a \ (\x \ (set fs). irreducible G x) \ foldr (\\<^bsub>G\<^esub>) fs \\<^bsub>G\<^esub> \\<^bsub>G\<^esub> a" ``` ballarin@27701 ` 856` wenzelm@63832 ` 857` ```abbreviation list_assoc :: "('a,_) monoid_scheme \ 'a list \ 'a list \ bool" (infix "[\]\" 44) ``` nipkow@67399 ` 858` ``` where "list_assoc G \ list_all2 (\\<^bsub>G\<^esub>)" ``` wenzelm@63832 ` 859` wenzelm@63832 ` 860` ```definition essentially_equal :: "[_, 'a list, 'a list] \ bool" ``` wenzelm@35848 ` 861` ``` where "essentially_equal G fs1 fs2 \ (\fs1'. fs1 <~~> fs1' \ fs1' [\]\<^bsub>G\<^esub> fs2)" ``` ballarin@27701 ` 862` ballarin@27701 ` 863` ballarin@27701 ` 864` ```locale factorial_monoid = comm_monoid_cancel + ``` wenzelm@63832 ` 865` ``` assumes factors_exist: "\a \ carrier G; a \ Units G\ \ \fs. set fs \ carrier G \ factors G fs a" ``` wenzelm@63832 ` 866` ``` and factors_unique: ``` wenzelm@63832 ` 867` ``` "\factors G fs a; factors G fs' a; a \ carrier G; a \ Units G; ``` wenzelm@63832 ` 868` ``` set fs \ carrier G; set fs' \ carrier G\ \ essentially_equal G fs fs'" ``` ballarin@27701 ` 869` ballarin@27701 ` 870` wenzelm@61382 ` 871` ```subsubsection \Comparing lists of elements\ ``` wenzelm@61382 ` 872` wenzelm@61382 ` 873` ```text \Association on lists\ ``` ballarin@27701 ` 874` ballarin@27701 ` 875` ```lemma (in monoid) listassoc_refl [simp, intro]: ``` ballarin@27701 ` 876` ``` assumes "set as \ carrier G" ``` ballarin@27701 ` 877` ``` shows "as [\] as" ``` wenzelm@63832 ` 878` ``` using assms by (induct as) simp_all ``` ballarin@27701 ` 879` ballarin@27701 ` 880` ```lemma (in monoid) listassoc_sym [sym]: ``` ballarin@27701 ` 881` ``` assumes "as [\] bs" ``` wenzelm@63832 ` 882` ``` and "set as \ carrier G" ``` wenzelm@63832 ` 883` ``` and "set bs \ carrier G" ``` ballarin@27701 ` 884` ``` shows "bs [\] as" ``` wenzelm@63832 ` 885` ``` using assms ``` ballarin@27701 ` 886` ```proof (induct as arbitrary: bs, simp) ``` ballarin@27701 ` 887` ``` case Cons ``` wenzelm@63832 ` 888` ``` then show ?case ``` wenzelm@63832 ` 889` ``` apply (induct bs) ``` wenzelm@63832 ` 890` ``` apply simp ``` ballarin@27701 ` 891` ``` apply clarsimp ``` ballarin@27701 ` 892` ``` apply (iprover intro: associated_sym) ``` wenzelm@63832 ` 893` ``` done ``` ballarin@27701 ` 894` ```qed ``` ballarin@27701 ` 895` ballarin@27701 ` 896` ```lemma (in monoid) listassoc_trans [trans]: ``` ballarin@27701 ` 897` ``` assumes "as [\] bs" and "bs [\] cs" ``` ballarin@27701 ` 898` ``` and "set as \ carrier G" and "set bs \ carrier G" and "set cs \ carrier G" ``` ballarin@27701 ` 899` ``` shows "as [\] cs" ``` wenzelm@63832 ` 900` ``` using assms ``` wenzelm@63832 ` 901` ``` apply (simp add: list_all2_conv_all_nth set_conv_nth, safe) ``` wenzelm@63832 ` 902` ``` apply (rule associated_trans) ``` wenzelm@63832 ` 903` ``` apply (subgoal_tac "as ! i \ bs ! i", assumption) ``` wenzelm@63832 ` 904` ``` apply (simp, simp) ``` wenzelm@63832 ` 905` ``` apply blast+ ``` wenzelm@63832 ` 906` ``` done ``` ballarin@27701 ` 907` ballarin@27701 ` 908` ```lemma (in monoid_cancel) irrlist_listassoc_cong: ``` ballarin@27701 ` 909` ``` assumes "\a\set as. irreducible G a" ``` ballarin@27701 ` 910` ``` and "as [\] bs" ``` ballarin@27701 ` 911` ``` and "set as \ carrier G" and "set bs \ carrier G" ``` ballarin@27701 ` 912` ``` shows "\a\set bs. irreducible G a" ``` wenzelm@63832 ` 913` ``` using assms ``` wenzelm@63832 ` 914` ``` apply (clarsimp simp add: list_all2_conv_all_nth set_conv_nth) ``` wenzelm@63832 ` 915` ``` apply (blast intro: irreducible_cong) ``` wenzelm@63832 ` 916` ``` done ``` ballarin@27701 ` 917` ballarin@27701 ` 918` wenzelm@61382 ` 919` ```text \Permutations\ ``` ballarin@27701 ` 920` ballarin@27701 ` 921` ```lemma perm_map [intro]: ``` ballarin@27701 ` 922` ``` assumes p: "a <~~> b" ``` ballarin@27701 ` 923` ``` shows "map f a <~~> map f b" ``` wenzelm@63832 ` 924` ``` using p by induct auto ``` ballarin@27701 ` 925` ballarin@27701 ` 926` ```lemma perm_map_switch: ``` ballarin@27701 ` 927` ``` assumes m: "map f a = map f b" and p: "b <~~> c" ``` ballarin@27701 ` 928` ``` shows "\d. a <~~> d \ map f d = map f c" ``` wenzelm@63832 ` 929` ``` using p m by (induct arbitrary: a) (simp, force, force, blast) ``` ballarin@27701 ` 930` ballarin@27701 ` 931` ```lemma (in monoid) perm_assoc_switch: ``` wenzelm@63832 ` 932` ``` assumes a:"as [\] bs" and p: "bs <~~> cs" ``` wenzelm@63832 ` 933` ``` shows "\bs'. as <~~> bs' \ bs' [\] cs" ``` wenzelm@63832 ` 934` ``` using p a ``` wenzelm@63832 ` 935` ``` apply (induct bs cs arbitrary: as, simp) ``` wenzelm@63832 ` 936` ``` apply (clarsimp simp add: list_all2_Cons2, blast) ``` wenzelm@63832 ` 937` ``` apply (clarsimp simp add: list_all2_Cons2) ``` wenzelm@63832 ` 938` ``` apply blast ``` wenzelm@63832 ` 939` ``` apply blast ``` wenzelm@63832 ` 940` ``` done ``` ballarin@27701 ` 941` ballarin@27701 ` 942` ```lemma (in monoid) perm_assoc_switch_r: ``` wenzelm@63832 ` 943` ``` assumes p: "as <~~> bs" and a:"bs [\] cs" ``` wenzelm@63832 ` 944` ``` shows "\bs'. as [\] bs' \ bs' <~~> cs" ``` wenzelm@63832 ` 945` ``` using p a ``` wenzelm@63832 ` 946` ``` apply (induct as bs arbitrary: cs, simp) ``` wenzelm@63832 ` 947` ``` apply (clarsimp simp add: list_all2_Cons1, blast) ``` wenzelm@63832 ` 948` ``` apply (clarsimp simp add: list_all2_Cons1) ``` wenzelm@63832 ` 949` ``` apply blast ``` wenzelm@63832 ` 950` ``` apply blast ``` wenzelm@63832 ` 951` ``` done ``` ballarin@27701 ` 952` ballarin@27701 ` 953` ```declare perm_sym [sym] ``` ballarin@27701 ` 954` ballarin@27701 ` 955` ```lemma perm_setP: ``` ballarin@27701 ` 956` ``` assumes perm: "as <~~> bs" ``` ballarin@27701 ` 957` ``` and as: "P (set as)" ``` ballarin@27701 ` 958` ``` shows "P (set bs)" ``` ballarin@27701 ` 959` ```proof - ``` wenzelm@63832 ` 960` ``` from perm have "mset as = mset bs" ``` wenzelm@63832 ` 961` ``` by (simp add: mset_eq_perm) ``` wenzelm@63832 ` 962` ``` then have "set as = set bs" ``` wenzelm@63832 ` 963` ``` by (rule mset_eq_setD) ``` wenzelm@63832 ` 964` ``` with as show "P (set bs)" ``` wenzelm@63832 ` 965` ``` by simp ``` ballarin@27701 ` 966` ```qed ``` ballarin@27701 ` 967` wenzelm@63832 ` 968` ```lemmas (in monoid) perm_closed = perm_setP[of _ _ "\as. as \ carrier G"] ``` wenzelm@63832 ` 969` wenzelm@63832 ` 970` ```lemmas (in monoid) irrlist_perm_cong = perm_setP[of _ _ "\as. \a\as. irreducible G a"] ``` ballarin@27701 ` 971` ballarin@27701 ` 972` wenzelm@61382 ` 973` ```text \Essentially equal factorizations\ ``` ballarin@27701 ` 974` ballarin@27701 ` 975` ```lemma (in monoid) essentially_equalI: ``` ballarin@27701 ` 976` ``` assumes ex: "fs1 <~~> fs1'" "fs1' [\] fs2" ``` ballarin@27701 ` 977` ``` shows "essentially_equal G fs1 fs2" ``` wenzelm@63832 ` 978` ``` using ex unfolding essentially_equal_def by fast ``` ballarin@27701 ` 979` ballarin@27701 ` 980` ```lemma (in monoid) essentially_equalE: ``` ballarin@27701 ` 981` ``` assumes ee: "essentially_equal G fs1 fs2" ``` ballarin@27701 ` 982` ``` and e: "\fs1'. \fs1 <~~> fs1'; fs1' [\] fs2\ \ P" ``` ballarin@27701 ` 983` ``` shows "P" ``` wenzelm@63832 ` 984` ``` using ee unfolding essentially_equal_def by (fast intro: e) ``` ballarin@27701 ` 985` ballarin@27701 ` 986` ```lemma (in monoid) ee_refl [simp,intro]: ``` ballarin@27701 ` 987` ``` assumes carr: "set as \ carrier G" ``` ballarin@27701 ` 988` ``` shows "essentially_equal G as as" ``` wenzelm@63832 ` 989` ``` using carr by (fast intro: essentially_equalI) ``` ballarin@27701 ` 990` ballarin@27701 ` 991` ```lemma (in monoid) ee_sym [sym]: ``` ballarin@27701 ` 992` ``` assumes ee: "essentially_equal G as bs" ``` ballarin@27701 ` 993` ``` and carr: "set as \ carrier G" "set bs \ carrier G" ``` ballarin@27701 ` 994` ``` shows "essentially_equal G bs as" ``` wenzelm@63832 ` 995` ``` using ee ``` ballarin@27701 ` 996` ```proof (elim essentially_equalE) ``` ballarin@27701 ` 997` ``` fix fs ``` ballarin@27701 ` 998` ``` assume "as <~~> fs" "fs [\] bs" ``` wenzelm@63847 ` 999` ``` from perm_assoc_switch_r [OF this] obtain fs' where a: "as [\] fs'" and p: "fs' <~~> bs" ``` wenzelm@63847 ` 1000` ``` by blast ``` ballarin@27701 ` 1001` ``` from p have "bs <~~> fs'" by (rule perm_sym) ``` wenzelm@63832 ` 1002` ``` with a[symmetric] carr show ?thesis ``` wenzelm@63832 ` 1003` ``` by (iprover intro: essentially_equalI perm_closed) ``` ballarin@27701 ` 1004` ```qed ``` ballarin@27701 ` 1005` ballarin@27701 ` 1006` ```lemma (in monoid) ee_trans [trans]: ``` ballarin@27701 ` 1007` ``` assumes ab: "essentially_equal G as bs" and bc: "essentially_equal G bs cs" ``` wenzelm@63832 ` 1008` ``` and ascarr: "set as \ carrier G" ``` ballarin@27701 ` 1009` ``` and bscarr: "set bs \ carrier G" ``` ballarin@27701 ` 1010` ``` and cscarr: "set cs \ carrier G" ``` ballarin@27701 ` 1011` ``` shows "essentially_equal G as cs" ``` wenzelm@63832 ` 1012` ``` using ab bc ``` ballarin@27701 ` 1013` ```proof (elim essentially_equalE) ``` ballarin@27701 ` 1014` ``` fix abs bcs ``` wenzelm@63847 ` 1015` ``` assume "abs [\] bs" and pb: "bs <~~> bcs" ``` wenzelm@63847 ` 1016` ``` from perm_assoc_switch [OF this] obtain bs' where p: "abs <~~> bs'" and a: "bs' [\] bcs" ``` wenzelm@63847 ` 1017` ``` by blast ``` ballarin@27701 ` 1018` ballarin@27701 ` 1019` ``` assume "as <~~> abs" ``` wenzelm@63832 ` 1020` ``` with p have pp: "as <~~> bs'" by fast ``` ballarin@27701 ` 1021` ballarin@27701 ` 1022` ``` from pp ascarr have c1: "set bs' \ carrier G" by (rule perm_closed) ``` ballarin@27701 ` 1023` ``` from pb bscarr have c2: "set bcs \ carrier G" by (rule perm_closed) ``` ballarin@27701 ` 1024` ``` note a ``` ballarin@27701 ` 1025` ``` also assume "bcs [\] cs" ``` wenzelm@63832 ` 1026` ``` finally (listassoc_trans) have "bs' [\] cs" by (simp add: c1 c2 cscarr) ``` wenzelm@63832 ` 1027` ``` with pp show ?thesis ``` wenzelm@63832 ` 1028` ``` by (rule essentially_equalI) ``` ballarin@27701 ` 1029` ```qed ``` ballarin@27701 ` 1030` ballarin@27701 ` 1031` wenzelm@61382 ` 1032` ```subsubsection \Properties of lists of elements\ ``` wenzelm@61382 ` 1033` wenzelm@61382 ` 1034` ```text \Multiplication of factors in a list\ ``` ballarin@27701 ` 1035` ballarin@27701 ` 1036` ```lemma (in monoid) multlist_closed [simp, intro]: ``` ballarin@27701 ` 1037` ``` assumes ascarr: "set fs \ carrier G" ``` nipkow@67399 ` 1038` ``` shows "foldr (\) fs \ \ carrier G" ``` wenzelm@63832 ` 1039` ``` using ascarr by (induct fs) simp_all ``` ballarin@27701 ` 1040` ballarin@27701 ` 1041` ```lemma (in comm_monoid) multlist_dividesI (*[intro]*): ``` ballarin@27701 ` 1042` ``` assumes "f \ set fs" and "f \ carrier G" and "set fs \ carrier G" ``` nipkow@67399 ` 1043` ``` shows "f divides (foldr (\) fs \)" ``` wenzelm@63832 ` 1044` ``` using assms ``` wenzelm@63832 ` 1045` ``` apply (induct fs) ``` wenzelm@63832 ` 1046` ``` apply simp ``` wenzelm@63832 ` 1047` ``` apply (case_tac "f = a") ``` wenzelm@63832 ` 1048` ``` apply simp ``` wenzelm@63832 ` 1049` ``` apply (fast intro: dividesI) ``` wenzelm@63832 ` 1050` ``` apply clarsimp ``` wenzelm@63832 ` 1051` ``` apply (metis assms(2) divides_prod_l multlist_closed) ``` wenzelm@63832 ` 1052` ``` done ``` ballarin@27701 ` 1053` ballarin@27701 ` 1054` ```lemma (in comm_monoid_cancel) multlist_listassoc_cong: ``` ballarin@27701 ` 1055` ``` assumes "fs [\] fs'" ``` ballarin@27701 ` 1056` ``` and "set fs \ carrier G" and "set fs' \ carrier G" ``` nipkow@67399 ` 1057` ``` shows "foldr (\) fs \ \ foldr (\) fs' \" ``` wenzelm@63832 ` 1058` ``` using assms ``` ballarin@27701 ` 1059` ```proof (induct fs arbitrary: fs', simp) ``` ballarin@27701 ` 1060` ``` case (Cons a as fs') ``` wenzelm@63832 ` 1061` ``` then show ?case ``` wenzelm@63832 ` 1062` ``` apply (induct fs', simp) ``` ballarin@27701 ` 1063` ``` proof clarsimp ``` ballarin@27701 ` 1064` ``` fix b bs ``` wenzelm@63832 ` 1065` ``` assume "a \ b" ``` ballarin@27701 ` 1066` ``` and acarr: "a \ carrier G" and bcarr: "b \ carrier G" ``` ballarin@27701 ` 1067` ``` and ascarr: "set as \ carrier G" ``` nipkow@67399 ` 1068` ``` then have p: "a \ foldr (\) as \ \ b \ foldr (\) as \" ``` wenzelm@63832 ` 1069` ``` by (fast intro: mult_cong_l) ``` ballarin@27701 ` 1070` ``` also ``` wenzelm@63832 ` 1071` ``` assume "as [\] bs" ``` wenzelm@63832 ` 1072` ``` and bscarr: "set bs \ carrier G" ``` nipkow@67399 ` 1073` ``` and "\fs'. \as [\] fs'; set fs' \ carrier G\ \ foldr (\) as \ \ foldr (\) fs' \" ``` nipkow@67399 ` 1074` ``` then have "foldr (\) as \ \ foldr (\) bs \" by simp ``` nipkow@67399 ` 1075` ``` with ascarr bscarr bcarr have "b \ foldr (\) as \ \ b \ foldr (\) bs \" ``` wenzelm@63832 ` 1076` ``` by (fast intro: mult_cong_r) ``` nipkow@67399 ` 1077` ``` finally show "a \ foldr (\) as \ \ b \ foldr (\) bs \" ``` wenzelm@63832 ` 1078` ``` by (simp add: ascarr bscarr acarr bcarr) ``` ballarin@27701 ` 1079` ``` qed ``` ballarin@27701 ` 1080` ```qed ``` ballarin@27701 ` 1081` ballarin@27701 ` 1082` ```lemma (in comm_monoid) multlist_perm_cong: ``` ballarin@27701 ` 1083` ``` assumes prm: "as <~~> bs" ``` ballarin@27701 ` 1084` ``` and ascarr: "set as \ carrier G" ``` nipkow@67399 ` 1085` ``` shows "foldr (\) as \ = foldr (\) bs \" ``` wenzelm@63832 ` 1086` ``` using prm ascarr ``` wenzelm@63832 ` 1087` ``` apply (induct, simp, clarsimp simp add: m_ac, clarsimp) ``` ballarin@27701 ` 1088` ```proof clarsimp ``` ballarin@27701 ` 1089` ``` fix xs ys zs ``` ballarin@27701 ` 1090` ``` assume "xs <~~> ys" "set xs \ carrier G" ``` wenzelm@63832 ` 1091` ``` then have "set ys \ carrier G" by (rule perm_closed) ``` nipkow@67399 ` 1092` ``` moreover assume "set ys \ carrier G \ foldr (\) ys \ = foldr (\) zs \" ``` nipkow@67399 ` 1093` ``` ultimately show "foldr (\) ys \ = foldr (\) zs \" by simp ``` ballarin@27701 ` 1094` ```qed ``` ballarin@27701 ` 1095` ballarin@27701 ` 1096` ```lemma (in comm_monoid_cancel) multlist_ee_cong: ``` ballarin@27701 ` 1097` ``` assumes "essentially_equal G fs fs'" ``` ballarin@27701 ` 1098` ``` and "set fs \ carrier G" and "set fs' \ carrier G" ``` nipkow@67399 ` 1099` ``` shows "foldr (\) fs \ \ foldr (\) fs' \" ``` wenzelm@63832 ` 1100` ``` using assms ``` wenzelm@63832 ` 1101` ``` apply (elim essentially_equalE) ``` wenzelm@63832 ` 1102` ``` apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed) ``` wenzelm@63832 ` 1103` ``` done ``` ballarin@27701 ` 1104` ballarin@27701 ` 1105` wenzelm@61382 ` 1106` ```subsubsection \Factorization in irreducible elements\ ``` ballarin@27701 ` 1107` ballarin@27701 ` 1108` ```lemma wfactorsI: ``` ballarin@28599 ` 1109` ``` fixes G (structure) ``` ballarin@27701 ` 1110` ``` assumes "\f\set fs. irreducible G f" ``` nipkow@67399 ` 1111` ``` and "foldr (\) fs \ \ a" ``` ballarin@27701 ` 1112` ``` shows "wfactors G fs a" ``` wenzelm@63832 ` 1113` ``` using assms unfolding wfactors_def by simp ``` ballarin@27701 ` 1114` ballarin@27701 ` 1115` ```lemma wfactorsE: ``` ballarin@28599 ` 1116` ``` fixes G (structure) ``` ballarin@27701 ` 1117` ``` assumes wf: "wfactors G fs a" ``` nipkow@67399 ` 1118` ``` and e: "\\f\set fs. irreducible G f; foldr (\) fs \ \ a\ \ P" ``` ballarin@27701 ` 1119` ``` shows "P" ``` wenzelm@63832 ` 1120` ``` using wf unfolding wfactors_def by (fast dest: e) ``` ballarin@27701 ` 1121` ballarin@27701 ` 1122` ```lemma (in monoid) factorsI: ``` ballarin@27701 ` 1123` ``` assumes "\f\set fs. irreducible G f" ``` nipkow@67399 ` 1124` ``` and "foldr (\) fs \ = a" ``` ballarin@27701 ` 1125` ``` shows "factors G fs a" ``` wenzelm@63832 ` 1126` ``` using assms unfolding factors_def by simp ``` ballarin@27701 ` 1127` ballarin@27701 ` 1128` ```lemma factorsE: ``` ballarin@28599 ` 1129` ``` fixes G (structure) ``` ballarin@27701 ` 1130` ``` assumes f: "factors G fs a" ``` nipkow@67399 ` 1131` ``` and e: "\\f\set fs. irreducible G f; foldr (\) fs \ = a\ \ P" ``` ballarin@27701 ` 1132` ``` shows "P" ``` wenzelm@63832 ` 1133` ``` using f unfolding factors_def by (simp add: e) ``` ballarin@27701 ` 1134` ballarin@27701 ` 1135` ```lemma (in monoid) factors_wfactors: ``` ballarin@27701 ` 1136` ``` assumes "factors G as a" and "set as \ carrier G" ``` ballarin@27701 ` 1137` ``` shows "wfactors G as a" ``` wenzelm@63832 ` 1138` ``` using assms by (blast elim: factorsE intro: wfactorsI) ``` ballarin@27701 ` 1139` ballarin@27701 ` 1140` ```lemma (in monoid) wfactors_factors: ``` ballarin@27701 ` 1141` ``` assumes "wfactors G as a" and "set as \ carrier G" ``` ballarin@27701 ` 1142` ``` shows "\a'. factors G as a' \ a' \ a" ``` wenzelm@63832 ` 1143` ``` using assms by (blast elim: wfactorsE intro: factorsI) ``` ballarin@27701 ` 1144` ballarin@27701 ` 1145` ```lemma (in monoid) factors_closed [dest]: ``` ballarin@27701 ` 1146` ``` assumes "factors G fs a" and "set fs \ carrier G" ``` ballarin@27701 ` 1147` ``` shows "a \ carrier G" ``` wenzelm@63832 ` 1148` ``` using assms by (elim factorsE, clarsimp) ``` ballarin@27701 ` 1149` ballarin@27701 ` 1150` ```lemma (in monoid) nunit_factors: ``` ballarin@27701 ` 1151` ``` assumes anunit: "a \ Units G" ``` ballarin@27701 ` 1152` ``` and fs: "factors G as a" ``` ballarin@27701 ` 1153` ``` shows "length as > 0" ``` haftmann@46129 ` 1154` ```proof - ``` haftmann@46129 ` 1155` ``` from anunit Units_one_closed have "a \ \" by auto ``` haftmann@46129 ` 1156` ``` with fs show ?thesis by (auto elim: factorsE) ``` haftmann@46129 ` 1157` ```qed ``` ballarin@27701 ` 1158` ballarin@27701 ` 1159` ```lemma (in monoid) unit_wfactors [simp]: ``` ballarin@27701 ` 1160` ``` assumes aunit: "a \ Units G" ``` ballarin@27701 ` 1161` ``` shows "wfactors G [] a" ``` wenzelm@63832 ` 1162` ``` using aunit by (intro wfactorsI) (simp, simp add: Units_assoc) ``` ballarin@27701 ` 1163` ballarin@27701 ` 1164` ```lemma (in comm_monoid_cancel) unit_wfactors_empty: ``` ballarin@27701 ` 1165` ``` assumes aunit: "a \ Units G" ``` ballarin@27701 ` 1166` ``` and wf: "wfactors G fs a" ``` ballarin@27701 ` 1167` ``` and carr[simp]: "set fs \ carrier G" ``` ballarin@27701 ` 1168` ``` shows "fs = []" ``` wenzelm@63846 ` 1169` ```proof (cases fs) ``` wenzelm@63846 ` 1170` ``` case Nil ``` wenzelm@63846 ` 1171` ``` then show ?thesis . ``` wenzelm@63846 ` 1172` ```next ``` wenzelm@63846 ` 1173` ``` case fs: (Cons f fs') ``` wenzelm@63832 ` 1174` ``` from carr have fcarr[simp]: "f \ carrier G" and carr'[simp]: "set fs' \ carrier G" ``` wenzelm@63832 ` 1175` ``` by (simp_all add: fs) ``` wenzelm@63832 ` 1176` wenzelm@63832 ` 1177` ``` from fs wf have "irreducible G f" by (simp add: wfactors_def) ``` wenzelm@63832 ` 1178` ``` then have fnunit: "f \ Units G" by (fast elim: irreducibleE) ``` wenzelm@63832 ` 1179` nipkow@67399 ` 1180` ``` from fs wf have a: "f \ foldr (\) fs' \ \ a" by (simp add: wfactors_def) ``` ballarin@27701 ` 1181` ballarin@27701 ` 1182` ``` note aunit ``` ballarin@27701 ` 1183` ``` also from fs wf ``` nipkow@67399 ` 1184` ``` have a: "f \ foldr (\) fs' \ \ a" by (simp add: wfactors_def) ``` nipkow@67399 ` 1185` ``` have "a \ f \ foldr (\) fs' \" ``` wenzelm@63832 ` 1186` ``` by (simp add: Units_closed[OF aunit] a[symmetric]) ``` nipkow@67399 ` 1187` ``` finally have "f \ foldr (\) fs' \ \ Units G" by simp ``` wenzelm@63832 ` 1188` ``` then have "f \ Units G" by (intro unit_factor[of f], simp+) ``` wenzelm@63846 ` 1189` ``` with fnunit show ?thesis by contradiction ``` ballarin@27701 ` 1190` ```qed ``` ballarin@27701 ` 1191` ballarin@27701 ` 1192` wenzelm@61382 ` 1193` ```text \Comparing wfactors\ ``` ballarin@27701 ` 1194` ballarin@27701 ` 1195` ```lemma (in comm_monoid_cancel) wfactors_listassoc_cong_l: ``` ballarin@27701 ` 1196` ``` assumes fact: "wfactors G fs a" ``` ballarin@27701 ` 1197` ``` and asc: "fs [\] fs'" ``` ballarin@27701 ` 1198` ``` and carr: "a \ carrier G" "set fs \ carrier G" "set fs' \ carrier G" ``` ballarin@27701 ` 1199` ``` shows "wfactors G fs' a" ``` wenzelm@63832 ` 1200` ``` using fact ``` wenzelm@63832 ` 1201` ``` apply (elim wfactorsE, intro wfactorsI) ``` wenzelm@63832 ` 1202` ``` apply (metis assms(2) assms(4) assms(5) irrlist_listassoc_cong) ``` ballarin@27701 ` 1203` ```proof - ``` nipkow@67399 ` 1204` ``` from asc[symmetric] have "foldr (\) fs' \ \ foldr (\) fs \" ``` wenzelm@63832 ` 1205` ``` by (simp add: multlist_listassoc_cong carr) ``` nipkow@67399 ` 1206` ``` also assume "foldr (\) fs \ \ a" ``` nipkow@67399 ` 1207` ``` finally show "foldr (\) fs' \ \ a" by (simp add: carr) ``` ballarin@27701 ` 1208` ```qed ``` ballarin@27701 ` 1209` ballarin@27701 ` 1210` ```lemma (in comm_monoid) wfactors_perm_cong_l: ``` ballarin@27701 ` 1211` ``` assumes "wfactors G fs a" ``` ballarin@27701 ` 1212` ``` and "fs <~~> fs'" ``` ballarin@27701 ` 1213` ``` and "set fs \ carrier G" ``` ballarin@27701 ` 1214` ``` shows "wfactors G fs' a" ``` wenzelm@63832 ` 1215` ``` using assms ``` wenzelm@63832 ` 1216` ``` apply (elim wfactorsE, intro wfactorsI) ``` wenzelm@63832 ` 1217` ``` apply (rule irrlist_perm_cong, assumption+) ``` wenzelm@63832 ` 1218` ``` apply (simp add: multlist_perm_cong[symmetric]) ``` wenzelm@63832 ` 1219` ``` done ``` ballarin@27701 ` 1220` ballarin@27701 ` 1221` ```lemma (in comm_monoid_cancel) wfactors_ee_cong_l [trans]: ``` ballarin@27701 ` 1222` ``` assumes ee: "essentially_equal G as bs" ``` ballarin@27701 ` 1223` ``` and bfs: "wfactors G bs b" ``` ballarin@27701 ` 1224` ``` and carr: "b \ carrier G" "set as \ carrier G" "set bs \ carrier G" ``` ballarin@27701 ` 1225` ``` shows "wfactors G as b" ``` wenzelm@63832 ` 1226` ``` using ee ``` ballarin@27701 ` 1227` ```proof (elim essentially_equalE) ``` ballarin@27701 ` 1228` ``` fix fs ``` ballarin@27701 ` 1229` ``` assume prm: "as <~~> fs" ``` wenzelm@63832 ` 1230` ``` with carr have fscarr: "set fs \ carrier G" by (simp add: perm_closed) ``` ballarin@27701 ` 1231` ballarin@27701 ` 1232` ``` note bfs ``` ballarin@27701 ` 1233` ``` also assume [symmetric]: "fs [\] bs" ``` ballarin@27701 ` 1234` ``` also (wfactors_listassoc_cong_l) ``` wenzelm@63832 ` 1235` ``` note prm[symmetric] ``` ballarin@27701 ` 1236` ``` finally (wfactors_perm_cong_l) ``` wenzelm@63832 ` 1237` ``` show "wfactors G as b" by (simp add: carr fscarr) ``` ballarin@27701 ` 1238` ```qed ``` ballarin@27701 ` 1239` ballarin@27701 ` 1240` ```lemma (in monoid) wfactors_cong_r [trans]: ``` ballarin@27701 ` 1241` ``` assumes fac: "wfactors G fs a" and aa': "a \ a'" ``` ballarin@27701 ` 1242` ``` and carr[simp]: "a \ carrier G" "a' \ carrier G" "set fs \ carrier G" ``` ballarin@27701 ` 1243` ``` shows "wfactors G fs a'" ``` wenzelm@63832 ` 1244` ``` using fac ``` ballarin@27701 ` 1245` ```proof (elim wfactorsE, intro wfactorsI) ``` nipkow@67399 ` 1246` ``` assume "foldr (\) fs \ \ a" also note aa' ``` nipkow@67399 ` 1247` ``` finally show "foldr (\) fs \ \ a'" by simp ``` ballarin@27701 ` 1248` ```qed ``` ballarin@27701 ` 1249` ballarin@27701 ` 1250` wenzelm@61382 ` 1251` ```subsubsection \Essentially equal factorizations\ ``` ballarin@27701 ` 1252` ballarin@27701 ` 1253` ```lemma (in comm_monoid_cancel) unitfactor_ee: ``` ballarin@27701 ` 1254` ``` assumes uunit: "u \ Units G" ``` ballarin@27701 ` 1255` ``` and carr: "set as \ carrier G" ``` wenzelm@63832 ` 1256` ``` shows "essentially_equal G (as[0 := (as!0 \ u)]) as" ``` wenzelm@63832 ` 1257` ``` (is "essentially_equal G ?as' as") ``` wenzelm@63832 ` 1258` ``` using assms ``` wenzelm@63832 ` 1259` ``` apply (intro essentially_equalI[of _ ?as'], simp) ``` wenzelm@63832 ` 1260` ``` apply (cases as, simp) ``` wenzelm@63832 ` 1261` ``` apply (clarsimp, fast intro: associatedI2[of u]) ``` wenzelm@63832 ` 1262` ``` done ``` ballarin@27701 ` 1263` ballarin@27701 ` 1264` ```lemma (in comm_monoid_cancel) factors_cong_unit: ``` wenzelm@63832 ` 1265` ``` assumes uunit: "u \ Units G" ``` wenzelm@63832 ` 1266` ``` and anunit: "a \ Units G" ``` ballarin@27701 ` 1267` ``` and afs: "factors G as a" ``` ballarin@27701 ` 1268` ``` and ascarr: "set as \ carrier G" ``` wenzelm@63832 ` 1269` ``` shows "factors G (as[0 := (as!0 \ u)]) (a \ u)" ``` wenzelm@63832 ` 1270` ``` (is "factors G ?as' ?a'") ``` wenzelm@63832 ` 1271` ``` using assms ``` wenzelm@63832 ` 1272` ``` apply (elim factorsE, clarify) ``` wenzelm@63832 ` 1273` ``` apply (cases as) ``` wenzelm@63832 ` 1274` ``` apply (simp add: nunit_factors) ``` wenzelm@63832 ` 1275` ``` apply clarsimp ``` wenzelm@63832 ` 1276` ``` apply (elim factorsE, intro factorsI) ``` wenzelm@63832 ` 1277` ``` apply (clarsimp, fast intro: irreducible_prod_rI) ``` wenzelm@63832 ` 1278` ``` apply (simp add: m_ac Units_closed) ``` wenzelm@63832 ` 1279` ``` done ``` ballarin@27701 ` 1280` ballarin@27701 ` 1281` ```lemma (in comm_monoid) perm_wfactorsD: ``` ballarin@27701 ` 1282` ``` assumes prm: "as <~~> bs" ``` wenzelm@63832 ` 1283` ``` and afs: "wfactors G as a" ``` wenzelm@63832 ` 1284` ``` and bfs: "wfactors G bs b" ``` ballarin@27701 ` 1285` ``` and [simp]: "a \ carrier G" "b \ carrier G" ``` wenzelm@63832 ` 1286` ``` and ascarr [simp]: "set as \ carrier G" ``` ballarin@27701 ` 1287` ``` shows "a \ b" ``` wenzelm@63832 ` 1288` ``` using afs bfs ``` ballarin@27701 ` 1289` ```proof (elim wfactorsE) ``` ballarin@27701 ` 1290` ``` from prm have [simp]: "set bs \ carrier G" by (simp add: perm_closed) ``` nipkow@67399 ` 1291` ``` assume "foldr (\) as \ \ a" ``` nipkow@67399 ` 1292` ``` then have "a \ foldr (\) as \" by (rule associated_sym, simp+) ``` ballarin@27701 ` 1293` ``` also from prm ``` nipkow@67399 ` 1294` ``` have "foldr (\) as \ = foldr (\) bs \" by (rule multlist_perm_cong, simp) ``` nipkow@67399 ` 1295` ``` also assume "foldr (\) bs \ \ b" ``` wenzelm@63832 ` 1296` ``` finally show "a \ b" by simp ``` ballarin@27701 ` 1297` ```qed ``` ballarin@27701 ` 1298` ballarin@27701 ` 1299` ```lemma (in comm_monoid_cancel) listassoc_wfactorsD: ``` ballarin@27701 ` 1300` ``` assumes assoc: "as [\] bs" ``` wenzelm@63832 ` 1301` ``` and afs: "wfactors G as a" ``` wenzelm@63832 ` 1302` ``` and bfs: "wfactors G bs b" ``` ballarin@27701 ` 1303` ``` and [simp]: "a \ carrier G" "b \ carrier G" ``` ballarin@27701 ` 1304` ``` and [simp]: "set as \ carrier G" "set bs \ carrier G" ``` ballarin@27701 ` 1305` ``` shows "a \ b" ``` wenzelm@63832 ` 1306` ``` using afs bfs ``` ballarin@27701 ` 1307` ```proof (elim wfactorsE) ``` nipkow@67399 ` 1308` ``` assume "foldr (\) as \ \ a" ``` nipkow@67399 ` 1309` ``` then have "a \ foldr (\) as \" by (rule associated_sym, simp+) ``` ballarin@27701 ` 1310` ``` also from assoc ``` nipkow@67399 ` 1311` ``` have "foldr (\) as \ \ foldr (\) bs \" by (rule multlist_listassoc_cong, simp+) ``` nipkow@67399 ` 1312` ``` also assume "foldr (\) bs \ \ b" ``` wenzelm@63832 ` 1313` ``` finally show "a \ b" by simp ``` ballarin@27701 ` 1314` ```qed ``` ballarin@27701 ` 1315` ballarin@27701 ` 1316` ```lemma (in comm_monoid_cancel) ee_wfactorsD: ``` ballarin@27701 ` 1317` ``` assumes ee: "essentially_equal G as bs" ``` ballarin@27701 ` 1318` ``` and afs: "wfactors G as a" and bfs: "wfactors G bs b" ``` ballarin@27701 ` 1319` ``` and [simp]: "a \ carrier G" "b \ carrier G" ``` ballarin@27701 ` 1320` ``` and ascarr[simp]: "set as \ carrier G" and bscarr[simp]: "set bs \ carrier G" ``` ballarin@27701 ` 1321` ``` shows "a \ b" ``` wenzelm@63832 ` 1322` ``` using ee ``` ballarin@27701 ` 1323` ```proof (elim essentially_equalE) ``` ballarin@27701 ` 1324` ``` fix fs ``` ballarin@27701 ` 1325` ``` assume prm: "as <~~> fs" ``` wenzelm@63832 ` 1326` ``` then have as'carr[simp]: "set fs \ carrier G" ``` wenzelm@63832 ` 1327` ``` by (simp add: perm_closed) ``` wenzelm@63832 ` 1328` ``` from afs prm have afs': "wfactors G fs a" ``` wenzelm@63832 ` 1329` ``` by (rule wfactors_perm_cong_l) simp ``` ballarin@27701 ` 1330` ``` assume "fs [\] bs" ``` wenzelm@63832 ` 1331` ``` from this afs' bfs show "a \ b" ``` wenzelm@63832 ` 1332` ``` by (rule listassoc_wfactorsD) simp_all ``` ballarin@27701 ` 1333` ```qed ``` ballarin@27701 ` 1334` ballarin@27701 ` 1335` ```lemma (in comm_monoid_cancel) ee_factorsD: ``` ballarin@27701 ` 1336` ``` assumes ee: "essentially_equal G as bs" ``` ballarin@27701 ` 1337` ``` and afs: "factors G as a" and bfs:"factors G bs b" ``` ballarin@27701 ` 1338` ``` and "set as \ carrier G" "set bs \ carrier G" ``` ballarin@27701 ` 1339` ``` shows "a \ b" ``` wenzelm@63832 ` 1340` ``` using assms by (blast intro: factors_wfactors dest: ee_wfactorsD) ``` ballarin@27701 ` 1341` ballarin@27701 ` 1342` ```lemma (in factorial_monoid) ee_factorsI: ``` ballarin@27701 ` 1343` ``` assumes ab: "a \ b" ``` ballarin@27701 ` 1344` ``` and afs: "factors G as a" and anunit: "a \ Units G" ``` ballarin@27701 ` 1345` ``` and bfs: "factors G bs b" and bnunit: "b \ Units G" ``` ballarin@27701 ` 1346` ``` and ascarr: "set as \ carrier G" and bscarr: "set bs \ carrier G" ``` ballarin@27701 ` 1347` ``` shows "essentially_equal G as bs" ``` ballarin@27701 ` 1348` ```proof - ``` ballarin@27701 ` 1349` ``` note carr[simp] = factors_closed[OF afs ascarr] ascarr[THEN subsetD] ``` wenzelm@63832 ` 1350` ``` factors_closed[OF bfs bscarr] bscarr[THEN subsetD] ``` wenzelm@63832 ` 1351` wenzelm@63847 ` 1352` ``` from ab carr obtain u where uunit: "u \ Units G" and a: "a = b \ u" ``` wenzelm@63847 ` 1353` ``` by (elim associatedE2) ``` wenzelm@63832 ` 1354` wenzelm@63832 ` 1355` ``` from uunit bscarr have ee: "essentially_equal G (bs[0 := (bs!0 \ u)]) bs" ``` wenzelm@63832 ` 1356` ``` (is "essentially_equal G ?bs' bs") ``` wenzelm@63832 ` 1357` ``` by (rule unitfactor_ee) ``` wenzelm@63832 ` 1358` wenzelm@63832 ` 1359` ``` from bscarr uunit have bs'carr: "set ?bs' \ carrier G" ``` wenzelm@63832 ` 1360` ``` by (cases bs) (simp_all add: Units_closed) ``` wenzelm@63832 ` 1361` wenzelm@63832 ` 1362` ``` from uunit bnunit bfs bscarr have fac: "factors G ?bs' (b \ u)" ``` wenzelm@63832 ` 1363` ``` by (rule factors_cong_unit) ``` ballarin@27701 ` 1364` ballarin@27701 ` 1365` ``` from afs fac[simplified a[symmetric]] ascarr bs'carr anunit ``` wenzelm@63832 ` 1366` ``` have "essentially_equal G as ?bs'" ``` wenzelm@63832 ` 1367` ``` by (blast intro: factors_unique) ``` ballarin@27701 ` 1368` ``` also note ee ``` wenzelm@63832 ` 1369` ``` finally show "essentially_equal G as bs" ``` wenzelm@63832 ` 1370` ``` by (simp add: ascarr bscarr bs'carr) ``` ballarin@27701 ` 1371` ```qed ``` ballarin@27701 ` 1372` ballarin@27701 ` 1373` ```lemma (in factorial_monoid) ee_wfactorsI: ``` ballarin@27701 ` 1374` ``` assumes asc: "a \ b" ``` ballarin@27701 ` 1375` ``` and asf: "wfactors G as a" and bsf: "wfactors G bs b" ``` ballarin@27701 ` 1376` ``` and acarr[simp]: "a \ carrier G" and bcarr[simp]: "b \ carrier G" ``` ballarin@27701 ` 1377` ``` and ascarr[simp]: "set as \ carrier G" and bscarr[simp]: "set bs \ carrier G" ``` ballarin@27701 ` 1378` ``` shows "essentially_equal G as bs" ``` wenzelm@63832 ` 1379` ``` using assms ``` ballarin@27701 ` 1380` ```proof (cases "a \ Units G") ``` wenzelm@63832 ` 1381` ``` case aunit: True ``` ballarin@27701 ` 1382` ``` also note asc ``` ballarin@27701 ` 1383` ``` finally have bunit: "b \ Units G" by simp ``` ballarin@27701 ` 1384` wenzelm@63832 ` 1385` ``` from aunit asf ascarr have e: "as = []" ``` wenzelm@63832 ` 1386` ``` by (rule unit_wfactors_empty) ``` wenzelm@63832 ` 1387` ``` from bunit bsf bscarr have e': "bs = []" ``` wenzelm@63832 ` 1388` ``` by (rule unit_wfactors_empty) ``` ballarin@27701 ` 1389` ballarin@27701 ` 1390` ``` have "essentially_equal G [] []" ``` wenzelm@63832 ` 1391` ``` by (fast intro: essentially_equalI) ``` wenzelm@63832 ` 1392` ``` then show ?thesis ``` wenzelm@63832 ` 1393` ``` by (simp add: e e') ``` ballarin@27701 ` 1394` ```next ``` wenzelm@63832 ` 1395` ``` case anunit: False ``` ballarin@27701 ` 1396` ``` have bnunit: "b \ Units G" ``` ballarin@27701 ` 1397` ``` proof clarify ``` ballarin@27701 ` 1398` ``` assume "b \ Units G" ``` ballarin@27701 ` 1399` ``` also note asc[symmetric] ``` ballarin@27701 ` 1400` ``` finally have "a \ Units G" by simp ``` wenzelm@63832 ` 1401` ``` with anunit show False .. ``` ballarin@27701 ` 1402` ``` qed ``` ballarin@27701 ` 1403` wenzelm@63847 ` 1404` ``` from wfactors_factors[OF asf ascarr] obtain a' where fa': "factors G as a'" and a': "a' \ a" ``` wenzelm@63847 ` 1405` ``` by blast ``` wenzelm@63832 ` 1406` ``` from fa' ascarr have a'carr[simp]: "a' \ carrier G" ``` wenzelm@63832 ` 1407` ``` by fast ``` ballarin@27701 ` 1408` ballarin@27701 ` 1409` ``` have a'nunit: "a' \ Units G" ``` wenzelm@63832 ` 1410` ``` proof clarify ``` ballarin@27701 ` 1411` ``` assume "a' \ Units G" ``` ballarin@27701 ` 1412` ``` also note a' ``` ballarin@27701 ` 1413` ``` finally have "a \ Units G" by simp ``` ballarin@27701 ` 1414` ``` with anunit ``` wenzelm@63832 ` 1415` ``` show "False" .. ``` ballarin@27701 ` 1416` ``` qed ``` ballarin@27701 ` 1417` wenzelm@63847 ` 1418` ``` from wfactors_factors[OF bsf bscarr] obtain b' where fb': "factors G bs b'" and b': "b' \ b" ``` wenzelm@63847 ` 1419` ``` by blast ``` wenzelm@63832 ` 1420` ``` from fb' bscarr have b'carr[simp]: "b' \ carrier G" ``` wenzelm@63832 ` 1421` ``` by fast ``` ballarin@27701 ` 1422` ballarin@27701 ` 1423` ``` have b'nunit: "b' \ Units G" ``` wenzelm@63832 ` 1424` ``` proof clarify ``` ballarin@27701 ` 1425` ``` assume "b' \ Units G" ``` ballarin@27701 ` 1426` ``` also note b' ``` ballarin@27701 ` 1427` ``` finally have "b \ Units G" by simp ``` wenzelm@63832 ` 1428` ``` with bnunit show False .. ``` ballarin@27701 ` 1429` ``` qed ``` ballarin@27701 ` 1430` ballarin@27701 ` 1431` ``` note a' ``` ballarin@27701 ` 1432` ``` also note asc ``` ballarin@27701 ` 1433` ``` also note b'[symmetric] ``` wenzelm@63832 ` 1434` ``` finally have "a' \ b'" by simp ``` wenzelm@63832 ` 1435` ``` from this fa' a'nunit fb' b'nunit ascarr bscarr show "essentially_equal G as bs" ``` wenzelm@63832 ` 1436` ``` by (rule ee_factorsI) ``` ballarin@27701 ` 1437` ```qed ``` ballarin@27701 ` 1438` ballarin@27701 ` 1439` ```lemma (in factorial_monoid) ee_wfactors: ``` ballarin@27701 ` 1440` ``` assumes asf: "wfactors G as a" ``` ballarin@27701 ` 1441` ``` and bsf: "wfactors G bs b" ``` ballarin@27701 ` 1442` ``` and acarr: "a \ carrier G" and bcarr: "b \ carrier G" ``` ballarin@27701 ` 1443` ``` and ascarr: "set as \ carrier G" and bscarr: "set bs \ carrier G" ``` ballarin@27701 ` 1444` ``` shows asc: "a \ b = essentially_equal G as bs" ``` wenzelm@63832 ` 1445` ``` using assms by (fast intro: ee_wfactorsI ee_wfactorsD) ``` ballarin@27701 ` 1446` ballarin@27701 ` 1447` ```lemma (in factorial_monoid) wfactors_exist [intro, simp]: ``` ballarin@27701 ` 1448` ``` assumes acarr[simp]: "a \ carrier G" ``` ballarin@27701 ` 1449` ``` shows "\fs. set fs \ carrier G \ wfactors G fs a" ``` ballarin@27701 ` 1450` ```proof (cases "a \ Units G") ``` wenzelm@63832 ` 1451` ``` case True ``` wenzelm@63832 ` 1452` ``` then have "wfactors G [] a" by (rule unit_wfactors) ``` wenzelm@63832 ` 1453` ``` then show ?thesis by (intro exI) force ``` ballarin@27701 ` 1454` ```next ``` wenzelm@63832 ` 1455` ``` case False ``` wenzelm@63847 ` 1456` ``` with factors_exist [OF acarr] obtain fs where fscarr: "set fs \ carrier G" and f: "factors G fs a" ``` wenzelm@63847 ` 1457` ``` by blast ``` ballarin@27701 ` 1458` ``` from f have "wfactors G fs a" by (rule factors_wfactors) fact ``` wenzelm@63832 ` 1459` ``` with fscarr show ?thesis by fast ``` ballarin@27701 ` 1460` ```qed ``` ballarin@27701 ` 1461` ballarin@27701 ` 1462` ```lemma (in monoid) wfactors_prod_exists [intro, simp]: ``` ballarin@27701 ` 1463` ``` assumes "\a \ set as. irreducible G a" and "set as \ carrier G" ``` ballarin@27701 ` 1464` ``` shows "\a. a \ carrier G \ wfactors G as a" ``` wenzelm@63832 ` 1465` ``` unfolding wfactors_def using assms by blast ``` ballarin@27701 ` 1466` ballarin@27701 ` 1467` ```lemma (in factorial_monoid) wfactors_unique: ``` wenzelm@63832 ` 1468` ``` assumes "wfactors G fs a" ``` wenzelm@63832 ` 1469` ``` and "wfactors G fs' a" ``` ballarin@27701 ` 1470` ``` and "a \ carrier G" ``` wenzelm@63832 ` 1471` ``` and "set fs \ carrier G" ``` wenzelm@63832 ` 1472` ``` and "set fs' \ carrier G" ``` ballarin@27701 ` 1473` ``` shows "essentially_equal G fs fs'" ``` wenzelm@63832 ` 1474` ``` using assms by (fast intro: ee_wfactorsI[of a a]) ``` ballarin@27701 ` 1475` ballarin@27701 ` 1476` ```lemma (in monoid) factors_mult_single: ``` ballarin@27701 ` 1477` ``` assumes "irreducible G a" and "factors G fb b" and "a \ carrier G" ``` ballarin@27701 ` 1478` ``` shows "factors G (a # fb) (a \ b)" ``` wenzelm@63832 ` 1479` ``` using assms unfolding factors_def by simp ``` ballarin@27701 ` 1480` ballarin@27701 ` 1481` ```lemma (in monoid_cancel) wfactors_mult_single: ``` ballarin@27701 ` 1482` ``` assumes f: "irreducible G a" "wfactors G fb b" ``` wenzelm@63832 ` 1483` ``` "a \ carrier G" "b \ carrier G" "set fb \ carrier G" ``` ballarin@27701 ` 1484` ``` shows "wfactors G (a # fb) (a \ b)" ``` wenzelm@63832 ` 1485` ``` using assms unfolding wfactors_def by (simp add: mult_cong_r) ``` ballarin@27701 ` 1486` ballarin@27701 ` 1487` ```lemma (in monoid) factors_mult: ``` ballarin@27701 ` 1488` ``` assumes factors: "factors G fa a" "factors G fb b" ``` wenzelm@63832 ` 1489` ``` and ascarr: "set fa \ carrier G" ``` wenzelm@63832 ` 1490` ``` and bscarr: "set fb \ carrier G" ``` ballarin@27701 ` 1491` ``` shows "factors G (fa @ fb) (a \ b)" ``` wenzelm@63832 ` 1492` ``` using assms ``` wenzelm@63832 ` 1493` ``` unfolding factors_def ``` wenzelm@63832 ` 1494` ``` apply safe ``` wenzelm@63832 ` 1495` ``` apply force ``` wenzelm@63832 ` 1496` ``` apply hypsubst_thin ``` wenzelm@63832 ` 1497` ``` apply (induct fa) ``` wenzelm@63832 ` 1498` ``` apply simp ``` wenzelm@63832 ` 1499` ``` apply (simp add: m_assoc) ``` wenzelm@63832 ` 1500` ``` done ``` ballarin@27701 ` 1501` ballarin@27701 ` 1502` ```lemma (in comm_monoid_cancel) wfactors_mult [intro]: ``` ballarin@27701 ` 1503` ``` assumes asf: "wfactors G as a" and bsf:"wfactors G bs b" ``` ballarin@27701 ` 1504` ``` and acarr: "a \ carrier G" and bcarr: "b \ carrier G" ``` ballarin@27701 ` 1505` ``` and ascarr: "set as \ carrier G" and bscarr:"set bs \ carrier G" ``` ballarin@27701 ` 1506` ``` shows "wfactors G (as @ bs) (a \ b)" ``` wenzelm@63832 ` 1507` ``` using wfactors_factors[OF asf ascarr] and wfactors_factors[OF bsf bscarr] ``` wenzelm@63832 ` 1508` ```proof clarsimp ``` ballarin@27701 ` 1509` ``` fix a' b' ``` ballarin@27701 ` 1510` ``` assume asf': "factors G as a'" and a'a: "a' \ a" ``` wenzelm@63832 ` 1511` ``` and bsf': "factors G bs b'" and b'b: "b' \ b" ``` ballarin@27701 ` 1512` ``` from asf' have a'carr: "a' \ carrier G" by (rule factors_closed) fact ``` ballarin@27701 ` 1513` ``` from bsf' have b'carr: "b' \ carrier G" by (rule factors_closed) fact ``` ballarin@27701 ` 1514` ballarin@27701 ` 1515` ``` note carr = acarr bcarr a'carr b'carr ascarr bscarr ``` ballarin@27701 ` 1516` wenzelm@63832 ` 1517` ``` from asf' bsf' have "factors G (as @ bs) (a' \ b')" ``` wenzelm@63832 ` 1518` ``` by (rule factors_mult) fact+ ``` wenzelm@63832 ` 1519` wenzelm@63832 ` 1520` ``` with carr have abf': "wfactors G (as @ bs) (a' \ b')" ``` wenzelm@63832 ` 1521` ``` by (intro factors_wfactors) simp_all ``` wenzelm@63832 ` 1522` ``` also from b'b carr have trb: "a' \ b' \ a' \ b" ``` wenzelm@63832 ` 1523` ``` by (intro mult_cong_r) ``` wenzelm@63832 ` 1524` ``` also from a'a carr have tra: "a' \ b \ a \ b" ``` wenzelm@63832 ` 1525` ``` by (intro mult_cong_l) ``` wenzelm@63832 ` 1526` ``` finally show "wfactors G (as @ bs) (a \ b)" ``` wenzelm@63832 ` 1527` ``` by (simp add: carr) ``` ballarin@27701 ` 1528` ```qed ``` ballarin@27701 ` 1529` ballarin@27701 ` 1530` ```lemma (in comm_monoid) factors_dividesI: ``` wenzelm@63832 ` 1531` ``` assumes "factors G fs a" ``` wenzelm@63832 ` 1532` ``` and "f \ set fs" ``` ballarin@27701 ` 1533` ``` and "set fs \ carrier G" ``` ballarin@27701 ` 1534` ``` shows "f divides a" ``` wenzelm@63832 ` 1535` ``` using assms by (fast elim: factorsE intro: multlist_dividesI) ``` ballarin@27701 ` 1536` ballarin@27701 ` 1537` ```lemma (in comm_monoid) wfactors_dividesI: ``` ballarin@27701 ` 1538` ``` assumes p: "wfactors G fs a" ``` ballarin@27701 ` 1539` ``` and fscarr: "set fs \ carrier G" and acarr: "a \ carrier G" ``` ballarin@27701 ` 1540` ``` and f: "f \ set fs" ``` ballarin@27701 ` 1541` ``` shows "f divides a" ``` wenzelm@63832 ` 1542` ``` using wfactors_factors[OF p fscarr] ``` wenzelm@63832 ` 1543` ```proof clarsimp ``` ballarin@27701 ` 1544` ``` fix a' ``` wenzelm@63832 ` 1545` ``` assume fsa': "factors G fs a'" and a'a: "a' \ a" ``` wenzelm@63832 ` 1546` ``` with fscarr have a'carr: "a' \ carrier G" ``` wenzelm@63832 ` 1547` ``` by (simp add: factors_closed) ``` wenzelm@63832 ` 1548` wenzelm@63832 ` 1549` ``` from fsa' fscarr f have "f divides a'" ``` wenzelm@63832 ` 1550` ``` by (fast intro: factors_dividesI) ``` ballarin@27701 ` 1551` ``` also note a'a ``` wenzelm@63832 ` 1552` ``` finally show "f divides a" ``` wenzelm@63832 ` 1553` ``` by (simp add: f fscarr[THEN subsetD] acarr a'carr) ``` ballarin@27701 ` 1554` ```qed ``` ballarin@27701 ` 1555` ballarin@27701 ` 1556` wenzelm@61382 ` 1557` ```subsubsection \Factorial monoids and wfactors\ ``` ballarin@27701 ` 1558` ballarin@27701 ` 1559` ```lemma (in comm_monoid_cancel) factorial_monoidI: ``` wenzelm@63832 ` 1560` ``` assumes wfactors_exists: "\a. a \ carrier G \ \fs. set fs \ carrier G \ wfactors G fs a" ``` wenzelm@63832 ` 1561` ``` and wfactors_unique: ``` wenzelm@63832 ` 1562` ``` "\a fs fs'. \a \ carrier G; set fs \ carrier G; set fs' \ carrier G; ``` wenzelm@63832 ` 1563` ``` wfactors G fs a; wfactors G fs' a\ \ essentially_equal G fs fs'" ``` ballarin@27701 ` 1564` ``` shows "factorial_monoid G" ``` haftmann@28823 ` 1565` ```proof ``` ballarin@27701 ` 1566` ``` fix a ``` ballarin@27701 ` 1567` ``` assume acarr: "a \ carrier G" and anunit: "a \ Units G" ``` ballarin@27701 ` 1568` ballarin@27701 ` 1569` ``` from wfactors_exists[OF acarr] ``` wenzelm@63832 ` 1570` ``` obtain as where ascarr: "set as \ carrier G" and afs: "wfactors G as a" ``` wenzelm@63847 ` 1571` ``` by blast ``` wenzelm@63847 ` 1572` ``` from wfactors_factors [OF afs ascarr] obtain a' where afs': "factors G as a'" and a'a: "a' \ a" ``` wenzelm@63847 ` 1573` ``` by blast ``` wenzelm@63832 ` 1574` ``` from afs' ascarr have a'carr: "a' \ carrier G" ``` wenzelm@63832 ` 1575` ``` by fast ``` ballarin@27701 ` 1576` ``` have a'nunit: "a' \ Units G" ``` ballarin@27701 ` 1577` ``` proof clarify ``` ballarin@27701 ` 1578` ``` assume "a' \ Units G" ``` ballarin@27701 ` 1579` ``` also note a'a ``` ballarin@27701 ` 1580` ``` finally have "a \ Units G" by (simp add: acarr) ``` wenzelm@63832 ` 1581` ``` with anunit show False .. ``` ballarin@27701 ` 1582` ``` qed ``` ballarin@27701 ` 1583` wenzelm@63847 ` 1584` ``` from a'carr acarr a'a obtain u where uunit: "u \ Units G" and a': "a' = a \ u" ``` wenzelm@63832 ` 1585` ``` by (blast elim: associatedE2) ``` ballarin@27701 ` 1586` ballarin@27701 ` 1587` ``` note [simp] = acarr Units_closed[OF uunit] Units_inv_closed[OF uunit] ``` ballarin@27701 ` 1588` ballarin@27701 ` 1589` ``` have "a = a \ \" by simp ``` wenzelm@57865 ` 1590` ``` also have "\ = a \ (u \ inv u)" by (simp add: uunit) ``` ballarin@27701 ` 1591` ``` also have "\ = a' \ inv u" by (simp add: m_assoc[symmetric] a'[symmetric]) ``` wenzelm@63832 ` 1592` ``` finally have a: "a = a' \ inv u" . ``` wenzelm@63832 ` 1593` wenzelm@63832 ` 1594` ``` from ascarr uunit have cr: "set (as[0:=(as!0 \ inv u)]) \ carrier G" ``` wenzelm@63832 ` 1595` ``` by (cases as) auto ``` wenzelm@63832 ` 1596` wenzelm@63832 ` 1597` ``` from afs' uunit a'nunit acarr ascarr have "factors G (as[0:=(as!0 \ inv u)]) a" ``` wenzelm@63832 ` 1598` ``` by (simp add: a factors_cong_unit) ``` wenzelm@63832 ` 1599` ``` with cr show "\fs. set fs \ carrier G \ factors G fs a" ``` wenzelm@63832 ` 1600` ``` by fast ``` ballarin@27701 ` 1601` ```qed (blast intro: factors_wfactors wfactors_unique) ``` ballarin@27701 ` 1602` ballarin@27701 ` 1603` wenzelm@61382 ` 1604` ```subsection \Factorizations as Multisets\ ``` wenzelm@61382 ` 1605` wenzelm@61382 ` 1606` ```text \Gives useful operations like intersection\ ``` ballarin@27701 ` 1607` ballarin@27701 ` 1608` ```(* FIXME: use class_of x instead of closure_of {x} *) ``` ballarin@27701 ` 1609` wenzelm@63832 ` 1610` ```abbreviation "assocs G x \ eq_closure_of (division_rel G) {x}" ``` wenzelm@63832 ` 1611` wenzelm@63832 ` 1612` ```definition "fmset G as = mset (map (\a. assocs G a) as)" ``` ballarin@27701 ` 1613` ballarin@27701 ` 1614` wenzelm@61382 ` 1615` ```text \Helper lemmas\ ``` ballarin@27701 ` 1616` ballarin@27701 ` 1617` ```lemma (in monoid) assocs_repr_independence: ``` ballarin@27701 ` 1618` ``` assumes "y \ assocs G x" ``` ballarin@27701 ` 1619` ``` and "x \ carrier G" ``` ballarin@27701 ` 1620` ``` shows "assocs G x = assocs G y" ``` wenzelm@63832 ` 1621` ``` using assms ``` wenzelm@63832 ` 1622` ``` apply safe ``` wenzelm@63832 ` 1623` ``` apply (elim closure_ofE2, intro closure_ofI2[of _ _ y]) ``` wenzelm@63832 ` 1624` ``` apply (clarsimp, iprover intro: associated_trans associated_sym, simp+) ``` wenzelm@63832 ` 1625` ``` apply (elim closure_ofE2, intro closure_ofI2[of _ _ x]) ``` wenzelm@63832 ` 1626` ``` apply (clarsimp, iprover intro: associated_trans, simp+) ``` wenzelm@63832 ` 1627` ``` done ``` ballarin@27701 ` 1628` ballarin@27701 ` 1629` ```lemma (in monoid) assocs_self: ``` ballarin@27701 ` 1630` ``` assumes "x \ carrier G" ``` ballarin@27701 ` 1631` ``` shows "x \ assocs G x" ``` wenzelm@63832 ` 1632` ``` using assms by (fastforce intro: closure_ofI2) ``` ballarin@27701 ` 1633` ballarin@27701 ` 1634` ```lemma (in monoid) assocs_repr_independenceD: ``` ballarin@27701 ` 1635` ``` assumes repr: "assocs G x = assocs G y" ``` ballarin@27701 ` 1636` ``` and ycarr: "y \ carrier G" ``` ballarin@27701 ` 1637` ``` shows "y \ assocs G x" ``` wenzelm@63832 ` 1638` ``` unfolding repr using ycarr by (intro assocs_self) ``` ballarin@27701 ` 1639` ballarin@27701 ` 1640` ```lemma (in comm_monoid) assocs_assoc: ``` ballarin@27701 ` 1641` ``` assumes "a \ assocs G b" ``` ballarin@27701 ` 1642` ``` and "b \ carrier G" ``` ballarin@27701 ` 1643` ``` shows "a \ b" ``` wenzelm@63832 ` 1644` ``` using assms by (elim closure_ofE2) simp ``` wenzelm@63832 ` 1645` wenzelm@63832 ` 1646` ```lemmas (in comm_monoid) assocs_eqD = assocs_repr_independenceD[THEN assocs_assoc] ``` ballarin@27701 ` 1647` ballarin@27701 ` 1648` wenzelm@61382 ` 1649` ```subsubsection \Comparing multisets\ ``` ballarin@27701 ` 1650` ballarin@27701 ` 1651` ```lemma (in monoid) fmset_perm_cong: ``` ballarin@27701 ` 1652` ``` assumes prm: "as <~~> bs" ``` ballarin@27701 ` 1653` ``` shows "fmset G as = fmset G bs" ``` wenzelm@63832 ` 1654` ``` using perm_map[OF prm] unfolding mset_eq_perm fmset_def by blast ``` ballarin@27701 ` 1655` ballarin@27701 ` 1656` ```lemma (in comm_monoid_cancel) eqc_listassoc_cong: ``` ballarin@27701 ` 1657` ``` assumes "as [\] bs" ``` ballarin@27701 ` 1658` ``` and "set as \ carrier G" and "set bs \ carrier G" ``` ballarin@27701 ` 1659` ``` shows "map (assocs G) as = map (assocs G) bs" ``` wenzelm@63832 ` 1660` ``` using assms ``` wenzelm@63832 ` 1661` ``` apply (induct as arbitrary: bs, simp) ``` wenzelm@63832 ` 1662` ``` apply (clarsimp simp add: Cons_eq_map_conv list_all2_Cons1, safe) ``` wenzelm@63832 ` 1663` ``` apply (clarsimp elim!: closure_ofE2) defer 1 ``` wenzelm@63832 ` 1664` ``` apply (clarsimp elim!: closure_ofE2) defer 1 ``` ballarin@27701 ` 1665` ```proof - ``` ballarin@27701 ` 1666` ``` fix a x z ``` ballarin@27701 ` 1667` ``` assume carr[simp]: "a \ carrier G" "x \ carrier G" "z \ carrier G" ``` ballarin@27701 ` 1668` ``` assume "x \ a" ``` ballarin@27701 ` 1669` ``` also assume "a \ z" ``` ballarin@27701 ` 1670` ``` finally have "x \ z" by simp ``` wenzelm@63832 ` 1671` ``` with carr show "x \ assocs G z" ``` wenzelm@63832 ` 1672` ``` by (intro closure_ofI2) simp_all ``` ballarin@27701 ` 1673` ```next ``` ballarin@27701 ` 1674` ``` fix a x z ``` ballarin@27701 ` 1675` ``` assume carr[simp]: "a \ carrier G" "x \ carrier G" "z \ carrier G" ``` ballarin@27701 ` 1676` ``` assume "x \ z" ``` ballarin@27701 ` 1677` ``` also assume [symmetric]: "a \ z" ``` ballarin@27701 ` 1678` ``` finally have "x \ a" by simp ``` wenzelm@63832 ` 1679` ``` with carr show "x \ assocs G a" ``` wenzelm@63832 ` 1680` ``` by (intro closure_ofI2) simp_all ``` ballarin@27701 ` 1681` ```qed ``` ballarin@27701 ` 1682` ballarin@27701 ` 1683` ```lemma (in comm_monoid_cancel) fmset_listassoc_cong: ``` wenzelm@63832 ` 1684` ``` assumes "as [\] bs" ``` ballarin@27701 ` 1685` ``` and "set as \ carrier G" and "set bs \ carrier G" ``` ballarin@27701 ` 1686` ``` shows "fmset G as = fmset G bs" ``` wenzelm@63832 ` 1687` ``` using assms unfolding fmset_def by (simp add: eqc_listassoc_cong) ``` ballarin@27701 ` 1688` ballarin@27701 ` 1689` ```lemma (in comm_monoid_cancel) ee_fmset: ``` wenzelm@63832 ` 1690` ``` assumes ee: "essentially_equal G as bs" ``` ballarin@27701 ` 1691` ``` and ascarr: "set as \ carrier G" and bscarr: "set bs \ carrier G" ``` ballarin@27701 ` 1692` ``` shows "fmset G as = fmset G bs" ``` wenzelm@63832 ` 1693` ``` using ee ``` ballarin@27701 ` 1694` ```proof (elim essentially_equalE) ``` ballarin@27701 ` 1695` ``` fix as' ``` ballarin@27701 ` 1696` ``` assume prm: "as <~~> as'" ``` wenzelm@63832 ` 1697` ``` from prm ascarr have as'carr: "set as' \ carrier G" ``` wenzelm@63832 ` 1698` ``` by (rule perm_closed) ``` wenzelm@63832 ` 1699` wenzelm@63832 ` 1700` ``` from prm have "fmset G as = fmset G as'" ``` wenzelm@63832 ` 1701` ``` by (rule fmset_perm_cong) ``` ballarin@27701 ` 1702` ``` also assume "as' [\] bs" ``` wenzelm@63832 ` 1703` ``` with as'carr bscarr have "fmset G as' = fmset G bs" ``` wenzelm@63832 ` 1704` ``` by (simp add: fmset_listassoc_cong) ``` wenzelm@63832 ` 1705` ``` finally show "fmset G as = fmset G bs" . ``` ballarin@27701 ` 1706` ```qed ``` ballarin@27701 ` 1707` ballarin@27701 ` 1708` ```lemma (in monoid_cancel) fmset_ee__hlp_induct: ``` ballarin@27701 ` 1709` ``` assumes prm: "cas <~~> cbs" ``` ballarin@27701 ` 1710` ``` and cdef: "cas = map (assocs G) as" "cbs = map (assocs G) bs" ``` wenzelm@63832 ` 1711` ``` shows "\as bs. (cas <~~> cbs \ cas = map (assocs G) as \ ``` wenzelm@63832 ` 1712` ``` cbs = map (assocs G) bs) \ (\as'. as <~~> as' \ map (assocs G) as' = cbs)" ``` wenzelm@63832 ` 1713` ``` apply (rule perm.induct[of cas cbs], rule prm) ``` wenzelm@63832 ` 1714` ``` apply safe ``` wenzelm@63832 ` 1715` ``` apply (simp_all del: mset_map) ``` wenzelm@63832 ` 1716` ``` apply (simp add: map_eq_Cons_conv) ``` wenzelm@63832 ` 1717` ``` apply blast ``` wenzelm@63832 ` 1718` ``` apply force ``` ballarin@27701 ` 1719` ```proof - ``` ballarin@27701 ` 1720` ``` fix ys as bs ``` ballarin@27701 ` 1721` ``` assume p1: "map (assocs G) as <~~> ys" ``` ballarin@27701 ` 1722` ``` and r1[rule_format]: ``` wenzelm@63832 ` 1723` ``` "\asa bs. map (assocs G) as = map (assocs G) asa \ ys = map (assocs G) bs ``` wenzelm@63832 ` 1724` ``` \ (\as'. asa <~~> as' \ map (assocs G) as' = map (assocs G) bs)" ``` ballarin@27701 ` 1725` ``` and p2: "ys <~~> map (assocs G) bs" ``` wenzelm@63832 ` 1726` ``` and r2[rule_format]: "\as bsa. ys = map (assocs G) as \ map (assocs G) bs = map (assocs G) bsa ``` wenzelm@63832 ` 1727` ``` \ (\as'. as <~~> as' \ map (assocs G) as' = map (assocs G) bsa)" ``` ballarin@27701 ` 1728` ``` and p3: "map (assocs G) as <~~> map (assocs G) bs" ``` ballarin@27701 ` 1729` wenzelm@63832 ` 1730` ``` from p1 have "mset (map (assocs G) as) = mset ys" ``` wenzelm@63832 ` 1731` ``` by (simp add: mset_eq_perm del: mset_map) ``` wenzelm@63832 ` 1732` ``` then have setys: "set (map (assocs G) as) = set ys" ``` wenzelm@63832 ` 1733` ``` by (rule mset_eq_setD) ``` wenzelm@63832 ` 1734` wenzelm@63832 ` 1735` ``` have "set (map (assocs G) as) = {assocs G x | x. x \ set as}" by auto ``` ballarin@27701 ` 1736` ``` with setys have "set ys \ { assocs G x | x. x \ set as}" by simp ``` wenzelm@63832 ` 1737` ``` then have "\yy. ys = map (assocs G) yy" ``` wenzelm@63847 ` 1738` ``` proof (induct ys) ``` wenzelm@63847 ` 1739` ``` case Nil ``` wenzelm@63847 ` 1740` ``` then show ?case by simp ``` wenzelm@63847 ` 1741` ``` next ``` wenzelm@63847 ` 1742` ``` case Cons ``` wenzelm@63847 ` 1743` ``` then show ?case ``` wenzelm@63847 ` 1744` ``` proof clarsimp ``` wenzelm@63847 ` 1745` ``` fix yy x ``` wenzelm@63847 ` 1746` ``` show "\yya. assocs G x # map (assocs G) yy = map (assocs G) yya" ``` wenzelm@63847 ` 1747` ``` by (rule exI[of _ "x#yy"]) simp ``` wenzelm@63847 ` 1748` ``` qed ``` ballarin@27701 ` 1749` ``` qed ``` wenzelm@63847 ` 1750` ``` then obtain yy where ys: "ys = map (assocs G) yy" .. ``` wenzelm@63832 ` 1751` wenzelm@63832 ` 1752` ``` from p1 ys have "\as'. as <~~> as' \ map (assocs G) as' = map (assocs G) yy" ``` wenzelm@63832 ` 1753` ``` by (intro r1) simp ``` wenzelm@63832 ` 1754` ``` then obtain as' where asas': "as <~~> as'" and as'yy: "map (assocs G) as' = map (assocs G) yy" ``` wenzelm@63832 ` 1755` ``` by auto ``` wenzelm@63832 ` 1756` wenzelm@63832 ` 1757` ``` from p2 ys have "\as'. yy <~~> as' \ map (assocs G) as' = map (assocs G) bs" ``` wenzelm@63832 ` 1758` ``` by (intro r2) simp ``` wenzelm@63832 ` 1759` ``` then obtain as'' where yyas'': "yy <~~> as''" and as''bs: "map (assocs G) as'' = map (assocs G) bs" ``` wenzelm@63832 ` 1760` ``` by auto ``` wenzelm@63832 ` 1761` wenzelm@63847 ` 1762` ``` from perm_map_switch [OF as'yy yyas''] ``` wenzelm@63847 ` 1763` ``` obtain cs where as'cs: "as' <~~> cs" and csas'': "map (assocs G) cs = map (assocs G) as''" ``` wenzelm@63847 ` 1764` ``` by blast ``` wenzelm@63847 ` 1765` wenzelm@63847 ` 1766` ``` from asas' and as'cs have ascs: "as <~~> cs" ``` wenzelm@63847 ` 1767` ``` by fast ``` wenzelm@63847 ` 1768` ``` from csas'' and as''bs have "map (assocs G) cs = map (assocs G) bs" ``` wenzelm@63847 ` 1769` ``` by simp ``` wenzelm@63847 ` 1770` ``` with ascs show "\as'. as <~~> as' \ map (assocs G) as' = map (assocs G) bs" ``` wenzelm@63847 ` 1771` ``` by fast ``` ballarin@27701 ` 1772` ```qed ``` ballarin@27701 ` 1773` ballarin@27701 ` 1774` ```lemma (in comm_monoid_cancel) fmset_ee: ``` ballarin@27701 ` 1775` ``` assumes mset: "fmset G as = fmset G bs" ``` ballarin@27701 ` 1776` ``` and ascarr: "set as \ carrier G" and bscarr: "set bs \ carrier G" ``` ballarin@27701 ` 1777` ``` shows "essentially_equal G as bs" ``` ballarin@27701 ` 1778` ```proof - ``` wenzelm@63832 ` 1779` ``` from mset have mpp: "map (assocs G) as <~~> map (assocs G) bs" ``` wenzelm@63832 ` 1780` ``` by (simp add: fmset_def mset_eq_perm del: mset_map) ``` ballarin@27701 ` 1781` wenzelm@63847 ` 1782` ``` define cas where "cas = map (assocs G) as" ``` wenzelm@63847 ` 1783` ``` define cbs where "cbs = map (assocs G) bs" ``` wenzelm@63847 ` 1784` wenzelm@63847 ` 1785` ``` from cas_def cbs_def mpp have [rule_format]: ``` wenzelm@63832 ` 1786` ``` "\as bs. (cas <~~> cbs \ cas = map (assocs G) as \ cbs = map (assocs G) bs) ``` wenzelm@63832 ` 1787` ``` \ (\as'. as <~~> as' \ map (assocs G) as' = cbs)" ``` wenzelm@63832 ` 1788` ``` by (intro fmset_ee__hlp_induct, simp+) ``` wenzelm@63847 ` 1789` ``` with mpp cas_def cbs_def have "\as'. as <~~> as' \ map (assocs G) as' = map (assocs G) bs" ``` wenzelm@63832 ` 1790` ``` by simp ``` wenzelm@63832 ` 1791` wenzelm@63832 ` 1792` ``` then obtain as' where tp: "as <~~> as'" and tm: "map (assocs G) as' = map (assocs G) bs" ``` wenzelm@63832 ` 1793` ``` by auto ``` wenzelm@63832 ` 1794` ``` from tm have lene: "length as' = length bs" ``` wenzelm@63832 ` 1795` ``` by (rule map_eq_imp_length_eq) ``` wenzelm@63832 ` 1796` ``` from tp have "set as = set as'" ``` wenzelm@63832 ` 1797` ``` by (simp add: mset_eq_perm mset_eq_setD) ``` wenzelm@63832 ` 1798` ``` with ascarr have as'carr: "set as' \ carrier G" ``` wenzelm@63832 ` 1799` ``` by simp ``` ballarin@27701 ` 1800` wenzelm@63847 ` 1801` ``` from tm as'carr[THEN subsetD] bscarr[THEN subsetD] have "as' [\] bs" ``` nipkow@44890 ` 1802` ``` by (induct as' arbitrary: bs) (simp, fastforce dest: assocs_eqD[THEN associated_sym]) ``` wenzelm@63832 ` 1803` ``` with tp show "essentially_equal G as bs" ``` wenzelm@63832 ` 1804` ``` by (fast intro: essentially_equalI) ``` ballarin@27701 ` 1805` ```qed ``` ballarin@27701 ` 1806` ballarin@27701 ` 1807` ```lemma (in comm_monoid_cancel) ee_is_fmset: ``` ballarin@27701 ` 1808` ``` assumes "set as \ carrier G" and "set bs \ carrier G" ``` ballarin@27701 ` 1809` ``` shows "essentially_equal G as bs = (fmset G as = fmset G bs)" ``` wenzelm@63832 ` 1810` ``` using assms by (fast intro: ee_fmset fmset_ee) ``` ballarin@27701 ` 1811` ballarin@27701 ` 1812` wenzelm@61382 ` 1813` ```subsubsection \Interpreting multisets as factorizations\ ``` ballarin@27701 ` 1814` ballarin@27701 ` 1815` ```lemma (in monoid) mset_fmsetEx: ``` nipkow@60495 ` 1816` ``` assumes elems: "\X. X \ set_mset Cs \ \x. P x \ X = assocs G x" ``` ballarin@27701 ` 1817` ``` shows "\cs. (\c \ set cs. P c) \ fmset G cs = Cs" ``` ballarin@27701 ` 1818` ```proof - ``` wenzelm@63847 ` 1819` ``` from surjE[OF surj_mset] obtain Cs' where Cs: "Cs = mset Cs'" ``` wenzelm@63847 ` 1820` ``` by blast ``` nipkow@60515 ` 1821` ``` have "\cs. (\c \ set cs. P c) \ mset (map (assocs G) cs) = Cs" ``` wenzelm@63832 ` 1822` ``` using elems ``` wenzelm@63832 ` 1823` ``` unfolding Cs ``` ballarin@27701 ` 1824` ``` apply (induct Cs', simp) ``` Mathias@63524 ` 1825` ``` proof (clarsimp simp del: mset_map) ``` wenzelm@63832 ` 1826` ``` fix a Cs' cs ``` ballarin@27701 ` 1827` ``` assume ih: "\X. X = a \ X \ set Cs' \ \x. P x \ X = assocs G x" ``` ballarin@27701 ` 1828` ``` and csP: "\x\set cs. P x" ``` nipkow@60515 ` 1829` ``` and mset: "mset (map (assocs G) cs) = mset Cs'" ``` wenzelm@63847 ` 1830` ``` from ih obtain c where cP: "P c" and a: "a = assocs G c" ``` wenzelm@63847 ` 1831` ``` by auto ``` wenzelm@63847 ` 1832` ``` from cP csP have tP: "\x\set (c#cs). P x" ``` wenzelm@63847 ` 1833` ``` by simp ``` wenzelm@63847 ` 1834` ``` from mset a have "mset (map (assocs G) (c#cs)) = add_mset a (mset Cs')" ``` wenzelm@63847 ` 1835` ``` by simp ``` wenzelm@63847 ` 1836` ``` with tP show "\cs. (\x\set cs. P x) \ mset (map (assocs G) cs) = add_mset a (mset Cs')" ``` wenzelm@63847 ` 1837` ``` by fast ``` nipkow@60143 ` 1838` ``` qed ``` wenzelm@63832 ` 1839` ``` then show ?thesis by (simp add: fmset_def) ``` ballarin@27701 ` 1840` ```qed ``` ballarin@27701 ` 1841` ballarin@27701 ` 1842` ```lemma (in monoid) mset_wfactorsEx: ``` wenzelm@63832 ` 1843` ``` assumes elems: "\X. X \ set_mset Cs \ \x. (x \ carrier G \ irreducible G x) \ X = assocs G x" ``` ballarin@27701 ` 1844` ``` shows "\c cs. c \ carrier G \ set cs \ carrier G \ wfactors G cs c \ fmset G cs = Cs" ``` ballarin@27701 ` 1845` ```proof - ``` ballarin@27701 ` 1846` ``` have "\cs. (\c\set cs. c \ carrier G \ irreducible G c) \ fmset G cs = Cs" ``` wenzelm@63832 ` 1847` ``` by (intro mset_fmsetEx, rule elems) ``` wenzelm@63832 ` 1848` ``` then obtain cs where p[rule_format]: "\c\set cs. c \ carrier G \ irreducible G c" ``` wenzelm@63832 ` 1849` ``` and Cs[symmetric]: "fmset G cs = Cs" by auto ``` wenzelm@63832 ` 1850` ``` from p have cscarr: "set cs \ carrier G" by fast ``` wenzelm@63832 ` 1851` ``` from p have "\c. c \ carrier G \ wfactors G cs c" ``` wenzelm@63832 ` 1852` ``` by (intro wfactors_prod_exists) auto ``` wenzelm@63832 ` 1853` ``` then obtain c where ccarr: "c \ carrier G" and cfs: "wfactors G cs c" by auto ``` wenzelm@63832 ` 1854` ``` with cscarr Cs show ?thesis by fast ``` ballarin@27701 ` 1855` ```qed ``` ballarin@27701 ` 1856` ballarin@27701 ` 1857` wenzelm@61382 ` 1858` ```subsubsection \Multiplication on multisets\ ``` ballarin@27701 ` 1859` ballarin@27701 ` 1860` ```lemma (in factorial_monoid) mult_wfactors_fmset: ``` wenzelm@63832 ` 1861` ``` assumes afs: "wfactors G as a" ``` wenzelm@63832 ` 1862` ``` and bfs: "wfactors G bs b" ``` wenzelm@63832 ` 1863` ``` and cfs: "wfactors G cs (a \ b)" ``` ballarin@27701 ` 1864` ``` and carr: "a \ carrier G" "b \ carrier G" ``` ballarin@27701 ` 1865` ``` "set as \ carrier G" "set bs \ carrier G" "set cs \ carrier G" ``` ballarin@27701 ` 1866` ``` shows "fmset G cs = fmset G as + fmset G bs" ``` ballarin@27701 ` 1867` ```proof - ``` wenzelm@63832 ` 1868` ``` from assms have "wfactors G (as @ bs) (a \ b)" ``` wenzelm@63832 ` 1869` ``` by (intro wfactors_mult) ``` wenzelm@63832 ` 1870` ``` with carr cfs have "essentially_equal G cs (as@bs)" ``` wenzelm@63832 ` 1871` ``` by (intro ee_wfactorsI[of "a\b" "a\b"]) simp_all ``` wenzelm@63832 ` 1872` ``` with carr have "fmset G cs = fmset G (as@bs)" ``` wenzelm@63832 ` 1873` ``` by (intro ee_fmset) simp_all ``` wenzelm@63832 ` 1874` ``` also have "fmset G (as@bs) = fmset G as + fmset G bs" ``` wenzelm@63832 ` 1875` ``` by (simp add: fmset_def) ``` ballarin@27701 ` 1876` ``` finally show "fmset G cs = fmset G as + fmset G bs" . ``` ballarin@27701 ` 1877` ```qed ``` ballarin@27701 ` 1878` ballarin@27701 ` 1879` ```lemma (in factorial_monoid) mult_factors_fmset: ``` wenzelm@63832 ` 1880` ``` assumes afs: "factors G as a" ``` wenzelm@63832 ` 1881` ``` and bfs: "factors G bs b" ``` wenzelm@63832 ` 1882` ``` and cfs: "factors G cs (a \ b)" ``` ballarin@27701 ` 1883` ``` and "set as \ carrier G" "set bs \ carrier G" "set cs \ carrier G" ``` ballarin@27701 ` 1884` ``` shows "fmset G cs = fmset G as + fmset G bs" ``` wenzelm@63832 ` 1885` ``` using assms by (blast intro: factors_wfactors mult_wfactors_fmset) ``` ballarin@27701 ` 1886` ballarin@27701 ` 1887` ```lemma (in comm_monoid_cancel) fmset_wfactors_mult: ``` ballarin@27701 ` 1888` ``` assumes mset: "fmset G cs = fmset G as + fmset G bs" ``` ballarin@27701 ` 1889` ``` and carr: "a \ carrier G" "b \ carrier G" "c \ carrier G" ``` wenzelm@63832 ` 1890` ``` "set as \ carrier G" "set bs \ carrier G" "set cs \ carrier G" ``` ballarin@27701 ` 1891` ``` and fs: "wfactors G as a" "wfactors G bs b" "wfactors G cs c" ``` ballarin@27701 ` 1892` ``` shows "c \ a \ b" ``` ballarin@27701 ` 1893` ```proof - ``` wenzelm@63832 ` 1894` ``` from carr fs have m: "wfactors G (as @ bs) (a \ b)" ``` wenzelm@63832 ` 1895` ``` by (intro wfactors_mult) ``` wenzelm@63832 ` 1896` wenzelm@63832 ` 1897` ``` from mset have "fmset G cs = fmset G (as@bs)" ``` wenzelm@63832 ` 1898` ``` by (simp add: fmset_def) ``` wenzelm@63832 ` 1899` ``` then have "essentially_equal G cs (as@bs)" ``` wenzelm@63832 ` 1900` ``` by (rule fmset_ee) (simp_all add: carr) ``` wenzelm@63832 ` 1901` ``` then show "c \ a \ b" ``` wenzelm@63832 ` 1902` ``` by (rule ee_wfactorsD[of "cs" "as@bs"]) (simp_all add: assms m) ``` ballarin@27701 ` 1903` ```qed ``` ballarin@27701 ` 1904` ballarin@27701 ` 1905` wenzelm@61382 ` 1906` ```subsubsection \Divisibility on multisets\ ``` ballarin@27701 ` 1907` ballarin@27701 ` 1908` ```lemma (in factorial_monoid) divides_fmsubset: ``` ballarin@27701 ` 1909` ``` assumes ab: "a divides b" ``` wenzelm@63832 ` 1910` ``` and afs: "wfactors G as a" ``` wenzelm@63832 ` 1911` ``` and bfs: "wfactors G bs b" ``` ballarin@27701 ` 1912` ``` and carr: "a \ carrier G" "b \ carrier G" "set as \ carrier G" "set bs \ carrier G" ``` haftmann@64587 ` 1913` ``` shows "fmset G as \# fmset G bs" ``` wenzelm@63832 ` 1914` ``` using ab ``` ballarin@27701 ` 1915` ```proof (elim dividesE) ``` ballarin@27701 ` 1916` ``` fix c ``` ballarin@27701 ` 1917` ``` assume ccarr: "c \ carrier G" ``` wenzelm@63847 ` 1918` ``` from wfactors_exist [OF this] ``` wenzelm@63847 ` 1919` ``` obtain cs where cscarr: "set cs \ carrier G" and cfs: "wfactors G cs c" ``` wenzelm@63847 ` 1920` ``` by blast ``` ballarin@27701 ` 1921` ``` note carr = carr ccarr cscarr ``` ballarin@27701 ` 1922` ballarin@27701 ` 1923` ``` assume "b = a \ c" ``` wenzelm@63832 ` 1924` ``` with afs bfs cfs carr have "fmset G bs = fmset G as + fmset G cs" ``` wenzelm@63832 ` 1925` ``` by (intro mult_wfactors_fmset[OF afs cfs]) simp_all ``` wenzelm@63832 ` 1926` ``` then show ?thesis by simp ``` ballarin@27701 ` 1927` ```qed ``` ballarin@27701 ` 1928` ballarin@27701 ` 1929` ```lemma (in comm_monoid_cancel) fmsubset_divides: ``` haftmann@64587 ` 1930` ``` assumes msubset: "fmset G as \# fmset G bs" ``` wenzelm@63832 ` 1931` ``` and afs: "wfactors G as a" ``` wenzelm@63832 ` 1932` ``` and bfs: "wfactors G bs b" ``` wenzelm@63832 ` 1933` ``` and acarr: "a \ carrier G" ``` wenzelm@63832 ` 1934` ``` and bcarr: "b \ carrier G" ``` wenzelm@63832 ` 1935` ``` and ascarr: "set as \ carrier G" ``` wenzelm@63832 ` 1936` ``` and bscarr: "set bs \ carrier G" ``` ballarin@27701 ` 1937` ``` shows "a divides b" ``` ballarin@27701 ` 1938` ```proof - ``` ballarin@27701 ` 1939` ``` from afs have airr: "\a \ set as. irreducible G a" by (fast elim: wfactorsE) ``` ballarin@27701 ` 1940` ``` from bfs have birr: "\b \ set bs. irreducible G b" by (fast elim: wfactorsE) ``` ballarin@27701 ` 1941` ballarin@27701 ` 1942` ``` have "\c cs. c \ carrier G \ set cs \ carrier G \ wfactors G cs c \ fmset G cs = fmset G bs - fmset G as" ``` ballarin@27701 ` 1943` ``` proof (intro mset_wfactorsEx, simp) ``` ballarin@27701 ` 1944` ``` fix X ``` haftmann@62430 ` 1945` ``` assume "X \# fmset G bs - fmset G as" ``` wenzelm@63832 ` 1946` ``` then have "X \# fmset G bs" by (rule in_diffD) ``` wenzelm@63832 ` 1947` ``` then have "X \ set (map (assocs G) bs)" by (simp add: fmset_def) ``` wenzelm@63832 ` 1948` ``` then have "\x. x \ set bs \ X = assocs G x" by (induct bs) auto ``` wenzelm@63832 ` 1949` ``` then obtain x where xbs: "x \ set bs" and X: "X = assocs G x" by auto ``` ballarin@27701 ` 1950` ``` with bscarr have xcarr: "x \ carrier G" by fast ``` ballarin@27701 ` 1951` ``` from xbs birr have xirr: "irreducible G x" by simp ``` ballarin@27701 ` 1952` wenzelm@63832 ` 1953` ``` from xcarr and xirr and X show "\x. x \ carrier G \ irreducible G x \ X = assocs G x" ``` wenzelm@63832 ` 1954` ``` by fast ``` ballarin@27701 ` 1955` ``` qed ``` wenzelm@63832 ` 1956` ``` then obtain c cs ``` wenzelm@63832 ` 1957` ``` where ccarr: "c \ carrier G" ``` wenzelm@63832 ` 1958` ``` and cscarr: "set cs \ carrier G" ``` ballarin@27701 ` 1959` ``` and csf: "wfactors G cs c" ``` ballarin@27701 ` 1960` ``` and csmset: "fmset G cs = fmset G bs - fmset G as" by auto ``` ballarin@27701 ` 1961` ballarin@27701 ` 1962` ``` from csmset msubset ``` wenzelm@63832 ` 1963` ``` have "fmset G bs = fmset G as + fmset G cs" ``` wenzelm@63832 ` 1964` ``` by (simp add: multiset_eq_iff subseteq_mset_def) ``` wenzelm@63832 ` 1965` ``` then have basc: "b \ a \ c" ``` wenzelm@63832 ` 1966` ``` by (rule fmset_wfactors_mult) fact+ ``` wenzelm@63832 ` 1967` ``` then show ?thesis ``` ballarin@27701 ` 1968` ``` proof (elim associatedE2) ``` ballarin@27701 ` 1969` ``` fix u ``` ballarin@27701 ` 1970` ``` assume "u \ Units G" "b = a \ c \ u" ``` wenzelm@63832 ` 1971` ``` with acarr ccarr show "a divides b" ``` wenzelm@63832 ` 1972` ``` by (fast intro: dividesI[of "c \ u"] m_assoc) ``` wenzelm@63832 ` 1973` ``` qed (simp_all add: acarr bcarr ccarr) ``` ballarin@27701 ` 1974` ```qed ``` ballarin@27701 ` 1975` ballarin@27701 ` 1976` ```lemma (in factorial_monoid) divides_as_fmsubset: ``` wenzelm@63832 ` 1977` ``` assumes "wfactors G as a" ``` wenzelm@63832 ` 1978` ``` and "wfactors G bs b" ``` wenzelm@63832 ` 1979` ``` and "a \ carrier G" ``` wenzelm@63832 ` 1980` ``` and "b \ carrier G" ``` wenzelm@63832 ` 1981` ``` and "set as \ carrier G" ``` wenzelm@63832 ` 1982` ``` and "set bs \ carrier G" ``` haftmann@64587 ` 1983` ``` shows "a divides b = (fmset G as \# fmset G bs)" ``` wenzelm@63832 ` 1984` ``` using assms ``` wenzelm@63832 ` 1985` ``` by (blast intro: divides_fmsubset fmsubset_divides) ``` ballarin@27701 ` 1986` ballarin@27701 ` 1987` wenzelm@61382 ` 1988` ```text \Proper factors on multisets\ ``` ballarin@27701 ` 1989` ballarin@27701 ` 1990` ```lemma (in factorial_monoid) fmset_properfactor: ``` haftmann@64587 ` 1991` ``` assumes asubb: "fmset G as \# fmset G bs" ``` ballarin@27701 ` 1992` ``` and anb: "fmset G as \ fmset G bs" ``` wenzelm@63832 ` 1993` ``` and "wfactors G as a" ``` wenzelm@63832 ` 1994` ``` and "wfactors G bs b" ``` wenzelm@63832 ` 1995` ``` and "a \ carrier G" ``` wenzelm@63832 ` 1996` ``` and "b \ carrier G" ``` wenzelm@63832 ` 1997` ``` and "set as \ carrier G" ``` wenzelm@63832 ` 1998` ``` and "set bs \ carrier G" ``` ballarin@27701 ` 1999` ``` shows "properfactor G a b" ``` wenzelm@63832 ` 2000` ``` apply (rule properfactorI) ``` wenzelm@63832 ` 2001` ``` apply (rule fmsubset_divides[of as bs], fact+) ``` ballarin@27701 ` 2002` ```proof ``` ballarin@27701 ` 2003` ``` assume "b divides a" ``` haftmann@64587 ` 2004` ``` then have "fmset G bs \# fmset G as" ``` wenzelm@63832 ` 2005` ``` by (rule divides_fmsubset) fact+ ``` wenzelm@63832 ` 2006` ``` with asubb have "fmset G as = fmset G bs" ``` wenzelm@63832 ` 2007` ``` by (rule subset_mset.antisym) ``` wenzelm@63832 ` 2008` ``` with anb show False .. ``` ballarin@27701 ` 2009` ```qed ``` ballarin@27701 ` 2010` ballarin@27701 ` 2011` ```lemma (in factorial_monoid) properfactor_fmset: ``` ballarin@27701 ` 2012` ``` assumes pf: "properfactor G a b" ``` wenzelm@63832 ` 2013` ``` and "wfactors G as a" ``` wenzelm@63832 ` 2014` ``` and "wfactors G bs b" ``` wenzelm@63832 ` 2015` ``` and "a \ carrier G" ``` wenzelm@63832 ` 2016` ``` and "b \ carrier G" ``` wenzelm@63832 ` 2017` ``` and "set as \ carrier G" ``` wenzelm@63832 ` 2018` ``` and "set bs \ carrier G" ``` haftmann@64587 ` 2019` ``` shows "fmset G as \# fmset G bs \ fmset G as \ fmset G bs" ``` wenzelm@63832 ` 2020` ``` using pf ``` wenzelm@63832 ` 2021` ``` apply (elim properfactorE) ``` wenzelm@63832 ` 2022` ``` apply rule ``` wenzelm@63832 ` 2023` ``` apply (intro divides_fmsubset, assumption) ``` wenzelm@63832 ` 2024` ``` apply (rule assms)+ ``` wenzelm@63832 ` 2025` ``` using assms(2,3,4,6,7) divides_as_fmsubset ``` wenzelm@63832 ` 2026` ``` apply auto ``` wenzelm@63832 ` 2027` ``` done ``` ballarin@27701 ` 2028` wenzelm@61382 ` 2029` ```subsection \Irreducible Elements are Prime\ ``` ballarin@27701 ` 2030` eberlm@63633 ` 2031` ```lemma (in factorial_monoid) irreducible_prime: ``` ballarin@27701 ` 2032` ``` assumes pirr: "irreducible G p" ``` ballarin@27701 ` 2033` ``` and pcarr: "p \ carrier G" ``` ballarin@27701 ` 2034` ``` shows "prime G p" ``` wenzelm@63832 ` 2035` ``` using pirr ``` ballarin@27701 ` 2036` ```proof (elim irreducibleE, intro primeI) ``` ballarin@27701 ` 2037` ``` fix a b ``` ballarin@27701 ` 2038` ``` assume acarr: "a \ carrier G" and bcarr: "b \ carrier G" ``` ballarin@27701 ` 2039` ``` and pdvdab: "p divides (a \ b)" ``` ballarin@27701 ` 2040` ``` and pnunit: "p \ Units G" ``` ballarin@27701 ` 2041` ``` assume irreduc[rule_format]: ``` wenzelm@63832 ` 2042` ``` "\b. b \ carrier G \ properfactor G b p \ b \ Units G" ``` wenzelm@63847 ` 2043` ``` from pdvdab obtain c where ccarr: "c \ carrier G" and abpc: "a \ b = p \ c" ``` wenzelm@63847 ` 2044` ``` by (rule dividesE) ``` wenzelm@63847 ` 2045` wenzelm@63847 ` 2046` ``` from wfactors_exist [OF acarr] ``` wenzelm@63847 ` 2047` ``` obtain as where ascarr: "set as \ carrier G" and afs: "wfactors G as a" ``` wenzelm@63847 ` 2048` ``` by blast ``` wenzelm@63847 ` 2049` wenzelm@63847 ` 2050` ``` from wfactors_exist [OF bcarr] ``` wenzelm@63847 ` 2051` ``` obtain bs where bscarr: "set bs \ carrier G" and bfs: "wfactors G bs b" ``` wenzelm@63832 ` 2052` ``` by auto ``` wenzelm@63832 ` 2053` wenzelm@63847 ` 2054` ``` from wfactors_exist [OF ccarr] ``` wenzelm@63847 ` 2055` ``` obtain cs where cscarr: "set cs \ carrier G" and cfs: "wfactors G cs c" ``` wenzelm@63832 ` 2056` ``` by auto ``` ballarin@27701 ` 2057` ballarin@27701 ` 2058` ``` note carr[simp] = pcarr acarr bcarr ccarr ascarr bscarr cscarr ``` ballarin@27701 ` 2059` wenzelm@63832 ` 2060` ``` from afs and bfs have abfs: "wfactors G (as @ bs) (a \ b)" ``` wenzelm@63832 ` 2061` ``` by (rule wfactors_mult) fact+ ``` wenzelm@63832 ` 2062` wenzelm@63832 ` 2063` ``` from pirr cfs have pcfs: "wfactors G (p # cs) (p \ c)" ``` wenzelm@63832 ` 2064` ``` by (rule wfactors_mult_single) fact+ ``` wenzelm@63832 ` 2065` ``` with abpc have abfs': "wfactors G (p # cs) (a \ b)" ``` wenzelm@63832 ` 2066` ``` by simp ``` wenzelm@63832 ` 2067` wenzelm@63832 ` 2068` ``` from abfs' abfs have "essentially_equal G (p # cs) (as @ bs)" ``` wenzelm@63832 ` 2069` ``` by (rule wfactors_unique) simp+ ``` wenzelm@63832 ` 2070` wenzelm@63847 ` 2071` ``` then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\] (as @ bs)" ``` wenzelm@63832 ` 2072` ``` by (fast elim: essentially_equalE) ``` ballarin@27701 ` 2073` ``` then have "p \ set ds" ``` wenzelm@63832 ` 2074` ``` by (simp add: perm_set_eq[symmetric]) ``` wenzelm@63847 ` 2075` ``` with dsassoc obtain p' where "p' \ set (as@bs)" and pp': "p \ p'" ``` wenzelm@63832 ` 2076` ``` unfolding list_all2_conv_all_nth set_conv_nth by force ``` wenzelm@63832 ` 2077` ``` then consider "p' \ set as" | "p' \ set bs" by auto ``` wenzelm@63832 ` 2078` ``` then show "p divides a \ p divides b" ``` wenzelm@63832 ` 2079` ``` proof cases ``` wenzelm@63832 ` 2080` ``` case 1 ``` ballarin@27701 ` 2081` ``` with ascarr have [simp]: "p' \ carrier G" by fast ``` ballarin@27701 ` 2082` ballarin@27701 ` 2083` ``` note pp' ``` ballarin@27701 ` 2084` ``` also from afs ``` wenzelm@63832 ` 2085` ``` have "p' divides a" by (rule wfactors_dividesI) fact+ ``` wenzelm@63832 ` 2086` ``` finally have "p divides a" by simp ``` wenzelm@63832 ` 2087` ``` then show ?thesis .. ``` wenzelm@63832 ` 2088` ``` next ``` wenzelm@63832 ` 2089` ``` case 2 ``` ballarin@27701 ` 2090` ``` with bscarr have [simp]: "p' \ carrier G" by fast ``` ballarin@27701 ` 2091` ballarin@27701 ` 2092` ``` note pp' ``` ballarin@27701 ` 2093` ``` also from bfs ``` wenzelm@63832 ` 2094` ``` have "p' divides b" by (rule wfactors_dividesI) fact+ ``` wenzelm@63832 ` 2095` ``` finally have "p divides b" by simp ``` wenzelm@63832 ` 2096` ``` then show ?thesis .. ``` wenzelm@63832 ` 2097` ``` qed ``` ballarin@27701 ` 2098` ```qed ``` ballarin@27701 ` 2099` ballarin@27701 ` 2100` wenzelm@67443 ` 2101` ```\ \A version using @{const factors}, more complicated\ ``` eberlm@63633 ` 2102` ```lemma (in factorial_monoid) factors_irreducible_prime: ``` ballarin@27701 ` 2103` ``` assumes pirr: "irreducible G p" ``` ballarin@27701 ` 2104` ``` and pcarr: "p \ carrier G" ``` ballarin@27701 ` 2105` ``` shows "prime G p" ``` wenzelm@63832 ` 2106` ``` using pirr ``` wenzelm@63832 ` 2107` ``` apply (elim irreducibleE, intro primeI) ``` wenzelm@63832 ` 2108` ``` apply assumption ``` ballarin@27701 ` 2109` ```proof - ``` ballarin@27701 ` 2110` ``` fix a b ``` wenzelm@63832 ` 2111` ``` assume acarr: "a \ carrier G" ``` ballarin@27701 ` 2112` ``` and bcarr: "b \ carrier G" ``` ballarin@27701 ` 2113` ``` and pdvdab: "p divides (a \ b)" ``` wenzelm@63832 ` 2114` ``` assume irreduc[rule_format]: "\b. b \ carrier G \ properfactor G b p \ b \ Units G" ``` wenzelm@63847 ` 2115` ``` from pdvdab obtain c where ccarr: "c \ carrier G" and abpc: "a \ b = p \ c" ``` wenzelm@63847 ` 2116` ``` by (rule dividesE) ``` ballarin@27701 ` 2117` ``` note [simp] = pcarr acarr bcarr ccarr ``` ballarin@27701 ` 2118` ballarin@27701 ` 2119` ``` show "p divides a \ p divides b" ``` ballarin@27701 ` 2120` ``` proof (cases "a \ Units G") ``` wenzelm@63832 ` 2121` ``` case aunit: True ``` ballarin@27701 ` 2122` ballarin@27701 ` 2123` ``` note pdvdab ``` ballarin@27701 ` 2124` ``` also have "a \ b = b \ a" by (simp add: m_comm) ``` wenzelm@63832 ` 2125` ``` also from aunit have bab: "b \ a \ b" ``` wenzelm@63832 ` 2126` ``` by (intro associatedI2[of "a"], simp+) ``` wenzelm@63832 ` 2127` ``` finally have "p divides b" by simp ``` wenzelm@63832 ` 2128` ``` then show ?thesis .. ``` ballarin@27701 ` 2129` ``` next ``` wenzelm@63832 ` 2130` ``` case anunit: False ``` wenzelm@63832 ` 2131` ``` show ?thesis ``` ballarin@27701 ` 2132` ``` proof (cases "b \ Units G") ``` wenzelm@63832 ` 2133` ``` case bunit: True ``` ballarin@27701 ` 2134` ``` note pdvdab ``` ballarin@27701 ` 2135` ``` also from bunit ``` wenzelm@63832 ` 2136` ``` have baa: "a \ b \ a" ``` wenzelm@63832 ` 2137` ``` by (intro associatedI2[of "b"], simp+) ``` wenzelm@63832 ` 2138` ``` finally have "p divides a" by simp ``` wenzelm@63832 ` 2139` ``` then show ?thesis .. ``` ballarin@27701 ` 2140` ``` next ``` wenzelm@63832 ` 2141` ``` case bnunit: False ``` ballarin@27701 ` 2142` ``` have cnunit: "c \ Units G" ``` wenzelm@63846 ` 2143` ``` proof ``` ballarin@27701 ` 2144` ``` assume cunit: "c \ Units G" ``` wenzelm@63832 ` 2145` ``` from bnunit have "properfactor G a (a \ b)" ``` wenzelm@63832 ` 2146` ``` by (intro properfactorI3[of _ _ b], simp+) ``` ballarin@27701 ` 2147` ``` also note abpc ``` wenzelm@63832 ` 2148` ``` also from cunit have "p \ c \ p" ``` wenzelm@63832 ` 2149` ``` by (intro associatedI2[of c], simp+) ``` wenzelm@63832 ` 2150` ``` finally have "properfactor G a p" by simp ``` wenzelm@63832 ` 2151` ``` with acarr have "a \ Units G" by (fast intro: irreduc) ``` wenzelm@63832 ` 2152` ``` with anunit show False .. ``` ballarin@27701 ` 2153` ``` qed ``` ballarin@27701 ` 2154` ballarin@27701 ` 2155` ``` have abnunit: "a \ b \ Units G" ``` ballarin@27701 ` 2156` ``` proof clarsimp ``` wenzelm@63832 ` 2157` ``` assume "a \ b \ Units G" ``` wenzelm@63832 ` 2158` ``` then have "a \ Units G" by (rule unit_factor) fact+ ``` wenzelm@63832 ` 2159` ``` with anunit show False .. ``` ballarin@27701 ` 2160` ``` qed ``` ballarin@27701 ` 2161` wenzelm@63847 ` 2162` ``` from factors_exist [OF acarr anunit] ``` wenzelm@63847 ` 2163` ``` obtain as where ascarr: "set as \ carrier G" and afac: "factors G as a" ``` wenzelm@63847 ` 2164` ``` by blast ``` wenzelm@63847 ` 2165` wenzelm@63847 ` 2166` ``` from factors_exist [OF bcarr bnunit] ``` wenzelm@63847 ` 2167` ``` obtain bs where bscarr: "set bs \ carrier G" and bfac: "factors G bs b" ``` wenzelm@63847 ` 2168` ``` by blast ``` wenzelm@63847 ` 2169` wenzelm@63847 ` 2170` ``` from factors_exist [OF ccarr cnunit] ``` wenzelm@63847 ` 2171` ``` obtain cs where cscarr: "set cs \ carrier G" and cfac: "factors G cs c" ``` wenzelm@63832 ` 2172` ``` by auto ``` ballarin@27701 ` 2173` ballarin@27701 ` 2174` ``` note [simp] = ascarr bscarr cscarr ``` ballarin@27701 ` 2175` wenzelm@63832 ` 2176` ``` from afac and bfac have abfac: "factors G (as @ bs) (a \ b)" ``` wenzelm@63832 ` 2177` ``` by (rule factors_mult) fact+ ``` wenzelm@63832 ` 2178` wenzelm@63832 ` 2179` ``` from pirr cfac have pcfac: "factors G (p # cs) (p \ c)" ``` wenzelm@63832 ` 2180` ``` by (rule factors_mult_single) fact+ ``` wenzelm@63832 ` 2181` ``` with abpc have abfac': "factors G (p # cs) (a \ b)" ``` wenzelm@63832 ` 2182` ``` by simp ``` wenzelm@63832 ` 2183` wenzelm@63832 ` 2184` ``` from abfac' abfac have "essentially_equal G (p # cs) (as @ bs)" ``` wenzelm@63832 ` 2185` ``` by (rule factors_unique) (fact | simp)+ ``` wenzelm@63847 ` 2186` ``` then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\] (as @ bs)" ``` wenzelm@63832 ` 2187` ``` by (fast elim: essentially_equalE) ``` ballarin@27701 ` 2188` ``` then have "p \ set ds" ``` wenzelm@63832 ` 2189` ``` by (simp add: perm_set_eq[symmetric]) ``` wenzelm@63847 ` 2190` ``` with dsassoc obtain p' where "p' \ set (as@bs)" and pp': "p \ p'" ``` wenzelm@63832 ` 2191` ``` unfolding list_all2_conv_all_nth set_conv_nth by force ``` wenzelm@63832 ` 2192` ``` then consider "p' \ set as" | "p' \ set bs" by auto ``` wenzelm@63832 ` 2193` ``` then show "p divides a \ p divides b" ``` wenzelm@63832 ` 2194` ``` proof cases ``` wenzelm@63832 ` 2195` ``` case 1 ``` wenzelm@32960 ` 2196` ``` with ascarr have [simp]: "p' \ carrier G" by fast ``` wenzelm@32960 ` 2197` wenzelm@32960 ` 2198` ``` note pp' ``` wenzelm@63832 ` 2199` ``` also from afac 1 have "p' divides a" by (rule factors_dividesI) fact+ ``` wenzelm@63832 ` 2200` ``` finally have "p divides a" by simp ``` wenzelm@63832 ` 2201` ``` then show ?thesis .. ``` wenzelm@63832 ` 2202` ``` next ``` wenzelm@63832 ` 2203` ``` case 2 ``` wenzelm@32960 ` 2204` ``` with bscarr have [simp]: "p' \ carrier G" by fast ``` wenzelm@32960 ` 2205` wenzelm@32960 ` 2206` ``` note pp' ``` wenzelm@32960 ` 2207` ``` also from bfac ``` wenzelm@63832 ` 2208` ``` have "p' divides b" by (rule factors_dividesI) fact+ ``` wenzelm@32960 ` 2209` ``` finally have "p divides b" by simp ``` wenzelm@63832 ` 2210` ``` then show ?thesis .. ``` wenzelm@63832 ` 2211` ``` qed ``` ballarin@27701 ` 2212` ``` qed ``` ballarin@27701 ` 2213` ``` qed ``` ballarin@27701 ` 2214` ```qed ``` ballarin@27701 ` 2215` ballarin@27701 ` 2216` wenzelm@61382 ` 2217` ```subsection \Greatest Common Divisors and Lowest Common Multiples\ ``` wenzelm@61382 ` 2218` wenzelm@61382 ` 2219` ```subsubsection \Definitions\ ``` ballarin@27701 ` 2220` wenzelm@63832 ` 2221` ```definition isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \ bool" ("(_ gcdof\ _ _)" [81,81,81] 80) ``` wenzelm@35848 ` 2222` ``` where "x gcdof\<^bsub>G\<^esub> a b \ x divides\<^bsub>G\<^esub> a \ x divides\<^bsub>G\<^esub> b \ ``` wenzelm@35847 ` 2223` ``` (\y\carrier G. (y divides\<^bsub>G\<^esub> a \ y divides\<^bsub>G\<^esub> b \ y divides\<^bsub>G\<^esub> x))" ``` wenzelm@35847 ` 2224` wenzelm@63832 ` 2225` ```definition islcm :: "[_, 'a, 'a, 'a] \ bool" ("(_ lcmof\ _ _)" [81,81,81] 80) ``` wenzelm@35848 ` 2226` ``` where "x lcmof\<^bsub>G\<^esub> a b \ a divides\<^bsub>G\<^esub> x \ b divides\<^bsub>G\<^esub> x \ ``` wenzelm@35847 ` 2227` ``` (\y\carrier G. (a divides\<^bsub>G\<^esub> y \ b divides\<^bsub>G\<^esub> y \ x divides\<^bsub>G\<^esub> y))" ``` wenzelm@35847 ` 2228` wenzelm@63832 ` 2229` ```definition somegcd :: "('a,_) monoid_scheme \ 'a \ 'a \ 'a" ``` wenzelm@35848 ` 2230` ``` where "somegcd G a b = (SOME x. x \ carrier G \ x gcdof\<^bsub>G\<^esub> a b)" ``` wenzelm@35847 ` 2231` wenzelm@63832 ` 2232` ```definition somelcm :: "('a,_) monoid_scheme \ 'a \ 'a \ 'a" ``` wenzelm@35848 ` 2233` ``` where "somelcm G a b = (SOME x. x \ carrier G \ x lcmof\<^bsub>G\<^esub> a b)" ``` wenzelm@35847 ` 2234` wenzelm@63832 ` 2235` ```definition "SomeGcd G A = inf (division_rel G) A" ``` ballarin@27701 ` 2236` ballarin@27701 ` 2237` ballarin@27701 ` 2238` ```locale gcd_condition_monoid = comm_monoid_cancel + ``` wenzelm@63832 ` 2239` ``` assumes gcdof_exists: "\a \ carrier G; b \ carrier G\ \ \c. c \ carrier G \ c gcdof a b" ``` ballarin@27701 ` 2240` ballarin@27701 ` 2241` ```locale primeness_condition_monoid = comm_monoid_cancel + ``` wenzelm@63832 ` 2242` ``` assumes irreducible_prime: "\a \ carrier G; irreducible G a\ \ prime G a" ``` ballarin@27701 ` 2243` ballarin@27701 ` 2244` ```locale divisor_chain_condition_monoid = comm_monoid_cancel + ``` wenzelm@63832 ` 2245` ``` assumes division_wellfounded: "wf {(x, y). x \ carrier G \ y \ carrier G \ properfactor G x y}" ``` ballarin@27701 ` 2246` ballarin@27701 ` 2247` wenzelm@61382 ` 2248` ```subsubsection \Connections to \texttt{Lattice.thy}\ ``` ballarin@27701 ` 2249` ballarin@27713 ` 2250` ```lemma gcdof_greatestLower: ``` ballarin@27701 ` 2251` ``` fixes G (structure) ``` ballarin@27701 ` 2252` ``` assumes carr[simp]: "a \ carrier G" "b \ carrier G" ``` wenzelm@63832 ` 2253` ``` shows "(x \ carrier G \ x gcdof a b) = greatest (division_rel G) x (Lower (division_rel G) {a, b})" ``` wenzelm@63832 ` 2254` ``` by (auto simp: isgcd_def greatest_def Lower_def elem_def) ``` ballarin@27701 ` 2255` ballarin@27713 ` 2256` ```lemma lcmof_leastUpper: ``` ballarin@27701 ` 2257` ``` fixes G (structure) ``` ballarin@27701 ` 2258` ``` assumes carr[simp]: "a \ carrier G" "b \ carrier G" ``` wenzelm@63832 ` 2259` ``` shows "(x \ carrier G \ x lcmof a b) = least (division_rel G) x (Upper (division_rel G) {a, b})" ``` wenzelm@63832 ` 2260` ``` by (auto simp: islcm_def least_def Upper_def elem_def) ``` ballarin@27701 ` 2261` ballarin@27713 ` 2262` ```lemma somegcd_meet: ``` ballarin@27701 ` 2263` ``` fixes G (structure) ``` ballarin@27701 ` 2264` ``` assumes carr: "a \ carrier G" "b \ carrier G" ``` ballarin@27713 ` 2265` ``` shows "somegcd G a b = meet (division_rel G) a b" ``` wenzelm@63832 ` 2266` ``` by (simp add: somegcd_def meet_def inf_def gcdof_greatestLower[OF carr]) ``` ballarin@27701 ` 2267` ballarin@27701 ` 2268` ```lemma (in monoid) isgcd_divides_l: ``` ballarin@27701 ` 2269` ``` assumes "a divides b" ``` ballarin@27701 ` 2270` ``` and "a \ carrier G" "b \ carrier G" ``` ballarin@27701 ` 2271` ``` shows "a gcdof a b" ``` wenzelm@63832 ` 2272` ``` using assms unfolding isgcd_def by fast ``` ballarin@27701 ` 2273` ballarin@27701 ` 2274` ```lemma (in monoid) isgcd_divides_r: ``` ballarin@27701 ` 2275` ``` assumes "b divides a" ``` ballarin@27701 ` 2276` ``` and "a \ carrier G" "b \ carrier G" ``` ballarin@27701 ` 2277` ``` shows "b gcdof a b" ``` wenzelm@63832 ` 2278` ``` using assms unfolding isgcd_def by fast ``` ballarin@27701 ` 2279` ballarin@27701 ` 2280` wenzelm@61382 ` 2281` ```subsubsection \Existence of gcd and lcm\ ``` ballarin@27701 ` 2282` ballarin@27701 ` 2283` ```lemma (in factorial_monoid) gcdof_exists: ``` wenzelm@63832 ` 2284` ``` assumes acarr: "a \ carrier G" ``` wenzelm@63832 ` 2285` ``` and bcarr: "b \ carrier G" ``` ballarin@27701 ` 2286` ``` shows "\c. c \ carrier G \ c gcdof a b" ``` ballarin@27701 ` 2287` ```proof - ``` wenzelm@63847 ` 2288` ``` from wfactors_exist [OF acarr] ``` wenzelm@63847 ` 2289` ``` obtain as where ascarr: "set as \ carrier G" and afs: "wfactors G as a" ``` wenzelm@63847 ` 2290` ``` by blast ``` wenzelm@63832 ` 2291` ``` from afs have airr: "\a \ set as. irreducible G a" ``` wenzelm@63832 ` 2292` ``` by (fast elim: wfactorsE) ``` wenzelm@63832 ` 2293` wenzelm@63847 ` 2294` ``` from wfactors_exist [OF bcarr] ``` wenzelm@63847 ` 2295` ``` obtain bs where bscarr: "set bs \ carrier G" and bfs: "wfactors G bs b" ``` wenzelm@63847 ` 2296` ``` by blast ``` wenzelm@63832 ` 2297` ``` from bfs have birr: "\b \ set bs. irreducible G b" ``` wenzelm@63832 ` 2298` ``` by (fast elim: wfactorsE) ``` wenzelm@63832 ` 2299` wenzelm@63832 ` 2300` ``` have "\c cs. c \ carrier G \ set cs \ carrier G \ wfactors G cs c \ ``` Mathias@63919 ` 2301` ``` fmset G cs = fmset G as \# fmset G bs" ``` ballarin@27701 ` 2302` ``` proof (intro mset_wfactorsEx) ``` ballarin@27701 ` 2303` ``` fix X ``` Mathias@63919 ` 2304` ``` assume "X \# fmset G as \# fmset G bs" ``` wenzelm@63832 ` 2305` ``` then have "X \# fmset G as" by simp ``` wenzelm@63832 ` 2306` ``` then have "X \ set (map (assocs G) as)" ``` wenzelm@63832 ` 2307` ``` by (simp add: fmset_def) ``` wenzelm@63832 ` 2308` ``` then have "\x. X = assocs G x \ x \ set as" ``` wenzelm@63832 ` 2309` ``` by (induct as) auto ``` wenzelm@63832 ` 2310` ``` then obtain x where X: "X = assocs G x" and xas: "x \ set as" ``` wenzelm@63847 ` 2311` ``` by blast ``` wenzelm@63832 ` 2312` ``` with ascarr have xcarr: "x \ carrier G" ``` wenzelm@63847 ` 2313` ``` by blast ``` wenzelm@63832 ` 2314` ``` from xas airr have xirr: "irreducible G x" ``` wenzelm@63832 ` 2315` ``` by simp ``` wenzelm@63832 ` 2316` ``` from xcarr and xirr and X show "\x. (x \ carrier G \ irreducible G x) \ X = assocs G x" ``` wenzelm@63847 ` 2317` ``` by blast ``` ballarin@27701 ` 2318` ``` qed ``` wenzelm@63832 ` 2319` ``` then obtain c cs ``` wenzelm@63832 ` 2320` ``` where ccarr: "c \ carrier G" ``` wenzelm@63832 ` 2321` ``` and cscarr: "set cs \ carrier G" ``` ballarin@27701 ` 2322` ``` and csirr: "wfactors G cs c" ``` Mathias@63919 ` 2323` ``` and csmset: "fmset G cs = fmset G as \# fmset G bs" ``` wenzelm@63832 ` 2324` ``` by auto ``` ballarin@27701 ` 2325` ballarin@27701 ` 2326` ``` have "c gcdof a b" ``` ballarin@27701 ` 2327` ``` proof (simp add: isgcd_def, safe) ``` ballarin@27701 ` 2328` ``` from csmset ``` haftmann@64587 ` 2329` ``` have "fmset G cs \# fmset G as" ``` wenzelm@63832 ` 2330` ``` by (simp add: multiset_inter_def subset_mset_def) ``` wenzelm@63832 ` 2331` ``` then show "c divides a" by (rule fmsubset_divides) fact+ ``` ballarin@27701 ` 2332` ``` next ``` haftmann@64587 ` 2333` ``` from csmset have "fmset G cs \# fmset G bs" ``` wenzelm@63832 ` 2334` ``` by (simp add: multiset_inter_def subseteq_mset_def, force) ``` wenzelm@63832 ` 2335` ``` then show "c divides b" ``` wenzelm@63832 ` 2336` ``` by (rule fmsubset_divides) fact+ ``` ballarin@27701 ` 2337` ``` next ``` ballarin@27701 ` 2338` ``` fix y ``` wenzelm@63847 ` 2339` ``` assume "y \ carrier G" ``` wenzelm@63847 ` 2340` ``` from wfactors_exist [OF this] ``` wenzelm@63847 ` 2341` ``` obtain ys where yscarr: "set ys \ carrier G" and yfs: "wfactors G ys y" ``` wenzelm@63847 ` 2342` ``` by blast ``` ballarin@27701 ` 2343` ballarin@27701 ` 2344` ``` assume "y divides a" ``` haftmann@64587 ` 2345` ``` then have ya: "fmset G ys \# fmset G as" ``` wenzelm@63832 ` 2346` ``` by (rule divides_fmsubset) fact+ ``` ballarin@27701 ` 2347` ballarin@27701 ` 2348` ``` assume "y divides b" ``` haftmann@64587 ` 2349` ``` then have yb: "fmset G ys \# fmset G bs" ``` wenzelm@63832 ` 2350` ``` by (rule divides_fmsubset) fact+ ``` wenzelm@63832 ` 2351` haftmann@64587 ` 2352` ``` from ya yb csmset have "fmset G ys \# fmset G cs" ``` wenzelm@63832 ` 2353` ``` by (simp add: subset_mset_def) ``` wenzelm@63832 ` 2354` ``` then show "y divides c" ``` wenzelm@63832 ` 2355` ``` by (rule fmsubset_divides) fact+ ``` ballarin@27701 ` 2356` ``` qed ``` wenzelm@63832 ` 2357` ``` with ccarr show "\c. c \ carrier G \ c gcdof a b" ``` wenzelm@63832 ` 2358` ``` by fast ``` ballarin@27701 ` 2359` ```qed ``` ballarin@27701 ` 2360` ballarin@27701 ` 2361` ```lemma (in factorial_monoid) lcmof_exists: ``` wenzelm@63832 ` 2362` ``` assumes acarr: "a \ carrier G" ``` wenzelm@63832 ` 2363` ``` and bcarr: "b \ carrier G" ``` ballarin@27701 ` 2364` ``` shows "\c. c \ carrier G \ c lcmof a b" ``` ballarin@27701 ` 2365` ```proof - ``` wenzelm@63847 ` 2366` ``` from wfactors_exist [OF acarr] ``` wenzelm@63847 ` 2367` ``` obtain as where ascarr: "set as \ carrier G" and afs: "wfactors G as a" ``` wenzelm@63847 ` 2368` ``` by blast ``` wenzelm@63832 ` 2369` ``` from afs have airr: "\a \ set as. irreducible G a" ``` wenzelm@63832 ` 2370` ``` by (fast elim: wfactorsE) ``` wenzelm@63832 ` 2371` wenzelm@63847 ` 2372` ``` from wfactors_exist [OF bcarr] ``` wenzelm@63847 ` 2373` ``` obtain bs where bscarr: "set bs \ carrier G" and bfs: "wfactors G bs b" ``` wenzelm@63847 ` 2374` ``` by blast ``` wenzelm@63832 ` 2375` ``` from bfs have birr: "\b \ set bs. irreducible G b" ``` wenzelm@63832 ` 2376` ``` by (fast elim: wfactorsE) ``` wenzelm@63832 ` 2377` wenzelm@63832 ` 2378` ``` have "\c cs. c \ carrier G \ set cs \ carrier G \ wfactors G cs c \ ``` wenzelm@63832 ` 2379` ``` fmset G cs = (fmset G as - fmset G bs) + fmset G bs" ``` ballarin@27701 ` 2380` ``` proof (intro mset_wfactorsEx) ``` ballarin@27701 ` 2381` ``` fix X ``` haftmann@62430 ` 2382` ``` assume "X \# (fmset G as - fmset G bs) + fmset G bs" ``` wenzelm@63832 ` 2383` ``` then have "X \# fmset G as \ X \# fmset G bs" ``` haftmann@62430 ` 2384` ``` by (auto dest: in_diffD) ``` wenzelm@63832 ` 2385` ``` then consider "X \ set_mset (fmset G as)" | "X \ set_mset (fmset G bs)" ``` wenzelm@63832 ` 2386` ``` by fast ``` wenzelm@63832 ` 2387` ``` then show "\x. (x \ carrier G \ irreducible G x) \ X = assocs G x" ``` wenzelm@63832 ` 2388` ``` proof cases ``` wenzelm@63832 ` 2389` ``` case 1 ``` wenzelm@63832 ` 2390` ``` then have "X \ set (map (assocs G) as)" by (simp add: fmset_def) ``` wenzelm@63832 ` 2391` ``` then have "\x. x \ set as \ X = assocs G x" by (induct as) auto ``` wenzelm@63832 ` 2392` ``` then obtain x where xas: "x \ set as" and X: "X = assocs G x" by auto ``` ballarin@27701 ` 2393` ``` with ascarr have xcarr: "x \ carrier G" by fast ``` ballarin@27701 ` 2394` ``` from xas airr have xirr: "irreducible G x" by simp ``` wenzelm@63832 ` 2395` ``` from xcarr and xirr and X show ?thesis by fast ``` wenzelm@63832 ` 2396` ``` next ``` wenzelm@63832 ` 2397` ``` case 2 ``` wenzelm@63832 ` 2398` ``` then have "X \ set (map (assocs G) bs)" by (simp add: fmset_def) ``` wenzelm@63832 ` 2399` ``` then have "\x. x \ set bs \ X = assocs G x" by (induct as) auto ``` wenzelm@63832 ` 2400` ``` then obtain x where xbs: "x \ set bs" and X: "X = assocs G x" by auto ``` ballarin@27701 ` 2401` ``` with bscarr have xcarr: "x \ carrier G" by fast ``` ballarin@27701 ` 2402` ``` from xbs birr have xirr: "irreducible G x" by simp ``` wenzelm@63832 ` 2403` ``` from xcarr and xirr and X show ?thesis by fast ``` wenzelm@63832 ` 2404` ``` qed ``` ballarin@27701 ` 2405` ``` qed ``` wenzelm@63832 ` 2406` ``` then obtain c cs ``` wenzelm@63832 ` 2407` ``` where ccarr: "c \ carrier G" ``` wenzelm@63832 ` 2408` ``` and cscarr: "set cs \ carrier G" ``` ballarin@27701 ` 2409` ``` and csirr: "wfactors G cs c" ``` wenzelm@63832 ` 2410` ``` and csmset: "fmset G cs = fmset G as - fmset G bs + fmset G bs" ``` wenzelm@63832 ` 2411` ``` by auto ``` ballarin@27701 ` 2412` ballarin@27701 ` 2413` ``` have "c lcmof a b" ``` ballarin@27701 ` 2414` ``` proof (simp add: islcm_def, safe) ``` haftmann@64587 ` 2415` ``` from csmset have "fmset G as \# fmset G cs" ``` wenzelm@63832 ` 2416` ``` by (simp add: subseteq_mset_def, force) ``` wenzelm@63832 ` 2417` ``` then show "a divides c" ``` wenzelm@63832 ` 2418` ``` by (rule fmsubset_divides) fact+ ``` ballarin@27701 ` 2419` ``` next ``` haftmann@64587 ` 2420` ``` from csmset have "fmset G bs \# fmset G cs" ``` wenzelm@63832 ` 2421` ``` by (simp add: subset_mset_def) ``` wenzelm@63832 ` 2422` ``` then show "b divides c" ``` wenzelm@63832 ` 2423` ``` by (rule fmsubset_divides) fact+ ``` ballarin@27701 ` 2424` ``` next ``` ballarin@27701 ` 2425` ``` fix y ``` wenzelm@63847 ` 2426` ``` assume "y \ carrier G" ``` wenzelm@63847 ` 2427` ``` from wfactors_exist [OF this] ``` wenzelm@63847 ` 2428` ``` obtain ys where yscarr: "set ys \ carrier G" and yfs: "wfactors G ys y" ``` wenzelm@63847 ` 2429` ``` by blast ``` ballarin@27701 ` 2430` ballarin@27701 ` 2431` ``` assume "a divides y" ``` haftmann@64587 ` 2432` ``` then have ya: "fmset G as \# fmset G ys" ``` wenzelm@63832 ` 2433` ``` by (rule divides_fmsubset) fact+ ``` ballarin@27701 ` 2434` ballarin@27701 ` 2435` ``` assume "b divides y" ``` haftmann@64587 ` 2436` ``` then have yb: "fmset G bs \# fmset G ys" ``` wenzelm@63832 ` 2437` ``` by (rule divides_fmsubset) fact+ ``` wenzelm@63832 ` 2438` haftmann@64587 ` 2439` ``` from ya yb csmset have "fmset G cs \# fmset G ys" ``` Mathias@60397 ` 2440` ``` apply (simp add: subseteq_mset_def, clarify) ``` ballarin@27701 ` 2441` ``` apply (case_tac "count (fmset G as) a < count (fmset G bs) a") ``` ballarin@27701 ` 2442` ``` apply simp ``` ballarin@27701 ` 2443` ``` apply simp ``` wenzelm@63832 ` 2444` ``` done ``` wenzelm@63832 ` 2445` ``` then show "c divides y" ``` wenzelm@63832 ` 2446` ``` by (rule fmsubset_divides) fact+ ``` ballarin@27701 ` 2447` ``` qed ``` wenzelm@63832 ` 2448` ``` with ccarr show "\c. c \ carrier G \ c lcmof a b" ``` wenzelm@63832 ` 2449` ``` by fast ``` ballarin@27701 ` 2450` ```qed ``` ballarin@27701 ` 2451` ballarin@27701 ` 2452` wenzelm@61382 ` 2453` ```subsection \Conditions for Factoriality\ ``` wenzelm@61382 ` 2454` wenzelm@61382 ` 2455` ```subsubsection \Gcd condition\ ``` ballarin@27701 ` 2456` ballarin@27713 ` 2457` ```lemma (in gcd_condition_monoid) division_weak_lower_semilattice [simp]: ``` wenzelm@63832 ` 2458` ``` "weak_lower_semilattice (division_rel G)" ``` ballarin@27701 ` 2459` ```proof - ``` ballarin@29237 ` 2460` ``` interpret weak_partial_order "division_rel G" .. ``` ballarin@27701 ` 2461` ``` show ?thesis ``` wenzelm@63832 ` 2462` ``` apply (unfold_locales, simp_all) ``` ballarin@27701 ` 2463` ``` proof - ``` ballarin@27701 ` 2464` ``` fix x y ``` ballarin@27701 ` 2465` ``` assume carr: "x \ carrier G" "y \ carrier G" ``` wenzelm@63847 ` 2466` ``` from gcdof_exists [OF this] obtain z where zcarr: "z \ carrier G" and isgcd: "z gcdof x y" ``` wenzelm@63847 ` 2467` ``` by blast ``` wenzelm@63832 ` 2468` ``` with carr have "greatest (division_rel G) z (Lower (division_rel G) {x, y})" ``` wenzelm@63832 ` 2469` ``` by (subst gcdof_greatestLower[symmetric], simp+) ``` wenzelm@63832 ` 2470` ``` then show "\z. greatest (division_rel G) z (Lower (division_rel G) {x, y})" ``` wenzelm@63832 ` 2471` ``` by fast ``` ballarin@27701 ` 2472` ``` qed ``` ballarin@27701 ` 2473` ```qed ``` ballarin@27701 ` 2474` ballarin@27701 ` 2475` ```lemma (in gcd_condition_monoid) gcdof_cong_l: ``` ballarin@27701 ` 2476` ``` assumes a'a: "a' \ a" ``` ballarin@27701 ` 2477` ``` and agcd: "a gcdof b c" ``` ballarin@27701 ` 2478` ``` and a'carr: "a' \ carrier G" and carr': "a \ carrier G" "b \ carrier G" "c \ carrier G" ``` ballarin@27701 ` 2479` ``` shows "a' gcdof b c" ``` ballarin@27701 ` 2480` ```proof - ``` ballarin@27701 ` 2481` ``` note carr = a'carr carr' ``` ballarin@29237 ` 2482` ``` interpret weak_lower_semilattice "division_rel G" by simp ``` ballarin@27701 ` 2483` ``` have "a' \ carrier G \ a' gcdof b c" ``` ballarin@27713 ` 2484` ``` apply (simp add: gcdof_greatestLower carr') ``` ballarin@27713 ` 2485` ``` apply (subst greatest_Lower_cong_l[of _ a]) ``` lp15@68004 ` 2486` ``` apply (simp_all add: a'a carr gcdof_greatestLower[symmetric] agcd) ``` wenzelm@63832 ` 2487` ``` done ``` wenzelm@63832 ` 2488` ``` then show ?thesis .. ``` ballarin@27701 ` 2489` ```qed ``` ballarin@27701 ` 2490` ballarin@27701 ` 2491` ```lemma (in gcd_condition_monoid) gcd_closed [simp]: ``` ballarin@27701 ` 2492` ``` assumes carr: "a \ carrier G" "b \ carrier G" ``` ballarin@27701 ` 2493` ``` shows "somegcd G a b \ carrier G" ``` ballarin@27701 ` 2494` ```proof - ``` ballarin@29237 ` 2495` ``` interpret weak_lower_semilattice "division_rel G" by simp ``` ballarin@27701 ` 2496` ``` show ?thesis ``` ballarin@27713 ` 2497` ``` apply (simp add: somegcd_meet[OF carr]) ``` ballarin@27713 ` 2498` ``` apply (rule meet_closed[simplified], fact+) ``` wenzelm@63832 ` 2499` ``` done ``` ballarin@27701 ` 2500` ```qed ``` ballarin@27701 ` 2501` ballarin@27701 ` 2502` ```lemma (in gcd_condition_monoid) gcd_isgcd: ``` ballarin@27701 ` 2503` ``` assumes carr: "a \ carrier G" "b \ carrier G" ``` ballarin@27701 ` 2504` ``` shows "(somegcd G a b) gcdof a b" ``` ballarin@27701 ` 2505` ```proof - ``` wenzelm@63832 ` 2506` ``` interpret weak_lower_semilattice "division_rel G" ``` wenzelm@63832 ` 2507` ``` by simp ``` wenzelm@63832 ` 2508` ``` from carr have "somegcd G a b \ carrier G \ (somegcd G a b) gcdof a b" ``` ballarin@27713 ` 2509` ``` apply (subst gcdof_greatestLower, simp, simp) ``` ballarin@27713 ` 2510` ``` apply (simp add: somegcd_meet[OF carr] meet_def) ``` ballarin@27713 ` 2511` ``` apply (rule inf_of_two_greatest[simplified], assumption+) ``` wenzelm@63832 ` 2512` ``` done ``` wenzelm@63832 ` 2513` ``` then show "(somegcd G a b) gcdof a b" ``` wenzelm@63832 ` 2514` ``` by simp ``` ballarin@27701 ` 2515` ```qed ``` ballarin@27701 ` 2516` ballarin@27701 ` 2517` ```lemma (in gcd_condition_monoid) gcd_exists: ``` ballarin@27701 ` 2518` ``` assumes carr: "a \ carrier G" "b \ carrier G" ``` ballarin@27701 ` 2519` ``` shows "\x\carrier G. x = somegcd G a b" ``` ballarin@27701 ` 2520` ```proof - ``` wenzelm@63832 ` 2521` ``` interpret weak_lower_semilattice "division_rel G" ``` wenzelm@63832 ` 2522` ``` by simp ``` ballarin@27701 ` 2523` ``` show ?thesis ``` lp15@55242 ` 2524` ``` by (metis carr(1) carr(2) gcd_closed) ``` ballarin@27701 ` 2525` ```qed ``` ballarin@27701 ` 2526` ballarin@27701 ` 2527` ```lemma (in gcd_condition_monoid) gcd_divides_l: ``` ballarin@27701 ` 2528` ``` assumes carr: "a \ carrier G" "b \ carrier G" ``` ballarin@27701 ` 2529` ``` shows "(somegcd G a b) divides a" ``` ballarin@27701 ` 2530` ```proof - ``` wenzelm@63832 ` 2531` ``` interpret weak_lower_semilattice "division_rel G" ``` wenzelm@63832 ` 2532` ``` by simp ``` ballarin@27701 ` 2533` ``` show ?thesis ``` lp15@55242 ` 2534` ``` by (metis carr(1) carr(2) gcd_isgcd isgcd_def) ``` ballarin@27701 ` 2535` ```qed ``` ballarin@27701 ` 2536` ballarin@27701 ` 2537` ```lemma (in gcd_condition_monoid) gcd_divides_r: ``` ballarin@27701 ` 2538` ``` assumes carr: "a \ carrier G" "b \ carrier G" ``` ballarin@27701 ` 2539` ``` shows "(somegcd G a b) divides b" ``` ballarin@27701 ` 2540` ```proof - ``` wenzelm@63832 ` 2541` ``` interpret weak_lower_semilattice "division_rel G" ``` wenzelm@63832 ` 2542` ``` by simp ``` ballarin@27701 ` 2543` ``` show ?thesis ``` lp15@55242 ` 2544` ``` by (metis carr gcd_isgcd isgcd_def) ``` ballarin@27701 ` 2545` ```qed ``` ballarin@27701 ` 2546` ballarin@27701 ` 2547` ```lemma (in gcd_condition_monoid) gcd_divides: ``` ballarin@27701 ` 2548` ``` assumes sub: "z divides x" "z divides y" ``` ballarin@27701 ` 2549` ``` and L: "x \ carrier G" "y \ carrier G" "z \ carrier G" ``` ballarin@27701 ` 2550` ``` shows "z divides (somegcd G x y)" ``` ballarin@27701 ` 2551` ```proof - ``` wenzelm@63832 ` 2552` ``` interpret weak_lower_semilattice "division_rel G" ``` wenzelm@63832 ` 2553` ``` by simp ``` ballarin@27701 ` 2554` ``` show ?thesis ``` lp15@55242 ` 2555` ``` by (metis gcd_isgcd isgcd_def assms) ``` ballarin@27701 ` 2556` ```qed ``` ballarin@27701 ` 2557` ballarin@27701 ` 2558` ```lemma (in gcd_condition_monoid) gcd_cong_l: ``` ballarin@27701 ` 2559` ``` assumes xx': "x \ x'" ``` ballarin@27701 ` 2560` ``` and carr: "x \ carrier G" "x' \ carrier G" "y \ carrier G" ``` ballarin@27701 ` 2561` ``` shows "somegcd G x y \ somegcd G x' y" ``` ballarin@27701 ` 2562` ```proof - ``` wenzelm@63832 ` 2563` ``` interpret weak_lower_semilattice "division_rel G" ``` wenzelm@63832 ` 2564` ``` by simp ``` ballarin@27701 ` 2565` ``` show ?thesis ``` ballarin@27713 ` 2566` ``` apply (simp add: somegcd_meet carr) ``` ballarin@27713 ` 2567` ``` apply (rule meet_cong_l[simplified], fact+) ``` wenzelm@63832 ` 2568` ``` done ``` ballarin@27701 ` 2569` ```qed ``` ballarin@27701 ` 2570` ballarin@27701 ` 2571` ```lemma (in gcd_condition_monoid) gcd_cong_r: ```