# Theory Matrix_Change_Row

```section ‹Missing Matrix Operations›

text ‹In this theory we provide an operation that can change a single
row in a matrix efficiently, and all other rows in the matrix implementation
will be reused.›

(* TODO: move this part into JNF-AFP-entry *)

theory Matrix_Change_Row
imports
Jordan_Normal_Form.Matrix_IArray_Impl
Polynomial_Interpolation.Missing_Unsorted
begin

definition change_row :: "nat ⇒ (nat ⇒ 'a ⇒ 'a) ⇒ 'a mat ⇒ 'a mat" where
"change_row k f A = mat (dim_row A) (dim_col A) (λ (i,j).
if i = k then f j (A \$\$ (k,j)) else A \$\$ (i,j))"

lemma change_row_carrier[simp]:
"(change_row k f A ∈ carrier_mat nr nc) = (A ∈ carrier_mat nr nc)"
"dim_row (change_row k f A) = dim_row A"
"dim_col (change_row k f A) = dim_col A"
unfolding change_row_def carrier_mat_def by auto

lemma change_row_index[simp]: "A ∈ carrier_mat nr nc ⟹ i < nr ⟹ j < nc ⟹
change_row k f A \$\$ (i,j) = (if i = k then f j (A \$\$ (k,j)) else A \$\$ (i,j))"
"i < dim_row A ⟹ j < dim_col A ⟹ change_row k f A \$\$ (i,j) = (if i = k then f j (A \$\$ (k,j)) else A \$\$ (i,j))"
unfolding change_row_def by auto

lift_definition change_row_impl :: "nat ⇒ (nat ⇒ 'a ⇒ 'a) ⇒ 'a mat_impl ⇒ 'a mat_impl" is
"λ k f (nr,nc,A). let Ak = IArray.sub A k; Arows = IArray.list_of A;
Ak' = IArray.IArray (map (λ (i,c). f i c) (zip [0 ..< nc] (IArray.list_of Ak)));
A' = IArray.IArray (Arows [k := Ak'])
in (nr,nc,A')"
proof (auto, goal_cases)
case (1 k f nc b row)
show ?case
proof (cases b)
case (IArray rows)
with 1 have "row ∈ set rows ∨ k < length rows
∧ row = IArray (map (λ (i,c). f i c) (zip [0 ..< nc] (IArray.list_of (rows ! k))))"
by (cases "k < length rows", auto simp: set_list_update dest: in_set_takeD in_set_dropD)
with 1 IArray show ?thesis by (cases, auto)
qed
qed

lemma change_row_code[code]: "change_row k f (mat_impl A) = (if k < dim_row_impl A
then mat_impl (change_row_impl k f A)
else Code.abort (STR ''index out of bounds in change_row'') (λ _. change_row k f (mat_impl A)))"
(is "?l = ?r")
proof (cases "k < dim_row_impl A")
case True
hence id: "?r = mat_impl (change_row_impl k f A)" by simp
show ?thesis unfolding id unfolding change_row_def
proof (rule eq_matI, goal_cases)
case (1 i j)
thus ?case using True
by (transfer, auto simp: mk_mat_def)
qed (transfer, auto)+
qed simp

end
```