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