# Theory Uniqueness_Hermite_JNF

section ‹Uniqueness of Hermite normal form in JNF›

text ‹This theory contains the proof of the uniqueness theorem of the Hermite normal form in JNF,
moved from HOL Analysis.›

theory Uniqueness_Hermite_JNF
imports
Hermite.Hermite
Uniqueness_Hermite
Smith_Normal_Form.SNF_Missing_Lemmas
Smith_Normal_Form.Mod_Type_Connect
Smith_Normal_Form.Finite_Field_Mod_Type_Connection
begin

hide_const (open) residues

text ‹We first define some properties that currently exist in HOL Analysis, but not in
JNF, namely a predicate for being in echelon form, another one for being in Hermite normal form,
definition of a row of zeros up to a concrete position, and so on.›

definition is_zero_row_upt_k_JNF :: "nat  => nat =>'a::{zero} mat => bool"
where "is_zero_row_upt_k_JNF i k A = (∀j. j < k ⟶ A $$(i,j) = 0)" definition is_zero_row_JNF :: "nat =>'a::{zero} mat => bool" where "is_zero_row_JNF i A = (∀j<dim_col A. A$$ (i, j) = 0)"

lemma echelon_form_def':
"echelon_form A = (
(∀i. is_zero_row i A ⟶ ¬ (∃j. j>i ∧ ¬ is_zero_row j A))
∧
(∀i j. i<j ∧ ¬ (is_zero_row i A) ∧ ¬ (is_zero_row j A)
⟶ ((LEAST n. A $i$ n ≠ 0) < (LEAST n. A $j$ n ≠ 0))))"
unfolding echelon_form_def echelon_form_upt_k_def unfolding is_zero_row_def by auto

definition
echelon_form_JNF :: "'a::{bezout_ring} mat ⇒ bool"
where
"echelon_form_JNF A = (
(∀i<dim_row A. is_zero_row_JNF i A ⟶ ¬ (∃j. j < dim_row A ∧ j>i ∧ ¬ is_zero_row_JNF j A))
∧
(∀i j. i<j ∧ j<dim_row A ∧ ¬ (is_zero_row_JNF i A) ∧ ¬ (is_zero_row_JNF j A)
⟶ ((LEAST n. A $$(i, n) ≠ 0) < (LEAST n. A$$ (j, n) ≠ 0))))"

text ‹Now, we connect the existing definitions in HOL Analysis to the ones just defined in JNF by
means of transfer rules.›

context includes lifting_syntax
begin

lemma HMA_is_zero_row_mod_type[transfer_rule]:
"((Mod_Type_Connect.HMA_I) ===> (Mod_Type_Connect.HMA_M :: _ ⇒ 'a :: comm_ring_1 ^ 'n :: mod_type ^ 'm :: mod_type ⇒ _)
===> (=)) is_zero_row_JNF is_zero_row"
proof (intro rel_funI, goal_cases)
case (1 i i' A A')
note ii' = "1"(1)[transfer_rule]
note AA' = "1"(2)[transfer_rule]
have "(∀j<dim_col A. A $$(i, j) = 0) = (∀j. A' h i' h j = 0)" proof (rule;rule+) fix j'::'n assume Aij_0: "∀j<dim_col A. A$$ (i, j) = 0"
define j where "j = mod_type_class.to_nat j'"
have [transfer_rule]: "Mod_Type_Connect.HMA_I j j'" unfolding Mod_Type_Connect.HMA_I_def j_def by auto
have A_ij0': "A $$(i,j) = 0" using Aij_0 unfolding j_def by (metis AA' Mod_Type_Connect.HMA_M_def Mod_Type_Connect.from_hma⇩m_def dim_col_mat(1) mod_type_class.to_nat_less_card) hence "index_hma A' i' j' = 0" by transfer thus "A' h i' h j' = 0" unfolding index_hma_def by simp next fix j assume 1: "∀j'. A' h i' h j' = 0" and 2: "j < dim_col A" define j'::'n where "j' = mod_type_class.from_nat j" have [transfer_rule]: "Mod_Type_Connect.HMA_I j j'" unfolding Mod_Type_Connect.HMA_I_def j'_def using Mod_Type.to_nat_from_nat_id[of j, where ?'a = 'n] 2 using AA' Mod_Type_Connect.dim_col_transfer_rule by force have "A' h i' h j' = 0" using 1 by auto hence "index_hma A' i' j' = 0" unfolding index_hma_def by simp thus "A$$ (i, j) = 0" by transfer
qed
thus ?case unfolding is_zero_row_def' is_zero_row_JNF_def by auto
qed

lemma HMA_echelon_form_mod_type[transfer_rule]:
"((Mod_Type_Connect.HMA_M :: _ ⇒ 'a ::bezout_ring ^ 'n :: mod_type ^ 'm :: mod_type ⇒ _) ===> (=))
echelon_form_JNF echelon_form"
proof (intro rel_funI, goal_cases)
case (1 A A')
note AA' = "1"(1)[transfer_rule]
have 1: "(∀i<dim_row A. is_zero_row_JNF i A ⟶ ¬ (∃j < dim_row A. j>i ∧ ¬ is_zero_row_JNF j A))
= (∀i. is_zero_row i A' ⟶ ¬ (∃j>i. ¬ is_zero_row j A'))"
proof (auto)
fix i' j' assume 1: "∀i<dim_row A. is_zero_row_JNF i A ⟶ (∀j>i. j < dim_row A ⟶ is_zero_row_JNF j A)"
and 2: "is_zero_row i' A'" and 3: "i' < j'"
let ?i = "Mod_Type.to_nat i'"
let ?j = "Mod_Type.to_nat j'"
have ii'[transfer_rule]: "Mod_Type_Connect.HMA_I ?i i'" and jj'[transfer_rule]: "Mod_Type_Connect.HMA_I ?j j'"
unfolding Mod_Type_Connect.HMA_I_def by auto
have "is_zero_row_JNF ?i A" using 2 by transfer'
hence "is_zero_row_JNF ?j A" using 1 3 to_nat_mono
by (metis AA' Mod_Type_Connect.HMA_M_def Mod_Type_Connect.from_hma⇩m_def
dim_row_mat(1) mod_type_class.to_nat_less_card)
thus "is_zero_row j' A'" by transfer'
next
fix i j assume 1: "∀i'. is_zero_row i' A' ⟶ (∀j'>i'. is_zero_row j' A')"
and 2: "is_zero_row_JNF i A" and 3: "i < j" and 4: "j<dim_row A"
let ?i' = "Mod_Type.from_nat i::'m"
let ?j' = "Mod_Type.from_nat j::'m"
have ii'[transfer_rule]: "Mod_Type_Connect.HMA_I i ?i'"
unfolding Mod_Type_Connect.HMA_I_def using Mod_Type.to_nat_from_nat_id[of i]
using 3 4 AA' Mod_Type_Connect.dim_row_transfer_rule less_trans by fastforce
have jj'[transfer_rule]: "Mod_Type_Connect.HMA_I j ?j'"
unfolding Mod_Type_Connect.HMA_I_def  using Mod_Type.to_nat_from_nat_id[of j]
using 3 4 AA' Mod_Type_Connect.dim_row_transfer_rule less_trans by fastforce
have "is_zero_row ?i' A'" using 2 by transfer
moreover have "?i' < ?j'" using 3 4 AA' Mod_Type_Connect.dim_row_transfer_rule from_nat_mono by fastforce
ultimately have "is_zero_row ?j' A'" using 1 3 by auto
thus "is_zero_row_JNF j A" by transfer
qed
have 2: "((∀i j. i<j ∧ ¬ (is_zero_row i A') ∧ ¬ (is_zero_row j A')
⟶ ((LEAST n. A' $h i$h n ≠ 0) < (LEAST n. A' $h j$h n ≠ 0))))
= (∀i j. i<j ∧ j<dim_row A ∧ ¬ (is_zero_row_JNF i A) ∧ ¬ (is_zero_row_JNF j A)
⟶ ((LEAST n. A $$(i, n) ≠ 0) < (LEAST n. A$$ (j, n) ≠ 0)))"
proof (auto)
fix i j assume 1: "∀i' j'. i' < j' ∧ ¬ is_zero_row i' A' ∧ ¬ is_zero_row j' A'
⟶ (LEAST n'. A' $h i'$h n' ≠ 0) < (LEAST n'. A' $h j'$h n' ≠ 0)"
and ij: "i < j" and j: "j < dim_row A" and i0: "¬ is_zero_row_JNF i A"
and j0: "¬ is_zero_row_JNF j A"
let ?i' = "Mod_Type.from_nat i::'m"
let ?j' = "Mod_Type.from_nat j::'m"
have ii'[transfer_rule]: "Mod_Type_Connect.HMA_I i ?i'"
unfolding Mod_Type_Connect.HMA_I_def using Mod_Type.to_nat_from_nat_id[of i]
using ij j AA' Mod_Type_Connect.dim_row_transfer_rule less_trans by fastforce
have jj'[transfer_rule]: "Mod_Type_Connect.HMA_I j ?j'"
unfolding Mod_Type_Connect.HMA_I_def  using Mod_Type.to_nat_from_nat_id[of j]
using ij j AA' Mod_Type_Connect.dim_row_transfer_rule less_trans by fastforce
have i'0: "¬ is_zero_row ?i' A'" using i0 by transfer
have j'0: "¬ is_zero_row ?j' A'" using j0 by transfer
have i'j': "?i' < ?j'"
using AA' Mod_Type_Connect.dim_row_transfer_rule from_nat_mono ij j by fastforce
have l1l2: "(LEAST n'. A' $h ?i'$h n' ≠ 0) < (LEAST n'. A' $h ?j'$h n' ≠ 0)"
using 1 i'0 j'0 i'j' by auto
define l1 where "l1 = (LEAST n'. A' $h ?i'$h n' ≠ 0)"
define l2 where "l2 = (LEAST n'. A' $h ?j'$h n' ≠ 0)"
let ?least_n1 = "Mod_Type.to_nat l1"
let ?least_n2 = "Mod_Type.to_nat l2"
have l1[transfer_rule]: "Mod_Type_Connect.HMA_I ?least_n1 l1" and [transfer_rule]: "Mod_Type_Connect.HMA_I ?least_n2 l2"
unfolding Mod_Type_Connect.HMA_I_def by auto
have "(LEAST n. A $$(i, n) ≠ 0) = ?least_n1" proof (rule Least_equality) obtain n' where n'1: "A$$ (i,n') ≠ 0" and n'2: "n'<dim_col A"
using i0 unfolding is_zero_row_JNF_def by auto
let ?n' = "Mod_Type.from_nat n'::'n"
have n'n'[transfer_rule]: "Mod_Type_Connect.HMA_I n' ?n'"
unfolding Mod_Type_Connect.HMA_I_def using Mod_Type.to_nat_from_nat_id n'2
using AA' Mod_Type_Connect.dim_col_transfer_rule by fastforce
have "index_hma A' ?i' ?n' ≠ 0" using n'1 by transfer
hence A'i'n': "A' $h ?i'$h ?n' ≠ 0" unfolding index_hma_def by simp
have least_le_n': "(LEAST n. A $$(i, n) ≠ 0) ≤ n'" by (simp add: Least_le n'1) have l1_le_n': "l1 ≤ ?n'" by (simp add: A'i'n' Least_le l1_def) have "A$$ (i, ?least_n1) = index_hma A' ?i' l1" by (transfer, simp)
also have "... = A' $h mod_type_class.from_nat i$h l1" unfolding index_hma_def by simp
also have "... ≠ 0" unfolding l1_def by (metis (mono_tags, lifting) LeastI i'0 is_zero_row_def')
finally show "A $$(i, mod_type_class.to_nat l1) ≠ 0" . fix y assume Aiy: "A$$ (i, y) ≠ 0"
let ?y' = "Mod_Type.from_nat y::'n"
show "Mod_Type.to_nat l1 ≤ y"
proof (cases "y≤n'")
case True
hence y: "y < dim_col A" using n'2 by auto
have yy'[transfer_rule]: "Mod_Type_Connect.HMA_I y ?y'" unfolding Mod_Type_Connect.HMA_I_def
apply (rule Mod_Type.to_nat_from_nat_id[symmetric])
using y Mod_Type_Connect.dim_col_transfer_rule[OF AA'] by auto
have "Mod_Type.to_nat l1 ≤ Mod_Type.to_nat ?y'"
proof (rule to_nat_mono')
have "index_hma A' ?i' ?y' ≠ 0" using Aiy by transfer
hence "A' $h ?i'$h ?y' ≠ 0" unfolding index_hma_def by simp
thus "l1 ≤ ?y'" unfolding l1_def by (simp add: Least_le)
qed
then show ?thesis by (metis Mod_Type_Connect.HMA_I_def yy')
next
case False
hence "n' < y" by auto
then show ?thesis
by (metis False Mod_Type_Connect.HMA_I_def dual_order.trans l1_le_n' linear n'n' to_nat_mono')
qed
qed
moreover have "(LEAST n. A $$(j, n) ≠ 0) = ?least_n2" proof (rule Least_equality) obtain n' where n'1: "A$$ (j,n') ≠ 0" and n'2: "n'<dim_col A"
using j0 unfolding is_zero_row_JNF_def by auto
let ?n' = "Mod_Type.from_nat n'::'n"
have n'n'[transfer_rule]: "Mod_Type_Connect.HMA_I n' ?n'"
unfolding Mod_Type_Connect.HMA_I_def using Mod_Type.to_nat_from_nat_id n'2
using AA' Mod_Type_Connect.dim_col_transfer_rule by fastforce
have "index_hma A' ?j' ?n' ≠ 0" using n'1 by transfer
hence A'i'n': "A' $h ?j'$h ?n' ≠ 0" unfolding index_hma_def by simp
have least_le_n': "(LEAST n. A $$(j, n) ≠ 0) ≤ n'" by (simp add: Least_le n'1) have l1_le_n': "l2 ≤ ?n'" by (simp add: A'i'n' Least_le l2_def) have "A$$ (j, ?least_n2) = index_hma A' ?j' l2" by (transfer, simp)
also have "... = A' $h ?j'$h l2" unfolding index_hma_def by simp
also have "... ≠ 0" unfolding l2_def by (metis (mono_tags, lifting) LeastI j'0 is_zero_row_def')
finally show "A $$(j, mod_type_class.to_nat l2) ≠ 0" . fix y assume Aiy: "A$$ (j, y) ≠ 0"
let ?y' = "Mod_Type.from_nat y::'n"
show "Mod_Type.to_nat l2 ≤ y"
proof (cases "y≤n'")
case True
hence y: "y < dim_col A" using n'2 by auto
have yy'[transfer_rule]: "Mod_Type_Connect.HMA_I y ?y'" unfolding Mod_Type_Connect.HMA_I_def
apply (rule Mod_Type.to_nat_from_nat_id[symmetric])
using y Mod_Type_Connect.dim_col_transfer_rule[OF AA'] by auto
have "Mod_Type.to_nat l2 ≤ Mod_Type.to_nat ?y'"
proof (rule to_nat_mono')
have "index_hma A' ?j' ?y' ≠ 0" using Aiy by transfer
hence "A' $h ?j'$h ?y' ≠ 0" unfolding index_hma_def by simp
thus "l2 ≤ ?y'" unfolding l2_def by (simp add: Least_le)
qed
then show ?thesis by (metis Mod_Type_Connect.HMA_I_def yy')
next
case False
hence "n' < y" by auto
then show ?thesis
by (metis False Mod_Type_Connect.HMA_I_def dual_order.trans l1_le_n' linear n'n' to_nat_mono')
qed
qed
ultimately show "(LEAST n. A $$(i, n) ≠ 0) < (LEAST n. A$$ (j, n) ≠ 0)"
using l1l2 unfolding l1_def l2_def by (simp add: to_nat_mono)
next
fix i' j' assume 1: "∀i j. i < j ∧ j < dim_row A ∧ ¬ is_zero_row_JNF i A ∧ ¬ is_zero_row_JNF j A
⟶ (LEAST n. A $$(i, n) ≠ 0) < (LEAST n. A$$ (j, n) ≠ 0)"
and i'j': "i' < j'" and i': "¬ is_zero_row i' A'" and j': "¬ is_zero_row j' A'"
let ?i = "Mod_Type.to_nat i'"
let ?j = "Mod_Type.to_nat j'"
have [transfer_rule]: "Mod_Type_Connect.HMA_I ?i i'"
and [transfer_rule]: "Mod_Type_Connect.HMA_I ?j j'"
unfolding Mod_Type_Connect.HMA_I_def by auto
have i: "¬ is_zero_row_JNF ?i A" using i' by transfer'
have j: "¬ is_zero_row_JNF ?j A" using j' by transfer'
have ij: "?i < ?j" using i'j' to_nat_mono by blast
have j_dim_row: "?j < dim_row A"
using AA' Mod_Type_Connect.dim_row_transfer_rule mod_type_class.to_nat_less_card by fastforce
have least_ij: "(LEAST n. A $$(?i, n) ≠ 0) < (LEAST n. A$$ (?j, n) ≠ 0)"
using i j ij j_dim_row 1 by auto
define l1 where "l1 = (LEAST n'. A $$(?i, n') ≠ 0)" define l2 where "l2 = (LEAST n'. A$$ (?j, n') ≠ 0)"
let ?least_n1 = "Mod_Type.from_nat l1::'n"
let ?least_n2 = "Mod_Type.from_nat l2::'n"
have l1_dim_col: "l1 < dim_col A"
by (smt is_zero_row_JNF_def j l1_def leI le_less_trans least_ij less_trans not_less_Least)
have l2_dim_col: "l2 < dim_col A"
by (metis (mono_tags, lifting) Least_le is_zero_row_JNF_def j l2_def le_less_trans)
have [transfer_rule]: "Mod_Type_Connect.HMA_I l1 ?least_n1" unfolding Mod_Type_Connect.HMA_I_def
using AA' Mod_Type_Connect.dim_col_transfer_rule l1_dim_col Mod_Type.to_nat_from_nat_id
by fastforce
have [transfer_rule]: "Mod_Type_Connect.HMA_I l2 ?least_n2" unfolding Mod_Type_Connect.HMA_I_def
using AA' Mod_Type_Connect.dim_col_transfer_rule l2_dim_col Mod_Type.to_nat_from_nat_id
by fastforce
have "(LEAST n. A' $h i'$h n ≠ 0) = ?least_n1"
proof (rule Least_equality)
obtain n' where n'1: "A' $h i'$h n' ≠ 0" using i' unfolding is_zero_row_def' by auto
have "A' $h i'$h ?least_n1 = index_hma A' i' ?least_n1" unfolding index_hma_def by simp
also have "... = A$$(?i, l1)" by (transfer, simp) also have "... ≠ 0" by (metis (mono_tags, lifting) LeastI i is_zero_row_JNF_def l1_def) finally show "A' h i' h ?least_n1 ≠ 0" . next fix y assume y: "A' h i' h y ≠ 0" let ?y' = "Mod_Type.to_nat y" have [transfer_rule]: "Mod_Type_Connect.HMA_I ?y' y" unfolding Mod_Type_Connect.HMA_I_def by simp have "?least_n1 ≤ Mod_Type.from_nat ?y'" proof (unfold l1_def, rule from_nat_mono') show "Mod_Type.to_nat y < CARD('n)" by (simp add: mod_type_class.to_nat_less_card) have *: "A$$ (mod_type_class.to_nat i', mod_type_class.to_nat y) ≠ 0"
using y[unfolded index_hma_def[symmetric]] by transfer'
show "(LEAST n'. A $$(mod_type_class.to_nat i', n') ≠ 0) ≤ mod_type_class.to_nat y" by (rule Least_le, simp add: *) qed also have "... = y" by simp finally show "?least_n1 ≤ y" . qed moreover have "(LEAST n. A' h j' h n ≠ 0) = ?least_n2" proof (rule Least_equality) obtain n' where n'1: "A' h j' h n' ≠ 0" using j' unfolding is_zero_row_def' by auto have "A' h j' h ?least_n2 = index_hma A' j' ?least_n2" unfolding index_hma_def by simp also have "... = A$$ (?j, l2)"  by (transfer, simp)
also have "... ≠ 0" by (metis (mono_tags, lifting) LeastI j is_zero_row_JNF_def l2_def)
finally show "A' $h j'$h ?least_n2 ≠ 0" .
next
fix y assume y: "A' $h j'$h y ≠ 0"
let ?y' = "Mod_Type.to_nat y"
have [transfer_rule]: "Mod_Type_Connect.HMA_I ?y' y" unfolding Mod_Type_Connect.HMA_I_def by simp
have "?least_n2 ≤ Mod_Type.from_nat ?y'"
proof (unfold l2_def, rule from_nat_mono')
show "Mod_Type.to_nat y < CARD('n)" by (simp add: mod_type_class.to_nat_less_card)
have *: "A $$(mod_type_class.to_nat j', mod_type_class.to_nat y) ≠ 0" using y[unfolded index_hma_def[symmetric]] by transfer' show "(LEAST n'. A$$ (mod_type_class.to_nat j', n') ≠ 0) ≤ mod_type_class.to_nat y"
by (rule Least_le, simp add: *)
qed
also have "... = y" by simp
finally show "?least_n2 ≤ y" .
qed
ultimately show "(LEAST n. A' $h i'$h n ≠ 0) < (LEAST n. A' $h j'$h n ≠ 0)" using least_ij
unfolding l1_def l2_def
using AA' Mod_Type_Connect.dim_col_transfer_rule from_nat_mono l2_def l2_dim_col
by fastforce
qed
show ?case unfolding echelon_form_JNF_def echelon_form_def' using 1 2 by auto
qed

definition Hermite_JNF :: "'a::{bezout_ring_div,normalization_semidom} set ⇒ ('a ⇒ 'a set) ⇒ 'a mat ⇒ bool"
where "Hermite_JNF associates residues A = (
Complete_set_non_associates associates ∧ (Complete_set_residues residues) ∧ echelon_form_JNF A
∧ (∀i<dim_row A. ¬ is_zero_row_JNF i A ⟶ A $$(i, LEAST n. A$$ (i, n) ≠ 0) ∈ associates)
∧ (∀i<dim_row A. ¬ is_zero_row_JNF i A ⟶ (∀j. j<i ⟶ A $$(j, (LEAST n. A$$ (i, n) ≠ 0))
∈ residues (A $$(i,(LEAST n. A$$ (i,n) ≠ 0)))
)))"

lemma HMA_LEAST[transfer_rule]:
assumes AA': "(Mod_Type_Connect.HMA_M :: _ ⇒ 'a :: comm_ring_1 ^ 'n :: mod_type ^ 'm :: mod_type ⇒ _) A A'"
and ii': "Mod_Type_Connect.HMA_I i i'" and zero_i: "¬ is_zero_row_JNF i A"
shows "Mod_Type_Connect.HMA_I (LEAST n. A $$(i, n) ≠ 0) (LEAST n. index_hma A' i' n ≠ 0)" proof - define l where "l = (LEAST n'. A' h i' h n' ≠ 0)" let ?least_n2 = "Mod_Type.to_nat l" note AA'[transfer_rule] ii'[transfer_rule] have [transfer_rule]: "Mod_Type_Connect.HMA_I ?least_n2 l" by (simp add: Mod_Type_Connect.HMA_I_def) have zero_i': "¬ is_zero_row i' A'" using zero_i by transfer have "(LEAST n. A$$ (i, n) ≠ 0) = ?least_n2"
proof (rule Least_equality)
obtain n' where n'1: "A $$(i,n') ≠ 0" and n'2: "n'<dim_col A" using zero_i unfolding is_zero_row_JNF_def by auto let ?n' = "Mod_Type.from_nat n'::'n" have n'n'[transfer_rule]: "Mod_Type_Connect.HMA_I n' ?n'" unfolding Mod_Type_Connect.HMA_I_def using Mod_Type.to_nat_from_nat_id n'2 using AA' Mod_Type_Connect.dim_col_transfer_rule by fastforce have "index_hma A' i' ?n' ≠ 0" using n'1 by transfer hence A'i'n': "A' h i' h ?n' ≠ 0" unfolding index_hma_def by simp have least_le_n': "(LEAST n. A$$ (i, n) ≠ 0)  ≤ n'" by (simp add: Least_le n'1)
have l1_le_n': "l ≤ ?n'" by (simp add: A'i'n' Least_le l_def)
have "A $$(i, ?least_n2) = index_hma A' i' l" by (transfer, simp) also have "... = A' h i' h l" unfolding index_hma_def by simp also have "... ≠ 0" unfolding l_def by (metis (mono_tags) A'i'n' LeastI) finally show "A$$ (i, mod_type_class.to_nat l) ≠ 0" .
fix y assume Aiy: "A $$(i, y) ≠ 0" let ?y' = "Mod_Type.from_nat y::'n" show "Mod_Type.to_nat l ≤ y" proof (cases "y≤n'") case True hence y: "y < dim_col A" using n'2 by auto have yy'[transfer_rule]: "Mod_Type_Connect.HMA_I y ?y'" unfolding Mod_Type_Connect.HMA_I_def apply (rule Mod_Type.to_nat_from_nat_id[symmetric]) using y Mod_Type_Connect.dim_col_transfer_rule[OF AA'] by auto have "Mod_Type.to_nat l ≤ Mod_Type.to_nat ?y'" proof (rule to_nat_mono') have "index_hma A' i' ?y' ≠ 0" using Aiy by transfer hence "A' h i' h ?y' ≠ 0" unfolding index_hma_def by simp thus "l ≤ ?y'" unfolding l_def by (simp add: Least_le) qed then show ?thesis by (metis Mod_Type_Connect.HMA_I_def yy') next case False hence "n' < y" by auto then show ?thesis by (metis False Mod_Type_Connect.HMA_I_def dual_order.trans l1_le_n' linear n'n' to_nat_mono') qed qed thus ?thesis unfolding Mod_Type_Connect.HMA_I_def l_def index_hma_def by auto qed lemma element_least_not_zero_eq_HMA_JNF: fixes A':: "'a :: comm_ring_1 ^ 'n :: mod_type ^ 'm :: mod_type" assumes AA': "Mod_Type_Connect.HMA_M A A'" and jj': "Mod_Type_Connect.HMA_I j j'" and ii': "Mod_Type_Connect.HMA_I i i'" and zero_i': "¬ is_zero_row i' A'" shows "A$$ (j, LEAST n. A $$(i, n) ≠ 0) = A' h j' h (LEAST n. A' h i' h n ≠ 0)" proof - note AA'[transfer_rule] jj'[transfer_rule] ii'[transfer_rule] have [transfer_rule]: "Mod_Type_Connect.HMA_I (LEAST n. A$$ (i, n) ≠ 0) (LEAST n. index_hma A' i' n ≠ 0)"
by (rule HMA_LEAST[OF AA' ii'], insert zero_i', transfer, simp)
have "A' $h j'$h (LEAST n. A' $h i'$h n ≠ 0) = index_hma A' j' (LEAST n. index_hma A' i' n ≠ 0)"
unfolding index_hma_def by simp
also have "... = A $$(j, LEAST n. A$$ (i, n) ≠ 0)" by (transfer', simp)
finally show ?thesis by simp
qed

lemma HMA_Hermite[transfer_rule]:
shows "((Mod_Type_Connect.HMA_M :: _ ⇒ 'a :: {bezout_ring_div,normalization_semidom} ^ 'n :: mod_type ^ 'm :: mod_type ⇒ _) ===> (=))
(Hermite_JNF associates residues) (Hermite associates residues)"
proof (intro rel_funI, goal_cases)
case (1 A A')
note AA' = "1"(1)[transfer_rule]
have 1: "echelon_form A' = echelon_form_JNF A" by (transfer, simp)
have 2: "(∀i<dim_row A. ¬ is_zero_row_JNF i A ⟶ A $$(i, LEAST n. A$$ (i, n) ≠ 0) ∈ associates) =
(∀i. ¬ is_zero_row i A' ⟶ A' $h i$h (LEAST n. A' $h i$h n ≠ 0) ∈ associates)" (is "?lhs = ?rhs")
proof
assume lhs: "?lhs"
show "?rhs"
proof (rule allI, rule impI)
fix i' assume zero_i': "¬ is_zero_row i' A'"
let ?i = "Mod_Type.to_nat i'"
have ii'[transfer_rule]: "Mod_Type_Connect.HMA_I ?i i'" unfolding Mod_Type_Connect.HMA_I_def by simp
have [simp]: "?i < dim_row A" using Mod_Type.to_nat_less_card[of i']
using AA' Mod_Type_Connect.dim_row_transfer_rule by fastforce
have zero_i: "¬ is_zero_row_JNF ?i A" using zero_i' by transfer
have [transfer_rule]: "Mod_Type_Connect.HMA_I (LEAST n. A $$(?i, n) ≠ 0) (LEAST n. index_hma A' i' n ≠ 0)" by (rule HMA_LEAST[OF AA' ii'], insert zero_i', transfer, simp) have "A' h i' h (LEAST n. A' h i' h n ≠ 0) = A$$ (?i, LEAST n. A $$(?i, n) ≠ 0)" by (rule element_least_not_zero_eq_HMA_JNF[OF AA' ii' ii' zero_i', symmetric]) also have "... ∈ associates" using lhs zero_i by simp finally show "A' h i' h (LEAST n. A' h i' h n ≠ 0) ∈ associates" . qed next assume rhs: "?rhs" show "?lhs" proof (rule allI, rule impI, rule impI) fix i assume zero_i: "¬ is_zero_row_JNF i A" and i: "i < dim_row A" let ?i' = "Mod_Type.from_nat i :: 'm" have ii'[transfer_rule]: "Mod_Type_Connect.HMA_I i ?i'" unfolding Mod_Type_Connect.HMA_I_def using Mod_Type.to_nat_from_nat_id AA' Mod_Type_Connect.dim_row_transfer_rule i by fastforce have zero_i': "¬ is_zero_row ?i' A'" using zero_i by transfer have "A$$ (i, LEAST n. A $$(i, n) ≠ 0) = A' h ?i' h (LEAST n. A' h ?i' h n ≠ 0)" by (rule element_least_not_zero_eq_HMA_JNF[OF AA' ii' ii' zero_i']) also have "... ∈ associates" using rhs zero_i' i by simp finally show "A$$ (i, LEAST n. A $$(i, n) ≠ 0) ∈ associates" . qed qed have 3: "(∀i<dim_row A. ¬ is_zero_row_JNF i A ⟶ (∀j<i. A$$ (j, LEAST n. A $$(i, n) ≠ 0) ∈ residues (A$$ (i, LEAST n. A $$(i, n) ≠ 0)))) = (∀i. ¬ is_zero_row i A' ⟶ (∀j<i. A' h j h (LEAST n. A' h i h n ≠ 0) ∈ residues (A' h i h (LEAST n. A' h i h n ≠ 0))))" (is "?lhs = ?rhs") proof assume lhs: "?lhs" show "?rhs" proof (rule allI, rule impI, rule allI, rule impI) fix i' j' :: 'm assume zero_i': "¬ is_zero_row i' A'" and j'i': "j' < i'" let ?i = "Mod_Type.to_nat i'" have ii'[transfer_rule]: "Mod_Type_Connect.HMA_I ?i i'" unfolding Mod_Type_Connect.HMA_I_def by simp have i: "?i < dim_row A" using AA' Mod_Type_Connect.dim_row_transfer_rule mod_type_class.to_nat_less_card by fastforce have zero_i: "¬ is_zero_row_JNF ?i A" using zero_i' by transfer' let ?j = "Mod_Type.to_nat j'" have jj'[transfer_rule]: "Mod_Type_Connect.HMA_I ?j j'" unfolding Mod_Type_Connect.HMA_I_def by simp have ji: "?j<?i" using j'i' to_nat_mono by blast have eq1: "A$$ (?j, LEAST n. A $$(?i, n) ≠ 0) = A' h j' h (LEAST n. A' h i' h n ≠ 0)" by (rule element_least_not_zero_eq_HMA_JNF[OF AA' jj' ii' zero_i']) have eq2: "A$$ (?i, LEAST n. A $$(?i, n) ≠ 0) = A' h i' h (LEAST n. A' h i' h n ≠ 0)" by (rule element_least_not_zero_eq_HMA_JNF[OF AA' ii' ii' zero_i']) show "A' h j' h (LEAST n. A' h i' h n ≠ 0) ∈ residues (A' h i' h (LEAST n. A' h i' h n ≠ 0))" using lhs eq1 eq2 ji i zero_i by fastforce qed next assume rhs: "?rhs" show "?lhs" proof (safe) fix i j assume i: "i < dim_row A" and zero_i: "¬ is_zero_row_JNF i A" and ji: "j < i" let ?i' = "Mod_Type.from_nat i :: 'm" have ii'[transfer_rule]: "Mod_Type_Connect.HMA_I i ?i'" unfolding Mod_Type_Connect.HMA_I_def using Mod_Type.to_nat_from_nat_id AA' Mod_Type_Connect.dim_row_transfer_rule i by fastforce have zero_i': "¬ is_zero_row ?i' A'" using zero_i by transfer let ?j' = "Mod_Type.from_nat j :: 'm" have j'i': "?j' < ?i'" using AA' Mod_Type_Connect.dim_row_transfer_rule from_nat_mono i ji by fastforce have jj'[transfer_rule]: "Mod_Type_Connect.HMA_I j ?j'" unfolding Mod_Type_Connect.HMA_I_def using Mod_Type.to_nat_from_nat_id[of j, where ?'a='m] AA' Mod_Type_Connect.dim_row_transfer_rule[OF AA'] j'i' i ji by auto have zero_i': "¬ is_zero_row ?i' A'" using zero_i by transfer have eq1: "A$$ (j, LEAST n. A $$(i, n) ≠ 0) = A' h ?j' h (LEAST n. A' h ?i' h n ≠ 0)" by (rule element_least_not_zero_eq_HMA_JNF[OF AA' jj' ii' zero_i']) have eq2: "A$$ (i, LEAST n. A $$(i, n) ≠ 0) = A' h ?i' h (LEAST n. A' h ?i' h n ≠ 0)" by (rule element_least_not_zero_eq_HMA_JNF[OF AA' ii' ii' zero_i']) show "A$$ (j, LEAST n. A $$(i, n) ≠ 0) ∈ residues (A$$ (i, LEAST n. A $$(i, n) ≠ 0))" using rhs eq1 eq2 j'i' i zero_i' by fastforce qed qed show "Hermite_JNF associates residues A = Hermite associates residues A'" unfolding Hermite_def Hermite_JNF_def using 1 2 3 by auto qed corollary HMA_Hermite2[transfer_rule]: shows "((=) ===> (=) ===> (Mod_Type_Connect.HMA_M :: _ ⇒ 'a :: {bezout_ring_div,normalization_semidom} ^ 'n :: mod_type ^ 'm :: mod_type ⇒ _) ===> (=)) (Hermite_JNF) (Hermite)" by (simp add: HMA_Hermite rel_funI) text ‹Once the definitions of both libraries are connected, we start to move the theorem about the uniqueness of the Hermite normal form (stated in HOL Analysis, named @{text "Hermite_unique"}) to JNF.› text ‹Using the previous transfer rules, we get an statement in JNF. However, the matrices have @{text "CARD('n::mod_type)"} rows and columns. We want to get rid of that type variable and just state that they are of dimension n \times n (expressed via the predicate @{text "carrier_mat"}› lemma Hermite_unique_JNF': fixes A::"'a::{bezout_ring_div,normalization_euclidean_semiring,unique_euclidean_ring} mat" assumes "A ∈ carrier_mat CARD('n::mod_type) CARD('n::mod_type)" "P ∈ carrier_mat CARD('n::mod_type) CARD('n::mod_type)" "H ∈ carrier_mat CARD('n::mod_type) CARD('n::mod_type)" "Q ∈ carrier_mat CARD('n::mod_type) CARD('n::mod_type)" "K ∈ carrier_mat CARD('n::mod_type) CARD('n::mod_type)" assumes "A = P * H" and "A = Q * K" and "invertible_mat A" and "invertible_mat P" and "invertible_mat Q" and "Hermite_JNF associates res H" and "Hermite_JNF associates res K" shows "H = K" proof - define A' where "A' = (Mod_Type_Connect.to_hma⇩m A :: 'a ^'n :: mod_type ^'n :: mod_type)" define P' where "P' = (Mod_Type_Connect.to_hma⇩m P :: 'a ^'n :: mod_type ^'n :: mod_type)" define H' where "H' = (Mod_Type_Connect.to_hma⇩m H :: 'a ^'n :: mod_type ^'n :: mod_type)" define Q' where "Q' = (Mod_Type_Connect.to_hma⇩m Q :: 'a ^'n :: mod_type ^'n :: mod_type)" define K' where "K' = (Mod_Type_Connect.to_hma⇩m K :: 'a ^'n :: mod_type ^'n :: mod_type)" have AA'[transfer_rule]: "Mod_Type_Connect.HMA_M A A'" unfolding Mod_Type_Connect.HMA_M_def using assms A'_def by auto have PP'[transfer_rule]: "Mod_Type_Connect.HMA_M P P'" unfolding Mod_Type_Connect.HMA_M_def using assms P'_def by auto have HH'[transfer_rule]: "Mod_Type_Connect.HMA_M H H'" unfolding Mod_Type_Connect.HMA_M_def using assms H'_def by auto have QQ'[transfer_rule]: "Mod_Type_Connect.HMA_M Q Q'" unfolding Mod_Type_Connect.HMA_M_def using assms Q'_def by auto have KK'[transfer_rule]: "Mod_Type_Connect.HMA_M K K'" unfolding Mod_Type_Connect.HMA_M_def using assms K'_def by auto have A_PH: "A' = P' ** H'" using assms by transfer moreover have A_QK: "A' = Q' ** K'" using assms by transfer moreover have inv_A: "invertible A'" using assms by transfer moreover have inv_P: "invertible P'" using assms by transfer moreover have inv_Q: "invertible Q'" using assms by transfer moreover have H: "Hermite associates res H'" using assms by transfer moreover have K: "Hermite associates res K'" using assms by transfer ultimately have "H' = K'" using Hermite_unique by blast thus "H=K" by transfer qed text ‹Since the @{text "mod_type"} restriction relies on many things, the shortcut is to use the @{text "mod_ring"} typedef developed in the Berlekamp-Zassenhaus development. This type definition allows us to apply local type definitions easily. Since @{text "mod_ring"} is just an instance of @{text "mod_type"}, it is straightforward to obtain the following lemma, where @{text "CARD('n::mod_type)"} has now been substituted by @{text "CARD('n::nontriv mod_ring)"}› corollary Hermite_unique_JNF_with_nontriv_mod_ring: fixes A::"'a::{bezout_ring_div,normalization_euclidean_semiring,unique_euclidean_ring} mat" assumes "A ∈ carrier_mat CARD('n) CARD('n::nontriv mod_ring)" "P ∈ carrier_mat CARD('n) CARD('n)" "H ∈ carrier_mat CARD('n) CARD('n)" "Q ∈ carrier_mat CARD('n) CARD('n)" "K ∈ carrier_mat CARD('n) CARD('n)" assumes "A = P * H" and "A = Q * K" and "invertible_mat A" and "invertible_mat P" and "invertible_mat Q" and "Hermite_JNF associates res H" and "Hermite_JNF associates res K" shows "H = K" using Hermite_unique_JNF' assms by (smt CARD_mod_ring) text ‹Now, we assume in a context that there exists a type text @{text "'b"} of cardinality n and we prove inside this context the lemma.› context fixes n::nat assumes local_typedef: "∃(Rep :: ('b ⇒ int)) Abs. type_definition Rep Abs {0..<n :: int}" and p: "n>1" begin private lemma type_to_set: shows "class.nontriv TYPE('b)" (is ?a) and "n=CARD('b)" (is ?b) proof - from local_typedef obtain Rep::"('b ⇒ int)" and Abs where t: "type_definition Rep Abs {0..<n :: int}" by auto have "card (UNIV :: 'b set) = card {0..<n}" using t type_definition.card by fastforce also have "... = n" by auto finally show ?b .. then show ?a unfolding class.nontriv_def using p by auto qed lemma Hermite_unique_JNF_aux: fixes A::"'a::{bezout_ring_div,normalization_euclidean_semiring,unique_euclidean_ring} mat" assumes "A ∈ carrier_mat n n" "P ∈ carrier_mat n n" "H ∈ carrier_mat n n" "Q ∈ carrier_mat n n " "K ∈ carrier_mat n n" assumes "A = P * H" and "A = Q * K" and "invertible_mat A" and "invertible_mat P" and "invertible_mat Q" and "Hermite_JNF associates res H" and "Hermite_JNF associates res K" shows "H = K" using Hermite_unique_JNF_with_nontriv_mod_ring[unfolded CARD_mod_ring, internalize_sort "'n::nontriv", where ?'a='b] unfolding type_to_set(2)[symmetric] using type_to_set(1) assms by blast end text ‹Now, we cancel the local type definition of the previous context. Since the @{text "mod_type"} restriction imposes the type to have cardinality greater than 1, the cases n=0 and n=1 must be proved separately (they are trivial)› lemma Hermite_unique_JNF: fixes A::"'a::{bezout_ring_div,normalization_euclidean_semiring,unique_euclidean_ring} mat" assumes A: "A ∈ carrier_mat n n" and P: "P ∈ carrier_mat n n" and H: "H ∈ carrier_mat n n" and Q: "Q ∈ carrier_mat n n" and K: "K ∈ carrier_mat n n" assumes A_PH: "A = P * H" and A_QK: "A = Q * K" and inv_A: "invertible_mat A" and inv_P: "invertible_mat P" and inv_Q: "invertible_mat Q" and HNF_H: "Hermite_JNF associates res H" and HNF_K: "Hermite_JNF associates res K" shows "H = K" proof (cases "n=0 ∨ n=1") case True note zero_or_one = True show ?thesis proof (cases "n=0") case True then show ?thesis using assms by auto next case False have CS_A: "Complete_set_non_associates associates" using HNF_H unfolding Hermite_JNF_def by simp have H: "H ∈ carrier_mat 1 1" and K: "K∈ carrier_mat 1 1" using False zero_or_one assms by auto have det_P_dvd_1: "Determinant.det P dvd 1" using invertible_iff_is_unit_JNF inv_P P by blast have det_Q_dvd_1: "Determinant.det Q dvd 1" using invertible_iff_is_unit_JNF inv_Q Q by blast have PH_QK: "Determinant.det P * Determinant.det H = Determinant.det Q * Determinant.det K" using Determinant.det_mult assms by metis hence "Determinant.det P * H$$ (0,0) = Determinant.det Q * K $$(0,0)" by (metis H K determinant_one_element) obtain u where uH_K: "u * H$$(0,0) = K $$(0,0)" and unit_u: "is_unit u" by (metis (no_types, opaque_lifting) H K PH_QK algebraic_semidom_class.dvd_mult_unit_iff det_P_dvd_1 det_Q_dvd_1 det_singleton dvdE dvd_mult_cancel_left mult.commute mult.right_neutral one_dvd) have H00_not_0: "H$$ (0,0) ≠ 0"
by (metis A A_PH Determinant.det_mult False H P determinant_one_element inv_A
invertible_iff_is_unit_JNF mult_not_zero not_is_unit_0 zero_or_one)
hence LEAST_H: "(LEAST n. H $$(0,n) ≠ 0) = 0" by simp have H00: "H$$ (0,0) ∈ associates" using HNF_H LEAST_H H H00_not_0
unfolding Hermite_JNF_def is_zero_row_JNF_def by auto
have K00_not_0: "K $$(0,0) ≠ 0" by (metis A A_QK Determinant.det_mult False K Q determinant_one_element inv_A invertible_iff_is_unit_JNF mult_not_zero not_is_unit_0 zero_or_one) hence LEAST_K: "(LEAST n. K$$ (0,n) ≠ 0) = 0" by simp
have K00: "K $$(0,0) ∈ associates" using HNF_K LEAST_K K K00_not_0 unfolding Hermite_JNF_def is_zero_row_JNF_def by auto have ass_H00_K00: "normalize (H$$ (0,0)) = normalize (K $$(0,0))" by (metis normalize_mult_unit_left uH_K unit_u) have H00_eq_K00: "H$$ (0,0) = K $$(0,0)" using in_Ass_not_associated[OF CS_A H00 K00] ass_H00_K00 by auto show ?thesis by (rule eq_matI, insert H K H00_eq_K00, auto) qed next case False hence "{0..<int n} ≠ {}" by auto moreover have "n>1" using False by simp ultimately show ?thesis using Hermite_unique_JNF_aux[cancel_type_definition] assms by metis (*Cancel local type definition*) qed end text ‹From here on, we apply the same approach to move the new generalized statement about the uniqueness Hermite normal form, i.e., the version restricted to integer matrices, but imposing invertibility over the rationals.› (*TODO: move to Mod_Type_Connect in SNF development. There are two definitions of map_matrix, one in HMA_Connect and one in Finite_Cartesian_Product, but they are the same.*) lemma HMA_map_matrix [transfer_rule]: "((=) ===> Mod_Type_Connect.HMA_M ===> Mod_Type_Connect.HMA_M) map_mat map_matrix" unfolding map_vector_def map_matrix_def[abs_def] map_mat_def[abs_def] Mod_Type_Connect.HMA_M_def Mod_Type_Connect.from_hma⇩m_def by auto lemma Hermite_unique_generalized_JNF': fixes A::"int mat" assumes "A ∈ carrier_mat CARD('n::mod_type) CARD('n::mod_type)" "P ∈ carrier_mat CARD('n::mod_type) CARD('n::mod_type)" "H ∈ carrier_mat CARD('n::mod_type) CARD('n::mod_type)" "Q ∈ carrier_mat CARD('n::mod_type) CARD('n::mod_type)" "K ∈ carrier_mat CARD('n::mod_type) CARD('n::mod_type)" assumes "A = P * H" and "A = Q * K" and "invertible_mat (map_mat rat_of_int A)" and "invertible_mat P" and "invertible_mat Q" and "Hermite_JNF associates res H" and "Hermite_JNF associates res K" shows "H = K" proof - define A' where "A' = (Mod_Type_Connect.to_hma⇩m A :: int ^'n :: mod_type ^'n :: mod_type)" define P' where "P' = (Mod_Type_Connect.to_hma⇩m P :: int ^'n :: mod_type ^'n :: mod_type)" define H' where "H' = (Mod_Type_Connect.to_hma⇩m H :: int ^'n :: mod_type ^'n :: mod_type)" define Q' where "Q' = (Mod_Type_Connect.to_hma⇩m Q :: int ^'n :: mod_type ^'n :: mod_type)" define K' where "K' = (Mod_Type_Connect.to_hma⇩m K :: int ^'n :: mod_type ^'n :: mod_type)" have AA'[transfer_rule]: "Mod_Type_Connect.HMA_M A A'" unfolding Mod_Type_Connect.HMA_M_def using assms A'_def by auto have PP'[transfer_rule]: "Mod_Type_Connect.HMA_M P P'" unfolding Mod_Type_Connect.HMA_M_def using assms P'_def by auto have HH'[transfer_rule]: "Mod_Type_Connect.HMA_M H H'" unfolding Mod_Type_Connect.HMA_M_def using assms H'_def by auto have QQ'[transfer_rule]: "Mod_Type_Connect.HMA_M Q Q'" unfolding Mod_Type_Connect.HMA_M_def using assms Q'_def by auto have KK'[transfer_rule]: "Mod_Type_Connect.HMA_M K K'" unfolding Mod_Type_Connect.HMA_M_def using assms K'_def by auto have A_PH: "A' = P' ** H'" using assms by transfer moreover have A_QK: "A' = Q' ** K'" using assms by transfer moreover have inv_A: "invertible (map_matrix rat_of_int A')" using assms by transfer moreover have "invertible (Finite_Cartesian_Product.map_matrix rat_of_int A')" using inv_A unfolding Finite_Cartesian_Product.map_matrix_def map_matrix_def map_vector_def by simp moreover have inv_P: "invertible P'" using assms by transfer moreover have inv_Q: "invertible Q'" using assms by transfer moreover have H: "Hermite associates res H'" using assms by transfer moreover have K: "Hermite associates res K'" using assms by transfer ultimately have "H' = K'" using Hermite_unique_generalized by blast thus "H=K" by transfer qed corollary Hermite_unique_generalized_JNF_with_nontriv_mod_ring: fixes A::"int mat" assumes "A ∈ carrier_mat CARD('n) CARD('n::nontriv mod_ring)" "P ∈ carrier_mat CARD('n) CARD('n)" "H ∈ carrier_mat CARD('n) CARD('n)" "Q ∈ carrier_mat CARD('n) CARD('n)" "K ∈ carrier_mat CARD('n) CARD('n)" assumes "A = P * H" and "A = Q * K" and "invertible_mat (map_mat rat_of_int A)" and "invertible_mat P" and "invertible_mat Q" and "Hermite_JNF associates res H" and "Hermite_JNF associates res K" shows "H = K" using Hermite_unique_generalized_JNF' assms by (smt CARD_mod_ring) context fixes p::nat assumes local_typedef: "∃(Rep :: ('b ⇒ int)) Abs. type_definition Rep Abs {0..<p :: int}" and p: "p>1" begin private lemma type_to_set2: shows "class.nontriv TYPE('b)" (is ?a) and "p=CARD('b)" (is ?b) proof - from local_typedef obtain Rep::"('b ⇒ int)" and Abs where t: "type_definition Rep Abs {0..<p :: int}" by auto have "card (UNIV :: 'b set) = card {0..<p}" using t type_definition.card by fastforce also have "... = p" by auto finally show ?b .. then show ?a unfolding class.nontriv_def using p by auto qed lemma Hermite_unique_generalized_JNF_aux: fixes A::"int mat" assumes "A ∈ carrier_mat p p" "P ∈ carrier_mat p p" "H ∈ carrier_mat p p" "Q ∈ carrier_mat p p" "K ∈ carrier_mat p p" assumes "A = P * H" and "A = Q * K" and "invertible_mat (map_mat rat_of_int A)" and "invertible_mat P" and "invertible_mat Q" and "Hermite_JNF associates res H" and "Hermite_JNF associates res K" shows "H = K" using Hermite_unique_generalized_JNF_with_nontriv_mod_ring[unfolded CARD_mod_ring, internalize_sort "'n::nontriv", where ?'a='b] unfolding type_to_set2(2)[symmetric] using type_to_set2(1) assms by blast end lemma HNF_unique_generalized_JNF: fixes A::"int mat" assumes A: "A ∈ carrier_mat n n" and P: "P ∈ carrier_mat n n" and H: "H ∈ carrier_mat n n" and Q: "Q ∈ carrier_mat n n" and K: "K ∈ carrier_mat n n" assumes A_PH: "A = P * H" and A_QK: "A = Q * K" and inv_A: "invertible_mat (map_mat rat_of_int A)" and inv_P: "invertible_mat P" and inv_Q: "invertible_mat Q" and HNF_H: "Hermite_JNF associates res H" and HNF_K: "Hermite_JNF associates res K" shows "H = K" proof (cases "n=0 ∨ n=1") case True note zero_or_one = True show ?thesis proof (cases "n=0") case True then show ?thesis using assms by auto next let ?RAT = "map_mat rat_of_int" case False hence n: "n=1" using zero_or_one by auto have CS_A: "Complete_set_non_associates associates" using HNF_H unfolding Hermite_JNF_def by simp have H: "H ∈ carrier_mat 1 1" and K: "K∈ carrier_mat 1 1" using False zero_or_one assms by auto have det_P_dvd_1: "Determinant.det P dvd 1" using invertible_iff_is_unit_JNF inv_P P by blast have det_Q_dvd_1: "Determinant.det Q dvd 1" using invertible_iff_is_unit_JNF inv_Q Q by blast have PH_QK: "Determinant.det P * Determinant.det H = Determinant.det Q * Determinant.det K" using Determinant.det_mult assms by metis hence "Determinant.det P * H$$ (0,0) = Determinant.det Q * K $$(0,0)" by (metis H K determinant_one_element) obtain u where uH_K: "u * H$$(0,0) = K $$(0,0)" and unit_u: "is_unit u" by (metis (no_types, opaque_lifting) H K PH_QK algebraic_semidom_class.dvd_mult_unit_iff det_P_dvd_1 det_Q_dvd_1 det_singleton dvdE dvd_mult_cancel_left mult.commute mult.right_neutral one_dvd) have H00_not_0: "H$$ (0,0) ≠ 0"
proof -
have "?RAT A = ?RAT P * ?RAT H" using A_PH
using P H n of_int_hom.mat_hom_mult by blast
hence "det (?RAT H) ≠ 0"
by (metis A Determinant.det_mult False H P inv_A invertible_iff_is_unit_JNF
map_carrier_mat mult_eq_0_iff not_is_unit_0 zero_or_one)
thus ?thesis
using H determinant_one_element by force
qed
hence LEAST_H: "(LEAST n. H $$(0,n) ≠ 0) = 0" by simp have H00: "H$$ (0,0) ∈ associates" using HNF_H LEAST_H H H00_not_0
unfolding Hermite_JNF_def is_zero_row_JNF_def by auto
have K00_not_0: "K $$(0,0) ≠ 0" proof - have "?RAT A = ?RAT Q * ?RAT K" using A_QK using Q K n of_int_hom.mat_hom_mult by blast hence "det (?RAT K) ≠ 0" by (metis A Determinant.det_mult False Q K inv_A invertible_iff_is_unit_JNF map_carrier_mat mult_eq_0_iff not_is_unit_0 zero_or_one) thus ?thesis using K determinant_one_element by force qed hence LEAST_K: "(LEAST n. K$$ (0,n) ≠ 0) = 0" by simp
have K00: "K $$(0,0) ∈ associates" using HNF_K LEAST_K K K00_not_0 unfolding Hermite_JNF_def is_zero_row_JNF_def by auto have ass_H00_K00: "normalize (H$$ (0,0)) = normalize (K $$(0,0))" by (metis normalize_mult_unit_left uH_K unit_u) have H00_eq_K00: "H$$ (0,0) = K  (0,0)"
using in_Ass_not_associated[OF CS_A H00 K00] ass_H00_K00 by auto
show ?thesis by (rule eq_matI, insert H K H00_eq_K00, auto)
qed
next
case False
hence "{0..<int n} ≠ {}" by auto
moreover have "n>1" using False by simp
ultimately show ?thesis
using Hermite_unique_generalized_JNF_aux[cancel_type_definition] assms by metis (*Cancel local type definition*)
qed

end