(* Authors: Jose Divasón Sebastiaan Joosten René Thiemann Akihisa Yamada *) section ‹Polynomials in Rings and Fields› subsection ‹Polynomials in Rings› text ‹We use a locale to work with polynomials in some integer-modulo ring.› theory Poly_Mod imports "HOL-Computational_Algebra.Primes" Polynomial_Factorization.Square_Free_Factorization Unique_Factorization_Poly begin locale poly_mod = fixes m :: "int" begin definition M :: "int ⇒ int" where "M x = x mod m" lemma M_0[simp]: "M 0 = 0" by (auto simp add: M_def) lemma M_M[simp]: "M (M x) = M x" by (auto simp add: M_def) lemma M_plus[simp]: "M (M x + y) = M (x + y)" "M (x + M y) = M (x + y)" by (auto simp add: M_def mod_simps) lemma M_minus[simp]: "M (M x - y) = M (x - y)" "M (x - M y) = M (x - y)" by (auto simp add: M_def mod_simps) lemma M_times[simp]: "M (M x * y) = M (x * y)" "M (x * M y) = M (x * y)" by (auto simp add: M_def mod_simps) lemma M_sum: "M (sum (λ x. M (f x)) A) = M (sum f A)" proof (induct A rule: infinite_finite_induct) case (insert x A) from insert(1-2) have "M (∑x∈insert x A. M (f x)) = M (f x + M ((∑x∈A. M (f x))))" by simp also have "M ((∑x∈A. M (f x))) = M ((∑x∈A. f x))" using insert by simp finally show ?case using insert by simp qed auto definition inv_M :: "int ⇒ int" where "inv_M = (λ x. if x + x ≤ m then x else x - m)" lemma M_inv_M_id[simp]: "M (inv_M x) = M x" unfolding inv_M_def M_def by simp definition Mp :: "int poly ⇒ int poly" where "Mp = map_poly M" lemma Mp_0[simp]: "Mp 0 = 0" unfolding Mp_def by auto lemma Mp_coeff: "coeff (Mp f) i = M (coeff f i)" unfolding Mp_def by (simp add: M_def coeff_map_poly) abbreviation eq_m :: "int poly ⇒ int poly ⇒ bool" (infixl "=m" 50) where "f =m g ≡ (Mp f = Mp g)" notation eq_m (infixl "=m" 50) abbreviation degree_m :: "int poly ⇒ nat" where "degree_m f ≡ degree (Mp f)" lemma mult_Mp[simp]: "Mp (Mp f * g) = Mp (f * g)" "Mp (f * Mp g) = Mp (f * g)" proof - { fix f g have "Mp (Mp f * g) = Mp (f * g)" unfolding poly_eq_iff Mp_coeff unfolding coeff_mult Mp_coeff proof fix n show "M (∑i≤n. M (coeff f i) * coeff g (n - i)) = M (∑i≤n. coeff f i * coeff g (n - i))" by (subst M_sum[symmetric], rule sym, subst M_sum[symmetric], unfold M_times, simp) qed } from this[of f g] this[of g f] show "Mp (Mp f * g) = Mp (f * g)" "Mp (f * Mp g) = Mp (f * g)" by (auto simp: ac_simps) qed lemma plus_Mp[simp]: "Mp (Mp f + g) = Mp (f + g)" "Mp (f + Mp g) = Mp (f + g)" unfolding poly_eq_iff Mp_coeff unfolding coeff_mult Mp_coeff by (auto simp add: Mp_coeff) lemma minus_Mp[simp]: "Mp (Mp f - g) = Mp (f - g)" "Mp (f - Mp g) = Mp (f - g)" unfolding poly_eq_iff Mp_coeff unfolding coeff_mult Mp_coeff by (auto simp add: Mp_coeff) lemma Mp_smult[simp]: "Mp (smult (M a) f) = Mp (smult a f)" "Mp (smult a (Mp f)) = Mp (smult a f)" unfolding Mp_def smult_as_map_poly by (rule poly_eqI, auto simp: coeff_map_poly)+ lemma Mp_Mp[simp]: "Mp (Mp f) = Mp f" unfolding Mp_def by (intro poly_eqI, auto simp: coeff_map_poly) lemma Mp_smult_m_0[simp]: "Mp (smult m f) = 0" by (intro poly_eqI, auto simp: Mp_coeff, auto simp: M_def) definition dvdm :: "int poly ⇒ int poly ⇒ bool" (infix "dvdm" 50) where "f dvdm g = (∃ h. g =m f * h)" notation dvdm (infix "dvdm" 50) lemma dvdmE: assumes fg: "f dvdm g" and main: "⋀h. g =m f * h ⟹ Mp h = h ⟹ thesis" shows "thesis" proof- from fg obtain h where "g =m f * h" by (auto simp: dvdm_def) then have "g =m f * Mp h" by auto from main[OF this] show thesis by auto qed lemma Mp_dvdm[simp]: "Mp f dvdm g ⟷ f dvdm g" and dvdm_Mp[simp]: "f dvdm Mp g ⟷ f dvdm g" by (auto simp: dvdm_def) definition irreducible_m where "irreducible_m f = (¬f =m 0 ∧ ¬ f dvdm 1 ∧ (∀a b. f =m a * b ⟶ a dvdm 1 ∨ b dvdm 1))" definition irreducible⇩_{d}_m :: "int poly ⇒ bool" where "irreducible⇩_{d}_m f ≡ degree_m f > 0 ∧ (∀ g h. degree_m g < degree_m f ⟶ degree_m h < degree_m f ⟶ ¬ f =m g * h)" definition prime_elem_m where "prime_elem_m f ≡ ¬ f =m 0 ∧ ¬ f dvdm 1 ∧ (∀g h. f dvdm g * h ⟶ f dvdm g ∨ f dvdm h)" lemma degree_m_le_degree [intro!]: "degree_m f ≤ degree f" by (simp add: Mp_def degree_map_poly_le) lemma irreducible⇩_{d}_mI: assumes f0: "degree_m f > 0" and main: "⋀g h. Mp g = g ⟹ Mp h = h ⟹ degree g > 0 ⟹ degree g < degree_m f ⟹ degree h > 0 ⟹ degree h < degree_m f ⟹ f =m g * h ⟹ False" shows "irreducible⇩_{d}_m f" proof (unfold irreducible⇩_{d}_m_def, intro conjI allI impI f0 notI) fix g h assume deg: "degree_m g < degree_m f" "degree_m h < degree_m f" and "f =m g * h" then have f: "f =m Mp g * Mp h" by simp have "degree_m f ≤ degree_m g + degree_m h" unfolding f using degree_mult_le order.trans by blast with main[of "Mp g" "Mp h"] deg f show False by auto qed lemma irreducible⇩_{d}_mE: assumes "irreducible⇩_{d}_m f" and "degree_m f > 0 ⟹ (⋀g h. degree_m g < degree_m f ⟹ degree_m h < degree_m f ⟹ ¬ f =m g * h) ⟹ thesis" shows thesis using assms by (unfold irreducible⇩_{d}_m_def, auto) lemma irreducible⇩_{d}_mD: assumes "irreducible⇩_{d}_m f" shows "degree_m f > 0" and "⋀g h. degree_m g < degree_m f ⟹ degree_m h < degree_m f ⟹ ¬ f =m g * h" using assms by (auto elim: irreducible⇩_{d}_mE) definition square_free_m :: "int poly ⇒ bool" where "square_free_m f = (¬ f =m 0 ∧ (∀ g. degree_m g ≠ 0 ⟶ ¬ (g * g dvdm f)))" definition coprime_m :: "int poly ⇒ int poly ⇒ bool" where "coprime_m f g = (∀ h. h dvdm f ⟶ h dvdm g ⟶ h dvdm 1)" lemma Mp_square_free_m[simp]: "square_free_m (Mp f) = square_free_m f" unfolding square_free_m_def dvdm_def by simp lemma square_free_m_cong: "square_free_m f ⟹ Mp f = Mp g ⟹ square_free_m g" unfolding square_free_m_def dvdm_def by simp lemma Mp_prod_mset[simp]: "Mp (prod_mset (image_mset Mp b)) = Mp (prod_mset b)" proof (induct b) case (add x b) have "Mp (prod_mset (image_mset Mp ({#x#}+b))) = Mp (Mp x * prod_mset (image_mset Mp b))" by simp also have "… = Mp (Mp x * Mp (prod_mset (image_mset Mp b)))" by simp also have "… = Mp ( Mp x * Mp (prod_mset b))" unfolding add by simp finally show ?case by simp qed simp lemma Mp_prod_list: "Mp (prod_list (map Mp b)) = Mp (prod_list b)" proof (induct b) case (Cons b xs) have "Mp (prod_list (map Mp (b # xs))) = Mp (Mp b * prod_list (map Mp xs))" by simp also have "… = Mp (Mp b * Mp (prod_list (map Mp xs)))" by simp also have "… = Mp (Mp b * Mp (prod_list xs))" unfolding Cons by simp finally show ?case by simp qed simp text ‹Polynomial evaluation modulo› definition "M_poly p x ≡ M (poly p x)" lemma M_poly_Mp[simp]: "M_poly (Mp p) = M_poly p" proof(intro ext, induct p) case 0 show ?case by auto next case IH: (pCons a p) from IH(1) have "M_poly (Mp (pCons a p)) x = M (a + M(x * M_poly (Mp p) x))" by (simp add: M_poly_def Mp_def) also note IH(2)[of x] finally show ?case by (simp add: M_poly_def) qed lemma Mp_lift_modulus: assumes "f =m g" shows "poly_mod.eq_m (m * k) (smult k f) (smult k g)" using assms unfolding poly_eq_iff poly_mod.Mp_coeff coeff_smult unfolding poly_mod.M_def by simp lemma Mp_ident_product: "n > 0 ⟹ Mp f = f ⟹ poly_mod.Mp (m * n) f = f" unfolding poly_eq_iff poly_mod.Mp_coeff poly_mod.M_def by (auto simp add: zmod_zmult2_eq) (metis mod_div_trivial mod_0) lemma Mp_shrink_modulus: assumes "poly_mod.eq_m (m * k) f g" "k ≠ 0" shows "f =m g" proof - from assms have a: "⋀ n. coeff f n mod (m * k) = coeff g n mod (m * k)" unfolding poly_eq_iff poly_mod.Mp_coeff unfolding poly_mod.M_def by auto show ?thesis unfolding poly_eq_iff poly_mod.Mp_coeff unfolding poly_mod.M_def proof fix n show "coeff f n mod m = coeff g n mod m" using a[of n] ‹k ≠ 0› by (metis mod_mult_right_eq mult.commute mult_cancel_left mult_mod_right) qed qed lemma degree_m_le: "degree_m f ≤ degree f" unfolding Mp_def by (rule degree_map_poly_le) lemma degree_m_eq: "coeff f (degree f) mod m ≠ 0 ⟹ m > 1 ⟹ degree_m f = degree f" using degree_m_le[of f] unfolding Mp_def by (auto intro: degree_map_poly simp: Mp_def poly_mod.M_def) lemma degree_m_mult_le: assumes eq: "f =m g * h" shows "degree_m f ≤ degree_m g + degree_m h" proof - have "degree_m f = degree_m (Mp g * Mp h)" using eq by simp also have "… ≤ degree (Mp g * Mp h)" by (rule degree_m_le) also have "… ≤ degree_m g + degree_m h" by (rule degree_mult_le) finally show ?thesis by auto qed lemma degree_m_smult_le: "degree_m (smult c f) ≤ degree_m f" by (metis Mp_0 coeff_0 degree_le degree_m_le degree_smult_eq poly_mod.Mp_smult(2) smult_eq_0_iff) lemma irreducible_m_Mp[simp]: "irreducible_m (Mp f) ⟷ irreducible_m f" by (simp add: irreducible_m_def) lemma eq_m_irreducible_m: "f =m g ⟹ irreducible_m f ⟷ irreducible_m g" using irreducible_m_Mp by metis definition mset_factors_m where "mset_factors_m F p ≡ F ≠ {#} ∧ (∀f. f ∈# F ⟶ irreducible_m f) ∧ p =m prod_mset F" end declare poly_mod.M_def[code] declare poly_mod.Mp_def[code] declare poly_mod.inv_M_def[code] definition Irr_Mon :: "'a :: comm_semiring_1 poly set" where "Irr_Mon = {x. irreducible x ∧ monic x}" definition factorization :: "'a :: comm_semiring_1 poly set ⇒ 'a poly ⇒ ('a × 'a poly multiset) ⇒ bool" where "factorization Factors f cfs ≡ (case cfs of (c,fs) ⇒ f = (smult c (prod_mset fs)) ∧ (set_mset fs ⊆ Factors))" definition unique_factorization :: "'a :: comm_semiring_1 poly set ⇒ 'a poly ⇒ ('a × 'a poly multiset) ⇒ bool" where "unique_factorization Factors f cfs = (Collect (factorization Factors f) = {cfs})" lemma irreducible_multD: assumes l: "irreducible (a*b)" shows "a dvd 1 ∧ irreducible b ∨ b dvd 1 ∧ irreducible a" proof- from l have "a dvd 1 ∨ b dvd 1" by auto then show ?thesis proof(elim disjE) assume a: "a dvd 1" with l have "irreducible b" unfolding irreducible_def by (meson is_unit_mult_iff mult.left_commute mult_not_zero) with a show ?thesis by auto next assume a: "b dvd 1" with l have "irreducible a" unfolding irreducible_def by (meson is_unit_mult_iff mult_not_zero semiring_normalization_rules(16)) with a show ?thesis by auto qed qed lemma irreducible_dvd_prod_mset: fixes p :: "'a :: field poly" assumes irr: "irreducible p" and dvd: "p dvd prod_mset as" shows "∃ a ∈# as. p dvd a" proof - from irr[unfolded irreducible_def] have deg: "degree p ≠ 0" by auto hence p1: "¬ p dvd 1" unfolding dvd_def by (metis degree_1 nonzero_mult_div_cancel_left div_poly_less linorder_neqE_nat mult_not_zero not_less0 zero_neq_one) from dvd show ?thesis proof (induct as) case (add a as) hence "prod_mset (add_mset a as) = a * prod_mset as" by auto from add(2)[unfolded this] add(1) irr show ?case by auto qed (insert p1, auto) qed lemma monic_factorization_unique_mset: fixes P::"'a::field poly multiset" assumes eq: "prod_mset P = prod_mset Q" and P: "set_mset P ⊆ {q. irreducible q ∧ monic q}" and Q: "set_mset Q ⊆ {q. irreducible q ∧ monic q}" shows "P = Q" proof - { fix P Q :: "'a poly multiset" assume id: "prod_mset P = prod_mset Q" and P: "set_mset P ⊆ {q. irreducible q ∧ monic q}" and Q: "set_mset Q ⊆ {q. irreducible q ∧ monic q}" hence "P ⊆# Q" proof (induct P arbitrary: Q) case (add x P Q') from add(3) have irr: "irreducible x" and mon: "monic x" by auto have "∃ a ∈# Q'. x dvd a" proof (rule irreducible_dvd_prod_mset[OF irr]) show "x dvd prod_mset Q'" unfolding add(2)[symmetric] by simp qed then obtain y Q where Q': "Q' = add_mset y Q" and xy: "x dvd y" by (meson mset_add) from add(4) Q' have irr': "irreducible y" and mon': "monic y" by auto have "x = y" using irr irr' xy mon mon' by (metis irreducibleD' irreducible_not_unit poly_dvd_antisym) hence Q': "Q' = Q + {#x#}" using Q' by auto from mon have x0: "x ≠ 0" by auto from arg_cong[OF add(2)[unfolded Q'], of "λ z. z div x"] have eq: "prod_mset P = prod_mset Q" using x0 by auto from add(3-4)[unfolded Q'] have "set_mset P ⊆ {q. irreducible q ∧ monic q}" "set_mset Q ⊆ {q. irreducible q ∧ monic q}" by auto from add(1)[OF eq this] show ?case unfolding Q' by auto qed auto } from this[OF eq P Q] this[OF eq[symmetric] Q P] show ?thesis by auto qed lemma exactly_one_monic_factorization: assumes mon: "monic (f :: 'a :: field poly)" shows "∃! fs. f = prod_mset fs ∧ set_mset fs ⊆ {q. irreducible q ∧ monic q}" proof - from monic_irreducible_factorization[OF mon] obtain gs g where fin: "finite gs" and f: "f = (∏a∈gs. a ^ Suc (g a))" and gs: "gs ⊆ {q. irreducible q ∧ monic q}" by blast from fin have "∃ fs. set_mset fs ⊆ gs ∧ prod_mset fs = (∏a∈gs. a ^ Suc (g a))" proof (induct gs) case (insert a gs) from insert(3) obtain fs where *: "set_mset fs ⊆ gs" "prod_mset fs = (∏a∈gs. a ^ Suc (g a))" by auto let ?fs = "fs + replicate_mset (Suc (g a)) a" show ?case proof (rule exI[of _ "fs + replicate_mset (Suc (g a)) a"], intro conjI) show "set_mset ?fs ⊆ insert a gs" using *(1) by auto show "prod_mset ?fs = (∏a∈insert a gs. a ^ Suc (g a))" by (subst prod.insert[OF insert(1-2)], auto simp: *(2)) qed qed simp then obtain fs where "set_mset fs ⊆ gs" "prod_mset fs = (∏a∈gs. a ^ Suc (g a))" by auto with gs f have ex: "∃fs. f = prod_mset fs ∧ set_mset fs ⊆ {q. irreducible q ∧ monic q}" by (intro exI[of _ fs], auto) thus ?thesis using monic_factorization_unique_mset by blast qed lemma monic_prod_mset: fixes as :: "'a :: idom poly multiset" assumes "⋀ a. a ∈ set_mset as ⟹ monic a" shows "monic (prod_mset as)" using assms by (induct as, auto intro: monic_mult) lemma exactly_one_factorization: assumes f: "f ≠ (0 :: 'a :: field poly)" shows "∃! cfs. factorization Irr_Mon f cfs" proof - let ?a = "coeff f (degree f)" let ?b = "inverse ?a" let ?g = "smult ?b f" define g where "g = ?g" from f have a: "?a ≠ 0" "?b ≠ 0" by (auto simp: field_simps) hence "monic g" unfolding g_def by simp note ex1 = exactly_one_monic_factorization[OF this, folded Irr_Mon_def] then obtain fs where g: "g = prod_mset fs" "set_mset fs ⊆ Irr_Mon" by auto let ?cfs = "(?a,fs)" have cfs: "factorization Irr_Mon f ?cfs" unfolding factorization_def split g(1)[symmetric] using g(2) unfolding g_def by (simp add: a field_simps) show ?thesis proof (rule, rule cfs) fix dgs assume fact: "factorization Irr_Mon f dgs" obtain d gs where dgs: "dgs = (d,gs)" by force from fact[unfolded factorization_def dgs split] have fd: "f = smult d (prod_mset gs)" and gs: "set_mset gs ⊆ Irr_Mon" by auto have "monic (prod_mset gs)" by (rule monic_prod_mset, insert gs[unfolded Irr_Mon_def], auto) hence d: "d = ?a" unfolding fd by auto from arg_cong[OF fd, of "λ x. smult ?b x", unfolded d g_def[symmetric]] have "g = prod_mset gs" using a by (simp add: field_simps) with ex1 g gs have "gs = fs" by auto thus "dgs = ?cfs" unfolding dgs d by auto qed qed lemma mod_ident_iff: "m > 0 ⟹ (x :: int) mod m = x ⟷ x ∈ {0 ..< m}" by (metis Divides.pos_mod_bound Divides.pos_mod_sign atLeastLessThan_iff mod_pos_pos_trivial) declare prod_mset_prod_list[simp] lemma mult_1_is_id[simp]: "(*) (1 :: 'a :: ring_1) = id" by auto context poly_mod begin lemma degree_m_eq_monic: "monic f ⟹ m > 1 ⟹ degree_m f = degree f" by (rule degree_m_eq) auto lemma monic_degree_m_lift: assumes "monic f" "k > 1" "m > 1" shows "monic (poly_mod.Mp (m * k) f)" proof - have deg: "degree (poly_mod.Mp (m * k) f) = degree f" by (rule poly_mod.degree_m_eq_monic[of f "m * k"], insert assms, auto simp: less_1_mult) show ?thesis unfolding poly_mod.Mp_coeff deg assms poly_mod.M_def using assms(2-) by (simp add: less_1_mult) qed end locale poly_mod_2 = poly_mod m for m + assumes m1: "m > 1" begin lemma M_1[simp]: "M 1 = 1" unfolding M_def using m1 by auto lemma Mp_1[simp]: "Mp 1 = 1" unfolding Mp_def by simp lemma monic_degree_m[simp]: "monic f ⟹ degree_m f = degree f" using degree_m_eq_monic[of f] using m1 by auto lemma monic_Mp: "monic f ⟹ monic (Mp f)" by (auto simp: Mp_coeff) lemma Mp_0_smult_sdiv_poly: assumes "Mp f = 0" shows "smult m (sdiv_poly f m) = f" proof (intro poly_eqI, unfold Mp_coeff coeff_smult sdiv_poly_def, subst coeff_map_poly, force) fix n from assms have "coeff (Mp f) n = 0" by simp hence 0: "coeff f n mod m = 0" unfolding Mp_coeff M_def . thus "m * (coeff f n div m) = coeff f n" by auto qed lemma Mp_product_modulus: "m' = m * k ⟹ k > 0 ⟹ Mp (poly_mod.Mp m' f) = Mp f" by (intro poly_eqI, unfold poly_mod.Mp_coeff poly_mod.M_def, auto simp: mod_mod_cancel) lemma inv_M_rev: assumes bnd: "2 * abs c < m" shows "inv_M (M c) = c" proof (cases "c ≥ 0") case True with bnd show ?thesis unfolding M_def inv_M_def by auto next case False have 2: "⋀ v :: int. 2 * v = v + v" by auto from False have c: "c < 0" by auto from bnd c have "c + m > 0" "c + m < m" by auto with c have cm: "c mod m = c + m" by (metis le_less mod_add_self2 mod_pos_pos_trivial) from c bnd have "2 * (c mod m) > m" unfolding cm by auto with bnd c show ?thesis unfolding M_def inv_M_def cm by auto qed end lemma (in poly_mod) degree_m_eq_prime: assumes f0: "Mp f ≠ 0" and deg: "degree_m f = degree f" and eq: "f =m g * h" and p: "prime m" shows "degree_m f = degree_m g + degree_m h" proof - interpret poly_mod_2 m using prime_ge_2_int[OF p] unfolding poly_mod_2_def by simp from f0 eq have "Mp (Mp g * Mp h) ≠ 0" by auto hence "Mp g * Mp h ≠ 0" using Mp_0 by (cases "Mp g * Mp h", auto) hence g0: "Mp g ≠ 0" and h0: "Mp h ≠ 0" by auto have "degree (Mp (g * h)) = degree_m (Mp g * Mp h)" by simp also have "… = degree (Mp g * Mp h)" proof (rule degree_m_eq[OF _ m1], rule) have id: "⋀ g. coeff (Mp g) (degree (Mp g)) mod m = coeff (Mp g) (degree (Mp g))" unfolding M_def[symmetric] Mp_coeff by simp from p have p': "prime m" unfolding prime_int_nat_transfer unfolding prime_nat_iff by auto assume "coeff (Mp g * Mp h) (degree (Mp g * Mp h)) mod m = 0" from this[unfolded coeff_degree_mult] have "coeff (Mp g) (degree (Mp g)) mod m = 0 ∨ coeff (Mp h) (degree (Mp h)) mod m = 0" unfolding dvd_eq_mod_eq_0[symmetric] using m1 prime_dvd_mult_int[OF p'] by auto with g0 h0 show False unfolding id by auto qed also have "… = degree (Mp g) + degree (Mp h)" by (rule degree_mult_eq[OF g0 h0]) finally show ?thesis using eq by simp qed lemma monic_smult_add_small: assumes "f = 0 ∨ degree f < degree g" and mon: "monic g" shows "monic (g + smult q f)" proof (cases "f = 0") case True thus ?thesis using mon by auto next case False with assms have "degree f < degree g" by auto hence "degree (smult q f) < degree g" by (meson degree_smult_le not_less order_trans) thus ?thesis using mon using coeff_eq_0 degree_add_eq_left by fastforce qed context poly_mod begin definition factorization_m :: "int poly ⇒ (int × int poly multiset) ⇒ bool" where "factorization_m f cfs ≡ (case cfs of (c,fs) ⇒ f =m (smult c (prod_mset fs)) ∧ (∀ f ∈ set_mset fs. irreducible⇩_{d}_m f ∧ monic (Mp f)))" definition Mf :: "int × int poly multiset ⇒ int × int poly multiset" where "Mf cfs ≡ case cfs of (c,fs) ⇒ (M c, image_mset Mp fs)" lemma Mf_Mf[simp]: "Mf (Mf x) = Mf x" proof (cases x, auto simp: Mf_def, goal_cases) case (1 c fs) show ?case by (induct fs, auto) qed definition equivalent_fact_m :: "int × int poly multiset ⇒ int × int poly multiset ⇒ bool" where "equivalent_fact_m cfs dgs = (Mf cfs = Mf dgs)" definition unique_factorization_m :: "int poly ⇒ (int × int poly multiset) ⇒ bool" where "unique_factorization_m f cfs = (Mf ` Collect (factorization_m f) = {Mf cfs})" lemma Mp_irreducible⇩_{d}_m[simp]: "irreducible⇩_{d}_m (Mp f) = irreducible⇩_{d}_m f" unfolding irreducible⇩_{d}_m_def dvdm_def by simp lemma Mf_factorization_m[simp]: "factorization_m f (Mf cfs) = factorization_m f cfs" unfolding factorization_m_def Mf_def proof (cases cfs, simp, goal_cases) case (1 c fs) have "Mp (smult c (prod_mset fs)) = Mp (smult (M c) (Mp (prod_mset fs)))" by simp also have "… = Mp (smult (M c) (Mp (prod_mset (image_mset Mp fs))))" unfolding Mp_prod_mset by simp also have "… = Mp (smult (M c) (prod_mset (image_mset Mp fs)))" unfolding Mp_smult .. finally show ?case by auto qed lemma unique_factorization_m_imp_factorization: assumes "unique_factorization_m f cfs" shows "factorization_m f cfs" proof - from assms[unfolded unique_factorization_m_def] obtain dfs where fact: "factorization_m f dfs" and id: "Mf cfs = Mf dfs" by blast from fact have "factorization_m f (Mf dfs)" by simp from this[folded id] show ?thesis by simp qed lemma unique_factorization_m_alt_def: "unique_factorization_m f cfs = (factorization_m f cfs ∧ (∀ dgs. factorization_m f dgs ⟶ Mf dgs = Mf cfs))" using unique_factorization_m_imp_factorization[of f cfs] unfolding unique_factorization_m_def by auto end context poly_mod_2 begin lemma factorization_m_lead_coeff: assumes "factorization_m f (c,fs)" shows "lead_coeff (Mp f) = M c" proof - note * = assms[unfolded factorization_m_def split] have "monic (prod_mset (image_mset Mp fs))" by (rule monic_prod_mset, insert *, auto) hence "monic (Mp (prod_mset (image_mset Mp fs)))" by (rule monic_Mp) from this[unfolded Mp_prod_mset] have monic: "monic (Mp (prod_mset fs))" by simp from * have "lead_coeff (Mp f) = lead_coeff (Mp (smult c (prod_mset fs)))" by simp also have "Mp (smult c (prod_mset fs)) = Mp (smult (M c) (Mp (prod_mset fs)))" by simp finally show ?thesis using monic ‹smult c (prod_mset fs) =m smult (M c) (Mp (prod_mset fs))› by (metis M_M M_def Mp_0 Mp_coeff lead_coeff_smult m1 mult_cancel_left2 poly_mod.degree_m_eq smult_eq_0_iff) qed lemma factorization_m_smult: assumes "factorization_m f (c,fs)" shows "factorization_m (smult d f) (c * d,fs)" proof - note * = assms[unfolded factorization_m_def split] from * have f: "Mp f = Mp (smult c (prod_mset fs))" by simp have "Mp (smult d f) = Mp (smult d (Mp f))" by simp also have "… = Mp (smult (c * d) (prod_mset fs))" unfolding f by (simp add: ac_simps) finally show ?thesis using assms unfolding factorization_m_def split by auto qed lemma factorization_m_prod: assumes "factorization_m f (c,fs)" "factorization_m g (d,gs)" shows "factorization_m (f * g) (c * d, fs + gs)" proof - note * = assms[unfolded factorization_m_def split] have "Mp (f * g) = Mp (Mp f * Mp g)" by simp also have "Mp f = Mp (smult c (prod_mset fs))" using * by simp also have "Mp g = Mp (smult d (prod_mset gs))" using * by simp finally have "Mp (f * g) = Mp (smult (c * d) (prod_mset (fs + gs)))" unfolding mult_Mp by (simp add: ac_simps) with * show ?thesis unfolding factorization_m_def split by auto qed lemma Mp_factorization_m[simp]: "factorization_m (Mp f) cfs = factorization_m f cfs" unfolding factorization_m_def by simp lemma Mp_unique_factorization_m[simp]: "unique_factorization_m (Mp f) cfs = unique_factorization_m f cfs" unfolding unique_factorization_m_alt_def by simp lemma unique_factorization_m_cong: "unique_factorization_m f cfs ⟹ Mp f = Mp g ⟹ unique_factorization_m g cfs" unfolding Mp_unique_factorization_m[of f, symmetric] by simp lemma unique_factorization_mI: assumes "factorization_m f (c,fs)" and "⋀ d gs. factorization_m f (d,gs) ⟹ Mf (d,gs) = Mf (c,fs)" shows "unique_factorization_m f (c,fs)" unfolding unique_factorization_m_alt_def by (intro conjI[OF assms(1)] allI impI, insert assms(2), auto) lemma unique_factorization_m_smult: assumes uf: "unique_factorization_m f (c,fs)" and d: "M (di * d) = 1" shows "unique_factorization_m (smult d f) (c * d,fs)" proof (rule unique_factorization_mI[OF factorization_m_smult]) show "factorization_m f (c, fs)" using uf[unfolded unique_factorization_m_alt_def] by auto fix e gs assume fact: "factorization_m (smult d f) (e,gs)" from factorization_m_smult[OF this, of di] have "factorization_m (Mp (smult di (smult d f))) (e * di, gs)" by simp also have "Mp (smult di (smult d f)) = Mp (smult (M (di * d)) f)" by simp also have "… = Mp f" unfolding d by simp finally have fact: "factorization_m f (e * di, gs)" by simp with uf[unfolded unique_factorization_m_alt_def] have eq: "Mf (e * di, gs) = Mf (c, fs)" by blast from eq[unfolded Mf_def] have "M (e * di) = M c" by simp from arg_cong[OF this, of "λ x. M (x * d)"] have "M (e * M (di * d)) = M (c * d)" by (simp add: ac_simps) from this[unfolded d] have e: "M e = M (c * d)" by simp with eq show "Mf (e,gs) = Mf (c * d, fs)" unfolding Mf_def split by simp qed lemma unique_factorization_m_smultD: assumes uf: "unique_factorization_m (smult d f) (c,fs)" and d: "M (di * d) = 1" shows "unique_factorization_m f (c * di,fs)" proof - from d have d': "M (d * di) = 1" by (simp add: ac_simps) show ?thesis proof (rule unique_factorization_m_cong[OF unique_factorization_m_smult[OF uf d']], rule poly_eqI, unfold Mp_coeff coeff_smult) fix n have "M (di * (d * coeff f n)) = M (M (di * d) * coeff f n)" by (auto simp: ac_simps) from this[unfolded d] show "M (di * (d * coeff f n)) = M (coeff f n)" by simp qed qed lemma degree_m_eq_lead_coeff: "degree_m f = degree f ⟹ lead_coeff (Mp f) = M (lead_coeff f)" by (simp add: Mp_coeff) lemma unique_factorization_m_zero: assumes "unique_factorization_m f (c,fs)" shows "M c ≠ 0" proof assume c: "M c = 0" from unique_factorization_m_imp_factorization[OF assms] have "Mp f = Mp (smult (M c) (prod_mset fs))" unfolding factorization_m_def split by simp from this[unfolded c] have f: "Mp f = 0" by simp have "factorization_m f (0,{#})" unfolding factorization_m_def split f by auto moreover have "Mf (0,{#}) = (0,{#})" unfolding Mf_def by auto ultimately have fact1: "(0, {#}) ∈ Mf ` Collect (factorization_m f)" by force define g :: "int poly" where "g = [:0,1:]" have mpg: "Mp g = [:0,1:]" unfolding Mp_def by (auto simp: g_def) { fix g h assume *: "degree (Mp g) = 0" "degree (Mp h) = 0" "[:0, 1:] = Mp (g * h)" from arg_cong[OF *(3), of degree] have "1 = degree_m (Mp g * Mp h)" by simp also have "… ≤ degree (Mp g * Mp h)" by (rule degree_m_le) also have "… ≤ degree (Mp g) + degree (Mp h)" by (rule degree_mult_le) also have "… ≤ 0" using * by simp finally have False by simp } note irr = this have "factorization_m f (0,{# g #})" unfolding factorization_m_def split using irr by (auto simp: irreducible⇩_{d}_m_def f mpg) moreover have "Mf (0,{# g #}) = (0,{# g #})" unfolding Mf_def by (auto simp: mpg, simp add: g_def) ultimately have fact2: "(0, {#g#}) ∈ Mf ` Collect (factorization_m f)" by force note [simp] = assms[unfolded unique_factorization_m_def] from fact1[simplified, folded fact2[simplified]] show False by auto qed end context poly_mod begin lemma dvdm_smult: assumes "f dvdm g" shows "f dvdm smult c g" proof - from assms[unfolded dvdm_def] obtain h where g: "g =m f * h" by auto show ?thesis unfolding dvdm_def proof (intro exI[of _ "smult c h"]) have "Mp (smult c g) = Mp (smult c (Mp g))" by simp also have "Mp g = Mp (f * h)" using g by simp finally show "Mp (smult c g) = Mp (f * smult c h)" by simp qed qed lemma dvdm_factor: assumes "f dvdm g" shows "f dvdm g * h" proof - from assms[unfolded dvdm_def] obtain k where g: "g =m f * k" by auto show ?thesis unfolding dvdm_def proof (intro exI[of _ "h * k"]) have "Mp (g * h) = Mp (Mp g * h)" by simp also have "Mp g = Mp (f * k)" using g by simp finally show "Mp (g * h) = Mp (f * (h * k))" by (simp add: ac_simps) qed qed lemma square_free_m_smultD: assumes "square_free_m (smult c f)" shows "square_free_m f" unfolding square_free_m_def proof (intro conjI allI impI) fix g assume "degree_m g ≠ 0" with assms[unfolded square_free_m_def] have "¬ g * g dvdm smult c f" by auto thus "¬ g * g dvdm f" using dvdm_smult[of "g * g" f c] by blast next from assms[unfolded square_free_m_def] have "¬ smult c f =m 0" by simp thus "¬ f =m 0" by (metis Mp_smult(2) smult_0_right) qed lemma square_free_m_smultI: assumes sf: "square_free_m f" and inv: "M (ci * c) = 1" shows "square_free_m (smult c f)" proof - have "square_free_m (smult ci (smult c f))" proof (rule square_free_m_cong[OF sf], rule poly_eqI, unfold Mp_coeff coeff_smult) fix n have "M (ci * (c * coeff f n)) = M ( M (ci * c) * coeff f n)" by (simp add: ac_simps) from this[unfolded inv] show "M (coeff f n) = M (ci * (c * coeff f n))" by simp qed from square_free_m_smultD[OF this] show ?thesis . qed lemma square_free_m_factor: assumes "square_free_m (f * g)" shows "square_free_m f" "square_free_m g" proof - { fix f g assume sf: "square_free_m (f * g)" have "square_free_m f" unfolding square_free_m_def proof (intro conjI allI impI) fix h assume "degree_m h ≠ 0" with sf[unfolded square_free_m_def] have "¬ h * h dvdm f * g" by auto thus "¬ h * h dvdm f" using dvdm_factor[of "h * h" f g] by blast next from sf[unfolded square_free_m_def] have "¬ f * g =m 0" by simp thus "¬ f =m 0" by (metis mult.commute mult_zero_right poly_mod.mult_Mp(2)) qed } from this[of f g] this[of g f] assms show "square_free_m f" "square_free_m g" by (auto simp: ac_simps) qed end context poly_mod_2 begin lemma Mp_ident_iff: "Mp f = f ⟷ (∀ n. coeff f n ∈ {0 ..< m})" proof - have m0: "m > 0" using m1 by simp show ?thesis unfolding poly_eq_iff Mp_coeff M_def mod_ident_iff[OF m0] by simp qed lemma Mp_ident_iff': "Mp f = f ⟷ (set (coeffs f) ⊆ {0 ..< m})" proof - have 0: "0 ∈ {0 ..< m}" using m1 by auto have ran: "(∀n. coeff f n ∈ {0..<m}) ⟷ range (coeff f) ⊆ {0 ..< m}" by blast show ?thesis unfolding Mp_ident_iff ran using range_coeff[of f] 0 by auto qed end lemma Mp_Mp_pow_is_Mp: "n ≠ 0 ⟹ p > 1 ⟹ poly_mod.Mp p (poly_mod.Mp (p^n) f) = poly_mod.Mp p f" using poly_mod_2.Mp_product_modulus poly_mod_2_def by(subst power_eq_if, auto) lemma M_M_pow_is_M: "n ≠ 0 ⟹ p > 1 ⟹ poly_mod.M p (poly_mod.M (p^n) f) = poly_mod.M p f" using Mp_Mp_pow_is_Mp[of n p "[:f:]"] by (metis coeff_pCons_0 poly_mod.Mp_coeff) definition inverse_mod :: "int ⇒ int ⇒ int" where "inverse_mod x m = fst (bezout_coefficients x m)" lemma inverse_mod: "(inverse_mod x m * x) mod m = 1" if "coprime x m" "m > 1" proof - from bezout_coefficients [of x m "inverse_mod x m" "snd (bezout_coefficients x m)"] have "inverse_mod x m * x + snd (bezout_coefficients x m) * m = gcd x m" by (simp add: inverse_mod_def) with that have "inverse_mod x m * x + snd (bezout_coefficients x m) * m = 1" by simp then have "(inverse_mod x m * x + snd (bezout_coefficients x m) * m) mod m = 1 mod m" by simp with ‹m > 1› show ?thesis by simp qed lemma inverse_mod_pow: "(inverse_mod x (p ^ n) * x) mod (p ^ n) = 1" if "coprime x p" "p > 1" "n ≠ 0" using that by (auto intro: inverse_mod) lemma (in poly_mod) inverse_mod_coprime: assumes p: "prime m" and cop: "coprime x m" shows "M (inverse_mod x m * x) = 1" unfolding M_def using inverse_mod_pow[OF cop, of 1] p by (auto simp: prime_int_iff) lemma (in poly_mod) inverse_mod_coprime_exp: assumes m: "m = p^n" and p: "prime p" and n: "n ≠ 0" and cop: "coprime x p" shows "M (inverse_mod x m * x) = 1" unfolding M_def unfolding m using inverse_mod_pow[OF cop _ n] p by (auto simp: prime_int_iff) locale poly_mod_prime = poly_mod p for p :: int + assumes prime: "prime p" begin sublocale poly_mod_2 p using prime unfolding poly_mod_2_def using prime_gt_1_int by force lemma square_free_m_prod_imp_coprime_m: assumes sf: "square_free_m (A * B)" shows "coprime_m A B" unfolding coprime_m_def proof (intro allI impI) fix h assume dvd: "h dvdm A" "h dvdm B" then obtain ha hb where *: "Mp A = Mp (h * ha)" "Mp B = Mp (h * hb)" unfolding dvdm_def by auto have AB: "Mp (A * B) = Mp (Mp A * Mp B)" by simp from this[unfolded *, simplified] have eq: "Mp (A * B) = Mp (h * h * (ha * hb))" by (simp add: ac_simps) hence dvd_hh: "(h * h) dvdm (A * B)" unfolding dvdm_def by auto { assume "degree_m h ≠ 0" from sf[unfolded square_free_m_def, THEN conjunct2, rule_format, OF this] have "¬ h * h dvdm A * B" . with dvd_hh have False by simp } hence "degree (Mp h) = 0" by auto then obtain c where hc: "Mp h = [: c :]" by (rule degree_eq_zeroE) { assume "c = 0" hence "Mp h = 0" unfolding hc by auto with *(1) have "Mp A = 0" by (metis Mp_0 mult_zero_left poly_mod.mult_Mp(1)) with sf[unfolded square_free_m_def, THEN conjunct1] have False by (simp add: AB) } hence c0: "c ≠ 0" by auto with arg_cong[OF hc[symmetric], of "λ f. coeff f 0", unfolded Mp_coeff M_def] m1 have "c ≥ 0" "c < p" by auto with c0 have c_props:"c > 0" "c < p" by auto with prime have "prime p" by simp with c_props have "coprime p c" by (auto intro: prime_imp_coprime dest: zdvd_not_zless) then have "coprime c p" by (simp add: ac_simps) from inverse_mod_coprime[OF prime this] obtain d where d: "M (c * d) = 1" by (auto simp: ac_simps) show "h dvdm 1" unfolding dvdm_def proof (intro exI[of _ "[:d:]"]) have "Mp (h * [: d :]) = Mp (Mp h * [: d :])" by simp also have "… = Mp ([: c * d :])" unfolding hc by (auto simp: ac_simps) also have "… = [: M (c * d) :]" unfolding Mp_def by (metis (no_types) M_0 map_poly_pCons Mp_0 Mp_def d zero_neq_one) also have "… = 1" unfolding d by simp finally show "Mp 1 = Mp (h * [:d:])" by simp qed qed lemma coprime_exp_mod: "coprime lu p ⟹ n ≠ 0 ⟹ lu mod p ^ n ≠ 0" using prime by fastforce end context poly_mod begin definition Dp :: "int poly ⇒ int poly" where "Dp f = map_poly (λ a. a div m) f" lemma Dp_Mp_eq: "f = Mp f + smult m (Dp f)" by (rule poly_eqI, auto simp: Mp_coeff M_def Dp_def coeff_map_poly) lemma dvd_imp_dvdm: assumes "a dvd b" shows "a dvdm b" by (metis assms dvd_def dvdm_def) lemma dvdm_add: assumes a: "u dvdm a" and b: "u dvdm b" shows "u dvdm (a+b)" proof - obtain a' where a: "a =m u*a'" using a unfolding dvdm_def by auto obtain b' where b: "b =m u*b'" using b unfolding dvdm_def by auto have "Mp (a + b) = Mp (u*a'+u*b')" using a b by (metis poly_mod.plus_Mp(1) poly_mod.plus_Mp(2)) also have "... = Mp (u * (a'+ b'))" by (simp add: distrib_left) finally show ?thesis unfolding dvdm_def by auto qed lemma monic_dvdm_constant: assumes uk: "u dvdm [:k:]" and u1: "monic u" and u2: "degree u > 0" shows "k mod m = 0" proof - have d1: "degree_m [:k:] = degree [:k:]" by (metis degree_pCons_0 le_zero_eq poly_mod.degree_m_le) obtain h where h: "Mp [:k:] = Mp (u * h)" using uk unfolding dvdm_def by auto have d2: "degree_m [:k:] = degree_m (u*h)" using h by metis have d3: "degree (map_poly M (u * map_poly M h)) = degree (u * map_poly M h)" by (rule degree_map_poly) (metis coeff_degree_mult leading_coeff_0_iff mult.right_neutral M_M Mp_coeff Mp_def u1) thus ?thesis using assms d1 d2 d3 by (auto, metis M_def map_poly_pCons degree_mult_right_le h leD map_poly_0 mult_poly_0_right pCons_eq_0_iff M_0 Mp_def mult_Mp(2)) qed lemma div_mod_imp_dvdm: assumes "∃q r. b = q * a + Polynomial.smult m r" shows "a dvdm b" proof - from assms obtain q r where b:"b = a * q + smult m r" by (metis mult.commute) have a: "Mp (Polynomial.smult m r) = 0" by auto show ?thesis proof (unfold dvdm_def, rule exI[of _ q]) have "Mp (a * q + smult m r) = Mp (a * q + Mp (smult m r))" using plus_Mp(2)[of "a*q" "smult m r"] by auto also have "... = Mp (a*q)" by auto finally show "eq_m b (a * q)" using b by auto qed qed lemma lead_coeff_monic_mult: fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly" assumes "monic p" shows "lead_coeff (p * q) = lead_coeff q" using assms by (simp add: lead_coeff_mult) lemma degree_m_mult_eq: assumes p: "monic p" and q: "lead_coeff q mod m ≠ 0" and m1: "m > 1" shows "degree (Mp (p * q)) = degree p + degree q" proof- have "lead_coeff (p * q) mod m ≠ 0" using q p by (auto simp: lead_coeff_monic_mult) with m1 show ?thesis by (auto simp: degree_m_eq intro!: degree_mult_eq) qed lemma dvdm_imp_degree_le: assumes pq: "p dvdm q" and p: "monic p" and q0: "Mp q ≠ 0" and m1: "m > 1" shows "degree p ≤ degree q" proof- from q0 have q: "lead_coeff (Mp q) mod m ≠ 0" by (metis Mp_Mp Mp_coeff leading_coeff_neq_0 M_def) from pq obtain r where Mpq: "Mp q = Mp (p * Mp r)" by (auto elim: dvdmE) with p q have "lead_coeff (Mp r) mod m ≠ 0" by (metis Mp_Mp Mp_coeff leading_coeff_0_iff mult_poly_0_right M_def) from degree_m_mult_eq[OF p this m1] Mpq have "degree p ≤ degree_m q" by simp thus ?thesis using degree_m_le le_trans by blast qed lemma dvdm_uminus [simp]: "p dvdm -q ⟷ p dvdm q" by (metis add.inverse_inverse dvdm_smult smult_1_left smult_minus_left) (*TODO: simp?*) lemma Mp_const_poly: "Mp [:a:] = [:a mod m:]" by (simp add: Mp_def M_def Polynomial.map_poly_pCons) lemma dvdm_imp_div_mod: assumes "u dvdm g" shows "∃q r. g = q*u + smult m r" proof - obtain q where q: "Mp g = Mp (u*q)" using assms unfolding dvdm_def by fast have "(u*q) = Mp (u*q) + smult m (Dp (u*q))" by (simp add: poly_mod.Dp_Mp_eq[of "u*q"]) hence uq: "Mp (u*q) = (u*q) - smult m (Dp (u*q))" by auto have g: "g = Mp g + smult m (Dp g)" by (simp add: poly_mod.Dp_Mp_eq[of "g"]) also have "... = poly_mod.Mp m (u*q) + smult m (Dp g)" using q by simp also have "... = u * q - smult m (Dp (u * q)) + smult m (Dp g)" unfolding uq by auto also have "... = u * q + smult m (-Dp (u*q)) + smult m (Dp g)" by auto also have "... = u * q + smult m (-Dp (u*q) + Dp g)" unfolding smult_add_right by auto also have "... = q * u + smult m (-Dp (u*q) + Dp g)" by auto finally show ?thesis by auto qed corollary div_mod_iff_dvdm: shows "a dvdm b = (∃q r. b = q * a + Polynomial.smult m r)" using div_mod_imp_dvdm dvdm_imp_div_mod by blast lemma dvdmE': assumes "p dvdm q" and "⋀r. q =m p * Mp r ⟹ thesis" shows thesis using assms by (auto simp: dvdm_def) end context poly_mod_2 begin lemma factorization_m_mem_dvdm: assumes fact: "factorization_m f (c,fs)" and mem: "Mp g ∈# image_mset Mp fs" shows "g dvdm f" proof - from fact have "factorization_m f (Mf (c, fs))" by auto then obtain l where f: "factorization_m f (l, image_mset Mp fs)" by (auto simp: Mf_def) from multi_member_split[OF mem] obtain ls where fs: "image_mset Mp fs = {# Mp g #} + ls" by auto from f[unfolded fs split factorization_m_def] show "g dvdm f" unfolding dvdm_def by (intro exI[of _ "smult l (prod_mset ls)"], auto simp del: Mp_smult simp add: Mp_smult(2)[of _ "Mp g * prod_mset ls", symmetric], simp) qed lemma dvdm_degree: "monic u ⟹ u dvdm f ⟹ Mp f ≠ 0 ⟹ degree u ≤ degree f" using dvdm_imp_degree_le m1 by blast end lemma (in poly_mod_prime) pl_dvdm_imp_p_dvdm: assumes l0: "l ≠ 0" and pl_dvdm: "poly_mod.dvdm (p^l) a b" shows "a dvdm b" proof - from l0 have l_gt_0: "l > 0" by auto with m1 interpret pl: poly_mod_2 "p^l" by (unfold_locales, auto) from l_gt_0 have p_rw: "p * p ^ (l - 1) = p ^ l" by (cases l) simp_all obtain q r where b: "b = q * a + smult (p^l) r" using pl.dvdm_imp_div_mod[OF pl_dvdm] by auto have "smult (p^l) r = smult p (smult (p ^ (l - 1)) r)" unfolding smult_smult p_rw .. hence b2: "b = q * a + smult p (smult (p ^ (l - 1)) r)" using b by auto show ?thesis by (rule div_mod_imp_dvdm, rule exI[of _ q], rule exI[of _ "(smult (p ^ (l - 1)) r)"], auto simp add: b2) qed end