Theory Vector_Matrix_Mod
section ‹ Matrices/Vectors mod x ›
text ‹ This section formalises operations and properties mod some integer x on integer matrices and
vectors. Much of this file was no longer needed for fishers once the generic idea of lifting a 0-1 matrix
was introduced, however it is left as an example for future work on matrices mod n, beyond 0-1 matrices ›
theory Vector_Matrix_Mod imports Matrix_Vector_Extras
Berlekamp_Zassenhaus.Finite_Field Berlekamp_Zassenhaus.More_Missing_Multiset
begin
text ‹Simple abbreviations for main mapping functions ›
abbreviation to_int_mat :: "'a :: finite mod_ring mat ⇒ int mat" where
"to_int_mat ≡ map_mat to_int_mod_ring"
abbreviation to_int_vec :: "'a :: finite mod_ring vec ⇒ int vec" where
"to_int_vec ≡ map_vec to_int_mod_ring"
interpretation of_int_mod_ring_hom_sr: semiring_hom of_int_mod_ring
proof (unfold_locales)
show "⋀x y. of_int_mod_ring (x + y) = of_int_mod_ring x + of_int_mod_ring y"
by (transfer,presburger)
show "of_int_mod_ring 1 = 1" by (metis of_int_hom.hom_one of_int_of_int_mod_ring)
show "⋀x y. of_int_mod_ring (x * y) = of_int_mod_ring x * of_int_mod_ring y"
by (transfer, simp add: mod_mult_eq)
qed
text ‹NOTE: The context directly below is copied from Matrix Vector Extras, as for some reason
they can't be used locally if not? Ideally remove in future if possible ›
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)
end
subsection ‹ Basic Mod Context ›
locale mat_mod = fixes m :: int
assumes non_triv_m: "m > 1"
begin
text ‹First define the mod operations on vectors ›
definition vec_mod :: "int vec ⇒ int vec" where
"vec_mod v ≡ map_vec (λ x . x mod m) v"
lemma vec_mod_dim[simp]: "dim_vec (vec_mod v) = dim_vec v"
using vec_mod_def by simp
lemma vec_mod_index[simp]: "i < dim_vec v ⟹ (vec_mod v) $ i = (v $ i) mod m"
using vec_mod_def by simp
lemma vec_mod_index_same[simp]: "i < dim_vec v ⟹ v $ i < m ⟹ v $ i ≥ 0 ⟹ (vec_mod v) $ i = v $ i"
by simp
lemma vec_setI2: "i < dim_vec v ⟹ v $ i ∈ set⇩v v"
by (simp add: vec_setI)
lemma vec_mod_eq: "set⇩v v ⊆ {0..<m} ⟹ vec_mod v = v"
apply (intro eq_vecI, simp_all)
using vec_setI2 vec_mod_index_same by (metis atLeastLessThan_iff subset_iff zmod_trivial_iff)
lemma vec_mod_set_vec_same:"set⇩v v ⊆ {0..<m} ⟹ set⇩v (vec_mod v) = set⇩v v"
using vec_mod_eq by auto
text ‹Define the mod operation on matrices ›
definition mat_mod :: "int mat ⇒ int mat" where
"mat_mod M ≡ map_mat (λ x. x mod m) M"
lemma mat_mod_dim[simp]: "dim_row (mat_mod M) = dim_row M" "dim_col (mat_mod M) = dim_col M"
using mat_mod_def by simp_all
lemma mat_mod_index [simp]: "i < dim_row M ⟹ j < dim_col M ⟹ (mat_mod M) $$ (i, j) = (M $$ (i, j)) mod m"
by(simp add: mat_mod_def)
lemma mat_mod_index_same[simp]: "i < dim_row M ⟹ j < dim_col M ⟹ M $$ (i, j) < m ⟹
M $$ (i, j) ≥ 0 ⟹ mat_mod M $$ (i, j) = M $$ (i, j)"
by (simp add: mat_mod_def)
lemma elements_matI2: "i < dim_row A ⟹ j < dim_col A ⟹ A $$ (i, j) ∈ elements_mat A"
by auto
lemma mat_mod_elements_in:
assumes "x ∈ elements_mat M"
shows "x mod m ∈ elements_mat (mat_mod M)"
proof -
obtain i j where "M $$ (i, j) = x" and ilt: "i < dim_row M" and jlt: "j < dim_col M" using assms by auto
then have "mat_mod M $$ (i, j) = x mod m" by simp
thus ?thesis using ilt jlt
by (metis elements_matI2 mat_mod_dim(1) mat_mod_dim(2))
qed
lemma mat_mod_elements_map:
assumes "x ∈ elements_mat M"
shows "elements_mat (mat_mod M) = (λ x. x mod m) ` (elements_mat M)"
proof (auto simp add: mat_mod_elements_in)
fix x assume "x ∈ elements_mat (local.mat_mod M)"
then obtain i j where "(mat_mod M) $$ (i, j) = x" and "i < dim_row (mat_mod M)" and "j < dim_col (mat_mod M)" by auto
then show "x ∈ (λx. x mod m) ` elements_mat M"
by auto
qed
lemma mat_mod_eq_cond:
assumes "elements_mat M ⊆ {0..<m}"
shows "mat_mod M = M"
proof (intro eq_matI, simp_all)
fix i j assume "i < dim_row M" "j < dim_col M"
then have "M $$ (i, j) ∈ {0..<m}"
using assms elements_matI2 by blast
then show "M $$ (i, j) mod m = M $$ (i, j)"
by (simp)
qed
lemma mat_mod_eq_elements_cond: "elements_mat M ⊆ {0..<m} ⟹ elements_mat (mat_mod M) = elements_mat M"
using mat_mod_eq_cond by auto
lemma mat_mod_vec_mod_row: "i < dim_row A ⟹ row (mat_mod A) i = vec_mod (row A i)"
unfolding mat_mod_def vec_mod_def by (simp)
lemma mat_mod_vec_mod_col: "j < dim_col A ⟹ col (mat_mod A) j = vec_mod (col A j)"
unfolding mat_mod_def vec_mod_def by (simp)
lemma count_vec_mod_eq: "set⇩v v ⊆ {0..<m} ⟹ count_vec v x = count_vec (vec_mod v) x"
using vec_mod_eq by (simp)
lemma elems_mat_setv_row_0m: "i < dim_row M ⟹ elements_mat M ⊆ {0..<m} ⟹ set⇩v (row M i) ⊆ {0..<m}"
by (metis row_elems_subset_mat subset_trans)
lemma elems_mat_setv_col_0m: "j < dim_col M ⟹ elements_mat M ⊆ {0..<m} ⟹ set⇩v (col M j) ⊆ {0..<m}"
by (metis col_elems_subset_mat subset_trans)
lemma mat_mod_count_row_eq: "i < dim_row M ⟹ elements_mat M ⊆ {0..<m} ⟹
count_vec (row (mat_mod M) i) x = count_vec (row M i) x"
using count_vec_mod_eq mat_mod_vec_mod_row elems_mat_setv_row_0m by simp
lemma mat_mod_count_col_eq: "j < dim_col M ⟹ elements_mat M ⊆ {0..<m} ⟹
count_vec (col (mat_mod M) j) x = count_vec (col M j) x"
using count_vec_mod_eq mat_mod_vec_mod_col elems_mat_setv_col_0m by simp
lemma mod_mat_one: "mat_mod (1⇩m n) = (1⇩m n)"
by (intro eq_matI, simp_all add: mat_mod_def non_triv_m)
lemma mod_mat_zero: "mat_mod (0⇩m nr nc) = (0⇩m nr nc)"
by (intro eq_matI, simp_all add: mat_mod_def non_triv_m)
lemma vec_mod_unit: "vec_mod (unit_vec n i) = (unit_vec n i)"
by (intro eq_vecI, simp_all add: unit_vec_def vec_mod_def non_triv_m)
lemma vec_mod_zero: "vec_mod (0⇩v n) = (0⇩v n)"
by (intro eq_vecI, simp_all add: non_triv_m)
lemma mat_mod_cond_iff: "elements_mat M ⊆ {0..<m} ⟹ P M ⟷ P (mat_mod M)"
by (simp add: mat_mod_eq_cond)
end
subsection ‹Mod Type ›
text ‹ The below locale takes lemmas from the Poly Mod Finite Field theory in the Berlekamp Zassenhaus
AFP entry, however has removed any excess material on polynomials mod, and only included the general
factors. Ideally, this could be used as the base locale for both in the future ›
locale mod_type =
fixes m :: int and ty :: "'a :: nontriv itself"
assumes m: "m = CARD('a)"
begin
lemma m1: "m > 1" using nontriv[where 'a = 'a] by (auto simp:m)
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_1[simp]: "M 1 = 1" unfolding M_def
using m1 by auto
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 M_Rel :: "int ⇒ 'a mod_ring ⇒ bool"
where "M_Rel x x' ≡ (M x = to_int_mod_ring x')"
lemma to_int_mod_ring_plus: "to_int_mod_ring ((x :: 'a mod_ring) + y) = M (to_int_mod_ring x + to_int_mod_ring y)"
unfolding M_def using m by (transfer, auto)
lemma to_int_mod_ring_times: "to_int_mod_ring ((x :: 'a mod_ring) * y) = M (to_int_mod_ring x * to_int_mod_ring y)"
unfolding M_def using m by (transfer, auto)
lemma eq_M_Rel[transfer_rule]: "(M_Rel ===> M_Rel ===> (=)) (λ x y. M x = M y) (=)"
unfolding M_Rel_def rel_fun_def by auto
lemma one_M_Rel[transfer_rule]: "M_Rel 1 1"
unfolding M_Rel_def M_def
unfolding m by auto
lemma zero_M_Rel[transfer_rule]: "M_Rel 0 0"
unfolding M_Rel_def M_def
unfolding m by auto
lemma M_to_int_mod_ring: "M (to_int_mod_ring (x :: 'a mod_ring)) = to_int_mod_ring x"
unfolding M_def unfolding m by (transfer, auto)
lemma right_total_M_Rel[transfer_rule]: "right_total M_Rel"
unfolding right_total_def M_Rel_def using M_to_int_mod_ring by blast
lemma left_total_M_Rel[transfer_rule]: "left_total M_Rel"
unfolding left_total_def M_Rel_def[abs_def]
proof
fix x
show "∃ x' :: 'a mod_ring. M x = to_int_mod_ring x'" unfolding M_def unfolding m
by (rule exI[of _ "of_int x"], transfer, simp)
qed
lemma bi_total_M_Rel[transfer_rule]: "bi_total M_Rel"
using right_total_M_Rel left_total_M_Rel by (metis bi_totalI)
lemma to_int_mod_ring_of_int_M: "to_int_mod_ring (of_int x :: 'a mod_ring) = M x" unfolding M_def
unfolding m by transfer auto
lemma UNIV_M_Rel[transfer_rule]: "rel_set M_Rel {0..<m} UNIV"
unfolding rel_set_def M_Rel_def[abs_def] M_def
by (auto simp: M_def m, goal_cases, metis to_int_mod_ring_of_int_mod_ring, (transfer, auto)+)
end
subsection ‹ Mat mod type ›
text ‹ Define a context to work on matrices and vectors of type @{typ "'a mod_ring"} ›
locale mat_mod_type = mat_mod + mod_type
begin
lemma to_int_mod_ring_plus: "to_int_mod_ring ((x :: 'a mod_ring) + y) = (to_int_mod_ring x + to_int_mod_ring y) mod m"
using m by (transfer, auto)
lemma to_int_mod_ring_times: "to_int_mod_ring ((x :: 'a mod_ring) * y) = (to_int_mod_ring x * to_int_mod_ring y) mod m"
using m by (transfer, auto)
text ‹ Set up transfer relation for matrices and vectors ›
definition MM_Rel :: "int mat ⇒ 'a mod_ring mat ⇒ bool"
where "MM_Rel f f' ≡ (mat_mod f = to_int_mat f')"
definition MV_Rel :: "int vec ⇒ 'a mod_ring vec ⇒ bool"
where "MV_Rel v v' ≡ (vec_mod v = to_int_vec v')"
lemma to_int_mat_index[simp]: "i < dim_row N ⟹ j < dim_col N ⟹ (to_int_mat N $$ (i, j)) = to_int_mod_ring (N $$ (i, j))"
by simp
lemma to_int_vec_index[simp]: "i < dim_vec v ⟹ (to_int_vec v $i) = to_int_mod_ring (v $i)"
by simp
lemma eq_dim_row_MM_Rel[transfer_rule]: "(MM_Rel ===> (=)) dim_row dim_row "
by (metis (mono_tags) MM_Rel_def index_map_mat(2) mat_mod_dim(1) rel_funI)
lemma lt_dim_row_MM_Rel[transfer_rule]: "(MM_Rel ===> (=) ===> (=)) (λ M i. i < dim_row M) (λ M i. i < dim_row M)"
using eq_dim_row_MM_Rel unfolding MM_Rel_def rel_fun_def by auto
lemma eq_dim_col_MM_Rel[transfer_rule]: "(MM_Rel ===> (=)) dim_col dim_col "
unfolding MM_Rel_def rel_fun_def
by (metis index_map_mat(3) mat_mod_dim(2))
lemma lt_dim_col_MM_Rel[transfer_rule]: "(MM_Rel ===> (=) ===> (=)) (λ M j. j < dim_col M) (λ M j. j < dim_col M)"
using eq_dim_col_MM_Rel unfolding MM_Rel_def rel_fun_def by auto
lemma eq_dim_vec_MV_Rel[transfer_rule]: "(MV_Rel ===> (=)) dim_vec dim_vec"
unfolding MV_Rel_def rel_fun_def using index_map_vec(2) vec_mod_dim by metis
lemma lt_dim_vec_MV_Rel[transfer_rule]: "(MV_Rel ===> (=) ===> (=)) (λ v j. j < dim_vec v) (λ v j. j < dim_vec v)"
unfolding MV_Rel_def rel_fun_def using index_map_vec(2) vec_mod_dim by metis
lemma eq_MM_Rel[transfer_rule]: "(MM_Rel ===> MM_Rel ===> (=)) (λ f f' . mat_mod f = mat_mod f') (=) "
unfolding MM_Rel_def rel_fun_def using to_int_mod_ring_hom.mat_hom_inj by (auto)
lemma eq_MV_Rel[transfer_rule]: "(MV_Rel ===> MV_Rel ===> (=)) (λ v v' . vec_mod v = vec_mod v') (=) "
unfolding MV_Rel_def rel_fun_def using to_int_mod_ring_hom.vec_hom_inj by auto
lemma index_MV_Rel[transfer_rule]: "(MV_Rel ===> (=) ===> M_Rel)
(λ v i. if i < dim_vec v then v $ i else 0) (λ v i. if i < dim_vec v then v $ i else 0)"
using lt_dim_vec_MV_Rel unfolding MV_Rel_def M_Rel_def M_def rel_fun_def
by (simp, metis to_int_vec_index vec_mod_index)
lemma index_MM_Rel[transfer_rule]: "(MM_Rel ===> (=) ===> (=) ===> M_Rel)
(λ M i j. if (i < dim_row M ∧ j < dim_col M) then M $$ (i, j) else 0)
(λ M i j. if (i < dim_row M ∧ j < dim_col M) then M $$ (i, j) else 0)"
using lt_dim_row_MM_Rel lt_dim_col_MM_Rel unfolding M_Rel_def M_def rel_fun_def
by (simp, metis mat_mod_index to_int_mat_index MM_Rel_def)
lemma index_MM_Rel_explicit:
assumes "MM_Rel N N'"
assumes "i < dim_row N" "j < dim_col N"
shows "(N $$ (i, j)) mod m = to_int_mod_ring (N' $$ (i, j))"
proof -
have eq: "(to_int_mat N') $$ (i, j) = to_int_mod_ring (N' $$ (i, j))"
by (metis MM_Rel_def assms(1) assms(2) assms(3) index_map_mat mat_mod.mat_mod_dim mat_mod_axioms)
have "mat_mod N = to_int_mat N'" using assms by (simp add: MM_Rel_def)
then have "(mat_mod N) $$ (i, j) = (to_int_mat N') $$ (i, j)"
by simp
thus ?thesis using mat_mod_index eq
using assms(2) assms(3) by auto
qed
lemma one_MV_Rel[transfer_rule]: "MV_Rel (unit_vec n i) (unit_vec n i)"
unfolding MV_Rel_def vec_mod_unit non_triv_m unit_vec_def
by (intro eq_vecI, simp_all add: non_triv_m)
lemma one_MM_Rel[transfer_rule]: "MM_Rel (1⇩m n) (1⇩m n)"
unfolding MM_Rel_def mod_mat_one
by (intro eq_matI, simp_all)
lemma zero_MM_Rel[transfer_rule]: "MM_Rel (0⇩m nr nc) (0⇩m nr nc)"
unfolding MM_Rel_def
by (intro eq_matI, simp_all)
lemma zero_MV_Rel[transfer_rule]: "MV_Rel (0⇩v n) (0⇩v n)"
unfolding MV_Rel_def by (intro eq_vecI, simp_all)
lemma right_unique_MV_Rel[transfer_rule]: "right_unique MV_Rel"
unfolding right_unique_def MV_Rel_def
using to_int_mod_ring_hom.vec_hom_inj by auto
lemma right_unique_MM_Rel[transfer_rule]: "right_unique MM_Rel"
unfolding right_unique_def MM_Rel_def
using to_int_mod_ring_hom.mat_hom_inj by auto
lemma mod_to_int_mod_ring: "(to_int_mod_ring (x :: 'a mod_ring)) mod m = to_int_mod_ring x"
unfolding m by (transfer, auto)
lemma mat_mod_to_int_mat: "mat_mod (to_int_mat (N :: 'a mod_ring mat)) = to_int_mat N"
using mod_to_int_mod_ring by (intro eq_matI, simp_all)
lemma vec_mod_to_int_vec: "vec_mod (to_int_vec (v :: 'a mod_ring vec)) = to_int_vec v"
using mod_to_int_mod_ring by (intro eq_vecI, simp_all)
lemma right_total_MM_Rel[transfer_rule]: "right_total MM_Rel"
unfolding right_total_def MM_Rel_def
proof
fix M :: "'a mod_ring mat"
show "∃x. mat_mod x = to_int_mat M"
by (intro exI[of _ "to_int_mat M"], simp add: mat_mod_to_int_mat)
qed
lemma right_total_MV_Rel[transfer_rule]: "right_total MV_Rel"
unfolding right_total_def MV_Rel_def
proof
fix v :: "'a mod_ring vec"
show "∃x. vec_mod x = to_int_vec v"
by (intro exI[of _ "to_int_vec v"], simp add: vec_mod_to_int_vec)
qed
lemma to_int_mod_ring_of_int_mod: "to_int_mod_ring (of_int x :: 'a mod_ring) = x mod m"
unfolding m by transfer auto
lemma vec_mod_v_representative: "vec_mod v = to_int_vec (map_vec of_int v :: 'a mod_ring vec)"
unfolding mat_mod_def by (auto simp: to_int_mod_ring_of_int_mod)
lemma mat_mod_N_representative: "mat_mod N = to_int_mat (map_mat of_int N :: 'a mod_ring mat)"
unfolding mat_mod_def by (auto simp: to_int_mod_ring_of_int_mod)
lemma left_total_MV_Rel[transfer_rule]: "left_total MV_Rel"
unfolding left_total_def MV_Rel_def[abs_def] using vec_mod_v_representative by blast
lemma left_total_MM_Rel[transfer_rule]: "left_total MM_Rel"
unfolding left_total_def MM_Rel_def[abs_def] using mat_mod_N_representative by blast
lemma bi_total_MV_Rel[transfer_rule]: "bi_total MV_Rel"
using right_total_MV_Rel left_total_MV_Rel by (metis bi_totalI)
lemma bi_total_MM_Rel[transfer_rule]: "bi_total MM_Rel"
using right_total_MM_Rel left_total_MM_Rel by (metis bi_totalI)
lemma domain_MV_rel[transfer_domain_rule]: "Domainp MV_Rel = (λ f. True)"
proof
fix v :: "int vec"
show "Domainp MV_Rel v = True" unfolding MV_Rel_def[abs_def] Domainp.simps
by (auto simp: vec_mod_v_representative)
qed
lemma domain_MM_rel[transfer_domain_rule]: "Domainp MM_Rel = (λ f. True)"
proof
fix N :: "int mat"
show "Domainp MM_Rel N = True" unfolding MM_Rel_def[abs_def] Domainp.simps
by (auto simp: mat_mod_N_representative)
qed
lemma mem_MV_Rel[transfer_rule]:
"(MV_Rel ===> rel_set MV_Rel ===> (=)) (λ x Y. ∃y ∈ Y. vec_mod x = vec_mod y) (∈)"
proof (intro rel_funI iffI)
fix x y X Y assume xy: "MV_Rel x y" and XY: "rel_set MV_Rel X Y"
{ assume "∃x' ∈ X. vec_mod x = vec_mod x'"
then obtain x' where x'X: "x' ∈ X" and xx': "vec_mod x = vec_mod x'" by auto
with xy have x'y: "MV_Rel x' y" by (auto simp: MV_Rel_def)
from rel_setD1[OF XY x'X] obtain y' where "MV_Rel x' y'" and "y' ∈ Y" by auto
with x'y
show "y ∈ Y" using to_int_mod_ring_hom.vec_hom_inj by (auto simp: MV_Rel_def)
}
assume "y ∈ Y"
from rel_setD2[OF XY this] obtain x' where x'X: "x' ∈ X" and x'y: "MV_Rel x' y" by auto
from xy x'y have "vec_mod x = vec_mod x'" by (auto simp: MV_Rel_def)
with x'X show "∃x' ∈ X. vec_mod x = vec_mod x'" by auto
qed
lemma mem_MM_Rel[transfer_rule]:
"(MM_Rel ===> rel_set MM_Rel ===> (=)) (λ x Y. ∃y ∈ Y. mat_mod x = mat_mod y) (∈)"
proof (intro rel_funI iffI)
fix x y X Y assume xy: "MM_Rel x y" and XY: "rel_set MM_Rel X Y"
{ assume "∃x' ∈ X. mat_mod x = mat_mod x'"
then obtain x' where x'X: "x' ∈ X" and xx': "mat_mod x = mat_mod x'" by auto
with xy have x'y: "MM_Rel x' y" by (auto simp: MM_Rel_def)
from rel_setD1[OF XY x'X] obtain y' where "MM_Rel x' y'" and "y' ∈ Y" by auto
with x'y
show "y ∈ Y" using to_int_mod_ring_hom.mat_hom_inj by (auto simp: MM_Rel_def)
}
assume "y ∈ Y"
from rel_setD2[OF XY this] obtain x' where x'X: "x' ∈ X" and x'y: "MM_Rel x' y" by auto
from xy x'y have "mat_mod x = mat_mod x'" by (auto simp: MM_Rel_def)
with x'X show "∃x' ∈ X. mat_mod x = mat_mod x'" by auto
qed
lemma conversep_MM_Rel_OO_MM_Rel [simp]: "MM_Rel¯¯ OO MM_Rel = (=)"
using mat_mod_to_int_mat apply (intro ext, auto simp: OO_def MM_Rel_def)
using to_int_mod_ring_hom.mat_hom_inj by auto
lemma MM_Rel_OO_conversep_MM_Rel [simp]: "MM_Rel OO MM_Rel¯¯ = (λ M M' . mat_mod M = mat_mod M')"
by (intro ext, auto simp: OO_def MM_Rel_def mat_mod_N_representative)
lemma conversep_MM_Rel_OO_eq_m [simp]: "MM_Rel¯¯ OO (λ M M' . mat_mod M = mat_mod M') = MM_Rel¯¯"
by (intro ext, auto simp: OO_def MM_Rel_def)
lemma eq_m_OO_MM_Rel [simp]: "(λ M M' . mat_mod M = mat_mod M') OO MM_Rel = MM_Rel"
by (intro ext, auto simp: OO_def MM_Rel_def)
lemma eq_mset_MM_Rel [transfer_rule]:
"(rel_mset MM_Rel ===> rel_mset MM_Rel ===> (=)) (rel_mset (λ M M' . mat_mod M = mat_mod M')) (=)"
proof (intro rel_funI iffI)
fix A B X Y
assume AX: "rel_mset MM_Rel A X" and BY: "rel_mset MM_Rel B Y"
{
assume AB: "rel_mset (λ M M' . mat_mod M = mat_mod M') A B"
from AX have "rel_mset MM_Rel¯¯ X A" by (simp add: multiset.rel_flip)
note rel_mset_OO[OF this AB]
note rel_mset_OO[OF this BY]
then show "X = Y" by (simp add: multiset.rel_eq)
}
assume "X = Y"
with BY have "rel_mset MM_Rel¯¯ X B" by (simp add: multiset.rel_flip)
from rel_mset_OO[OF AX this]
show "rel_mset (λ M M' . mat_mod M = mat_mod M') A B" by simp
qed
lemma vec_mset_MV_Rel[transfer_rule]:
"(MV_Rel ===> (=)) (λ v. vec_mset (vec_mod v)) (λ v. image_mset (to_int_mod_ring) (vec_mset v))"
unfolding MV_Rel_def rel_fun_def
proof (intro allI impI subset_antisym subsetI)
fix x :: "int vec" fix y :: "'a mod_ring vec"
assume assm: "vec_mod x = to_int_vec y"
have "image_mset to_int_mod_ring (vec_mset y) = vec_mset (to_int_vec y)"
using inj_zero_hom.vec_hom_mset to_int_mod_ring_hom.inj_zero_hom_axioms by auto
then show " vec_mset (vec_mod x) = image_mset to_int_mod_ring (vec_mset y)" using assm by simp
qed
lemma vec_count_MV_Rel_direct:
assumes "MV_Rel v1 v2"
shows "count_vec v2 i = count_vec (vec_mod v1) (to_int_mod_ring i)"
proof-
have eq_vecs: "to_int_vec v2 = vec_mod v1" using assms unfolding MV_Rel_def by simp
have "count_vec v2 i = count (vec_mset v2) i" by simp
also have 1: "... = count (image_mset to_int_mod_ring (vec_mset v2)) (to_int_mod_ring i)"
using count_image_mset_inj by (metis to_int_mod_ring_hom.inj_f)
also have 2: "... = count (vec_mset (vec_mod v1)) (to_int_mod_ring i)" using assms
by (simp add: eq_vecs inj_zero_hom.vec_hom_mset to_int_mod_ring_hom.inj_zero_hom_axioms)
finally show "count_vec v2 i = count_vec (vec_mod v1) (to_int_mod_ring i)"
by (simp add: 1 2 )
qed
lemma MM_Rel_MV_Rel_row: "MM_Rel A B ⟹ i < dim_row A ⟹ MV_Rel (row A i) (row B i)"
unfolding MM_Rel_def MV_Rel_def
by (metis index_map_mat(2) mat_mod_dim(1) mat_mod_vec_mod_row row_map_mat)
lemma MM_Rel_MV_Rel_col: "MM_Rel A B ⟹ j < dim_col A ⟹ MV_Rel (col A j) (col B j)"
unfolding MM_Rel_def MV_Rel_def
using index_map_mat(3) mat_mod_dim(2) mat_mod_vec_mod_col col_map_mat by (metis)
end
end