(*  Title:      HOL/Algebra/Divisibility.thy

    Author:     Clemens Ballarin

    Author:     Stephan Hohe

*)

header {* Divisibility in monoids and rings *}

theory Divisibility

imports "~~/src/HOL/Library/Permutation" Coset Group

begin

section {* Factorial Monoids *}

subsection {* Monoids with Cancellation Law *}

locale monoid_cancel = monoid +

  assumes l_cancel: 

          "\<lbrakk>c \<otimes> a = c \<otimes> b; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"

      and r_cancel: 

          "\<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"

lemma (in monoid) monoid_cancelI:

  assumes l_cancel: 

          "\<And>a b c. \<lbrakk>c \<otimes> a = c \<otimes> b; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"

      and r_cancel: 

          "\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"

  shows "monoid_cancel G"

    by default fact+

lemma (in monoid_cancel) is_monoid_cancel:

  "monoid_cancel G"

  ..

sublocale group \<subseteq> monoid_cancel

  by default simp_all

locale comm_monoid_cancel = monoid_cancel + comm_monoid

lemma comm_monoid_cancelI:

  fixes G (structure)

  assumes "comm_monoid G"

  assumes cancel: 

          "\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"

  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 {* Products of Units in Monoids *}

lemma (in monoid) Units_m_closed[simp, intro]:

  assumes h1unit: "h1 \<in> Units G" and h2unit: "h2 \<in> Units G"

  shows "h1 \<otimes> h2 \<in> Units G"

unfolding Units_def

using assms

by auto (metis Units_inv_closed Units_l_inv Units_m_closed Units_r_inv)

lemma (in monoid) prod_unit_l:

  assumes abunit[simp]: "a \<otimes> b \<in> Units G" and aunit[simp]: "a \<in> Units G"

    and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"

  shows "b \<in> Units G"

proof -

  have c: "inv (a \<otimes> b) \<otimes> a \<in> carrier G" by simp

  have "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = inv (a \<otimes> b) \<otimes> (a \<otimes> b)" by (simp add: m_assoc)

  also have "\<dots> = \<one>" by (simp add: Units_l_inv)

  finally have li: "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = \<one>" .

  have "\<one> = inv a \<otimes> a" by (simp add: Units_l_inv[symmetric])

  also have "\<dots> = inv a \<otimes> \<one> \<otimes> a" by simp

  also have "\<dots> = inv a \<otimes> ((a \<otimes> b) \<otimes> inv (a \<otimes> b)) \<otimes> a"

       by (simp add: Units_r_inv[OF abunit, symmetric] del: Units_r_inv)

  also have "\<dots> = ((inv a \<otimes> a) \<otimes> b) \<otimes> inv (a \<otimes> b) \<otimes> a"

    by (simp add: m_assoc del: Units_l_inv)

  also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by (simp add: Units_l_inv)

  also have "\<dots> = b \<otimes> (inv (a \<otimes> b) \<otimes> a)" by (simp add: m_assoc)

  finally have ri: "b \<otimes> (inv (a \<otimes> b) \<otimes> a) = \<one> " by simp

  from c li ri

      show "b \<in> Units G" by (simp add: Units_def, fast)

qed

lemma (in monoid) prod_unit_r:

  assumes abunit[simp]: "a \<otimes> b \<in> Units G" and bunit[simp]: "b \<in> Units G"

    and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"

  shows "a \<in> Units G"

proof -

  have c: "b \<otimes> inv (a \<otimes> b) \<in> carrier G" by simp

  have "a \<otimes> (b \<otimes> inv (a \<otimes> b)) = (a \<otimes> b) \<otimes> inv (a \<otimes> b)"

    by (simp add: m_assoc del: Units_r_inv)

  also have "\<dots> = \<one>" by simp

  finally have li: "a \<otimes> (b \<otimes> inv (a \<otimes> b)) = \<one>" .

  have "\<one> = b \<otimes> inv b" by (simp add: Units_r_inv[symmetric])

  also have "\<dots> = b \<otimes> \<one> \<otimes> inv b" by simp

  also have "\<dots> = b \<otimes> (inv (a \<otimes> b) \<otimes> (a \<otimes> b)) \<otimes> inv b" 

       by (simp add: Units_l_inv[OF abunit, symmetric] del: Units_l_inv)

  also have "\<dots> = (b \<otimes> inv (a \<otimes> b) \<otimes> a) \<otimes> (b \<otimes> inv b)"

    by (simp add: m_assoc del: Units_l_inv)

  also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by simp

  finally have ri: "(b \<otimes> inv (a \<otimes> b)) \<otimes> a = \<one> " by simp

  from c li ri

      show "a \<in> Units G" by (simp add: Units_def, fast)

qed

lemma (in comm_monoid) unit_factor:

  assumes abunit: "a \<otimes> b \<in> Units G"

    and [simp]: "a \<in> carrier G"  "b \<in> carrier G"

  shows "a \<in> Units G"

using abunit[simplified Units_def]

proof clarsimp

  fix i

  assume [simp]: "i \<in> carrier G"

    and li: "i \<otimes> (a \<otimes> b) = \<one>"

    and ri: "a \<otimes> b \<otimes> i = \<one>"

  have carr': "b \<otimes> i \<in> carrier G" by simp

  have "(b \<otimes> i) \<otimes> a = (i \<otimes> b) \<otimes> a" by (simp add: m_comm)

  also have "\<dots> = i \<otimes> (b \<otimes> a)" by (simp add: m_assoc)

  also have "\<dots> = i \<otimes> (a \<otimes> b)" by (simp add: m_comm)

  also note li

  finally have li': "(b \<otimes> i) \<otimes> a = \<one>" .

  have "a \<otimes> (b \<otimes> i) = a \<otimes> b \<otimes> i" by (simp add: m_assoc)

  also note ri

  finally have ri': "a \<otimes> (b \<otimes> i) = \<one>" .

  from carr' li' ri'

      show "a \<in> Units G" by (simp add: Units_def, fast)

qed

subsection {* Divisibility and Association *}

subsubsection {* Function definitions *}

definition

  factor :: "[_, 'a, 'a] \<Rightarrow> bool" (infix "divides\<index>" 65)

  where "a divides\<^bsub>G\<^esub> b \<longleftrightarrow> (\<exists>c\<in>carrier G. b = a \<otimes>\<^bsub>G\<^esub> c)"

definition

  associated :: "[_, 'a, 'a] => bool" (infix "\<sim>\<index>" 55)

  where "a \<sim>\<^bsub>G\<^esub> b \<longleftrightarrow> a divides\<^bsub>G\<^esub> b \<and> b divides\<^bsub>G\<^esub> a"

abbreviation

  "division_rel G == \<lparr>carrier = carrier G, eq = op \<sim>\<^bsub>G\<^esub>, le = op divides\<^bsub>G\<^esub>\<rparr>"

definition

  properfactor :: "[_, 'a, 'a] \<Rightarrow> bool"

  where "properfactor G a b \<longleftrightarrow> a divides\<^bsub>G\<^esub> b \<and> \<not>(b divides\<^bsub>G\<^esub> a)"

definition

  irreducible :: "[_, 'a] \<Rightarrow> bool"

  where "irreducible G a \<longleftrightarrow> a \<notin> Units G \<and> (\<forall>b\<in>carrier G. properfactor G b a \<longrightarrow> b \<in> Units G)"

definition

  prime :: "[_, 'a] \<Rightarrow> bool" where

  "prime G p \<longleftrightarrow>

    p \<notin> Units G \<and> 

    (\<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 {* Divisibility *}

lemma dividesI:

  fixes G (structure)

  assumes carr: "c \<in> carrier G"

    and p: "b = a \<otimes> c"

  shows "a divides b"

unfolding factor_def

using assms by fast

lemma dividesI' [intro]:

   fixes G (structure)

  assumes p: "b = a \<otimes> c"

    and carr: "c \<in> carrier G"

  shows "a divides b"

using assms

by (fast intro: dividesI)

lemma dividesD:

  fixes G (structure)

  assumes "a divides b"

  shows "\<exists>c\<in>carrier G. b = a \<otimes> c"

using assms

unfolding factor_def

by fast

lemma dividesE [elim]:

  fixes G (structure)

  assumes d: "a divides b"

    and elim: "\<And>c. \<lbrakk>b = a \<otimes> c; c \<in> carrier G\<rbrakk> \<Longrightarrow> P"

  shows "P"

proof -

  from dividesD[OF d]

      obtain c

      where "c\<in>carrier G"

      and "b = a \<otimes> c"

      by auto

  thus "P" by (elim elim)

qed

lemma (in monoid) divides_refl[simp, intro!]:

  assumes carr: "a \<in> carrier G"

  shows "a divides a"

apply (intro dividesI[of "\<one>"])

apply (simp, simp add: carr)

done

lemma (in monoid) divides_trans [trans]:

  assumes dvds: "a divides b"  "b divides c"

    and acarr: "a \<in> carrier G"

  shows "a divides c"

using dvds[THEN dividesD]

by (blast intro: dividesI m_assoc acarr)

lemma (in monoid) divides_mult_lI [intro]:

  assumes ab: "a divides b"

    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"

  shows "(c \<otimes> a) divides (c \<otimes> b)"

using ab

apply (elim dividesE, simp add: m_assoc[symmetric] carr)

apply (fast intro: dividesI)

done

lemma (in monoid_cancel) divides_mult_l [simp]:

  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"

  shows "(c \<otimes> a) divides (c \<otimes> b) = a divides b"

apply safe

 apply (elim dividesE, intro dividesI, assumption)

 apply (rule l_cancel[of c])

    apply (simp add: m_assoc carr)+

apply (fast intro: carr)

done

lemma (in comm_monoid) divides_mult_rI [intro]:

  assumes ab: "a divides b"

    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"

  shows "(a \<otimes> c) divides (b \<otimes> c)"

using carr ab

apply (simp add: m_comm[of a c] m_comm[of b c])

apply (rule divides_mult_lI, assumption+)

done

lemma (in comm_monoid_cancel) divides_mult_r [simp]:

  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"

  shows "(a \<otimes> c) divides (b \<otimes> c) = a divides b"

using carr

by (simp add: m_comm[of a c] m_comm[of b c])

lemma (in monoid) divides_prod_r:

  assumes ab: "a divides b"

    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"

  shows "a divides (b \<otimes> c)"

using ab carr

by (fast intro: m_assoc)

lemma (in comm_monoid) divides_prod_l:

  assumes carr[intro]: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"

    and ab: "a divides b"

  shows "a divides (c \<otimes> b)"

using ab carr

apply (simp add: m_comm[of c b])

apply (fast intro: divides_prod_r)

done

lemma (in monoid) unit_divides:

  assumes uunit: "u \<in> Units G"

      and acarr: "a \<in> carrier G"

  shows "u divides a"

proof (intro dividesI[of "(inv u) \<otimes> a"], fast intro: uunit acarr)

  from uunit acarr

      have xcarr: "inv u \<otimes> a \<in> carrier G" by fast

  from uunit acarr

       have "u \<otimes> (inv u \<otimes> a) = (u \<otimes> inv u) \<otimes> a" by (fast intro: m_assoc[symmetric])

  also have "\<dots> = \<one> \<otimes> a" by (simp add: Units_r_inv[OF uunit])

  also from acarr 

       have "\<dots> = a" by simp

  finally

       show "a = u \<otimes> (inv u \<otimes> a)" ..

qed

lemma (in comm_monoid) divides_unit:

  assumes udvd: "a divides u"

      and  carr: "a \<in> carrier G"  "u \<in> Units G"

  shows "a \<in> Units G"

using udvd carr

by (blast intro: unit_factor)

lemma (in comm_monoid) Unit_eq_dividesone:

  assumes ucarr: "u \<in> carrier G"

  shows "u \<in> Units G = u divides \<one>"

using ucarr

by (fast dest: divides_unit intro: unit_divides)

subsubsection {* Association *}

lemma associatedI:

  fixes G (structure)

  assumes "a divides b"  "b divides a"

  shows "a \<sim> b"

using assms

by (simp add: associated_def)

lemma (in monoid) associatedI2:

  assumes uunit[simp]: "u \<in> Units G"

    and a: "a = b \<otimes> u"

    and bcarr[simp]: "b \<in> carrier G"

  shows "a \<sim> b"

using uunit bcarr

unfolding a

apply (intro associatedI)

 apply (rule dividesI[of "inv u"], simp)

 apply (simp add: m_assoc Units_closed Units_r_inv)

apply fast

done

lemma (in monoid) associatedI2':

  assumes a: "a = b \<otimes> u"

    and uunit: "u \<in> Units G"

    and bcarr: "b \<in> carrier G"

  shows "a \<sim> b"

using assms by (intro associatedI2)

lemma associatedD:

  fixes G (structure)

  assumes "a \<sim> b"

  shows "a divides b"

using assms by (simp add: associated_def)

lemma (in monoid_cancel) associatedD2:

  assumes assoc: "a \<sim> b"

    and carr: "a \<in> carrier G"  "b \<in> carrier G"

  shows "\<exists>u\<in>Units G. a = b \<otimes> u"

using assoc

unfolding associated_def

proof clarify

  assume "b divides a"

  hence "\<exists>u\<in>carrier G. a = b \<otimes> u" by (rule dividesD)

  from this obtain u

      where ucarr: "u \<in> carrier G" and a: "a = b \<otimes> u"

      by auto

  assume "a divides b"

  hence "\<exists>u'\<in>carrier G. b = a \<otimes> u'" by (rule dividesD)

  from this obtain u'

      where u'carr: "u' \<in> carrier G" and b: "b = a \<otimes> u'"

      by auto

  note carr = carr ucarr u'carr

  from carr

       have "a \<otimes> \<one> = a" by simp

  also have "\<dots> = b \<otimes> u" by (simp add: a)

  also have "\<dots> = a \<otimes> u' \<otimes> u" by (simp add: b)

  also from carr

       have "\<dots> = a \<otimes> (u' \<otimes> u)" by (simp add: m_assoc)

  finally

       have "a \<otimes> \<one> = a \<otimes> (u' \<otimes> u)" .

  with carr

      have u1: "\<one> = u' \<otimes> u" by (fast dest: l_cancel)

  from carr

       have "b \<otimes> \<one> = b" by simp

  also have "\<dots> = a \<otimes> u'" by (simp add: b)

  also have "\<dots> = b \<otimes> u \<otimes> u'" by (simp add: a)

  also from carr

       have "\<dots> = b \<otimes> (u \<otimes> u')" by (simp add: m_assoc)

  finally

       have "b \<otimes> \<one> = b \<otimes> (u \<otimes> u')" .

  with carr

      have u2: "\<one> = u \<otimes> u'" by (fast dest: l_cancel)

  from u'carr u1[symmetric] u2[symmetric]

      have "\<exists>u'\<in>carrier G. u' \<otimes> u = \<one> \<and> u \<otimes> u' = \<one>" by fast

  hence "u \<in> Units G" by (simp add: Units_def ucarr)

  from ucarr this a

      show "\<exists>u\<in>Units G. a = b \<otimes> u" by fast

qed

lemma associatedE:

  fixes G (structure)

  assumes assoc: "a \<sim> b"

    and e: "\<lbrakk>a divides b; b divides a\<rbrakk> \<Longrightarrow> P"

  shows "P"

proof -

  from assoc

      have "a divides b"  "b divides a"

      by (simp add: associated_def)+

  thus "P" by (elim e)

qed

lemma (in monoid_cancel) associatedE2:

  assumes assoc: "a \<sim> b"

    and e: "\<And>u. \<lbrakk>a = b \<otimes> u; u \<in> Units G\<rbrakk> \<Longrightarrow> P"

    and carr: "a \<in> carrier G"  "b \<in> carrier G"

  shows "P"

proof -

  from assoc and carr

      have "\<exists>u\<in>Units G. a = b \<otimes> u" by (rule associatedD2)

  from this obtain u

      where "u \<in> Units G"  "a = b \<otimes> u"

      by auto

  thus "P" by (elim e)

qed

lemma (in monoid) associated_refl [simp, intro!]:

  assumes "a \<in> carrier G"

  shows "a \<sim> a"

using assms

by (fast intro: associatedI)

lemma (in monoid) associated_sym [sym]:

  assumes "a \<sim> b"

    and "a \<in> carrier G"  "b \<in> carrier G"

  shows "b \<sim> a"

using assms

by (iprover intro: associatedI elim: associatedE)

lemma (in monoid) associated_trans [trans]:

  assumes "a \<sim> b"  "b \<sim> c"

    and "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"

  shows "a \<sim> c"

using assms

by (iprover intro: associatedI divides_trans elim: associatedE)

lemma (in monoid) division_equiv [intro, simp]:

  "equivalence (division_rel G)"

  apply unfold_locales

  apply simp_all

  apply (metis associated_def)

  apply (iprover intro: associated_trans)

  done

subsubsection {* Division and associativity *}

lemma divides_antisym:

  fixes G (structure)

  assumes "a divides b"  "b divides a"

    and "a \<in> carrier G"  "b \<in> carrier G"

  shows "a \<sim> b"

using assms

by (fast intro: associatedI)

lemma (in monoid) divides_cong_l [trans]:

  assumes xx': "x \<sim> x'"

    and xdvdy: "x' divides y"

    and carr [simp]: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"

  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

qed

lemma (in monoid) divides_cong_r [trans]:

  assumes xdvdy: "x divides y"

    and yy': "y \<sim> y'"

    and carr[simp]: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"

  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

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 (blast intro: divides_cong_l divides_cong_r associated_sym)

  done

subsubsection {* Multiplication and associativity *}

lemma (in monoid_cancel) mult_cong_r:

  assumes "b \<sim> b'"

    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "b' \<in> carrier G"

  shows "a \<otimes> b \<sim> a \<otimes> b'"

using assms

apply (elim associatedE2, intro associatedI2)

apply (auto intro: m_assoc[symmetric])

done

lemma (in comm_monoid_cancel) mult_cong_l:

  assumes "a \<sim> a'"

    and carr: "a \<in> carrier G"  "a' \<in> carrier G"  "b \<in> carrier G"

  shows "a \<otimes> b \<sim> a' \<otimes> b"

using assms

apply (elim associatedE2, intro associatedI2)

    apply assumption

   apply (simp add: m_assoc Units_closed)

   apply (simp add: m_comm Units_closed)

  apply simp+

done

lemma (in monoid_cancel) assoc_l_cancel:

  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "b' \<in> carrier G"

    and "a \<otimes> b \<sim> a \<otimes> b'"

  shows "b \<sim> b'"

using assms

apply (elim associatedE2, intro associatedI2)

    apply assumption

   apply (rule l_cancel[of a])

      apply (simp add: m_assoc Units_closed)

     apply fast+

done

lemma (in comm_monoid_cancel) assoc_r_cancel:

  assumes "a \<otimes> b \<sim> a' \<otimes> b"

    and carr: "a \<in> carrier G"  "a' \<in> carrier G"  "b \<in> carrier G"

  shows "a \<sim> a'"

using assms

apply (elim associatedE2, intro associatedI2)

    apply assumption

   apply (rule r_cancel[of a b])

      apply (metis Units_closed assms(3) assms(4) m_ac)

     apply fast+

done

subsubsection {* Units *}

lemma (in monoid_cancel) assoc_unit_l [trans]:

  assumes asc: "a \<sim> b" and bunit: "b \<in> Units G"

    and carr: "a \<in> carrier G" 

  shows "a \<in> Units G"

using assms

by (fast elim: associatedE2)

lemma (in monoid_cancel) assoc_unit_r [trans]:

  assumes aunit: "a \<in> Units G" and asc: "a \<sim> b"

    and bcarr: "b \<in> carrier G"

  shows "b \<in> Units G"

using aunit bcarr associated_sym[OF asc]

by (blast intro: assoc_unit_l)

lemma (in comm_monoid) Units_cong:

  assumes aunit: "a \<in> Units G" and asc: "a \<sim> b"

    and bcarr: "b \<in> carrier G"

  shows "b \<in> Units G"

using assms

by (blast intro: divides_unit elim: associatedE)

lemma (in monoid) Units_assoc:

  assumes units: "a \<in> Units G"  "b \<in> Units G"

  shows "a \<sim> b"

using units

by (fast intro: associatedI unit_divides)

lemma (in monoid) Units_are_ones:

  "Units G {.=}\<^bsub>(division_rel G)\<^esub> {\<one>}"

apply (simp add: set_eq_def elem_def, rule, simp_all)

proof clarsimp

  fix a

  assume aunit: "a \<in> Units G"

  show "a \<sim> \<one>"

  apply (rule associatedI)

   apply (fast intro: dividesI[of "inv a"] aunit Units_r_inv[symmetric])

  apply (fast intro: dividesI[of "a"] l_one[symmetric] Units_closed[OF aunit])

  done

next

  have "\<one> \<in> Units G" by simp

  moreover have "\<one> \<sim> \<one>" by simp

  ultimately show "\<exists>a \<in> Units G. \<one> \<sim> a" by fast

qed

lemma (in comm_monoid) Units_Lower:

  "Units G = Lower (division_rel G) (carrier G)"

apply (simp add: Units_def Lower_def)

apply (rule, rule)

 apply clarsimp

  apply (rule unit_divides)

   apply (unfold Units_def, fast)

  apply assumption

apply clarsimp

apply (metis Unit_eq_dividesone Units_r_inv_ex m_ac(2) one_closed)

done

subsubsection {* Proper factors *}

lemma properfactorI:

  fixes G (structure)

  assumes "a divides b"

    and "\<not>(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: "\<not>(a \<sim> b)"

  shows "properfactor G a b"

apply (rule properfactorI, rule advdb)

proof (rule ccontr, simp)

  assume "b divides a"

  with advdb have "a \<sim> b" by (rule associatedI)

  with neq show "False" by fast

qed

lemma (in comm_monoid_cancel) properfactorI3:

  assumes p: "p = a \<otimes> b"

    and nunit: "b \<notin> Units G"

    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "p \<in> carrier G"

  shows "properfactor G a p"

unfolding p

using carr

apply (intro properfactorI, fast)

proof (clarsimp, elim dividesE)

  fix c

  assume ccarr: "c \<in> carrier G"

  note [simp] = carr ccarr

  have "a \<otimes> \<one> = a" by simp

  also assume "a = a \<otimes> b \<otimes> c"

  also have "\<dots> = a \<otimes> (b \<otimes> c)" by (simp add: m_assoc)

  finally have "a \<otimes> \<one> = a \<otimes> (b \<otimes> c)" .

  hence rinv: "\<one> = b \<otimes> c" by (intro l_cancel[of "a" "\<one>" "b \<otimes> c"], simp+)

  also have "\<dots> = c \<otimes> b" by (simp add: m_comm)

  finally have linv: "\<one> = c \<otimes> b" .

  from ccarr linv[symmetric] rinv[symmetric]

  have "b \<in> Units G" unfolding Units_def by fastforce

  with nunit

      show "False" ..

qed

lemma properfactorE:

  fixes G (structure)

  assumes pf: "properfactor G a b"

    and r: "\<lbrakk>a divides b; \<not>(b divides a)\<rbrakk> \<Longrightarrow> P"

  shows "P"

using pf

unfolding properfactor_def

by (fast intro: r)

lemma properfactorE2:

  fixes G (structure)

  assumes pf: "properfactor G a b"

    and elim: "\<lbrakk>a divides b; \<not>(a \<sim> b)\<rbrakk> \<Longrightarrow> P"

  shows "P"

using pf

unfolding properfactor_def

by (fast elim: elim associatedE)

lemma (in monoid) properfactor_unitE:

  assumes uunit: "u \<in> Units G"

    and pf: "properfactor G a u"

    and acarr: "a \<in> carrier G"

  shows "P"

using pf unit_divides[OF uunit acarr]

by (fast elim: properfactorE)

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 dvds: "a divides b"  "properfactor G b c"

    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"

  shows "properfactor G a c"

using dvds carr

apply (elim properfactorE, intro properfactorI)

 apply (iprover intro: divides_trans)+

done

lemma (in monoid) properfactor_trans2 [trans]:

  assumes dvds: "properfactor G a b"  "b divides c"

    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"

  shows "properfactor G a c"

using dvds carr

apply (elim properfactorE, intro properfactorI)

 apply (iprover intro: divides_trans)+

done

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

lemma (in monoid) properfactor_cong_l [trans]:

  assumes x'x: "x' \<sim> x"

    and pf: "properfactor G x y"

    and carr: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"

  shows "properfactor G x' y"

using pf

unfolding properfactor_lless

proof -

  interpret weak_partial_order "division_rel G" ..

  from x'x

       have "x' .=\<^bsub>division_rel G\<^esub> x" by simp

  also assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"

  finally

       show "x' \<sqsubset>\<^bsub>division_rel G\<^esub> y" by (simp add: carr)

qed

lemma (in monoid) properfactor_cong_r [trans]:

  assumes pf: "properfactor G x y"

    and yy': "y \<sim> y'"

    and carr: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"

  shows "properfactor G x y'"

using pf

unfolding properfactor_lless

proof -

  interpret weak_partial_order "division_rel G" ..

  assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"

  also from yy'

       have "y .=\<^bsub>division_rel G\<^esub> y'" by simp

  finally

       show "x \<sqsubset>\<^bsub>division_rel G\<^esub> y'" by (simp add: carr)

qed

lemma (in monoid_cancel) properfactor_mult_lI [intro]:

  assumes ab: "properfactor G a b"

    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"

  shows "properfactor G (c \<otimes> a) (c \<otimes> b)"

using ab carr

by (fastforce elim: properfactorE intro: properfactorI)

lemma (in monoid_cancel) properfactor_mult_l [simp]:

  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"

  shows "properfactor G (c \<otimes> a) (c \<otimes> b) = properfactor G a b"

using carr

by (fastforce elim: properfactorE intro: properfactorI)

lemma (in comm_monoid_cancel) properfactor_mult_rI [intro]:

  assumes ab: "properfactor G a b"

    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"

  shows "properfactor G (a \<otimes> c) (b \<otimes> c)"

using ab carr

by (fastforce elim: properfactorE intro: properfactorI)

lemma (in comm_monoid_cancel) properfactor_mult_r [simp]:

  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"

  shows "properfactor G (a \<otimes> c) (b \<otimes> c) = properfactor G a b"

using carr

by (fastforce elim: properfactorE intro: properfactorI)

lemma (in monoid) properfactor_prod_r:

  assumes ab: "properfactor G a b"

    and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"

  shows "properfactor G a (b \<otimes> c)"

by (intro properfactor_trans2[OF ab] divides_prod_r, simp+)

lemma (in comm_monoid) properfactor_prod_l:

  assumes ab: "properfactor G a b"

    and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"

  shows "properfactor G a (c \<otimes> b)"

by (intro properfactor_trans2[OF ab] divides_prod_l, simp+)

subsection {* Irreducible Elements and Primes *}

subsubsection {* Irreducible elements *}

lemma irreducibleI:

  fixes G (structure)

  assumes "a \<notin> Units G"

    and "\<And>b. \<lbrakk>b \<in> carrier G; properfactor G b a\<rbrakk> \<Longrightarrow> b \<in> Units G"

  shows "irreducible G a"

using assms 

unfolding irreducible_def

by blast

lemma irreducibleE:

  fixes G (structure)

  assumes irr: "irreducible G a"

     and elim: "\<lbrakk>a \<notin> Units G; \<forall>b. b \<in> carrier G \<and> properfactor G b a \<longrightarrow> b \<in> Units G\<rbrakk> \<Longrightarrow> P"

  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 \<in> carrier G"

  shows "b \<in> Units G"

using assms

by (fast elim: irreducibleE)

lemma (in monoid_cancel) irreducible_cong [trans]:

  assumes irred: "irreducible G a"

    and aa': "a \<sim> a'"

    and carr[simp]: "a \<in> carrier G"  "a' \<in> carrier G"

  shows "irreducible G a'"

using assms

apply (elim irreducibleE, intro irreducibleI)

apply simp_all

apply (metis assms(2) assms(3) assoc_unit_l)

apply (metis assms(2) assms(3) assms(4) associated_sym properfactor_cong_r)

done

lemma (in monoid) irreducible_prod_rI:

  assumes airr: "irreducible G a"

    and bunit: "b \<in> Units G"

    and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"

  shows "irreducible G (a \<otimes> b)"

using airr carr bunit

apply (elim irreducibleE, intro irreducibleI, clarify)

 apply (subgoal_tac "a \<in> Units G", simp)

 apply (intro prod_unit_r[of a b] carr bunit, assumption)

apply (metis assms associatedI2 m_closed properfactor_cong_r)

done

lemma (in comm_monoid) irreducible_prod_lI:

  assumes birr: "irreducible G b"

    and aunit: "a \<in> Units G"

    and carr [simp]: "a \<in> carrier G"  "b \<in> carrier G"

  shows "irreducible G (a \<otimes> b)"

apply (subst m_comm, simp+)

apply (intro irreducible_prod_rI assms)

done

lemma (in comm_monoid_cancel) irreducible_prodE [elim]:

  assumes irr: "irreducible G (a \<otimes> b)"

    and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"

    and e1: "\<lbrakk>irreducible G a; b \<in> Units G\<rbrakk> \<Longrightarrow> P"

    and e2: "\<lbrakk>a \<in> Units G; irreducible G b\<rbrakk> \<Longrightarrow> P"

  shows "P"

using irr

proof (elim irreducibleE)

  assume abnunit: "a \<otimes> b \<notin> Units G"

    and isunit[rule_format]: "\<forall>ba. ba \<in> carrier G \<and> properfactor G ba (a \<otimes> b) \<longrightarrow> ba \<in> Units G"

  show "P"

  proof (cases "a \<in> Units G")

    assume aunit: "a \<in>  Units G"

    have "irreducible G b"

    apply (rule irreducibleI)

    proof (rule ccontr, simp)

      assume "b \<in> Units G"

      with aunit have "(a \<otimes> b) \<in> Units G" by fast

      with abnunit show "False" ..

    next

      fix c

      assume ccarr: "c \<in> carrier G"

        and "properfactor G c b"

      hence "properfactor G c (a \<otimes> b)" by (simp add: properfactor_prod_l[of c b a])

      from ccarr this show "c \<in> Units G" by (fast intro: isunit)

    qed

    from aunit this show "P" by (rule e2)

  next

    assume anunit: "a \<notin> Units G"

    with carr have "properfactor G b (b \<otimes> a)" by (fast intro: properfactorI3)

    hence bf: "properfactor G b (a \<otimes> b)" by (subst m_comm[of a b], simp+)

    hence bunit: "b \<in> Units G" by (intro isunit, simp)

    have "irreducible G a"

    apply (rule irreducibleI)

    proof (rule ccontr, simp)

      assume "a \<in> Units G"

      with bunit have "(a \<otimes> b) \<in> Units G" by fast

      with abnunit show "False" ..

    next

      fix c

      assume ccarr: "c \<in> carrier G"

        and "properfactor G c a"

      hence "properfactor G c (a \<otimes> b)" by (simp add: properfactor_prod_r[of c a b])

      from ccarr this show "c \<in> Units G" by (fast intro: isunit)

    qed

    from this bunit show "P" by (rule e1)

  qed

qed

subsubsection {* Prime elements *}

lemma primeI:

  fixes G (structure)

  assumes "p \<notin> Units G"

    and "\<And>a b. \<lbrakk>a \<in> carrier G; b \<in> carrier G; p divides (a \<otimes> b)\<rbrakk> \<Longrightarrow> p divides a \<or> p divides b"

  shows "prime G p"

using assms

unfolding prime_def

by blast

lemma primeE:

  fixes G (structure)

  assumes pprime: "prime G p"

    and e: "\<lbrakk>p \<notin> Units G; \<forall>a\<in>carrier G. \<forall>b\<in>carrier G.

                          p divides a \<otimes> b \<longrightarrow> p divides a \<or> p divides b\<rbrakk> \<Longrightarrow> P"

  shows "P"

using pprime

unfolding prime_def

by (blast dest: e)

lemma (in comm_monoid_cancel) prime_divides:

  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"

    and pprime: "prime G p"

    and pdvd: "p divides a \<otimes> b"

  shows "p divides a \<or> p divides b"

using assms

by (blast elim: primeE)

lemma (in monoid_cancel) prime_cong [trans]:

  assumes pprime: "prime G p"

    and pp': "p \<sim> p'"

    and carr[simp]: "p \<in> carrier G"  "p' \<in> carrier G"

  shows "prime G p'"

using pprime

apply (elim primeE, intro primeI)

apply (metis assms(2) assms(3) assoc_unit_l)

apply (metis assms(2) assms(3) assms(4) associated_sym divides_cong_l m_closed)

done

subsection {* Factorization and Factorial Monoids *}

subsubsection {* Function definitions *}

definition

  factors :: "[_, 'a list, 'a] \<Rightarrow> bool"

  where "factors G fs a \<longleftrightarrow> (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>\<^bsub>G\<^esub>) fs \<one>\<^bsub>G\<^esub> = a"

definition

  wfactors ::"[_, 'a list, 'a] \<Rightarrow> bool"

  where "wfactors G fs a \<longleftrightarrow> (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>\<^bsub>G\<^esub>) fs \<one>\<^bsub>G\<^esub> \<sim>\<^bsub>G\<^esub> a"

abbreviation

  list_assoc :: "('a,_) monoid_scheme \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "[\<sim>]\<index>" 44)

  where "list_assoc G == list_all2 (op \<sim>\<^bsub>G\<^esub>)"

definition

  essentially_equal :: "[_, 'a list, 'a list] \<Rightarrow> bool"

  where "essentially_equal G fs1 fs2 \<longleftrightarrow> (\<exists>fs1'. fs1 <~~> fs1' \<and> fs1' [\<sim>]\<^bsub>G\<^esub> fs2)"

locale factorial_monoid = comm_monoid_cancel +

  assumes factors_exist: 

          "\<lbrakk>a \<in> carrier G; a \<notin> Units G\<rbrakk> \<Longrightarrow> \<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a"

      and factors_unique: 

          "\<lbrakk>factors G fs a; factors G fs' a; a \<in> carrier G; a \<notin> Units G; 

            set fs \<subseteq> carrier G; set fs' \<subseteq> carrier G\<rbrakk> \<Longrightarrow> essentially_equal G fs fs'"

subsubsection {* Comparing lists of elements *}

text {* Association on lists *}

lemma (in monoid) listassoc_refl [simp, intro]:

  assumes "set as \<subseteq> carrier G"

  shows "as [\<sim>] as"

using assms

by (induct as) simp+

lemma (in monoid) listassoc_sym [sym]:

  assumes "as [\<sim>] bs"

    and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"

  shows "bs [\<sim>] as"

using assms

proof (induct as arbitrary: bs, simp)

  case Cons

  thus ?case

    apply (induct bs, simp)

    apply clarsimp