# Theory Matrix_Vector_Extras

```(* Title: Matrix_Vector_Extras.thy
Author: Chelsea Edmonds
*)
section ‹ Matrix and Vector Additions ›

theory Matrix_Vector_Extras imports Set_Multiset_Extras Jordan_Normal_Form.Matrix
Design_Theory.Multisets_Extras "Groebner_Bases.Macaulay_Matrix" "Polynomial_Factorization.Missing_List"
begin

subsection ‹Vector Extras›
text ‹For ease of use, a number of additions to the existing vector library as initially developed
in the JNF AFP Entry, are given below›

text ‹We define the concept of summing up elements of a vector ›

definition (in comm_monoid_add) sum_vec :: "'a vec ⇒ 'a" where
"sum_vec v ≡ sum (λ i . v \$ i) {0..<dim_vec v}"

lemma sum_vec_vNil[simp]: "sum_vec vNil = 0"

lemma sum_vec_vCons: "sum_vec (vCons a v) = a + sum_vec v"
proof -
have 0: "a = (vCons a v) \$ 0"
by simp
have "sum_vec v = sum (λ i . v \$ i) {0..<dim_vec v}" by (simp add: sum_vec_def)
also have "... = sum (λ i . (vCons a v) \$ Suc i) {0..< dim_vec v}"
by force
also have "... = sum (λ i . (vCons a v) \$ i) {Suc 0..< (Suc (dim_vec v))}"
by (metis sum.shift_bounds_Suc_ivl)
finally have sum: "sum_vec v = sum (λ i . (vCons a v) \$ i) {Suc 0..< dim_vec (vCons a v)}" by simp
have "sum_vec (vCons a v) = sum (λ i . (vCons a v) \$ i){0..< dim_vec (vCons a v)}"
then have "sum_vec (vCons a v) = (vCons a v) \$ 0 + sum (λ i . (vCons a v) \$ i){Suc 0..< dim_vec (vCons a v)}"
by (metis dim_vec_vCons sum.atLeast_Suc_lessThan zero_less_Suc)
thus ?thesis using sum 0 by simp
qed

lemma sum_vec_list: "sum_list (list_of_vec v) = sum_vec v"

lemma sum_vec_mset: "sum_vec v = (∑ x ∈# (mset (list_of_vec v)) . x)"

lemma dim_vec_vCons_ne_0: "dim_vec (vCons a v) > 0"
by (cases v) simp_all

lemma sum_vec_vCons_lt:
assumes "⋀ i. i < dim_vec (vCons a v) ⟹ (vCons a v) \$ i ≤ (n ::int)"
assumes "sum_vec v ≤ m"
shows "sum_vec (vCons a v) ≤ n + m"
proof -
have split: "sum_vec (vCons a v) = a + sum_vec v" by (simp add: sum_vec_vCons)
have a: "(vCons a v) \$ 0 = a" by simp
then have "0 < dim_vec (vCons a v)" using dim_vec_vCons_ne_0 by simp
then have "a ≤ n" using assms by (metis a)
thus ?thesis using split assms
qed

lemma sum_vec_one_zero:
assumes "⋀ i. i < dim_vec (v :: int vec) ⟹ v \$ i ≤ (1 ::int)"
shows "sum_vec v ≤ dim_vec v"
using assms
proof (induct v)
case vNil
then show ?case by simp
next
case (vCons a v)
then have "(⋀ i. i < dim_vec v ⟹ v \$ i ≤ (1 ::int))"
using vCons.prems by force
then have lt: "sum_vec v ≤ int (dim_vec v)" by (simp add: vCons.hyps)
then show ?case using sum_vec_vCons_lt lt vCons.prems by simp
qed

text ‹Definition to convert a vector to a multiset ›

definition vec_mset:: "'a vec ⇒ 'a multiset" where
"vec_mset v ≡ image_mset (vec_index v) (mset_set {..<dim_vec v})"

lemma vec_elem_exists_mset: "(∃ i ∈ {..<dim_vec v}. v \$ i = x) ⟷ x ∈# vec_mset v"

lemma mset_vec_same_size: "dim_vec v = size (vec_mset v)"

lemma mset_vec_eq_mset_list: "vec_mset v = mset (list_of_vec v)"
(metis list_of_vec_map mset_map mset_set_upto_eq_mset_upto)

lemma vec_mset_img_map: "image_mset f (mset (xs)) = vec_mset (map_vec f (vec_of_list xs))"
by (metis list_vec mset_map mset_vec_eq_mset_list vec_of_list_map)

lemma vec_mset_vNil: "vec_mset vNil = {#}"

lemma vec_mset_vCons: "vec_mset (vCons x v) = add_mset x (vec_mset v)"
proof -
have "vec_mset (vCons x v) = mset (list_of_vec (vCons x v))"
then have "mset (list_of_vec (vCons x v)) = add_mset x (mset (list_of_vec v))"
by simp
thus ?thesis
by (metis mset_vec_eq_mset_list)
qed

lemma vec_mset_set: "vec_set v = set_mset (vec_mset v)"

lemma vCons_set_contains_in: "a ∈ set⇩v v ⟹ set⇩v (vCons a v) = set⇩v v"
by (metis remdups_mset_singleton_sum set_mset_remdups_mset vec_mset_set vec_mset_vCons)

lemma vCons_set_contains_add: "a ∉ set⇩v v ⟹ set⇩v (vCons a v) = set⇩v v ∪ {a}"
using vec_mset_set vec_mset_vCons

lemma setv_vec_mset_not_in_iff: "a ∉ set⇩v v ⟷ a ∉# vec_mset v"

text ‹Abbreviation for counting occurrences of an element in a vector ›

abbreviation "count_vec v a ≡ count (vec_mset v) a"

lemma vec_count_lt_dim: "count_vec v a ≤ dim_vec v"
by (metis mset_vec_same_size order_refl set_count_size_min)

lemma count_vec_empty: "dim_vec v = 0 ⟹ count_vec v a = 0"

lemma count_vec_vNil: "count_vec vNil a = 0"

lemma count_vec_vCons: "count_vec (vCons aa v) a = (if (aa = a) then count_vec v a + 1 else count_vec v a)"

lemma elem_exists_count_min: "∃ i ∈{..<dim_vec v}. v \$ i = x ⟹ count_vec v x ≥ 1"

lemma count_vec_count_mset: "vec_mset v = image_mset f A ⟹ count_vec v a = count (image_mset f A) a"
by (simp)

lemma count_vec_alt_list: "count_vec v a = length (filter (λy. a = y) (list_of_vec v))"
by (simp add: mset_vec_eq_mset_list) (metis count_mset)

lemma count_vec_alt: "count_vec v x = card { i. v \$ i = x ∧ i< dim_vec v}"
proof -
have "count_vec v x = count (image_mset ((\$) v) (mset_set {..<dim_vec v})) x" by (simp add: vec_mset_def)
also have "... = size {#a ∈# (image_mset ((\$) v) (mset_set {..<dim_vec v})) . x = a#}"
also have "... = size {#a ∈# (mset_set {..<dim_vec v}) . x = (v \$ a) #}"
finally have "count_vec v x = card {a ∈ {..<dim_vec v} . x = (v \$ a)}" by simp
thus ?thesis by (smt (verit) Collect_cong lessThan_iff)
qed

lemma count_vec_sum_ones:
fixes v :: "'a :: {ring_1} vec"
assumes "⋀ i. i < dim_vec v ⟹ v \$ i = 1 ∨ v \$ i = 0"
shows "of_nat (count_vec v 1) = sum_vec v"
using assms
proof (induct v)
case vNil
then show ?case
next
case (vCons a v)
then have lim: "dim_vec (vCons a v) ≥ 1"
by simp
have "(⋀ i. i < dim_vec v ⟹ v \$ i = 1 ∨ v\$ i = 0)"
using vCons.prems by force
then have hyp: "of_nat (count_vec v 1) = sum_vec v"
using vCons.hyps by blast
have "sum ((\$) (vCons a v)) {0..<dim_vec (vCons a v)} = sum_vec (vCons a v)"
then have sv: "sum ((\$) (vCons a v)) {0..<dim_vec (vCons a v)} = sum_vec (v) + a"
then show ?case using count_vec_vCons dim_vec_vCons_ne_0 sum_vec_vCons vCons.prems
qed

lemma count_vec_two_elems:
fixes v :: "'a :: {zero_neq_one} vec"
assumes "⋀ i. i < dim_vec v ⟹ v \$ i = 1 ∨ v \$ i = 0"
shows "count_vec v 1 + count_vec v 0 = dim_vec v"
proof -
have ss: "vec_set v ⊆ {0, 1}" using assms by (auto simp add: vec_set_def)
have "dim_vec v = size (vec_mset v)"
have "size (vec_mset v) = (∑ x ∈ (vec_set v) . count (vec_mset v) x)"
also have  "... = (∑ x ∈ {0, 1} . count (vec_mset v) x)"
using size_count_mset_ss ss
by (metis calculation finite.emptyI finite.insertI vec_mset_set)
finally have "size (vec_mset v) = count (vec_mset v) 0 + count (vec_mset v) 1" by simp
thus ?thesis
by (simp add: ‹dim_vec v = size (vec_mset v)›)
qed

lemma count_vec_sum_zeros:
fixes v :: "'a :: {ring_1} vec"
assumes "⋀ i. i < dim_vec v ⟹ v \$ i = 1 ∨ v \$ i = 0"
shows "of_nat (count_vec v 0) = of_nat (dim_vec v) - sum_vec v"
using count_vec_two_elems assms count_vec_sum_ones

lemma count_vec_sum_ones_alt:
fixes v :: "'a :: {ring_1} vec"
assumes "vec_set v ⊆ {0, 1}"
shows "of_nat (count_vec v 1) = sum_vec v"
proof -
have "⋀ i. i < dim_vec v ⟹ v \$ i = 1 ∨ v \$ i = 0" using assms
by (meson insertE singletonD subsetD vec_setI)
thus ?thesis using count_vec_sum_ones
by blast
qed

lemma setv_not_in_count0_iff: "a ∉ set⇩v v ⟷ count_vec v a = 0"
using setv_vec_mset_not_in_iff
by (metis count_eq_zero_iff)

lemma sum_count_vec:
assumes "finite (set⇩v v)"
shows "(∑ i ∈ set⇩v v. count_vec v i) = dim_vec v"
using assms proof (induct "v")
case vNil
then show ?case
next
case (vCons a v)
then show ?case proof (cases "a ∈ set⇩v v")
case True
have cv: "⋀ x. x ∈(set⇩v v) - {a} ⟹ count_vec (vCons a v) x = count_vec v x"
using count_vec_vCons by (metis DiffD2 singletonI)
then have "sum (count_vec (vCons a v)) (set⇩v (vCons a v)) =  sum (count_vec (vCons a v)) (set⇩v v)"
using vCons_set_contains_in True by metis
also have "... = count_vec (vCons a v) a + sum (count_vec (vCons a v)) ((set⇩v v) - {a})"
using sum.remove True vCons.prems(1) by (metis vCons_set_contains_in)
also have "... = count_vec v a + 1 + sum (count_vec v) ((set⇩v v) - {a})"
using cv count_vec_vCons by (metis sum.cong)
also have "... = 1 + sum (count_vec v) ((set⇩v v))"
using sum.remove add.commute vCons.prems vCons_set_contains_in True
also have "... = 1 + dim_vec v" using vCons.hyps
by (metis True vCons.prems vCons_set_contains_in)
finally show ?thesis by simp
next
case False
then have cv: "⋀ x. x ∈(set⇩v v) ⟹ count_vec (vCons a v) x = count_vec v x"
using count_vec_vCons by (metis)
have f: "finite (set⇩v v)"
using vCons.prems False vCons_set_contains_add by (metis Un_infinite)
have "sum (count_vec (vCons a v)) (set⇩v (vCons a v)) =
count_vec (vCons a v) a + sum (count_vec (vCons a v)) (set⇩v v)"
by (metis Un_insert_right finite_Un sum.insert sup_bot_right vCons.prems )
also have "... = count_vec v a + 1 + sum (count_vec v) ((set⇩v v) )"
using cv count_vec_vCons by (metis sum.cong)
also have "... = 1 + sum (count_vec v) ((set⇩v v))"
using False setv_not_in_count0_iff by (metis add_0)
finally show ?thesis using vCons.hyps f by simp
qed
qed

lemma sum_setv_subset_eq:
assumes "finite A"
assumes "set⇩v v ⊆ A"
shows "(∑ i ∈ set⇩v v. count_vec v i) = (∑ i ∈ A. count_vec v i)"
proof -
have ni: "⋀ x. x ∉ set⇩v v ⟹ count_vec v x = 0"
have "(∑ i ∈ A. count_vec v i) = (∑ i ∈ A - (set⇩v v). count_vec v i) + (∑ i ∈ (set⇩v v). count_vec v i)"
using sum.subset_diff assms by auto
then show ?thesis using ni
by simp
qed

lemma sum_count_vec_subset:  "finite A ⟹ set⇩v v ⊆ A ⟹ (∑ i ∈ A. count_vec v i) = dim_vec v"
using sum_setv_subset_eq sum_count_vec finite_subset by metis

text ‹An abbreviation for checking if an element is in a vector ›

abbreviation vec_contains :: "'a ⇒ 'a vec ⇒ bool" (infix "∈\$" 50)where
"a ∈\$ v ≡ a ∈ set⇩v v"

lemma vec_set_mset_contains_iff: "a ∈\$ v ⟷ a ∈# vec_mset v"

lemma vec_contains_count_gt1_iff: "a ∈\$ v ⟷ count_vec v a ≥ 1"

lemma vec_contains_obtains_index:
assumes "a ∈\$ v"
obtains i where "i < dim_vec v" and "v \$ i = a"
by (metis assms vec_setE)

lemma vec_count_eq_list_count: "count (mset xs) a = count_vec (vec_of_list xs) a"

lemma vec_contains_col_elements_mat:
assumes "j < dim_col M"
assumes "a ∈\$ col M j"
shows "a ∈ elements_mat M"
proof -
have "dim_vec (col M j) = dim_row M" by simp
then obtain i where ilt: "i < dim_row M" and "(col M j) \$ i = a"
using vec_setE by (metis assms(2))
then have "M \$\$ (i, j) = a"
thus ?thesis using assms(1) ilt
by blast
qed

lemma vec_contains_row_elements_mat:
assumes "i < dim_row M"
assumes "a ∈\$ row M i"
shows "a ∈ elements_mat M"
proof -
have "dim_vec (row M i) = dim_col M" by simp
then obtain j where jlt: "j < dim_col M" and "(row M i) \$ j = a" using vec_setE
by (metis assms(2))
then have "M \$\$ (i, j) = a"
thus ?thesis using assms(1) jlt
by blast
qed

lemma vec_contains_img: "a ∈\$ v ⟹ f a ∈\$ (map_vec f v)"
by (metis index_map_vec(1) index_map_vec(2) vec_contains_obtains_index vec_setI)

text ‹ The existing vector library contains the identity and zero vectors, but no definition
of a vector where all elements are 1, as defined below ›

definition all_ones_vec ::  "nat ⇒ 'a :: {zero,one} vec" ("u⇩v") where
"u⇩v n ≡ vec n (λ i. 1)"

lemma dim_vec_all_ones[simp]: "dim_vec (u⇩v n) = n"

lemma all_ones_index [simp]: "i < n ⟹ u⇩v n \$ i = 1"

lemma dim_vec_mult_vec_mat [simp]: "dim_vec (v ⇩v* A) = dim_col A"
unfolding mult_vec_mat_def by simp

lemma all_ones_vec_smult[simp]: "i < n ⟹ ((k :: ('a :: {one, zero, monoid_mult})) ⋅⇩v (u⇩v n)) \$ i = k"

text ‹Extra lemmas on existing vector operations ›

lemma smult_scalar_prod_sum:
fixes x :: "'a :: {comm_ring_1}"
assumes "vx ∈ carrier_vec n"
assumes "vy ∈ carrier_vec n"
shows "(∑ i ∈ {0..<n} .((x ⋅⇩v vx) \$ i) * ((y ⋅⇩v vy) \$ i)) = x * y * (vx ∙ vy)"
proof -
have "⋀ i . i < n ⟹ ((x ⋅⇩v vx) \$ i) * ((y ⋅⇩v vy) \$ i) = x * y * (vx \$ i) * (vy \$ i)"
using assms by simp
then have "(∑ i ∈ {0..<n} .((x ⋅⇩v vx) \$ i) * ((y ⋅⇩v vy) \$ i)) =
(∑ i ∈ {0..<n} .x * y * (vx \$ i) * (vy \$ i))"
by simp
also have "... = x * y * (∑ i ∈ {0..<n} . (vx \$ i) * (vy \$ i))"
using sum_distrib_left[of "x * y" "(λ i. (vx \$ i) * (vy \$ i))" "{0..<n}"]
by (metis (no_types, lifting) mult.assoc sum.cong)
finally have "(∑ i ∈ {0..<n} .((x ⋅⇩v vx) \$ i) * ((y ⋅⇩v vy) \$ i)) = x * y * (vx ∙ vy)"
using scalar_prod_def assms by (metis carrier_vecD)
thus ?thesis by simp
qed

lemma scalar_prod_double_sum_fn_vec:
fixes c :: "nat ⇒ ('a :: {comm_semiring_0})"
fixes f :: "nat ⇒ 'a vec"
assumes "⋀ j . j < k ⟹ dim_vec (f j) = n"
shows "(vec n (λi. ∑j = 0..<k. c j * (f j) \$ i)) ∙ (vec n (λi. ∑j = 0..<k. c j * (f j) \$ i)) =
(∑ j1 ∈ {0..<k} . c j1 * c j1 * ((f j1) ∙ (f j1))) +
(∑ j1 ∈ {0..<k} . (∑ j2 ∈ ({0..< k} - {j1}) . c j1 * c j2 * ((f j1) ∙ (f j2))))"
proof -
have sum_simp: "⋀ j1 j2. (∑l ∈ {0..<n} . c j1 * (f j1) \$ l * (c j2 * (f j2) \$ l)) =
c j1 * c j2 *(∑l ∈ {0..<n} .  (f j1) \$ l * (f j2) \$ l)"
proof -
fix j1 j2
have "(∑l ∈ {0..<n} . c j1 * (f j1) \$ l * (c j2 * (f j2) \$ l)) =
(∑l ∈ {0..<n} . c j1  * c j2 * (f j1) \$ l * (f j2) \$ l)"
using mult.commute sum.cong
by (smt (z3) ab_semigroup_mult_class.mult_ac(1)) (* SLOW *)
then show "(∑l ∈ {0..<n} . c j1 * (f j1) \$ l * (c j2 * (f j2) \$ l)) =
c j1 * c j2 *(∑l ∈ {0..<n} .  (f j1) \$ l * (f j2) \$ l)"
using sum_distrib_left[of " c j1 * c j2" "λ l. (f j1) \$ l * (f j2) \$ l" "{0..<n}"]
by (metis (no_types, lifting) mult.assoc sum.cong)
qed
have "(vec n (λi. ∑j = 0..<k. c j * (f j) \$ i)) ∙ (vec n (λi. ∑j = 0..<k. c j * (f j) \$ i))
= (∑ l = 0..<n. (∑j1 = 0..<k. c j1 * (f j1) \$ l) * (∑j2 = 0..<k. c j2 * (f j2) \$ l))"
unfolding scalar_prod_def by simp
also have "... = (∑ l ∈ {0..<n} . (∑ j1 ∈ {0..<k} . (∑ j2 ∈ {0..< k}. c j1 * (f j1) \$ l *  (c j2 * (f j2) \$ l))))"
by (metis (no_types) sum_product)
also have "... = (∑ j1 ∈ {0..<k} . (∑ j2 ∈ {0..<k} . (∑l ∈ {0..<n} . c j1 * (f j1) \$ l * (c j2 * (f j2) \$ l))))"
using sum_reorder_triple[of "λ l j1 j2 .(c j1 * (f j1) \$ l * (c j2 * (f j2) \$ l))" "{0..<k}" "{0..<k}" "{0..<n}"]
by simp
also have "... = (∑ j1 ∈ {0..<k} . (∑ j2 ∈ {0..<k} . c j1 * c j2 * (∑l ∈ {0..<n} . (f j1) \$ l * (f j2) \$ l)))"
using sum_simp by simp
also have "... = (∑ j1 ∈ {0..<k} . (∑ j2 ∈ {0..<k} . c j1 * c j2 * ((f j1) ∙ (f j2))))"
unfolding scalar_prod_def using dim_col assms by simp
finally show ?thesis
using double_sum_split_case by fastforce
qed

lemma vec_prod_zero: "(0⇩v n) ∙ (0⇩v n) = 0"
by simp

lemma map_vec_compose: "map_vec f (map_vec g v) = map_vec (f ∘ g) v"
by auto

subsection ‹Matrix Extras›

text ‹As with vectors, the all ones mat definition defines the concept of a matrix where all
elements are 1 ›

definition all_ones_mat :: "nat ⇒ 'a :: {zero,one} mat" ("J⇩m") where
"J⇩m n ≡ mat n n (λ (i,j). 1)"

lemma all_ones_mat_index[simp]: "i < dim_row (J⇩m n) ⟹ j < dim_col (J⇩m n) ⟹ J⇩m n \$\$ (i, j)= 1"

lemma all_ones_mat_dim_row[simp]: "dim_row (J⇩m n) = n"

lemma all_ones_mat_dim_col[simp]: "dim_col (J⇩m n) = n"

text ‹Basic lemmas on existing matrix operations ›
lemma index_mult_vec_mat[simp]: "j < dim_col A ⟹ (v ⇩v* A) \$ j = v ∙ col A j"
by (auto simp: mult_vec_mat_def)

lemma transpose_mat_mult_entries: "i < dim_row A ⟹ j < dim_row A ⟹
(A * A⇧T) \$\$ (i, j) = (∑k∈ {0..<(dim_col A)}. (A \$\$ (i, k)) * (A \$\$ (j, k)))"

lemma transpose_mat_elems: "elements_mat A = elements_mat A⇧T"
by fastforce

lemma row_elems_subset_mat: "i < dim_row N ⟹ vec_set (row N i) ⊆ elements_mat N"
by (auto simp add: vec_set_def elements_matI)

lemma col_elems_subset_mat: "i < dim_col N ⟹ vec_set (col N i) ⊆ elements_mat N"
by (auto simp add: vec_set_def elements_matI)

lemma obtain_row_index:
assumes "r ∈ set (rows M)"
obtains i where "row M i = r" and "i < dim_row M"
by (metis assms in_set_conv_nth length_rows nth_rows)

lemma row_prop_cond: "(⋀ i. i < dim_row M ⟹ P (row M i)) ⟹ r ∈ set (rows M) ⟹ P r"
using obtain_row_index by metis

lemma obtain_col_index:
assumes "c ∈ set (cols M)"
obtains j where "col M j = c" and "j < dim_col M"
by (metis assms cols_length cols_nth obtain_set_list_item)

lemma col_prop_cond: "(⋀ j. j < dim_col M ⟹ P (col M j)) ⟹ c ∈ set (cols M) ⟹ P c"
using obtain_col_index by metis

text ‹ Lemmas on the @{term "map_mat"} definition ›

lemma row_map_mat[simp]:
assumes "i < dim_row A" shows "row (map_mat f A) i = map_vec f (row A i)"
unfolding map_mat_def map_vec_def using assms by auto

lemma map_vec_mat_rows: "map (map_vec f) (rows M) = rows ((map_mat f) M)"

lemma map_vec_mat_cols: "map (map_vec f) (cols M) = cols ((map_mat f) M)"

lemma map_mat_compose: "map_mat f (map_mat g A) = map_mat (f ∘ g) A"
by (auto)

lemmas map_mat_elements = elements_mat_map

text ‹ Reasoning on sets and multisets of matrix elements ›
lemma set_cols_carrier: "A ∈ carrier_mat m n ⟹ v ∈ set (cols A) ⟹ v ∈ carrier_vec m"
by (auto simp: cols_def)

lemma mset_cols_index_map:  "image_mset (λ j. col M j) (mset_set {0..< dim_col M}) = mset (cols M)"

lemma mset_rows_index_map:  "image_mset (λ i. row M i) (mset_set {0..< dim_row M}) = mset (rows M)"

lemma index_to_col_card_size_prop:
assumes "i < dim_row M"
assumes "⋀ j. j < dim_col M ⟹ P j ⟷ Q (col M j)"
shows "card {j . j < dim_col M ∧ P j} = size {#c ∈# (mset (cols M)) . Q c #}"
proof -
have "card {j . j < dim_col M ∧ P j} = size (mset_set({j ∈ {0..<dim_col M}.  P j}))"
by simp
also have "... = size (mset_set({j ∈ {0..<dim_col M}.  Q (col M j)}))"
using assms(2)
by (metis lessThan_atLeast0 lessThan_iff)
also have "... = size (image_mset (λ j. col M j)  {# j ∈# mset_set {0..< dim_col M} . Q (col M j) #})"
by simp
also have "... = size ({# c ∈# (image_mset (λ j. col M j) (mset_set {0..< dim_col M})) .  Q c #})"
using image_mset_filter_swap[of "(λ j. col M j)"  "Q" "(mset_set {0..< dim_col M})"] by simp
finally have "card {j . j < dim_col M ∧ P j} = size ({# c ∈# (mset (cols M)) .  Q c #})"
using mset_cols_index_map by metis
thus ?thesis by simp
qed

lemma index_to_row_card_size_prop:
assumes "j < dim_col M"
assumes "⋀ i. i < dim_row M ⟹ P i ⟷ Q (row M i)"
shows "card {i . i < dim_row M ∧ P i} = size {#r ∈# (mset (rows M)) . Q r #}"
proof -
have "card {i . i < dim_row M ∧ P i} = size (mset_set({i ∈ {0..<dim_row M}.  P i}))"
by simp
also have "... = size (mset_set({i ∈ {0..<dim_row M}.  Q (row M i)}))"
using assms(2)
by (metis lessThan_atLeast0 lessThan_iff)
also have "... = size (image_mset (λ i. row M i)  {# i ∈# mset_set {0..< dim_row M} . Q (row M i) #})"
by simp
also have "... = size ({# r ∈# (image_mset (λ i. row M i) (mset_set {0..< dim_row M})) .  Q r #})"
using image_mset_filter_swap[of "(λ j. row M j)"  "Q" "(mset_set {0..< dim_row M})"] by simp
finally have "card {j . j < dim_row M ∧ P j} = size ({# c ∈# (mset (rows M)) .  Q c #})"
using mset_rows_index_map by metis
thus ?thesis by simp
qed

lemma setv_row_subset_mat_elems:
assumes "v ∈ set (rows M)"
shows "set⇩v v ⊆ elements_mat M"
proof (intro subsetI)
fix x assume "x ∈\$ v"
then obtain i where "v = row M i" and "i < dim_row M"
by (metis assms obtain_row_index)
then show "x ∈ elements_mat M"
by (metis ‹x ∈\$ v› vec_contains_row_elements_mat)
qed

lemma setv_col_subset_mat_elems:
assumes "v ∈ set (cols M)"
shows "set⇩v v ⊆ elements_mat M"
proof (intro subsetI)
fix x assume "x ∈\$ v"
then obtain i where "v = col M i" and "i < dim_col M"
by (metis assms obtain_col_index)
then show "x ∈ elements_mat M"
by (metis ‹x ∈\$ v› vec_contains_col_elements_mat)
qed

subsection ‹ Vector and Matrix Homomorphism ›

text ‹We extend on the existing lemmas on homomorphism mappings as applied to vectors and matrices ›

context semiring_hom
begin

lemma  vec_hom_smult2:
assumes "dim_vec v2 ≤ dim_vec v1"
shows "hom (v1 ∙ v2) = vec⇩h v1 ∙ vec⇩h v2"
unfolding scalar_prod_def using index_map_vec assms by (auto simp add: hom_distribs)

end

lemma map_vec_vCons: "vCons (f a) (map_vec f v) = map_vec f (vCons a v)"
by (intro eq_vecI, simp_all add: vec_index_vCons)

context inj_zero_hom
begin

lemma  vec_hom_zero_iff[simp]: "(map_vec hom x = 0⇩v n) = (x = 0⇩v n)"
proof -
{
fix i
assume i: "i < n" "dim_vec x = n"
hence "map_vec hom x \$ i = 0 ⟷ x \$ i = 0"
using index_map_vec(1)[of i x] by simp
} note main = this
show ?thesis unfolding vec_eq_iff by (simp, insert main, auto)
qed

lemma  mat_hom_inj: "map_mat hom A = map_mat hom B ⟹ A = B"
unfolding mat_eq_iff by auto

lemma  vec_hom_inj: "map_vec hom v = map_vec hom w ⟹ v = w"
unfolding vec_eq_iff by auto

lemma  vec_hom_set_distinct_iff:
fixes xs :: "'a vec list"
shows "distinct xs ⟷ distinct (map (map_vec hom) xs)"
using vec_hom_inj by (induct xs) (auto)

lemma vec_hom_mset: "image_mset hom (vec_mset v) = vec_mset (map_vec hom v)"
apply (induction v)
apply (metis mset.simps(1) vec_mset_img_map vec_mset_vNil vec_of_list_Nil)
by (metis mset_vec_eq_mset_list vec_list vec_mset_img_map)

lemma vec_hom_set: "hom ` set⇩v v = set⇩v (map_vec hom v)"
proof (induct v)
case vNil
then show ?case by (metis image_mset_empty set_image_mset vec_hom_zero_iff vec_mset_set vec_mset_vNil zero_vec_zero)
next
case (vCons a v)
have "hom ` set⇩v (vCons a v) = hom ` ({a} ∪ set⇩v v)"
by (metis Un_commute insert_absorb insert_is_Un vCons_set_contains_add vCons_set_contains_in)
also have "... = {hom a} ∪ (hom ` (set⇩v v))" by simp
also have "... = {hom a} ∪ (set⇩v (map_vec hom v))" using vCons.hyps by simp
also have "... = set⇩v (vCons (hom a) (map_vec hom v))"
by (metis Un_commute insert_absorb insert_is_Un vCons_set_contains_add vCons_set_contains_in)
finally show ?case using map_vec_vCons
by metis
qed

end

subsection ‹ Zero One injections and homomorphisms ›

text ‹Define a locale to encapsulate when a function is injective on a certain set (i.e. not
a universal homomorphism for the type›
locale injective_lim =
fixes A :: "'a set"
fixes f :: "'a ⇒ 'b" assumes injectivity_lim: "⋀x y. x ∈ A ⟹ y ∈ A ⟹ f x = f y ⟹ x = y"
begin
lemma eq_iff[simp]: "x ∈ A ⟹ y ∈ A ⟹ f x = f y ⟷ x = y" using injectivity_lim by auto
lemma inj_on_f: "inj_on f A" by (auto intro: inj_onI)

end

sublocale injective ⊆ injective_lim Univ
by(unfold_locales) simp

context injective_lim
begin

lemma mat_hom_inj_lim:
assumes "elements_mat M ⊆ A" and "elements_mat N ⊆ A"
shows "map_mat f M = map_mat f N ⟹ M = N"
unfolding mat_eq_iff apply auto
using assms injectivity_lim by blast

lemma vec_hom_inj_lim: assumes "set⇩v v ⊆ A" "set⇩v w ⊆ A"
shows "map_vec f v = map_vec f w ⟹ v = w"
unfolding vec_eq_iff apply (auto)
using vec_setI in_mono assms injectivity_lim by metis

lemma lim_inj_hom_count_vec:
assumes "set⇩v v ⊆ A"
assumes "x ∈ A"
shows "count_vec v x = count_vec (map_vec f v) (f x)"
using assms proof (induct v)
case vNil
have "(map_vec f vNil) = vNil" by auto
then show ?case
by (smt (verit) count_vec_vNil)
next
case (vCons a v)
have 1: "map_vec f (vCons a v) = vCons (f a) (map_vec f v)"
then show ?case proof (cases "a = x")
case True
have "count_vec (vCons a v) x = count_vec v x + 1"
then show ?thesis using Un_subset_iff 1 count_vec_vCons vCons.hyps vCons.prems(1)
by metis
next
case False
then have "count_vec (vCons a v) x = count_vec v x"
then show ?thesis using "1" Un_empty_right Un_insert_right count_vec_vCons insert_absorb insert_subset
by (metis (no_types, lifting) injectivity_lim)
qed
qed

lemma vec_hom_lim_set_distinct_iff:
fixes xs :: "'a vec list"
assumes "⋀ v . v ∈ set (xs) ⟹ set⇩v v ⊆ A"
shows "distinct xs ⟷ distinct (map (map_vec f) xs)"
using assms vec_hom_inj_lim by (induct xs, simp_all) (metis (no_types, lifting) image_iff)

lemma mat_rows_hom_lim_distinct_iff:
assumes "elements_mat M ⊆ A"
shows "distinct (rows M) ⟷ distinct (map (map_vec f) (rows M))"
apply (intro vec_hom_lim_set_distinct_iff)
using setv_row_subset_mat_elems assms by blast

lemma mat_cols_hom_lim_distinct_iff:
assumes "elements_mat M ⊆ A"
shows "distinct (cols M) ⟷ distinct (map (map_vec f) (cols M))"
apply (intro vec_hom_lim_set_distinct_iff)
using setv_col_subset_mat_elems assms by blast

end

locale inj_on_01_hom = zero_hom + one_hom + injective_lim "{0, 1}" hom
begin

lemma inj_0_iff: "x ∈ {0, 1} ⟹ hom x = 0 ⟷ x = 0"
by (metis hom_zero insertI1 local.eq_iff)

lemma inj_1_iff: "x ∈ {0, 1} ⟹ hom x = 1 ⟷ x = 1"
using inj_0_iff by fastforce

end

context zero_neq_one
begin

definition of_zero_neq_one :: "'b :: {zero_neq_one} ⇒ 'a" where
"of_zero_neq_one x ≡ if (x = 0) then 0 else 1"

lemma of_zero_neq_one_1 [simp]: "of_zero_neq_one 1 = 1"

lemma of_zero_neq_one_0 [simp]:  "of_zero_neq_one 0 = 0"

lemma of_zero_neq_one_0_iff[iff]: "of_zero_neq_one x = 0 ⟷ x = 0"

lemma of_zero_neq_one_lim_eq: "x ∈ {0, 1} ⟹ y ∈ {0, 1} ⟹ of_zero_neq_one x = of_zero_neq_one y ⟷ x = y"

end

interpretation of_zero_hom: zero_hom_0 of_zero_neq_one
by(unfold_locales) (simp_all)

interpretation of_injective_lim: injective_lim "{0, 1}" of_zero_neq_one

interpretation of_inj_on_01_hom: inj_on_01_hom of_zero_neq_one

text ‹We want the ability to transform any 0-1 vector or matrix to another @{typ "'c :: zero_neq_one"} type ›
definition lift_01_vec :: "'b :: {zero_neq_one} vec ⇒ 'c :: {zero_neq_one} vec" where
"lift_01_vec v ≡ map_vec of_zero_neq_one v"

lemma lift_01_vec_simp[simp]: "dim_vec (lift_01_vec v) = dim_vec v"
"i < dim_vec v ⟹ (lift_01_vec v) \$ i = of_zero_neq_one (v \$ i)"

lemma lift_01_vec_count:
assumes "set⇩v v ⊆ {0, 1}"
assumes "x ∈ {0, 1}"
shows "count_vec v x = count_vec (lift_01_vec v) (of_zero_neq_one x)"
using of_injective_lim.lim_inj_hom_count_vec
by (metis assms(1) assms(2) lift_01_vec_def)

definition lift_01_mat :: "'b :: {zero_neq_one} mat ⇒ 'c :: {zero_neq_one} mat" where
"lift_01_mat M ≡ map_mat of_zero_neq_one M"

lemma lift_01_mat_simp[simp]: "dim_row (lift_01_mat M) = dim_row M"
"dim_col (lift_01_mat M) = dim_col M"
"i < dim_row M ⟹ j < dim_col M ⟹ (lift_01_mat M) \$\$ (i, j) = of_zero_neq_one (M \$\$ (i, j))"