# Theory Smith_Normal_Form

(*
Author: Jose Divasón
Email:  jose.divason@unirioja.es
*)

section ‹Definition of Smith normal form in HOL Analysis›

theory Smith_Normal_Form
imports
Hermite.Hermite
begin

subsection ‹Definitions›

text‹Definition of diagonal matrix›

definition "isDiagonal_upt_k A k = (∀ a b. (to_nat a ≠ to_nat b ∧ (to_nat a < k ∨ (to_nat b < k))) ⟶ A $a$ b = 0)"
definition "isDiagonal A = (∀ a b. to_nat a ≠ to_nat b ⟶ A $a$ b = 0)"

lemma isDiagonal_intro:
fixes A::"'a::{zero}^'cols::mod_type^'rows::mod_type"
assumes "⋀a::'rows. ⋀b::'cols. to_nat a = to_nat b"
shows "isDiagonal A"
using assms
unfolding isDiagonal_def by auto

text‹Definition of Smith normal form up to position k. The element $A_{k-1,k-1}$
does not need to divide $A_{k,k}$ and $A_{k,k}$ could have non-zero entries above and below.›

definition "Smith_normal_form_upt_k A k =
(
(∀a b. to_nat a = to_nat b ∧ to_nat a + 1 < k ∧ to_nat b + 1< k ⟶ A $a$ b dvd A $(a+1)$ (b+1))
∧ isDiagonal_upt_k A k
)"

definition "Smith_normal_form A =
(
(∀a b. to_nat a = to_nat b ∧ to_nat a + 1 < nrows A ∧ to_nat b + 1 < ncols A ⟶ A $a$ b dvd A $(a+1)$ (b+1))
∧ isDiagonal A
)"

subsection ‹Basic properties›

lemma Smith_normal_form_min:
"Smith_normal_form A = Smith_normal_form_upt_k A (min (nrows A) (ncols A))"
unfolding Smith_normal_form_def Smith_normal_form_upt_k_def nrows_def ncols_def
unfolding isDiagonal_upt_k_def isDiagonal_def
by (auto, smt Suc_le_eq le_trans less_le min.boundedI not_less_eq_eq suc_not_zero
to_nat_less_card to_nat_plus_one_less_card')

lemma Smith_normal_form_upt_k_0[simp]: "Smith_normal_form_upt_k A 0"
unfolding Smith_normal_form_upt_k_def
unfolding isDiagonal_upt_k_def isDiagonal_def
by auto

lemma Smith_normal_form_upt_k_intro:
assumes "(⋀a b. to_nat a = to_nat b ∧ to_nat a + 1 < k ∧ to_nat b + 1< k ⟹ A $a$ b dvd A $(a+1)$ (b+1))"
and "(⋀a b. (to_nat a ≠ to_nat b ∧ (to_nat a < k ∨ (to_nat b < k))) ⟹ A $a$ b = 0)"
shows "Smith_normal_form_upt_k A k"
unfolding Smith_normal_form_upt_k_def
unfolding isDiagonal_upt_k_def isDiagonal_def using assms by simp

lemma Smith_normal_form_upt_k_intro_alt:
assumes "(⋀a b. to_nat a = to_nat b ∧ to_nat a + 1 < k ∧ to_nat b + 1 < k ⟹ A $a$ b dvd A $(a+1)$ (b+1))"
and "isDiagonal_upt_k A k"
shows "Smith_normal_form_upt_k A k"
using assms
unfolding Smith_normal_form_upt_k_def by auto

lemma Smith_normal_form_upt_k_condition1:
fixes A::"'a::{bezout_ring}^'cols::mod_type^'rows::mod_type"
assumes "Smith_normal_form_upt_k A k"
and "to_nat a = to_nat b" and " to_nat a + 1 < k" and "to_nat b + 1 < k "
shows "A $a$ b dvd A $(a+1)$ (b+1)"
using assms unfolding Smith_normal_form_upt_k_def by auto

lemma Smith_normal_form_upt_k_condition2:
fixes A::"'a::{bezout_ring}^'cols::mod_type^'rows::mod_type"
assumes "Smith_normal_form_upt_k A k"
and "to_nat a ≠ to_nat b" and "(to_nat a < k ∨ to_nat b < k)"
shows "((A $a)$ b) = 0"
using assms unfolding Smith_normal_form_upt_k_def
unfolding isDiagonal_upt_k_def isDiagonal_def by auto

lemma Smith_normal_form_upt_k1_intro:
fixes A::"'a::{bezout_ring}^'cols::mod_type^'rows::mod_type"
assumes s: "Smith_normal_form_upt_k A k"
and cond1: "A $from_nat (k - 1)$ from_nat (k-1) dvd A $(from_nat k)$ (from_nat k)"
and cond2a: "∀a. to_nat a > k ⟶ A $a$ from_nat k = 0"
and cond2b: "∀b. to_nat b > k ⟶ A $from_nat k$ b = 0"
shows "Smith_normal_form_upt_k A (Suc k)"
proof (rule Smith_normal_form_upt_k_intro)
fix a::'rows and b::'cols
assume a: "to_nat a ≠ to_nat b ∧ (to_nat a < Suc k ∨ to_nat b < Suc k)"
show "A $a$ b = 0"
by (metis Smith_normal_form_upt_k_condition2 a
assms(1) cond2a cond2b from_nat_to_nat_id less_SucE nat_neq_iff)
next
fix a::'rows and b::'cols
assume a: "to_nat a = to_nat b ∧ to_nat a + 1 < Suc k ∧ to_nat b + 1 < Suc k"
show "A $a$ b dvd A $(a + 1)$ (b + 1)"
by (metis (mono_tags, lifting) Smith_normal_form_upt_k_condition1 a add_diff_cancel_right' cond1
from_nat_suc from_nat_to_nat_id less_SucE s)
qed

lemma Smith_normal_form_upt_k1_intro_diagonal:
fixes A::"'a::{bezout_ring}^'cols::mod_type^'rows::mod_type"
assumes s: "Smith_normal_form_upt_k A k"
and d: "isDiagonal A"
and cond1: "A $from_nat (k - 1)$ from_nat (k-1) dvd A $(from_nat k)$ (from_nat k)"
shows "Smith_normal_form_upt_k A (Suc k)"
proof (rule Smith_normal_form_upt_k_intro)
fix a::'rows and b::'cols
assume a: "to_nat a = to_nat b ∧ to_nat a + 1 < Suc k ∧ to_nat b + 1 < Suc k"
show "A $a$ b dvd A $(a + 1)$ (b + 1)"
by (metis (mono_tags, lifting) Smith_normal_form_upt_k_condition1 a
add_diff_cancel_right' cond1 from_nat_suc from_nat_to_nat_id less_SucE s)
next
show "⋀a b. to_nat a ≠ to_nat b ∧ (to_nat a < Suc k ∨ to_nat b < Suc k) ⟹ A $a$ b = 0"
using d isDiagonal_def by blast
qed

end

# Theory Diagonal_To_Smith

(*
Author:      Jose Divasón
Email:       jose.divason@unirioja.es
*)

section ‹Algorithm to transform a diagonal matrix into its Smith normal form›

theory Diagonal_To_Smith
imports Hermite.Hermite
"HOL-Types_To_Sets.Types_To_Sets"
Smith_Normal_Form
begin

(*Move this theorem:*)
lemma invertible_mat_1: "invertible (mat (1::'a::comm_ring_1))"
unfolding invertible_iff_is_unit by simp

subsection ‹Implementation of the algorithm›

type_synonym 'a bezout = "'a ⇒ 'a ⇒ 'a × 'a × 'a × 'a × 'a"

hide_const Countable.from_nat
hide_const Countable.to_nat

text ‹The algorithm is based on the one presented by Bradley in his article entitled
Algorithms for Hermite and Smith normal matrices and linear diophantine equations''.
Some improvements have been introduced to get a general version for any matrix (including
non-square and singular ones).›

text ‹I also introduced another improvement: the element in the position j does not need
to be checked each time, since the element $A_{ii}$ will already divide $A_{jj}$ (where $j \le k$).
The gcd will be placed in $A_{ii}$.›

(*This version is a valid implementation and permits the formalization,
but it would not be executable due to the abstraction*)

(*
primrec diagonal_to_Smith_i :: "nat list ⇒ 'a:: {gcd,divide}^'n::mod_type^'n::mod_type ⇒ 'n::mod_type ⇒ 'a^'n::mod_type^'n::mod_type"
where
"diagonal_to_Smith_i [] A i  = A" |
"diagonal_to_Smith_i (j#xs) A i  = (
if A $i$ i dvd A $(from_nat j)$ (from_nat j) then diagonal_to_Smith_i xs A i  (*If it divides, then we proceed.*)
else
let c = gcd (A$i$i) (A$(from_nat j)$(from_nat j));
A' = (χ a b. if a = i ∧ b = i then c else
if a = from_nat j ∧ b = from_nat j
then A$i$ i * (A $(from_nat j)$ (from_nat j) div c) else A $a$ b)
in diagonal_to_Smith_i xs A' i (*We do the step and proceed*)
)
"
*)

text ‹This function transforms the element $A_{jj}$ in order to be divisible by $A_{ii}$
(and it changes $A_{ii}$ as well).

The use of @{text "from_nat"} and @{text "from_nat"} is mandatory since the same
index $i$ cannot be used for both rows
and columns at the same time, since they could have different type, concretely,
when the matrix is rectangular.›

text‹The following definition is valid, but since execution requires the trick of converting
all operations in terms of rows, then we would be recalculating the B\'ezout coefficients each time.›

(*
definition "diagonal_step A i j bezout = (let
(p, q, u, v, d) = bezout (A $from_nat i$ from_nat i) (A $(from_nat j)$ (from_nat j)) in
(χ a b. if a = from_nat i ∧ b = from_nat i then d else
if a = from_nat j ∧ b = from_nat j
then  v * (A $(from_nat j)$ (from_nat j)) else A $a$ b))"
*)

text‹Thus, the definition is parameterized by the necessary elements instead of the operation,
to avoid recalculations.›

definition "diagonal_step A i j d v =
(χ a b. if a = from_nat i ∧ b = from_nat i then d else
if a = from_nat j ∧ b = from_nat j
then  v * (A $(from_nat j)$ (from_nat j)) else A $a$ b)"

fun diagonal_to_Smith_i ::
"nat list ⇒ 'a::{bezout_ring}^'cols::mod_type^'rows::mod_type ⇒ nat ⇒ ('a bezout)
⇒ 'a^'cols::mod_type^'rows::mod_type"
where
"diagonal_to_Smith_i [] A i bezout = A" |
"diagonal_to_Smith_i (j#xs) A i bezout = (
if A $(from_nat i)$ (from_nat i) dvd A $(from_nat j)$ (from_nat j)
then diagonal_to_Smith_i xs A i bezout
else let (p, q, u, v, d) = bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j);
A' = diagonal_step A i j d v
in diagonal_to_Smith_i xs A' i bezout
)
"

definition "Diagonal_to_Smith_row_i A i bezout
= diagonal_to_Smith_i [i+1..<min (nrows A) (ncols A)] A i bezout"

fun diagonal_to_Smith_aux :: " 'a::{bezout_ring}^'cols::mod_type^'rows::mod_type
⇒ nat list ⇒ ('a bezout) ⇒  'a^'cols::mod_type^'rows::mod_type"
where
"diagonal_to_Smith_aux A [] bezout = A" |
"diagonal_to_Smith_aux A (i#xs) bezout
= diagonal_to_Smith_aux (Diagonal_to_Smith_row_i A i bezout) xs bezout"

text‹The minimum arises to include the case of non-square matrices (we do not
demand the input diagonal matrix to be square, just have zeros in non-diagonal entries).

This iteration does not need to be performed until the last element of the diagonal,
because in the second-to-last step the matrix will be already in Smith normal form.›

definition "diagonal_to_Smith A bezout
= diagonal_to_Smith_aux A [0..<min (nrows A) (ncols A) - 1] bezout"

subsection‹Code equations to get an executable version›

definition diagonal_step_row
where "diagonal_step_row A i j c v a = vec_lambda (%b. if a = from_nat i ∧ b = from_nat i then c else
if a = from_nat j ∧ b = from_nat j
then v * (A $(from_nat j)$ (from_nat j)) else A $a$ b)"

lemma diagonal_step_code [code abstract]:
"vec_nth (diagonal_step_row A i j c v a) = (%b. if a = from_nat i ∧ b = from_nat i then c else
if a = from_nat j ∧ b = from_nat j
then v * (A $(from_nat j)$ (from_nat j)) else A $a$ b)"
unfolding diagonal_step_row_def by auto

lemma diagonal_step_code_nth [code abstract]: "vec_nth (diagonal_step A i j c v)
= diagonal_step_row A i j c v"
unfolding diagonal_step_def unfolding diagonal_step_row_def[abs_def]
by auto

text‹Code equation to avoid recalculations when computing the Bezout coefficients. ›
lemma euclid_ext2_code[code]:
"euclid_ext2 a b = (let ((p,q),d) = euclid_ext a b in (p,q, - b div d, a div d, d))"
unfolding euclid_ext2_def split_beta Let_def
by auto

subsection‹Examples of execution›

value "let A= list_of_list_to_matrix [[12,0,0::int],[0,6,0::int],[0,0,2::int]]::int^3^3
in matrix_to_list_of_list (diagonal_to_Smith A euclid_ext2)"

text‹Example obtained from:
\url{https://math.stackexchange.com/questions/77063/how-do-i-get-this-matrix-in-smith-normal-form-and-is-smith-normal-form-unique}
›

value "let A= list_of_list_to_matrix
[
[[:-3,1:],0,0,0],
[0,[:1,1:],0,0],
[0,0,[:1,1:],0],
[0,0,0,[:1,1:]]]::rat poly^4^4
in matrix_to_list_of_list (diagonal_to_Smith A euclid_ext2)"

text‹Polynomial matrix›
value "let A = list_of_list_to_matrix
[
[[:-3,1:],0,0,0],
[0,[:1,1:],0,0],
[0,0,[:1,1:],0],
[0,0,0,[:1,1:]],
[0,0,0,0]]::rat poly^4^5
in matrix_to_list_of_list (diagonal_to_Smith A euclid_ext2)"

subsection‹Soundness of the algorithm›

lemma nrows_diagonal_step[simp]: "nrows (diagonal_step A i j c v) = nrows A"

lemma ncols_diagonal_step[simp]: "ncols (diagonal_step A i j c v) = ncols A"

context
fixes bezout::"'a::{bezout_ring} ⇒ 'a ⇒ 'a × 'a × 'a × 'a × 'a"
assumes ib: "is_bezout_ext bezout"
begin

lemma split_beta_bezout: "bezout a b =
(fst(bezout a b),
fst (snd (bezout a b)),
fst (snd(snd (bezout a b))),
fst (snd(snd(snd (bezout a b)))),
snd (snd(snd(snd (bezout a b)))))" unfolding split_beta by (auto simp add: split_beta)

text‹The following lemma shows that @{text "diagonal_to_Smith_i"} preserves the previous element.
We use the assumption @{text "to_nat a = to_nat b"} in order to ensure that we are treating with
a diagonal entry. Since the matrix could be rectangular, the types of a and b can be different,
and thus we cannot write either @{text "a = b"} or @{text "A $a$ b"}.›

lemma diagonal_to_Smith_i_preserves_previous_diagonal:
fixes A::"'a:: {bezout_ring}^'b::mod_type^'c::mod_type"
assumes i_min: "i < min (nrows A) (ncols A)"
and "to_nat a ∉ set xs" and "to_nat a = to_nat b"
and "to_nat a ≠ i"
and elements_xs_range: "∀x. x ∈ set xs ⟶ x<min (nrows A) (ncols A)"
shows "(diagonal_to_Smith_i xs A i bezout) $a$ b = A $a$ b"
using assms
proof (induct xs A i bezout rule: diagonal_to_Smith_i.induct)
case (1 A i bezout)
then show ?case by auto
next
case (2 j xs A i bezout)
let ?Aii = "A $from_nat i$ from_nat i"
let ?Ajj = "A $from_nat j$ from_nat j"
let ?p="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ p"
let ?q="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ q"
let ?u="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ u"
let ?v="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ v"
let ?d="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ d"
let ?A'="diagonal_step A i j ?d ?v"
have pquvd: "(?p, ?q, ?u, ?v,?d) = bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j)"
show ?case
proof (cases "?Aii dvd ?Ajj")
case True
then show ?thesis
using "2.hyps" "2.prems" by auto
next
case False
note i_min = 2(3)
note hyp = 2(2)
note i_notin = 2(4)
note a_eq_b = "2.prems"(3)
note elements_xs = 2(7)
note a_not_i = 2(6)
have a_not_j: "a ≠ from_nat j"
by (metis elements_xs i_notin list.set_intros(1) min_less_iff_conj nrows_def to_nat_from_nat_id)
have "diagonal_to_Smith_i (j # xs) A i bezout = diagonal_to_Smith_i xs ?A' i bezout"
using False by (auto simp add: split_beta)
also have "... $a$ b = ?A' $a$ b"
by (rule hyp[OF False], insert i_notin i_min a_eq_b a_not_i pquvd elements_xs, auto)
also have "... = A $a$ b"
unfolding diagonal_step_def
using a_not_j a_not_i
by (smt i_min min.strict_boundedE nrows_def to_nat_from_nat_id vec_lambda_beta)
finally show ?thesis .
qed
qed

lemma diagonal_step_dvd1[simp]:
fixes A::"'a::{bezout_ring}^'b::mod_type^'c::mod_type" and j i
defines "v==case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ v"
and "d==case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ d"
shows "diagonal_step A i j d v $from_nat i$ from_nat i dvd A $from_nat i$ from_nat i"
using ib unfolding is_bezout_ext_def diagonal_step_def v_def d_def

lemma diagonal_step_dvd2[simp]:
fixes A::"'a::{bezout_ring}^'b::mod_type^'c::mod_type" and j i
defines "v==case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ v"
and "d==case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ d"
shows "diagonal_step A i j d v $from_nat i$ from_nat i dvd A $from_nat j$ from_nat j"
using ib unfolding is_bezout_ext_def diagonal_step_def v_def d_def

end

text‹Once the step is carried out, the new element ${A'}_{ii}$ will divide the element $A_{ii}$›

lemma diagonal_to_Smith_i_dvd_ii:
fixes A::"'a::{bezout_ring}^'b::mod_type^'c::mod_type"
assumes ib: "is_bezout_ext bezout"
shows "diagonal_to_Smith_i xs A i bezout $from_nat i$ from_nat i dvd A $from_nat i$ from_nat i"
using ib
proof (induct xs A i bezout rule: diagonal_to_Smith_i.induct)
case (1 A i bezout)
then show ?case by auto
next
case (2 j xs A i bezout)
let ?Aii = "A $from_nat i$ from_nat i"
let ?Ajj = "A $from_nat j$ from_nat j"
let ?p="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ p"
let ?q="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ q"
let ?u="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ u"
let ?v="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ v"
let ?d="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ d"
let ?A'="diagonal_step A i j ?d ?v"
have pquvd: "(?p, ?q, ?u, ?v,?d) = bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j)"
note ib = "2.prems"(1)
show ?case
proof (cases "?Aii dvd ?Ajj")
case True
then show ?thesis
using "2.hyps"(1) "2.prems" by auto
next
case False
note hyp = "2.hyps"(2)
have "diagonal_to_Smith_i (j # xs) A i bezout = diagonal_to_Smith_i xs ?A' i bezout"
using False by (auto simp add: split_beta)
also have "... $from_nat i$ from_nat i dvd ?A' $from_nat i$ from_nat i"
by (rule hyp[OF False], insert pquvd ib, auto)
also have "... dvd A $from_nat i$ from_nat i"
unfolding diagonal_step_def using ib unfolding is_bezout_ext_def
finally show ?thesis .
qed
qed

text‹Once the step is carried out, the new element ${A'}_{ii}$
divides the rest of elements of the diagonal. This proof requires commutativity (already
included in the type restriction @{text "bezout_ring"}).›

lemma diagonal_to_Smith_i_dvd_jj:
fixes A::"'a::{bezout_ring}^'b::mod_type^'c::mod_type"
assumes ib: "is_bezout_ext bezout"
and i_min: "i < min (nrows A) (ncols A)"
and elements_xs_range: "∀x. x ∈ set xs ⟶ x<min (nrows A) (ncols A)"
and "to_nat a ∈ set xs"
and "to_nat a = to_nat b"
and "to_nat a ≠ i"
and "distinct xs"
shows "(diagonal_to_Smith_i xs A i bezout) $(from_nat i)$ (from_nat i)
dvd (diagonal_to_Smith_i xs A i bezout) $a$ b"
using assms
proof (induct xs A i bezout rule: diagonal_to_Smith_i.induct)
case (1 A i)
then show ?case by auto
next
case (2 j xs A i bezout)
let ?Aii = "A $from_nat i$ from_nat i"
let ?Ajj = "A $from_nat j$ from_nat j"
let ?p="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ p"
let ?q="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ q"
let ?u="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ u"
let ?v="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ v"
let ?d="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ d"
let ?A'="diagonal_step A i j ?d ?v"
have pquvd: "(?p, ?q, ?u, ?v,?d) = bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j)"
note ib = "2.prems"(1)
note to_nat_a_not_i = 2(8)
note i_min = 2(4)
note elements_xs = "2.prems"(3)
note a_eq_b = "2.prems"(5)
note a_in_j_xs = 2(6)
note distinct = 2(9)
show ?case
proof (cases "?Aii dvd ?Ajj")
case True note Aii_dvd_Ajj = True
show ?thesis
proof (cases "to_nat a = j")
case True
have a: "a = (from_nat j::'c)" using True by auto
have b: "b = (from_nat j::'b)"
using True a_eq_b by auto
have "diagonal_to_Smith_i (j # xs) A i bezout = diagonal_to_Smith_i xs A i bezout"
using Aii_dvd_Ajj by auto
also have "... $from_nat j$ from_nat j = A $from_nat j$ from_nat j"
proof (rule diagonal_to_Smith_i_preserves_previous_diagonal[OF ib i_min])
show "to_nat (from_nat j::'c) ∉ set xs" using True a_in_j_xs distinct by auto
show "to_nat (from_nat j::'c) = to_nat (from_nat j::'b)"
by (metis True a_eq_b from_nat_to_nat_id)
show "to_nat (from_nat j::'c) ≠ i"
using True to_nat_a_not_i by auto
show "∀x. x ∈ set xs ⟶ x < min (nrows A) (ncols A)" using elements_xs by auto
qed
finally have "diagonal_to_Smith_i (j # xs) A i bezout $from_nat j$ from_nat j
= A $from_nat j$ from_nat j " .
hence "diagonal_to_Smith_i (j # xs) A i bezout $a$ b = ?Ajj" unfolding a b .
moreover have "diagonal_to_Smith_i (j # xs) A i bezout $from_nat i$ from_nat i dvd ?Aii"
by (rule diagonal_to_Smith_i_dvd_ii[OF ib])
ultimately show ?thesis using Aii_dvd_Ajj dvd_trans by auto
next
case False
have a_in_xs: "to_nat a ∈ set xs" using False using "2.prems"(4) by auto
have "diagonal_to_Smith_i (j # xs) A i bezout = diagonal_to_Smith_i xs A i bezout"
using True by auto
also have "...  $(from_nat i)$ (from_nat i) dvd diagonal_to_Smith_i xs A i bezout $a$ b"
by (rule "2.hyps"(1)[OF True ib i_min _ a_in_xs a_eq_b to_nat_a_not_i])
(insert elements_xs distinct, auto)
finally show ?thesis .
qed
next
case False note Aii_not_dvd_Ajj = False
show ?thesis
proof (cases "to_nat a ∈ set xs")
case True note a_in_xs = True
have "diagonal_to_Smith_i (j # xs) A i bezout = diagonal_to_Smith_i xs ?A' i bezout"
using False by (auto simp add: split_beta)
also have "... $from_nat i$ from_nat i dvd diagonal_to_Smith_i xs ?A' i bezout $a$ b"
by (rule "2.hyps"(2)[OF False _ _ _ _ _ _ _ _ _ a_in_xs a_eq_b to_nat_a_not_i ])
(insert elements_xs distinct i_min ib pquvd, auto simp add: nrows_def ncols_def)
finally show ?thesis .
next
case False
have to_nat_a_eq_j: "to_nat a = j"
using False a_in_j_xs by auto
have a: "a = (from_nat j::'c)" using to_nat_a_eq_j by auto
have b: "b = (from_nat j::'b)" using to_nat_a_eq_j a_eq_b by auto
have d_eq: "diagonal_to_Smith_i (j # xs) A i bezout = diagonal_to_Smith_i xs ?A' i bezout"
using Aii_not_dvd_Ajj by (simp add: split_beta)
also have "... $a$ b = ?A' $a$ b"
by (rule diagonal_to_Smith_i_preserves_previous_diagonal[OF ib _ False a_eq_b to_nat_a_not_i])
(insert i_min elements_xs ib, auto)
finally have "diagonal_to_Smith_i (j # xs) A i bezout $a$ b = ?A' $a$ b" .
moreover have "diagonal_to_Smith_i (j # xs) A i bezout $from_nat i$ from_nat i
dvd ?A' $from_nat i$ from_nat i"
using d_eq diagonal_to_Smith_i_dvd_ii[OF ib] by simp
moreover have "?A' $from_nat i$ from_nat i dvd ?A' $from_nat j$ from_nat j"
unfolding diagonal_step_def using ib unfolding is_bezout_ext_def split_beta
by (auto, meson dvd_mult)+
ultimately show ?thesis using dvd_trans a b by auto
qed
qed
qed

text‹The step preserves everything that is not in the diagonal›

lemma diagonal_to_Smith_i_preserves_previous:
fixes A::"'a:: {bezout_ring}^'b::mod_type^'c::mod_type"
assumes ib: "is_bezout_ext bezout"
and i_min: "i < min (nrows A) (ncols A)"
and a_not_b: "to_nat a ≠ to_nat b"
and elements_xs_range: "∀x. x ∈ set xs ⟶ x<min (nrows A) (ncols A)"
shows "(diagonal_to_Smith_i xs A i bezout) $a$ b = A $a$ b"
using assms
proof (induct xs A i bezout rule: diagonal_to_Smith_i.induct)
case (1 A i)
then show ?case by auto
next
case (2 j xs A i bezout)
let ?Aii = "A $from_nat i$ from_nat i"
let ?Ajj = "A $from_nat j$ from_nat j"
let ?p="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ p"
let ?q="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ q"
let ?u="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ u"
let ?v="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ v"
let ?d="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ d"
let ?A'="diagonal_step A i j ?d ?v"
have pquvd: "(?p, ?q, ?u, ?v,?d) = bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j)"
note ib = "2.prems"(1)
show ?case
proof (cases "?Aii dvd ?Ajj")
case True
then show ?thesis
using "2.hyps"(1) "2.prems" by auto
next
case False
note hyp = "2.hyps"(2)
have a1: "a = from_nat i ⟶ b ≠ from_nat i"
by (metis "2.prems" a_not_b from_nat_not_eq min.strict_boundedE ncols_def nrows_def)
have a2: "a = from_nat j ⟶ b ≠ from_nat j"
by (metis "2.prems" a_not_b list.set_intros(1) min_less_iff_conj
ncols_def nrows_def to_nat_from_nat_id)
have "diagonal_to_Smith_i (j # xs) A i bezout = diagonal_to_Smith_i xs ?A' i bezout"
using False by (simp add: split_beta)
also have "... $a$ b = ?A' $a$ b"
by (rule hyp[OF False], insert "2.prems" ib pquvd, auto)
also have "... = A $a$ b" unfolding diagonal_step_def using a1 a2 by auto
finally show ?thesis .
qed
qed

lemma diagonal_step_preserves:
fixes A::"'a::{times}^'b::mod_type^'c::mod_type"
assumes ai: "a ≠ i" and aj: "a ≠ j" and a_min: "a < min (nrows A) (ncols A)"
and i_min: "i < min (nrows A) (ncols A)"
and j_min: "j < min (nrows A) (ncols A)"
shows "diagonal_step A i j d v $from_nat a$ from_nat b = A $from_nat a$ from_nat b"
proof -
have 1: "(from_nat a::'c) ≠ from_nat i"
by (metis a_min ai from_nat_eq_imp_eq i_min min.strict_boundedE nrows_def)
have 2: "(from_nat a::'c) ≠ from_nat j"
by (metis a_min aj from_nat_eq_imp_eq j_min min.strict_boundedE nrows_def)
show ?thesis
using 1 2 unfolding diagonal_step_def by auto
qed

context GCD_ring
begin

lemma gcd_greatest:
assumes "is_gcd gcd'" and "c dvd a" and "c dvd b"
shows "c dvd gcd' a b"
using assms is_gcd_def by blast

end

text‹This is a key lemma for the soundness of the algorithm.›

lemma diagonal_to_Smith_i_dvd:
fixes A::"'a:: {bezout_ring}^'b::mod_type^'c::mod_type"
assumes ib: "is_bezout_ext bezout"
and i_min: "i < min (nrows A) (ncols A)"
and elements_xs_range: "∀x. x ∈ set xs ⟶ x<min (nrows A) (ncols A)"
and "∀a b. to_nat a∈insert i (set xs) ∧ to_nat a = to_nat b ⟶
A $(from_nat c)$ (from_nat c) dvd A $a$ b"
and "c ∉ (set xs)" and c: "c<min (nrows A) (ncols A)"
and "distinct xs"
shows "A $(from_nat c)$ (from_nat c) dvd
(diagonal_to_Smith_i xs A i bezout) $(from_nat i)$ (from_nat i)"
using assms
proof (induct xs A i bezout rule: diagonal_to_Smith_i.induct)
case (1 A i)
then show ?case
by (auto simp add: ncols_def nrows_def to_nat_from_nat_id)
next
case (2 j xs A i bezout)
let ?Aii = "A $from_nat i$ from_nat i"
let ?Ajj = "A $from_nat j$ from_nat j"
let ?p="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ p"
let ?q="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ q"
let ?u="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ u"
let ?v="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ v"
let ?d="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ d"
let ?A'="diagonal_step A i j ?d ?v"
have pquvd: "(?p, ?q, ?u, ?v,?d) = bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j)"
note ib = "2.prems"(1)
show ?case
proof (cases "?Aii dvd ?Ajj")
case True note Aii_dvd_Ajj = True
show ?thesis using True
using "2.hyps" "2.prems" by force
next
case False
let ?Acc = "A $from_nat c$ from_nat c"
let ?D="diagonal_step A i j ?d ?v"
note hyp = "2.hyps"(2)
note dvd_condition = "2.prems"(4)
note a_eq_b = "2.hyps"
have 1: "(from_nat c::'c) ≠ from_nat i"
by (metis "2.prems" False c insert_iff list.set_intros(1)
min.strict_boundedE ncols_def nrows_def to_nat_from_nat_id)
have 2: "(from_nat c::'c) ≠ from_nat j"
by (metis  "2.prems" c insertI1 list.simps(15) min_less_iff_conj nrows_def
to_nat_from_nat_id)
have "?D $from_nat c$ from_nat c = ?Acc"
unfolding diagonal_step_def using 1 2 by auto
have aux: "?D $from_nat c$ from_nat c dvd ?D $a$ b"
if a_in_set: "to_nat a ∈ insert i (set xs)" and ab: "to_nat a = to_nat b" for a b
proof -
have Acc_dvd_Aii: "?Acc dvd ?Aii"
by (metis "2.prems"(2) "2.prems"(4) insert_iff min.strict_boundedE
ncols_def nrows_def to_nat_from_nat_id)
moreover have Acc_dvd_Ajj: "?Acc dvd ?Ajj"
by (metis "2.prems"(3) "2.prems"(4) insert_iff list.set_intros(1)
min_less_iff_conj ncols_def nrows_def to_nat_from_nat_id)
ultimately have Acc_dvd_gcd: "?Acc dvd ?d"
by (metis (mono_tags, lifting) ib is_gcd_def is_gcd_is_bezout_ext)
show ?thesis
using 1 2 Acc_dvd_Ajj Acc_dvd_Aii Acc_dvd_gcd a_in_set ab dvd_condition
unfolding diagonal_step_def by auto
qed
have "?A' $from_nat c$ from_nat c = A $from_nat c$ from_nat c"
unfolding diagonal_step_def using 1 2 by auto
moreover have "?A' $from_nat c$ from_nat c
dvd diagonal_to_Smith_i xs ?A' i bezout $from_nat i$ from_nat i"
by (rule hyp[OF False _ _ _ _ _ _ ib])
(insert nrows_def ncols_def "2.prems" "2.hyps" aux pquvd, auto)
ultimately show ?thesis using False by (auto simp add: split_beta)
qed
qed

lemma diagonal_to_Smith_i_dvd2:
fixes A::"'a:: {bezout_ring}^'b::mod_type^'c::mod_type"
assumes ib: "is_bezout_ext bezout"
and i_min: "i < min (nrows A) (ncols A)"
and elements_xs_range: "∀x. x ∈ set xs ⟶ x<min (nrows A) (ncols A)"
and dvd_condition: "∀a b. to_nat a ∈ insert i (set xs) ∧ to_nat a = to_nat b ⟶
A $(from_nat c)$ (from_nat c) dvd A $a$ b"
and c_notin: "c ∉ (set xs)"
and c: "c < min (nrows A) (ncols A)"
and distinct: "distinct xs"
and ab: "to_nat a = to_nat b"
and a_in: "to_nat a ∈ insert i (set xs)"
shows "A $(from_nat c)$ (from_nat c) dvd (diagonal_to_Smith_i xs A i bezout) $a$ b"
proof (cases "a = from_nat i")
case True
hence b: "b = from_nat i"
by (metis ab from_nat_to_nat_id i_min min_less_iff_conj nrows_def to_nat_from_nat_id)
show ?thesis by (unfold True b, rule diagonal_to_Smith_i_dvd, insert assms, auto)
next
case False
have ai: "to_nat a ≠ i" using False by auto
hence bi: "to_nat b ≠ i" by (simp add: ab)
have "A $(from_nat c)$ (from_nat c) dvd (diagonal_to_Smith_i xs A i bezout) $from_nat i$ from_nat i"
by (rule diagonal_to_Smith_i_dvd, insert assms, auto)
also have "... dvd (diagonal_to_Smith_i xs A i bezout) $a$ b"
by (rule diagonal_to_Smith_i_dvd_jj, insert assms False ai bi, auto)
finally show ?thesis .
qed

lemma diagonal_to_Smith_i_dvd2_k:
fixes A::"'a::{bezout_ring}^'b::mod_type^'c::mod_type"
assumes ib: "is_bezout_ext bezout"
and i_min: "i < min (nrows A) (ncols A)"
and elements_xs_range: "∀x. x ∈ set xs ⟶ x<k" and "k≤min (nrows A) (ncols A)"
and dvd_condition: "∀a b. to_nat a ∈ insert i (set xs) ∧ to_nat a = to_nat b ⟶
A $(from_nat c)$ (from_nat c) dvd A $a$ b"
and c_notin: "c ∉ (set xs)"
and c: "c < min (nrows A) (ncols A)"
and distinct: "distinct xs"
and ab: "to_nat a = to_nat b"
and a_in: "to_nat a ∈ insert i (set xs)"
shows "A $(from_nat c)$ (from_nat c) dvd (diagonal_to_Smith_i xs A i bezout) $a$ b"
proof (cases "a = from_nat i")
case True
hence b: "b = from_nat i"
by (metis ab from_nat_to_nat_id i_min min_less_iff_conj nrows_def to_nat_from_nat_id)
show ?thesis by (unfold True b, rule diagonal_to_Smith_i_dvd, insert assms, auto)
next
case False
have ai: "to_nat a ≠ i" using False by auto
hence bi: "to_nat b ≠ i" by (simp add: ab)
have "A $(from_nat c)$ (from_nat c) dvd (diagonal_to_Smith_i xs A i bezout) $from_nat i$ from_nat i"
by (rule diagonal_to_Smith_i_dvd, insert assms, auto)
also have "... dvd (diagonal_to_Smith_i xs A i bezout) $a$ b"
by (rule diagonal_to_Smith_i_dvd_jj, insert assms False ai bi, auto)
finally show ?thesis .
qed

lemma diagonal_to_Smith_row_i_preserves_previous:
fixes A::"'a:: {bezout_ring}^'b::mod_type^'c::mod_type"
assumes ib: "is_bezout_ext bezout"
and i_min: "i < min (nrows A) (ncols A)"
and a_not_b: "to_nat a ≠ to_nat b"
shows "Diagonal_to_Smith_row_i A i bezout $a$ b = A $a$ b"
unfolding Diagonal_to_Smith_row_i_def
by (rule diagonal_to_Smith_i_preserves_previous, insert assms, auto)

lemma diagonal_to_Smith_row_i_preserves_previous_diagonal:
fixes A::"'a:: {bezout_ring}^'b::mod_type^'c::mod_type"
assumes ib: "is_bezout_ext bezout"
and i_min: "i < min (nrows A) (ncols A)"
and a_notin: "to_nat a ∉ set [i + 1..<min (nrows A) (ncols A)]"
and ab: "to_nat a = to_nat b"
and ai: "to_nat a ≠ i"
shows "Diagonal_to_Smith_row_i A i bezout $a$ b = A $a$ b"
unfolding Diagonal_to_Smith_row_i_def
by (rule diagonal_to_Smith_i_preserves_previous_diagonal[OF ib i_min a_notin ab ai], auto)

context
fixes bezout::"'a::{bezout_ring} ⇒ 'a ⇒ 'a × 'a × 'a × 'a × 'a"
assumes ib: "is_bezout_ext bezout"
begin

lemma diagonal_to_Smith_row_i_dvd_jj:
fixes A::"'a::{bezout_ring}^'b::mod_type^'c::mod_type"
assumes "to_nat a ∈ {i..<min (nrows A) (ncols A)}"
and "to_nat a = to_nat b"
shows "(Diagonal_to_Smith_row_i A i bezout) $(from_nat i)$ (from_nat i)
dvd (Diagonal_to_Smith_row_i A i bezout) $a$ b"
proof (cases "to_nat a = i")
case True
then show ?thesis
by (metis assms(2) dvd_refl from_nat_to_nat_id)
next
case False
show ?thesis
unfolding Diagonal_to_Smith_row_i_def
by (rule diagonal_to_Smith_i_dvd_jj, insert assms False ib, auto)
qed

lemma diagonal_to_Smith_row_i_dvd_ii:
fixes A::"'a::{bezout_ring}^'b::mod_type^'c::mod_type"
shows "Diagonal_to_Smith_row_i A i bezout $from_nat i$ from_nat i dvd A $from_nat i$ from_nat i"
unfolding Diagonal_to_Smith_row_i_def
by (rule diagonal_to_Smith_i_dvd_ii[OF ib])

lemma diagonal_to_Smith_row_i_dvd_jj':
fixes A::"'a::{bezout_ring}^'b::mod_type^'c::mod_type"
assumes a_in: "to_nat a ∈ {i..<min (nrows A) (ncols A)}"
and ab: "to_nat a = to_nat b"
and ci: "c≤i"
and dvd_condition: "∀a b. to_nat a ∈ (set [i..<min (nrows A) (ncols A)]) ∧ to_nat a = to_nat b
⟶ A $from_nat c$ from_nat c dvd A $a$ b"
shows "(Diagonal_to_Smith_row_i A i bezout) $(from_nat c)$ (from_nat c)
dvd (Diagonal_to_Smith_row_i A i bezout) $a$ b"
proof (cases "c = i")
case True
then show ?thesis using assms True diagonal_to_Smith_row_i_dvd_jj
by metis
next
case False
hence ci2: "c<i" using ci by auto
have 1: "to_nat (from_nat c::'c) ∉ (set [i+1..<min (nrows A) (ncols A)])"
by (metis Suc_eq_plus1 ci atLeastLessThan_iff from_nat_mono
le_imp_less_Suc less_irrefl less_le_trans set_upt to_nat_le to_nat_less_card)
have 2: "to_nat (from_nat c) ≠ i"
using ci2 from_nat_mono to_nat_less_card by fastforce
have 3: "to_nat (from_nat c::'c) = to_nat (from_nat c::'b)"
by (metis a_in ab atLeastLessThan_iff ci dual_order.strict_trans2 to_nat_from_nat_id to_nat_less_card)
have "(Diagonal_to_Smith_row_i A i bezout) $(from_nat c)$ (from_nat c)
= A $(from_nat c)$ (from_nat c)"
unfolding Diagonal_to_Smith_row_i_def
by (rule diagonal_to_Smith_i_preserves_previous_diagonal[OF ib _ 1 3 2], insert assms, auto)
also have "... dvd (Diagonal_to_Smith_row_i A i bezout) $a$ b"
unfolding Diagonal_to_Smith_row_i_def
by (rule diagonal_to_Smith_i_dvd2, insert assms False ci ib, auto)
finally show ?thesis .
qed
end

lemma diagonal_to_Smith_aux_append:
"diagonal_to_Smith_aux A (xs @ ys) bezout
= diagonal_to_Smith_aux (diagonal_to_Smith_aux A xs bezout) ys bezout"
by (induct A xs bezout rule: diagonal_to_Smith_aux.induct, auto)

lemma diagonal_to_Smith_aux_append2[simp]:
"diagonal_to_Smith_aux A (xs @ [ys]) bezout
= Diagonal_to_Smith_row_i (diagonal_to_Smith_aux A xs bezout) ys bezout"
by (induct A xs bezout rule: diagonal_to_Smith_aux.induct, auto)

lemma isDiagonal_eq_upt_k_min:
"isDiagonal A = isDiagonal_upt_k A (min (nrows A) (ncols A))"
unfolding isDiagonal_def isDiagonal_upt_k_def nrows_def ncols_def
by (auto, meson less_trans not_less_iff_gr_or_eq to_nat_less_card)

lemma isDiagonal_eq_upt_k_max:
"isDiagonal A = isDiagonal_upt_k A (max (nrows A) (ncols A))"
unfolding isDiagonal_def isDiagonal_upt_k_def nrows_def ncols_def
by (auto simp add: less_max_iff_disj to_nat_less_card)

lemma isDiagonal:
assumes "isDiagonal A"
and "to_nat a ≠ to_nat b" shows "A $a$ b = 0"
using assms unfolding isDiagonal_def by auto

lemma nrows_diagonal_to_Smith_aux[simp]:
shows "nrows (diagonal_to_Smith_aux A xs bezout) = nrows A" unfolding nrows_def by auto

lemma ncols_diagonal_to_Smith_aux[simp]:
shows "ncols (diagonal_to_Smith_aux A xs bezout) = ncols A" unfolding ncols_def by auto

context
fixes bezout::"'a::{bezout_ring} ⇒ 'a ⇒ 'a × 'a × 'a × 'a × 'a"
assumes ib: "is_bezout_ext bezout"
begin

lemma isDiagonal_diagonal_to_Smith_aux:
assumes diag_A: "isDiagonal A" and k: "k < min (nrows A) (ncols A)"
shows "isDiagonal (diagonal_to_Smith_aux A [0..<k] bezout)"
using k
proof (induct k)
case 0
then show ?case using diag_A by auto
next
case (Suc k)
have "Diagonal_to_Smith_row_i (diagonal_to_Smith_aux A [0..<k] bezout) k bezout $a$ b = 0"
if a_not_b: "to_nat a ≠ to_nat b" for a b
proof -
have "Diagonal_to_Smith_row_i (diagonal_to_Smith_aux A [0..<k] bezout) k bezout $a$ b
= (diagonal_to_Smith_aux A [0..<k] bezout) $a$ b"
by (rule diagonal_to_Smith_row_i_preserves_previous[OF ib _ a_not_b], insert Suc.prems, auto)
also have "... = 0"
by (rule isDiagonal[OF Suc.hyps a_not_b], insert Suc.prems, auto)
finally show ?thesis .
qed
thus ?case unfolding isDiagonal_def by auto
qed
end

(*TODO: move!*)
lemma to_nat_less_nrows[simp]:
fixes A::"'a^'b::mod_type^'c::mod_type"
and a::'c
shows "to_nat a < nrows A"

lemma to_nat_less_ncols[simp]:
fixes A::"'a^'b::mod_type^'c::mod_type"
and a::'b
shows "to_nat a < ncols A"

context
fixes bezout::"'a::{bezout_ring} ⇒ 'a ⇒ 'a × 'a × 'a × 'a × 'a"
assumes ib: "is_bezout_ext bezout"
begin

text‹The variables a and b must be arbitrary in the induction›
lemma diagonal_to_Smith_aux_dvd:
fixes A::"'a::{bezout_ring}^'b::mod_type^'c::mod_type"
assumes ab: "to_nat a = to_nat b"
and c: "c < k" and ca: "c ≤ to_nat a" and k: "k<min (nrows A) (ncols A)"
shows "diagonal_to_Smith_aux A [0..<k] bezout $from_nat c$ from_nat c
dvd diagonal_to_Smith_aux A [0..<k] bezout $a$ b"
using c ab ca k
proof (induct k arbitrary: a b)
case 0
then show ?case by auto
next
case (Suc k)
note c = Suc.prems(1)
note ab = Suc.prems(2)
note ca = Suc.prems(3)
note k = Suc.prems(4)
have k_min: "k < min (nrows A) (ncols A)" using k by auto
have a_less_ncols: "to_nat a < ncols A" using ab by auto
show ?case
proof (cases "c=k")
case True
hence k: "k≤to_nat a" using ca by auto
show ?thesis unfolding True
by (auto, rule diagonal_to_Smith_row_i_dvd_jj[OF ib _ ab], insert k a_less_ncols, auto)
next
case False note c_not_k = False
let ?Dk="diagonal_to_Smith_aux A [0..<k] bezout"
have ck: "c<k" using Suc.prems False by auto
have hyp: "?Dk $from_nat c$ from_nat c dvd ?Dk $a$ b"
by (rule Suc.hyps[OF ck ab ca k_min])
have Dkk_Daa_bb: "?Dk $from_nat c$ from_nat c dvd ?Dk $aa$ bb"
if "to_nat aa ∈ set [k..<min (nrows ?Dk) (ncols ?Dk)]" and "to_nat aa = to_nat bb"
for aa bb using Suc.hyps ck k_min that(1) that(2) by auto
show ?thesis
proof (cases "k≤to_nat a")
case True
show ?thesis
by (auto, rule diagonal_to_Smith_row_i_dvd_jj'[OF ib _ ab])
(insert True a_less_ncols ck Dkk_Daa_bb, force+)
next
case False
have "diagonal_to_Smith_aux A [0..<Suc k] bezout $from_nat c$ from_nat c
= Diagonal_to_Smith_row_i ?Dk k bezout $from_nat c$ from_nat c" by auto
also have "... = ?Dk $from_nat c$ from_nat c"
proof (rule diagonal_to_Smith_row_i_preserves_previous_diagonal[OF ib])
show "k < min (nrows ?Dk) (ncols ?Dk)" using k by auto
show "to_nat (from_nat c::'c) = to_nat (from_nat c::'b)"
by (metis assms(2) assms(4) less_trans min_less_iff_conj
ncols_def nrows_def to_nat_from_nat_id)
show "to_nat (from_nat c::'c) ≠ k"
using False ca from_nat_mono' to_nat_less_card to_nat_mono' by fastforce
show "to_nat (from_nat c::'c) ∉ set [k + 1..<min (nrows ?Dk) (ncols ?Dk)]"
by (metis Suc_eq_plus1 atLeastLessThan_iff c ca from_nat_not_eq
le_less_trans not_le set_upt to_nat_less_card)
qed
also have "... dvd ?Dk $a$ b" using hyp .
also have "... = Diagonal_to_Smith_row_i ?Dk k bezout $a$ b"
by (rule diagonal_to_Smith_row_i_preserves_previous_diagonal[symmetric, OF ib _ _ ab])
(insert False k, auto)
also have "... = diagonal_to_Smith_aux A [0..<Suc k] bezout $a$ b" by auto
finally show ?thesis .
qed
qed
qed

lemma Smith_normal_form_upt_k_Suc_imp_k:
fixes A::"'a::{bezout_ring}^'b::mod_type^'c::mod_type"
assumes s: "Smith_normal_form_upt_k (diagonal_to_Smith_aux A [0..<Suc k] bezout) k"
and k: "k<min (nrows A) (ncols A)"
shows "Smith_normal_form_upt_k (diagonal_to_Smith_aux A [0..<k] bezout) k"
proof (rule Smith_normal_form_upt_k_intro)
let ?Dk="diagonal_to_Smith_aux A [0..<k] bezout"
fix a::'c and b::'b assume "to_nat a = to_nat b ∧ to_nat a + 1 < k ∧ to_nat b + 1 < k"
hence ab: "to_nat a = to_nat b" and ak: "to_nat a + 1 < k" and bk: "to_nat b + 1 < k" by auto
have a_not_k: "to_nat a ≠ k" using ak by auto
have a1_less_k1: "to_nat a + 1 < k + 1" using ak by linarith
have "?Dk $a$ b = diagonal_to_Smith_aux A [0..<Suc k] bezout $a$ b"
by (auto, rule diagonal_to_Smith_row_i_preserves_previous_diagonal[symmetric, OF ib _ _ ab a_not_k])
(insert ak k, auto)
also have "... dvd diagonal_to_Smith_aux A [0..<Suc k] bezout $(a + 1)$ (b + 1)"
using ab ak bk s unfolding Smith_normal_form_upt_k_def by auto
also have "... = ?Dk $(a+1)$ (b+1)"
proof (auto, rule diagonal_to_Smith_row_i_preserves_previous_diagonal[OF ib])
show "to_nat (a + 1) ≠ k" using ak
to_nat_plus_one_less_card' to_nat_suc)
show "to_nat (a + 1) = to_nat (b + 1)"
by (metis ab ak from_nat_suc from_nat_to_nat_id k less_asym' min_less_iff_conj
ncols_def nrows_def suc_not_zero to_nat_from_nat_id to_nat_plus_one_less_card')
show "to_nat (a + 1) ∉ set [k + 1..<min (nrows ?Dk) (ncols ?Dk)]"
by (metis a1_less_k1 add_to_nat_def atLeastLessThan_iff k less_asym' min.strict_boundedE
not_less nrows_def set_upt suc_not_zero to_nat_1 to_nat_from_nat_id to_nat_plus_one_less_card')
show "k < min (nrows ?Dk) (ncols ?Dk)" using k by auto
qed
finally show "?Dk $a$ b dvd ?Dk $(a+1)$ (b+1)" .
next
let ?Dk="diagonal_to_Smith_aux A [0..<k] bezout"
fix a::'c and b::'b
assume "to_nat a ≠ to_nat b ∧ (to_nat a < k ∨ to_nat b < k)"
hence ab: "to_nat a ≠ to_nat b" and ak_bk: "(to_nat a < k ∨ to_nat b < k)" by auto
have "?Dk $a$ b = diagonal_to_Smith_aux A [0..<Suc k] bezout $a$ b"
by (auto, rule diagonal_to_Smith_row_i_preserves_previous[symmetric, OF ib _ ab], insert k, auto)
also have "... = 0"
using ab ak_bk s unfolding Smith_normal_form_upt_k_def isDiagonal_upt_k_def
by auto
finally show "?Dk $a$ b = 0" .
qed

lemma Smith_normal_form_upt_k_le:
assumes "a≤k" and "Smith_normal_form_upt_k A k"
shows "Smith_normal_form_upt_k A a" using assms
by (smt Smith_normal_form_upt_k_def isDiagonal_upt_k_def less_le_trans)

lemma Smith_normal_form_upt_k_imp_Suc_k:
assumes s: "Smith_normal_form_upt_k (diagonal_to_Smith_aux A [0..<k] bezout) k"
and k: "k<min (nrows A) (ncols A)"
shows "Smith_normal_form_upt_k (diagonal_to_Smith_aux A [0..<Suc k] bezout) k"
proof (rule Smith_normal_form_upt_k_intro)
let ?Dk="diagonal_to_Smith_aux A [0..<k] bezout"
fix a::'c and b::'b assume "to_nat a = to_nat b ∧ to_nat a + 1 < k ∧ to_nat b + 1 < k"
hence ab: "to_nat a = to_nat b" and ak: "to_nat a + 1 < k" and bk: "to_nat b + 1 < k" by auto
have a_not_k: "to_nat a ≠ k" using ak by auto
have a1_less_k1: "to_nat a + 1 < k + 1" using ak by linarith
have "diagonal_to_Smith_aux A [0..<Suc k] bezout $a$ b = ?Dk $a$ b"
by (auto, rule diagonal_to_Smith_row_i_preserves_previous_diagonal[OF ib _ _ ab a_not_k])
(insert ak k, auto)
also have "... dvd ?Dk $(a+1)$ (b+1)"
using s ak k ab unfolding Smith_normal_form_upt_k_def by auto
also have "... = diagonal_to_Smith_aux A [0..<Suc k] bezout $(a + 1)$ (b + 1)"
proof (auto, rule diagonal_to_Smith_row_i_preserves_previous_diagonal[symmetric, OF ib])
show "to_nat (a + 1) ≠ k" using ak
to_nat_plus_one_less_card' to_nat_suc)
show "to_nat (a + 1) = to_nat (b + 1)"
by (metis ab ak from_nat_suc from_nat_to_nat_id k less_asym' min_less_iff_conj
ncols_def nrows_def suc_not_zero to_nat_from_nat_id to_nat_plus_one_less_card')
show "to_nat (a + 1) ∉ set [k + 1..<min (nrows ?Dk) (ncols ?Dk)]"
by (metis a1_less_k1 add_to_nat_def to_nat_plus_one_less_card' less_asym' min.strict_boundedE
not_less nrows_def set_upt suc_not_zero to_nat_1 to_nat_from_nat_id atLeastLessThan_iff k)
show "k < min (nrows ?Dk) (ncols ?Dk)" using k by auto
qed
finally show "diagonal_to_Smith_aux A [0..<Suc k] bezout $a$ b
dvd diagonal_to_Smith_aux A [0..<Suc k] bezout $(a + 1)$ (b + 1)" .
next
let ?Dk="diagonal_to_Smith_aux A [0..<k] bezout"
fix a::'c and b::'b
assume "to_nat a ≠ to_nat b ∧ (to_nat a < k ∨ to_nat b < k)"
hence ab: "to_nat a ≠ to_nat b" and ak_bk: "(to_nat a < k ∨ to_nat b < k)" by auto
have "diagonal_to_Smith_aux A [0..<Suc k] bezout $a$ b = ?Dk $a$ b"
by (auto, rule diagonal_to_Smith_row_i_preserves_previous[OF ib _ ab], insert k, auto)
also have "... = 0"
using ab ak_bk s unfolding Smith_normal_form_upt_k_def isDiagonal_upt_k_def
by auto
finally show "diagonal_to_Smith_aux A [0..<Suc k] bezout $a$ b = 0" .
qed

corollary Smith_normal_form_upt_k_Suc_eq:
assumes k: "k<min (nrows A) (ncols A)"
shows "Smith_normal_form_upt_k (diagonal_to_Smith_aux A [0..<Suc k] bezout) k
= Smith_normal_form_upt_k (diagonal_to_Smith_aux A [0..<k] bezout) k"
using Smith_normal_form_upt_k_Suc_imp_k Smith_normal_form_upt_k_imp_Suc_k k
by blast

end

lemma nrows_diagonal_to_Smith_i[simp]: "nrows (diagonal_to_Smith_i xs A i bezout) = nrows A"
by (induct xs A i bezout rule: diagonal_to_Smith_i.induct, auto simp add: nrows_def)

lemma ncols_diagonal_to_Smith_i[simp]: "ncols (diagonal_to_Smith_i xs A i bezout) = ncols A"
by (induct xs A i bezout rule: diagonal_to_Smith_i.induct, auto simp add: ncols_def)

lemma nrows_Diagonal_to_Smith_row_i[simp]: "nrows (Diagonal_to_Smith_row_i A i bezout) = nrows A"
unfolding Diagonal_to_Smith_row_i_def by auto

lemma ncols_Diagonal_to_Smith_row_i[simp]: "ncols (Diagonal_to_Smith_row_i A i bezout) = ncols A"
unfolding Diagonal_to_Smith_row_i_def by auto

lemma isDiagonal_diagonal_step:
assumes diag_A: "isDiagonal A" and i: "i<min (nrows A) (ncols A)"
and j: "j<min (nrows A) (ncols A)"
shows "isDiagonal (diagonal_step A i j d v)"
proof -
have i_eq: "to_nat (from_nat i::'b) = to_nat (from_nat i::'c)" using i
by (simp add: ncols_def nrows_def to_nat_from_nat_id)
moreover have j_eq: "to_nat (from_nat j::'b) = to_nat (from_nat j::'c)" using j
by (simp add: ncols_def nrows_def to_nat_from_nat_id)
ultimately show ?thesis
using assms
unfolding isDiagonal_def diagonal_step_def by auto
qed

lemma isDiagonal_diagonal_to_Smith_i:
assumes "isDiagonal A"
and elements_xs_range: "∀x. x ∈ set xs ⟶ x<min (nrows A) (ncols A)"
and "i<min (nrows A) (ncols A)"
shows "isDiagonal (diagonal_to_Smith_i xs A i bezout)"
using assms
proof (induct xs A i bezout rule: diagonal_to_Smith_i.induct)
case (1 A i bezout)
then show ?case by auto
next
case (2 j xs A i bezout)
let ?Aii = "A $from_nat i$ from_nat i"
let ?Ajj = "A $from_nat j$ from_nat j"
let ?p="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ p"
let ?q="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ q"
let ?u="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ u"
let ?v="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ v"
let ?d="case bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ d"
let ?A'="diagonal_step A i j ?d ?v"
have pquvd: "(?p, ?q, ?u, ?v,?d) = bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j)"
show ?case
proof (cases "?Aii dvd ?Ajj")
case True
thus ?thesis
using "2.hyps" "2.prems" by auto
next
case False
have "diagonal_to_Smith_i (j # xs) A i bezout = diagonal_to_Smith_i xs ?A' i bezout"
using False by (simp add: split_beta)
also have "isDiagonal ..." thm "2.prems"
proof (rule "2.hyps"(2)[OF False])
show "isDiagonal
(diagonal_step A i j ?d ?v)" by (rule isDiagonal_diagonal_step, insert "2.prems", auto)
qed (insert pquvd "2.prems", auto)
finally show ?thesis .
qed
qed

lemma isDiagonal_Diagonal_to_Smith_row_i:
assumes "isDiagonal A" and "i < min (nrows A) (ncols A)"
shows "isDiagonal (Diagonal_to_Smith_row_i A i bezout)"
using assms isDiagonal_diagonal_to_Smith_i
unfolding Diagonal_to_Smith_row_i_def by force

lemma isDiagonal_diagonal_to_Smith_aux_general:
assumes elements_xs_range: "∀x. x ∈ set xs ⟶ x<min (nrows A) (ncols A)"
and "isDiagonal A"
shows "isDiagonal (diagonal_to_Smith_aux A xs bezout)"
using assms
proof (induct A xs bezout rule: diagonal_to_Smith_aux.induct)
case (1 A)
then show ?case by auto
next
case (2 A i xs bezout)
note k = "2.prems"(1)
note elements_xs_range = "2.prems"(2)
have "diagonal_to_Smith_aux A (i # xs) bezout
= diagonal_to_Smith_aux (Diagonal_to_Smith_row_i A i bezout) xs bezout"
by auto
also have "isDiagonal (...)"
by (rule "2.hyps", insert isDiagonal_Diagonal_to_Smith_row_i "2.prems" k, auto)
finally show ?case .
qed

context
fixes bezout::"'a::{bezout_ring} ⇒ 'a ⇒ 'a × 'a × 'a × 'a × 'a"
assumes ib: "is_bezout_ext bezout"
begin

text‹The algorithm is iterated up to position k (not included). Thus, the matrix
is in Smith normal form up to position k (not included).›

lemma Smith_normal_form_upt_k_diagonal_to_Smith_aux:
fixes A::"'a::{bezout_ring}^'b::mod_type^'c::mod_type"
assumes "k<min (nrows A) (ncols A)" and d: "isDiagonal A"
shows "Smith_normal_form_upt_k (diagonal_to_Smith_aux A [0..<k] bezout) k"
using assms
proof (induct k)
case 0
then show ?case by auto
next
case (Suc k)
note Suc_k = "Suc.prems"(1)
have hyp: "Smith_normal_form_upt_k (diagonal_to_Smith_aux A [0..<k] bezout) k"
by (rule Suc.hyps, insert Suc.prems, simp)
have k: "k < min (nrows A) (ncols A)" using Suc.prems by auto
let ?A = "diagonal_to_Smith_aux A [0..<k] bezout"
let ?D_Suck = "diagonal_to_Smith_aux A [0..<Suc k] bezout"
have set_rw: "[0..<Suc k] = [0..<k] @ [k]" by auto
show ?case
proof (rule Smith_normal_form_upt_k1_intro_diagonal)
show "Smith_normal_form_upt_k (?D_Suck) k"
by (rule Smith_normal_form_upt_k_imp_Suc_k[OF ib hyp k])
show "?D_Suck $from_nat (k - 1)$ from_nat (k - 1) dvd ?D_Suck $from_nat k$ from_nat k"
proof (rule diagonal_to_Smith_aux_dvd[OF ib _ _ _ Suc_k])
show "to_nat (from_nat k::'c) = to_nat (from_nat k::'b)"
by (metis k min_less_iff_conj ncols_def nrows_def to_nat_from_nat_id)
show "k - 1 ≤ to_nat (from_nat k::'c)"
by (metis diff_le_self k min_less_iff_conj nrows_def to_nat_from_nat_id)
qed auto
show "isDiagonal (diagonal_to_Smith_aux A [0..<Suc k] bezout)"
by (rule isDiagonal_diagonal_to_Smith_aux[OF ib d Suc_k])
qed
qed

end

lemma nrows_diagonal_to_Smith[simp]: "nrows (diagonal_to_Smith A bezout) = nrows A"
unfolding diagonal_to_Smith_def by auto

lemma ncols_diagonal_to_Smith[simp]: "ncols (diagonal_to_Smith A bezout) = ncols A"
unfolding diagonal_to_Smith_def by auto

lemma isDiagonal_diagonal_to_Smith:
assumes d: "isDiagonal A"
shows "isDiagonal (diagonal_to_Smith A bezout)"
unfolding diagonal_to_Smith_def
by (rule isDiagonal_diagonal_to_Smith_aux_general[OF _ d], auto)

text‹This is the soundess lemma.›

lemma Smith_normal_form_diagonal_to_Smith:
fixes A::"'a::{bezout_ring}^'b::mod_type^'c::mod_type"
assumes ib: "is_bezout_ext bezout"
and d: "isDiagonal A"
shows "Smith_normal_form (diagonal_to_Smith A bezout)"
proof -
let ?k = "min (nrows A) (ncols A) - 2"
let ?Dk = "(diagonal_to_Smith_aux A [0..<?k] bezout)"
have min_eq: "min (nrows A) (ncols A) - 1 = Suc ?k"
by (metis Suc_1 Suc_diff_Suc min_less_iff_conj ncols_def nrows_def to_nat_1 to_nat_less_card)
have set_rw: "[0..<min (nrows A) (ncols A) - 1] = [0..<?k] @ [?k]"
unfolding min_eq by auto
have d2: "isDiagonal (diagonal_to_Smith A bezout)"
by (rule isDiagonal_diagonal_to_Smith[OF d])
have smith_Suc_k: "Smith_normal_form_upt_k (diagonal_to_Smith A bezout) (Suc ?k)"
proof (rule Smith_normal_form_upt_k1_intro_diagonal[OF _ d2])
have "diagonal_to_Smith A bezout = diagonal_to_Smith_aux A [0..<min (nrows A) (ncols A) - 1] bezout"
unfolding diagonal_to_Smith_def by auto
also have "... = Diagonal_to_Smith_row_i ?Dk ?k bezout"
unfolding set_rw
unfolding diagonal_to_Smith_aux_append2 by auto
finally have d_rw: "diagonal_to_Smith A bezout = Diagonal_to_Smith_row_i ?Dk ?k bezout" .
have "Smith_normal_form_upt_k ?Dk ?k"
by (rule Smith_normal_form_upt_k_diagonal_to_Smith_aux[OF ib _ d], insert min_eq, linarith)
thus "Smith_normal_form_upt_k (diagonal_to_Smith A bezout) ?k" unfolding d_rw
by (metis Smith_normal_form_upt_k_Suc_eq Suc_1 ib d_rw diagonal_to_Smith_def diff_0_eq_0
diff_less min_eq not_gr_zero zero_less_Suc)
show "diagonal_to_Smith A bezout $from_nat (?k - 1)$ from_nat (?k - 1) dvd
diagonal_to_Smith A bezout $from_nat ?k$ from_nat ?k"
proof (unfold diagonal_to_Smith_def, rule diagonal_to_Smith_aux_dvd[OF ib])
show "?k - 1 < min (nrows A) (ncols A) - 1"
using min_eq by linarith
show "min (nrows A) (ncols A) - 1 < min (nrows A) (ncols A)" using min_eq by linarith
thus "to_nat (from_nat ?k::'c) = to_nat (from_nat ?k::'b)"
by (metis (mono_tags, lifting) Suc_lessD min_eq min_less_iff_conj
ncols_def nrows_def to_nat_from_nat_id)
show "?k - 1 ≤ to_nat (from_nat ?k::'c)"
by (metis (no_types, lifting) diff_le_self from_nat_not_eq lessI less_le_trans
min.cobounded1 min_eq nrows_def)
qed
qed
have s_eq: "Smith_normal_form (diagonal_to_Smith A bezout)
= Smith_normal_form_upt_k (diagonal_to_Smith A bezout)
(Suc (min (nrows (diagonal_to_Smith A bezout)) (ncols (diagonal_to_Smith A bezout)) - 1))"
unfolding Smith_normal_form_min by (simp add: ncols_def nrows_def)
let ?min1="(min (nrows (diagonal_to_Smith A bezout)) (ncols (diagonal_to_Smith A bezout)) - 1)"
show ?thesis unfolding s_eq
proof (rule Smith_normal_form_upt_k1_intro_diagonal[OF _ d2])
show "Smith_normal_form_upt_k (diagonal_to_Smith A bezout) ?min1"
using smith_Suc_k min_eq by auto
have "diagonal_to_Smith A bezout $from_nat ?k$ from_nat ?k
dvd diagonal_to_Smith A bezout $from_nat (?k + 1)$ from_nat (?k + 1)"
by (smt One_nat_def Suc_eq_plus1 ib Suc_pred diagonal_to_Smith_aux_dvd diagonal_to_Smith_def
le_add1 lessI min_eq min_less_iff_conj ncols_def nrows_def to_nat_from_nat_id zero_less_card_finite)
thus "diagonal_to_Smith A bezout $from_nat (?min1 - 1)$ from_nat (?min1 - 1)
dvd diagonal_to_Smith A bezout $from_nat ?min1$ from_nat ?min1"
using min_eq by auto
qed
qed

subsection‹Implementation and formal proof
of the matrices $P$ and $Q$ which transform the input matrix by means of elementary operations.›

fun diagonal_step_PQ :: "'a::{bezout_ring}^'cols::mod_type^'rows::mod_type ⇒ nat ⇒ nat ⇒ 'a bezout ⇒
(
('a::{bezout_ring}^'rows::mod_type^'rows::mod_type) ×
('a::{bezout_ring}^'cols::mod_type^'cols::mod_type)
)"
where "diagonal_step_PQ A i k bezout =
(let  i_row = from_nat i; k_row = from_nat k; i_col = from_nat i; k_col = from_nat k;
(p, q, u, v, d) = bezout (A $i_row$ from_nat i) (A $k_row$ from_nat k);
P = row_add (interchange_rows (row_add (mat 1) k_row i_row p) i_row k_row) k_row i_row (-v);
Q = mult_column (column_add (column_add (mat 1) i_col k_col q) k_col i_col u) k_col (-1)
in (P,Q)
)"

text‹Examples›

value "let A = list_of_list_to_matrix [[12,0,0::int],[0,6,0::int],[0,0,2::int]]::int^3^3;
i=0; k=1;
(p, q, u, v, d) = euclid_ext2 (A $from_nat i$ from_nat i) (A $from_nat k$ from_nat k);
(P,Q) = diagonal_step_PQ A i k euclid_ext2
in matrix_to_list_of_list (diagonal_step A i k d v)"

value "let A = list_of_list_to_matrix [[12,0,0::int],[0,6,0::int],[0,0,2::int]]::int^3^3;
i=0; k=1;
(p, q, u, v, d) = euclid_ext2 (A $from_nat i$ from_nat i) (A $from_nat k$ from_nat k);
(P,Q) = diagonal_step_PQ A i k euclid_ext2
in matrix_to_list_of_list (P**(A)**Q)"

value "let A = list_of_list_to_matrix [[12,0,0::int],[0,6,0::int],[0,0,2::int]]::int^3^3;
i=0; k=1;
(p, q, u, v, d) = euclid_ext2 (A $from_nat i$ from_nat i) (A $from_nat k$ from_nat k);
(P,Q) = diagonal_step_PQ A i k euclid_ext2
in matrix_to_list_of_list (P**(A)**Q)"

lemmas diagonal_step_PQ_def = diagonal_step_PQ.simps

lemma from_nat_neq_rows:
fixes A::"'a^'cols::mod_type^'rows::mod_type"
assumes i: "i<(nrows A)" and k: "k<(nrows A)" and ik: "i ≠ k"
shows "from_nat i ≠ (from_nat k::'rows)"
proof (rule ccontr, auto)
let ?i="from_nat i::'rows"
let ?k="from_nat k::'rows"
assume "?i = ?k"
hence "to_nat ?i = to_nat ?k" by auto
hence "i = k"
unfolding to_nat_from_nat_id[OF i[unfolded nrows_def]]
unfolding to_nat_from_nat_id[OF k[unfolded nrows_def]] .
thus False using ik by contradiction
qed

lemma from_nat_neq_cols:
fixes A::"'a^'cols::mod_type^'rows::mod_type"
assumes i: "i<(ncols A)" and k: "k<(ncols A)" and ik: "i ≠ k"
shows "from_nat i ≠ (from_nat k::'cols)"
proof (rule ccontr, auto)
let ?i="from_nat i::'cols"
let ?k="from_nat k::'cols"
assume "?i = ?k"
hence "to_nat ?i = to_nat ?k" by auto
hence "i = k"
unfolding to_nat_from_nat_id[OF i[unfolded ncols_def]]
unfolding to_nat_from_nat_id[OF k[unfolded ncols_def]] .
thus False using ik by contradiction
qed

lemma diagonal_step_PQ_invertible_P:
fixes A::"'a::{bezout_ring}^'cols::mod_type^'rows::mod_type"
assumes PQ: "(P,Q) = diagonal_step_PQ A i k bezout"
and pquvd: "(p,q,u,v,d) = bezout (A $from_nat i$ from_nat i) (A $from_nat k$ from_nat k)"
and i_not_k: "i ≠ k"
and i: "i<min (nrows A) (ncols A)" and k: "k<min (nrows A) (ncols A)"
shows "invertible P"
proof -
let ?step1 = "(row_add (mat 1) (from_nat k::'rows) (from_nat i) p)"
let ?step2 = "interchange_rows ?step1 (from_nat i) (from_nat k)"
let ?step3 = "row_add (?step2) (from_nat k) (from_nat i) (- v)"
have p: "p = fst (bezout (A $from_nat i$ from_nat i) (A $from_nat k$ from_nat k))"
using pquvd by (metis fst_conv)
have v: "-v = (- fst (snd (snd (snd (bezout (A $from_nat i$ from_nat i) (A $from_nat k$ from_nat k))))))"
using pquvd by (metis fst_conv snd_conv)
have i_not_k2: "from_nat k ≠ (from_nat i::'rows)"
by (rule from_nat_neq_rows, insert i k i_not_k, auto)
have "invertible ?step3"
unfolding row_add_mat_1[of _ _ _ ?step2, symmetric]
proof (rule invertible_mult)
show "invertible (row_add (mat 1) (from_nat k::'rows) (from_nat i) (- v))"
show "invertible ?step2"
by (metis i_not_k2 interchange_rows_mat_1 invertible_interchange_rows
qed
thus ?thesis
using PQ p v unfolding diagonal_step_PQ_def Let_def split_beta
by auto
qed

lemma diagonal_step_PQ_invertible_Q:
fixes A::"'a::{bezout_ring}^'cols::mod_type^'rows::mod_type"
assumes PQ: "(P,Q) = diagonal_step_PQ A i k bezout"
and pquvd: "(p,q,u,v,d) = bezout (A $from_nat i$ from_nat i) (A $from_nat k$ from_nat k)"
and i_not_k: "i ≠ k"
and i: "i<min (nrows A) (ncols A)" and k: "k<min (nrows A) (ncols A)"
shows "invertible Q"
proof -
let ?step1 = "column_add (mat 1) (from_nat i::'cols) (from_nat k) q"
let ?step2 = "column_add ?step1 (from_nat k) (from_nat i) u"
let ?step3 = "mult_column ?step2 (from_nat k) (- 1)"
have u: "u = (fst (snd (snd (bezout (A $from_nat i$ from_nat i) (A $from_nat k$ from_nat k)))))"
by (metis fst_conv pquvd snd_conv)
have q: "q = (fst (snd (bezout (A $from_nat i$ from_nat i) (A $from_nat k$ from_nat k))))"
by (metis fst_conv pquvd snd_conv)
have "invertible ?step3"
unfolding column_add_mat_1[of _ _ _ ?step2, symmetric]
unfolding mult_column_mat_1[of  ?step2, symmetric]
proof (rule invertible_mult)
show "invertible (mult_column (mat 1) (from_nat k::'cols) (- 1::'a))"
by (rule invertible_mult_column[of _ "-1"], auto)
show "invertible ?step2"
min_less_iff_conj ncols_def to_nat_from_nat_id)
qed
thus ?thesis
using PQ pquvd u q unfolding diagonal_step_PQ_def
by (auto simp add: Let_def split_beta)
qed

lemma mat_q_1[simp]: "mat q $a$ a = q" unfolding mat_def by auto

lemma mat_q_0[simp]:
assumes ab: "a ≠ b"
shows "mat q $a$ b = 0" using ab unfolding mat_def by auto

text‹This is an alternative definition for the matrix P in each step, where entries are
given explicitly instead of being computed as a composition of elementary operations. ›

lemma diagonal_step_PQ_P_alt:
fixes A::"'a::{bezout_ring}^'cols::mod_type^'rows::mod_type"
assumes PQ: "(P,Q) = diagonal_step_PQ A i k bezout"
and pquvd: "(p,q,u,v,d) = bezout (A $from_nat i$ from_nat i) (A $from_nat k$ from_nat k)"
and i: "i<min (nrows A) (ncols A)" and k: "k<min (nrows A) (ncols A)" and ik: "i ≠ k"
shows "
P = (χ a b.
if a = from_nat i ∧ b = from_nat i then p else
if a = from_nat i ∧ b = from_nat k then 1 else
if a = from_nat k ∧ b = from_nat i then -v * p + 1 else
if a = from_nat k ∧ b = from_nat k then -v else
if a = b then 1 else 0)"
proof -
have ik1: "from_nat i ≠ (from_nat k::'rows)"
using from_nat_neq_rows i ik k by auto
have "P $a$ b =
(if a = from_nat i ∧ b = from_nat i then p
else if a = from_nat i ∧ b = from_nat k then 1
else if a = from_nat k ∧ b = from_nat i then - v * p + 1
else if a = from_nat k ∧ b = from_nat k then - v else if a = b then 1 else 0)"
for a b
using PQ ik1  pquvd
unfolding diagonal_step_PQ_def
by (auto simp add: Let_def split_beta)
(metis (mono_tags, hide_lams) fst_conv snd_conv)+
thus ?thesis unfolding vec_eq_iff unfolding vec_lambda_beta by auto
qed

text‹This is an alternative definition for the matrix Q in each step, where entries are
given explicitly instead of being computed as a composition of elementary operations.›

lemma diagonal_step_PQ_Q_alt:
fixes A::"'a::{bezout_ring}^'cols::mod_type^'rows::mod_type"
assumes PQ: "(P,Q) = diagonal_step_PQ A i k bezout"
and pquvd: "(p,q,u,v,d) = bezout (A $from_nat i$ from_nat i) (A $from_nat k$ from_nat k)"
and i: "i<min (nrows A) (ncols A)" and k: "k<min (nrows A) (ncols A)" and ik: "i ≠ k"
shows "
Q = (χ a b.
if a = from_nat i ∧ b = from_nat i then 1 else
if a = from_nat i ∧ b = from_nat k then -u else
if a = from_nat k ∧ b = from_nat i then q else
if a = from_nat k ∧ b = from_nat k then -q*u-1 else
if a = b then 1 else 0)"
proof -
have ik1: "from_nat i ≠ (from_nat k::'cols)"
using from_nat_neq_cols i ik k by auto
have "Q $a$ b =
(if a = from_nat i ∧ b = from_nat i then 1 else
if a = from_nat i ∧ b = from_nat k then -u else
if a = from_nat k ∧ b = from_nat i then q else
if a = from_nat k ∧ b = from_nat k then -q*u-1 else
if a = b then 1 else 0)"  for a b
using PQ ik1 pquvd unfolding diagonal_step_PQ_def
by (auto simp add: Let_def split_beta)
(metis (mono_tags, hide_lams) fst_conv snd_conv)+
thus ?thesis unfolding vec_eq_iff unfolding vec_lambda_beta by auto
qed

text‹P**A can be rewriten as elementary operations over A.›

lemma diagonal_step_PQ_PA:
fixes A::"'a::{bezout_ring}^'cols::mod_type^'rows::mod_type"
assumes PQ: "(P,Q) = diagonal_step_PQ A i k bezout"
and b: "(p,q,u,v,d) = bezout (A $from_nat i$ from_nat i) (A $from_nat k$ from_nat k)"
(row_add A (from_nat k) (from_nat i) p) (from_nat i) (from_nat k)) (from_nat k) (from_nat i) (- v)"
proof -
let ?i_row = "from_nat i::'rows" and ?k_row = "from_nat k::'rows"
let ?P1 = "row_add (mat 1) ?k_row ?i_row p"
let ?P2' = "interchange_rows ?P1 ?i_row ?k_row"
let ?P2 = "interchange_rows (mat 1) (from_nat i) (from_nat k)"
let ?P3 = "row_add (mat 1) (from_nat k) (from_nat i) (- v)"
have "P = row_add ?P2' ?k_row ?i_row (- v)"
using PQ b unfolding diagonal_step_PQ_def
by (auto simp add: Let_def split_beta, metis fstI sndI)
also have "... = ?P3 ** ?P2'"
unfolding row_add_mat_1[of _ _ _ ?P2', symmetric] by auto
also have "... = ?P3 ** (?P2 ** ?P1)"
unfolding interchange_rows_mat_1[of _ _ ?P1, symmetric] by auto
also have "... ** A = row_add (interchange_rows
(row_add A (from_nat k) (from_nat i) p) (from_nat i) (from_nat k)) (from_nat k) (from_nat i) (- v)"
finally show ?thesis .
qed

lemma diagonal_step_PQ_PAQ':
fixes A::"'a::{bezout_ring}^'cols::mod_type^'rows::mod_type"
assumes PQ: "(P,Q) = diagonal_step_PQ A i k bezout"
and b: "(p,q,u,v,d) = bezout (A $from_nat i$ from_nat i) (A $from_nat k$ from_nat k)"
shows "P**A**Q = (mult_column (column_add (column_add (P**A) (from_nat i) (from_nat k) q)
(from_nat k) (from_nat i) u) (from_nat k) (- 1))"
proof -
let ?i_col = "from_nat i::'cols" and ?k_col = "from_nat k::'cols"
let ?Q1="(column_add (mat 1) ?i_col ?k_col q)"
let ?Q2' = "(column_add ?Q1 ?k_col ?i_col u)"
let ?Q2 = "column_add (mat 1) (from_nat k) (from_nat i) u"
let ?Q3 = "mult_column (mat 1) (from_nat k) (- 1)"
have "Q = mult_column ?Q2' ?k_col (-1)"
using PQ b unfolding diagonal_step_PQ_def
by (auto simp add: Let_def split_beta, metis fstI sndI)
also have "... = ?Q2' ** ?Q3"
unfolding mult_column_mat_1[of ?Q2', symmetric] by auto
also have "... = (?Q1**?Q2)**?Q3"
unfolding column_add_mat_1[of ?Q1, symmetric] by auto
also have " (P**A) **  ((?Q1**?Q2)**?Q3) =
(mult_column (column_add (column_add (P**A) ?i_col ?k_col q) ?k_col ?i_col u) ?k_col (- 1))"
by (metis (no_types, lifting) column_add_mat_1 matrix_mul_assoc mult_column_mat_1)
finally show ?thesis .
qed

corollary diagonal_step_PQ_PAQ:
fixes A::"'a::{bezout_ring}^'cols::mod_type^'rows::mod_type"
assumes PQ: "(P,Q) = diagonal_step_PQ A i k bezout"
and b: "(p,q,u,v,d) = bezout (A $from_nat i$ from_nat i) (A $from_nat k$ from_nat k)"
(row_add A (from_nat k) (from_nat i) p) (from_nat i)
(from_nat k)) (from_nat k) (from_nat i) (- v)) (from_nat i) (from_nat k) q)
(from_nat k) (from_nat i) u) (from_nat k) (- 1))"
using diagonal_step_PQ_PA diagonal_step_PQ_PAQ' assms by metis

lemma isDiagonal_imp_0:
assumes "isDiagonal A"
and "from_nat a ≠ from_nat b"
and "a < min (nrows A) (ncols A)"
and "b < min (nrows A) (ncols A)"
shows "A $from_nat a$ from_nat b = 0"
by (metis assms isDiagonal min.strict_boundedE ncols_def nrows_def to_nat_from_nat_id)

lemma diagonal_step_PQ:
fixes A::"'a::{bezout_ring}^'cols::mod_type^'rows::mod_type"
assumes PQ: "(P,Q) = diagonal_step_PQ A i k bezout"
and b: "(p,q,u,v,d) = bezout (A $from_nat i$ from_nat i) (A $from_nat k$ from_nat k)"
and i: "i<min (nrows A) (ncols A)" and k: "k<min (nrows A) (ncols A)" and ik: "i ≠ k"
and ib: "is_bezout_ext bezout" and diag: "isDiagonal A"
shows "diagonal_step A i k d v = P**A**Q"
proof -
let ?i_row = "from_nat i::'rows"
and ?k_row = "from_nat k::'rows" and ?i_col = "from_nat i::'cols" and ?k_col = "from_nat k::'cols"
let ?P1 = "(row_add (mat 1) ?k_row ?i_row p)"
let ?Aii = "A $?i_row$ ?i_col"
let ?Akk = "A $?k_row$ ?k_col"
have k1: "k<ncols A" and k2: "k<nrows A" and i1: "i<nrows A" and i2: "i<ncols A" using i k by auto
have Aik0: "A $?i_row$ ?k_col = 0"
by (metis diag i ik isDiagonal k min.strict_boundedE ncols_def nrows_def to_nat_from_nat_id)
have Aki0: "A $?k_row$ ?i_col = 0"
by (metis diag i ik isDiagonal k min.strict_boundedE ncols_def nrows_def to_nat_from_nat_id)
have du: "d * u = - A $?k_row$ ?k_col"
using b ib unfolding is_bezout_ext_def
by (auto simp add: split_beta) (metis fst_conv snd_conv)
have dv: "d * v = A $?i_row$ ?i_col"
using b ib unfolding is_bezout_ext_def
by (auto simp add: split_beta) (metis fst_conv snd_conv)
have d: "d = p * ?Aii + ?Akk * q"
using b ib unfolding is_bezout_ext_def
by (auto simp add: split_beta) (metis fst_conv mult.commute snd_conv)
have "(?Aii - v * (p * ?Aii) - v * ?Akk * q) * u = (?Aii - v * ((p * ?Aii) + ?Akk * q)) * u"
also have "... = (?Aii*u - d* v *u)"
by (simp add: mult.commute right_diff_distrib d)
also have "... = 0" by (simp add: dv)
finally have rw: "(?Aii - v * (p * ?Aii) - v * ?Akk * q) * u = 0" .
have a1: "from_nat k ≠ (from_nat i::'rows)"
using from_nat_neq_rows i ik k by auto
have a2: "from_nat k ≠ (from_nat i::'cols)"
using from_nat_neq_cols i ik k by auto
have Aab0: "A $a$ from_nat b = 0" if ab: "a ≠ from_nat b" and b_ncols: "b < ncols A" for a b
by (metis ab b_ncols diag from_nat_to_nat_id isDiagonal ncols_def to_nat_from_nat_id)
have Aab0': "A $from_nat a$ b = 0" if ab: "from_nat a ≠ b" and a_nrows: "a < nrows A" for a b
by (metis ab a_nrows diag from_nat_to_nat_id isDiagonal nrows_def to_nat_from_nat_id)
show ?thesis
proof (unfold diagonal_step_def vec_eq_iff, auto)
show "d = (P ** A ** Q) $from_nat i$ from_nat i"
and "d = (P ** A ** Q) $from_nat i$ from_nat i"
and "d = (P ** A ** Q) $from_nat i$ from_nat i"
unfolding diagonal_step_PQ_PAQ[OF PQ b]
unfolding vec_lambda_beta using a1 a2
using Aik0 Aki0 d by auto
show "v * A $from_nat k$ from_nat k = (P ** A ** Q) $from_nat k$ from_nat k"
and "v * A $from_nat k$ from_nat k = (P ** A ** Q) $from_nat k$ from_nat k"
using a1 a2
unfolding diagonal_step_PQ_PAQ[OF PQ b] mult_column_def column_add_def
unfolding vec_lambda_beta unfolding Aik0 Aki0 by (auto simp add: rw)
fix a::'rows and b::'cols
assume ak: "a ≠ from_nat k" and ai: "a ≠ from_nat i"
show "A $a$ b = (P ** A ** Q) $a$ b"
using ai ak a1 a2 Aab0 k1 i2
unfolding diagonal_step_PQ_PAQ[OF PQ b]
unfolding vec_lambda_beta by auto
next
fix a::'rows and b::'cols
assume ak: "a ≠ from_nat k" and ai: "b ≠ from_nat i"
show "A $a$ b = (P ** A ** Q) $a$ b"
using ai ak a1 a2 Aab0 Aab0' d du k1 k2 i1 i2
unfolding diagonal_step_PQ_PAQ[OF PQ b]
unfolding vec_lambda_beta by auto
next
fix a::'rows and b::'cols
assume ak: "b ≠ from_nat k" and ai: "a ≠ from_nat i"
show "A $a$ b = (P ** A ** Q) $a$ b"
using ai ak a1 a2 Aab0 Aab0' d du k1 k2 i1 i2
unfolding diagonal_step_PQ_PAQ[OF PQ b]
unfolding vec_lambda_beta apply auto (*TODO: cleanup this sledeghammer proof*)
proof -
assume "d = p * ?Aii+ ?Akk* q"
then have "v * (p * ?Aii) + v * (?Akk* q) = d * v"
then have "?Aii- v * (p * ?Aii) - v * (?Akk* q) = 0"
then show "?Aii- v * (p * ?Aii) = v * ?Akk* q"
by force
qed
next
fix a::'rows and b::'cols
assume ak: "b ≠ from_nat k" and ai: "b ≠ from_nat i"
show "A $a$ b = (P ** A ** Q) $a$ b"
using ai ak a1 a2 Aab0 Aab0' d du k1 k2 i1 i2
unfolding diagonal_step_PQ_PAQ[OF PQ b]
unfolding vec_lambda_beta by auto
qed
qed

fun diagonal_to_Smith_i_PQ ::
"nat list ⇒ nat ⇒ ('a::{bezout_ring} bezout)
⇒ (('a^'rows::mod_type^'rows::mod_type)×('a^'cols::mod_type^'rows::mod_type)× ('a^'cols::mod_type^'cols::mod_type))
⇒ (('a^'rows::mod_type^'rows::mod_type)× ('a^'cols::mod_type^'rows::mod_type) × ('a^'cols::mod_type^'cols::mod_type))"
where
"diagonal_to_Smith_i_PQ [] i bezout (P,A,Q) = (P,A,Q)" |
"diagonal_to_Smith_i_PQ (j#xs) i bezout (P,A,Q) = (
if A $(from_nat i)$ (from_nat i) dvd A $(from_nat j)$ (from_nat j)
then diagonal_to_Smith_i_PQ xs i bezout (P,A,Q)
else let (p, q, u, v, d) = bezout (A $from_nat i$ from_nat i) (A $from_nat j$ from_nat j);
A' = diagonal_step A i j d v;
(P',Q') = diagonal_step_PQ A i j bezout
in diagonal_to_Smith_i_PQ xs i bezout (P'**P,A',Q**Q') ― ‹Apply the step›
)
"

text‹This is implemented by fun. This way, I can do pattern-matching for $(P,A,Q)$.›

fun Diagonal_to_Smith_row_i_PQ
where "Diagonal_to_Smith_row_i_PQ i bezout (P,A,Q)
= diagonal_to_Smith_i_PQ [i + 1..<min (nrows A) (ncols A)] i bezout (P,A,Q)"

text‹Deleted from the simplified and renamed as it would be a definition.›

declare Diagonal_to_Smith_row_i_PQ.simps[simp del]
lemmas Diagonal_to_Smith_row_i_PQ_def = Diagonal_to_Smith_row_i_PQ.simps

fun diagonal_to_Smith_aux_PQ
where
"diagonal_to_Smith_aux_PQ [] bezout (P,A,Q) = (P,A,Q)" |
"diagonal_to_Smith_aux_PQ (i#xs) bezout (P,A,Q)
= diagonal_to_Smith_aux_PQ xs bezout (Diagonal_to_Smith_row_i_PQ i bezout (P,A,Q))"

lemma diagonal_to_Smith_aux_PQ_append:
"diagonal_to_Smith_aux_PQ (xs @ ys) bezout (P,A,Q)
= diagonal_to_Smith_aux_PQ ys bezout (diagonal_to_Smith_aux_PQ xs bezout (P,A,Q))"
by (induct xs bezout "(P,A,Q)" arbitrary: P A Q rule: diagonal_to_Smith_aux_PQ.induct)
(auto, metis prod_cases3)

lemma diagonal_to_Smith_aux_PQ_append2[simp]:
"diagonal_to_Smith_aux_PQ (xs @ [ys]) bezout (P,A,Q)
= Diagonal_to_Smith_row_i_PQ ys bezout (diagonal_to_Smith_aux_PQ xs bezout (P,A,Q))"
proof (induct xs bezout "(P,A,Q)" arbitrary: P A Q rule: diagonal_to_Smith_aux_PQ.induct)
case (1 bezout P A Q)
then show ?case
by (metis append.simps(1) diagonal_to_Smith_aux_PQ.simps prod.exhaust)
next
case (2 i xs bezout P A Q)
then show ?case
by (metis (no_types, hide_lams) append_Cons diagonal_to_Smith_aux_PQ.simps(2) prod_cases3)
qed

(*
definition "diagonal_to_Smith_PQ A bezout
= diagonal_to_Smith_aux_PQ [0..<min (nrows A) (ncols A) - 1] bezout (mat 1, A, mat 1)"
*)

context
fixes A::"'a::{bezout_ring}^'cols::mod_type^'rows::mod_type" (*This is the input matrix*)
and B::"'a::{bezout_ring}^'cols::mod_type^'rows::mod_type" (*This is the matrix in each step*)
and P and Q
and bezout::"'a bezout"
assumes PAQ: "P**A**Q = B"
and P: "invertible P" and Q: "invertible Q"
and ib: "is_bezout_ext bezout"
begin

text‹The output is the same as the one in the version where $P$ and $Q$ are not computed.›

lemma diagonal_to_Smith_i_PQ_eq:
assumes P'B'Q': "(P',B',Q') = diagonal_to_Smith_i_PQ xs i bezout (P,B,Q)"
and xs: "∀x. x ∈ set xs ⟶ x < min (nrows A) (ncols A)"
and diag: "isDiagonal B" and i_notin: "i ∉ set xs" and i: "i<min (nrows A) (ncols A)"
shows "B' = diagonal_to_Smith_i xs B i bezout"
using assms PAQ ib P Q
proof (induct xs i bezout "(P,B,Q)" arbitrary: P B Q rule:diagonal_to_Smith_i_PQ.induct)
case (1 i bezout P A Q)
then show ?case by auto
next
case (2 j xs i bezout P B Q)
let ?Bii = "B $from_nat i$ from_nat i"
let ?Bjj = "B $from_nat j$ from_nat j"
let ?p="case bezout (B $from_nat i$ from_nat i) (B $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ p"
let ?q="case bezout (B $from_nat i$ from_nat i) (B $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ q"
let ?u="case bezout (B $from_nat i$ from_nat i) (B $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ u"
let ?v="case bezout (B $from_nat i$ from_nat i) (B $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ v"
let ?d="case bezout (B $from_nat i$ from_nat i) (B $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ d"
let ?B'="diagonal_step B i j ?d ?v"
let ?P' = "fst (diagonal_step_PQ B i j bezout)"
let ?Q' = "snd (diagonal_step_PQ B i j bezout)"
have pquvd: "(?p, ?q, ?u, ?v,?d) = bezout (B $from_nat i$ from_nat i) (B $from_nat j$ from_nat j)"
note hyp = "2.hyps"(2)
note P'B'Q' = "2.prems"(1)
note i_min = "2.prems"(5)
note PAQ_B = "2.prems"(6)
note i_notin = "2.prems"(4)
note diagB = "2.prems"(3)
note xs_min = "2.prems"(2)
note ib = "2.prems"(7)
note inv_P = "2.prems"(8)
note inv_Q = "2.prems"(9)
show ?case
proof (cases "?Bii dvd ?Bjj")
case True
show ?thesis using "2.prems" "2.hyps"(1) True by auto
next
case False
have aux: "diagonal_to_Smith_i_PQ (j # xs) i bezout (P, B, Q)
= diagonal_to_Smith_i_PQ xs i bezout (?P'**P,?B', Q**?Q')"
using False by (auto simp add: split_beta)
have i: "i < min (nrows B) (ncols B)" using i_min unfolding nrows_def ncols_def by auto
have j: "j < min (nrows B) (ncols B)" using xs_min unfolding nrows_def ncols_def by auto
have aux2: "diagonal_to_Smith_i(j # xs) B i bezout = diagonal_to_Smith_i xs ?B' i bezout"
using False by (auto simp add: split_beta)
have res: " B' = diagonal_to_Smith_i xs ?B' i bezout"
proof (rule hyp[OF False])
show "(P', B', Q') = diagonal_to_Smith_i_PQ xs i bezout (?P'**P,?B', Q**?Q')"
using aux P'B'Q' by auto
have B'_P'B'Q': "?B' = ?P'**B**?Q'"
by (rule diagonal_step_PQ[OF _ _ i j _ ib diagB], insert i_notin pquvd, auto)
show "?P'**P ** A ** (Q**?Q') = ?B'"
unfolding B'_P'B'Q' unfolding PAQ_B[symmetric]
show "isDiagonal ?B'" by (rule isDiagonal_diagonal_step[OF diagB i j])
show "invertible (?P'** P)"
by (metis inv_P diagonal_step_PQ_invertible_P i i_notin in_set_member
invertible_mult j member_rec(1) prod.exhaust_sel)
show "invertible (Q ** ?Q')"
by (metis diagonal_step_PQ_invertible_Q i i_notin inv_Q
invertible_mult j list.set_intros(1) prod.collapse)
qed (insert pquvd xs_min i_min i_notin ib, auto)
show ?thesis using aux aux2 res by auto
qed
qed

lemma diagonal_to_Smith_i_PQ':
assumes P'B'Q': "(P',B',Q') = diagonal_to_Smith_i_PQ xs i bezout (P,B,Q)"
and xs: "∀x. x ∈ set xs ⟶ x < min (nrows A) (ncols A)"
and diag: "isDiagonal B" and i_notin: "i ∉ set xs" and i: "i<min (nrows A) (ncols A)"
shows "B' = P'**A**Q' ∧ invertible P' ∧ invertible Q'"
using assms PAQ ib P Q
proof (induct xs i bezout "(P,B,Q)" arbitrary: P B Q rule:diagonal_to_Smith_i_PQ.induct)
case (1 i bezout)
then show ?case using PAQ by auto
next
case (2 j xs i bezout P B Q)
let ?Bii = "B $from_nat i$ from_nat i"
let ?Bjj = "B $from_nat j$ from_nat j"
let ?p="case bezout (B $from_nat i$ from_nat i) (B $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ p"
let ?q="case bezout (B $from_nat i$ from_nat i) (B $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ q"
let ?u="case bezout (B $from_nat i$ from_nat i) (B $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ u"
let ?v="case bezout (B $from_nat i$ from_nat i) (B $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ v"
let ?d="case bezout (B $from_nat i$ from_nat i) (B $from_nat j$ from_nat j) of (p,q,u,v,d) ⇒ d"
let ?B'="diagonal_step B i j ?d ?v"
let ?P' = "fst (diagonal_step_PQ B i j bezout)"
let ?Q' = "snd (diagonal_step_PQ B i j bezout)"
have pquvd: "(?p, ?q, ?u, ?v,?d) = bezout (B $from_nat i$ from_nat i) (B $from_nat j$ from_nat j)"
show ?case
proof (cases "?Bii dvd ?Bjj")
case True
then show ?thesis using "2.prems"
using "2.hyps"(1) by auto
next
case False
note hyp = "2.hyps"(2)
note P'B'Q' = "2.prems"(1)
note i_min = "2.prems"(5)
note PAQ_B = "2.prems"(6)
note i_notin = "2.prems"(4)
note diagB = "2.prems"(3)
note xs_min = "2.prems"(2)
note ib = "2.prems"(7)
note inv_P = "2.prems"(8)
note inv_Q = "2.prems"(9)
have aux: "diagonal_to_Smith_i_PQ (j # xs) i bezout (P, B, Q)
= diagonal_to_Smith_i_PQ xs i bezout (?P'**P,?B', Q**?Q')"
using False by (auto simp add: split_beta)
have i: "i < min (nrows B) (ncols B)" using i_min unfolding nrows_def ncols_def by auto
have j: "j < min (nrows B) (ncols B)" using xs_min unfolding nrows_def ncols_def by auto
show ?thesis
proof (rule hyp[OF False])
show "(P', B', Q') = diagonal_to_Smith_i_PQ xs i bezout (?P'**P,?B', Q**?Q')"
using aux P'B'Q' by auto
have B'_P'B'Q': "?B' = ?P'**B**?Q'"
by (rule diagonal_step_PQ[OF _ _ i j _ ib diagB], insert i_notin pquvd, auto)
show "?P'**P ** A ** (Q**?Q') = ?B'"
unfolding B'_P'B'Q' unfolding PAQ_B[symmetric]
show "isDiagonal ?B'" by (rule isDiagonal_diagonal_step[OF diagB i j])
show "invertible (?P'** P)"
by (metis inv_P diagonal_step_PQ_invertible_P i i_notin in_set_member
invertible_mult j member_rec(1) prod.exhaust_sel)
show "invertible (Q ** ?Q')"
by (metis diagonal_step_PQ_invertible_Q i i_notin inv_Q
invertible_mult j list.set_intros(1) prod.collapse)
qed (insert pquvd xs_min i_min i_notin ib, auto)
qed
qed

corollary diagonal_to_Smith_i_PQ:
assumes P'B'Q': "(P',B',Q') = diagonal_to_Smith_i_PQ xs i bezout (P,B,Q)"
and xs: "∀x. x ∈ set xs ⟶ x < min (nrows A) (ncols A)"
and diag: "isDiagonal B" and i_notin: "i ∉ set xs" and i: "i<min (nrows A) (ncols A)"
shows "B' = P'**A**Q' ∧ invertible P' ∧ invertible Q' ∧ B' = diagonal_to_Smith_i xs B i bezout"
using assms diagonal_to_Smith_i_PQ' diagonal_to_Smith_i_PQ_eq by metis

lemma Diagonal_to_Smith_row_i_PQ_eq:
assumes P'B'Q': "(P',B',Q') = Diagonal_to_Smith_row_i_PQ i bezout (P,B,Q)"
and diag: "isDiagonal B" and i: "i < min (nrows A) (ncols A)"
shows "B' = Diagonal_to_Smith_row_i B i bezout"
using assms unfolding Diagonal_to_Smith_row_i_def Diagonal_to_Smith_row_i_PQ_def
using diagonal_to_Smith_i_PQ by (auto simp add: nrows_def ncols_def)

lemma Diagonal_to_Smith_row_i_PQ':
assumes P'B'Q': "(P',B',Q') = Diagonal_to_Smith_row_i_PQ i bezout (P,B,Q)"
and diag: "isDiagonal B" and i: "i < min (nrows A) (ncols A)"
shows "B' = P'**A**Q' ∧ invertible P' ∧ invertible Q'"
by (rule diagonal_to_Smith_i_PQ'[OF P'B'Q'[unfolded Diagonal_to_Smith_row_i_PQ_def] _ diag _ i],

lemma Diagonal_to_Smith_row_i_PQ:
assumes P'B'Q': "(P',B',Q') = Diagonal_to_Smith_row_i_PQ i bezout (P,B,Q)"
and diag: "isDiagonal B" and i: "i < min (nrows A) (ncols A)"
shows "B' = P'**A**Q' ∧ invertible P' ∧ invertible Q' ∧ B' = Diagonal_to_Smith_row_i B i bezout"
using assms Diagonal_to_Smith_row_i_PQ' Diagonal_to_Smith_row_i_PQ_eq by presburger

end

context
fixes A::"'a::{bezout_ring}^'cols::mod_type^'rows::mod_type" (*This is the input matrix*)
and B::"'a::{bezout_ring}^'cols::mod_type^'rows::mod_type" (*This is the matrix in each step*)
and P and Q
and bezout::"'a bezout"
assumes PAQ: "P**A**Q = B"
and P: "invertible P" and Q: "invertible Q"
and ib: "is_bezout_ext bezout"
begin

lemma diagonal_to_Smith_aux_PQ:
assumes P'B'Q': "(P',B',Q') = diagonal_to_Smith_aux_PQ [0..<k] bezout (P,B,Q)"
and diag: "isDiagonal B" and k:"k<min (nrows A) (ncols A)"
shows "B' = P'**A**Q' ∧ invertible P' ∧ invertible Q' ∧ B' = diagonal_to_Smith_aux B [0..<k] bezout"
using k P'B'Q' P Q PAQ diag
proof (induct k arbitrary: P B Q P' Q' B')
case 0
then show ?case using P Q PAQ by auto
next
case (Suc k P B Q P' Q' B')
note Suc_k = Suc.prems(1)
note PBQ = Suc.prems(2)
note P = Suc.prems(3)
note Q = Suc.prems(4)
note PAQ_B = Suc.prems(5)
note diag_B = Suc.prems(6)
let ?Dk = "(diagonal_to_Smith_aux_PQ [0..<k] bezout (P, P ** A ** Q, Q))"
let ?P' = "fst ?Dk"
let ?B'="fst (snd ?Dk)"
let ?Q' = "snd (snd ?Dk)"
have k: "k<min (nrows A) (ncols A)" using Suc_k by auto
have hyp: "?B' = ?P' ** A ** ?Q' ∧ invertible ?P' ∧ invertible ?Q'
∧ ?B' = diagonal_to_Smith_aux B [0..<k] bezout"
by (rule Suc.hyps[OF k _ P Q PAQ_B diag_B], auto simp add: PAQ_B)
have diag_B': "isDiagonal ?B'"
by (metis diag_B hyp ib isDiagonal_diagonal_to_Smith_aux k ncols_def nrows_def)
have "B' = diagonal_to_Smith_aux B [0..<Suc k] bezout"
by (auto, metis Diagonal_to_Smith_row_i_PQ_eq PAQ_B Suc(3) diag_B'
diagonal_to_Smith_aux_PQ_append2 eq_fst_iff hyp ib k sndI upt.simps(2) zero_order(1))
moreover have "B' = P' ** A ** Q' ∧ invertible P' ∧ invertible Q'"
proof (rule Diagonal_to_Smith_row_i_PQ')
show "(P', B', Q') = Diagonal_to_Smith_row_i_PQ k bezout (?P',?B',?Q')" using Suc.prems by auto
show "invertible ?P'" using hyp by auto
show "?P' ** A ** ?Q' = ?B'" using hyp by auto
show "invertible ?Q'" using hyp by auto
show "is_bezout_ext bezout" using ib by auto
show "k < min (nrows A) (ncols A)" using k by auto
show diag_B': "isDiagonal ?B'" using diag_B' by auto
qed
ultimately show ?case by auto
qed

end

fun diagonal_to_Smith_PQ
where "diagonal_to_Smith_PQ A bezout
= diagonal_to_Smith_aux_PQ  [0..<min (nrows A) (ncols A) - 1] bezout (mat 1, A ,mat 1)"

declare diagonal_to_Smith_PQ.simps[simp del]
lemmas diagonal_to_Smith_PQ_def = diagonal_to_Smith_PQ.simps

lemma diagonal_to_Smith_PQ:
fixes A::"'a::{bezout_ring}^'cols::{mod_type}^'rows::{mod_type}"
assumes A: "isDiagonal A" and ib: "is_bezout_ext bezout"
assumes PBQ: "(P,B,Q) = diagonal_to_Smith_PQ A bezout"
shows "B = P**A**Q ∧ invertible P ∧ invertible Q ∧ B = diagonal_to_Smith A bezout"
proof (unfold diagonal_to_Smith_def, rule diagonal_to_Smith_aux_PQ[OF  _ _ _ ib _ A])
let ?P = "mat 1::'a^'rows::mod_type^'rows::mod_type"
let ?Q = "mat 1::'a^'cols::mod_type^'cols::mod_type"
show "(P, B, Q) = diagonal_to_Smith_aux_PQ [0..<min (nrows A) (ncols A) - 1] bezout (?P, A, ?Q)"
using PBQ unfolding diagonal_to_Smith_PQ_def .
show "?P ** A ** ?Q = A" by simp
show " min (nrows A) (ncols A) - 1 < min (nrows A) (ncols A)"
by (metis (no_types, lifting) One_nat_def diff_less dual_order.strict_iff_order le_less_trans
min_def mod_type_class.to_nat_less_card ncols_def not_less_eq nrows_not_0 zero_order(1))

lemma diagonal_to_Smith_PQ_exists:
fixes A::"'a::{bezout_ring}^'cols::{mod_type}^'rows::{mod_type}"
assumes A: "isDiagonal A"
shows "∃P Q.
invertible (P::'a^'rows::{mod_type}^'rows::{mod_type})
∧ invertible (Q::'a^'cols::{mod_type}^'cols::{mod_type})
∧ Smith_normal_form (P**A**Q)"
proof -
obtain bezout::"'a bezout" where ib: "is_bezout_ext bezout"
using exists_bezout_ext by blast
obtain P B Q where PBQ: "(P,B,Q) = diagonal_to_Smith_PQ A bezout"
by (metis prod_cases3)
have "B = P**A**Q ∧ invertible P ∧ invertible Q ∧ B = diagonal_to_Smith A bezout"
by (rule diagonal_to_Smith_PQ[OF A ib PBQ])
moreover have "Smith_normal_form (P**A**Q)"
using Smith_normal_form_diagonal_to_Smith assms calculation ib by fastforce
ultimately show ?thesis by auto
qed

subsection‹The final soundness theorem›

lemma diagonal_to_Smith_PQ':
fixes A::"'a::{bezout_ring}^'cols::{mod_type}^'rows::{mod_type}"
assumes A: "isDiagonal A" and ib: "is_bezout_ext bezout"
assumes PBQ: "(P,S,Q) = diagonal_to_Smith_PQ A bezout"
shows "S = P**A**Q ∧ invertible P ∧ invertible Q ∧ Smith_normal_form S"
using A PBQ Smith_normal_form_diagonal_to_Smith diagonal_to_Smith_PQ ib by fastforce

end


# Theory Mod_Type_Connect

(*
Author: Jose Divasón
Email:  jose.divason@unirioja.es
*)

section ‹A new bridge to convert theorems from JNF to HOL Analysis and vice-versa,
based on the @{text "mod_type"} class›

theory Mod_Type_Connect
imports
Perron_Frobenius.HMA_Connect
Rank_Nullity_Theorem.Mod_Type
Gauss_Jordan.Elementary_Operations
begin

text ‹Some lemmas on @{text "Mod_Type.to_nat"} and @{text "Mod_Type.from_nat"} are added to have
them with the same names as the analogous ones for @{text "Bij_Nat.to_nat"}
and @{text "Bij_Nat.to_nat"}.›

lemma inj_to_nat: "inj to_nat" by (simp add: inj_on_def)
lemmas from_nat_inj = from_nat_eq_imp_eq
lemma range_to_nat: "range (to_nat :: 'a :: mod_type ⇒ nat) = {0 ..< CARD('a)}"

text ‹This theory is an adaptation of the one presented in @{text "Perron_Frobenius.HMA_Connect"},
but for matrices and vectors where indexes have the @{text "mod_type"} class restriction.

It is worth noting that some definitions still use the old abbreviation for HOL Analysis
(HMA, from HOL Multivariate Analysis) instead of HA. This is done to be consistent with
the existing names in the Perron-Frobenius development›

context includes vec.lifting
begin
end

definition from_hma⇩v :: "'a ^ 'n :: mod_type ⇒ 'a Matrix.vec" where
"from_hma⇩v v = Matrix.vec CARD('n) (λ i. v $h from_nat i)" definition from_hma⇩m :: "'a ^ 'nc :: mod_type ^ 'nr :: mod_type ⇒ 'a Matrix.mat" where "from_hma⇩m a = Matrix.mat CARD('nr) CARD('nc) (λ (i,j). a$h from_nat i $h from_nat j)" definition to_hma⇩v :: "'a Matrix.vec ⇒ 'a ^ 'n :: mod_type" where "to_hma⇩v v = (χ i. v$v to_nat i)"

definition to_hma⇩m :: "'a Matrix.mat ⇒ 'a ^ 'nc :: mod_type ^ 'nr :: mod_type " where
"to_hma⇩m a = (χ i j. a $$(to_nat i, to_nat j))" lemma to_hma_from_hma⇩v[simp]: "to_hma⇩v (from_hma⇩v v) = v" by (auto simp: to_hma⇩v_def from_hma⇩v_def to_nat_less_card) lemma to_hma_from_hma⇩m[simp]: "to_hma⇩m (from_hma⇩m v) = v" by (auto simp: to_hma⇩m_def from_hma⇩m_def to_nat_less_card) lemma from_hma_to_hma⇩v[simp]: "v ∈ carrier_vec (CARD('n)) ⟹ from_hma⇩v (to_hma⇩v v :: 'a ^ 'n :: mod_type) = v" by (auto simp: to_hma⇩v_def from_hma⇩v_def to_nat_from_nat_id) lemma from_hma_to_hma⇩m[simp]: "A ∈ carrier_mat (CARD('nr)) (CARD('nc)) ⟹ from_hma⇩m (to_hma⇩m A :: 'a ^ 'nc :: mod_type ^ 'nr :: mod_type) = A" by (auto simp: to_hma⇩m_def from_hma⇩m_def to_nat_from_nat_id) lemma from_hma⇩v_inj[simp]: "from_hma⇩v x = from_hma⇩v y ⟷ x = y" by (intro iffI, insert to_hma_from_hma⇩v[of x], auto) lemma from_hma⇩m_inj[simp]: "from_hma⇩m x = from_hma⇩m y ⟷ x = y" by(intro iffI, insert to_hma_from_hma⇩m[of x], auto) definition HMA_V :: "'a Matrix.vec ⇒ 'a ^ 'n :: mod_type ⇒ bool" where "HMA_V = (λ v w. v = from_hma⇩v w)" definition HMA_M :: "'a Matrix.mat ⇒ 'a ^ 'nc :: mod_type ^ 'nr :: mod_type ⇒ bool" where "HMA_M = (λ a b. a = from_hma⇩m b)" definition HMA_I :: "nat ⇒ 'n :: mod_type ⇒ bool" where "HMA_I = (λ i a. i = to_nat a)" context includes lifting_syntax begin lemma Domainp_HMA_V [transfer_domain_rule]: "Domainp (HMA_V :: 'a Matrix.vec ⇒ 'a ^ 'n :: mod_type ⇒ bool) = (λ v. v ∈ carrier_vec (CARD('n )))" by(intro ext iffI, insert from_hma_to_hma⇩v[symmetric], auto simp: from_hma⇩v_def HMA_V_def) lemma Domainp_HMA_M [transfer_domain_rule]: "Domainp (HMA_M :: 'a Matrix.mat ⇒ 'a ^ 'nc :: mod_type ^ 'nr :: mod_type ⇒ bool) = (λ A. A ∈ carrier_mat CARD('nr) CARD('nc))" by (intro ext iffI, insert from_hma_to_hma⇩m[symmetric], auto simp: from_hma⇩m_def HMA_M_def) lemma Domainp_HMA_I [transfer_domain_rule]: "Domainp (HMA_I :: nat ⇒ 'n :: mod_type ⇒ bool) = (λ i. i < CARD('n))" (is "?l = ?r") proof (intro ext) fix i :: nat show "?l i = ?r i" unfolding HMA_I_def Domainp_iff by (auto intro: exI[of _ "from_nat i"] simp: to_nat_from_nat_id to_nat_less_card) qed lemma bi_unique_HMA_V [transfer_rule]: "bi_unique HMA_V" "left_unique HMA_V" "right_unique HMA_V" unfolding HMA_V_def bi_unique_def left_unique_def right_unique_def by auto lemma bi_unique_HMA_M [transfer_rule]: "bi_unique HMA_M" "left_unique HMA_M" "right_unique HMA_M" unfolding HMA_M_def bi_unique_def left_unique_def right_unique_def by auto lemma bi_unique_HMA_I [transfer_rule]: "bi_unique HMA_I" "left_unique HMA_I" "right_unique HMA_I" unfolding HMA_I_def bi_unique_def left_unique_def right_unique_def by auto lemma right_total_HMA_V [transfer_rule]: "right_total HMA_V" unfolding HMA_V_def right_total_def by simp lemma right_total_HMA_M [transfer_rule]: "right_total HMA_M" unfolding HMA_M_def right_total_def by simp lemma right_total_HMA_I [transfer_rule]: "right_total HMA_I" unfolding HMA_I_def right_total_def by simp lemma HMA_V_index [transfer_rule]: "(HMA_V ===> HMA_I ===> (=)) (v) (h)" unfolding rel_fun_def HMA_V_def HMA_I_def from_hma⇩v_def by (auto simp: to_nat_less_card) lemma HMA_M_index [transfer_rule]: "(HMA_M ===> HMA_I ===> HMA_I ===> (=)) (λ A i j. A$$ (i,j)) index_hma"
by (intro rel_funI, simp add: index_hma_def to_nat_less_card HMA_M_def HMA_I_def from_hma⇩m_def)

lemma HMA_V_0 [transfer_rule]: "HMA_V (0⇩v CARD('n)) (0 :: 'a :: zero ^ 'n:: mod_type)"
unfolding HMA_V_def from_hma⇩v_def by auto

lemma HMA_M_0 [transfer_rule]:
"HMA_M (0⇩m CARD('nr) CARD('nc)) (0 :: 'a :: zero ^ 'nc:: mod_type  ^ 'nr :: mod_type)"
unfolding HMA_M_def from_hma⇩m_def by auto

lemma HMA_M_1[transfer_rule]:
"HMA_M (1⇩m (CARD('n))) (mat 1 :: 'a::{zero,one}^'n:: mod_type^'n:: mod_type)"
unfolding HMA_M_def
by (auto simp add: mat_def from_hma⇩m_def from_nat_inj)

lemma from_hma⇩v_add: "from_hma⇩v v + from_hma⇩v w = from_hma⇩v (v + w)"
unfolding from_hma⇩v_def by auto

lemma HMA_V_add [transfer_rule]: "(HMA_V ===> HMA_V ===> HMA_V) (+) (+) "
unfolding rel_fun_def HMA_V_def

lemma from_hma⇩v_diff: "from_hma⇩v v - from_hma⇩v w = from_hma⇩v (v - w)"
unfolding from_hma⇩v_def by auto

lemma HMA_V_diff [transfer_rule]: "(HMA_V ===> HMA_V ===> HMA_V) (-) (-)"
unfolding rel_fun_def HMA_V_def
by (auto simp: from_hma⇩v_diff)

lemma from_hma⇩m_add: "from_hma⇩m a + from_hma⇩m b = from_hma⇩m (a + b)"
unfolding from_hma⇩m_def by auto

lemma HMA_M_add [transfer_rule]: "(HMA_M ===> HMA_M ===> HMA_M) (+) (+) "
unfolding rel_fun_def HMA_M_def

lemma from_hma⇩m_diff: "from_hma⇩m a - from_hma⇩m b = from_hma⇩m (a - b)"
unfolding from_hma⇩m_def by auto

lemma HMA_M_diff [transfer_rule]: "(HMA_M ===> HMA_M ===> HMA_M) (-) (-) "
unfolding rel_fun_def HMA_M_def
by (auto simp: from_hma⇩m_diff)

lemma scalar_product: fixes v :: "'a :: semiring_1 ^ 'n :: mod_type"
shows "scalar_prod (from_hma⇩v v) (from_hma⇩v w) = scalar_product v w"
unfolding scalar_product_def scalar_prod_def from_hma⇩v_def dim_vec
by (simp add: sum.reindex[OF inj_to_nat, unfolded range_to_nat])

lemma [simp]:
"from_hma⇩m (y :: 'a ^ 'nc :: mod_type ^ 'nr:: mod_type) ∈ carrier_mat (CARD('nr)) (CARD('nc))"
"dim_row (from_hma⇩m (y :: 'a ^ 'nc:: mod_type  ^ 'nr :: mod_type)) = CARD('nr)"
"dim_col (from_hma⇩m (y :: 'a ^ 'nc :: mod_type ^ 'nr:: mod_type )) = CARD('nc)"
unfolding from_hma⇩m_def by simp_all

lemma [simp]:
"from_hma⇩v (y :: 'a ^ 'n:: mod_type) ∈ carrier_vec (CARD('n))"
"dim_vec (from_hma⇩v (y :: 'a ^ 'n:: mod_type)) = CARD('n)"
unfolding from_hma⇩v_def by simp_all

lemma HMA_scalar_prod [transfer_rule]:
"(HMA_V ===> HMA_V ===> (=)) scalar_prod scalar_product"
by (auto simp: HMA_V_def scalar_product)

lemma HMA_row [transfer_rule]: "(HMA_I ===> HMA_M ===> HMA_V) (λ i a. Matrix.row a i) row"
unfolding HMA_M_def HMA_I_def HMA_V_def
by (auto simp: from_hma⇩m_def from_hma⇩v_def to_nat_less_card row_def)

lemma HMA_col [transfer_rule]: "(HMA_I ===> HMA_M ===> HMA_V) (λ i a. col a i) column"
unfolding HMA_M_def HMA_I_def HMA_V_def
by (auto simp: from_hma⇩m_def from_hma⇩v_def to_nat_less_card column_def)

lemma HMA_M_mk_mat[transfer_rule]: "((HMA_I ===> HMA_I ===> (=)) ===> HMA_M)
(λ f. Matrix.mat (CARD('nr)) (CARD('nc)) (λ (i,j). f i j))
(mk_mat :: (('nr ⇒ 'nc ⇒ 'a) ⇒ 'a^'nc:: mod_type^'nr:: mod_type))"
proof-
{
fix x y i j
assume id: "∀ (ya :: 'nr) (yb :: 'nc). (x (to_nat ya) (to_nat yb) :: 'a) = y ya yb"
and i: "i < CARD('nr)" and j: "j < CARD('nc)"
from to_nat_from_nat_id[OF i] to_nat_from_nat_id[OF j] id[rule_format, of "from_nat i" "from_nat j"]
have "x i j = y (from_nat i) (from_nat j)" by auto
}
thus ?thesis
unfolding rel_fun_def mk_mat_def HMA_M_def HMA_I_def from_hma⇩m_def by auto
qed

lemma HMA_M_mk_vec[transfer_rule]: "((HMA_I ===> (=)) ===> HMA_V)
(λ f. Matrix.vec (CARD('n)) (λ i. f i))
(mk_vec :: (('n ⇒ 'a) ⇒ 'a^'n:: mod_type))"
proof-
{
fix x y i
assume id: "∀ (ya :: 'n). (x (to_nat ya) :: 'a) = y ya"
and i: "i < CARD('n)"
from to_nat_from_nat_id[OF i] id[rule_format, of "from_nat i"]
have "x i = y (from_nat i)" by auto
}
thus ?thesis
unfolding rel_fun_def mk_vec_def HMA_V_def HMA_I_def from_hma⇩v_def by auto
qed

lemma mat_mult_scalar: "A ** B = mk_mat (λ i j. scalar_product (row i A) (column j B))"
unfolding vec_eq_iff matrix_matrix_mult_def scalar_product_def mk_mat_def
by (auto simp: row_def column_def)

lemma mult_mat_vec_scalar: "A *v v = mk_vec (λ i. scalar_product (row i A) v)"
unfolding vec_eq_iff matrix_vector_mult_def scalar_product_def mk_mat_def mk_vec_def
by (auto simp: row_def column_def)

lemma dim_row_transfer_rule:
"HMA_M A (A' :: 'a ^ 'nc:: mod_type ^ 'nr:: mod_type) ⟹ (=) (dim_row A) (CARD('nr))"
unfolding HMA_M_def by auto

lemma dim_col_transfer_rule:
"HMA_M A (A' :: 'a ^ 'nc:: mod_type ^ 'nr:: mod_type) ⟹ (=) (dim_col A) (CARD('nc))"
unfolding HMA_M_def by auto

lemma HMA_M_mult [transfer_rule]: "(HMA_M ===> HMA_M ===> HMA_M) (*) (**)"
proof -
{
fix A B :: "'a :: semiring_1 mat" and A' :: "'a ^ 'n :: mod_type ^ 'nr:: mod_type"
and B' :: "'a ^ 'nc :: mod_type ^ 'n:: mod_type"
assume 1[transfer_rule]: "HMA_M A A'" "HMA_M B B'"
note [transfer_rule] = dim_row_transfer_rule[OF 1(1)] dim_col_transfer_rule[OF 1(2)]
have "HMA_M (A * B) (A' ** B')"
unfolding times_mat_def mat_mult_scalar
by (transfer_prover_start, transfer_step+, transfer, auto)
}
thus ?thesis by blast
qed

lemma HMA_V_smult [transfer_rule]: "((=) ===> HMA_V ===> HMA_V) (⋅⇩v) (*s)"
unfolding smult_vec_def
unfolding rel_fun_def HMA_V_def from_hma⇩v_def
by auto

lemma HMA_M_mult_vec [transfer_rule]: "(HMA_M ===> HMA_V ===> HMA_V) (*⇩v) (*v)"
proof -
{
fix A :: "'a :: semiring_1 mat" and v :: "'a Matrix.vec"
and A' :: "'a ^ 'nc :: mod_type ^ 'nr :: mod_type" and v' :: "'a ^ 'nc :: mod_type"
assume 1[transfer_rule]: "HMA_M A A'" "HMA_V v v'"
note [transfer_rule] = dim_row_transfer_rule
have "HMA_V (A *⇩v v) (A' *v v')"
unfolding mult_mat_vec_def mult_mat_vec_scalar
by (transfer_prover_start, transfer_step+, transfer, auto)
}
thus ?thesis by blast
qed

lemma HMA_det [transfer_rule]: "(HMA_M ===> (=)) Determinant.det
(det :: 'a :: comm_ring_1 ^ 'n :: mod_type ^ 'n :: mod_type ⇒ 'a)"
proof -
{
fix a :: "'a ^ 'n :: mod_type^ 'n:: mod_type"
let ?tn = "to_nat :: 'n :: mod_type ⇒ nat"
let ?fn = "from_nat :: nat ⇒ 'n"
let ?zn = "{0..< CARD('n)}"
let ?U = "UNIV :: 'n set"
let ?p1 = "{p. p permutes ?zn}"
let ?p2 = "{p. p permutes ?U}"
let ?f= "λ p i. if i ∈ ?U then ?fn (p (?tn i)) else i"
let ?g = "λ p i. ?fn (p (?tn i))"
have fg: "⋀ a b c. (if a ∈ ?U then b else c) = b" by auto
have "?p2 = ?f  ?p1"
by (rule permutes_bij', auto simp: to_nat_less_card to_nat_from_nat_id)
hence id: "?p2 = ?g  ?p1" by simp
have inj_g: "inj_on ?g ?p1"
unfolding inj_on_def
proof (intro ballI impI ext, auto)
fix p q i
assume p: "p permutes ?zn" and q: "q permutes ?zn"
and id: "(λ i. ?fn (p (?tn i))) = (λ i. ?fn (q (?tn i)))"
{
fix i
from permutes_in_image[OF p] have pi: "p (?tn i) < CARD('n)" by (simp add: to_nat_less_card)
from permutes_in_image[OF q] have qi: "q (?tn i) < CARD('n)" by (simp add: to_nat_less_card)
from fun_cong[OF id] have "?fn (p (?tn i))  = from_nat (q (?tn i))" .
from arg_cong[OF this, of ?tn] have "p (?tn i) = q (?tn i)"
by (simp add: to_nat_from_nat_id pi qi)
} note id = this
show "p i = q i"
proof (cases "i < CARD('n)")
case True
hence "?tn (?fn i) = i" by (simp add: to_nat_from_nat_id)
from id[of "?fn i", unfolded this] show ?thesis .
next
case False
thus ?thesis using p q unfolding permutes_def by simp
qed
qed
have mult_cong: "⋀ a b c d. a = b ⟹ c = d ⟹ a * c = b * d" by simp
have "sum (λ p.
signof p * (∏i∈?zn. a $h ?fn i$h ?fn (p i))) ?p1
= sum (λ p. of_int (sign p) * (∏i∈UNIV. a $h i$h p i)) ?p2"
unfolding id sum.reindex[OF inj_g]
proof (rule sum.cong[OF refl], unfold mem_Collect_eq o_def, rule mult_cong)
fix p
assume p: "p permutes ?zn"
let ?q = "λ i. ?fn (p (?tn i))"
from id p have q: "?q permutes ?U" by auto
from p have pp: "permutation p" unfolding permutation_permutes by auto
let ?ft = "λ p i. ?fn (p (?tn i))"
have fin: "finite ?zn" by simp
have "sign p = sign ?q ∧ p permutes ?zn"
using p fin proof (induction rule: permutes_induct)
case id
show ?case by (auto simp: sign_id[unfolded id_def] permutes_id[unfolded id_def])
next
case (swap a b p)
then have ‹permutation p›
using permutes_imp_permutation by blast
let ?sab = "Fun.swap a b id"
let ?sfab = "Fun.swap (?fn a) (?fn b) id"
have p_sab: "permutation ?sab" by (rule permutation_swap_id)
have p_sfab: "permutation ?sfab" by (rule permutation_swap_id)
from swap(4) have IH1: "p permutes ?zn" and IH2: "sign p = sign (?ft p)" by auto
have sab_perm: "?sab permutes ?zn" using swap(1-2) by (rule permutes_swap_id)
from permutes_compose[OF IH1 this] have perm1: "?sab o p permutes ?zn" .
from IH1 have p_p1: "p ∈ ?p1" by simp
hence "?ft p ∈ ?ft  ?p1" by (rule imageI)
from this[folded id] have "?ft p permutes ?U" by simp
hence p_ftp: "permutation (?ft p)" unfolding permutation_permutes by auto
{
fix a b
assume a: "a ∈ ?zn" and b: "b ∈ ?zn"
hence "(?fn a = ?fn b) = (a = b)" using swap(1-2)
} note inj = this
from inj[OF swap(1-2)] have id2: "sign ?sfab = sign ?sab" unfolding sign_swap_id by simp
have id: "?ft (Fun.swap a b id ∘ p) = Fun.swap (?fn a) (?fn b) id ∘ ?ft p"
proof
fix c
show "?ft (Fun.swap a b id ∘ p) c = (Fun.swap (?fn a) (?fn b) id ∘ ?ft p) c"
proof (cases "p (?tn c) = a ∨ p (?tn c) = b")
case True
thus ?thesis by (cases, auto simp add: o_def swap_id_eq)
next
case False
hence neq: "p (?tn c) ≠ a" "p (?tn c) ≠ b" by auto
have pc: "p (?tn c) ∈ ?zn" unfolding permutes_in_image[OF IH1]
from neq[folded inj[OF pc swap(1)] inj[OF pc swap(2)]]
have "?fn (p (?tn c)) ≠ ?fn a" "?fn (p (?tn c)) ≠ ?fn b" .
with neq show ?thesis by (auto simp: o_def swap_id_eq)
qed
qed
show ?case unfolding IH2 id sign_compose[OF p_sab ‹permutation p›] sign_compose[OF p_sfab p_ftp] id2
by (rule conjI[OF refl perm1])
qed
thus "signof p = of_int (sign ?q)" unfolding signof_def sign_def by auto
show "(∏i = 0..<CARD('n). a $h ?fn i$h ?fn (p i)) =
(∏i∈UNIV. a $h i$h ?q i)" unfolding
range_to_nat[symmetric] prod.reindex[OF inj_to_nat]
by (rule prod.cong[OF refl], unfold o_def, simp)
qed
}
thus ?thesis unfolding HMA_M_def
by (auto simp: from_hma⇩m_def Determinant.det_def det_def)
qed

lemma HMA_mat[transfer_rule]: "((=) ===> HMA_M) (λ k. k ⋅⇩m 1⇩m CARD('n))
(Finite_Cartesian_Product.mat :: 'a::semiring_1 ⇒ 'a^'n :: mod_type^'n :: mod_type)"
unfolding Finite_Cartesian_Product.mat_def[abs_def] rel_fun_def HMA_M_def
by (auto simp: from_hma⇩m_def from_nat_inj)

lemma HMA_mat_minus[transfer_rule]: "(HMA_M ===> HMA_M ===> HMA_M)
(λ A B. A + map_mat uminus B) ((-) :: 'a :: group_add ^'nc:: mod_type^'nr:: mod_type
⇒ 'a^'nc:: mod_type^'nr:: mod_type ⇒ 'a^'nc:: mod_type^'nr:: mod_type)"
unfolding rel_fun_def HMA_M_def from_hma⇩m_def by auto

lemma HMA_transpose_matrix [transfer_rule]:
"(HMA_M ===> HMA_M) transpose_mat transpose"
unfolding transpose_mat_def transpose_def HMA_M_def from_hma⇩m_def by auto

lemma HMA_invertible_matrix_mod_type[transfer_rule]:
"((Mod_Type_Connect.HMA_M :: _ ⇒ 'a :: comm_ring_1 ^ 'n :: mod_type ^ 'n :: mod_type
⇒ _) ===> (=)) invertible_mat invertible"
proof (intro rel_funI, goal_cases)
case (1 x y)
note rel_xy[transfer_rule] = "1"
have eq_dim: "dim_col x = dim_row x"
using Mod_Type_Connect.dim_col_transfer_rule Mod_Type_Connect.dim_row_transfer_rule rel_xy
by fastforce
moreover have "∃A'. y ** A' = mat 1 ∧ A' ** y = mat 1"
if xB: "x * B = 1⇩m (dim_row x)" and Bx: "B * x = 1⇩m (dim_row B)" for B
proof -
let ?A' = "Mod_Type_Connect.to_hma⇩m B:: 'a :: comm_ring_1 ^ 'n :: mod_type^ 'n :: mod_type"
have rel_BA[transfer_rule]: "Mod_Type_Connect.HMA_M B ?A'"
by (metis (no_types, lifting) Bx Mod_Type_Connect.HMA_M_def eq_dim carrier_mat_triv dim_col_mat(1)
Mod_Type_Connect.from_hma⇩m_def Mod_Type_Connect.from_hma_to_hma⇩m index_mult_mat(3)
index_one_mat(3) rel_xy xB)
have [simp]: "dim_row B = CARD('n)" using Mod_Type_Connect.dim_row_transfer_rule rel_BA by blast
have [simp]: "dim_row x = CARD('n)" using Mod_Type_Connect.dim_row_transfer_rule rel_xy by blast
have "y ** ?A' = mat 1" using xB by (transfer, simp)
moreover have "?A' ** y  = mat 1" using Bx by (transfer, simp)
ultimately show ?thesis by blast
qed
moreover have "∃B. x * B = 1⇩m (dim_row x) ∧ B * x = 1⇩m (dim_row B)"
if yA: "y ** A' = mat 1" and Ay: "A' ** y = mat 1" for A'
proof -
let ?B = "(Mod_Type_Connect.from_hma⇩m A')"
have [simp]: "dim_row x = CARD('n)" using rel_xy Mod_Type_Connect.dim_row_transfer_rule by blast
have [transfer_rule]: "Mod_Type_Connect.HMA_M ?B A'" by (simp add: Mod_Type_Connect.HMA_M_def)
hence [simp]: "dim_row ?B = CARD('n)" using dim_row_transfer_rule by auto
have "x * ?B = 1⇩m (dim_row x)" using yA by (transfer', auto)
moreover have "?B * x = 1⇩m (dim_row ?B)" using Ay by (transfer', auto)
ultimately show ?thesis by auto
qed
ultimately show ?case unfolding invertible_mat_def invertible_def inverts_mat_def by auto
qed

end

text ‹Some transfer rules for relating the elementary operations are also proved.›

context
includes lifting_syntax
begin

lemma HMA_swaprows[transfer_rule]:
"((Mod_Type_Connect.HMA_M :: _ ⇒ 'a :: comm_ring_1 ^ 'nc :: mod_type ^ 'nr :: mod_type ⇒ _)
===> (Mod_Type_Connect.HMA_I :: _ ⇒'nr :: mod_type ⇒ _ )
===> (Mod_Type_Connect.HMA_I :: _ ⇒'nr :: mod_type ⇒ _ )
===> Mod_Type_Connect.HMA_M)
(λA a b. swaprows a b A) interchange_rows"
by (intro rel_funI, goal_cases, auto simp add: Mod_Type_Connect.HMA_M_def interchange_rows_def)
(rule eq_matI, auto simp add: Mod_Type_Connect.from_hma⇩m_def Mod_Type_Connect.HMA_I_def
to_nat_less_card to_nat_from_nat_id)

lemma HMA_swapcols[transfer_rule]:
"((Mod_Type_Connect.HMA_M :: _ ⇒ 'a :: comm_ring_1 ^ 'nc :: mod_type ^ 'nr :: mod_type ⇒ _)
===> (Mod_Type_Connect.HMA_I :: _ ⇒'nc :: mod_type ⇒ _ )
===> (Mod_Type_Connect.HMA_I :: _ ⇒'nc :: mod_type ⇒ _ )
===> Mod_Type_Connect.HMA_M)
(λA a b. swapcols a b A) interchange_columns"
by (intro rel_funI, goal_cases, auto simp add: Mod_Type_Connect.HMA_M_def interchange_columns_def)
(rule eq_matI, auto simp add: Mod_Type_Connect.from_hma⇩m_def Mod_Type_Connect.HMA_I_def
to_nat_less_card to_nat_from_nat_id)

"((Mod_Type_Connect.HMA_M :: _ ⇒ 'a :: comm_ring_1 ^ 'nc :: mod_type ^ 'nr :: mod_type ⇒ _)
===> (Mod_Type_Connect.HMA_I :: _ ⇒'nr :: mod_type ⇒ _ )
===> (Mod_Type_Connect.HMA_I :: _ ⇒'nr :: mod_type ⇒ _ )
===> (=)
===> Mod_Type_Connect.HMA_M)
(rule eq_matI, auto simp add: Mod_Type_Connect.from_hma⇩m_def Mod_Type_Connect.HMA_I_def
to_nat_less_card to_nat_from_nat_id)

"((Mod_Type_Connect.HMA_M :: _ ⇒ 'a :: comm_ring_1 ^ 'nc :: mod_type ^ 'nr :: mod_type ⇒ _)
===> (Mod_Type_Connect.HMA_I :: _ ⇒'nc :: mod_type ⇒ _ )
===> (Mod_Type_Connect.HMA_I :: _ ⇒'nc :: mod_type ⇒ _ )
===> (=)
===> Mod_Type_Connect.HMA_M)
(rule eq_matI, auto simp add: Mod_Type_Connect.from_hma⇩m_def Mod_Type_Connect.HMA_I_def
to_nat_less_card to_nat_from_nat_id)

lemma HMA_multrow[transfer_rule]:
"((Mod_Type_Connect.HMA_M :: _ ⇒ 'a :: comm_ring_1 ^ 'nc :: mod_type ^ 'nr :: mod_type ⇒ _)
===> (Mod_Type_Connect.HMA_I :: _ ⇒'nr :: mod_type ⇒ _ )
===> (=)
===> Mod_Type_Connect.HMA_M)
(λA i q. multrow i q A) mult_row"
by (intro rel_funI, goal_cases, auto simp add: Mod_Type_Connect.HMA_M_def mult_row_def)
(rule eq_matI, auto simp add: Mod_Type_Connect.from_hma⇩m_def Mod_Type_Connect.HMA_I_def
to_nat_less_card to_nat_from_nat_id)

lemma HMA_multcol[transfer_rule]:
"((Mod_Type_Connect.HMA_M :: _ ⇒ 'a :: comm_ring_1 ^ 'nc :: mod_type ^ 'nr :: mod_type ⇒ _)
===> (Mod_Type_Connect.HMA_I :: _ ⇒'nc :: mod_type ⇒ _ )
===> (=)
===> Mod_Type_Connect.HMA_M)
(λA i q. multcol i q A) mult_column"
by (intro rel_funI, goal_cases, auto simp add: Mod_Type_Connect.HMA_M_def mult_column_def)
(rule eq_matI, auto simp add: Mod_Type_Connect.from_hma⇩m_def Mod_Type_Connect.HMA_I_def
to_nat_less_card to_nat_from_nat_id)

end

fun HMA_M3 where
"HMA_M3 (P,A,Q)
(P' :: 'a :: comm_ring_1 ^ 'nr :: mod_type ^ 'nr :: mod_type,
A' :: 'a ^ 'nc :: mod_type ^ 'nr :: mod_type,
Q' :: 'a ^ 'nc :: mod_type ^ 'nc :: mod_type) =
(Mod_Type_Connect.HMA_M P P' ∧ Mod_Type_Connect.HMA_M A A' ∧ Mod_Type_Connect.HMA_M Q Q')"

lemma HMA_M3_def:
"HMA_M3 A B = (Mod_Type_Connect.HMA_M (fst A) (fst B)
∧ Mod_Type_Connect.HMA_M (fst (snd A)) (fst (snd B))
∧ Mod_Type_Connect.HMA_M (snd (snd A)) (snd (snd B)))"
by (smt HMA_M3.simps prod.collapse)

context
includes lifting_syntax
begin

lemma Domainp_HMA_M3 [transfer_domain_rule]:
"Domainp (HMA_M3 :: _⇒(_×('a::comm_ring_1^'nc::mod_type^'nr::mod_type)×_)⇒_)
= (λ(P,A,Q). P ∈ carrier_mat CARD('nr) CARD('nr) ∧ A ∈ carrier_mat CARD('nr) CARD('nc)
∧ Q ∈ carrier_mat CARD('nc) CARD('nc))"
proof -
let ?HMA_M3 = "HMA_M3::_⇒(_×('a::comm_ring_1^'nc::mod_type^'nr::mod_type)×_)⇒_"
have 1: "P ∈ carrier_mat CARD('nr) CARD('nr) ∧
A ∈ carrier_mat CARD('nr) CARD('nc) ∧ Q ∈ carrier_mat CARD('nc) CARD('nc)"
if "Domainp ?HMA_M3 (P,A,Q)" for P A Q
using that unfolding Domainp_iff by (auto simp add: Mod_Type_Connect.HMA_M_def)
have 2: "Domainp ?HMA_M3 (P,A,Q)" if PAQ: "P ∈ carrier_mat CARD('nr) CARD('nr)
∧ A ∈ carrier_mat CARD('nr) CARD('nc) ∧Q ∈ carrier_mat CARD('nc) CARD('nc)" for P A Q
proof -
let ?P = "Mod_Type_Connect.to_hma⇩m P::'a^'nr::mod_type^'nr::mod_type"
let ?A = "Mod_Type_Connect.to_hma⇩m A::'a^'nc::mod_type^'nr::mod_type"
let ?Q = "Mod_Type_Connect.to_hma⇩m Q::'a^'nc::mod_type^'nc::mod_type"
have "HMA_M3 (P,A,Q) (?P,?A,?Q)"
by (auto simp add: Mod_Type_Connect.HMA_M_def PAQ)
thus ?thesis unfolding Domainp_iff by auto
qed
have "fst x ∈ carrier_mat CARD('nr) CARD('nr) ∧ fst (snd x) ∈ carrier_mat CARD('nr) CARD('nc)
∧ (snd (snd x)) ∈ carrier_mat CARD('nc) CARD('nc)"
if "Domainp ?HMA_M3 x" for x using 1
by (metis (full_types) surjective_pairing that)
moreover have "Domainp ?HMA_M3 x"
if "fst x ∈ carrier_mat CARD('nr) CARD('nr) ∧ fst (snd x) ∈ carrier_mat CARD('nr) CARD('nc)
∧ (snd (snd x)) ∈ carrier_mat CARD('nc) CARD('nc)" for x
using 2
by (metis (full_types) surjective_pairing that)
ultimately show ?thesis by (intro ext iffI, unfold split_beta, metis+)
qed

lemma bi_unique_HMA_M3 [transfer_rule]: "bi_unique HMA_M3" "left_unique HMA_M3" "right_unique HMA_M3"
unfolding HMA_M3_def bi_unique_def left_unique_def right_unique_def

lemma right_total_HMA_M3 [transfer_rule]: "right_total HMA_M3"
unfolding HMA_M_def right_total_def

end

(*
TODO: add more theorems to connect everything from HA to JNF in this setting.
*)
end


# Theory SNF_Missing_Lemmas

(*
Author: Jose Divasón
Email:  jose.divason@unirioja.es
*)

section ‹Missing results›

theory SNF_Missing_Lemmas
imports
Hermite.Hermite
Mod_Type_Connect
Jordan_Normal_Form.DL_Rank_Submatrix
"List-Index.List_Index"
begin

text ‹This theory presents some missing lemmas that are required for the Smith normal form
development. Some of them could be added to different AFP entries, such as the Jordan Normal
Form AFP entry by Ren\'e Thiemann and Akihisa Yamada.

However, not all the lemmas can be added directly, since some imports are required.›

hide_const (open) C
hide_const (open) measure

subsection ‹Miscellaneous lemmas›

lemma sum_two_rw: "(∑i = 0..<2. f i) = (∑i ∈ {0,1::nat}. f i)"
by (rule sum.cong, auto)

lemma sum_common_left:
fixes f::"'a ⇒ 'b::comm_ring_1"
assumes "finite A"
shows "sum (λi. c * f i) A = c * sum f A"

lemma prod3_intro:
assumes "fst A = a" and "fst (snd A) = b" and "snd (snd A) = c"
shows "A = (a,b,c)" using assms by auto

subsection ‹Transfer rules for the HMA\_Connect file of the Perron-Frobenius development›

hide_const (open) HMA_M HMA_I to_hma⇩m from_hma⇩m
hide_fact (open) from_hma⇩m_def from_hma_to_hma⇩m HMA_M_def HMA_I_def dim_row_transfer_rule
dim_col_transfer_rule

context
includes lifting_syntax
begin

lemma HMA_invertible_matrix[transfer_rule]:
"((HMA_Connect.HMA_M :: _ ⇒ 'a :: comm_ring_1 ^ 'n ^ 'n ⇒ _) ===> (=)) invertible_mat invertible"
proof (intro rel_funI, goal_cases)
case (1 x y)
note rel_xy[transfer_rule] = "1"
have eq_dim: "dim_col x = dim_row x"
using HMA_Connect.dim_col_transfer_rule HMA_Connect.dim_row_transfer_rule rel_xy
by fastforce
moreover have "∃A'. y ** A' = Finite_Cartesian_Product.mat 1 ∧ A' ** y = Finite_Cartesian_Product.mat 1"
if xB: "x * B = 1⇩m (dim_row x)" and Bx: "B * x = 1⇩m (dim_row B)" for B
proof -
let ?A' = "HMA_Connect.to_hma⇩m B:: 'a :: comm_ring_1 ^ 'n ^ 'n"
have rel_BA[transfer_rule]: "HMA_M B ?A'"
by (metis (no_types, lifting) Bx HMA_M_def eq_dim carrier_mat_triv dim_col_mat(1)
from_hma⇩m_def from_hma_to_hma⇩m index_mult_mat(3) index_one_mat(3) rel_xy xB)
have [simp]: "dim_row B = CARD('n)" using dim_row_transfer_rule rel_BA by blast
have [simp]: "dim_row x = CARD('n)" using dim_row_transfer_rule rel_xy by blast
have "y ** ?A' = Finite_Cartesian_Product.mat 1" using xB by (transfer, simp)
moreover have "?A' ** y  = Finite_Cartesian_Product.mat 1" using Bx by (transfer, simp)
ultimately show ?thesis by blast
qed
moreover have "∃B. x * B = 1⇩m (dim_row x) ∧ B * x = 1⇩m (dim_row B)"
if yA: "y ** A' = Finite_Cartesian_Product.mat 1" and Ay: "A' ** y = Finite_Cartesian_Product.mat 1" for A'
proof -
let ?B = "(from_hma⇩m A')"
have [simp]: "dim_row x = CARD('n)" using dim_row_transfer_rule rel_xy by blast
have [transfer_rule]: "HMA_M ?B A'" by (simp add: HMA_M_def)
hence [simp]: "dim_row ?B = CARD('n)" using dim_row_transfer_rule by auto
have "x * ?B = 1⇩m (dim_row x)" using yA by (transfer', auto)
moreover have "?B * x = 1⇩m (dim_row ?B)" using Ay by (transfer', auto)
ultimately show ?thesis by auto
qed
ultimately show ?case unfolding invertible_mat_def invertible_def inverts_mat_def by auto
qed
end

subsection ‹Lemmas obtained from HOL Analysis using local type definitions›

thm Cartesian_Space.invertible_mult (*In HOL Analysis*)
thm invertible_iff_is_unit (*In HOL Analysis*)
thm det_non_zero_imp_unit (*In JNF, but only for fields*)
thm mat_mult_left_right_inverse (*In JNF, but only for fields*)

lemma invertible_mat_zero:
assumes A: "A ∈ carrier_mat 0 0"
shows "invertible_mat A"
using A unfolding invertible_mat_def inverts_mat_def one_mat_def times_mat_def scalar_prod_def
Matrix.row_def col_def carrier_mat_def
by (auto, metis (no_types, lifting) cong_mat not_less_zero)

lemma invertible_mult_JNF:
fixes A::"'a::comm_ring_1 mat"
assumes A: "A∈carrier_mat n n" and B: "B∈carrier_mat n n"
and inv_A: "invertible_mat A" and inv_B: "invertible_mat B"
shows "invertible_mat (A*B)"
proof (cases "n = 0")
case True
then show ?thesis using assms
next
case False
then show ?thesis using
invertible_mult[where ?'a="'a::comm_ring_1", where ?'b="'n::finite", where ?'c="'n::finite",
where ?'d="'n::finite", untransferred, cancel_card_constraint, OF assms] by auto
qed

lemma invertible_iff_is_unit_JNF:
assumes A: "A ∈ carrier_mat n n"
shows "invertible_mat A ⟷ (Determinant.det A) dvd 1"
proof (cases "n=0")
case True
then show ?thesis using det_dim_zero invertible_mat_zero A by auto
next
case False
then show ?thesis using invertible_iff_is_unit[untransferred, cancel_card_constraint] A by auto
qed

subsection ‹Lemmas about matrices, submatrices and determinants›

(*This is a generalization of thm mat_mult_left_right_inverse*)
thm mat_mult_left_right_inverse
lemma mat_mult_left_right_inverse:
fixes A :: "'a::comm_ring_1 mat"
assumes A: "A ∈ carrier_mat n n"
and B: "B ∈ carrier_mat n n" and AB: "A * B = 1⇩m n"
shows "B * A = 1⇩m n"
proof -
have "Determinant.det (A * B) = Determinant.det (1⇩m n)" using AB by auto
hence "Determinant.det A * Determinant.det B = 1"
using Determinant.det_mult[OF A B] det_one by auto
hence det_A: "(Determinant.det A) dvd 1" and det_B: "(Determinant.det B) dvd 1"
using dvd_triv_left dvd_triv_right by metis+
hence inv_A: "invertible_mat A" and inv_B: "invertible_mat B"
using A B invertible_iff_is_unit_JNF by blast+
obtain B' where inv_BB': "inverts_mat B B'" and inv_B'B: "inverts_mat B' B"
using inv_B unfolding invertible_mat_def by auto
have B'_carrier: "B' ∈ carrier_mat n n"
by (metis B inv_B'B inv_BB' carrier_matD(1) carrier_matD(2) carrier_mat_triv
index_mult_mat(3) index_one_mat(3) inverts_mat_def)
have "B * A * B = B" using A AB B by auto
hence "B * A * (B * B') = B * B'"
by (smt A AB B B'_carrier assoc_mult_mat carrier_matD(1) inv_BB' inverts_mat_def one_carrier_mat)
thus ?thesis
by (metis A B carrier_matD(1) carrier_matD(2) index_mult_mat(3) inv_BB'
inverts_mat_def right_mult_one_mat')
qed

context comm_ring_1
begin

lemma col_submatrix_UNIV:
assumes "j < card {i. i < dim_col A ∧ i ∈ J}"
shows "col (submatrix A UNIV J) j = col A (pick J j)"
proof (rule eq_vecI)
show dim_eq:"dim_vec (col (submatrix A UNIV J) j) = dim_vec (col A (pick J j))"
fix i assume "i < dim_vec (col A (pick J j))"
show "col (submatrix A UNIV J) j $v i = col A (pick J j)$v i"
by (smt Collect_cong assms col_def dim_col dim_eq dim_submatrix(1)
eq_vecI index_vec pick_UNIV submatrix_index)
qed

lemma submatrix_split2: "submatrix A I J = submatrix (submatrix A I UNIV) UNIV J" (is "?lhs = ?rhs")
proof (rule eq_matI)
show dr: "dim_row ?lhs = dim_row ?rhs"
show dc: "dim_col ?lhs = dim_col ?rhs"
fix i j assume i: "i < dim_row ?rhs"
and j: "j < dim_col ?rhs"
have "?rhs $$(i, j) = (submatrix A I UNIV)$$ (pick UNIV i, pick J j)"
proof (rule submatrix_index)
show "i < card {i. i < dim_row (submatrix A I UNIV) ∧ i ∈ UNIV}"
by (metis (full_types) dim_submatrix(1) i)
show "j < card {j. j < dim_col (submatrix A I UNIV) ∧ j ∈ J}"
by (metis (full_types) dim_submatrix(2) j)
qed
also have "... = A $$(pick I (pick UNIV i), pick UNIV (pick J j))" proof (rule submatrix_index) show "pick UNIV i < card {i. i < dim_row A ∧ i ∈ I}" by (metis (full_types) dr dim_submatrix(1) i pick_UNIV) show "pick J j < card {j. j < dim_col A ∧ j ∈ UNIV}" by (metis (full_types) dim_submatrix(2) j pick_le) qed also have "... = ?lhs$$ (i,j)"
proof (unfold pick_UNIV, rule submatrix_index[symmetric])
show "i < card {i. i < dim_row A ∧ i ∈ I}"
by (metis (full_types) dim_submatrix(1) dr i)
show "j < card {j. j < dim_col A ∧ j ∈ J}"
by (metis (full_types) dim_submatrix(2) dc j)
qed
finally show "?lhs $$(i, j) = ?rhs$$ (i, j)" ..
qed

lemma submatrix_mult:
"submatrix (A*B) I J = submatrix A I UNIV * submatrix B UNIV J" (is "?lhs = ?rhs")
proof (rule eq_matI)
show "dim_row ?lhs = dim_row ?rhs" unfolding submatrix_def by auto
show "dim_col ?lhs = dim_col ?rhs" unfolding submatrix_def by auto
fix i j assume i: "i < dim_row ?rhs" and j: "j < dim_col ?rhs"
have i1: "i < card {i. i < dim_row (A * B) ∧ i ∈ I}"
by (metis (full_types) dim_submatrix(1) i index_mult_mat(2))
have j1: "j < card {j. j < dim_col (A * B) ∧ j ∈ J}"
by (metis dim_submatrix(2) index_mult_mat(3) j)
have pi: "pick I i < dim_row A" using i1 pick_le by auto
have pj: "pick J j < dim_col B" using j1 pick_le by auto
have row_rw: "Matrix.row (submatrix A I UNIV) i = Matrix.row A (pick I i)"
using i1 row_submatrix_UNIV by auto
have col_rw: "col (submatrix B UNIV J) j = col B (pick J j)" using j1 col_submatrix_UNIV by auto
have "?lhs $$(i,j) = (A*B)$$ (pick I i, pick J j)" by (rule submatrix_index[OF i1 j1])
also have "... = Matrix.row A (pick I i) ∙ col B (pick J j)" by (rule index_mult_mat(1)[OF pi pj])
also have "... = Matrix.row (submatrix A I UNIV) i ∙ col (submatrix B UNIV J) j"
using row_rw col_rw by simp
also have "... = (?rhs) $$(i,j)" by (rule index_mult_mat[symmetric], insert i j, auto) finally show "?lhs$$ (i, j) = ?rhs $$(i, j)" . qed lemma det_singleton: assumes A: "A ∈ carrier_mat 1 1" shows "det A = A$$ (0,0)"
using A unfolding carrier_mat_def Determinant.det_def by auto

lemma submatrix_singleton_index:
assumes A: "A ∈ carrier_mat n m"
and an: "a < n" and bm: "b < m"
shows "submatrix A {a} {b} $$(0,0) = A$$ (a,b)"
proof -
have a: "{i. i = a ∧ i < dim_row A} = {a}" using an A unfolding carrier_mat_def by auto
have b: "{i. i = b ∧ i < dim_col A} = {b}" using bm A unfolding carrier_mat_def by auto
have "submatrix A {a} {b} $$(0,0) = A$$ (pick {a} 0,pick {b} 0)"
by (rule submatrix_index, insert a b, auto)
moreover have "pick {a} 0 = a" by (auto, metis (full_types) LeastI)
moreover have "pick {b} 0 = b" by (auto, metis (full_types) LeastI)
ultimately show ?thesis by simp
qed
end

lemma det_not_inj_on:
assumes not_inj_on: "¬ inj_on f {0..<n}"
shows "det (mat⇩r n n (λi. Matrix.row B (f i))) = 0"
proof -
obtain i j where i: "i<n" and j: "j<n" and fi_fj: "f i = f j" and ij: "i≠j"
using not_inj_on unfolding inj_on_def by auto
show ?thesis
proof (rule det_identical_rows[OF _ ij i j])
let ?B="(mat⇩r n n (λi. row B (f i)))"
show "row ?B i = row ?B j"
proof (rule eq_vecI, auto)
fix ia assume ia: "ia < n"
have "row ?B i $ia = ?B $$(i, ia)" by (rule index_row(1), insert i ia, auto) also have "... = ?B$$ (j, ia)" by (simp add: fi_fj i ia j) also have "... = row ?B j$ ia" by (rule index_row(1)[symmetric], insert j ia, auto)
finally show "row ?B i $ia = row (mat⇩r n n (λi. row B (f i))) j$ ia" by simp
qed
show "mat⇩r n n (λi. Matrix.row B (f i)) ∈ carrier_mat n n" by auto
qed
qed

lemma mat_row_transpose: "(mat⇩r nr nc f)⇧T = mat nc nr (λ(i,j). vec_index (f j) i)"
by (rule eq_matI, auto)

lemma obtain_inverse_matrix:
assumes A: "A ∈ carrier_mat n n" and i: "invertible_mat A"
obtains B where "inverts_mat A B" and "inverts_mat B A" and "B ∈ carrier_mat n n"
proof -
have "(∃B. inverts_mat A B ∧ inverts_mat B A)" using i unfolding invertible_mat_def by auto
from this obtain B where AB: "inverts_mat A B" and BA: "inverts_mat B A" by auto
moreover have "B ∈ carrier_mat n n" using A AB BA unfolding carrier_mat_def inverts_mat_def
by (auto, metis index_mult_mat(3) index_one_mat(3))+
ultimately show ?thesis using that by blast
qed

lemma invertible_mat_smult_mat:
fixes A :: "'a::comm_ring_1 mat"
assumes inv_A: "invertible_mat A" and k: "k dvd 1"
shows "invertible_mat (k ⋅⇩m A)"
proof -
obtain n where A: "A ∈ carrier_mat n n" using inv_A unfolding invertible_mat_def by auto
have det_dvd_1: "Determinant.det A dvd 1" using inv_A invertible_iff_is_unit_JNF[OF A] by auto
have "Determinant.det (k ⋅⇩m A) = k ^ dim_col A * Determinant.det A" by simp
also have "... dvd 1" by (rule unit_prod, insert k det_dvd_1 dvd_power_same, force+)
finally show ?thesis using invertible_iff_is_unit_JNF by (metis A smult_carrier_mat)
qed

lemma invertible_mat_one[simp]: "invertible_mat (1⇩m n)"
unfolding invertible_mat_def using inverts_mat_def by fastforce

lemma four_block_mat_dim0:
assumes A: "A ∈ carrier_mat n n"
and B: "B ∈ carrier_mat n 0"
and C: "C ∈ carrier_mat 0 n"
and D: "D ∈ carrier_mat 0 0"
shows "four_block_mat A B C D = A"
unfolding four_block_mat_def using assms by auto

lemma det_four_block_mat_lower_right_id:
assumes A: "A ∈ carrier_mat m m"
and B: "B = 0⇩m m (n-m)"
and C: "C = 0⇩m (n-m) m"
and D: "D = 1⇩m (n-m)"
and "n>m"
shows "Determinant.det (four_block_mat A B C D) = Determinant.det A"
using assms
proof (induct n arbitrary: A B C D)
case 0
then show ?case by auto
next
case (Suc n)
let ?block = "(four_block_mat A B C D)"
let ?B = "Matrix.mat m (n-m) (λ(i,j). 0)"
let ?C = "Matrix.mat (n-m) m (λ(i,j). 0)"
let ?D = "1⇩m (n-m)"
have mat_eq: "(mat_delete ?block n n) = four_block_mat A ?B ?C ?D" (is "?lhs = ?rhs")
proof (rule eq_matI)
fix i j assume i: "i < dim_row (four_block_mat A ?B ?C ?D)"
and j: "j < dim_col (four_block_mat A ?B ?C ?D)"
let ?f = " (if i < dim_row A then if j < dim_col A then A $$(i, j) else B$$ (i, j - dim_col A)
else if j < dim_col A then C $$(i - dim_row A, j) else D$$ (i - dim_row A, j - dim_col A))"
let ?g = "(if i < dim_row A then if j < dim_col A then A $$(i, j) else ?B$$ (i, j - dim_col A)
else if j < dim_col A then ?C $$(i - dim_row A, j) else ?D$$ (i - dim_row A, j - dim_col A))"
have "(mat_delete ?block n n) $$(i,j) = ?block$$ (i,j)"
using i j Suc.prems unfolding mat_delete_def by auto
also have "... = ?f"
by (rule index_mat_four_block, insert Suc.prems i j, auto)
also have "... = ?g" using i j Suc.prems by auto
also have "... = four_block_mat A ?B ?C ?D $$(i,j)" by (rule index_mat_four_block[symmetric], insert Suc.prems i j, auto) finally show "?lhs$$ (i,j) = ?rhs $$(i,j)" . qed (insert Suc.prems, auto) have nn_1: "?block$$ (n, n) = 1" using Suc.prems by auto
have rw0: "(∑i<n. ?block $$(i,n) * Determinant.cofactor ?block i n) = 0" proof (rule sum.neutral, rule) fix x assume x: "x ∈ {..<n}" have block_index: "?block$$ (x,n) = (if x < dim_row A then if n < dim_col A then A $$(x, n) else B$$ (x, n - dim_col A) else if n < dim_col A then C $$(x - dim_row A, n) else D$$ (x - dim_row A, n - dim_col A))"
by (rule index_mat_four_block, insert Suc.prems x, auto)
have "four_block_mat A B C D $$(x,n) = 0" using x Suc.prems by auto thus "four_block_mat A B C D$$ (x, n) * Determinant.cofactor (four_block_mat A B C D) x n = 0"
by simp
qed
have "Determinant.det ?block = (∑i<Suc n. ?block $$(i, n) * Determinant.cofactor ?block i n)" by (rule laplace_expansion_column, insert Suc.prems, auto) also have "... = ?block$$ (n, n) * Determinant.cofactor ?block n n
+ (∑i<n. ?block $$(i,n) * Determinant.cofactor ?block i n)" by simp also have "... = ?block$$ (n, n) * Determinant.cofactor ?block n n" using rw0 by auto
also have "... = Determinant.cofactor ?block n n" using nn_1 by simp
also have "... = Determinant.det (mat_delete ?block n n)" unfolding cofactor_def by auto
also have "... = Determinant.det (four_block_mat A ?B ?C ?D)" using mat_eq by simp
also have "... = Determinant.det A" (is "Determinant.det ?lhs = Determinant.det ?rhs")
proof (cases "n = m")
case True
have "?lhs = ?rhs" by (rule four_block_mat_dim0, insert Suc.prems True, auto)
then show ?thesis by simp
next
case False
show ?thesis by (rule Suc.hyps, insert Suc.prems False, auto)
qed
finally show ?case .
qed

lemma mult_eq_first_row:
assumes A: "A ∈ carrier_mat 1 n"
and B: "B ∈ carrier_mat m n"
and m0: "m ≠ 0"
and r: "Matrix.row A 0 = Matrix.row B 0"
shows "Matrix.row (A * V) 0 = Matrix.row (B * V) 0"
proof (rule eq_vecI)
show "dim_vec (Matrix.row (A * V) 0) = dim_vec (Matrix.row (B * V) 0)" using A B r by auto
fix i assume i: "i < dim_vec (Matrix.row (B * V) 0)"
have "Matrix.row (A * V) 0 $v i = (A * V) $$(0,i)" by (rule index_row, insert i A, auto) also have "... = Matrix.row A 0 ∙ col V i" by (rule index_mult_mat, insert A i, auto) also have "... = Matrix.row B 0 ∙ col V i" using r by auto also have "... = (B * V)$$ (0,i)" by (rule index_mult_mat[symmetric], insert m0 B i, auto) also have "... = Matrix.row (B * V) 0$v i" by (rule index_row[symmetric], insert i B m0, auto)
finally show "Matrix.row (A * V) 0 $v i = Matrix.row (B * V) 0$v i" .
qed

lemma smult_mat_mat_one_element:
assumes A: "A ∈ carrier_mat 1 1" and B: "B ∈ carrier_mat 1 n"
shows "A * B = A $$(0,0) ⋅⇩m B" proof (rule eq_matI) fix i j assume i: "i < dim_row (A$$ (0, 0) ⋅⇩m B)" and j: "j < dim_col (A $$(0, 0) ⋅⇩m B)" have i0: "i = 0" using A B i by auto have "(A * B)$$ (i, j) =  Matrix.row A i ∙ col B j"
by (rule index_mult_mat, insert i j A B, auto)
also have "... =  Matrix.row A i $v 0 * col B j$v 0" unfolding scalar_prod_def using B by auto
also have "... = A$$(i,i) * B$$(i,j)" using A i i0 j by auto
also have "... = (A $$(i, i) ⋅⇩m B)$$ (i, j)"
unfolding i by (rule index_smult_mat[symmetric], insert i j B, auto)
finally show "(A * B) $$(i, j) = (A$$ (0, 0) ⋅⇩m B) $$(i, j)" using i0 by simp qed (insert A B, auto) lemma determinant_one_element: assumes A: "A ∈ carrier_mat 1 1" shows "Determinant.det A = A$$ (0,0)"
proof -
have "Determinant.det A = prod_list (diag_mat A)"
by (rule det_upper_triangular[OF _ A], insert A, unfold upper_triangular_def, auto)
also have "... = A $$(0,0)" using A unfolding diag_mat_def by auto finally show ?thesis . qed lemma invertible_mat_transpose: assumes inv_A: "invertible_mat (A::'a::comm_ring_1 mat)" shows "invertible_mat A⇧T" proof - obtain n where A: "A ∈ carrier_mat n n" using inv_A unfolding invertible_mat_def square_mat.simps by auto hence At: "A⇧T ∈ carrier_mat n n" by simp have "Determinant.det A⇧T = Determinant.det A" by (metis Determinant.det_def Determinant.det_transpose carrier_matI index_transpose_mat(2) index_transpose_mat(3)) also have "... dvd 1" using invertible_iff_is_unit_JNF[OF A] inv_A by simp finally show ?thesis using invertible_iff_is_unit_JNF[OF At] by auto qed lemma dvd_elements_mult_matrix_left: assumes A: "(A::'a::comm_ring_1 mat) ∈ carrier_mat m n" and P: "P ∈ carrier_mat m m" and x: "(∀i j. i<m ∧ j<n ⟶ x dvd A$$(i,j))"
shows "(∀i j. i<m ∧ j<n ⟶ x dvd (P*A)$$(i,j))" proof - have "x dvd (P * A)$$ (i, j)" if i: "i < m" and j: "j < n" for i j
proof -
have "(P * A) $$(i, j) = (∑ia = 0..<m. Matrix.row P i v ia * col A j v ia)" unfolding times_mat_def scalar_prod_def using A P j i by auto also have "... = (∑ia = 0..<m. Matrix.row P i v ia * A$$ (ia,j))"
by (rule sum.cong, insert A j, auto)
also have "x dvd ..." using x by (meson atLeastLessThan_iff dvd_mult dvd_sum j)
finally show ?thesis .
qed
thus ?thesis by auto
qed

lemma dvd_elements_mult_matrix_right:
assumes A: "(A::'a::comm_ring_1 mat) ∈ carrier_mat m n"
and Q: "Q ∈ carrier_mat n n"
and x: "(∀i j. i<m ∧ j<n ⟶ x dvd A$$(i,j))" shows "(∀i j. i<m ∧ j<n ⟶ x dvd (A*Q)$$(i,j))"
proof -
have "x dvd (A*Q) $$(i, j)" if i: "i < m" and j: "j < n" for i j proof - have "(A*Q)$$ (i, j) =  (∑ia = 0..<n. Matrix.row A i $v ia * col Q j$v ia)"
unfolding times_mat_def scalar_prod_def using A Q j i by auto
also have "... = (∑ia = 0..<n. A $$(i, ia) * col Q j v ia)" by (rule sum.cong, insert A Q i, auto) also have "x dvd ..." using x by (meson atLeastLessThan_iff dvd_mult2 dvd_sum i) finally show ?thesis . qed thus ?thesis by auto qed lemma dvd_elements_mult_matrix_left_right: assumes A: "(A::'a::comm_ring_1 mat) ∈ carrier_mat m n" and P: "P ∈ carrier_mat m m" and Q: "Q ∈ carrier_mat n n" and x: "(∀i j. i<m ∧ j<n ⟶ x dvd A$$(i,j))"
shows "(∀i j. i<m ∧ j<n ⟶ x dvd (P*A*Q)$$(i,j))" using dvd_elements_mult_matrix_left[OF A P x] by (meson P A Q dvd_elements_mult_matrix_right mult_carrier_mat) definition append_cols :: "'a :: zero mat ⇒ 'a mat ⇒ 'a mat" (infixr "@⇩c" 65)where "A @⇩c B = four_block_mat A B (0⇩m 0 (dim_col A)) (0⇩m 0 (dim_col B))" lemma append_cols_carrier[simp,intro]: "A ∈ carrier_mat n a ⟹ B ∈ carrier_mat n b ⟹ (A @⇩c B) ∈ carrier_mat n (a+b)" unfolding append_cols_def by auto lemma append_cols_mult_left: assumes A: "A ∈ carrier_mat n a" and B: "B ∈ carrier_mat n b" and P: "P ∈ carrier_mat n n" shows "P * (A @⇩c B) = (P*A) @⇩c (P*B)" proof - let ?P = "four_block_mat P (0⇩m n 0) (0⇩m 0 n) (0⇩m 0 0)" have "P = ?P" by (rule eq_matI, auto) hence "P * (A @⇩c B) = ?P * (A @⇩c B)" by simp also have "?P * (A @⇩c B) = four_block_mat (P * A + 0⇩m n 0 * 0⇩m 0 (dim_col A)) (P * B + 0⇩m n 0 * 0⇩m 0 (dim_col B)) (0⇩m 0 n * A + 0⇩m 0 0 * 0⇩m 0 (dim_col A)) (0⇩m 0 n * B + 0⇩m 0 0 * 0⇩m 0 (dim_col B))" unfolding append_cols_def by (rule mult_four_block_mat, insert A B P, auto) also have "... = four_block_mat (P * A) (P * B) (0⇩m 0 (dim_col (P*A))) (0⇩m 0 (dim_col (P*B)))" by (rule cong_four_block_mat, insert P, auto) also have "... = (P*A) @⇩c (P*B)" unfolding append_cols_def by auto finally show ?thesis . qed lemma append_cols_mult_right_id: assumes A: "(A::'a::semiring_1 mat) ∈ carrier_mat n 1" and B: "B ∈ carrier_mat n (m-1)" and C: "C = four_block_mat (1⇩m 1) (0⇩m 1 (m - 1)) (0⇩m (m - 1) 1) D" and D: "D ∈ carrier_mat (m-1) (m-1)" shows "(A @⇩c B) * C = A @⇩c (B * D)" proof - let ?C = "four_block_mat (1⇩m 1) (0⇩m 1 (m - 1)) (0⇩m (m - 1) 1) D" have "(A @⇩c B) * C = (A @⇩c B) * ?C" unfolding C by auto also have "... = four_block_mat A B (0⇩m 0 (dim_col A)) (0⇩m 0 (dim_col B)) * ?C" unfolding append_cols_def by auto also have "... = four_block_mat (A * 1⇩m 1 + B * 0⇩m (m - 1) 1) (A * 0⇩m 1 (m - 1) + B * D) (0⇩m 0 (dim_col A) * 1⇩m 1 + 0⇩m 0 (dim_col B) * 0⇩m (m - 1) 1) (0⇩m 0 (dim_col A) * 0⇩m 1 (m - 1) + 0⇩m 0 (dim_col B) * D)" by (rule mult_four_block_mat, insert assms, auto) also have "... = four_block_mat A (B * D) (0⇩m 0 (dim_col A)) (0⇩m 0 (dim_col (B*D)))" by (rule cong_four_block_mat, insert assms, auto) also have "... = A @⇩c (B * D)" unfolding append_cols_def by auto finally show ?thesis . qed lemma append_cols_mult_right_id2: assumes A: "(A::'a::semiring_1 mat) ∈ carrier_mat n a" and B: "B ∈ carrier_mat n b" and C: "C = four_block_mat D (0⇩m a b) (0⇩m b a) (1⇩m b)" and D: "D ∈ carrier_mat a a" shows "(A @⇩c B) * C = (A * D) @⇩c B" proof - let ?C = "four_block_mat D (0⇩m a b) (0⇩m b a) (1⇩m b)" have "(A @⇩c B) * C = (A @⇩c B) * ?C" unfolding C by auto also have "... = four_block_mat A B (0⇩m 0 a) (0⇩m 0 b) * ?C" unfolding append_cols_def using A B by auto also have "... = four_block_mat (A * D + B * 0⇩m b a) (A * 0⇩m a b + B * 1⇩m b) (0⇩m 0 a * D + 0⇩m 0 b * 0⇩m b a) (0⇩m 0 a * 0⇩m a b + 0⇩m 0 b * 1⇩m b)" by (rule mult_four_block_mat, insert A B C D, auto) also have "... = four_block_mat (A * D) B (0⇩m 0 (dim_col (A*D))) (0⇩m 0 (dim_col B))" by (rule cong_four_block_mat, insert assms, auto) also have "... = (A * D) @⇩c B" unfolding append_cols_def by auto finally show ?thesis . qed lemma append_cols_nth: assumes A: "A ∈ carrier_mat n a" and B: "B ∈ carrier_mat n b" and i: "i<n" and j: "j < a + b" shows "(A @⇩c B)$$ (i, j) = (if j < dim_col A then A $$(i,j) else B$$(i,j-a))" (is "?lhs = ?rhs")
proof -
let ?C = "(0⇩m 0 (dim_col A))"
let ?D = "(0⇩m 0 (dim_col B))"
have i2: "i < dim_row A + dim_row ?D" using i A by auto
have j2: "j < dim_col A + dim_col (0⇩m 0 (dim_col B))" using j B A by auto
have "(A @⇩c B) $$(i, j) = four_block_mat A B ?C ?D$$ (i, j)"
unfolding append_cols_def by auto
also have "... = (if i < dim_row A then if j < dim_col A then A $$(i, j) else B$$ (i, j - dim_col A) else if j < dim_col A then ?C $$(i - dim_row A, j) else 0⇩m 0 (dim_col B)$$ (i - dim_row A, j - dim_col A))"
by (rule index_mat_four_block(1)[OF i2 j2])
also have "... = ?rhs" using i A by auto
finally show ?thesis .
qed

lemma append_cols_split:
assumes d: "dim_col A > 0"
shows "A = mat_of_cols (dim_row A) [col A 0] @⇩c
mat_of_cols (dim_row A) (map (col A) [1..<dim_col A])" (is "?lhs = ?A1 @⇩c ?A2")
proof (rule eq_matI)
fix i j assume i: "i < dim_row (?A1 @⇩c ?A2)" and j: "j < dim_col (?A1 @⇩c ?A2)"
have "(?A1 @⇩c ?A2) $$(i, j) = (if j < dim_col ?A1 then ?A1$$(i,j) else ?A2$$(i,j-(dim_col ?A1)))" by (rule append_cols_nth, insert i j, auto simp add: append_cols_def) also have "... = A$$ (i,j)"
proof (cases "j< dim_col ?A1")
case True
then show ?thesis
by (metis One_nat_def Suc_eq_plus1 add.right_neutral append_cols_def col_def i
index_mat_four_block(2) index_vec index_zero_mat(2) less_one list.size(3) list.size(4)
mat_of_cols_Cons_index_0 mat_of_cols_carrier(2) mat_of_cols_carrier(3))
next
case False
then show ?thesis
by (metis (no_types, lifting) Suc_eq_plus1 Suc_less_eq Suc_pred add_diff_cancel_right' append_cols_def
diff_zero i index_col index_mat_four_block(2) index_mat_four_block(3) index_zero_mat(2)
index_zero_mat(3) j length_map length_upt linordered_semidom_class.add_diff_inverse list.size(3)
list.size(4) mat_of_cols_carrier(2) mat_of_cols_carrier(3) mat_of_cols_index nth_map_upt
plus_1_eq_Suc upt_0)
qed
finally show "A $$(i, j) = (?A1 @⇩c ?A2)$$ (i, j)" ..
qed (auto simp add: append_cols_def d)

lemma append_rows_nth:
assumes A: "A ∈ carrier_mat a n"
and B: "B ∈ carrier_mat b n"
and i: "i<a+b" and j: "j < n"
shows "(A @⇩r B) $$(i, j) = (if i < dim_row A then A$$(i,j) else B$$(i-a,j))" (is "?lhs = ?rhs") proof - let ?C = "(0⇩m (dim_row A) 0)" let ?D = "(0⇩m (dim_row B) 0)" have i2: "i < dim_row A + dim_row ?D" using i j A B by auto have j2: "j < dim_col A + dim_col ?D" using i j A B by auto have "(A @⇩r B)$$ (i, j) = four_block_mat A ?C B ?D $$(i, j)" unfolding append_rows_def by auto also have "... = (if i < dim_row A then if j < dim_col A then A$$ (i, j) else ?C $$(i, j - dim_col A) else if j < dim_col A then B$$ (i - dim_row A, j) else ?D $$(i - dim_row A, j - dim_col A))" by (rule index_mat_four_block(1)[OF i2 j2]) also have "... = ?rhs" using i A j B by auto finally show ?thesis . qed lemma append_rows_split: assumes k: "k≤dim_row A" shows "A = (mat_of_rows (dim_col A) [Matrix.row A i. i ← [0..<k]]) @⇩r (mat_of_rows (dim_col A) [Matrix.row A i. i ← [k..<dim_row A]])" (is "?lhs = ?A1 @⇩r ?A2") proof (rule eq_matI) have "(?A1 @⇩r ?A2) ∈ carrier_mat (k + (dim_row A-k)) (dim_col A)" by (rule carrier_append_rows, insert k, auto) hence A1_A2: "(?A1 @⇩r ?A2) ∈ carrier_mat (dim_row A) (dim_col A)" using k by simp thus "dim_row A = dim_row (?A1 @⇩r ?A2)" and "dim_col A = dim_col (?A1 @⇩r ?A2)" by auto fix i j assume i: "i < dim_row (?A1 @⇩r ?A2)" and j: "j < dim_col (?A1 @⇩r ?A2)" have "(?A1 @⇩r ?A2)$$ (i, j) = (if i < dim_row ?A1 then ?A1 $$(i,j) else ?A2$$(i-(dim_row ?A1),j))"
by (rule append_rows_nth, insert k i j, auto simp add: append_rows_def)
also have "... = A $$(i,j)" proof (cases "i<dim_row ?A1") case True then show ?thesis by (metis (no_types, lifting) Matrix.row_def add.left_neutral add.right_neutral append_rows_def index_mat(1) index_mat_four_block(3) index_vec index_zero_mat(3) j length_map length_upt mat_of_rows_carrier(2,3) mat_of_rows_def nth_map_upt prod.simps(2)) next case False let ?xs = "(map (Matrix.row A) [k..<dim_row A])" have dim_row_A1: "dim_row ?A1 = k" by auto have "?A2$$ (i-k,j) = ?xs ! (i-k) $v j" by (rule mat_of_rows_index, insert i k False A1_A2 j, auto) also have "... = A $$(i,j)" using A1_A2 False i j by auto finally show ?thesis using A1_A2 False i j by auto qed finally show " A$$ (i, j) = (?A1 @⇩r ?A2)$\$ (i,j)" by simp
qed

lemma transpose_mat_append_rows:
assumes A: "A ∈ carrier_mat a n" and B: "B ∈ carrier_mat b n"
shows "(A @⇩r B)⇧T = A⇧T @⇩c B⇧T"
by (smt append_cols_def append_rows_def A B carrier_matD(1) index_transpose_mat(3)
transpose_four_block_mat zero_carrier_mat zero_transpose_mat)

lemma transpose_mat_append_cols:
assumes A: "A ∈ carrier_mat n a" and B: "B ∈ carrier_mat n b"
shows "(A @⇩c B)⇧T = A⇧T @⇩r B⇧T"
by (metis Matrix.transpose_transpose A B carrier_matD(1) carrier_mat_triv
index_transpose_mat(3) transpose_mat_append_rows)

lemma append_rows_mult_right:
assumes A: "(A::'a::comm_semiring_1 mat) ∈ carrier_mat a n" and B: "B ∈ carrier_mat b n"
and Q: "Q∈ carrier_mat n n"
shows "(A @⇩r B) * Q = (A * Q) @⇩r (B*Q)"
proof -
have "transpose_mat ((A @⇩r B) * Q) = Q⇧T * (A @⇩r B)⇧T"
by (rule transpose_mult, insert A B Q, auto)
also have "... = Q⇧T * (A⇧T @⇩c B⇧T)" using transpose_mat_append_rows assms by metis
also have "... = Q⇧T * A⇧T @⇩c Q⇧T * B⇧T"
using append_cols_mult_left assms by (metis transpose_carrier_mat)
also have "transpose_mat ... = (A * Q) @⇩r (B*Q)"
by (smt A B Matrix.transpose_mult Matrix.transpose_transpose append_cols_def append_rows_def Q
carrier_mat_triv index_mult_mat(2) index_transpose_mat(2) transpose_four_block`