[STATEMENT]
lemma list_to_mat_to_cols_list [simp]:
  fixes l::"complex list list"
  assumes "mat nr nc l"
  shows "mat_to_cols_list (mat_of_cols_list nr l) = l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_to_cols_list (Tensor.mat_of_cols_list nr l) = l
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat_to_cols_list (Tensor.mat_of_cols_list nr l) = l
[PROOF STEP]
have "length (mat_to_cols_list (mat_of_cols_list nr l)) = length l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (mat_to_cols_list (Tensor.mat_of_cols_list nr l)) = length l
[PROOF STEP]
by (simp add: mat_of_cols_list_def)
[PROOF STATE]
proof (state)
this:
length (mat_to_cols_list (Tensor.mat_of_cols_list nr l)) = length l

goal (1 subgoal):
 1. mat_to_cols_list (Tensor.mat_of_cols_list nr l) = l
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length (mat_to_cols_list (Tensor.mat_of_cols_list nr l)) = length l

goal (1 subgoal):
 1. mat_to_cols_list (Tensor.mat_of_cols_list nr l) = l
[PROOF STEP]
have f1:"\<forall>j<length l. length(l ! j) = mult.row_length l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j<length l. length (l ! j) = mult.row_length l
[PROOF STEP]
using assms plus_mult.row_length_constant plus_mult_cpx
[PROOF STATE]
proof (prove)
using this:
Matrix_Legacy.mat nr nc l
\<lbrakk>plus_mult ?id ?f ?zer ?g ?inver; Matrix_Legacy.mat ?nr ?nc ?A; ?j < length ?A\<rbrakk> \<Longrightarrow> length (?A ! ?j) = mult.row_length ?A
plus_mult 1 (*) 0 (+) (a_inv cpx_rng)

goal (1 subgoal):
 1. \<forall>j<length l. length (l ! j) = mult.row_length l
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>j<length l. length (l ! j) = mult.row_length l

goal (1 subgoal):
 1. mat_to_cols_list (Tensor.mat_of_cols_list nr l) = l
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>j<length l. length (l ! j) = mult.row_length l

goal (1 subgoal):
 1. mat_to_cols_list (Tensor.mat_of_cols_list nr l) = l
[PROOF STEP]
have "\<And>j. j<length l \<longrightarrow> mat_to_cols_list (mat_of_cols_list nr l) ! j = l ! j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. j < length l \<longrightarrow> mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! j = l ! j
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. j < length l \<Longrightarrow> mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! j = l ! j
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. j < length l \<Longrightarrow> mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! j = l ! j
[PROOF STEP]
assume a:"j < length l"
[PROOF STATE]
proof (state)
this:
j < length l

goal (1 subgoal):
 1. \<And>j. j < length l \<Longrightarrow> mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! j = l ! j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j < length l
[PROOF STEP]
have f2:"length (mat_to_cols_list (mat_of_cols_list nr l) ! j) = length (l ! j)"
[PROOF STATE]
proof (prove)
using this:
j < length l

goal (1 subgoal):
 1. length (mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! j) = length (l ! j)
[PROOF STEP]
by (metis col_def mat_def vec_def mat_of_cols_list_def assms dim_col_mat(1) dim_row_mat(1)
length_col_mat_to_cols_list nth_mem)
[PROOF STATE]
proof (state)
this:
length (mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! j) = length (l ! j)

goal (1 subgoal):
 1. \<And>j. j < length l \<Longrightarrow> mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! j = l ! j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! j) = length (l ! j)
[PROOF STEP]
have "\<forall>i<mult.row_length l. mat_to_cols_list (mat_of_cols_list nr l) ! j ! i = l ! j ! i"
[PROOF STATE]
proof (prove)
using this:
length (mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! j) = length (l ! j)

goal (1 subgoal):
 1. \<forall>i<mult.row_length l. mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! j ! i = l ! j ! i
[PROOF STEP]
using a mat_to_cols_list_def mat_of_cols_list_def f1
[PROOF STATE]
proof (prove)
using this:
length (mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! j) = length (l ! j)
j < length l
mat_to_cols_list ?A = map (\<lambda>j. map (\<lambda>i. ?A $$ (i, j)) [0..<dim_row ?A]) [0..<dim_col ?A]
Tensor.mat_of_cols_list ?nr ?cs = Matrix.mat ?nr (length ?cs) (\<lambda>(i, j). ?cs ! j ! i)
\<forall>j<length l. length (l ! j) = mult.row_length l

goal (1 subgoal):
 1. \<forall>i<mult.row_length l. mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! j ! i = l ! j ! i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>i<mult.row_length l. mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! j ! i = l ! j ! i

goal (1 subgoal):
 1. \<And>j. j < length l \<Longrightarrow> mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! j = l ! j
[PROOF STEP]
thus "mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! j = l ! j"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<mult.row_length l. mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! j ! i = l ! j ! i

goal (1 subgoal):
 1. mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! j = l ! j
[PROOF STEP]
using f2
[PROOF STATE]
proof (prove)
using this:
\<forall>i<mult.row_length l. mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! j ! i = l ! j ! i
length (mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! j) = length (l ! j)

goal (1 subgoal):
 1. mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! j = l ! j
[PROOF STEP]
by(simp add: nth_equalityI a f1)
[PROOF STATE]
proof (state)
this:
mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! j = l ! j

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?j < length l \<longrightarrow> mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! ?j = l ! ?j

goal (1 subgoal):
 1. mat_to_cols_list (Tensor.mat_of_cols_list nr l) = l
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length (mat_to_cols_list (Tensor.mat_of_cols_list nr l)) = length l
\<forall>j<length l. length (l ! j) = mult.row_length l
?j < length l \<longrightarrow> mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! ?j = l ! ?j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length (mat_to_cols_list (Tensor.mat_of_cols_list nr l)) = length l
\<forall>j<length l. length (l ! j) = mult.row_length l
?j < length l \<longrightarrow> mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! ?j = l ! ?j

goal (1 subgoal):
 1. mat_to_cols_list (Tensor.mat_of_cols_list nr l) = l
[PROOF STEP]
using nth_equalityI
[PROOF STATE]
proof (prove)
using this:
length (mat_to_cols_list (Tensor.mat_of_cols_list nr l)) = length l
\<forall>j<length l. length (l ! j) = mult.row_length l
?j < length l \<longrightarrow> mat_to_cols_list (Tensor.mat_of_cols_list nr l) ! ?j = l ! ?j
\<lbrakk>length ?xs = length ?ys; \<And>i. i < length ?xs \<Longrightarrow> ?xs ! i = ?ys ! i\<rbrakk> \<Longrightarrow> ?xs = ?ys

goal (1 subgoal):
 1. mat_to_cols_list (Tensor.mat_of_cols_list nr l) = l
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
mat_to_cols_list (Tensor.mat_of_cols_list nr l) = l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma col_mat_of_cols_list [simp]:
  assumes "j < length l"
  shows "Matrix.col (mat_of_cols_list (length (l ! j)) l) j = vec_of_list (l ! j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix.col (Tensor.mat_of_cols_list (length (l ! j)) l) j = vec_of_list (l ! j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Matrix.col (Tensor.mat_of_cols_list (length (l ! j)) l) j = vec_of_list (l ! j)
[PROOF STEP]
define u where "u = Matrix.col (mat_of_cols_list (length (l ! j)) l) j"
[PROOF STATE]
proof (state)
this:
u = Matrix.col (Tensor.mat_of_cols_list (length (l ! j)) l) j

goal (1 subgoal):
 1. Matrix.col (Tensor.mat_of_cols_list (length (l ! j)) l) j = vec_of_list (l ! j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u = Matrix.col (Tensor.mat_of_cols_list (length (l ! j)) l) j
[PROOF STEP]
have "dim_vec u = dim_vec (vec_of_list (l ! j))"
[PROOF STATE]
proof (prove)
using this:
u = Matrix.col (Tensor.mat_of_cols_list (length (l ! j)) l) j

goal (1 subgoal):
 1. dim_vec u = dim_vec (vec_of_list (l ! j))
[PROOF STEP]
by (auto simp: u_def mat_of_cols_list_def Matrix.col_def vec_of_list_def)
      (metis dim_vec_of_list vec_of_list.abs_eq)
[PROOF STATE]
proof (state)
this:
dim_vec u = dim_vec (vec_of_list (l ! j))

goal (1 subgoal):
 1. Matrix.col (Tensor.mat_of_cols_list (length (l ! j)) l) j = vec_of_list (l ! j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dim_vec u = dim_vec (vec_of_list (l ! j))

goal (1 subgoal):
 1. Matrix.col (Tensor.mat_of_cols_list (length (l ! j)) l) j = vec_of_list (l ! j)
[PROOF STEP]
have "\<forall>i<length(l ! j). u $ i = vec_of_list (l ! j) $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<length (l ! j). u $ i = vec_of_list (l ! j) $ i
[PROOF STEP]
by (simp add: u_def vec_of_list_index mat_of_cols_list_def assms)
[PROOF STATE]
proof (state)
this:
\<forall>i<length (l ! j). u $ i = vec_of_list (l ! j) $ i

goal (1 subgoal):
 1. Matrix.col (Tensor.mat_of_cols_list (length (l ! j)) l) j = vec_of_list (l ! j)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dim_vec u = dim_vec (vec_of_list (l ! j))
\<forall>i<length (l ! j). u $ i = vec_of_list (l ! j) $ i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dim_vec u = dim_vec (vec_of_list (l ! j))
\<forall>i<length (l ! j). u $ i = vec_of_list (l ! j) $ i

goal (1 subgoal):
 1. Matrix.col (Tensor.mat_of_cols_list (length (l ! j)) l) j = vec_of_list (l ! j)
[PROOF STEP]
by(simp add: vec_eq_iff u_def)
[PROOF STATE]
proof (state)
this:
Matrix.col (Tensor.mat_of_cols_list (length (l ! j)) l) j = vec_of_list (l ! j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dim_row_tensor_mat [simp]:
  "dim_row (A \<Otimes> B) = dim_row A * dim_row B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (A \<Otimes> B) = dim_row A * dim_row B
[PROOF STEP]
by (simp add: mat_of_cols_list_def tensor_mat_def)


[STATEMENT]
lemma dim_col_tensor_mat [simp]:
  "dim_col (A \<Otimes> B) = dim_col A * dim_col B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col (A \<Otimes> B) = dim_col A * dim_col B
[PROOF STEP]
using tensor_mat_def mat_of_cols_list_def mult.length_Tensor[of "1" "(*)"]
[PROOF STATE]
proof (prove)
using this:
?A \<Otimes> ?B \<equiv> Tensor.mat_of_cols_list (dim_row ?A * dim_row ?B) (mult.Tensor (*) (mat_to_cols_list ?A) (mat_to_cols_list ?B))
Tensor.mat_of_cols_list ?nr ?cs = Matrix.mat ?nr (length ?cs) (\<lambda>(i, j). ?cs ! j ! i)
Matrix_Tensor.mult (1::?'a1) (*) \<Longrightarrow> length (mult.Tensor (*) ?M1.0 ?M2.0) = length ?M1.0 * length ?M2.0

goal (1 subgoal):
 1. dim_col (A \<Otimes> B) = dim_col A * dim_col B
[PROOF STEP]
by(simp add: \<open>\<And>M2 M1. Matrix_Tensor.mult 1 (*) \<Longrightarrow> length (mult.Tensor (*) M1 M2) = length M1 * length M2\<close> mult.intro)


[STATEMENT]
lemma index_tensor_mat [simp]:
  assumes a1:"dim_row A = rA" and a2:"dim_col A = cA" and a3:"dim_row B = rB" and a4:"dim_col B = cB"
    and a5:"i < rA * rB" and a6:"j < cA * cB" and a7:"cA > 0" and a8:"cB > 0"
  shows "(A \<Otimes> B) $$ (i,j) = A $$ (i div rB, j div cB) * B $$ (i mod rB, j mod cB)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<Otimes> B) $$ (i, j) = A $$ (i div rB, j div cB) * B $$ (i mod rB, j mod cB)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (A \<Otimes> B) $$ (i, j) = A $$ (i div rB, j div cB) * B $$ (i mod rB, j mod cB)
[PROOF STEP]
have "(A \<Otimes> B) $$ (i,j) = (mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B)) ! j ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<Otimes> B) $$ (i, j) = mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) ! j ! i
[PROOF STEP]
using assms tensor_mat_def mat_of_cols_list_def dim_col_tensor_mat
[PROOF STATE]
proof (prove)
using this:
dim_row A = rA
dim_col A = cA
dim_row B = rB
dim_col B = cB
i < rA * rB
j < cA * cB
0 < cA
0 < cB
?A \<Otimes> ?B \<equiv> Tensor.mat_of_cols_list (dim_row ?A * dim_row ?B) (mult.Tensor (*) (mat_to_cols_list ?A) (mat_to_cols_list ?B))
Tensor.mat_of_cols_list ?nr ?cs = Matrix.mat ?nr (length ?cs) (\<lambda>(i, j). ?cs ! j ! i)
dim_col (?A \<Otimes> ?B) = dim_col ?A * dim_col ?B

goal (1 subgoal):
 1. (A \<Otimes> B) $$ (i, j) = mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) ! j ! i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(A \<Otimes> B) $$ (i, j) = mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) ! j ! i

goal (1 subgoal):
 1. (A \<Otimes> B) $$ (i, j) = A $$ (i div rB, j div cB) * B $$ (i mod rB, j mod cB)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(A \<Otimes> B) $$ (i, j) = mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) ! j ! i

goal (1 subgoal):
 1. (A \<Otimes> B) $$ (i, j) = A $$ (i div rB, j div cB) * B $$ (i mod rB, j mod cB)
[PROOF STEP]
have f:"i < mult.row_length (mat_to_cols_list A) * mult.row_length (mat_to_cols_list B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < mult.row_length (mat_to_cols_list A) * mult.row_length (mat_to_cols_list B)
[PROOF STEP]
by (simp add: a1 a2 a3 a4 a5 a7 a8)
[PROOF STATE]
proof (state)
this:
i < mult.row_length (mat_to_cols_list A) * mult.row_length (mat_to_cols_list B)

goal (1 subgoal):
 1. (A \<Otimes> B) $$ (i, j) = A $$ (i div rB, j div cB) * B $$ (i mod rB, j mod cB)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i < mult.row_length (mat_to_cols_list A) * mult.row_length (mat_to_cols_list B)

goal (1 subgoal):
 1. (A \<Otimes> B) $$ (i, j) = A $$ (i div rB, j div cB) * B $$ (i mod rB, j mod cB)
[PROOF STEP]
have "j < length (mat_to_cols_list A) * length (mat_to_cols_list B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < length (mat_to_cols_list A) * length (mat_to_cols_list B)
[PROOF STEP]
by (simp add: a2 a4 a6)
[PROOF STATE]
proof (state)
this:
j < length (mat_to_cols_list A) * length (mat_to_cols_list B)

goal (1 subgoal):
 1. (A \<Otimes> B) $$ (i, j) = A $$ (i div rB, j div cB) * B $$ (i mod rB, j mod cB)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j < length (mat_to_cols_list A) * length (mat_to_cols_list B)

goal (1 subgoal):
 1. (A \<Otimes> B) $$ (i, j) = A $$ (i div rB, j div cB) * B $$ (i mod rB, j mod cB)
[PROOF STEP]
have "mat (mult.row_length (mat_to_cols_list A)) (length (mat_to_cols_list A)) (mat_to_cols_list A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (length (mat_to_cols_list A)) (mat_to_cols_list A)
[PROOF STEP]
using a2 a7 mat_to_cols_list_is_mat
[PROOF STATE]
proof (prove)
using this:
dim_col A = cA
0 < cA
0 < dim_col ?A \<Longrightarrow> Matrix_Legacy.mat (mult.row_length (mat_to_cols_list ?A)) (length (mat_to_cols_list ?A)) (mat_to_cols_list ?A)

goal (1 subgoal):
 1. Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (length (mat_to_cols_list A)) (mat_to_cols_list A)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (length (mat_to_cols_list A)) (mat_to_cols_list A)

goal (1 subgoal):
 1. (A \<Otimes> B) $$ (i, j) = A $$ (i div rB, j div cB) * B $$ (i mod rB, j mod cB)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (length (mat_to_cols_list A)) (mat_to_cols_list A)

goal (1 subgoal):
 1. (A \<Otimes> B) $$ (i, j) = A $$ (i div rB, j div cB) * B $$ (i mod rB, j mod cB)
[PROOF STEP]
have "mat (mult.row_length (mat_to_cols_list B)) (length (mat_to_cols_list B)) (mat_to_cols_list B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix_Legacy.mat (mult.row_length (mat_to_cols_list B)) (length (mat_to_cols_list B)) (mat_to_cols_list B)
[PROOF STEP]
using a4 a8 mat_to_cols_list_is_mat
[PROOF STATE]
proof (prove)
using this:
dim_col B = cB
0 < cB
0 < dim_col ?A \<Longrightarrow> Matrix_Legacy.mat (mult.row_length (mat_to_cols_list ?A)) (length (mat_to_cols_list ?A)) (mat_to_cols_list ?A)

goal (1 subgoal):
 1. Matrix_Legacy.mat (mult.row_length (mat_to_cols_list B)) (length (mat_to_cols_list B)) (mat_to_cols_list B)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Matrix_Legacy.mat (mult.row_length (mat_to_cols_list B)) (length (mat_to_cols_list B)) (mat_to_cols_list B)

goal (1 subgoal):
 1. (A \<Otimes> B) $$ (i, j) = A $$ (i div rB, j div cB) * B $$ (i mod rB, j mod cB)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(A \<Otimes> B) $$ (i, j) = mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) ! j ! i
i < mult.row_length (mat_to_cols_list A) * mult.row_length (mat_to_cols_list B)
j < length (mat_to_cols_list A) * length (mat_to_cols_list B)
Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (length (mat_to_cols_list A)) (mat_to_cols_list A)
Matrix_Legacy.mat (mult.row_length (mat_to_cols_list B)) (length (mat_to_cols_list B)) (mat_to_cols_list B)
[PROOF STEP]
have "(A \<Otimes> B) $$ (i,j) =
    (mat_to_cols_list A) ! (j div length (mat_to_cols_list B)) ! (i div mult.row_length (mat_to_cols_list B))
    * (mat_to_cols_list B) ! (j mod length (mat_to_cols_list B)) ! (i mod mult.row_length (mat_to_cols_list B))"
[PROOF STATE]
proof (prove)
using this:
(A \<Otimes> B) $$ (i, j) = mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) ! j ! i
i < mult.row_length (mat_to_cols_list A) * mult.row_length (mat_to_cols_list B)
j < length (mat_to_cols_list A) * length (mat_to_cols_list B)
Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (length (mat_to_cols_list A)) (mat_to_cols_list A)
Matrix_Legacy.mat (mult.row_length (mat_to_cols_list B)) (length (mat_to_cols_list B)) (mat_to_cols_list B)

goal (1 subgoal):
 1. (A \<Otimes> B) $$ (i, j) = mat_to_cols_list A ! (j div length (mat_to_cols_list B)) ! (i div mult.row_length (mat_to_cols_list B)) * mat_to_cols_list B ! (j mod length (mat_to_cols_list B)) ! (i mod mult.row_length (mat_to_cols_list B))
[PROOF STEP]
using mult.matrix_Tensor_elements[of "1" "(*)"]
[PROOF STATE]
proof (prove)
using this:
(A \<Otimes> B) $$ (i, j) = mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) ! j ! i
i < mult.row_length (mat_to_cols_list A) * mult.row_length (mat_to_cols_list B)
j < length (mat_to_cols_list A) * length (mat_to_cols_list B)
Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (length (mat_to_cols_list A)) (mat_to_cols_list A)
Matrix_Legacy.mat (mult.row_length (mat_to_cols_list B)) (length (mat_to_cols_list B)) (mat_to_cols_list B)
Matrix_Tensor.mult (1::?'a1) (*) \<Longrightarrow> \<forall>i j. (i < mult.row_length ?M1.0 * mult.row_length ?M2.0 \<and> j < length ?M1.0 * length ?M2.0) \<and> Matrix_Legacy.mat (mult.row_length ?M1.0) (length ?M1.0) ?M1.0 \<and> Matrix_Legacy.mat (mult.row_length ?M2.0) (length ?M2.0) ?M2.0 \<longrightarrow> mult.Tensor (*) ?M1.0 ?M2.0 ! j ! i = ?M1.0 ! (j div length ?M2.0) ! (i div mult.row_length ?M2.0) * ?M2.0 ! (j mod length ?M2.0) ! (i mod mult.row_length ?M2.0)

goal (1 subgoal):
 1. (A \<Otimes> B) $$ (i, j) = mat_to_cols_list A ! (j div length (mat_to_cols_list B)) ! (i div mult.row_length (mat_to_cols_list B)) * mat_to_cols_list B ! (j mod length (mat_to_cols_list B)) ! (i mod mult.row_length (mat_to_cols_list B))
[PROOF STEP]
by(simp add: \<open>\<And>M2 M1. mult 1 (*) \<Longrightarrow> \<forall>i j. (i<mult.row_length M1 * mult.row_length M2
    \<and> j<length M1 * length M2) \<and> mat (mult.row_length M1) (length M1) M1 \<and> mat (mult.row_length M2) (length M2) M2 \<longrightarrow>
    mult.Tensor (*) M1 M2 ! j ! i = M1 ! (j div length M2) ! (i div mult.row_length M2) * M2 ! (j mod length M2) ! (i mod mult.row_length M2)\<close>  mult.intro)
[PROOF STATE]
proof (state)
this:
(A \<Otimes> B) $$ (i, j) = mat_to_cols_list A ! (j div length (mat_to_cols_list B)) ! (i div mult.row_length (mat_to_cols_list B)) * mat_to_cols_list B ! (j mod length (mat_to_cols_list B)) ! (i mod mult.row_length (mat_to_cols_list B))

goal (1 subgoal):
 1. (A \<Otimes> B) $$ (i, j) = A $$ (i div rB, j div cB) * B $$ (i mod rB, j mod cB)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(A \<Otimes> B) $$ (i, j) = mat_to_cols_list A ! (j div length (mat_to_cols_list B)) ! (i div mult.row_length (mat_to_cols_list B)) * mat_to_cols_list B ! (j mod length (mat_to_cols_list B)) ! (i mod mult.row_length (mat_to_cols_list B))

goal (1 subgoal):
 1. (A \<Otimes> B) $$ (i, j) = A $$ (i div rB, j div cB) * B $$ (i mod rB, j mod cB)
[PROOF STEP]
using mat_to_cols_list_def
[PROOF STATE]
proof (prove)
using this:
(A \<Otimes> B) $$ (i, j) = mat_to_cols_list A ! (j div length (mat_to_cols_list B)) ! (i div mult.row_length (mat_to_cols_list B)) * mat_to_cols_list B ! (j mod length (mat_to_cols_list B)) ! (i mod mult.row_length (mat_to_cols_list B))
mat_to_cols_list ?A = map (\<lambda>j. map (\<lambda>i. ?A $$ (i, j)) [0..<dim_row ?A]) [0..<dim_col ?A]

goal (1 subgoal):
 1. (A \<Otimes> B) $$ (i, j) = A $$ (i div rB, j div cB) * B $$ (i mod rB, j mod cB)
[PROOF STEP]
by (metis a2 a3 a4 a6 f index_mat_of_cols_list length_mat_to_cols_list less_mult_imp_div_less
less_nat_zero_code mat_to_cols_list_to_mat mult_0_right neq0_conv row_length_mat_to_cols_list
unique_euclidean_semiring_numeral_class.pos_mod_bound)
[PROOF STATE]
proof (state)
this:
(A \<Otimes> B) $$ (i, j) = A $$ (i div rB, j div cB) * B $$ (i mod rB, j mod cB)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Matrix_row_is_Legacy_row:
  assumes "i < dim_row A"
  shows "Matrix.row A i = vec_of_list (row (mat_to_cols_list A) i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix.row A i = vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ia. ia < dim_vec (vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i)) \<Longrightarrow> Matrix.row A i $ ia = vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i) $ ia
 2. dim_vec (Matrix.row A i) = dim_vec (vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i))
[PROOF STEP]
show "dim_vec (Matrix.row A i) = dim_vec (vec_of_list (row (mat_to_cols_list A) i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (Matrix.row A i) = dim_vec (vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i))
[PROOF STEP]
using length_mat_to_cols_list Matrix.dim_vec_of_list
[PROOF STATE]
proof (prove)
using this:
length (mat_to_cols_list ?A) = dim_col ?A
dim_vec (vec_of_list ?as) = length ?as

goal (1 subgoal):
 1. dim_vec (Matrix.row A i) = dim_vec (vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i))
[PROOF STEP]
by (metis row_def index_row(2) length_map)
[PROOF STATE]
proof (state)
this:
dim_vec (Matrix.row A i) = dim_vec (vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i))

goal (1 subgoal):
 1. \<And>ia. ia < dim_vec (vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i)) \<Longrightarrow> Matrix.row A i $ ia = vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i) $ ia
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ia. ia < dim_vec (vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i)) \<Longrightarrow> Matrix.row A i $ ia = vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i) $ ia
[PROOF STEP]
show "\<And>j. j<dim_vec (vec_of_list (row (mat_to_cols_list A) i)) \<Longrightarrow>
              Matrix.row A i $ j = vec_of_list (row (mat_to_cols_list A) i) $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. j < dim_vec (vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i)) \<Longrightarrow> Matrix.row A i $ j = vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i) $ j
[PROOF STEP]
using Matrix.row_def vec_of_list_def mat_to_cols_list_def
[PROOF STATE]
proof (prove)
using this:
Matrix.row ?A ?i = Matrix.vec (dim_col ?A) (\<lambda>j. ?A $$ (?i, j))
vec_of_list \<equiv> map_fun id Abs_vec (\<lambda>v. (length v, mk_vec (length v) ((!) v)))
mat_to_cols_list ?A = map (\<lambda>j. map (\<lambda>i. ?A $$ (i, j)) [0..<dim_row ?A]) [0..<dim_col ?A]

goal (1 subgoal):
 1. \<And>j. j < dim_vec (vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i)) \<Longrightarrow> Matrix.row A i $ j = vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i) $ j
[PROOF STEP]
by(smt row_def assms dim_vec_of_list index_mat_of_cols_list index_row(1)
length_mat_to_cols_list length_row_mat_to_cols_list mat_to_cols_list_to_mat nth_map vec_of_list_index)
[PROOF STATE]
proof (state)
this:
?j < dim_vec (vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i)) \<Longrightarrow> Matrix.row A i $ ?j = vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i) $ ?j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Legacy_row_is_Matrix_row:
  assumes "i < mult.row_length A"
  shows "row A i = list_of_vec (Matrix.row (mat_of_cols_list (mult.row_length A) A) i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix_Legacy.row A i = list_of_vec (Matrix.row (Tensor.mat_of_cols_list (mult.row_length A) A) i)
[PROOF STEP]
proof (rule nth_equalityI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length (Matrix_Legacy.row A i) = length (list_of_vec (Matrix.row (Tensor.mat_of_cols_list (mult.row_length A) A) i))
 2. \<And>ia. ia < length (Matrix_Legacy.row A i) \<Longrightarrow> Matrix_Legacy.row A i ! ia = list_of_vec (Matrix.row (Tensor.mat_of_cols_list (mult.row_length A) A) i) ! ia
[PROOF STEP]
show "length (row A i) = length (list_of_vec (Matrix.row (mat_of_cols_list (mult.row_length A) A) i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (Matrix_Legacy.row A i) = length (list_of_vec (Matrix.row (Tensor.mat_of_cols_list (mult.row_length A) A) i))
[PROOF STEP]
using row_def length_list_of_vec
[PROOF STATE]
proof (prove)
using this:
Matrix_Legacy.row ?m ?i \<equiv> map (\<lambda>w. w ! ?i) ?m
length (list_of_vec ?v) = dim_vec ?v

goal (1 subgoal):
 1. length (Matrix_Legacy.row A i) = length (list_of_vec (Matrix.row (Tensor.mat_of_cols_list (mult.row_length A) A) i))
[PROOF STEP]
by(metis mat_of_cols_list_def dim_col_mat(1) index_row(2) length_map)
[PROOF STATE]
proof (state)
this:
length (Matrix_Legacy.row A i) = length (list_of_vec (Matrix.row (Tensor.mat_of_cols_list (mult.row_length A) A) i))

goal (1 subgoal):
 1. \<And>ia. ia < length (Matrix_Legacy.row A i) \<Longrightarrow> Matrix_Legacy.row A i ! ia = list_of_vec (Matrix.row (Tensor.mat_of_cols_list (mult.row_length A) A) i) ! ia
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ia. ia < length (Matrix_Legacy.row A i) \<Longrightarrow> Matrix_Legacy.row A i ! ia = list_of_vec (Matrix.row (Tensor.mat_of_cols_list (mult.row_length A) A) i) ! ia
[PROOF STEP]
fix j:: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ia. ia < length (Matrix_Legacy.row A i) \<Longrightarrow> Matrix_Legacy.row A i ! ia = list_of_vec (Matrix.row (Tensor.mat_of_cols_list (mult.row_length A) A) i) ! ia
[PROOF STEP]
assume "j < length (row A i)"
[PROOF STATE]
proof (state)
this:
j < length (Matrix_Legacy.row A i)

goal (1 subgoal):
 1. \<And>ia. ia < length (Matrix_Legacy.row A i) \<Longrightarrow> Matrix_Legacy.row A i ! ia = list_of_vec (Matrix.row (Tensor.mat_of_cols_list (mult.row_length A) A) i) ! ia
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j < length (Matrix_Legacy.row A i)
[PROOF STEP]
show "row A i ! j = list_of_vec (Matrix.row (mat_of_cols_list (mult.row_length A) A) i) ! j"
[PROOF STATE]
proof (prove)
using this:
j < length (Matrix_Legacy.row A i)

goal (1 subgoal):
 1. Matrix_Legacy.row A i ! j = list_of_vec (Matrix.row (Tensor.mat_of_cols_list (mult.row_length A) A) i) ! j
[PROOF STEP]
using assms index_mat_of_cols_list
[PROOF STATE]
proof (prove)
using this:
j < length (Matrix_Legacy.row A i)
i < mult.row_length A
\<lbrakk>?i < ?nr; ?j < length ?cs\<rbrakk> \<Longrightarrow> Tensor.mat_of_cols_list ?nr ?cs $$ (?i, ?j) = ?cs ! ?j ! ?i

goal (1 subgoal):
 1. Matrix_Legacy.row A i ! j = list_of_vec (Matrix.row (Tensor.mat_of_cols_list (mult.row_length A) A) i) ! j
[PROOF STEP]
by(metis row_def mat_of_cols_list_def dim_col_mat(1) dim_row_mat(1) index_row(1) length_map list_of_vec_index nth_map)
[PROOF STATE]
proof (state)
this:
Matrix_Legacy.row A i ! j = list_of_vec (Matrix.row (Tensor.mat_of_cols_list (mult.row_length A) A) i) ! j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Matrix_col_is_Legacy_col:
  assumes "j < dim_col A"
  shows "Matrix.col A j = vec_of_list (col (mat_to_cols_list A) j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix.col A j = vec_of_list (Matrix_Legacy.col (mat_to_cols_list A) j)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i < dim_vec (vec_of_list (Matrix_Legacy.col (mat_to_cols_list A) j)) \<Longrightarrow> Matrix.col A j $ i = vec_of_list (Matrix_Legacy.col (mat_to_cols_list A) j) $ i
 2. dim_vec (Matrix.col A j) = dim_vec (vec_of_list (Matrix_Legacy.col (mat_to_cols_list A) j))
[PROOF STEP]
show "dim_vec (Matrix.col A j) = dim_vec (vec_of_list (col (mat_to_cols_list A) j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (Matrix.col A j) = dim_vec (vec_of_list (Matrix_Legacy.col (mat_to_cols_list A) j))
[PROOF STEP]
by (simp add: col_def assms mat_to_cols_list_def)
[PROOF STATE]
proof (state)
this:
dim_vec (Matrix.col A j) = dim_vec (vec_of_list (Matrix_Legacy.col (mat_to_cols_list A) j))

goal (1 subgoal):
 1. \<And>i. i < dim_vec (vec_of_list (Matrix_Legacy.col (mat_to_cols_list A) j)) \<Longrightarrow> Matrix.col A j $ i = vec_of_list (Matrix_Legacy.col (mat_to_cols_list A) j) $ i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < dim_vec (vec_of_list (Matrix_Legacy.col (mat_to_cols_list A) j)) \<Longrightarrow> Matrix.col A j $ i = vec_of_list (Matrix_Legacy.col (mat_to_cols_list A) j) $ i
[PROOF STEP]
show "\<And>i. i < dim_vec (vec_of_list (col (mat_to_cols_list A) j)) \<Longrightarrow>
         Matrix.col A j $ i = vec_of_list (col (mat_to_cols_list A) j) $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < dim_vec (vec_of_list (Matrix_Legacy.col (mat_to_cols_list A) j)) \<Longrightarrow> Matrix.col A j $ i = vec_of_list (Matrix_Legacy.col (mat_to_cols_list A) j) $ i
[PROOF STEP]
using mat_to_cols_list_def
[PROOF STATE]
proof (prove)
using this:
mat_to_cols_list ?A = map (\<lambda>j. map (\<lambda>i. ?A $$ (i, j)) [0..<dim_row ?A]) [0..<dim_col ?A]

goal (1 subgoal):
 1. \<And>i. i < dim_vec (vec_of_list (Matrix_Legacy.col (mat_to_cols_list A) j)) \<Longrightarrow> Matrix.col A j $ i = vec_of_list (Matrix_Legacy.col (mat_to_cols_list A) j) $ i
[PROOF STEP]
by (metis col_def assms col_mat_of_cols_list length_col_mat_to_cols_list length_mat_to_cols_list
mat_to_cols_list_to_mat)
[PROOF STATE]
proof (state)
this:
?i < dim_vec (vec_of_list (Matrix_Legacy.col (mat_to_cols_list A) j)) \<Longrightarrow> Matrix.col A j $ ?i = vec_of_list (Matrix_Legacy.col (mat_to_cols_list A) j) $ ?i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Legacy_col_is_Matrix_col:
  assumes a1:"j < length A" and a2:"length (A ! j) = mult.row_length A"
  shows "col A j = list_of_vec (Matrix.col (mat_of_cols_list (mult.row_length A) A) j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix_Legacy.col A j = list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j)
[PROOF STEP]
proof (rule nth_equalityI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length (Matrix_Legacy.col A j) = length (list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j))
 2. \<And>i. i < length (Matrix_Legacy.col A j) \<Longrightarrow> Matrix_Legacy.col A j ! i = list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j) ! i
[PROOF STEP]
have "length (list_of_vec (Matrix.col (mat_of_cols_list (mult.row_length A) A) j)) =
dim_vec (Matrix.col (mat_of_cols_list (mult.row_length A) A) j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j)) = dim_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j)
[PROOF STEP]
using length_list_of_vec
[PROOF STATE]
proof (prove)
using this:
length (list_of_vec ?v) = dim_vec ?v

goal (1 subgoal):
 1. length (list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j)) = dim_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
length (list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j)) = dim_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j)

goal (2 subgoals):
 1. length (Matrix_Legacy.col A j) = length (list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j))
 2. \<And>i. i < length (Matrix_Legacy.col A j) \<Longrightarrow> Matrix_Legacy.col A j ! i = list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j) ! i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j)) = dim_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j)

goal (2 subgoals):
 1. length (Matrix_Legacy.col A j) = length (list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j))
 2. \<And>i. i < length (Matrix_Legacy.col A j) \<Longrightarrow> Matrix_Legacy.col A j ! i = list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j) ! i
[PROOF STEP]
have "\<dots> = dim_row (mat_of_cols_list (mult.row_length A) A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j) = dim_row (Tensor.mat_of_cols_list (mult.row_length A) A)
[PROOF STEP]
using Matrix.col_def
[PROOF STATE]
proof (prove)
using this:
Matrix.col ?A ?j = Matrix.vec (dim_row ?A) (\<lambda>i. ?A $$ (i, ?j))

goal (1 subgoal):
 1. dim_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j) = dim_row (Tensor.mat_of_cols_list (mult.row_length A) A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j) = dim_row (Tensor.mat_of_cols_list (mult.row_length A) A)

goal (2 subgoals):
 1. length (Matrix_Legacy.col A j) = length (list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j))
 2. \<And>i. i < length (Matrix_Legacy.col A j) \<Longrightarrow> Matrix_Legacy.col A j ! i = list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j) ! i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dim_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j) = dim_row (Tensor.mat_of_cols_list (mult.row_length A) A)

goal (2 subgoals):
 1. length (Matrix_Legacy.col A j) = length (list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j))
 2. \<And>i. i < length (Matrix_Legacy.col A j) \<Longrightarrow> Matrix_Legacy.col A j ! i = list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j) ! i
[PROOF STEP]
have f1:"\<dots> = mult.row_length A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (Tensor.mat_of_cols_list (mult.row_length A) A) = mult.row_length A
[PROOF STEP]
by (simp add: mat_of_cols_list_def)
[PROOF STATE]
proof (state)
this:
dim_row (Tensor.mat_of_cols_list (mult.row_length A) A) = mult.row_length A

goal (2 subgoals):
 1. length (Matrix_Legacy.col A j) = length (list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j))
 2. \<And>i. i < length (Matrix_Legacy.col A j) \<Longrightarrow> Matrix_Legacy.col A j ! i = list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j) ! i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
length (list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j)) = mult.row_length A
[PROOF STEP]
show f2:"length (col A j) = length (list_of_vec (Matrix.col (mat_of_cols_list (mult.row_length A) A) j))"
[PROOF STATE]
proof (prove)
using this:
length (list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j)) = mult.row_length A

goal (1 subgoal):
 1. length (Matrix_Legacy.col A j) = length (list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j))
[PROOF STEP]
using a2
[PROOF STATE]
proof (prove)
using this:
length (list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j)) = mult.row_length A
length (A ! j) = mult.row_length A

goal (1 subgoal):
 1. length (Matrix_Legacy.col A j) = length (list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j))
[PROOF STEP]
by (simp add: col_def)
[PROOF STATE]
proof (state)
this:
length (Matrix_Legacy.col A j) = length (list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j))

goal (1 subgoal):
 1. \<And>i. i < length (Matrix_Legacy.col A j) \<Longrightarrow> Matrix_Legacy.col A j ! i = list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j) ! i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < length (Matrix_Legacy.col A j) \<Longrightarrow> Matrix_Legacy.col A j ! i = list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j) ! i
[PROOF STEP]
fix i:: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < length (Matrix_Legacy.col A j) \<Longrightarrow> Matrix_Legacy.col A j ! i = list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j) ! i
[PROOF STEP]
assume "i<length (col A j)"
[PROOF STATE]
proof (state)
this:
i < length (Matrix_Legacy.col A j)

goal (1 subgoal):
 1. \<And>i. i < length (Matrix_Legacy.col A j) \<Longrightarrow> Matrix_Legacy.col A j ! i = list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j) ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length (Matrix_Legacy.col A j)
[PROOF STEP]
show "(col A j) ! i = (list_of_vec (Matrix.col (mat_of_cols_list (mult.row_length A) A) j)) ! i"
[PROOF STATE]
proof (prove)
using this:
i < length (Matrix_Legacy.col A j)

goal (1 subgoal):
 1. Matrix_Legacy.col A j ! i = list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j) ! i
[PROOF STEP]
by (metis col_def a1 a2 col_mat_of_cols_list list_vec)
[PROOF STATE]
proof (state)
this:
Matrix_Legacy.col A j ! i = list_of_vec (Matrix.col (Tensor.mat_of_cols_list (mult.row_length A) A) j) ! i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma scalar_prod_is_Matrix_scalar_prod [simp]:
  fixes u::"complex list" and v::"complex list"
  assumes "length u = length v"
  shows "plus_mult.scalar_product (*) 0 (+) u v = (vec_of_list u) \<bullet> (vec_of_list v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. plus_mult.scalar_product (*) 0 (+) u v = vec_of_list u \<bullet> vec_of_list v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. plus_mult.scalar_product (*) 0 (+) u v = vec_of_list u \<bullet> vec_of_list v
[PROOF STEP]
have f:"(vec_of_list u) \<bullet> (vec_of_list v) = (\<Sum>i=0..<length v. u ! i * v ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_list u \<bullet> vec_of_list v = (\<Sum>i = 0..<length v. u ! i * v ! i)
[PROOF STEP]
using assms scalar_prod_def[of "vec_of_list u" "vec_of_list v"] Matrix.dim_vec_of_list[of v] index_vec_of_list
[PROOF STATE]
proof (prove)
using this:
length u = length v
vec_of_list u \<bullet> vec_of_list v \<equiv> \<Sum>i = 0..<dim_vec (vec_of_list v). vec_of_list u $ i * vec_of_list v $ i
dim_vec (vec_of_list v) = length v
?i < length ?xs \<Longrightarrow> vec_of_list ?xs $ ?i = ?xs ! ?i

goal (1 subgoal):
 1. vec_of_list u \<bullet> vec_of_list v = (\<Sum>i = 0..<length v. u ! i * v ! i)
[PROOF STEP]
by (metis (no_types, lifting) atLeastLessThan_iff sum.cong)
[PROOF STATE]
proof (state)
this:
vec_of_list u \<bullet> vec_of_list v = (\<Sum>i = 0..<length v. u ! i * v ! i)

goal (1 subgoal):
 1. plus_mult.scalar_product (*) 0 (+) u v = vec_of_list u \<bullet> vec_of_list v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
vec_of_list u \<bullet> vec_of_list v = (\<Sum>i = 0..<length v. u ! i * v ! i)

goal (1 subgoal):
 1. plus_mult.scalar_product (*) 0 (+) u v = vec_of_list u \<bullet> vec_of_list v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vec_of_list u \<bullet> vec_of_list v = (\<Sum>i = 0..<length v. u ! i * v ! i) \<Longrightarrow> plus_mult.scalar_product (*) 0 (+) u v = vec_of_list u \<bullet> vec_of_list v
[PROOF STEP]
have "plus_mult.scalar_product (*) 0 (+) u v = semiring_0_class.scalar_prod u v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. plus_mult.scalar_product (*) 0 (+) u v = semiring_0_class.scalar_prod u v
[PROOF STEP]
using  plus_mult.scalar_product_def[of 1 "(*)" 0 "(+)" "a_inv cpx_rng" u v]
[PROOF STATE]
proof (prove)
using this:
plus_mult 1 (*) 0 (+) (a_inv cpx_rng) \<Longrightarrow> plus_mult.scalar_product (*) 0 (+) u v = semiring_0_class.scalar_prod u v

goal (1 subgoal):
 1. plus_mult.scalar_product (*) 0 (+) u v = semiring_0_class.scalar_prod u v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
plus_mult.scalar_product (*) 0 (+) u v = semiring_0_class.scalar_prod u v

goal (1 subgoal):
 1. vec_of_list u \<bullet> vec_of_list v = (\<Sum>i = 0..<length v. u ! i * v ! i) \<Longrightarrow> plus_mult.scalar_product (*) 0 (+) u v = vec_of_list u \<bullet> vec_of_list v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
plus_mult.scalar_product (*) 0 (+) u v = semiring_0_class.scalar_prod u v

goal (1 subgoal):
 1. vec_of_list u \<bullet> vec_of_list v = (\<Sum>i = 0..<length v. u ! i * v ! i) \<Longrightarrow> plus_mult.scalar_product (*) 0 (+) u v = vec_of_list u \<bullet> vec_of_list v
[PROOF STEP]
have "\<dots> = sum_list (map (\<lambda>(x,y). x * y) (zip u v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semiring_0_class.scalar_prod u v = sum_list (map2 (*) u v)
[PROOF STEP]
by (simp add: scalar_prod)
[PROOF STATE]
proof (state)
this:
semiring_0_class.scalar_prod u v = sum_list (map2 (*) u v)

goal (1 subgoal):
 1. vec_of_list u \<bullet> vec_of_list v = (\<Sum>i = 0..<length v. u ! i * v ! i) \<Longrightarrow> plus_mult.scalar_product (*) 0 (+) u v = vec_of_list u \<bullet> vec_of_list v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
semiring_0_class.scalar_prod u v = sum_list (map2 (*) u v)

goal (1 subgoal):
 1. vec_of_list u \<bullet> vec_of_list v = (\<Sum>i = 0..<length v. u ! i * v ! i) \<Longrightarrow> plus_mult.scalar_product (*) 0 (+) u v = vec_of_list u \<bullet> vec_of_list v
[PROOF STEP]
have "\<forall>i<length v. (zip u v) ! i = (u ! i, v ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<length v. zip u v ! i = (u ! i, v ! i)
[PROOF STEP]
using assms zip_def
[PROOF STATE]
proof (prove)
using this:
length u = length v
zip \<equiv> \<lambda>uu uua. rec_list (\<lambda>xs. []) (\<lambda>y ys ysa xs. case xs of [] \<Rightarrow> [] | z # zs \<Rightarrow> (z, y) # ysa zs) uua uu

goal (1 subgoal):
 1. \<forall>i<length v. zip u v ! i = (u ! i, v ! i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>i<length v. zip u v ! i = (u ! i, v ! i)

goal (1 subgoal):
 1. vec_of_list u \<bullet> vec_of_list v = (\<Sum>i = 0..<length v. u ! i * v ! i) \<Longrightarrow> plus_mult.scalar_product (*) 0 (+) u v = vec_of_list u \<bullet> vec_of_list v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length v. zip u v ! i = (u ! i, v ! i)
[PROOF STEP]
have "\<forall>i<length v. (map (\<lambda>(x,y). x * y) (zip u v)) ! i = u ! i * v ! i"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length v. zip u v ! i = (u ! i, v ! i)

goal (1 subgoal):
 1. \<forall>i<length v. map2 (*) u v ! i = u ! i * v ! i
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
this:
\<forall>i<length v. map2 (*) u v ! i = u ! i * v ! i

goal (1 subgoal):
 1. vec_of_list u \<bullet> vec_of_list v = (\<Sum>i = 0..<length v. u ! i * v ! i) \<Longrightarrow> plus_mult.scalar_product (*) 0 (+) u v = vec_of_list u \<bullet> vec_of_list v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
plus_mult.scalar_product (*) 0 (+) u v = semiring_0_class.scalar_prod u v
semiring_0_class.scalar_prod u v = sum_list (map2 (*) u v)
\<forall>i<length v. map2 (*) u v ! i = u ! i * v ! i
[PROOF STEP]
have "plus_mult.scalar_product (*) 0 (+) u v = (\<Sum>i=0..<length v. u ! i * v ! i)"
[PROOF STATE]
proof (prove)
using this:
plus_mult.scalar_product (*) 0 (+) u v = semiring_0_class.scalar_prod u v
semiring_0_class.scalar_prod u v = sum_list (map2 (*) u v)
\<forall>i<length v. map2 (*) u v ! i = u ! i * v ! i

goal (1 subgoal):
 1. plus_mult.scalar_product (*) 0 (+) u v = (\<Sum>i = 0..<length v. u ! i * v ! i)
[PROOF STEP]
by(metis (no_types, lifting) assms atLeastLessThan_iff length_map map_fst_zip sum.cong sum_list_sum_nth)
[PROOF STATE]
proof (state)
this:
plus_mult.scalar_product (*) 0 (+) u v = (\<Sum>i = 0..<length v. u ! i * v ! i)

goal (1 subgoal):
 1. vec_of_list u \<bullet> vec_of_list v = (\<Sum>i = 0..<length v. u ! i * v ! i) \<Longrightarrow> plus_mult.scalar_product (*) 0 (+) u v = vec_of_list u \<bullet> vec_of_list v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
plus_mult.scalar_product (*) 0 (+) u v = (\<Sum>i = 0..<length v. u ! i * v ! i)

goal (1 subgoal):
 1. plus_mult.scalar_product (*) 0 (+) u v = vec_of_list u \<bullet> vec_of_list v
[PROOF STEP]
by (simp add: f)
[PROOF STATE]
proof (state)
this:
plus_mult.scalar_product (*) 0 (+) u v = vec_of_list u \<bullet> vec_of_list v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
plus_mult.scalar_product (*) 0 (+) u v = vec_of_list u \<bullet> vec_of_list v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matrix_mult_to_times_mat:
  assumes "dim_col A > 0" and "dim_col B > 0" and "dim_col (A::complex Matrix.mat) = dim_row B"
  shows "A * B = mat_of_cols_list (dim_row A) (plus_mult.matrix_mult (*) 0 (+) (mat_to_cols_list A) (mat_to_cols_list B))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A * B = Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B))); j < dim_col (Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)))\<rbrakk> \<Longrightarrow> (A * B) $$ (i, j) = Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)) $$ (i, j)
 2. dim_row (A * B) = dim_row (Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)))
 3. dim_col (A * B) = dim_col (Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)))
[PROOF STEP]
define M where "M = mat_of_cols_list (dim_row A) (plus_mult.matrix_mult (*) 0 (+) (mat_to_cols_list A) (mat_to_cols_list B))"
[PROOF STATE]
proof (state)
this:
M = Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B))

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B))); j < dim_col (Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)))\<rbrakk> \<Longrightarrow> (A * B) $$ (i, j) = Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)) $$ (i, j)
 2. dim_row (A * B) = dim_row (Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)))
 3. dim_col (A * B) = dim_col (Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
M = Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B))
[PROOF STEP]
show f1:"dim_row (A * B) = dim_row M"
[PROOF STATE]
proof (prove)
using this:
M = Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B))

goal (1 subgoal):
 1. dim_row (A * B) = dim_row M
[PROOF STEP]
by (simp add: mat_of_cols_list_def times_mat_def)
[PROOF STATE]
proof (state)
this:
dim_row (A * B) = dim_row M

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B))); j < dim_col (Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)))\<rbrakk> \<Longrightarrow> (A * B) $$ (i, j) = Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)) $$ (i, j)
 2. dim_col (A * B) = dim_col (Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)))
[PROOF STEP]
have "length (plus_mult.matrix_mult (*) 0 (+) (mat_to_cols_list A) (mat_to_cols_list B)) = dim_col B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)) = dim_col B
[PROOF STEP]
by (simp add: mat_multI_def)
[PROOF STATE]
proof (state)
this:
length (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)) = dim_col B

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B))); j < dim_col (Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)))\<rbrakk> \<Longrightarrow> (A * B) $$ (i, j) = Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)) $$ (i, j)
 2. dim_col (A * B) = dim_col (Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)) = dim_col B
[PROOF STEP]
show f2:"dim_col (A * B) = dim_col M"
[PROOF STATE]
proof (prove)
using this:
length (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)) = dim_col B

goal (1 subgoal):
 1. dim_col (A * B) = dim_col M
[PROOF STEP]
by (simp add: M_def times_mat_def mat_of_cols_list_def)
[PROOF STATE]
proof (state)
this:
dim_col (A * B) = dim_col M

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B))); j < dim_col (Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)))\<rbrakk> \<Longrightarrow> (A * B) $$ (i, j) = Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)) $$ (i, j)
[PROOF STEP]
show "\<And>i j. i < dim_row M \<Longrightarrow> j < dim_col M \<Longrightarrow> (A * B) $$ (i, j) = M $$ (i, j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row M; j < dim_col M\<rbrakk> \<Longrightarrow> (A * B) $$ (i, j) = M $$ (i, j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row M; j < dim_col M\<rbrakk> \<Longrightarrow> (A * B) $$ (i, j) = M $$ (i, j)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row M; j < dim_col M\<rbrakk> \<Longrightarrow> (A * B) $$ (i, j) = M $$ (i, j)
[PROOF STEP]
assume a1:"i < dim_row M" and a2:"j < dim_col M"
[PROOF STATE]
proof (state)
this:
i < dim_row M
j < dim_col M

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row M; j < dim_col M\<rbrakk> \<Longrightarrow> (A * B) $$ (i, j) = M $$ (i, j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < dim_row M
j < dim_col M
[PROOF STEP]
have "(A * B) $$ (i,j) = Matrix.row A i \<bullet> Matrix.col B j"
[PROOF STATE]
proof (prove)
using this:
i < dim_row M
j < dim_col M

goal (1 subgoal):
 1. (A * B) $$ (i, j) = Matrix.row A i \<bullet> Matrix.col B j
[PROOF STEP]
using f1 f2
[PROOF STATE]
proof (prove)
using this:
i < dim_row M
j < dim_col M
dim_row (A * B) = dim_row M
dim_col (A * B) = dim_col M

goal (1 subgoal):
 1. (A * B) $$ (i, j) = Matrix.row A i \<bullet> Matrix.col B j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(A * B) $$ (i, j) = Matrix.row A i \<bullet> Matrix.col B j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row M; j < dim_col M\<rbrakk> \<Longrightarrow> (A * B) $$ (i, j) = M $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(A * B) $$ (i, j) = Matrix.row A i \<bullet> Matrix.col B j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row M; j < dim_col M\<rbrakk> \<Longrightarrow> (A * B) $$ (i, j) = M $$ (i, j)
[PROOF STEP]
have "\<dots> = vec_of_list (row (mat_to_cols_list A) i) \<bullet> vec_of_list (col (mat_to_cols_list B) j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix.row A i \<bullet> Matrix.col B j = vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i) \<bullet> vec_of_list (Matrix_Legacy.col (mat_to_cols_list B) j)
[PROOF STEP]
using f1 f2 a1 a2
[PROOF STATE]
proof (prove)
using this:
dim_row (A * B) = dim_row M
dim_col (A * B) = dim_col M
i < dim_row M
j < dim_col M

goal (1 subgoal):
 1. Matrix.row A i \<bullet> Matrix.col B j = vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i) \<bullet> vec_of_list (Matrix_Legacy.col (mat_to_cols_list B) j)
[PROOF STEP]
by (simp add: Matrix_row_is_Legacy_row Matrix_col_is_Legacy_col)
[PROOF STATE]
proof (state)
this:
Matrix.row A i \<bullet> Matrix.col B j = vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i) \<bullet> vec_of_list (Matrix_Legacy.col (mat_to_cols_list B) j)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row M; j < dim_col M\<rbrakk> \<Longrightarrow> (A * B) $$ (i, j) = M $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Matrix.row A i \<bullet> Matrix.col B j = vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i) \<bullet> vec_of_list (Matrix_Legacy.col (mat_to_cols_list B) j)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row M; j < dim_col M\<rbrakk> \<Longrightarrow> (A * B) $$ (i, j) = M $$ (i, j)
[PROOF STEP]
have "\<dots> = plus_mult.scalar_product (*) 0 (+) (row (mat_to_cols_list A) i) (col (mat_to_cols_list B) j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i) \<bullet> vec_of_list (Matrix_Legacy.col (mat_to_cols_list B) j) = plus_mult.scalar_product (*) 0 (+) (Matrix_Legacy.row (mat_to_cols_list A) i) (Matrix_Legacy.col (mat_to_cols_list B) j)
[PROOF STEP]
using a1 a2 assms(3) f1 f2
[PROOF STATE]
proof (prove)
using this:
i < dim_row M
j < dim_col M
dim_col A = dim_row B
dim_row (A * B) = dim_row M
dim_col (A * B) = dim_col M

goal (1 subgoal):
 1. vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i) \<bullet> vec_of_list (Matrix_Legacy.col (mat_to_cols_list B) j) = plus_mult.scalar_product (*) 0 (+) (Matrix_Legacy.row (mat_to_cols_list A) i) (Matrix_Legacy.col (mat_to_cols_list B) j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i) \<bullet> vec_of_list (Matrix_Legacy.col (mat_to_cols_list B) j) = plus_mult.scalar_product (*) 0 (+) (Matrix_Legacy.row (mat_to_cols_list A) i) (Matrix_Legacy.col (mat_to_cols_list B) j)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row M; j < dim_col M\<rbrakk> \<Longrightarrow> (A * B) $$ (i, j) = M $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i) \<bullet> vec_of_list (Matrix_Legacy.col (mat_to_cols_list B) j) = plus_mult.scalar_product (*) 0 (+) (Matrix_Legacy.row (mat_to_cols_list A) i) (Matrix_Legacy.col (mat_to_cols_list B) j)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row M; j < dim_col M\<rbrakk> \<Longrightarrow> (A * B) $$ (i, j) = M $$ (i, j)
[PROOF STEP]
have "M $$ (i,j) =  plus_mult.scalar_product (*) 0 (+) (row (mat_to_cols_list A) i) (col (mat_to_cols_list B) j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M $$ (i, j) = plus_mult.scalar_product (*) 0 (+) (Matrix_Legacy.row (mat_to_cols_list A) i) (Matrix_Legacy.col (mat_to_cols_list B) j)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. M $$ (i, j) = plus_mult.scalar_product (*) 0 (+) (Matrix_Legacy.row (mat_to_cols_list A) i) (Matrix_Legacy.col (mat_to_cols_list B) j)
[PROOF STEP]
have "M $$ (i,j) = (plus_mult.matrix_mult (*) 0 (+) (mat_to_cols_list A) (mat_to_cols_list B)) ! j ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M $$ (i, j) = mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B) ! j ! i
[PROOF STEP]
using M_def f1 f2
\<open>length (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)) = dim_col B\<close> a1 a2
[PROOF STATE]
proof (prove)
using this:
M = Tensor.mat_of_cols_list (dim_row A) (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B))
dim_row (A * B) = dim_row M
dim_col (A * B) = dim_col M
length (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)) = dim_col B
i < dim_row M
j < dim_col M

goal (1 subgoal):
 1. M $$ (i, j) = mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B) ! j ! i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
M $$ (i, j) = mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B) ! j ! i

goal (1 subgoal):
 1. M $$ (i, j) = plus_mult.scalar_product (*) 0 (+) (Matrix_Legacy.row (mat_to_cols_list A) i) (Matrix_Legacy.col (mat_to_cols_list B) j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
M $$ (i, j) = mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B) ! j ! i

goal (1 subgoal):
 1. M $$ (i, j) = plus_mult.scalar_product (*) 0 (+) (Matrix_Legacy.row (mat_to_cols_list A) i) (Matrix_Legacy.col (mat_to_cols_list B) j)
[PROOF STEP]
have "mat (mult.row_length (mat_to_cols_list A)) (dim_col A) (mat_to_cols_list A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (dim_col A) (mat_to_cols_list A)
[PROOF STEP]
using mat_to_cols_list_is_mat assms(1)
[PROOF STATE]
proof (prove)
using this:
0 < dim_col ?A \<Longrightarrow> Matrix_Legacy.mat (mult.row_length (mat_to_cols_list ?A)) (length (mat_to_cols_list ?A)) (mat_to_cols_list ?A)
0 < dim_col A

goal (1 subgoal):
 1. Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (dim_col A) (mat_to_cols_list A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (dim_col A) (mat_to_cols_list A)

goal (1 subgoal):
 1. M $$ (i, j) = plus_mult.scalar_product (*) 0 (+) (Matrix_Legacy.row (mat_to_cols_list A) i) (Matrix_Legacy.col (mat_to_cols_list B) j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (dim_col A) (mat_to_cols_list A)

goal (1 subgoal):
 1. M $$ (i, j) = plus_mult.scalar_product (*) 0 (+) (Matrix_Legacy.row (mat_to_cols_list A) i) (Matrix_Legacy.col (mat_to_cols_list B) j)
[PROOF STEP]
have "mat (dim_col A) (dim_col B) (mat_to_cols_list B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix_Legacy.mat (dim_col A) (dim_col B) (mat_to_cols_list B)
[PROOF STEP]
using assms(2) assms(3) mat_to_cols_list_is_mat
[PROOF STATE]
proof (prove)
using this:
0 < dim_col B
dim_col A = dim_row B
0 < dim_col ?A \<Longrightarrow> Matrix_Legacy.mat (mult.row_length (mat_to_cols_list ?A)) (length (mat_to_cols_list ?A)) (mat_to_cols_list ?A)

goal (1 subgoal):
 1. Matrix_Legacy.mat (dim_col A) (dim_col B) (mat_to_cols_list B)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Matrix_Legacy.mat (dim_col A) (dim_col B) (mat_to_cols_list B)

goal (1 subgoal):
 1. M $$ (i, j) = plus_mult.scalar_product (*) 0 (+) (Matrix_Legacy.row (mat_to_cols_list A) i) (Matrix_Legacy.col (mat_to_cols_list B) j)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
M $$ (i, j) = mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B) ! j ! i
Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (dim_col A) (mat_to_cols_list A)
Matrix_Legacy.mat (dim_col A) (dim_col B) (mat_to_cols_list B)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
M $$ (i, j) = mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B) ! j ! i
Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (dim_col A) (mat_to_cols_list A)
Matrix_Legacy.mat (dim_col A) (dim_col B) (mat_to_cols_list B)

goal (1 subgoal):
 1. M $$ (i, j) = plus_mult.scalar_product (*) 0 (+) (Matrix_Legacy.row (mat_to_cols_list A) i) (Matrix_Legacy.col (mat_to_cols_list B) j)
[PROOF STEP]
using assms(1) a1 a2 row_length_mat_to_cols_list plus_mult.matrix_index[of 1 "(*)" 0 "(+)"] plus_mult_cpx
[PROOF STATE]
proof (prove)
using this:
M $$ (i, j) = mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B) ! j ! i
Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (dim_col A) (mat_to_cols_list A)
Matrix_Legacy.mat (dim_col A) (dim_col B) (mat_to_cols_list B)
0 < dim_col A
i < dim_row M
j < dim_col M
0 < dim_col ?A \<Longrightarrow> mult.row_length (mat_to_cols_list ?A) = dim_row ?A
\<lbrakk>plus_mult (1::?'a1) (*) (0::?'a1) (+) ?inver; Matrix_Legacy.mat (mult.row_length ?m1.0) ?n ?m1.0; Matrix_Legacy.mat ?n ?nc ?m2.0; ?i < mult.row_length ?m1.0; ?j < ?nc\<rbrakk> \<Longrightarrow> mat_multI (0::?'a1) (+) (*) (mult.row_length ?m1.0) ?m1.0 ?m2.0 ! ?j ! ?i = plus_mult.scalar_product (*) (0::?'a1) (+) (Matrix_Legacy.row ?m1.0 ?i) (Matrix_Legacy.col ?m2.0 ?j)
plus_mult 1 (*) 0 (+) (a_inv cpx_rng)

goal (1 subgoal):
 1. M $$ (i, j) = plus_mult.scalar_product (*) 0 (+) (Matrix_Legacy.row (mat_to_cols_list A) i) (Matrix_Legacy.col (mat_to_cols_list B) j)
[PROOF STEP]
by (smt f1 f2 index_mult_mat(2) index_mult_mat(3))
[PROOF STATE]
proof (state)
this:
M $$ (i, j) = plus_mult.scalar_product (*) 0 (+) (Matrix_Legacy.row (mat_to_cols_list A) i) (Matrix_Legacy.col (mat_to_cols_list B) j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
M $$ (i, j) = plus_mult.scalar_product (*) 0 (+) (Matrix_Legacy.row (mat_to_cols_list A) i) (Matrix_Legacy.col (mat_to_cols_list B) j)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row M; j < dim_col M\<rbrakk> \<Longrightarrow> (A * B) $$ (i, j) = M $$ (i, j)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
M $$ (i, j) = (A * B) $$ (i, j)
[PROOF STEP]
show "(A * B) $$ (i, j) = M $$ (i, j)"
[PROOF STATE]
proof (prove)
using this:
M $$ (i, j) = (A * B) $$ (i, j)

goal (1 subgoal):
 1. (A * B) $$ (i, j) = M $$ (i, j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(A * B) $$ (i, j) = M $$ (i, j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i < dim_row M; ?j < dim_col M\<rbrakk> \<Longrightarrow> (A * B) $$ (?i, ?j) = M $$ (?i, ?j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mat_to_cols_list_times_mat [simp]:
  assumes "dim_col A = dim_row B" and "dim_col A > 0"
  shows "mat_to_cols_list (A * B) = plus_mult.matrix_mult (*) 0 (+) (mat_to_cols_list A) (mat_to_cols_list B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_to_cols_list (A * B) = mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)
[PROOF STEP]
proof (rule nth_equalityI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length (mat_to_cols_list (A * B)) = length (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B))
 2. \<And>i. i < length (mat_to_cols_list (A * B)) \<Longrightarrow> mat_to_cols_list (A * B) ! i = mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B) ! i
[PROOF STEP]
define M where "M = plus_mult.matrix_mult (*) 0 (+) (mat_to_cols_list A) (mat_to_cols_list B)"
[PROOF STATE]
proof (state)
this:
M = mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)

goal (2 subgoals):
 1. length (mat_to_cols_list (A * B)) = length (mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B))
 2. \<And>i. i < length (mat_to_cols_list (A * B)) \<Longrightarrow> mat_to_cols_list (A * B) ! i = mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B) ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
M = mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)
[PROOF STEP]
show f0:"length (mat_to_cols_list (A * B)) = length M"
[PROOF STATE]
proof (prove)
using this:
M = mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)

goal (1 subgoal):
 1. length (mat_to_cols_list (A * B)) = length M
[PROOF STEP]
by (simp add: mat_multI_def)
[PROOF STATE]
proof (state)
this:
length (mat_to_cols_list (A * B)) = length M

goal (1 subgoal):
 1. \<And>i. i < length (mat_to_cols_list (A * B)) \<Longrightarrow> mat_to_cols_list (A * B) ! i = mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B) ! i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length (mat_to_cols_list (A * B)) = length M

goal (1 subgoal):
 1. \<And>i. i < length (mat_to_cols_list (A * B)) \<Longrightarrow> mat_to_cols_list (A * B) ! i = mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B) ! i
[PROOF STEP]
have f1:"\<And>j. j<length (mat_to_cols_list (A * B)) \<longrightarrow> mat_to_cols_list (A * B) ! j = M ! j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. j < length (mat_to_cols_list (A * B)) \<longrightarrow> mat_to_cols_list (A * B) ! j = M ! j
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. j < length (mat_to_cols_list (A * B)) \<Longrightarrow> mat_to_cols_list (A * B) ! j = M ! j
[PROOF STEP]
fix j:: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. j < length (mat_to_cols_list (A * B)) \<Longrightarrow> mat_to_cols_list (A * B) ! j = M ! j
[PROOF STEP]
assume a0:"j < length (mat_to_cols_list (A * B))"
[PROOF STATE]
proof (state)
this:
j < length (mat_to_cols_list (A * B))

goal (1 subgoal):
 1. \<And>j. j < length (mat_to_cols_list (A * B)) \<Longrightarrow> mat_to_cols_list (A * B) ! j = M ! j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j < length (mat_to_cols_list (A * B))
[PROOF STEP]
have "length (mat_to_cols_list (A * B) ! j) = dim_row A"
[PROOF STATE]
proof (prove)
using this:
j < length (mat_to_cols_list (A * B))

goal (1 subgoal):
 1. length (mat_to_cols_list (A * B) ! j) = dim_row A
[PROOF STEP]
by (simp add: mat_to_cols_list_def)
[PROOF STATE]
proof (state)
this:
length (mat_to_cols_list (A * B) ! j) = dim_row A

goal (1 subgoal):
 1. \<And>j. j < length (mat_to_cols_list (A * B)) \<Longrightarrow> mat_to_cols_list (A * B) ! j = M ! j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (mat_to_cols_list (A * B) ! j) = dim_row A
[PROOF STEP]
also
[PROOF STATE]
proof (chain)
picking this:
length (mat_to_cols_list (A * B) ! j) = dim_row A
[PROOF STEP]
have f2:"length (M ! j) = dim_row A"
[PROOF STATE]
proof (prove)
using this:
length (mat_to_cols_list (A * B) ! j) = dim_row A

goal (1 subgoal):
 1. length (M ! j) = dim_row A
[PROOF STEP]
using a0 M_def mat_multI_def[of 0 "(+)" "(*)" "dim_row A" "mat_to_cols_list A" "mat_to_cols_list B"]
        row_length_mat_to_cols_list assms(2)
[PROOF STATE]
proof (prove)
using this:
length (mat_to_cols_list (A * B) ! j) = dim_row A
j < length (mat_to_cols_list (A * B))
M = mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)
mat_mult (dim_row A) (mat_to_cols_list A) (mat_to_cols_list B) \<equiv> map (matT_vec_multI 0 (+) (*) (Matrix_Legacy.transpose (dim_row A) (mat_to_cols_list A))) (mat_to_cols_list B)
0 < dim_col ?A \<Longrightarrow> mult.row_length (mat_to_cols_list ?A) = dim_row ?A
0 < dim_col A

goal (1 subgoal):
 1. length (M ! j) = dim_row A
[PROOF STEP]
by (metis assms(1) f0 length_greater_0_conv length_map length_mat_to_cols_list
list_to_mat_to_cols_list mat_mult mat_to_cols_list_is_mat matrix_mult_to_times_mat)
[PROOF STATE]
proof (state)
this:
length (M ! j) = dim_row A

goal (1 subgoal):
 1. \<And>j. j < length (mat_to_cols_list (A * B)) \<Longrightarrow> mat_to_cols_list (A * B) ! j = M ! j
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length (mat_to_cols_list (A * B) ! j) = dim_row A
length (M ! j) = dim_row A
[PROOF STEP]
have "length (mat_to_cols_list (A * B) ! j) = length (M ! j)"
[PROOF STATE]
proof (prove)
using this:
length (mat_to_cols_list (A * B) ! j) = dim_row A
length (M ! j) = dim_row A

goal (1 subgoal):
 1. length (mat_to_cols_list (A * B) ! j) = length (M ! j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (mat_to_cols_list (A * B) ! j) = length (M ! j)

goal (1 subgoal):
 1. \<And>j. j < length (mat_to_cols_list (A * B)) \<Longrightarrow> mat_to_cols_list (A * B) ! j = M ! j
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length (mat_to_cols_list (A * B) ! j) = length (M ! j)

goal (1 subgoal):
 1. \<And>j. j < length (mat_to_cols_list (A * B)) \<Longrightarrow> mat_to_cols_list (A * B) ! j = M ! j
[PROOF STEP]
have "\<And>i. i<dim_row A \<longrightarrow> mat_to_cols_list (A * B) ! j ! i = M ! j ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < dim_row A \<longrightarrow> mat_to_cols_list (A * B) ! j ! i = M ! j ! i
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < dim_row A \<Longrightarrow> mat_to_cols_list (A * B) ! j ! i = M ! j ! i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < dim_row A \<Longrightarrow> mat_to_cols_list (A * B) ! j ! i = M ! j ! i
[PROOF STEP]
assume a1:"i < dim_row A"
[PROOF STATE]
proof (state)
this:
i < dim_row A

goal (1 subgoal):
 1. \<And>i. i < dim_row A \<Longrightarrow> mat_to_cols_list (A * B) ! j ! i = M ! j ! i
[PROOF STEP]
have "mat (mult.row_length (mat_to_cols_list A)) (dim_col A) (mat_to_cols_list A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (dim_col A) (mat_to_cols_list A)
[PROOF STEP]
using mat_to_cols_list_is_mat assms(2)
[PROOF STATE]
proof (prove)
using this:
0 < dim_col ?A \<Longrightarrow> Matrix_Legacy.mat (mult.row_length (mat_to_cols_list ?A)) (length (mat_to_cols_list ?A)) (mat_to_cols_list ?A)
0 < dim_col A

goal (1 subgoal):
 1. Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (dim_col A) (mat_to_cols_list A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (dim_col A) (mat_to_cols_list A)

goal (1 subgoal):
 1. \<And>i. i < dim_row A \<Longrightarrow> mat_to_cols_list (A * B) ! j ! i = M ! j ! i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (dim_col A) (mat_to_cols_list A)

goal (1 subgoal):
 1. \<And>i. i < dim_row A \<Longrightarrow> mat_to_cols_list (A * B) ! j ! i = M ! j ! i
[PROOF STEP]
have "mat (dim_col A) (dim_col B) (mat_to_cols_list B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix_Legacy.mat (dim_col A) (dim_col B) (mat_to_cols_list B)
[PROOF STEP]
using mat_to_cols_list_is_mat assms(1) a0
[PROOF STATE]
proof (prove)
using this:
0 < dim_col ?A \<Longrightarrow> Matrix_Legacy.mat (mult.row_length (mat_to_cols_list ?A)) (length (mat_to_cols_list ?A)) (mat_to_cols_list ?A)
dim_col A = dim_row B
j < length (mat_to_cols_list (A * B))

goal (1 subgoal):
 1. Matrix_Legacy.mat (dim_col A) (dim_col B) (mat_to_cols_list B)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Matrix_Legacy.mat (dim_col A) (dim_col B) (mat_to_cols_list B)

goal (1 subgoal):
 1. \<And>i. i < dim_row A \<Longrightarrow> mat_to_cols_list (A * B) ! j ! i = M ! j ! i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (dim_col A) (mat_to_cols_list A)
Matrix_Legacy.mat (dim_col A) (dim_col B) (mat_to_cols_list B)
[PROOF STEP]
have "M ! j ! i = plus_mult.scalar_product (*) 0 (+) (row (mat_to_cols_list A) i) (col (mat_to_cols_list B) j)"
[PROOF STATE]
proof (prove)
using this:
Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (dim_col A) (mat_to_cols_list A)
Matrix_Legacy.mat (dim_col A) (dim_col B) (mat_to_cols_list B)

goal (1 subgoal):
 1. M ! j ! i = plus_mult.scalar_product (*) 0 (+) (Matrix_Legacy.row (mat_to_cols_list A) i) (Matrix_Legacy.col (mat_to_cols_list B) j)
[PROOF STEP]
using plus_mult.matrix_index a0 a1 row_length_mat_to_cols_list assms(2) plus_mult_cpx M_def
[PROOF STATE]
proof (prove)
using this:
Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (dim_col A) (mat_to_cols_list A)
Matrix_Legacy.mat (dim_col A) (dim_col B) (mat_to_cols_list B)
\<lbrakk>plus_mult ?id ?f ?zer ?g ?inver; Matrix_Legacy.mat (mult.row_length ?m1.0) ?n ?m1.0; Matrix_Legacy.mat ?n ?nc ?m2.0; ?i < mult.row_length ?m1.0; ?j < ?nc\<rbrakk> \<Longrightarrow> mat_multI ?zer ?g ?f (mult.row_length ?m1.0) ?m1.0 ?m2.0 ! ?j ! ?i = plus_mult.scalar_product ?f ?zer ?g (Matrix_Legacy.row ?m1.0 ?i) (Matrix_Legacy.col ?m2.0 ?j)
j < length (mat_to_cols_list (A * B))
i < dim_row A
0 < dim_col ?A \<Longrightarrow> mult.row_length (mat_to_cols_list ?A) = dim_row ?A
0 < dim_col A
plus_mult 1 (*) 0 (+) (a_inv cpx_rng)
M = mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B)

goal (1 subgoal):
 1. M ! j ! i = plus_mult.scalar_product (*) 0 (+) (Matrix_Legacy.row (mat_to_cols_list A) i) (Matrix_Legacy.col (mat_to_cols_list B) j)
[PROOF STEP]
by (metis index_mult_mat(3) length_mat_to_cols_list)
[PROOF STATE]
proof (state)
this:
M ! j ! i = plus_mult.scalar_product (*) 0 (+) (Matrix_Legacy.row (mat_to_cols_list A) i) (Matrix_Legacy.col (mat_to_cols_list B) j)

goal (1 subgoal):
 1. \<And>i. i < dim_row A \<Longrightarrow> mat_to_cols_list (A * B) ! j ! i = M ! j ! i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M ! j ! i = plus_mult.scalar_product (*) 0 (+) (Matrix_Legacy.row (mat_to_cols_list A) i) (Matrix_Legacy.col (mat_to_cols_list B) j)

goal (1 subgoal):
 1. \<And>i. i < dim_row A \<Longrightarrow> mat_to_cols_list (A * B) ! j ! i = M ! j ! i
[PROOF STEP]
have "\<dots> = vec_of_list (row (mat_to_cols_list A) i) \<bullet> vec_of_list (col (mat_to_cols_list B) j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. plus_mult.scalar_product (*) 0 (+) (Matrix_Legacy.row (mat_to_cols_list A) i) (Matrix_Legacy.col (mat_to_cols_list B) j) = vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i) \<bullet> vec_of_list (Matrix_Legacy.col (mat_to_cols_list B) j)
[PROOF STEP]
using a0 a1 assms(1)
[PROOF STATE]
proof (prove)
using this:
j < length (mat_to_cols_list (A * B))
i < dim_row A
dim_col A = dim_row B

goal (1 subgoal):
 1. plus_mult.scalar_product (*) 0 (+) (Matrix_Legacy.row (mat_to_cols_list A) i) (Matrix_Legacy.col (mat_to_cols_list B) j) = vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i) \<bullet> vec_of_list (Matrix_Legacy.col (mat_to_cols_list B) j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
plus_mult.scalar_product (*) 0 (+) (Matrix_Legacy.row (mat_to_cols_list A) i) (Matrix_Legacy.col (mat_to_cols_list B) j) = vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i) \<bullet> vec_of_list (Matrix_Legacy.col (mat_to_cols_list B) j)

goal (1 subgoal):
 1. \<And>i. i < dim_row A \<Longrightarrow> mat_to_cols_list (A * B) ! j ! i = M ! j ! i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
M ! j ! i = vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i) \<bullet> vec_of_list (Matrix_Legacy.col (mat_to_cols_list B) j)
[PROOF STEP]
show "mat_to_cols_list (A * B) ! j ! i = M ! j ! i"
[PROOF STATE]
proof (prove)
using this:
M ! j ! i = vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i) \<bullet> vec_of_list (Matrix_Legacy.col (mat_to_cols_list B) j)

goal (1 subgoal):
 1. mat_to_cols_list (A * B) ! j ! i = M ! j ! i
[PROOF STEP]
using mat_to_cols_list_def index_mult_mat(1) a0 a1
[PROOF STATE]
proof (prove)
using this:
M ! j ! i = vec_of_list (Matrix_Legacy.row (mat_to_cols_list A) i) \<bullet> vec_of_list (Matrix_Legacy.col (mat_to_cols_list B) j)
mat_to_cols_list ?A = map (\<lambda>j. map (\<lambda>i. ?A $$ (i, j)) [0..<dim_row ?A]) [0..<dim_col ?A]
\<lbrakk>?i < dim_row ?A; ?j < dim_col ?B\<rbrakk> \<Longrightarrow> (?A * ?B) $$ (?i, ?j) = Matrix.row ?A ?i \<bullet> Matrix.col ?B ?j
j < length (mat_to_cols_list (A * B))
i < dim_row A

goal (1 subgoal):
 1. mat_to_cols_list (A * B) ! j ! i = M ! j ! i
[PROOF STEP]
by(simp add: Matrix_row_is_Legacy_row Matrix_col_is_Legacy_col)
[PROOF STATE]
proof (state)
this:
mat_to_cols_list (A * B) ! j ! i = M ! j ! i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i < dim_row A \<longrightarrow> mat_to_cols_list (A * B) ! j ! ?i = M ! j ! ?i

goal (1 subgoal):
 1. \<And>j. j < length (mat_to_cols_list (A * B)) \<Longrightarrow> mat_to_cols_list (A * B) ! j = M ! j
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length (mat_to_cols_list (A * B) ! j) = length (M ! j)
?i < dim_row A \<longrightarrow> mat_to_cols_list (A * B) ! j ! ?i = M ! j ! ?i
[PROOF STEP]
show "mat_to_cols_list (A * B) ! j = M ! j"
[PROOF STATE]
proof (prove)
using this:
length (mat_to_cols_list (A * B) ! j) = length (M ! j)
?i < dim_row A \<longrightarrow> mat_to_cols_list (A * B) ! j ! ?i = M ! j ! ?i

goal (1 subgoal):
 1. mat_to_cols_list (A * B) ! j = M ! j
[PROOF STEP]
by(simp add: nth_equalityI f2)
[PROOF STATE]
proof (state)
this:
mat_to_cols_list (A * B) ! j = M ! j

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?j < length (mat_to_cols_list (A * B)) \<longrightarrow> mat_to_cols_list (A * B) ! ?j = M ! ?j

goal (1 subgoal):
 1. \<And>i. i < length (mat_to_cols_list (A * B)) \<Longrightarrow> mat_to_cols_list (A * B) ! i = mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B) ! i
[PROOF STEP]
fix i:: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < length (mat_to_cols_list (A * B)) \<Longrightarrow> mat_to_cols_list (A * B) ! i = mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B) ! i
[PROOF STEP]
assume "i < length (mat_to_cols_list (A * B))"
[PROOF STATE]
proof (state)
this:
i < length (mat_to_cols_list (A * B))

goal (1 subgoal):
 1. \<And>i. i < length (mat_to_cols_list (A * B)) \<Longrightarrow> mat_to_cols_list (A * B) ! i = mat_mult (mult.row_length (mat_to_cols_list A)) (mat_to_cols_list A) (mat_to_cols_list B) ! i
[PROOF STEP]
thus "mat_to_cols_list (A * B) ! i = M ! i"
[PROOF STATE]
proof (prove)
using this:
i < length (mat_to_cols_list (A * B))

goal (1 subgoal):
 1. mat_to_cols_list (A * B) ! i = M ! i
[PROOF STEP]
by (simp add: f1)
[PROOF STATE]
proof (state)
this:
mat_to_cols_list (A * B) ! i = M ! i

goal:
No subgoals!
[PROOF STEP]
qed