# HG changeset patch # User nipkow # Date 1473610336 -7200 # Node ID 9c22a97b767445cc323e6e7a3b5d9000b9c344e2 # Parent f738df816abfa397824ee0f763fde565a714a86d# Parent ade7c3a20917c6c824cc765187e40dbe17e66fa8 merged diff -r ade7c3a20917 -r 9c22a97b7674 src/HOL/Algebra/Divisibility.thy --- a/src/HOL/Algebra/Divisibility.thy Sun Sep 11 18:12:05 2016 +0200 +++ b/src/HOL/Algebra/Divisibility.thy Sun Sep 11 18:12:16 2016 +0200 @@ -6,7 +6,7 @@ section \Divisibility in monoids and rings\ theory Divisibility -imports "~~/src/HOL/Library/Permutation" Coset Group + imports "~~/src/HOL/Library/Permutation" Coset Group begin section \Factorial Monoids\ @@ -14,22 +14,16 @@ subsection \Monoids with Cancellation Law\ locale monoid_cancel = monoid + - assumes l_cancel: - "\c \ a = c \ b; a \ carrier G; b \ carrier G; c \ carrier G\ \ a = b" - and r_cancel: - "\a \ c = b \ c; a \ carrier G; b \ carrier G; c \ carrier G\ \ a = b" + assumes l_cancel: "\c \ a = c \ b; a \ carrier G; b \ carrier G; c \ carrier G\ \ a = b" + and r_cancel: "\a \ c = b \ c; a \ carrier G; b \ carrier G; c \ carrier G\ \ a = b" lemma (in monoid) monoid_cancelI: - assumes l_cancel: - "\a b c. \c \ a = c \ b; a \ carrier G; b \ carrier G; c \ carrier G\ \ a = b" - and r_cancel: - "\a b c. \a \ c = b \ c; a \ carrier G; b \ carrier G; c \ carrier G\ \ a = b" + assumes l_cancel: "\a b c. \c \ a = c \ b; a \ carrier G; b \ carrier G; c \ carrier G\ \ a = b" + and r_cancel: "\a b c. \a \ c = b \ c; a \ carrier G; b \ carrier G; c \ carrier G\ \ 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 \ monoid_cancel by standard simp_all @@ -40,8 +34,7 @@ lemma comm_monoid_cancelI: fixes G (structure) assumes "comm_monoid G" - assumes cancel: - "\a b c. \a \ c = b \ c; a \ carrier G; b \ carrier G; c \ carrier G\ \ a = b" + assumes cancel: "\a b c. \a \ c = b \ c; a \ carrier G; b \ carrier G; c \ carrier G\ \ 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 \ comm_monoid_cancel - .. +sublocale comm_group \ comm_monoid_cancel .. subsection \Products of Units in Monoids\ lemma (in monoid) Units_m_closed[simp, intro]: - assumes h1unit: "h1 \ Units G" and h2unit: "h2 \ Units G" + assumes h1unit: "h1 \ Units G" + and h2unit: "h2 \ Units G" shows "h1 \ h2 \ 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 \ b \ Units G" and aunit[simp]: "a \ Units G" + assumes abunit[simp]: "a \ b \ Units G" + and aunit[simp]: "a \ Units G" and carr[simp]: "a \ carrier G" "b \ carrier G" shows "b \ Units G" proof - have c: "inv (a \ b) \ a \ carrier G" by simp - have "(inv (a \ b) \ a) \ b = inv (a \ b) \ (a \ b)" by (simp add: m_assoc) + have "(inv (a \ b) \ a) \ b = inv (a \ b) \ (a \ b)" + by (simp add: m_assoc) also have "\ = \" by simp finally have li: "(inv (a \ b) \ a) \ b = \" . have "\ = inv a \ a" by (simp add: Units_l_inv[symmetric]) also have "\ = inv a \ \ \ a" by simp also have "\ = inv a \ ((a \ b) \ inv (a \ b)) \ 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 "\ = ((inv a \ a) \ b) \ inv (a \ b) \ a" by (simp add: m_assoc del: Units_l_inv) also have "\ = b \ inv (a \ b) \ a" by simp also have "\ = b \ (inv (a \ b) \ a)" by (simp add: m_assoc) finally have ri: "b \ (inv (a \ b) \ a) = \ " by simp - from c li ri - show "b \ Units G" by (simp add: Units_def, fast) + from c li ri show "b \ Units G" by (auto simp: Units_def) qed lemma (in monoid) prod_unit_r: - assumes abunit[simp]: "a \ b \ Units G" and bunit[simp]: "b \ Units G" + assumes abunit[simp]: "a \ b \ Units G" + and bunit[simp]: "b \ Units G" and carr[simp]: "a \ carrier G" "b \ carrier G" shows "a \ Units G" proof - @@ -105,42 +99,39 @@ have "\ = b \ inv b" by (simp add: Units_r_inv[symmetric]) also have "\ = b \ \ \ inv b" by simp - also have "\ = b \ (inv (a \ b) \ (a \ b)) \ inv b" - by (simp add: Units_l_inv[OF abunit, symmetric] del: Units_l_inv) + also have "\ = b \ (inv (a \ b) \ (a \ b)) \ inv b" + by (simp add: Units_l_inv[OF abunit, symmetric] del: Units_l_inv) also have "\ = (b \ inv (a \ b) \ a) \ (b \ inv b)" by (simp add: m_assoc del: Units_l_inv) also have "\ = b \ inv (a \ b) \ a" by simp finally have ri: "(b \ inv (a \ b)) \ a = \ " by simp - from c li ri - show "a \ Units G" by (simp add: Units_def, fast) + from c li ri show "a \ Units G" by (auto simp: Units_def) qed lemma (in comm_monoid) unit_factor: assumes abunit: "a \ b \ Units G" and [simp]: "a \ carrier G" "b \ carrier G" shows "a \ Units G" -using abunit[simplified Units_def] + using abunit[simplified Units_def] proof clarsimp fix i assume [simp]: "i \ carrier G" - and li: "i \ (a \ b) = \" - and ri: "a \ b \ i = \" have carr': "b \ i \ carrier G" by simp have "(b \ i) \ a = (i \ b) \ a" by (simp add: m_comm) also have "\ = i \ (b \ a)" by (simp add: m_assoc) also have "\ = i \ (a \ b)" by (simp add: m_comm) - also note li + also assume "i \ (a \ b) = \" finally have li': "(b \ i) \ a = \" . have "a \ (b \ i) = a \ b \ i" by (simp add: m_assoc) - also note ri + also assume "a \ b \ i = \" finally have ri': "a \ (b \ i) = \" . from carr' li' ri' - show "a \ Units G" by (simp add: Units_def, fast) + show "a \ Units G" by (simp add: Units_def, fast) qed @@ -148,29 +139,23 @@ subsubsection \Function definitions\ -definition - factor :: "[_, 'a, 'a] \ bool" (infix "divides\" 65) +definition factor :: "[_, 'a, 'a] \ bool" (infix "divides\" 65) where "a divides\<^bsub>G\<^esub> b \ (\c\carrier G. b = a \\<^bsub>G\<^esub> c)" -definition - associated :: "[_, 'a, 'a] => bool" (infix "\\" 55) +definition associated :: "[_, 'a, 'a] \ bool" (infix "\\" 55) where "a \\<^bsub>G\<^esub> b \ a divides\<^bsub>G\<^esub> b \ b divides\<^bsub>G\<^esub> a" -abbreviation - "division_rel G == \carrier = carrier G, eq = op \\<^bsub>G\<^esub>, le = op divides\<^bsub>G\<^esub>\" - -definition - properfactor :: "[_, 'a, 'a] \ bool" +abbreviation "division_rel G \ \carrier = carrier G, eq = op \\<^bsub>G\<^esub>, le = op divides\<^bsub>G\<^esub>\" + +definition properfactor :: "[_, 'a, 'a] \ bool" where "properfactor G a b \ a divides\<^bsub>G\<^esub> b \ \(b divides\<^bsub>G\<^esub> a)" -definition - irreducible :: "[_, 'a] \ bool" +definition irreducible :: "[_, 'a] \ bool" where "irreducible G a \ a \ Units G \ (\b\carrier G. properfactor G b a \ b \ Units G)" -definition - prime :: "[_, 'a] \ bool" where - "prime G p \ - p \ Units G \ +definition prime :: "[_, 'a] \ bool" + where "prime G p \ + p \ Units G \ (\a\carrier G. \b\carrier G. p divides\<^bsub>G\<^esub> (a \\<^bsub>G\<^esub> b) \ p divides\<^bsub>G\<^esub> a \ p divides\<^bsub>G\<^esub> b)" @@ -181,24 +166,20 @@ assumes carr: "c \ carrier G" and p: "b = a \ 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 \ c" and carr: "c \ 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 "\c\carrier G. b = a \ 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\carrier G" - and "b = a \ c" - by auto - thus "P" by (elim elim) + obtain c where "c \ carrier G" and "b = a \ c" by auto + then show P by (elim elim) qed lemma (in monoid) divides_refl[simp, intro!]: assumes carr: "a \ carrier G" shows "a divides a" -apply (intro dividesI[of "\"]) -apply (simp, simp add: carr) -done + by (intro dividesI[of "\"]) (simp_all add: carr) lemma (in monoid) divides_trans [trans]: assumes dvds: "a divides b" "b divides c" and acarr: "a \ 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 \ carrier G" "b \ carrier G" "c \ carrier G" shows "(c \ a) divides (c \ 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 \ carrier G" "b \ carrier G" "c \ carrier G" shows "(c \ a) divides (c \ 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 \ carrier G" "b \ carrier G" "c \ carrier G" shows "(a \ c) divides (b \ 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 \ carrier G" "b \ carrier G" "c \ carrier G" shows "(a \ c) divides (b \ 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 \ carrier G" "b \ carrier G" "c \ carrier G" shows "a divides (b \ 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 \ carrier G" "b \ carrier G" "c \ carrier G" and ab: "a divides b" shows "a divides (c \ 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 \ Units G" - and acarr: "a \ carrier G" + and acarr: "a \ carrier G" shows "u divides a" proof (intro dividesI[of "(inv u) \ a"], fast intro: uunit acarr) - from uunit acarr - have xcarr: "inv u \ a \ carrier G" by fast - - from uunit acarr - have "u \ (inv u \ a) = (u \ inv u) \ a" by (fast intro: m_assoc[symmetric]) + from uunit acarr have xcarr: "inv u \ a \ carrier G" by fast + from uunit acarr have "u \ (inv u \ a) = (u \ inv u) \ a" + by (fast intro: m_assoc[symmetric]) also have "\ = \ \ a" by (simp add: Units_r_inv[OF uunit]) - also from acarr - have "\ = a" by simp - finally - show "a = u \ (inv u \ a)" .. + also from acarr have "\ = a" by simp + finally show "a = u \ (inv u \ a)" .. qed lemma (in comm_monoid) divides_unit: assumes udvd: "a divides u" - and carr: "a \ carrier G" "u \ Units G" + and carr: "a \ carrier G" "u \ Units G" shows "a \ 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 \ carrier G" shows "u \ Units G = u divides \" -using ucarr -by (fast dest: divides_unit intro: unit_divides) + using ucarr by (fast dest: divides_unit intro: unit_divides) subsubsection \Association\ @@ -315,83 +283,71 @@ fixes G (structure) assumes "a divides b" "b divides a" shows "a \ b" -using assms -by (simp add: associated_def) + using assms by (simp add: associated_def) lemma (in monoid) associatedI2: assumes uunit[simp]: "u \ Units G" and a: "a = b \ u" and bcarr[simp]: "b \ carrier G" shows "a \ 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 \ u" - and uunit: "u \ Units G" - and bcarr: "b \ carrier G" + assumes "a = b \ u" + and "u \ Units G" + and "b \ carrier G" shows "a \ b" -using assms by (intro associatedI2) + using assms by (intro associatedI2) lemma associatedD: fixes G (structure) assumes "a \ 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 \ b" and carr: "a \ carrier G" "b \ carrier G" shows "\u\Units G. a = b \ u" -using assoc -unfolding associated_def + using assoc + unfolding associated_def proof clarify assume "b divides a" - hence "\u\carrier G. a = b \ u" by (rule dividesD) - from this obtain u - where ucarr: "u \ carrier G" and a: "a = b \ u" - by auto + then have "\u\carrier G. a = b \ u" by (rule dividesD) + then obtain u where ucarr: "u \ carrier G" and a: "a = b \ u" + by auto assume "a divides b" - hence "\u'\carrier G. b = a \ u'" by (rule dividesD) - from this obtain u' - where u'carr: "u' \ carrier G" and b: "b = a \ u'" - by auto + then have "\u'\carrier G. b = a \ u'" by (rule dividesD) + then obtain u' where u'carr: "u' \ carrier G" and b: "b = a \ u'" + by auto note carr = carr ucarr u'carr - from carr - have "a \ \ = a" by simp + from carr have "a \ \ = a" by simp also have "\ = b \ u" by (simp add: a) also have "\ = a \ u' \ u" by (simp add: b) - also from carr - have "\ = a \ (u' \ u)" by (simp add: m_assoc) - finally - have "a \ \ = a \ (u' \ u)" . - with carr - have u1: "\ = u' \ u" by (fast dest: l_cancel) - - from carr - have "b \ \ = b" by simp + also from carr have "\ = a \ (u' \ u)" by (simp add: m_assoc) + finally have "a \ \ = a \ (u' \ u)" . + with carr have u1: "\ = u' \ u" by (fast dest: l_cancel) + + from carr have "b \ \ = b" by simp also have "\ = a \ u'" by (simp add: b) also have "\ = b \ u \ u'" by (simp add: a) - also from carr - have "\ = b \ (u \ u')" by (simp add: m_assoc) - finally - have "b \ \ = b \ (u \ u')" . - with carr - have u2: "\ = u \ u'" by (fast dest: l_cancel) - - from u'carr u1[symmetric] u2[symmetric] - have "\u'\carrier G. u' \ u = \ \ u \ u' = \" by fast - hence "u \ Units G" by (simp add: Units_def ucarr) - - from ucarr this a - show "\u\Units G. a = b \ u" by fast + also from carr have "\ = b \ (u \ u')" by (simp add: m_assoc) + finally have "b \ \ = b \ (u \ u')" . + with carr have u2: "\ = u \ u'" by (fast dest: l_cancel) + + from u'carr u1[symmetric] u2[symmetric] have "\u'\carrier G. u' \ u = \ \ u \ u' = \" + by fast + then have "u \ Units G" + by (simp add: Units_def ucarr) + with ucarr a show "\u\Units G. a = b \ u" by fast qed lemma associatedE: @@ -400,10 +356,9 @@ and e: "\a divides b; b divides a\ \ 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 \ carrier G" "b \ carrier G" shows "P" proof - - from assoc and carr - have "\u\Units G. a = b \ u" by (rule associatedD2) - from this obtain u - where "u \ Units G" "a = b \ u" - by auto - thus "P" by (elim e) + from assoc and carr have "\u\Units G. a = b \ u" + by (rule associatedD2) + then obtain u where "u \ Units G" "a = b \ u" + by auto + then show P by (elim e) qed lemma (in monoid) associated_refl [simp, intro!]: assumes "a \ carrier G" shows "a \ a" -using assms -by (fast intro: associatedI) + using assms by (fast intro: associatedI) lemma (in monoid) associated_sym [sym]: assumes "a \ b" and "a \ carrier G" "b \ carrier G" shows "b \ 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 \ b" "b \ c" and "a \ carrier G" "b \ carrier G" "c \ carrier G" shows "a \ 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 \ carrier G" "b \ carrier G" shows "a \ b" -using assms -by (fast intro: associatedI) + using assms by (fast intro: associatedI) lemma (in monoid) divides_cong_l [trans]: - assumes xx': "x \ x'" - and xdvdy: "x' divides y" - and carr [simp]: "x \ carrier G" "x' \ carrier G" "y \ carrier G" + assumes "x \ x'" + and "x' divides y" + and [simp]: "x \ carrier G" "x' \ carrier G" "y \ 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 \ y'" - and carr[simp]: "x \ carrier G" "y \ carrier G" "y' \ carrier G" + assumes "x divides y" + and "y \ y'" + and [simp]: "x \ carrier G" "y \ carrier G" "y' \ 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 \Multiplication and associativity\ lemma (in monoid_cancel) mult_cong_r: assumes "b \ b'" and carr: "a \ carrier G" "b \ carrier G" "b' \ carrier G" shows "a \ b \ a \ 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 \ a'" and carr: "a \ carrier G" "a' \ carrier G" "b \ carrier G" shows "a \ b \ a' \ 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 \ carrier G" "b \ carrier G" "b' \ carrier G" and "a \ b \ a \ b'" shows "b \ 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 \ b \ a' \ b" and carr: "a \ carrier G" "a' \ carrier G" "b \ carrier G" shows "a \ 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 \Units\ lemma (in monoid_cancel) assoc_unit_l [trans]: - assumes asc: "a \ b" and bunit: "b \ Units G" - and carr: "a \ carrier G" + assumes "a \ b" + and "b \ Units G" + and "a \ carrier G" shows "a \ 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 \ Units G" and asc: "a \ b" + assumes aunit: "a \ Units G" + and asc: "a \ b" and bcarr: "b \ carrier G" shows "b \ 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 \ Units G" and asc: "a \ b" and bcarr: "b \ carrier G" shows "b \ 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 \ Units G" "b \ Units G" shows "a \ b" -using units -by (fast intro: associatedI unit_divides) - -lemma (in monoid) Units_are_ones: - "Units G {.=}\<^bsub>(division_rel G)\<^esub> {\}" -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> {\}" + apply (simp add: set_eq_def elem_def, rule, simp_all) proof clarsimp fix a assume aunit: "a \ Units G" show "a \ \" - 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 "\ \ Units G" by simp moreover have "\ \ \" by simp ultimately show "\a \ Units G. \ \ 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 \Proper factors\ @@ -611,16 +552,14 @@ assumes "a divides b" and "\(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: "\(a \ 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 \ b" by (rule associatedI) @@ -632,9 +571,9 @@ and nunit: "b \ Units G" and carr: "a \ carrier G" "b \ carrier G" "p \ 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 \ carrier G" @@ -645,14 +584,13 @@ also have "\ = a \ (b \ c)" by (simp add: m_assoc) finally have "a \ \ = a \ (b \ c)" . - hence rinv: "\ = b \ c" by (intro l_cancel[of "a" "\" "b \ c"], simp+) + then have rinv: "\ = b \ c" by (intro l_cancel[of "a" "\" "b \ c"], simp+) also have "\ = c \ b" by (simp add: m_comm) finally have linv: "\ = c \ b" . - from ccarr linv[symmetric] rinv[symmetric] - have "b \ Units G" unfolding Units_def by fastforce - with nunit - show "False" .. + from ccarr linv[symmetric] rinv[symmetric] have "b \ 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: "\a divides b; \(b divides a)\ \ 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: "\a divides b; \(a \ b)\ \ 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 \ Units G" and pf: "properfactor G a u" and acarr: "a \ 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 \ carrier G" "b \ carrier G" "c \ 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 \ carrier G" "b \ carrier G" "c \ 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' \ x" and pf: "properfactor G x y" and carr: "x \ carrier G" "x' \ carrier G" "y \ 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 \\<^bsub>division_rel G\<^esub> y" - finally - show "x' \\<^bsub>division_rel G\<^esub> y" by (simp add: carr) + finally show "x' \\<^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 \ y'" and carr: "x \ carrier G" "y \ carrier G" "y' \ 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 \\<^bsub>division_rel G\<^esub> y" also from yy' - have "y .=\<^bsub>division_rel G\<^esub> y'" by simp - finally - show "x \\<^bsub>division_rel G\<^esub> y'" by (simp add: carr) + have "y .=\<^bsub>division_rel G\<^esub> y'" by simp + finally show "x \\<^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 \ carrier G" "b \ carrier G" "c \ carrier G" shows "properfactor G (c \ a) (c \ 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 \ carrier G" "b \ carrier G" "c \ carrier G" shows "properfactor G (c \ a) (c \ 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 \ carrier G" "b \ carrier G" "c \ carrier G" shows "properfactor G (a \ c) (b \ 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 \ carrier G" "b \ carrier G" "c \ carrier G" shows "properfactor G (a \ c) (b \ 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 \ carrier G" "b \ carrier G" "c \ carrier G" shows "properfactor G a (b \ 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 \ carrier G" "b \ carrier G" "c \ carrier G" shows "properfactor G a (c \ b)" -by (intro properfactor_trans2[OF ab] divides_prod_l, simp+) + by (intro properfactor_trans2[OF ab] divides_prod_l) simp_all subsection \Irreducible Elements and Primes\ @@ -794,77 +720,71 @@ assumes "a \ Units G" and "\b. \b \ carrier G; properfactor G b a\ \ b \ 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: "\a \ Units G; \b. b \ carrier G \ properfactor G b a \ b \ Units G\ \ P" + and elim: "\a \ Units G; \b. b \ carrier G \ properfactor G b a \ b \ Units G\ \ 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 \ carrier G" + and pf: "properfactor G b a" + and bcarr: "b \ carrier G" shows "b \ 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 \ a'" and carr[simp]: "a \ carrier G" "a' \ 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 \ Units G" and carr[simp]: "a \ carrier G" "b \ carrier G" shows "irreducible G (a \ b)" -using airr carr bunit -apply (elim irreducibleE, intro irreducibleI, clarify) - apply (subgoal_tac "a \ 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 \ 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 \ Units G" and carr [simp]: "a \ carrier G" "b \ carrier G" shows "irreducible G (a \ 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 \ b)" and carr[simp]: "a \ carrier G" "b \ carrier G" and e1: "\irreducible G a; b \ Units G\ \ P" and e2: "\a \ Units G; irreducible G b\ \ P" - shows "P" -using irr + shows P + using irr proof (elim irreducibleE) assume abnunit: "a \ b \ Units G" and isunit[rule_format]: "\ba. ba \ carrier G \ properfactor G ba (a \ b) \ ba \ Units G" - - show "P" + show P proof (cases "a \ Units G") - assume aunit: "a \ Units G" + case aunit: True have "irreducible G b" - apply (rule irreducibleI) + apply (rule irreducibleI) proof (rule ccontr, simp) assume "b \ Units G" with aunit have "(a \ b) \ Units G" by fast @@ -873,19 +793,18 @@ fix c assume ccarr: "c \ carrier G" and "properfactor G c b" - hence "properfactor G c (a \ b)" by (simp add: properfactor_prod_l[of c b a]) - from ccarr this show "c \ Units G" by (fast intro: isunit) + then have "properfactor G c (a \ b)" by (simp add: properfactor_prod_l[of c b a]) + with ccarr show "c \ 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 \ Units G" + case anunit: False with carr have "properfactor G b (b \ a)" by (fast intro: properfactorI3) - hence bf: "properfactor G b (a \ b)" by (subst m_comm[of a b], simp+) - hence bunit: "b \ Units G" by (intro isunit, simp) + then have bf: "properfactor G b (a \ b)" by (subst m_comm[of a b], simp+) + then have bunit: "b \ Units G" by (intro isunit, simp) have "irreducible G a" - apply (rule irreducibleI) + apply (rule irreducibleI) proof (rule ccontr, simp) assume "a \ Units G" with bunit have "(a \ b) \ Units G" by fast @@ -894,10 +813,10 @@ fix c assume ccarr: "c \ carrier G" and "properfactor G c a" - hence "properfactor G c (a \ b)" by (simp add: properfactor_prod_r[of c a b]) - from ccarr this show "c \ Units G" by (fast intro: isunit) + then have "properfactor G c (a \ b)" + by (simp add: properfactor_prod_r[of c a b]) + with ccarr show "c \ Units G" by (fast intro: isunit) qed - from this bunit show "P" by (rule e1) qed qed @@ -910,66 +829,57 @@ assumes "p \ Units G" and "\a b. \a \ carrier G; b \ carrier G; p divides (a \ b)\ \ p divides a \ 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: "\p \ Units G; \a\carrier G. \b\carrier G. - p divides a \ b \ p divides a \ p divides b\ \ P" + p divides a \ b \ p divides a \ p divides b\ \ 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 \ carrier G" "b \ carrier G" and pprime: "prime G p" and pdvd: "p divides a \ b" shows "p divides a \ 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 \ p'" and carr[simp]: "p \ carrier G" "p' \ 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 \Factorization and Factorial Monoids\ subsubsection \Function definitions\ -definition - factors :: "[_, 'a list, 'a] \ bool" +definition factors :: "[_, 'a list, 'a] \ bool" where "factors G fs a \ (\x \ (set fs). irreducible G x) \ foldr (op \\<^bsub>G\<^esub>) fs \\<^bsub>G\<^esub> = a" -definition - wfactors ::"[_, 'a list, 'a] \ bool" +definition wfactors ::"[_, 'a list, 'a] \ bool" where "wfactors G fs a \ (\x \ (set fs). irreducible G x) \ foldr (op \\<^bsub>G\<^esub>) fs \\<^bsub>G\<^esub> \\<^bsub>G\<^esub> a" -abbreviation - list_assoc :: "('a,_) monoid_scheme \ 'a list \ 'a list \ bool" (infix "[\]\" 44) - where "list_assoc G == list_all2 (op \\<^bsub>G\<^esub>)" - -definition - essentially_equal :: "[_, 'a list, 'a list] \ bool" +abbreviation list_assoc :: "('a,_) monoid_scheme \ 'a list \ 'a list \ bool" (infix "[\]\" 44) + where "list_assoc G \ list_all2 (op \\<^bsub>G\<^esub>)" + +definition essentially_equal :: "[_, 'a list, 'a list] \ bool" where "essentially_equal G fs1 fs2 \ (\fs1'. fs1 <~~> fs1' \ fs1' [\]\<^bsub>G\<^esub> fs2)" locale factorial_monoid = comm_monoid_cancel + - assumes factors_exist: - "\a \ carrier G; a \ Units G\ \ \fs. set fs \ carrier G \ factors G fs a" - and factors_unique: - "\factors G fs a; factors G fs' a; a \ carrier G; a \ Units G; - set fs \ carrier G; set fs' \ carrier G\ \ essentially_equal G fs fs'" + assumes factors_exist: "\a \ carrier G; a \ Units G\ \ \fs. set fs \ carrier G \ factors G fs a" + and factors_unique: + "\factors G fs a; factors G fs' a; a \ carrier G; a \ Units G; + set fs \ carrier G; set fs' \ carrier G\ \ essentially_equal G fs fs'" subsubsection \Comparing lists of elements\ @@ -979,44 +889,45 @@ lemma (in monoid) listassoc_refl [simp, intro]: assumes "set as \ carrier G" shows "as [\] as" -using assms -by (induct as) simp+ + using assms by (induct as) simp_all lemma (in monoid) listassoc_sym [sym]: assumes "as [\] bs" - and "set as \ carrier G" and "set bs \ carrier G" + and "set as \ carrier G" + and "set bs \ carrier G" shows "bs [\] 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 [\] bs" and "bs [\] cs" and "set as \ carrier G" and "set bs \ carrier G" and "set cs \ carrier G" shows "as [\] cs" -using assms -apply (simp add: list_all2_conv_all_nth set_conv_nth, safe) -apply (rule associated_trans) - apply (subgoal_tac "as ! i \ 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 \ bs ! i", assumption) + apply (simp, simp) + apply blast+ + done lemma (in monoid_cancel) irrlist_listassoc_cong: assumes "\a\set as. irreducible G a" and "as [\] bs" and "set as \ carrier G" and "set bs \ carrier G" shows "\a\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 \Permutations\ @@ -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 "\d. a <~~> d \ 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 [\] bs" and p: "bs <~~> cs" - shows "\bs'. as <~~> bs' \ bs' [\] 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 [\] bs" and p: "bs <~~> cs" + shows "\bs'. as <~~> bs' \ bs' [\] 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 [\] cs" - shows "\bs'. as [\] bs' \ 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 [\] cs" + shows "\bs'. as [\] bs' \ 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 _ _ "\as. as \ carrier G"] - -lemmas (in monoid) irrlist_perm_cong = - perm_setP[of _ _ "\as. \a\as. irreducible G a"] +lemmas (in monoid) perm_closed = perm_setP[of _ _ "\as. as \ carrier G"] + +lemmas (in monoid) irrlist_perm_cong = perm_setP[of _ _ "\as. \a\as. irreducible G a"] text \Essentially equal factorizations\ @@ -1082,70 +989,61 @@ lemma (in monoid) essentially_equalI: assumes ex: "fs1 <~~> fs1'" "fs1' [\] 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: "\fs1'. \fs1 <~~> fs1'; fs1' [\] fs2\ \ 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 \ 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 \ carrier G" "set bs \ carrier G" shows "essentially_equal G bs as" -using ee + using ee proof (elim essentially_equalE) fix fs assume "as <~~> fs" "fs [\] bs" - hence "\fs'. as [\] fs' \ fs' <~~> bs" by (rule perm_assoc_switch_r) - from this obtain fs' - where a: "as [\] fs'" and p: "fs' <~~> bs" - by auto + then have "\fs'. as [\] fs' \ fs' <~~> bs" + by (rule perm_assoc_switch_r) + then obtain fs' where a: "as [\] 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 \ carrier G" + and ascarr: "set as \ carrier G" and bscarr: "set bs \ carrier G" and cscarr: "set cs \ carrier G" shows "essentially_equal G as cs" -using ab bc + using ab bc proof (elim essentially_equalE) fix abs bcs assume "abs [\] bs" and pb: "bs <~~> bcs" - hence "\bs'. abs <~~> bs' \ bs' [\] bcs" by (rule perm_assoc_switch) - from this obtain bs' - where p: "abs <~~> bs'" and a: "bs' [\] bcs" - by auto + then have "\bs'. abs <~~> bs' \ bs' [\] bcs" + by (rule perm_assoc_switch) + then obtain bs' where p: "abs <~~> bs'" and a: "bs' [\] 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' \ carrier G" by (rule perm_closed) from pb bscarr have c2: "set bcs \ carrier G" by (rule perm_closed) note a also assume "bcs [\] cs" - finally (listassoc_trans) have"bs' [\] cs" by (simp add: c1 c2 cscarr) - - with pp - show ?thesis - by (rule essentially_equalI) + finally (listassoc_trans) have "bs' [\] 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 \ carrier G" shows "foldr (op \) fs \ \ carrier G" -by (insert ascarr, induct fs, simp+) + using ascarr by (induct fs) simp_all lemma (in comm_monoid) multlist_dividesI (*[intro]*): assumes "f \ set fs" and "f \ carrier G" and "set fs \ carrier G" shows "f divides (foldr (op \) fs \)" -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 [\] fs'" and "set fs \ carrier G" and "set fs' \ carrier G" shows "foldr (op \) fs \ \ foldr (op \) fs' \" -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 \ b" + assume "a \ b" and acarr: "a \ carrier G" and bcarr: "b \ carrier G" and ascarr: "set as \ carrier G" - hence p: "a \ foldr op \ as \ \ b \ foldr op \ as \" - by (fast intro: mult_cong_l) + then have p: "a \ foldr op \ as \ \ b \ foldr op \ as \" + by (fast intro: mult_cong_l) also - assume "as [\] bs" - and bscarr: "set bs \ carrier G" - and "\fs'. \as [\] fs'; set fs' \ carrier G\ \ foldr op \ as \ \ foldr op \ fs' \" - hence "foldr op \ as \ \ foldr op \ bs \" by simp - with ascarr bscarr bcarr - have "b \ foldr op \ as \ \ b \ foldr op \ bs \" - by (fast intro: mult_cong_r) - finally - show "a \ foldr op \ as \ \ b \ foldr op \ bs \" - by (simp add: ascarr bscarr acarr bcarr) + assume "as [\] bs" + and bscarr: "set bs \ carrier G" + and "\fs'. \as [\] fs'; set fs' \ carrier G\ \ foldr op \ as \ \ foldr op \ fs' \" + then have "foldr op \ as \ \ foldr op \ bs \" by simp + with ascarr bscarr bcarr have "b \ foldr op \ as \ \ b \ foldr op \ bs \" + by (fast intro: mult_cong_r) + finally show "a \ foldr op \ as \ \ b \ foldr op \ bs \" + by (simp add: ascarr bscarr acarr bcarr) qed qed @@ -1204,12 +1101,12 @@ assumes prm: "as <~~> bs" and ascarr: "set as \ carrier G" shows "foldr (op \) as \ = foldr (op \) bs \" -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 \ carrier G" - hence "set ys \ carrier G" by (rule perm_closed) + then have "set ys \ carrier G" by (rule perm_closed) moreover assume "set ys \ carrier G \ foldr op \ ys \ = foldr op \ zs \" ultimately show "foldr op \ ys \ = foldr op \ zs \" by simp qed @@ -1218,10 +1115,10 @@ assumes "essentially_equal G fs fs'" and "set fs \ carrier G" and "set fs' \ carrier G" shows "foldr (op \) fs \ \ foldr (op \) fs' \" -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 \Factorization in irreducible elements\ @@ -1231,53 +1128,42 @@ assumes "\f\set fs. irreducible G f" and "foldr (op \) fs \ \ 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: "\\f\set fs. irreducible G f; foldr (op \) fs \ \ a\ \ 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 "\f\set fs. irreducible G f" and "foldr (op \) fs \ = 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: "\\f\set fs. irreducible G f; foldr (op \) fs \ = a\ \ 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 \ 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 \ carrier G" shows "\a'. factors G as a' \ a' \ 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 \ carrier G" shows "a \ carrier G" -using assms -by (elim factorsE, clarsimp) + using assms by (elim factorsE, clarsimp) lemma (in monoid) nunit_factors: assumes anunit: "a \ Units G" @@ -1291,8 +1177,7 @@ lemma (in monoid) unit_wfactors [simp]: assumes aunit: "a \ 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 \ Units G" @@ -1303,27 +1188,21 @@ fix f fs' assume fs: "fs = f # fs'" - from carr - have fcarr[simp]: "f \ carrier G" - and carr'[simp]: "set fs' \ carrier G" - by (simp add: fs)+ - - from fs wf - have "irreducible G f" by (simp add: wfactors_def) - hence fnunit: "f \ Units G" by (fast elim: irreducibleE) - - from fs wf - have a: "f \ foldr (op \) fs' \ \ a" by (simp add: wfactors_def) + from carr have fcarr[simp]: "f \ carrier G" and carr'[simp]: "set fs' \ carrier G" + by (simp_all add: fs) + + from fs wf have "irreducible G f" by (simp add: wfactors_def) + then have fnunit: "f \ Units G" by (fast elim: irreducibleE) + + from fs wf have a: "f \ foldr (op \) fs' \ \ a" by (simp add: wfactors_def) note aunit also from fs wf - have a: "f \ foldr (op \) fs' \ \ a" by (simp add: wfactors_def) - have "a \ f \ foldr (op \) fs' \" - by (simp add: Units_closed[OF aunit] a[symmetric]) - finally - have "f \ foldr (op \) fs' \ \ Units G" by simp - hence "f \ Units G" by (intro unit_factor[of f], simp+) - + have a: "f \ foldr (op \) fs' \ \ a" by (simp add: wfactors_def) + have "a \ f \ foldr (op \) fs' \" + by (simp add: Units_closed[OF aunit] a[symmetric]) + finally have "f \ foldr (op \) fs' \ \ Units G" by simp + then have "f \ Units G" by (intro unit_factor[of f], simp+) with fnunit show "False" by simp qed @@ -1335,16 +1214,14 @@ and asc: "fs [\] fs'" and carr: "a \ carrier G" "set fs \ carrier G" "set fs' \ 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 \ fs' \ \ foldr op \ fs \" - by (simp add: multlist_listassoc_cong carr) + from asc[symmetric] have "foldr op \ fs' \ \ foldr op \ fs \" + by (simp add: multlist_listassoc_cong carr) also assume "foldr op \ fs \ \ a" - finally - show "foldr op \ fs' \ \ a" by (simp add: carr) + finally show "foldr op \ fs' \ \ a" by (simp add: carr) qed lemma (in comm_monoid) wfactors_perm_cong_l: @@ -1352,37 +1229,36 @@ and "fs <~~> fs'" and "set fs \ 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 \ carrier G" "set as \ carrier G" "set bs \ 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 \ carrier G" by (simp add: perm_closed) + with carr have fscarr: "set fs \ carrier G" by (simp add: perm_closed) note bfs also assume [symmetric]: "fs [\] 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 \ a'" and carr[simp]: "a \ carrier G" "a' \ carrier G" "set fs \ carrier G" shows "wfactors G fs a'" -using fac + using fac proof (elim wfactorsE, intro wfactorsI) assume "foldr op \ fs \ \ a" also note aa' finally show "foldr op \ fs \ \ a'" by simp @@ -1394,61 +1270,64 @@ lemma (in comm_monoid_cancel) unitfactor_ee: assumes uunit: "u \ Units G" and carr: "set as \ carrier G" - shows "essentially_equal G (as[0 := (as!0 \ 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 \ 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 \ Units G" and anunit: "a \ Units G" + assumes uunit: "u \ Units G" + and anunit: "a \ Units G" and afs: "factors G as a" and ascarr: "set as \ carrier G" - shows "factors G (as[0 := (as!0 \ u)]) (a \ 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 \ u)]) (a \ 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 \ carrier G" "b \ carrier G" - and ascarr[simp]: "set as \ carrier G" + and ascarr [simp]: "set as \ carrier G" shows "a \ b" -using afs bfs + using afs bfs proof (elim wfactorsE) from prm have [simp]: "set bs \ carrier G" by (simp add: perm_closed) assume "foldr op \ as \ \ a" - hence "a \ foldr op \ as \" by (rule associated_sym, simp+) + then have "a \ foldr op \ as \" by (rule associated_sym, simp+) also from prm - have "foldr op \ as \ = foldr op \ bs \" by (rule multlist_perm_cong, simp) + have "foldr op \ as \ = foldr op \ bs \" by (rule multlist_perm_cong, simp) also assume "foldr op \ bs \ \ b" - finally - show "a \ b" by simp + finally show "a \ b" by simp qed lemma (in comm_monoid_cancel) listassoc_wfactorsD: assumes assoc: "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 \ carrier G" "b \ carrier G" and [simp]: "set as \ carrier G" "set bs \ carrier G" shows "a \ b" -using afs bfs + using afs bfs proof (elim wfactorsE) assume "foldr op \ as \ \ a" - hence "a \ foldr op \ as \" by (rule associated_sym, simp+) + then have "a \ foldr op \ as \" by (rule associated_sym, simp+) also from assoc - have "foldr op \ as \ \ foldr op \ bs \" by (rule multlist_listassoc_cong, simp+) + have "foldr op \ as \ \ foldr op \ bs \" by (rule multlist_listassoc_cong, simp+) also assume "foldr op \ bs \ \ b" - finally - show "a \ b" by simp + finally show "a \ b" by simp qed lemma (in comm_monoid_cancel) ee_wfactorsD: @@ -1457,16 +1336,17 @@ and [simp]: "a \ carrier G" "b \ carrier G" and ascarr[simp]: "set as \ carrier G" and bscarr[simp]: "set bs \ carrier G" shows "a \ b" -using ee + using ee proof (elim essentially_equalE) fix fs assume prm: "as <~~> fs" - hence as'carr[simp]: "set fs \ 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 \ 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 [\] bs" - from this afs' bfs - show "a \ b" by (rule listassoc_wfactorsD, simp+) + from this afs' bfs show "a \ 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 \ carrier G" "set bs \ carrier G" shows "a \ 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 \ 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 "\u\Units G. a = b \ u" by (fast elim: associatedE2) - from this obtain u - where uunit: "u \ Units G" - and a: "a = b \ u" by auto - - from uunit bscarr - have ee: "essentially_equal G (bs[0 := (bs!0 \ u)]) bs" - (is "essentially_equal G ?bs' bs") - by (rule unitfactor_ee) - - from bscarr uunit - have bs'carr: "set ?bs' \ carrier G" - by (cases bs) (simp add: Units_closed)+ - - from uunit bnunit bfs bscarr - have fac: "factors G ?bs' (b \ u)" - by (rule factors_cong_unit) + factors_closed[OF bfs bscarr] bscarr[THEN subsetD] + + from ab carr have "\u\Units G. a = b \ u" + by (fast elim: associatedE2) + then obtain u where uunit: "u \ Units G" and a: "a = b \ u" + by auto + + from uunit bscarr have ee: "essentially_equal G (bs[0 := (bs!0 \ u)]) bs" + (is "essentially_equal G ?bs' bs") + by (rule unitfactor_ee) + + from bscarr uunit have bs'carr: "set ?bs' \ carrier G" + by (cases bs) (simp_all add: Units_closed) + + from uunit bnunit bfs bscarr have fac: "factors G ?bs' (b \ 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 \ carrier G" and bcarr[simp]: "b \ carrier G" and ascarr[simp]: "set as \ carrier G" and bscarr[simp]: "set bs \ carrier G" shows "essentially_equal G as bs" -using assms + using assms proof (cases "a \ Units G") - assume aunit: "a \ Units G" + case aunit: True also note asc finally have bunit: "b \ 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 \ Units G" + case anunit: False have bnunit: "b \ Units G" proof clarify assume "b \ Units G" also note asc[symmetric] finally have "a \ Units G" by simp - with anunit - show "False" .. + with anunit show False .. qed - have "\a'. factors G as a' \ a' \ a" by (rule wfactors_factors[OF asf ascarr]) - from this obtain a' - where fa': "factors G as a'" - and a': "a' \ a" - by auto - from fa' ascarr - have a'carr[simp]: "a' \ carrier G" by fast + have "\a'. factors G as a' \ a' \ a" + by (rule wfactors_factors[OF asf ascarr]) + then obtain a' where fa': "factors G as a'" and a': "a' \ a" + by auto + from fa' ascarr have a'carr[simp]: "a' \ carrier G" + by fast have a'nunit: "a' \ Units G" - proof (clarify) + proof clarify assume "a' \ Units G" also note a' finally have "a \ Units G" by simp with anunit - show "False" .. + show "False" .. qed - have "\b'. factors G bs b' \ b' \ b" by (rule wfactors_factors[OF bsf bscarr]) - from this obtain b' - where fb': "factors G bs b'" - and b': "b' \ b" - by auto - from fb' bscarr - have b'carr[simp]: "b' \ carrier G" by fast + have "\b'. factors G bs b' \ b' \ b" + by (rule wfactors_factors[OF bsf bscarr]) + then obtain b' where fb': "factors G bs b'" and b': "b' \ b" + by auto + from fb' bscarr have b'carr[simp]: "b' \ carrier G" + by fast have b'nunit: "b' \ Units G" - proof (clarify) + proof clarify assume "b' \ Units G" also note b' finally have "b \ 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' \ 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' \ 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 \ carrier G" and bcarr: "b \ carrier G" and ascarr: "set as \ carrier G" and bscarr: "set bs \ carrier G" shows asc: "a \ 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 \ carrier G" shows "\fs. set fs \ carrier G \ wfactors G fs a" proof (cases "a \ Units G") - assume "a \ 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 \ Units G" - hence "\fs. set fs \ carrier G \ factors G fs a" by (intro factors_exist acarr) - from this obtain fs - where fscarr: "set fs \ carrier G" - and f: "factors G fs a" - by auto + case False + then have "\fs. set fs \ carrier G \ factors G fs a" + by (intro factors_exist acarr) + then obtain fs where fscarr: "set fs \ 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 "\a \ set as. irreducible G a" and "set as \ carrier G" shows "\a. a \ carrier G \ 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 \ carrier G" - and "set fs \ carrier G" and "set fs' \ carrier G" + and "set fs \ carrier G" + and "set fs' \ 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 \ carrier G" shows "factors G (a # fb) (a \ 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 \ carrier G" "b \ carrier G" "set fb \ carrier G" + "a \ carrier G" "b \ carrier G" "set fb \ carrier G" shows "wfactors G (a # fb) (a \ 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 \ carrier G" and bscarr:"set fb \ carrier G" + and ascarr: "set fa \ carrier G" + and bscarr: "set fb \ carrier G" shows "factors G (fa @ fb) (a \ 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 \ carrier G" and bcarr: "b \ carrier G" and ascarr: "set as \ carrier G" and bscarr:"set bs \ carrier G" shows "wfactors G (as @ bs) (a \ 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' \ a" - and bsf': "factors G bs b'" and b'b: "b' \ b" + and bsf': "factors G bs b'" and b'b: "b' \ b" from asf' have a'carr: "a' \ carrier G" by (rule factors_closed) fact from bsf' have b'carr: "b' \ 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' \ b')" by (rule factors_mult) fact+ - - with carr - have abf': "wfactors G (as @ bs) (a' \ b')" by (intro factors_wfactors) simp+ - also from b'b carr - have trb: "a' \ b' \ a' \ b" by (intro mult_cong_r) - also from a'a carr - have tra: "a' \ b \ a \ b" by (intro mult_cong_l) - finally - show "wfactors G (as @ bs) (a \ b)" - by (simp add: carr) + from asf' bsf' have "factors G (as @ bs) (a' \ b')" + by (rule factors_mult) fact+ + + with carr have abf': "wfactors G (as @ bs) (a' \ b')" + by (intro factors_wfactors) simp_all + also from b'b carr have trb: "a' \ b' \ a' \ b" + by (intro mult_cong_r) + also from a'a carr have tra: "a' \ b \ a \ b" + by (intro mult_cong_l) + finally show "wfactors G (as @ bs) (a \ b)" + by (simp add: carr) qed lemma (in comm_monoid) factors_dividesI: - assumes "factors G fs a" and "f \ set fs" + assumes "factors G fs a" + and "f \ set fs" and "set fs \ 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 \ carrier G" and acarr: "a \ carrier G" and f: "f \ 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' \ a" - with fscarr - have a'carr: "a' \ 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' \ a" + with fscarr have a'carr: "a' \ 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 \Factorial monoids and wfactors\ lemma (in comm_monoid_cancel) factorial_monoidI: - assumes wfactors_exists: - "\a. a \ carrier G \ \fs. set fs \ carrier G \ wfactors G fs a" - and wfactors_unique: - "\a fs fs'. \a \ carrier G; set fs \ carrier G; set fs' \ carrier G; - wfactors G fs a; wfactors G fs' a\ \ essentially_equal G fs fs'" + assumes wfactors_exists: "\a. a \ carrier G \ \fs. set fs \ carrier G \ wfactors G fs a" + and wfactors_unique: + "\a fs fs'. \a \ carrier G; set fs \ carrier G; set fs' \ carrier G; + wfactors G fs a; wfactors G fs' a\ \ essentially_equal G fs fs'" shows "factorial_monoid G" proof fix a assume acarr: "a \ carrier G" and anunit: "a \ Units G" from wfactors_exists[OF acarr] - obtain as - where ascarr: "set as \ carrier G" - and afs: "wfactors G as a" - by auto - from afs ascarr - have "\a'. factors G as a' \ a' \ a" by (rule wfactors_factors) - from this obtain a' - where afs': "factors G as a'" - and a'a: "a' \ a" - by auto - from afs' ascarr - have a'carr: "a' \ carrier G" by fast + obtain as where ascarr: "set as \ carrier G" and afs: "wfactors G as a" + by auto + from afs ascarr have "\a'. factors G as a' \ a' \ a" + by (rule wfactors_factors) + then obtain a' where afs': "factors G as a'" and a'a: "a' \ a" + by auto + from afs' ascarr have a'carr: "a' \ carrier G" + by fast have a'nunit: "a' \ Units G" proof clarify assume "a' \ Units G" also note a'a finally have "a \ Units G" by (simp add: acarr) - with anunit - show "False" .. + with anunit show False .. qed - from a'carr acarr a'a - have "\u. u \ Units G \ a' = a \ u" by (blast elim: associatedE2) - from this obtain u - where uunit: "u \ Units G" - and a': "a' = a \ u" - by auto + from a'carr acarr a'a have "\u. u \ Units G \ a' = a \ u" + by (blast elim: associatedE2) + then obtain u where uunit: "u \ Units G" and a': "a' = a \ u" + by auto note [simp] = acarr Units_closed[OF uunit] Units_inv_closed[OF uunit] have "a = a \ \" by simp also have "\ = a \ (u \ inv u)" by (simp add: uunit) also have "\ = a' \ inv u" by (simp add: m_assoc[symmetric] a'[symmetric]) - finally - have a: "a = a' \ inv u" . - - from ascarr uunit - have cr: "set (as[0:=(as!0 \ inv u)]) \ carrier G" - by (cases as, clarsimp+) - - from afs' uunit a'nunit acarr ascarr - have "factors G (as[0:=(as!0 \ inv u)]) a" - by (simp add: a factors_cong_unit) - - with cr - show "\fs. set fs \ carrier G \ factors G fs a" by fast + finally have a: "a = a' \ inv u" . + + from ascarr uunit have cr: "set (as[0:=(as!0 \ inv u)]) \ carrier G" + by (cases as) auto + + from afs' uunit a'nunit acarr ascarr have "factors G (as[0:=(as!0 \ inv u)]) a" + by (simp add: a factors_cong_unit) + with cr show "\fs. set fs \ carrier G \ 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 (\a. assocs G a) as)" +abbreviation "assocs G x \ eq_closure_of (division_rel G) {x}" + +definition "fmset G as = mset (map (\a. assocs G a) as)" text \Helper lemmas\ @@ -1801,37 +1647,32 @@ assumes "y \ assocs G x" and "x \ 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 \ carrier G" shows "x \ 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 \ carrier G" shows "y \ 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 \ assocs G b" and "b \ carrier G" shows "a \ 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 \Comparing multisets\ @@ -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 [\] bs" and "set as \ carrier G" and "set bs \ 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 \ carrier G" "x \ carrier G" "z \ carrier G" assume "x \ a" also assume "a \ z" finally have "x \ z" by simp - with carr - show "x \ assocs G z" - by (intro closure_ofI2) simp+ + with carr show "x \ assocs G z" + by (intro closure_ofI2) simp_all next fix a x z assume carr[simp]: "a \ carrier G" "x \ carrier G" "z \ carrier G" assume "x \ z" also assume [symmetric]: "a \ z" finally have "x \ a" by simp - with carr - show "x \ assocs G a" - by (intro closure_ofI2) simp+ + with carr show "x \ assocs G a" + by (intro closure_ofI2) simp_all qed lemma (in comm_monoid_cancel) fmset_listassoc_cong: - assumes "as [\] bs" + assumes "as [\] bs" and "set as \ carrier G" and "set bs \ 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 \ carrier G" and bscarr: "set bs \ 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' \ 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' \ carrier G" + by (rule perm_closed) + + from prm have "fmset G as = fmset G as'" + by (rule fmset_perm_cong) also assume "as' [\] 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 "\as bs. (cas <~~> cbs \ cas = map (assocs G) as \ - cbs = map (assocs G) bs) \ (\as'. as <~~> as' \ 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 "\as bs. (cas <~~> cbs \ cas = map (assocs G) as \ + cbs = map (assocs G) bs) \ (\as'. as <~~> as' \ 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]: - "\asa bs. map (assocs G) as = map (assocs G) asa \ - ys = map (assocs G) bs - \ (\as'. asa <~~> as' \ map (assocs G) as' = map (assocs G) bs)" + "\asa bs. map (assocs G) as = map (assocs G) asa \ ys = map (assocs G) bs + \ (\as'. asa <~~> as' \ map (assocs G) as' = map (assocs G) bs)" and p2: "ys <~~> map (assocs G) bs" - and r2[rule_format]: - "\as bsa. ys = map (assocs G) as \ - map (assocs G) bs = map (assocs G) bsa - \ (\as'. as <~~> as' \ map (assocs G) as' = map (assocs G) bsa)" + and r2[rule_format]: "\as bsa. ys = map (assocs G) as \ map (assocs G) bs = map (assocs G) bsa + \ (\as'. as <~~> as' \ 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 \ 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 \ set as}" by auto with setys have "set ys \ { assocs G x | x. x \ set as}" by simp - hence "\yy. ys = map (assocs G) yy" - apply (induct ys, simp, clarsimp) + then have "\yy. ys = map (assocs G) yy" + apply (induct ys) + apply simp + apply clarsimp proof - fix yy x - show "\yya. (assocs G x) # map (assocs G) yy = - map (assocs G) yya" - by (rule exI[of _ "x#yy"], simp) + show "\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 "\as'. as <~~> as' \ 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 "\as'. yy <~~> as' \ 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 "\cs. as' <~~> cs \ 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 "\as'. as <~~> as' \ 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 "\as'. as <~~> as' \ 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 "\as'. yy <~~> as' \ 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 "\cs. as' <~~> cs \ 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 "\as'. as <~~> as' \ 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 \ carrier G" and bscarr: "set bs \ 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 "\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 "\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]: - "\as bs. (cas <~~> cbs \ cas = map (assocs G) as \ - cbs = map (assocs G) bs) - \ (\as'. as <~~> as' \ map (assocs G) as' = cbs)" - by (intro fmset_ee__hlp_induct, simp+) - with mpp cas cbs - have "\as'. as <~~> as' \ 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' \ carrier G" by simp + then obtain cbs where cbs: "cbs = map (assocs G) bs" by simp + + from cas cbs mpp have [rule_format]: + "\as bs. (cas <~~> cbs \ cas = map (assocs G) as \ cbs = map (assocs G) bs) + \ (\as'. as <~~> as' \ map (assocs G) as' = cbs)" + by (intro fmset_ee__hlp_induct, simp+) + with mpp cas cbs have "\as'. as <~~> as' \ 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' \ carrier G" + by simp from tm as'carr[THEN subsetD] bscarr[THEN subsetD] have "as' [\] 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 \ carrier G" and "set bs \ 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 \Interpreting multisets as factorizations\ @@ -2028,105 +1845,90 @@ shows "\cs. (\c \ set cs. P c) \ fmset G cs = Cs" proof - have "\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 "\cs. (\c \ set cs. P c) \ 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: "\X. X = a \ X \ set Cs' \ \x. P x \ X = assocs G x" and csP: "\x\set cs. P x" and mset: "mset (map (assocs G) cs) = mset Cs'" - from ih - have "\x. P x \ 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: "\x\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 "\cs. (\x\set cs. P x) \ - mset (map (assocs G) cs) = - add_mset a (mset Cs')" by fast + from ih have "\x. P x \ 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: "\x\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 "\cs. (\x\set cs. P x) \ 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: "\X. X \ set_mset Cs - \ \x. (x \ carrier G \ irreducible G x) \ X = assocs G x" + assumes elems: "\X. X \ set_mset Cs \ \x. (x \ carrier G \ irreducible G x) \ X = assocs G x" shows "\c cs. c \ carrier G \ set cs \ carrier G \ wfactors G cs c \ fmset G cs = Cs" proof - have "\cs. (\c\set cs. c \ carrier G \ irreducible G c) \ fmset G cs = Cs" - by (intro mset_fmsetEx, rule elems) - from this obtain cs - where p[rule_format]: "\c\set cs. c \ carrier G \ irreducible G c" - and Cs[symmetric]: "fmset G cs = Cs" - by auto - - from p - have cscarr: "set cs \ carrier G" by fast - - from p - have "\c. c \ carrier G \ wfactors G cs c" - by (intro wfactors_prod_exists) fast+ - from this obtain c - where ccarr: "c \ 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]: "\c\set cs. c \ carrier G \ irreducible G c" + and Cs[symmetric]: "fmset G cs = Cs" by auto + + from p have cscarr: "set cs \ carrier G" by fast + from p have "\c. c \ carrier G \ wfactors G cs c" + by (intro wfactors_prod_exists) auto + then obtain c where ccarr: "c \ carrier G" and cfs: "wfactors G cs c" by auto + with cscarr Cs show ?thesis by fast qed subsubsection \Multiplication on multisets\ 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 \ b)" + assumes afs: "wfactors G as a" + and bfs: "wfactors G bs b" + and cfs: "wfactors G cs (a \ b)" and carr: "a \ carrier G" "b \ carrier G" "set as \ carrier G" "set bs \ carrier G" "set cs \ carrier G" shows "fmset G cs = fmset G as + fmset G bs" proof - - from assms - have "wfactors G (as @ bs) (a \ b)" by (intro wfactors_mult) - with carr cfs - have "essentially_equal G cs (as@bs)" by (intro ee_wfactorsI[of "a\b" "a\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 \ b)" + by (intro wfactors_mult) + with carr cfs have "essentially_equal G cs (as@bs)" + by (intro ee_wfactorsI[of "a\b" "a\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 \ b)" + assumes afs: "factors G as a" + and bfs: "factors G bs b" + and cfs: "factors G cs (a \ b)" and "set as \ carrier G" "set bs \ carrier G" "set cs \ 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 \ carrier G" "b \ carrier G" "c \ carrier G" - "set as \ carrier G" "set bs \ carrier G" "set cs \ carrier G" + "set as \ carrier G" "set bs \ carrier G" "set cs \ carrier G" and fs: "wfactors G as a" "wfactors G bs b" "wfactors G cs c" shows "c \ a \ b" proof - - from carr fs - have m: "wfactors G (as @ bs) (a \ 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 \ a \ b" by (rule ee_wfactorsD[of "cs" "as@bs"]) (simp add: assms m)+ + from carr fs have m: "wfactors G (as @ bs) (a \ 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 \ a \ 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 \ carrier G" "b \ carrier G" "set as \ carrier G" "set bs \ carrier G" shows "fmset G as \# fmset G bs" -using ab + using ab proof (elim dividesE) fix c assume ccarr: "c \ carrier G" - hence "\cs. set cs \ carrier G \ wfactors G cs c" by (rule wfactors_exist) - from this obtain cs - where cscarr: "set cs \ carrier G" - and cfs: "wfactors G cs c" by auto + then have "\cs. set cs \ carrier G \ wfactors G cs c" + by (rule wfactors_exist) + then obtain cs where cscarr: "set cs \ carrier G" and cfs: "wfactors G cs c" + by auto note carr = carr ccarr cscarr assume "b = a \ 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 \# fmset G bs" - and afs: "wfactors G as a" and bfs: "wfactors G bs b" - and acarr: "a \ carrier G" and bcarr: "b \ carrier G" - and ascarr: "set as \ carrier G" and bscarr: "set bs \ carrier G" + and afs: "wfactors G as a" + and bfs: "wfactors G bs b" + and acarr: "a \ carrier G" + and bcarr: "b \ carrier G" + and ascarr: "set as \ carrier G" + and bscarr: "set bs \ carrier G" shows "a divides b" proof - from afs have airr: "\a \ set as. irreducible G a" by (fast elim: wfactorsE) @@ -2169,48 +1973,46 @@ proof (intro mset_wfactorsEx, simp) fix X assume "X \# fmset G bs - fmset G as" - hence "X \# fmset G bs" by (rule in_diffD) - hence "X \ set (map (assocs G) bs)" by (simp add: fmset_def) - hence "\x. x \ set bs \ X = assocs G x" by (induct bs) auto - from this obtain x - where xbs: "x \ set bs" - and X: "X = assocs G x" - by auto - + then have "X \# fmset G bs" by (rule in_diffD) + then have "X \ set (map (assocs G) bs)" by (simp add: fmset_def) + then have "\x. x \ set bs \ X = assocs G x" by (induct bs) auto + then obtain x where xbs: "x \ set bs" and X: "X = assocs G x" by auto with bscarr have xcarr: "x \ carrier G" by fast from xbs birr have xirr: "irreducible G x" by simp - from xcarr and xirr and X - show "\x. x \ carrier G \ irreducible G x \ X = assocs G x" by fast + from xcarr and xirr and X show "\x. x \ carrier G \ irreducible G x \ X = assocs G x" + by fast qed - from this obtain c cs - where ccarr: "c \ carrier G" - and cscarr: "set cs \ carrier G" + then obtain c cs + where ccarr: "c \ carrier G" + and cscarr: "set cs \ 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 \ a \ 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 \ a \ c" + by (rule fmset_wfactors_mult) fact+ + then show ?thesis proof (elim associatedE2) fix u assume "u \ Units G" "b = a \ c \ u" - with acarr ccarr - show "a divides b" by (fast intro: dividesI[of "c \ u"] m_assoc) - qed (simp add: acarr bcarr ccarr)+ + with acarr ccarr show "a divides b" + by (fast intro: dividesI[of "c \ 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 \ carrier G" and "b \ carrier G" - and "set as \ carrier G" and "set bs \ carrier G" + assumes "wfactors G as a" + and "wfactors G bs b" + and "a \ carrier G" + and "b \ carrier G" + and "set as \ carrier G" + and "set bs \ carrier G" shows "a divides b = (fmset G as \# fmset G bs)" -using assms -by (blast intro: divides_fmsubset fmsubset_divides) + using assms + by (blast intro: divides_fmsubset fmsubset_divides) text \Proper factors on multisets\ @@ -2218,35 +2020,41 @@ lemma (in factorial_monoid) fmset_properfactor: assumes asubb: "fmset G as \# fmset G bs" and anb: "fmset G as \ fmset G bs" - and "wfactors G as a" and "wfactors G bs b" - and "a \ carrier G" and "b \ carrier G" - and "set as \ carrier G" and "set bs \ carrier G" + and "wfactors G as a" + and "wfactors G bs b" + and "a \ carrier G" + and "b \ carrier G" + and "set as \ carrier G" + and "set bs \ 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 \# 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 \# 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 \ carrier G" and "b \ carrier G" - and "set as \ carrier G" and "set bs \ carrier G" + and "wfactors G as a" + and "wfactors G bs b" + and "a \ carrier G" + and "b \ carrier G" + and "set as \ carrier G" + and "set bs \ carrier G" shows "fmset G as \# fmset G bs \ fmset G as \ 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 \Irreducible Elements are Prime\ @@ -2254,88 +2062,78 @@ assumes pirr: "irreducible G p" and pcarr: "p \ carrier G" shows "prime G p" -using pirr + using pirr proof (elim irreducibleE, intro primeI) fix a b assume acarr: "a \ carrier G" and bcarr: "b \ carrier G" and pdvdab: "p divides (a \ b)" and pnunit: "p \ Units G" assume irreduc[rule_format]: - "\b. b \ carrier G \ properfactor G b p \ b \ Units G" + "\b. b \ carrier G \ properfactor G b p \ b \ Units G" from pdvdab - have "\c\carrier G. a \ b = p \ c" by (rule dividesD) - from this obtain c - where ccarr: "c \ carrier G" - and abpc: "a \ b = p \ c" - by auto - - from acarr have "\fs. set fs \ carrier G \ wfactors G fs a" by (rule wfactors_exist) - from this obtain as where ascarr: "set as \ carrier G" and afs: "wfactors G as a" by auto - - from bcarr have "\fs. set fs \ carrier G \ wfactors G fs b" by (rule wfactors_exist) - from this obtain bs where bscarr: "set bs \ carrier G" and bfs: "wfactors G bs b" by auto - - from ccarr have "\fs. set fs \ carrier G \ wfactors G fs c" by (rule wfactors_exist) - from this obtain cs where cscarr: "set cs \ carrier G" and cfs: "wfactors G cs c" by auto + have "\c\carrier G. a \ b = p \ c" by (rule dividesD) + then obtain c where ccarr: "c \ carrier G" and abpc: "a \ b = p \ c" + by auto + + from acarr have "\fs. set fs \ carrier G \ wfactors G fs a" + by (rule wfactors_exist) + then obtain as where ascarr: "set as \ carrier G" and afs: "wfactors G as a" + by auto + + from bcarr have "\fs. set fs \ carrier G \ wfactors G fs b" + by (rule wfactors_exist) + then obtain bs where bscarr: "set bs \ carrier G" and bfs: "wfactors G bs b" + by auto + + from ccarr have "\fs. set fs \ carrier G \ wfactors G fs c" + by (rule wfactors_exist) + then obtain cs where cscarr: "set cs \ 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 \ b)" by (rule wfactors_mult) fact+ - - from pirr cfs - have pcfs: "wfactors G (p # cs) (p \ c)" by (rule wfactors_mult_single) fact+ - with abpc - have abfs': "wfactors G (p # cs) (a \ b)" by simp - - from abfs' abfs - have "essentially_equal G (p # cs) (as @ bs)" - by (rule wfactors_unique) simp+ - - hence "\ds. p # cs <~~> ds \ ds [\] (as @ bs)" - by (fast elim: essentially_equalE) - from this obtain ds - where "p # cs <~~> ds" - and dsassoc: "ds [\] (as @ bs)" - by auto - + from afs and bfs have abfs: "wfactors G (as @ bs) (a \ b)" + by (rule wfactors_mult) fact+ + + from pirr cfs have pcfs: "wfactors G (p # cs) (p \ c)" + by (rule wfactors_mult_single) fact+ + with abpc have abfs': "wfactors G (p # cs) (a \ b)" + by simp + + from abfs' abfs have "essentially_equal G (p # cs) (as @ bs)" + by (rule wfactors_unique) simp+ + + then have "\ds. p # cs <~~> ds \ ds [\] (as @ bs)" + by (fast elim: essentially_equalE) + then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\] (as @ bs)" + by auto then have "p \ set ds" - by (simp add: perm_set_eq[symmetric]) - with dsassoc - have "\p'. p' \ set (as@bs) \ p \ p'" - unfolding list_all2_conv_all_nth set_conv_nth - by force - - from this obtain p' - where "p' \ set (as@bs)" - and pp': "p \ p'" - by auto - - hence "p' \ set as \ p' \ set bs" by simp - moreover - { - assume p'elem: "p' \ set as" + by (simp add: perm_set_eq[symmetric]) + with dsassoc have "\p'. p' \ set (as@bs) \ p \ p'" + unfolding list_all2_conv_all_nth set_conv_nth by force + then obtain p' where "p' \ set (as@bs)" and pp': "p \ p'" + by auto + then consider "p' \ set as" | "p' \ set bs" by auto + then show "p divides a \ p divides b" + proof cases + case 1 with ascarr have [simp]: "p' \ 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' \ 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' \ 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 \ 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 \ 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 \ carrier G" + assume acarr: "a \ carrier G" and bcarr: "b \ carrier G" and pdvdab: "p divides (a \ b)" - assume irreduc[rule_format]: - "\b. b \ carrier G \ properfactor G b p \ b \ Units G" - from pdvdab - have "\c\carrier G. a \ b = p \ c" by (rule dividesD) - from this obtain c - where ccarr: "c \ carrier G" - and abpc: "a \ b = p \ c" - by auto + assume irreduc[rule_format]: "\b. b \ carrier G \ properfactor G b p \ b \ Units G" + from pdvdab have "\c\carrier G. a \ b = p \ c" + by (rule dividesD) + then obtain c where ccarr: "c \ carrier G" and abpc: "a \ b = p \ c" + by auto note [simp] = pcarr acarr bcarr ccarr show "p divides a \ p divides b" proof (cases "a \ Units G") - assume aunit: "a \ Units G" + case aunit: True note pdvdab also have "a \ b = b \ a" by (simp add: m_comm) - also from aunit - have bab: "b \ a \ b" - by (intro associatedI2[of "a"], simp+) - finally - have "p divides b" by simp - thus "p divides a \ p divides b" .. + also from aunit have bab: "b \ a \ b" + by (intro associatedI2[of "a"], simp+) + finally have "p divides b" by simp + then show ?thesis .. next - assume anunit: "a \ Units G" - - show "p divides a \ p divides b" + case anunit: False + show ?thesis proof (cases "b \ Units G") - assume bunit: "b \ Units G" - + case bunit: True note pdvdab also from bunit - have baa: "a \ b \ a" - by (intro associatedI2[of "b"], simp+) - finally - have "p divides a" by simp - thus "p divides a \ p divides b" .. + have baa: "a \ b \ a" + by (intro associatedI2[of "b"], simp+) + finally have "p divides a" by simp + then show ?thesis .. next - assume bnunit: "b \ Units G" - + case bnunit: False have cnunit: "c \ Units G" proof (rule ccontr, simp) assume cunit: "c \ Units G" - from bnunit - have "properfactor G a (a \ b)" - by (intro properfactorI3[of _ _ b], simp+) + from bnunit have "properfactor G a (a \ b)" + by (intro properfactorI3[of _ _ b], simp+) also note abpc - also from cunit - have "p \ c \ p" - by (intro associatedI2[of c], simp+) - finally - have "properfactor G a p" by simp - - with acarr - have "a \ Units G" by (fast intro: irreduc) - with anunit - show "False" .. + also from cunit have "p \ c \ p" + by (intro associatedI2[of c], simp+) + finally have "properfactor G a p" by simp + with acarr have "a \ Units G" by (fast intro: irreduc) + with anunit show False .. qed have abnunit: "a \ b \ Units G" proof clarsimp - assume abunit: "a \ b \ Units G" - hence "a \ Units G" by (rule unit_factor) fact+ - with anunit - show "False" .. + assume "a \ b \ Units G" + then have "a \ Units G" by (rule unit_factor) fact+ + with anunit show False .. qed - from acarr anunit have "\fs. set fs \ carrier G \ factors G fs a" by (rule factors_exist) - then obtain as where ascarr: "set as \ carrier G" and afac: "factors G as a" by auto - - from bcarr bnunit have "\fs. set fs \ carrier G \ factors G fs b" by (rule factors_exist) - then obtain bs where bscarr: "set bs \ carrier G" and bfac: "factors G bs b" by auto - - from ccarr cnunit have "\fs. set fs \ carrier G \ factors G fs c" by (rule factors_exist) - then obtain cs where cscarr: "set cs \ carrier G" and cfac: "factors G cs c" by auto + from acarr anunit have "\fs. set fs \ carrier G \ factors G fs a" + by (rule factors_exist) + then obtain as where ascarr: "set as \ carrier G" and afac: "factors G as a" + by auto + + from bcarr bnunit have "\fs. set fs \ carrier G \ factors G fs b" + by (rule factors_exist) + then obtain bs where bscarr: "set bs \ carrier G" and bfac: "factors G bs b" + by auto + + from ccarr cnunit have "\fs. set fs \ carrier G \ factors G fs c" + by (rule factors_exist) + then obtain cs where cscarr: "set cs \ 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 \ b)" by (rule factors_mult) fact+ - - from pirr cfac - have pcfac: "factors G (p # cs) (p \ c)" by (rule factors_mult_single) fact+ - with abpc - have abfac': "factors G (p # cs) (a \ b)" by simp - - from abfac' abfac - have "essentially_equal G (p # cs) (as @ bs)" - by (rule factors_unique) (fact | simp)+ - - hence "\ds. p # cs <~~> ds \ ds [\] (as @ bs)" - by (fast elim: essentially_equalE) - from this obtain ds - where "p # cs <~~> ds" - and dsassoc: "ds [\] (as @ bs)" - by auto - + from afac and bfac have abfac: "factors G (as @ bs) (a \ b)" + by (rule factors_mult) fact+ + + from pirr cfac have pcfac: "factors G (p # cs) (p \ c)" + by (rule factors_mult_single) fact+ + with abpc have abfac': "factors G (p # cs) (a \ b)" + by simp + + from abfac' abfac have "essentially_equal G (p # cs) (as @ bs)" + by (rule factors_unique) (fact | simp)+ + then have "\ds. p # cs <~~> ds \ ds [\] (as @ bs)" + by (fast elim: essentially_equalE) + then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\] (as @ bs)" + by auto then have "p \ set ds" - by (simp add: perm_set_eq[symmetric]) - with dsassoc - have "\p'. p' \ set (as@bs) \ p \ p'" - unfolding list_all2_conv_all_nth set_conv_nth - by force - - from this obtain p' - where "p' \ set (as@bs)" - and pp': "p \ p'" by auto - - hence "p' \ set as \ p' \ set bs" by simp - moreover - { - assume p'elem: "p' \ set as" + by (simp add: perm_set_eq[symmetric]) + with dsassoc have "\p'. p' \ set (as@bs) \ p \ p'" + unfolding list_all2_conv_all_nth set_conv_nth by force + then obtain p' where "p' \ set (as@bs)" and pp': "p \ p'" + by auto + then consider "p' \ set as" | "p' \ set bs" by auto + then show "p divides a \ p divides b" + proof cases + case 1 with ascarr have [simp]: "p' \ 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' \ 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' \ 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 \ p divides b" by fast + then show ?thesis .. + qed qed qed qed @@ -2492,39 +2266,31 @@ subsubsection \Definitions\ -definition - isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \ bool" ("(_ gcdof\ _ _)" [81,81,81] 80) +definition isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \ bool" ("(_ gcdof\ _ _)" [81,81,81] 80) where "x gcdof\<^bsub>G\<^esub> a b \ x divides\<^bsub>G\<^esub> a \ x divides\<^bsub>G\<^esub> b \ (\y\carrier G. (y divides\<^bsub>G\<^esub> a \ y divides\<^bsub>G\<^esub> b \ y divides\<^bsub>G\<^esub> x))" -definition - islcm :: "[_, 'a, 'a, 'a] \ bool" ("(_ lcmof\ _ _)" [81,81,81] 80) +definition islcm :: "[_, 'a, 'a, 'a] \ bool" ("(_ lcmof\ _ _)" [81,81,81] 80) where "x lcmof\<^bsub>G\<^esub> a b \ a divides\<^bsub>G\<^esub> x \ b divides\<^bsub>G\<^esub> x \ (\y\carrier G. (a divides\<^bsub>G\<^esub> y \ b divides\<^bsub>G\<^esub> y \ x divides\<^bsub>G\<^esub> y))" -definition - somegcd :: "('a,_) monoid_scheme \ 'a \ 'a \ 'a" +definition somegcd :: "('a,_) monoid_scheme \ 'a \ 'a \ 'a" where "somegcd G a b = (SOME x. x \ carrier G \ x gcdof\<^bsub>G\<^esub> a b)" -definition - somelcm :: "('a,_) monoid_scheme \ 'a \ 'a \ 'a" +definition somelcm :: "('a,_) monoid_scheme \ 'a \ 'a \ 'a" where "somelcm G a b = (SOME x. x \ carrier G \ 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: - "\a \ carrier G; b \ carrier G\ \ \c. c \ carrier G \ c gcdof a b" + assumes gcdof_exists: "\a \ carrier G; b \ carrier G\ \ \c. c \ carrier G \ c gcdof a b" locale primeness_condition_monoid = comm_monoid_cancel + - assumes irreducible_prime: - "\a \ carrier G; irreducible G a\ \ prime G a" + assumes irreducible_prime: "\a \ carrier G; irreducible G a\ \ prime G a" locale divisor_chain_condition_monoid = comm_monoid_cancel + - assumes division_wellfounded: - "wf {(x, y). x \ carrier G \ y \ carrier G \ properfactor G x y}" + assumes division_wellfounded: "wf {(x, y). x \ carrier G \ y \ carrier G \ properfactor G x y}" subsubsection \Connections to \texttt{Lattice.thy}\ @@ -2532,222 +2298,208 @@ lemma gcdof_greatestLower: fixes G (structure) assumes carr[simp]: "a \ carrier G" "b \ carrier G" - shows "(x \ carrier G \ 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 \ carrier G \ 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 \ carrier G" "b \ carrier G" - shows "(x \ carrier G \ 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 \ carrier G \ 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 \ carrier G" "b \ 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 \ carrier G" "b \ 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 \ carrier G" "b \ carrier G" shows "b gcdof a b" -using assms -unfolding isgcd_def -by fast + using assms unfolding isgcd_def by fast subsubsection \Existence of gcd and lcm\ lemma (in factorial_monoid) gcdof_exists: - assumes acarr: "a \ carrier G" and bcarr: "b \ carrier G" + assumes acarr: "a \ carrier G" + and bcarr: "b \ carrier G" shows "\c. c \ carrier G \ c gcdof a b" proof - from acarr have "\as. set as \ carrier G \ wfactors G as a" by (rule wfactors_exist) - from this obtain as - where ascarr: "set as \ carrier G" - and afs: "wfactors G as a" - by auto - from afs have airr: "\a \ set as. irreducible G a" by (fast elim: wfactorsE) - - from bcarr have "\bs. set bs \ carrier G \ wfactors G bs b" by (rule wfactors_exist) - from this obtain bs - where bscarr: "set bs \ carrier G" - and bfs: "wfactors G bs b" - by auto - from bfs have birr: "\b \ set bs. irreducible G b" by (fast elim: wfactorsE) - - have "\c cs. c \ carrier G \ set cs \ carrier G \ wfactors G cs c \ - fmset G cs = fmset G as #\ fmset G bs" + then obtain as where ascarr: "set as \ carrier G" and afs: "wfactors G as a" + by auto + from afs have airr: "\a \ set as. irreducible G a" + by (fast elim: wfactorsE) + + from bcarr have "\bs. set bs \ carrier G \ wfactors G bs b" + by (rule wfactors_exist) + then obtain bs where bscarr: "set bs \ carrier G" and bfs: "wfactors G bs b" + by auto + from bfs have birr: "\b \ set bs. irreducible G b" + by (fast elim: wfactorsE) + + have "\c cs. c \ carrier G \ set cs \ carrier G \ wfactors G cs c \ + fmset G cs = fmset G as #\ fmset G bs" proof (intro mset_wfactorsEx) fix X assume "X \# fmset G as #\ fmset G bs" - hence "X \# fmset G as" by simp - hence "X \ set (map (assocs G) as)" by (simp add: fmset_def) - hence "\x. X = assocs G x \ x \ set as" by (induct as) auto - from this obtain x - where X: "X = assocs G x" - and xas: "x \ set as" - by auto - with ascarr have xcarr: "x \ carrier G" by fast - from xas airr have xirr: "irreducible G x" by simp - - from xcarr and xirr and X - show "\x. (x \ carrier G \ irreducible G x) \ X = assocs G x" by fast + then have "X \# fmset G as" by simp + then have "X \ set (map (assocs G) as)" + by (simp add: fmset_def) + then have "\x. X = assocs G x \ x \ set as" + by (induct as) auto + then obtain x where X: "X = assocs G x" and xas: "x \ set as" + by auto + with ascarr have xcarr: "x \ carrier G" + by fast + from xas airr have xirr: "irreducible G x" + by simp + from xcarr and xirr and X show "\x. (x \ carrier G \ irreducible G x) \ X = assocs G x" + by fast qed - - from this obtain c cs - where ccarr: "c \ carrier G" - and cscarr: "set cs \ carrier G" + then obtain c cs + where ccarr: "c \ carrier G" + and cscarr: "set cs \ carrier G" and csirr: "wfactors G cs c" - and csmset: "fmset G cs = fmset G as #\ fmset G bs" by auto + and csmset: "fmset G cs = fmset G as #\ fmset G bs" + by auto have "c gcdof a b" proof (simp add: isgcd_def, safe) from csmset - have "fmset G cs \# 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 \# 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 \# 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 \# 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 \ carrier G" - hence "\ys. set ys \ carrier G \ wfactors G ys y" by (rule wfactors_exist) - from this obtain ys - where yscarr: "set ys \ carrier G" - and yfs: "wfactors G ys y" - by auto + then have "\ys. set ys \ carrier G \ wfactors G ys y" + by (rule wfactors_exist) + then obtain ys where yscarr: "set ys \ carrier G" and yfs: "wfactors G ys y" + by auto assume "y divides a" - hence ya: "fmset G ys \# fmset G as" by (rule divides_fmsubset) fact+ + then have ya: "fmset G ys \# fmset G as" + by (rule divides_fmsubset) fact+ assume "y divides b" - hence yb: "fmset G ys \# fmset G bs" by (rule divides_fmsubset) fact+ - - from ya yb csmset - have "fmset G ys \# fmset G cs" by (simp add: subset_mset_def) - thus "y divides c" by (rule fmsubset_divides) fact+ + then have yb: "fmset G ys \# fmset G bs" + by (rule divides_fmsubset) fact+ + + from ya yb csmset have "fmset G ys \# fmset G cs" + by (simp add: subset_mset_def) + then show "y divides c" + by (rule fmsubset_divides) fact+ qed - - with ccarr - show "\c. c \ carrier G \ c gcdof a b" by fast + with ccarr show "\c. c \ carrier G \ c gcdof a b" + by fast qed lemma (in factorial_monoid) lcmof_exists: - assumes acarr: "a \ carrier G" and bcarr: "b \ carrier G" + assumes acarr: "a \ carrier G" + and bcarr: "b \ carrier G" shows "\c. c \ carrier G \ c lcmof a b" proof - - from acarr have "\as. set as \ carrier G \ wfactors G as a" by (rule wfactors_exist) - from this obtain as - where ascarr: "set as \ carrier G" - and afs: "wfactors G as a" - by auto - from afs have airr: "\a \ set as. irreducible G a" by (fast elim: wfactorsE) - - from bcarr have "\bs. set bs \ carrier G \ wfactors G bs b" by (rule wfactors_exist) - from this obtain bs - where bscarr: "set bs \ carrier G" - and bfs: "wfactors G bs b" - by auto - from bfs have birr: "\b \ set bs. irreducible G b" by (fast elim: wfactorsE) - - have "\c cs. c \ carrier G \ set cs \ carrier G \ wfactors G cs c \ - fmset G cs = (fmset G as - fmset G bs) + fmset G bs" + from acarr have "\as. set as \ carrier G \ wfactors G as a" + by (rule wfactors_exist) + then obtain as where ascarr: "set as \ carrier G" and afs: "wfactors G as a" + by auto + from afs have airr: "\a \ set as. irreducible G a" + by (fast elim: wfactorsE) + + from bcarr have "\bs. set bs \ carrier G \ wfactors G bs b" + by (rule wfactors_exist) + then obtain bs where bscarr: "set bs \ carrier G" and bfs: "wfactors G bs b" + by auto + from bfs have birr: "\b \ set bs. irreducible G b" + by (fast elim: wfactorsE) + + have "\c cs. c \ carrier G \ set cs \ carrier G \ wfactors G cs c \ + fmset G cs = (fmset G as - fmset G bs) + fmset G bs" proof (intro mset_wfactorsEx) fix X assume "X \# (fmset G as - fmset G bs) + fmset G bs" - hence "X \# fmset G as \ X \# fmset G bs" + then have "X \# fmset G as \ X \# fmset G bs" by (auto dest: in_diffD) - moreover - { - assume "X \ set_mset (fmset G as)" - hence "X \ set (map (assocs G) as)" by (simp add: fmset_def) - hence "\x. x \ set as \ X = assocs G x" by (induct as) auto - from this obtain x - where xas: "x \ set as" - and X: "X = assocs G x" by auto - + then consider "X \ set_mset (fmset G as)" | "X \ set_mset (fmset G bs)" + by fast + then show "\x. (x \ carrier G \ irreducible G x) \ X = assocs G x" + proof cases + case 1 + then have "X \ set (map (assocs G) as)" by (simp add: fmset_def) + then have "\x. x \ set as \ X = assocs G x" by (induct as) auto + then obtain x where xas: "x \ set as" and X: "X = assocs G x" by auto with ascarr have xcarr: "x \ carrier G" by fast from xas airr have xirr: "irreducible G x" by simp - - from xcarr and xirr and X - have "\x. (x \ carrier G \ irreducible G x) \ X = assocs G x" by fast - } - moreover - { - assume "X \ set_mset (fmset G bs)" - hence "X \ set (map (assocs G) bs)" by (simp add: fmset_def) - hence "\x. x \ set bs \ X = assocs G x" by (induct as) auto - from this obtain x - where xbs: "x \ 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 \ set (map (assocs G) bs)" by (simp add: fmset_def) + then have "\x. x \ set bs \ X = assocs G x" by (induct as) auto + then obtain x where xbs: "x \ set bs" and X: "X = assocs G x" by auto with bscarr have xcarr: "x \ carrier G" by fast from xbs birr have xirr: "irreducible G x" by simp - - from xcarr and xirr and X - have "\x. (x \ carrier G \ irreducible G x) \ X = assocs G x" by fast - } - ultimately - show "\x. (x \ carrier G \ irreducible G x) \ 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 \ carrier G" - and cscarr: "set cs \ carrier G" + then obtain c cs + where ccarr: "c \ carrier G" + and cscarr: "set cs \ 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 \# 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 \# 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 \# fmset G cs" by (simp add: subset_mset_def) - thus "b divides c" by (rule fmsubset_divides) fact+ + from csmset have "fmset G bs \# 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 \ carrier G" - hence "\ys. set ys \ carrier G \ wfactors G ys y" by (rule wfactors_exist) - from this obtain ys - where yscarr: "set ys \ carrier G" - and yfs: "wfactors G ys y" - by auto + then have "\ys. set ys \ carrier G \ wfactors G ys y" + by (rule wfactors_exist) + then obtain ys where yscarr: "set ys \ carrier G" and yfs: "wfactors G ys y" + by auto assume "a divides y" - hence ya: "fmset G as \# fmset G ys" by (rule divides_fmsubset) fact+ + then have ya: "fmset G as \# fmset G ys" + by (rule divides_fmsubset) fact+ assume "b divides y" - hence yb: "fmset G bs \# fmset G ys" by (rule divides_fmsubset) fact+ - - from ya yb csmset - have "fmset G cs \# fmset G ys" + then have yb: "fmset G bs \# fmset G ys" + by (rule divides_fmsubset) fact+ + + from ya yb csmset have "fmset G cs \# 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 "\c. c \ carrier G \ c lcmof a b" by fast + with ccarr show "\c. c \ carrier G \ c lcmof a b" + by fast qed @@ -2756,23 +2508,21 @@ subsubsection \Gcd condition\ 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 \ carrier G" "y \ carrier G" - hence "\z. z \ carrier G \ z gcdof x y" by (rule gcdof_exists) - from this obtain z - where zcarr: "z \ 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 "\z. greatest (division_rel G) z (Lower (division_rel G) {x, y})" by fast + then have "\z. z \ carrier G \ z gcdof x y" by (rule gcdof_exists) + then obtain z where zcarr: "z \ 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 "\z. greatest (division_rel G) z (Lower (division_rel G) {x, y})" + by fast qed qed @@ -2787,13 +2537,13 @@ have "a' \ carrier G \ 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 \ carrier G" "b \ 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 \ carrier G \ (somegcd G a b) gcdof a b" + interpret weak_lower_semilattice "division_rel G" + by simp + from carr have "somegcd G a b \ carrier G \ (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 \ carrier G" "b \ carrier G" shows "\x\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 \ carrier G" "b \ 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 \ carrier G" "b \ 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 \ carrier G" "y \ carrier G" "z \ 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 \ carrier G" "x' \ carrier G" "y \ carrier G" shows "somegcd G x y \ 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: "\y\carrier G. y divides b \ y divides c \ y divides a" and acarr: "a \ carrier G" and bcarr: "b \ carrier G" and ccarr: "c \ carrier G" shows "a \ 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 \ carrier G" and bcarr: "b \ carrier G" and ccarr: "c \ carrier G" + assumes "a gcdof b c" and "a \ carrier G" and "b \ carrier G" and "c \ carrier G" shows "a \ 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 \ carrier G" "A \ {}" shows "\x\ 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 \ carrier G" "b \ carrier G" "c \ carrier G" shows "somegcd G (somegcd G a b) c \ 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 \ ?d divides (c \ a)" by (simp add: divides_mult_lI) + then have cd'ca: "c \ ?d divides (c \ a)" by (simp add: divides_mult_lI) have "?d divides b" by (simp add: gcd_divides_r) - hence cd'cb: "c \ ?d divides (c \ b)" by (simp add: divides_mult_lI) - - from cd'ca cd'cb - have cd'e: "c \ ?d divides ?e" - by (rule gcd_divides) simp+ - - hence "\u. u \ carrier G \ ?e = c \ ?d \ u" - by (elim dividesE, fast) - from this obtain u - where ucarr[simp]: "u \ carrier G" - and e_cdu: "?e = c \ ?d \ u" - by auto + then have cd'cb: "c \ ?d divides (c \ b)" by (simp add: divides_mult_lI) + + from cd'ca cd'cb have cd'e: "c \ ?d divides ?e" + by (rule gcd_divides) simp_all + then have "\u. u \ carrier G \ ?e = c \ ?d \ u" + by (elim dividesE) fast + then obtain u where ucarr[simp]: "u \ carrier G" and e_cdu: "?e = c \ ?d \ u" + by auto note carr = carr ucarr - have "?e divides c \ a" by (rule gcd_divides_l) simp+ - hence "\x. x \ carrier G \ c \ a = ?e \ x" - by (elim dividesE, fast) - from this obtain x - where xcarr: "x \ carrier G" - and ca_ex: "c \ a = ?e \ x" - by auto - with e_cdu - have ca_cdux: "c \ a = c \ ?d \ u \ x" by simp - - from ca_cdux xcarr - have "c \ a = c \ (?d \ u \ x)" by (simp add: m_assoc) - then have "a = ?d \ u \ x" by (rule l_cancel[of c a]) (simp add: xcarr)+ - hence du'a: "?d \ u divides a" by (rule dividesI[OF xcarr]) - - have "?e divides c \ b" by (intro gcd_divides_r, simp+) - hence "\x. x \ carrier G \ c \ b = ?e \ x" - by (elim dividesE, fast) - from this obtain x - where xcarr: "x \ carrier G" - and cb_ex: "c \ b = ?e \ x" - by auto - with e_cdu - have cb_cdux: "c \ b = c \ ?d \ u \ x" by simp - - from cb_cdux xcarr - have "c \ b = c \ (?d \ u \ x)" by (simp add: m_assoc) - with xcarr - have "b = ?d \ u \ x" by (intro l_cancel[of c b], simp+) - hence du'b: "?d \ u divides b" by (intro dividesI[OF xcarr]) - - from du'a du'b carr - have du'd: "?d \ u divides ?d" - by (intro gcd_divides, simp+) - hence uunit: "u \ Units G" + have "?e divides c \ a" by (rule gcd_divides_l) simp_all + then have "\x. x \ carrier G \ c \ a = ?e \ x" + by (elim dividesE) fast + then obtain x where xcarr: "x \ carrier G" and ca_ex: "c \ a = ?e \ x" + by auto + with e_cdu have ca_cdux: "c \ a = c \ ?d \ u \ x" + by simp + + from ca_cdux xcarr have "c \ a = c \ (?d \ u \ x)" + by (simp add: m_assoc) + then have "a = ?d \ u \ x" + by (rule l_cancel[of c a]) (simp add: xcarr)+ + then have du'a: "?d \ u divides a" + by (rule dividesI[OF xcarr]) + + have "?e divides c \ b" by (intro gcd_divides_r) simp_all + then have "\x. x \ carrier G \ c \ b = ?e \ x" + by (elim dividesE) fast + then obtain x where xcarr: "x \ carrier G" and cb_ex: "c \ b = ?e \ x" + by auto + with e_cdu have cb_cdux: "c \ b = c \ ?d \ u \ x" + by simp + + from cb_cdux xcarr have "c \ b = c \ (?d \ u \ x)" + by (simp add: m_assoc) + with xcarr have "b = ?d \ u \ x" + by (intro l_cancel[of c b]) simp_all + then have du'b: "?d \ u divides b" + by (intro dividesI[OF xcarr]) + + from du'a du'b carr have du'd: "?d \ u divides ?d" + by (intro gcd_divides) simp_all + then have uunit: "u \ Units G" proof (elim dividesE) fix v assume vcarr[simp]: "v \ carrier G" @@ -3017,108 +2766,100 @@ have "?d \ \ = ?d \ u \ v" by simp fact also have "?d \ u \ v = ?d \ (u \ v)" by (simp add: m_assoc) finally have "?d \ \ = ?d \ (u \ v)" . - hence i2: "\ = u \ v" by (rule l_cancel) simp+ - hence i1: "\ = v \ u" by (simp add: m_comm) - from vcarr i1[symmetric] i2[symmetric] - show "u \ Units G" - by (unfold Units_def, simp, fast) + then have i2: "\ = u \ v" by (rule l_cancel) simp_all + then have i1: "\ = v \ u" by (simp add: m_comm) + from vcarr i1[symmetric] i2[symmetric] show "u \ Units G" + by (auto simp: Units_def) qed - from e_cdu uunit - have "somegcd G (c \ a) (c \ b) \ c \ somegcd G a b" - by (intro associatedI2[of u], simp+) - from this[symmetric] - show "c \ somegcd G a b \ somegcd G (c \ a) (c \ b)" by simp + from e_cdu uunit have "somegcd G (c \ a) (c \ b) \ c \ somegcd G a b" + by (intro associatedI2[of u]) simp_all + from this[symmetric] show "c \ somegcd G a b \ somegcd G (c \ a) (c \ b)" + by simp qed lemma (in monoid) assoc_subst: assumes ab: "a \ b" - and cP: "ALL a b. a : carrier G & b : carrier G & a \ b - --> f a : carrier G & f b : carrier G & f a \ f b" + and cP: "\a b. a \ carrier G \ b \ carrier G \ a \ b + \ f a \ carrier G \ f b \ carrier G \ f a \ f b" and carr: "a \ carrier G" "b \ carrier G" shows "f a \ f b" using assms by auto lemma (in gcd_condition_monoid) relprime_mult: - assumes abrelprime: "somegcd G a b \ \" and acrelprime: "somegcd G a c \ \" + assumes abrelprime: "somegcd G a b \ \" + and acrelprime: "somegcd G a c \ \" and carr[simp]: "a \ carrier G" "b \ carrier G" "c \ carrier G" shows "somegcd G a (b \ c) \ \" proof - have "c = c \ \" by simp also from abrelprime[symmetric] - have "\ \ c \ somegcd G a b" - by (rule assoc_subst) (simp add: mult_cong_r)+ - also have "\ \ somegcd G (c \ a) (c \ b)" by (rule gcd_mult) fact+ - finally - have c: "c \ somegcd G (c \ a) (c \ b)" by simp - - from carr - have a: "a \ somegcd G a (c \ a)" - by (fast intro: gcdI divides_prod_l) - - have "somegcd G a (b \ c) \ somegcd G a (c \ b)" by (simp add: m_comm) - also from a - have "\ \ somegcd G (somegcd G a (c \ a)) (c \ b)" - by (rule assoc_subst) (simp add: gcd_cong_l)+ - also from gcd_assoc - have "\ \ somegcd G a (somegcd G (c \ a) (c \ b))" - by (rule assoc_subst) simp+ - also from c[symmetric] - have "\ \ somegcd G a c" - by (rule assoc_subst) (simp add: gcd_cong_r)+ + have "\ \ c \ somegcd G a b" + by (rule assoc_subst) (simp add: mult_cong_r)+ + also have "\ \ somegcd G (c \ a) (c \ b)" + by (rule gcd_mult) fact+ + finally have c: "c \ somegcd G (c \ a) (c \ b)" + by simp + + from carr have a: "a \ somegcd G a (c \ a)" + by (fast intro: gcdI divides_prod_l) + + have "somegcd G a (b \ c) \ somegcd G a (c \ b)" + by (simp add: m_comm) + also from a have "\ \ somegcd G (somegcd G a (c \ a)) (c \ b)" + by (rule assoc_subst) (simp add: gcd_cong_l)+ + also from gcd_assoc have "\ \ somegcd G a (somegcd G (c \ a) (c \ b))" + by (rule assoc_subst) simp+ + also from c[symmetric] have "\ \ somegcd G a c" + by (rule assoc_subst) (simp add: gcd_cong_r)+ also note acrelprime - finally - show "somegcd G a (b \ c) \ \" by simp + finally show "somegcd G a (b \ c) \ \" + 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 \ carrier G" and acarr: "a \ carrier G" and bcarr: "b \ carrier G" and pirr: "irreducible G p" and pdvdab: "p divides a \ b" - from pirr - have pnunit: "p \ Units G" - and r[rule_format]: "\b. b \ carrier G \ properfactor G b p \ b \ Units G" - by - (fast elim: irreducibleE)+ + from pirr have pnunit: "p \ Units G" + and r[rule_format]: "\b. b \ carrier G \ properfactor G b p \ b \ Units G" + by (fast elim: irreducibleE)+ show "p divides a \ p divides b" proof (rule ccontr, clarsimp) assume npdvda: "\ p divides a" - with pcarr acarr - have "\ \ 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 "\ \ 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 \ 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 \ \" by (fast intro: associated_sym[of "\"] 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 \ \" + by (fast intro: associated_sym[of "\"] gcd_closed) assume npdvdb: "\ p divides b" - with pcarr bcarr - have "\ \ 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 "\ \ 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 \ 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 \ \" by (fast intro: associated_sym[of "\"] gcd_closed) - - from pcarr acarr bcarr pdvdab - have "p gcdof p (a \ b)" by (fast intro: isgcd_divides_l) - - with pcarr acarr bcarr - have "p \ somegcd G p (a \ b)" by (fast intro: gcdI2) - also from pa pb pcarr acarr bcarr - have "somegcd G p (a \ b) \ \" by (rule relprime_mult) - finally have "p \ \" by (simp add: pcarr acarr bcarr) - - with pcarr - have "p \ 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 \ \" + by (fast intro: associated_sym[of "\"] gcd_closed) + + from pcarr acarr bcarr pdvdab have "p gcdof p (a \ b)" + by (fast intro: isgcd_divides_l) + with pcarr acarr bcarr have "p \ somegcd G p (a \ b)" + by (fast intro: gcdI2) + also from pa pb pcarr acarr bcarr have "somegcd G p (a \ b) \ \" + by (rule relprime_mult) + finally have "p \ \" + by (simp add: pcarr acarr bcarr) + with pcarr have "p \ Units G" + by (fast intro: assoc_unit_l) + with pnunit show False .. qed qed @@ -3158,86 +2897,70 @@ shows "\as. set as \ carrier G \ wfactors G as a" proof - have r[rule_format]: "a \ carrier G \ (\as. set as \ carrier G \ wfactors G as a)" - apply (rule wf_induct[OF division_wellfounded]) - proof - + proof (rule wf_induct[OF division_wellfounded]) fix x assume ih: "\y. (y, x) \ {(x, y). x \ carrier G \ y \ carrier G \ properfactor G x y} \ y \ carrier G \ (\as. set as \ carrier G \ wfactors G as y)" show "x \ carrier G \ (\as. set as \ carrier G \ wfactors G as x)" - apply clarify - apply (cases "x \ 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 \ 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 \ carrier G" and xnunit: "x \ Units G" and xnirr: "\ irreducible G x" - hence "\y. y \ carrier G \ properfactor G y x \ y \ Units G" - apply - apply (rule ccontr, simp) + then have "\y. y \ carrier G \ properfactor G y x \ y \ 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 \ carrier G" - and ynunit: "y \ Units G" - and pfyx: "properfactor G y x" - by auto - - have ih': - "\y. \y \ carrier G; properfactor G y x\ - \ \as. set as \ carrier G \ wfactors G as y" - by (rule ih[rule_format, simplified]) (simp add: xcarr)+ - - from ycarr pfyx - have "\as. set as \ carrier G \ wfactors G as y" - by (rule ih') - from this obtain ys - where yscarr: "set ys \ carrier G" - and yfs: "wfactors G ys y" - by auto - - from pfyx - have "y divides x" - and nyx: "\ y \ x" - by - (fast elim: properfactorE2)+ - hence "\z. z \ carrier G \ x = y \ z" - by fast - - from this obtain z - where zcarr: "z \ carrier G" - and x: "x = y \ z" - by auto - - from zcarr ycarr - have "properfactor G z x" + done + then obtain y where ycarr: "y \ carrier G" and ynunit: "y \ Units G" + and pfyx: "properfactor G y x" + by auto + + have ih': "\y. \y \ carrier G; properfactor G y x\ + \ \as. set as \ carrier G \ wfactors G as y" + by (rule ih[rule_format, simplified]) (simp add: xcarr)+ + + from ycarr pfyx have "\as. set as \ carrier G \ wfactors G as y" + by (rule ih') + then obtain ys where yscarr: "set ys \ carrier G" and yfs: "wfactors G ys y" + by auto + + from pfyx have "y divides x" and nyx: "\ y \ x" + by (fast elim: properfactorE2)+ + then have "\z. z \ carrier G \ x = y \ z" + by fast + then obtain z where zcarr: "z \ carrier G" and x: "x = y \ 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 "\as. set as \ carrier G \ wfactors G as z" - by (rule ih') - from this obtain zs - where zscarr: "set zs \ carrier G" - and zfs: "wfactors G zs z" - by auto - - from yscarr zscarr - have xscarr: "set (ys@zs) \ carrier G" by simp - from yfs zfs ycarr zcarr yscarr zscarr - have "wfactors G (ys@zs) (y\z)" by (rule wfactors_mult) - hence "wfactors G (ys@zs) x" by (simp add: x) - - from xscarr this - show "\xs. set xs \ carrier G \ wfactors G xs x" by fast + apply (simp add: m_comm) + apply (simp add: ynunit)+ + done + with zcarr have "\as. set as \ carrier G \ wfactors G as z" + by (rule ih') + then obtain zs where zscarr: "set zs \ carrier G" and zfs: "wfactors G zs z" + by auto + + from yscarr zscarr have xscarr: "set (ys@zs) \ carrier G" + by simp + from yfs zfs ycarr zcarr yscarr zscarr have "wfactors G (ys@zs) (y\z)" + by (rule wfactors_mult) + then have "wfactors G (ys@zs) x" + by (simp add: x) + with xscarr show "\xs. set xs \ carrier G \ 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 \) as \)" shows "\i carrier G \ a divides (foldr (op \) as \) - \ (\i. i < length as \ a divides (as!i))" + have r[rule_format]: "set as \ carrier G \ a divides (foldr (op \) as \) + \ (\i. i < length as \ a divides (as!i))" apply (induct as) apply clarsimp defer 1 apply clarsimp defer 1 proof - assume "a divides \" - with carr - have "a \ Units G" - by (fast intro: divides_unit[of a \]) - with aprime - show "False" by (elim primeE, simp) + with carr have "a \ Units G" + by (fast intro: divides_unit[of a \]) + with aprime show False + by (elim primeE, simp) next fix aa as assume ih[rule_format]: "a divides foldr op \ as \ \ (\i carrier G" "set as \ carrier G" and "a divides aa \ foldr op \ as \" - with carr aprime - have "a divides aa \ a divides foldr op \ as \" - by (intro prime_divides) simp+ - moreover { + with carr aprime have "a divides aa \ a divides foldr op \ as \" + by (intro prime_divides) simp+ + then show "\ii as \" - hence "\i. i < length as \ 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 "\i. i < length as \ 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 "\iia as'. a \ carrier G \ set as \ carrier G \ set as' \ carrier G \ + "\a as'. a \ carrier G \ set as \ carrier G \ set as' \ carrier G \ wfactors G as a \ wfactors G as' a \ 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 \ 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]: "\a as'. a \ carrier G \ set as' \ carrier G \ wfactors G as a \ wfactors G as' a \ essentially_equal G as as'" and acarr: "a \ carrier G" and ahcarr: "ah \ carrier G" and ascarr: "set as \ carrier G" and as'carr: "set as' \ 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 "\a'\ carrier G. a = ah \ a'" by fast - from this obtain a' - where a'carr: "a' \ carrier G" - and a: "a = ah \ a'" + then have "\a'\ carrier G. a = ah \ a'" by fast + then obtain a' where a'carr: "a' \ carrier G" and a: "a = ah \ 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 \) as' \)" + also from afs' have "a divides (foldr (op \) as' \)" by (elim wfactorsE associatedE, simp) - finally have "ah divides (foldr (op \) as' \)" by simp - - with ahprime - have "\i) as' \)" + by simp + with ahprime have "\i carrier G" by (unfold set_conv_nth, force) + from len carr have asicarr[simp]: "as'!i \ carrier G" + unfolding set_conv_nth by force note carr = carr asicarr - from ahdvd have "\x \ carrier G. as'!i = ah \ x" by fast - from this obtain x where "x \ carrier G" and asi: "as'!i = ah \ x" by auto - - with carr irrasi[simplified asi] - have asiah: "as'!i \ ah" apply - + from ahdvd have "\x \ carrier G. as'!i = ah \ x" + by fast + then obtain x where "x \ carrier G" and asi: "as'!i = ah \ x" + by auto + with carr irrasi[simplified asi] have asiah: "as'!i \ 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 "\aa_1. aa_1 \ carrier G \ 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 \ 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 \ carrier G" and aa1fs: "wfactors G (take i as') aa_1" + by auto have "\aa_2. aa_2 \ carrier G \ 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 \ 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 \ 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 \ aa_2)" + have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \ aa_2)" by (intro wfactors_mult, simp+) - hence v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \ (aa_1 \ aa_2))" + then have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \ (aa_1 \ 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 \ 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 \ 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 \ (as'!i \ aa_2))" + have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \ (as'!i \ 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 \ (as'!i \ aa_2) \ a" - by (metis as' ee_wfactorsD m_closed) - then - have t1: "as'!i \ (aa_1 \ aa_2) \ a" + with v2 afs' carr aa1carr aa2carr nth_mem[OF len] have "aa_1 \ (as'!i \ aa_2) \ a" + by (metis as' ee_wfactorsD m_closed) + then have t1: "as'!i \ (aa_1 \ aa_2) \ a" by (metis aa1carr aa2carr asicarr m_lcomm) - from carr asiah - have "ah \ (aa_1 \ aa_2) \ as'!i \ (aa_1 \ aa_2)" + from carr asiah have "ah \ (aa_1 \ aa_2) \ as'!i \ (aa_1 \ aa_2)" by (metis associated_sym m_closed mult_cong_l) also note t1 - finally - have "ah \ (aa_1 \ aa_2) \ a" by simp - - with carr aa1carr aa2carr a'carr nth_mem[OF len] - have a': "aa_1 \ aa_2 \ a'" + finally have "ah \ (aa_1 \ aa_2) \ a" by simp + + with carr aa1carr aa2carr a'carr nth_mem[OF len] have a': "aa_1 \ aa_2 \ 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' [\] 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 \ carrier G" "set as \ carrier G" "set as' \ 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 \Application to factorial monoids\ text \Number of factors for wellfoundedness\ -definition - factorcount :: "_ \ 'a \ nat" where - "factorcount G a = - (THE c. (ALL as. set as \ carrier G \ wfactors G as a \ c = length as))" +definition factorcount :: "_ \ 'a \ nat" + where "factorcount G a = + (THE c. \as. set as \ carrier G \ wfactors G as a \ 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 \ carrier G" - shows "EX c. ALL as. set as \ carrier G \ wfactors G as a \ c = length as" + shows "\c. \as. set as \ carrier G \ wfactors G as a \ c = length as" proof - - have "\as. set as \ carrier G \ wfactors G as a" by (intro wfactors_exist, simp) - from this obtain as - where ascarr[simp]: "set as \ carrier G" - and afs: "wfactors G as a" - by (auto simp del: carr) - have "ALL as'. set as' \ carrier G \ wfactors G as' a \ length as = length as'" + have "\as. set as \ carrier G \ wfactors G as a" + by (intro wfactors_exist) simp + then obtain as where ascarr[simp]: "set as \ carrier G" and afs: "wfactors G as a" + by (auto simp del: carr) + have "\as'. set as' \ carrier G \ wfactors G as' a \ length as = length as'" by (metis afs ascarr assms ee_length wfactors_unique) - thus "EX c. ALL as'. set as' \ carrier G \ wfactors G as' a \ c = length as'" .. + then show "\c. \as'. set as' \ carrier G \ wfactors G as' a \ c = length as'" .. qed lemma (in factorial_monoid) factorcount_unique: @@ -3514,164 +3217,158 @@ and acarr[simp]: "a \ carrier G" and ascarr[simp]: "set as \ carrier G" shows "factorcount G a = length as" proof - - have "EX ac. ALL as. set as \ carrier G \ wfactors G as a \ ac = length as" by (rule factorcount_exists, simp) - from this obtain ac where - alen: "ALL as. set as \ carrier G \ wfactors G as a \ ac = length as" - by auto + have "\ac. \as. set as \ carrier G \ wfactors G as a \ ac = length as" + by (rule factorcount_exists) simp + then obtain ac where alen: "\as. set as \ carrier G \ wfactors G as a \ 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 \ carrier G" and bcarr:"b \ carrier G" - shows "factorcount G a <= factorcount G b" -apply (rule dividesE[OF dvd]) -proof - + and acarr: "a \ carrier G" + and bcarr:"b \ carrier G" + shows "factorcount G a \ factorcount G b" +proof (rule dividesE[OF dvd]) fix c - from assms - have "\as. set as \ carrier G \ wfactors G as a" by fast - from this obtain as - where ascarr: "set as \ 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 "\as. set as \ carrier G \ wfactors G as a" + by fast + then obtain as where ascarr: "set as \ 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 \ carrier G" - hence "\cs. set cs \ carrier G \ wfactors G cs c" by fast - from this obtain cs - where cscarr: "set cs \ carrier G" - and cfs: "wfactors G cs c" - by auto + then have "\cs. set cs \ carrier G \ wfactors G cs c" + by fast + then obtain cs where cscarr: "set cs \ carrier G" and cfs: "wfactors G cs c" + by auto note [simp] = acarr bcarr ccarr ascarr cscarr assume b: "b = a \ c" - from afs cfs - have "wfactors G (as@cs) (a \ 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 \ 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 \ carrier G" and bcarr:"b \ carrier G" + assumes acarr: "a \ carrier G" + and bcarr: "b \ carrier G" and asc: "a \ 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 \ carrier G" and bcarr:"b \ 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 "\as. set as \ carrier G \ wfactors G as a" by fast - from this obtain as - where ascarr: "set as \ 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 "\as. set as \ carrier G \ wfactors G as a" + by fast + then obtain as where ascarr: "set as \ 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 \ carrier G" - hence "\cs. set cs \ carrier G \ wfactors G cs c" by fast - from this obtain cs - where cscarr: "set cs \ carrier G" - and cfs: "wfactors G cs c" - by auto + then have "\cs. set cs \ carrier G \ wfactors G cs c" + by fast + then obtain cs where cscarr: "set cs \ carrier G" and cfs: "wfactors G cs c" + by auto assume b: "b = a \ c" - have "wfactors G (as@cs) (a \ 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 \ 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: "\ b divides a" have "c \ Units G" proof (rule ccontr, simp) assume cunit:"c \ Units G" - - have "b \ inv c = a \ c \ inv c" by (simp add: b) - also from ccarr acarr cunit - have "\ = a \ (c \ inv c)" by (fast intro: m_assoc) - also from ccarr cunit - have "\ = a \ \" by simp - also from acarr - have "\ = a" by simp + have "b \ inv c = a \ c \ inv c" + by (simp add: b) + also from ccarr acarr cunit have "\ = a \ (c \ inv c)" + by (fast intro: m_assoc) + also from ccarr cunit have "\ = a \ \" by simp + also from acarr have "\ = a" by simp finally have "a = b \ 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 \ 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 \ 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 \ 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 \ carrier G" "y \ carrier G" - - hence "\z. z \ carrier G \ z lcmof x y" by (rule lcmof_exists) - from this obtain z - where zcarr: "z \ 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 "\z. least (division_rel G) z (Upper (division_rel G) {x, y})" by fast + then have "\z. z \ carrier G \ z lcmof x y" + by (rule lcmof_exists) + then obtain z where zcarr: "z \ 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 "\z. least (division_rel G) z (Upper (division_rel G) {x, y})" + by fast qed qed @@ -3679,39 +3376,37 @@ subsection \Factoriality Theorems\ theorem factorial_condition_one: (* Jacobson theorem 2.21 *) - shows "(divisor_chain_condition_monoid G \ primeness_condition_monoid G) = - factorial_monoid G" -apply rule + "(divisor_chain_condition_monoid G \ 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 \ 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 \ 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 \ gcd_condition_monoid G" - by rule unfold_locales + by rule unfold_locales qed end diff -r ade7c3a20917 -r 9c22a97b7674 src/HOL/BNF_Def.thy --- a/src/HOL/BNF_Def.thy Sun Sep 11 18:12:05 2016 +0200 +++ b/src/HOL/BNF_Def.thy Sun Sep 11 18:12:16 2016 +0200 @@ -200,7 +200,7 @@ by (simp add: the_inv_f_f) lemma vimage2pI: "R (f x) (g y) \ vimage2p f g R x y" - unfolding vimage2p_def by - + unfolding vimage2p_def . lemma rel_fun_iff_leq_vimage2p: "(rel_fun R S) f g = (R \ vimage2p f g S)" unfolding rel_fun_def vimage2p_def by auto diff -r ade7c3a20917 -r 9c22a97b7674 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Sun Sep 11 18:12:05 2016 +0200 +++ b/src/HOL/Divides.thy Sun Sep 11 18:12:16 2016 +0200 @@ -1793,13 +1793,14 @@ by (rule div_int_unique) next fix a b c :: int - assume "c \ 0" - hence "\q r. divmod_int_rel a b (q, r) + assume c: "c \ 0" + have "\q r. divmod_int_rel a b (q, r) \ divmod_int_rel (c * a) (c * b) (q, c * r)" unfolding divmod_int_rel_def - by - (rule linorder_cases [of 0 b], auto simp: algebra_simps + by (rule linorder_cases [of 0 b]) + (use c in \auto simp: algebra_simps mult_less_0_iff zero_less_mult_iff mult_strict_right_mono - mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff) + mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff\) hence "divmod_int_rel (c * a) (c * b) (a div b, c * (a mod b))" using divmod_int_rel [of a b] . thus "(c * a) div (c * b) = a div b" diff -r ade7c3a20917 -r 9c22a97b7674 src/HOL/List.thy --- a/src/HOL/List.thy Sun Sep 11 18:12:05 2016 +0200 +++ b/src/HOL/List.thy Sun Sep 11 18:12:16 2016 +0200 @@ -4661,8 +4661,7 @@ from Suc have "k < card A" by simp moreover have "finite A" using assms by (simp add: card_ge_0_finite) moreover have "finite {xs. ?k_list k xs}" - using finite_lists_length_eq[OF \finite A\, of k] - by - (rule finite_subset, auto) + by (rule finite_subset) (use finite_lists_length_eq[OF \finite A\, of k] in auto) moreover have "\i j. i \ j \ {i} \ (A - set i) \ {j} \ (A - set j) = {}" by auto moreover have "\i. i \Collect (?k_list k) \ card (A - set i) = card A - k" diff -r ade7c3a20917 -r 9c22a97b7674 src/HOL/Map.thy --- a/src/HOL/Map.thy Sun Sep 11 18:12:05 2016 +0200 +++ b/src/HOL/Map.thy Sun Sep 11 18:12:16 2016 +0200 @@ -695,17 +695,23 @@ by (metis map_add_subsumed1 map_le_iff_map_add_commute) lemma dom_eq_singleton_conv: "dom f = {x} \ (\v. f = [x \ v])" -proof(rule iffI) - assume "\v. f = [x \ v]" - thus "dom f = {x}" by(auto split: if_split_asm) + (is "?lhs \ ?rhs") +proof + assume ?rhs + then show ?lhs by (auto split: if_split_asm) next - assume "dom f = {x}" - then obtain v where "f x = Some v" by auto - hence "[x \ v] \\<^sub>m f" by(auto simp add: map_le_def) - moreover have "f \\<^sub>m [x \ v]" using \dom f = {x}\ \f x = Some v\ - by(auto simp add: map_le_def) - ultimately have "f = [x \ v]" by-(rule map_le_antisym) - thus "\v. f = [x \ v]" by blast + assume ?lhs + then obtain v where v: "f x = Some v" by auto + show ?rhs + proof + show "f = [x \ v]" + proof (rule map_le_antisym) + show "[x \ v] \\<^sub>m f" + using v by (auto simp add: map_le_def) + show "f \\<^sub>m [x \ v]" + using \dom f = {x}\ \f x = Some v\ by (auto simp add: map_le_def) + qed + qed qed diff -r ade7c3a20917 -r 9c22a97b7674 src/HOL/Old_Number_Theory/Pocklington.thy --- a/src/HOL/Old_Number_Theory/Pocklington.thy Sun Sep 11 18:12:05 2016 +0200 +++ b/src/HOL/Old_Number_Theory/Pocklington.thy Sun Sep 11 18:12:16 2016 +0200 @@ -492,8 +492,8 @@ {fix m assume m: "0 < m" "m < n" "\ coprime m n" hence mS': "m \ ?S'" by auto have "insert m ?S' \ ?S" using m by auto - from m have "card (insert m ?S') \ card ?S" - by - (rule card_mono[of ?S "insert m ?S'"], auto) + have "card (insert m ?S') \ card ?S" + by (rule card_mono[of ?S "insert m ?S'"]) (use m in auto) hence False unfolding card_insert_disjoint[of "?S'" m, OF fS' mS'] ceq by simp } @@ -767,7 +767,7 @@ hence "(n - 1) mod m = 0" by auto then have mn: "m dvd n - 1" by presburger then obtain r where r: "n - 1 = m*r" unfolding dvd_def by blast - from n01 r m(2) have r01: "r\0" "r\1" by - (rule ccontr, simp)+ + from n01 r m(2) have r01: "r\0" "r\1" by auto from prime_factor[OF r01(2)] obtain p where p: "prime p" "p dvd r" by blast hence th: "prime p \ p dvd n - 1" unfolding r by (auto intro: dvd_mult) have "(a ^ ((n - 1) div p)) mod n = (a^(m*r div p)) mod n" using r @@ -800,8 +800,8 @@ moreover {assume "n\0 \ n\1" hence n2:"n \ 2" by arith from na have na': "coprime a n" by (simp add: coprime_commute) - from phi_lowerbound_1[OF n2] fermat_little[OF na'] - have ex: "\m>0. ?P m" by - (rule exI[where x="\ n"], auto) } + have ex: "\m>0. ?P m" + by (rule exI[where x="\ n"]) (use phi_lowerbound_1[OF n2] fermat_little[OF na'] in auto) } ultimately have ex: "\m>0. ?P m" by blast from nat_exists_least_iff'[of ?P] ex na show ?thesis unfolding o[symmetric] by auto @@ -992,7 +992,7 @@ from prime_factor[OF d(3)] obtain p where p: "prime p" "p dvd d" by blast from n have np: "n > 0" by arith - from d(1) n have "d \ 0" by - (rule ccontr, auto) + have "d \ 0" by (rule ccontr) (use d(1) n in auto) hence dp: "d > 0" by arith from mult_mono[OF dvd_imp_le[OF p(2) dp] dvd_imp_le[OF p(2) dp]] d(2) have "p\<^sup>2 \ n" unfolding power2_eq_square by arith @@ -1029,7 +1029,7 @@ from d dvd_mult[OF P(2), of "ord p (a^r)"] have Pq: "P dvd q" by simp from aq P(1) Pq have caP:"coprime (a^ ((n - 1) div P) - 1) n" by blast from Pq obtain s where s: "q = P*s" unfolding dvd_def by blast - have P0: "P \ 0" using P(1) prime_0 by - (rule ccontr, simp) + have P0: "P \ 0" by (rule ccontr) (use P(1) prime_0 in simp) from P(2) obtain t where t: "d = P*t" unfolding dvd_def by blast from d s t P0 have s': "ord p (a^r) * t = s" by algebra have "ord p (a^r) * t*r = r * ord p (a^r) * t" by algebra @@ -1052,8 +1052,8 @@ with divides_rexp[OF d(2)[unfolded dp], of "n - 2"] have th0: "p dvd a ^ (n - 1)" by simp from n have n0: "n \ 0" by simp - from d(2) an n12[symmetric] have a0: "a \ 0" - by - (rule ccontr, simp add: modeq_def) + have a0: "a \ 0" + by (rule ccontr) (use d(2) an n12[symmetric] in \simp add: modeq_def\) have th1: "a^ (n - 1) \ 0" using n d(2) dp a0 by auto from coprime_minus1[OF th1, unfolded coprime] dvd_trans[OF pn cong_1_divides[OF an]] th0 d(3) dp @@ -1064,7 +1064,7 @@ from fermat_little[OF arp, simplified ord_divides] o phip have "q dvd (p - 1)" by simp then obtain d where d:"p - 1 = q * d" unfolding dvd_def by blast - from prime_0 pp have p0:"p \ 0" by - (rule ccontr, auto) + have p0: "p \ 0" by (rule ccontr) (use prime_0 pp in auto) from p0 d have "p + q * 0 = 1 + q * d" by simp with nat_mod[of p 1 q, symmetric] show ?thesis by blast diff -r ade7c3a20917 -r 9c22a97b7674 src/HOL/Old_Number_Theory/Primes.thy --- a/src/HOL/Old_Number_Theory/Primes.thy Sun Sep 11 18:12:05 2016 +0200 +++ b/src/HOL/Old_Number_Theory/Primes.thy Sun Sep 11 18:12:16 2016 +0200 @@ -406,37 +406,44 @@ lemma prime_Suc0[simp]: "~ prime (Suc 0)" by (simp add: prime_def) lemma prime_ge_2: "prime p ==> p \ 2" by (simp add: prime_def) -lemma prime_factor: assumes n: "n \ 1" shows "\ p. prime p \ p dvd n" -using n -proof(induct n rule: nat_less_induct) + +lemma prime_factor: "n \ 1 \ \p. prime p \ p dvd n" +proof (induct n rule: nat_less_induct) fix n assume H: "\m 1 \ (\p. prime p \ p dvd m)" "n \ 1" - let ?ths = "\p. prime p \ p dvd n" - {assume "n=0" hence ?ths using two_is_prime by auto} - moreover - {assume nz: "n\0" - {assume "prime n" hence ?ths by - (rule exI[where x="n"], simp)} - moreover - {assume n: "\ prime n" - with nz H(2) - obtain k where k:"k dvd n" "k \ 1" "k \ n" by (auto simp add: prime_def) + show "\p. prime p \ p dvd n" + proof (cases "n = 0") + case True + with two_is_prime show ?thesis by auto + next + case nz: False + show ?thesis + proof (cases "prime n") + case True + then have "prime n \ n dvd n" by simp + then show ?thesis .. + next + case n: False + with nz H(2) obtain k where k: "k dvd n" "k \ 1" "k \ n" + by (auto simp: prime_def) from dvd_imp_le[OF k(1)] nz k(3) have kn: "k < n" by simp from H(1)[rule_format, OF kn k(2)] obtain p where p: "prime p" "p dvd k" by blast - from dvd_trans[OF p(2) k(1)] p(1) have ?ths by blast} - ultimately have ?ths by blast} - ultimately show ?ths by blast + from dvd_trans[OF p(2) k(1)] p(1) show ?thesis by blast + qed + qed qed -lemma prime_factor_lt: assumes p: "prime p" and n: "n \ 0" and npm:"n = p * m" +lemma prime_factor_lt: + assumes p: "prime p" and n: "n \ 0" and npm:"n = p * m" shows "m < n" -proof- - {assume "m=0" with n have ?thesis by simp} - moreover - {assume m: "m \ 0" - from npm have mn: "m dvd n" unfolding dvd_def by auto - from npm m have "n \ m" using p by auto - with dvd_imp_le[OF mn] n have ?thesis by simp} - ultimately show ?thesis by blast +proof (cases "m = 0") + case True + with n show ?thesis by simp +next + case m: False + from npm have mn: "m dvd n" unfolding dvd_def by auto + from npm m have "n \ m" using p by auto + with dvd_imp_le[OF mn] n show ?thesis by simp qed lemma euclid_bound: "\p. prime p \ n < p \ p <= Suc (fact n)" @@ -491,7 +498,7 @@ lemma coprime_bezout_strong: assumes ab: "coprime a b" and b: "b \ 1" shows "\x y. a * x = b * y + 1" proof- - from ab b have az: "a \ 0" by - (rule ccontr, auto) + have az: "a \ 0" by (rule ccontr) (use ab b in auto) from bezout_gcd_strong[OF az, of b] ab[unfolded coprime_def] show ?thesis by auto qed @@ -577,15 +584,15 @@ lemma distinct_prime_coprime: "prime p \ prime q \ p \ q \ coprime p q" unfolding prime_def coprime_prime_eq by blast -lemma prime_coprime_lt: assumes p: "prime p" and x: "0 < x" and xp: "x < p" +lemma prime_coprime_lt: + assumes p: "prime p" and x: "0 < x" and xp: "x < p" shows "coprime x p" -proof- - {assume c: "\ coprime x p" - then obtain g where g: "g \ 1" "g dvd x" "g dvd p" unfolding coprime_def by blast +proof (rule ccontr) + assume c: "\ ?thesis" + then obtain g where g: "g \ 1" "g dvd x" "g dvd p" unfolding coprime_def by blast from dvd_imp_le[OF g(2)] x xp have gp: "g < p" by arith - from g(2) x have "g \ 0" by - (rule ccontr, simp) - with g gp p[unfolded prime_def] have False by blast} -thus ?thesis by blast + have "g \ 0" by (rule ccontr) (use g(2) x in simp) + with g gp p[unfolded prime_def] show False by blast qed lemma prime_odd: "prime p \ p = 2 \ odd p" unfolding prime_def by auto @@ -755,28 +762,30 @@ shows "\i j. x = p ^i \ y = p^ j" using xy proof(induct k arbitrary: x y) - case 0 thus ?case apply simp by (rule exI[where x="0"], simp) + case 0 + thus ?case apply simp by (rule exI[where x="0"], simp) next case (Suc k x y) + have p0: "p \ 0" by (rule ccontr) (use p in simp) from Suc.prems have pxy: "p dvd x*y" by auto - from prime_divprod[OF p pxy] have pxyc: "p dvd x \ p dvd y" . - from p have p0: "p \ 0" by - (rule ccontr, simp) - {assume px: "p dvd x" + from prime_divprod[OF p pxy] show ?case + proof + assume px: "p dvd x" then obtain d where d: "x = p*d" unfolding dvd_def by blast from Suc.prems d have "p*d*y = p^Suc k" by simp hence th: "d*y = p^k" using p0 by simp from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "y = p^j" by blast with d have "x = p^Suc i" by simp - with ij(2) have ?case by blast} - moreover - {assume px: "p dvd y" + with ij(2) show ?thesis by blast + next + assume px: "p dvd y" then obtain d where d: "y = p*d" unfolding dvd_def by blast from Suc.prems d have "p*d*x = p^Suc k" by (simp add: mult.commute) hence th: "d*x = p^k" using p0 by simp from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast with d have "y = p^Suc i" by simp - with ij(2) have ?case by blast} - ultimately show ?case using pxyc by blast + with ij(2) show ?thesis by blast + qed qed lemma prime_power_exp: assumes p: "prime p" and n:"n \ 0" diff -r ade7c3a20917 -r 9c22a97b7674 src/HOL/Tools/BNF/bnf_comp.ML --- a/src/HOL/Tools/BNF/bnf_comp.ML Sun Sep 11 18:12:05 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Sun Sep 11 18:12:16 2016 +0200 @@ -68,8 +68,8 @@ val mk_repT: typ -> typ -> typ -> typ val mk_abs: typ -> term -> term val mk_rep: typ -> term -> term - val seal_bnf: (binding -> binding) -> unfold_set -> binding -> bool -> typ list -> BNF_Def.bnf -> - local_theory -> (BNF_Def.bnf * (typ list * absT_info)) * local_theory + val seal_bnf: (binding -> binding) -> unfold_set -> binding -> bool -> typ list -> typ list -> + BNF_Def.bnf -> local_theory -> (BNF_Def.bnf * (typ list * absT_info)) * local_theory end; structure BNF_Comp : BNF_COMP = @@ -829,13 +829,13 @@ @{thm type_definition.Abs_cases[OF type_definition_id_bnf_UNIV]})), lthy) end; -fun seal_bnf qualify (unfold_set : unfold_set) b force_out_of_line Ds bnf lthy = +fun seal_bnf qualify (unfold_set : unfold_set) b force_out_of_line Ds all_Ds bnf lthy = let val live = live_of_bnf bnf; val nwits = nwits_of_bnf bnf; val ((As, As'), lthy1) = apfst (`(map TFree)) - (Variable.invent_types (replicate live @{sort type}) (fold Variable.declare_typ Ds lthy)); + (Variable.invent_types (replicate live @{sort type}) (fold Variable.declare_typ all_Ds lthy)); val (Bs, _) = apfst (map TFree) (Variable.invent_types (replicate live @{sort type}) lthy1); val ((((fs, fs'), (Rs, Rs')), (Ps, Ps')), _(*names_lthy*)) = lthy @@ -845,10 +845,11 @@ val repTA = mk_T_of_bnf Ds As bnf; val T_bind = qualify b; - val all_TA_params_in_order = Term.add_tfreesT repTA As'; + val repTA_tfrees = Term.add_tfreesT repTA []; + val all_TA_params_in_order = fold_rev Term.add_tfreesT all_Ds As'; val TA_params = (if force_out_of_line then all_TA_params_in_order - else inter (op =) (Term.add_tfreesT repTA []) all_TA_params_in_order); + else inter (op =) repTA_tfrees all_TA_params_in_order); val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, _)), lthy) = maybe_typedef force_out_of_line (T_bind, TA_params, NoSyn) (HOLogic.mk_UNIV repTA) NONE (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy; @@ -879,7 +880,7 @@ val bd_repT = fst (dest_relT (fastype_of bnf_bd)); val bdT_bind = qualify (Binding.suffix_name ("_" ^ bdTN) b); val params = Term.add_tfreesT bd_repT []; - val all_deads = map TFree (fold Term.add_tfreesT Ds []); + val all_deads = map TFree (fold_rev Term.add_tfreesT all_Ds []); val ((bdT, (_, Abs_bd_name, _, _, Abs_bdT_inject, Abs_bdT_cases)), lthy) = maybe_typedef false (bdT_bind, params, NoSyn) (HOLogic.mk_UNIV bd_repT) NONE diff -r ade7c3a20917 -r 9c22a97b7674 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Sep 11 18:12:05 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Sep 11 18:12:16 2016 +0200 @@ -114,14 +114,14 @@ val define_ctrs_dtrs_for_type: string -> typ -> term -> term -> thm -> thm -> int -> int list -> term -> binding list -> mixfix list -> typ list list -> local_theory -> (term list list * term list * thm * thm list) * local_theory - val wrap_ctrs: BNF_Util.fp_kind -> (string -> bool) -> bool -> string -> thm -> int -> int list -> + val wrap_ctrs: (string -> bool) -> BNF_Util.fp_kind -> bool -> string -> thm -> int -> int list -> thm -> thm -> binding list -> binding list list -> term list -> term list -> thm -> thm list -> local_theory -> Ctr_Sugar.ctr_sugar * local_theory val derive_map_set_rel_pred_thms: (string -> bool) -> BNF_Util.fp_kind -> int -> typ list -> typ list -> typ -> typ -> thm list -> thm list -> thm list -> thm list -> thm list -> - thm list -> thm list -> thm list -> string -> BNF_Def.bnf -> BNF_Def.bnf list -> typ -> term -> - thm -> thm -> thm -> thm list -> thm -> thm -> thm list -> thm -> typ list list -> term -> - Ctr_Sugar.ctr_sugar -> Proof.context -> + thm list -> thm list -> thm list -> thm list -> string -> BNF_Def.bnf -> BNF_Def.bnf list -> + typ -> term -> thm -> thm -> thm -> thm list -> thm -> thm -> thm list -> thm -> + typ list list -> term -> Ctr_Sugar.ctr_sugar -> local_theory -> (thm list * thm list * thm list list * thm list * thm list * thm list * thm list * thm list * thm list * thm list * thm list list list list * thm list list list list * thm list * thm list * thm list * thm list * thm list) * local_theory @@ -660,7 +660,7 @@ ((xss, ctrs0, ctor_iff_dtor_thm, ctr_defs), lthy) end; -fun wrap_ctrs fp plugins discs_sels fp_b_name ctor_inject n ms abs_inject type_definition +fun wrap_ctrs plugins fp discs_sels fp_b_name ctor_inject n ms abs_inject type_definition disc_bindings sel_bindingss sel_default_eqs ctrs0 ctor_iff_dtor_thm ctr_defs lthy = let val sumEN_thm' = unfold_thms lthy @{thms unit_all_eq1} (mk_absumprodE type_definition ms); @@ -701,9 +701,9 @@ end; fun derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs fp_nesting_set_maps - fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps live_nesting_rel_eqs - live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor ctor_dtor dtor_ctor pre_map_def - pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm ctr_Tss abs + fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_map_ident0s live_nesting_set_maps + live_nesting_rel_eqs live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor ctor_dtor + dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm ctr_Tss abs ({casex, case_thms, discs, selss, sel_defs, ctrs, exhaust, exhaust_discs, disc_thmss, sel_thmss, injects, distincts, distinct_discsss, ...} : ctr_sugar) lthy = @@ -713,6 +713,7 @@ val ms = map length ctr_Tss; val B_ify_T = Term.typ_subst_atomic (As ~~ Bs); + val B_ify = Term.map_types B_ify_T; val fpBT = B_ify_T fpT; val live_AsBs = filter (op <>) (As ~~ Bs); @@ -735,6 +736,8 @@ val ctr_defs' = map2 (fn m => fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) ms ctr_defs; + val ABfs = live_AsBs ~~ fs; + fun derive_rel_case relAsBs rel_inject_thms rel_distinct_thms = let val rel_Rs_a_b = list_comb (relAsBs, Rs) $ ta $ tb; @@ -827,16 +830,6 @@ end; val cxIns = map2 (mk_cIn ctor) ks xss; - val cyIns = map2 (mk_cIn (Term.map_types B_ify_T ctor)) ks yss; - - fun mk_map_thm ctr_def' cxIn = - Local_Defs.fold lthy [ctr_def'] - (unfold_thms lthy (o_apply :: pre_map_def :: - (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_map @ abs_inverses) - (infer_instantiate' lthy (map (SOME o Thm.cterm_of lthy) fs @ [SOME cxIn]) - (if fp = Least_FP then fp_map_thm - else fp_map_thm RS ctor_cong RS (ctor_dtor RS sym RS trans)))) - |> singleton (Proof_Context.export names_lthy lthy); fun mk_set0_thm fp_set_thm ctr_def' cxIn = Local_Defs.fold lthy [ctr_def'] @@ -848,48 +841,114 @@ fun mk_set0_thms fp_set_thm = map2 (mk_set0_thm fp_set_thm) ctr_defs' cxIns; - val map_thms = map2 mk_map_thm ctr_defs' cxIns; val set0_thmss = map mk_set0_thms fp_set_thms; val set0_thms = flat set0_thmss; val set_thms = set0_thms |> map (unfold_thms lthy @{thms insert_is_Un[THEN sym] Un_empty_left Un_insert_left}); - val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns); - - fun mk_rel_thm postproc ctr_defs' cxIn cyIn = - Local_Defs.fold lthy ctr_defs' - (unfold_thms lthy (pre_rel_def :: abs_inverses @ - (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @ - @{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]}) - (infer_instantiate' lthy (map (SOME o Thm.cterm_of lthy) Rs @ [SOME cxIn, SOME cyIn]) - fp_rel_thm)) - |> postproc - |> singleton (Proof_Context.export names_lthy lthy); - - fun mk_rel_inject_thm ((ctr_def', cxIn), (_, cyIn)) = - mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] cxIn cyIn; - - fun mk_rel_intro_thm m thm = - uncurry_thm m (thm RS iffD2) handle THM _ => thm; - - fun mk_half_rel_distinct_thm ((xctr_def', cxIn), (yctr_def', cyIn)) = - mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def'] - cxIn cyIn; + val map_thms = + let + fun mk_goal ctrA ctrB xs ys = + let + val mapx = mk_map live As Bs (map_of_bnf fp_bnf); + val fmap = list_comb (mapx, fs); + + fun mk_arg (x as Free (_, T)) (Free (_, U)) = + if T = U then x + else build_map lthy [] (the o AList.lookup (op =) ABfs) (T, U) $ x; + + val xs' = map2 mk_arg xs ys; + in + mk_Trueprop_eq (fmap $ list_comb (ctrA, xs), list_comb (ctrB, xs')) + end; + + val goals = @{map 4} mk_goal ctrAs ctrBs xss yss; + val goal = Logic.mk_conjunction_balanced goals; + val vars = Variable.add_free_names lthy goal []; + + val fp_map_thm' = + if fp = Least_FP then fp_map_thm + else fp_map_thm RS ctor_cong RS (ctor_dtor RS sym RS trans); + in + Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => + mk_map_tac ctxt abs_inverses pre_map_def dtor_ctor fp_map_thm' + live_nesting_map_ident0s ctr_defs') + |> Thm.close_derivation + |> Conjunction.elim_balanced (length goals) + end; + + val rel_inject_thms = + let + fun mk_goal ctrA ctrB xs ys = + let + val rel = mk_rel live As Bs (rel_of_bnf fp_bnf); + val Rrel = list_comb (rel, Rs); + + val lhs = Rrel $ list_comb (ctrA, xs) $ list_comb (ctrB, ys); + val conjuncts = map2 (build_rel_app lthy Rs []) xs ys; + in + HOLogic.mk_Trueprop + (if null conjuncts then lhs + else HOLogic.mk_eq (lhs, Library.foldr1 HOLogic.mk_conj conjuncts)) + end; + + val goals = @{map 4} mk_goal ctrAs ctrBs xss yss; + val goal = Logic.mk_conjunction_balanced goals; + val vars = Variable.add_free_names lthy goal []; + in + Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => + mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel_thm live_nesting_rel_eqs + ctr_defs') + |> Thm.close_derivation + |> Conjunction.elim_balanced (length goals) + end; + + val half_rel_distinct_thmss = + let + fun mk_goal ((ctrA, xs), (ctrB, ys)) = + let + val rel = mk_rel live As Bs (rel_of_bnf fp_bnf); + val Rrel = list_comb (rel, Rs); + in + HOLogic.mk_Trueprop (HOLogic.mk_not + (Rrel $ list_comb (ctrA, xs) $ list_comb (ctrB, ys))) + end; + + val rel_infos = (ctrAs ~~ xss, ctrBs ~~ yss); + + val goalss = map (map mk_goal) (mk_half_pairss rel_infos); + val goals = flat goalss; + in + unflat goalss + (if null goals then [] + else + let + val goal = Logic.mk_conjunction_balanced goals; + val vars = Variable.add_free_names lthy goal []; + in + Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => + mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel_thm + live_nesting_rel_eqs ctr_defs') + |> Thm.close_derivation + |> Conjunction.elim_balanced (length goals) + end) + end; val rel_flip = rel_flip_of_bnf fp_bnf; fun mk_other_half_rel_distinct_thm thm = flip_rels lthy live thm RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2); - val rel_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos); - val rel_intro_thms = map2 mk_rel_intro_thm ms rel_inject_thms; - - val half_rel_distinct_thmss = map (map mk_half_rel_distinct_thm) (mk_half_pairss rel_infos); val other_half_rel_distinct_thmss = map (map mk_other_half_rel_distinct_thm) half_rel_distinct_thmss; val (rel_distinct_thms, _) = join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss; + fun mk_rel_intro_thm m thm = + uncurry_thm m (thm RS iffD2) handle THM _ => thm; + + val rel_intro_thms = map2 mk_rel_intro_thm ms rel_inject_thms; + val rel_code_thms = map (fn thm => thm RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms @ map2 (fn thm => fn 0 => thm RS @{thm eq_True[THEN iffD2]} | _ => thm) rel_inject_thms ms; @@ -983,20 +1042,19 @@ apfst flat (fold_map (fn set => fn ctxt => let val T = HOLogic.dest_setT (range_type (fastype_of set)); - val (x, ctxt') = yield_singleton (mk_Frees "x") T ctxt; - val assm = mk_Trueprop_mem (x, set $ t); + val (y, ctxt') = yield_singleton (mk_Frees "y") T ctxt; + val assm = mk_Trueprop_mem (y, set $ t); in - apfst (map (Logic.mk_implies o pair assm)) (mk_goals A setA ctr_args x ctxt') + apfst (map (Logic.mk_implies o pair assm)) (mk_goals A setA ctr_args y ctxt') end) (map (mk_set innerTs) (sets_of_bnf bnf)) ctxt)) | T => (if T = A then [mk_Trueprop_mem (t, setA $ ctr_args)] else [], ctxt)); val (goalssss, _) = fold_map (fn set => let val A = HOLogic.dest_setT (range_type (fastype_of set)) in - fold_map (fn ctr => fn ctxt => - let val (args, ctxt') = mk_Frees "a" (binder_types (fastype_of ctr)) ctxt in - fold_map (mk_goals A set (Term.list_comb (ctr, args))) args ctxt' - end) ctrAs + @{fold_map 2} (fn ctr => fn xs => + fold_map (mk_goals A set (Term.list_comb (ctr, xs))) xs) + ctrAs xss end) setAs lthy; val goals = flat (flat (flat goalssss)); in @@ -1273,7 +1331,8 @@ |> Proof_Context.export names_lthy lthy end; - val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else []; + val code_attrs = + if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else []; val anonymous_notes = [(rel_code_thms, code_attrs @ nitpicksimp_attrs)] @@ -1524,7 +1583,7 @@ ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs = let val B_ify_T = Term.typ_subst_atomic (As ~~ Bs); - val B_ify = Term.subst_atomic_types (As ~~ Bs); + val B_ify = Term.map_types B_ify_T; val fpB_Ts = map B_ify_T fpA_Ts; val ctrBs_Tsss = map (map (map B_ify_T)) ctrAs_Tsss; @@ -1704,7 +1763,8 @@ val rec_thmss = mk_rec_thmss (the rec_args_typess) recs rec_defs ctor_rec_thms; - val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else []; + val code_attrs = + if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else []; in ((induct_thms, induct_thm, mk_induct_attrs ctrss), (rec_thmss, code_attrs @ nitpicksimp_attrs @ simp_attrs)) @@ -2339,6 +2399,8 @@ liveness As Bs0; val B_ify_T = Term.typ_subst_atomic (As ~~ Bs); + val B_ify = Term.map_types B_ify_T; + val live_AsBs = filter (op <>) (As ~~ Bs); val abss = map #abs absT_infos; @@ -2399,14 +2461,15 @@ fun massage_res (ctr_sugar, maps_sets_rels) = (maps_sets_rels, (ctrs, xss, ctor_iff_dtor_thm, ctr_defs, ctr_sugar)); in - (wrap_ctrs fp plugins discs_sels fp_b_name ctor_inject n ms abs_inject type_definition + (wrap_ctrs plugins fp discs_sels fp_b_name ctor_inject n ms abs_inject type_definition disc_bindings sel_bindingss sel_default_eqs ctrs0 ctor_iff_dtor_thm ctr_defs #> (fn (ctr_sugar, lthy) => derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs - fp_nesting_set_maps fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps - live_nesting_rel_eqs live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor - ctor_dtor dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms - fp_rel_thm ctr_Tss abs ctr_sugar lthy + fp_nesting_set_maps fp_nesting_rel_eq_onps live_nesting_map_id0s + live_nesting_map_ident0s live_nesting_set_maps live_nesting_rel_eqs + live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor ctor_dtor dtor_ctor + pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm ctr_Tss abs + ctr_sugar lthy |>> pair ctr_sugar) ##>> (if fp = Least_FP then define_rec (the recs_args_types) mk_binding fpTs Cs reps @@ -2426,13 +2489,13 @@ fun mk_co_rec_transfer_goals lthy co_recs = let - val B_ify = Term.subst_atomic_types (live_AsBs @ (Cs ~~ Es)); + val BE_ify = Term.subst_atomic_types (live_AsBs @ (Cs ~~ Es)); val ((Rs, Ss), names_lthy) = lthy |> mk_Frees "R" (map (uncurry mk_pred2T) live_AsBs) ||>> mk_Frees "S" (map2 mk_pred2T Cs Es); - val co_recBs = map B_ify co_recs; + val co_recBs = map BE_ify co_recs; in (Rs, Ss, map2 (mk_parametricity_goal lthy (Rs @ Ss)) co_recs co_recBs, names_lthy) end; @@ -2468,8 +2531,6 @@ val rec_arg_Ts = binder_fun_types (hd (map fastype_of recs)); - val B_ify_T = Term.typ_subst_atomic (As ~~ Bs); - val num_rec_args = length rec_arg_Ts; val g_Ts = map B_ify_T rec_arg_Ts; val g_names = variant_names num_rec_args "g"; @@ -2621,9 +2682,6 @@ val corec_arg_Ts = binder_fun_types (hd (map fastype_of corecs)); - val B_ify = Term.subst_atomic_types (As ~~ Bs); - val B_ify_T = Term.typ_subst_atomic (As ~~ Bs); - val num_rec_args = length corec_arg_Ts; val g_names = variant_names num_rec_args "g"; val gs = map2 (curry Free) g_names corec_arg_Ts; diff -r ade7c3a20917 -r 9c22a97b7674 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sun Sep 11 18:12:05 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sun Sep 11 18:12:16 2016 +0200 @@ -8,10 +8,9 @@ signature BNF_FP_DEF_SUGAR_TACTICS = sig - val sumprod_thms_map: thm list + val sumprod_thms_rel: thm list val sumprod_thms_set: thm list val basic_sumprod_thms_set: thm list - val sumprod_thms_rel: thm list val mk_case_transfer_tac: Proof.context -> thm -> thm list -> tactic val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list -> @@ -33,6 +32,7 @@ val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list -> thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic + val mk_map_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> thm list -> tactic val mk_map_disc_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic val mk_map_sel_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> thm list -> tactic @@ -40,6 +40,7 @@ tactic val mk_rec_transfer_tac: Proof.context -> int -> int list -> cterm list -> cterm list -> term list list list list -> thm list -> thm list -> thm list -> thm list -> tactic + val mk_rel_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> thm list -> tactic val mk_rel_case_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> thm list -> thm list -> thm list -> tactic val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list -> @@ -75,15 +76,15 @@ val simp_thms' = @{thms simp_thms(6,7,8,11,12,15,16,22,24)}; val sumprod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps}; +val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_inject prod.inject id_apply conj_assoc}; val basic_sumprod_thms_set = @{thms UN_empty UN_insert UN_iff Un_empty_left Un_empty_right Un_iff Union_Un_distrib - o_apply map_prod_simp mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps}; + o_apply map_prod_simp mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps}; val sumprod_thms_set = @{thms UN_simps(10) image_iff} @ basic_sumprod_thms_set; -val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_inject prod.inject id_apply conj_assoc}; fun is_def_looping def = (case Thm.prop_of def of - Const (@{const_name Pure.eq}, _) $ lhs $ rhs => Term.exists_subterm (curry (op =) lhs) rhs + Const (@{const_name Pure.eq}, _) $ lhs $ rhs => Term.exists_subterm (curry (op aconv) lhs) rhs | _ => false); fun hhf_concl_conv cv ctxt ct = @@ -389,6 +390,13 @@ (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss selsss)); +fun mk_map_tac ctxt abs_inverses pre_map_def dtor_ctor fp_map' live_nesting_map_ident0s ctr_defs' = + TRYALL Goal.conjunction_tac THEN + unfold_thms_tac ctxt (pre_map_def :: dtor_ctor :: fp_map' :: abs_inverses @ + live_nesting_map_ident0s @ + ctr_defs' @ sumprod_thms_map @ @{thms o_def[abs_def] id_def}) THEN + ALLGOALS (rtac ctxt refl); + fun mk_map_disc_iff_tac ctxt ct exhaust discs maps = TRYALL Goal.conjunction_tac THEN ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW @@ -400,13 +408,20 @@ fun mk_map_sel_tac ctxt ct exhaust discs maps sels map_id0s = TRYALL Goal.conjunction_tac THEN - ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW - REPEAT_DETERM o hyp_subst_tac ctxt) THEN - unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ - @{thms not_True_eq_False not_False_eq_True}) THEN - TRYALL (etac ctxt FalseE ORELSE' etac ctxt @{thm TrueE}) THEN - unfold_thms_tac ctxt (@{thm id_apply} :: maps @ sels @ map_id0s) THEN - ALLGOALS (rtac ctxt refl); + ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW + REPEAT_DETERM o hyp_subst_tac ctxt) THEN + unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ + @{thms not_True_eq_False not_False_eq_True}) THEN + TRYALL (etac ctxt FalseE ORELSE' etac ctxt @{thm TrueE}) THEN + unfold_thms_tac ctxt (@{thm id_apply} :: maps @ sels @ map_id0s) THEN + ALLGOALS (rtac ctxt refl); + +fun mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel live_nesting_rel_eqs ctr_defs' = + TRYALL Goal.conjunction_tac THEN + unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: fp_rel :: abs_inverses @ live_nesting_rel_eqs @ + ctr_defs' @ sumprod_thms_rel @ @{thms vimage2p_def o_apply sum.inject + sum.distinct(1)[THEN eq_False[THEN iffD2]] not_False_eq_True}) THEN + ALLGOALS (resolve_tac ctxt [TrueI, refl]); fun mk_rel_case_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs = HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct1] exhaust) THEN_ALL_NEW @@ -477,16 +492,16 @@ fun mk_set_sel_tac ctxt ct exhaust discs sels sets = TRYALL Goal.conjunction_tac THEN - ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW - REPEAT_DETERM o hyp_subst_tac ctxt) THEN - unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ - @{thms not_True_eq_False not_False_eq_True}) THEN - TRYALL (etac ctxt FalseE ORELSE' etac ctxt @{thm TrueE}) THEN - unfold_thms_tac ctxt (sels @ sets) THEN - ALLGOALS (REPEAT o (resolve_tac ctxt @{thms UnI1 UnI2 imageI} ORELSE' - eresolve_tac ctxt @{thms UN_I UN_I[rotated] imageE} ORELSE' - hyp_subst_tac ctxt) THEN' - (rtac ctxt @{thm singletonI} ORELSE' assume_tac ctxt)); + ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW + REPEAT_DETERM o hyp_subst_tac ctxt) THEN + unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ + @{thms not_True_eq_False not_False_eq_True}) THEN + TRYALL (etac ctxt FalseE ORELSE' etac ctxt @{thm TrueE}) THEN + unfold_thms_tac ctxt (sels @ sets) THEN + ALLGOALS (REPEAT o (resolve_tac ctxt @{thms UnI1 UnI2 imageI} ORELSE' + eresolve_tac ctxt @{thms UN_I UN_I[rotated] imageE} ORELSE' + hyp_subst_tac ctxt) THEN' + (rtac ctxt @{thm singletonI} ORELSE' assume_tac ctxt)); fun mk_set_cases_tac ctxt ct assms exhaust sets = HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) diff -r ade7c3a20917 -r 9c22a97b7674 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Sun Sep 11 18:12:05 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Sun Sep 11 18:12:16 2016 +0200 @@ -957,10 +957,12 @@ val timer = time (timer "Construction of BNFs"); - val ((kill_poss, _), (bnfs', ((comp_cache', unfold_set'), lthy''))) = + val ((kill_posss, _), (bnfs', ((comp_cache', unfold_set'), lthy''))) = normalize_bnfs norm_qualify Ass Ds (K (resBs' @ Xs)) bnfs (comp_cache_unfold_set, lthy'); - val Dss = @{map 3} (uncurry append oo curry swap oo map o nth) livess kill_poss deadss; + val Dss = @{map 3} (fn lives => fn kill_posss => fn deads => deads @ map (nth lives) kill_posss) + livess kill_posss deadss; + val all_Dss = Dss |> force_out_of_line ? map (fn Ds' => union (op =) Ds' (map TFree Ds0)); fun pre_qualify b = Binding.qualify false (Binding.name_of b) @@ -968,8 +970,9 @@ #> not (Config.get lthy'' bnf_internals) ? Binding.concealed; val ((pre_bnfs, (deadss, absT_infos)), lthy''') = lthy'' - |> @{fold_map 4} (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b)) - bs (replicate (length rhsXs) (force_out_of_line orelse not (null live_phantoms))) Dss bnfs' + |> @{fold_map 5} (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b)) + bs (replicate (length rhsXs) (force_out_of_line orelse not (null live_phantoms))) Dss + all_Dss bnfs' |>> split_list |>> apsnd split_list; diff -r ade7c3a20917 -r 9c22a97b7674 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Sun Sep 11 18:12:05 2016 +0200 +++ b/src/HOL/Transcendental.thy Sun Sep 11 18:12:16 2016 +0200 @@ -205,7 +205,7 @@ also have "card {0<..<2*n} \ 2*n - 1" by (cases n) simp_all also have "(2 * n - 1) * (2 * n choose n) + (2 * n choose n) = ((2*n) choose n) * (2*n)" using assms by (simp add: algebra_simps) - finally have "4 ^ n \ (2 * n choose n) * (2 * n)" by - simp_all + finally have "4 ^ n \ (2 * n choose n) * (2 * n)" by simp_all hence "real (4 ^ n) \ real ((2 * n choose n) * (2 * n))" by (subst of_nat_le_iff) with assms show ?thesis by (simp add: field_simps)