Theory Diagonalize

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

section ‹Diagonalizing matrices in JNF and HOL Analysis›

theory Diagonalize
  imports Admits_SNF_From_Diagonal_Iff_Bezout_Ring
begin


text ‹This section presents a @{text "locale"} that assumes a sound operation to make a matrix
diagonal. Then, the result is transferred to HOL Analysis.›

subsection ‹Diagonalizing matrices in JNF›

text ‹We assume a @{text "diagonalize_JNF"} operation in JNF, which is applied to matrices over
a B\'ezout ring. However, probably a more restrictive type class is required.›

locale diagonalize =
  fixes diagonalize_JNF :: "'a::bezout_ring mat ⇒ 'a bezout ⇒ ('a mat × 'a mat × 'a mat)"
  assumes soundness_diagonalize_JNF: 
    "∀A bezout. A ∈ carrier_mat m n ∧ is_bezout_ext bezout ⟶
     (case diagonalize_JNF A bezout of (P,S,Q) ⇒    
      P ∈ carrier_mat m m ∧ Q ∈ carrier_mat n n ∧ S ∈ carrier_mat m n 
      ∧ invertible_mat P ∧ invertible_mat Q ∧ isDiagonal_mat S ∧ S = P*A*Q)"
begin

lemma soundness_diagonalize_JNF':
  fixes A::"'a mat"
  assumes "is_bezout_ext bezout" and "A ∈ carrier_mat m n"
  and "diagonalize_JNF A bezout = (P,S,Q)"
  shows "P ∈ carrier_mat m m ∧ Q ∈ carrier_mat n n ∧ S ∈ carrier_mat m n 
      ∧ invertible_mat P ∧ invertible_mat Q ∧ isDiagonal_mat S ∧ S = P*A*Q"
  using soundness_diagonalize_JNF assms unfolding case_prod_beta by (metis fst_conv snd_conv)


subsection ‹Implementation and soundness result moved to HOL Analysis.›

definition diagonalize :: "'a::bezout_ring ^ 'nc :: mod_type ^ 'nr :: mod_type
     ⇒ 'a bezout ⇒ 
    (('a ^ 'nr :: mod_type ^ 'nr :: mod_type) 
    × ('a ^ 'nc :: mod_type ^ 'nr :: mod_type) 
    × ('a ^ 'nc :: mod_type ^ 'nc :: mod_type))"
  where "diagonalize A bezout = (
    let (P,S,Q) = diagonalize_JNF (Mod_Type_Connect.from_hmam A) bezout
    in (Mod_Type_Connect.to_hmam P,Mod_Type_Connect.to_hmam S,Mod_Type_Connect.to_hmam Q)
  )"

lemma soundness_diagonalize:
  assumes b: "is_bezout_ext bezout"
  and d: "diagonalize A bezout = (P,S,Q)"
shows "invertible P ∧ invertible Q ∧ isDiagonal S ∧ S = P**A**Q"
proof -
  define A' where "A' = Mod_Type_Connect.from_hmam A"  
  obtain P' S' Q' where d_JNF: "(P',S',Q') = diagonalize_JNF A' bezout"
    by (metis prod_cases3)
  define m and n where "m = dim_row A'" and "n = dim_col A'"
  hence A': "A' ∈ carrier_mat m n" by auto
  have res_JNF: "P' ∈ carrier_mat m m ∧ Q' ∈ carrier_mat n n ∧ S' ∈ carrier_mat m n 
      ∧ invertible_mat P' ∧ invertible_mat Q' ∧ isDiagonal_mat S' ∧ S' = P'*A'*Q'"
    by (rule soundness_diagonalize_JNF'[OF b A' d_JNF[symmetric]])
  have "Mod_Type_Connect.to_hmam P' = P" using d unfolding diagonalize_def Let_def
    by (metis A'_def d_JNF fst_conv old.prod.case)
  hence "P' = Mod_Type_Connect.from_hmam P" using A'_def m_def res_JNF by auto
  hence [transfer_rule]: "Mod_Type_Connect.HMA_M P' P" 
    unfolding Mod_Type_Connect.HMA_M_def by auto
  have "Mod_Type_Connect.to_hmam Q' = Q" using d unfolding diagonalize_def Let_def
    by (metis A'_def d_JNF snd_conv old.prod.case)
  hence "Q' = Mod_Type_Connect.from_hmam Q" using A'_def n_def res_JNF by auto
  hence [transfer_rule]: "Mod_Type_Connect.HMA_M Q' Q"
    unfolding Mod_Type_Connect.HMA_M_def by auto
  have "Mod_Type_Connect.to_hmam S' = S" using d unfolding diagonalize_def Let_def
    by (metis A'_def d_JNF snd_conv old.prod.case)
  hence "S' = Mod_Type_Connect.from_hmam S" using A'_def m_def n_def res_JNF by auto
  hence [transfer_rule]: "Mod_Type_Connect.HMA_M S' S"
    unfolding Mod_Type_Connect.HMA_M_def by auto
  have [transfer_rule]: "Mod_Type_Connect.HMA_M A' A"
    using A'_def unfolding Mod_Type_Connect.HMA_M_def by auto
  have "invertible P" using res_JNF by (transfer, simp)
  moreover have "invertible Q" using res_JNF by (transfer, simp)
  moreover have "isDiagonal S" using res_JNF by (transfer, simp)
  moreover have "S = P**A**Q" using res_JNF by (transfer, simp)
  ultimately show ?thesis by simp
qed
end

end