Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: convergence_top.pvs Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Algebra/Divisibility.thy
    Author:     Clemens Ballarin
    Author:     Stephan Hohe
*)

section \<open>Divisibility in monoids and rings\<close>

theory Divisibility
  imports "HOL-Library.Permutation" Coset Group
begin

section \<open>Factorial Monoids\<close>

subsection \<open>Monoids with Cancellation Law\<close>

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"

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"
  shows "monoid_cancel G"
    by standard fact+

lemma (in monoid_cancel) is_monoid_cancel: "monoid_cancel G" ..

sublocale group \<subseteq> monoid_cancel
  by standard simp_all

locale comm_monoid_cancel = monoid_cancel + comm_monoid

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"
  shows "comm_monoid_cancel G"
proof -
  interpret comm_monoid G by fact
  show "comm_monoid_cancel G"
    by unfold_locales (metis assms(2) m_ac(2))+
qed

lemma (in comm_monoid_cancel) is_comm_monoid_cancel: "comm_monoid_cancel G"
  by intro_locales

sublocale comm_group \<subseteq> comm_monoid_cancel ..

subsection \<open>Products of Units in Monoids\<close>

lemma (in monoid) prod_unit_l:
  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)
  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)
  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 (auto simp: Units_def)
qed

lemma (in monoid) prod_unit_r:
  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 -
  have c: "b \ inv (a \ b) \ carrier G" by simp

  have "a \ (b \ inv (a \ b)) = (a \ b) \ inv (a \ b)"
    by (simp add: m_assoc del: Units_r_inv)
  also have "\ = \" by simp
  finally have li: "a \ (b \ inv (a \ b)) = \" .

  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: 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 (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]
proof clarsimp
  fix i
  assume [simp]: "i \ carrier G"

  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 assume "i \ (a \ b) = \"
  finally have li': "(b \ i) \ a = \" .

  have "a \ (b \ i) = a \ b \ i" by (simp add: m_assoc)
  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)
qed

subsection \<open>Divisibility and Association\<close>

subsubsection \<open>Function definitions\<close>

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)
  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 = (\\<^bsub>G\<^esub>), le = (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"
  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 \<notin> Units G \<and>
    (\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. p divides\<^bsub>G\<^esub> (a \<otimes>\<^bsub>G\<^esub> b) \<longrightarrow> p divides\<^bsub>G\<^esub> a \<or> p divides\<^bsub>G\<^esub> b)"

subsubsection \<open>Divisibility\<close>

lemma dividesI:
  fixes G (structure)
  assumes carr: "c \ carrier G"
    and p: "b = a \ c"
  shows "a divides b"
  unfolding factor_def using assms by fast

lemma dividesI' [intro]:
  fixes G (structure)
  assumes p: "b = a \ c"
    and carr: "c \ carrier G"
  shows "a divides b"
  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

lemma dividesE [elim]:
  fixes G (structure)
  assumes d: "a divides b"
    and elim: "\c. \b = a \ c; c \ carrier G\ \ P"
  shows "P"
proof -
  from dividesD[OF d] 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"
  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)

lemma (in monoid) divides_mult_lI [intro]:
  assumes  "a divides b" "a \ carrier G" "c \ carrier G"
  shows "(c \ a) divides (c \ b)"
  by (metis assms factor_def m_assoc)

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"
proof
  show "c \ a divides c \ b \ a divides b"
    using carr monoid.m_assoc monoid_axioms monoid_cancel.l_cancel monoid_cancel_axioms by fastforce
  show "a divides b \ c \ a divides c \ b"
  using carr(1) carr(3) by blast
qed

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 by (metis divides_mult_lI m_comm)

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])

lemma (in monoid) divides_prod_r:
  assumes ab: "a divides b"
    and carr: "a \ carrier G" "c \ carrier G"
  shows "a divides (b \ c)"
  using ab carr by (fast intro: m_assoc)

lemma (in comm_monoid) divides_prod_l:
  assumes "a \ carrier G" "b \ carrier G" "c \ carrier G" "a divides b"
  shows "a divides (c \ b)"
  using assms  by (simp add: divides_prod_r m_comm)

lemma (in monoid) unit_divides:
  assumes uunit: "u \ Units 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])
  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)" ..
qed

lemma (in comm_monoid) divides_unit:
  assumes udvd: "a divides u"
    and  carr: "a \ carrier G" "u \ Units G"
  shows "a \ Units G"
  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)

subsubsection \<open>Association\<close>

lemma associatedI:
  fixes G (structure)
  assumes "a divides b" "b divides a"
  shows "a \ b"
  using assms by (simp add: associated_def)

lemma (in monoid) associatedI2:
  assumes uunit[simp]: "u \ Units G"
    and a: "a = b \ u"
    and bcarr: "b \ carrier G"
  shows "a \ b"
  using uunit bcarr
  unfolding a
  apply (intro associatedI)
  apply (metis Units_closed divides_mult_lI one_closed r_one unit_divides)
  by blast

lemma (in monoid) associatedI2':
  assumes "a = b \ u"
    and "u \ Units G"
    and "b \ carrier G"
  shows "a \ b"
  using assms by (intro associatedI2)

lemma associatedD:
  fixes G (structure)
  assumes "a \ b"
  shows "a divides b"
  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
proof clarify
  assume "b divides a"
  then obtain u where ucarr: "u \ carrier G" and a: "a = b \ u"
    by (rule dividesE)

  assume "a divides b"
  then obtain u' where u'carr: "u' \ carrier G" and b: "b = a \ u'"
    by (rule dividesE)
  note carr = carr ucarr u'carr

  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 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
  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:
  fixes G (structure)
  assumes assoc: "a \ b"
    and e: "\a divides b; b divides a\ \ P"
  shows "P"
proof -
  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:
  assumes assoc: "a \ b"
    and e: "\u. \a = b \ u; u \ Units G\ \ P"
    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)
  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)

lemma (in monoid) associated_sym [sym]:
  assumes "a \ b"
  shows "b \ a"
  using assms by (iprover intro: associatedI elim: associatedE)

lemma (in monoid) associated_trans [trans]:
  assumes "a \ b" "b \ c"
    and "a \ 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)"
  apply unfold_locales
    apply simp_all
   apply (metis associated_def)
  apply (iprover intro: associated_trans)
  done

subsubsection \<open>Division and associativity\<close>

lemmas divides_antisym = associatedI

lemma (in monoid) divides_cong_l [trans]:
  assumes "x \ x'" "x' divides y" "x \ carrier G"
  shows "x divides y"
  by (meson assms associatedD divides_trans)

lemma (in monoid) divides_cong_r [trans]:
  assumes "x divides y" "y \ y'" "x \ carrier G"
  shows "x divides y'"
  by (meson assms associatedD divides_trans)

lemma (in monoid) division_weak_partial_order [simp, intro!]:
  "weak_partial_order (division_rel G)"
  apply unfold_locales
      apply (simp_all add: associated_sym divides_antisym)
     apply (metis associated_trans)
   apply (metis divides_trans)
  by (meson associated_def divides_trans)

subsubsection \<open>Multiplication and associativity\<close>

lemma (in monoid) mult_cong_r:
  assumes "b \ b'" "a \ carrier G" "b \ carrier G" "b' \ carrier G"
  shows "a \ b \ a \ b'"
  by (meson assms associated_def divides_mult_lI)

lemma (in comm_monoid) mult_cong_l:
  assumes "a \ a'" "a \ carrier G" "a' \ carrier G" "b \ carrier G"
  shows "a \ b \ a' \ b"
  using assms m_comm mult_cong_r by auto

lemma (in monoid_cancel) assoc_l_cancel:
  assumes "a \ carrier G" "b \ carrier G" "b' \ carrier G" "a \ b \ a \ b'"
  shows "b \ b'"
  by (meson assms associated_def divides_mult_l)

lemma (in comm_monoid_cancel) assoc_r_cancel:
  assumes "a \ b \ a' \ b" "a \ carrier G" "a' \ carrier G" "b \ carrier G"
  shows "a \ a'"
  using assms assoc_l_cancel m_comm by presburger

subsubsection \<open>Units\<close>

lemma (in monoid_cancel) assoc_unit_l [trans]:
  assumes "a \ b"
    and "b \ Units G"
    and "a \ carrier G"
  shows "a \ Units G"
  using assms by (fast elim: associatedE2)

lemma (in monoid_cancel) assoc_unit_r [trans]:
  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)

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)

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> {\}"
proof -
  have "a .\\<^bsub>division_rel G\<^esub> {\}" if "a \ Units G" for a
  proof -
    have "a \ \"
      by (rule associatedI) (simp_all add: Units_closed that unit_divides)
    then show ?thesis
      by (simp add: elem_def)
  qed
  moreover have "\ .\\<^bsub>division_rel G\<^esub> Units G"
    by (simp add: equivalence.mem_imp_elem)
  ultimately show ?thesis
    by (auto simp: set_eq_def)
qed

lemma (in comm_monoid) Units_Lower: "Units G = Lower (division_rel G) (carrier G)"
  apply (auto simp add: Units_def Lower_def)
   apply (metis Units_one_closed unit_divides unit_factor)
  apply (metis Unit_eq_dividesone Units_r_inv_ex m_ac(2) one_closed)
  done

lemma (in monoid_cancel) associated_iff:
  assumes "a \ carrier G" "b \ carrier G"
  shows "a \ b \ (\c \ Units G. a = b \ c)"
  using assms associatedI2' associatedD2 by auto

subsubsection \<open>Proper factors\<close>

lemma properfactorI:
  fixes G (structure)
  assumes "a divides b"
    and "\(b divides a)"
  shows "properfactor G a b"
  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"
proof (rule properfactorI, rule advdb, rule notI)
  assume "b divides a"
  with advdb have "a \ b" by (rule associatedI)
  with neq show "False" by fast
qed

lemma (in comm_monoid_cancel) properfactorI3:
  assumes p: "p = a \ b"
    and nunit: "b \ Units G"
    and carr: "a \ carrier G" "b \ carrier G"
  shows "properfactor G a p"
  unfolding p
  using carr
  apply (intro properfactorI, fast)
proof (clarsimp, elim dividesE)
  fix c
  assume ccarr: "c \ carrier G"
  note [simp] = carr ccarr

  have "a \ \ = a" by simp
  also assume "a = a \ b \ c"
  also have "\ = a \ (b \ c)" by (simp add: m_assoc)
  finally have "a \ \ = a \ (b \ c)" .

  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 ..
qed

lemma properfactorE:
  fixes G (structure)
  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)

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)

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)

lemma (in monoid) properfactor_divides:
  assumes pf: "properfactor G a b"
  shows "a divides b"
  using pf by (elim properfactorE)

lemma (in monoid) properfactor_trans1 [trans]:
  assumes "a divides b"  "properfactor G b c" "a \ carrier G" "c \ carrier G"
  shows "properfactor G a c"
  by (meson divides_trans properfactorE properfactorI assms)

lemma (in monoid) properfactor_trans2 [trans]:
  assumes "properfactor G a b"  "b divides c" "a \ carrier G" "b \ carrier G"
  shows "properfactor G a c"
  by (meson divides_trans properfactorE properfactorI assms)

lemma properfactor_lless:
  fixes G (structure)
  shows "properfactor G = lless (division_rel G)"
  by (force simp: lless_def properfactor_def associated_def)

lemma (in monoid) properfactor_cong_l [trans]:
  assumes x'x: "x' \<sim> 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
proof -
  interpret weak_partial_order "division_rel G" ..
  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)
qed

lemma (in monoid) properfactor_cong_r [trans]:
  assumes pf: "properfactor G x y"
    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
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)
qed

lemma (in monoid_cancel) properfactor_mult_lI [intro]:
  assumes ab: "properfactor G a b"
    and carr: "a \ carrier G" "c \ carrier G"
  shows "properfactor G (c \ a) (c \ b)"
  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)

lemma (in comm_monoid_cancel) properfactor_mult_rI [intro]:
  assumes ab: "properfactor G a b"
    and carr: "a \ carrier G" "c \ carrier G"
  shows "properfactor G (a \ c) (b \ c)"
  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)

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_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_all

subsection \<open>Irreducible Elements and Primes\<close>

subsubsection \<open>Irreducible elements\<close>

lemma irreducibleI:
  fixes G (structure)
  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

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"
  shows "P"
  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"
  shows "b \ Units G"
  using assms by (fast elim: irreducibleE)

lemma (in monoid_cancel) irreducible_cong [trans]:
  assumes "irreducible G a" "a \ a'" "a \ carrier G" "a' \ carrier G"
  shows "irreducible G a'"
proof -
  have "a' divides a"
    by (meson \<open>a \<sim> a'\<close> associated_def)
  then show ?thesis
    by (metis (no_types) assms assoc_unit_l irreducibleE irreducibleI monoid.properfactor_trans2 monoid_axioms)
qed

lemma (in monoid) irreducible_prod_rI:
  assumes "irreducible G a" "b \ Units G" "a \ carrier G" "b \ carrier G"
  shows "irreducible G (a \ b)"
  using assms
  by (metis (no_types, lifting) associatedI2' irreducible_def monoid.m_closed monoid_axioms prod_unit_r properfactor_cong_r)

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)"
  by (metis aunit birr carr irreducible_prod_rI m_comm)

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
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
  proof (cases "a \ Units G")
    case aunit: True
    have "irreducible G b"
    proof (rule irreducibleI, rule notI)
      assume "b \ Units G"
      with aunit have "(a \ b) \ Units G" by fast
      with abnunit show "False" ..
    next
      fix c
      assume ccarr: "c \ carrier G"
        and "properfactor G c b"
      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
    with aunit show "P" by (rule e2)
  next
    case anunit: False
    with carr have "properfactor G b (b \ a)" by (fast intro: properfactorI3)
    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"
    proof (rule irreducibleI, rule notI)
      assume "a \ Units G"
      with bunit have "(a \ b) \ Units G" by fast
      with abnunit show "False" ..
    next
      fix c
      assume ccarr: "c \ carrier G"
        and "properfactor G c a"
      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

lemma divides_irreducible_condition:
  assumes "irreducible G r" and "a \ carrier G"
  shows "a divides\<^bsub>G\<^esub> r \ a \ Units G \ a \\<^bsub>G\<^esub> r"
  using assms unfolding irreducible_def properfactor_def associated_def
  by (cases "r divides\<^bsub>G\<^esub> a", auto)

subsubsection \<open>Prime elements\<close>

lemma primeI:
  fixes G (structure)
  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

lemma primeE:
  fixes G (structure)
  assumes pprime: "prime G p"
    and e: "\p \ Units G; \a\carrier G. \b\carrier G.
      p divides a \<otimes> b \<longrightarrow> p divides a \<or> p divides b\<rbrakk> \<Longrightarrow> P"
  shows "P"
  using pprime unfolding prime_def by (blast dest: e)

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)

lemma (in monoid_cancel) prime_cong [trans]:
  assumes "prime G p"
    and pp': "p \ p'" "p \ carrier G" "p' \ carrier G"
  shows "prime G p'"
  using assms
  by (auto simp: prime_def assoc_unit_l) (metis pp' associated_sym divides_cong_l)

lemma (in comm_monoid_cancel) prime_irreducible: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  assumes "prime G p"
  shows "irreducible G p"
proof (rule irreducibleI)
  show "p \ Units G"
    using assms unfolding prime_def by simp
next
  fix b assume A: "b \ carrier G" "properfactor G b p"
  then obtain c where c: "c \ carrier G" "p = b \ c"
    unfolding properfactor_def factor_def by auto
  hence "p divides c"
    using A assms unfolding prime_def properfactor_def by auto
  then obtain b' where b': "b' \ carrier G" "c = p \ b'"
    unfolding factor_def by auto
  hence "\ = b \ b'"
    by (metis A(1) l_cancel m_closed m_lcomm one_closed r_one c)
  thus "b \ Units G"
    using A(1) Units_one_closed b'(1) unit_factor by presburger
qed

lemma (in comm_monoid_cancel) prime_pow_divides_iff:
  assumes "p \ carrier G" "a \ carrier G" "b \ carrier G" and "prime G p" and "\ (p divides a)"
  shows "(p [^] (n :: nat)) divides (a \ b) \ (p [^] n) divides b"
proof
  assume "(p [^] n) divides b" thus "(p [^] n) divides (a \ b)"
    using divides_prod_l[of "p [^] n" b a] assms by simp
next
  assume "(p [^] n) divides (a \ b)" thus "(p [^] n) divides b"
  proof (induction n)
    case 0 with \<open>b \<in> carrier G\<close> show ?case
      by (simp add: unit_divides)
  next
    case (Suc n)
    hence "(p [^] n) divides (a \ b)" and "(p [^] n) divides b"
      using assms(1) divides_prod_r by auto
    with \<open>(p [^] (Suc n)) divides (a \<otimes> b)\<close> obtain c d
      where c: "c \ carrier G" and "b = (p [^] n) \ c"
        and d: "d \ carrier G" and "a \ b = (p [^] (Suc n)) \ d"
      using assms by blast
    hence "(p [^] n) \ (a \ c) = (p [^] n) \ (p \ d)"
      using assms by (simp add: m_assoc m_lcomm)
    hence "a \ c = p \ d"
      using c d assms(1) assms(2) l_cancel by blast
    with \<open>\<not> (p divides a)\<close> and \<open>prime G p\<close> have "p divides c"
      by (metis assms(2) c d dividesI' prime_divides)
    with \<open>b = (p [^] n) \<otimes> c\<close> show ?case
      using assms(1) c by simp
  qed
qed

subsection \<open>Factorization and Factorial Monoids\<close>

subsubsection \<open>Function definitions\<close>

definition factors :: "[_, 'a list, 'a] \ bool"
  where "factors G fs a \ (\x \ (set fs). irreducible G x) \ foldr (\\<^bsub>G\<^esub>) fs \\<^bsub>G\<^esub> = a"

definition wfactors ::"[_, 'a list, 'a] \ bool"
  where "wfactors G fs a \ (\x \ (set fs). irreducible G x) \ foldr (\\<^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 (\\<^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 \<subseteq> carrier G; set fs' \<subseteq> carrier G\<rbrakk> \<Longrightarrow> essentially_equal G fs fs'"

subsubsection \<open>Comparing lists of elements\<close>

text \<open>Association on lists\<close>

lemma (in monoid) listassoc_refl [simp, intro]:
  assumes "set as \ carrier G"
  shows "as [\] as"
  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"
  shows "bs [\] as"
  using assms
proof (induction as arbitrary: bs)
  case Cons
  then show ?case
    by (induction bs) (use associated_sym in auto)
qed auto

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)
  by (metis (mono_tags, lifting) associated_trans nth_mem subsetCE)

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
  by (fastforce simp add: list_all2_conv_all_nth set_conv_nth intro: irreducible_cong)

text \<open>Permutations\<close>

lemma perm_map [intro]:
  assumes p: "a <~~> b"
  shows "map f a <~~> map f b"
  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)

lemma (in monoid) perm_assoc_switch:
  assumes a:"as [\] bs" and p: "bs <~~> cs"
  shows "\bs'. as <~~> bs' \ bs' [\] cs"
  using p a
proof (induction bs cs arbitrary: as)
  case (swap y x l)
  then show ?case
    by (metis (no_types, hide_lams) list_all2_Cons2 perm.swap)
next
case (Cons xs ys z)
  then show ?case
    by (metis list_all2_Cons2 perm.Cons)
next
  case (trans xs ys zs)
  then show ?case
    by (meson perm.trans)
qed auto

lemma (in monoid) perm_assoc_switch_r:
  assumes p: "as <~~> bs" and a:"bs [\] cs"
  shows "\bs'. as [\] bs' \ bs' <~~> cs"
  using p a
proof (induction as bs arbitrary: cs)
  case Nil
  then show ?case
    by auto
next
  case (swap y x l)
  then show ?case
    by (metis (no_types, hide_lams) list_all2_Cons1 perm.swap)
next
  case (Cons xs ys z)
  then show ?case
    by (metis list_all2_Cons1 perm.Cons)
next
  case (trans xs ys zs)
  then show ?case
    by (blast intro:  elim: )
qed

declare perm_sym [sym]

lemma perm_setP:
  assumes perm: "as <~~> bs"
    and as: "P (set as)"
  shows "P (set bs)"
proof -
  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"]

text \<open>Essentially equal factorizations\<close>

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

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)

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)

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
proof (elim essentially_equalE)
  fix fs
  assume "as <~~> fs"  "fs [\] bs"
  from perm_assoc_switch_r [OF this] obtain fs' where a: "as [\] fs'" and p: "fs' <~~> bs"
    by blast
  from p have "bs <~~> fs'" by (rule perm_sym)
  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 bscarr: "set bs \ carrier G"
    and cscarr: "set cs \ carrier G"
  shows "essentially_equal G as cs"
  using ab bc
proof (elim essentially_equalE)
  fix abs bcs
  assume "abs [\] bs" and pb: "bs <~~> bcs"
  from perm_assoc_switch [OF this] obtain bs' where p: "abs <~~> bs'" and a: "bs' [\] bcs"
    by blast
  assume "as <~~> abs"
  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)
  assume "bcs [\] cs"
  then have "bs' [\] cs"
    using a c1 c2 cscarr listassoc_trans by blast
  with pp show ?thesis
    by (rule essentially_equalI)
qed

subsubsection \<open>Properties of lists of elements\<close>

text \<open>Multiplication of factors in a list\<close>

lemma (in monoid) multlist_closed [simp, intro]:
  assumes ascarr: "set fs \ carrier G"
  shows "foldr (\) fs \ \ carrier G"
  using ascarr by (induct fs) simp_all

lemma  (in comm_monoid) multlist_dividesI:
  assumes "f \ set fs" and "set fs \ carrier G"
  shows "f divides (foldr (\) fs \)"
  using assms
proof (induction fs)
  case (Cons a fs)
  then have f: "f \ carrier G"
    by blast
  show ?case
    using Cons.IH Cons.prems(1) Cons.prems(2) divides_prod_l f by auto
qed auto

lemma (in comm_monoid_cancel) multlist_listassoc_cong:
  assumes "fs [\] fs'"
    and "set fs \ carrier G" and "set fs' \ carrier G"
  shows "foldr (\) fs \ \ foldr (\) fs' \"
  using assms
proof (induct fs arbitrary: fs')
  case (Cons a as fs')
  then show ?case
  proof (induction fs')
    case (Cons b bs)
    then have p: "a \ foldr (\) as \ \ b \ foldr (\) as \"
      by (simp add: mult_cong_l)
    then have "foldr (\) as \ \ foldr (\) bs \"
      using Cons by auto
    with Cons have "b \ foldr (\) as \ \ b \ foldr (\) bs \"
      by (simp add: mult_cong_r)
    then show ?case
      using Cons.prems(3) Cons.prems(4) monoid.associated_trans monoid_axioms p by force
  qed auto
qed auto

lemma (in comm_monoid) multlist_perm_cong:
  assumes prm: "as <~~> bs"
    and ascarr: "set as \ carrier G"
  shows "foldr (\) as \ = foldr (\) bs \"
  using prm ascarr
proof induction
  case (swap y x l) then show ?case
    by (simp add: m_lcomm)
next
  case (trans xs ys zs) then show ?case
    using perm_closed by auto
qed auto

lemma (in comm_monoid_cancel) multlist_ee_cong:
  assumes "essentially_equal G fs fs'"
    and "set fs \ carrier G" and "set fs' \ carrier G"
  shows "foldr (\) fs \ \ foldr (\) fs' \"
  using assms
  by (metis essentially_equal_def multlist_listassoc_cong multlist_perm_cong perm_closed)

subsubsection \<open>Factorization in irreducible elements\<close>

lemma wfactorsI:
  fixes G (structure)
  assumes "\f\set fs. irreducible G f"
    and "foldr (\) fs \ \ a"
  shows "wfactors G fs a"
  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 (\) fs \ \ a\ \ P"
  shows "P"
  using wf unfolding wfactors_def by (fast dest: e)

lemma (in monoid) factorsI:
  assumes "\f\set fs. irreducible G f"
    and "foldr (\) fs \ = a"
  shows "factors G fs a"
  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 (\) fs \ = a\ \ P"
  shows "P"
  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)

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)

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)

lemma (in monoid) nunit_factors:
  assumes anunit: "a \ Units G"
    and fs: "factors G as a"
  shows "length as > 0"
proof -
  from anunit Units_one_closed have "a \ \" by auto
  with fs show ?thesis by (auto elim: factorsE)
qed

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)

lemma (in comm_monoid_cancel) unit_wfactors_empty:
  assumes aunit: "a \ Units G"
    and wf: "wfactors G fs a"
    and carr[simp]: "set fs \ carrier G"
  shows "fs = []"
proof (cases fs)
  case fs: (Cons f fs')
  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 (\) fs' \ \ a" by (simp add: wfactors_def)

  note aunit
  also from fs wf
  have a: "f \ foldr (\) fs' \ \ a" by (simp add: wfactors_def)
  have "a \ f \ foldr (\) fs' \"
    by (simp add: Units_closed[OF aunit] a[symmetric])
  finally have "f \ foldr (\) fs' \ \ Units G" by simp
  then have "f \ Units G" by (intro unit_factor[of f], simp+)
  with fnunit show ?thesis by contradiction
qed

text \<open>Comparing wfactors\<close>

lemma (in comm_monoid_cancel) wfactors_listassoc_cong_l:
  assumes fact: "wfactors G fs a"
    and asc: "fs [\] fs'"
    and carr: "a \ carrier G" "set fs \ carrier G" "set fs' \ carrier G"
  shows "wfactors G fs' a"
proof -
  { from asc[symmetric] have "foldr (\) fs' \ \ foldr (\) fs \"
      by (simp add: multlist_listassoc_cong carr)
    also assume "foldr (\) fs \ \ a"
    finally have "foldr (\) fs' \ \ a" by (simp add: carr) }
  then show ?thesis
  using fact
  by (meson asc carr(2) carr(3) irrlist_listassoc_cong wfactors_def)
qed

lemma (in comm_monoid) wfactors_perm_cong_l:
  assumes "wfactors G fs a"
    and "fs <~~> fs'"
    and "set fs \ carrier G"
  shows "wfactors G fs' a"
  using assms irrlist_perm_cong multlist_perm_cong wfactors_def by fastforce

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
proof (elim essentially_equalE)
  fix fs
  assume prm: "as <~~> fs"
  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]
  finally (wfactors_perm_cong_l)
  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
proof (elim wfactorsE, intro wfactorsI)
  assume "foldr (\) fs \ \ a" also note aa'
  finally show "foldr (\) fs \ \ a'" by simp
qed

subsubsection \<open>Essentially equal factorizations\<close>

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")
proof -
  have "as[0 := as ! 0 \ u] [\] as"
  proof (cases as)
    case (Cons a as')
    then show ?thesis
      using associatedI2 carr uunit by auto
  qed auto
  then show ?thesis
    using essentially_equal_def by blast
qed

lemma (in comm_monoid_cancel) factors_cong_unit:
  assumes u: "u \ Units G"
    and a: "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'")
proof (cases as)
  case Nil
  then show ?thesis
    using afs a nunit_factors by auto
next
  case (Cons b bs)
  have *: "\f\set as. irreducible G f" "foldr (\) as \ = a"
    using afs  by (auto simp: factors_def)
  show ?thesis
  proof (intro factorsI)
    show "foldr (\) (as[0 := as ! 0 \ u]) \ = a \ u"
      using Cons u ascarr * by (auto simp add: m_ac Units_closed)
    show "\f\set (as[0 := as ! 0 \ u]). irreducible G f"
      using Cons u ascarr * by (force intro: irreducible_prod_rI)
  qed
qed

lemma (in comm_monoid) perm_wfactorsD:
  assumes prm: "as <~~> bs"
    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"
  shows "a \ b"
  using afs bfs
proof (elim wfactorsE)
  from prm have [simp]: "set bs \ carrier G" by (simp add: perm_closed)
  assume "foldr (\) as \ \ a"
  then have "a \ foldr (\) as \"
    by (simp add: associated_sym)
  also from prm
  have "foldr (\) as \ = foldr (\) bs \" by (rule multlist_perm_cong, simp)
  also assume "foldr (\) bs \ \ b"
  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 [simp]: "a \ carrier G" "b \ carrier G"
    and [simp]: "set as \ carrier G" "set bs \ carrier G"
  shows "a \ b"
  using afs bfs
proof (elim wfactorsE)
  assume "foldr (\) as \ \ a"
  then have "a \ foldr (\) as \" by (simp add: associated_sym)
  also from assoc
  have "foldr (\) as \ \ foldr (\) bs \" by (rule multlist_listassoc_cong, simp+)
  also assume "foldr (\) bs \ \ b"
  finally show "a \ b" by simp
qed

lemma (in comm_monoid_cancel) ee_wfactorsD:
  assumes ee: "essentially_equal G as bs"
    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 bscarr[simp]: "set bs \ carrier G"
  shows "a \ b"
  using ee
proof (elim essentially_equalE)
  fix fs
  assume prm: "as <~~> fs"
  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_all
qed

lemma (in comm_monoid_cancel) ee_factorsD:
  assumes ee: "essentially_equal G as bs"
    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)

lemma (in factorial_monoid) ee_factorsI:
  assumes ab: "a \ b"
    and afs: "factors G as a" and anunit: "a \ Units G"
    and bfs: "factors G bs b" and bnunit: "b \ Units G"
    and ascarr: "set as \ carrier G" and bscarr: "set bs \ carrier G"
  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 obtain u where uunit: "u \ Units G" and a: "a = b \ u"
    by (elim associatedE2)

  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' \<subseteq> 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)
  also note ee
  finally show "essentially_equal G as bs"
    by (simp add: ascarr bscarr bs'carr)
qed

lemma (in factorial_monoid) ee_wfactorsI:
  assumes asc: "a \ b"
    and asf: "wfactors G as a" and bsf: "wfactors G bs b"
    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
proof (cases "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)

  have "essentially_equal G [] []"
    by (fast intro: essentially_equalI)
  then show ?thesis
    by (simp add: e e')
next
  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 ..
  qed

  from wfactors_factors[OF asf ascarr] obtain a' where fa': "factors G as a'" and a': "a' \<sim> a"
    by blast
  from fa' ascarr have a'carr[simp]: "a' \ carrier G"
    by fast

  have a'nunit: "a' \<notin> Units G"
  proof clarify
    assume "a' \ Units G"
    also note a'
    finally have "a \ Units G" by simp
    with anunit
    show "False" ..
  qed

  from wfactors_factors[OF bsf bscarr] obtain b' where fb': "factors G bs b'" and b': "b' \<sim> b"
    by blast
  from fb' bscarr have b'carr[simp]: "b' \ carrier G"
    by fast

  have b'nunit: "b' \<notin> Units G"
  proof clarify
    assume "b' \ Units G"
    also note b'
    finally have "b \ Units G" by simp
    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)
qed

lemma (in factorial_monoid) ee_wfactors:
  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 asc: "a \ b = essentially_equal G as bs"
  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")
  case True
  then have "wfactors G [] a" by (rule unit_wfactors)
  then show ?thesis by (intro exI) force
next
  case False
  with factors_exist [OF acarr] obtain fs where fscarr: "set fs \ carrier G" and f: "factors G fs a"
    by blast
  from f have "wfactors G fs a" by (rule factors_wfactors) fact
  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

lemma (in factorial_monoid) wfactors_unique:
  assumes "wfactors G fs a"
    and "wfactors G fs' a"
    and "a \ 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])

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

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"
  shows "wfactors G (a # fb) (a \ b)"
  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"
  shows "factors G (fa @ fb) (a \ b)"
proof -
  have "foldr (\) (fa @ fb) \ = foldr (\) fa \ \ foldr (\) fb \" if "set fa \ carrier G"
    "Ball (set fa) (irreducible G)"
    using that bscarr by (induct fa) (simp_all add: m_assoc)
  then show ?thesis
    using assms unfolding factors_def by force
qed

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)"
  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"
  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' \<otimes> b')"
    by (intro factors_wfactors) simp_all
  also from b'b carr have trb: "a' \<otimes> b' \<sim> a' \<otimes> b"
    by (intro mult_cong_r)
  also from a'a carr have tra: "a' \<otimes> b \<sim> a \<otimes> b"
    by (intro mult_cong_l)
  finally show "wfactors G (as @ bs) (a \ b)"
    by (simp add: carr)
qed

lemma (in comm_monoid) factors_dividesI:
  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)

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"
  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' \<in> carrier G"
    by (simp add: factors_closed)

  from fsa' fscarr f have "f divides a'"
    by (fast intro: factors_dividesI)
  also note a'a
  finally show "f divides a"
    by (simp add: f fscarr[THEN subsetD] acarr a'carr)
qed

subsubsection \<open>Factorial monoids and wfactors\<close>

lemma (in comm_monoid_cancel) factorial_monoidI:
  assumes wfactors_exists: "\a. \ a \ carrier G; a \ Units 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 anunit]
  obtain as where ascarr: "set as \ carrier G" and afs: "wfactors G as a"
    by blast
  from wfactors_factors [OF afs ascarr] obtain a' where afs': "factors G as a'" and a'a: "a' \<sim> a"
    by blast
  from afs' ascarr have a'carr: "a' \ carrier G"
    by fast
  have a'nunit: "a' \<notin> 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 ..
  qed

  from a'carr acarr a'a obtain u where uunit: "u \ Units G" and a': "a' = a \ u"
    by (blast elim: associatedE2)

  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) 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)

subsection \<open>Factorizations as Multisets\<close>

text \<open>Gives useful operations like intersection\<close>

(* 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)"

text \<open>Helper lemmas\<close>

lemma (in monoid) assocs_repr_independence:
  assumes "y \ assocs G x" "x \ carrier G"
  shows "assocs G x = assocs G y"
  using assms
  by (simp add: eq_closure_of_def elem_def) (use associated_sym associated_trans in \<open>blast+\<close>)

lemma (in monoid) assocs_self:
  assumes "x \ carrier G"
  shows "x \ assocs G x"
  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)

lemma (in comm_monoid) assocs_assoc:
  assumes "a \ assocs G b" "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]

subsubsection \<open>Comparing multisets\<close>

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

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
proof (induction as arbitrary: bs)
  case Nil
  then show ?case by simp
next
  case (Cons a as)
  then show ?case
  proof (clarsimp simp add: Cons_eq_map_conv list_all2_Cons1)
    fix z zs
    assume zzs: "a \ carrier G" "set as \ carrier G" "bs = z # zs" "a \ z"
      "as [\] zs" "z \ carrier G" "set zs \ carrier G"
    then show "assocs G a = assocs G z"
      apply (simp add: eq_closure_of_def elem_def)
      using \<open>a \<in> carrier G\<close> \<open>z \<in> carrier G\<close> \<open>a \<sim> z\<close> associated_sym associated_trans by blast+
  qed
qed

lemma (in comm_monoid_cancel) fmset_listassoc_cong:
  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)

lemma (in comm_monoid_cancel) ee_fmset:
  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
proof (elim essentially_equalE)
  fix as'
  assume prm: "as <~~> as'"
  from prm ascarr have as'carr: "set as' \<subseteq> carrier G"
    by (rule perm_closed)
  from prm have "fmset G as = fmset G as'"
    by (rule fmset_perm_cong)
  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" .
qed

lemma (in monoid_cancel) fmset_ee_aux:
  assumes "cas <~~> cbs" "cas = map (assocs G) as" "cbs = map (assocs G) bs"
  shows "\as'. as <~~> as' \ map (assocs G) as' = cbs"
  using assms
proof (induction cas cbs arbitrary: as bs rule: perm.induct)
  case (Cons xs ys z)
  then show ?case
    by (clarsimp simp add: map_eq_Cons_conv) blast
next
  case (trans xs ys zs)
  then obtain as' where " as <~~> as' \<and> map (assocs G) as' = ys"
    by (metis (no_types, lifting) ex_map_conv mset_eq_perm set_mset_mset)
  then show ?case
    using trans.IH(2) trans.prems(2) by blast
qed auto

lemma (in comm_monoid_cancel) fmset_ee:
  assumes mset: "fmset G as = fmset G bs"
    and ascarr: "set as \ carrier G" and bscarr: "set bs \ carrier G"
  shows "essentially_equal G as bs"
proof -
  from mset have "map (assocs G) as <~~> map (assocs G) bs"
    by (simp add: fmset_def mset_eq_perm del: mset_map)
  then obtain as' where tp: "as <~~> as'" and tm: "map (assocs G) as' = map (assocs G) bs"
    using fmset_ee_aux by blast
  with ascarr have as'carr: "set as' \<subseteq> carrier G"
    using perm_closed by blast
  from tm as'carr[THEN subsetD] bscarr[THEN subsetD] have "as' [\<sim>] bs"
    by (induct as' arbitrary: bs) (simp, fastforce dest: assocs_eqD[THEN associated_sym])
  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)

subsubsection \<open>Interpreting multisets as factorizations\<close>

lemma (in monoid) mset_fmsetEx:
  assumes elems: "\X. X \ set_mset Cs \ \x. P x \ X = assocs G x"
  shows "\cs. (\c \ set cs. P c) \ fmset G cs = Cs"
proof -
  from surjE[OF surj_mset] obtain Cs' where Cs: "Cs = mset Cs'"
    by blast
  have "\cs. (\c \ set cs. P c) \ mset (map (assocs G) cs) = Cs"
    using elems unfolding Cs
  proof (induction Cs')
    case (Cons a Cs')
    then obtain c cs where csP: "\x\set cs. P x" and mset: "mset (map (assocs G) cs) = mset Cs'"
            and cP: "P c" and a: "a = assocs G c"
      by force
    then have tP: "\x\set (c#cs). P x"
      by simp
    show ?case
      using tP mset a by fastforce
  qed auto
  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"
  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)
  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 \<open>Multiplication on multisets\<close>

lemma (in factorial_monoid) mult_wfactors_fmset:
  assumes afs: "wfactors G as a"
    and bfs: "wfactors G bs b"
    and cfs: "wfactors G cs (a \ 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)"
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.75 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.