Session Smith_Normal_Form

Theory Smith_Normal_Form

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

section ‹Definition of Smith normal form in HOL Analysis›

theory Smith_Normal_Form
  imports   
    Hermite.Hermite   
begin


subsection ‹Definitions›

text‹Definition of diagonal matrix›

definition "isDiagonal_upt_k A k = ( a b. (to_nat a  to_nat b  (to_nat a < k  (to_nat b < k)))  A $ a $ b = 0)"
definition "isDiagonal A = ( a b. to_nat a  to_nat b  A $ a $ b = 0)"

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

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

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

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

subsection ‹Basic properties›

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


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

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

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

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


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


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

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


end

Theory Diagonal_To_Smith

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

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

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


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

subsection ‹Implementation of the algorithm›

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

hide_const Countable.from_nat
hide_const Countable.to_nat

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

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


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

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

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

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

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

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

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

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


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

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

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

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

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

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

subsection‹Code equations to get an executable version›

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

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

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

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

subsection‹Examples of execution›

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

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

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


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


subsection‹Soundness of the algorithm›

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

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


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

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

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

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

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

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

end

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

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

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

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


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

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


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

context GCD_ring
begin

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

end


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

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


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


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



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


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

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

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


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


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


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

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


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


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

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

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

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

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

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

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

lemma to_nat_less_ncols[simp]:
  fixes A::"'a^'b::mod_type^'c::mod_type"
    and a::'b
  shows "to_nat a < ncols A"
  by (simp add: ncols_def to_nat_less_card)

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

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


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


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

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

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

end

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

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

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

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

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

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


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


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

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

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

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

end

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

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

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

text‹This is the soundess lemma.›

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

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


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

text‹Examples›

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

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


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


lemmas diagonal_step_PQ_def = diagonal_step_PQ.simps

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


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



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



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

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

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

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

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


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

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

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


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

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

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



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



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


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

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


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

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

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


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


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

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

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

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

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


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


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

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

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

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

end

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


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

end

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

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

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


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

subsection‹The final soundness theorem›

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

end

Theory Mod_Type_Connect

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

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

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

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

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


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

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

context includes vec.lifting 
begin
end

definition from_hmav :: "'a ^ 'n :: mod_type  'a Matrix.vec" where
  "from_hmav v = Matrix.vec CARD('n) (λ i. v $h from_nat i)"

definition from_hmam :: "'a ^ 'nc :: mod_type ^ 'nr :: mod_type  'a Matrix.mat" where
  "from_hmam a = Matrix.mat CARD('nr) CARD('nc) (λ (i,j). a $h from_nat i $h from_nat j)"

definition to_hmav :: "'a Matrix.vec  'a ^ 'n :: mod_type" where
  "to_hmav v = (χ i. v $v to_nat i)"

definition to_hmam :: "'a Matrix.mat  'a ^ 'nc :: mod_type ^ 'nr :: mod_type " where
  "to_hmam a = (χ i j. a $$ (to_nat i, to_nat j))"

lemma to_hma_from_hmav[simp]: "to_hmav (from_hmav v) = v"
  by (auto simp: to_hmav_def from_hmav_def to_nat_less_card)

lemma to_hma_from_hmam[simp]: "to_hmam (from_hmam v) = v"
  by (auto simp: to_hmam_def from_hmam_def to_nat_less_card)

lemma from_hma_to_hmav[simp]:
  "v  carrier_vec (CARD('n))  from_hmav (to_hmav v :: 'a ^ 'n :: mod_type) = v"
  by (auto simp: to_hmav_def from_hmav_def to_nat_from_nat_id)

lemma from_hma_to_hmam[simp]:
  "A  carrier_mat (CARD('nr)) (CARD('nc))  from_hmam (to_hmam A :: 'a ^ 'nc :: mod_type  ^ 'nr :: mod_type) = A"
  by (auto simp: to_hmam_def from_hmam_def to_nat_from_nat_id)

lemma from_hmav_inj[simp]: "from_hmav x = from_hmav y  x = y"
  by (intro iffI, insert to_hma_from_hmav[of x], auto)

lemma from_hmam_inj[simp]: "from_hmam x = from_hmam y  x = y"
  by(intro iffI, insert to_hma_from_hmam[of x], auto)

definition HMA_V :: "'a Matrix.vec  'a ^ 'n :: mod_type  bool" where 
  "HMA_V = (λ v w. v = from_hmav w)"

definition HMA_M :: "'a Matrix.mat  'a ^ 'nc :: mod_type ^ 'nr :: mod_type   bool" where 
  "HMA_M = (λ a b. a = from_hmam b)"

definition HMA_I :: "nat  'n :: mod_type  bool" where
  "HMA_I = (λ i a. i = to_nat a)"



context includes lifting_syntax
begin

lemma Domainp_HMA_V [transfer_domain_rule]: 
  "Domainp (HMA_V :: 'a Matrix.vec  'a ^ 'n :: mod_type  bool) = (λ v. v  carrier_vec (CARD('n )))"
  by(intro ext iffI, insert from_hma_to_hmav[symmetric], auto simp: from_hmav_def HMA_V_def)

lemma Domainp_HMA_M [transfer_domain_rule]: 
  "Domainp (HMA_M :: 'a Matrix.mat  'a ^ 'nc :: mod_type  ^ 'nr :: mod_type  bool) 
  = (λ A. A  carrier_mat CARD('nr) CARD('nc))"
  by (intro ext iffI, insert from_hma_to_hmam[symmetric], auto simp: from_hmam_def HMA_M_def)

lemma Domainp_HMA_I [transfer_domain_rule]: 
  "Domainp (HMA_I :: nat  'n :: mod_type  bool) = (λ i. i < CARD('n))" (is "?l = ?r")
proof (intro ext)
  fix i :: nat
  show "?l i = ?r i"
    unfolding HMA_I_def Domainp_iff
    by (auto intro: exI[of _ "from_nat i"] simp: to_nat_from_nat_id to_nat_less_card)
qed

lemma bi_unique_HMA_V [transfer_rule]: "bi_unique HMA_V" "left_unique HMA_V" "right_unique HMA_V"
  unfolding HMA_V_def bi_unique_def left_unique_def right_unique_def by auto

lemma bi_unique_HMA_M [transfer_rule]: "bi_unique HMA_M" "left_unique HMA_M" "right_unique HMA_M"
  unfolding HMA_M_def bi_unique_def left_unique_def right_unique_def by auto

lemma bi_unique_HMA_I [transfer_rule]: "bi_unique HMA_I" "left_unique HMA_I" "right_unique HMA_I"
  unfolding HMA_I_def bi_unique_def left_unique_def right_unique_def by auto

lemma right_total_HMA_V [transfer_rule]: "right_total HMA_V"
  unfolding HMA_V_def right_total_def by simp

lemma right_total_HMA_M [transfer_rule]: "right_total HMA_M"
  unfolding HMA_M_def right_total_def by simp

lemma right_total_HMA_I [transfer_rule]: "right_total HMA_I"
  unfolding HMA_I_def right_total_def by simp

lemma HMA_V_index [transfer_rule]: "(HMA_V ===> HMA_I ===> (=)) ($v) ($h)"
  unfolding rel_fun_def HMA_V_def HMA_I_def from_hmav_def
  by (auto simp: to_nat_less_card)


lemma HMA_M_index [transfer_rule]:
  "(HMA_M ===> HMA_I ===> HMA_I ===> (=)) (λ A i j. A $$ (i,j)) index_hma"
  by (intro rel_funI, simp add: index_hma_def to_nat_less_card HMA_M_def HMA_I_def from_hmam_def)  


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

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

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

lemma from_hmav_add: "from_hmav v + from_hmav w = from_hmav (v + w)"
  unfolding from_hmav_def by auto

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

lemma from_hmav_diff: "from_hmav v - from_hmav w = from_hmav (v - w)"
  unfolding from_hmav_def by auto

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

lemma from_hmam_add: "from_hmam a + from_hmam b = from_hmam (a + b)"
  unfolding from_hmam_def by auto

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

lemma from_hmam_diff: "from_hmam a - from_hmam b = from_hmam (a - b)"
  unfolding from_hmam_def by auto

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

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

lemma [simp]:
  "from_hmam (y :: 'a ^ 'nc :: mod_type ^ 'nr:: mod_type)  carrier_mat (CARD('nr)) (CARD('nc))"
  "dim_row (from_hmam (y :: 'a ^ 'nc:: mod_type  ^ 'nr :: mod_type)) = CARD('nr)"
  "dim_col (from_hmam (y :: 'a ^ 'nc :: mod_type ^ 'nr:: mod_type )) = CARD('nc)"
  unfolding from_hmam_def by simp_all

lemma [simp]:
  "from_hmav (y :: 'a ^ 'n:: mod_type)  carrier_vec (CARD('n))"
  "dim_vec (from_hmav (y :: 'a ^ 'n:: mod_type)) = CARD('n)"
  unfolding from_hmav_def by simp_all

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

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

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


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

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


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

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

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

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


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

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

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


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

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


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

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


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


end


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

context
  includes lifting_syntax
begin

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

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

lemma HMA_addrow[transfer_rule]: 
  "((Mod_Type_Connect.HMA_M :: _  'a :: comm_ring_1 ^ 'nc :: mod_type ^ 'nr :: mod_type  _) 
    ===> (Mod_Type_Connect.HMA_I :: _ 'nr :: mod_type  _ )
    ===> (Mod_Type_Connect.HMA_I :: _ 'nr :: mod_type  _ ) 
    ===> (=)
    ===> Mod_Type_Connect.HMA_M) 
    (λA a b q. addrow q a b A) row_add"
  by (intro rel_funI, goal_cases, auto simp add: Mod_Type_Connect.HMA_M_def row_add_def)
     (rule eq_matI, auto simp add: Mod_Type_Connect.from_hmam_def Mod_Type_Connect.HMA_I_def 
      to_nat_less_card to_nat_from_nat_id)

lemma HMA_addcol[transfer_rule]: 
  "((Mod_Type_Connect.HMA_M :: _  'a :: comm_ring_1 ^ 'nc :: mod_type ^ 'nr :: mod_type  _) 
    ===> (Mod_Type_Connect.HMA_I :: _ 'nc :: mod_type  _ )
    ===> (Mod_Type_Connect.HMA_I :: _ 'nc :: mod_type  _ ) 
    ===> (=)
    ===> Mod_Type_Connect.HMA_M) 
    (λA a b q. addcol q a b A) column_add"
  by (intro rel_funI, goal_cases, auto simp add: Mod_Type_Connect.HMA_M_def column_add_def)
     (rule eq_matI, auto simp add: Mod_Type_Connect.from_hmam_def Mod_Type_Connect.HMA_I_def 
      to_nat_less_card to_nat_from_nat_id)

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

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

end

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

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


context 
  includes lifting_syntax
begin

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

lemma bi_unique_HMA_M3 [transfer_rule]: "bi_unique HMA_M3" "left_unique HMA_M3" "right_unique HMA_M3"
  unfolding HMA_M3_def bi_unique_def left_unique_def right_unique_def
  by (auto simp add: Mod_Type_Connect.HMA_M_def)

lemma right_total_HMA_M3 [transfer_rule]: "right_total HMA_M3"
  unfolding HMA_M_def right_total_def
  by (simp add: Mod_Type_Connect.HMA_M_def)

end

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

Theory SNF_Missing_Lemmas

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

section ‹Missing results›

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

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

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

hide_const (open) C
hide_const (open) measure

subsection ‹Miscellaneous lemmas›

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

lemma sum_common_left:
  fixes f::"'a  'b::comm_ring_1"
  assumes "finite A"
  shows "sum (λi. c * f i) A = c * sum f A"
  by (simp add: mult_hom.hom_sum)

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


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

hide_const (open) HMA_M HMA_I to_hmam from_hmam
hide_fact (open) from_hmam_def from_hma_to_hmam HMA_M_def HMA_I_def dim_row_transfer_rule
                  dim_col_transfer_rule

context
  includes lifting_syntax
begin

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

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

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

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

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

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


subsection ‹Lemmas about matrices, submatrices and determinants›

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

context comm_ring_1
begin

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

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

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

lemma det_singleton:
  assumes A: "A  carrier_mat 1 1"
  shows "det A = A $$ (0,0)"
  using A unfolding carrier_mat_def Determinant.det_def by auto

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

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



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


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


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

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

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


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


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


lemma smult_mat_mat_one_element:
  assumes A: "A  carrier_mat 1 1" and B: "B  carrier_mat 1 n"
  shows "A * B = A $$ (0,0) m B"
proof (rule eq_matI)
  fix i j assume i: "i < dim_row (A $$ (0, 0) m B)" and j: "j < dim_col (A $$ (0, 0) m B)"
  have i0: "i = 0" using A B i by auto
  have "(A * B) $$ (i, j) =  Matrix.row A i  col B j"
    by (rule index_mult_mat, insert i j A B, auto)
  also have "... =  Matrix.row A i $v 0 * col B j $v 0" unfolding scalar_prod_def using B by auto
  also have "... = A$$(i,i) * B$$(i,j)" using A i i0 j by auto
  also have "... = (A $$ (i, i) m B) $$ (i, j)"
    unfolding i by (rule index_smult_mat[symmetric], insert i j B, auto)
  finally show "(A * B) $$ (i, j) = (A $$ (0, 0) m B) $$ (i, j)" using i0 by simp
qed (insert A B, auto)

lemma determinant_one_element:
  assumes A: "A  carrier_mat 1 1" shows "Determinant.det A = A $$ (0,0)"
proof -
  have "Determinant.det A = prod_list (diag_mat A)"
    by (rule det_upper_triangular[OF _ A], insert A, unfold upper_triangular_def, auto)
  also have "... = A $$ (0,0)" using A unfolding diag_mat_def by auto
  finally show ?thesis .
qed



lemma invertible_mat_transpose:
  assumes inv_A: "invertible_mat (A::'a::comm_ring_1 mat)"
  shows "invertible_mat AT"
proof -
  obtain n where A: "A  carrier_mat n n"
    using inv_A unfolding invertible_mat_def square_mat.simps by auto
  hence At: "AT  carrier_mat n n" by simp
  have "Determinant.det AT = Determinant.det A"
    by (metis Determinant.det_def Determinant.det_transpose carrier_matI
        index_transpose_mat(2) index_transpose_mat(3))
  also have "... dvd 1" using invertible_iff_is_unit_JNF[OF A] inv_A by simp
  finally show ?thesis  using invertible_iff_is_unit_JNF[OF At] by auto
qed

lemma dvd_elements_mult_matrix_left:
  assumes A: "(A::'a::comm_ring_1 mat)  carrier_mat m n"
  and P: "P  carrier_mat m m"
  and x: "(i j. i<m  j<n  x dvd A$$(i,j))"
  shows "(i j. i<m  j<n  x dvd (P*A)$$(i,j))"
proof -
  have "x dvd (P * A) $$ (i, j)" if i: "i < m" and j: "j < n" for i j
  proof -
    have "(P * A) $$ (i, j) =  (ia = 0..<m. Matrix.row P i $v ia * col A j $v ia)"
      unfolding times_mat_def scalar_prod_def using A P j i by auto
    also have "... = (ia = 0..<m. Matrix.row P i $v ia *  A $$ (ia,j))"
      by (rule sum.cong, insert A j, auto)
    also have "x dvd ..." using x by (meson atLeastLessThan_iff dvd_mult dvd_sum j)
    finally show ?thesis .
  qed
  thus ?thesis by auto
qed


lemma dvd_elements_mult_matrix_right:
  assumes A: "(A::'a::comm_ring_1 mat)  carrier_mat m n"
  and Q: "Q  carrier_mat n n"
  and x: "(i j. i<m  j<n  x dvd A$$(i,j))"
  shows "(i j. i<m  j<n  x dvd (A*Q)$$(i,j))"
proof -
  have "x dvd (A*Q) $$ (i, j)" if i: "i < m" and j: "j < n" for i j
  proof -
    have "(A*Q) $$ (i, j) =  (ia = 0..<n. Matrix.row A i $v ia * col Q j $v ia)"
      unfolding times_mat_def scalar_prod_def using A Q j i by auto
    also have "... = (ia = 0..<n. A $$ (i, ia) * col Q j $v ia)"
      by (rule sum.cong, insert A Q i, auto)
    also have "x dvd ..." using x
      by (meson atLeastLessThan_iff dvd_mult2 dvd_sum i)
    finally show ?thesis .
  qed
  thus ?thesis by auto
qed


lemma dvd_elements_mult_matrix_left_right:
  assumes A: "(A::'a::comm_ring_1 mat)  carrier_mat m n"
  and P: "P  carrier_mat m m"
  and Q: "Q  carrier_mat n n"
  and x: "(i j. i<m  j<n  x dvd A$$(i,j))"
shows "(i j. i<m  j<n  x dvd (P*A*Q)$$(i,j))"
  using dvd_elements_mult_matrix_left[OF A P x]
  by (meson P A Q dvd_elements_mult_matrix_right mult_carrier_mat)


definition append_cols :: "'a :: zero mat  'a mat  'a mat" (infixr "@c" 65)where
  "A @c B = four_block_mat A B (0m 0 (dim_col A)) (0m 0 (dim_col B))"

lemma append_cols_carrier[simp,intro]:
  "A  carrier_mat n a  B  carrier_mat n b  (A @c B)  carrier_mat n (a+b)"
  unfolding append_cols_def by auto

lemma append_cols_mult_left:
  assumes A: "A  carrier_mat n a"
  and B: "B  carrier_mat n b"
  and P: "P  carrier_mat n n"
shows "P * (A @c B) = (P*A) @c (P*B)"
proof -
  let ?P = "four_block_mat P (0m n 0) (0m 0 n) (0m 0 0)"
  have "P = ?P" by (rule eq_matI, auto)
  hence "P * (A @c B) = ?P * (A @c B)" by simp
  also have "?P * (A @c B) = four_block_mat (P * A + 0m n 0 * 0m 0 (dim_col A))
  (P * B + 0m n 0 * 0m 0 (dim_col B)) (0m 0 n * A + 0m 0 0 * 0m 0 (dim_col A))
  (0m 0 n * B + 0m 0 0 * 0m 0 (dim_col B))" unfolding append_cols_def
    by (rule mult_four_block_mat, insert A B P, auto)
  also have "... = four_block_mat (P * A) (P * B) (0m 0 (dim_col (P*A))) (0m 0 (dim_col (P*B)))"
    by (rule cong_four_block_mat, insert P, auto)
  also have "... = (P*A) @c (P*B)" unfolding append_cols_def by auto
  finally show ?thesis .
qed

lemma append_cols_mult_right_id:
  assumes A: "(A::'a::semiring_1 mat)  carrier_mat n 1"
  and B: "B  carrier_mat n (m-1)"
  and C: "C = four_block_mat (1m 1) (0m 1 (m - 1)) (0m (m - 1) 1) D"
  and D: "D  carrier_mat (m-1) (m-1)"
shows "(A @c B) * C = A @c (B * D)"
proof -
  let ?C = "four_block_mat (1m 1) (0m 1 (m - 1)) (0m (m - 1) 1) D"
  have "(A @c B) * C = (A @c B) * ?C" unfolding C by auto
  also have "... = four_block_mat A B (0m 0 (dim_col A)) (0m 0 (dim_col B)) * ?C"
    unfolding append_cols_def by auto
  also have "... = four_block_mat (A * 1m 1 + B * 0m (m - 1) 1) (A * 0m 1 (m - 1) + B * D)
    (0m 0 (dim_col A) * 1m 1 + 0m 0 (dim_col B) * 0m (m - 1) 1)
    (0m 0 (dim_col A) * 0m 1 (m - 1) + 0m 0 (dim_col B) * D)"
    by (rule mult_four_block_mat, insert assms, auto)
  also have "... = four_block_mat A (B * D) (0m 0 (dim_col A)) (0m 0 (dim_col (B*D)))"
    by (rule cong_four_block_mat, insert assms, auto)
  also have "... = A @c (B * D)" unfolding append_cols_def by auto
  finally show ?thesis .
qed


lemma append_cols_mult_right_id2:
 assumes A: "(A::'a::semiring_1 mat)  carrier_mat n a"
   and B: "B  carrier_mat n b"
   and C: "C = four_block_mat D (0m a b) (0m b a) (1m b)"
   and D: "D  carrier_mat a a"
shows "(A @c B) * C = (A * D) @c B"
proof -
  let ?C = "four_block_mat D (0m a b) (0m b a) (1m b)"
  have "(A @c B) * C = (A @c B) * ?C" unfolding C by auto
  also have "... = four_block_mat A B (0m 0 a) (0m 0 b) * ?C"
    unfolding append_cols_def using A B by auto
  also have "... = four_block_mat (A * D + B * 0m b a) (A * 0m a b + B * 1m b)
    (0m 0 a * D + 0m 0 b * 0m b a) (0m 0 a * 0m a b + 0m 0 b * 1m b)"
    by (rule mult_four_block_mat, insert A B C D, auto)
  also have "... = four_block_mat (A * D) B (0m 0 (dim_col (A*D))) (0m 0 (dim_col B))"
    by (rule cong_four_block_mat, insert assms, auto)
  also have "... = (A * D) @c B" unfolding append_cols_def by auto
  finally show ?thesis .
qed


lemma append_cols_nth:
  assumes A: "A  carrier_mat n a"
  and B: "B  carrier_mat n b"
  and i: "i<n" and j: "j < a + b"
shows "(A @c B) $$ (i, j) = (if j < dim_col A then A $$(i,j) else B$$(i,j-a))" (is "?lhs = ?rhs")
proof -
  let ?C = "(0m 0 (dim_col A))"
  let ?D = "(0m 0 (dim_col B))"
  have i2: "i < dim_row A + dim_row ?D" using i A by auto
  have j2: "j < dim_col A + dim_col (0m 0 (dim_col B))" using j B A by auto
  have "(A @c B) $$ (i, j) = four_block_mat A B ?C ?D $$ (i, j)"
    unfolding append_cols_def by auto
  also have "... = (if i < dim_row A then if j < dim_col A then A $$ (i, j)
  else B $$ (i, j - dim_col A) else if j < dim_col A then ?C $$ (i - dim_row A, j)
  else 0m 0 (dim_col B) $$ (i - dim_row A, j - dim_col A))"
    by (rule index_mat_four_block(1)[OF i2 j2])
  also have "... = ?rhs" using i A by auto
  finally show ?thesis .
qed

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


lemma append_rows_nth:
  assumes A: "A  carrier_mat a n"
  and B: "B  carrier_mat b n"
  and i: "i<a+b" and j: "j < n"
shows "(A @r B) $$ (i, j) = (if i < dim_row A then A $$(i,j) else B$$(i-a,j))" (is "?lhs = ?rhs")
proof -
  let ?C = "(0m (dim_row A) 0)"
  let ?D = "(0m (dim_row B) 0)"
  have i2: "i < dim_row A + dim_row ?D" using i j A B by auto
  have j2: "j < dim_col A + dim_col ?D" using i j A B by auto
  have "(A @r B) $$ (i, j) = four_block_mat A ?C B ?D $$ (i, j)"
    unfolding append_rows_def by auto
  also have "... =  (if i < dim_row A then if j < dim_col A then A $$ (i, j) else ?C $$ (i, j - dim_col A)
   else if j < dim_col A then B $$ (i - dim_row A, j) else ?D $$ (i - dim_row A, j - dim_col A))"
    by (rule index_mat_four_block(1)[OF i2 j2])
  also have "... = ?rhs" using i A j B by auto
  finally show ?thesis .
qed

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



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

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


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