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