Theory Matrix_Record_Based

(*
    Authors:      Jose Divasón
                  Sebastiaan Joosten
                  René Thiemann
                  Akihisa Yamada
*)
subsection ‹Matrix Operations in Fields›

text ‹We use our record based description of a field to perform matrix operations.›

theory Matrix_Record_Based
imports 
  Jordan_Normal_Form.Gauss_Jordan_Elimination
  Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
  Arithmetic_Record_Based   
begin


definition mat_rel :: "('a  'b  bool)  'a mat  'b mat  bool" where
  "mat_rel R A B  dim_row A = dim_row B  dim_col A = dim_col B  
     ( i j. i < dim_row B  j < dim_col B  R (A $$ (i,j)) (B $$ (i,j)))"

lemma right_total_mat_rel: "right_total R  right_total (mat_rel R)" 
  unfolding right_total_def
proof
  fix B
  assume " y.  x. R x y"
  from choice[OF this] obtain f where f: " x. R (f x) x" by auto
  show " A. mat_rel R A B"
    by (rule exI[of _ "map_mat f B"], unfold mat_rel_def, auto simp: f)
qed

lemma left_unique_mat_rel: "left_unique R  left_unique (mat_rel R)"
  unfolding left_unique_def mat_rel_def mat_eq_iff by (auto, blast)

lemma right_unique_mat_rel: "right_unique R  right_unique (mat_rel R)"
  unfolding right_unique_def mat_rel_def mat_eq_iff by (auto, blast)

lemma bi_unique_mat_rel: "bi_unique R  bi_unique (mat_rel R)"
  using left_unique_mat_rel[of R] right_unique_mat_rel[of R]
  unfolding bi_unique_def left_unique_def right_unique_def by blast

lemma mat_rel_eq: "((R ===> R ===> (=))) (=) (=)  
  ((mat_rel R ===> mat_rel R ===> (=))) (=) (=)"
  unfolding mat_rel_def rel_fun_def mat_eq_iff by (auto, blast+)

definition vec_rel :: "('a  'b  bool)  'a vec  'b vec  bool" where
  "vec_rel R A B  dim_vec A = dim_vec B  ( i. i < dim_vec B  R (A $ i) (B $ i))"

lemma right_total_vec_rel: "right_total R  right_total (vec_rel R)" 
  unfolding right_total_def
proof
  fix B
  assume " y.  x. R x y"
  from choice[OF this] obtain f where f: " x. R (f x) x" by auto
  show " A. vec_rel R A B"
    by (rule exI[of _ "map_vec f B"], unfold vec_rel_def, auto simp: f)
qed

lemma left_unique_vec_rel: "left_unique R  left_unique (vec_rel R)"
  unfolding left_unique_def vec_rel_def vec_eq_iff by auto

lemma right_unique_vec_rel: "right_unique R  right_unique (vec_rel R)"
  unfolding right_unique_def vec_rel_def vec_eq_iff by auto

lemma bi_unique_vec_rel: "bi_unique R  bi_unique (vec_rel R)"
  using left_unique_vec_rel[of R] right_unique_vec_rel[of R]
  unfolding bi_unique_def left_unique_def right_unique_def by blast

lemma vec_rel_eq: "((R ===> R ===> (=))) (=) (=)  
  ((vec_rel R ===> vec_rel R ===> (=))) (=) (=)"
  unfolding vec_rel_def rel_fun_def vec_eq_iff by (auto, blast+)

lemma multrow_transfer[transfer_rule]: "((R ===> R ===> R) ===> (=) ===> R
  ===> mat_rel R ===> mat_rel R) mat_multrow_gen mat_multrow_gen"
  unfolding mat_rel_def[abs_def] mat_multrow_gen_def[abs_def]
  by (intro rel_funI conjI allI impI eq_matI, auto simp: rel_fun_def) 

(* we need index restrictions, TODO: can this be incorporated into transfer rule? *)
lemma swap_rows_transfer: "mat_rel R A B  i < dim_row B  j < dim_row B  
  mat_rel R (mat_swaprows i j A) (mat_swaprows i j B)"
  unfolding mat_rel_def mat_swaprows_def
  by (intro rel_funI conjI allI impI eq_matI, auto)

lemma pivot_positions_gen_transfer: assumes [transfer_rule]: "(R ===> R ===> (=)) (=) (=)" 
  shows 
  "(R ===> mat_rel R ===> (=)) pivot_positions_gen pivot_positions_gen" 
proof (intro rel_funI, goal_cases)
  case (1 ze ze' A A')
  note trans[transfer_rule] = 1  
  from 1 have dim: "dim_row A = dim_row A'" "dim_col A = dim_col A'" unfolding mat_rel_def by auto
  obtain i j where id: "i = 0" "j = 0" and ij: "i  dim_row A'" "j  dim_col A'" by auto
  have "pivot_positions_main_gen ze A (dim_row A) (dim_col A) i j =
    pivot_positions_main_gen ze' A' (dim_row A') (dim_col A') i j"
    using ij
  proof (induct i j rule: pivot_positions_main_gen.induct[of "dim_row A'" "dim_col A'" A' ze'])
    case (1 i j)    
    note simps[simp] = pivot_positions_main_gen.simps[of _ _ _ _ i j]
    show ?case 
    proof (cases "i < dim_row A'  j < dim_col A'")
      case False
      with dim show ?thesis by auto
    next
      case True
      hence ij: "i < dim_row A'" "j < dim_col A'" and j: "Suc j  dim_col A'" by auto
      note IH = 1(1-2)[OF ij _ _ j]
      from ij True trans have [transfer_rule]:"R (A $$ (i,j)) (A' $$ (i,j))" 
        unfolding mat_rel_def by auto
      have eq: "(A $$ (i,j) = ze) = (A' $$ (i,j) = ze')" by transfer_prover
      show ?thesis
      proof (cases "A' $$ (i,j) = ze'")
        case True
        from ij have "i  dim_row A'" by auto
        note IH = IH(1)[OF True this]
        thus ?thesis using True ij dim eq by simp
      next
        case False
        from ij have "Suc i  dim_row A'" by auto
        note IH = IH(2)[OF False this]
        thus ?thesis using False ij dim eq by simp
      qed
    qed
  qed
  thus "pivot_positions_gen ze A = pivot_positions_gen ze' A'"
    unfolding pivot_positions_gen_def id .
qed

lemma set_pivot_positions_main_gen: 
  "set (pivot_positions_main_gen ze A nr nc i j)  {0 ..< nr} × {0 ..< nc}"
proof (induct i j rule: pivot_positions_main_gen.induct[of nr nc A ze])
  case (1 i j)
  note [simp] = pivot_positions_main_gen.simps[of _ _ _ _ i j]
  from 1 show ?case
    by (cases "i < nr  j < nc", auto)
qed
  
lemma find_base_vectors_transfer: assumes [transfer_rule]: "(R ===> R ===> (=)) (=) (=)"
  shows "((R ===> R) ===> R ===> R ===> mat_rel R 
  ===> list_all2 (vec_rel R)) find_base_vectors_gen find_base_vectors_gen"
proof (intro rel_funI, goal_cases)
  case (1 um um' ze ze' on on' A A')
  note trans[transfer_rule] = 1 pivot_positions_gen_transfer[OF assms]
  from 1(4) have dim: "dim_row A = dim_row A'" "dim_col A = dim_col A'" unfolding mat_rel_def by auto
  have id: "pivot_positions_gen ze A = pivot_positions_gen ze' A'" by transfer_prover
  obtain xs where xs: "map snd (pivot_positions_gen ze' A') = xs" by auto
  obtain ys where ys: "[j[0..<dim_col A'] . j  set xs] = ys" by auto
  show "list_all2 (vec_rel R) (find_base_vectors_gen um ze on A) 
    (find_base_vectors_gen um' ze' on' A')"
    unfolding find_base_vectors_gen_def Let_def id xs list_all2_conv_all_nth length_map ys dim
  proof (intro conjI[OF refl] allI impI)
    fix i
    assume i: "i < length ys" 
    define y where "y = ys ! i" 
    from i have y: "y < dim_col A'" unfolding y_def ys[symmetric] using nth_mem by fastforce
    let ?map = "map_of (map prod.swap (pivot_positions_gen ze' A'))"
    {
      fix i
      assume i: "i < dim_col A'"
      and neq: "i  y" 
      have "R (case ?map i of None  ze | Some j  um (A $$ (j, y)))
          (case ?map i of None  ze' | Some j  um' (A' $$ (j, y)))"
      proof (cases "?map i")
        case None
        with trans(2) show ?thesis by auto
      next 
        case (Some j)
        from map_of_SomeD[OF this] have "(j,i)  set (pivot_positions_gen ze' A')" by auto
        from subsetD[OF set_pivot_positions_main_gen this[unfolded pivot_positions_gen_def]]
        have j: "j < dim_row A'" by auto
        with trans(4) y have [transfer_rule]: "R (A $$ (j,y)) (A' $$ (j,y))" unfolding mat_rel_def by auto
        show ?thesis unfolding Some by (simp, transfer_prover)
      qed
    } note main = this
    show "vec_rel R (map (non_pivot_base_gen um ze on A (pivot_positions_gen ze' A')) ys ! i)
          (map (non_pivot_base_gen um' ze' on' A' (pivot_positions_gen ze' A')) ys ! i)"
      unfolding y_def[symmetric] nth_map[OF i]
      unfolding non_pivot_base_gen_def Let_def dim vec_rel_def
      by (intro conjI allI impI, force, insert main, auto simp: trans(3))
  qed
qed
  

lemma eliminate_entries_gen_transfer: assumes *[transfer_rule]: "(R ===> R ===> R) ad ad'"
  "(R ===> R ===> R) mul mul'"
  and vs: " j. j < dim_row B'  R (vs j) (vs' j)" 
  and i: "i < dim_row B'"  
  and B: "mat_rel R B B'"
  shows "mat_rel R 
   (eliminate_entries_gen ad mul vs B i j) 
   (eliminate_entries_gen ad' mul' vs' B' i j)"
proof - 
  note BB = B[unfolded mat_rel_def]  
  show ?thesis unfolding mat_rel_def dim_eliminate_entries_gen
  proof (intro conjI impI allI)
    fix i' j'
    assume ij': "i' < dim_row B'" "j' < dim_col B'"
    with BB have ij: "i'< dim_row B" "j' < dim_col B" by auto
    have [transfer_rule]: "R (B $$ (i', j')) (B' $$ (i', j'))" using BB ij' by auto
    have [transfer_rule]: "R (B $$ (i, j')) (B' $$ (i, j'))" using BB ij' i by auto
    have [transfer_rule]: "R (vs i') (vs' i')" using ij' vs[of i'] by auto
    show "R (eliminate_entries_gen ad mul vs B i j $$ (i', j'))
        (eliminate_entries_gen ad' mul' vs' B' i j $$ (i', j'))" 
      unfolding eliminate_entries_gen_def index_mat(1)[OF ij] index_mat(1)[OF ij'] split
      by transfer_prover
  qed (insert BB, auto)
qed

context
  fixes ops :: "'i arith_ops_record" (structure)
begin
private abbreviation (input) zero where "zero  arith_ops_record.zero ops"
private abbreviation (input) one where "one  arith_ops_record.one ops"
private abbreviation (input) plus where "plus  arith_ops_record.plus ops"
private abbreviation (input) times where "times  arith_ops_record.times ops"
private abbreviation (input) minus where "minus  arith_ops_record.minus ops"
private abbreviation (input) uminus where "uminus  arith_ops_record.uminus ops"
private abbreviation (input) divide where "divide  arith_ops_record.divide ops"
private abbreviation (input) inverse where "inverse  arith_ops_record.inverse ops"
private abbreviation (input) modulo where "modulo  arith_ops_record.modulo ops"
private abbreviation (input) normalize where "normalize  arith_ops_record.normalize ops"

definition eliminate_entries_gen_zero :: "('a  'a  'a)  ('a  'a  'a)  'a  (integer  'a)  'a mat  nat  nat  'a mat" where
  "eliminate_entries_gen_zero minu time z v A I J = mat (dim_row A) (dim_col A) (λ (i, j).
     if v (integer_of_nat i)  z  i  I then minu (A $$ (i,j)) (time (v (integer_of_nat i)) (A $$ (I,j))) else A $$ (i,j))" 
  
definition eliminate_entries_i where "eliminate_entries_i  eliminate_entries_gen_zero minus times zero"
definition multrow_i where "multrow_i  mat_multrow_gen times"
  
lemma dim_eliminate_entries_gen_zero[simp]:
  "dim_row (eliminate_entries_gen_zero mm tt z v B i as) = dim_row B"
  "dim_col (eliminate_entries_gen_zero mm tt z v B i as) = dim_col B"
  unfolding eliminate_entries_gen_zero_def by auto

partial_function (tailrec) gauss_jordan_main_i :: "nat  nat  'i mat  nat  nat  'i mat" where
  [code]: "gauss_jordan_main_i nr nc A i j = (
    if i < nr  j < nc then let aij = A $$ (i,j) in if aij = zero then
      (case [ i' . i' <- [Suc i ..< nr],  A $$ (i',j)  zero] 
        of []  gauss_jordan_main_i nr nc A i (Suc j)
         | (i' # _)  gauss_jordan_main_i nr nc (swaprows i i' A) i j)
      else if aij = one then let 
        v = (λ i. A $$ (nat_of_integer i,j)) in
        gauss_jordan_main_i nr nc
        (eliminate_entries_i v A i j) (Suc i) (Suc j)
      else let iaij = inverse aij; A' = multrow_i i iaij A;
        v = (λ i. A' $$ (nat_of_integer i,j))
        in gauss_jordan_main_i nr nc (eliminate_entries_i v A' i j) (Suc i) (Suc j)
    else A)"

definition gauss_jordan_single_i :: "'i mat  'i mat" where
  "gauss_jordan_single_i A  gauss_jordan_main_i (dim_row A) (dim_col A) A 0 0"

definition find_base_vectors_i :: "'i mat  'i vec list" where
  "find_base_vectors_i A  find_base_vectors_gen uminus zero one A"
end

(* **************************************************************************** *)
(* subsection ‹Proofs› *)

context field_ops
begin

lemma right_total_poly_rel[transfer_rule]: "right_total (mat_rel R)"
  using right_total_mat_rel[of R] right_total .

lemma bi_unique_poly_rel[transfer_rule]: "bi_unique (mat_rel R)"
  using bi_unique_mat_rel[of R] bi_unique .

lemma eq_mat_rel[transfer_rule]: "(mat_rel R ===> mat_rel R ===> (=)) (=) (=)"
  by (rule mat_rel_eq[OF eq])

lemma multrow_i[transfer_rule]: "((=) ===> R ===> mat_rel R ===> mat_rel R)
  (multrow_i ops) multrow" 
  using multrow_transfer[of R] times unfolding multrow_i_def rel_fun_def by blast  

lemma eliminate_entries_gen_zero[simp]:
  assumes "mat_rel R A A'" "I < dim_row A'" shows
  "eliminate_entries_gen_zero minus times zero v A I J = eliminate_entries_gen minus times (v o integer_of_nat) A I J"
  unfolding eliminate_entries_gen_def eliminate_entries_gen_zero_def
proof(standard,goal_cases)
  case (1 i j)
  have d1:"DP (A $$ (I, j))" and d2:"DP (A $$ (i, j))" using assms DPR 1
    unfolding mat_rel_def dim_col_mat dim_row_mat
    by (metis Domainp.DomainI)+
  have e1:" x. (0::'a) * x = 0" and e2:" x. x - (0::'a) = x" by auto
  from e1[untransferred,OF d1] e2[untransferred,OF d2] 1 show ?case by auto
qed auto

lemma eliminate_entries_i: assumes  
  vs: " j. j < dim_row B'  R (vs (integer_of_nat j)) (vs' j)" 
  and i: "i < dim_row B'"  
  and B: "mat_rel R B B'"  
  shows "mat_rel R (eliminate_entries_i ops vs B i j) 
    (eliminate_entries vs' B' i j)"
  unfolding eliminate_entries_i_def eliminate_entries_gen_zero[OF B i]
  by (rule eliminate_entries_gen_transfer, insert assms, auto simp: plus times minus)

lemma gauss_jordan_main_i:  
  "nr = dim_row A'  nc = dim_col A'  mat_rel R A A'  i  nr  j  nc 
    mat_rel R (gauss_jordan_main_i ops nr nc A i j) (fst (gauss_jordan_main A' B' i j))"
proof -
  obtain P where P: "P = (A',i,j)" by auto
  let ?Rel = "measures [λ (A' :: 'a mat,i,j). nc - j, λ (A',i,j). if A' $$ (i,j) = 0 then 1 else 0]"
  have wf: "wf ?Rel" by simp
  show "nr = dim_row A'  nc = dim_col A'  mat_rel R A A'  i  nr  j  nc 
    mat_rel R (gauss_jordan_main_i ops nr nc A i j) (fst (gauss_jordan_main A' B' i j))"
    using P
  proof (induct P arbitrary: A' B' A i j rule: wf_induct[OF wf])
    case (1 P A' B' A i j)
    note prems = 1(2-6)
    note P = 1(7)
    note A[transfer_rule] = prems(3)
    note IH = 1(1)[rule_format, OF _ _ _ _ _ _ refl]
    note simps = gauss_jordan_main_code[of A' B' i j, unfolded Let_def, folded prems(1-2)] 
      gauss_jordan_main_i.simps[of ops nr nc A i j] Let_def if_True if_False
    show ?case
    proof (cases "i < nr  j < nc")
      case False
      hence id: "(i < nr  j < nc) = False" by simp
      show ?thesis unfolding simps id by simp transfer_prover
    next
      case True note ij' = this
      hence id: "(i < nr  j < nc) = True" " x y z. (if x = x then y else z) = y" by auto
      from True prems have ij [transfer_rule]:"R (A $$ (i,j)) (A' $$ (i,j))" 
        unfolding mat_rel_def by auto
      from True prems have i: "i < dim_row A'" "j < dim_col A'" and i': "i < nr" "j < nc" by auto
      {
        fix i
        assume "i < dim_row A'"
        with i True prems have R[transfer_rule]:"R (A $$ (i,j)) (A' $$ (i,j))" 
          unfolding mat_rel_def by auto
        have "(A $$ (i,j) = zero) = (A' $$ (i,j) = 0)" by transfer_prover
        note this R
      } note eq_gen = this    
      have eq: "(A $$ (i,j) = zero) = (A' $$ (i,j) = 0)"
        "(A $$ (i,j) = one) = (A' $$ (i,j) = 1)"
        by transfer_prover+
      show ?thesis
      proof (cases "A' $$ (i, j) = 0")
        case True
        hence eq: "A $$ (i,j) = zero" using eq by auto
        let ?is = "[ i' . i' <- [Suc i ..< nr],  A $$ (i',j)  zero]"
        let ?is' = "[ i' . i' <- [Suc i ..< nr],  A' $$ (i',j)  0]"
        define xs where "xs = [Suc i..<nr]" 
        have xs: "set xs  {0 ..< dim_row A'}" unfolding xs_def using prems by auto
        hence id': "?is = ?is'" unfolding xs_def[symmetric]
          by (induct xs, insert eq_gen, auto)
        show ?thesis
        proof (cases ?is')
          case Nil
          have "?thesis = (mat_rel R (gauss_jordan_main_i ops nr nc A i (Suc j)) 
            (fst (gauss_jordan_main A' B' i (Suc j))))" 
            unfolding True simps id eq unfolding Nil id'[unfolded Nil] by simp
          also have ""
            by (rule IH, insert i prems P, auto)
          finally show ?thesis .
        next
          case (Cons i' idx')
          from arg_cong[OF this, of set] i 
          have i': "i' < nr" "A' $$ (i', j)  0" by auto
          with ij' prems(1-2) have *: "i' < dim_row A'" "i < dim_row A'" "j < dim_col A'" by auto
          have rel: "((swaprows i i' A', i, j), P)  ?Rel"
            by (simp add: P True * i')
          have "?thesis = (mat_rel R (gauss_jordan_main_i ops nr nc (swaprows i i' A) i j)
            (fst (gauss_jordan_main (swaprows i i' A') (swaprows i i' B') i j)))"
             unfolding True simps id eq Cons id'[unfolded Cons] by simp
          also have "" 
            by (rule IH[OF rel _ _ swap_rows_transfer], insert i i' prems P True, auto)
          finally show ?thesis .
        qed
      next
        case False
        from False eq have neq: "(A $$ (i, j) = zero) = False" "(A' $$ (i, j) = 0) = False" by auto
        {
          fix B B' i
          assume B[transfer_rule]: "mat_rel R B B'" and dim: "dim_col B' = nc" and i: "i < dim_row B'"
          from dim i True have "j < dim_col B'" by simp
          with B i have "R (B $$ (i,j)) (B' $$ (i,j))"
            by (simp add: mat_rel_def)
        } note vec_rel = this        
        from prems have dim: "dim_row A = dim_row A'" unfolding mat_rel_def by auto
        show ?thesis 
        proof (cases "A' $$ (i, j) = 1")
          case True
          from True eq have eq: "(A $$ (i,j) = one) = True" "(A' $$ (i,j) = 1) = True" by auto
          note rel = vec_rel[OF A]
          show ?thesis unfolding simps id neq eq
            by (rule IH[OF _ _ _ eliminate_entries_i], insert rel prems ij i P dim, auto)
        next
          case False
          from False eq have eq: "(A $$ (i,j) = one) = False" "(A' $$ (i,j) = 1) = False" by auto
          show ?thesis unfolding simps id neq eq 
          proof (rule IH, goal_cases)
            case 4
            have A': "mat_rel R (multrow_i ops i (inverse (A $$ (i, j))) A)
              (multrow i (inverse_class.inverse (A' $$ (i, j))) A')" by transfer_prover
            note rel = vec_rel[OF A']
            show ?case 
              by (rule eliminate_entries_i[OF _ _ A'], insert rel prems i dim, auto)
          qed (insert prems i P, auto)
        qed
      qed
    qed
  qed   
qed

lemma gauss_jordan_i[transfer_rule]:  
  "(mat_rel R ===> mat_rel R) (gauss_jordan_single_i ops) gauss_jordan_single"
proof (intro rel_funI)
  fix A A'
  assume A: "mat_rel R A A'"
  show "mat_rel R (gauss_jordan_single_i ops A) (gauss_jordan_single A')"
    unfolding gauss_jordan_single_def gauss_jordan_single_i_def gauss_jordan_def
    by (rule gauss_jordan_main_i[OF _ _ A], insert A, auto simp: mat_rel_def)
qed

lemma find_base_vectors_i[transfer_rule]:  
  "(mat_rel R ===> list_all2 (vec_rel R)) (find_base_vectors_i ops) find_base_vectors"
  unfolding find_base_vectors_i_def[abs_def] 
  using find_base_vectors_transfer[OF eq] uminus zero one 
  unfolding rel_fun_def by blast
  
end

lemma list_of_vec_transfer[transfer_rule]: "(vec_rel A ===> list_all2 A) list_of_vec list_of_vec"
  unfolding rel_fun_def vec_rel_def vec_eq_iff list_all2_conv_all_nth
  by auto

lemma IArray_sub'[simp]: "i < IArray.length a  IArray.sub' (a, integer_of_nat i) = IArray.sub a i" 
  by auto

lift_definition eliminate_entries_i2 ::
  "'a  ('a  'a  'a)  ('a  'a  'a)  (integer  'a)  'a mat_impl  integer  'a mat_impl" is
  "λ z mminus ttimes v (nr, nc, a) i'.
   (nr,nc,let ai' = IArray.sub' (a, i') in (IArray.tabulate (integer_of_nat nr, λ i. let ai = IArray.sub' (a, i) in
     if i = i' then ai else 
     let vi'j = v i 
     in if vi'j = z then ai
        else 
             IArray.tabulate (integer_of_nat nc, λ j. mminus (IArray.sub' (ai, j)) (ttimes vi'j 
               (IArray.sub' (ai', j))))
       )))" 
proof(goal_cases)
  case (1 z mm tt  vec prod nat2)
  thus ?case by(cases prod;cases "snd (snd prod)";auto simp:Let_def)
qed

lemma eliminate_entries_gen_zero [simp]:
  assumes "i<(dim_row A)" "j<(dim_col A)" shows
  "eliminate_entries_gen_zero mminus ttimes z v A I J $$ (i, j) =
   (if v (integer_of_nat i) = z  i = I then A $$ (i,j) else mminus (A $$ (i,j)) (ttimes (v (integer_of_nat i)) (A $$ (I,j))))"
using assms unfolding eliminate_entries_gen_zero_def by auto


lemma eliminate_entries_gen [simp]:
  assumes "i<(dim_row A)" "j<(dim_col A)" shows
  "eliminate_entries_gen mminus ttimes v A I J $$ (i, j) =
   (if i = I then A $$ (i,j) else mminus (A $$ (i,j)) (ttimes (v i) (A $$ (I,j))))"
using assms unfolding eliminate_entries_gen_def by auto

lemma dim_mat_impl [simp]:
  "dim_row (mat_impl x) = dim_row_impl x"
  "dim_col (mat_impl x) = dim_col_impl x"
  by (cases "Rep_mat_impl x";auto simp:mat_impl.rep_eq dim_row_def dim_col_def dim_row_impl.rep_eq dim_col_impl.rep_eq)+

lemma dim_eliminate_entries_i2 [simp]:
  "dim_row_impl (eliminate_entries_i2 z mm tt v m i) = dim_row_impl m"
  "dim_col_impl (eliminate_entries_i2 z mm tt v m i) = dim_col_impl m"
  by (transfer, auto)+

lemma tabulate_nth: "i < n  IArray.tabulate (integer_of_nat n, f) !! i = f (integer_of_nat i)" 
  using of_fun_nth[of i n] by auto

lemma eliminate_entries_i2[code]:"eliminate_entries_gen_zero mm tt z v (mat_impl m) i j
   = (if i < dim_row_impl m 
     then mat_impl (eliminate_entries_i2 z mm tt v m (integer_of_nat i))
     else (Code.abort (STR ''index out of range in eliminate_entries'') 
       (λ _. eliminate_entries_gen_zero mm tt z v (mat_impl m) i j)))"
proof (cases "i < dim_row_impl m")
  case True
  hence id: "(i < dim_row_impl m) = True" by simp
  show ?thesis unfolding id if_True
  proof (standard;goal_cases)
    case (1 i j)
    have dims: "i < dim_row (mat_impl m)" "j < dim_col (mat_impl m)" using 1 by (auto simp:eliminate_entries_i2.rep_eq)
    then show ?case unfolding eliminate_entries_gen_zero[OF dims] using True
    proof(transfer, goal_cases)
      case (1 i m j ia v z mm tt)
      obtain nr nc M where m: "m = (nr,nc,M)" by (cases m) 
      note 1 = 1[unfolded m, simplified]
      have mk: " f. mk_mat nr nc f (i,j) = f (i,j)" 
         " f. mk_mat nr nc f (ia,j) = f (ia,j)" 
        using 1 unfolding mk_mat_def mk_vec_def by auto
      note of_fun = of_fun_nth[OF 1(2)] of_fun_nth[OF 1(3)] tabulate_nth[OF 1(2)] tabulate_nth[OF 1(3)]
      let ?c1 = "v (integer_of_nat i) = z" 
      show ?case
      proof (cases "?c1  i = ia")
        case True
        hence id: "(if ?c1  i = ia then x else y) = x" 
          "(if integer_of_nat i = integer_of_nat ia then x else if ?c1 then x else y) = x" for x y 
          by auto
        show ?thesis unfolding id m o_def Let_def split snd_conv mk of_fun by (auto simp: 1)
      next
        case False
        hence id: "?c1 = False " "(integer_of_nat i = integer_of_nat ia) = False" "(False  i = ia) = False" 
          by (auto simp add: integer_of_nat_eq_of_nat)
        show ?thesis unfolding m o_def Let_def split snd_conv mk of_fun id if_False 
          by (auto simp: 1)
      qed
    qed  
  qed (auto simp:eliminate_entries_i2.rep_eq)
qed auto

end