Theory Admits_SNF_From_Diagonal_Iff_Bezout_Ring
section ‹Generality of the Algorithm to transform from diagonal to Smith normal form›
theory Admits_SNF_From_Diagonal_Iff_Bezout_Ring
imports
Diagonal_To_Smith
Rings2_Extended
Smith_Normal_Form_JNF
Finite_Field_Mod_Type_Connection
begin
hide_const (open) mat
text ‹This section provides a formal proof on the generality of the algorithm that transforms
a diagonal matrix into its Smith normal form. More concretely, we prove that
all diagonal matrices with coefficients in a ring R admit Smith normal form if and only if
R is a B\'ezout ring.
Since our algorithm is defined for B\'ezout rings and for any matrices (including non-square and
singular ones), this means that it does not exist another algorithm that performs the transformation
in a more abstract structure.›
text ‹Firstly, we hide some definitions and facts, since we are interested in the ones
developed for the @{text "mod_type"} class.›
hide_const (open) Bij_Nat.to_nat Bij_Nat.from_nat Countable.to_nat Countable.from_nat
hide_fact (open) Bij_Nat.to_nat_from_nat_id Bij_Nat.to_nat_less_card
definition "admits_SNF_HA (A::'a::comm_ring_1^'n::{mod_type}^'n::{mod_type}) = (isDiagonal A
⟶ (∃P Q. invertible ((P::'a::comm_ring_1^'n::{mod_type}^'n::{mod_type}))
∧ invertible (Q::'a::comm_ring_1^'n::{mod_type}^'n::{mod_type}) ∧ Smith_normal_form (P**A**Q)))"
definition "admits_SNF_JNF A = (square_mat (A::'a::comm_ring_1 mat) ∧ isDiagonal_mat A
⟶ (∃P Q. P ∈ carrier_mat (dim_row A) (dim_row A) ∧ Q ∈ carrier_mat (dim_row A) (dim_row A)
∧ invertible_mat P ∧ invertible_mat Q ∧ Smith_normal_form_mat (P*A*Q)))"
subsection ‹Proof of the @{text "⟸"} implication in HA.›
lemma exists_f_PAQ_Aii':
fixes A::"'a::{comm_ring_1}^'n::{mod_type}^'n::{mod_type}"
assumes diag_A: "isDiagonal A"
shows "∃f. (P**A**Q) $h i $h i = (∑i∈(UNIV::'n set). f i * A $h i $h i)"
proof -
have rw: "(∑ka∈UNIV. P $h i $h ka * A $h ka $h k) = P $h i $h k * A $h k $h k" for k
proof -
have "(∑ka∈UNIV. P $h i $h ka * A $h ka $h k) = (∑ka∈{k}. P $h i $h ka * A $h ka $h k)"
proof (rule sum.mono_neutral_right, auto)
fix ia assume "P $h i $h ia * A $h ia $h k ≠ 0"
hence "A $h ia $h k ≠ 0" by auto
thus" ia = k" using diag_A unfolding isDiagonal_def by auto
qed
also have "... = P $h i $h k * A $h k $h k" by auto
finally show ?thesis .
qed
let ?f = "λk. (∑ka∈UNIV. P $h i $h ka) * Q $h k $h i"
have "(P**A**Q) $h i $h i = (∑k∈UNIV. (∑ka∈UNIV. P $h i $h ka * A $h ka $h k) * Q $h k $h i)"
unfolding matrix_matrix_mult_def by auto
also have "... = (∑k∈UNIV. P $h i $h k * Q $h k $h i * A $h k $h k)"
unfolding rw
by (meson semiring_normalization_rules(16))
finally show ?thesis by auto
qed
text ‹We apply @{text "internalize_sort"} to the lemma that we need›
lemmas diagonal_to_Smith_PQ_exists_internalize_sort
= diagonal_to_Smith_PQ_exists[internalize_sort "'a :: bezout_ring"]
text ‹We get the @{text "⟸"} implication in HA.›
lemma bezout_ring_imp_diagonal_admits_SNF:
assumes of: "OFCLASS('a::comm_ring_1, bezout_ring_class)"
shows "∀A::'a^'n::{mod_type}^'n::{mod_type}. isDiagonal A
⟶ (∃P Q.
invertible (P::'a^'n::mod_type^'n::mod_type) ∧
invertible (Q::'a^'n::mod_type^'n::mod_type) ∧
Smith_normal_form (P**A**Q))"
proof (rule allI, rule impI)
fix A::"'a^'n::{mod_type}^'n::{mod_type}"
assume A: "isDiagonal A"
have br: "class.bezout_ring (*) (1::'a) (+) 0 (-) uminus"
by (rule OFCLASS_bezout_ring_imp_class_bezout_ring[OF of])
show "∃P Q.
invertible (P::'a^'n::mod_type^'n::mod_type) ∧
invertible (Q::'a^'n::mod_type^'n::mod_type) ∧
Smith_normal_form (P**A**Q)" by (rule diagonal_to_Smith_PQ_exists_internalize_sort[OF br A])
qed
subsection ‹Trying to prove the @{text "⟹"} implication in HA.›
text‹There is a problem: we need to define a matrix with a concrete dimension, which is not
possible in HA (the dimension depends on the number of elements on a set, and Isabelle/HOL does
not feature dependent types)›
lemma
assumes "∀A::'a::comm_ring_1^'n::{mod_type}^'n::{mod_type}. admits_SNF_HA A"
shows "OFCLASS('a::comm_ring_1, bezout_ring_class)" oops
subsection ‹Proof of the @{text "⟹"} implication in JNF.›
lemma exists_f_PAQ_Aii:
assumes diag_A: "isDiagonal_mat (A::'a:: comm_ring_1 mat)"
and P: "P ∈ carrier_mat n n"
and A: "A ∈ carrier_mat n n"
and Q: "Q ∈ carrier_mat n n"
and i: "i < n"
shows "∃f. (P*A*Q) $$ (i, i) = (∑i∈set (diag_mat A). f i * i)"
proof -
let ?xs = "diag_mat A"
let ?n = "length ?xs"
have length_n: "length (diag_mat A) = n"
by (metis A carrier_matD(1) diag_mat_def diff_zero length_map length_upt)
have xs_index: "?xs ! i = A $$ (i, i)" if "i<n" for i
by (metis (no_types, lifting) add.left_neutral diag_mat_def length_map
length_n length_upt nth_map_upt that)
have i_length: "i<length ?xs" using i length_n by auto
have rw: "(∑ka = 0..<?n. P $$ (i, ka) * A $$ (ka, k)) = P $$(i, k) * A $$ (k, k)"
if k: "k<length ?xs" for k
proof -
have "(∑ka= 0..<?n. P $$ (i, ka) * A $$ (ka, k)) = (∑ka∈{k}. P $$ (i, ka) * A $$ (ka, k))"
by (rule sum.mono_neutral_right, auto simp add: k,
insert diag_A A length_n that, unfold isDiagonal_mat_def, fastforce)
also have "... = P $$(i, k) * A $$ (k, k)" by auto
finally show ?thesis .
qed
let ?positions_of ="λx. {i. A$$(i,i) = x ∧ i<length ?xs}"
let ?T="set ?xs"
let ?S ="{0..<?n}"
let ?f = "λx.(∑k∈{i. A $$ (i, i) = x ∧ i < length (diag_mat A)}. P $$ (i, k) * Q $$ (k, i))"
let ?g = "(λk. P $$ (i,k) * Q $$ (k, i) * A $$ (k, k))"
have UNION_positions_of: "⋃(?positions_of ` ?T) = ?S" unfolding diag_mat_def by auto
have "(P*A*Q) $$ (i,i) = (∑ia = 0..<?n.
Matrix.row (Matrix.mat ?n ?n (λ(i, j). ∑ia = 0..<?n.
Matrix.row P i $v ia * col A j $v ia)) i $v ia * col Q i $v ia)"
unfolding times_mat_def scalar_prod_def
using P Q i_length length_n A by auto
also have "... = (∑k = 0..<?n. (∑ka = 0..<?n. P$$(i,ka) * A$$(ka,k)) * Q $$ (k,i))"
proof (rule sum.cong, auto)
fix x assume x: "x < length ?xs"
have rw_colQ: "col Q i $v x = Q $$ (x, i)"
using Q i_length x length_n A by auto
have rw2: " Matrix.row (Matrix.mat ?n ?n
(λ(i, j). ∑ia = 0..<length ?xs. Matrix.row P i $v ia * col A j $v ia)) i $v x
=(∑ia = 0..<length ?xs. Matrix.row P i $v ia * col A x $v ia)"
unfolding row_mat[OF i_length] unfolding index_vec[OF x] by auto
also have "... = (∑ia = 0..<length ?xs. P $$ (i,ia) * A $$ (ia,x))"
by (rule sum.cong, insert P i_length x length_n A, auto)
finally show "Matrix.row (Matrix.mat ?n ?n (λ(i, j). ∑ia = 0..<?n. Matrix.row P i $v ia
* col A j $v ia)) i $v x * col Q i $v x
= (∑ka = 0..<?n. P $$ (i, ka) * A $$ (ka, x)) * Q $$ (x, i)" unfolding rw_colQ by auto
qed
also have "... = (∑k = 0..<?n. P $$ (i,k) * Q $$ (k, i) * A $$ (k, k))"
by (smt rw semiring_normalization_rules(16) sum.ivl_cong)
also have "... = sum ?g (⋃(?positions_of ` ?T))"
using UNION_positions_of by auto
also have "... = (∑x∈?T. sum ?g (?positions_of x))"
by (rule sum.UNION_disjoint, auto)
also have "... = (∑x∈set (diag_mat A). (∑k∈{i. A $$ (i, i) = x ∧ i < length (diag_mat A)}.
P $$ (i, k) * Q $$ (k, i)) * x)"
by (rule sum.cong, auto simp add: Groups_Big.sum_distrib_right)
finally show ?thesis by auto
qed
text ‹Proof of the @{text "⟹"} implication in JNF.›
lemma diagonal_admits_SNF_imp_bezout_ring_JNF:
assumes admits_SNF: "∀A n. (A::'a mat) ∈ carrier_mat n n ∧ isDiagonal_mat A
⟶ (∃P Q. P ∈ carrier_mat n n ∧ Q ∈ carrier_mat n n ∧ invertible_mat P ∧ invertible_mat Q
∧ Smith_normal_form_mat (P*A*Q))"
shows "OFCLASS('a::comm_ring_1, bezout_ring_class)"
proof (rule all_fin_gen_ideals_are_principal_imp_bezout, rule allI, rule impI)
fix I::"'a set"
assume fin: "finitely_generated_ideal I"
obtain S where ig_S: "ideal_generated S = I" and fin_S: "finite S"
using fin unfolding finitely_generated_ideal_def by auto
show "principal_ideal I"
proof (cases "S = {}")
case True
then show ?thesis
by (metis ideal_generated_0 ideal_generated_empty ig_S principal_ideal_def)
next
case False
obtain xs where set_xs: "set xs = S" and d: "distinct xs"
using finite_distinct_list[OF fin_S] by blast
hence length_eq_card: "length xs = card S" using distinct_card by force
let ?n = "length xs"
let ?A = "Matrix.mat ?n ?n (λ(a,b). if a = b then xs!a else 0)"
have A_carrier: "?A ∈ carrier_mat ?n ?n" by auto
have diag_A: "isDiagonal_mat ?A" unfolding isDiagonal_mat_def by auto
have set_xs_eq: "set xs = {?A$$(i,i)| i. i<dim_row ?A}"
by (auto, smt case_prod_conv d distinct_Ex1 index_mat(1))
have set_xs_diag_mat: "set xs = set (diag_mat ?A)"
using set_xs_eq unfolding diag_mat_def by auto
obtain P Q where P: "P ∈ carrier_mat ?n ?n"
and Q: "Q ∈ carrier_mat ?n ?n" and inv_P: "invertible_mat P" and inv_Q: "invertible_mat Q"
and SNF_PAQ: "Smith_normal_form_mat (P*?A*Q)"
using admits_SNF A_carrier diag_A by blast
define ys where ys_def: "ys = diag_mat (P*?A*Q)"
have ys: "∀i<?n. ys ! i = (P*?A*Q) $$ (i,i)" using P by (auto simp add: ys_def diag_mat_def)
have length_ys: "length ys = ?n" unfolding ys_def
by (metis (no_types, lifting) P carrier_matD(1) diag_mat_def
index_mult_mat(2) length_map map_nth)
have n0: "?n > 0" using False set_xs by blast
have set_ys_diag_mat: "set ys = set (diag_mat (P*?A*Q))" using ys_def by auto
let ?i = "ys ! 0"
have dvd_all: "∀a ∈ set ys. ?i dvd a"
proof
fix a assume a: "a ∈ set ys"
obtain j where ys_j_a: "ys ! j = a" and jn: "j<?n" by (metis a in_set_conv_nth length_ys)
have jP: "j < dim_row P" using jn P by auto
have jQ: "j < dim_col Q" using jn Q by auto
have "(P*?A*Q)$$(0,0) dvd (P*?A*Q)$$(j,j)"
by (rule SNF_first_divides[OF SNF_PAQ], auto simp add: jP jQ)
thus "ys ! 0 dvd a" using ys length_ys ys_j_a jn n0 by auto
qed
have "ideal_generated S = ideal_generated (set xs)" using set_xs by simp
also have "... = ideal_generated (set ys)"
proof
show "ideal_generated (set xs) ⊆ ideal_generated (set ys)"
proof (rule ideal_generated_subset2, rule ballI)
fix b assume b: "b ∈ set xs"
obtain i where b_A_ii: "b = ?A $$ (i,i)" and i_length: "i<length xs"
using b set_xs_eq by auto
obtain P' where inverts_mat_P': "inverts_mat P P' ∧ inverts_mat P' P"
using inv_P unfolding invertible_mat_def by auto
have P': "P' ∈ carrier_mat ?n ?n"
using inverts_mat_P'
unfolding carrier_mat_def inverts_mat_def
by (auto,metis P carrier_matD index_mult_mat(3) one_carrier_mat)+
obtain Q' where inverts_mat_Q': "inverts_mat Q Q' ∧ inverts_mat Q' Q"
using inv_Q unfolding invertible_mat_def by auto
have Q': "Q' ∈ carrier_mat ?n ?n"
using inverts_mat_Q'
unfolding carrier_mat_def inverts_mat_def
by (auto,metis Q carrier_matD index_mult_mat(3) one_carrier_mat)+
have rw_PAQ: "(P'*(P*?A*Q)*Q') $$ (i, i) = ?A $$ (i,i)"
using inv_P'PAQQ'[OF A_carrier P _ _ Q P' Q'] inverts_mat_P' inverts_mat_Q' by auto
have diag_PAQ: "isDiagonal_mat (P*?A*Q)"
using SNF_PAQ unfolding Smith_normal_form_mat_def by auto
have PAQ_carrier: "(P*?A*Q) ∈ carrier_mat ?n ?n" using P Q by auto
obtain f where f: "(P'*(P*?A*Q)*Q') $$ (i, i) = (∑i∈set (diag_mat (P*?A*Q)). f i * i)"
using exists_f_PAQ_Aii[OF diag_PAQ P' PAQ_carrier Q' i_length] by auto
hence "?A $$ (i,i) = (∑i∈set (diag_mat (P*?A*Q)). f i * i)" unfolding rw_PAQ .
thus "b∈ ideal_generated (set ys)"
unfolding ideal_explicit using set_ys_diag_mat b_A_ii by auto
qed
show "ideal_generated (set ys) ⊆ ideal_generated (set xs)"
proof (rule ideal_generated_subset2, rule ballI)
fix b assume b: "b ∈ set ys"
have d: "distinct (diag_mat ?A)"
by (metis (no_types, lifting) A_carrier card_distinct carrier_matD(1) diag_mat_def
length_eq_card length_map map_nth set_xs set_xs_diag_mat)
obtain i where b_PAQ_ii: "(P*?A*Q) $$ (i,i) = b" and i_length: "i<length xs" using b ys
by (metis (no_types, lifting) in_set_conv_nth length_ys)
obtain f where "(P * ?A * Q) $$ (i, i) = (∑i∈set (diag_mat ?A). f i * i)"
using exists_f_PAQ_Aii[OF diag_A P _ Q i_length] by auto
thus "b ∈ ideal_generated (set xs)"
using b_PAQ_ii unfolding set_xs_diag_mat ideal_explicit by auto
qed
qed
also have "... = ideal_generated (set ys - (set ys - {ys!0}))"
proof (rule ideal_generated_dvd_eq_diff_set)
show "?i ∈ set ys" using n0
by (simp add: length_ys)
show "?i ∉ set ys - {?i}" by auto
show "∀j∈set ys - {?i}. ?i dvd j" using dvd_all by auto
show "finite (set ys - {?i})" by auto
qed
also have "... = ideal_generated {?i}"
by (metis Diff_cancel Diff_not_in insert_Diff insert_Diff_if length_ys n0 nth_mem)
finally show "principal_ideal I" unfolding principal_ideal_def using ig_S by auto
qed
qed
corollary diagonal_admits_SNF_imp_bezout_ring_JNF_alt:
assumes admits_SNF: "∀A. square_mat (A::'a mat) ∧ isDiagonal_mat A
⟶ (∃P Q. P ∈ carrier_mat (dim_row A) (dim_row A)
∧ Q ∈ carrier_mat (dim_row A) (dim_row A) ∧ invertible_mat P ∧ invertible_mat Q
∧ Smith_normal_form_mat (P*A*Q))"
shows "OFCLASS('a::comm_ring_1, bezout_ring_class)"
proof (rule diagonal_admits_SNF_imp_bezout_ring_JNF, rule allI, rule allI, rule impI)
fix A::"'a mat" and n assume A: "A ∈ carrier_mat n n ∧ isDiagonal_mat A"
have "square_mat A" using A by auto
thus "∃P Q. P ∈ carrier_mat n n ∧ Q ∈ carrier_mat n n
∧ invertible_mat P ∧ invertible_mat Q ∧ Smith_normal_form_mat (P * A * Q)"
using A admits_SNF by blast
qed
subsection ‹Trying to transfer the @{text "⟹"} implication to HA.›
text ‹We first hide some constants defined in @{text "Mod_Type_Connect"} in order to use the ones
presented in @{text "Perron_Frobenius.HMA_Connect"} by default.›
context
includes lifting_syntax
begin
lemma to_nat_mod_type_Bij_Nat:
fixes a::"'n::mod_type"
obtains b::'n where "mod_type_class.to_nat a = Bij_Nat.to_nat b"
using Bij_Nat.to_nat_from_nat_id mod_type_class.to_nat_less_card by metis
lemma inj_on_Bij_nat_from_nat: "inj_on (Bij_Nat.from_nat::nat ⇒ 'a) {0..<CARD('a::finite)}"
by (auto simp add: inj_on_def Bij_Nat.from_nat_def length_univ_list_card
nth_eq_iff_index_eq univ_list(1))
text ‹This lemma only holds if $a$ and $b$ have the same type. Otherwise,
it is possible that @{text "Bij_Nat.to_nat a = Bij_Nat.to_nat b"}›
lemma Bij_Nat_to_nat_neq:
fixes a b ::"'n::mod_type"
assumes "to_nat a ≠ to_nat b"
shows "Bij_Nat.to_nat a ≠ Bij_Nat.to_nat b"
using assms to_nat_inj by blast
text ‹The following proof (a transfer rule for diagonal matrices)
is weird, since it does not hold
@{text "Bij_Nat.to_nat a = mod_type_class.to_nat a"}.
At first, it seems possible to obtain the element $a'$ that satisfies
@{text "Bij_Nat.to_nat a' = mod_type_class.to_nat a"} and then continue with the proof, but then
we cannot prove @{text "HMA_I (Bij_Nat.to_nat a') a"}.
This means that we must use the previous lemma @{text "Bij_Nat_to_nat_neq"}, but this imposes the
matrix to be square.
›
lemma HMA_isDiagonal[transfer_rule]: "(HMA_M ===> (=))
isDiagonal_mat (isDiagonal::('a::{zero}^'n::{mod_type}^'n::{mod_type} => bool))"
proof (intro rel_funI, goal_cases)
case (1 x y)
note rel_xy [transfer_rule] = "1"
have "y $h a $h b = 0"
if all0: "∀i j. i ≠ j ∧ i < dim_row x ∧ j < dim_col x ⟶ x $$ (i, j) = 0"
and a_noteq_b: "a ≠ b" for a::'n and b::'n
proof -
have "to_nat a ≠ to_nat b" using a_noteq_b by auto
hence distinct: "Bij_Nat.to_nat a ≠ Bij_Nat.to_nat b" by (rule Bij_Nat_to_nat_neq)
moreover have "Bij_Nat.to_nat a < dim_row x" and "Bij_Nat.to_nat b < dim_col x"
using Bij_Nat.to_nat_less_card dim_row_transfer_rule rel_xy dim_col_transfer_rule
by fastforce+
ultimately have b: "x $$ (Bij_Nat.to_nat a, Bij_Nat.to_nat b) = 0" using all0 by auto
have [transfer_rule]: "HMA_I (Bij_Nat.to_nat a) a" by (simp add: HMA_I_def)
have [transfer_rule]: "HMA_I (Bij_Nat.to_nat b) b" by (simp add: HMA_I_def)
have "index_hma y a b = 0" using b by (transfer', auto)
thus ?thesis unfolding index_hma_def .
qed
moreover have "x $$ (i, j) = 0"
if all0: "∀a b. a ≠ b ⟶ y $h a $h b = 0"
and ij: "i ≠ j" and i: "i < dim_row x" and j: "j < dim_col x" for i j
proof -
have i_n: "i < CARD('n)" and j_n: "j < CARD('n)"
using i j rel_xy dim_row_transfer_rule dim_col_transfer_rule
by fastforce+
let ?i' = "Bij_Nat.from_nat i::'n"
let ?j' = "Bij_Nat.from_nat j::'n"
have i'_neq_j': "?i' ≠ ?j'" using ij i_n j_n Bij_Nat.from_nat_inj by blast
hence y0: "index_hma y ?i' ?j' = 0" using all0 unfolding index_hma_def by auto
have [transfer_rule]: "HMA_I i ?i'" unfolding HMA_I_def
by (simp add: Bij_Nat.to_nat_from_nat_id i_n)
have [transfer_rule]: "HMA_I j ?j'" unfolding HMA_I_def
by (simp add: Bij_Nat.to_nat_from_nat_id j_n)
show ?thesis using y0 by (transfer, auto)
qed
ultimately show ?case unfolding isDiagonal_mat_def isDiagonal_def
by auto
qed
text ‹Indeed, we can prove the transfer rules with the new connection based on the
@{text "mod_type"} class, which was developed in the @{text "Mod_Type_Connect"} file›
text ‹This is the same lemma as the one presented above, but now using the @{text "to_nat"} function
defined in the @{text "mod_type"} class and then we can prove it for non-square matrices,
which is very useful since our algorithms are not restricted to square matrices.›
lemma HMA_isDiagonal_Mod_Type[transfer_rule]: "(Mod_Type_Connect.HMA_M ===> (=))
isDiagonal_mat (isDiagonal::('a::{zero}^'n::{mod_type}^'m::{mod_type} => bool))"
proof (intro rel_funI, goal_cases)
case (1 x y)
note rel_xy [transfer_rule] = "1"
have "y $h a $h b = 0"
if all0: "∀i j. i ≠ j ∧ i < dim_row x ∧ j < dim_col x ⟶ x $$ (i, j) = 0"
and a_noteq_b: "to_nat a ≠ to_nat b" for a::'m and b::'n
proof -
have distinct: "to_nat a ≠ to_nat b" using a_noteq_b by auto
moreover have "to_nat a < dim_row x" and "to_nat b < dim_col x"
using to_nat_less_card rel_xy
using Mod_Type_Connect.dim_row_transfer_rule Mod_Type_Connect.dim_col_transfer_rule
by fastforce+
ultimately have b: "x $$ (to_nat a, to_nat b) = 0" using all0 by auto
have [transfer_rule]: "Mod_Type_Connect.HMA_I (to_nat a) a"
by (simp add: Mod_Type_Connect.HMA_I_def)
have [transfer_rule]: "Mod_Type_Connect.HMA_I (to_nat b) b"
by (simp add: Mod_Type_Connect.HMA_I_def)
have "index_hma y a b = 0" using b by (transfer', auto)
thus ?thesis unfolding index_hma_def .
qed
moreover have "x $$ (i, j) = 0"
if all0: "∀a b. to_nat a ≠ to_nat b ⟶ y $h a $h b = 0"
and ij: "i ≠ j" and i: "i < dim_row x" and j: "j < dim_col x" for i j
proof -
have i_n: "i < CARD('m)"
using i rel_xy by (simp add: Mod_Type_Connect.dim_row_transfer_rule)
have j_n: "j < CARD('n)"
using j rel_xy by (simp add: Mod_Type_Connect.dim_col_transfer_rule)
let ?i' = "from_nat i::'m"
let ?j' = "from_nat j::'n"
have "to_nat ?i' ≠ to_nat ?j'"
by (simp add: i_n ij j_n mod_type_class.to_nat_from_nat_id)
hence y0: "index_hma y ?i' ?j' = 0" using all0 unfolding index_hma_def by auto
have [transfer_rule]: "Mod_Type_Connect.HMA_I i ?i'"
unfolding Mod_Type_Connect.HMA_I_def
by (simp add: to_nat_from_nat_id i_n)
have [transfer_rule]: "Mod_Type_Connect.HMA_I j ?j'"
unfolding Mod_Type_Connect.HMA_I_def
by (simp add: to_nat_from_nat_id j_n)
show ?thesis using y0 by (transfer, auto)
qed
ultimately show ?case unfolding isDiagonal_mat_def isDiagonal_def
by auto
qed
text‹We state the transfer rule using the relations developed in the new bride of the file
@{text "Mod_Type_Connect"}.›
lemma HMA_SNF[transfer_rule]: "(Mod_Type_Connect.HMA_M ===> (=)) Smith_normal_form_mat
(Smith_normal_form::'a::{comm_ring_1}^'n::{mod_type}^'m::{mod_type}⇒bool)"
proof (intro rel_funI, goal_cases)
case (1 x y)
note rel_xy[transfer_rule] = "1"
have "y $h a $h b dvd y $h (a + 1) $h (b + 1)"
if SNF_condition: "∀a. Suc a < dim_row x ∧ Suc a < dim_col x
⟶ x $$ (a, a) dvd x $$ (Suc a, Suc a)"
and a1: "Suc (to_nat a) < nrows y" and a2: "Suc (to_nat b) < ncols y"
and ab: "to_nat a = to_nat b" for a::'m and b::'n
proof -
have [transfer_rule]: "Mod_Type_Connect.HMA_I (to_nat a) a"
by (simp add: Mod_Type_Connect.HMA_I_def)
have [transfer_rule]: "Mod_Type_Connect.HMA_I (to_nat (a+1)) (a+1)"
by (simp add: Mod_Type_Connect.HMA_I_def)
have [transfer_rule]: "Mod_Type_Connect.HMA_I (to_nat b) b"
by (simp add: Mod_Type_Connect.HMA_I_def)
have [transfer_rule]: "Mod_Type_Connect.HMA_I (to_nat (b+1)) (b+1)"
by (simp add: Mod_Type_Connect.HMA_I_def)
have "Suc (to_nat a) < dim_row x" using a1
by (metis Mod_Type_Connect.dim_row_transfer_rule nrows_def rel_xy)
moreover have "Suc (to_nat b) < dim_col x"
by (metis Mod_Type_Connect.dim_col_transfer_rule a2 ncols_def rel_xy)
ultimately have "x $$ (to_nat a, to_nat b) dvd x $$ (Suc (to_nat a), Suc (to_nat b))"
using SNF_condition by (simp add: ab)
also have "... = x $$ (to_nat (a+1), to_nat (b+1))"
by (metis Suc_eq_plus1 a1 a2 nrows_def ncols_def to_nat_suc)
finally have SNF_cond: "x $$ (to_nat a, to_nat b) dvd x $$ (to_nat (a + 1), to_nat (b + 1))" .
have "x $$ (to_nat a, to_nat b) = index_hma y a b" by (transfer, simp)
moreover have "x $$ (to_nat (a + 1), to_nat (b + 1)) = index_hma y (a+1) (b+1)"
by (transfer, simp)
ultimately show ?thesis using SNF_cond unfolding index_hma_def by auto
qed
moreover have "x $$ (a, a) dvd x $$ (Suc a, Suc a)"
if SNF: "∀a b. to_nat a = to_nat b ∧ Suc (to_nat a) < nrows y ∧ Suc (to_nat b) < ncols y
⟶ y $h a $h b dvd y $h (a + 1) $h (b + 1)"
and a1: "Suc a < dim_row x" and a2: "Suc a < dim_col x" for a
proof -
have dim_row_CARD: "dim_row x = CARD('m)"
using Mod_Type_Connect.dim_row_transfer_rule rel_xy by blast
have dim_col_CARD: "dim_col x = CARD('n)"
using Mod_Type_Connect.dim_col_transfer_rule rel_xy by blast
let ?a' = "from_nat a::'m"
let ?b' = "from_nat a::'n"
have Suc_a_less_CARD: "a + 1 < CARD('m)" using a1 dim_row_CARD by auto
have Suc_b_less_CARD: "a + 1 < CARD('n)" using a2
by (metis Mod_Type_Connect.dim_col_transfer_rule Suc_eq_plus1 rel_xy)
have aa'[transfer_rule]: "Mod_Type_Connect.HMA_I a ?a'"
unfolding Mod_Type_Connect.HMA_I_def
by (metis Suc_a_less_CARD add_lessD1 mod_type_class.to_nat_from_nat_id)
have [transfer_rule]: "Mod_Type_Connect.HMA_I (a+1) (?a' + 1)"
unfolding Mod_Type_Connect.HMA_I_def
unfolding from_nat_suc[symmetric] using to_nat_from_nat_id[OF Suc_a_less_CARD] by auto
have ab'[transfer_rule]: "Mod_Type_Connect.HMA_I a ?b'"
unfolding Mod_Type_Connect.HMA_I_def
by (metis Suc_b_less_CARD add_lessD1 mod_type_class.to_nat_from_nat_id)
have [transfer_rule]: "Mod_Type_Connect.HMA_I (a+1) (?b' + 1)"
unfolding Mod_Type_Connect.HMA_I_def
unfolding from_nat_suc[symmetric] using to_nat_from_nat_id[OF Suc_b_less_CARD] by auto
have aa'1: "a = to_nat ?a'" using aa' by (simp add: Mod_Type_Connect.HMA_I_def)
have ab'1: "a = to_nat ?b'" using ab' by (simp add: Mod_Type_Connect.HMA_I_def)
have "Suc (to_nat ?a') < nrows y" using a1 dim_row_CARD
by (simp add: mod_type_class.to_nat_from_nat_id nrows_def)
moreover have "Suc (to_nat ?b') < ncols y" using a2 dim_col_CARD
by (simp add: mod_type_class.to_nat_from_nat_id ncols_def)
ultimately have SNF': "y $h ?a' $h ?b' dvd y $h (?a' + 1) $h (?b' + 1)"
using SNF ab'1 aa'1 by auto
have "index_hma y ?a' ?b' = x $$ (a, a)" by (transfer, simp)
moreover have "index_hma y (?a'+1) (?b'+1) = x $$ (a+1, a+1)" by (transfer, simp)
ultimately show ?thesis using SNF' unfolding index_hma_def by auto
qed
ultimately show ?case unfolding Smith_normal_form_mat_def Smith_normal_form_def
using rel_xy by (auto) (transfer', auto)+
qed
lemma HMA_admits_SNF [transfer_rule]:
"((Mod_Type_Connect.HMA_M :: _ ⇒ 'a :: comm_ring_1 ^ 'n::{mod_type} ^ 'n::{mod_type} ⇒ _) ===> (=))
admits_SNF_JNF admits_SNF_HA"
proof (intro rel_funI, goal_cases)
case (1 x y)
note [transfer_rule] = this
hence id: "dim_row x = CARD('n)" by (auto simp: Mod_Type_Connect.HMA_M_def)
then show ?case unfolding admits_SNF_JNF_def admits_SNF_HA_def
by (transfer, auto, metis "1" Mod_Type_Connect.dim_col_transfer_rule)
qed
end
text‹Here we have a problem when trying to apply local type definitions›
lemma diagonal_admits_SNF_imp_bezout_ring:
assumes admits_SNF: "∀A::'a::comm_ring_1^'n::{mod_type}^'n::{mod_type}. isDiagonal A
⟶ (∃P Q. invertible (P::'a::comm_ring_1^'n::{mod_type}^'n::{mod_type})
∧ invertible (Q::'a::comm_ring_1^'n::{mod_type}^'n::{mod_type})
∧ Smith_normal_form (P**A**Q))"
shows "OFCLASS('a::comm_ring_1, bezout_ring_class)"
proof (rule diagonal_admits_SNF_imp_bezout_ring_JNF, auto)
fix A::"'a mat" and n
assume A: "A ∈ carrier_mat n n" and diag_A: "isDiagonal_mat A"
have a: "∀A::'a::comm_ring_1^'n::{mod_type}^'n::{mod_type}. admits_SNF_HA A"
using admits_SNF unfolding admits_SNF_HA_def .
have JNF: "∀(A::'a mat)∈ carrier_mat CARD('n) CARD('n). admits_SNF_JNF A"
proof
fix A::"'a mat"
assume A: "A ∈ carrier_mat CARD('n) CARD('n)"
let ?B = "(Mod_Type_Connect.to_hma⇩m A::'a::comm_ring_1^'n::{mod_type}^'n::{mod_type})"
have [transfer_rule]: "Mod_Type_Connect.HMA_M A ?B"
using A unfolding Mod_Type_Connect.HMA_M_def by auto
have b: "admits_SNF_HA ?B" using a by auto
show "admits_SNF_JNF A" using b by transfer
qed
thus "∃P. P ∈ carrier_mat n n ∧
(∃Q. Q ∈ carrier_mat n n ∧ invertible_mat P
∧ invertible_mat Q ∧ Smith_normal_form_mat (P * A * Q))"
using JNF A diag_A unfolding admits_SNF_JNF_def unfolding square_mat.simps oops
text‹This means that the @{text "⟹"} implication cannot be proven in HA, since we cannot quantify
over type variables in Isabelle/HOL. We then prove both implications in JNF.›
subsection ‹Transfering the @{text "⟸"} implication from HA to JNF using transfer rules
and local type definitions›
lemma bezout_ring_imp_diagonal_admits_SNF_mod_ring:
assumes of: "OFCLASS('a::comm_ring_1, bezout_ring_class)"
shows "∀A::'a^'n::nontriv mod_ring^'n::nontriv mod_ring. isDiagonal A
⟶ (∃P Q.
invertible (P::'a^'n::nontriv mod_ring^'n::nontriv mod_ring) ∧
invertible (Q::'a^'n::nontriv mod_ring^'n::nontriv mod_ring) ∧
Smith_normal_form (P**A**Q))"
using bezout_ring_imp_diagonal_admits_SNF[OF assms] by auto
lemma bezout_ring_imp_diagonal_admits_SNF_mod_ring_admits:
assumes of: "class.bezout_ring (*) (1::'a::comm_ring_1) (+) 0 (-) uminus"
shows "∀A::'a^'n::nontriv mod_ring^'n::nontriv mod_ring. admits_SNF_HA A"
using bezout_ring_imp_diagonal_admits_SNF
[OF bezout_ring.intro_of_class[OF of]]
unfolding admits_SNF_HA_def by auto
text‹I start here to apply local type definitions›
context
fixes p::nat
assumes local_typedef: "∃(Rep :: ('b ⇒ int)) Abs. type_definition Rep Abs {0..<p :: int}"
and p: "p>1"
begin
lemma type_to_set:
shows "class.nontriv TYPE('b)" (is ?a) and "p=CARD('b)" (is ?b)
proof -
from local_typedef obtain Rep::"('b ⇒ int)" and Abs
where t: "type_definition Rep Abs {0..<p :: int}" by auto
have "card (UNIV :: 'b set) = card {0..<p}" using t type_definition.card by fastforce
also have "... = p" by auto
finally show ?b ..
then show ?a unfolding class.nontriv_def using p by auto
qed
text‹I transfer the lemma from HA to JNF, substituting @{text "CARD('n)"} by $p$.
I apply @{text "internalize-sort"} to @{text "'n"} and get rid of
the @{text "nontriv"} restriction.›
lemma bezout_ring_imp_diagonal_admits_SNF_mod_ring_admits_aux:
assumes "class.bezout_ring (*) (1::'a::comm_ring_1) (+) 0 (-) uminus"
shows "Ball {A::'a::comm_ring_1 mat. A ∈ carrier_mat p p} admits_SNF_JNF"
using bezout_ring_imp_diagonal_admits_SNF_mod_ring_admits[untransferred, unfolded CARD_mod_ring,
internalize_sort "'n::nontriv", where ?'a='b]
unfolding type_to_set(2)[symmetric] using type_to_set(1) assms by auto
end
text‹The @{text "⟸"} implication in JNF›
text‹Since @{text "nontriv"} imposes the type to have more than one element,
the cases $n=0$ (@{text "A ∈ carrier_mat 0 0"}) and $n = 1$ (@{text "A ∈ carrier_mat 1 1"})
must be treated separately.›
lemma bezout_ring_imp_diagonal_admits_SNF_mod_ring_admits_aux2:
assumes of: "class.bezout_ring (*) (1::'a::comm_ring_1) (+) 0 (-) uminus"
shows "∀(A::'a mat)∈carrier_mat n n. admits_SNF_JNF A"
proof (cases "n = 0")
case True
show ?thesis
by (rule, unfold True admits_SNF_JNF_def isDiagonal_mat_def invertible_mat_def
Smith_normal_form_mat_def carrier_mat_def inverts_mat_def, fastforce)
next
case False note not0 = False
show ?thesis
proof (cases "n=1")
case True
show ?thesis
by (rule, unfold True admits_SNF_JNF_def isDiagonal_mat_def invertible_mat_def
Smith_normal_form_mat_def carrier_mat_def inverts_mat_def, auto)
(metis dvd_1_left index_one_mat(2) index_one_mat(3) less_Suc0 nat_dvd_not_less
right_mult_one_mat' zero_less_Suc)
next
case False
then have "n>1" using not0 by auto
then show ?thesis
using bezout_ring_imp_diagonal_admits_SNF_mod_ring_admits_aux[cancel_type_definition, of n] of
by auto
qed
qed
text ‹Alternative statements›
lemma bezout_ring_imp_diagonal_admits_SNF_JNF:
assumes of: "class.bezout_ring (*) (1::'a::comm_ring_1) (+) 0 (-) uminus"
shows "∀A::'a mat. admits_SNF_JNF A"
proof
fix A::"'a mat"
have "A∈ carrier_mat (dim_row A) (dim_col A)" unfolding carrier_mat_def by auto
thus "admits_SNF_JNF A"
using bezout_ring_imp_diagonal_admits_SNF_mod_ring_admits_aux2[OF of]
by (metis admits_SNF_JNF_def square_mat.elims(2))
qed
lemma admits_SNF_JNF_alt_def:
"(∀A::'a::comm_ring_1 mat. admits_SNF_JNF A)
= (∀A n. (A::'a mat) ∈ carrier_mat n n ∧ isDiagonal_mat A
⟶ (∃P Q. P ∈ carrier_mat n n ∧ Q ∈ carrier_mat n n ∧ invertible_mat P ∧ invertible_mat Q
∧ Smith_normal_form_mat (P*A*Q)))" (is "?a = ?b")
by (auto simp add: admits_SNF_JNF_def, metis carrier_matD(1) carrier_matD(2), blast)
subsection ‹Final theorem in JNF›
text ‹Final theorem using @{text "class.bezout_ring"}›
theorem diagonal_admits_SNF_iff_bezout_ring:
shows "class.bezout_ring (*) (1::'a::comm_ring_1) (+) 0 (-) uminus
⟷ (∀A::'a mat. admits_SNF_JNF A)" (is "?a ⟷ ?b")
proof
assume ?a
thus ?b using bezout_ring_imp_diagonal_admits_SNF_JNF by auto
next
assume b: ?b
have rw: "∀A n. (A::'a mat) ∈ carrier_mat n n ∧ isDiagonal_mat A ⟶
(∃P Q. P ∈ carrier_mat n n ∧ Q ∈ carrier_mat n n ∧ invertible_mat P
∧ invertible_mat Q ∧ Smith_normal_form_mat (P * A * Q))"
using admits_SNF_JNF_alt_def b by auto
show ?a
using diagonal_admits_SNF_imp_bezout_ring_JNF[OF rw]
using OFCLASS_bezout_ring_imp_class_bezout_ring[where ?'a='a]
by auto
qed
text ‹Final theorem using @{text "OFCLASS"}›
theorem diagonal_admits_SNF_iff_bezout_ring':
shows "OFCLASS('a::comm_ring_1, bezout_ring_class) ≡ (⋀A::'a mat. admits_SNF_JNF A)"
proof
fix A::"'a mat"
assume a: "OFCLASS('a, bezout_ring_class)"
show "admits_SNF_JNF A"
using OFCLASS_bezout_ring_imp_class_bezout_ring[OF a] diagonal_admits_SNF_iff_bezout_ring
by auto
next
assume "(⋀A::'a mat. admits_SNF_JNF A)"
hence *: "class.bezout_ring (*) (1::'a) (+) 0 (-) uminus"
using diagonal_admits_SNF_iff_bezout_ring by auto
show "OFCLASS('a, bezout_ring_class)"
by (rule bezout_ring.intro_of_class, rule *)
qed
end