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