[STATEMENT]
lemma mult_distr_tensor:
  assumes a1:"dim_col A = dim_row B" and a2:"dim_col C = dim_row D" and a3:"dim_col A > 0" and
    a4:"dim_col B > 0" and a5:"dim_col C > 0" and a6:"dim_col D > 0"
  shows "(A * B) \<Otimes> (C * D) = (A \<Otimes> C) * (B \<Otimes> D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A * B \<Otimes> C * D = (A \<Otimes> C) * (B \<Otimes> D)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A * B \<Otimes> C * D = (A \<Otimes> C) * (B \<Otimes> D)
[PROOF STEP]
define A' B' C' D' M N where "A' = mat_to_cols_list A" and "B' = mat_to_cols_list B" and
    "C' = mat_to_cols_list C" and "D' = mat_to_cols_list D" and
    "M = mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list C))" and
    "N = mat_of_cols_list (dim_row B * dim_row D) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list D))"
[PROOF STATE]
proof (state)
this:
A' = mat_to_cols_list A
B' = mat_to_cols_list B
C' = mat_to_cols_list C
D' = mat_to_cols_list D
M = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list C))
N = Tensor.mat_of_cols_list (dim_row B * dim_row D) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list D))

goal (1 subgoal):
 1. A * B \<Otimes> C * D = (A \<Otimes> C) * (B \<Otimes> D)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A' = mat_to_cols_list A
B' = mat_to_cols_list B
C' = mat_to_cols_list C
D' = mat_to_cols_list D
M = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list C))
N = Tensor.mat_of_cols_list (dim_row B * dim_row D) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list D))
[PROOF STEP]
have "(A \<Otimes> C) * (B \<Otimes> D) = M * N"
[PROOF STATE]
proof (prove)
using this:
A' = mat_to_cols_list A
B' = mat_to_cols_list B
C' = mat_to_cols_list C
D' = mat_to_cols_list D
M = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list C))
N = Tensor.mat_of_cols_list (dim_row B * dim_row D) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list D))

goal (1 subgoal):
 1. (A \<Otimes> C) * (B \<Otimes> D) = M * N
[PROOF STEP]
by (simp add: tensor_mat_def)
[PROOF STATE]
proof (state)
this:
(A \<Otimes> C) * (B \<Otimes> D) = M * N

goal (1 subgoal):
 1. A * B \<Otimes> C * D = (A \<Otimes> C) * (B \<Otimes> D)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(A \<Otimes> C) * (B \<Otimes> D) = M * N

goal (1 subgoal):
 1. A * B \<Otimes> C * D = (A \<Otimes> C) * (B \<Otimes> D)
[PROOF STEP]
have "\<dots> = mat_of_cols_list (dim_row A * dim_row C) (plus_mult.matrix_mult (*) 0 (+)
  (mat_to_cols_list M) (mat_to_cols_list N))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M * N = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mat_to_cols_list M)) (mat_to_cols_list M) (mat_to_cols_list N))
[PROOF STEP]
using assms M_def N_def dim_col_tensor_mat dim_row_tensor_mat tensor_mat_def
[PROOF STATE]
proof (prove)
using this:
dim_col A = dim_row B
dim_col C = dim_row D
0 < dim_col A
0 < dim_col B
0 < dim_col C
0 < dim_col D
M = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list C))
N = Tensor.mat_of_cols_list (dim_row B * dim_row D) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list D))
dim_col (?A \<Otimes> ?B) = dim_col ?A * dim_col ?B
dim_row (?A \<Otimes> ?B) = dim_row ?A * dim_row ?B
?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))

goal (1 subgoal):
 1. M * N = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mat_to_cols_list M)) (mat_to_cols_list M) (mat_to_cols_list N))
[PROOF STEP]
by(simp add: matrix_mult_to_times_mat)
[PROOF STATE]
proof (state)
this:
M * N = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mat_to_cols_list M)) (mat_to_cols_list M) (mat_to_cols_list N))

goal (1 subgoal):
 1. A * B \<Otimes> C * D = (A \<Otimes> C) * (B \<Otimes> D)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M * N = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mat_to_cols_list M)) (mat_to_cols_list M) (mat_to_cols_list N))

goal (1 subgoal):
 1. A * B \<Otimes> C * D = (A \<Otimes> C) * (B \<Otimes> D)
[PROOF STEP]
have f1:"\<dots> = mat_of_cols_list (dim_row A * dim_row C) (plus_mult.matrix_mult (*) 0 (+)
  (mult.Tensor (*) A' C') (mult.Tensor (*) B' D'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mat_to_cols_list M)) (mat_to_cols_list M) (mat_to_cols_list N)) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D'))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mat_to_cols_list M)) (mat_to_cols_list M) (mat_to_cols_list N)) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D'))
[PROOF STEP]
define M' N' where "M' = mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list C)" and
      "N' = mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list D)"
[PROOF STATE]
proof (state)
this:
M' = mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list C)
N' = mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list D)

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mat_to_cols_list M)) (mat_to_cols_list M) (mat_to_cols_list N)) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
M' = mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list C)
N' = mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list D)
[PROOF STEP]
have "mat (mult.row_length M') (length M') M'"
[PROOF STATE]
proof (prove)
using this:
M' = mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list C)
N' = mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list D)

goal (1 subgoal):
 1. Matrix_Legacy.mat (mult.row_length M') (length M') M'
[PROOF STEP]
using M'_def mult.effective_well_defined_Tensor[of 1 "(*)"] mat_to_cols_list_is_mat a3 a5
[PROOF STATE]
proof (prove)
using this:
M' = mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list C)
N' = mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list D)
M' = mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list C)
\<lbrakk>Matrix_Tensor.mult (1::?'a1) (*); Matrix_Legacy.mat (mult.row_length ?M1.0) (length ?M1.0) ?M1.0; Matrix_Legacy.mat (mult.row_length ?M2.0) (length ?M2.0) ?M2.0\<rbrakk> \<Longrightarrow> Matrix_Legacy.mat (mult.row_length ?M1.0 * mult.row_length ?M2.0) (length ?M1.0 * length ?M2.0) (mult.Tensor (*) ?M1.0 ?M2.0)
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
0 < dim_col C

goal (1 subgoal):
 1. Matrix_Legacy.mat (mult.row_length M') (length M') M'
[PROOF STEP]
by (smt mult.length_Tensor mult.row_length_mat plus_mult_cpx plus_mult_def)
[PROOF STATE]
proof (state)
this:
Matrix_Legacy.mat (mult.row_length M') (length M') M'

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mat_to_cols_list M)) (mat_to_cols_list M) (mat_to_cols_list N)) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Matrix_Legacy.mat (mult.row_length M') (length M') M'

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mat_to_cols_list M)) (mat_to_cols_list M) (mat_to_cols_list N)) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D'))
[PROOF STEP]
have "mat (mult.row_length N') (length N') N'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix_Legacy.mat (mult.row_length N') (length N') N'
[PROOF STEP]
using N'_def mult.effective_well_defined_Tensor[of 1 "(*)"] mat_to_cols_list_is_mat a4 a6
[PROOF STATE]
proof (prove)
using this:
N' = mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list D)
\<lbrakk>Matrix_Tensor.mult (1::?'a1) (*); Matrix_Legacy.mat (mult.row_length ?M1.0) (length ?M1.0) ?M1.0; Matrix_Legacy.mat (mult.row_length ?M2.0) (length ?M2.0) ?M2.0\<rbrakk> \<Longrightarrow> Matrix_Legacy.mat (mult.row_length ?M1.0 * mult.row_length ?M2.0) (length ?M1.0 * length ?M2.0) (mult.Tensor (*) ?M1.0 ?M2.0)
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 B
0 < dim_col D

goal (1 subgoal):
 1. Matrix_Legacy.mat (mult.row_length N') (length N') N'
[PROOF STEP]
by (smt mult.length_Tensor mult.row_length_mat plus_mult_cpx plus_mult_def)
[PROOF STATE]
proof (state)
this:
Matrix_Legacy.mat (mult.row_length N') (length N') N'

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mat_to_cols_list M)) (mat_to_cols_list M) (mat_to_cols_list N)) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D'))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Matrix_Legacy.mat (mult.row_length M') (length M') M'
Matrix_Legacy.mat (mult.row_length N') (length N') N'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Matrix_Legacy.mat (mult.row_length M') (length M') M'
Matrix_Legacy.mat (mult.row_length N') (length N') N'

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mat_to_cols_list M)) (mat_to_cols_list M) (mat_to_cols_list N)) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D'))
[PROOF STEP]
using list_to_mat_to_cols_list M_def N_def mult.row_length_mat row_length_mat_to_cols_list
      assms(3) a4 a5 a6 A'_def B'_def C'_def D'_def
[PROOF STATE]
proof (prove)
using this:
Matrix_Legacy.mat (mult.row_length M') (length M') M'
Matrix_Legacy.mat (mult.row_length N') (length N') N'
Matrix_Legacy.mat ?nr ?nc ?l \<Longrightarrow> mat_to_cols_list (Tensor.mat_of_cols_list ?nr ?l) = ?l
M = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list C))
N = Tensor.mat_of_cols_list (dim_row B * dim_row D) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list D))
Matrix_Tensor.mult ?id ?f \<Longrightarrow> mult.row_length (mult.Tensor ?f ?m1.0 ?m2.0) = mult.row_length ?m1.0 * mult.row_length ?m2.0
0 < dim_col ?A \<Longrightarrow> mult.row_length (mat_to_cols_list ?A) = dim_row ?A
0 < dim_col A
0 < dim_col B
0 < dim_col C
0 < dim_col D
A' = mat_to_cols_list A
B' = mat_to_cols_list B
C' = mat_to_cols_list C
D' = mat_to_cols_list D

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mat_to_cols_list M)) (mat_to_cols_list M) (mat_to_cols_list N)) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D'))
[PROOF STEP]
by(metis M'_def N'_def plus_mult_cpx plus_mult_def)
[PROOF STATE]
proof (state)
this:
Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mat_to_cols_list M)) (mat_to_cols_list M) (mat_to_cols_list N)) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D'))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mat_to_cols_list M)) (mat_to_cols_list M) (mat_to_cols_list N)) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D'))

goal (1 subgoal):
 1. A * B \<Otimes> C * D = (A \<Otimes> C) * (B \<Otimes> D)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mat_to_cols_list M)) (mat_to_cols_list M) (mat_to_cols_list N)) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D'))

goal (1 subgoal):
 1. A * B \<Otimes> C * D = (A \<Otimes> C) * (B \<Otimes> D)
[PROOF STEP]
have "\<dots> = mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*)
    (plus_mult.matrix_mult (*) 0 (+) A' B')
    (plus_mult.matrix_mult (*) 0 (+) C' D'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D'))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D'))
[PROOF STEP]
have f2:"mat (mult.row_length A') (length A') A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix_Legacy.mat (mult.row_length A') (length A') A'
[PROOF STEP]
using A'_def a3 mat_to_cols_list_is_mat
[PROOF STATE]
proof (prove)
using this:
A' = mat_to_cols_list A
0 < dim_col A
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 A') (length A') A'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Matrix_Legacy.mat (mult.row_length A') (length A') A'

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Matrix_Legacy.mat (mult.row_length A') (length A') A'

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D'))
[PROOF STEP]
have "mat (mult.row_length B') (length B') B'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix_Legacy.mat (mult.row_length B') (length B') B'
[PROOF STEP]
using B'_def a4 mat_to_cols_list_is_mat
[PROOF STATE]
proof (prove)
using this:
B' = mat_to_cols_list B
0 < dim_col 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 (mult.row_length B') (length B') B'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Matrix_Legacy.mat (mult.row_length B') (length B') B'

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Matrix_Legacy.mat (mult.row_length B') (length B') B'

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D'))
[PROOF STEP]
have "mat (mult.row_length C') (length C') C'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix_Legacy.mat (mult.row_length C') (length C') C'
[PROOF STEP]
using C'_def a5 mat_to_cols_list_is_mat
[PROOF STATE]
proof (prove)
using this:
C' = mat_to_cols_list C
0 < dim_col C
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 C') (length C') C'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Matrix_Legacy.mat (mult.row_length C') (length C') C'

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Matrix_Legacy.mat (mult.row_length C') (length C') C'

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D'))
[PROOF STEP]
have "mat (mult.row_length D') (length D') D'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix_Legacy.mat (mult.row_length D') (length D') D'
[PROOF STEP]
using D'_def a6 mat_to_cols_list_is_mat
[PROOF STATE]
proof (prove)
using this:
D' = mat_to_cols_list D
0 < dim_col D
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 D') (length D') D'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Matrix_Legacy.mat (mult.row_length D') (length D') D'

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Matrix_Legacy.mat (mult.row_length D') (length D') D'

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D'))
[PROOF STEP]
have "length A' = mult.row_length B'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length A' = mult.row_length B'
[PROOF STEP]
using A'_def B'_def a1 a4
[PROOF STATE]
proof (prove)
using this:
A' = mat_to_cols_list A
B' = mat_to_cols_list B
dim_col A = dim_row B
0 < dim_col B

goal (1 subgoal):
 1. length A' = mult.row_length B'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length A' = mult.row_length B'

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length A' = mult.row_length B'

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D'))
[PROOF STEP]
have "length C' = mult.row_length D'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length C' = mult.row_length D'
[PROOF STEP]
using C'_def D'_def a2 a6
[PROOF STATE]
proof (prove)
using this:
C' = mat_to_cols_list C
D' = mat_to_cols_list D
dim_col C = dim_row D
0 < dim_col D

goal (1 subgoal):
 1. length C' = mult.row_length D'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length C' = mult.row_length D'

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length C' = mult.row_length D'

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D'))
[PROOF STEP]
have "A' \<noteq> [] \<and> B' \<noteq> [] \<and> C' \<noteq> [] \<and> D' \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' \<noteq> [] \<and> B' \<noteq> [] \<and> C' \<noteq> [] \<and> D' \<noteq> []
[PROOF STEP]
using A'_def B'_def C'_def D'_def a3 a4 a5 a6
[PROOF STATE]
proof (prove)
using this:
A' = mat_to_cols_list A
B' = mat_to_cols_list B
C' = mat_to_cols_list C
D' = mat_to_cols_list D
0 < dim_col A
0 < dim_col B
0 < dim_col C
0 < dim_col D

goal (1 subgoal):
 1. A' \<noteq> [] \<and> B' \<noteq> [] \<and> C' \<noteq> [] \<and> D' \<noteq> []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A' \<noteq> [] \<and> B' \<noteq> [] \<and> C' \<noteq> [] \<and> D' \<noteq> []

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D'))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Matrix_Legacy.mat (mult.row_length A') (length A') A'
Matrix_Legacy.mat (mult.row_length B') (length B') B'
Matrix_Legacy.mat (mult.row_length C') (length C') C'
Matrix_Legacy.mat (mult.row_length D') (length D') D'
length A' = mult.row_length B'
length C' = mult.row_length D'
A' \<noteq> [] \<and> B' \<noteq> [] \<and> C' \<noteq> [] \<and> D' \<noteq> []
[PROOF STEP]
have "plus_mult.matrix_match A' B' C' D'"
[PROOF STATE]
proof (prove)
using this:
Matrix_Legacy.mat (mult.row_length A') (length A') A'
Matrix_Legacy.mat (mult.row_length B') (length B') B'
Matrix_Legacy.mat (mult.row_length C') (length C') C'
Matrix_Legacy.mat (mult.row_length D') (length D') D'
length A' = mult.row_length B'
length C' = mult.row_length D'
A' \<noteq> [] \<and> B' \<noteq> [] \<and> C' \<noteq> [] \<and> D' \<noteq> []

goal (1 subgoal):
 1. plus_mult.matrix_match A' B' C' D'
[PROOF STEP]
using plus_mult.matrix_match_def[of 1 "(*)" 0 "(+)" "a_inv cpx_rng"]
[PROOF STATE]
proof (prove)
using this:
Matrix_Legacy.mat (mult.row_length A') (length A') A'
Matrix_Legacy.mat (mult.row_length B') (length B') B'
Matrix_Legacy.mat (mult.row_length C') (length C') C'
Matrix_Legacy.mat (mult.row_length D') (length D') D'
length A' = mult.row_length B'
length C' = mult.row_length D'
A' \<noteq> [] \<and> B' \<noteq> [] \<and> C' \<noteq> [] \<and> D' \<noteq> []
plus_mult 1 (*) 0 (+) (a_inv cpx_rng) \<Longrightarrow> plus_mult.matrix_match ?A1.0 ?A2.0 ?B1.0 ?B2.0 \<equiv> Matrix_Legacy.mat (mult.row_length ?A1.0) (length ?A1.0) ?A1.0 \<and> Matrix_Legacy.mat (mult.row_length ?A2.0) (length ?A2.0) ?A2.0 \<and> Matrix_Legacy.mat (mult.row_length ?B1.0) (length ?B1.0) ?B1.0 \<and> Matrix_Legacy.mat (mult.row_length ?B2.0) (length ?B2.0) ?B2.0 \<and> length ?A1.0 = mult.row_length ?A2.0 \<and> length ?B1.0 = mult.row_length ?B2.0 \<and> ?A1.0 \<noteq> [] \<and> ?A2.0 \<noteq> [] \<and> ?B1.0 \<noteq> [] \<and> ?B2.0 \<noteq> []

goal (1 subgoal):
 1. plus_mult.matrix_match A' B' C' D'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
plus_mult.matrix_match A' B' C' D'

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D'))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
plus_mult.matrix_match A' B' C' D'

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D'))
[PROOF STEP]
using f1 plus_mult.distributivity plus_mult_cpx
[PROOF STATE]
proof (prove)
using this:
plus_mult.matrix_match A' B' C' D'
Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mat_to_cols_list M)) (mat_to_cols_list M) (mat_to_cols_list N)) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D'))
\<lbrakk>plus_mult ?id ?f ?zer ?g ?inver; plus_mult.matrix_match ?A1.0 ?A2.0 ?B1.0 ?B2.0\<rbrakk> \<Longrightarrow> mult.Tensor ?f (mat_multI ?zer ?g ?f (mult.row_length ?A1.0) ?A1.0 ?A2.0) (mat_multI ?zer ?g ?f (mult.row_length ?B1.0) ?B1.0 ?B2.0) = mat_multI ?zer ?g ?f (mult.row_length (mult.Tensor ?f ?A1.0 ?B1.0)) (mult.Tensor ?f ?A1.0 ?B1.0) (mult.Tensor ?f ?A2.0 ?B2.0)
plus_mult 1 (*) 0 (+) (a_inv cpx_rng)

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D'))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D'))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D'))

goal (1 subgoal):
 1. A * B \<Otimes> C * D = (A \<Otimes> C) * (B \<Otimes> D)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Tensor.mat_of_cols_list (dim_row A * dim_row C) (mat_mult (mult.row_length (mult.Tensor (*) A' C')) (mult.Tensor (*) A' C') (mult.Tensor (*) B' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D'))

goal (1 subgoal):
 1. A * B \<Otimes> C * D = (A \<Otimes> C) * (B \<Otimes> D)
[PROOF STEP]
have "\<dots> = mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*)
   (mat_to_cols_list (A * B)) (mat_to_cols_list (C * D)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_to_cols_list (A * B)) (mat_to_cols_list (C * D)))
[PROOF STEP]
using A'_def B'_def C'_def D'_def a1 a2 a3 a5
[PROOF STATE]
proof (prove)
using this:
A' = mat_to_cols_list A
B' = mat_to_cols_list B
C' = mat_to_cols_list C
D' = mat_to_cols_list D
dim_col A = dim_row B
dim_col C = dim_row D
0 < dim_col A
0 < dim_col C

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_to_cols_list (A * B)) (mat_to_cols_list (C * D)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_mult (mult.row_length A') A' B') (mat_mult (mult.row_length C') C' D')) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_to_cols_list (A * B)) (mat_to_cols_list (C * D)))

goal (1 subgoal):
 1. A * B \<Otimes> C * D = (A \<Otimes> C) * (B \<Otimes> D)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(A \<Otimes> C) * (B \<Otimes> D) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_to_cols_list (A * B)) (mat_to_cols_list (C * D)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(A \<Otimes> C) * (B \<Otimes> D) = Tensor.mat_of_cols_list (dim_row A * dim_row C) (mult.Tensor (*) (mat_to_cols_list (A * B)) (mat_to_cols_list (C * D)))

goal (1 subgoal):
 1. A * B \<Otimes> C * D = (A \<Otimes> C) * (B \<Otimes> D)
[PROOF STEP]
by(simp add: tensor_mat_def)
[PROOF STATE]
proof (state)
this:
A * B \<Otimes> C * D = (A \<Otimes> C) * (B \<Otimes> D)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tensor_mat_is_assoc:
  fixes A B C:: "complex Matrix.mat"
  shows "A \<Otimes> (B \<Otimes> C) = (A \<Otimes> B) \<Otimes> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Otimes> (B \<Otimes> C) = A \<Otimes> B \<Otimes> C
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<Otimes> (B \<Otimes> C) = A \<Otimes> B \<Otimes> C
[PROOF STEP]
define M where d:"M = mat_of_cols_list (dim_row B * dim_row C) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C))"
[PROOF STATE]
proof (state)
this:
M = Tensor.mat_of_cols_list (dim_row B * dim_row C) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C))

goal (1 subgoal):
 1. A \<Otimes> (B \<Otimes> C) = A \<Otimes> B \<Otimes> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
M = Tensor.mat_of_cols_list (dim_row B * dim_row C) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C))
[PROOF STEP]
have "B \<Otimes> C = M"
[PROOF STATE]
proof (prove)
using this:
M = Tensor.mat_of_cols_list (dim_row B * dim_row C) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C))

goal (1 subgoal):
 1. B \<Otimes> C = M
[PROOF STEP]
using tensor_mat_def
[PROOF STATE]
proof (prove)
using this:
M = Tensor.mat_of_cols_list (dim_row B * dim_row C) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C))
?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))

goal (1 subgoal):
 1. B \<Otimes> C = M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
B \<Otimes> C = M

goal (1 subgoal):
 1. A \<Otimes> (B \<Otimes> C) = A \<Otimes> B \<Otimes> C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
B \<Otimes> C = M

goal (1 subgoal):
 1. A \<Otimes> (B \<Otimes> C) = A \<Otimes> B \<Otimes> C
[PROOF STEP]
have "A \<Otimes> (B \<Otimes> C) = mat_of_cols_list (dim_row A * (dim_row B * dim_row C))
(mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Otimes> (B \<Otimes> C) = Tensor.mat_of_cols_list (dim_row A * (dim_row B * dim_row C)) (mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list M))
[PROOF STEP]
using tensor_mat_def d dim_row_tensor_mat
[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))
M = Tensor.mat_of_cols_list (dim_row B * dim_row C) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C))
dim_row (?A \<Otimes> ?B) = dim_row ?A * dim_row ?B

goal (1 subgoal):
 1. A \<Otimes> (B \<Otimes> C) = Tensor.mat_of_cols_list (dim_row A * (dim_row B * dim_row C)) (mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list M))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A \<Otimes> (B \<Otimes> C) = Tensor.mat_of_cols_list (dim_row A * (dim_row B * dim_row C)) (mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list M))

goal (1 subgoal):
 1. A \<Otimes> (B \<Otimes> C) = A \<Otimes> B \<Otimes> C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A \<Otimes> (B \<Otimes> C) = Tensor.mat_of_cols_list (dim_row A * (dim_row B * dim_row C)) (mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list M))

goal (1 subgoal):
 1. A \<Otimes> (B \<Otimes> C) = A \<Otimes> B \<Otimes> C
[PROOF STEP]
have "mat_to_cols_list M = mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_to_cols_list M = mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C)
[PROOF STEP]
using d list_to_mat_to_cols_list
[PROOF STATE]
proof (prove)
using this:
M = Tensor.mat_of_cols_list (dim_row B * dim_row C) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C))
Matrix_Legacy.mat ?nr ?nc ?l \<Longrightarrow> mat_to_cols_list (Tensor.mat_of_cols_list ?nr ?l) = ?l

goal (1 subgoal):
 1. mat_to_cols_list M = mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C)
[PROOF STEP]
by (smt calculation(1) dim_col_tensor_mat length_greater_0_conv length_mat_to_cols_list mat_to_cols_list_is_mat
mult.Tensor.simps(1) mult.Tensor_null mult.well_defined_Tensor nat_0_less_mult_iff plus_mult_cpx plus_mult_def row_length_mat_to_cols_list)
[PROOF STATE]
proof (state)
this:
mat_to_cols_list M = mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C)

goal (1 subgoal):
 1. A \<Otimes> (B \<Otimes> C) = A \<Otimes> B \<Otimes> C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
B \<Otimes> C = M
A \<Otimes> (B \<Otimes> C) = Tensor.mat_of_cols_list (dim_row A * (dim_row B * dim_row C)) (mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list M))
mat_to_cols_list M = mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C)
[PROOF STEP]
have "A \<Otimes> (B \<Otimes> C) = mat_of_cols_list (dim_row A * (dim_row B * dim_row C))
(mult.Tensor (*) (mat_to_cols_list A) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C)))"
[PROOF STATE]
proof (prove)
using this:
B \<Otimes> C = M
A \<Otimes> (B \<Otimes> C) = Tensor.mat_of_cols_list (dim_row A * (dim_row B * dim_row C)) (mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list M))
mat_to_cols_list M = mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C)

goal (1 subgoal):
 1. A \<Otimes> (B \<Otimes> C) = Tensor.mat_of_cols_list (dim_row A * (dim_row B * dim_row C)) (mult.Tensor (*) (mat_to_cols_list A) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A \<Otimes> (B \<Otimes> C) = Tensor.mat_of_cols_list (dim_row A * (dim_row B * dim_row C)) (mult.Tensor (*) (mat_to_cols_list A) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C)))

goal (1 subgoal):
 1. A \<Otimes> (B \<Otimes> C) = A \<Otimes> B \<Otimes> C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A \<Otimes> (B \<Otimes> C) = Tensor.mat_of_cols_list (dim_row A * (dim_row B * dim_row C)) (mult.Tensor (*) (mat_to_cols_list A) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C)))

goal (1 subgoal):
 1. A \<Otimes> (B \<Otimes> C) = A \<Otimes> B \<Otimes> C
[PROOF STEP]
have "\<dots> = mat_of_cols_list ((dim_row A * dim_row B) * dim_row C)
(mult.Tensor (*) (mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B)) (mat_to_cols_list C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * (dim_row B * dim_row C)) (mult.Tensor (*) (mat_to_cols_list A) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C))) = Tensor.mat_of_cols_list (dim_row A * dim_row B * dim_row C) (mult.Tensor (*) (mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B)) (mat_to_cols_list C))
[PROOF STEP]
using Matrix_Tensor.mult.associativity
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Matrix_Tensor.mult ?id ?f; 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 \<and> Matrix_Legacy.mat (mult.row_length ?M3.0) (length ?M3.0) ?M3.0\<rbrakk> \<Longrightarrow> mult.Tensor ?f ?M1.0 (mult.Tensor ?f ?M2.0 ?M3.0) = mult.Tensor ?f (mult.Tensor ?f ?M1.0 ?M2.0) ?M3.0

goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A * (dim_row B * dim_row C)) (mult.Tensor (*) (mat_to_cols_list A) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C))) = Tensor.mat_of_cols_list (dim_row A * dim_row B * dim_row C) (mult.Tensor (*) (mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B)) (mat_to_cols_list C))
[PROOF STEP]
by (smt ab_semigroup_mult_class.mult_ac(1) length_greater_0_conv length_mat_to_cols_list
mat_to_cols_list_is_mat mult.Tensor.simps(1) mult.Tensor_null plus_mult_cpx plus_mult_def)
[PROOF STATE]
proof (state)
this:
Tensor.mat_of_cols_list (dim_row A * (dim_row B * dim_row C)) (mult.Tensor (*) (mat_to_cols_list A) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C))) = Tensor.mat_of_cols_list (dim_row A * dim_row B * dim_row C) (mult.Tensor (*) (mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B)) (mat_to_cols_list C))

goal (1 subgoal):
 1. A \<Otimes> (B \<Otimes> C) = A \<Otimes> B \<Otimes> C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A \<Otimes> (B \<Otimes> C) = Tensor.mat_of_cols_list (dim_row A * (dim_row B * dim_row C)) (mult.Tensor (*) (mat_to_cols_list A) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C)))
Tensor.mat_of_cols_list (dim_row A * (dim_row B * dim_row C)) (mult.Tensor (*) (mat_to_cols_list A) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C))) = Tensor.mat_of_cols_list (dim_row A * dim_row B * dim_row C) (mult.Tensor (*) (mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B)) (mat_to_cols_list C))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A \<Otimes> (B \<Otimes> C) = Tensor.mat_of_cols_list (dim_row A * (dim_row B * dim_row C)) (mult.Tensor (*) (mat_to_cols_list A) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C)))
Tensor.mat_of_cols_list (dim_row A * (dim_row B * dim_row C)) (mult.Tensor (*) (mat_to_cols_list A) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C))) = Tensor.mat_of_cols_list (dim_row A * dim_row B * dim_row C) (mult.Tensor (*) (mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B)) (mat_to_cols_list C))

goal (1 subgoal):
 1. A \<Otimes> (B \<Otimes> C) = A \<Otimes> B \<Otimes> C
[PROOF STEP]
using tensor_mat_def
[PROOF STATE]
proof (prove)
using this:
A \<Otimes> (B \<Otimes> C) = Tensor.mat_of_cols_list (dim_row A * (dim_row B * dim_row C)) (mult.Tensor (*) (mat_to_cols_list A) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C)))
Tensor.mat_of_cols_list (dim_row A * (dim_row B * dim_row C)) (mult.Tensor (*) (mat_to_cols_list A) (mult.Tensor (*) (mat_to_cols_list B) (mat_to_cols_list C))) = Tensor.mat_of_cols_list (dim_row A * dim_row B * dim_row C) (mult.Tensor (*) (mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B)) (mat_to_cols_list C))
?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))

goal (1 subgoal):
 1. A \<Otimes> (B \<Otimes> C) = A \<Otimes> B \<Otimes> C
[PROOF STEP]
by (smt Tensor.mat_of_cols_list_def dim_col_mat(1) dim_col_tensor_mat dim_row_tensor_mat length_0_conv
list_to_mat_to_cols_list mat_to_cols_list_is_mat mult.well_defined_Tensor mult_is_0 neq0_conv
plus_mult_cpx plus_mult_def row_length_mat_to_cols_list)
[PROOF STATE]
proof (state)
this:
A \<Otimes> (B \<Otimes> C) = A \<Otimes> B \<Otimes> C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma SeqQuoteP_subst [simp]:
      "(SeqQuoteP t u s k)(j::=w) =
       SeqQuoteP (subst j w t) (subst j w u) (subst j w s) (subst j w k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SeqQuoteP t u s k)(j::=w) = SeqQuoteP (subst j w t) (subst j w u) (subst j w s) (subst j w k)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (SeqQuoteP t u s k)(j::=w) = SeqQuoteP (subst j w t) (subst j w u) (subst j w s) (subst j w k)
[PROOF STEP]
obtain l::name and sl::name and sl'::name and m::name and n::name and
         sm::name and sm'::name and sn::name and sn'::name
    where "atom l \<sharp> (s,k,w,j,sl,sl',m,n,sm,sm',sn,sn')"
          "atom sl \<sharp> (s,w,j,sl',m,n,sm,sm',sn,sn')"  "atom sl' \<sharp> (s,w,j,m,n,sm,sm',sn,sn')"
          "atom m \<sharp> (s,w,j,n,sm,sm',sn,sn')"  "atom n \<sharp> (s,w,j,sm,sm',sn,sn')"
          "atom sm \<sharp> (s,w,j,sm',sn,sn')"  "atom sm' \<sharp> (s,w,j,sn,sn')"
          "atom sn \<sharp> (s,w,j,sn')"  "atom sn' \<sharp> (s,w,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l sl sl' m n sm sm' sn sn'. \<lbrakk>atom l \<sharp> (s, k, w, j, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (s, w, j, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (s, w, j, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, w, j, n, sm, sm', sn, sn'); atom n \<sharp> (s, w, j, sm, sm', sn, sn'); atom sm \<sharp> (s, w, j, sm', sn, sn'); atom sm' \<sharp> (s, w, j, sn, sn'); atom sn \<sharp> (s, w, j, sn'); atom sn' \<sharp> (s, w, j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom l \<sharp> (s, k, w, j, sl, sl', m, n, sm, sm', sn, sn')
atom sl \<sharp> (s, w, j, sl', m, n, sm, sm', sn, sn')
atom sl' \<sharp> (s, w, j, m, n, sm, sm', sn, sn')
atom m \<sharp> (s, w, j, n, sm, sm', sn, sn')
atom n \<sharp> (s, w, j, sm, sm', sn, sn')
atom sm \<sharp> (s, w, j, sm', sn, sn')
atom sm' \<sharp> (s, w, j, sn, sn')
atom sn \<sharp> (s, w, j, sn')
atom sn' \<sharp> (s, w, j)

goal (1 subgoal):
 1. (SeqQuoteP t u s k)(j::=w) = SeqQuoteP (subst j w t) (subst j w u) (subst j w s) (subst j w k)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
atom l \<sharp> (s, k, w, j, sl, sl', m, n, sm, sm', sn, sn')
atom sl \<sharp> (s, w, j, sl', m, n, sm, sm', sn, sn')
atom sl' \<sharp> (s, w, j, m, n, sm, sm', sn, sn')
atom m \<sharp> (s, w, j, n, sm, sm', sn, sn')
atom n \<sharp> (s, w, j, sm, sm', sn, sn')
atom sm \<sharp> (s, w, j, sm', sn, sn')
atom sm' \<sharp> (s, w, j, sn, sn')
atom sn \<sharp> (s, w, j, sn')
atom sn' \<sharp> (s, w, j)

goal (1 subgoal):
 1. (SeqQuoteP t u s k)(j::=w) = SeqQuoteP (subst j w t) (subst j w u) (subst j w s) (subst j w k)
[PROOF STEP]
by (force simp add: SeqQuoteP.simps [of l _ _ sl sl' m n sm sm' sn sn'])
[PROOF STATE]
proof (state)
this:
(SeqQuoteP t u s k)(j::=w) = SeqQuoteP (subst j w t) (subst j w u) (subst j w s) (subst j w k)

goal:
No subgoals!
[PROOF STEP]
qed