Theory Macaulay_Matrix
section ‹Macaulay Matrices›
theory Macaulay_Matrix
imports More_MPoly_Type_Class Jordan_Normal_Form.Gauss_Jordan_Elimination
begin
text ‹We build upon vectors and matrices represented by dimension and characteristic function, because
later on we need to quantify the dimensions of certain matrices existentially. This is not possible
(at least not easily possible) with a type-based approach, as in HOL-Multivariate Analysis.›
subsection ‹More about Vectors›
lemma vec_of_list_alt: "vec_of_list xs = vec (length xs) (nth xs)"
by (transfer, rule refl)
lemma vec_cong:
assumes "n = m" and "⋀i. i < m ⟹ f i = g i"
shows "vec n f = vec m g"
using assms by auto
lemma scalar_prod_comm:
assumes "dim_vec v = dim_vec w"
shows "v ∙ w = w ∙ (v::'a::comm_semiring_0 vec)"
by (simp add: scalar_prod_def assms, rule sum.cong, rule refl, simp only: ac_simps)
lemma vec_scalar_mult_fun: "vec n (λx. c * f x) = c ⋅⇩v vec n f"
by (simp add: smult_vec_def, rule vec_cong, rule refl, simp)
definition mult_vec_mat :: "'a vec ⇒ 'a :: semiring_0 mat ⇒ 'a vec" (infixl "⇩v*" 70)
where "v ⇩v* A ≡ vec (dim_col A) (λj. v ∙ col A j)"
definition resize_vec :: "nat ⇒ 'a vec ⇒ 'a vec"
where "resize_vec n v = vec n (vec_index v)"
lemma dim_resize_vec[simp]: "dim_vec (resize_vec n v) = n"
by (simp add: resize_vec_def)
lemma resize_vec_carrier: "resize_vec n v ∈ carrier_vec n"
by (simp add: carrier_dim_vec)
lemma resize_vec_dim[simp]: "resize_vec (dim_vec v) v = v"
by (simp add: resize_vec_def eq_vecI)
lemma resize_vec_index:
assumes "i < n"
shows "resize_vec n v $ i = v $ i"
using assms by (simp add: resize_vec_def)
lemma mult_mat_vec_resize:
"v ⇩v* A = (resize_vec (dim_row A) v) ⇩v* A"
by (simp add: mult_vec_mat_def scalar_prod_def, rule arg_cong2[of _ _ _ _ vec], rule, rule,
rule sum.cong, rule, simp add: resize_vec_index)
lemma assoc_mult_vec_mat:
assumes "v ∈ carrier_vec n1" and "A ∈ carrier_mat n1 n2" and "B ∈ carrier_mat n2 n3"
shows "v ⇩v* (A * B) = (v ⇩v* A) ⇩v* B"
using assms by (intro eq_vecI, auto simp add: mult_vec_mat_def mult_mat_vec_def assoc_scalar_prod)
lemma mult_vec_mat_transpose:
assumes "dim_vec v = dim_row A"
shows "v ⇩v* A = (transpose_mat A) *⇩v (v::'a::comm_semiring_0 vec)"
proof (simp add: mult_vec_mat_def mult_mat_vec_def, rule vec_cong, rule refl, simp)
fix j
show "v ∙ col A j = col A j ∙ v" by (rule scalar_prod_comm, simp add: assms)
qed
subsection ‹More about Matrices›
definition nzrows :: "'a::zero mat ⇒ 'a vec list"
where "nzrows A = filter (λr. r ≠ 0⇩v (dim_col A)) (rows A)"
definition row_space :: "'a mat ⇒ 'a::semiring_0 vec set"
where "row_space A = (λv. mult_vec_mat v A) ` (carrier_vec (dim_row A))"
definition row_echelon :: "'a mat ⇒ 'a::field mat"
where "row_echelon A = fst (gauss_jordan A (1⇩m (dim_row A)))"
subsubsection ‹@{const nzrows}›
lemma length_nzrows: "length (nzrows A) ≤ dim_row A"
by (simp add: nzrows_def length_rows[symmetric] del: length_rows)
lemma set_nzrows: "set (nzrows A) = set (rows A) - {0⇩v (dim_col A)}"
by (auto simp add: nzrows_def)
lemma nzrows_nth_not_zero:
assumes "i < length (nzrows A)"
shows "nzrows A ! i ≠ 0⇩v (dim_col A)"
using assms unfolding nzrows_def using nth_mem by force
subsubsection ‹@{const row_space}›
lemma row_spaceI:
assumes "x = v ⇩v* A"
shows "x ∈ row_space A"
unfolding row_space_def assms by (rule, fact mult_mat_vec_resize, fact resize_vec_carrier)
lemma row_spaceE:
assumes "x ∈ row_space A"
obtains v where "v ∈ carrier_vec (dim_row A)" and "x = v ⇩v* A"
using assms unfolding row_space_def by auto
lemma row_space_alt: "row_space A = range (λv. mult_vec_mat v A)"
proof
show "row_space A ⊆ range (λv. v ⇩v* A)" unfolding row_space_def by auto
next
show "range (λv. v ⇩v* A) ⊆ row_space A"
proof
fix x
assume "x ∈ range (λv. v ⇩v* A)"
then obtain v where "x = v ⇩v* A" ..
thus "x ∈ row_space A" by (rule row_spaceI)
qed
qed
lemma row_space_mult:
assumes "A ∈ carrier_mat nr nc" and "B ∈ carrier_mat nr nr"
shows "row_space (B * A) ⊆ row_space A"
proof
from assms(2) assms(1) have "B * A ∈ carrier_mat nr nc" by (rule mult_carrier_mat)
hence "nr = dim_row (B * A)" by blast
fix x
assume "x ∈ row_space (B * A)"
then obtain v where "v ∈ carrier_vec nr" and x: "x = v ⇩v* (B * A)"
unfolding ‹nr = dim_row (B * A)› by (rule row_spaceE)
from this(1) assms(2) assms(1) have "x = (v ⇩v* B) ⇩v* A" unfolding x by (rule assoc_mult_vec_mat)
thus "x ∈ row_space A" by (rule row_spaceI)
qed
lemma row_space_mult_unit:
assumes "P ∈ Units (ring_mat TYPE('a::semiring_1) (dim_row A) b)"
shows "row_space (P * A) = row_space A"
proof -
have A: "A ∈ carrier_mat (dim_row A) (dim_col A)" by simp
from assms have P: "P ∈ carrier (ring_mat TYPE('a) (dim_row A) b)" and
*: "∃Q∈(carrier (ring_mat TYPE('a) (dim_row A) b)).
Q ⊗⇘ring_mat TYPE('a) (dim_row A) b⇙ P = 𝟭⇘ring_mat TYPE('a) (dim_row A) b⇙"
unfolding Units_def by auto
from P have P_in: "P ∈ carrier_mat (dim_row A) (dim_row A)" by (simp add: ring_mat_def)
from * obtain Q where "Q ∈ carrier (ring_mat TYPE('a) (dim_row A) b)"
and "Q ⊗⇘ring_mat TYPE('a) (dim_row A) b⇙ P = 𝟭⇘ring_mat TYPE('a) (dim_row A) b⇙" ..
hence Q_in: "Q ∈ carrier_mat (dim_row A) (dim_row A)" and QP: "Q * P = 1⇩m (dim_row A)"
by (simp_all add: ring_mat_def)
show ?thesis
proof
from A P_in show "row_space (P * A) ⊆ row_space A" by (rule row_space_mult)
next
from A P_in Q_in have "Q * (P * A) = (Q * P) * A" by (simp only: assoc_mult_mat)
also from A have "... = A" by (simp add: QP)
finally have eq: "row_space A = row_space (Q * (P * A))" by simp
show "row_space A ⊆ row_space (P * A)" unfolding eq by (rule row_space_mult, rule mult_carrier_mat, fact+)
qed
qed
subsubsection ‹@{const row_echelon}›
lemma row_eq_zero_iff_pivot_fun:
assumes "pivot_fun A f (dim_col A)" and "i < dim_row (A::'a::zero_neq_one mat)"
shows "(row A i = 0⇩v (dim_col A)) ⟷ (f i = dim_col A)"
proof -
have *: "dim_row A = dim_row A" ..
show ?thesis
proof
assume a: "row A i = 0⇩v (dim_col A)"
show "f i = dim_col A"
proof (rule ccontr)
assume "f i ≠ dim_col A"
with pivot_funD(1)[OF * assms] have **: "f i < dim_col A" by simp
with * assms have "A $$ (i, f i) = 1" by (rule pivot_funD)
with ** assms(2) have "row A i $ (f i) = 1" by simp
hence "(1::'a) = (0⇩v (dim_col A)) $ (f i)" by (simp only: a)
also have "... = (0::'a)" using ** by simp
finally show False by simp
qed
next
assume a: "f i = dim_col A"
show "row A i = 0⇩v (dim_col A)"
proof (rule, simp_all add: assms(2))
fix j
assume "j < dim_col A"
hence "j < f i" by (simp only: a)
with * assms show "A $$ (i, j) = 0" by (rule pivot_funD)
qed
qed
qed
lemma row_not_zero_iff_pivot_fun:
assumes "pivot_fun A f (dim_col A)" and "i < dim_row (A::'a::zero_neq_one mat)"
shows "(row A i ≠ 0⇩v (dim_col A)) ⟷ (f i < dim_col A)"
proof (simp only: row_eq_zero_iff_pivot_fun[OF assms])
have "f i ≤ dim_col A" by (rule pivot_funD[where ?f = f], rule refl, fact+)
thus "(f i ≠ dim_col A) = (f i < dim_col A)" by auto
qed
lemma pivot_fun_stabilizes:
assumes "pivot_fun A f nc" and "i1 ≤ i2" and "i2 < dim_row A" and "nc ≤ f i1"
shows "f i2 = nc"
proof -
from assms(2) have "i2 = i1 + (i2 - i1)" by simp
then obtain k where "i2 = i1 + k" ..
from assms(3) assms(4) show ?thesis unfolding ‹i2 = i1 + k›
proof (induct k arbitrary: i1)
case 0
from this(1) have "i1 < dim_row A" by simp
from _ assms(1) this have "f i1 ≤ nc" by (rule pivot_funD, intro refl)
with ‹nc ≤ f i1› show ?case by simp
next
case (Suc k)
from Suc(2) have "Suc (i1 + k) < dim_row A" by simp
hence "Suc i1 + k < dim_row A" by simp
hence "Suc i1 < dim_row A" by simp
hence "i1 < dim_row A" by simp
have "nc ≤ f (Suc i1)"
proof -
have "f i1 < f (Suc i1) ∨ f (Suc i1) = nc" by (rule pivot_funD, rule refl, fact+)
with Suc(3) show ?thesis by auto
qed
with ‹Suc i1 + k < dim_row A› have "f (Suc i1 + k) = nc" by (rule Suc(1))
thus ?case by simp
qed
qed
lemma pivot_fun_mono_strict:
assumes "pivot_fun A f nc" and "i1 < i2" and "i2 < dim_row A" and "f i1 < nc"
shows "f i1 < f i2"
proof -
from assms(2) have "i2 - i1 ≠ 0" and "i2 = i1 + (i2 - i1)" by simp_all
then obtain k where "k ≠ 0" and "i2 = i1 + k" ..
from this(1) assms(3) assms(4) show ?thesis unfolding ‹i2 = i1 + k›
proof (induct k arbitrary: i1)
case 0
thus ?case by simp
next
case (Suc k)
from Suc(3) have "Suc (i1 + k) < dim_row A" by simp
hence "Suc i1 + k < dim_row A" by simp
hence "Suc i1 < dim_row A" by simp
hence "i1 < dim_row A" by simp
have *: "f i1 < f (Suc i1)"
proof -
have "f i1 < f (Suc i1) ∨ f (Suc i1) = nc" by (rule pivot_funD, rule refl, fact+)
with Suc(4) show ?thesis by auto
qed
show ?case
proof (simp, cases "k = 0")
case True
show "f i1 < f (Suc (i1 + k))" by (simp add: True *)
next
case False
have "f (Suc i1) ≤ f (Suc i1 + k)"
proof (cases "f (Suc i1) < nc")
case True
from False ‹Suc i1 + k < dim_row A› True have "f (Suc i1) < f (Suc i1 + k)" by (rule Suc(1))
thus ?thesis by simp
next
case False
hence "nc ≤ f (Suc i1)" by simp
from assms(1) _ ‹Suc i1 + k < dim_row A› this have "f (Suc i1 + k) = nc"
by (rule pivot_fun_stabilizes[where ?f=f], simp)
moreover have "f (Suc i1) = nc" by (rule pivot_fun_stabilizes[where ?f=f], fact, rule le_refl, fact+)
ultimately show ?thesis by simp
qed
also have "... = f (i1 + Suc k)" by simp
finally have "f (Suc i1) ≤ f (i1 + Suc k)" .
with * show "f i1 < f (Suc (i1 + k))" by simp
qed
qed
qed
lemma pivot_fun_mono:
assumes "pivot_fun A f nc" and "i1 ≤ i2" and "i2 < dim_row A"
shows "f i1 ≤ f i2"
proof -
from assms(2) have "i1 < i2 ∨ i1 = i2" by auto
thus ?thesis
proof
assume "i1 < i2"
show ?thesis
proof (cases "f i1 < nc")
case True
from assms(1) ‹i1 < i2› assms(3) this have "f i1 < f i2" by (rule pivot_fun_mono_strict)
thus ?thesis by simp
next
case False
hence "nc ≤ f i1" by simp
from assms(1) _ _ this have "f i1 = nc"
proof (rule pivot_fun_stabilizes[where ?f=f], simp)
from assms(2) assms(3) show "i1 < dim_row A" by (rule le_less_trans)
qed
moreover have "f i2 = nc" by (rule pivot_fun_stabilizes[where ?f=f], fact+)
ultimately show ?thesis by simp
qed
next
assume "i1 = i2"
thus ?thesis by simp
qed
qed
lemma row_echelon_carrier:
assumes "A ∈ carrier_mat nr nc"
shows "row_echelon A ∈ carrier_mat nr nc"
proof -
from assms have "dim_row A = nr" by simp
let ?B = "1⇩m (dim_row A)"
note assms
moreover have "?B ∈ carrier_mat nr nr" by (simp add: ‹dim_row A = nr›)
moreover from surj_pair obtain A' B' where *: "gauss_jordan A ?B = (A', B')" by metis
ultimately have "A' ∈ carrier_mat nr nc" by (rule gauss_jordan_carrier)
thus ?thesis by (simp add: row_echelon_def *)
qed
lemma dim_row_echelon[simp]:
shows "dim_row (row_echelon A) = dim_row A" and "dim_col (row_echelon A) = dim_col A"
proof -
have "A ∈ carrier_mat (dim_row A) (dim_col A)" by simp
hence "row_echelon A ∈ carrier_mat (dim_row A) (dim_col A)" by (rule row_echelon_carrier)
thus "dim_row (row_echelon A) = dim_row A" and "dim_col (row_echelon A) = dim_col A" by simp_all
qed
lemma row_echelon_transform:
obtains P where "P ∈ Units (ring_mat TYPE('a::field) (dim_row A) b)" and "row_echelon A = P * A"
proof -
let ?B = "1⇩m (dim_row A)"
have "A ∈ carrier_mat (dim_row A) (dim_col A)" by simp
moreover have "?B ∈ carrier_mat (dim_row A) (dim_row A)" by simp
moreover from surj_pair obtain A' B' where *: "gauss_jordan A ?B = (A', B')" by metis
ultimately have "∃P∈Units (ring_mat TYPE('a) (dim_row A) b). A' = P * A ∧ B' = P * ?B"
by (rule gauss_jordan_transform)
then obtain P where "P ∈ Units (ring_mat TYPE('a) (dim_row A) b)" and **: "A' = P * A ∧ B' = P * ?B" ..
from this(1) show ?thesis
proof
from ** have "A' = P * A" ..
thus "row_echelon A = P * A" by (simp add: row_echelon_def *)
qed
qed
lemma row_space_row_echelon[simp]: "row_space (row_echelon A) = row_space A"
proof -
obtain P where *: "P ∈ Units (ring_mat TYPE('a::field) (dim_row A) Nil)" and **: "row_echelon A = P * A"
by (rule row_echelon_transform)
from * have "row_space (P * A) = row_space A" by (rule row_space_mult_unit)
thus ?thesis by (simp only: **)
qed
lemma row_echelon_pivot_fun:
obtains f where "pivot_fun (row_echelon A) f (dim_col (row_echelon A))"
proof -
let ?B = "1⇩m (dim_row A)"
have "A ∈ carrier_mat (dim_row A) (dim_col A)" by simp
moreover from surj_pair obtain A' B' where *: "gauss_jordan A ?B = (A', B')" by metis
ultimately have "row_echelon_form A'" by (rule gauss_jordan_row_echelon)
then obtain f where "pivot_fun A' f (dim_col A')" unfolding row_echelon_form_def ..
hence "pivot_fun (row_echelon A) f (dim_col (row_echelon A))" by (simp add: row_echelon_def *)
thus ?thesis ..
qed
lemma distinct_nzrows_row_echelon: "distinct (nzrows (row_echelon A))"
unfolding nzrows_def
proof (rule distinct_filterI, simp del: dim_row_echelon)
let ?B = "row_echelon A"
fix i j::nat
assume "i < j" and "j < dim_row ?B"
hence "i ≠ j" and "i < dim_row ?B" by simp_all
assume ri: "row ?B i ≠ 0⇩v (dim_col ?B)" and rj: "row ?B j ≠ 0⇩v (dim_col ?B)"
obtain f where pf: "pivot_fun ?B f (dim_col ?B)" by (fact row_echelon_pivot_fun)
from rj have "f j < dim_col ?B" by (simp only: row_not_zero_iff_pivot_fun[OF pf ‹j < dim_row ?B›])
from _ pf ‹j < dim_row ?B› this ‹i < dim_row ?B› ‹i ≠ j› have *: "?B $$ (i, f j) = 0"
by (rule pivot_funD(5), intro refl)
show "row ?B i ≠ row ?B j"
proof
assume "row ?B i = row ?B j"
hence "row ?B i $ (f j) = row ?B j $ (f j)" by simp
with ‹i < dim_row ?B› ‹j < dim_row ?B› ‹f j < dim_col ?B› have "?B $$ (i, f j) = ?B $$ (j, f j)" by simp
also from _ pf ‹j < dim_row ?B› ‹f j < dim_col ?B› have "... = 1" by (rule pivot_funD, intro refl)
finally show False by (simp add: *)
qed
qed
subsection ‹Converting Between Polynomials and Macaulay Matrices›
definition poly_to_row :: "'a list ⇒ ('a ⇒⇩0 'b::zero) ⇒ 'b vec" where
"poly_to_row ts p = vec_of_list (map (lookup p) ts)"
definition polys_to_mat :: "'a list ⇒ ('a ⇒⇩0 'b::zero) list ⇒ 'b mat" where
"polys_to_mat ts ps = mat_of_rows (length ts) (map (poly_to_row ts) ps)"
definition list_to_fun :: "'a list ⇒ ('b::zero) list ⇒ 'a ⇒ 'b" where
"list_to_fun ts cs t = (case map_of (zip ts cs) t of Some c ⇒ c | None ⇒ 0)"
definition list_to_poly :: "'a list ⇒ 'b list ⇒ ('a ⇒⇩0 'b::zero)" where
"list_to_poly ts cs = Abs_poly_mapping (list_to_fun ts cs)"
definition row_to_poly :: "'a list ⇒ 'b vec ⇒ ('a ⇒⇩0 'b::zero)" where
"row_to_poly ts r = list_to_poly ts (list_of_vec r)"
definition mat_to_polys :: "'a list ⇒ 'b mat ⇒ ('a ⇒⇩0 'b::zero) list" where
"mat_to_polys ts A = map (row_to_poly ts) (rows A)"
lemma dim_poly_to_row: "dim_vec (poly_to_row ts p) = length ts"
by (simp add: poly_to_row_def)
lemma poly_to_row_index:
assumes "i < length ts"
shows "poly_to_row ts p $ i = lookup p (ts ! i)"
by (simp add: poly_to_row_def vec_of_list_index assms)
context term_powerprod
begin
lemma poly_to_row_scalar_mult:
assumes "keys p ⊆ set ts"
shows "row_to_poly ts (c ⋅⇩v (poly_to_row ts p)) = c ⋅ p"
proof -
have eq: "(vec (length ts) (λi. c * poly_to_row ts p $ i)) =
(vec (length ts) (λi. c * lookup p (ts ! i)))"
by (rule vec_cong, rule, simp only: poly_to_row_index)
have *: "list_to_fun ts (list_of_vec (c ⋅⇩v (poly_to_row ts p))) = (λt. c * lookup p t)"
proof (rule, simp add: list_to_fun_def smult_vec_def dim_poly_to_row eq,
simp add: map_upt[of "λx. c * lookup p x"] map_of_zip_map, rule)
fix t
assume "t ∉ set ts"
with assms(1) have "t ∉ keys p" by auto
thus "c * lookup p t = 0" by (simp add: in_keys_iff)
qed
have **: "lookup (Abs_poly_mapping (list_to_fun ts (list_of_vec (c ⋅⇩v (poly_to_row ts p))))) =
(λt. c * lookup p t)"
proof (simp only: *, rule Abs_poly_mapping_inverse, simp, rule finite_subset, rule, simp)
fix t
assume "c * lookup p t ≠ 0"
hence "lookup p t ≠ 0" using mult_not_zero by blast
thus "t ∈ keys p" by (simp add: in_keys_iff)
qed (fact finite_keys)
show ?thesis unfolding row_to_poly_def
by (rule poly_mapping_eqI) (simp only: list_to_poly_def ** lookup_map_scale)
qed
lemma poly_to_row_to_poly:
assumes "keys p ⊆ set ts"
shows "row_to_poly ts (poly_to_row ts p) = (p::'t ⇒⇩0 'b::semiring_1)"
proof -
have "1 ⋅⇩v (poly_to_row ts p) = poly_to_row ts p" by simp
thus ?thesis using poly_to_row_scalar_mult[OF assms, of 1] by simp
qed
lemma lookup_list_to_poly: "lookup (list_to_poly ts cs) = list_to_fun ts cs"
unfolding list_to_poly_def
proof (rule Abs_poly_mapping_inverse, rule, rule finite_subset)
show "{x. list_to_fun ts cs x ≠ 0} ⊆ set ts"
proof (rule, simp)
fix t
assume "list_to_fun ts cs t ≠ 0"
then obtain c where "map_of (zip ts cs) t = Some c" unfolding list_to_fun_def by fastforce
thus "t ∈ set ts" by (meson in_set_zipE map_of_SomeD)
qed
qed simp
lemma list_to_fun_Nil [simp]: "list_to_fun [] cs = 0"
by (simp only: zero_fun_def, rule, simp add: list_to_fun_def)
lemma list_to_poly_Nil [simp]: "list_to_poly [] cs = 0"
by (rule poly_mapping_eqI, simp add: lookup_list_to_poly)
lemma row_to_poly_Nil [simp]: "row_to_poly [] r = 0"
by (simp only: row_to_poly_def, fact list_to_poly_Nil)
lemma lookup_row_to_poly:
assumes "distinct ts" and "dim_vec r = length ts" and "i < length ts"
shows "lookup (row_to_poly ts r) (ts ! i) = r $ i"
proof (simp only: row_to_poly_def lookup_list_to_poly)
from assms(2) assms(3) have "i < dim_vec r" by simp
have "map_of (zip ts (list_of_vec r)) (ts ! i) = Some ((list_of_vec r) ! i)"
by (rule map_of_zip_nth, simp_all only: length_list_of_vec assms(2), fact, fact)
also have "... = Some (r $ i)" by (simp only: list_of_vec_index)
finally show "list_to_fun ts (list_of_vec r) (ts ! i) = r $ i" by (simp add: list_to_fun_def)
qed
lemma keys_row_to_poly: "keys (row_to_poly ts r) ⊆ set ts"
proof
fix t
assume "t ∈ keys (row_to_poly ts r)"
hence "lookup (row_to_poly ts r) t ≠ 0" by (simp add: in_keys_iff)
thus "t ∈ set ts"
proof (simp add: row_to_poly_def lookup_list_to_poly list_to_fun_def del: lookup_not_eq_zero_eq_in_keys
split: option.splits)
fix c
assume "map_of (zip ts (list_of_vec r)) t = Some c"
thus "t ∈ set ts" by (meson in_set_zipE map_of_SomeD)
qed
qed
lemma lookup_row_to_poly_not_zeroE:
assumes "lookup (row_to_poly ts r) t ≠ 0"
obtains i where "i < length ts" and "t = ts ! i"
proof -
from assms have "t ∈ keys (row_to_poly ts r)" by (simp add: in_keys_iff)
have "t ∈ set ts" by (rule, fact, fact keys_row_to_poly)
then obtain i where "i < length ts" and "t = ts ! i" by (metis in_set_conv_nth)
thus ?thesis ..
qed
lemma row_to_poly_zero [simp]: "row_to_poly ts (0⇩v (length ts)) = (0::'t ⇒⇩0 'b::zero)"
proof -
have eq: "map (λ_. 0::'b) [0..<length ts] = map (λ_. 0) ts" by (simp add: map_replicate_const)
show ?thesis
by (simp add: row_to_poly_def zero_vec_def, rule poly_mapping_eqI,
simp add: lookup_list_to_poly list_to_fun_def eq map_of_zip_map)
qed
lemma row_to_poly_zeroD:
assumes "distinct ts" and "dim_vec r = length ts" and "row_to_poly ts r = 0"
shows "r = 0⇩v (length ts)"
proof (rule, simp_all add: assms(2))
fix i
assume "i < length ts"
from assms(3) have "0 = lookup (row_to_poly ts r) (ts ! i)" by simp
also from assms(1) assms(2) ‹i < length ts› have "... = r $ i" by (rule lookup_row_to_poly)
finally show "r $ i = 0" by simp
qed
lemma row_to_poly_inj:
assumes "distinct ts" and "dim_vec r1 = length ts" and "dim_vec r2 = length ts"
and "row_to_poly ts r1 = row_to_poly ts r2"
shows "r1 = r2"
proof (rule, simp_all add: assms(2) assms(3))
fix i
assume "i < length ts"
have "r1 $ i = lookup (row_to_poly ts r1) (ts ! i)"
by (simp only: lookup_row_to_poly[OF assms(1) assms(2) ‹i < length ts›])
also from assms(4) have "... = lookup (row_to_poly ts r2) (ts ! i)" by simp
also from assms(1) assms(3) ‹i < length ts› have "... = r2 $ i" by (rule lookup_row_to_poly)
finally show "r1 $ i = r2 $ i" .
qed
lemma row_to_poly_vec_plus:
assumes "distinct ts" and "length ts = n"
shows "row_to_poly ts (vec n (f1 + f2)) = row_to_poly ts (vec n f1) + row_to_poly ts (vec n f2)"
proof (rule poly_mapping_eqI)
fix t
show "lookup (row_to_poly ts (vec n (f1 + f2))) t =
lookup (row_to_poly ts (vec n f1) + row_to_poly ts (vec n f2)) t"
(is "lookup ?l t = lookup (?r1 + ?r2) t")
proof (cases "t ∈ set ts")
case True
then obtain j where j: "j < length ts" and t: "t = ts ! j" by (metis in_set_conv_nth)
have d1: "dim_vec (vec n f1) = length ts" and d2: "dim_vec (vec n f2) = length ts"
and da: "dim_vec (vec n (f1 + f2)) = length ts" by (simp_all add: assms(2))
from j have j': "j < n" by (simp only: assms(2))
show ?thesis
by (simp only: t lookup_add lookup_row_to_poly[OF assms(1) d1 j]
lookup_row_to_poly[OF assms(1) d2 j] lookup_row_to_poly[OF assms(1) da j] index_vec[OF j'],
simp only: plus_fun_def)
next
case False
with keys_row_to_poly[of ts "vec n (f1 + f2)"] keys_row_to_poly[of ts "vec n f1"]
keys_row_to_poly[of ts "vec n f2"] have "t ∉ keys ?l" and "t ∉ keys ?r1" and "t ∉ keys ?r2"
by auto
from this(2) this(3) have "t ∉ keys (?r1 + ?r2)"
by (meson Poly_Mapping.keys_add UnE in_mono)
with ‹t ∉ keys ?l› show ?thesis by (simp add: in_keys_iff)
qed
qed
lemma row_to_poly_vec_sum:
assumes "distinct ts" and "length ts = n"
shows "row_to_poly ts (vec n (λj. ∑i∈I. f i j)) = ((∑i∈I. row_to_poly ts (vec n (f i)))::'t ⇒⇩0 'b::comm_monoid_add)"
proof (cases "finite I")
case True
thus ?thesis
proof (induct I)
case empty
thus ?case by (simp add: zero_vec_def[symmetric] assms(2)[symmetric])
next
case (insert x I)
have "row_to_poly ts (vec n (λj. ∑i∈insert x I. f i j)) = row_to_poly ts (vec n (λj. f x j + (∑i∈I. f i j)))"
by (simp add: insert(1) insert(2))
also have "... = row_to_poly ts (vec n (f x + (λj. (∑i∈I. f i j))))" by (simp only: plus_fun_def)
also from assms have "... = row_to_poly ts (vec n (f x)) + row_to_poly ts (vec n (λj. (∑i∈I. f i j)))"
by (rule row_to_poly_vec_plus)
also have "... = row_to_poly ts (vec n (f x)) + (∑i∈I. row_to_poly ts (vec n (f i)))"
by (simp only: insert(3))
also have "... = (∑i∈insert x I. row_to_poly ts (vec n (f i)))"
by (simp add: insert(1) insert(2))
finally show ?case .
qed
next
case False
thus ?thesis by (simp add: zero_vec_def[symmetric] assms(2)[symmetric])
qed
lemma row_to_poly_smult:
assumes "distinct ts" and "dim_vec r = length ts"
shows "row_to_poly ts (c ⋅⇩v r) = c ⋅ (row_to_poly ts r)"
proof (rule poly_mapping_eqI, simp only: lookup_map_scale)
fix t
show "lookup (row_to_poly ts (c ⋅⇩v r)) t = c * lookup (row_to_poly ts r) t" (is "lookup ?l t = c * lookup ?r t")
proof (cases "t ∈ set ts")
case True
then obtain j where j: "j < length ts" and t: "t = ts ! j" by (metis in_set_conv_nth)
from assms(2) have dm: "dim_vec (c ⋅⇩v r) = length ts" by simp
from j have j': "j < dim_vec r" by (simp only: assms(2))
show ?thesis
by (simp add: t lookup_row_to_poly[OF assms j] lookup_row_to_poly[OF assms(1) dm j] index_smult_vec(1)[OF j'])
next
case False
with keys_row_to_poly[of ts "c ⋅⇩v r"] keys_row_to_poly[of ts r] have
"t ∉ keys ?l" and "t ∉ keys ?r" by auto
thus ?thesis by (simp add: in_keys_iff)
qed
qed
lemma poly_to_row_Nil [simp]: "poly_to_row [] p = vec 0 f"
proof -
have "dim_vec (poly_to_row [] p) = 0" by (simp add: dim_poly_to_row)
thus ?thesis by auto
qed
lemma polys_to_mat_Nil [simp]: "polys_to_mat ts [] = mat 0 (length ts) f"
by (simp add: polys_to_mat_def mat_eq_iff)
lemma dim_row_polys_to_mat[simp]: "dim_row (polys_to_mat ts ps) = length ps"
by (simp add: polys_to_mat_def)
lemma dim_col_polys_to_mat[simp]: "dim_col (polys_to_mat ts ps) = length ts"
by (simp add: polys_to_mat_def)
lemma polys_to_mat_index:
assumes "i < length ps" and "j < length ts"
shows "(polys_to_mat ts ps) $$ (i, j) = lookup (ps ! i) (ts ! j)"
by (simp add: polys_to_mat_def index_mat(1)[OF assms] mat_of_rows_def nth_map[OF assms(1)],
rule poly_to_row_index, fact)
lemma row_polys_to_mat:
assumes "i < length ps"
shows "row (polys_to_mat ts ps) i = poly_to_row ts (ps ! i)"
proof -
have "row (polys_to_mat ts ps) i = (map (poly_to_row ts) ps) ! i" unfolding polys_to_mat_def
proof (rule mat_of_rows_row)
from assms show "i < length (map (poly_to_row ts) ps)" by simp
next
show "map (poly_to_row ts) ps ! i ∈ carrier_vec (length ts)" unfolding nth_map[OF assms]
by (rule carrier_vecI, fact dim_poly_to_row)
qed
also from assms have "... = poly_to_row ts (ps ! i)" by (rule nth_map)
finally show ?thesis .
qed
lemma col_polys_to_mat:
assumes "j < length ts"
shows "col (polys_to_mat ts ps) j = vec_of_list (map (λp. lookup p (ts ! j)) ps)"
by (simp add: vec_of_list_alt col_def, rule vec_cong, rule refl, simp add: polys_to_mat_index assms)
lemma length_mat_to_polys[simp]: "length (mat_to_polys ts A) = dim_row A"
by (simp add: mat_to_polys_def mat_to_list_def)
lemma mat_to_polys_nth:
assumes "i < dim_row A"
shows "(mat_to_polys ts A) ! i = row_to_poly ts (row A i)"
proof -
from assms have "i < length (rows A)" by (simp only: length_rows)
thus ?thesis by (simp add: mat_to_polys_def)
qed
lemma Keys_mat_to_polys: "Keys (set (mat_to_polys ts A)) ⊆ set ts"
proof
fix t
assume "t ∈ Keys (set (mat_to_polys ts A))"
then obtain p where "p ∈ set (mat_to_polys ts A)" and t: "t ∈ keys p" by (rule in_KeysE)
from this(1) obtain i where "i < length (mat_to_polys ts A)" and p: "p = (mat_to_polys ts A) ! i"
by (metis in_set_conv_nth)
from this(1) have "i < dim_row A" by simp
with p have "p = row_to_poly ts (row A i)" by (simp only: mat_to_polys_nth)
with t have "t ∈ keys (row_to_poly ts (row A i))" by simp
also have "... ⊆ set ts" by (fact keys_row_to_poly)
finally show "t ∈ set ts" .
qed
lemma polys_to_mat_to_polys:
assumes "Keys (set ps) ⊆ set ts"
shows "mat_to_polys ts (polys_to_mat ts ps) = (ps::('t ⇒⇩0 'b::semiring_1) list)"
unfolding mat_to_polys_def mat_to_list_def
proof (rule nth_equalityI, simp_all)
fix i
assume "i < length ps"
have *: "keys (ps ! i) ⊆ set ts"
using ‹i < length ps› assms keys_subset_Keys nth_mem by blast
show "row_to_poly ts (row (polys_to_mat ts ps) i) = ps ! i"
by (simp only: row_polys_to_mat[OF ‹i < length ps›] poly_to_row_to_poly[OF *])
qed
lemma mat_to_polys_to_mat:
assumes "distinct ts" and "length ts = dim_col A"
shows "(polys_to_mat ts (mat_to_polys ts A)) = A"
proof
fix i j
assume i: "i < dim_row A" and j: "j < dim_col A"
hence i': "i < length (mat_to_polys ts A)" and j': "j < length ts" by (simp, simp only: assms(2))
have r: "dim_vec (row A i) = length ts" by (simp add: assms(2))
show "polys_to_mat ts (mat_to_polys ts A) $$ (i, j) = A $$ (i, j)"
by (simp only: polys_to_mat_index[OF i' j'] mat_to_polys_nth[OF ‹i < dim_row A›]
lookup_row_to_poly[OF assms(1) r j'] index_row(1)[OF i j])
qed (simp_all add: assms)
subsection ‹Properties of Macaulay Matrices›
lemma row_to_poly_vec_times:
assumes "distinct ts" and "length ts = dim_col A"
shows "row_to_poly ts (v ⇩v* A) = ((∑i=0..<dim_row A. (v $ i) ⋅ (row_to_poly ts (row A i)))::'t ⇒⇩0 'b::comm_semiring_0)"
proof (simp add: mult_vec_mat_def scalar_prod_def row_to_poly_vec_sum[OF assms], rule sum.cong, rule)
fix i
assume "i ∈ {0..<dim_row A}"
hence "i < dim_row A" by simp
have "dim_vec (row A i) = length ts" by (simp add: assms(2))
have *: "vec (dim_col A) (λj. col A j $ i) = vec (dim_col A) (λj. A $$ (i, j))"
by (rule vec_cong, rule refl, simp add: ‹i < dim_row A›)
have "vec (dim_col A) (λj. v $ i * col A j $ i) = v $ i ⋅⇩v vec (dim_col A) (λj. col A j $ i)"
by (simp only: vec_scalar_mult_fun)
also have "... = v $ i ⋅⇩v (row A i)" by (simp only: * row_def[symmetric])
finally show "row_to_poly ts (vec (dim_col A) (λj. v $ i * col A j $ i)) =
(v $ i) ⋅ (row_to_poly ts (row A i))"
by (simp add: row_to_poly_smult[OF assms(1) ‹dim_vec (row A i) = length ts›])
qed
lemma vec_times_polys_to_mat:
assumes "Keys (set ps) ⊆ set ts" and "v ∈ carrier_vec (length ps)"
shows "row_to_poly ts (v ⇩v* (polys_to_mat ts ps)) = (∑(c, p)←zip (list_of_vec v) ps. c ⋅ p)"
(is "?l = ?r")
proof -
from assms have *: "dim_vec v = length ps" by (simp only: carrier_dim_vec)
have eq: "map (λi. v ∙ col (polys_to_mat ts ps) i) [0..<length ts] =
map (λs. v ∙ (vec_of_list (map (λp. lookup p s) ps))) ts"
proof (rule nth_equalityI, simp_all)
fix i
assume "i < length ts"
hence "col (polys_to_mat ts ps) i = vec_of_list (map (λp. lookup p (ts ! i)) ps)"
by (rule col_polys_to_mat)
thus "v ∙ col (polys_to_mat ts ps) i = v ∙ map_vec (λp. lookup p (ts ! i)) (vec_of_list ps)"
by simp
qed
show ?thesis
proof (rule poly_mapping_eqI, simp add: mult_vec_mat_def row_to_poly_def lookup_list_to_poly
eq list_to_fun_def map_of_zip_map lookup_sum_list o_def, intro conjI impI)
fix t
assume "t ∈ set ts"
have "v ∙ vec_of_list (map (λp. lookup p t) ps) =
(∑(c, p)←zip (list_of_vec v) ps. lookup (c ⋅ p) t)"
proof (simp add: scalar_prod_def vec_of_list_index)
have "(∑i = 0..<length ps. v $ i * lookup (ps ! i) t) =
(∑i = 0..<length ps. (list_of_vec v) ! i * lookup (ps ! i) t)"
by (rule sum.cong, rule refl, simp add: *)
also have "... = (∑(c, p)←zip (list_of_vec v) ps. c * lookup p t)"
by (simp only: sum_set_upt_eq_sum_list, rule sum_list_upt_zip, simp only: length_list_of_vec *)
finally show "(∑i = 0..<length ps. v $ i * lookup (ps ! i) t) =
(∑(c, p)←zip (list_of_vec v) ps. c * lookup p t)" .
qed
thus "v ∙ map_vec (λp. lookup p t) (vec_of_list ps) =
(∑x←zip (list_of_vec v) ps. lookup (case x of (c, x) ⇒ c ⋅ x) t)"
by (metis (mono_tags, lifting) case_prod_conv cond_case_prod_eta vec_of_list_map)
next
fix t
assume "t ∉ set ts"
with assms(1) have "t ∉ Keys (set ps)" by auto
have "(∑(c, p)←zip (list_of_vec v) ps. lookup (c ⋅ p) t) = 0"
proof (rule sum_list_zeroI, rule, simp)
fix x
assume "x ∈ (λ(c, p). c * lookup p t) ` set (zip (list_of_vec v) ps)"
then obtain c p where cp: "(c, p) ∈ set (zip (list_of_vec v) ps)"
and x: "x = c * lookup p t" by auto
from cp have "p ∈ set ps" by (rule set_zip_rightD)
with ‹t ∉ Keys (set ps)› have "t ∉ keys p" by (auto intro: in_KeysI)
thus "x = 0" by (simp add: x in_keys_iff)
qed
thus "(∑x←zip (list_of_vec v) ps. lookup (case x of (c, x) ⇒ c ⋅ x) t) = 0"
by (metis (mono_tags, lifting) case_prod_conv cond_case_prod_eta)
qed
qed
lemma row_space_subset_phull:
assumes "Keys (set ps) ⊆ set ts"
shows "row_to_poly ts ` row_space (polys_to_mat ts ps) ⊆ phull (set ps)"
(is "?r ⊆ ?h")
proof
fix q
assume "q ∈ ?r"
then obtain x where x1: "x ∈ row_space (polys_to_mat ts ps)"
and q1: "q = row_to_poly ts x" ..
from x1 obtain v where v: "v ∈ carrier_vec (dim_row (polys_to_mat ts ps))" and x: "x = v ⇩v* polys_to_mat ts ps"
by (rule row_spaceE)
from v have "v ∈ carrier_vec (length ps)" by (simp only: dim_row_polys_to_mat)
thm vec_times_polys_to_mat
with x q1 have q: "q = (∑(c, p)←zip (list_of_vec v) ps. c ⋅ p)"
by (simp add: vec_times_polys_to_mat[OF assms])
show "q ∈ ?h" unfolding q by (rule phull.span_listI)
qed
lemma phull_subset_row_space:
assumes "Keys (set ps) ⊆ set ts"
shows "phull (set ps) ⊆ row_to_poly ts ` row_space (polys_to_mat ts ps)"
(is "?h ⊆ ?r")
proof
fix q
assume "q ∈ ?h"
then obtain cs where l: "length cs = length ps" and q: "q = (∑(c, p)←zip cs ps. c ⋅ p)"
by (rule phull.span_listE)
let ?v = "vec_of_list cs"
from l have *: "?v ∈ carrier_vec (length ps)" by (simp only: carrier_dim_vec dim_vec_of_list)
let ?q = "?v ⇩v* polys_to_mat ts ps"
show "q ∈ ?r"
proof
show "q = row_to_poly ts ?q"
by (simp add: vec_times_polys_to_mat[OF assms *] q list_vec)
next
show "?q ∈ row_space (polys_to_mat ts ps)" by (rule row_spaceI, rule)
qed
qed
lemma row_space_eq_phull:
assumes "Keys (set ps) ⊆ set ts"
shows "row_to_poly ts ` row_space (polys_to_mat ts ps) = phull (set ps)"
by (rule, rule row_space_subset_phull, fact, rule phull_subset_row_space, fact)
lemma row_space_row_echelon_eq_phull:
assumes "Keys (set ps) ⊆ set ts"
shows "row_to_poly ts ` row_space (row_echelon (polys_to_mat ts ps)) = phull (set ps)"
by (simp add: row_space_eq_phull[OF assms])
lemma phull_row_echelon:
assumes "Keys (set ps) ⊆ set ts" and "distinct ts"
shows "phull (set (mat_to_polys ts (row_echelon (polys_to_mat ts ps)))) = phull (set ps)"
proof -
have len_ts: "length ts = dim_col (row_echelon (polys_to_mat ts ps))" by simp
have *: "Keys (set (mat_to_polys ts (row_echelon (polys_to_mat ts ps)))) ⊆ set ts"
by (fact Keys_mat_to_polys)
show ?thesis
by (simp only: row_space_eq_phull[OF *, symmetric] mat_to_polys_to_mat[OF assms(2) len_ts],
rule row_space_row_echelon_eq_phull, fact)
qed
lemma pmdl_row_echelon:
assumes "Keys (set ps) ⊆ set ts" and "distinct ts"
shows "pmdl (set (mat_to_polys ts (row_echelon (polys_to_mat ts ps)))) = pmdl (set ps)"
(is "?l = ?r")
proof
show "?l ⊆ ?r"
by (rule pmdl.span_subset_spanI, rule subset_trans, rule phull.span_superset,
simp only: phull_row_echelon[OF assms] phull_subset_module)
next
show "?r ⊆ ?l"
by (rule pmdl.span_subset_spanI, rule subset_trans, rule phull.span_superset,
simp only: phull_row_echelon[OF assms, symmetric] phull_subset_module)
qed
end
context ordered_term
begin
lemma lt_row_to_poly_pivot_fun:
assumes "card S = dim_col (A::'b::semiring_1 mat)" and "pivot_fun A f (dim_col A)"
and "i < dim_row A" and "f i < dim_col A"
shows "lt ((mat_to_polys (pps_to_list S) A) ! i) = (pps_to_list S) ! (f i)"
proof -
let ?ts = "pps_to_list S"
have len_ts: "length ?ts = dim_col A" by (simp add: length_pps_to_list assms(1))
show ?thesis
proof (simp add: mat_to_polys_nth[OF assms(3)], rule lt_eqI)
have "lookup (row_to_poly ?ts (row A i)) (?ts ! f i) = (row A i) $ (f i)"
by (rule lookup_row_to_poly, fact distinct_pps_to_list, simp_all add: len_ts assms(4))
also have "... = A $$ (i, f i)" using assms(3) assms(4) by simp
also have "... = 1" by (rule pivot_funD, rule refl, fact+)
finally show "lookup (row_to_poly ?ts (row A i)) (?ts ! f i) ≠ 0" by simp
next
fix u
assume a: "lookup (row_to_poly ?ts (row A i)) u ≠ 0"
then obtain j where j: "j < length ?ts" and u: "u = ?ts ! j"
by (rule lookup_row_to_poly_not_zeroE)
from j have "j < card S" and "j < dim_col A" by (simp only: length_pps_to_list, simp only: len_ts)
from a have "0 ≠ lookup (row_to_poly ?ts (row A i)) (?ts ! j)" by (simp add: u)
also have "lookup (row_to_poly ?ts (row A i)) (?ts ! j) = (row A i) $ j"
by (rule lookup_row_to_poly, fact distinct_pps_to_list, simp add: len_ts, fact)
finally have "A $$ (i, j) ≠ 0" using assms(3) ‹j < dim_col A› by simp
from _ ‹j < card S› show "u ≼⇩t ?ts ! f i" unfolding u
proof (rule pps_to_list_nth_leI)
show "f i ≤ j"
proof (rule ccontr)
assume "¬ f i ≤ j"
hence "j < f i" by simp
have "A $$ (i, j) = 0" by (rule pivot_funD, rule refl, fact+)
with ‹A $$ (i, j) ≠ 0› show False ..
qed
qed
qed
qed
lemma lc_row_to_poly_pivot_fun:
assumes "card S = dim_col (A::'b::semiring_1 mat)" and "pivot_fun A f (dim_col A)"
and "i < dim_row A" and "f i < dim_col A"
shows "lc ((mat_to_polys (pps_to_list S) A) ! i) = 1"
proof -
let ?ts = "pps_to_list S"
have len_ts: "length ?ts = dim_col A" by (simp only: length_pps_to_list assms(1))
have "lookup (row_to_poly ?ts (row A i)) (?ts ! f i) = (row A i) $ (f i)"
by (rule lookup_row_to_poly, fact distinct_pps_to_list, simp_all add: len_ts assms(4))
also have "... = A $$ (i, f i)" using assms(3) assms(4) by simp
finally have eq: "lookup (row_to_poly ?ts (row A i)) (?ts ! f i) = A $$ (i, f i)" .
show ?thesis
by (simp only: lc_def lt_row_to_poly_pivot_fun[OF assms], simp only: mat_to_polys_nth[OF assms(3)] eq,
rule pivot_funD, rule refl, fact+)
qed
lemma lt_row_to_poly_pivot_fun_less:
assumes "card S = dim_col (A::'b::semiring_1 mat)" and "pivot_fun A f (dim_col A)"
and "i1 < i2" and "i2 < dim_row A" and "f i1 < dim_col A" and "f i2 < dim_col A"
shows "(pps_to_list S) ! (f i2) ≺⇩t (pps_to_list S) ! (f i1)"
proof -
let ?ts = "pps_to_list S"
have len_ts: "length ?ts = dim_col A" by (simp add: length_pps_to_list assms(1))
from assms(3) assms(4) have "i1 < dim_row A" by simp
show ?thesis
by (rule pps_to_list_nth_lessI, rule pivot_fun_mono_strict[where ?f=f], fact, fact, fact, fact,
simp only: assms(1) assms(6))
qed
lemma lt_row_to_poly_pivot_fun_eqD:
assumes "card S = dim_col (A::'b::semiring_1 mat)" and "pivot_fun A f (dim_col A)"
and "i1 < dim_row A" and "i2 < dim_row A" and "f i1 < dim_col A" and "f i2 < dim_col A"
and "(pps_to_list S) ! (f i1) = (pps_to_list S) ! (f i2)"
shows "i1 = i2"
proof (rule linorder_cases)
assume "i1 < i2"
from assms(1) assms(2) this assms(4) assms(5) assms(6) have
"(pps_to_list S) ! (f i2) ≺⇩t (pps_to_list S) ! (f i1)" by (rule lt_row_to_poly_pivot_fun_less)
with assms(7) show ?thesis by auto
next
assume "i2 < i1"
from assms(1) assms(2) this assms(3) assms(6) assms(5) have
"(pps_to_list S) ! (f i1) ≺⇩t (pps_to_list S) ! (f i2)" by (rule lt_row_to_poly_pivot_fun_less)
with assms(7) show ?thesis by auto
qed
lemma lt_row_to_poly_pivot_in_keysD:
assumes "card S = dim_col (A::'b::semiring_1 mat)" and "pivot_fun A f (dim_col A)"
and "i1 < dim_row A" and "i2 < dim_row A" and "f i1 < dim_col A"
and "(pps_to_list S) ! (f i1) ∈ keys ((mat_to_polys (pps_to_list S) A) ! i2)"
shows "i1 = i2"
proof (rule ccontr)
assume "i1 ≠ i2"
hence "i2 ≠ i1" by simp
let ?ts = "pps_to_list S"
have len_ts: "length ?ts = dim_col A" by (simp only: length_pps_to_list assms(1))
from assms(6) have "0 ≠ lookup (row_to_poly ?ts (row A i2)) (?ts ! (f i1))"
by (auto simp: mat_to_polys_nth[OF assms(4)])
also have "lookup (row_to_poly ?ts (row A i2)) (?ts ! (f i1)) = (row A i2) $ (f i1)"
by (rule lookup_row_to_poly, fact distinct_pps_to_list, simp_all add: len_ts assms(5))
finally have "A $$ (i2, f i1) ≠ 0" using assms(4) assms(5) by simp
moreover have "A $$ (i2, f i1) = 0" by (rule pivot_funD(5), rule refl, fact+)
ultimately show False ..
qed
lemma lt_row_space_pivot_fun:
assumes "card S = dim_col (A::'b::{comm_semiring_0,semiring_1_no_zero_divisors} mat)"
and "pivot_fun A f (dim_col A)" and "p ∈ row_to_poly (pps_to_list S) ` row_space A" and "p ≠ 0"
shows "lt p ∈ lt_set (set (mat_to_polys (pps_to_list S) A))"
proof -
let ?ts = "pps_to_list S"
let ?I = "{0..<dim_row A}"
have len_ts: "length ?ts = dim_col A" by (simp add: length_pps_to_list assms(1))
from assms(3) obtain x where "x ∈ row_space A" and p: "p = row_to_poly ?ts x" ..
from this(1) obtain v where "v ∈ carrier_vec (dim_row A)" and x: "x = v ⇩v* A" by (rule row_spaceE)
have p': "p = (∑i∈?I. (v $ i) ⋅ (row_to_poly ?ts (row A i)))"
unfolding p x by (rule row_to_poly_vec_times, fact distinct_pps_to_list, fact len_ts)
have "lt (∑i = 0..<dim_row A. (v $ i) ⋅ (row_to_poly ?ts (row A i)))
∈ lt_set ((λi. (v $ i) ⋅ (row_to_poly ?ts (row A i))) ` {0..<dim_row A})"
proof (rule lt_sum_distinct_in_lt_set, rule, simp add: p'[symmetric] ‹p ≠ 0›)
fix i1 i2
let ?p1 = "(v $ i1) ⋅ (row_to_poly ?ts (row A i1))"
let ?p2 = "(v $ i2) ⋅ (row_to_poly ?ts (row A i2))"
assume "i1 ∈ ?I" and "i2 ∈ ?I"
hence "i1 < dim_row A" and "i2 < dim_row A" by simp_all
assume "?p1 ≠ 0"
hence "v $ i1 ≠ 0" and "row_to_poly ?ts (row A i1) ≠ 0" by auto
hence "row A i1 ≠ 0⇩v (length ?ts)" by auto
hence "f i1 < dim_col A"
by (simp add: len_ts row_not_zero_iff_pivot_fun[OF assms(2) ‹i1 < dim_row A›])
have "lt ?p1 = lt (row_to_poly ?ts (row A i1))" by (rule lt_map_scale, fact)
also have "... = lt ((mat_to_polys ?ts A) ! i1)" by (simp only: mat_to_polys_nth[OF ‹i1 < dim_row A›])
also have "... = ?ts ! (f i1)" by (rule lt_row_to_poly_pivot_fun, fact+)
finally have lt1: "lt ?p1 = ?ts ! (f i1)" .
assume "?p2 ≠ 0"
hence "v $ i2 ≠ 0" and "row_to_poly ?ts (row A i2) ≠ 0" by auto
hence "row A i2 ≠ 0⇩v (length ?ts)" by auto
hence "f i2 < dim_col A"
by (simp add: len_ts row_not_zero_iff_pivot_fun[OF assms(2) ‹i2 < dim_row A›])
have "lt ?p2 = lt (row_to_poly ?ts (row A i2))" by (rule lt_map_scale, fact)
also have "... = lt ((mat_to_polys ?ts A) ! i2)" by (simp only: mat_to_polys_nth[OF ‹i2 < dim_row A›])
also have "... = ?ts ! (f i2)" by (rule lt_row_to_poly_pivot_fun, fact+)
finally have lt2: "lt ?p2 = ?ts ! (f i2)" .
assume "lt ?p1 = lt ?p2"
with assms(1) assms(2) ‹i1 < dim_row A› ‹i2 < dim_row A› ‹f i1 < dim_col A› ‹f i2 < dim_col A›
show "i1 = i2" unfolding lt1 lt2 by (rule lt_row_to_poly_pivot_fun_eqD)
qed
also have "... ⊆ lt_set ((λi. row_to_poly ?ts (row A i)) ` {0..<dim_row A})"
proof
fix s
assume "s ∈ lt_set ((λi. (v $ i) ⋅ (row_to_poly ?ts (row A i))) ` {0..<dim_row A})"
then obtain f
where "f ∈ (λi. (v $ i) ⋅ (row_to_poly ?ts (row A i))) ` {0..<dim_row A}"
and "f ≠ 0" and "lt f = s" by (rule lt_setE)
from this(1) obtain i where "i ∈ {0..<dim_row A}"
and f: "f = (v $ i) ⋅ (row_to_poly ?ts (row A i))" ..
from this(2) ‹f ≠ 0› have "v $ i ≠ 0" and **: "row_to_poly ?ts (row A i) ≠ 0" by auto
from ‹lt f = s› have "s = lt ((v $ i) ⋅ (row_to_poly ?ts (row A i)))" by (simp only: f)
also from ‹v $ i ≠ 0› have "... = lt (row_to_poly ?ts (row A i))" by (rule lt_map_scale)
finally have s: "s = lt (row_to_poly ?ts (row A i))" .
show "s ∈ lt_set ((λi. row_to_poly ?ts (row A i)) ` {0..<dim_row A})"
unfolding s by (rule lt_setI, rule, rule refl, fact+)
qed
also have "... = lt_set ((λr. row_to_poly ?ts r) ` (row A ` {0..<dim_row A}))"
by (simp only: image_comp o_def)
also have "... = lt_set (set (map (λr. row_to_poly ?ts r) (map (row A) [0..<dim_row A])))"
by (metis image_set set_upt)
also have "... = lt_set (set (mat_to_polys ?ts A))" by (simp only: mat_to_polys_def rows_def)
finally show ?thesis unfolding p' .
qed
subsection ‹Functions ‹Macaulay_mat› and ‹Macaulay_list››
definition Macaulay_mat :: "('t ⇒⇩0 'b) list ⇒ 'b::field mat"
where "Macaulay_mat ps = polys_to_mat (Keys_to_list ps) ps"
definition Macaulay_list :: "('t ⇒⇩0 'b) list ⇒ ('t ⇒⇩0 'b::field) list"
where "Macaulay_list ps =
filter (λp. p ≠ 0) (mat_to_polys (Keys_to_list ps) (row_echelon (Macaulay_mat ps)))"
lemma dim_Macaulay_mat[simp]:
"dim_row (Macaulay_mat ps) = length ps"
"dim_col (Macaulay_mat ps) = card (Keys (set ps))"
by (simp_all add: Macaulay_mat_def length_Keys_to_list)
lemma Macaulay_list_Nil [simp]: "Macaulay_list [] = ([]::('t ⇒⇩0 'b::field) list)" (is "?l = _")
proof -
have "length ?l ≤ length (mat_to_polys (Keys_to_list ([]::('t ⇒⇩0 'b) list))
(row_echelon (Macaulay_mat ([]::('t ⇒⇩0 'b) list))))"
unfolding Macaulay_list_def by (fact length_filter_le)
also have "... = 0" by simp
finally show ?thesis by simp
qed
lemma set_Macaulay_list:
"set (Macaulay_list ps) =
set (mat_to_polys (Keys_to_list ps) (row_echelon (Macaulay_mat ps))) - {0}"
by (auto simp add: Macaulay_list_def)
lemma Keys_Macaulay_list: "Keys (set (Macaulay_list ps)) ⊆ Keys (set ps)"
proof -
have "Keys (set (Macaulay_list ps)) ⊆ set (Keys_to_list ps)"
by (simp only: set_Macaulay_list Keys_minus_zero, fact Keys_mat_to_polys)
also have "... = Keys (set ps)" by (fact set_Keys_to_list)
finally show ?thesis .
qed
lemma in_Macaulay_listE:
assumes "p ∈ set (Macaulay_list ps)"
and "pivot_fun (row_echelon (Macaulay_mat ps)) f (dim_col (row_echelon (Macaulay_mat ps)))"
obtains i where "i < dim_row (row_echelon (Macaulay_mat ps))"
and "p = (mat_to_polys (Keys_to_list ps) (row_echelon (Macaulay_mat ps))) ! i"
and "f i < dim_col (row_echelon (Macaulay_mat ps))"
proof -
let ?ts = "Keys_to_list ps"
let ?A = "Macaulay_mat ps"
let ?E = "row_echelon ?A"
from assms(1) have "p ∈ set (mat_to_polys ?ts ?E) - {0}" by (simp add: set_Macaulay_list)
hence "p ∈ set (mat_to_polys ?ts ?E)" and "p ≠ 0" by auto
from this(1) obtain i where "i < length (mat_to_polys ?ts ?E)" and p: "p = (mat_to_polys ?ts ?E) ! i"
by (metis in_set_conv_nth)
from this(1) have "i < dim_row ?E" and "i < dim_row ?A" by simp_all
from this(1) p show ?thesis
proof
from ‹p ≠ 0› have "0 ≠ (mat_to_polys ?ts ?E) ! i" by (simp only: p)
also have "(mat_to_polys ?ts ?E) ! i = row_to_poly ?ts (row ?E i)"
by (simp only: Macaulay_list_def mat_to_polys_nth[OF ‹i < dim_row ?E›])
finally have *: "row_to_poly ?ts (row ?E i) ≠ 0" by simp
have "row ?E i ≠ 0⇩v (length ?ts)"
proof
assume "row ?E i = 0⇩v (length ?ts)"
with * show False by simp
qed
hence "row ?E i ≠ 0⇩v (dim_col ?E)" by (simp add: length_Keys_to_list)
thus "f i < dim_col ?E"
by (simp only: row_not_zero_iff_pivot_fun[OF assms(2) ‹i < dim_row ?E›])
qed
qed
lemma phull_Macaulay_list: "phull (set (Macaulay_list ps)) = phull (set ps)"
proof -
have *: "Keys (set ps) ⊆ set (Keys_to_list ps)"
by (simp add: set_Keys_to_list)
have "phull (set (Macaulay_list ps)) =
phull (set (mat_to_polys (Keys_to_list ps) (row_echelon (Macaulay_mat ps))))"
by (simp only: set_Macaulay_list phull.span_Diff_zero)
also have "... = phull (set ps)"
by (simp only: Macaulay_mat_def phull_row_echelon[OF * distinct_Keys_to_list])
finally show ?thesis .
qed
lemma pmdl_Macaulay_list: "pmdl (set (Macaulay_list ps)) = pmdl (set ps)"
proof -
have *: "Keys (set ps) ⊆ set (Keys_to_list ps)"
by (simp add: set_Keys_to_list)
have "pmdl (set (Macaulay_list ps)) =
pmdl (set (mat_to_polys (Keys_to_list ps) (row_echelon (Macaulay_mat ps))))"
by (simp only: set_Macaulay_list pmdl.span_Diff_zero)
also have "... = pmdl (set ps)"
by (simp only: Macaulay_mat_def pmdl_row_echelon[OF * distinct_Keys_to_list])
finally show ?thesis .
qed
lemma Macaulay_list_is_monic_set: "is_monic_set (set (Macaulay_list ps))"
proof (rule is_monic_setI)
let ?ts = "Keys_to_list ps"
let ?E = "row_echelon (Macaulay_mat ps)"
fix p
assume "p ∈ set (Macaulay_list ps)"
obtain h where "pivot_fun ?E h (dim_col ?E)" by (rule row_echelon_pivot_fun)
with ‹p ∈ set (Macaulay_list ps)› obtain i where "i < dim_row ?E"
and p: "p = (mat_to_polys ?ts ?E) ! i" and "h i < dim_col ?E"
by (rule in_Macaulay_listE)
show "lc p = 1" unfolding p Keys_to_list_eq_pps_to_list
by (rule lc_row_to_poly_pivot_fun, simp, fact+)
qed
lemma Macaulay_list_not_zero: "0 ∉ set (Macaulay_list ps)"
by (simp add: Macaulay_list_def)
lemma Macaulay_list_distinct_lt:
assumes "x ∈ set (Macaulay_list ps)" and "y ∈ set (Macaulay_list ps)"
and "x ≠ y"
shows "lt x ≠ lt y"
proof
let ?S = "Keys (set ps)"
let ?ts = "Keys_to_list ps"
let ?E = "row_echelon (Macaulay_mat ps)"
assume "lt x = lt y"
obtain h where pf: "pivot_fun ?E h (dim_col ?E)" by (rule row_echelon_pivot_fun)
with assms(1) obtain i1 where "i1 < dim_row ?E"
and x: "x = (mat_to_polys ?ts ?E) ! i1" and "h i1 < dim_col ?E"
by (rule in_Macaulay_listE)
from assms(2) pf obtain i2 where "i2 < dim_row ?E"
and y: "y = (mat_to_polys ?ts ?E) ! i2" and "h i2 < dim_col ?E"
by (rule in_Macaulay_listE)
have "lt x = ?ts ! (h i1)"
by (simp only: x Keys_to_list_eq_pps_to_list, rule lt_row_to_poly_pivot_fun, simp, fact+)
moreover have "lt y = ?ts ! (h i2)"
by (simp only: y Keys_to_list_eq_pps_to_list, rule lt_row_to_poly_pivot_fun, simp, fact+)
ultimately have "?ts ! (h i1) = ?ts ! (h i2)" by (simp only: ‹lt x = lt y›)
hence "pps_to_list (Keys (set ps)) ! h i1 = pps_to_list (Keys (set ps)) ! h i2"
by (simp only: Keys_to_list_eq_pps_to_list)
have "i1 = i2"
proof (rule lt_row_to_poly_pivot_fun_eqD)
show "card ?S = dim_col ?E" by simp
qed fact+
hence "x = y" by (simp only: x y)
with ‹x ≠ y› show False ..
qed
lemma Macaulay_list_lt:
assumes "p ∈ phull (set ps)" and "p ≠ 0"
obtains g where "g ∈ set (Macaulay_list ps)" and "g ≠ 0" and "lt p = lt g"
proof -
let ?S = "Keys (set ps)"
let ?ts = "Keys_to_list ps"
let ?E = "row_echelon (Macaulay_mat ps)"
let ?gs = "mat_to_polys ?ts ?E"
have "finite ?S" by (rule finite_Keys, rule)
have "?S ⊆ set ?ts" by (simp only: set_Keys_to_list)
from assms(1) ‹?S ⊆ set ?ts› have "p ∈ row_to_poly ?ts ` row_space ?E"
by (simp only: Macaulay_mat_def row_space_row_echelon_eq_phull[symmetric])
hence "p ∈ row_to_poly (pps_to_list ?S) ` row_space ?E"
by (simp only: Keys_to_list_eq_pps_to_list)
obtain f where "pivot_fun ?E f (dim_col ?E)" by (rule row_echelon_pivot_fun)
have "lt p ∈ lt_set (set ?gs)" unfolding Keys_to_list_eq_pps_to_list
by (rule lt_row_space_pivot_fun, simp, fact+)
then obtain g where "g ∈ set ?gs" and "g ≠ 0" and "lt g = lt p" by (rule lt_setE)
show ?thesis
proof
from ‹g ∈ set ?gs› ‹g ≠ 0› show "g ∈ set (Macaulay_list ps)" by (simp add: set_Macaulay_list)
next
from ‹lt g = lt p› show "lt p = lt g" by simp
qed fact
qed
end
end