Commit 10a137a0 authored by Rene Thiemann's avatar Rene Thiemann
Browse files

moved lemmas and definitions from Missing_Lemmas.thy to better suitable theories

parent a621572958bd
......@@ -271,6 +271,71 @@ end
context poly_mod_prime
begin
lemma unique_factorization_m_factor_partition: assumes l0: "l \<noteq> 0"
and uf: "poly_mod.unique_factorization_m (p^l) f (lead_coeff f, mset gs)"
and f: "f = f1 * f2"
and cop: "coprime (lead_coeff f) p"
and sf: "square_free_m f"
and part: "List.partition (\<lambda>gi. gi dvdm f1) gs = (gs1, gs2)"
shows "poly_mod.unique_factorization_m (p^l) f1 (lead_coeff f1, mset gs1)"
"poly_mod.unique_factorization_m (p^l) f2 (lead_coeff f2, mset gs2)"
proof -
interpret pl: poly_mod_2 "p^l" by (standard, insert m1 l0, auto)
let ?I = "image_mset pl.Mp"
note Mp_pow [simp] = Mp_Mp_pow_is_Mp[OF l0 m1]
have [simp]: "pl.Mp x dvdm u = (x dvdm u)" for x u unfolding dvdm_def using Mp_pow[of x]
by (metis poly_mod.mult_Mp(1))
have gs_split: "set gs = set gs1 \<union> set gs2" using part by auto
from pl.unique_factorization_m_factor[OF prime uf[unfolded f] _ _ l0 refl, folded f, OF cop sf]
obtain hs1 hs2 where uf': "pl.unique_factorization_m f1 (lead_coeff f1, hs1)"
"pl.unique_factorization_m f2 (lead_coeff f2, hs2)"
and gs_hs: "?I (mset gs) = hs1 + hs2"
unfolding pl.Mf_def split by auto
have gs_gs: "?I (mset gs) = ?I (mset gs1) + ?I (mset gs2)" using part
by (auto, induct gs arbitrary: gs1 gs2, auto)
with gs_hs have gs_hs12: "?I (mset gs1) + ?I (mset gs2) = hs1 + hs2" by auto
note pl_dvdm_imp_p_dvdm = pl_dvdm_imp_p_dvdm[OF l0]
note fact = pl.unique_factorization_m_imp_factorization[OF uf]
have gs1: "?I (mset gs1) = {#x \<in># ?I (mset gs). x dvdm f1#}"
using part by (auto, induct gs arbitrary: gs1 gs2, auto)
also have "\<dots> = {#x \<in># hs1. x dvdm f1#} + {#x \<in># hs2. x dvdm f1#}" unfolding gs_hs by simp
also have "{#x \<in># hs2. x dvdm f1#} = {#}"
proof (rule ccontr)
assume "\<not> ?thesis"
then obtain x where x: "x \<in># hs2" and dvd: "x dvdm f1" by fastforce
from x gs_hs have "x \<in># ?I (mset gs)" by auto
with fact[unfolded pl.factorization_m_def]
have xx: "pl.irreducible\<^sub>d_m x" "monic x" by auto
from square_free_m_prod_imp_coprime_m[OF sf[unfolded f]]
have cop_h_f: "coprime_m f1 f2" by auto
from pl.factorization_m_mem_dvdm[OF pl.unique_factorization_m_imp_factorization[OF uf'(2)], of x] x
have "pl.dvdm x f2" by auto
hence "x dvdm f2" by (rule pl_dvdm_imp_p_dvdm)
from cop_h_f[unfolded coprime_m_def, rule_format, OF dvd this]
have "x dvdm 1" by auto
from dvdm_imp_degree_le[OF this xx(2) _ m1] have "degree x = 0" by auto
with xx show False unfolding pl.irreducible\<^sub>d_m_def by auto
qed
also have "{#x \<in># hs1. x dvdm f1#} = hs1"
proof (rule ccontr)
assume "\<not> ?thesis"
from filter_mset_inequality[OF this]
obtain x where x: "x \<in># hs1" and dvd: "\<not> x dvdm f1" by blast
from pl.factorization_m_mem_dvdm[OF pl.unique_factorization_m_imp_factorization[OF uf'(1)],
of x] x dvd
have "pl.dvdm x f1" by auto
from pl_dvdm_imp_p_dvdm[OF this] dvd show False by auto
qed
finally have gs_hs1: "?I (mset gs1) = hs1" by simp
with gs_hs12 have "?I (mset gs2) = hs2" by auto
with uf' gs_hs1 have "pl.unique_factorization_m f1 (lead_coeff f1, ?I (mset gs1))"
"pl.unique_factorization_m f2 (lead_coeff f2, ?I (mset gs2))" by auto
thus "pl.unique_factorization_m f1 (lead_coeff f1, mset gs1)"
"pl.unique_factorization_m f2 (lead_coeff f2, mset gs2)"
unfolding pl.unique_factorization_m_def
by (auto simp: pl.Mf_def image_mset.compositionality o_def)
qed
lemma factorization_pn_to_factorization_p: assumes fact: "poly_mod.factorization_m (p^n) C (c,fs)"
and sf: "square_free_m C"
and n: "n \<noteq> 0"
......
......@@ -19,7 +19,8 @@ imports
"HOL-Computational_Algebra.Field_as_Ring"
begin
hide_const (open) up_ring.coeff up_ring.monom Modules.module
hide_const (open) up_ring.coeff up_ring.monom Modules.module subspace
Modules.module_hom
subsection \<open>Auxiliary lemmas\<close>
......@@ -1850,7 +1851,7 @@ qed
lemma linear_Poly_list_of_vec:
shows "(Poly \<circ> list_of_vec) \<in> module_hom class_ring V (vector_space_poly.vs {v. [v^(CARD('a)) = v] (mod u)})"
proof (auto simp add: module_hom_def Matrix.module_vec_def)
proof (auto simp add: LinearCombinations.module_hom_def Matrix.module_vec_def)
fix m1 m2::" 'a mod_ring vec"
assume m1: "m1 \<in> mat_kernel (berlekamp_resulting_mat u)"
and m2: "m2 \<in> mat_kernel (berlekamp_resulting_mat u)"
......@@ -1938,7 +1939,7 @@ qed
lemma linear_Poly_list_of_vec':
assumes "degree u > 0"
shows "(Poly \<circ> list_of_vec) \<in> module_hom R V W"
proof (auto simp add: module_hom_def Matrix.module_vec_def)
proof (auto simp add: LinearCombinations.module_hom_def Matrix.module_vec_def)
fix m1 m2::" 'a mod_ring vec"
assume m1: "m1 \<in> mat_kernel (berlekamp_resulting_mat u)"
and m2: "m2 \<in> mat_kernel (berlekamp_resulting_mat u)"
......@@ -2042,7 +2043,7 @@ proof -
hence "x \<in> mat_kernel (berlekamp_resulting_mat u)" using x by auto
hence "[Poly (list_of_vec x) ^ CARD('a) = Poly (list_of_vec x)] (mod u)"
using linear_Poly_list_of_vec
unfolding module_hom_def Matrix.module_vec_def by auto
unfolding LinearCombinations.module_hom_def Matrix.module_vec_def by auto
}
thus "[v ^ CARD('a) = v] (mod u)" using v unfolding set_berlekamp_basis_eq by auto
qed
......@@ -2056,7 +2057,7 @@ proof (auto simp add: image_def)
assume xa: "xa \<in> mat_kernel (berlekamp_resulting_mat u)"
thus "[Poly (list_of_vec xa) ^ CARD('a) = Poly (list_of_vec xa)] (mod u)"
using linear_Poly_list_of_vec
unfolding module_hom_def Matrix.module_vec_def by auto
unfolding LinearCombinations.module_hom_def Matrix.module_vec_def by auto
show "degree (Poly (list_of_vec xa)) < degree u"
proof (rule degree_Poly_list_of_vec[OF _ deg_u])
show "xa \<in> carrier_vec (degree u)" using xa unfolding mat_kernel_def by simp
......@@ -2441,7 +2442,7 @@ proof -
interpret vec_VS: vectorspace class_ring "(module_vec TYPE('a mod_ring) n)"
by (rule VS_Connect.vec_vs)
interpret linear_map class_ring W "(module_vec TYPE('a mod_ring) n)" ?f
by (intro_locales, unfold mod_hom_axioms_def module_hom_def,
by (intro_locales, unfold mod_hom_axioms_def LinearCombinations.module_hom_def,
auto simp add: vec_eq_iff module_vec_def mod_smult_left poly_mod_add_left)
have "linear_map class_ring W (module_vec TYPE('a mod_ring) n) ?f"
by (intro_locales)
......
......@@ -476,16 +476,6 @@ proof -
finally show ?thesis using 0 by auto
qed
context poly_mod
begin
definition Dp :: "int poly \<Rightarrow> int poly" where
"Dp f = map_poly (\<lambda> 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)
end
context
fixes C :: "int poly"
begin
......
......@@ -15,6 +15,7 @@ theory Poly_Mod
"HOL-Computational_Algebra.Primes"
Polynomial_Factorization.Square_Free_Factorization
Unique_Factorization_Poly
"HOL-Word.Misc_Arithmetic"
begin
locale poly_mod = fixes m :: "int"
......@@ -872,6 +873,181 @@ proof (intro allI impI)
qed
qed
lemma coprime_exp_mod: "coprime lu p \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> lu mod p ^ n \<noteq> 0"
using prime by fastforce
end
context poly_mod
begin
definition Dp :: "int poly \<Rightarrow> int poly" where
"Dp f = map_poly (\<lambda> 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 "\<exists>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 \<noteq> 0" and m1: "m > 1"
shows "degree (Mp (p * q)) = degree p + degree q"
proof-
have "lead_coeff (p * q) mod m \<noteq> 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 \<noteq> 0" and m1: "m > 1"
shows "degree p \<le> degree q"
proof-
from q0
have q: "lead_coeff (Mp q) mod m \<noteq> 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 \<noteq> 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 \<le> degree_m q" by simp
thus ?thesis using degree_m_le le_trans by blast
qed
lemma dvdm_uminus [simp]:
"p dvdm -q \<longleftrightarrow> 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 "\<exists>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 = (\<exists>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 "\<And>r. q =m p * Mp r \<Longrightarrow> 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 \<in># 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 \<Longrightarrow> u dvdm f \<Longrightarrow> Mp f \<noteq> 0 \<Longrightarrow> degree u \<le> degree f"
using dvdm_imp_degree_le m1 by blast
end
lemma (in poly_mod_prime) pl_dvdm_imp_p_dvdm:
assumes l0: "l \<noteq> 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)
have p_rw: "p * p ^ (l - 1) = p ^ l" by (rule power_minus_simp[symmetric, OF l_gt_0])
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
\ No newline at end of file
......@@ -21,6 +21,11 @@ hide_fact(open)
hide_const (open) Rings.coprime
lemma irreducible_uminus [simp]:
fixes a::"'a::idom"
shows "irreducible (-a) \<longleftrightarrow> irreducible a"
using irreducible_mult_unit_left[of "-1::'a"] by auto
context comm_monoid_mult begin
definition coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
......
......@@ -665,7 +665,7 @@ begin
abbreviation "M == \<lambda>k. module_vec TYPE('a) k"
abbreviation "span == \<lambda>k. module.span class_ring (M k)"
abbreviation "span == \<lambda>k. LinearCombinations.module.span class_ring (M k)"
abbreviation "lincomb == \<lambda>k. module.lincomb (M k)"
abbreviation "lin_dep == \<lambda>k. module.lin_dep class_ring (M k)"
abbreviation "padr m v == v @\<^sub>v 0\<^sub>v m"
......@@ -901,11 +901,11 @@ proof (rule, intro conjI)
qed
lemma kernel_padl:
assumes dD: "d : mat_kernel (D :: 'a :: field mat)"
and A: "A : carrier_mat nr1 nc1"
and C: "C : carrier_mat nr2 nc1"
and D: "D : carrier_mat nr2 nc2"
shows "padl nc1 d : mat_kernel (four_block_mat A (0\<^sub>m nr1 nc2) C D)" (is "_ : mat_kernel ?ABCD")
assumes dD: "d \<in> mat_kernel (D :: 'a :: field mat)"
and A: "A \<in> carrier_mat nr1 nc1"
and C: "C \<in> carrier_mat nr2 nc1"
and D: "D \<in> carrier_mat nr2 nc2"
shows "padl nc1 d \<in> mat_kernel (four_block_mat A (0\<^sub>m nr1 nc2) C D)" (is "_ \<in> mat_kernel ?ABCD")
unfolding mat_kernel_def
proof (rule, intro conjI)
have [simp]: "dim_row A = nr1" "dim_row D = nr2" "dim_row ?ABCD = nr1 + nr2" using A D by auto
......@@ -947,12 +947,12 @@ proof (rule, intro conjI)
qed
lemma mat_kernel_split:
assumes A: "A : carrier_mat n n"
and D: "D : carrier_mat m m"
and kAD: "k : mat_kernel (four_block_mat A (0\<^sub>m n m) (0\<^sub>m m n) D)"
(is "_ : mat_kernel ?A00D")
shows "vec_first k n : mat_kernel A" (is "?a : _")
and "vec_last k m : mat_kernel D" (is "?d : _")
assumes A: "A \<in> carrier_mat n n"
and D: "D \<in> carrier_mat m m"
and kAD: "k \<in> mat_kernel (four_block_mat A (0\<^sub>m n m) (0\<^sub>m m n) D)"
(is "_ \<in> mat_kernel ?A00D")
shows "vec_first k n \<in> mat_kernel A" (is "?a \<in> _")
and "vec_last k m \<in> mat_kernel D" (is "?d \<in> _")
proof -
have "0\<^sub>v n @\<^sub>v 0\<^sub>v m = 0\<^sub>v (n+m)" by auto
also
......
This diff is collapsed.
This diff is collapsed.
......@@ -115,4 +115,7 @@ proof (induct vs arbitrary: ws)
qed simp
qed simp
lemma filter_mset_inequality: "filter_mset f xs \<noteq> xs \<Longrightarrow> \<exists> x \<in># xs. \<not> f x"
by (induct xs, auto)
end
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment