summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sun, 11 Sep 2016 00:13:25 +0200 | |

changeset 63832 | a400b127853c |

parent 63831 | ea7471c921f5 |

child 63833 | 4aaeb9427c96 |

misc tuning and modernization;

--- a/src/HOL/Algebra/Divisibility.thy Sat Sep 10 14:11:04 2016 +0200 +++ b/src/HOL/Algebra/Divisibility.thy Sun Sep 11 00:13:25 2016 +0200 @@ -6,7 +6,7 @@ section \<open>Divisibility in monoids and rings\<close> theory Divisibility -imports "~~/src/HOL/Library/Permutation" Coset Group + imports "~~/src/HOL/Library/Permutation" Coset Group begin section \<open>Factorial Monoids\<close> @@ -14,22 +14,16 @@ subsection \<open>Monoids with Cancellation Law\<close> locale monoid_cancel = monoid + - assumes l_cancel: - "\<lbrakk>c \<otimes> a = c \<otimes> b; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b" - and r_cancel: - "\<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b" + assumes l_cancel: "\<lbrakk>c \<otimes> a = c \<otimes> b; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b" + and r_cancel: "\<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b" lemma (in monoid) monoid_cancelI: - assumes l_cancel: - "\<And>a b c. \<lbrakk>c \<otimes> a = c \<otimes> b; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b" - and r_cancel: - "\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b" + assumes l_cancel: "\<And>a b c. \<lbrakk>c \<otimes> a = c \<otimes> b; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b" + and r_cancel: "\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b" shows "monoid_cancel G" by standard fact+ -lemma (in monoid_cancel) is_monoid_cancel: - "monoid_cancel G" - .. +lemma (in monoid_cancel) is_monoid_cancel: "monoid_cancel G" .. sublocale group \<subseteq> monoid_cancel by standard simp_all @@ -40,8 +34,7 @@ lemma comm_monoid_cancelI: fixes G (structure) assumes "comm_monoid G" - assumes cancel: - "\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b" + assumes cancel: "\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b" shows "comm_monoid_cancel G" proof - interpret comm_monoid G by fact @@ -49,50 +42,51 @@ by unfold_locales (metis assms(2) m_ac(2))+ qed -lemma (in comm_monoid_cancel) is_comm_monoid_cancel: - "comm_monoid_cancel G" +lemma (in comm_monoid_cancel) is_comm_monoid_cancel: "comm_monoid_cancel G" by intro_locales -sublocale comm_group \<subseteq> comm_monoid_cancel - .. +sublocale comm_group \<subseteq> comm_monoid_cancel .. subsection \<open>Products of Units in Monoids\<close> lemma (in monoid) Units_m_closed[simp, intro]: - assumes h1unit: "h1 \<in> Units G" and h2unit: "h2 \<in> Units G" + assumes h1unit: "h1 \<in> Units G" + and h2unit: "h2 \<in> Units G" shows "h1 \<otimes> h2 \<in> Units G" -unfolding Units_def -using assms -by auto (metis Units_inv_closed Units_l_inv Units_m_closed Units_r_inv) + unfolding Units_def + using assms + by auto (metis Units_inv_closed Units_l_inv Units_m_closed Units_r_inv) lemma (in monoid) prod_unit_l: - assumes abunit[simp]: "a \<otimes> b \<in> Units G" and aunit[simp]: "a \<in> Units G" + assumes abunit[simp]: "a \<otimes> b \<in> Units G" + and aunit[simp]: "a \<in> Units G" and carr[simp]: "a \<in> carrier G" "b \<in> carrier G" shows "b \<in> Units G" proof - have c: "inv (a \<otimes> b) \<otimes> a \<in> carrier G" by simp - have "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = inv (a \<otimes> b) \<otimes> (a \<otimes> b)" by (simp add: m_assoc) + have "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = inv (a \<otimes> b) \<otimes> (a \<otimes> b)" + by (simp add: m_assoc) also have "\<dots> = \<one>" by simp finally have li: "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = \<one>" . have "\<one> = inv a \<otimes> a" by (simp add: Units_l_inv[symmetric]) also have "\<dots> = inv a \<otimes> \<one> \<otimes> a" by simp also have "\<dots> = inv a \<otimes> ((a \<otimes> b) \<otimes> inv (a \<otimes> b)) \<otimes> a" - by (simp add: Units_r_inv[OF abunit, symmetric] del: Units_r_inv) + by (simp add: Units_r_inv[OF abunit, symmetric] del: Units_r_inv) also have "\<dots> = ((inv a \<otimes> a) \<otimes> b) \<otimes> inv (a \<otimes> b) \<otimes> a" by (simp add: m_assoc del: Units_l_inv) also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by simp also have "\<dots> = b \<otimes> (inv (a \<otimes> b) \<otimes> a)" by (simp add: m_assoc) finally have ri: "b \<otimes> (inv (a \<otimes> b) \<otimes> a) = \<one> " by simp - from c li ri - show "b \<in> Units G" by (simp add: Units_def, fast) + from c li ri show "b \<in> Units G" by (auto simp: Units_def) qed lemma (in monoid) prod_unit_r: - assumes abunit[simp]: "a \<otimes> b \<in> Units G" and bunit[simp]: "b \<in> Units G" + assumes abunit[simp]: "a \<otimes> b \<in> Units G" + and bunit[simp]: "b \<in> Units G" and carr[simp]: "a \<in> carrier G" "b \<in> carrier G" shows "a \<in> Units G" proof - @@ -105,42 +99,39 @@ have "\<one> = b \<otimes> inv b" by (simp add: Units_r_inv[symmetric]) also have "\<dots> = b \<otimes> \<one> \<otimes> inv b" by simp - also have "\<dots> = b \<otimes> (inv (a \<otimes> b) \<otimes> (a \<otimes> b)) \<otimes> inv b" - by (simp add: Units_l_inv[OF abunit, symmetric] del: Units_l_inv) + also have "\<dots> = b \<otimes> (inv (a \<otimes> b) \<otimes> (a \<otimes> b)) \<otimes> inv b" + by (simp add: Units_l_inv[OF abunit, symmetric] del: Units_l_inv) also have "\<dots> = (b \<otimes> inv (a \<otimes> b) \<otimes> a) \<otimes> (b \<otimes> inv b)" by (simp add: m_assoc del: Units_l_inv) also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by simp finally have ri: "(b \<otimes> inv (a \<otimes> b)) \<otimes> a = \<one> " by simp - from c li ri - show "a \<in> Units G" by (simp add: Units_def, fast) + from c li ri show "a \<in> Units G" by (auto simp: Units_def) qed lemma (in comm_monoid) unit_factor: assumes abunit: "a \<otimes> b \<in> Units G" and [simp]: "a \<in> carrier G" "b \<in> carrier G" shows "a \<in> Units G" -using abunit[simplified Units_def] + using abunit[simplified Units_def] proof clarsimp fix i assume [simp]: "i \<in> carrier G" - and li: "i \<otimes> (a \<otimes> b) = \<one>" - and ri: "a \<otimes> b \<otimes> i = \<one>" have carr': "b \<otimes> i \<in> carrier G" by simp have "(b \<otimes> i) \<otimes> a = (i \<otimes> b) \<otimes> a" by (simp add: m_comm) also have "\<dots> = i \<otimes> (b \<otimes> a)" by (simp add: m_assoc) also have "\<dots> = i \<otimes> (a \<otimes> b)" by (simp add: m_comm) - also note li + also assume "i \<otimes> (a \<otimes> b) = \<one>" finally have li': "(b \<otimes> i) \<otimes> a = \<one>" . have "a \<otimes> (b \<otimes> i) = a \<otimes> b \<otimes> i" by (simp add: m_assoc) - also note ri + also assume "a \<otimes> b \<otimes> i = \<one>" finally have ri': "a \<otimes> (b \<otimes> i) = \<one>" . from carr' li' ri' - show "a \<in> Units G" by (simp add: Units_def, fast) + show "a \<in> Units G" by (simp add: Units_def, fast) qed @@ -148,29 +139,23 @@ subsubsection \<open>Function definitions\<close> -definition - factor :: "[_, 'a, 'a] \<Rightarrow> bool" (infix "divides\<index>" 65) +definition factor :: "[_, 'a, 'a] \<Rightarrow> bool" (infix "divides\<index>" 65) where "a divides\<^bsub>G\<^esub> b \<longleftrightarrow> (\<exists>c\<in>carrier G. b = a \<otimes>\<^bsub>G\<^esub> c)" -definition - associated :: "[_, 'a, 'a] => bool" (infix "\<sim>\<index>" 55) +definition associated :: "[_, 'a, 'a] \<Rightarrow> bool" (infix "\<sim>\<index>" 55) where "a \<sim>\<^bsub>G\<^esub> b \<longleftrightarrow> a divides\<^bsub>G\<^esub> b \<and> b divides\<^bsub>G\<^esub> a" -abbreviation - "division_rel G == \<lparr>carrier = carrier G, eq = op \<sim>\<^bsub>G\<^esub>, le = op divides\<^bsub>G\<^esub>\<rparr>" - -definition - properfactor :: "[_, 'a, 'a] \<Rightarrow> bool" +abbreviation "division_rel G \<equiv> \<lparr>carrier = carrier G, eq = op \<sim>\<^bsub>G\<^esub>, le = op divides\<^bsub>G\<^esub>\<rparr>" + +definition properfactor :: "[_, 'a, 'a] \<Rightarrow> bool" where "properfactor G a b \<longleftrightarrow> a divides\<^bsub>G\<^esub> b \<and> \<not>(b divides\<^bsub>G\<^esub> a)" -definition - irreducible :: "[_, 'a] \<Rightarrow> bool" +definition irreducible :: "[_, 'a] \<Rightarrow> bool" where "irreducible G a \<longleftrightarrow> a \<notin> Units G \<and> (\<forall>b\<in>carrier G. properfactor G b a \<longrightarrow> b \<in> Units G)" -definition - prime :: "[_, 'a] \<Rightarrow> bool" where - "prime G p \<longleftrightarrow> - p \<notin> Units G \<and> +definition prime :: "[_, 'a] \<Rightarrow> bool" + where "prime G p \<longleftrightarrow> + p \<notin> Units G \<and> (\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. p divides\<^bsub>G\<^esub> (a \<otimes>\<^bsub>G\<^esub> b) \<longrightarrow> p divides\<^bsub>G\<^esub> a \<or> p divides\<^bsub>G\<^esub> b)" @@ -181,24 +166,20 @@ assumes carr: "c \<in> carrier G" and p: "b = a \<otimes> c" shows "a divides b" -unfolding factor_def -using assms by fast + unfolding factor_def using assms by fast lemma dividesI' [intro]: - fixes G (structure) + fixes G (structure) assumes p: "b = a \<otimes> c" and carr: "c \<in> carrier G" shows "a divides b" -using assms -by (fast intro: dividesI) + using assms by (fast intro: dividesI) lemma dividesD: fixes G (structure) assumes "a divides b" shows "\<exists>c\<in>carrier G. b = a \<otimes> c" -using assms -unfolding factor_def -by fast + using assms unfolding factor_def by fast lemma dividesE [elim]: fixes G (structure) @@ -207,106 +188,93 @@ shows "P" proof - from dividesD[OF d] - obtain c - where "c\<in>carrier G" - and "b = a \<otimes> c" - by auto - thus "P" by (elim elim) + obtain c where "c \<in> carrier G" and "b = a \<otimes> c" by auto + then show P by (elim elim) qed lemma (in monoid) divides_refl[simp, intro!]: assumes carr: "a \<in> carrier G" shows "a divides a" -apply (intro dividesI[of "\<one>"]) -apply (simp, simp add: carr) -done + by (intro dividesI[of "\<one>"]) (simp_all add: carr) lemma (in monoid) divides_trans [trans]: assumes dvds: "a divides b" "b divides c" and acarr: "a \<in> carrier G" shows "a divides c" -using dvds[THEN dividesD] -by (blast intro: dividesI m_assoc acarr) + using dvds[THEN dividesD] by (blast intro: dividesI m_assoc acarr) lemma (in monoid) divides_mult_lI [intro]: assumes ab: "a divides b" and carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" shows "(c \<otimes> a) divides (c \<otimes> b)" -using ab -apply (elim dividesE, simp add: m_assoc[symmetric] carr) -apply (fast intro: dividesI) -done + using ab + apply (elim dividesE) + apply (simp add: m_assoc[symmetric] carr) + apply (fast intro: dividesI) + done lemma (in monoid_cancel) divides_mult_l [simp]: assumes carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" shows "(c \<otimes> a) divides (c \<otimes> b) = a divides b" -apply safe - apply (elim dividesE, intro dividesI, assumption) - apply (rule l_cancel[of c]) - apply (simp add: m_assoc carr)+ -apply (fast intro: carr) -done + apply safe + apply (elim dividesE, intro dividesI, assumption) + apply (rule l_cancel[of c]) + apply (simp add: m_assoc carr)+ + apply (fast intro: carr) + done lemma (in comm_monoid) divides_mult_rI [intro]: assumes ab: "a divides b" and carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" shows "(a \<otimes> c) divides (b \<otimes> c)" -using carr ab -apply (simp add: m_comm[of a c] m_comm[of b c]) -apply (rule divides_mult_lI, assumption+) -done + using carr ab + apply (simp add: m_comm[of a c] m_comm[of b c]) + apply (rule divides_mult_lI, assumption+) + done lemma (in comm_monoid_cancel) divides_mult_r [simp]: assumes carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" shows "(a \<otimes> c) divides (b \<otimes> c) = a divides b" -using carr -by (simp add: m_comm[of a c] m_comm[of b c]) + using carr by (simp add: m_comm[of a c] m_comm[of b c]) lemma (in monoid) divides_prod_r: assumes ab: "a divides b" and carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" shows "a divides (b \<otimes> c)" -using ab carr -by (fast intro: m_assoc) + using ab carr by (fast intro: m_assoc) lemma (in comm_monoid) divides_prod_l: assumes carr[intro]: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" and ab: "a divides b" shows "a divides (c \<otimes> b)" -using ab carr -apply (simp add: m_comm[of c b]) -apply (fast intro: divides_prod_r) -done + using ab carr + apply (simp add: m_comm[of c b]) + apply (fast intro: divides_prod_r) + done lemma (in monoid) unit_divides: assumes uunit: "u \<in> Units G" - and acarr: "a \<in> carrier G" + and acarr: "a \<in> carrier G" shows "u divides a" proof (intro dividesI[of "(inv u) \<otimes> a"], fast intro: uunit acarr) - from uunit acarr - have xcarr: "inv u \<otimes> a \<in> carrier G" by fast - - from uunit acarr - have "u \<otimes> (inv u \<otimes> a) = (u \<otimes> inv u) \<otimes> a" by (fast intro: m_assoc[symmetric]) + from uunit acarr have xcarr: "inv u \<otimes> a \<in> carrier G" by fast + from uunit acarr have "u \<otimes> (inv u \<otimes> a) = (u \<otimes> inv u) \<otimes> a" + by (fast intro: m_assoc[symmetric]) also have "\<dots> = \<one> \<otimes> a" by (simp add: Units_r_inv[OF uunit]) - also from acarr - have "\<dots> = a" by simp - finally - show "a = u \<otimes> (inv u \<otimes> a)" .. + also from acarr have "\<dots> = a" by simp + finally show "a = u \<otimes> (inv u \<otimes> a)" .. qed lemma (in comm_monoid) divides_unit: assumes udvd: "a divides u" - and carr: "a \<in> carrier G" "u \<in> Units G" + and carr: "a \<in> carrier G" "u \<in> Units G" shows "a \<in> Units G" -using udvd carr -by (blast intro: unit_factor) + using udvd carr by (blast intro: unit_factor) lemma (in comm_monoid) Unit_eq_dividesone: assumes ucarr: "u \<in> carrier G" shows "u \<in> Units G = u divides \<one>" -using ucarr -by (fast dest: divides_unit intro: unit_divides) + using ucarr by (fast dest: divides_unit intro: unit_divides) subsubsection \<open>Association\<close> @@ -315,83 +283,71 @@ fixes G (structure) assumes "a divides b" "b divides a" shows "a \<sim> b" -using assms -by (simp add: associated_def) + using assms by (simp add: associated_def) lemma (in monoid) associatedI2: assumes uunit[simp]: "u \<in> Units G" and a: "a = b \<otimes> u" and bcarr[simp]: "b \<in> carrier G" shows "a \<sim> b" -using uunit bcarr -unfolding a -apply (intro associatedI) - apply (rule dividesI[of "inv u"], simp) - apply (simp add: m_assoc Units_closed) -apply fast -done + using uunit bcarr + unfolding a + apply (intro associatedI) + apply (rule dividesI[of "inv u"], simp) + apply (simp add: m_assoc Units_closed) + apply fast + done lemma (in monoid) associatedI2': - assumes a: "a = b \<otimes> u" - and uunit: "u \<in> Units G" - and bcarr: "b \<in> carrier G" + assumes "a = b \<otimes> u" + and "u \<in> Units G" + and "b \<in> carrier G" shows "a \<sim> b" -using assms by (intro associatedI2) + using assms by (intro associatedI2) lemma associatedD: fixes G (structure) assumes "a \<sim> b" shows "a divides b" -using assms by (simp add: associated_def) + using assms by (simp add: associated_def) lemma (in monoid_cancel) associatedD2: assumes assoc: "a \<sim> b" and carr: "a \<in> carrier G" "b \<in> carrier G" shows "\<exists>u\<in>Units G. a = b \<otimes> u" -using assoc -unfolding associated_def + using assoc + unfolding associated_def proof clarify assume "b divides a" - hence "\<exists>u\<in>carrier G. a = b \<otimes> u" by (rule dividesD) - from this obtain u - where ucarr: "u \<in> carrier G" and a: "a = b \<otimes> u" - by auto + then have "\<exists>u\<in>carrier G. a = b \<otimes> u" by (rule dividesD) + then obtain u where ucarr: "u \<in> carrier G" and a: "a = b \<otimes> u" + by auto assume "a divides b" - hence "\<exists>u'\<in>carrier G. b = a \<otimes> u'" by (rule dividesD) - from this obtain u' - where u'carr: "u' \<in> carrier G" and b: "b = a \<otimes> u'" - by auto + then have "\<exists>u'\<in>carrier G. b = a \<otimes> u'" by (rule dividesD) + then obtain u' where u'carr: "u' \<in> carrier G" and b: "b = a \<otimes> u'" + by auto note carr = carr ucarr u'carr - from carr - have "a \<otimes> \<one> = a" by simp + from carr have "a \<otimes> \<one> = a" by simp also have "\<dots> = b \<otimes> u" by (simp add: a) also have "\<dots> = a \<otimes> u' \<otimes> u" by (simp add: b) - also from carr - have "\<dots> = a \<otimes> (u' \<otimes> u)" by (simp add: m_assoc) - finally - have "a \<otimes> \<one> = a \<otimes> (u' \<otimes> u)" . - with carr - have u1: "\<one> = u' \<otimes> u" by (fast dest: l_cancel) - - from carr - have "b \<otimes> \<one> = b" by simp + also from carr have "\<dots> = a \<otimes> (u' \<otimes> u)" by (simp add: m_assoc) + finally have "a \<otimes> \<one> = a \<otimes> (u' \<otimes> u)" . + with carr have u1: "\<one> = u' \<otimes> u" by (fast dest: l_cancel) + + from carr have "b \<otimes> \<one> = b" by simp also have "\<dots> = a \<otimes> u'" by (simp add: b) also have "\<dots> = b \<otimes> u \<otimes> u'" by (simp add: a) - also from carr - have "\<dots> = b \<otimes> (u \<otimes> u')" by (simp add: m_assoc) - finally - have "b \<otimes> \<one> = b \<otimes> (u \<otimes> u')" . - with carr - have u2: "\<one> = u \<otimes> u'" by (fast dest: l_cancel) - - from u'carr u1[symmetric] u2[symmetric] - have "\<exists>u'\<in>carrier G. u' \<otimes> u = \<one> \<and> u \<otimes> u' = \<one>" by fast - hence "u \<in> Units G" by (simp add: Units_def ucarr) - - from ucarr this a - show "\<exists>u\<in>Units G. a = b \<otimes> u" by fast + also from carr have "\<dots> = b \<otimes> (u \<otimes> u')" by (simp add: m_assoc) + finally have "b \<otimes> \<one> = b \<otimes> (u \<otimes> u')" . + with carr have u2: "\<one> = u \<otimes> u'" by (fast dest: l_cancel) + + from u'carr u1[symmetric] u2[symmetric] have "\<exists>u'\<in>carrier G. u' \<otimes> u = \<one> \<and> u \<otimes> u' = \<one>" + by fast + then have "u \<in> Units G" + by (simp add: Units_def ucarr) + with ucarr a show "\<exists>u\<in>Units G. a = b \<otimes> u" by fast qed lemma associatedE: @@ -400,10 +356,9 @@ and e: "\<lbrakk>a divides b; b divides a\<rbrakk> \<Longrightarrow> P" shows "P" proof - - from assoc - have "a divides b" "b divides a" - by (simp add: associated_def)+ - thus "P" by (elim e) + from assoc have "a divides b" "b divides a" + by (simp_all add: associated_def) + then show P by (elim e) qed lemma (in monoid_cancel) associatedE2: @@ -412,39 +367,34 @@ and carr: "a \<in> carrier G" "b \<in> carrier G" shows "P" proof - - from assoc and carr - have "\<exists>u\<in>Units G. a = b \<otimes> u" by (rule associatedD2) - from this obtain u - where "u \<in> Units G" "a = b \<otimes> u" - by auto - thus "P" by (elim e) + from assoc and carr have "\<exists>u\<in>Units G. a = b \<otimes> u" + by (rule associatedD2) + then obtain u where "u \<in> Units G" "a = b \<otimes> u" + by auto + then show P by (elim e) qed lemma (in monoid) associated_refl [simp, intro!]: assumes "a \<in> carrier G" shows "a \<sim> a" -using assms -by (fast intro: associatedI) + using assms by (fast intro: associatedI) lemma (in monoid) associated_sym [sym]: assumes "a \<sim> b" and "a \<in> carrier G" "b \<in> carrier G" shows "b \<sim> a" -using assms -by (iprover intro: associatedI elim: associatedE) + using assms by (iprover intro: associatedI elim: associatedE) lemma (in monoid) associated_trans [trans]: assumes "a \<sim> b" "b \<sim> c" and "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" shows "a \<sim> c" -using assms -by (iprover intro: associatedI divides_trans elim: associatedE) - -lemma (in monoid) division_equiv [intro, simp]: - "equivalence (division_rel G)" + using assms by (iprover intro: associatedI divides_trans elim: associatedE) + +lemma (in monoid) division_equiv [intro, simp]: "equivalence (division_rel G)" apply unfold_locales - apply simp_all - apply (metis associated_def) + apply simp_all + apply (metis associated_def) apply (iprover intro: associated_trans) done @@ -456,152 +406,143 @@ assumes "a divides b" "b divides a" and "a \<in> carrier G" "b \<in> carrier G" shows "a \<sim> b" -using assms -by (fast intro: associatedI) + using assms by (fast intro: associatedI) lemma (in monoid) divides_cong_l [trans]: - assumes xx': "x \<sim> x'" - and xdvdy: "x' divides y" - and carr [simp]: "x \<in> carrier G" "x' \<in> carrier G" "y \<in> carrier G" + assumes "x \<sim> x'" + and "x' divides y" + and [simp]: "x \<in> carrier G" "x' \<in> carrier G" "y \<in> carrier G" shows "x divides y" proof - - from xx' - have "x divides x'" by (simp add: associatedD) - also note xdvdy - finally - show "x divides y" by simp + from assms(1) have "x divides x'" by (simp add: associatedD) + also note assms(2) + finally show "x divides y" by simp qed lemma (in monoid) divides_cong_r [trans]: - assumes xdvdy: "x divides y" - and yy': "y \<sim> y'" - and carr[simp]: "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G" + assumes "x divides y" + and "y \<sim> y'" + and [simp]: "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G" shows "x divides y'" proof - - note xdvdy - also from yy' - have "y divides y'" by (simp add: associatedD) - finally - show "x divides y'" by simp + note assms(1) + also from assms(2) have "y divides y'" by (simp add: associatedD) + finally show "x divides y'" by simp qed lemma (in monoid) division_weak_partial_order [simp, intro!]: "weak_partial_order (division_rel G)" apply unfold_locales - apply simp_all - apply (simp add: associated_sym) - apply (blast intro: associated_trans) - apply (simp add: divides_antisym) - apply (blast intro: divides_trans) + apply simp_all + apply (simp add: associated_sym) + apply (blast intro: associated_trans) + apply (simp add: divides_antisym) + apply (blast intro: divides_trans) apply (blast intro: divides_cong_l divides_cong_r associated_sym) done - + subsubsection \<open>Multiplication and associativity\<close> lemma (in monoid_cancel) mult_cong_r: assumes "b \<sim> b'" and carr: "a \<in> carrier G" "b \<in> carrier G" "b' \<in> carrier G" shows "a \<otimes> b \<sim> a \<otimes> b'" -using assms -apply (elim associatedE2, intro associatedI2) -apply (auto intro: m_assoc[symmetric]) -done + using assms + apply (elim associatedE2, intro associatedI2) + apply (auto intro: m_assoc[symmetric]) + done lemma (in comm_monoid_cancel) mult_cong_l: assumes "a \<sim> a'" and carr: "a \<in> carrier G" "a' \<in> carrier G" "b \<in> carrier G" shows "a \<otimes> b \<sim> a' \<otimes> b" -using assms -apply (elim associatedE2, intro associatedI2) - apply assumption - apply (simp add: m_assoc Units_closed) - apply (simp add: m_comm Units_closed) - apply simp+ -done + using assms + apply (elim associatedE2, intro associatedI2) + apply assumption + apply (simp add: m_assoc Units_closed) + apply (simp add: m_comm Units_closed) + apply simp_all + done lemma (in monoid_cancel) assoc_l_cancel: assumes carr: "a \<in> carrier G" "b \<in> carrier G" "b' \<in> carrier G" and "a \<otimes> b \<sim> a \<otimes> b'" shows "b \<sim> b'" -using assms -apply (elim associatedE2, intro associatedI2) - apply assumption - apply (rule l_cancel[of a]) - apply (simp add: m_assoc Units_closed) - apply fast+ -done + using assms + apply (elim associatedE2, intro associatedI2) + apply assumption + apply (rule l_cancel[of a]) + apply (simp add: m_assoc Units_closed) + apply fast+ + done lemma (in comm_monoid_cancel) assoc_r_cancel: assumes "a \<otimes> b \<sim> a' \<otimes> b" and carr: "a \<in> carrier G" "a' \<in> carrier G" "b \<in> carrier G" shows "a \<sim> a'" -using assms -apply (elim associatedE2, intro associatedI2) - apply assumption - apply (rule r_cancel[of a b]) - apply (metis Units_closed assms(3) assms(4) m_ac) - apply fast+ -done + using assms + apply (elim associatedE2, intro associatedI2) + apply assumption + apply (rule r_cancel[of a b]) + apply (metis Units_closed assms(3) assms(4) m_ac) + apply fast+ + done subsubsection \<open>Units\<close> lemma (in monoid_cancel) assoc_unit_l [trans]: - assumes asc: "a \<sim> b" and bunit: "b \<in> Units G" - and carr: "a \<in> carrier G" + assumes "a \<sim> b" + and "b \<in> Units G" + and "a \<in> carrier G" shows "a \<in> Units G" -using assms -by (fast elim: associatedE2) + using assms by (fast elim: associatedE2) lemma (in monoid_cancel) assoc_unit_r [trans]: - assumes aunit: "a \<in> Units G" and asc: "a \<sim> b" + assumes aunit: "a \<in> Units G" + and asc: "a \<sim> b" and bcarr: "b \<in> carrier G" shows "b \<in> Units G" -using aunit bcarr associated_sym[OF asc] -by (blast intro: assoc_unit_l) + using aunit bcarr associated_sym[OF asc] by (blast intro: assoc_unit_l) lemma (in comm_monoid) Units_cong: assumes aunit: "a \<in> Units G" and asc: "a \<sim> b" and bcarr: "b \<in> carrier G" shows "b \<in> Units G" -using assms -by (blast intro: divides_unit elim: associatedE) + using assms by (blast intro: divides_unit elim: associatedE) lemma (in monoid) Units_assoc: assumes units: "a \<in> Units G" "b \<in> Units G" shows "a \<sim> b" -using units -by (fast intro: associatedI unit_divides) - -lemma (in monoid) Units_are_ones: - "Units G {.=}\<^bsub>(division_rel G)\<^esub> {\<one>}" -apply (simp add: set_eq_def elem_def, rule, simp_all) + using units by (fast intro: associatedI unit_divides) + +lemma (in monoid) Units_are_ones: "Units G {.=}\<^bsub>(division_rel G)\<^esub> {\<one>}" + apply (simp add: set_eq_def elem_def, rule, simp_all) proof clarsimp fix a assume aunit: "a \<in> Units G" show "a \<sim> \<one>" - apply (rule associatedI) - apply (fast intro: dividesI[of "inv a"] aunit Units_r_inv[symmetric]) - apply (fast intro: dividesI[of "a"] l_one[symmetric] Units_closed[OF aunit]) - done + apply (rule associatedI) + apply (fast intro: dividesI[of "inv a"] aunit Units_r_inv[symmetric]) + apply (fast intro: dividesI[of "a"] l_one[symmetric] Units_closed[OF aunit]) + done next have "\<one> \<in> Units G" by simp moreover have "\<one> \<sim> \<one>" by simp ultimately show "\<exists>a \<in> Units G. \<one> \<sim> a" by fast qed -lemma (in comm_monoid) Units_Lower: - "Units G = Lower (division_rel G) (carrier G)" -apply (simp add: Units_def Lower_def) -apply (rule, rule) - apply clarsimp - apply (rule unit_divides) - apply (unfold Units_def, fast) - apply assumption -apply clarsimp -apply (metis Unit_eq_dividesone Units_r_inv_ex m_ac(2) one_closed) -done +lemma (in comm_monoid) Units_Lower: "Units G = Lower (division_rel G) (carrier G)" + apply (simp add: Units_def Lower_def) + apply (rule, rule) + apply clarsimp + apply (rule unit_divides) + apply (unfold Units_def, fast) + apply assumption + apply clarsimp + apply (metis Unit_eq_dividesone Units_r_inv_ex m_ac(2) one_closed) + done subsubsection \<open>Proper factors\<close> @@ -611,16 +552,14 @@ assumes "a divides b" and "\<not>(b divides a)" shows "properfactor G a b" -using assms -unfolding properfactor_def -by simp + using assms unfolding properfactor_def by simp lemma properfactorI2: fixes G (structure) assumes advdb: "a divides b" and neq: "\<not>(a \<sim> b)" shows "properfactor G a b" -apply (rule properfactorI, rule advdb) + apply (rule properfactorI, rule advdb) proof (rule ccontr, simp) assume "b divides a" with advdb have "a \<sim> b" by (rule associatedI) @@ -632,9 +571,9 @@ and nunit: "b \<notin> Units G" and carr: "a \<in> carrier G" "b \<in> carrier G" "p \<in> carrier G" shows "properfactor G a p" -unfolding p -using carr -apply (intro properfactorI, fast) + unfolding p + using carr + apply (intro properfactorI, fast) proof (clarsimp, elim dividesE) fix c assume ccarr: "c \<in> carrier G" @@ -645,14 +584,13 @@ also have "\<dots> = a \<otimes> (b \<otimes> c)" by (simp add: m_assoc) finally have "a \<otimes> \<one> = a \<otimes> (b \<otimes> c)" . - hence rinv: "\<one> = b \<otimes> c" by (intro l_cancel[of "a" "\<one>" "b \<otimes> c"], simp+) + then have rinv: "\<one> = b \<otimes> c" by (intro l_cancel[of "a" "\<one>" "b \<otimes> c"], simp+) also have "\<dots> = c \<otimes> b" by (simp add: m_comm) finally have linv: "\<one> = c \<otimes> b" . - from ccarr linv[symmetric] rinv[symmetric] - have "b \<in> Units G" unfolding Units_def by fastforce - with nunit - show "False" .. + from ccarr linv[symmetric] rinv[symmetric] have "b \<in> Units G" + unfolding Units_def by fastforce + with nunit show False .. qed lemma properfactorE: @@ -660,74 +598,67 @@ assumes pf: "properfactor G a b" and r: "\<lbrakk>a divides b; \<not>(b divides a)\<rbrakk> \<Longrightarrow> P" shows "P" -using pf -unfolding properfactor_def -by (fast intro: r) + using pf unfolding properfactor_def by (fast intro: r) lemma properfactorE2: fixes G (structure) assumes pf: "properfactor G a b" and elim: "\<lbrakk>a divides b; \<not>(a \<sim> b)\<rbrakk> \<Longrightarrow> P" shows "P" -using pf -unfolding properfactor_def -by (fast elim: elim associatedE) + using pf unfolding properfactor_def by (fast elim: elim associatedE) lemma (in monoid) properfactor_unitE: assumes uunit: "u \<in> Units G" and pf: "properfactor G a u" and acarr: "a \<in> carrier G" shows "P" -using pf unit_divides[OF uunit acarr] -by (fast elim: properfactorE) - + using pf unit_divides[OF uunit acarr] by (fast elim: properfactorE) lemma (in monoid) properfactor_divides: assumes pf: "properfactor G a b" shows "a divides b" -using pf -by (elim properfactorE) + using pf by (elim properfactorE) lemma (in monoid) properfactor_trans1 [trans]: assumes dvds: "a divides b" "properfactor G b c" and carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" shows "properfactor G a c" -using dvds carr -apply (elim properfactorE, intro properfactorI) - apply (iprover intro: divides_trans)+ -done + using dvds carr + apply (elim properfactorE, intro properfactorI) + apply (iprover intro: divides_trans)+ + done lemma (in monoid) properfactor_trans2 [trans]: assumes dvds: "properfactor G a b" "b divides c" and carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" shows "properfactor G a c" -using dvds carr -apply (elim properfactorE, intro properfactorI) - apply (iprover intro: divides_trans)+ -done + using dvds carr + apply (elim properfactorE, intro properfactorI) + apply (iprover intro: divides_trans)+ + done lemma properfactor_lless: fixes G (structure) shows "properfactor G = lless (division_rel G)" -apply (rule ext) apply (rule ext) apply rule - apply (fastforce elim: properfactorE2 intro: weak_llessI) -apply (fastforce elim: weak_llessE intro: properfactorI2) -done + apply (rule ext) + apply (rule ext) + apply rule + apply (fastforce elim: properfactorE2 intro: weak_llessI) + apply (fastforce elim: weak_llessE intro: properfactorI2) + done lemma (in monoid) properfactor_cong_l [trans]: assumes x'x: "x' \<sim> x" and pf: "properfactor G x y" and carr: "x \<in> carrier G" "x' \<in> carrier G" "y \<in> carrier G" shows "properfactor G x' y" -using pf -unfolding properfactor_lless + using pf + unfolding properfactor_lless proof - interpret weak_partial_order "division_rel G" .. - from x'x - have "x' .=\<^bsub>division_rel G\<^esub> x" by simp + from x'x have "x' .=\<^bsub>division_rel G\<^esub> x" by simp also assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y" - finally - show "x' \<sqsubset>\<^bsub>division_rel G\<^esub> y" by (simp add: carr) + finally show "x' \<sqsubset>\<^bsub>division_rel G\<^esub> y" by (simp add: carr) qed lemma (in monoid) properfactor_cong_r [trans]: @@ -735,54 +666,49 @@ and yy': "y \<sim> y'" and carr: "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G" shows "properfactor G x y'" -using pf -unfolding properfactor_lless + using pf + unfolding properfactor_lless proof - interpret weak_partial_order "division_rel G" .. assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y" also from yy' - have "y .=\<^bsub>division_rel G\<^esub> y'" by simp - finally - show "x \<sqsubset>\<^bsub>division_rel G\<^esub> y'" by (simp add: carr) + have "y .=\<^bsub>division_rel G\<^esub> y'" by simp + finally show "x \<sqsubset>\<^bsub>division_rel G\<^esub> y'" by (simp add: carr) qed lemma (in monoid_cancel) properfactor_mult_lI [intro]: assumes ab: "properfactor G a b" and carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" shows "properfactor G (c \<otimes> a) (c \<otimes> b)" -using ab carr -by (fastforce elim: properfactorE intro: properfactorI) + using ab carr by (fastforce elim: properfactorE intro: properfactorI) lemma (in monoid_cancel) properfactor_mult_l [simp]: assumes carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" shows "properfactor G (c \<otimes> a) (c \<otimes> b) = properfactor G a b" -using carr -by (fastforce elim: properfactorE intro: properfactorI) + using carr by (fastforce elim: properfactorE intro: properfactorI) lemma (in comm_monoid_cancel) properfactor_mult_rI [intro]: assumes ab: "properfactor G a b" and carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" shows "properfactor G (a \<otimes> c) (b \<otimes> c)" -using ab carr -by (fastforce elim: properfactorE intro: properfactorI) + using ab carr by (fastforce elim: properfactorE intro: properfactorI) lemma (in comm_monoid_cancel) properfactor_mult_r [simp]: assumes carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" shows "properfactor G (a \<otimes> c) (b \<otimes> c) = properfactor G a b" -using carr -by (fastforce elim: properfactorE intro: properfactorI) + using carr by (fastforce elim: properfactorE intro: properfactorI) lemma (in monoid) properfactor_prod_r: assumes ab: "properfactor G a b" and carr[simp]: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" shows "properfactor G a (b \<otimes> c)" -by (intro properfactor_trans2[OF ab] divides_prod_r, simp+) + by (intro properfactor_trans2[OF ab] divides_prod_r) simp_all lemma (in comm_monoid) properfactor_prod_l: assumes ab: "properfactor G a b" and carr[simp]: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" shows "properfactor G a (c \<otimes> b)" -by (intro properfactor_trans2[OF ab] divides_prod_l, simp+) + by (intro properfactor_trans2[OF ab] divides_prod_l) simp_all subsection \<open>Irreducible Elements and Primes\<close> @@ -794,77 +720,71 @@ assumes "a \<notin> Units G" and "\<And>b. \<lbrakk>b \<in> carrier G; properfactor G b a\<rbrakk> \<Longrightarrow> b \<in> Units G" shows "irreducible G a" -using assms -unfolding irreducible_def -by blast + using assms unfolding irreducible_def by blast lemma irreducibleE: fixes G (structure) assumes irr: "irreducible G a" - and elim: "\<lbrakk>a \<notin> Units G; \<forall>b. b \<in> carrier G \<and> properfactor G b a \<longrightarrow> b \<in> Units G\<rbrakk> \<Longrightarrow> P" + and elim: "\<lbrakk>a \<notin> Units G; \<forall>b. b \<in> carrier G \<and> properfactor G b a \<longrightarrow> b \<in> Units G\<rbrakk> \<Longrightarrow> P" shows "P" -using assms -unfolding irreducible_def -by blast + using assms unfolding irreducible_def by blast lemma irreducibleD: fixes G (structure) assumes irr: "irreducible G a" - and pf: "properfactor G b a" - and bcarr: "b \<in> carrier G" + and pf: "properfactor G b a" + and bcarr: "b \<in> carrier G" shows "b \<in> Units G" -using assms -by (fast elim: irreducibleE) + using assms by (fast elim: irreducibleE) lemma (in monoid_cancel) irreducible_cong [trans]: assumes irred: "irreducible G a" and aa': "a \<sim> a'" and carr[simp]: "a \<in> carrier G" "a' \<in> carrier G" shows "irreducible G a'" -using assms -apply (elim irreducibleE, intro irreducibleI) -apply simp_all -apply (metis assms(2) assms(3) assoc_unit_l) -apply (metis assms(2) assms(3) assms(4) associated_sym properfactor_cong_r) -done + using assms + apply (elim irreducibleE, intro irreducibleI) + apply simp_all + apply (metis assms(2) assms(3) assoc_unit_l) + apply (metis assms(2) assms(3) assms(4) associated_sym properfactor_cong_r) + done lemma (in monoid) irreducible_prod_rI: assumes airr: "irreducible G a" and bunit: "b \<in> Units G" and carr[simp]: "a \<in> carrier G" "b \<in> carrier G" shows "irreducible G (a \<otimes> b)" -using airr carr bunit -apply (elim irreducibleE, intro irreducibleI, clarify) - apply (subgoal_tac "a \<in> Units G", simp) - apply (intro prod_unit_r[of a b] carr bunit, assumption) -apply (metis assms associatedI2 m_closed properfactor_cong_r) -done + using airr carr bunit + apply (elim irreducibleE, intro irreducibleI, clarify) + apply (subgoal_tac "a \<in> Units G", simp) + apply (intro prod_unit_r[of a b] carr bunit, assumption) + apply (metis assms associatedI2 m_closed properfactor_cong_r) + done lemma (in comm_monoid) irreducible_prod_lI: assumes birr: "irreducible G b" and aunit: "a \<in> Units G" and carr [simp]: "a \<in> carrier G" "b \<in> carrier G" shows "irreducible G (a \<otimes> b)" -apply (subst m_comm, simp+) -apply (intro irreducible_prod_rI assms) -done + apply (subst m_comm, simp+) + apply (intro irreducible_prod_rI assms) + done lemma (in comm_monoid_cancel) irreducible_prodE [elim]: assumes irr: "irreducible G (a \<otimes> b)" and carr[simp]: "a \<in> carrier G" "b \<in> carrier G" and e1: "\<lbrakk>irreducible G a; b \<in> Units G\<rbrakk> \<Longrightarrow> P" and e2: "\<lbrakk>a \<in> Units G; irreducible G b\<rbrakk> \<Longrightarrow> P" - shows "P" -using irr + shows P + using irr proof (elim irreducibleE) assume abnunit: "a \<otimes> b \<notin> Units G" and isunit[rule_format]: "\<forall>ba. ba \<in> carrier G \<and> properfactor G ba (a \<otimes> b) \<longrightarrow> ba \<in> Units G" - - show "P" + show P proof (cases "a \<in> Units G") - assume aunit: "a \<in> Units G" + case aunit: True have "irreducible G b" - apply (rule irreducibleI) + apply (rule irreducibleI) proof (rule ccontr, simp) assume "b \<in> Units G" with aunit have "(a \<otimes> b) \<in> Units G" by fast @@ -873,19 +793,18 @@ fix c assume ccarr: "c \<in> carrier G" and "properfactor G c b" - hence "properfactor G c (a \<otimes> b)" by (simp add: properfactor_prod_l[of c b a]) - from ccarr this show "c \<in> Units G" by (fast intro: isunit) + then have "properfactor G c (a \<otimes> b)" by (simp add: properfactor_prod_l[of c b a]) + with ccarr show "c \<in> Units G" by (fast intro: isunit) qed - - from aunit this show "P" by (rule e2) + with aunit show "P" by (rule e2) next - assume anunit: "a \<notin> Units G" + case anunit: False with carr have "properfactor G b (b \<otimes> a)" by (fast intro: properfactorI3) - hence bf: "properfactor G b (a \<otimes> b)" by (subst m_comm[of a b], simp+) - hence bunit: "b \<in> Units G" by (intro isunit, simp) + then have bf: "properfactor G b (a \<otimes> b)" by (subst m_comm[of a b], simp+) + then have bunit: "b \<in> Units G" by (intro isunit, simp) have "irreducible G a" - apply (rule irreducibleI) + apply (rule irreducibleI) proof (rule ccontr, simp) assume "a \<in> Units G" with bunit have "(a \<otimes> b) \<in> Units G" by fast @@ -894,10 +813,10 @@ fix c assume ccarr: "c \<in> carrier G" and "properfactor G c a" - hence "properfactor G c (a \<otimes> b)" by (simp add: properfactor_prod_r[of c a b]) - from ccarr this show "c \<in> Units G" by (fast intro: isunit) + then have "properfactor G c (a \<otimes> b)" + by (simp add: properfactor_prod_r[of c a b]) + with ccarr show "c \<in> Units G" by (fast intro: isunit) qed - from this bunit show "P" by (rule e1) qed qed @@ -910,66 +829,57 @@ assumes "p \<notin> Units G" and "\<And>a b. \<lbrakk>a \<in> carrier G; b \<in> carrier G; p divides (a \<otimes> b)\<rbrakk> \<Longrightarrow> p divides a \<or> p divides b" shows "prime G p" -using assms -unfolding prime_def -by blast + using assms unfolding prime_def by blast lemma primeE: fixes G (structure) assumes pprime: "prime G p" and e: "\<lbrakk>p \<notin> Units G; \<forall>a\<in>carrier G. \<forall>b\<in>carrier G. - p divides a \<otimes> b \<longrightarrow> p divides a \<or> p divides b\<rbrakk> \<Longrightarrow> P" + p divides a \<otimes> b \<longrightarrow> p divides a \<or> p divides b\<rbrakk> \<Longrightarrow> P" shows "P" -using pprime -unfolding prime_def -by (blast dest: e) + using pprime unfolding prime_def by (blast dest: e) lemma (in comm_monoid_cancel) prime_divides: assumes carr: "a \<in> carrier G" "b \<in> carrier G" and pprime: "prime G p" and pdvd: "p divides a \<otimes> b" shows "p divides a \<or> p divides b" -using assms -by (blast elim: primeE) + using assms by (blast elim: primeE) lemma (in monoid_cancel) prime_cong [trans]: assumes pprime: "prime G p" and pp': "p \<sim> p'" and carr[simp]: "p \<in> carrier G" "p' \<in> carrier G" shows "prime G p'" -using pprime -apply (elim primeE, intro primeI) -apply (metis assms(2) assms(3) assoc_unit_l) -apply (metis assms(2) assms(3) assms(4) associated_sym divides_cong_l m_closed) -done + using pprime + apply (elim primeE, intro primeI) + apply (metis assms(2) assms(3) assoc_unit_l) + apply (metis assms(2) assms(3) assms(4) associated_sym divides_cong_l m_closed) + done + subsection \<open>Factorization and Factorial Monoids\<close> subsubsection \<open>Function definitions\<close> -definition - factors :: "[_, 'a list, 'a] \<Rightarrow> bool" +definition factors :: "[_, 'a list, 'a] \<Rightarrow> bool" where "factors G fs a \<longleftrightarrow> (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>\<^bsub>G\<^esub>) fs \<one>\<^bsub>G\<^esub> = a" -definition - wfactors ::"[_, 'a list, 'a] \<Rightarrow> bool" +definition wfactors ::"[_, 'a list, 'a] \<Rightarrow> bool" where "wfactors G fs a \<longleftrightarrow> (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>\<^bsub>G\<^esub>) fs \<one>\<^bsub>G\<^esub> \<sim>\<^bsub>G\<^esub> a" -abbreviation - list_assoc :: "('a,_) monoid_scheme \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "[\<sim>]\<index>" 44) - where "list_assoc G == list_all2 (op \<sim>\<^bsub>G\<^esub>)" - -definition - essentially_equal :: "[_, 'a list, 'a list] \<Rightarrow> bool" +abbreviation list_assoc :: "('a,_) monoid_scheme \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "[\<sim>]\<index>" 44) + where "list_assoc G \<equiv> list_all2 (op \<sim>\<^bsub>G\<^esub>)" + +definition essentially_equal :: "[_, 'a list, 'a list] \<Rightarrow> bool" where "essentially_equal G fs1 fs2 \<longleftrightarrow> (\<exists>fs1'. fs1 <~~> fs1' \<and> fs1' [\<sim>]\<^bsub>G\<^esub> fs2)" locale factorial_monoid = comm_monoid_cancel + - assumes factors_exist: - "\<lbrakk>a \<in> carrier G; a \<notin> Units G\<rbrakk> \<Longrightarrow> \<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a" - and factors_unique: - "\<lbrakk>factors G fs a; factors G fs' a; a \<in> carrier G; a \<notin> Units G; - set fs \<subseteq> carrier G; set fs' \<subseteq> carrier G\<rbrakk> \<Longrightarrow> essentially_equal G fs fs'" + assumes factors_exist: "\<lbrakk>a \<in> carrier G; a \<notin> Units G\<rbrakk> \<Longrightarrow> \<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a" + and factors_unique: + "\<lbrakk>factors G fs a; factors G fs' a; a \<in> carrier G; a \<notin> Units G; + set fs \<subseteq> carrier G; set fs' \<subseteq> carrier G\<rbrakk> \<Longrightarrow> essentially_equal G fs fs'" subsubsection \<open>Comparing lists of elements\<close> @@ -979,44 +889,45 @@ lemma (in monoid) listassoc_refl [simp, intro]: assumes "set as \<subseteq> carrier G" shows "as [\<sim>] as" -using assms -by (induct as) simp+ + using assms by (induct as) simp_all lemma (in monoid) listassoc_sym [sym]: assumes "as [\<sim>] bs" - and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G" + and "set as \<subseteq> carrier G" + and "set bs \<subseteq> carrier G" shows "bs [\<sim>] as" -using assms + using assms proof (induct as arbitrary: bs, simp) case Cons - thus ?case - apply (induct bs, simp) + then show ?case + apply (induct bs) + apply simp apply clarsimp apply (iprover intro: associated_sym) - done + done qed lemma (in monoid) listassoc_trans [trans]: assumes "as [\<sim>] bs" and "bs [\<sim>] cs" and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G" and "set cs \<subseteq> carrier G" shows "as [\<sim>] cs" -using assms -apply (simp add: list_all2_conv_all_nth set_conv_nth, safe) -apply (rule associated_trans) - apply (subgoal_tac "as ! i \<sim> bs ! i", assumption) - apply (simp, simp) - apply blast+ -done + using assms + apply (simp add: list_all2_conv_all_nth set_conv_nth, safe) + apply (rule associated_trans) + apply (subgoal_tac "as ! i \<sim> bs ! i", assumption) + apply (simp, simp) + apply blast+ + done lemma (in monoid_cancel) irrlist_listassoc_cong: assumes "\<forall>a\<in>set as. irreducible G a" and "as [\<sim>] bs" and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G" shows "\<forall>a\<in>set bs. irreducible G a" -using assms -apply (clarsimp simp add: list_all2_conv_all_nth set_conv_nth) -apply (blast intro: irreducible_cong) -done + using assms + apply (clarsimp simp add: list_all2_conv_all_nth set_conv_nth) + apply (blast intro: irreducible_cong) + done text \<open>Permutations\<close> @@ -1024,36 +935,34 @@ lemma perm_map [intro]: assumes p: "a <~~> b" shows "map f a <~~> map f b" -using p -by induct auto + using p by induct auto lemma perm_map_switch: assumes m: "map f a = map f b" and p: "b <~~> c" shows "\<exists>d. a <~~> d \<and> map f d = map f c" -using p m -by (induct arbitrary: a) (simp, force, force, blast) + using p m by (induct arbitrary: a) (simp, force, force, blast) lemma (in monoid) perm_assoc_switch: - assumes a:"as [\<sim>] bs" and p: "bs <~~> cs" - shows "\<exists>bs'. as <~~> bs' \<and> bs' [\<sim>] cs" -using p a -apply (induct bs cs arbitrary: as, simp) - apply (clarsimp simp add: list_all2_Cons2, blast) - apply (clarsimp simp add: list_all2_Cons2) - apply blast -apply blast -done + assumes a:"as [\<sim>] bs" and p: "bs <~~> cs" + shows "\<exists>bs'. as <~~> bs' \<and> bs' [\<sim>] cs" + using p a + apply (induct bs cs arbitrary: as, simp) + apply (clarsimp simp add: list_all2_Cons2, blast) + apply (clarsimp simp add: list_all2_Cons2) + apply blast + apply blast + done lemma (in monoid) perm_assoc_switch_r: - assumes p: "as <~~> bs" and a:"bs [\<sim>] cs" - shows "\<exists>bs'. as [\<sim>] bs' \<and> bs' <~~> cs" -using p a -apply (induct as bs arbitrary: cs, simp) - apply (clarsimp simp add: list_all2_Cons1, blast) - apply (clarsimp simp add: list_all2_Cons1) - apply blast -apply blast -done + assumes p: "as <~~> bs" and a:"bs [\<sim>] cs" + shows "\<exists>bs'. as [\<sim>] bs' \<and> bs' <~~> cs" + using p a + apply (induct as bs arbitrary: cs, simp) + apply (clarsimp simp add: list_all2_Cons1, blast) + apply (clarsimp simp add: list_all2_Cons1) + apply blast + apply blast + done declare perm_sym [sym] @@ -1062,19 +971,17 @@ and as: "P (set as)" shows "P (set bs)" proof - - from perm - have "mset as = mset bs" - by (simp add: mset_eq_perm) - hence "set as = set bs" by (rule mset_eq_setD) - with as - show "P (set bs)" by simp + from perm have "mset as = mset bs" + by (simp add: mset_eq_perm) + then have "set as = set bs" + by (rule mset_eq_setD) + with as show "P (set bs)" + by simp qed -lemmas (in monoid) perm_closed = - perm_setP[of _ _ "\<lambda>as. as \<subseteq> carrier G"] - -lemmas (in monoid) irrlist_perm_cong = - perm_setP[of _ _ "\<lambda>as. \<forall>a\<in>as. irreducible G a"] +lemmas (in monoid) perm_closed = perm_setP[of _ _ "\<lambda>as. as \<subseteq> carrier G"] + +lemmas (in monoid) irrlist_perm_cong = perm_setP[of _ _ "\<lambda>as. \<forall>a\<in>as. irreducible G a"] text \<open>Essentially equal factorizations\<close> @@ -1082,70 +989,61 @@ lemma (in monoid) essentially_equalI: assumes ex: "fs1 <~~> fs1'" "fs1' [\<sim>] fs2" shows "essentially_equal G fs1 fs2" -using ex -unfolding essentially_equal_def -by fast + using ex unfolding essentially_equal_def by fast lemma (in monoid) essentially_equalE: assumes ee: "essentially_equal G fs1 fs2" and e: "\<And>fs1'. \<lbrakk>fs1 <~~> fs1'; fs1' [\<sim>] fs2\<rbrakk> \<Longrightarrow> P" shows "P" -using ee -unfolding essentially_equal_def -by (fast intro: e) + using ee unfolding essentially_equal_def by (fast intro: e) lemma (in monoid) ee_refl [simp,intro]: assumes carr: "set as \<subseteq> carrier G" shows "essentially_equal G as as" -using carr -by (fast intro: essentially_equalI) + using carr by (fast intro: essentially_equalI) lemma (in monoid) ee_sym [sym]: assumes ee: "essentially_equal G as bs" and carr: "set as \<subseteq> carrier G" "set bs \<subseteq> carrier G" shows "essentially_equal G bs as" -using ee + using ee proof (elim essentially_equalE) fix fs assume "as <~~> fs" "fs [\<sim>] bs" - hence "\<exists>fs'. as [\<sim>] fs' \<and> fs' <~~> bs" by (rule perm_assoc_switch_r) - from this obtain fs' - where a: "as [\<sim>] fs'" and p: "fs' <~~> bs" - by auto + then have "\<exists>fs'. as [\<sim>] fs' \<and> fs' <~~> bs" + by (rule perm_assoc_switch_r) + then obtain fs' where a: "as [\<sim>] fs'" and p: "fs' <~~> bs" + by auto from p have "bs <~~> fs'" by (rule perm_sym) - with a[symmetric] carr - show ?thesis - by (iprover intro: essentially_equalI perm_closed) + with a[symmetric] carr show ?thesis + by (iprover intro: essentially_equalI perm_closed) qed lemma (in monoid) ee_trans [trans]: assumes ab: "essentially_equal G as bs" and bc: "essentially_equal G bs cs" - and ascarr: "set as \<subseteq> carrier G" + and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G" and cscarr: "set cs \<subseteq> carrier G" shows "essentially_equal G as cs" -using ab bc + using ab bc proof (elim essentially_equalE) fix abs bcs assume "abs [\<sim>] bs" and pb: "bs <~~> bcs" - hence "\<exists>bs'. abs <~~> bs' \<and> bs' [\<sim>] bcs" by (rule perm_assoc_switch) - from this obtain bs' - where p: "abs <~~> bs'" and a: "bs' [\<sim>] bcs" - by auto + then have "\<exists>bs'. abs <~~> bs' \<and> bs' [\<sim>] bcs" + by (rule perm_assoc_switch) + then obtain bs' where p: "abs <~~> bs'" and a: "bs' [\<sim>] bcs" + by auto assume "as <~~> abs" - with p - have pp: "as <~~> bs'" by fast + with p have pp: "as <~~> bs'" by fast from pp ascarr have c1: "set bs' \<subseteq> carrier G" by (rule perm_closed) from pb bscarr have c2: "set bcs \<subseteq> carrier G" by (rule perm_closed) note a also assume "bcs [\<sim>] cs" - finally (listassoc_trans) have"bs' [\<sim>] cs" by (simp add: c1 c2 cscarr) - - with pp - show ?thesis - by (rule essentially_equalI) + finally (listassoc_trans) have "bs' [\<sim>] cs" by (simp add: c1 c2 cscarr) + with pp show ?thesis + by (rule essentially_equalI) qed @@ -1156,47 +1054,46 @@ lemma (in monoid) multlist_closed [simp, intro]: assumes ascarr: "set fs \<subseteq> carrier G" shows "foldr (op \<otimes>) fs \<one> \<in> carrier G" -by (insert ascarr, induct fs, simp+) + using ascarr by (induct fs) simp_all lemma (in comm_monoid) multlist_dividesI (*[intro]*): assumes "f \<in> set fs" and "f \<in> carrier G" and "set fs \<subseteq> carrier G" shows "f divides (foldr (op \<otimes>) fs \<one>)" -using assms -apply (induct fs) - apply simp -apply (case_tac "f = a", simp) - apply (fast intro: dividesI) -apply clarsimp -apply (metis assms(2) divides_prod_l multlist_closed) -done + using assms + apply (induct fs) + apply simp + apply (case_tac "f = a") + apply simp + apply (fast intro: dividesI) + apply clarsimp + apply (metis assms(2) divides_prod_l multlist_closed) + done lemma (in comm_monoid_cancel) multlist_listassoc_cong: assumes "fs [\<sim>] fs'" and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G" shows "foldr (op \<otimes>) fs \<one> \<sim> foldr (op \<otimes>) fs' \<one>" -using assms + using assms proof (induct fs arbitrary: fs', simp) case (Cons a as fs') - thus ?case - apply (induct fs', simp) + then show ?case + apply (induct fs', simp) proof clarsimp fix b bs - assume "a \<sim> b" + assume "a \<sim> b" and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ascarr: "set as \<subseteq> carrier G" - hence p: "a \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> as \<one>" - by (fast intro: mult_cong_l) + then have p: "a \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> as \<one>" + by (fast intro: mult_cong_l) also - assume "as [\<sim>] bs" - and bscarr: "set bs \<subseteq> carrier G" - and "\<And>fs'. \<lbrakk>as [\<sim>] fs'; set fs' \<subseteq> carrier G\<rbrakk> \<Longrightarrow> foldr op \<otimes> as \<one> \<sim> foldr op \<otimes> fs' \<one>" - hence "foldr op \<otimes> as \<one> \<sim> foldr op \<otimes> bs \<one>" by simp - with ascarr bscarr bcarr - have "b \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> bs \<one>" - by (fast intro: mult_cong_r) - finally - show "a \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> bs \<one>" - by (simp add: ascarr bscarr acarr bcarr) + assume "as [\<sim>] bs" + and bscarr: "set bs \<subseteq> carrier G" + and "\<And>fs'. \<lbrakk>as [\<sim>] fs'; set fs' \<subseteq> carrier G\<rbrakk> \<Longrightarrow> foldr op \<otimes> as \<one> \<sim> foldr op \<otimes> fs' \<one>" + then have "foldr op \<otimes> as \<one> \<sim> foldr op \<otimes> bs \<one>" by simp + with ascarr bscarr bcarr have "b \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> bs \<one>" + by (fast intro: mult_cong_r) + finally show "a \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> bs \<one>" + by (simp add: ascarr bscarr acarr bcarr) qed qed @@ -1204,12 +1101,12 @@ assumes prm: "as <~~> bs" and ascarr: "set as \<subseteq> carrier G" shows "foldr (op \<otimes>) as \<one> = foldr (op \<otimes>) bs \<one>" -using prm ascarr -apply (induct, simp, clarsimp simp add: m_ac, clarsimp) + using prm ascarr + apply (induct, simp, clarsimp simp add: m_ac, clarsimp) proof clarsimp fix xs ys zs assume "xs <~~> ys" "set xs \<subseteq> carrier G" - hence "set ys \<subseteq> carrier G" by (rule perm_closed) + then have "set ys \<subseteq> carrier G" by (rule perm_closed) moreover assume "set ys \<subseteq> carrier G \<Longrightarrow> foldr op \<otimes> ys \<one> = foldr op \<otimes> zs \<one>" ultimately show "foldr op \<otimes> ys \<one> = foldr op \<otimes> zs \<one>" by simp qed @@ -1218,10 +1115,10 @@ assumes "essentially_equal G fs fs'" and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G" shows "foldr (op \<otimes>) fs \<one> \<sim> foldr (op \<otimes>) fs' \<one>" -using assms -apply (elim essentially_equalE) -apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed) -done + using assms + apply (elim essentially_equalE) + apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed) + done subsubsection \<open>Factorization in irreducible elements\<close> @@ -1231,53 +1128,42 @@ assumes "\<forall>f\<in>set fs. irreducible G f" and "foldr (op \<otimes>) fs \<one> \<sim> a" shows "wfactors G fs a" -using assms -unfolding wfactors_def -by simp + using assms unfolding wfactors_def by simp lemma wfactorsE: fixes G (structure) assumes wf: "wfactors G fs a" and e: "\<lbrakk>\<forall>f\<in>set fs. irreducible G f; foldr (op \<otimes>) fs \<one> \<sim> a\<rbrakk> \<Longrightarrow> P" shows "P" -using wf -unfolding wfactors_def -by (fast dest: e) + using wf unfolding wfactors_def by (fast dest: e) lemma (in monoid) factorsI: assumes "\<forall>f\<in>set fs. irreducible G f" and "foldr (op \<otimes>) fs \<one> = a" shows "factors G fs a" -using assms -unfolding factors_def -by simp + using assms unfolding factors_def by simp lemma factorsE: fixes G (structure) assumes f: "factors G fs a" and e: "\<lbrakk>\<forall>f\<in>set fs. irreducible G f; foldr (op \<otimes>) fs \<one> = a\<rbrakk> \<Longrightarrow> P" shows "P" -using f -unfolding factors_def -by (simp add: e) + using f unfolding factors_def by (simp add: e) lemma (in monoid) factors_wfactors: assumes "factors G as a" and "set as \<subseteq> carrier G" shows "wfactors G as a" -using assms -by (blast elim: factorsE intro: wfactorsI) + using assms by (blast elim: factorsE intro: wfactorsI) lemma (in monoid) wfactors_factors: assumes "wfactors G as a" and "set as \<subseteq> carrier G" shows "\<exists>a'. factors G as a' \<and> a' \<sim> a" -using assms -by (blast elim: wfactorsE intro: factorsI) + using assms by (blast elim: wfactorsE intro: factorsI) lemma (in monoid) factors_closed [dest]: assumes "factors G fs a" and "set fs \<subseteq> carrier G" shows "a \<in> carrier G" -using assms -by (elim factorsE, clarsimp) + using assms by (elim factorsE, clarsimp) lemma (in monoid) nunit_factors: assumes anunit: "a \<notin> Units G" @@ -1291,8 +1177,7 @@ lemma (in monoid) unit_wfactors [simp]: assumes aunit: "a \<in> Units G" shows "wfactors G [] a" -using aunit -by (intro wfactorsI) (simp, simp add: Units_assoc) + using aunit by (intro wfactorsI) (simp, simp add: Units_assoc) lemma (in comm_monoid_cancel) unit_wfactors_empty: assumes aunit: "a \<in> Units G" @@ -1303,27 +1188,21 @@ fix f fs' assume fs: "fs = f # fs'" - from carr - have fcarr[simp]: "f \<in> carrier G" - and carr'[simp]: "set fs' \<subseteq> carrier G" - by (simp add: fs)+ - - from fs wf - have "irreducible G f" by (simp add: wfactors_def) - hence fnunit: "f \<notin> Units G" by (fast elim: irreducibleE) - - from fs wf - have a: "f \<otimes> foldr (op \<otimes>) fs' \<one> \<sim> a" by (simp add: wfactors_def) + from carr have fcarr[simp]: "f \<in> carrier G" and carr'[simp]: "set fs' \<subseteq> carrier G" + by (simp_all add: fs) + + from fs wf have "irreducible G f" by (simp add: wfactors_def) + then have fnunit: "f \<notin> Units G" by (fast elim: irreducibleE) + + from fs wf have a: "f \<otimes> foldr (op \<otimes>) fs' \<one> \<sim> a" by (simp add: wfactors_def) note aunit also from fs wf - have a: "f \<otimes> foldr (op \<otimes>) fs' \<one> \<sim> a" by (simp add: wfactors_def) - have "a \<sim> f \<otimes> foldr (op \<otimes>) fs' \<one>" - by (simp add: Units_closed[OF aunit] a[symmetric]) - finally - have "f \<otimes> foldr (op \<otimes>) fs' \<one> \<in> Units G" by simp - hence "f \<in> Units G" by (intro unit_factor[of f], simp+) - + have a: "f \<otimes> foldr (op \<otimes>) fs' \<one> \<sim> a" by (simp add: wfactors_def) + have "a \<sim> f \<otimes> foldr (op \<otimes>) fs' \<one>" + by (simp add: Units_closed[OF aunit] a[symmetric]) + finally have "f \<otimes> foldr (op \<otimes>) fs' \<one> \<in> Units G" by simp + then have "f \<in> Units G" by (intro unit_factor[of f], simp+) with fnunit show "False" by simp qed @@ -1335,16 +1214,14 @@ and asc: "fs [\<sim>] fs'" and carr: "a \<in> carrier G" "set fs \<subseteq> carrier G" "set fs' \<subseteq> carrier G" shows "wfactors G fs' a" -using fact -apply (elim wfactorsE, intro wfactorsI) -apply (metis assms(2) assms(4) assms(5) irrlist_listassoc_cong) + using fact + apply (elim wfactorsE, intro wfactorsI) + apply (metis assms(2) assms(4) assms(5) irrlist_listassoc_cong) proof - - from asc[symmetric] - have "foldr op \<otimes> fs' \<one> \<sim> foldr op \<otimes> fs \<one>" - by (simp add: multlist_listassoc_cong carr) + from asc[symmetric] have "foldr op \<otimes> fs' \<one> \<sim> foldr op \<otimes> fs \<one>" + by (simp add: multlist_listassoc_cong carr) also assume "foldr op \<otimes> fs \<one> \<sim> a" - finally - show "foldr op \<otimes> fs' \<one> \<sim> a" by (simp add: carr) + finally show "foldr op \<otimes> fs' \<one> \<sim> a" by (simp add: carr) qed lemma (in comm_monoid) wfactors_perm_cong_l: @@ -1352,37 +1229,36 @@ and "fs <~~> fs'" and "set fs \<subseteq> carrier G" shows "wfactors G fs' a" -using assms -apply (elim wfactorsE, intro wfactorsI) - apply (rule irrlist_perm_cong, assumption+) -apply (simp add: multlist_perm_cong[symmetric]) -done + using assms + apply (elim wfactorsE, intro wfactorsI) + apply (rule irrlist_perm_cong, assumption+) + apply (simp add: multlist_perm_cong[symmetric]) + done lemma (in comm_monoid_cancel) wfactors_ee_cong_l [trans]: assumes ee: "essentially_equal G as bs" and bfs: "wfactors G bs b" and carr: "b \<in> carrier G" "set as \<subseteq> carrier G" "set bs \<subseteq> carrier G" shows "wfactors G as b" -using ee + using ee proof (elim essentially_equalE) fix fs assume prm: "as <~~> fs" - with carr - have fscarr: "set fs \<subseteq> carrier G" by (simp add: perm_closed) + with carr have fscarr: "set fs \<subseteq> carrier G" by (simp add: perm_closed) note bfs also assume [symmetric]: "fs [\<sim>] bs" also (wfactors_listassoc_cong_l) - note prm[symmetric] + note prm[symmetric] finally (wfactors_perm_cong_l) - show "wfactors G as b" by (simp add: carr fscarr) + show "wfactors G as b" by (simp add: carr fscarr) qed lemma (in monoid) wfactors_cong_r [trans]: assumes fac: "wfactors G fs a" and aa': "a \<sim> a'" and carr[simp]: "a \<in> carrier G" "a' \<in> carrier G" "set fs \<subseteq> carrier G" shows "wfactors G fs a'" -using fac + using fac proof (elim wfactorsE, intro wfactorsI) assume "foldr op \<otimes> fs \<one> \<sim> a" also note aa' finally show "foldr op \<otimes> fs \<one> \<sim> a'" by simp @@ -1394,61 +1270,64 @@ lemma (in comm_monoid_cancel) unitfactor_ee: assumes uunit: "u \<in> Units G" and carr: "set as \<subseteq> carrier G" - shows "essentially_equal G (as[0 := (as!0 \<otimes> u)]) as" (is "essentially_equal G ?as' as") -using assms -apply (intro essentially_equalI[of _ ?as'], simp) -apply (cases as, simp) -apply (clarsimp, fast intro: associatedI2[of u]) -done + shows "essentially_equal G (as[0 := (as!0 \<otimes> u)]) as" + (is "essentially_equal G ?as' as") + using assms + apply (intro essentially_equalI[of _ ?as'], simp) + apply (cases as, simp) + apply (clarsimp, fast intro: associatedI2[of u]) + done lemma (in comm_monoid_cancel) factors_cong_unit: - assumes uunit: "u \<in> Units G" and anunit: "a \<notin> Units G" + assumes uunit: "u \<in> Units G" + and anunit: "a \<notin> Units G" and afs: "factors G as a" and ascarr: "set as \<subseteq> carrier G" - shows "factors G (as[0 := (as!0 \<otimes> u)]) (a \<otimes> u)" (is "factors G ?as' ?a'") -using assms -apply (elim factorsE, clarify) -apply (cases as) - apply (simp add: nunit_factors) -apply clarsimp -apply (elim factorsE, intro factorsI) - apply (clarsimp, fast intro: irreducible_prod_rI) -apply (simp add: m_ac Units_closed) -done + shows "factors G (as[0 := (as!0 \<otimes> u)]) (a \<otimes> u)" + (is "factors G ?as' ?a'") + using assms + apply (elim factorsE, clarify) + apply (cases as) + apply (simp add: nunit_factors) + apply clarsimp + apply (elim factorsE, intro factorsI) + apply (clarsimp, fast intro: irreducible_prod_rI) + apply (simp add: m_ac Units_closed) + done lemma (in comm_monoid) perm_wfactorsD: assumes prm: "as <~~> bs" - and afs: "wfactors G as a" and bfs: "wfactors G bs b" + and afs: "wfactors G as a" + and bfs: "wfactors G bs b" and [simp]: "a \<in> carrier G" "b \<in> carrier G" - and ascarr[simp]: "set as \<subseteq> carrier G" + and ascarr [simp]: "set as \<subseteq> carrier G" shows "a \<sim> b" -using afs bfs + using afs bfs proof (elim wfactorsE) from prm have [simp]: "set bs \<subseteq> carrier G" by (simp add: perm_closed) assume "foldr op \<otimes> as \<one> \<sim> a" - hence "a \<sim> foldr op \<otimes> as \<one>" by (rule associated_sym, simp+) + then have "a \<sim> foldr op \<otimes> as \<one>" by (rule associated_sym, simp+) also from prm - have "foldr op \<otimes> as \<one> = foldr op \<otimes> bs \<one>" by (rule multlist_perm_cong, simp) + have "foldr op \<otimes> as \<one> = foldr op \<otimes> bs \<one>" by (rule multlist_perm_cong, simp) also assume "foldr op \<otimes> bs \<one> \<sim> b" - finally - show "a \<sim> b" by simp + finally show "a \<sim> b" by simp qed lemma (in comm_monoid_cancel) listassoc_wfactorsD: assumes assoc: "as [\<sim>] bs" - and afs: "wfactors G as a" and bfs: "wfactors G bs b" + and afs: "wfactors G as a" + and bfs: "wfactors G bs b" and [simp]: "a \<in> carrier G" "b \<in> carrier G" and [simp]: "set as \<subseteq> carrier G" "set bs \<subseteq> carrier G" shows "a \<sim> b" -using afs bfs + using afs bfs proof (elim wfactorsE) assume "foldr op \<otimes> as \<one> \<sim> a" - hence "a \<sim> foldr op \<otimes> as \<one>" by (rule associated_sym, simp+) + then have "a \<sim> foldr op \<otimes> as \<one>" by (rule associated_sym, simp+) also from assoc - have "foldr op \<otimes> as \<one> \<sim> foldr op \<otimes> bs \<one>" by (rule multlist_listassoc_cong, simp+) + have "foldr op \<otimes> as \<one> \<sim> foldr op \<otimes> bs \<one>" by (rule multlist_listassoc_cong, simp+) also assume "foldr op \<otimes> bs \<one> \<sim> b" - finally - show "a \<sim> b" by simp + finally show "a \<sim> b" by simp qed lemma (in comm_monoid_cancel) ee_wfactorsD: @@ -1457,16 +1336,17 @@ and [simp]: "a \<in> carrier G" "b \<in> carrier G" and ascarr[simp]: "set as \<subseteq> carrier G" and bscarr[simp]: "set bs \<subseteq> carrier G" shows "a \<sim> b" -using ee + using ee proof (elim essentially_equalE) fix fs assume prm: "as <~~> fs" - hence as'carr[simp]: "set fs \<subseteq> carrier G" by (simp add: perm_closed) - from afs prm - have afs': "wfactors G fs a" by (rule wfactors_perm_cong_l, simp) + then have as'carr[simp]: "set fs \<subseteq> carrier G" + by (simp add: perm_closed) + from afs prm have afs': "wfactors G fs a" + by (rule wfactors_perm_cong_l) simp assume "fs [\<sim>] bs" - from this afs' bfs - show "a \<sim> b" by (rule listassoc_wfactorsD, simp+) + from this afs' bfs show "a \<sim> b" + by (rule listassoc_wfactorsD) simp_all qed lemma (in comm_monoid_cancel) ee_factorsD: @@ -1474,8 +1354,7 @@ and afs: "factors G as a" and bfs:"factors G bs b" and "set as \<subseteq> carrier G" "set bs \<subseteq> carrier G" shows "a \<sim> b" -using assms -by (blast intro: factors_wfactors dest: ee_wfactorsD) + using assms by (blast intro: factors_wfactors dest: ee_wfactorsD) lemma (in factorial_monoid) ee_factorsI: assumes ab: "a \<sim> b" @@ -1485,33 +1364,29 @@ shows "essentially_equal G as bs" proof - note carr[simp] = factors_closed[OF afs ascarr] ascarr[THEN subsetD] - factors_closed[OF bfs bscarr] bscarr[THEN subsetD] - - from ab carr - have "\<exists>u\<in>Units G. a = b \<otimes> u" by (fast elim: associatedE2) - from this obtain u - where uunit: "u \<in> Units G" - and a: "a = b \<otimes> u" by auto - - from uunit bscarr - have ee: "essentially_equal G (bs[0 := (bs!0 \<otimes> u)]) bs" - (is "essentially_equal G ?bs' bs") - by (rule unitfactor_ee) - - from bscarr uunit - have bs'carr: "set ?bs' \<subseteq> carrier G" - by (cases bs) (simp add: Units_closed)+ - - from uunit bnunit bfs bscarr - have fac: "factors G ?bs' (b \<otimes> u)" - by (rule factors_cong_unit) + factors_closed[OF bfs bscarr] bscarr[THEN subsetD] + + from ab carr have "\<exists>u\<in>Units G. a = b \<otimes> u" + by (fast elim: associatedE2) + then obtain u where uunit: "u \<in> Units G" and a: "a = b \<otimes> u" + by auto + + from uunit bscarr have ee: "essentially_equal G (bs[0 := (bs!0 \<otimes> u)]) bs" + (is "essentially_equal G ?bs' bs") + by (rule unitfactor_ee) + + from bscarr uunit have bs'carr: "set ?bs' \<subseteq> carrier G" + by (cases bs) (simp_all add: Units_closed) + + from uunit bnunit bfs bscarr have fac: "factors G ?bs' (b \<otimes> u)" + by (rule factors_cong_unit) from afs fac[simplified a[symmetric]] ascarr bs'carr anunit - have "essentially_equal G as ?bs'" - by (blast intro: factors_unique) + have "essentially_equal G as ?bs'" + by (blast intro: factors_unique) also note ee - finally - show "essentially_equal G as bs" by (simp add: ascarr bscarr bs'carr) + finally show "essentially_equal G as bs" + by (simp add: ascarr bscarr bs'carr) qed lemma (in factorial_monoid) ee_wfactorsI: @@ -1520,74 +1395,68 @@ and acarr[simp]: "a \<in> carrier G" and bcarr[simp]: "b \<in> carrier G" and ascarr[simp]: "set as \<subseteq> carrier G" and bscarr[simp]: "set bs \<subseteq> carrier G" shows "essentially_equal G as bs" -using assms + using assms proof (cases "a \<in> Units G") - assume aunit: "a \<in> Units G" + case aunit: True also note asc finally have bunit: "b \<in> Units G" by simp - from aunit asf ascarr - have e: "as = []" by (rule unit_wfactors_empty) - from bunit bsf bscarr - have e': "bs = []" by (rule unit_wfactors_empty) + from aunit asf ascarr have e: "as = []" + by (rule unit_wfactors_empty) + from bunit bsf bscarr have e': "bs = []" + by (rule unit_wfactors_empty) have "essentially_equal G [] []" - by (fast intro: essentially_equalI) - thus ?thesis by (simp add: e e') + by (fast intro: essentially_equalI) + then show ?thesis + by (simp add: e e') next - assume anunit: "a \<notin> Units G" + case anunit: False have bnunit: "b \<notin> Units G" proof clarify assume "b \<in> Units G" also note asc[symmetric] finally have "a \<in> Units G" by simp - with anunit - show "False" .. + with anunit show False .. qed - have "\<exists>a'. factors G as a' \<and> a' \<sim> a" by (rule wfactors_factors[OF asf ascarr]) - from this obtain a' - where fa': "factors G as a'" - and a': "a' \<sim> a" - by auto - from fa' ascarr - have a'carr[simp]: "a' \<in> carrier G" by fast + have "\<exists>a'. factors G as a' \<and> a' \<sim> a" + by (rule wfactors_factors[OF asf ascarr]) + then obtain a' where fa': "factors G as a'" and a': "a' \<sim> a" + by auto + from fa' ascarr have a'carr[simp]: "a' \<in> carrier G" + by fast have a'nunit: "a' \<notin> Units G" - proof (clarify) + proof clarify assume "a' \<in> Units G" also note a' finally have "a \<in> Units G" by simp with anunit - show "False" .. + show "False" .. qed - have "\<exists>b'. factors G bs b' \<and> b' \<sim> b" by (rule wfactors_factors[OF bsf bscarr]) - from this obtain b' - where fb': "factors G bs b'" - and b': "b' \<sim> b" - by auto - from fb' bscarr - have b'carr[simp]: "b' \<in> carrier G" by fast + have "\<exists>b'. factors G bs b' \<and> b' \<sim> b" + by (rule wfactors_factors[OF bsf bscarr]) + then obtain b' where fb': "factors G bs b'" and b': "b' \<sim> b" + by auto + from fb' bscarr have b'carr[simp]: "b' \<in> carrier G" + by fast have b'nunit: "b' \<notin> Units G" - proof (clarify) + proof clarify assume "b' \<in> Units G" also note b' finally have "b \<in> Units G" by simp - with bnunit - show "False" .. + with bnunit show False .. qed note a' also note asc also note b'[symmetric] - finally - have "a' \<sim> b'" by simp - - from this fa' a'nunit fb' b'nunit ascarr bscarr - show "essentially_equal G as bs" - by (rule ee_factorsI) + finally have "a' \<sim> b'" by simp + from this fa' a'nunit fb' b'nunit ascarr bscarr show "essentially_equal G as bs" + by (rule ee_factorsI) qed lemma (in factorial_monoid) ee_wfactors: @@ -1596,189 +1465,168 @@ and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G" shows asc: "a \<sim> b = essentially_equal G as bs" -using assms -by (fast intro: ee_wfactorsI ee_wfactorsD) + using assms by (fast intro: ee_wfactorsI ee_wfactorsD) lemma (in factorial_monoid) wfactors_exist [intro, simp]: assumes acarr[simp]: "a \<in> carrier G" shows "\<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs a" proof (cases "a \<in> Units G") - assume "a \<in> Units G" - hence "wfactors G [] a" by (rule unit_wfactors) - thus ?thesis by (intro exI) force + case True + then have "wfactors G [] a" by (rule unit_wfactors) + then show ?thesis by (intro exI) force next - assume "a \<notin> Units G" - hence "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a" by (intro factors_exist acarr) - from this obtain fs - where fscarr: "set fs \<subseteq> carrier G" - and f: "factors G fs a" - by auto + case False + then have "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a" + by (intro factors_exist acarr) + then obtain fs where fscarr: "set fs \<subseteq> carrier G" and f: "factors G fs a" + by auto from f have "wfactors G fs a" by (rule factors_wfactors) fact - from fscarr this - show ?thesis by fast + with fscarr show ?thesis by fast qed lemma (in monoid) wfactors_prod_exists [intro, simp]: assumes "\<forall>a \<in> set as. irreducible G a" and "set as \<subseteq> carrier G" shows "\<exists>a. a \<in> carrier G \<and> wfactors G as a" -unfolding wfactors_def -using assms -by blast + unfolding wfactors_def using assms by blast lemma (in factorial_monoid) wfactors_unique: - assumes "wfactors G fs a" and "wfactors G fs' a" + assumes "wfactors G fs a" + and "wfactors G fs' a" and "a \<in> carrier G" - and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G" + and "set fs \<subseteq> carrier G" + and "set fs' \<subseteq> carrier G" shows "essentially_equal G fs fs'" -using assms -by (fast intro: ee_wfactorsI[of a a]) + using assms by (fast intro: ee_wfactorsI[of a a]) lemma (in monoid) factors_mult_single: assumes "irreducible G a" and "factors G fb b" and "a \<in> carrier G" shows "factors G (a # fb) (a \<otimes> b)" -using assms -unfolding factors_def -by simp + using assms unfolding factors_def by simp lemma (in monoid_cancel) wfactors_mult_single: assumes f: "irreducible G a" "wfactors G fb b" - "a \<in> carrier G" "b \<in> carrier G" "set fb \<subseteq> carrier G" + "a \<in> carrier G" "b \<in> carrier G" "set fb \<subseteq> carrier G" shows "wfactors G (a # fb) (a \<otimes> b)" -using assms -unfolding wfactors_def -by (simp add: mult_cong_r) + using assms unfolding wfactors_def by (simp add: mult_cong_r) lemma (in monoid) factors_mult: assumes factors: "factors G fa a" "factors G fb b" - and ascarr: "set fa \<subseteq> carrier G" and bscarr:"set fb \<subseteq> carrier G" + and ascarr: "set fa \<subseteq> carrier G" + and bscarr: "set fb \<subseteq> carrier G" shows "factors G (fa @ fb) (a \<otimes> b)" -using assms -unfolding factors_def -apply (safe, force) -apply hypsubst_thin -apply (induct fa) - apply simp -apply (simp add: m_assoc) -done + using assms + unfolding factors_def + apply safe + apply force + apply hypsubst_thin + apply (induct fa) + apply simp + apply (simp add: m_assoc) + done lemma (in comm_monoid_cancel) wfactors_mult [intro]: assumes asf: "wfactors G as a" and bsf:"wfactors G bs b" and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ascarr: "set as \<subseteq> carrier G" and bscarr:"set bs \<subseteq> carrier G" shows "wfactors G (as @ bs) (a \<otimes> b)" -apply (insert wfactors_factors[OF asf ascarr]) -apply (insert wfactors_factors[OF bsf bscarr]) -proof (clarsimp) + using wfactors_factors[OF asf ascarr] and wfactors_factors[OF bsf bscarr] +proof clarsimp fix a' b' assume asf': "factors G as a'" and a'a: "a' \<sim> a" - and bsf': "factors G bs b'" and b'b: "b' \<sim> b" + and bsf': "factors G bs b'" and b'b: "b' \<sim> b" from asf' have a'carr: "a' \<in> carrier G" by (rule factors_closed) fact from bsf' have b'carr: "b' \<in> carrier G" by (rule factors_closed) fact note carr = acarr bcarr a'carr b'carr ascarr bscarr - from asf' bsf' - have "factors G (as @ bs) (a' \<otimes> b')" by (rule factors_mult) fact+ - - with carr - have abf': "wfactors G (as @ bs) (a' \<otimes> b')" by (intro factors_wfactors) simp+ - also from b'b carr - have trb: "a' \<otimes> b' \<sim> a' \<otimes> b" by (intro mult_cong_r) - also from a'a carr - have tra: "a' \<otimes> b \<sim> a \<otimes> b" by (intro mult_cong_l) - finally - show "wfactors G (as @ bs) (a \<otimes> b)" - by (simp add: carr) + from asf' bsf' have "factors G (as @ bs) (a' \<otimes> b')" + by (rule factors_mult) fact+ + + with carr have abf': "wfactors G (as @ bs) (a' \<otimes> b')" + by (intro factors_wfactors) simp_all + also from b'b carr have trb: "a' \<otimes> b' \<sim> a' \<otimes> b" + by (intro mult_cong_r) + also from a'a carr have tra: "a' \<otimes> b \<sim> a \<otimes> b" + by (intro mult_cong_l) + finally show "wfactors G (as @ bs) (a \<otimes> b)" + by (simp add: carr) qed lemma (in comm_monoid) factors_dividesI: - assumes "factors G fs a" and "f \<in> set fs" + assumes "factors G fs a" + and "f \<in> set fs" and "set fs \<subseteq> carrier G" shows "f divides a" -using assms -by (fast elim: factorsE intro: multlist_dividesI) + using assms by (fast elim: factorsE intro: multlist_dividesI) lemma (in comm_monoid) wfactors_dividesI: assumes p: "wfactors G fs a" and fscarr: "set fs \<subseteq> carrier G" and acarr: "a \<in> carrier G" and f: "f \<in> set fs" shows "f divides a" -apply (insert wfactors_factors[OF p fscarr], clarsimp) -proof - + using wfactors_factors[OF p fscarr] +proof clarsimp fix a' - assume fsa': "factors G fs a'" - and a'a: "a' \<sim> a" - with fscarr - have a'carr: "a' \<in> carrier G" by (simp add: factors_closed) - - from fsa' fscarr f - have "f divides a'" by (fast intro: factors_dividesI) + assume fsa': "factors G fs a'" and a'a: "a' \<sim> a" + with fscarr have a'carr: "a' \<in> carrier G" + by (simp add: factors_closed) + + from fsa' fscarr f have "f divides a'" + by (fast intro: factors_dividesI) also note a'a - finally - show "f divides a" by (simp add: f fscarr[THEN subsetD] acarr a'carr) + finally show "f divides a" + by (simp add: f fscarr[THEN subsetD] acarr a'carr) qed subsubsection \<open>Factorial monoids and wfactors\<close> lemma (in comm_monoid_cancel) factorial_monoidI: - assumes wfactors_exists: - "\<And>a. a \<in> carrier G \<Longrightarrow> \<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs a" - and wfactors_unique: - "\<And>a fs fs'. \<lbrakk>a \<in> carrier G; set fs \<subseteq> carrier G; set fs' \<subseteq> carrier G; - wfactors G fs a; wfactors G fs' a\<rbrakk> \<Longrightarrow> essentially_equal G fs fs'" + assumes wfactors_exists: "\<And>a. a \<in> carrier G \<Longrightarrow> \<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs a" + and wfactors_unique: + "\<And>a fs fs'. \<lbrakk>a \<in> carrier G; set fs \<subseteq> carrier G; set fs' \<subseteq> carrier G; + wfactors G fs a; wfactors G fs' a\<rbrakk> \<Longrightarrow> essentially_equal G fs fs'" shows "factorial_monoid G" proof fix a assume acarr: "a \<in> carrier G" and anunit: "a \<notin> Units G" from wfactors_exists[OF acarr] - obtain as - where ascarr: "set as \<subseteq> carrier G" - and afs: "wfactors G as a" - by auto - from afs ascarr - have "\<exists>a'. factors G as a' \<and> a' \<sim> a" by (rule wfactors_factors) - from this obtain a' - where afs': "factors G as a'" - and a'a: "a' \<sim> a" - by auto - from afs' ascarr - have a'carr: "a' \<in> carrier G" by fast + obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a" + by auto + from afs ascarr have "\<exists>a'. factors G as a' \<and> a' \<sim> a" + by (rule wfactors_factors) + then obtain a' where afs': "factors G as a'" and a'a: "a' \<sim> a" + by auto + from afs' ascarr have a'carr: "a' \<in> carrier G" + by fast have a'nunit: "a' \<notin> Units G" proof clarify assume "a' \<in> Units G" also note a'a finally have "a \<in> Units G" by (simp add: acarr) - with anunit - show "False" .. + with anunit show False .. qed - from a'carr acarr a'a - have "\<exists>u. u \<in> Units G \<and> a' = a \<otimes> u" by (blast elim: associatedE2) - from this obtain u - where uunit: "u \<in> Units G" - and a': "a' = a \<otimes> u" - by auto + from a'carr acarr a'a have "\<exists>u. u \<in> Units G \<and> a' = a \<otimes> u" + by (blast elim: associatedE2) + then obtain u where uunit: "u \<in> Units G" and a': "a' = a \<otimes> u" + by auto note [simp] = acarr Units_closed[OF uunit] Units_inv_closed[OF uunit] have "a = a \<otimes> \<one>" by simp also have "\<dots> = a \<otimes> (u \<otimes> inv u)" by (simp add: uunit) also have "\<dots> = a' \<otimes> inv u" by (simp add: m_assoc[symmetric] a'[symmetric]) - finally - have a: "a = a' \<otimes> inv u" . - - from ascarr uunit - have cr: "set (as[0:=(as!0 \<otimes> inv u)]) \<subseteq> carrier G" - by (cases as, clarsimp+) - - from afs' uunit a'nunit acarr ascarr - have "factors G (as[0:=(as!0 \<otimes> inv u)]) a" - by (simp add: a factors_cong_unit) - - with cr - show "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a" by fast + finally have a: "a = a' \<otimes> inv u" . + + from ascarr uunit have cr: "set (as[0:=(as!0 \<otimes> inv u)]) \<subseteq> carrier G" + by (cases as) auto + + from afs' uunit a'nunit acarr ascarr have "factors G (as[0:=(as!0 \<otimes> inv u)]) a" + by (simp add: a factors_cong_unit) + with cr show "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a" + by fast qed (blast intro: factors_wfactors wfactors_unique) @@ -1788,11 +1636,9 @@ (* FIXME: use class_of x instead of closure_of {x} *) -abbreviation - "assocs G x == eq_closure_of (division_rel G) {x}" - -definition - "fmset G as = mset (map (\<lambda>a. assocs G a) as)" +abbreviation "assocs G x \<equiv> eq_closure_of (division_rel G) {x}" + +definition "fmset G as = mset (map (\<lambda>a. assocs G a) as)" text \<open>Helper lemmas\<close> @@ -1801,37 +1647,32 @@ assumes "y \<in> assocs G x" and "x \<in> carrier G" shows "assocs G x = assocs G y" -using assms -apply safe - apply (elim closure_ofE2, intro closure_ofI2[of _ _ y]) - apply (clarsimp, iprover intro: associated_trans associated_sym, simp+) -apply (elim closure_ofE2, intro closure_ofI2[of _ _ x]) - apply (clarsimp, iprover intro: associated_trans, simp+) -done + using assms + apply safe + apply (elim closure_ofE2, intro closure_ofI2[of _ _ y]) + apply (clarsimp, iprover intro: associated_trans associated_sym, simp+) + apply (elim closure_ofE2, intro closure_ofI2[of _ _ x]) + apply (clarsimp, iprover intro: associated_trans, simp+) + done lemma (in monoid) assocs_self: assumes "x \<in> carrier G" shows "x \<in> assocs G x" -using assms -by (fastforce intro: closure_ofI2) + using assms by (fastforce intro: closure_ofI2) lemma (in monoid) assocs_repr_independenceD: assumes repr: "assocs G x = assocs G y" and ycarr: "y \<in> carrier G" shows "y \<in> assocs G x" -unfolding repr -using ycarr -by (intro assocs_self) + unfolding repr using ycarr by (intro assocs_self) lemma (in comm_monoid) assocs_assoc: assumes "a \<in> assocs G b" and "b \<in> carrier G" shows "a \<sim> b" -using assms -by (elim closure_ofE2, simp) - -lemmas (in comm_monoid) assocs_eqD = - assocs_repr_independenceD[THEN assocs_assoc] + using assms by (elim closure_ofE2) simp + +lemmas (in comm_monoid) assocs_eqD = assocs_repr_independenceD[THEN assocs_assoc] subsubsection \<open>Comparing multisets\<close> @@ -1839,137 +1680,119 @@ lemma (in monoid) fmset_perm_cong: assumes prm: "as <~~> bs" shows "fmset G as = fmset G bs" -using perm_map[OF prm] unfolding mset_eq_perm fmset_def by blast + using perm_map[OF prm] unfolding mset_eq_perm fmset_def by blast lemma (in comm_monoid_cancel) eqc_listassoc_cong: assumes "as [\<sim>] bs" and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G" shows "map (assocs G) as = map (assocs G) bs" -using assms -apply (induct as arbitrary: bs, simp) -apply (clarsimp simp add: Cons_eq_map_conv list_all2_Cons1, safe) - apply (clarsimp elim!: closure_ofE2) defer 1 - apply (clarsimp elim!: closure_ofE2) defer 1 + using assms + apply (induct as arbitrary: bs, simp) + apply (clarsimp simp add: Cons_eq_map_conv list_all2_Cons1, safe) + apply (clarsimp elim!: closure_ofE2) defer 1 + apply (clarsimp elim!: closure_ofE2) defer 1 proof - fix a x z assume carr[simp]: "a \<in> carrier G" "x \<in> carrier G" "z \<in> carrier G" assume "x \<sim> a" also assume "a \<sim> z" finally have "x \<sim> z" by simp - with carr - show "x \<in> assocs G z" - by (intro closure_ofI2) simp+ + with carr show "x \<in> assocs G z" + by (intro closure_ofI2) simp_all next fix a x z assume carr[simp]: "a \<in> carrier G" "x \<in> carrier G" "z \<in> carrier G" assume "x \<sim> z" also assume [symmetric]: "a \<sim> z" finally have "x \<sim> a" by simp - with carr - show "x \<in> assocs G a" - by (intro closure_ofI2) simp+ + with carr show "x \<in> assocs G a" + by (intro closure_ofI2) simp_all qed lemma (in comm_monoid_cancel) fmset_listassoc_cong: - assumes "as [\<sim>] bs" + assumes "as [\<sim>] bs" and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G" shows "fmset G as = fmset G bs" -using assms -unfolding fmset_def -by (simp add: eqc_listassoc_cong) + using assms unfolding fmset_def by (simp add: eqc_listassoc_cong) lemma (in comm_monoid_cancel) ee_fmset: - assumes ee: "essentially_equal G as bs" + assumes ee: "essentially_equal G as bs" and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G" shows "fmset G as = fmset G bs" -using ee + using ee proof (elim essentially_equalE) fix as' assume prm: "as <~~> as'" - from prm ascarr - have as'carr: "set as' \<subseteq> carrier G" by (rule perm_closed) - - from prm - have "fmset G as = fmset G as'" by (rule fmset_perm_cong) + from prm ascarr have as'carr: "set as' \<subseteq> carrier G" + by (rule perm_closed) + + from prm have "fmset G as = fmset G as'" + by (rule fmset_perm_cong) also assume "as' [\<sim>] bs" - with as'carr bscarr - have "fmset G as' = fmset G bs" by (simp add: fmset_listassoc_cong) - finally - show "fmset G as = fmset G bs" . + with as'carr bscarr have "fmset G as' = fmset G bs" + by (simp add: fmset_listassoc_cong) + finally show "fmset G as = fmset G bs" . qed lemma (in monoid_cancel) fmset_ee__hlp_induct: assumes prm: "cas <~~> cbs" and cdef: "cas = map (assocs G) as" "cbs = map (assocs G) bs" - shows "\<forall>as bs. (cas <~~> cbs \<and> cas = map (assocs G) as \<and> - cbs = map (assocs G) bs) \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = cbs)" -apply (rule perm.induct[of cas cbs], rule prm) -apply safe apply (simp_all del: mset_map) - apply (simp add: map_eq_Cons_conv, blast) - apply force + shows "\<forall>as bs. (cas <~~> cbs \<and> cas = map (assocs G) as \<and> + cbs = map (assocs G) bs) \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = cbs)" + apply (rule perm.induct[of cas cbs], rule prm) + apply safe + apply (simp_all del: mset_map) + apply (simp add: map_eq_Cons_conv) + apply blast + apply force proof - fix ys as bs assume p1: "map (assocs G) as <~~> ys" and r1[rule_format]: - "\<forall>asa bs. map (assocs G) as = map (assocs G) asa \<and> - ys = map (assocs G) bs - \<longrightarrow> (\<exists>as'. asa <~~> as' \<and> map (assocs G) as' = map (assocs G) bs)" + "\<forall>asa bs. map (assocs G) as = map (assocs G) asa \<and> ys = map (assocs G) bs + \<longrightarrow> (\<exists>as'. asa <~~> as' \<and> map (assocs G) as' = map (assocs G) bs)" and p2: "ys <~~> map (assocs G) bs" - and r2[rule_format]: - "\<forall>as bsa. ys = map (assocs G) as \<and> - map (assocs G) bs = map (assocs G) bsa - \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bsa)" + and r2[rule_format]: "\<forall>as bsa. ys = map (assocs G) as \<and> map (assocs G) bs = map (assocs G) bsa + \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bsa)" and p3: "map (assocs G) as <~~> map (assocs G) bs" - from p1 - have "mset (map (assocs G) as) = mset ys" - by (simp add: mset_eq_perm del: mset_map) - hence setys: "set (map (assocs G) as) = set ys" by (rule mset_eq_setD) - - have "set (map (assocs G) as) = { assocs G x | x. x \<in> set as}" by clarsimp fast + from p1 have "mset (map (assocs G) as) = mset ys" + by (simp add: mset_eq_perm del: mset_map) + then have setys: "set (map (assocs G) as) = set ys" + by (rule mset_eq_setD) + + have "set (map (assocs G) as) = {assocs G x | x. x \<in> set as}" by auto with setys have "set ys \<subseteq> { assocs G x | x. x \<in> set as}" by simp - hence "\<exists>yy. ys = map (assocs G) yy" - apply (induct ys, simp, clarsimp) + then have "\<exists>yy. ys = map (assocs G) yy" + apply (induct ys) + apply simp + apply clarsimp proof - fix yy x - show "\<exists>yya. (assocs G x) # map (assocs G) yy = - map (assocs G) yya" - by (rule exI[of _ "x#yy"], simp) + show "\<exists>yya. (assocs G x) # map (assocs G) yy = map (assocs G) yya" + by (rule exI[of _ "x#yy"]) simp qed - from this obtain yy - where ys: "ys = map (assocs G) yy" - by auto - - from p1 ys - have "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) yy" - by (intro r1, simp) - from this obtain as' - where asas': "as <~~> as'" - and as'yy: "map (assocs G) as' = map (assocs G) yy" - by auto - - from p2 ys - have "\<exists>as'. yy <~~> as' \<and> map (assocs G) as' = map (assocs G) bs" - by (intro r2, simp) - from this obtain as'' - where yyas'': "yy <~~> as''" - and as''bs: "map (assocs G) as'' = map (assocs G) bs" - by auto - - from as'yy and yyas'' - have "\<exists>cs. as' <~~> cs \<and> map (assocs G) cs = map (assocs G) as''" - by (rule perm_map_switch) - from this obtain cs - where as'cs: "as' <~~> cs" - and csas'': "map (assocs G) cs = map (assocs G) as''" - by auto - - from asas' and as'cs - have ascs: "as <~~> cs" by fast - from csas'' and as''bs - have "map (assocs G) cs = map (assocs G) bs" by simp - from ascs and this - show "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bs" by fast + then obtain yy where ys: "ys = map (assocs G) yy" + by auto + + from p1 ys have "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) yy" + by (intro r1) simp + then obtain as' where asas': "as <~~> as'" and as'yy: "map (assocs G) as' = map (assocs G) yy" + by auto + + from p2 ys have "\<exists>as'. yy <~~> as' \<and> map (assocs G) as' = map (assocs G) bs" + by (intro r2) simp + then obtain as'' where yyas'': "yy <~~> as''" and as''bs: "map (assocs G) as'' = map (assocs G) bs" + by auto + + from as'yy and yyas'' have "\<exists>cs. as' <~~> cs \<and> map (assocs G) cs = map (assocs G) as''" + by (rule perm_map_switch) + then obtain cs where as'cs: "as' <~~> cs" and csas'': "map (assocs G) cs = map (assocs G) as''" + by auto + + from asas' and as'cs have ascs: "as <~~> cs" by fast + from csas'' and as''bs have "map (assocs G) cs = map (assocs G) bs" by simp + with ascs show "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bs" by fast qed lemma (in comm_monoid_cancel) fmset_ee: @@ -1977,48 +1800,42 @@ and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G" shows "essentially_equal G as bs" proof - - from mset - have mpp: "map (assocs G) as <~~> map (assocs G) bs" - by (simp add: fmset_def mset_eq_perm del: mset_map) + from mset have mpp: "map (assocs G) as <~~> map (assocs G) bs" + by (simp add: fmset_def mset_eq_perm del: mset_map) have "\<exists>cas. cas = map (assocs G) as" by simp - from this obtain cas where cas: "cas = map (assocs G) as" by simp + then obtain cas where cas: "cas = map (assocs G) as" by simp have "\<exists>cbs. cbs = map (assocs G) bs" by simp - from this obtain cbs where cbs: "cbs = map (assocs G) bs" by simp - - from cas cbs mpp - have [rule_format]: - "\<forall>as bs. (cas <~~> cbs \<and> cas = map (assocs G) as \<and> - cbs = map (assocs G) bs) - \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = cbs)" - by (intro fmset_ee__hlp_induct, simp+) - with mpp cas cbs - have "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bs" - by simp - - from this obtain as' - where tp: "as <~~> as'" - and tm: "map (assocs G) as' = map (assocs G) bs" - by auto - from tm have lene: "length as' = length bs" by (rule map_eq_imp_length_eq) - from tp have "set as = set as'" by (simp add: mset_eq_perm mset_eq_setD) - with ascarr - have as'carr: "set as' \<subseteq> carrier G" by simp + then obtain cbs where cbs: "cbs = map (assocs G) bs" by simp + + from cas cbs mpp have [rule_format]: + "\<forall>as bs. (cas <~~> cbs \<and> cas = map (assocs G) as \<and> cbs = map (assocs G) bs) + \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = cbs)" + by (intro fmset_ee__hlp_induct, simp+) + with mpp cas cbs have "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bs" + by simp + + then obtain as' where tp: "as <~~> as'" and tm: "map (assocs G) as' = map (assocs G) bs" + by auto + from tm have lene: "length as' = length bs" + by (rule map_eq_imp_length_eq) + from tp have "set as = set as'" + by (simp add: mset_eq_perm mset_eq_setD) + with ascarr have as'carr: "set as' \<subseteq> carrier G" + by simp from tm as'carr[THEN subsetD] bscarr[THEN subsetD] have "as' [\<sim>] bs" by (induct as' arbitrary: bs) (simp, fastforce dest: assocs_eqD[THEN associated_sym]) - - from tp and this - show "essentially_equal G as bs" by (fast intro: essentially_equalI) + with tp show "essentially_equal G as bs" + by (fast intro: essentially_equalI) qed lemma (in comm_monoid_cancel) ee_is_fmset: assumes "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G" shows "essentially_equal G as bs = (fmset G as = fmset G bs)" -using assms -by (fast intro: ee_fmset fmset_ee) + using assms by (fast intro: ee_fmset fmset_ee) subsubsection \<open>Interpreting multisets as factorizations\<close> @@ -2028,105 +1845,90 @@ shows "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> fmset G cs = Cs" proof - have "\<exists>Cs'. Cs = mset Cs'" - by (rule surjE[OF surj_mset], fast) - from this obtain Cs' - where Cs: "Cs = mset Cs'" - by auto + by (rule surjE[OF surj_mset], fast) + then obtain Cs' where Cs: "Cs = mset Cs'" + by auto have "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> mset (map (assocs G) cs) = Cs" - using elems - unfolding Cs + using elems + unfolding Cs apply (induct Cs', simp) proof (clarsimp simp del: mset_map) - fix a Cs' cs + fix a Cs' cs assume ih: "\<And>X. X = a \<or> X \<in> set Cs' \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x" and csP: "\<forall>x\<in>set cs. P x" and mset: "mset (map (assocs G) cs) = mset Cs'" - from ih - have "\<exists>x. P x \<and> a = assocs G x" by fast - from this obtain c - where cP: "P c" - and a: "a = assocs G c" - by auto - from cP csP - have tP: "\<forall>x\<in>set (c#cs). P x" by simp - from mset a - have "mset (map (assocs G) (c#cs)) = add_mset a (mset Cs')" by simp - from tP this - show "\<exists>cs. (\<forall>x\<in>set cs. P x) \<and> - mset (map (assocs G) cs) = - add_mset a (mset Cs')" by fast + from ih have "\<exists>x. P x \<and> a = assocs G x" by fast + then obtain c where cP: "P c" and a: "a = assocs G c" by auto + from cP csP have tP: "\<forall>x\<in>set (c#cs). P x" by simp + from mset a have "mset (map (assocs G) (c#cs)) = add_mset a (mset Cs')" by simp + with tP show "\<exists>cs. (\<forall>x\<in>set cs. P x) \<and> mset (map (assocs G) cs) = add_mset a (mset Cs')" by fast qed - thus ?thesis by (simp add: fmset_def) + then show ?thesis by (simp add: fmset_def) qed lemma (in monoid) mset_wfactorsEx: - assumes elems: "\<And>X. X \<in> set_mset Cs - \<Longrightarrow> \<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x" + assumes elems: "\<And>X. X \<in> set_mset Cs \<Longrightarrow> \<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x" shows "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> fmset G cs = Cs" proof - have "\<exists>cs. (\<forall>c\<in>set cs. c \<in> carrier G \<and> irreducible G c) \<and> fmset G cs = Cs" - by (intro mset_fmsetEx, rule elems) - from this obtain cs - where p[rule_format]: "\<forall>c\<in>set cs. c \<in> carrier G \<and> irreducible G c" - and Cs[symmetric]: "fmset G cs = Cs" - by auto - - from p - have cscarr: "set cs \<subseteq> carrier G" by fast - - from p - have "\<exists>c. c \<in> carrier G \<and> wfactors G cs c" - by (intro wfactors_prod_exists) fast+ - from this obtain c - where ccarr: "c \<in> carrier G" - and cfs: "wfactors G cs c" - by auto - - with cscarr Cs - show ?thesis by fast + by (intro mset_fmsetEx, rule elems) + then obtain cs where p[rule_format]: "\<forall>c\<in>set cs. c \<in> carrier G \<and> irreducible G c" + and Cs[symmetric]: "fmset G cs = Cs" by auto + + from p have cscarr: "set cs \<subseteq> carrier G" by fast + from p have "\<exists>c. c \<in> carrier G \<and> wfactors G cs c" + by (intro wfactors_prod_exists) auto + then obtain c where ccarr: "c \<in> carrier G" and cfs: "wfactors G cs c" by auto + with cscarr Cs show ?thesis by fast qed subsubsection \<open>Multiplication on multisets\<close> lemma (in factorial_monoid) mult_wfactors_fmset: - assumes afs: "wfactors G as a" and bfs: "wfactors G bs b" and cfs: "wfactors G cs (a \<otimes> b)" + assumes afs: "wfactors G as a" + and bfs: "wfactors G bs b" + and cfs: "wfactors G cs (a \<otimes> b)" and carr: "a \<in> carrier G" "b \<in> carrier G" "set as \<subseteq> carrier G" "set bs \<subseteq> carrier G" "set cs \<subseteq> carrier G" shows "fmset G cs = fmset G as + fmset G bs" proof - - from assms - have "wfactors G (as @ bs) (a \<otimes> b)" by (intro wfactors_mult) - with carr cfs - have "essentially_equal G cs (as@bs)" by (intro ee_wfactorsI[of "a\<otimes>b" "a\<otimes>b"], simp+) - with carr - have "fmset G cs = fmset G (as@bs)" by (intro ee_fmset, simp+) - also have "fmset G (as@bs) = fmset G as + fmset G bs" by (simp add: fmset_def) + from assms have "wfactors G (as @ bs) (a \<otimes> b)" + by (intro wfactors_mult) + with carr cfs have "essentially_equal G cs (as@bs)" + by (intro ee_wfactorsI[of "a\<otimes>b" "a\<otimes>b"]) simp_all + with carr have "fmset G cs = fmset G (as@bs)" + by (intro ee_fmset) simp_all + also have "fmset G (as@bs) = fmset G as + fmset G bs" + by (simp add: fmset_def) finally show "fmset G cs = fmset G as + fmset G bs" . qed lemma (in factorial_monoid) mult_factors_fmset: - assumes afs: "factors G as a" and bfs: "factors G bs b" and cfs: "factors G cs (a \<otimes> b)" + assumes afs: "factors G as a" + and bfs: "factors G bs b" + and cfs: "factors G cs (a \<otimes> b)" and "set as \<subseteq> carrier G" "set bs \<subseteq> carrier G" "set cs \<subseteq> carrier G" shows "fmset G cs = fmset G as + fmset G bs" -using assms -by (blast intro: factors_wfactors mult_wfactors_fmset) + using assms by (blast intro: factors_wfactors mult_wfactors_fmset) lemma (in comm_monoid_cancel) fmset_wfactors_mult: assumes mset: "fmset G cs = fmset G as + fmset G bs" and carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" - "set as \<subseteq> carrier G" "set bs \<subseteq> carrier G" "set cs \<subseteq> carrier G" + "set as \<subseteq> carrier G" "set bs \<subseteq> carrier G" "set cs \<subseteq> carrier G" and fs: "wfactors G as a" "wfactors G bs b" "wfactors G cs c" shows "c \<sim> a \<otimes> b" proof - - from carr fs - have m: "wfactors G (as @ bs) (a \<otimes> b)" by (intro wfactors_mult) - - from mset - have "fmset G cs = fmset G (as@bs)" by (simp add: fmset_def) - then have "essentially_equal G cs (as@bs)" by (rule fmset_ee) (simp add: carr)+ - then show "c \<sim> a \<otimes> b" by (rule ee_wfactorsD[of "cs" "as@bs"]) (simp add: assms m)+ + from carr fs have m: "wfactors G (as @ bs) (a \<otimes> b)" + by (intro wfactors_mult) + + from mset have "fmset G cs = fmset G (as@bs)" + by (simp add: fmset_def) + then have "essentially_equal G cs (as@bs)" + by (rule fmset_ee) (simp_all add: carr) + then show "c \<sim> a \<otimes> b" + by (rule ee_wfactorsD[of "cs" "as@bs"]) (simp_all add: assms m) qed @@ -2134,32 +1936,34 @@ lemma (in factorial_monoid) divides_fmsubset: assumes ab: "a divides b" - and afs: "wfactors G as a" and bfs: "wfactors G bs b" + and afs: "wfactors G as a" + and bfs: "wfactors G bs b" and carr: "a \<in> carrier G" "b \<in> carrier G" "set as \<subseteq> carrier G" "set bs \<subseteq> carrier G" shows "fmset G as \<le># fmset G bs" -using ab + using ab proof (elim dividesE) fix c assume ccarr: "c \<in> carrier G" - hence "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c" by (rule wfactors_exist) - from this obtain cs - where cscarr: "set cs \<subseteq> carrier G" - and cfs: "wfactors G cs c" by auto + then have "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c" + by (rule wfactors_exist) + then obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfs: "wfactors G cs c" + by auto note carr = carr ccarr cscarr assume "b = a \<otimes> c" - with afs bfs cfs carr - have "fmset G bs = fmset G as + fmset G cs" - by (intro mult_wfactors_fmset[OF afs cfs]) simp+ - - thus ?thesis by simp + with afs bfs cfs carr have "fmset G bs = fmset G as + fmset G cs" + by (intro mult_wfactors_fmset[OF afs cfs]) simp_all + then show ?thesis by simp qed lemma (in comm_monoid_cancel) fmsubset_divides: assumes msubset: "fmset G as \<le># fmset G bs" - and afs: "wfactors G as a" and bfs: "wfactors G bs b" - and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" - and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G" + and afs: "wfactors G as a" + and bfs: "wfactors G bs b" + and acarr: "a \<in> carrier G" + and bcarr: "b \<in> carrier G" + and ascarr: "set as \<subseteq> carrier G" + and bscarr: "set bs \<subseteq> carrier G" shows "a divides b" proof - from afs have airr: "\<forall>a \<in> set as. irreducible G a" by (fast elim: wfactorsE) @@ -2169,48 +1973,46 @@ proof (intro mset_wfactorsEx, simp) fix X assume "X \<in># fmset G bs - fmset G as" - hence "X \<in># fmset G bs" by (rule in_diffD) - hence "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def) - hence "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct bs) auto - from this obtain x - where xbs: "x \<in> set bs" - and X: "X = assocs G x" - by auto - + then have "X \<in># fmset G bs" by (rule in_diffD) + then have "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def) + then have "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct bs) auto + then obtain x where xbs: "x \<in> set bs" and X: "X = assocs G x" by auto with bscarr have xcarr: "x \<in> carrier G" by fast from xbs birr have xirr: "irreducible G x" by simp - from xcarr and xirr and X - show "\<exists>x. x \<in> carrier G \<and> irreducible G x \<and> X = assocs G x" by fast + from xcarr and xirr and X show "\<exists>x. x \<in> carrier G \<and> irreducible G x \<and> X = assocs G x" + by fast qed - from this obtain c cs - where ccarr: "c \<in> carrier G" - and cscarr: "set cs \<subseteq> carrier G" + then obtain c cs + where ccarr: "c \<in> carrier G" + and cscarr: "set cs \<subseteq> carrier G" and csf: "wfactors G cs c" and csmset: "fmset G cs = fmset G bs - fmset G as" by auto from csmset msubset - have "fmset G bs = fmset G as + fmset G cs" - by (simp add: multiset_eq_iff subseteq_mset_def) - hence basc: "b \<sim> a \<otimes> c" - by (rule fmset_wfactors_mult) fact+ - - thus ?thesis + have "fmset G bs = fmset G as + fmset G cs" + by (simp add: multiset_eq_iff subseteq_mset_def) + then have basc: "b \<sim> a \<otimes> c" + by (rule fmset_wfactors_mult) fact+ + then show ?thesis proof (elim associatedE2) fix u assume "u \<in> Units G" "b = a \<otimes> c \<otimes> u" - with acarr ccarr - show "a divides b" by (fast intro: dividesI[of "c \<otimes> u"] m_assoc) - qed (simp add: acarr bcarr ccarr)+ + with acarr ccarr show "a divides b" + by (fast intro: dividesI[of "c \<otimes> u"] m_assoc) + qed (simp_all add: acarr bcarr ccarr) qed lemma (in factorial_monoid) divides_as_fmsubset: - assumes "wfactors G as a" and "wfactors G bs b" - and "a \<in> carrier G" and "b \<in> carrier G" - and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G" + assumes "wfactors G as a" + and "wfactors G bs b" + and "a \<in> carrier G" + and "b \<in> carrier G" + and "set as \<subseteq> carrier G" + and "set bs \<subseteq> carrier G" shows "a divides b = (fmset G as \<le># fmset G bs)" -using assms -by (blast intro: divides_fmsubset fmsubset_divides) + using assms + by (blast intro: divides_fmsubset fmsubset_divides) text \<open>Proper factors on multisets\<close> @@ -2218,35 +2020,41 @@ lemma (in factorial_monoid) fmset_properfactor: assumes asubb: "fmset G as \<le># fmset G bs" and anb: "fmset G as \<noteq> fmset G bs" - and "wfactors G as a" and "wfactors G bs b" - and "a \<in> carrier G" and "b \<in> carrier G" - and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G" + and "wfactors G as a" + and "wfactors G bs b" + and "a \<in> carrier G" + and "b \<in> carrier G" + and "set as \<subseteq> carrier G" + and "set bs \<subseteq> carrier G" shows "properfactor G a b" -apply (rule properfactorI) -apply (rule fmsubset_divides[of as bs], fact+) + apply (rule properfactorI) + apply (rule fmsubset_divides[of as bs], fact+) proof assume "b divides a" - hence "fmset G bs \<le># fmset G as" - by (rule divides_fmsubset) fact+ - with asubb - have "fmset G as = fmset G bs" by (rule subset_mset.antisym) - with anb - show "False" .. + then have "fmset G bs \<le># fmset G as" + by (rule divides_fmsubset) fact+ + with asubb have "fmset G as = fmset G bs" + by (rule subset_mset.antisym) + with anb show False .. qed lemma (in factorial_monoid) properfactor_fmset: assumes pf: "properfactor G a b" - and "wfactors G as a" and "wfactors G bs b" - and "a \<in> carrier G" and "b \<in> carrier G" - and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G" + and "wfactors G as a" + and "wfactors G bs b" + and "a \<in> carrier G" + and "b \<in> carrier G" + and "set as \<subseteq> carrier G" + and "set bs \<subseteq> carrier G" shows "fmset G as \<le># fmset G bs \<and> fmset G as \<noteq> fmset G bs" -using pf -apply (elim properfactorE) -apply rule - apply (intro divides_fmsubset, assumption) - apply (rule assms)+ -apply (metis assms divides_fmsubset fmsubset_divides) -done + using pf + apply (elim properfactorE) + apply rule + apply (intro divides_fmsubset, assumption) + apply (rule assms)+ + using assms(2,3,4,6,7) divides_as_fmsubset + apply auto + done subsection \<open>Irreducible Elements are Prime\<close> @@ -2254,88 +2062,78 @@ assumes pirr: "irreducible G p" and pcarr: "p \<in> carrier G" shows "prime G p" -using pirr + using pirr proof (elim irreducibleE, intro primeI) fix a b assume acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and pdvdab: "p divides (a \<otimes> b)" and pnunit: "p \<notin> Units G" assume irreduc[rule_format]: - "\<forall>b. b \<in> carrier G \<and> properfactor G b p \<longrightarrow> b \<in> Units G" + "\<forall>b. b \<in> carrier G \<and> properfactor G b p \<longrightarrow> b \<in> Units G" from pdvdab - have "\<exists>c\<in>carrier G. a \<otimes> b = p \<otimes> c" by (rule dividesD) - from this obtain c - where ccarr: "c \<in> carrier G" - and abpc: "a \<otimes> b = p \<otimes> c" - by auto - - from acarr have "\<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs a" by (rule wfactors_exist) - from this obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a" by auto - - from bcarr have "\<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs b" by (rule wfactors_exist) - from this obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfs: "wfactors G bs b" by auto - - from ccarr have "\<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs c" by (rule wfactors_exist) - from this obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfs: "wfactors G cs c" by auto + have "\<exists>c\<in>carrier G. a \<otimes> b = p \<otimes> c" by (rule dividesD) + then obtain c where ccarr: "c \<in> carrier G" and abpc: "a \<otimes> b = p \<otimes> c" + by auto + + from acarr have "\<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs a" + by (rule wfactors_exist) + then obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a" + by auto + + from bcarr have "\<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs b" + by (rule wfactors_exist) + then obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfs: "wfactors G bs b" + by auto + + from ccarr have "\<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs c" + by (rule wfactors_exist) + then obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfs: "wfactors G cs c" + by auto note carr[simp] = pcarr acarr bcarr ccarr ascarr bscarr cscarr - from afs and bfs - have abfs: "wfactors G (as @ bs) (a \<otimes> b)" by (rule wfactors_mult) fact+ - - from pirr cfs - have pcfs: "wfactors G (p # cs) (p \<otimes> c)" by (rule wfactors_mult_single) fact+ - with abpc - have abfs': "wfactors G (p # cs) (a \<otimes> b)" by simp - - from abfs' abfs - have "essentially_equal G (p # cs) (as @ bs)" - by (rule wfactors_unique) simp+ - - hence "\<exists>ds. p # cs <~~> ds \<and> ds [\<sim>] (as @ bs)" - by (fast elim: essentially_equalE) - from this obtain ds - where "p # cs <~~> ds" - and dsassoc: "ds [\<sim>] (as @ bs)" - by auto - + from afs and bfs have abfs: "wfactors G (as @ bs) (a \<otimes> b)" + by (rule wfactors_mult) fact+ + + from pirr cfs have pcfs: "wfactors G (p # cs) (p \<otimes> c)" + by (rule wfactors_mult_single) fact+ + with abpc have abfs': "wfactors G (p # cs) (a \<otimes> b)" + by simp + + from abfs' abfs have "essentially_equal G (p # cs) (as @ bs)" + by (rule wfactors_unique) simp+ + + then have "\<exists>ds. p # cs <~~> ds \<and> ds [\<sim>] (as @ bs)" + by (fast elim: essentially_equalE) + then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\<sim>] (as @ bs)" + by auto then have "p \<in> set ds" - by (simp add: perm_set_eq[symmetric]) - with dsassoc - have "\<exists>p'. p' \<in> set (as@bs) \<and> p \<sim> p'" - unfolding list_all2_conv_all_nth set_conv_nth - by force - - from this obtain p' - where "p' \<in> set (as@bs)" - and pp': "p \<sim> p'" - by auto - - hence "p' \<in> set as \<or> p' \<in> set bs" by simp - moreover - { - assume p'elem: "p' \<in> set as" + by (simp add: perm_set_eq[symmetric]) + with dsassoc have "\<exists>p'. p' \<in> set (as@bs) \<and> p \<sim> p'" + unfolding list_all2_conv_all_nth set_conv_nth by force + then obtain p' where "p' \<in> set (as@bs)" and pp': "p \<sim> p'" + by auto + then consider "p' \<in> set as" | "p' \<in> set bs" by auto + then show "p divides a \<or> p divides b" + proof cases + case 1 with ascarr have [simp]: "p' \<in> carrier G" by fast note pp' also from afs - have "p' divides a" by (rule wfactors_dividesI) fact+ - finally - have "p divides a" by simp - } - moreover - { - assume p'elem: "p' \<in> set bs" + have "p' divides a" by (rule wfactors_dividesI) fact+ + finally have "p divides a" by simp + then show ?thesis .. + next + case 2 with bscarr have [simp]: "p' \<in> carrier G" by fast note pp' also from bfs - have "p' divides b" by (rule wfactors_dividesI) fact+ - finally - have "p divides b" by simp - } - ultimately - show "p divides a \<or> p divides b" by fast + have "p' divides b" by (rule wfactors_dividesI) fact+ + finally have "p divides b" by simp + then show ?thesis .. + qed qed @@ -2344,145 +2142,121 @@ assumes pirr: "irreducible G p" and pcarr: "p \<in> carrier G" shows "prime G p" -using pirr -apply (elim irreducibleE, intro primeI) - apply assumption + using pirr + apply (elim irreducibleE, intro primeI) + apply assumption proof - fix a b - assume acarr: "a \<in> carrier G" + assume acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and pdvdab: "p divides (a \<otimes> b)" - assume irreduc[rule_format]: - "\<forall>b. b \<in> carrier G \<and> properfactor G b p \<longrightarrow> b \<in> Units G" - from pdvdab - have "\<exists>c\<in>carrier G. a \<otimes> b = p \<otimes> c" by (rule dividesD) - from this obtain c - where ccarr: "c \<in> carrier G" - and abpc: "a \<otimes> b = p \<otimes> c" - by auto + assume irreduc[rule_format]: "\<forall>b. b \<in> carrier G \<and> properfactor G b p \<longrightarrow> b \<in> Units G" + from pdvdab have "\<exists>c\<in>carrier G. a \<otimes> b = p \<otimes> c" + by (rule dividesD) + then obtain c where ccarr: "c \<in> carrier G" and abpc: "a \<otimes> b = p \<otimes> c" + by auto note [simp] = pcarr acarr bcarr ccarr show "p divides a \<or> p divides b" proof (cases "a \<in> Units G") - assume aunit: "a \<in> Units G" + case aunit: True note pdvdab also have "a \<otimes> b = b \<otimes> a" by (simp add: m_comm) - also from aunit - have bab: "b \<otimes> a \<sim> b" - by (intro associatedI2[of "a"], simp+) - finally - have "p divides b" by simp - thus "p divides a \<or> p divides b" .. + also from aunit have bab: "b \<otimes> a \<sim> b" + by (intro associatedI2[of "a"], simp+) + finally have "p divides b" by simp + then show ?thesis .. next - assume anunit: "a \<notin> Units G" - - show "p divides a \<or> p divides b" + case anunit: False + show ?thesis proof (cases "b \<in> Units G") - assume bunit: "b \<in> Units G" - + case bunit: True note pdvdab also from bunit - have baa: "a \<otimes> b \<sim> a" - by (intro associatedI2[of "b"], simp+) - finally - have "p divides a" by simp - thus "p divides a \<or> p divides b" .. + have baa: "a \<otimes> b \<sim> a" + by (intro associatedI2[of "b"], simp+) + finally have "p divides a" by simp + then show ?thesis .. next - assume bnunit: "b \<notin> Units G" - + case bnunit: False have cnunit: "c \<notin> Units G" proof (rule ccontr, simp) assume cunit: "c \<in> Units G" - from bnunit - have "properfactor G a (a \<otimes> b)" - by (intro properfactorI3[of _ _ b], simp+) + from bnunit have "properfactor G a (a \<otimes> b)" + by (intro properfactorI3[of _ _ b], simp+) also note abpc - also from cunit - have "p \<otimes> c \<sim> p" - by (intro associatedI2[of c], simp+) - finally - have "properfactor G a p" by simp - - with acarr - have "a \<in> Units G" by (fast intro: irreduc) - with anunit - show "False" .. + also from cunit have "p \<otimes> c \<sim> p" + by (intro associatedI2[of c], simp+) + finally have "properfactor G a p" by simp + with acarr have "a \<in> Units G" by (fast intro: irreduc) + with anunit show False .. qed have abnunit: "a \<otimes> b \<notin> Units G" proof clarsimp - assume abunit: "a \<otimes> b \<in> Units G" - hence "a \<in> Units G" by (rule unit_factor) fact+ - with anunit - show "False" .. + assume "a \<otimes> b \<in> Units G" + then have "a \<in> Units G" by (rule unit_factor) fact+ + with anunit show False .. qed - from acarr anunit have "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a" by (rule factors_exist) - then obtain as where ascarr: "set as \<subseteq> carrier G" and afac: "factors G as a" by auto - - from bcarr bnunit have "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs b" by (rule factors_exist) - then obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfac: "factors G bs b" by auto - - from ccarr cnunit have "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs c" by (rule factors_exist) - then obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfac: "factors G cs c" by auto + from acarr anunit have "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a" + by (rule factors_exist) + then obtain as where ascarr: "set as \<subseteq> carrier G" and afac: "factors G as a" + by auto + + from bcarr bnunit have "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs b" + by (rule factors_exist) + then obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfac: "factors G bs b" + by auto + + from ccarr cnunit have "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs c" + by (rule factors_exist) + then obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfac: "factors G cs c" + by auto note [simp] = ascarr bscarr cscarr - from afac and bfac - have abfac: "factors G (as @ bs) (a \<otimes> b)" by (rule factors_mult) fact+ - - from pirr cfac - have pcfac: "factors G (p # cs) (p \<otimes> c)" by (rule factors_mult_single) fact+ - with abpc - have abfac': "factors G (p # cs) (a \<otimes> b)" by simp - - from abfac' abfac - have "essentially_equal G (p # cs) (as @ bs)" - by (rule factors_unique) (fact | simp)+ - - hence "\<exists>ds. p # cs <~~> ds \<and> ds [\<sim>] (as @ bs)" - by (fast elim: essentially_equalE) - from this obtain ds - where "p # cs <~~> ds" - and dsassoc: "ds [\<sim>] (as @ bs)" - by auto - + from afac and bfac have abfac: "factors G (as @ bs) (a \<otimes> b)" + by (rule factors_mult) fact+ + + from pirr cfac have pcfac: "factors G (p # cs) (p \<otimes> c)" + by (rule factors_mult_single) fact+ + with abpc have abfac': "factors G (p # cs) (a \<otimes> b)" + by simp + + from abfac' abfac have "essentially_equal G (p # cs) (as @ bs)" + by (rule factors_unique) (fact | simp)+ + then have "\<exists>ds. p # cs <~~> ds \<and> ds [\<sim>] (as @ bs)" + by (fast elim: essentially_equalE) + then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\<sim>] (as @ bs)" + by auto then have "p \<in> set ds" - by (simp add: perm_set_eq[symmetric]) - with dsassoc - have "\<exists>p'. p' \<in> set (as@bs) \<and> p \<sim> p'" - unfolding list_all2_conv_all_nth set_conv_nth - by force - - from this obtain p' - where "p' \<in> set (as@bs)" - and pp': "p \<sim> p'" by auto - - hence "p' \<in> set as \<or> p' \<in> set bs" by simp - moreover - { - assume p'elem: "p' \<in> set as" + by (simp add: perm_set_eq[symmetric]) + with dsassoc have "\<exists>p'. p' \<in> set (as@bs) \<and> p \<sim> p'" + unfolding list_all2_conv_all_nth set_conv_nth by force + then obtain p' where "p' \<in> set (as@bs)" and pp': "p \<sim> p'" + by auto + then consider "p' \<in> set as" | "p' \<in> set bs" by auto + then show "p divides a \<or> p divides b" + proof cases + case 1 with ascarr have [simp]: "p' \<in> carrier G" by fast note pp' - also from afac p'elem - have "p' divides a" by (rule factors_dividesI) fact+ - finally - have "p divides a" by simp - } - moreover - { - assume p'elem: "p' \<in> set bs" + also from afac 1 have "p' divides a" by (rule factors_dividesI) fact+ + finally have "p divides a" by simp + then show ?thesis .. + next + case 2 with bscarr have [simp]: "p' \<in> carrier G" by fast note pp' also from bfac - have "p' divides b" by (rule factors_dividesI) fact+ + have "p' divides b" by (rule factors_dividesI) fact+ finally have "p divides b" by simp - } - ultimately - show "p divides a \<or> p divides b" by fast + then show ?thesis .. + qed qed qed qed @@ -2492,39 +2266,31 @@ subsubsection \<open>Definitions\<close> -definition - isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \<Rightarrow> bool" ("(_ gcdof\<index> _ _)" [81,81,81] 80) +definition isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \<Rightarrow> bool" ("(_ gcdof\<index> _ _)" [81,81,81] 80) where "x gcdof\<^bsub>G\<^esub> a b \<longleftrightarrow> x divides\<^bsub>G\<^esub> a \<and> x divides\<^bsub>G\<^esub> b \<and> (\<forall>y\<in>carrier G. (y divides\<^bsub>G\<^esub> a \<and> y divides\<^bsub>G\<^esub> b \<longrightarrow> y divides\<^bsub>G\<^esub> x))" -definition - islcm :: "[_, 'a, 'a, 'a] \<Rightarrow> bool" ("(_ lcmof\<index> _ _)" [81,81,81] 80) +definition islcm :: "[_, 'a, 'a, 'a] \<Rightarrow> bool" ("(_ lcmof\<index> _ _)" [81,81,81] 80) where "x lcmof\<^bsub>G\<^esub> a b \<longleftrightarrow> a divides\<^bsub>G\<^esub> x \<and> b divides\<^bsub>G\<^esub> x \<and> (\<forall>y\<in>carrier G. (a divides\<^bsub>G\<^esub> y \<and> b divides\<^bsub>G\<^esub> y \<longrightarrow> x divides\<^bsub>G\<^esub> y))" -definition - somegcd :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" +definition somegcd :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where "somegcd G a b = (SOME x. x \<in> carrier G \<and> x gcdof\<^bsub>G\<^esub> a b)" -definition - somelcm :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" +definition somelcm :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where "somelcm G a b = (SOME x. x \<in> carrier G \<and> x lcmof\<^bsub>G\<^esub> a b)" -definition - "SomeGcd G A = inf (division_rel G) A" +definition "SomeGcd G A = inf (division_rel G) A" locale gcd_condition_monoid = comm_monoid_cancel + - assumes gcdof_exists: - "\<lbrakk>a \<in> carrier G; b \<in> carrier G\<rbrakk> \<Longrightarrow> \<exists>c. c \<in> carrier G \<and> c gcdof a b" + assumes gcdof_exists: "\<lbrakk>a \<in> carrier G; b \<in> carrier G\<rbrakk> \<Longrightarrow> \<exists>c. c \<in> carrier G \<and> c gcdof a b" locale primeness_condition_monoid = comm_monoid_cancel + - assumes irreducible_prime: - "\<lbrakk>a \<in> carrier G; irreducible G a\<rbrakk> \<Longrightarrow> prime G a" + assumes irreducible_prime: "\<lbrakk>a \<in> carrier G; irreducible G a\<rbrakk> \<Longrightarrow> prime G a" locale divisor_chain_condition_monoid = comm_monoid_cancel + - assumes division_wellfounded: - "wf {(x, y). x \<in> carrier G \<and> y \<in> carrier G \<and> properfactor G x y}" + assumes division_wellfounded: "wf {(x, y). x \<in> carrier G \<and> y \<in> carrier G \<and> properfactor G x y}" subsubsection \<open>Connections to \texttt{Lattice.thy}\<close> @@ -2532,222 +2298,208 @@ lemma gcdof_greatestLower: fixes G (structure) assumes carr[simp]: "a \<in> carrier G" "b \<in> carrier G" - shows "(x \<in> carrier G \<and> x gcdof a b) = - greatest (division_rel G) x (Lower (division_rel G) {a, b})" -unfolding isgcd_def greatest_def Lower_def elem_def -by auto + shows "(x \<in> carrier G \<and> x gcdof a b) = greatest (division_rel G) x (Lower (division_rel G) {a, b})" + by (auto simp: isgcd_def greatest_def Lower_def elem_def) lemma lcmof_leastUpper: fixes G (structure) assumes carr[simp]: "a \<in> carrier G" "b \<in> carrier G" - shows "(x \<in> carrier G \<and> x lcmof a b) = - least (division_rel G) x (Upper (division_rel G) {a, b})" -unfolding islcm_def least_def Upper_def elem_def -by auto + shows "(x \<in> carrier G \<and> x lcmof a b) = least (division_rel G) x (Upper (division_rel G) {a, b})" + by (auto simp: islcm_def least_def Upper_def elem_def) lemma somegcd_meet: fixes G (structure) assumes carr: "a \<in> carrier G" "b \<in> carrier G" shows "somegcd G a b = meet (division_rel G) a b" -unfolding somegcd_def meet_def inf_def -by (simp add: gcdof_greatestLower[OF carr]) + by (simp add: somegcd_def meet_def inf_def gcdof_greatestLower[OF carr]) lemma (in monoid) isgcd_divides_l: assumes "a divides b" and "a \<in> carrier G" "b \<in> carrier G" shows "a gcdof a b" -using assms -unfolding isgcd_def -by fast + using assms unfolding isgcd_def by fast lemma (in monoid) isgcd_divides_r: assumes "b divides a" and "a \<in> carrier G" "b \<in> carrier G" shows "b gcdof a b" -using assms -unfolding isgcd_def -by fast + using assms unfolding isgcd_def by fast subsubsection \<open>Existence of gcd and lcm\<close> lemma (in factorial_monoid) gcdof_exists: - assumes acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" + assumes acarr: "a \<in> carrier G" + and bcarr: "b \<in> carrier G" shows "\<exists>c. c \<in> carrier G \<and> c gcdof a b" proof - from acarr have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" by (rule wfactors_exist) - from this obtain as - where ascarr: "set as \<subseteq> carrier G" - and afs: "wfactors G as a" - by auto - from afs have airr: "\<forall>a \<in> set as. irreducible G a" by (fast elim: wfactorsE) - - from bcarr have "\<exists>bs. set bs \<subseteq> carrier G \<and> wfactors G bs b" by (rule wfactors_exist) - from this obtain bs - where bscarr: "set bs \<subseteq> carrier G" - and bfs: "wfactors G bs b" - by auto - from bfs have birr: "\<forall>b \<in> set bs. irreducible G b" by (fast elim: wfactorsE) - - have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> - fmset G cs = fmset G as #\<inter> fmset G bs" + then obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a" + by auto + from afs have airr: "\<forall>a \<in> set as. irreducible G a" + by (fast elim: wfactorsE) + + from bcarr have "\<exists>bs. set bs \<subseteq> carrier G \<and> wfactors G bs b" + by (rule wfactors_exist) + then obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfs: "wfactors G bs b" + by auto + from bfs have birr: "\<forall>b \<in> set bs. irreducible G b" + by (fast elim: wfactorsE) + + have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> + fmset G cs = fmset G as #\<inter> fmset G bs" proof (intro mset_wfactorsEx) fix X assume "X \<in># fmset G as #\<inter> fmset G bs" - hence "X \<in># fmset G as" by simp - hence "X \<in> set (map (assocs G) as)" by (simp add: fmset_def) - hence "\<exists>x. X = assocs G x \<and> x \<in> set as" by (induct as) auto - from this obtain x - where X: "X = assocs G x" - and xas: "x \<in> set as" - by auto - with ascarr have xcarr: "x \<in> carrier G" by fast - from xas airr have xirr: "irreducible G x" by simp - - from xcarr and xirr and X - show "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x" by fast + then have "X \<in># fmset G as" by simp + then have "X \<in> set (map (assocs G) as)" + by (simp add: fmset_def) + then have "\<exists>x. X = assocs G x \<and> x \<in> set as" + by (induct as) auto + then obtain x where X: "X = assocs G x" and xas: "x \<in> set as" + by auto + with ascarr have xcarr: "x \<in> carrier G" + by fast + from xas airr have xirr: "irreducible G x" + by simp + from xcarr and xirr and X show "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x" + by fast qed - - from this obtain c cs - where ccarr: "c \<in> carrier G" - and cscarr: "set cs \<subseteq> carrier G" + then obtain c cs + where ccarr: "c \<in> carrier G" + and cscarr: "set cs \<subseteq> carrier G" and csirr: "wfactors G cs c" - and csmset: "fmset G cs = fmset G as #\<inter> fmset G bs" by auto + and csmset: "fmset G cs = fmset G as #\<inter> fmset G bs" + by auto have "c gcdof a b" proof (simp add: isgcd_def, safe) from csmset - have "fmset G cs \<le># fmset G as" - by (simp add: multiset_inter_def subset_mset_def) - thus "c divides a" by (rule fmsubset_divides) fact+ + have "fmset G cs \<le># fmset G as" + by (simp add: multiset_inter_def subset_mset_def) + then show "c divides a" by (rule fmsubset_divides) fact+ next - from csmset - have "fmset G cs \<le># fmset G bs" - by (simp add: multiset_inter_def subseteq_mset_def, force) - thus "c divides b" by (rule fmsubset_divides) fact+ + from csmset have "fmset G cs \<le># fmset G bs" + by (simp add: multiset_inter_def subseteq_mset_def, force) + then show "c divides b" + by (rule fmsubset_divides) fact+ next fix y assume ycarr: "y \<in> carrier G" - hence "\<exists>ys. set ys \<subseteq> carrier G \<and> wfactors G ys y" by (rule wfactors_exist) - from this obtain ys - where yscarr: "set ys \<subseteq> carrier G" - and yfs: "wfactors G ys y" - by auto + then have "\<exists>ys. set ys \<subseteq> carrier G \<and> wfactors G ys y" + by (rule wfactors_exist) + then obtain ys where yscarr: "set ys \<subseteq> carrier G" and yfs: "wfactors G ys y" + by auto assume "y divides a" - hence ya: "fmset G ys \<le># fmset G as" by (rule divides_fmsubset) fact+ + then have ya: "fmset G ys \<le># fmset G as" + by (rule divides_fmsubset) fact+ assume "y divides b" - hence yb: "fmset G ys \<le># fmset G bs" by (rule divides_fmsubset) fact+ - - from ya yb csmset - have "fmset G ys \<le># fmset G cs" by (simp add: subset_mset_def) - thus "y divides c" by (rule fmsubset_divides) fact+ + then have yb: "fmset G ys \<le># fmset G bs" + by (rule divides_fmsubset) fact+ + + from ya yb csmset have "fmset G ys \<le># fmset G cs" + by (simp add: subset_mset_def) + then show "y divides c" + by (rule fmsubset_divides) fact+ qed - - with ccarr - show "\<exists>c. c \<in> carrier G \<and> c gcdof a b" by fast + with ccarr show "\<exists>c. c \<in> carrier G \<and> c gcdof a b" + by fast qed lemma (in factorial_monoid) lcmof_exists: - assumes acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" + assumes acarr: "a \<in> carrier G" + and bcarr: "b \<in> carrier G" shows "\<exists>c. c \<in> carrier G \<and> c lcmof a b" proof - - from acarr have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" by (rule wfactors_exist) - from this obtain as - where ascarr: "set as \<subseteq> carrier G" - and afs: "wfactors G as a" - by auto - from afs have airr: "\<forall>a \<in> set as. irreducible G a" by (fast elim: wfactorsE) - - from bcarr have "\<exists>bs. set bs \<subseteq> carrier G \<and> wfactors G bs b" by (rule wfactors_exist) - from this obtain bs - where bscarr: "set bs \<subseteq> carrier G" - and bfs: "wfactors G bs b" - by auto - from bfs have birr: "\<forall>b \<in> set bs. irreducible G b" by (fast elim: wfactorsE) - - have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> - fmset G cs = (fmset G as - fmset G bs) + fmset G bs" + from acarr have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" + by (rule wfactors_exist) + then obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a" + by auto + from afs have airr: "\<forall>a \<in> set as. irreducible G a" + by (fast elim: wfactorsE) + + from bcarr have "\<exists>bs. set bs \<subseteq> carrier G \<and> wfactors G bs b" + by (rule wfactors_exist) + then obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfs: "wfactors G bs b" + by auto + from bfs have birr: "\<forall>b \<in> set bs. irreducible G b" + by (fast elim: wfactorsE) + + have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> + fmset G cs = (fmset G as - fmset G bs) + fmset G bs" proof (intro mset_wfactorsEx) fix X assume "X \<in># (fmset G as - fmset G bs) + fmset G bs" - hence "X \<in># fmset G as \<or> X \<in># fmset G bs" + then have "X \<in># fmset G as \<or> X \<in># fmset G bs" by (auto dest: in_diffD) - moreover - { - assume "X \<in> set_mset (fmset G as)" - hence "X \<in> set (map (assocs G) as)" by (simp add: fmset_def) - hence "\<exists>x. x \<in> set as \<and> X = assocs G x" by (induct as) auto - from this obtain x - where xas: "x \<in> set as" - and X: "X = assocs G x" by auto - + then consider "X \<in> set_mset (fmset G as)" | "X \<in> set_mset (fmset G bs)" + by fast + then show "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x" + proof cases + case 1 + then have "X \<in> set (map (assocs G) as)" by (simp add: fmset_def) + then have "\<exists>x. x \<in> set as \<and> X = assocs G x" by (induct as) auto + then obtain x where xas: "x \<in> set as" and X: "X = assocs G x" by auto with ascarr have xcarr: "x \<in> carrier G" by fast from xas airr have xirr: "irreducible G x" by simp - - from xcarr and xirr and X - have "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x" by fast - } - moreover - { - assume "X \<in> set_mset (fmset G bs)" - hence "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def) - hence "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct as) auto - from this obtain x - where xbs: "x \<in> set bs" - and X: "X = assocs G x" by auto - + from xcarr and xirr and X show ?thesis by fast + next + case 2 + then have "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def) + then have "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct as) auto + then obtain x where xbs: "x \<in> set bs" and X: "X = assocs G x" by auto with bscarr have xcarr: "x \<in> carrier G" by fast from xbs birr have xirr: "irreducible G x" by simp - - from xcarr and xirr and X - have "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x" by fast - } - ultimately - show "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x" by fast + from xcarr and xirr and X show ?thesis by fast + qed qed - - from this obtain c cs - where ccarr: "c \<in> carrier G" - and cscarr: "set cs \<subseteq> carrier G" + then obtain c cs + where ccarr: "c \<in> carrier G" + and cscarr: "set cs \<subseteq> carrier G" and csirr: "wfactors G cs c" - and csmset: "fmset G cs = fmset G as - fmset G bs + fmset G bs" by auto + and csmset: "fmset G cs = fmset G as - fmset G bs + fmset G bs" + by auto have "c lcmof a b" proof (simp add: islcm_def, safe) - from csmset have "fmset G as \<le># fmset G cs" by (simp add: subseteq_mset_def, force) - thus "a divides c" by (rule fmsubset_divides) fact+ + from csmset have "fmset G as \<le># fmset G cs" + by (simp add: subseteq_mset_def, force) + then show "a divides c" + by (rule fmsubset_divides) fact+ next - from csmset have "fmset G bs \<le># fmset G cs" by (simp add: subset_mset_def) - thus "b divides c" by (rule fmsubset_divides) fact+ + from csmset have "fmset G bs \<le># fmset G cs" + by (simp add: subset_mset_def) + then show "b divides c" + by (rule fmsubset_divides) fact+ next fix y assume ycarr: "y \<in> carrier G" - hence "\<exists>ys. set ys \<subseteq> carrier G \<and> wfactors G ys y" by (rule wfactors_exist) - from this obtain ys - where yscarr: "set ys \<subseteq> carrier G" - and yfs: "wfactors G ys y" - by auto + then have "\<exists>ys. set ys \<subseteq> carrier G \<and> wfactors G ys y" + by (rule wfactors_exist) + then obtain ys where yscarr: "set ys \<subseteq> carrier G" and yfs: "wfactors G ys y" + by auto assume "a divides y" - hence ya: "fmset G as \<le># fmset G ys" by (rule divides_fmsubset) fact+ + then have ya: "fmset G as \<le># fmset G ys" + by (rule divides_fmsubset) fact+ assume "b divides y" - hence yb: "fmset G bs \<le># fmset G ys" by (rule divides_fmsubset) fact+ - - from ya yb csmset - have "fmset G cs \<le># fmset G ys" + then have yb: "fmset G bs \<le># fmset G ys" + by (rule divides_fmsubset) fact+ + + from ya yb csmset have "fmset G cs \<le># fmset G ys" apply (simp add: subseteq_mset_def, clarify) apply (case_tac "count (fmset G as) a < count (fmset G bs) a") apply simp apply simp - done - thus "c divides y" by (rule fmsubset_divides) fact+ + done + then show "c divides y" + by (rule fmsubset_divides) fact+ qed - - with ccarr - show "\<exists>c. c \<in> carrier G \<and> c lcmof a b" by fast + with ccarr show "\<exists>c. c \<in> carrier G \<and> c lcmof a b" + by fast qed @@ -2756,23 +2508,21 @@ subsubsection \<open>Gcd condition\<close> lemma (in gcd_condition_monoid) division_weak_lower_semilattice [simp]: - shows "weak_lower_semilattice (division_rel G)" + "weak_lower_semilattice (division_rel G)" proof - interpret weak_partial_order "division_rel G" .. show ?thesis - apply (unfold_locales, simp_all) + apply (unfold_locales, simp_all) proof - fix x y assume carr: "x \<in> carrier G" "y \<in> carrier G" - hence "\<exists>z. z \<in> carrier G \<and> z gcdof x y" by (rule gcdof_exists) - from this obtain z - where zcarr: "z \<in> carrier G" - and isgcd: "z gcdof x y" - by auto - with carr - have "greatest (division_rel G) z (Lower (division_rel G) {x, y})" - by (subst gcdof_greatestLower[symmetric], simp+) - thus "\<exists>z. greatest (division_rel G) z (Lower (division_rel G) {x, y})" by fast + then have "\<exists>z. z \<in> carrier G \<and> z gcdof x y" by (rule gcdof_exists) + then obtain z where zcarr: "z \<in> carrier G" and isgcd: "z gcdof x y" + by auto + with carr have "greatest (division_rel G) z (Lower (division_rel G) {x, y})" + by (subst gcdof_greatestLower[symmetric], simp+) + then show "\<exists>z. greatest (division_rel G) z (Lower (division_rel G) {x, y})" + by fast qed qed @@ -2787,13 +2537,13 @@ have "a' \<in> carrier G \<and> a' gcdof b c" apply (simp add: gcdof_greatestLower carr') apply (subst greatest_Lower_cong_l[of _ a]) - apply (simp add: a'a) + apply (simp add: a'a) + apply (simp add: carr) apply (simp add: carr) apply (simp add: carr) - apply (simp add: carr) apply (simp add: gcdof_greatestLower[symmetric] agcd carr) - done - thus ?thesis .. + done + then show ?thesis .. qed lemma (in gcd_condition_monoid) gcd_closed [simp]: @@ -2804,28 +2554,30 @@ show ?thesis apply (simp add: somegcd_meet[OF carr]) apply (rule meet_closed[simplified], fact+) - done + done qed lemma (in gcd_condition_monoid) gcd_isgcd: assumes carr: "a \<in> carrier G" "b \<in> carrier G" shows "(somegcd G a b) gcdof a b" proof - - interpret weak_lower_semilattice "division_rel G" by simp - from carr - have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b" + interpret weak_lower_semilattice "division_rel G" + by simp + from carr have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b" apply (subst gcdof_greatestLower, simp, simp) apply (simp add: somegcd_meet[OF carr] meet_def) apply (rule inf_of_two_greatest[simplified], assumption+) - done - thus "(somegcd G a b) gcdof a b" by simp + done + then show "(somegcd G a b) gcdof a b" + by simp qed lemma (in gcd_condition_monoid) gcd_exists: assumes carr: "a \<in> carrier G" "b \<in> carrier G" shows "\<exists>x\<in>carrier G. x = somegcd G a b" proof - - interpret weak_lower_semilattice "division_rel G" by simp + interpret weak_lower_semilattice "division_rel G" + by simp show ?thesis by (metis carr(1) carr(2) gcd_closed) qed @@ -2834,7 +2586,8 @@ assumes carr: "a \<in> carrier G" "b \<in> carrier G" shows "(somegcd G a b) divides a" proof - - interpret weak_lower_semilattice "division_rel G" by simp + interpret weak_lower_semilattice "division_rel G" + by simp show ?thesis by (metis carr(1) carr(2) gcd_isgcd isgcd_def) qed @@ -2843,7 +2596,8 @@ assumes carr: "a \<in> carrier G" "b \<in> carrier G" shows "(somegcd G a b) divides b" proof - - interpret weak_lower_semilattice "division_rel G" by simp + interpret weak_lower_semilattice "division_rel G" + by simp show ?thesis by (metis carr gcd_isgcd isgcd_def) qed @@ -2853,7 +2607,8 @@ and L: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" shows "z divides (somegcd G x y)" proof - - interpret weak_lower_semilattice "division_rel G" by simp + interpret weak_lower_semilattice "division_rel G" + by simp show ?thesis by (metis gcd_isgcd isgcd_def assms) qed @@ -2863,11 +2618,12 @@ and carr: "x \<in> carrier G" "x' \<in> carrier G" "y \<in> carrier G" shows "somegcd G x y \<sim> somegcd G x' y" proof - - interpret weak_lower_semilattice "division_rel G" by simp + interpret weak_lower_semilattice "division_rel G" + by simp show ?thesis apply (simp add: somegcd_meet carr) apply (rule meet_cong_l[simplified], fact+) - done + done qed lemma (in gcd_condition_monoid) gcd_cong_r: @@ -2879,7 +2635,7 @@ show ?thesis apply (simp add: somegcd_meet carr) apply (rule meet_cong_r[simplified], fact+) - done + done qed (* @@ -2897,7 +2653,7 @@ unfolding CONG_def by clarsimp (blast intro: gcd_cong_r) -lemmas (in gcd_condition_monoid) asc_cong_gcd_split [simp] = +lemmas (in gcd_condition_monoid) asc_cong_gcd_split [simp] = assoc_split[OF _ asc_cong_gcd_l] assoc_split[OF _ asc_cong_gcd_r] *) @@ -2906,43 +2662,42 @@ and others: "\<forall>y\<in>carrier G. y divides b \<and> y divides c \<longrightarrow> y divides a" and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ccarr: "c \<in> carrier G" shows "a \<sim> somegcd G b c" -apply (simp add: somegcd_def) -apply (rule someI2_ex) - apply (rule exI[of _ a], simp add: isgcd_def) - apply (simp add: assms) -apply (simp add: isgcd_def assms, clarify) -apply (insert assms, blast intro: associatedI) -done + apply (simp add: somegcd_def) + apply (rule someI2_ex) + apply (rule exI[of _ a], simp add: isgcd_def) + apply (simp add: assms) + apply (simp add: isgcd_def assms, clarify) + apply (insert assms, blast intro: associatedI) + done lemma (in gcd_condition_monoid) gcdI2: - assumes "a gcdof b c" - and "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ccarr: "c \<in> carrier G" + assumes "a gcdof b c" and "a \<in> carrier G" and "b \<in> carrier G" and "c \<in> carrier G" shows "a \<sim> somegcd G b c" -using assms -unfolding isgcd_def -by (blast intro: gcdI) + using assms unfolding isgcd_def by (blast intro: gcdI) lemma (in gcd_condition_monoid) SomeGcd_ex: assumes "finite A" "A \<subseteq> carrier G" "A \<noteq> {}" shows "\<exists>x\<in> carrier G. x = SomeGcd G A" proof - - interpret weak_lower_semilattice "division_rel G" by simp + interpret weak_lower_semilattice "division_rel G" + by simp show ?thesis apply (simp add: SomeGcd_def) apply (rule finite_inf_closed[simplified], fact+) - done + done qed lemma (in gcd_condition_monoid) gcd_assoc: assumes carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" shows "somegcd G (somegcd G a b) c \<sim> somegcd G a (somegcd G b c)" proof - - interpret weak_lower_semilattice "division_rel G" by simp + interpret weak_lower_semilattice "division_rel G" + by simp show ?thesis apply (subst (2 3) somegcd_meet, (simp add: carr)+) apply (simp add: somegcd_meet carr) apply (rule weak_meet_assoc[simplified], fact+) - done + done qed lemma (in gcd_condition_monoid) gcd_mult: @@ -2957,59 +2712,53 @@ note carr = carr dcarr ecarr have "?d divides a" by (simp add: gcd_divides_l) - hence cd'ca: "c \<otimes> ?d divides (c \<otimes> a)" by (simp add: divides_mult_lI) + then have cd'ca: "c \<otimes> ?d divides (c \<otimes> a)" by (simp add: divides_mult_lI) have "?d divides b" by (simp add: gcd_divides_r) - hence cd'cb: "c \<otimes> ?d divides (c \<otimes> b)" by (simp add: divides_mult_lI) - - from cd'ca cd'cb - have cd'e: "c \<otimes> ?d divides ?e" - by (rule gcd_divides) simp+ - - hence "\<exists>u. u \<in> carrier G \<and> ?e = c \<otimes> ?d \<otimes> u" - by (elim dividesE, fast) - from this obtain u - where ucarr[simp]: "u \<in> carrier G" - and e_cdu: "?e = c \<otimes> ?d \<otimes> u" - by auto + then have cd'cb: "c \<otimes> ?d divides (c \<otimes> b)" by (simp add: divides_mult_lI) + + from cd'ca cd'cb have cd'e: "c \<otimes> ?d divides ?e" + by (rule gcd_divides) simp_all + then have "\<exists>u. u \<in> carrier G \<and> ?e = c \<otimes> ?d \<otimes> u" + by (elim dividesE) fast + then obtain u where ucarr[simp]: "u \<in> carrier G" and e_cdu: "?e = c \<otimes> ?d \<otimes> u" + by auto note carr = carr ucarr - have "?e divides c \<otimes> a" by (rule gcd_divides_l) simp+ - hence "\<exists>x. x \<in> carrier G \<and> c \<otimes> a = ?e \<otimes> x" - by (elim dividesE, fast) - from this obtain x - where xcarr: "x \<in> carrier G" - and ca_ex: "c \<otimes> a = ?e \<otimes> x" - by auto - with e_cdu - have ca_cdux: "c \<otimes> a = c \<otimes> ?d \<otimes> u \<otimes> x" by simp - - from ca_cdux xcarr - have "c \<otimes> a = c \<otimes> (?d \<otimes> u \<otimes> x)" by (simp add: m_assoc) - then have "a = ?d \<otimes> u \<otimes> x" by (rule l_cancel[of c a]) (simp add: xcarr)+ - hence du'a: "?d \<otimes> u divides a" by (rule dividesI[OF xcarr]) - - have "?e divides c \<otimes> b" by (intro gcd_divides_r, simp+) - hence "\<exists>x. x \<in> carrier G \<and> c \<otimes> b = ?e \<otimes> x" - by (elim dividesE, fast) - from this obtain x - where xcarr: "x \<in> carrier G" - and cb_ex: "c \<otimes> b = ?e \<otimes> x" - by auto - with e_cdu - have cb_cdux: "c \<otimes> b = c \<otimes> ?d \<otimes> u \<otimes> x" by simp - - from cb_cdux xcarr - have "c \<otimes> b = c \<otimes> (?d \<otimes> u \<otimes> x)" by (simp add: m_assoc) - with xcarr - have "b = ?d \<otimes> u \<otimes> x" by (intro l_cancel[of c b], simp+) - hence du'b: "?d \<otimes> u divides b" by (intro dividesI[OF xcarr]) - - from du'a du'b carr - have du'd: "?d \<otimes> u divides ?d" - by (intro gcd_divides, simp+) - hence uunit: "u \<in> Units G" + have "?e divides c \<otimes> a" by (rule gcd_divides_l) simp_all + then have "\<exists>x. x \<in> carrier G \<and> c \<otimes> a = ?e \<otimes> x" + by (elim dividesE) fast + then obtain x where xcarr: "x \<in> carrier G" and ca_ex: "c \<otimes> a = ?e \<otimes> x" + by auto + with e_cdu have ca_cdux: "c \<otimes> a = c \<otimes> ?d \<otimes> u \<otimes> x" + by simp + + from ca_cdux xcarr have "c \<otimes> a = c \<otimes> (?d \<otimes> u \<otimes> x)" + by (simp add: m_assoc) + then have "a = ?d \<otimes> u \<otimes> x" + by (rule l_cancel[of c a]) (simp add: xcarr)+ + then have du'a: "?d \<otimes> u divides a" + by (rule dividesI[OF xcarr]) + + have "?e divides c \<otimes> b" by (intro gcd_divides_r) simp_all + then have "\<exists>x. x \<in> carrier G \<and> c \<otimes> b = ?e \<otimes> x" + by (elim dividesE) fast + then obtain x where xcarr: "x \<in> carrier G" and cb_ex: "c \<otimes> b = ?e \<otimes> x" + by auto + with e_cdu have cb_cdux: "c \<otimes> b = c \<otimes> ?d \<otimes> u \<otimes> x" + by simp + + from cb_cdux xcarr have "c \<otimes> b = c \<otimes> (?d \<otimes> u \<otimes> x)" + by (simp add: m_assoc) + with xcarr have "b = ?d \<otimes> u \<otimes> x" + by (intro l_cancel[of c b]) simp_all + then have du'b: "?d \<otimes> u divides b" + by (intro dividesI[OF xcarr]) + + from du'a du'b carr have du'd: "?d \<otimes> u divides ?d" + by (intro gcd_divides) simp_all + then have uunit: "u \<in> Units G" proof (elim dividesE) fix v assume vcarr[simp]: "v \<in> carrier G" @@ -3017,108 +2766,100 @@ have "?d \<otimes> \<one> = ?d \<otimes> u \<otimes> v" by simp fact also have "?d \<otimes> u \<otimes> v = ?d \<otimes> (u \<otimes> v)" by (simp add: m_assoc) finally have "?d \<otimes> \<one> = ?d \<otimes> (u \<otimes> v)" . - hence i2: "\<one> = u \<otimes> v" by (rule l_cancel) simp+ - hence i1: "\<one> = v \<otimes> u" by (simp add: m_comm) - from vcarr i1[symmetric] i2[symmetric] - show "u \<in> Units G" - by (unfold Units_def, simp, fast) + then have i2: "\<one> = u \<otimes> v" by (rule l_cancel) simp_all + then have i1: "\<one> = v \<otimes> u" by (simp add: m_comm) + from vcarr i1[symmetric] i2[symmetric] show "u \<in> Units G" + by (auto simp: Units_def) qed - from e_cdu uunit - have "somegcd G (c \<otimes> a) (c \<otimes> b) \<sim> c \<otimes> somegcd G a b" - by (intro associatedI2[of u], simp+) - from this[symmetric] - show "c \<otimes> somegcd G a b \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)" by simp + from e_cdu uunit have "somegcd G (c \<otimes> a) (c \<otimes> b) \<sim> c \<otimes> somegcd G a b" + by (intro associatedI2[of u]) simp_all + from this[symmetric] show "c \<otimes> somegcd G a b \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)" + by simp qed lemma (in monoid) assoc_subst: assumes ab: "a \<sim> b" - and cP: "ALL a b. a : carrier G & b : carrier G & a \<sim> b - --> f a : carrier G & f b : carrier G & f a \<sim> f b" + and cP: "\<forall>a b. a \<in> carrier G \<and> b \<in> carrier G \<and> a \<sim> b + \<longrightarrow> f a \<in> carrier G \<and> f b \<in> carrier G \<and> f a \<sim> f b" and carr: "a \<in> carrier G" "b \<in> carrier G" shows "f a \<sim> f b" using assms by auto lemma (in gcd_condition_monoid) relprime_mult: - assumes abrelprime: "somegcd G a b \<sim> \<one>" and acrelprime: "somegcd G a c \<sim> \<one>" + assumes abrelprime: "somegcd G a b \<sim> \<one>" + and acrelprime: "somegcd G a c \<sim> \<one>" and carr[simp]: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" shows "somegcd G a (b \<otimes> c) \<sim> \<one>" proof - have "c = c \<otimes> \<one>" by simp also from abrelprime[symmetric] - have "\<dots> \<sim> c \<otimes> somegcd G a b" - by (rule assoc_subst) (simp add: mult_cong_r)+ - also have "\<dots> \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)" by (rule gcd_mult) fact+ - finally - have c: "c \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)" by simp - - from carr - have a: "a \<sim> somegcd G a (c \<otimes> a)" - by (fast intro: gcdI divides_prod_l) - - have "somegcd G a (b \<otimes> c) \<sim> somegcd G a (c \<otimes> b)" by (simp add: m_comm) - also from a - have "\<dots> \<sim> somegcd G (somegcd G a (c \<otimes> a)) (c \<otimes> b)" - by (rule assoc_subst) (simp add: gcd_cong_l)+ - also from gcd_assoc - have "\<dots> \<sim> somegcd G a (somegcd G (c \<otimes> a) (c \<otimes> b))" - by (rule assoc_subst) simp+ - also from c[symmetric] - have "\<dots> \<sim> somegcd G a c" - by (rule assoc_subst) (simp add: gcd_cong_r)+ + have "\<dots> \<sim> c \<otimes> somegcd G a b" + by (rule assoc_subst) (simp add: mult_cong_r)+ + also have "\<dots> \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)" + by (rule gcd_mult) fact+ + finally have c: "c \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)" + by simp + + from carr have a: "a \<sim> somegcd G a (c \<otimes> a)" + by (fast intro: gcdI divides_prod_l) + + have "somegcd G a (b \<otimes> c) \<sim> somegcd G a (c \<otimes> b)" + by (simp add: m_comm) + also from a have "\<dots> \<sim> somegcd G (somegcd G a (c \<otimes> a)) (c \<otimes> b)" + by (rule assoc_subst) (simp add: gcd_cong_l)+ + also from gcd_assoc have "\<dots> \<sim> somegcd G a (somegcd G (c \<otimes> a) (c \<otimes> b))" + by (rule assoc_subst) simp+ + also from c[symmetric] have "\<dots> \<sim> somegcd G a c" + by (rule assoc_subst) (simp add: gcd_cong_r)+ also note acrelprime - finally - show "somegcd G a (b \<otimes> c) \<sim> \<one>" by simp + finally show "somegcd G a (b \<otimes> c) \<sim> \<one>" + by simp qed -lemma (in gcd_condition_monoid) primeness_condition: - "primeness_condition_monoid G" -apply unfold_locales -apply (rule primeI) - apply (elim irreducibleE, assumption) +lemma (in gcd_condition_monoid) primeness_condition: "primeness_condition_monoid G" + apply unfold_locales + apply (rule primeI) + apply (elim irreducibleE, assumption) proof - fix p a b assume pcarr: "p \<in> carrier G" and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and pirr: "irreducible G p" and pdvdab: "p divides a \<otimes> b" - from pirr - have pnunit: "p \<notin> Units G" - and r[rule_format]: "\<forall>b. b \<in> carrier G \<and> properfactor G b p \<longrightarrow> b \<in> Units G" - by - (fast elim: irreducibleE)+ + from pirr have pnunit: "p \<notin> Units G" + and r[rule_format]: "\<forall>b. b \<in> carrier G \<and> properfactor G b p \<longrightarrow> b \<in> Units G" + by (fast elim: irreducibleE)+ show "p divides a \<or> p divides b" proof (rule ccontr, clarsimp) assume npdvda: "\<not> p divides a" - with pcarr acarr - have "\<one> \<sim> somegcd G p a" - apply (intro gcdI, simp, simp, simp) - apply (fast intro: unit_divides) - apply (fast intro: unit_divides) - apply (clarsimp simp add: Unit_eq_dividesone[symmetric]) - apply (rule r, rule, assumption) - apply (rule properfactorI, assumption) + with pcarr acarr have "\<one> \<sim> somegcd G p a" + apply (intro gcdI, simp, simp, simp) + apply (fast intro: unit_divides) + apply (fast intro: unit_divides) + apply (clarsimp simp add: Unit_eq_dividesone[symmetric]) + apply (rule r, rule, assumption) + apply (rule properfactorI, assumption) proof (rule ccontr, simp) fix y assume ycarr: "y \<in> carrier G" assume "p divides y" also assume "y divides a" - finally - have "p divides a" by (simp add: pcarr ycarr acarr) - with npdvda - show "False" .. - qed simp+ - with pcarr acarr - have pa: "somegcd G p a \<sim> \<one>" by (fast intro: associated_sym[of "\<one>"] gcd_closed) + finally have "p divides a" + by (simp add: pcarr ycarr acarr) + with npdvda show False .. + qed simp_all + with pcarr acarr have pa: "somegcd G p a \<sim> \<one>" + by (fast intro: associated_sym[of "\<one>"] gcd_closed) assume npdvdb: "\<not> p divides b" - with pcarr bcarr - have "\<one> \<sim> somegcd G p b" - apply (intro gcdI, simp, simp, simp) - apply (fast intro: unit_divides) - apply (fast intro: unit_divides) - apply (clarsimp simp add: Unit_eq_dividesone[symmetric]) - apply (rule r, rule, assumption) - apply (rule properfactorI, assumption) + with pcarr bcarr have "\<one> \<sim> somegcd G p b" + apply (intro gcdI, simp, simp, simp) + apply (fast intro: unit_divides) + apply (fast intro: unit_divides) + apply (clarsimp simp add: Unit_eq_dividesone[symmetric]) + apply (rule r, rule, assumption) + apply (rule properfactorI, assumption) proof (rule ccontr, simp) fix y assume ycarr: "y \<in> carrier G" @@ -3126,24 +2867,22 @@ also assume "y divides b" finally have "p divides b" by (simp add: pcarr ycarr bcarr) with npdvdb - show "False" .. - qed simp+ - with pcarr bcarr - have pb: "somegcd G p b \<sim> \<one>" by (fast intro: associated_sym[of "\<one>"] gcd_closed) - - from pcarr acarr bcarr pdvdab - have "p gcdof p (a \<otimes> b)" by (fast intro: isgcd_divides_l) - - with pcarr acarr bcarr - have "p \<sim> somegcd G p (a \<otimes> b)" by (fast intro: gcdI2) - also from pa pb pcarr acarr bcarr - have "somegcd G p (a \<otimes> b) \<sim> \<one>" by (rule relprime_mult) - finally have "p \<sim> \<one>" by (simp add: pcarr acarr bcarr) - - with pcarr - have "p \<in> Units G" by (fast intro: assoc_unit_l) - with pnunit - show "False" .. + show "False" .. + qed simp_all + with pcarr bcarr have pb: "somegcd G p b \<sim> \<one>" + by (fast intro: associated_sym[of "\<one>"] gcd_closed) + + from pcarr acarr bcarr pdvdab have "p gcdof p (a \<otimes> b)" + by (fast intro: isgcd_divides_l) + with pcarr acarr bcarr have "p \<sim> somegcd G p (a \<otimes> b)" + by (fast intro: gcdI2) + also from pa pb pcarr acarr bcarr have "somegcd G p (a \<otimes> b) \<sim> \<one>" + by (rule relprime_mult) + finally have "p \<sim> \<one>" + by (simp add: pcarr acarr bcarr) + with pcarr have "p \<in> Units G" + by (fast intro: assoc_unit_l) + with pnunit show False .. qed qed @@ -3158,86 +2897,70 @@ shows "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" proof - have r[rule_format]: "a \<in> carrier G \<longrightarrow> (\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a)" - apply (rule wf_induct[OF division_wellfounded]) - proof - + proof (rule wf_induct[OF division_wellfounded]) fix x assume ih: "\<forall>y. (y, x) \<in> {(x, y). x \<in> carrier G \<and> y \<in> carrier G \<and> properfactor G x y} \<longrightarrow> y \<in> carrier G \<longrightarrow> (\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as y)" show "x \<in> carrier G \<longrightarrow> (\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as x)" - apply clarify - apply (cases "x \<in> Units G") - apply (rule exI[of _ "[]"], simp) - apply (cases "irreducible G x") - apply (rule exI[of _ "[x]"], simp add: wfactors_def) + apply clarify + apply (cases "x \<in> Units G") + apply (rule exI[of _ "[]"], simp) + apply (cases "irreducible G x") + apply (rule exI[of _ "[x]"], simp add: wfactors_def) proof - assume xcarr: "x \<in> carrier G" and xnunit: "x \<notin> Units G" and xnirr: "\<not> irreducible G x" - hence "\<exists>y. y \<in> carrier G \<and> properfactor G y x \<and> y \<notin> Units G" - apply - apply (rule ccontr, simp) + then have "\<exists>y. y \<in> carrier G \<and> properfactor G y x \<and> y \<notin> Units G" + apply - + apply (rule ccontr) + apply simp apply (subgoal_tac "irreducible G x", simp) apply (rule irreducibleI, simp, simp) - done - from this obtain y - where ycarr: "y \<in> carrier G" - and ynunit: "y \<notin> Units G" - and pfyx: "properfactor G y x" - by auto - - have ih': - "\<And>y. \<lbrakk>y \<in> carrier G; properfactor G y x\<rbrakk> - \<Longrightarrow> \<exists>as. set as \<subseteq> carrier G \<and> wfactors G as y" - by (rule ih[rule_format, simplified]) (simp add: xcarr)+ - - from ycarr pfyx - have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as y" - by (rule ih') - from this obtain ys - where yscarr: "set ys \<subseteq> carrier G" - and yfs: "wfactors G ys y" - by auto - - from pfyx - have "y divides x" - and nyx: "\<not> y \<sim> x" - by - (fast elim: properfactorE2)+ - hence "\<exists>z. z \<in> carrier G \<and> x = y \<otimes> z" - by fast - - from this obtain z - where zcarr: "z \<in> carrier G" - and x: "x = y \<otimes> z" - by auto - - from zcarr ycarr - have "properfactor G z x" + done + then obtain y where ycarr: "y \<in> carrier G" and ynunit: "y \<notin> Units G" + and pfyx: "properfactor G y x" + by auto + + have ih': "\<And>y. \<lbrakk>y \<in> carrier G; properfactor G y x\<rbrakk> + \<Longrightarrow> \<exists>as. set as \<subseteq> carrier G \<and> wfactors G as y" + by (rule ih[rule_format, simplified]) (simp add: xcarr)+ + + from ycarr pfyx have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as y" + by (rule ih') + then obtain ys where yscarr: "set ys \<subseteq> carrier G" and yfs: "wfactors G ys y" + by auto + + from pfyx have "y divides x" and nyx: "\<not> y \<sim> x" + by (fast elim: properfactorE2)+ + then have "\<exists>z. z \<in> carrier G \<and> x = y \<otimes> z" + by fast + then obtain z where zcarr: "z \<in> carrier G" and x: "x = y \<otimes> z" + by auto + + from zcarr ycarr have "properfactor G z x" apply (subst x) apply (intro properfactorI3[of _ _ y]) - apply (simp add: m_comm) - apply (simp add: ynunit)+ - done - with zcarr - have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as z" - by (rule ih') - from this obtain zs - where zscarr: "set zs \<subseteq> carrier G" - and zfs: "wfactors G zs z" - by auto - - from yscarr zscarr - have xscarr: "set (ys@zs) \<subseteq> carrier G" by simp - from yfs zfs ycarr zcarr yscarr zscarr - have "wfactors G (ys@zs) (y\<otimes>z)" by (rule wfactors_mult) - hence "wfactors G (ys@zs) x" by (simp add: x) - - from xscarr this - show "\<exists>xs. set xs \<subseteq> carrier G \<and> wfactors G xs x" by fast + apply (simp add: m_comm) + apply (simp add: ynunit)+ + done + with zcarr have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as z" + by (rule ih') + then obtain zs where zscarr: "set zs \<subseteq> carrier G" and zfs: "wfactors G zs z" + by auto + + from yscarr zscarr have xscarr: "set (ys@zs) \<subseteq> carrier G" + by simp + from yfs zfs ycarr zcarr yscarr zscarr have "wfactors G (ys@zs) (y\<otimes>z)" + by (rule wfactors_mult) + then have "wfactors G (ys@zs) x" + by (simp add: x) + with xscarr show "\<exists>xs. set xs \<subseteq> carrier G \<and> wfactors G xs x" + by fast qed qed - - from acarr - show ?thesis by (rule r) + from acarr show ?thesis by (rule r) qed @@ -3249,56 +2972,50 @@ and "a divides (foldr (op \<otimes>) as \<one>)" shows "\<exists>i<length as. a divides (as!i)" proof - - have r[rule_format]: - "set as \<subseteq> carrier G \<and> a divides (foldr (op \<otimes>) as \<one>) - \<longrightarrow> (\<exists>i. i < length as \<and> a divides (as!i))" + have r[rule_format]: "set as \<subseteq> carrier G \<and> a divides (foldr (op \<otimes>) as \<one>) + \<longrightarrow> (\<exists>i. i < length as \<and> a divides (as!i))" apply (induct as) apply clarsimp defer 1 apply clarsimp defer 1 proof - assume "a divides \<one>" - with carr - have "a \<in> Units G" - by (fast intro: divides_unit[of a \<one>]) - with aprime - show "False" by (elim primeE, simp) + with carr have "a \<in> Units G" + by (fast intro: divides_unit[of a \<one>]) + with aprime show False + by (elim primeE, simp) next fix aa as assume ih[rule_format]: "a divides foldr op \<otimes> as \<one> \<longrightarrow> (\<exists>i<length as. a divides as ! i)" and carr': "aa \<in> carrier G" "set as \<subseteq> carrier G" and "a divides aa \<otimes> foldr op \<otimes> as \<one>" - with carr aprime - have "a divides aa \<or> a divides foldr op \<otimes> as \<one>" - by (intro prime_divides) simp+ - moreover { + with carr aprime have "a divides aa \<or> a divides foldr op \<otimes> as \<one>" + by (intro prime_divides) simp+ + then show "\<exists>i<Suc (length as). a divides (aa # as) ! i" + proof assume "a divides aa" - hence p1: "a divides (aa#as)!0" by simp + then have p1: "a divides (aa#as)!0" by simp have "0 < Suc (length as)" by simp - with p1 have "\<exists>i<Suc (length as). a divides (aa # as) ! i" by fast - } - moreover { + with p1 show ?thesis by fast + next assume "a divides foldr op \<otimes> as \<one>" - hence "\<exists>i. i < length as \<and> a divides as ! i" by (rule ih) - from this obtain i where "a divides as ! i" and len: "i < length as" by auto - hence p1: "a divides (aa#as) ! (Suc i)" by simp + then have "\<exists>i. i < length as \<and> a divides as ! i" by (rule ih) + then obtain i where "a divides as ! i" and len: "i < length as" by auto + then have p1: "a divides (aa#as) ! (Suc i)" by simp from len have "Suc i < Suc (length as)" by simp - with p1 have "\<exists>i<Suc (length as). a divides (aa # as) ! i" by force - } - ultimately - show "\<exists>i<Suc (length as). a divides (aa # as) ! i" by fast + with p1 show ?thesis by force + qed qed - - from assms - show ?thesis - by (intro r, safe) + from assms show ?thesis + by (intro r) auto qed lemma (in primeness_condition_monoid) wfactors_unique__hlp_induct: - "\<forall>a as'. a \<in> carrier G \<and> set as \<subseteq> carrier G \<and> set as' \<subseteq> carrier G \<and> + "\<forall>a as'. a \<in> carrier G \<and> set as \<subseteq> carrier G \<and> set as' \<subseteq> carrier G \<and> wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'" proof (induct as) - case Nil show ?case apply auto - proof - + case Nil + show ?case + proof auto fix a as' assume a: "a \<in> carrier G" assume "wfactors G [] a" @@ -3310,56 +3027,55 @@ then show "essentially_equal G [] as'" by simp qed next - case (Cons ah as) then show ?case apply clarsimp - proof - + case (Cons ah as) + then show ?case + proof clarsimp fix a as' - assume ih [rule_format]: + assume ih [rule_format]: "\<forall>a as'. a \<in> carrier G \<and> set as' \<subseteq> carrier G \<and> wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'" and acarr: "a \<in> carrier G" and ahcarr: "ah \<in> carrier G" and ascarr: "set as \<subseteq> carrier G" and as'carr: "set as' \<subseteq> carrier G" and afs: "wfactors G (ah # as) a" and afs': "wfactors G as' a" - hence ahdvda: "ah divides a" + then have ahdvda: "ah divides a" by (intro wfactors_dividesI[of "ah#as" "a"], simp+) - hence "\<exists>a'\<in> carrier G. a = ah \<otimes> a'" by fast - from this obtain a' - where a'carr: "a' \<in> carrier G" - and a: "a = ah \<otimes> a'" + then have "\<exists>a'\<in> carrier G. a = ah \<otimes> a'" by fast + then obtain a' where a'carr: "a' \<in> carrier G" and a: "a = ah \<otimes> a'" by auto have a'fs: "wfactors G as a'" apply (rule wfactorsE[OF afs], rule wfactorsI, simp) apply (simp add: a, insert ascarr a'carr) apply (intro assoc_l_cancel[of ah _ a'] multlist_closed ahcarr, assumption+) done - from afs have ahirr: "irreducible G ah" by (elim wfactorsE, simp) - with ascarr have ahprime: "prime G ah" by (intro irreducible_prime ahcarr) + from afs have ahirr: "irreducible G ah" + by (elim wfactorsE) simp + with ascarr have ahprime: "prime G ah" + by (intro irreducible_prime ahcarr) note carr [simp] = acarr ahcarr ascarr as'carr a'carr note ahdvda - also from afs' - have "a divides (foldr (op \<otimes>) as' \<one>)" + also from afs' have "a divides (foldr (op \<otimes>) as' \<one>)" by (elim wfactorsE associatedE, simp) - finally have "ah divides (foldr (op \<otimes>) as' \<one>)" by simp - - with ahprime - have "\<exists>i<length as'. ah divides as'!i" + finally have "ah divides (foldr (op \<otimes>) as' \<one>)" + by simp + with ahprime have "\<exists>i<length as'. ah divides as'!i" by (intro multlist_prime_pos, simp+) - from this obtain i - where len: "i<length as'" and ahdvd: "ah divides as'!i" + then obtain i where len: "i<length as'" and ahdvd: "ah divides as'!i" by auto from afs' carr have irrasi: "irreducible G (as'!i)" by (fast intro: nth_mem[OF len] elim: wfactorsE) - from len carr - have asicarr[simp]: "as'!i \<in> carrier G" by (unfold set_conv_nth, force) + from len carr have asicarr[simp]: "as'!i \<in> carrier G" + unfolding set_conv_nth by force note carr = carr asicarr - from ahdvd have "\<exists>x \<in> carrier G. as'!i = ah \<otimes> x" by fast - from this obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x" by auto - - with carr irrasi[simplified asi] - have asiah: "as'!i \<sim> ah" apply - + from ahdvd have "\<exists>x \<in> carrier G. as'!i = ah \<otimes> x" + by fast + then obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x" + by auto + with carr irrasi[simplified asi] have asiah: "as'!i \<sim> ah" + apply - apply (elim irreducible_prodE[of "ah" "x"], assumption+) apply (rule associatedI2[of x], assumption+) apply (rule irreducibleE[OF ahirr], simp) @@ -3371,86 +3087,78 @@ have "\<exists>aa_1. aa_1 \<in> carrier G \<and> wfactors G (take i as') aa_1" apply (intro wfactors_prod_exists) - using setparts afs' by (fast elim: wfactorsE, simp) - from this obtain aa_1 - where aa1carr: "aa_1 \<in> carrier G" - and aa1fs: "wfactors G (take i as') aa_1" - by auto + using setparts afs' + apply (fast elim: wfactorsE) + apply simp + done + then obtain aa_1 where aa1carr: "aa_1 \<in> carrier G" and aa1fs: "wfactors G (take i as') aa_1" + by auto have "\<exists>aa_2. aa_2 \<in> carrier G \<and> wfactors G (drop (Suc i) as') aa_2" apply (intro wfactors_prod_exists) - using setparts afs' by (fast elim: wfactorsE, simp) - from this obtain aa_2 - where aa2carr: "aa_2 \<in> carrier G" - and aa2fs: "wfactors G (drop (Suc i) as') aa_2" - by auto + using setparts afs' + apply (fast elim: wfactorsE) + apply simp + done + then obtain aa_2 where aa2carr: "aa_2 \<in> carrier G" + and aa2fs: "wfactors G (drop (Suc i) as') aa_2" + by auto note carr = carr aa1carr[simp] aa2carr[simp] from aa1fs aa2fs - have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)" + have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)" by (intro wfactors_mult, simp+) - hence v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))" + then have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))" apply (intro wfactors_mult_single) using setparts afs' - by (fast intro: nth_mem[OF len] elim: wfactorsE, simp+) - - from aa2carr carr aa1fs aa2fs - have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)" - by (metis irrasi wfactors_mult_single) + apply (fast intro: nth_mem[OF len] elim: wfactorsE) + apply simp_all + done + + from aa2carr carr aa1fs aa2fs have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)" + by (metis irrasi wfactors_mult_single) with len carr aa1carr aa2carr aa1fs - have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))" + have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))" apply (intro wfactors_mult) apply fast apply (simp, (fast intro: nth_mem[OF len])?)+ - done - - from len - have as': "as' = (take i as' @ as'!i # drop (Suc i) as')" + done + + from len have as': "as' = (take i as' @ as'!i # drop (Suc i) as')" by (simp add: Cons_nth_drop_Suc) - with carr - have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'" + with carr have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'" by simp - with v2 afs' carr aa1carr aa2carr nth_mem[OF len] - have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a" - by (metis as' ee_wfactorsD m_closed) - then - have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" + with v2 afs' carr aa1carr aa2carr nth_mem[OF len] have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a" + by (metis as' ee_wfactorsD m_closed) + then have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" by (metis aa1carr aa2carr asicarr m_lcomm) - from carr asiah - have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)" + from carr asiah have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)" by (metis associated_sym m_closed mult_cong_l) also note t1 - finally - have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" by simp - - with carr aa1carr aa2carr a'carr nth_mem[OF len] - have a': "aa_1 \<otimes> aa_2 \<sim> a'" + finally have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" by simp + + with carr aa1carr aa2carr a'carr nth_mem[OF len] have a': "aa_1 \<otimes> aa_2 \<sim> a'" by (simp add: a, fast intro: assoc_l_cancel[of ah _ a']) note v1 also note a' - finally have "wfactors G (take i as' @ drop (Suc i) as') a'" by simp - - from a'fs this carr - have "essentially_equal G as (take i as' @ drop (Suc i) as')" + finally have "wfactors G (take i as' @ drop (Suc i) as') a'" + by simp + + from a'fs this carr have "essentially_equal G as (take i as' @ drop (Suc i) as')" by (intro ih[of a']) simp - - hence ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')" - apply (elim essentially_equalE) apply (fastforce intro: essentially_equalI) - done - - from carr - have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as') + then have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')" + by (elim essentially_equalE) (fastforce intro: essentially_equalI) + + from carr have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as') (as' ! i # take i as' @ drop (Suc i) as')" proof (intro essentially_equalI) show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'" by simp next show "ah # take i as' @ drop (Suc i) as' [\<sim>] as' ! i # take i as' @ drop (Suc i) as'" - apply (simp add: list_all2_append) - apply (simp add: asiah[symmetric]) - done + by (simp add: list_all2_append) (simp add: asiah[symmetric]) qed note ee1 @@ -3458,15 +3166,16 @@ also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as') (take i as' @ as' ! i # drop (Suc i) as')" apply (intro essentially_equalI) - apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~> - take i as' @ as' ! i # drop (Suc i) as'") + apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~> + take i as' @ as' ! i # drop (Suc i) as'") apply simp apply (rule perm_append_Cons) apply simp done - finally - have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')" by simp - then show "essentially_equal G (ah # as) as'" by (subst as', assumption) + finally have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')" + by simp + then show "essentially_equal G (ah # as) as'" + by (subst as') qed qed @@ -3474,39 +3183,33 @@ assumes "wfactors G as a" "wfactors G as' a" and "a \<in> carrier G" "set as \<subseteq> carrier G" "set as' \<subseteq> carrier G" shows "essentially_equal G as as'" -apply (rule wfactors_unique__hlp_induct[rule_format, of a]) -apply (simp add: assms) -done + by (rule wfactors_unique__hlp_induct[rule_format, of a]) (simp add: assms) subsubsection \<open>Application to factorial monoids\<close> text \<open>Number of factors for wellfoundedness\<close> -definition - factorcount :: "_ \<Rightarrow> 'a \<Rightarrow> nat" where - "factorcount G a = - (THE c. (ALL as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as))" +definition factorcount :: "_ \<Rightarrow> 'a \<Rightarrow> nat" + where "factorcount G a = + (THE c. \<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as)" lemma (in monoid) ee_length: assumes ee: "essentially_equal G as bs" shows "length as = length bs" -apply (rule essentially_equalE[OF ee]) -apply (metis list_all2_conv_all_nth perm_length) -done + by (rule essentially_equalE[OF ee]) (metis list_all2_conv_all_nth perm_length) lemma (in factorial_monoid) factorcount_exists: assumes carr[simp]: "a \<in> carrier G" - shows "EX c. ALL as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as" + shows "\<exists>c. \<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as" proof - - have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" by (intro wfactors_exist, simp) - from this obtain as - where ascarr[simp]: "set as \<subseteq> carrier G" - and afs: "wfactors G as a" - by (auto simp del: carr) - have "ALL as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> length as = length as'" + have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" + by (intro wfactors_exist) simp + then obtain as where ascarr[simp]: "set as \<subseteq> carrier G" and afs: "wfactors G as a" + by (auto simp del: carr) + have "\<forall>as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> length as = length as'" by (metis afs ascarr assms ee_length wfactors_unique) - thus "EX c. ALL as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> c = length as'" .. + then show "\<exists>c. \<forall>as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> c = length as'" .. qed lemma (in factorial_monoid) factorcount_unique: @@ -3514,164 +3217,158 @@ and acarr[simp]: "a \<in> carrier G" and ascarr[simp]: "set as \<subseteq> carrier G" shows "factorcount G a = length as" proof - - have "EX ac. ALL as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as" by (rule factorcount_exists, simp) - from this obtain ac where - alen: "ALL as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as" - by auto + have "\<exists>ac. \<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as" + by (rule factorcount_exists) simp + then obtain ac where alen: "\<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as" + by auto have ac: "ac = factorcount G a" apply (simp add: factorcount_def) apply (rule theI2) apply (rule alen) apply (metis afs alen ascarr)+ - done - - from ascarr afs have "ac = length as" by (iprover intro: alen[rule_format]) - with ac show ?thesis by simp + done + from ascarr afs have "ac = length as" + by (iprover intro: alen[rule_format]) + with ac show ?thesis + by simp qed lemma (in factorial_monoid) divides_fcount: assumes dvd: "a divides b" - and acarr: "a \<in> carrier G" and bcarr:"b \<in> carrier G" - shows "factorcount G a <= factorcount G b" -apply (rule dividesE[OF dvd]) -proof - + and acarr: "a \<in> carrier G" + and bcarr:"b \<in> carrier G" + shows "factorcount G a \<le> factorcount G b" +proof (rule dividesE[OF dvd]) fix c - from assms - have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" by fast - from this obtain as - where ascarr: "set as \<subseteq> carrier G" - and afs: "wfactors G as a" - by auto - with acarr have fca: "factorcount G a = length as" by (intro factorcount_unique) + from assms have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" + by fast + then obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a" + by auto + with acarr have fca: "factorcount G a = length as" + by (intro factorcount_unique) assume ccarr: "c \<in> carrier G" - hence "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c" by fast - from this obtain cs - where cscarr: "set cs \<subseteq> carrier G" - and cfs: "wfactors G cs c" - by auto + then have "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c" + by fast + then obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfs: "wfactors G cs c" + by auto note [simp] = acarr bcarr ccarr ascarr cscarr assume b: "b = a \<otimes> c" - from afs cfs - have "wfactors G (as@cs) (a \<otimes> c)" by (intro wfactors_mult, simp+) - with b have "wfactors G (as@cs) b" by simp - hence "factorcount G b = length (as@cs)" by (intro factorcount_unique, simp+) - hence "factorcount G b = length as + length cs" by simp - with fca show ?thesis by simp + from afs cfs have "wfactors G (as@cs) (a \<otimes> c)" + by (intro wfactors_mult) simp_all + with b have "wfactors G (as@cs) b" + by simp + then have "factorcount G b = length (as@cs)" + by (intro factorcount_unique) simp_all + then have "factorcount G b = length as + length cs" + by simp + with fca show ?thesis + by simp qed lemma (in factorial_monoid) associated_fcount: - assumes acarr: "a \<in> carrier G" and bcarr:"b \<in> carrier G" + assumes acarr: "a \<in> carrier G" + and bcarr: "b \<in> carrier G" and asc: "a \<sim> b" shows "factorcount G a = factorcount G b" -apply (rule associatedE[OF asc]) -apply (drule divides_fcount[OF _ acarr bcarr]) -apply (drule divides_fcount[OF _ bcarr acarr]) -apply simp -done + apply (rule associatedE[OF asc]) + apply (drule divides_fcount[OF _ acarr bcarr]) + apply (drule divides_fcount[OF _ bcarr acarr]) + apply simp + done lemma (in factorial_monoid) properfactor_fcount: assumes acarr: "a \<in> carrier G" and bcarr:"b \<in> carrier G" and pf: "properfactor G a b" shows "factorcount G a < factorcount G b" -apply (rule properfactorE[OF pf], elim dividesE) -proof - +proof (rule properfactorE[OF pf], elim dividesE) fix c - from assms - have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" by fast - from this obtain as - where ascarr: "set as \<subseteq> carrier G" - and afs: "wfactors G as a" - by auto - with acarr have fca: "factorcount G a = length as" by (intro factorcount_unique) + from assms have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" + by fast + then obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a" + by auto + with acarr have fca: "factorcount G a = length as" + by (intro factorcount_unique) assume ccarr: "c \<in> carrier G" - hence "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c" by fast - from this obtain cs - where cscarr: "set cs \<subseteq> carrier G" - and cfs: "wfactors G cs c" - by auto + then have "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c" + by fast + then obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfs: "wfactors G cs c" + by auto assume b: "b = a \<otimes> c" - have "wfactors G (as@cs) (a \<otimes> c)" by (rule wfactors_mult) fact+ - with b - have "wfactors G (as@cs) b" by simp - with ascarr cscarr bcarr - have "factorcount G b = length (as@cs)" by (simp add: factorcount_unique) - hence fcb: "factorcount G b = length as + length cs" by simp + have "wfactors G (as@cs) (a \<otimes> c)" + by (rule wfactors_mult) fact+ + with b have "wfactors G (as@cs) b" + by simp + with ascarr cscarr bcarr have "factorcount G b = length (as@cs)" + by (simp add: factorcount_unique) + then have fcb: "factorcount G b = length as + length cs" + by simp assume nbdvda: "\<not> b divides a" have "c \<notin> Units G" proof (rule ccontr, simp) assume cunit:"c \<in> Units G" - - have "b \<otimes> inv c = a \<otimes> c \<otimes> inv c" by (simp add: b) - also from ccarr acarr cunit - have "\<dots> = a \<otimes> (c \<otimes> inv c)" by (fast intro: m_assoc) - also from ccarr cunit - have "\<dots> = a \<otimes> \<one>" by simp - also from acarr - have "\<dots> = a" by simp + have "b \<otimes> inv c = a \<otimes> c \<otimes> inv c" + by (simp add: b) + also from ccarr acarr cunit have "\<dots> = a \<otimes> (c \<otimes> inv c)" + by (fast intro: m_assoc) + also from ccarr cunit have "\<dots> = a \<otimes> \<one>" by simp + also from acarr have "\<dots> = a" by simp finally have "a = b \<otimes> inv c" by simp - with ccarr cunit - have "b divides a" by (fast intro: dividesI[of "inv c"]) + with ccarr cunit have "b divides a" + by (fast intro: dividesI[of "inv c"]) with nbdvda show False by simp qed - with cfs have "length cs > 0" apply - apply (rule ccontr, simp) apply (metis Units_one_closed ccarr cscarr l_one one_closed properfactorI3 properfactor_fmset unit_wfactors) done - with fca fcb show ?thesis by simp + with fca fcb show ?thesis + by simp qed sublocale factorial_monoid \<subseteq> divisor_chain_condition_monoid -apply unfold_locales -apply (rule wfUNIVI) -apply (rule measure_induct[of "factorcount G"]) -apply simp -apply (metis properfactor_fcount) -done + apply unfold_locales + apply (rule wfUNIVI) + apply (rule measure_induct[of "factorcount G"]) + apply simp + apply (metis properfactor_fcount) + done sublocale factorial_monoid \<subseteq> primeness_condition_monoid by standard (rule irreducible_prime) -lemma (in factorial_monoid) primeness_condition: - shows "primeness_condition_monoid G" - .. - -lemma (in factorial_monoid) gcd_condition [simp]: - shows "gcd_condition_monoid G" +lemma (in factorial_monoid) primeness_condition: "primeness_condition_monoid G" .. + +lemma (in factorial_monoid) gcd_condition [simp]: "gcd_condition_monoid G" by standard (rule gcdof_exists) sublocale factorial_monoid \<subseteq> gcd_condition_monoid by standard (rule gcdof_exists) -lemma (in factorial_monoid) division_weak_lattice [simp]: - shows "weak_lattice (division_rel G)" +lemma (in factorial_monoid) division_weak_lattice [simp]: "weak_lattice (division_rel G)" proof - - interpret weak_lower_semilattice "division_rel G" by simp - + interpret weak_lower_semilattice "division_rel G" + by simp show "weak_lattice (division_rel G)" - apply (unfold_locales, simp_all) - proof - + proof (unfold_locales, simp_all) fix x y assume carr: "x \<in> carrier G" "y \<in> carrier G" - - hence "\<exists>z. z \<in> carrier G \<and> z lcmof x y" by (rule lcmof_exists) - from this obtain z - where zcarr: "z \<in> carrier G" - and isgcd: "z lcmof x y" - by auto - with carr - have "least (division_rel G) z (Upper (division_rel G) {x, y})" - by (simp add: lcmof_leastUpper[symmetric]) - thus "\<exists>z. least (division_rel G) z (Upper (division_rel G) {x, y})" by fast + then have "\<exists>z. z \<in> carrier G \<and> z lcmof x y" + by (rule lcmof_exists) + then obtain z where zcarr: "z \<in> carrier G" and isgcd: "z lcmof x y" + by auto + with carr have "least (division_rel G) z (Upper (division_rel G) {x, y})" + by (simp add: lcmof_leastUpper[symmetric]) + then show "\<exists>z. least (division_rel G) z (Upper (division_rel G) {x, y})" + by fast qed qed @@ -3679,39 +3376,37 @@ subsection \<open>Factoriality Theorems\<close> theorem factorial_condition_one: (* Jacobson theorem 2.21 *) - shows "(divisor_chain_condition_monoid G \<and> primeness_condition_monoid G) = - factorial_monoid G" -apply rule + "(divisor_chain_condition_monoid G \<and> primeness_condition_monoid G) = factorial_monoid G" + apply rule proof clarify assume dcc: "divisor_chain_condition_monoid G" - and pc: "primeness_condition_monoid G" + and pc: "primeness_condition_monoid G" interpret divisor_chain_condition_monoid "G" by (rule dcc) interpret primeness_condition_monoid "G" by (rule pc) - show "factorial_monoid G" - by (fast intro: factorial_monoidI wfactors_exist wfactors_unique) + by (fast intro: factorial_monoidI wfactors_exist wfactors_unique) next assume fm: "factorial_monoid G" interpret factorial_monoid "G" by (rule fm) show "divisor_chain_condition_monoid G \<and> primeness_condition_monoid G" - by rule unfold_locales + by rule unfold_locales qed theorem factorial_condition_two: (* Jacobson theorem 2.22 *) shows "(divisor_chain_condition_monoid G \<and> gcd_condition_monoid G) = factorial_monoid G" -apply rule + apply rule proof clarify assume dcc: "divisor_chain_condition_monoid G" - and gc: "gcd_condition_monoid G" + and gc: "gcd_condition_monoid G" interpret divisor_chain_condition_monoid "G" by (rule dcc) interpret gcd_condition_monoid "G" by (rule gc) show "factorial_monoid G" - by (simp add: factorial_condition_one[symmetric], rule, unfold_locales) + by (simp add: factorial_condition_one[symmetric], rule, unfold_locales) next assume fm: "factorial_monoid G" interpret factorial_monoid "G" by (rule fm) show "divisor_chain_condition_monoid G \<and> gcd_condition_monoid G" - by rule unfold_locales + by rule unfold_locales qed end