theory Unique_Factorization imports Polynomial_Interpolation.Ring_Hom_Poly Polynomial_Factorization.Polynomial_Divisibility "HOL-Combinatorics.Permutations" "HOL-Computational_Algebra.Euclidean_Algorithm" Containers.Containers_Auxiliary (* only for a lemma *) More_Missing_Multiset "HOL-Algebra.Divisibility" begin hide_const(open) Divisibility.prime Divisibility.irreducible hide_fact(open) Divisibility.irreducible_def Divisibility.irreducibleI Divisibility.irreducibleD Divisibility.irreducibleE hide_const (open) Rings.coprime lemma irreducible_uminus [simp]: fixes a::"'a::idom" shows "irreducible (-a) ⟷ irreducible a" using irreducible_mult_unit_left[of "-1::'a"] by auto context comm_monoid_mult begin definition coprime :: "'a ⇒ 'a ⇒ bool" where coprime_def': "coprime p q ≡ ∀r. r dvd p ⟶ r dvd q ⟶ r dvd 1" lemma coprimeI: assumes "⋀r. r dvd p ⟹ r dvd q ⟹ r dvd 1" shows "coprime p q" using assms by (auto simp: coprime_def') lemma coprimeE: assumes "coprime p q" and "(⋀r. r dvd p ⟹ r dvd q ⟹ r dvd 1) ⟹ thesis" shows thesis using assms by (auto simp: coprime_def') lemma coprime_commute [ac_simps]: "coprime p q ⟷ coprime q p" by (auto simp add: coprime_def') lemma not_coprime_iff_common_factor: "¬ coprime p q ⟷ (∃r. r dvd p ∧ r dvd q ∧ ¬ r dvd 1)" by (auto simp add: coprime_def') end lemma (in algebraic_semidom) coprime_iff_coprime [simp, code]: "coprime = Rings.coprime" by (simp add: fun_eq_iff coprime_def coprime_def') lemma (in comm_semiring_1) coprime_0 [simp]: "coprime p 0 ⟷ p dvd 1" "coprime 0 p ⟷ p dvd 1" by (auto intro: coprimeI elim: coprimeE dest: dvd_trans) (**** until here ****) (* TODO: move or...? *) lemma dvd_rewrites: "dvd.dvd ((*)) = (dvd)" by (unfold dvd.dvd_def dvd_def, rule) subsection ‹Interfacing UFD properties› hide_const (open) Divisibility.irreducible context comm_monoid_mult_isom begin lemma coprime_hom[simp]: "coprime (hom x) y' ⟷ coprime x (Hilbert_Choice.inv hom y')" proof- show ?thesis by (unfold coprime_def', fold ball_UNIV, subst surj[symmetric], simp) qed lemma coprime_inv_hom[simp]: "coprime (Hilbert_Choice.inv hom x') y ⟷ coprime x' (hom y)" proof- interpret inv: comm_monoid_mult_isom "Hilbert_Choice.inv hom".. show ?thesis by simp qed end subsubsection ‹Original part› lemma dvd_dvd_imp_smult: fixes p q :: "'a :: idom poly" assumes pq: "p dvd q" and qp: "q dvd p" shows "∃c. p = smult c q" proof (cases "p = 0") case True then show ?thesis by auto next case False from qp obtain r where r: "p = q * r" by (elim dvdE, auto) with False qp have r0: "r ≠ 0" and q0: "q ≠ 0" by auto with divides_degree[OF pq] divides_degree[OF qp] False have "degree p = degree q" by auto with r degree_mult_eq[OF q0 r0] have "degree r = 0" by auto from degree_0_id[OF this] obtain c where "r = [:c:]" by metis from r[unfolded this] show ?thesis by auto qed lemma dvd_const: assumes pq: "(p::'a::semidom poly) dvd q" and q0: "q ≠ 0" and degq: "degree q = 0" shows "degree p = 0" proof- from dvdE[OF pq] obtain r where *: "q = p * r". with q0 have "p ≠ 0" "r ≠ 0" by auto from degree_mult_eq[OF this] degq * show "degree p = 0" by auto qed context Rings.dvd begin abbreviation ddvd (infix "ddvd" 40) where "x ddvd y ≡ x dvd y ∧ y dvd x" lemma ddvd_sym[sym]: "x ddvd y ⟹ y ddvd x" by auto end context comm_monoid_mult begin lemma ddvd_trans[trans]: "x ddvd y ⟹ y ddvd z ⟹ x ddvd z" using dvd_trans by auto lemma ddvd_transp: "transp (ddvd)" by (intro transpI, fact ddvd_trans) end context comm_semiring_1 begin definition mset_factors where "mset_factors F p ≡ F ≠ {#} ∧ (∀f. f ∈# F ⟶ irreducible f) ∧ p = prod_mset F" lemma mset_factorsI[intro!]: assumes "⋀f. f ∈# F ⟹ irreducible f" and "F ≠ {#}" and "prod_mset F = p" shows "mset_factors F p" unfolding mset_factors_def using assms by auto lemma mset_factorsD: assumes "mset_factors F p" shows "f ∈# F ⟹ irreducible f" and "F ≠ {#}" and "prod_mset F = p" using assms[unfolded mset_factors_def] by auto lemma mset_factorsE[elim]: assumes "mset_factors F p" and "(⋀f. f ∈# F ⟹ irreducible f) ⟹ F ≠ {#} ⟹ prod_mset F = p ⟹ thesis" shows thesis using assms[unfolded mset_factors_def] by auto lemma mset_factors_imp_not_is_unit: assumes "mset_factors F p" shows "¬ p dvd 1" proof(cases F) case empty with assms show ?thesis by auto next case (add f F) with assms have "¬ f dvd 1" "p = f * prod_mset F" by (auto intro!: irreducible_not_unit) then show ?thesis by auto qed definition primitive_poly where "primitive_poly f ≡ ∀d. (∀i. d dvd coeff f i) ⟶ d dvd 1" end lemma(in semidom) mset_factors_imp_nonzero: assumes "mset_factors F p" shows "p ≠ 0" proof assume "p = 0" moreover from assms have "prod_mset F = p" by auto ultimately obtain f where "f ∈# F" "f = 0" by auto with assms show False by auto qed class ufd = idom + assumes mset_factors_exist: "⋀x. x ≠ 0 ⟹ ¬ x dvd 1 ⟹ ∃F. mset_factors F x" and mset_factors_unique: "⋀x F G. mset_factors F x ⟹ mset_factors G x ⟹ rel_mset (ddvd) F G" subsubsection ‹Connecting to HOL/Divisibility› context comm_semiring_1 begin abbreviation "mk_monoid ≡ ⦇carrier = UNIV - {0}, mult = (*), one = 1⦈" lemma carrier_0[simp]: "x ∈ carrier mk_monoid ⟷ x ≠ 0" by auto lemmas mk_monoid_simps = carrier_0 monoid.simps abbreviation irred where "irred ≡ Divisibility.irreducible mk_monoid" abbreviation factor where "factor ≡ Divisibility.factor mk_monoid" abbreviation factors where "factors ≡ Divisibility.factors mk_monoid" abbreviation properfactor where "properfactor ≡ Divisibility.properfactor mk_monoid" lemma factors: "factors fs y ⟷ prod_list fs = y ∧ Ball (set fs) irred" proof - have "prod_list fs = foldr (*) fs 1" by (induct fs, auto) thus ?thesis unfolding factors_def by auto qed lemma factor: "factor x y ⟷ (∃z. z ≠ 0 ∧ x * z = y)" unfolding factor_def by auto lemma properfactor_nz: shows "(y :: 'a) ≠ 0 ⟹ properfactor x y ⟷ x dvd y ∧ ¬ y dvd x" by (auto simp: properfactor_def factor_def dvd_def) lemma mem_Units[simp]: "y ∈ Units mk_monoid ⟷ y dvd 1" unfolding dvd_def Units_def by (auto simp: ac_simps) end context idom begin lemma irred_0[simp]: "irred (0::'a)" by (unfold Divisibility.irreducible_def, auto simp: factor properfactor_def) lemma factor_idom[simp]: "factor (x::'a) y ⟷ (if y = 0 then x = 0 else x dvd y)" by (cases "y = 0"; auto intro: exI[of _ 1] elim: dvdE simp: factor) lemma associated_connect[simp]: "(∼⇘mk_monoid⇙) = (ddvd)" by (intro ext, unfold associated_def, auto) lemma essentially_equal_connect[simp]: "essentially_equal mk_monoid fs gs ⟷ rel_mset (ddvd) (mset fs) (mset gs)" by (auto simp: essentially_equal_def rel_mset_via_perm) lemma irred_idom_nz: assumes x0: "(x::'a) ≠ 0" shows "irred x ⟷ irreducible x" using x0 by (auto simp: irreducible_altdef Divisibility.irreducible_def properfactor_nz) lemma dvd_dvd_imp_unit_mult: assumes xy: "x dvd y" and yx: "y dvd x" shows "∃z. z dvd 1 ∧ y = x * z" proof(cases "x = 0") case True with xy show ?thesis by (auto intro: exI[of _ 1]) next case x0: False from xy obtain z where z: "y = x * z" by (elim dvdE, auto) from yx obtain w where w: "x = y * w" by (elim dvdE, auto) from z w have "x * (z * w) = x" by (auto simp: ac_simps) then have "z * w = 1" using x0 by auto with z show ?thesis by (auto intro: exI[of _ z]) qed lemma irred_inner_nz: assumes x0: "x ≠ 0" shows "(∀b. b dvd x ⟶ ¬ x dvd b ⟶ b dvd 1) ⟷ (∀a b. x = a * b ⟶ a dvd 1 ∨ b dvd 1)" (is "?l ⟷ ?r") proof (intro iffI allI impI) assume l: ?l fix a b assume xab: "x = a * b" then have ax: "a dvd x" and bx: "b dvd x" by auto { assume a1: "¬ a dvd 1" with l ax have xa: "x dvd a" by auto from dvd_dvd_imp_unit_mult[OF ax xa] obtain z where z1: "z dvd 1" and xaz: "x = a * z" by auto from xab x0 have "a ≠ 0" by auto with xab xaz have "b = z" by auto with z1 have "b dvd 1" by auto } then show "a dvd 1 ∨ b dvd 1" by auto next assume r: ?r fix b assume bx: "b dvd x" and xb: "¬ x dvd b" then obtain a where xab: "x = a * b" by (elim dvdE, auto simp: ac_simps) with r consider "a dvd 1" | "b dvd 1" by auto then show "b dvd 1" proof(cases) case 2 then show ?thesis by auto next case 1 then obtain c where ac1: "a * c = 1" by (elim dvdE, auto) from xab have "x * c = b * (a * c)" by (auto simp: ac_simps) with ac1 have "x * c = b" by auto then have "x dvd b" by auto with xb show ?thesis by auto qed qed lemma irred_idom[simp]: "irred x ⟷ x = 0 ∨ irreducible x" by (cases "x = 0"; simp add: irred_idom_nz irred_inner_nz irreducible_def) lemma assumes "x ≠ 0" and "factors fs x" and "f ∈ set fs" shows "f ≠ 0" using assms by (auto simp: factors) lemma factors_as_mset_factors: assumes x0: "x ≠ 0" and x1: "x ≠ 1" shows "factors fs x ⟷ mset_factors (mset fs) x" using assms by (auto simp: factors prod_mset_prod_list) end context ufd begin interpretation comm_monoid_cancel: comm_monoid_cancel "mk_monoid::'a monoid" apply (unfold_locales) apply simp_all using mult_left_cancel apply (auto simp: ac_simps) done lemma factors_exist: assumes "a ≠ 0" and "¬ a dvd 1" shows "∃fs. set fs ⊆ UNIV - {0} ∧ factors fs a" proof- from mset_factors_exist[OF assms] obtain F where "mset_factors F a" by auto also from ex_mset obtain fs where "F = mset fs" by metis finally have fs: "mset_factors (mset fs) a". then have "factors fs a" using assms by (subst factors_as_mset_factors, auto) moreover have "set fs ⊆ UNIV - {0}" using fs by (auto elim!: mset_factorsE) ultimately show ?thesis by auto qed lemma factors_unique: assumes fs: "factors fs a" and gs: "factors gs a" and a0: "a ≠ 0" and a1: "¬ a dvd 1" shows "rel_mset (ddvd) (mset fs) (mset gs)" proof- from a1 have "a ≠ 1" by auto with a0 fs gs have "mset_factors (mset fs) a" "mset_factors (mset gs) a" by (unfold factors_as_mset_factors) from mset_factors_unique[OF this] show ?thesis. qed lemma factorial_monoid: "factorial_monoid (mk_monoid :: 'a monoid)" by (unfold_locales; auto simp add: factors_exist factors_unique) end lemma (in idom) factorial_monoid_imp_ufd: assumes "factorial_monoid (mk_monoid :: 'a monoid)" shows "class.ufd ((*) :: 'a ⇒ _) 1 (+) 0 (-) uminus" proof (unfold_locales) interpret factorial_monoid "mk_monoid :: 'a monoid" by (fact assms) { fix x assume x: "x ≠ 0" "¬ x dvd 1" note * = factors_exist[simplified, OF this] with x show "∃F. mset_factors F x" by (subst(asm) factors_as_mset_factors, auto) } fix x F G assume FG: "mset_factors F x" "mset_factors G x" with mset_factors_imp_not_is_unit have x1: "¬ x dvd 1" by auto from FG(1) have x0: "x ≠ 0" by (rule mset_factors_imp_nonzero) obtain fs gs where fsgs: "F = mset fs" "G = mset gs" using ex_mset by metis note FG = FG[unfolded this] then have 0: "0 ∉ set fs" "0 ∉ set gs" by (auto elim!: mset_factorsE) from x1 have "x ≠ 1" by auto note FG[folded factors_as_mset_factors[OF x0 this]] from factors_unique[OF this, simplified, OF x0 x1, folded fsgs] 0 show "rel_mset (ddvd) F G" by auto qed subsection ‹Preservation of Irreducibility› locale comm_semiring_1_hom = comm_monoid_mult_hom hom + zero_hom hom for hom :: "'a :: comm_semiring_1 ⇒ 'b :: comm_semiring_1" locale irreducibility_hom = comm_semiring_1_hom + assumes irreducible_imp_irreducible_hom: "irreducible a ⟹ irreducible (hom a)" begin lemma hom_mset_factors: assumes F: "mset_factors F p" shows "mset_factors (image_mset hom F) (hom p)" proof (unfold mset_factors_def, intro conjI allI impI) from F show "hom p = prod_mset (image_mset hom F)" "image_mset hom F ≠ {#}" by (auto simp: hom_distribs) fix f' assume "f' ∈# image_mset hom F" then obtain f where f: "f ∈# F" and f'f: "f' = hom f" by auto with F irreducible_imp_irreducible_hom show "irreducible f'" unfolding f'f by auto qed end locale unit_preserving_hom = comm_semiring_1_hom + assumes is_unit_hom_if: "⋀x. hom x dvd 1 ⟹ x dvd 1" begin lemma is_unit_hom_iff[simp]: "hom x dvd 1 ⟷ x dvd 1" using is_unit_hom_if hom_dvd by force lemma irreducible_hom_imp_irreducible: assumes irr: "irreducible (hom a)" shows "irreducible a" proof (intro irreducibleI) from irr show "a ≠ 0" by auto from irr show "¬ a dvd 1" by (auto dest: irreducible_not_unit) fix b c assume "a = b * c" then have "hom a = hom b * hom c" by (simp add: hom_distribs) with irr have "hom b dvd 1 ∨ hom c dvd 1" by (auto dest: irreducibleD) then show "b dvd 1 ∨ c dvd 1" by simp qed end locale factor_preserving_hom = unit_preserving_hom + irreducibility_hom begin lemma irreducible_hom[simp]: "irreducible (hom a) ⟷ irreducible a" using irreducible_hom_imp_irreducible irreducible_imp_irreducible_hom by metis end lemma factor_preserving_hom_comp: assumes f: "factor_preserving_hom f" and g: "factor_preserving_hom g" shows "factor_preserving_hom (f o g)" proof- interpret f: factor_preserving_hom f by (rule f) interpret g: factor_preserving_hom g by (rule g) show ?thesis by (unfold_locales, auto simp: hom_distribs) qed context comm_semiring_isom begin sublocale unit_preserving_hom by (unfold_locales, auto) sublocale factor_preserving_hom proof (standard) fix a :: 'a assume "irreducible a" note a = this[unfolded irreducible_def] show "irreducible (hom a)" proof (rule ccontr) assume "¬ irreducible (hom a)" from this[unfolded Factorial_Ring.irreducible_def,simplified] a obtain hb hc where eq: "hom a = hb * hc" and nu: "¬ hb dvd 1" "¬ hc dvd 1" by auto from bij obtain b where hb: "hb = hom b" by (elim bij_pointE) from bij obtain c where hc: "hc = hom c" by (elim bij_pointE) from eq[unfolded hb hc, folded hom_mult] have "a = b * c" by auto with nu hb hc have "a = b * c" "¬ b dvd 1" "¬ c dvd 1" by auto with a show False by auto qed qed end subsubsection‹Back to divisibility› lemma(in comm_semiring_1) mset_factors_mult: assumes F: "mset_factors F a" and G: "mset_factors G b" shows "mset_factors (F+G) (a*b)" proof(intro mset_factorsI) fix f assume "f ∈# F + G" then consider "f ∈# F" | "f ∈# G" by auto then show "irreducible f" by(cases, insert F G, auto) qed (insert F G, auto) lemma(in ufd) dvd_imp_subset_factors: assumes ab: "a dvd b" and F: "mset_factors F a" and G: "mset_factors G b" shows "∃G'. G' ⊆# G ∧ rel_mset (ddvd) F G'" proof- from F G have a0: "a ≠ 0" and b0: "b ≠ 0" by (simp_all add: mset_factors_imp_nonzero) from ab obtain c where c: "b = a * c" by (elim dvdE, auto) with b0 have c0: "c ≠ 0" by auto show ?thesis proof(cases "c dvd 1") case True show ?thesis proof(cases F) case empty with F show ?thesis by auto next case (add f F') with F have a: "f * prod_mset F' = a" and F': "⋀f. f ∈# F' ⟹ irreducible f" and irrf: "irreducible f" by auto from irrf have f0: "f ≠ 0" and f1: "¬f dvd 1" by (auto dest: irreducible_not_unit) from a c have "(f * c) * prod_mset F' = b" by (auto simp: ac_simps) moreover { have "irreducible (f * c)" using True irrf by (subst irreducible_mult_unit_right) with F' irrf have "⋀f'. f' ∈# F' + {#f * c#} ⟹ irreducible f'" by auto } ultimately have "mset_factors (F' + {#f * c#}) b" by (intro mset_factorsI, auto) from mset_factors_unique[OF this G] have F'G: "rel_mset (ddvd) (F' + {#f * c#}) G". from True add have FF': "rel_mset (ddvd) F (F' + {#f * c#})" by (auto simp add: multiset.rel_refl intro!: rel_mset_Plus) have "rel_mset (ddvd) F G" apply(rule transpD[OF multiset.rel_transp[OF transpI] FF' F'G]) using ddvd_trans. then show ?thesis by auto qed next case False from mset_factors_exist[OF c0 this] obtain H where H: "mset_factors H c" by auto from c mset_factors_mult[OF F H] have "mset_factors (F + H) b" by auto note mset_factors_unique[OF this G] from rel_mset_split[OF this] obtain G1 G2 where "G = G1 + G2" "rel_mset (ddvd) F G1" "rel_mset (ddvd) H G2" by auto then show ?thesis by (intro exI[of _ "G1"], auto) qed qed lemma(in idom) irreducible_factor_singleton: assumes a: "irreducible a" shows "mset_factors F a ⟷ F = {#a#}" proof(cases F) case empty with mset_factorsD show ?thesis by auto next case (add f F') show ?thesis proof assume F: "mset_factors F a" from add mset_factorsD[OF F] have *: "a = f * prod_mset F'" by auto then have fa: "f dvd a" by auto from * a have f0: "f ≠ 0" by auto from add have "f ∈# F" by auto with F have f: "irreducible f" by auto from add have "F' ⊆# F" by auto then have unitemp: "prod_mset F' dvd 1 ⟹ F' = {#}" proof(induct F') case empty then show ?case by auto next case (add f F') from add have "f ∈# F" by (simp add: mset_subset_eq_insertD) with F irreducible_not_unit have "¬ f dvd 1" by auto then have "¬ (prod_mset F' * f) dvd 1" by simp with add show ?case by auto qed show "F = {#a#}" proof(cases "a dvd f") case True then obtain r where "f = a * r" by (elim dvdE, auto) with * have "f = (r * prod_mset F') * f" by (auto simp: ac_simps) with f0 have "r * prod_mset F' = 1" by auto then have "prod_mset F' dvd 1" by (metis dvd_triv_right) with unitemp * add show ?thesis by auto next case False with fa a f show ?thesis by (auto simp: irreducible_altdef) qed qed (insert a, auto) qed lemma(in ufd) irreducible_dvd_imp_factor: assumes ab: "a dvd b" and a: "irreducible a" and G: "mset_factors G b" shows "∃g ∈# G. a ddvd g" proof- from a have "mset_factors {#a#} a" by auto from dvd_imp_subset_factors[OF ab this G] obtain G' where G'G: "G' ⊆# G" and rel: "rel_mset (ddvd) {#a#} G'" by auto with rel_mset_size size_1_singleton_mset size_single obtain g where gG': "G' = {#g#}" by fastforce from rel[unfolded this rel_mset_def] have "a ddvd g" by auto with gG' G'G show ?thesis by auto qed lemma(in idom) prod_mset_remove_units: "prod_mset F ddvd prod_mset {# f ∈# F. ¬f dvd 1 #}" proof(induct F) case (add f F) then show ?case by (cases "f = 0", auto) qed auto lemma(in comm_semiring_1) mset_factors_imp_dvd: assumes "mset_factors F x" and "f ∈# F" shows "f dvd x" using assms by (simp add: dvd_prod_mset mset_factors_def) lemma(in ufd) prime_elem_iff_irreducible[iff]: "prime_elem x ⟷ irreducible x" proof (intro iffI, fact prime_elem_imp_irreducible, rule prime_elemI) assume r: "irreducible x" then show x0: "x ≠ 0" and x1: "¬ x dvd 1" by (auto dest: irreducible_not_unit) from irreducible_factor_singleton[OF r] have *: "mset_factors {#x#} x" by auto fix a b assume "x dvd a * b" then obtain c where abxc: "a * b = x * c" by (elim dvdE, auto) show "x dvd a ∨ x dvd b" proof(cases "c = 0 ∨ a = 0 ∨ b = 0") case True with abxc show ?thesis by auto next case False then have a0: "a ≠ 0" and b0: "b ≠ 0" and c0: "c ≠ 0" by auto from x0 c0 have xc0: "x * c ≠ 0" by auto from x1 have xc1: "¬ x * c dvd 1" by auto show ?thesis proof (cases "a dvd 1 ∨ b dvd 1") case False then have a1: "¬ a dvd 1" and b1: "¬ b dvd 1" by auto from mset_factors_exist[OF a0 a1] obtain F where Fa: "mset_factors F a" by auto then have F0: "F ≠ {#}" by auto from mset_factors_exist[OF b0 b1] obtain G where Gb: "mset_factors G b" by auto then have G0: "G ≠ {#}" by auto from mset_factors_mult[OF Fa Gb] have FGxc: "mset_factors (F + G) (x * c)" by (simp add: abxc) show ?thesis proof (cases "c dvd 1") case True from r irreducible_mult_unit_right[OF this] have "irreducible (x*c)" by simp note irreducible_factor_singleton[OF this] FGxc with F0 G0 have False by (cases F; cases G; auto) then show ?thesis by auto next case False from mset_factors_exist[OF c0 this] obtain H where "mset_factors H c" by auto with * have xHxc: "mset_factors (add_mset x H) (x * c)" by force note rel = mset_factors_unique[OF this FGxc] obtain hs where "mset hs = H" using ex_mset by auto then have "mset (x#hs) = add_mset x H" by auto from rel_mset_free[OF rel this] obtain jjs where jjsGH: "mset jjs = F + G" and rel: "list_all2 (ddvd) (x # hs) jjs" by auto then obtain j js where jjs: "jjs = j # js" by (cases jjs, auto) with rel have xj: "x ddvd j" by auto from jjs jjsGH have j: "j ∈ set_mset (F + G)" by (intro union_single_eq_member, auto) from j consider "j ∈# F" | "j ∈# G" by auto then show ?thesis proof(cases) case 1 with Fa have "j dvd a" by (auto intro: mset_factors_imp_dvd) with xj dvd_trans have "x dvd a" by auto then show ?thesis by auto next case 2 with Gb have "j dvd b" by (auto intro: mset_factors_imp_dvd) with xj dvd_trans have "x dvd b" by auto then show ?thesis by auto qed qed next case True then consider "a dvd 1" | "b dvd 1" by auto then show ?thesis proof(cases) case 1 then obtain d where ad: "a * d = 1" by (elim dvdE, auto) from abxc have "x * (c * d) = a * b * d" by (auto simp: ac_simps) also have "... = a * d * b" by (auto simp: ac_simps) finally have "x dvd b" by (intro dvdI, auto simp: ad) then show ?thesis by auto next case 2 then obtain d where bd: "b * d = 1" by (elim dvdE, auto) from abxc have "x * (c * d) = a * b * d" by (auto simp: ac_simps) also have "... = (b * d) * a" by (auto simp: ac_simps) finally have "x dvd a" by (intro dvdI, auto simp:bd) then show ?thesis by auto qed qed qed qed subsection‹Results for GCDs etc.› lemma prod_list_remove1: "(x :: 'b :: comm_monoid_mult) ∈ set xs ⟹ prod_list (remove1 x xs) * x = prod_list xs" by (induct xs, auto simp: ac_simps) (* Isabelle 2015-style and generalized gcd-class without normalization and factors *) class comm_monoid_gcd = gcd + comm_semiring_1 + assumes gcd_dvd1[iff]: "gcd a b dvd a" and gcd_dvd2[iff]: "gcd a b dvd b" and gcd_greatest: "c dvd a ⟹ c dvd b ⟹ c dvd gcd a b" begin lemma gcd_0_0[simp]: "gcd 0 0 = 0" using gcd_greatest[OF dvd_0_right dvd_0_right, of 0] by auto lemma gcd_zero_iff[simp]: "gcd a b = 0 ⟷ a = 0 ∧ b = 0" proof assume "gcd a b = 0" from gcd_dvd1[of a b, unfolded this] gcd_dvd2[of a b, unfolded this] show "a = 0 ∧ b = 0" by auto qed auto lemma gcd_zero_iff'[simp]: "0 = gcd a b ⟷ a = 0 ∧ b = 0" using gcd_zero_iff by metis lemma dvd_gcd_0_iff[simp]: shows "x dvd gcd 0 a ⟷ x dvd a" (is ?g1) and "x dvd gcd a 0 ⟷ x dvd a" (is ?g2) proof- have "a dvd gcd a 0" "a dvd gcd 0 a" by (auto intro: gcd_greatest) with dvd_refl show ?g1 ?g2 by (auto dest: dvd_trans) qed lemma gcd_dvd_1[simp]: "gcd a b dvd 1 ⟷ coprime a b" using dvd_trans[OF gcd_greatest[of _ a b], of _ 1] by (cases "a = 0 ∧ b = 0") (auto intro!: coprimeI elim: coprimeE) lemma dvd_imp_gcd_dvd_gcd: "b dvd c ⟹ gcd a b dvd gcd a c" by (meson gcd_dvd1 gcd_dvd2 gcd_greatest dvd_trans) definition listgcd :: "'a list ⇒ 'a" where "listgcd xs = foldr gcd xs 0" lemma listgcd_simps[simp]: "listgcd [] = 0" "listgcd (x # xs) = gcd x (listgcd xs)" by (auto simp: listgcd_def) lemma listgcd: "x ∈ set xs ⟹ listgcd xs dvd x" proof (induct xs) case (Cons y ys) show ?case proof (cases "x = y") case False with Cons have dvd: "listgcd ys dvd x" by auto thus ?thesis unfolding listgcd_simps using dvd_trans by blast next case True thus ?thesis unfolding listgcd_simps using dvd_trans by blast qed qed simp lemma listgcd_greatest: "(⋀ x. x ∈ set xs ⟹ y dvd x) ⟹ y dvd listgcd xs" by (induct xs arbitrary:y, auto intro: gcd_greatest) end context Rings.dvd begin definition "is_gcd x a b ≡ x dvd a ∧ x dvd b ∧ (∀y. y dvd a ⟶ y dvd b ⟶ y dvd x)" definition "some_gcd a b ≡ SOME x. is_gcd x a b" lemma is_gcdI[intro!]: assumes "x dvd a" "x dvd b" "⋀y. y dvd a ⟹ y dvd b ⟹ y dvd x" shows "is_gcd x a b" by (insert assms, auto simp: is_gcd_def) lemma is_gcdE[elim!]: assumes "is_gcd x a b" and "x dvd a ⟹ x dvd b ⟹ (⋀y. y dvd a ⟹ y dvd b ⟹ y dvd x) ⟹ thesis" shows thesis by (insert assms, auto simp: is_gcd_def) lemma is_gcd_some_gcdI: assumes "∃x. is_gcd x a b" shows "is_gcd (some_gcd a b) a b" by (unfold some_gcd_def, rule someI_ex[OF assms]) end context comm_semiring_1 begin lemma some_gcd_0[intro!]: "is_gcd (some_gcd a 0) a 0" "is_gcd (some_gcd 0 b) 0 b" by (auto intro!: is_gcd_some_gcdI intro: exI[of _ a] exI[of _ b]) lemma some_gcd_0_dvd[intro!]: "some_gcd a 0 dvd a" "some_gcd 0 b dvd b" using some_gcd_0 by auto lemma dvd_some_gcd_0[intro!]: "a dvd some_gcd a 0" "b dvd some_gcd 0 b" using some_gcd_0[of a] some_gcd_0[of b] by auto end context idom begin lemma is_gcd_connect: assumes "a ≠ 0" "b ≠ 0" shows "isgcd mk_monoid x a b ⟷ is_gcd x a b" using assms by (force simp: isgcd_def) lemma some_gcd_connect: assumes "a ≠ 0" and "b ≠ 0" shows "somegcd mk_monoid a b = some_gcd a b" using assms by (auto intro!: arg_cong[of _ _ Eps] simp: is_gcd_connect some_gcd_def somegcd_def) end context comm_monoid_gcd begin lemma is_gcd_gcd: "is_gcd (gcd a b) a b" using gcd_greatest by auto lemma is_gcd_some_gcd: "is_gcd (some_gcd a b) a b" by (insert is_gcd_gcd, auto intro!: is_gcd_some_gcdI) lemma gcd_dvd_some_gcd: "gcd a b dvd some_gcd a b" using is_gcd_some_gcd by auto lemma some_gcd_dvd_gcd: "some_gcd a b dvd gcd a b" using is_gcd_some_gcd by (auto intro: gcd_greatest) lemma some_gcd_ddvd_gcd: "some_gcd a b ddvd gcd a b" by (auto intro: gcd_dvd_some_gcd some_gcd_dvd_gcd) lemma some_gcd_dvd: "some_gcd a b dvd d ⟷ gcd a b dvd d" "d dvd some_gcd a b ⟷ d dvd gcd a b" using some_gcd_ddvd_gcd[of a b] by (auto dest:dvd_trans) end class idom_gcd = comm_monoid_gcd + idom begin interpretation raw: comm_monoid_cancel "mk_monoid :: 'a monoid" by (unfold_locales, auto intro: mult_commute mult_assoc) interpretation raw: gcd_condition_monoid "mk_monoid :: 'a monoid" by (unfold_locales, auto simp: is_gcd_connect intro!: exI[of _ "gcd _ _"] dest: gcd_greatest) lemma gcd_mult_ddvd: "d * gcd a b ddvd gcd (d * a) (d * b)" proof (cases "d = 0") case True then show ?thesis by auto next case d0: False show ?thesis proof (cases "a = 0 ∨ b = 0") case False note some_gcd_ddvd_gcd[of a b] with d0 have "d * gcd a b ddvd d * some_gcd a b" by auto also have "d * some_gcd a b ddvd some_gcd (d * a) (d * b)" using False d0 raw.gcd_mult by (simp add: some_gcd_connect) also note some_gcd_ddvd_gcd finally show ?thesis. next case True with d0 show ?thesis apply (elim disjE) apply (rule ddvd_trans[of _ "d * b"]; force) apply (rule ddvd_trans[of _ "d * a"]; force) done qed qed lemma gcd_greatest_mult: assumes cad: "c dvd a * d" and cbd: "c dvd b * d" shows "c dvd gcd a b * d" proof- from gcd_greatest[OF assms] have c: "c dvd gcd (d * a) (d * b)" by (auto simp: ac_simps) note gcd_mult_ddvd[of d a b] then have "gcd (d * a) (d * b) dvd gcd a b * d" by (auto simp: ac_simps) from dvd_trans[OF c this] show ?thesis . qed lemma listgcd_greatest_mult: "(⋀ x :: 'a. x ∈ set xs ⟹ y dvd x * z) ⟹ y dvd listgcd xs * z" proof (induct xs) case (Cons x xs) from Cons have "y dvd x * z" "y dvd listgcd xs * z" by auto thus ?case unfolding listgcd_simps by (rule gcd_greatest_mult) qed (simp) lemma dvd_factor_mult_gcd: assumes dvd: "k dvd p * q" "k dvd p * r" and q0: "q ≠ 0" and r0: "r ≠ 0" shows "k dvd p * gcd q r" proof - from dvd gcd_greatest[of k "p * q" "p * r"] have "k dvd gcd (p * q) (p * r)" by simp also from gcd_mult_ddvd[of p q r] have "... dvd (p * gcd q r)" by auto finally show ?thesis . qed lemma coprime_mult_cross_dvd: assumes coprime: "coprime p q" and eq: "p' * p = q' * q" shows "p dvd q'" (is ?g1) and "q dvd p'" (is ?g2) proof (atomize(full), cases "p = 0 ∨ q = 0") case True then show "?g1 ∧ ?g2" proof assume p0: "p = 0" with coprime have "q dvd 1" by auto with eq p0 show ?thesis by auto next assume q0: "q = 0" with coprime have "p dvd 1" by auto with eq q0 show ?thesis by auto qed next case False { fix p q r p' q' :: 'a assume cop: "coprime p q" and eq: "p' * p = q' * q" and p: "p ≠ 0" and q: "q ≠ 0" and r: "r dvd p" "r dvd q" let ?gcd = "gcd q p" from eq have "p' * p dvd q' * q" by auto hence d1: "p dvd q' * q" by (rule dvd_mult_right) have d2: "p dvd q' * p" by auto from dvd_factor_mult_gcd[OF d1 d2 q p] have 1: "p dvd q' * ?gcd" . from q p have 2: "?gcd dvd q" by auto from q p have 3: "?gcd dvd p" by auto from cop[unfolded coprime_def', rule_format, OF 3 2] have "?gcd dvd 1" . from 1 dvd_mult_unit_iff[OF this] have "p dvd q'" by auto } note main = this from main[OF coprime eq,of 1] False coprime coprime_commute main[OF _ eq[symmetric], of 1] show "?g1 ∧ ?g2" by auto qed end subclass (in ring_gcd) idom_gcd by (unfold_locales, auto) lemma coprime_rewrites: "comm_monoid_mult.coprime ((*)) 1 = coprime" apply (intro ext) apply (subst comm_monoid_mult.coprime_def') apply (unfold_locales) apply (unfold dvd_rewrites) apply (fold coprime_def') .. (* TODO: incorporate into the default class hierarchy *) locale gcd_condition = fixes ty :: "'a :: idom itself" assumes gcd_exists: "⋀a b :: 'a. ∃x. is_gcd x a b" begin sublocale idom_gcd "(*)" "1 :: 'a" "(+)" 0 "(-)" uminus some_gcd rewrites "dvd.dvd ((*)) = (dvd)" and "comm_monoid_mult.coprime ((*) ) 1 = Unique_Factorization.coprime" proof- have "is_gcd (some_gcd a b) a b" for a b :: 'a by (intro is_gcd_some_gcdI gcd_exists) from this[unfolded is_gcd_def] show "class.idom_gcd (*) (1 :: 'a) (+) 0 (-) uminus some_gcd" by (unfold_locales, auto simp: dvd_rewrites) qed (simp_all add: dvd_rewrites coprime_rewrites) end instance semiring_gcd ⊆ comm_monoid_gcd by (intro_classes, auto) lemma listgcd_connect: "listgcd = gcd_list" proof (intro ext) fix xs :: "'a list" show "listgcd xs = gcd_list xs" by(induct xs, auto) qed interpretation some_gcd: gcd_condition "TYPE('a::ufd)" proof(unfold_locales, intro exI) interpret factorial_monoid "mk_monoid :: 'a monoid" by (fact factorial_monoid) note d = dvd.dvd_def some_gcd_def carrier_0 fix a b :: 'a show "is_gcd (some_gcd a b) a b" proof (cases "a = 0 ∨ b = 0") case True thus ?thesis using some_gcd_0 by auto next case False with gcdof_exists[of a b] show ?thesis by (auto intro!: is_gcd_some_gcdI simp add: is_gcd_connect some_gcd_connect) qed qed lemma some_gcd_listgcd_dvd_listgcd: "some_gcd.listgcd xs dvd listgcd xs" by (induct xs, auto simp:some_gcd_dvd intro:dvd_imp_gcd_dvd_gcd) lemma listgcd_dvd_some_gcd_listgcd: "listgcd xs dvd some_gcd.listgcd xs" by (induct xs, auto simp:some_gcd_dvd intro:dvd_imp_gcd_dvd_gcd) context factorial_ring_gcd begin text ‹Do not declare the following as subclass, to avoid conflict in ‹field ⊆ gcd_condition› vs. ‹factorial_ring_gcd ⊆ gcd_condition›. › sublocale as_ufd: ufd proof(unfold_locales, goal_cases) case (1 x) from prime_factorization_exists[OF ‹x ≠ 0›] obtain F where f: "⋀f. f ∈# F ⟹ prime_elem f" and Fx: "normalize (prod_mset F) = normalize x" by auto from associatedE2[OF Fx] obtain u where u: "is_unit u" "x = u * prod_mset F" by blast from ‹¬ is_unit x› Fx have "F ≠ {#}" by auto then obtain g G where F: "F = add_mset g G" by (cases F, auto) then have "g ∈# F" by auto with f[OF this]prime_elem_iff_irreducible irreducible_mult_unit_left[OF unit_factor_is_unit[OF ‹x ≠ 0›]] have g: "irreducible (u * g)" using u(1) by (subst irreducible_mult_unit_left) simp_all show ?case proof (intro exI conjI mset_factorsI) show "prod_mset (add_mset (u * g) G) = x" using ‹x ≠ 0› by (simp add: F ac_simps u) fix f assume "f ∈# add_mset (u * g) G" with f[unfolded F] g prime_elem_iff_irreducible show "irreducible f" by auto qed auto next case (2 x F G) note transpD[OF multiset.rel_transp[OF ddvd_transp],trans] obtain fs where F: "F = mset fs" by (metis ex_mset) have "list_all2 (ddvd) fs (map normalize fs)" by (intro list_all2_all_nthI, auto) then have FH: "rel_mset (ddvd) F (image_mset normalize F)" by (unfold rel_mset_def F, force) also have FG: "image_mset normalize F = image_mset normalize G" proof (intro prime_factorization_unique'') from 2 have xF: "x = prod_mset F" and xG: "x = prod_mset G" by auto from xF have "normalize x = normalize (prod_mset (image_mset normalize F))" by (simp add: normalize_prod_mset_normalize) with xG have nFG: "… = normalize (prod_mset (image_mset normalize G))" by (simp_all add: normalize_prod_mset_normalize) then show "normalize (∏i∈#image_mset normalize F. i) = normalize (∏i∈#image_mset normalize G. i)" by auto next from 2 prime_elem_iff_irreducible have "f ∈# F ⟹ prime_elem f" "g ∈# G ⟹ prime_elem g" for f g by (auto intro: prime_elemI) then show " Multiset.Ball (image_mset normalize F) prime" "Multiset.Ball (image_mset normalize G) prime" by auto qed also obtain gs where G: "G = mset gs" by (metis ex_mset) have "list_all2 ((ddvd)¯¯) gs (map normalize gs)" by (intro list_all2_all_nthI, auto) then have "rel_mset (ddvd) (image_mset normalize G) G" by (subst multiset.rel_flip[symmetric], unfold rel_mset_def G, force) finally show ?case. qed end instance int :: ufd by (intro ufd.intro_of_class as_ufd.ufd_axioms) instance int :: idom_gcd by (intro_classes, auto) instance field ⊆ ufd by (intro_classes, auto simp: dvd_field_iff) end