Theory Hermite
section‹Hermite Normal Form›
theory Hermite
imports
Echelon_Form.Echelon_Form_Inverse
Echelon_Form.Examples_Echelon_Form_Abstract
"HOL-Computational_Algebra.Euclidean_Algorithm"
begin
subsection‹Some previous properties›
subsubsection‹Rings›
subclass (in bezout_ring_div) euclidean_ring
proof
qed
subsubsection‹Polynomials›
lemma coeff_dvd_poly: "[:coeff a (degree a):] dvd (a::'a::{field} poly)"
proof (cases "a=0")
case True
thus ?thesis unfolding dvd_def by simp
next
case False
thus ?thesis
by (intro dvd_trans[OF is_unit_triv one_dvd]) simp
qed
lemma poly_dvd_antisym2:
fixes p q :: "'a::field poly"
assumes dvd1: "p dvd q" and dvd2: "q dvd p"
shows "p div [:coeff p (degree p):] = q div [:coeff q (degree q):]"
proof (cases "p = 0")
case True
thus ?thesis
by (metis dvd1 dvd_0_left_iff)
next
case False have q: "q ≠ 0"
by (metis False dvd2 dvd_0_left_iff)
have degree: "degree p = degree q"
using ‹p dvd q› ‹q dvd p› ‹p ≠ 0› ‹q ≠ 0›
by (intro order_antisym dvd_imp_degree_le)
from ‹p dvd q› obtain a where a: "q = p * a" ..
with ‹q ≠ 0› have "a ≠ 0" by auto
with degree a ‹p ≠ 0› have "degree a = 0"
by (simp add: degree_mult_eq)
with a show ?thesis
proof (cases a, auto split: if_splits, metis ‹a ≠ 0›)
fix aa :: 'a
assume a1: "aa ≠ 0"
assume "q = smult aa p"
have "[:aa * coeff p (degree p):] dvd smult aa p"
using a1 by (metis (no_types) coeff_dvd_poly coeff_smult degree_smult_eq)
thus "p div [:coeff p (degree p):] = smult aa p div [:aa * coeff p (degree p):]"
using a1 by (simp add: False coeff_dvd_poly dvd_div_div_eq_mult)
qed
qed
subsubsection‹Units›
lemma unit_prod:
assumes "finite S"
shows "is_unit (prod (λi. U $ i $ i) S) = (∀i∈S. is_unit (U $ i $ i))"
using assms
proof (induct)
case empty
thus ?case by auto
next
case (insert a S)
have "prod (λi. U $ i $ i) (insert a S) = U $ a $ a * prod (λi. U $ i $ i) S"
by (simp add: insert.hyps(2))
thus ?case using is_unit_mult_iff insert.hyps by auto
qed
subsubsection‹Upper triangular matrices›
lemma is_unit_diagonal:
fixes U::"'a::{comm_ring_1, algebraic_semidom}^'n::{finite, wellorder}^'n::{finite, wellorder}"
assumes U: "upper_triangular U"
and det_U: "is_unit (det U)"
shows "∀i. is_unit (U $ i $ i)"
proof -
have "is_unit (prod (λi. U $ i $ i) UNIV)"
using det_U det_upperdiagonal[of U] U
unfolding upper_triangular_def by auto
hence "∀i∈UNIV. is_unit (U $ i $ i)" using unit_prod[of UNIV U] by simp
thus ?thesis by simp
qed
lemma upper_triangular_mult:
fixes A::"'a::{semiring_1}^'n::{mod_type}^'n::{mod_type}"
assumes A: "upper_triangular A"
and B: "upper_triangular B"
shows "upper_triangular (A**B)"
proof (unfold upper_triangular_def matrix_matrix_mult_def, vector, auto)
fix i j::'n
assume ji: "j<i"
show "(∑k∈UNIV. A $ i $ k * B $ k $ j) = 0"
proof (rule sum.neutral, clarify)
fix x
show "A $ i $ x * B $ x $ j = 0"
proof (cases "x<i")
case True
thus ?thesis using A unfolding upper_triangular_def by auto
next
case False
hence "x>j" using ji by auto
thus ?thesis using A B ji unfolding upper_triangular_def by auto
qed
qed
qed
lemma upper_triangular_adjugate:
fixes A::"(('a::comm_ring_1,'n::{wellorder, finite}) vec, 'n) vec"
assumes A: "upper_triangular A"
shows "upper_triangular (adjugate A)"
proof (auto simp add: cofactor_def upper_triangular_def adjugate_def transpose_def cofactorM_def)
fix i j::'n assume ji: "j < i" with A show "det (minorM A j i) = 0"
unfolding minorM_eq det_sq_matrix_eq[symmetric] from_vec_to_vec det_minor_row
by (subst Square_Matrix.det_upperdiagonal)
(auto simp: upd_row.rep_eq from_vec.rep_eq row_def axis_def upper_triangular_def intro!: prod_zero)
qed
lemma upper_triangular_inverse:
fixes A::"(('a::{euclidean_semiring,comm_ring_1},'n::{wellorder, finite}) vec, 'n) vec"
assumes A: "upper_triangular A"
and inv_A: "invertible A"
shows "upper_triangular (matrix_inv A)"
using upper_triangular_adjugate[OF A]
unfolding invertible_imp_matrix_inv[OF inv_A]
unfolding matrix_scalar_mult_def upper_triangular_def by auto
lemma upper_triangular_mult_diagonal:
fixes A::"(('a::{semiring_1},'n::{wellorder, finite}) vec, 'n) vec"
assumes A: "upper_triangular A"
and B: "upper_triangular B"
shows "(A**B) $ i $ i = A $ i $ i * B $ i $ i"
proof -
have UNIV_rw: "UNIV = (insert i (UNIV-{i}))" by auto
have sum_0: "(∑k∈UNIV-{i}. A $ i $ k * B $ k $ i) = 0"
proof (rule sum.neutral, rule)
fix x assume x: "x ∈ UNIV - {i}"
show "A $ i $ x * B $ x $ i = 0"
proof (cases "x<i")
case True
thus ?thesis using A unfolding upper_triangular_def by auto
next
case False
hence "x>i" using x by auto
thus ?thesis using B unfolding upper_triangular_def by auto
qed
qed
have "(A**B) $ i $ i = (∑k∈UNIV. A $ i $ k * B $ k $ i)"
unfolding matrix_matrix_mult_def by simp
also have "... = (∑k∈(insert i (UNIV-{i})). A $ i $ k * B $ k $ i)"
using UNIV_rw by simp
also have "... = (A $ i $ i * B $ i $ i) + (∑k∈UNIV-{i}. A $ i $ k * B $ k $ i)"
by (rule sum.insert, simp_all)
finally show ?thesis unfolding sum_0 by simp
qed
subsubsection‹More properties of mod type›
lemma add_left_neutral:
fixes a::"'n::mod_type"
shows "(a + b = a) = (b = 0)"
by (auto, metis add_left_cancel monoid_add_class.add.right_neutral)
lemma from_nat_1: "from_nat 1 = 1"
unfolding from_nat_def o_def Abs'_def
by (metis Rep_1 Rep_mod of_nat_1 one_def)
subsubsection‹Div and Mod›
lemma dvd_minus_eq_mod:
fixes c::"'a::unique_euclidean_ring"
assumes "c ≠ 0" and "c dvd a - b" shows "a mod c = b mod c"
using assms dvd_div_mult_self[of c]
by (metis add.commute diff_add_cancel mod_mult_self1)
lemma eq_mod_dvd_minus:
fixes c::"'a::unique_euclidean_ring"
assumes "c ≠ 0" and "a mod c = b mod c"
shows "c dvd a - b"
using assms by (simp add: mod_eq_dvd_iff)
lemma dvd_cong_not_eq_mod:
fixes c::"'a::unique_euclidean_ring"
assumes "xa mod c ≠ xb" and "c dvd xa mod c - xb" and "c ≠ 0"
shows "xb mod c ≠ xb"
using assms
by (metis (no_types, lifting) diff_add_cancel dvdE mod_mod_trivial mod_mult_self4)
lemma diff_mod_cong_0:
fixes c::"'a::unique_euclidean_ring"
assumes "xa mod c ≠ xb mod c" and" c dvd xa mod c - xb mod c" shows "c = 0"
using assms dvd_cong_not_eq_mod mod_mod_trivial by blast
lemma cong_diff_mod:
fixes c::"'a::unique_euclidean_ring"
assumes "xa ≠ xb" and "c dvd xa - xb" and "xa = xa mod c" shows "xb ≠ xb mod c"
by (metis assms diff_eq_diff_eq diff_numeral_special(12) dvd_0_left dvd_minus_eq_mod)
lemma exists_k_mod:
fixes c::"'a::unique_euclidean_ring"
shows "∃k. a mod c = a + k * c"
by (metis add.commute diff_add_cancel diff_minus_eq_add
mult_div_mod_eq mult.commute mult_minus_left)
subsection‹Units, associated and congruent relations›
context semiring_1
begin
definition "Units = {x::'a. (∃k. 1 = x * k)}"
end
context ring_1
begin
definition cong::"'a⇒'a⇒'a⇒bool"
where "cong a c b = (∃k. (a - c) = b * k)"
lemma cong_eq: "cong a c b = (b dvd (a - c))"
unfolding ring_1_class.cong_def dvd_def by simp
end
context normalization_semidom
begin
lemma Units_eq: "Units = {x. x dvd 1}" unfolding Units_def dvd_def ..
lemma normalize_Units: "x ∈ Units ⟹ normalize x = 1"
by (intro is_unit_normalize) (simp_all add: Units_eq)
lemma associated_eq: "(normalize a = normalize b) ⟷ (∃u∈Units. a = u*b)"
proof
assume A: "normalize a = normalize b"
show "∃u∈Units. a = u*b"
proof (cases "a = 0 ∨ b = 0")
case False
from A have "a = (unit_factor a div unit_factor b) * b"
by (metis mult_not_zero normalize_0 normalize_mult_unit_factor mult.left_commute
unit_div_mult_self unit_factor_is_unit)
moreover from False have "unit_factor a div unit_factor b ∈ Units"
by (simp add: Units_eq unit_div)
ultimately show ?thesis by blast
next
case True
with A normalize_eq_0_iff[of a] normalize_eq_0_iff[of b] have "a = 0" "b = 0" by auto
thus ?thesis by (auto intro!: exI[of _ 1] simp: Units_def)
qed
qed (auto simp: normalize_Units Units_def)
end
context unique_euclidean_ring
begin
definition "associated_rel = {(a,b). normalize a = normalize b}"
lemma equiv_associated:
shows "equiv UNIV associated_rel"
unfolding associated_rel_def equiv_def refl_on_def sym_def trans_def by simp
definition "congruent_rel b = {(a,c). cong a c b}"
lemma relf_congruent_rel: "refl (congruent_rel b)"
unfolding refl_on_def congruent_rel_def
unfolding cong_def
by (auto, metis mult_zero_right)
lemma sym_congruent_rel: "sym (congruent_rel b)"
unfolding sym_def congruent_rel_def unfolding cong_def
by (auto, metis add_commute add_minus_cancel diff_conv_add_uminus
minus_mult_commute mult.left_commute mult_1_left)
lemma trans_congruent_rel: "trans (congruent_rel b)"
unfolding trans_def congruent_rel_def unfolding cong_def
by (auto, metis add_assoc diff_add_cancel
diff_conv_add_uminus distrib_left)
lemma equiv_congruent: "equiv UNIV (congruent_rel b)"
unfolding equiv_def
using relf_congruent_rel sym_congruent_rel trans_congruent_rel by auto
end
subsection‹Associates and residues functions›
context normalization_semidom
begin
definition ass_function :: "('a ⇒ 'a) ⇒ bool"
where "ass_function f
= ((∀a. normalize a = normalize (f a)) ∧ pairwise (λa b. normalize a ≠ normalize b) (range f))"
definition "Complete_set_non_associates S
= (∃f. ass_function f ∧ f`UNIV = S ∧ (pairwise (λa b. normalize a ≠ normalize b) S))"
end
context ring_1
begin
definition res_function :: "('a ⇒ 'a ⇒ 'a) ⇒ bool"
where "res_function f = (∀c. (∀a b. cong a b c ⟷ f c a = f c b)
∧ pairwise (λa b. ¬ cong a b c) (range (f c))
∧ (∀a. ∃k. f c a = a + k*c))"
definition "Complete_set_residues g
= (∃f. res_function f ∧ (∀c. (pairwise (λa b. ¬ cong a b c) (f c`UNIV)) ∧ g c = f c`UNIV))"
end
lemma ass_function_Complete_set_non_associates:
assumes f: "ass_function f"
shows "Complete_set_non_associates (f`UNIV)"
unfolding Complete_set_non_associates_def ass_function_def
apply (rule exI[of _ f])
using f unfolding ass_function_def unfolding pairwise_def by fast
lemma in_Ass_not_associated:
assumes Ass_S: "Complete_set_non_associates S"
and x: "x∈S" and y: "y∈S" and x_not_y: "x≠y"
shows "normalize x ≠ normalize y"
using assms unfolding Complete_set_non_associates_def pairwise_def by auto
lemma ass_function_0:
assumes r: "ass_function ass"
shows "(ass x = 0) = (x = 0)"
using assms unfolding ass_function_def pairwise_def
by (metis normalize_eq_0_iff)
lemma ass_function_0':
assumes r: "ass_function ass"
shows "(ass x div x = 0) = (x=0)"
proof safe
assume *: "ass x div x = 0"
from r have **: "normalize (ass x) = normalize x"
by (simp add: ass_function_def)
from associatedD2[OF this] have "x dvd ass x"
by simp
with * ** show "x = 0"
by (auto simp: dvd_div_eq_0_iff)
qed auto
lemma res_function_Complete_set_residues:
assumes f: "res_function f"
shows "Complete_set_residues (λc. (f c)`UNIV)"
unfolding Complete_set_residues_def
apply (rule exI[of _ f]) using f unfolding res_function_def by blast
lemma in_Res_not_congruent:
assumes res_g: "Complete_set_residues g"
and x: "x ∈ g b" and y: "y ∈ g b" and x_not_y: "x≠y"
shows "¬ cong x y b"
using assms
unfolding Complete_set_residues_def
unfolding pairwise_def
by auto
subsubsection‹Concrete instances in Euclidean rings›
definition "ass_function_euclidean (p::'a::{normalization_euclidean_semiring, euclidean_ring}) = normalize p"
definition "res_function_euclidean b (n::'a::{euclidean_ring}) = (if b = 0 then n else (n mod b))"
lemma ass_function_euclidean: "ass_function ass_function_euclidean"
unfolding ass_function_def image_def ass_function_euclidean_def pairwise_def by auto
lemma res_function_euclidean:
"res_function (res_function_euclidean :: 'a :: unique_euclidean_ring ⇒ _)"
by (auto simp add: pairwise_def res_function_def cong_eq image_def res_function_euclidean_def dvd_minus_eq_mod)
(auto simp add: dvd_cong_not_eq_mod eq_mod_dvd_minus diff_mod_cong_0 cong_diff_mod exists_k_mod)
subsubsection‹Concrete case of the integer ring›
definition "ass_function_int (n::int) = abs n"
lemma ass_function_int: "ass_function_int = ass_function_euclidean"
by (unfold ass_function_int_def ass_function_euclidean_def) simp
lemma ass_function_int_UNIV: "(ass_function_int` UNIV) = {x. x≥0}"
unfolding ass_function_int_def image_def
by (auto, metis abs_of_nonneg)
subsection‹Definition of Hermite Normal Form›
text‹
It is worth noting that there is not a single definition of Hermite Normal Form
in the literature. For instance, some authors restrict their definitions to the case
of square nonsingular matrices. Other authors just work with integer matrices.
Furthermore, given a matrix $A$ its Hermite Normal Form $H$ can be defined to be upper triangular
or lower triangular. In addition, the transformation from $A$ to $H$ can be made by means of
elementary row operations or elementary column operations. In our case, we will work as general as
possible, so our input will be any matrix (including nonsquare ones). The output will be an upper
triangular matrix obtained by means of elementary row operations.
Hence, given a complete set of nonassociates and a complete set of residues,
$H$ is said to be in Hermite Normal Form if:
\begin{enumerate}
\item H is in Echelon Form
\item The first nonzero element of a nonzero row belongs to the complete set of nonassociates
\item Let $h$ be the first nonzero element of a nonzero row. Then each element above $h$
belongs to the corresponding complete set of residues of $h$
\end{enumerate}
A matrix $H$ is the Hermite Normal Form of a matrix $A$ if:
\begin{enumerate}
\item There exists an invertible matrix $P$ such that $A = PH$
\item H is in Hermite Normal Form
\end{enumerate}
The Hermite Normal Form is usually applied to integer matrices. As we have already said, there is no
one single definition of it, so some authors impose different conditions. In the particular
case of integer matrices, leading coefficients (the first nonzero element of a nonzero row)
are usually required to be positive, but it is also possible to impose them to be negative
since we would only have to multiply by $-1$.
In the case of the elements $h_{ik}$ above a leading coefficient $h_{ij}$,
some authors demand $0 \leq h_{ik} < h_{ij}$,
other ones impose the conditions $h_{ik} \leq 0$ and \mbox{$\mid h_{ik} \mid < h_{ij}$}, and other ones
$- \frac{h_{ij}}{2} < h_{ik} \leq \frac{h_{ij}}{2}$. More different options are also possible.
All the possibilities can be represented selecting a complete set of nonassociates and a
complete set of residues. The algorithm to compute the Hermite Normal Form will be
parameterised by functions which obtain the appropriate leading coefficient and the
suitable elements above them. We can execute the algorithm with different functions to get
exactly which Hermite Normal Form we want. Once we fix such a complete set of nonassociates
and the corresponding complete set of residues, the Hermite Normal Form is unique.
›
subsubsection‹Echelon form up to row k›
text‹We present the definition of echelon form up to a row k (not included).›
definition "echelon_form_upt_row A k =
(
(∀i. to_nat i < k ∧ is_zero_row i A ⟶ ¬ (∃j. j>i ∧ to_nat j < k ∧ ¬ is_zero_row j A)) ∧
(∀i j. i < j ∧ to_nat j < k ∧ ¬ is_zero_row i A ∧ ¬ is_zero_row j A ⟶ (LEAST n. A $ i $ n ≠ 0) < (LEAST n. A $ j $ n ≠ 0))
)"
lemma echelon_form_upt_row_condition1_explicit:
assumes "echelon_form_upt_row A k"
and "to_nat i < k" and "is_zero_row i A"
shows "¬ (∃j. j>i ∧ to_nat j < k ∧ ¬ is_zero_row j A)"
using assms unfolding echelon_form_upt_row_def by blast
lemma echelon_form_upt_row_condition1_explicit':
assumes "echelon_form_upt_row A k"
and "to_nat i < k" and "is_zero_row i A" and "i≤j" and "to_nat j < k"
shows "is_zero_row j A"
proof (cases "i=j")
case True thus ?thesis using assms by auto
next
case False thus ?thesis using assms unfolding echelon_form_upt_row_def by simp
qed
lemma echelon_form_upt_row_condition1_explicit_neg:
assumes "echelon_form_upt_row A k"
and iA: "¬ is_zero_row i A" and ia_i: "ia < i"
and i: "to_nat i < k"
shows "¬ is_zero_row ia A"
proof -
have "to_nat ia < k" by (metis ia_i i less_trans to_nat_mono)
thus ?thesis using assms unfolding echelon_form_upt_row_def by blast
qed
lemma echelon_form_upt_row_condition2_explicit:
assumes "echelon_form_upt_row A k"
and "ia < j" and "to_nat j < k" and "¬ is_zero_row ia A" and "¬ is_zero_row j A"
shows "(LEAST n. A $ ia $ n ≠ 0) < (LEAST n. A $ j $ n ≠ 0)"
using assms unfolding echelon_form_upt_row_def by auto
lemma echelon_form_upt_row_intro:
assumes"(∀i. to_nat i < k ∧ is_zero_row i A ⟶ ¬ (∃j. i<j ∧ to_nat j < k ∧ ¬ is_zero_row j A))"
and "(∀i j. i < j ∧ to_nat j < k ∧ ¬ is_zero_row i A ∧ ¬ is_zero_row j A ⟶ (LEAST n. A $ i $ n ≠ 0) < (LEAST n. A $ j $ n ≠ 0))"
shows "echelon_form_upt_row A k"
using assms unfolding echelon_form_upt_row_def by simp
lemma echelon_form_echelon_form_upt_row: "echelon_form A = echelon_form_upt_row A (nrows A)"
by (simp add: to_nat_less_card echelon_form_def echelon_form_upt_row_def ncols_def nrows_def
echelon_form_upt_k_def is_zero_row_upt_k_def is_zero_row_def)
subsubsection‹Hermite Normal Form up to row k›
text‹Predicate to check if a matrix is in Hermite Normal form up to row k (not included).›
definition "Hermite_upt_row A k associates residues =
(
Complete_set_non_associates associates ∧
Complete_set_residues residues ∧
echelon_form_upt_row A k ∧
(∀i. to_nat i < k ∧ ¬ is_zero_row i A ⟶ A $ i $ (LEAST n. A $ i $ n ≠ 0) ∈ associates) ∧
(∀i. to_nat i < k ∧ ¬ is_zero_row i A ⟶ (∀j<i. A $ j $ (LEAST n. A $ i $ n ≠ 0) ∈ residues (A $ i $ (LEAST n. A $ i $ n ≠ 0))))
)"
text‹The definition of Hermite Normal Form is now introduced:›
definition Hermite::"'a::{bezout_ring_div,normalization_semidom} set ⇒ ('a ⇒ 'a set) ⇒
(('a, 'b::{mod_type}) vec, 'c::{mod_type}) vec ⇒ bool"
where "Hermite associates residues A = (
Complete_set_non_associates associates
∧ (Complete_set_residues residues)
∧ echelon_form A
∧ (∀i. ¬ is_zero_row i A ⟶ A $ i $ (LEAST n. A $ i $ n ≠ 0) ∈ associates)
∧ (∀i. ¬ is_zero_row i A ⟶ (∀j. j<i ⟶ A $ j $ (LEAST n. A $ i $ n ≠ 0) ∈ residues (A $ i $ (LEAST n. A $ i $ n ≠ 0))))
)"
lemma Hermite_Hermite_upt_row: "Hermite ass res A = Hermite_upt_row A (nrows A) ass res"
by (simp add: Hermite_def Hermite_upt_row_def to_nat_less_card is_zero_row_def
nrows_def ncols_def echelon_form_echelon_form_upt_row)
lemma Hermite_intro:
assumes "Complete_set_non_associates associates"
and "Complete_set_residues residues"
and "echelon_form A "
and "(∀i. ¬ is_zero_row i A ⟶ A $ i $ (LEAST n. A $ i $ n ≠ 0) ∈ associates)"
and "(∀i. ¬ is_zero_row i A ⟶ (∀j. j<i ⟶ A $ j $ (LEAST n. A $ i $ n ≠ 0) ∈ residues (A $ i $ (LEAST n. A $ i $ n ≠ 0))))"
shows "Hermite associates residues A"
using assms unfolding Hermite_def by simp
subsection‹Definition of an algorithm to compute the Hermite Normal Form›
text‹
The algorithm is parameterised by three functions:
\begin{itemize}
\item The function that computes de B\'ezout identity (necessary to compute the echelon form).
\item The function that given an element, it returns its representative element in the associated equivalent class,
which will be an element in the complete set of nonassociates.
\item The function that given two elements $a$ and $b$, it returns its representative
element in the congruent equivalent class of $b$, which will be an element in the complete set of residues of $b$.
\end{itemize}
›
primrec Hermite_reduce_above :: "'a::unique_euclidean_ring^'cols::mod_type^'rows::mod_type⇒nat
⇒'rows⇒'cols⇒ ('a⇒'a⇒'a) ⇒ 'a^'cols::mod_type^'rows::mod_type"
where "Hermite_reduce_above A 0 i j res = A"
| "Hermite_reduce_above A (Suc n) i j res = (let i'=((from_nat n)::'rows);
Aij = A $ i $ j;
Ai'j = A $ i' $ j
in
Hermite_reduce_above (row_add A i' i (((res Aij (Ai'j)) - (Ai'j)) div Aij)) n i j res)"
definition "Hermite_of_row_i ass res A i = (
if is_zero_row i A
then A
else
let j = (LEAST n. A $ i $ n ≠ 0); Aij= (A $ i $ j);
A' = mult_row A i ((ass Aij) div Aij)
in Hermite_reduce_above A' (to_nat i) i j res)"
definition "Hermite_of_upt_row_i A i ass res = foldl (Hermite_of_row_i ass res) A (map from_nat [0..<i])"
definition "Hermite_of A ass res bezout =
(let A'= echelon_form_of A bezout in Hermite_of_upt_row_i A' (nrows A) ass res)"
subsection‹Proving the correctness of the algorithm›
subsubsection‹The proof›
lemma Hermite_reduce_above_preserves:
assumes n: "n≤to_nat a"
shows "(Hermite_reduce_above A n i j res) $ a $ b = A $ a $ b"
using n
proof (induct n arbitrary: A)
case 0 thus ?case by simp
next
case (Suc n)
thus ?case by (auto simp add: Let_def row_add_def)
(metis Suc_le_eq from_nat_mono from_nat_to_nat_id less_irrefl to_nat_less_card)
qed
lemma Hermite_reduce_above_works:
assumes n: "n ≤ to_nat i" and a: "to_nat a < n"
shows "(Hermite_reduce_above A n i j res) $ a $ b
= row_add A a i ((res (A$i$j) (A$a$j) - (A$a$j)) div (A$i$j)) $ a $ b"
using n a
proof (induct n arbitrary: A)
case 0 thus ?case by (simp add: row_add_def)
next
case (Suc n)
define A' where "A' = row_add A (from_nat n) i
((res (A $ i $ j) (A $ from_nat n $ j) - A $ from_nat n $ j) div A $ i $ j)"
have n: "n < nrows A"
unfolding nrows_def by (metis Suc.prems(1) Suc_le_eq less_trans to_nat_less_card)
show ?case
proof (cases "to_nat a = n")
case False
have a_less_n: "to_nat a < n" by (metis False Suc.prems(2) less_antisym)
have "Hermite_reduce_above A (Suc n) i j res $ a $ b = Hermite_reduce_above A' n i j res $ a $ b "
by (simp add: Let_def A'_def)
also have "... = row_add A' a i ((res (A' $ i $ j) (A' $ a $ j) - A' $ a $ j) div A' $ i $ j) $ a $ b"
by (rule Suc.hyps[OF _ a_less_n], simp add: Suc.prems(1) Suc_leD)
also have "... = row_add A a i ((res (A $ i $ j) (A $ a $ j) - A $ a $ j) div A $ i $ j) $ a $ b"
unfolding row_add_def A'_def
using a_less_n Suc.prems n to_nat_from_nat_id[OF n[unfolded nrows_def]]
by auto
finally show ?thesis .
next
case True
hence a_eq_fn_n: "a = from_nat n" by auto
have "Hermite_reduce_above A (Suc n) i j res $ a $ b = Hermite_reduce_above A' n i j res $ a $ b "
by (simp add: Let_def A'_def)
also have "... = A' $ a $ b"
by (rule Hermite_reduce_above_preserves, simp add: True)
finally show ?thesis unfolding A'_def a_eq_fn_n .
qed
qed
lemma Hermite_of_row_preserves_below:
assumes i_a: "i<a"
shows "(Hermite_of_row_i ass res A i) $ a $ b = A $ a $ b"
proof (auto simp add: Hermite_of_row_i_def Let_def)
let ?M="(mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n ≠ 0)) div A $ i $ (LEAST n. A $ i $ n ≠ 0)))"
let ?H="Hermite_reduce_above ?M (to_nat i) i (LEAST n. A $ i $ n ≠ 0) res"
have "?H $ a $ b = ?M $ a $ b"
by (rule Hermite_reduce_above_preserves)
(metis i_a not_le not_less_iff_gr_or_eq to_nat_mono')
also have "... = A $ a $ b" unfolding mult_row_def using i_a by fastforce
finally show "?H $ a $ b = A $ a $ b" .
qed
lemma Hermite_of_row_preserves_previous_cols:
assumes b: "b<(LEAST n. A $ i $ n ≠ 0)"
and not_zero_i_A: "¬ is_zero_row i A"
and e: "echelon_form A"
shows "(Hermite_of_row_i ass res A i) $ a $ b = A $ a $ b"
proof (auto simp add: Hermite_of_row_i_def Let_def)
let ?n="(LEAST n. A $ i $ n ≠ 0)"
let ?M="(mult_row A i (ass (A $ i $ ?n) div A $ i $ ?n))"
let ?H="Hermite_reduce_above ?M (to_nat i) i (LEAST n. A $ i $ n ≠ 0) res"
have Aib: " A $ i $ b = 0" by (metis (mono_tags) b not_less_Least)
show "?H $ a $ b = A $ a $ b"
proof (cases "a≥i")
case True
have "?H $ a $ b = ?M $ a $ b"
by (rule Hermite_reduce_above_preserves) (metis True to_nat_mono')
also have "... = A $ a $ b" using Aib unfolding mult_row_def by auto
finally show ?thesis .
next
let ?R="row_add ?M a i ((res (?M $ i $ ?n) (?M $ a $ ?n) - ?M $ a $ ?n) div ?M $ i $ ?n)"
case False
hence ia: "i>a" by simp
have "?H $ a $ b = ?R $ a $ b" by (rule Hermite_reduce_above_works, auto simp add: ia to_nat_mono)
also have "... = A $ a $ b" using ia Aib unfolding row_add_def mult_row_def by auto
finally show ?thesis .
qed
qed
lemma echelon_form_Hermite_of_condition1:
fixes res ass i A
defines M: "M ≡ mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n ≠ 0)) div A $ i $ (LEAST n. A $ i $ n ≠ 0))"
defines H: "H ≡ Hermite_reduce_above M (to_nat i) i (LEAST n. A $ i $ n ≠ 0) res"
assumes e: "echelon_form A"
and a: "ass_function ass"
and not_zero_iA: "¬ is_zero_row i A"
and zero_ia_H: "is_zero_row ia H"
and ia_j: "ia < j"
shows "is_zero_row j H"
proof (cases "is_zero_row ia A")
case True
have zero_jA: "is_zero_row j A" by (metis True e echelon_form_condition1 ia_j)
have ij: "i<j" by (metis e echelon_form_condition1 neq_iff not_zero_iA zero_jA)
show ?thesis
proof (auto simp add: is_zero_row_def is_zero_row_upt_k_def ncols_def)
fix a
have "H $ j $ a = M $ j $ a"
unfolding H
by (rule Hermite_reduce_above_preserves) (metis dual_order.strict_iff_order ij to_nat_mono')
also have "... = A $ j $ a" unfolding M mult_row_def using ij by auto
also have "... = 0" using zero_jA by (simp add: is_zero_row_def is_zero_row_upt_k_def ncols_def)
finally show "H $ j $ a = 0" .
qed
next
case False note not_zero_ia_A=False
let ?n="(LEAST n. A $ ia $ n ≠ 0)"
have A_ia_n: "A $ ia $ ?n ≠ 0"
by (metis (mono_tags, lifting) LeastI is_zero_row_def is_zero_row_upt_k_def not_zero_ia_A)
show ?thesis
proof (cases "i ≤ ia")
case True
have "H $ ia $ ?n = M $ ia $ ?n"
unfolding H by (rule Hermite_reduce_above_preserves, simp add: True to_nat_mono')
also have "... ≠ 0" unfolding M mult_row_def using A_ia_n ass_function_0'[OF a] by auto
finally have "H $ ia $ ?n ≠ 0" .
hence not_zero_ia_H: "¬ is_zero_row ia H"
unfolding is_zero_row_def is_zero_row_upt_k_def ncols_def by auto
thus ?thesis using zero_ia_H by contradiction
next
case False
let ?m="(LEAST m. A $ i $ m ≠ 0)"
let ?R="row_add M ia i ((res (M $ i $ ?m) (M $ ia $ ?m) - M $ ia $ ?m) div M $ i $ ?m)"
have ia_less_i: "ia<i" by (metis False not_less)
have nm: "?n<?m" by (rule echelon_form_condition2_explicit[OF e ia_less_i not_zero_ia_A not_zero_iA])
have A_im: "A $ i $ ?n = 0" by (metis (full_types) nm not_less_Least)
have "H $ ia $ ?n = ?R $ ia $ ?n"
unfolding H
by (rule Hermite_reduce_above_works, auto simp add: ia_less_i to_nat_mono)
also have "... ≠ 0"
using ia_less_i A_im A_ia_n unfolding row_add_def M mult_row_def by auto
finally have "H $ ia $ ?n ≠ 0" .
hence not_zero_ia_H: "¬ is_zero_row ia H"
unfolding is_zero_row_def is_zero_row_upt_k_def ncols_def by auto
thus ?thesis using zero_ia_H by contradiction
qed
qed
lemma row_zero_A_imp_row_zero_H:
fixes res ass i A
defines M: "M ≡ mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n ≠ 0)) div A $ i $ (LEAST n. A $ i $ n ≠ 0))"
defines H: "H ≡ Hermite_reduce_above M (to_nat i) i (LEAST n. A $ i $ n ≠ 0) res"
assumes e: "echelon_form A"
and not_zero_iA: "¬ is_zero_row i A"
and zero_j_A: "is_zero_row j A"
shows "is_zero_row j H"
proof (auto simp add: is_zero_row_def is_zero_row_upt_k_def ncols_def)
fix a
have A_ja: "A $ j $ a = 0"
using zero_j_A
by (simp add: is_zero_row_def is_zero_row_upt_k_def ncols_def)
show "H $ j $ a = 0"
proof (cases "i≤j")
case True
have "H $ j $ a = M $ j $ a"
unfolding H by (rule Hermite_reduce_above_preserves, simp add: True to_nat_mono')
also have "... = 0" unfolding M mult_row_def using True A_ja by auto
finally show ?thesis .
next
let ?n="(LEAST n. A $ i $ n ≠ 0)"
let ?R="row_add M j i ((res (M $ i $ ?n) (M $ j $ ?n) - M $ j $ ?n) div M $ i $ ?n)"
case False
hence ji: "j<i" by simp
have "H $ j $ a = ?R $ j $ a"
unfolding H by (rule Hermite_reduce_above_works, auto simp add: ji to_nat_mono)
also have "... = 0"
using ji A_ja not_zero_iA e echelon_form_condition1 zero_j_A
unfolding row_add_def M mult_row_def by blast
finally show ?thesis .
qed
qed
lemma Hermite_reduce_above_Least_eq_le:
fixes res ass i A
defines M: "M ≡ mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n ≠ 0)) div A $ i $ (LEAST n. A $ i $ n ≠ 0))"
defines H: "H ≡ Hermite_reduce_above M (to_nat i) i (LEAST n. A $ i $ n ≠ 0) res"
assumes i_ia: "i<ia"
and not_zero_ia_H: "¬ is_zero_row ia H"
shows "(LEAST n. A $ ia $ n ≠ 0) = (LEAST n. H $ ia $ n ≠ 0)"
proof (rule Least_equality)
let ?n="(LEAST n. H $ ia $ n ≠ 0)"
have "A $ ia $ ?n = M $ ia $ ?n" unfolding M mult_row_def using i_ia by auto
also have "... = H $ ia $ ?n "
unfolding H
by (rule Hermite_reduce_above_preserves[symmetric])
(metis i_ia dual_order.strict_iff_order to_nat_mono')
also have "... ≠ 0" by (metis (mono_tags) LeastI is_zero_row_def' not_zero_ia_H)
finally show "A $ ia $ (LEAST n. H $ ia $ n ≠ 0) ≠ 0" .
next
fix y
assume A_ia_y: "A $ ia $ y ≠ 0"
have "H $ ia $ y = M $ ia $ y" unfolding H
by (rule Hermite_reduce_above_preserves)
(metis i_ia dual_order.strict_iff_order to_nat_mono')
also have "... ≠ 0" unfolding M mult_row_def using i_ia A_ia_y by auto
finally show "(LEAST n. H $ ia $ n ≠ 0) ≤ y" by (rule Least_le)
qed
lemma Hermite_reduce_above_Least_eq:
fixes res ass i A
defines M: "M ≡ mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n ≠ 0)) div A $ i $ (LEAST n. A $ i $ n ≠ 0))"
defines H: "H ≡ Hermite_reduce_above M (to_nat i) i (LEAST n. A $ i $ n ≠ 0) res"
assumes a: "ass_function ass"
and not_zero_iA: "¬ is_zero_row i A"
shows "(LEAST n. A $ i $ n ≠ 0) = (LEAST n. H $ i $ n ≠ 0)"
proof (rule Least_equality[symmetric])
let ?n="(LEAST n. A $ i $ n ≠ 0)"
have Ain: "A $ i $ ?n ≠ 0"
by (metis (mono_tags, lifting) LeastI is_zero_row_def' not_zero_iA)
have "H $ i $ ?n = M $ i $ ?n"
unfolding H
by (rule Hermite_reduce_above_preserves, simp)
also have "... ≠ 0" unfolding M mult_row_def by (auto simp add: Ain ass_function_0'[OF a])
finally show "H $ i $ ?n ≠ 0" .
fix y assume H_iy: "H $ i $ y ≠ 0"
show "(LEAST n. A $ i $ n ≠ 0) ≤ y"
proof (rule Least_le, rule ccontr, simp)
assume Aiy: "A $ i $ y = 0"
have "H $ i $ y = M $ i $ y"
unfolding H
by (rule Hermite_reduce_above_preserves, simp)
also have "... = (ass (A $ i $ ?n) div A $ i $ ?n) * A $ i $ y"
unfolding M mult_row_def by auto
also have "... = 0" unfolding Aiy by simp
finally show False using H_iy by contradiction
qed
qed
lemma Hermite_reduce_above_Least_eq_ge:
fixes res ass i A
defines M: "M ≡ mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n ≠ 0)) div A $ i $ (LEAST n. A $ i $ n ≠ 0))"
defines H: "H ≡ Hermite_reduce_above M (to_nat i) i (LEAST n. A $ i $ n ≠ 0) res"
assumes e: "echelon_form A"
and not_zero_iA: "¬ is_zero_row i A"
and not_zero_ia_A: "¬ is_zero_row ia A"
and not_zero_ia_H: "¬ is_zero_row ia H"
and ia_less_i: "ia < i"
shows "(LEAST n. H $ ia $ n ≠ 0) = (LEAST n. A $ ia $ n ≠ 0)"
proof -
let ?least_H = "(LEAST n. H $ ia $ n ≠ 0)"
let ?least_A = "(LEAST n. A $ ia $ n ≠ 0)"
let ?n= "(LEAST n. A $ i $ n ≠ 0)"
let ?Ain ="A $ i $ ?n"
let ?R="row_add M ia i ((res (M $ i $ ?n) (M $ ia $ ?n) - M $ ia $ ?n) div M $ i $ ?n)"
have A_ia_least_A: "A $ ia $ ?least_A ≠ 0"
by (metis (mono_tags, lifting) LeastI is_zero_row_def' not_zero_ia_A)
have H_ia_least_H: "H $ ia $ ?least_H ≠ 0"
by (metis (mono_tags, lifting) LeastI is_zero_row_def' not_zero_ia_H)
have A_i_least_ia_0: "A $ i $ (LEAST n. A $ ia $ n ≠ 0) = 0"
proof -
have "(LEAST n. A $ ia $ n ≠ 0) < (LEAST n. A $ i $ n ≠ 0)"
using e echelon_form_condition1 echelon_form_condition2_explicit
ia_less_i not_zero_iA by blast
thus ?thesis using not_less_Least by blast
qed
have H_ia_least_A: "H $ ia $ ?least_A ≠ 0"
proof -
have "H $ ia $ ?least_A = ?R $ ia $ ?least_A"
unfolding H
by (rule Hermite_reduce_above_works, simp_all add: ia_less_i to_nat_mono)
also have "... ≠ 0" using ia_less_i unfolding row_add_def M mult_row_def
by (auto simp add: A_i_least_ia_0 A_ia_least_A)
finally show ?thesis .
qed
hence least_H_le_least_A: "?least_H ≤ ?least_A"
by (metis (mono_tags) not_less not_less_Least)
have A_i_least_H: "A $ i $ ?least_H = 0"
proof -
have "(LEAST n. A $ ia $ n ≠ 0) < (LEAST n. A $ i $ n ≠ 0)"
using e echelon_form_condition1 echelon_form_condition2_explicit
ia_less_i not_zero_iA by blast
thus ?thesis using not_less_Least least_H_le_least_A
by (metis (mono_tags) dual_order.strict_trans2)
qed
have "A $ ia $ ?least_H ≠ 0"
proof -
have ia_not_i: "ia ≠ i" using ia_less_i by simp
have "?R $ ia $ ?least_H = H $ ia $ ?least_H"
unfolding H
by (rule Hermite_reduce_above_works[symmetric], simp_all add: ia_less_i to_nat_mono)
also have "... ≠ 0" by (rule H_ia_least_H)
finally have R_ia_least_H: "?R $ ia $ ?least_H ≠ 0" .
hence "A $ ia $ ?least_H + (res (ass (?Ain) div ?Ain * ?Ain)
(A $ ia $ (LEAST n. A $ i $ n ≠ 0)) - A $ ia $ (LEAST n. A $ i $ n ≠ 0))
div (ass (?Ain) div ?Ain * ?Ain) * (ass (?Ain) div ?Ain * A $ i $ ?least_H) ≠ 0"
using ia_not_i unfolding row_add_def M mult_row_def by auto
thus ?thesis using ia_less_i A_i_least_H unfolding row_add_def M mult_row_def by auto
qed
hence least_A_le_least_H: "?least_A ≤ ?least_H" by (metis (poly_guards_query) Least_le)
show ?thesis using least_A_le_least_H least_H_le_least_A by simp
qed
lemma Hermite_reduce_above_Least:
fixes res ass i A
defines M: "M ≡ mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n ≠ 0))
div A $ i $ (LEAST n. A $ i $ n ≠ 0))"
defines H: "H ≡ Hermite_reduce_above M (to_nat i) i (LEAST n. A $ i $ n ≠ 0) res"
assumes e: "echelon_form A"
and a: "ass_function ass"
and not_zero_iA: "¬ is_zero_row i A"
and not_zero_ia_A: "¬ is_zero_row ia A"
and not_zero_ia_H: "¬ is_zero_row ia H"
shows "(LEAST n. H $ ia $ n ≠ 0) = (LEAST n. A $ ia $ n ≠ 0)"
proof (cases "ia<i")
case True
show ?thesis
unfolding H M
by (rule Hermite_reduce_above_Least_eq_ge[OF e not_zero_iA not_zero_ia_A _ True])
(metis H M not_zero_ia_H)
next
case False
hence i_le_ia: "i≤ia" by simp
show ?thesis
proof (cases "ia=i")
case True
show ?thesis
unfolding True H M
by (rule Hermite_reduce_above_Least_eq[symmetric, OF a not_zero_iA])
next
case False
hence i_ia: "i<ia" using i_le_ia by simp
show ?thesis
unfolding H M
by (rule Hermite_reduce_above_Least_eq_le[symmetric, OF i_ia], metis H M not_zero_ia_H)
qed
qed
lemma echelon_form_Hermite_of_condition2:
fixes res ass i A
defines M: "M ≡ mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n ≠ 0)) div A $ i $ (LEAST n. A $ i $ n ≠ 0))"
defines H: "H ≡ Hermite_reduce_above M (to_nat i) i (LEAST n. A $ i $ n ≠ 0) res"
assumes e: "echelon_form A"
and a: "ass_function ass"
and not_zero_iA: "¬ is_zero_row i A"
and ia_less_j: "ia < j"
and not_zero_ia_H: "¬ is_zero_row ia H"
and not_zero_j_H: "¬ is_zero_row j H"
shows "(LEAST n. H $ ia $ n ≠ 0) < (LEAST n. H $ j $ n ≠ 0)"
proof -
let ?n= "(LEAST n. A $ i $ n ≠ 0)"
have Ain: "A $ i $ ?n ≠ 0"
by (metis (mono_tags) LeastI is_zero_row_def' not_zero_iA)
have not_zero_j_A: "¬ is_zero_row j A"
using row_zero_A_imp_row_zero_H[OF e not_zero_iA] not_zero_j_H
unfolding H M by blast
have not_zero_ia_A: "¬ is_zero_row ia A"
using row_zero_A_imp_row_zero_H[OF e not_zero_iA] not_zero_ia_H
unfolding H M by blast
have Least_le_A: "(LEAST n. A $ ia $ n ≠ 0) < (LEAST n. A $ j $ n ≠ 0)"
by (rule echelon_form_condition2_explicit[OF e ia_less_j not_zero_ia_A not_zero_j_A])
show ?thesis
proof (cases "i<ia")
case True
have ij: "i<j" by (metis True ia_less_j less_trans)
have Least_A_ia_H_ia: "(LEAST n. A $ ia $ n ≠ 0) = (LEAST n. H $ ia $ n ≠ 0)"
unfolding H M
by (rule Hermite_reduce_above_Least_eq_le[OF True], metis H M not_zero_ia_H)
moreover have Least_A_ia_H_ia: "(LEAST n. A $ j $ n ≠ 0) = (LEAST n. H $ j $ n ≠ 0)"
unfolding H M
by (rule Hermite_reduce_above_Least_eq_le[OF ij], metis H M not_zero_j_H)
ultimately show ?thesis using Least_le_A by simp
next
case False
hence ia_le_i: "ia≤i" by simp
show ?thesis
proof (cases "i=ia")
case True thus ?thesis
using Hermite_reduce_above_Least_eq[OF a not_zero_iA] Least_le_A
using Hermite_reduce_above_Least_eq_le[OF ia_less_j]
using not_zero_j_H unfolding H M by fastforce
next
case False
hence ia_less_i: "ia<i" using ia_le_i by simp
have Least_H_ia_A_ia: "(LEAST n. H $ ia $ n ≠ 0) = (LEAST n. A $ ia $ n ≠ 0)"
unfolding H M
by (rule Hermite_reduce_above_Least_eq_ge[OF e not_zero_iA not_zero_ia_A _ ia_less_i])
(metis H M not_zero_ia_H)
show ?thesis
proof (cases "j<i")
case True
have "(LEAST n. H $ j $ n ≠ 0) = (LEAST n. A $ j $ n ≠ 0)"
unfolding H M
by (rule Hermite_reduce_above_Least_eq_ge[OF e not_zero_iA not_zero_j_A _ True])
(metis H M not_zero_j_H)
thus ?thesis by (simp add: Least_H_ia_A_ia Least_le_A)
next
case False
hence j_ge_i: "j≥i" by auto
show ?thesis
proof (cases "j=i")
case True
have "(LEAST n. H $ j $ n ≠ 0) = (LEAST n. A $ j $ n ≠ 0)"
unfolding H M
using Hermite_reduce_above_Least_eq True a not_zero_iA by fastforce
thus ?thesis by (simp add: Least_H_ia_A_ia Least_le_A)
next
case False
hence j_sg_i: "j>i" using j_ge_i by simp
have "(LEAST n. H $ j $ n ≠ 0) = (LEAST n. A $ j $ n ≠ 0)"
unfolding H M
by (rule Hermite_reduce_above_Least_eq_le[symmetric, OF j_sg_i])
(metis H M not_zero_j_H)
thus ?thesis by (simp add: Least_H_ia_A_ia Least_le_A)
qed
qed
qed
qed
qed
lemma echelon_form_Hermite_of_row:
assumes a: "ass_function ass"
and "res_function res"
and e: "echelon_form A"
shows "echelon_form (Hermite_of_row_i ass res A i)"
proof (rule echelon_form_intro, auto simp add: Hermite_of_row_i_def Let_def)
fix ia j
assume "is_zero_row i A" and "is_zero_row ia A" and "ia < j"
thus "is_zero_row j A" using echelon_form_condition1[OF e] by blast
next
fix ia j
assume "is_zero_row i A" and "ia < j" and "¬ is_zero_row ia A" and "¬ is_zero_row j A"
thus "(LEAST n. A $ ia $ n ≠ 0) < (LEAST n. A $ j $ n ≠ 0)"
using echelon_form_condition2[OF e] by blast
next
fix ia j
assume "¬ is_zero_row i A"
and "is_zero_row ia (Hermite_reduce_above
(mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n ≠ 0)) div A $ i $ (LEAST n. A $ i $ n ≠ 0)))
(to_nat i) i (LEAST n. A $ i $ n ≠ 0) res)"
and "ia < j"
thus "is_zero_row j (Hermite_reduce_above
(mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n ≠ 0)) div A $ i $ (LEAST n. A $ i $ n ≠ 0)))
(to_nat i) i (LEAST n. A $ i $ n ≠ 0) res)"
using echelon_form_Hermite_of_condition1[OF e a] by blast
next
fix ia j
let ?H="(Hermite_reduce_above (mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n ≠ 0))
div A $ i $ (LEAST n. A $ i $ n ≠ 0))) (to_nat i) i (LEAST n. A $ i $ n ≠ 0) res)"
assume "¬ is_zero_row i A"
and "ia < j"
and "¬ is_zero_row ia ?H"
and "¬ is_zero_row j ?H"
thus "(LEAST n. ?H $ ia $ n ≠ 0) < (LEAST n. ?H $ j $ n ≠ 0)"
using echelon_form_Hermite_of_condition2[OF e a] by blast
qed
lemma echelon_form_fold_Hermite_of_row_i:
assumes e: "echelon_form A" and a: "ass_function ass" and r: "res_function res"
shows "echelon_form (foldl (Hermite_of_row_i ass res) A (map from_nat [0..<k]))"
proof (induct k)
case 0
thus ?case by (simp add: e)
next
case (Suc k)
show ?case by (simp, rule echelon_form_Hermite_of_row[OF a r Suc.hyps])
qed
lemma echelon_form_Hermite_of_upt_row_i:
assumes e: "echelon_form A" and a: "ass_function ass" and r: "res_function res"
shows "echelon_form (Hermite_of_upt_row_i A k ass res)"
unfolding Hermite_of_upt_row_i_def
using echelon_form_fold_Hermite_of_row_i assms by auto
lemma echelon_form_Hermite_of:
fixes A::"'a::{bezout_ring_div,normalization_semidom,unique_euclidean_ring}^'cols::{mod_type}^'rows::{mod_type}"
assumes a: "ass_function ass"
and r: "res_function res"
and b: "is_bezout_ext bezout"
shows "echelon_form (Hermite_of A ass res bezout)"
unfolding Hermite_of_def Hermite_of_upt_row_i_def Let_def nrows_def
by (rule echelon_form_fold_Hermite_of_row_i[OF echelon_form_echelon_form_of[OF b] a r])
lemma in_ass_Hermite_of_row:
assumes a: "ass_function ass"
and "res_function res"
and not_zero_i_A: "¬ is_zero_row i A"
shows "(Hermite_of_row_i ass res A i) $ i $ (LEAST n. (Hermite_of_row_i ass res A i) $ i $ n ≠ 0) ∈ range ass"
unfolding Hermite_of_row_i_def using not_zero_i_A
proof (auto simp add: Let_def)
let ?M="(mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n ≠ 0)) div A $ i $ (LEAST n. A $ i $ n ≠ 0))) "
let ?H="Hermite_reduce_above ?M (to_nat i) i (LEAST n. A $ i $ n ≠ 0) res"
let ?Ain="A $ i $ (LEAST n. A $ i $ n ≠ 0)"
have Ain: "?Ain ≠ 0"
by (metis (mono_tags) LeastI is_zero_row_def' not_zero_i_A)
have least_eq: "(LEAST n. ?H $ i $ n ≠ 0) = (LEAST n. A $ i $ n ≠ 0)"
by (rule Hermite_reduce_above_Least_eq[OF a not_zero_i_A, symmetric])
have "?H $ i $ (LEAST n. ?H $ i $ n ≠ 0) = ?M $ i $ (LEAST n. ?H $ i $ n ≠ 0)"
by (rule Hermite_reduce_above_preserves, simp)
also have "... = ass (?Ain) div ?Ain * ?Ain"
unfolding mult_row_def least_eq[unfolded mult_row_def] by simp
also have "... = ass ?Ain"
proof (rule dvd_div_mult_self)
show "?Ain dvd ass ?Ain"
using a unfolding ass_function_def by (simp add: associatedD2)
qed
also have "... ∈ range ass" by simp
finally show "?H $ i $ (LEAST n. ?H $ i $ n ≠ 0) ∈ range ass" .
qed
lemma Hermite_of_upt_row_preserves_below:
assumes i: "to_nat a≥k"
shows "Hermite_of_upt_row_i A k ass res $ a $ b = A $ a $ b"
using i
proof (induct k)
case 0
thus ?case unfolding Hermite_of_upt_row_i_def by auto
next
case (Suc k)
show ?case
by (simp add: Hermite_of_upt_row_i_def,
metis Hermite_of_upt_row_i_def Hermite_of_row_preserves_below Suc.hyps Suc.prems
Suc_leD Suc_le_eq from_nat_mono from_nat_to_nat_id to_nat_less_card)
qed
lemma not_zero_Hermite_reduce_above:
fixes ass i A
defines M: "M≡(mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n ≠ 0)) div A $ i $ (LEAST n. A $ i $ n ≠ 0)))"
assumes not_zero_a_A: "¬ is_zero_row a A"
and not_zero_i_A: "¬ is_zero_row i A"
and e: "echelon_form A"
and a: "ass_function ass"
and n: "n ≤ to_nat i"
shows "¬ is_zero_row a (Hermite_reduce_above M n i (LEAST n. A $ i $ n ≠ 0) res)"
proof -
let ?H = "(Hermite_reduce_above M n i (LEAST n. A $ i $ n ≠ 0) res)"
let ?n="LEAST n. A $ a $ n ≠ 0"
let ?m="LEAST n. A $ i $ n ≠ 0"
have Aan: "A $ a $ ?n ≠ 0"
by (metis (mono_tags) LeastI not_zero_a_A is_zero_row_def')
have Aim: "A $ i $ ?m ≠ 0"
by (metis (mono_tags) LeastI not_zero_i_A is_zero_row_def')
show ?thesis
proof (cases "n≤to_nat a")
case True
have "?H $ a $ ?n = M $ a $ ?n"
by (metis Hermite_reduce_above_preserves True)
also have "... ≠ 0" unfolding M mult_row_def using ass_function_0'[OF a] Aan by auto
finally show ?thesis unfolding is_zero_row_def is_zero_row_upt_k_def ncols_def by auto
next
let ?R="row_add M a i
((res (M $ i $ ?m) (M $ a $ ?m) - M $ a $ ?m) div M $ i $ ?m)"
case False
hence a_n: "to_nat a < n" by simp
have ai: "a < i"
by (metis False dual_order.trans n nat_less_le not_less_iff_gr_or_eq to_nat_mono)
have "(LEAST n. A $ a $ n ≠ 0) < ?m"
by (rule echelon_form_condition2_explicit[OF e ai not_zero_a_A not_zero_i_A])
hence Ain: "A $ i $ (LEAST n. A $ a $ n ≠ 0) = 0"
by (metis (full_types) not_less_Least)
have a_not_i: "a ≠ i" by (metis False n)
have "?H $ a $ ?n = ?R $ a $ ?n"
by (rule Hermite_reduce_above_works[OF n a_n])
also have "... ≠ 0" using a_not_i Aan Ain unfolding row_add_def M mult_row_def by auto
finally show ?thesis unfolding is_zero_row_def is_zero_row_upt_k_def ncols_def by auto
qed
qed
lemma Least_Hermite_of_row_i:
assumes i: "¬ is_zero_row i A"
and e: "echelon_form A"
and a: "ass_function ass"
shows "(LEAST n. Hermite_of_row_i ass res A i $ i $ n ≠ 0) = (LEAST n. A $ i $ n ≠ 0)"
proof -
let ?M="mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n ≠ 0)) div A $ i $ (LEAST n. A $ i $ n ≠ 0))"
let ?H="Hermite_reduce_above ?M (to_nat i) i (LEAST n. A $ i $ n ≠ 0) res"
have "(LEAST n. Hermite_of_row_i ass res A i $ i $ n ≠ 0) = (LEAST n. ?H $ i $ n ≠ 0)"
using i unfolding Hermite_of_row_i_def unfolding Let_def by auto
also have "... = (LEAST n. A $ i $ n ≠ 0)"
by (rule Hermite_reduce_above_Least[OF e a i i])
(rule not_zero_Hermite_reduce_above[OF i i e a], simp)
finally show ?thesis .
qed
lemma Least_Hermite_of_row_i2:
assumes i: "¬ is_zero_row i A" and k: "¬ is_zero_row k A"
and e: "echelon_form A"
and a: "ass_function ass"
shows "(LEAST n. Hermite_of_row_i ass res A k $ i $ n ≠ 0) = (LEAST n. A $ i $ n ≠ 0)"
proof -
let ?M="mult_row A k (ass (A $ k $ (LEAST n. A $ k $ n ≠ 0)) div A $ k $ (LEAST n. A $ k $ n ≠ 0))"
let ?H="Hermite_reduce_above ?M (to_nat k) k (LEAST n. A $ k $ n ≠ 0) res"
have "(LEAST n. Hermite_of_row_i ass res A k $ i $ n ≠ 0) = (LEAST n. ?H $ i $ n ≠ 0)"
using k unfolding Hermite_of_row_i_def unfolding Let_def by auto
also have "... = (LEAST n. A $ i $ n ≠ 0)"
by (rule Hermite_reduce_above_Least[OF e a k i])
(simp add: a e i k not_zero_Hermite_reduce_above)
finally show ?thesis .
qed
lemma Hermite_of_row_i_works:
fixes i A ass
defines n:"n ≡(LEAST n. A $ i $ n ≠ 0)"
defines M:"M ≡ (mult_row A i (ass (A $ i $ n) div A $ i $ n))"
assumes ai: "a < i"
and i: "¬ is_zero_row i A"
shows "Hermite_of_row_i ass res A i $ a $ b =
row_add M a i ((res (M $ i $ n) (M $ a $ n)
- M $ a $ n) div M $ i $ n) $ a $ b"
proof -
let ?H="Hermite_reduce_above M (to_nat i) i n res"
have "Hermite_of_row_i ass res A i $ a $ b = ?H $ a $ b"
unfolding Hermite_of_row_i_def Let_def M n using i by simp
also have "... = row_add M a i ((res (M $ i $ n) (M $ a $ n)
- M $ a $ n) div M $ i $ n) $ a $ b"
by (rule Hermite_reduce_above_works, auto simp add: ai to_nat_mono)
finally show ?thesis .
qed
lemma Hermite_of_row_i_works2:
fixes i A ass
defines n:"n ≡(LEAST n. A $ i $ n ≠ 0)"
defines M:"M ≡ (mult_row A i (ass (A $ i $ n) div A $ i $ n))"
assumes i: "¬ is_zero_row i A"
shows "Hermite_of_row_i ass res A i $ i $ b = M $ i $ b"
proof -
let ?H="Hermite_reduce_above M (to_nat i) i n res"
have "Hermite_of_row_i ass res A i $ i $ b = ?H $ i $ b"
unfolding Hermite_of_row_i_def Let_def M n using i by simp
also have "... = M $ i $ b" by (rule Hermite_reduce_above_preserves, simp)
finally show ?thesis .
qed
lemma Hermite_of_upt_row_preserves_nonzero_rows_ge:
assumes i: "¬ is_zero_row i A" and i2: "to_nat i≥k"
shows "¬ is_zero_row i (Hermite_of_upt_row_i A k ass res)"
proof -
let ?n="LEAST n. A $ i $ n ≠ 0"
have Ain: "A $ i $ ?n ≠ 0" by (metis (mono_tags) LeastI i is_zero_row_def')
have "Hermite_of_upt_row_i A k ass res $ i $ ?n = A $ i $ ?n"
by (rule Hermite_of_upt_row_preserves_below[OF i2])
also have "... ≠ 0" by (metis (mono_tags) LeastI i is_zero_row_def')
finally have "Hermite_of_upt_row_i A k ass res $ i $ (LEAST n. A $ i $ n ≠ 0) ≠ 0" .
thus ?thesis unfolding is_zero_row_def is_zero_row_upt_k_def ncols_def by auto
qed
lemma Hermite_of_upt_row_i_Least_ge:
assumes i: "¬ is_zero_row i A"
and i2: "to_nat i≥k"
shows "(LEAST n. Hermite_of_upt_row_i A k ass res $ i $ n ≠ 0) = (LEAST n. A $ i $ n ≠ 0)"
proof (rule Least_equality)
let ?n="LEAST n. A $ i $ n ≠ 0"
have Ain: "A $ i $ ?n ≠ 0" by (metis (mono_tags) LeastI i is_zero_row_def')
have "Hermite_of_upt_row_i A k ass res $ i $ ?n = A $ i $ ?n"
by (rule Hermite_of_upt_row_preserves_below[OF i2])
also have "... ≠ 0" by (metis (mono_tags) LeastI i is_zero_row_def')
finally show "Hermite_of_upt_row_i A k ass res $ i $ (LEAST n. A $ i $ n ≠ 0) ≠ 0" .
fix y
assume H: "Hermite_of_upt_row_i A k ass res $ i $ y ≠ 0"
show "(LEAST n. A $ i $ n ≠ 0) ≤ y"
by (rule Least_le, metis Hermite_of_upt_row_preserves_below H i2)
qed
lemma Hermite_of_upt_row_i_Least:
assumes iA: "¬ is_zero_row i A"
and e: "echelon_form A"
and a: "ass_function ass"
and r: "res_function res"
and k: "k≤nrows A"
shows "(LEAST n. Hermite_of_upt_row_i A k ass res $ i $ n ≠ 0) = (LEAST n. A $ i $ n ≠ 0)"
proof (cases "to_nat i≥k")
case True
thus ?thesis using Hermite_of_upt_row_i_Least_ge iA by blast
next
case False
hence i_less_k: "to_nat i<k" by simp
thus ?thesis using e iA k
proof (induct k arbitrary: A)
case 0
thus ?case
unfolding Hermite_of_upt_row_i_def by simp
next
case (Suc k)
have k: "k≤nrows A" using Suc.prems unfolding nrows_def by simp
have k2: "k<nrows A" using Suc.prems unfolding nrows_def by simp
define A' where "A' = foldl (Hermite_of_row_i ass res) A (map from_nat [0..<k])"
have A'_def2: "A' = Hermite_of_upt_row_i A k ass res"
unfolding Hermite_of_upt_row_i_def A'_def ..
have e: "echelon_form A'"
unfolding A'_def2
by (rule echelon_form_Hermite_of_upt_row_i[OF _ a r], auto simp add: Suc.prems)
show ?case
proof (cases "to_nat i = k")
case True
have i_fn_k: "from_nat k = i" by (metis True from_nat_to_nat_id)
have not_zero_i_A': "¬ is_zero_row i A'"
unfolding A'_def2
by (rule Hermite_of_upt_row_preserves_nonzero_rows_ge, auto simp add: Suc.prems True)
have "Hermite_of_upt_row_i A (Suc k) ass res = Hermite_of_row_i ass res A' (from_nat k)"
unfolding Hermite_of_upt_row_i_def A'_def by auto
also have "(LEAST n. ... $ i $ n ≠ 0) = (LEAST n. A' $ i $ n ≠ 0)"
unfolding i_fn_k
by (rule Least_Hermite_of_row_i[OF not_zero_i_A' e a])
also have "... = (LEAST n. A $ i $ n ≠ 0)"
unfolding A'_def2
by (rule Hermite_of_upt_row_i_Least_ge, auto simp add: True Suc.prems)
finally show ?thesis .
next
case False
hence i_less_k: "to_nat i < k" using Suc.prems by simp
hence i_less_k2: "i < from_nat k"
by (metis from_nat_mono from_nat_to_nat_id k2 nrows_def)
show ?thesis
proof (cases "is_zero_row (from_nat k) A'")
case True
have H: "Hermite_of_upt_row_i A (Suc k) ass res = Hermite_of_upt_row_i A k ass res"
using True by (simp add: Hermite_of_upt_row_i_def Hermite_of_row_i_def A'_def Let_def )
show ?thesis unfolding H by (rule Suc.hyps[OF i_less_k], auto simp add: Suc.prems k)
next
case False
have not_zero_i_A': "¬ is_zero_row i A'"
using e False i_less_k2 echelon_form_condition1 by blast
have "Hermite_of_upt_row_i A (Suc k) ass res = Hermite_of_row_i ass res A' (from_nat k)"
unfolding Hermite_of_upt_row_i_def A'_def by auto
also have "(LEAST n. ... $ i $ n ≠ 0) = (LEAST n. A' $ i $ n ≠ 0)"
by (rule Least_Hermite_of_row_i2[OF not_zero_i_A' False e a])
also have "... = (LEAST n. A $ i $ n ≠ 0)"
unfolding A'_def2 by (rule Suc.hyps[OF i_less_k], auto simp add: Suc.prems k)
finally show ?thesis .
qed
qed
qed
qed
lemma Hermite_of_upt_row_preserves_nonzero_rows:
assumes i: "¬ is_zero_row i A"
and e: "echelon_form A"
and a: "ass_function ass"
and r: "res_function res"
and k: "k≤nrows A"
shows "¬ is_zero_row i (Hermite_of_upt_row_i A k ass res)"
proof -
let ?n="LEAST n. A $ i $ n ≠ 0"
have Ain: "A $ i $ ?n ≠ 0" by (metis (mono_tags) LeastI i is_zero_row_def')
show ?thesis
proof (cases "to_nat i≥k")
case True thus ?thesis using Hermite_of_upt_row_preserves_nonzero_rows_ge i by blast
next
case False
hence i_less_k: "to_nat i<k" by auto
thus ?thesis using i k
proof (induct k)
case 0
thus ?case by (metis less_nat_zero_code)
next
case (Suc k)
have k_nrows: "k ≤ nrows A" using Suc.prems unfolding nrows_def by auto
have k_nrows2: "k < nrows A" using Suc.prems unfolding nrows_def by auto
define A' where "A' = foldl (Hermite_of_row_i ass res) A (map from_nat [0..<k])"
have A'_def2: "A' = Hermite_of_upt_row_i A k ass res"
unfolding Hermite_of_upt_row_i_def A'_def ..
have least_A'_A: "(LEAST n. A' $ i $ n ≠ 0) = (LEAST n. A $ i $ n ≠ 0)"
unfolding A'_def2
by (rule Hermite_of_upt_row_i_Least[OF _ e a r], auto simp add: k_nrows Suc.prems)
have e: "echelon_form A'"
unfolding A'_def2 by (simp add: a e echelon_form_Hermite_of_upt_row_i r)
show ?case
proof (cases "to_nat i = k")
let ?M="mult_row A' i (ass (A' $ i $ (LEAST n. A' $ i $ n ≠ 0)) div A' $ i $ (LEAST n. A' $ i $ n ≠ 0))"
case True
hence fn_k_i: "from_nat k = i" by (metis from_nat_to_nat_id)
have not_zero_i_A': "¬ is_zero_row i A'"
by (unfold A'_def2)
(rule Hermite_of_upt_row_preserves_nonzero_rows_ge, auto simp add: True Suc.prems)
have A'_i_l: "(A' $ i $ (LEAST n. A' $ i $ n ≠ 0)) ≠ 0"
by (metis (mono_tags) LeastI is_zero_row_def' not_zero_i_A')
have "Hermite_of_upt_row_i A (Suc k) ass res $ i $ ?n =
Hermite_of_row_i ass res A' (from_nat k) $ i $ ?n"
unfolding Hermite_of_upt_row_i_def A'_def by simp
also have "... = ?M $ i $ ?n" unfolding fn_k_i
by (rule Hermite_of_row_i_works2[OF not_zero_i_A'])
also have "... ≠ 0"
using A'_i_l unfolding mult_row_def
by (simp add: ass_function_0'[OF a] least_A'_A)
finally show ?thesis unfolding is_zero_row_def is_zero_row_upt_k_def ncols_def by auto
next
case False
hence i_k: "to_nat i < k" by (metis Suc.prems(1) less_antisym)
hence i_k2: "i< from_nat k" using i_k Suc.prems
by (metis from_nat_mono from_nat_to_nat_id k_nrows2 nrows_def)
have not_zero_i_A': "¬ is_zero_row i A'"
unfolding A'_def2 by (rule Suc.hyps[OF i_k Suc.prems(2) k_nrows])
show ?thesis
proof (cases "is_zero_row (from_nat k) A'")
case False
have Ain: "A' $ i $ (LEAST n. A $ i $ n ≠ 0) ≠ 0" unfolding least_A'_A[symmetric]
by (metis (mono_tags) LeastI is_zero_row_def' not_zero_i_A')
have Akn: "A' $ (from_nat k) $ (LEAST n. A $ i $ n ≠ 0) = 0"
proof -
have "(LEAST n. A' $ i $ n ≠ 0) < (LEAST n. A' $ (from_nat k) $ n ≠ 0)"
by (rule echelon_form_condition2_explicit[OF e i_k2 not_zero_i_A' False])
thus ?thesis by (metis (mono_tags) least_A'_A not_less_Least)
qed
let ?m="(LEAST n. A' $ from_nat k $ n ≠ 0)"
let ?M="mult_row A' (from_nat k)
(ass (A' $ from_nat k $ ?m) div
A' $ from_nat k $ ?m)"
have "Hermite_of_upt_row_i A (Suc k) ass res $ i $ ?n =
Hermite_of_row_i ass res A' (from_nat k) $ i $ ?n"
unfolding Hermite_of_upt_row_i_def A'_def by simp
also have "... = row_add (mult_row A' (from_nat k)
(ass (A' $ from_nat k $ ?m) div A' $ from_nat k $ ?m)) i (from_nat k)
((res (?M $ from_nat k $ ?m) (?M $ i $ ?m) - ?M $ i $ ?m) div ?M $ from_nat k $ ?m) $ i $ ?n"
by (rule Hermite_of_row_i_works[OF i_k2 False])
also have "... ≠ 0" using i_k2 Ain Akn unfolding row_add_def mult_row_def by auto
finally show ?thesis unfolding is_zero_row_def is_zero_row_upt_k_def ncols_def by auto
next
case True
have "Hermite_of_upt_row_i A (Suc k) ass res = Hermite_of_upt_row_i A k ass res"
using True by (simp add: Hermite_of_upt_row_i_def Hermite_of_row_i_def A'_def Let_def)
thus ?thesis using not_zero_i_A' unfolding A'_def2 by simp
qed
qed
qed
qed
qed
lemma Hermite_of_upt_row_i_in_range:
fixes k ass res
assumes not_zero_i_A: "¬ is_zero_row i A"
and e: "echelon_form A"
and a: "ass_function ass"
and r: "res_function res"
and k: "to_nat i<k"
and k2: "k≤nrows A"
shows "Hermite_of_upt_row_i A k ass res $ i $ (LEAST n. A $ i $ n ≠ 0) ∈ range ass"
using k not_zero_i_A k2
proof (induct k)
case 0
thus ?case by auto
next
case (Suc k)
have k: "k≤nrows A" using Suc.prems unfolding nrows_def by simp
have k2: "k<nrows A" using Suc.prems unfolding nrows_def by simp
define A' where "A' = foldl (Hermite_of_row_i ass res) A (map from_nat [0..<k])"
have A'_def2: "A' = Hermite_of_upt_row_i A k ass res" unfolding Hermite_of_upt_row_i_def A'_def ..
define M where "M = mult_row A' i (ass (A' $ i $ (LEAST n. A' $ i $ n ≠ 0)) div A' $ i $ (LEAST n. A' $ i $ n ≠ 0))"
have not_zero_A': "¬ is_zero_row i A'"
using Hermite_of_upt_row_preserves_nonzero_rows[OF not_zero_i_A e a r k]
unfolding A'_def Hermite_of_upt_row_i_def by simp
have e_A': "echelon_form A'" by (metis A'_def a e echelon_form_fold_Hermite_of_row_i r)
have least_eq: "(LEAST n. (Hermite_of_row_i ass res A' i) $ i $ n ≠ 0) = (LEAST n. A' $ i $ n ≠ 0)"
by (rule Least_Hermite_of_row_i[OF not_zero_A' e_A' a])
have least_eq2: "(LEAST n. A' $ i $ n ≠ 0) = (LEAST n. A $ i $ n ≠ 0)"
unfolding A'_def2
by (rule Hermite_of_upt_row_i_Least[OF not_zero_i_A e a r k])
show ?case
proof (cases "to_nat i = k")
case True
have fn_k_i: "from_nat k = i" by (metis True from_nat_to_nat_id)
have "(Hermite_of_upt_row_i A (Suc k) ass res) $ i $ (LEAST n. A $ i $ n ≠ 0) =
(Hermite_of_row_i ass res A' i) $ i $ (LEAST n. A $ i $ n ≠ 0)"
unfolding Hermite_of_upt_row_i_def
by (simp add: A'_def fn_k_i)
also have "... = (Hermite_of_row_i ass res A' i) $ i $ (LEAST n. (Hermite_of_row_i ass res A' i) $ i $ n ≠ 0)"
unfolding least_eq least_eq2 ..
also have "... ∈ range ass" by (rule in_ass_Hermite_of_row[OF a r not_zero_A'])
finally show ?thesis .
next
case False
hence i_less_k: "to_nat i < k" using Suc.prems by auto
hence i_less_k2: "i < from_nat k" using Suc.prems
by (metis from_nat_mono from_nat_to_nat_id k2 nrows_def)
show ?thesis
proof (cases "is_zero_row (from_nat k) A'")
case True
have "Hermite_of_upt_row_i A (Suc k) ass res = Hermite_of_upt_row_i A k ass res"
using True by (simp add: Hermite_of_upt_row_i_def Hermite_of_row_i_def A'_def Let_def )
thus ?thesis using Suc.hyps not_zero_i_A k i_less_k by auto
next
case False
have "(Hermite_of_upt_row_i A (Suc k) ass res) $ i $ (LEAST n. A $ i $ n ≠ 0)
= (Hermite_of_row_i ass res A' (from_nat k)) $ i $ (LEAST n. A $ i $ n ≠ 0)"
unfolding Hermite_of_upt_row_i_def A'_def by auto
also have "... = A' $ i $ (LEAST n. A $ i $ n ≠ 0)"
proof (rule Hermite_of_row_preserves_previous_cols[OF _ False e_A'])
show "(LEAST n. A $ i $ n ≠ 0) < (LEAST n. A' $ mod_type_class.from_nat k $ n ≠ 0)"
unfolding least_eq2[symmetric]
by (rule echelon_form_condition2_explicit[OF e_A' i_less_k2 not_zero_A' False])
qed
also have "... ∈ range ass"
unfolding A'_def using Suc.prems Suc.hyps
unfolding Hermite_of_upt_row_i_def using i_less_k by auto
finally show ?thesis .
qed
qed
qed
lemma Hermite_of_upt_row_preserves_zero_rows_ge:
assumes i: "is_zero_row i A"
and k: "k ≤ nrows A"
and ik: "to_nat i≥k"
shows "is_zero_row i (Hermite_of_upt_row_i A k ass res)"
proof (unfold is_zero_row_def', clarify)
fix j
have "Hermite_of_upt_row_i A k ass res $ i $ j = A $ i $ j"
by (metis Hermite_of_upt_row_preserves_below ik)
also have "... = 0" using i unfolding is_zero_row_def is_zero_row_upt_k_def ncols_def by simp
finally show "Hermite_of_upt_row_i A k ass res $ i $ j = 0" .
qed
lemma Hermite_of_upt_row_preserves_zero_rows:
fixes A::"'a::{bezout_ring_div,normalization_semidom,unique_euclidean_ring}^'cols::{mod_type}^'rows::{mod_type}"
assumes i: "is_zero_row i A"
and e: "echelon_form A" and a: "ass_function ass" and r: "res_function res" and k: "k ≤ nrows A"
shows "is_zero_row i (Hermite_of_upt_row_i A k ass res)"
proof (cases "to_nat i≥k")
case True
show ?thesis by (rule Hermite_of_upt_row_preserves_zero_rows_ge[OF i k True])
next
case False
hence i_k: "to_nat i < k" by simp
show ?thesis
using k i_k
proof (induct k)
case 0
thus ?case unfolding Hermite_of_upt_row_i_def by (simp add: i)
next
case (Suc k)
have k: "k≤nrows A" using Suc.prems unfolding nrows_def by auto
have k2: "k<nrows A" using Suc.prems unfolding nrows_def by simp
define A' where "A' = foldl (Hermite_of_row_i ass res) A (map from_nat [0..<k])"
have A'_def2: "A' = Hermite_of_upt_row_i A k ass res"
unfolding Hermite_of_upt_row_i_def A'_def ..
show ?case unfolding is_zero_row_def'
proof (clarify, cases "to_nat i = k")
fix j
case True
have fn_k_i: "from_nat k = i" by (metis True from_nat_to_nat_id)
have "(Hermite_of_upt_row_i A (Suc k) ass res) =
(Hermite_of_row_i ass res A' i)"
unfolding Hermite_of_upt_row_i_def
by (simp add: A'_def fn_k_i)
moreover have "is_zero_row i (Hermite_of_upt_row_i A k ass res)"
by (rule Hermite_of_upt_row_preserves_zero_rows_ge[OF i k], simp add: True)
ultimately show "(Hermite_of_upt_row_i A (Suc k) ass res) $ i $ j = 0"
unfolding is_zero_row_def' A'_def2 Hermite_of_row_i_def by auto
next
fix j
case False
hence i_less_k: "to_nat i < k" using Suc.prems by auto
hence i_less_k2: "i < from_nat k" using Suc.prems
by (metis from_nat_mono from_nat_to_nat_id k2 nrows_def)
show "(Hermite_of_upt_row_i A (Suc k) ass res) $ i $ j = 0"
proof (cases "is_zero_row (from_nat k) A'")
case True
have "is_zero_row i (Hermite_of_upt_row_i A k ass res)" by (metis Suc.hyps i_less_k k)
moreover have "Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = Hermite_of_upt_row_i A k ass res $ i $ j"
using True by (simp add: Hermite_of_upt_row_i_def Hermite_of_row_i_def A'_def Let_def)
ultimately show ?thesis unfolding is_zero_row_def' by auto
next
case False
have "is_zero_row i (Hermite_of_upt_row_i A k ass res)" by (metis Suc.hyps i_less_k k)
moreover have "¬ is_zero_row i (Hermite_of_upt_row_i A k ass res)"
using echelon_form_condition1
by (metis A'_def2 False e a r echelon_form_Hermite_of_upt_row_i i_less_k2)
ultimately show ?thesis by contradiction
qed
qed
qed
qed
lemma Hermite_of_preserves_zero_rows:
fixes A::"'a::{bezout_ring_div,normalization_semidom,unique_euclidean_ring}^'cols::{mod_type}^'rows::{mod_type}"
assumes i: "is_zero_row i (echelon_form_of A bezout)"
and a: "ass_function ass"
and r: "res_function res"
and b: "is_bezout_ext bezout"
shows "is_zero_row i (Hermite_of A ass res bezout)"
unfolding Hermite_of_def Let_def
by (rule Hermite_of_upt_row_preserves_zero_rows[OF i echelon_form_echelon_form_of[OF b] a r])
(auto simp add: nrows_def)
lemma Hermite_of_Least:
fixes A::"'a::{bezout_ring_div,normalization_semidom,unique_euclidean_ring}^'cols::{mod_type}^'rows::{mod_type}"
assumes i: "¬ is_zero_row i (Hermite_of A ass res bezout)"
and a: "ass_function ass"
and r: "res_function res"
and b: "is_bezout_ext bezout"
shows "(LEAST n. Hermite_of A ass res bezout $ i $ n ≠ 0) = (LEAST n. (echelon_form_of A bezout) $ i $ n ≠ 0)"
proof -
have non_zero_i_eA: "¬ is_zero_row i (echelon_form_of A bezout)"
using Hermite_of_preserves_zero_rows[OF _ a r b] i by auto
have e: "echelon_form (echelon_form_of A bezout)" by (rule echelon_form_echelon_form_of[OF b])
show ?thesis
unfolding Hermite_of_def Let_def
by (rule Hermite_of_upt_row_i_Least[OF non_zero_i_eA e a r], simp add: nrows_def)
qed
lemma in_associates_Hermite_of:
fixes A::"'a::{bezout_ring_div,normalization_semidom,unique_euclidean_ring}^'cols::{mod_type}^'rows::{mod_type}"
assumes a: "ass_function ass"
and r: "res_function res"
and b: "is_bezout_ext bezout"
and i: "¬ is_zero_row i (Hermite_of A ass res bezout)"
shows "Hermite_of A ass res bezout $ i $ (LEAST n. Hermite_of A ass res bezout $ i $ n ≠ 0) ∈ range ass"
proof -
have non_zero_i_eA: "¬ is_zero_row i (echelon_form_of A bezout)"
using Hermite_of_preserves_zero_rows[OF _ a r b] i by auto
have e: "echelon_form (echelon_form_of A bezout)"
by (rule echelon_form_echelon_form_of[OF b])
have least: "(LEAST n. Hermite_of A ass res bezout $ i $ n ≠ 0) = (LEAST n. (echelon_form_of A bezout) $ i $ n ≠ 0)"
by (rule Hermite_of_Least[OF i a r b])
show ?thesis unfolding least
unfolding Hermite_of_def Let_def
by (rule Hermite_of_upt_row_i_in_range[OF non_zero_i_eA e a r])
(auto simp add: to_nat_less_card nrows_def)
qed
lemma Hermite_of_row_i_range_res:
assumes ji: "j<i" and not_zero_i_A: "¬ is_zero_row i A" and r: "res_function res"
shows "Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n ≠ 0)
∈ range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n ≠ 0)))"
proof -
let ?n="(LEAST n. A $ i $ n ≠ 0)"
define M where "M = mult_row A i (ass (A $ i $ ?n) div A $ i $ ?n)"
let ?R="row_add M j i ((res (M $ i $ ?n) (M $ j $ ?n)
- M $ j $ ?n) div M $ i $ ?n)"
have Hii: "Hermite_of_row_i ass res A i $ i $ ?n = M $ i $ ?n"
unfolding M_def by (rule Hermite_of_row_i_works2[OF not_zero_i_A])
have rw: "Hermite_of_row_i ass res A i $ j $ ?n = ?R $ j $ ?n"
unfolding M_def by (rule Hermite_of_row_i_works[OF ji not_zero_i_A])
show ?thesis
proof -
have "∀b ba. ∃bb. ba + bb * b = res b ba"
using r unfolding res_function_def by metis
thus ?thesis using rw unfolding image_def Hii row_add_def by auto
(metis (lifting) add_diff_cancel_left' nonzero_mult_div_cancel_left mult.commute mult_eq_0_iff)
qed
qed
lemma Hermite_of_upt_row_i_in_range_res:
fixes k ass res
assumes not_zero_i_A: "¬ is_zero_row i A"
and e: "echelon_form A"
and a: "ass_function ass"
and r: "res_function res"
and k: "to_nat i<k"
and k2: "k≤nrows A"
and j: "j<i"
shows "Hermite_of_upt_row_i A k ass res $ j $ (LEAST n. A $ i $ n ≠ 0)
∈ range (res (Hermite_of_upt_row_i A k ass res $ i $ (LEAST n. A $ i $ n ≠ 0)))"
using k not_zero_i_A k2
proof (induct k)
case 0 thus ?case by auto
next
case (Suc k)
let ?n="(LEAST n. A $ i $ n ≠ 0)"
have k: "k≤nrows A" using Suc.prems unfolding nrows_def by simp
have k2: "k<nrows A" using Suc.prems unfolding nrows_def by simp
define A' where "A' = foldl (Hermite_of_row_i ass res) A (map from_nat [0..<k])"
have A'_def2: "A' = Hermite_of_upt_row_i A k ass res" unfolding Hermite_of_upt_row_i_def A'_def ..
define M where "M = mult_row A' i (ass (A' $ i $ (LEAST n. A' $ i $ n ≠ 0)) div A' $ i $ (LEAST n. A' $ i $ n ≠ 0))"
have not_zero_A': "¬ is_zero_row i A'"
using Hermite_of_upt_row_preserves_nonzero_rows[OF not_zero_i_A e a r k]
unfolding A'_def Hermite_of_upt_row_i_def by simp
have e_A': "echelon_form A'" by (metis A'_def a e echelon_form_fold_Hermite_of_row_i r)
have least_eq: "(LEAST n. (Hermite_of_row_i ass res A' i) $ i $ n ≠ 0) = (LEAST n. A' $ i $ n ≠ 0)"
by (rule Least_Hermite_of_row_i[OF not_zero_A' e_A' a])
have least_eq2: "(LEAST n. A' $ i $ n ≠ 0) = (LEAST n. A $ i $ n ≠ 0)"
unfolding A'_def2
by (rule Hermite_of_upt_row_i_Least[OF not_zero_i_A e a r k])
show ?case
proof (cases "to_nat i = k")
case True
have fn_k_i: "from_nat k = i" by (metis True from_nat_to_nat_id)
have H_rw: "(Hermite_of_upt_row_i A (Suc k) ass res $ i $ (LEAST n. A $ i $ n ≠ 0))
= (Hermite_of_row_i ass res A' i $ i $ (LEAST n. A' $ i $ n ≠ 0))"
by (simp add: Hermite_of_upt_row_i_def A'_def fn_k_i least_eq2[unfolded A'_def])
have "(Hermite_of_upt_row_i A (Suc k) ass res) $ j $ (LEAST n. A $ i $ n ≠ 0) =
(Hermite_of_row_i ass res A' i) $ j $ (LEAST n. A $ i $ n ≠ 0)"
unfolding Hermite_of_upt_row_i_def
by (simp add: A'_def fn_k_i)
also have "... = (Hermite_of_row_i ass res A' i) $ j $ (LEAST n. A' $ i $ n ≠ 0)"
unfolding least_eq2 ..
also have "... ∈ range (res (Hermite_of_row_i ass res A' i $ i $ (LEAST n. A' $ i $ n ≠ 0)))"
by (rule Hermite_of_row_i_range_res[OF j not_zero_A' r])
also have "... = range ((res (Hermite_of_upt_row_i A (Suc k) ass res $ i $ (LEAST n. A $ i $ n ≠ 0))))"
unfolding H_rw ..
finally show ?thesis .
next
case False
hence i_less_k: "to_nat i < k" using Suc.prems by auto
hence i_less_k2: "i < from_nat k" using Suc.prems
by (metis from_nat_mono from_nat_to_nat_id k2 nrows_def)
show ?thesis
proof (cases "is_zero_row (from_nat k) A'")
case True
have "Hermite_of_upt_row_i A (Suc k) ass res = Hermite_of_upt_row_i A k ass res"
using True by (simp add: Hermite_of_upt_row_i_def Hermite_of_row_i_def A'_def Let_def )
thus ?thesis using Suc.hyps not_zero_i_A k i_less_k by auto
next
case False
have H_rw: "(Hermite_of_upt_row_i A (Suc k) ass res $ i $ (LEAST n. A $ i $ n ≠ 0)) =
A' $ i $ (LEAST n. A $ i $ n ≠ 0)"
proof (auto simp add: Hermite_of_upt_row_i_def A'_def[symmetric],
rule Hermite_of_row_preserves_previous_cols[OF _ False e_A'])
have "(LEAST n. A' $ i $ n ≠ 0) < (LEAST n. A' $ mod_type_class.from_nat k $ n ≠ 0)"
by (rule echelon_form_condition2_explicit[OF e_A' i_less_k2 not_zero_A' False])
thus "(LEAST n. A $ i $ n ≠ 0) < (LEAST n. A' $ mod_type_class.from_nat k $ n ≠ 0)"
unfolding least_eq2 .
qed
have "(Hermite_of_upt_row_i A (Suc k) ass res) $ j $ (LEAST n. A $ i $ n ≠ 0)
= (Hermite_of_row_i ass res A' (from_nat k)) $ j $ (LEAST n. A $ i $ n ≠ 0)"
unfolding Hermite_of_upt_row_i_def A'_def by auto
also have "... = A' $ j $ (LEAST n. A $ i $ n ≠ 0)"
proof (rule Hermite_of_row_preserves_previous_cols[OF _ False e_A'])
show "(LEAST n. A $ i $ n ≠ 0) < (LEAST n. A' $ mod_type_class.from_nat k $ n ≠ 0)"
unfolding least_eq2[symmetric]
by (rule echelon_form_condition2_explicit[OF e_A' i_less_k2 not_zero_A' False])
qed
also have "... ∈ range (res (Hermite_of_upt_row_i A k ass res $ i $ (LEAST n. A $ i $ n ≠ 0)))"
unfolding A'_def2
by (rule Suc.hyps[OF i_less_k], auto simp add: Suc.prems k)
also have "... = range (res (Hermite_of_upt_row_i A (Suc k) ass res $ i $ (LEAST n. A $ i $ n ≠ 0)))"
unfolding H_rw A'_def2 ..
finally show ?thesis .
qed
qed
qed
lemma in_residues_Hermite_of:
fixes A::"'a::{bezout_ring_div,normalization_semidom,unique_euclidean_ring}^'cols::{mod_type}^'rows::{mod_type}"
assumes a: "ass_function ass"
and r: "res_function res"
and b: "is_bezout_ext bezout"
and i: "¬ is_zero_row i (Hermite_of A ass res bezout)"
and ji: "j < i"
shows "Hermite_of A ass res bezout $ j $ (LEAST n. Hermite_of A ass res bezout $ i $ n ≠ 0)
∈ range (res (Hermite_of A ass res bezout $ i $ (LEAST n. Hermite_of A ass res bezout $ i $ n ≠ 0)))"
proof -
have non_zero_i_eA: "¬ is_zero_row i (echelon_form_of A bezout)"
using Hermite_of_preserves_zero_rows[OF _ a r b] i by auto
have e: "echelon_form (echelon_form_of A bezout)"
by (rule echelon_form_echelon_form_of[OF b])
have least: "(LEAST n. Hermite_of A ass res bezout $ i $ n ≠ 0) = (LEAST n. (echelon_form_of A bezout) $ i $ n ≠ 0)"
by (rule Hermite_of_Least[OF i a r b])
show ?thesis unfolding least
unfolding Hermite_of_def Let_def
by (rule Hermite_of_upt_row_i_in_range_res[OF non_zero_i_eA e a r _ _ ji])
(auto simp add: to_nat_less_card nrows_def)
qed
lemma Hermite_Hermite_of:
assumes a: "ass_function ass"
and r: "res_function res"
and b: "is_bezout_ext bezout"
shows "Hermite (range ass) (λc. range (res c)) (Hermite_of A ass res bezout)"
proof (rule Hermite_intro, auto)
show "Complete_set_non_associates (range ass)"
by (simp add: ass_function_Complete_set_non_associates a)
show "Complete_set_residues (λc. range (res c))"
by (simp add: r res_function_Complete_set_residues)
show "echelon_form (Hermite_of A ass res bezout)"
by (simp add: a b echelon_form_Hermite_of r)
fix i
assume i: "¬ is_zero_row i (Hermite_of A ass res bezout)"
show "Hermite_of A ass res bezout $ i $ (LEAST n. Hermite_of A ass res bezout $ i $ n ≠ 0) ∈ range ass"
by (rule in_associates_Hermite_of[OF a r b i])
next
fix i j assume i: "¬ is_zero_row i (Hermite_of A ass res bezout)" and j: "j < i"
show "Hermite_of A ass res bezout $ j $ (LEAST n. Hermite_of A ass res bezout $ i $ n ≠ 0)
∈ range (res (Hermite_of A ass res bezout $ i $ (LEAST n. Hermite_of A ass res bezout $ i $ n ≠ 0)))"
by (rule in_residues_Hermite_of[OF a r b i j])
qed
subsubsection‹Proving that the Hermite Normal Form is computed by means of elementary operations›
lemma invertible_Hermite_reduce_above:
assumes n: "n ≤ to_nat i"
shows "∃P. invertible P ∧ Hermite_reduce_above A n i j res = P ** A"
using n
proof (induct n arbitrary: A)
case 0 thus ?case by (auto, metis invertible_def matrix_mul_lid)
next
case (Suc n)
let ?R="(row_add A (from_nat n) i ((res (A $ i $ j) (A $ from_nat n $ j) - A $ from_nat n $ j) div A $ i $ j))"
obtain Q where inv_Q: "invertible Q" and H_QR: "Hermite_reduce_above ?R n i j res = Q ** ?R"
using Suc.hyps Suc.prems by auto
let ?P="(row_add (mat 1) (from_nat n) i ((res (A $ i $ j) (A $ from_nat n $ j) - A $ from_nat n $ j) div A $ i $ j))"
have inv_P: "invertible ?P"
proof (rule invertible_row_add)
show "mod_type_class.from_nat n ≠ i"
by (metis Suc.prems Suc_le_eq add_to_nat_def from_nat_mono less_irrefl
monoid_add_class.add.right_neutral to_nat_0 to_nat_less_card)
qed
have inv_QP: "invertible (Q ** ?P)" by (metis inv_P inv_Q invertible_mult)
have "Hermite_reduce_above A (Suc n) i j res = Hermite_reduce_above ?R n i j res"
by (auto simp add: Let_def)
also have "... = Q ** ?R" unfolding H_QR ..
also have "... = Q ** (?P ** A)" by (subst row_add_mat_1[symmetric], rule refl)
also have "... = (Q ** ?P) ** A" by (simp add: matrix_mul_assoc)
finally show ?case using inv_QP by auto
qed
lemma invertible_Hermite_of_row_i:
assumes a: "ass_function ass"
shows "∃P. invertible P ∧ Hermite_of_row_i ass res A i = P ** A"
unfolding Hermite_of_row_i_def
proof (auto simp add: Let_def, metis invertible_def matrix_mul_lid)
let ?n="LEAST n. A $ i $ n ≠ 0"
let ?M="mult_row A i (ass (A $ i $ ?n) div A $ i $ ?n)"
let ?P="mult_row (mat 1) i (ass (A $ i $ ?n) div A $ i $ ?n)"
let ?Ain="A $ i $ ?n"
have ass_dvd: "ass ?Ain dvd ?Ain" using a unfolding ass_function_def by (simp add: associatedD1)
have ass_dvd': "?Ain dvd ass ?Ain" using a unfolding ass_function_def by (simp add: associatedD1)
assume iA: "¬ is_zero_row i A"
have Ain_0: "A $ i $ ?n ≠ 0" by (metis (mono_tags) LeastI iA is_zero_row_def')
have ass_Ain_0: "ass (A $ i $ ?n) ≠ 0" by (metis Ain_0 ass_dvd dvd_0_left_iff)
have inv_P: "invertible ?P"
proof (rule invertible_mult_row[of _ "A $ i $ ?n div ass (A $ i $ ?n)"])
have "ass ?Ain div ?Ain * (?Ain div ass ?Ain) = (ass ?Ain div ?Ain * ?Ain) div ass ?Ain"
by (rule div_mult_swap[OF ass_dvd])
also have "... = (ass ?Ain) div ass ?Ain" unfolding dvd_div_mult_self[OF ass_dvd'] ..
also have "... = 1" using ass_Ain_0 by auto
finally show "ass ?Ain div ?Ain * (?Ain div ass ?Ain) = 1" .
have "?Ain div ass (?Ain) * (ass (?Ain) div ?Ain) = (?Ain div ass (?Ain) * ass (?Ain)) div ?Ain"
by (rule div_mult_swap[OF ass_dvd'])
also have "... = ?Ain div ?Ain" unfolding dvd_div_mult_self[OF ass_dvd] ..
also have "... = 1" using Ain_0 by simp
finally show "?Ain div ass (?Ain) * (ass (?Ain) div ?Ain) = 1" .
qed
obtain Q where inv_Q: "invertible Q" and H_QM: "Hermite_reduce_above ?M (to_nat i) i ?n res = Q ** ?M"
using invertible_Hermite_reduce_above by fast
have inv_QP: "invertible (Q**?P)"
by (metis inv_P inv_Q invertible_mult)
have "Hermite_reduce_above ?M (to_nat i) i ?n res = Q ** ?M" by (rule H_QM)
also have "... = Q ** (?P ** A)" by (subst mult_row_mat_1[symmetric], rule refl)
also have "... = (Q ** ?P) ** A" by (simp add: matrix_mul_assoc)
finally show "∃P. invertible P ∧ Hermite_reduce_above ?M (to_nat i) i ?n res = P ** A"
using inv_QP by auto
qed
lemma invertible_Hermite_of_upt_row_i:
assumes a: "ass_function ass"
shows "∃P. invertible P ∧ Hermite_of_upt_row_i A k ass res = P ** A"
proof (induct k arbitrary: A)
case 0
thus ?case unfolding Hermite_of_upt_row_i_def by (auto, metis invertible_def matrix_mul_lid)
next
case (Suc k)
obtain Q where inv_Q: "invertible Q" and H_QA: "Hermite_of_upt_row_i A k ass res = Q ** A"
using Suc.hyps by auto
obtain P where inv_P: "invertible P"
and H_PH: "Hermite_of_row_i ass res (Hermite_of_upt_row_i A k ass res) (from_nat k)
= P ** (Hermite_of_upt_row_i A k ass res)" using invertible_Hermite_of_row_i[OF a] by blast
have inv_PQ: "invertible (P**Q)" by (simp add: inv_P inv_Q invertible_mult)
have "Hermite_of_upt_row_i A (Suc k) ass res
= Hermite_of_row_i ass res (Hermite_of_upt_row_i A k ass res) (from_nat k)"
unfolding Hermite_of_upt_row_i_def by auto
also have "... = P ** (Hermite_of_upt_row_i A k ass res)" unfolding H_PH ..
also have "... = P ** (Q ** A)" unfolding H_QA ..
also have "... = (P ** Q) ** A" by (simp add: matrix_mul_assoc)
finally show ?case using inv_PQ by blast
qed
lemma invertible_Hermite_of:
fixes A::"'a::{bezout_ring_div,normalization_semidom,unique_euclidean_ring}^'cols::{mod_type}^'rows::{mod_type}"
assumes a: "ass_function ass"
and b: "is_bezout_ext bezout"
shows "∃P. invertible P ∧ Hermite_of A ass res bezout = P ** A"
proof -
obtain P where inv_P: "invertible P"
and H_PH: "Hermite_of_upt_row_i (echelon_form_of A bezout) (nrows A) ass res
= P ** (echelon_form_of A bezout)" using invertible_Hermite_of_upt_row_i[OF a] by blast
obtain Q where inv_Q: "invertible Q" and E_QA: "(echelon_form_of A bezout) = Q ** A"
using echelon_form_of_invertible[OF b, of A] by auto
have inv_PQ: "invertible (P**Q)" by (simp add: inv_P inv_Q invertible_mult)
have "Hermite_of A ass res bezout
= Hermite_of_upt_row_i (echelon_form_of A bezout) (nrows A) ass res"
unfolding Hermite_of_def Let_def ..
also have "... = P ** (Q ** A)" unfolding H_PH unfolding E_QA ..
also have "... = (P ** Q) ** A" by (simp add: matrix_mul_assoc)
finally show ?thesis using inv_PQ by blast
qed
subsubsection‹The final theorem›
lemma Hermite:
assumes a: "ass_function ass"
and r: "res_function res"
and b: "is_bezout_ext bezout"
shows "∃P. invertible P ∧ (Hermite_of A ass res bezout) = P ** A ∧
Hermite (range ass) (λc. range (res c)) (Hermite_of A ass res bezout)"
using invertible_Hermite_of[OF a b] Hermite_Hermite_of[OF a r b] by fast
subsection‹Proving the uniqueness of the Hermite Normal Form›
lemma diagonal_least_nonzero:
fixes H :: "(('a :: {bezout_ring_div, normalization_euclidean_semiring, unique_euclidean_ring}, 'b :: mod_type) vec, 'b) vec"
assumes H: "Hermite associates residues H"
and inv_H: "invertible H" and up_H: "upper_triangular H"
shows "(LEAST n. H $ i $ n ≠ 0) = i"
proof (rule Least_equality)
show "H $ i $ i ≠ 0"
by (metis (full_types) inv_H invertible_iff_is_unit is_unit_diagonal not_is_unit_0 up_H)
fix y
assume Hiy: "H $ i $ y ≠ 0"
show "i ≤ y"
using up_H unfolding upper_triangular_def
by (metis (poly_guards_query) Hiy not_less)
qed
lemma diagonal_in_associates:
fixes H :: "(('a :: {bezout_ring_div, normalization_euclidean_semiring, unique_euclidean_ring}, 'b :: mod_type) vec, 'b) vec"
assumes H: "Hermite associates residues H"
and inv_H: "invertible H" and up_H: "upper_triangular H"
shows "H $ i $ i ∈ associates"
proof -
have "H $ i $ i ≠ 0"
by (metis (full_types) inv_H invertible_iff_is_unit is_unit_diagonal not_is_unit_0 up_H)
hence "¬ is_zero_row i H" unfolding is_zero_row_def is_zero_row_upt_k_def ncols_def by auto
thus ?thesis using H unfolding Hermite_def unfolding diagonal_least_nonzero[OF H inv_H up_H]
by auto
qed
lemma above_diagonal_in_residues:
fixes H :: "(('a :: {bezout_ring_div, normalization_euclidean_semiring, unique_euclidean_ring}, 'b :: mod_type) vec, 'b) vec"
assumes H: "Hermite associates residues H"
and inv_H: "invertible H" and up_H: "upper_triangular H"
and j_i: "j<i"
shows "H $ j $ (LEAST n. H $ i $ n ≠ 0) ∈ residues (H $ i $ (LEAST n. H $ i $ n ≠ 0))"
proof -
have "H $ i $ i ≠ 0"
by (metis (full_types) inv_H invertible_iff_is_unit is_unit_diagonal not_is_unit_0 up_H)
hence "¬ is_zero_row i H" unfolding is_zero_row_def is_zero_row_upt_k_def ncols_def by auto
thus ?thesis using H j_i unfolding Hermite_def unfolding diagonal_least_nonzero[OF H inv_H up_H]
by auto
qed
text‹The uniqueness of the Hermite Normal Form is proven following the proof presented in the book
Integral Matrices (1972) by Morris Newman.›
lemma Hermite_unique:
fixes K::"'a::{bezout_ring_div,normalization_euclidean_semiring,unique_euclidean_ring}^'n::mod_type^'n::mod_type"
assumes A_PH: "A = P ** H"
and A_QK: "A = Q ** K"
and inv_A: "invertible A"
and inv_P: "invertible P"
and inv_Q: "invertible Q"
and H: "Hermite associates residues H"
and K: "Hermite associates residues K"
shows "H = K"
proof -
have cs_residues: "Complete_set_residues residues" using H unfolding Hermite_def by simp
have inv_H: "invertible H"
by (metis A_PH inv_A inv_P invertible_def invertible_mult matrix_mul_assoc matrix_mul_lid)
have inv_K: "invertible K"
by (metis A_QK inv_A inv_Q invertible_def invertible_mult matrix_mul_assoc matrix_mul_lid)
define U where "U = (matrix_inv P)**Q"
have inv_U: "invertible U"
by (metis U_def inv_P inv_Q invertible_def invertible_mult matrix_inv_left matrix_inv_right)
have H_UK: "H = U ** K" using A_PH A_QK inv_P
by (metis U_def matrix_inv_left matrix_mul_assoc matrix_mul_lid)
have "det K *k U = H ** adjugate K"
unfolding H_UK matrix_mul_assoc[symmetric] mult_adjugate_det matrix_mul_mat ..
have upper_triangular_H: "upper_triangular H"
by (metis H Hermite_def echelon_form_imp_upper_triagular)
have upper_triangular_K: "upper_triangular K"
by (metis K Hermite_def echelon_form_imp_upper_triagular)
have upper_triangular_U: "upper_triangular U"
by (metis H_UK inv_K matrix_inv_right matrix_mul_assoc matrix_mul_rid upper_triangular_H
upper_triangular_K upper_triangular_inverse upper_triangular_mult)
have unit_det_U: "is_unit (det U)" by (metis inv_U invertible_iff_is_unit)
have is_unit_diagonal_U: "(∀i. is_unit (U $ i $ i))"
by (rule is_unit_diagonal[OF upper_triangular_U unit_det_U])
have Uii_1: "(∀i. (U $ i $ i) = 1)" and Hii_Kii: "(∀i. (H $ i $ i) = (K $ i $ i))"
proof (auto)
fix i
have Hii: "H $ i $ i ∈ associates"
by (rule diagonal_in_associates[OF H inv_H upper_triangular_H])
have Kii: "K $ i $ i ∈ associates"
by (rule diagonal_in_associates[OF K inv_K upper_triangular_K])
have ass_Hii_Kii: "normalize (H $ i $ i) = normalize (K $ i $ i)"
by (meson associatedI inv_H inv_K invertible_iff_is_unit is_unit_diagonal
unit_imp_dvd upper_triangular_H upper_triangular_K)
show Hii_eq_Kii: "H $ i $ i = K $ i $ i"
by (metis Hermite_def Hii K Kii ass_Hii_Kii in_Ass_not_associated)
have "H $ i $ i = U $ i $ i * K $ i $ i"
by (metis H_UK upper_triangular_K upper_triangular_U upper_triangular_mult_diagonal)
thus "U $ i $ i = 1" unfolding Hii_eq_Kii mult_cancel_right1
by (metis Hii_eq_Kii inv_H invertible_iff_is_unit
is_unit_diagonal not_is_unit_0 upper_triangular_H)
qed
have zero_above: "∀j s. j≥1 ∧ j < ncols A - to_nat s ⟶ U $ s $ (s + from_nat j) = 0"
proof (clarify)
fix j s assume "1 ≤ j" and "j < ncols A - (to_nat (s::'n))"
thus "U $ s $ (s + from_nat j) = 0"
proof (induct j rule: less_induct)
fix p
assume induct_step: "(⋀y. y < p ⟹ 1 ≤ y ⟹ y < ncols A - to_nat s ⟹ U $ s $ (s + from_nat y) = 0)"
and p1: "1 ≤ p" and p2: "p < ncols A - to_nat s"
have s_less: "s < s + from_nat p" using p1 p2 unfolding ncols_def
by (metis One_nat_def add.commute add_diff_cancel_right' add_lessD1 add_to_nat_def
from_nat_to_nat_id less_diff_conv neq_iff not_le
to_nat_from_nat_id to_nat_le zero_less_Suc)
show "U $ s $ (s + from_nat p) = 0"
proof -
have UNIV_rw: "UNIV = insert s (UNIV-{s})" by auto
have UNIV_s_rw: "UNIV-{s} = insert (s + from_nat p) ((UNIV-{s}) - {s + from_nat p})"
using p1 p2 s_less unfolding ncols_def by (auto simp: algebra_simps)
have sum_rw: "(∑k∈UNIV-{s}. U $ s $ k * K $ k $ (s + from_nat p))
= U $ s $ (s + from_nat p) * K $ (s + from_nat p) $ (s + from_nat p)
+ (∑k∈(UNIV-{s})-{s + from_nat p}. U $ s $ k * K $ k $ (s + from_nat p))"
using UNIV_s_rw sum.insert by (metis (erased, lifting) Diff_iff finite singletonI)
have sum_0: "(∑k∈(UNIV-{s})-{s + from_nat p}. U $ s $ k * K $ k $ (s + from_nat p)) = 0"
proof (rule sum.neutral, rule)
fix x assume x: "x ∈ UNIV - {s} - {s + from_nat p}"
show "U $ s $ x * K $ x $ (s + from_nat p) = 0"
proof (cases "x<s")
case True
thus ?thesis using upper_triangular_U unfolding upper_triangular_def
by auto
next
case False
hence x_g_s: "x>s" using x by (metis Diff_iff neq_iff singletonI)
show ?thesis
proof (cases "x<s+from_nat p")
case True
define a where "a = to_nat x - to_nat s"
from x_g_s have "to_nat s < to_nat x" by (rule to_nat_mono)
hence xa: "x=s+(from_nat a)" unfolding a_def add_to_nat_def
by (simp add: less_imp_diff_less to_nat_less_card algebra_simps to_nat_from_nat_id)
have "U $ s $ x =0"
proof (unfold xa, rule induct_step)
show a_p: "a<p" unfolding a_def using p2 unfolding ncols_def
proof -
have "x < from_nat (to_nat s + to_nat (from_nat p::'n))"
by (metis (no_types) True add_to_nat_def)
hence "to_nat x - to_nat s < to_nat (from_nat p::'n)"
by (simp add: add.commute less_diff_conv2 less_imp_le to_nat_le x_g_s)
thus "to_nat x - to_nat s < p"
by (metis (no_types) from_nat_eq_imp_eq from_nat_to_nat_id le_less_trans
less_imp_le not_le to_nat_less_card)
qed
show "1 ≤ a"
by (auto simp add: a_def p1 p2) (metis Suc_leI to_nat_mono x_g_s zero_less_diff)
show "a < ncols A - to_nat s" using a_p p2 by auto
qed
thus ?thesis by simp
next
case False
hence "x>s+from_nat p" using x_g_s x by auto
thus ?thesis using upper_triangular_K unfolding upper_triangular_def
by auto
qed
qed
qed
have "H $ s $ (s + from_nat p) = (∑k∈UNIV. U $ s $ k * K $ k $ (s + from_nat p))"
unfolding H_UK matrix_matrix_mult_def by auto
also have "... = (∑k∈insert s (UNIV-{s}). U $ s $ k * K $ k $ (s + from_nat p))"
using UNIV_rw by simp
also have "... = U $ s $ s * K $ s $ (s + from_nat p)
+ (∑k∈UNIV-{s}. U $ s $ k * K $ k $ (s + from_nat p))"
by (rule sum.insert, simp_all)
also have "... = U $ s $ s * K $ s $ (s + from_nat p)
+ U $ s $ (s + from_nat p) * K $ (s + from_nat p) $ (s + from_nat p)"
unfolding sum_rw sum_0 by simp
finally have H_s_sp: "H $ s $ (s + from_nat p)
= U $ s $ (s + from_nat p) * K $ (s + from_nat p) $ (s + from_nat p) + K $ s $ (s + from_nat p)"
using Uii_1 by auto
hence cong_HK: "cong (H $ s $ (s + from_nat p)) (K $ s $ (s + from_nat p)) (K $ (s+from_nat p) $ (s + from_nat p))"
unfolding cong_def by auto
have H_s_sp_residues: "(H $ s $ (s + from_nat p)) ∈ residues (K $ (s+from_nat p) $ (s + from_nat p))"
using above_diagonal_in_residues[OF H inv_H upper_triangular_H s_less]
unfolding diagonal_least_nonzero[OF H inv_H upper_triangular_H]
by (metis Hii_Kii)
have K_s_sp_residues: "(K $ s $ (s + from_nat p)) ∈ residues (K $ (s+from_nat p) $ (s + from_nat p))"
using above_diagonal_in_residues[OF K inv_K upper_triangular_K s_less]
unfolding diagonal_least_nonzero[OF K inv_K upper_triangular_K] .
have Hs_sp_Ks_sp: "(H $ s $ (s + from_nat p)) = (K $ s $ (s + from_nat p))"
using cong_HK in_Res_not_congruent[OF cs_residues H_s_sp_residues K_s_sp_residues]
by fast
have "is_unit (K $ (s + from_nat p) $ (s + from_nat p))"
by (metis Hii_Kii inv_H invertible_iff_is_unit is_unit_diagonal upper_triangular_H)
hence "K $ (s + from_nat p) $ (s + from_nat p) ≠ 0" by (metis not_is_unit_0)
thus ?thesis unfolding from_nat_1 using H_s_sp unfolding Hs_sp_Ks_sp by auto
qed
qed
qed
have "U = mat 1"
proof (unfold mat_def vec_eq_iff, auto)
fix ia show "U $ ia $ ia = 1" using Uii_1 by simp
fix i assume i_ia: "i ≠ ia"
show "U $ i $ ia = 0"
proof (cases "ia<i")
case True
thus ?thesis using upper_triangular_U unfolding upper_triangular_def by auto
next
case False
hence i_less_ia: "i<ia" using i_ia by auto
define a where "a = to_nat ia - to_nat i"
have ia_eq: "ia = i + from_nat a" unfolding a_def
by (metis i_less_ia a_def add_to_nat_def dual_order.strict_iff_order from_nat_to_nat_id
le_add_diff_inverse less_imp_diff_less to_nat_from_nat_id to_nat_less_card to_nat_mono)
have "1 ≤ a" unfolding a_def
by (metis diff_is_0_eq i_less_ia less_one not_less to_nat_mono)
moreover have "a < ncols A - to_nat i"
unfolding a_def ncols_def
by (metis False diff_less_mono not_less to_nat_less_card to_nat_mono')
ultimately show ?thesis using zero_above unfolding ia_eq by blast
qed
qed
thus ?thesis using H_UK matrix_mul_lid by fast
qed
subsection‹Examples of execution›
value[code] "let A = list_of_list_to_matrix ([[37,8,6],[5,4,-8],[3,24,-7]])::int^3^3
in matrix_to_list_of_list (Hermite_of A ass_function_euclidean res_function_euclidean euclid_ext2)"
value[code] "let A = list_of_list_to_matrix ([[[:3,4,5:],[:-2,1:]],[[:-1,0,2:],[:0,1,4,1:]]])::real poly^2^2
in matrix_to_list_of_list (Hermite_of A ass_function_euclidean res_function_euclidean euclid_ext2)"
end