# Theory Matrix_Tensor.Matrix_Tensor

(*  Title:       Tensor Product of Matrices
Author:      T. V. H. Prathamesh (prathamesh@imsc.res.in)
Maintainer:  T. V. H. Prathamesh
*)

text‹
We define Tensor Product of Matrics and prove properties such as associativity and mixed product
property(distributivity) of the tensor product.›

section‹Tensor Product of Matrices›

theory Matrix_Tensor
imports Matrix.Utility Matrix.Matrix_Legacy
begin

subsection‹Defining the Tensor Product›

text‹We define a multiplicative locale here - mult,
where the multiplication satisfies commutativity,
associativity and contains a left and right identity›

locale mult =
fixes id::"'a"
fixes f::" 'a ⇒ 'a ⇒ 'a " (infixl "*" 60)
assumes comm:" f a  b = f b  a "
assumes assoc:" (f (f a b) c) = (f a (f b c))"
assumes left_id:" f id x = x"
assumes right_id:"f x id = x"

context mult
begin

text‹times a v , gives us the product of the vector v with
multiplied pointwise with a›

primrec times:: "'a ⇒ 'a vec ⇒ 'a vec"
where
"times n [] = []"|
"times n (y#ys) = (f n y)#(times n ys)"

lemma times_scalar_id: "times id v = v"

lemma times_vector_id: "times v [id] = [v]"

lemma preserving_length: "length (times n y) = (length y)"
by(induction y)(auto)

text‹vec$\_$vec$\_$Tensor is the tensor product of two vectors. It is
illustrated by the following relation

$vec\_vec\_Tensor (v_1,v_2,...v_n) (w_1,w_2,...w_m) = (v_1 \cdot w_1,...,v_1 \cdot w_m,... , v_n \cdot w_1 , ..., v_n \cdot w_m)$›

primrec vec_vec_Tensor:: "'a vec ⇒ 'a vec ⇒ 'a vec"
where
"vec_vec_Tensor [] ys = []"|
"vec_vec_Tensor (x#xs) ys = (times x ys)@(vec_vec_Tensor xs ys)"

lemma vec_vec_Tensor_left_id: "vec_vec_Tensor [id] v = v"

lemma vec_vec_Tensor_right_id: "vec_vec_Tensor v [id] = v"

theorem vec_vec_Tensor_length :
"(length(vec_vec_Tensor x y)) = (length x)*(length y)"

theorem vec_length: assumes "vec m x" and "vec n y"
shows "vec (m*n) (vec_vec_Tensor x y)"
apply (metis assms(1) assms(2) vec_def)
done

text‹vec$\_$mat$\_$Tensor is the tensor product of two vectors. It is
illusstrated by the following relation

vec\_mat\_Tensor ($v_1,v_2,...v_n) (C_1,C_2,...C_m) = (v_1 \cdot C_1,...,v_n \cdot C_1, ...,v_1 \cdot C_m , ..., v_n \cdot C_m$)›

primrec vec_mat_Tensor::"'a vec ⇒ 'a mat ⇒'a mat"
where
"vec_mat_Tensor xs []  = []"|
"vec_mat_Tensor xs (ys#yss) = (vec_vec_Tensor xs ys)#(vec_mat_Tensor xs yss)"

lemma vec_mat_Tensor_vector_id: "vec_mat_Tensor [id] v = v"

lemma vec_mat_Tensor_matrix_id: "vec_mat_Tensor  v [[id]] = [v]"

theorem vec_mat_Tensor_length:
"length(vec_mat_Tensor xs ys) = length ys"
by(induction ys)(auto)

theorem length_matrix:
assumes "mat nr nc (y#ys)" and "length v = k"
and "(vec_mat_Tensor v (y#ys) = x#xs)"
shows "(vec (nr*k) x)"
proof-
have "vec_mat_Tensor v (y#ys) = (vec_vec_Tensor v y)#(vec_mat_Tensor v ys)"
using vec_mat_Tensor_def assms by auto
also have "(vec_vec_Tensor v y) = x" using assms by auto
also have "length y = nr" using assms mat_def
by (metis in_set_member member_rec(1) vec_def)
from this
have "length (vec_vec_Tensor v y) = nr*k"
using assms vec_vec_Tensor_length  by auto
from this
have "length x = nr*k" by (simp add: ‹vec_vec_Tensor v y = x›)
from this
have "vec (nr*k) x" using vec_def by auto
from this
show ?thesis by auto
qed

lemma matrix_set_list:
assumes "mat nr nc M"
and "length v = k"
and " x ∈ set M"
shows "∃ys.∃zs.(ys@x#zs = M)"
using assms set_def in_set_conv_decomp by metis

primrec reduct :: "'a mat ⇒ 'a mat"
where
"reduct [] = []"
|"reduct (x#xs) = xs"

lemma length_reduct:
assumes "m ≠ []"
shows "length (reduct m) +1  = (length m)"
apply(auto)
by (metis One_nat_def Suc_eq_plus1 assms list.size(4) neq_Nil_conv reduct.simps(2))

lemma mat_empty_column_length: assumes "mat nr nc M" and "M = []"
shows "nc = 0"
proof-
have "(length M = nc)" using mat_def assms by metis
from this
have "nc = 0" using assms by auto
from this
show ?thesis by simp
qed

lemma vec_uniqueness:
assumes "vec m v"
and "vec n v"
shows "m = n"
using vec_def assms(1) assms(2)  by metis

lemma mat_uniqueness:
assumes "mat nr1 nc M"
and "mat nr2 nc M" and "z = hd M" and "M ≠ []"
shows "(∀x∈(set M).(nr1 = nr2))"
proof-
have A:"z ∈ set M" using assms(1) assms(3) assms(4) set_def mat_def
by (metis hd_in_set)
have "Ball (set M) (vec nr1)" using mat_def assms(1) by auto
then have step1: "((x ∈ (set M)) ⟶ (vec nr1 x))" using Ball_def assms by auto
have "Ball (set M) (vec nr2)" using mat_def assms(2) by auto
then have step2: "((x ∈ (set M)) ⟶ (vec nr2 x))" using Ball_def assms by auto
from step1 and step2
have step3:"∀x.((x ∈ (set M))⟶ ((vec nr1 x)∧ (vec nr2 x)))"
by (metis ‹Ball (set M) (vec nr1)› ‹Ball (set M) (vec nr2)›)
have "((vec nr1 x)∧ (vec nr2 x)) ⟶ (nr1 = nr2)" using vec_uniqueness by auto
with step3
have "(∀x.((x ∈ (set M)) ⟶((nr1 = nr2))))" by (metis vec_uniqueness)
then
have "(∀x∈(set M).(nr1 = nr2))" by auto
then
show ?thesis by auto
qed

lemma mat_empty_row_length: assumes "mat nr nc M" and "M = []"
shows "mat 0 nc M"
proof-
have "set M = {}" using mat_def assms  empty_set  by auto
then have "Ball (set M) (vec 0)" using Ball_def by auto
then have "mat 0 nc M" using mat_def assms(1) assms(2) gen_length_code(1) length_code
by (metis (full_types) )
then show ?thesis by auto
qed

abbreviation null_matrix::"'a list list"
where
"null_matrix ≡ [Nil] "

lemma null_mat:"null_matrix = [[]]"
by auto

lemma zero_matrix:" mat 0 0 []" using mat_def in_set_insert insert_Nil list.size(3) not_Cons_self2
by (metis (full_types))

text‹row\_length gives the length of the first row of a matrix. For a valid'
matrix, it is equal to the number of rows›

definition row_length:: "'a mat ⇒ nat"
where
"row_length xs ≡ if (xs = []) then 0 else (length (hd xs))"

lemma row_length_Nil:
"row_length [] =0"
using row_length_def by (metis )

lemma row_length_Null:
"row_length [[]] =0"
using row_length_def by auto

lemma row_length_vect_mat:
"row_length (vec_mat_Tensor v m)  = length v*(row_length m)"
proof(induct m)
case Nil
have "row_length [] = 0"
using row_length_Nil by simp
moreover have "vec_mat_Tensor v [] = []"
using vec_mat_Tensor.simps(1) by auto
ultimately have
"row_length (vec_mat_Tensor v [])  = length v*(row_length [])"
using mult_0_right by (metis )
then show ?case by metis
next
fix a m
assume A:"row_length (vec_mat_Tensor v m) = length v * row_length m"
let ?case =
"row_length (vec_mat_Tensor v (a#m)) = (length v)*(row_length (a#m))"
have A:"row_length (a # m) = length a"
using row_length_def   list.distinct(1)
by auto
have "(vec_mat_Tensor v  (a#m)) = (vec_vec_Tensor v a)#(vec_mat_Tensor v m)"
using vec_mat_Tensor_def vec_mat_Tensor.simps(2)
by auto
from this have
"row_length (vec_mat_Tensor v (a#m)) = length (vec_vec_Tensor v a)"
using row_length_def   list.distinct(1)  vec_mat_Tensor.simps(2)
by auto
from this and vec_vec_Tensor_length have
"row_length (vec_mat_Tensor v (a#m)) = (length v)*(length a)"
by auto
from this and A  have
"row_length (vec_mat_Tensor v (a#m)) = (length v)*(row_length (a#m))"
by auto
from this show ?case by auto
qed

text‹Tensor is the tensor product of matrices›

primrec Tensor::" 'a mat ⇒ 'a mat ⇒'a mat" (infixl "⊗" 63)
where
"Tensor [] xs = []"|
"Tensor (x#xs) ys = (vec_mat_Tensor x ys)@(Tensor xs ys)"

lemma Tensor_null: "xs ⊗[] = []"
by(induction xs)(auto)

text‹Tensor commutes with left and right identity›

lemma Tensor_left_id: "  [[id]] ⊗ xs = xs"

lemma Tensor_right_id: "  xs ⊗ [[id]] = xs"

text‹row$\_$length of tensor product of matrices is the product of
their respective row lengths›

lemma row_length_mat:
"(row_length (m1⊗m2)) = (row_length m1)*(row_length m2)"
proof(induct m1)
case Nil
have "row_length ([]⊗m2) = 0"
using Tensor.simps(1) row_length_def
by metis
from this
have "row_length ([]⊗m2) = (row_length [])*(row_length m2)"
using  row_length_Nil
by auto
then show ?case by metis
next
fix a m1
assume "row_length (m1 ⊗ m2) = row_length m1 * row_length m2"
let ?case =
"row_length ((a # m1) ⊗ m2) = row_length (a # m1) * row_length m2"
have B: "row_length (a#m1) = length a"
using row_length_def   list.distinct(1)
by auto
have "row_length ((a # m1) ⊗ m2) = row_length (a # m1) * row_length m2"
proof(induct m2)
case Nil
show ?case using Tensor_null row_length_def  mult_0_right by (metis)
next
fix aa m2
assume "row_length (a # m1 ⊗ m2) = row_length (a # m1) * row_length m2"
let ?case=
"row_length (a # m1 ⊗ aa # m2)
= row_length (a # m1) * row_length (aa # m2)"
have "aa#m2 ≠ []"
by auto
from this have non_zero:"(vec_mat_Tensor a (aa#m2)) ≠ []"
using vec_mat_Tensor_def by auto
from this have
"hd ((vec_mat_Tensor a (aa#m2))@(m1⊗m2))
= hd (vec_mat_Tensor a (aa#m2))"
by auto
from this have
"hd ((a#m1)⊗(aa#m2)) = hd (vec_mat_Tensor a (aa#m2))"
using Tensor.simps(2) by auto
from this have s1: "row_length ((a#m1)⊗(aa#m2))
= row_length (vec_mat_Tensor a (aa#m2))"
using row_length_def  Nil_is_append_conv non_zero Tensor.simps(2)
by auto
have "row_length (vec_mat_Tensor a (aa#m2))
= (length a)*row_length(aa#m2)"
using row_length_vect_mat by metis
from this and s1
have "row_length (vec_mat_Tensor a (aa#m2))
= (length a)*row_length(aa#m2)"
by auto
from this and B
have "row_length (vec_mat_Tensor a (aa#m2))
= (row_length (a#m1))*row_length(aa#m2)"
by auto
from this  and s1 show ?case  by auto
qed
from this show ?case by auto
qed

lemma hd_set:assumes "x ∈ set (a#M)" shows "(x = a) ∨ (x∈(set M))"
using set_def assms set_ConsD  by auto

text‹for every valid matrix can also be written in the following form›

theorem matrix_row_length:
assumes "mat nr nc M"
shows "mat (row_length M) (length M) M"
proof(cases M)
case Nil
have "row_length M= 0 "
using row_length_def by (metis Nil)
moreover have "length M = 0"
by (metis Nil list.size(3))
moreover  have "mat 0 0 M"
using zero_matrix Nil by auto
ultimately show ?thesis
using mat_empty_row_length row_length_def mat_def  by metis
next
case (Cons a N)
have 1: "mat nr nc (a#N)"
using assms Cons by auto
from this have "(x ∈ set (a #N)) ⟶ (x = a) ∨ (x ∈ (set N))"
using hd_set by auto
from this and 1 have 2:"vec nr a"
using mat_def by (metis Ball_set_list_all list_all_simps(1))
have "row_length (a#N) = length a"
using row_length_def Cons  list.distinct(1) by auto
from this have " vec (row_length (a#N)) a"
using vec_def by auto
from this and 2 have 3:"(row_length M)  = nr"
using vec_uniqueness Cons by auto
have " nc = (length M)"
using 1 and mat_def and assms by metis
with 3
have "mat (row_length M) (length M) M"
using assms by auto
from this show ?thesis by auto
qed

lemma reduct_matrix:
assumes "mat (row_length (a#M)) (length (a#M)) (a#M)"
shows "mat (row_length M) (length M) M"
proof(cases M)
case Nil
show ?thesis
using row_length_def zero_matrix Nil  list.size(3)  by (metis)
next
case (Cons b N)
fix x
have 1: "b ∈ (set M)"
using set_def  Cons ListMem_iff elem  by auto
have "mat (row_length (a#M)) (length (a#M)) (a#M)"
using assms by auto
then have "(x ∈ (set (a#M))) ⟶ ((x = a) ∨ (x ∈ set M))"
by auto
then have " (x ∈ (set (a#M))) ⟶ (vec (row_length (a#M)) x)"
using mat_def Ball_def assms
by metis
then have "(x ∈ (set (a#M))) ⟶ (vec (length a) x)"
using row_length_def  list.distinct(1)
by auto
then have 2:"x ∈ (set M) ⟶ (vec (length a) x)"
by auto
with 1 have 3:"(vec (length a) b)"
using assms in_set_member mat_def member_rec(1) vec_def
by metis
have 5: "(vec (length b) b)"
using vec_def by auto
with 3 have "(length a) = (length b)"
using vec_uniqueness by auto
with 2 have 4: "x ∈ (set M) ⟶ (vec (length b) x)"
by auto
have 6: "row_length M = (length b)"
using row_length_def   Cons list.distinct(1)
by auto
with 4 have "x ∈ (set M) ⟶ (vec (row_length M) x)"
by auto
then have "(∀x. (x ∈ (set M) ⟶ (vec (row_length M) x)))"
using Cons 5 6 assms in_set_member mat_def member_rec(1)
vec_uniqueness
by metis
then have "Ball (set M) (vec (row_length M))"
using Ball_def by auto
then have "(mat (row_length M) (length M) M)"
using mat_def by auto
then show ?thesis by auto
qed

theorem well_defined_vec_mat_Tensor:
"(mat (row_length M) (length M) M) ⟹
(mat
((row_length M)*(length v))
(length M)
(vec_mat_Tensor v M))"
proof(induct M)
case Nil
have "(vec_mat_Tensor v []) = []"
using vec_mat_Tensor.simps(1) Nil
by simp
moreover have "(row_length [] = 0)"
using row_length_def Nil
by metis
moreover have "(length []) = 0"
using Nil by simp
ultimately have
"mat ((row_length [])*(length v)) (length []) (vec_mat_Tensor v [])"
using zero_matrix by (metis mult_zero_left)
then show ?case by simp
next
fix a M
assume hyp :
"(mat (row_length M) (length M) M
⟹ mat (row_length M * length v) (length M) (vec_mat_Tensor v M))"
"mat (row_length (a#M)) (length (a#M)) (a#M)"
let ?case =
"mat (row_length (a#M) * length v) (length (a#M)) (vec_mat_Tensor v (a#M))"
have step1: "mat (row_length M) (length M) M"
using hyp(2) reduct_matrix by auto
then have step2:
"mat (row_length M * length v) (length M) (vec_mat_Tensor v M)"
using hyp(1) by auto
have
"mat
(row_length (a#M) * length v)
(length (a#M))
(vec_mat_Tensor v (a#M))"
proof (cases M)
case Nil
fix x
have 1:"(vec_mat_Tensor v (a#M)) = [vec_vec_Tensor v a]"
using vec_mat_Tensor.simps Nil by auto
have   "(x ∈ (set [vec_vec_Tensor v a])) ⟶  x = (vec_vec_Tensor v a)"
using set_def by auto
then have 2:
"(x ∈ (set [vec_vec_Tensor v a]))
⟶ (vec (length (vec_vec_Tensor v a)) x)"
using vec_def by metis
have 3:"length (vec_vec_Tensor v a) = (length v)*(length a)"
using vec_vec_Tensor_length by auto
then have 4:
"length (vec_vec_Tensor v a) = (length v)*(row_length (a#M))"
using row_length_def  list.distinct(1)
by auto
have 6: "length (vec_mat_Tensor v (a#M)) = (length (a#M))"
using vec_mat_Tensor_length by auto
hence "mat (length (vec_vec_Tensor v a)) (length (a # M)) [vec_vec_Tensor v a]"
by (simp add: Nil mat_def vec_def)
hence
"mat (row_length (a#M) * length v)
(length (vec_mat_Tensor v (a#M)))
(vec_mat_Tensor v (a#M))"
using 1 4 6 by (simp add: mult.commute)
then show ?thesis using 6 by auto
next
case (Cons b L)
fix x
have 1:"x ∈ (set (a#M)) ⟶ ((x=a) ∨ (x ∈ (set M)))"
using hd_set by auto
have "mat (row_length (a#M)) (length (a#M)) (a#M)"
using hyp by auto
then have "x∈ (set (a#M)) ⟶ (vec (row_length (a#M)) x)"
using mat_def Ball_def by metis
then have "x∈ (set (a#M))⟶ (vec (length a) x)"
using row_length_def  list.distinct(1)
by auto
with 1 have "x∈ (set M)⟶ (vec (length a) x)"
by auto
moreover have " b ∈ (set M)"
using Cons by auto
ultimately have "vec (length a) b"
using  hyp(2) in_set_member mat_def member_rec(1) vec_def  by (metis)
then have "(length b) = (length a)"
using vec_def vec_uniqueness by auto
then have 2:"row_length M = (length a)"
using row_length_def   Cons list.distinct(1) by auto
have "mat (row_length M * length v) (length M) (vec_mat_Tensor v M)"
using step2 by auto
then have 3:
"Ball (set (vec_mat_Tensor v M)) (vec ((row_length M)*(length v)))"
using mat_def by auto
then have "(x ∈ set (vec_mat_Tensor v M))
⟶ (vec ((row_length M)*(length v)) x)"
using mat_def Ball_def by auto
then have 4:"(x ∈ set (vec_mat_Tensor v M))
⟶ (vec ((length a)*(length v)) x)"
using 2 by auto
have 5:"length (vec_vec_Tensor v a) = (length a)*(length v)"
using   vec_vec_Tensor_length by auto
then have 6:" vec ((length a)*(length v)) (vec_vec_Tensor v a)"
using vec_vec_Tensor_length vec_def by (metis (full_types))
have 7:"(length a) = (row_length (a#M))"
using row_length_def   list.distinct(1) by auto
have "vec_mat_Tensor v (a#M)
= (vec_vec_Tensor v a)#(vec_mat_Tensor v M)"
using vec_mat_Tensor.simps(2) by auto
then have "(x ∈ set (vec_mat_Tensor v (a#M)))
⟶ ((x = (vec_vec_Tensor v a))
∨ (x ∈ (set (vec_mat_Tensor v M))))"
using  hd_set by auto
with 4 6 have "(x ∈ set (vec_mat_Tensor v (a#M)))
⟶  vec ((length a)*(length v)) x"
by auto
with 7 have "(x ∈ set (vec_mat_Tensor v (a#M)))
⟶  vec ((row_length (a#M))*(length v)) x"
by auto
then have "∀x.((x ∈ set (vec_mat_Tensor v (a#M)))
⟶  vec ((row_length (a#M))*(length v)) x)"
using "2" "3" "6" "7" hd_set vec_mat_Tensor.simps(2) by auto
then have 7:
"Ball
(set (vec_mat_Tensor v (a#M)))
(vec ((row_length (a#M))*(length v)))"
using Ball_def  by auto
have 8: "length (vec_mat_Tensor v (a#M)) = length (a#M)"
using vec_mat_Tensor_length by auto
with 6  7 have
"mat
((row_length (a#M))*(length v))
(length (a#M))
(vec_mat_Tensor v (a#M))"
using mat_def  "5" length_code
by (metis (opaque_lifting, no_types))
then show ?thesis by auto
qed
with  hyp  show ?case by auto
qed

text‹The following theorem  gives length of tensor product of two matrices›

lemma length_Tensor:" (length (M1⊗M2)) = (length M1)*(length M2)"
proof(induct M1)
case Nil
show ?case by auto
next
case (Cons a M1)
have "((a # M1) ⊗ M2) = (vec_mat_Tensor a M2)@(M1 ⊗ M2)"
using Tensor.simps(2) by auto
then have 1:
"length ((a # M1) ⊗ M2) = length ((vec_mat_Tensor a M2)@(M1 ⊗ M2))"
by auto
have 2:"length ((vec_mat_Tensor a M2)@(M1 ⊗ M2))
= length (vec_mat_Tensor a M2)+ length (M1 ⊗ M2)"
using append_def
by auto
have 3:"(length (vec_mat_Tensor a M2)) = length M2"
using vec_mat_Tensor_length by (auto)
have 4:"length (M1 ⊗ M2) = (length M1)*(length M2)"
using  Cons.hyps by auto
with 2 3 have "length ((vec_mat_Tensor a M2)@(M1 ⊗ M2))
= (length M2) + (length M1)*(length M2)"
by auto
then have 5:
"length ((vec_mat_Tensor a M2)@(M1 ⊗ M2)) = (1 + (length M1))*(length M2)"
by auto
with 1  have "length ((a # M1) ⊗ M2) = ((length (a # M1)) * (length M2))"
by auto
then show ?case by auto
qed

lemma append_reduct_matrix:
"(mat (row_length (M1@M2)) (length (M1@M2)) (M1@M2))
⟹(mat (row_length M2) (length M2) M2)"
proof(induct M1)
case Nil
show ?thesis using Nil append.simps(1) by auto
next
case (Cons a M1)
have "mat (row_length (M1 @ M2)) (length (M1 @ M2)) (M1 @ M2)"
using reduct_matrix Cons.prems append_Cons by metis
from this have "(mat (row_length M2) (length M2) M2)"
using Cons.hyps by auto
from this show?thesis by simp
qed

text‹The following theorem proves that tensor product of two valid matrices
is a valid matrix›

theorem well_defined_Tensor:
"(mat (row_length M1) (length M1) M1)
∧ (mat (row_length M2) (length M2) M2)
⟹(mat ((row_length M1)*(row_length M2)) ((length M1)*(length M2)) (M1⊗M2))"
proof(induct M1)
case Nil
have "(row_length []) * (row_length M2) = 0"
using row_length_def  mult_zero_left  by (metis)
moreover have "(length []) * (length M2) = 0"
using  mult_zero_left list.size(3) by auto
moreover have "[] ⊗ M2 = []"
using Tensor.simps(1) by auto
ultimately have
"mat (row_length []*row_length M2) (length []*length M2) ([] ⊗ M2)"
using zero_matrix by metis
then show ?case by simp
next
case (Cons a M1)
have step1: "mat (row_length (a # M1)) (length (a # M1)) (a # M1)"
using Cons.prems by auto
then have "mat (row_length (M1)) (length (M1)) (M1)"
using reduct_matrix by auto
moreover have "mat (row_length (M2)) (length (M2)) (M2)"
using Cons.prems by auto
ultimately have step2:
"mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 ⊗ M2)"
using Cons.hyps by auto
have 0:"row_length (a#M1) = length a"
using row_length_def  list.distinct(1) by auto
have "mat
(row_length (a # M1)*row_length M2)
(length (a # M1)*length M2)
(a # M1 ⊗ M2)"
proof(cases M1)
case Nil
have "(mat ((row_length M2)*(length a)) (length M2) (vec_mat_Tensor a M2))"
using Cons.prems well_defined_vec_mat_Tensor by auto
moreover have "(length (a # M1)) * (length M2) = length M2"
using Nil by auto
moreover have "(a#M1)⊗M2 = (vec_mat_Tensor a M2)"
using Nil Tensor.simps append.simps(1) by auto
ultimately have
"(mat
((row_length M2)*(row_length (a#M1)))
((length (a # M1)) * (length M2))
((a#M1)⊗M2))"
using 0 by auto
then show ?thesis by (simp add: mult.commute)
next
case (Cons b N1)
fix x
have 1:"x ∈ (set (a#M1)) ⟶ ((x=a) ∨ (x ∈ (set M1)))"
using hd_set by auto
have "mat (row_length (a#M1)) (length (a#M1)) (a#M1)"
using Cons.prems by auto
then have "x∈ (set (a#M1)) ⟶ (vec (row_length (a#M1)) x)"
using mat_def Ball_def by metis
then have "x∈ (set (a#M1))⟶ (vec (length a) x)"
using row_length_def  list.distinct(1)
by auto
with 1 have "x∈ (set M1)⟶ (vec (length a) x)"
by auto
moreover have " b ∈ (set M1)"
using Cons by auto
ultimately have "vec (length a) b"
using  Cons.prems in_set_member mat_def member_rec(1) vec_def
by metis
then have "(length b) = (length a)"
using vec_def vec_uniqueness by auto
then have 2:"row_length M1 = (length a)"
using row_length_def Cons by auto
then have "mat
((length a) * row_length M2)
(length M1 * length M2)
(M1 ⊗ M2)"
using step2 by auto
then have "Ball (set (M1⊗M2)) (vec ((length a)*(row_length M2))) "
using mat_def by auto
from this have 3:
"∀x. x ∈ (set (M1 ⊗ M2)) ⟶ (vec ((length a)*(row_length M2)) x)"
using Ball_def by auto
have "mat
((row_length M2)*(length a))
(length M2)
(vec_mat_Tensor a M2)"
using well_defined_vec_mat_Tensor Cons.prems
by auto
then have "Ball
(set (vec_mat_Tensor a M2))
(vec ((row_length M2)*(length a)))"
using mat_def
by auto
then have 4:
"∀x. x ∈ (set (vec_mat_Tensor a M2))
⟶ (vec ((length a)*(row_length M2)) x)"
using mult.commute by metis

with 3 have 5: "∀x. (x ∈ (set (vec_mat_Tensor a M2)))
∨(x ∈ (set (M1 ⊗ M2)))
⟶ (vec ((length a)*(row_length M2)) x)"
by auto
have 6:"(a # M1 ⊗ M2) = (vec_mat_Tensor a M2)@(M1 ⊗M2)"
using Tensor.simps(2) by auto
then have "x ∈ (set (a # M1 ⊗ M2))
⟶ (x ∈ (set (vec_mat_Tensor a M2)))∨(x ∈ (set (M1 ⊗ M2)))"
using set_def append_def by auto
with 5 have 7:"∀x. (x ∈  (set (a # M1 ⊗ M2)))
⟶ (vec ((length a)*(row_length M2)) x)"
by auto
then have 8:
"Ball (set (a # M1 ⊗ M2)) (vec ((row_length (a#M1))*(row_length M2)))"
using Ball_def 0 by auto
have "(length ((a#M1)⊗M2)) = (length (a#M1))*(length M2)"
using length_Tensor by metis
with 7 8
have "mat
(row_length (a # M1) * row_length M2)
(length (a # M1) * length M2)
(a # M1 ⊗ M2)"
using mat_def by (metis "0"  length_Tensor)
then show ?thesis by auto
qed
then show ?case by auto
qed

theorem effective_well_defined_Tensor:
assumes "(mat (row_length M1) (length M1) M1)"
and "(mat (row_length M2) (length M2) M2)"
shows "mat
((row_length M1)*(row_length M2))
((length M1)*(length M2))
(M1⊗M2)"
using well_defined_Tensor assms by auto

definition natmod::"nat ⇒ nat ⇒ nat" (infixl "nmod" 50)
where
"natmod x y = nat ((int x) mod (int y))"

theorem times_elements:
"∀i.((i<(length v)) ⟶ (times a v)!i = f a (v!i))"
apply(rule allI)
proof(induct v)
case Nil
have "(length [] = 0)"
by auto
then have "i <(length []) ⟹ False"
by auto
moreover have "(times a []) = []"
using times.simps(1) by auto
ultimately have "(i<(length [])) ⟶ (times a [])!i = f a ([]!i)"
by auto
then have "∀i. ((i<(length [])) ⟶ (times a [])!i = f a ([]!i))"
by auto
then show ?case  by auto
next
case (Cons x xs)
have "∀i.((x#xs)!(i+1) = (xs)!i)"
by auto
have 0:"((i<length (x#xs))⟶ ((i<(length xs)) ∨ (i = (length xs))))"
by auto
have 1:" ((i<length xs) ⟶((times a xs)!i = f a (xs!i)))"
by (metis Cons.hyps)
have "∀i.((x#xs)!(i+1) = (xs)!i)" by auto
have "((i <length (x#xs)) ⟶(times a (x#xs))!i = f a ((x#xs)!i))"
proof(cases i)
case 0
have "((times a (x#xs))!i) = f a x"
using 0 times.simps(2) by auto
then have "(times a (x#xs))!i = f a ((x#xs)!i)"
using 0 by auto
then show ?thesis by auto
next
case (Suc j)
have 1:"(times a (x#xs))!i = ((f a x)#(times a xs))!i"
using times.simps(2) by auto
have 2:"((f a x)#(times a xs))!i = (times a xs)!j"
using Suc by auto
have 3:"(i <length (x#xs)) ⟶ (j<length xs)"
using One_nat_def Suc Suc_eq_plus1 list.size(4) not_less_eq
by metis
have 4:"(j<length xs) ⟶ ((times a xs)!j = (f a (xs!j)))"
using 1 by (metis Cons.hyps)
have 5:"(x#xs)!i = (xs!j)"
using Suc by (metis nth_Cons_Suc)
with 1 2 4  have "(j<length xs)
⟶ ((times a (x#xs))!i = (f a ((x#xs)!i)))"
by auto
with 3 have "(i <length (x#xs))
⟶ ((times a (x#xs))!i = (f a ((x#xs)!i)))"
by auto
then show ?thesis  by auto
qed
then show ?case by auto
qed

lemma simpl_times_elements:
assumes "(i<length xs)"
shows "((i<(length v)) ⟶ (times a v)!i = f a (v!i))"
using times_elements by auto

(*some lemmas which are used to prove theorems*)
lemma append_simpl: "i<(length xs) ⟶ (xs@ys)!i = (xs!i)"
using nth_append  by metis

lemma append_simpl2: "i ≥(length xs) ⟶ (xs@ys)!i = (ys!(i- (length xs)))"
using nth_append less_asym  leD  by metis

lemma append_simpl3:
assumes "i > (length y)"
shows " (i <((length (z#zs))*(length y)))
⟶ (i - (length y))< (length zs)*(length y)"
proof-
have "length (z#zs) = (length zs)+1"
by auto
then have "i <((length (z#zs))*(length y))
⟶ i <((length zs)+1)*(length y)"
by auto
then have 1: "i <((length (z#zs))*(length y))
⟶ (i <((length zs)*(length y)+ (length y)))"
by auto
have "i <((length zs)*(length y)+ (length y))
= ((i - (length y)) <((length zs)*(length y)))"
using assms by auto
then have "(i <((length (z#zs))*(length y)))
⟶ ((i - (length y)) <((length zs)*(length y)))"
by auto
then show ?thesis by auto
qed

lemma append_simpl4:
"(i > (length y))
⟶ ((i <((length (z#zs))*(length y))))
⟶ ((i - (length y))< (length zs)*(length y))"
using append_simpl3 by auto

lemma vec_vec_Tensor_simpl:
"i<(length y) ⟶ (vec_vec_Tensor (z#zs) y)!i = (times z y)!i"
proof-
have a: "vec_vec_Tensor (z#zs) y = (times z y)@(vec_vec_Tensor zs y)"
by auto
have b: "length (times z y) = (length y)" using preserving_length by auto
have "i<(length (times z y))
⟶ ((times z y)@(vec_vec_Tensor zs y))!i = (times z y)!i"
using append_simpl by metis
with b have "i<(length y)
⟶ ((times z y)@(vec_vec_Tensor zs y))!i = (times z y)!i"
by auto
with  a have "i<(length y)
⟶ (vec_vec_Tensor (z#zs) y)!i = (times z y)!i"
by auto
then show ?thesis by auto
qed

lemma vec_vec_Tensor_simpl2:
"(i ≥ (length y))
⟶ ((vec_vec_Tensor (z#zs) y)!i = (vec_vec_Tensor zs y)!(i- (length y)))"
using vec_vec_Tensor.simps(2) append_simpl2  preserving_length
by metis

lemma division_product:
assumes "(b::int)>0"
and "a ≥b"
shows " (a div b) = ((a - b) div b) + 1"
proof-
fix c
have "a -b ≥0"
using assms(2) by auto
have 1: "a - b = a + (-1)*b"
by auto
have "(b ≠ 0) ⟶ ((a + b * (-1)) div b = (-1) + a div b)"
using div_mult_self2 by metis
with 1 assms(1) have "((a - b) div b) = (-1) + a div b"
using less_int_code(1) by auto
then  have "(a div b) = ((a - b) div b) + 1"
by auto
then show ?thesis
by auto
qed

lemma int_nat_div:
"(int a) div (int b) = int ((a::nat) div b)"
by (metis zdiv_int)

lemma int_nat_eq:
assumes "int (a::nat) = int b"
shows "a = b"
using  assms of_nat_eq_iff by auto

lemma nat_div:
assumes "(b::nat) > 0"
and "a > b"
shows "(a div b) = ((a - b) div b) + 1"
proof-
fix x
have 1:"(int b)>0"
using assms(1) division_product by auto
moreover have "(int a)>(int b)"
using assms(2) by auto
with 1 have 2: "((int a) div (int b))
= (((int a) - (int b)) div (int b)) + 1"
using division_product by auto
from int_nat_div have 3: "((int a) div (int b)) = int ( a div b)"
by auto
from int_nat_div assms(2) have 4:
"(((int a) - (int b)) div (int b)) = int ((a - b) div b)"
by (metis (full_types) less_asym not_less of_nat_diff)
have "(int x) + 1 = int (x +1)"
by auto
with 2 3 4 have "int (a div b) = int (((a - b) div b) + 1)"
by auto
with int_nat_eq have "(a div b) = ((a - b) div b) + 1"
by auto
then show ?thesis by auto
qed

lemma mod_eq:
"(m::int) mod n = (m + (-1)*n) mod n"
using mod_mult_self1 by metis

lemma nat_mod_eq: "int m mod int n = int (m mod n)"

lemma nat_mod:
assumes  "(m::nat) > n"
shows "(m::nat) mod n = (m -n) mod n"
using assms mod_if not_less_iff_gr_or_eq by auto

lemma logic:
assumes "A ⟶ B"
and "¬A ⟶ B"
shows "B"
using assms(1) assms(2) by auto

theorem vec_vec_Tensor_elements:
assumes " (y ≠ [])"
shows
"∀i.((i<((length x)*(length y)))
⟶ ((vec_vec_Tensor x y)!i)
= f (x!(i div (length y))) (y!(i mod (length y))))"
apply(rule allI)
proof(induct x)
case Nil
have "(length [] = 0)"
by auto
also have "length (vec_vec_Tensor [] y) = 0"
using vec_vec_Tensor.simps(1) by auto
then have "i <(length (vec_vec_Tensor [] y)) ⟹ False"
by auto
moreover have "(vec_vec_Tensor [] y) = []"
by auto
moreover have
"(i<(length (vec_vec_Tensor [] y))) ⟶
((vec_vec_Tensor x y)!i) = f (x!(i div (length y))) (y!(i mod (length y)))"
by auto
then show ?case
by auto
next
case (Cons z zs)
have 1:"vec_vec_Tensor (z#zs) y = (times z y)@(vec_vec_Tensor zs y)"
by auto
have 2:"i<(length y)⟶((times z y)!i = f z (y!i))"
using times_elements by auto
moreover have 3:
"i<(length y)
⟶ (vec_vec_Tensor (z#zs) y)!i = (times z y)!i"
using vec_vec_Tensor_simpl by auto
moreover  have 35:
"i<(length y) ⟶ (vec_vec_Tensor (z#zs) y)!i = f z (y!i)"
using calculation(1) calculation(2) by metis
have 4:"(y ≠ []) ⟶ (length y) >0 "
by auto
have "(i <(length y)) ⟶  ((i div (length y)) = 0)"
by auto
then have  6:"(i <(length y)) ⟶ (z#zs)!(i div (length y)) = z"
using nth_Cons_0 by auto
then have 7:"(i <(length y)) ⟶ (i mod (length y)) = i"
by auto
with 2 6
have "(i < (length y))
⟶ (times z y)!i
= f  ((z#zs)!(i div (length y))) (y! (i mod (length y)))"
by auto
with 3 have step1:
"((i < (length y))
⟶ ((i<((length x)*(length y))
⟶ ((vec_vec_Tensor (z#zs) y)!i
=  f
((z#zs)!(i div (length y)))
(y! (i mod (length y)))))))"
by auto
have "((length y) ≤ i) ⟶ (i - (length y)) ≥ 0"
by auto
have step2:
"((length y) < i)
⟶ ((i < (length (z#zs)*(length y)))
⟶((vec_vec_Tensor (z#zs) y)!i)
= f
((z#zs)!(i div (length y)))
(y!(i mod (length y))))"
proof-
have "(length y)>0"
using assms by auto
then have 1:
"(i > (length y))
⟶(i div (length y)) = ((i-(length y)) div (length y)) + 1"
using nat_div by auto
have "zs!j = (z#zs)!(j+1)"
by auto
then have
"(zs!((i - (length y)) div (length y)))
= (z#zs)!(((i - (length y)) div (length y))+1)"
by auto
with 1 have 2:
"(i > (length y))
⟶ (zs!((i - (length y)) div (length y))
= (z#zs)!(i div (length y)))"
by auto
have "(i > (length y))
⟶((i mod (length y))
= ((i - (length y)) mod (length y)))"
using nat_mod by auto
then have 3:
"(i > (length y))
⟶((y! (i mod (length y)))
= (y! ((i - (length y)) mod (length y))))"
by auto
have 4:"(i > (length y))
⟶(vec_vec_Tensor (z#zs) y)!i
= (vec_vec_Tensor zs y)!(i- (length y))"
using vec_vec_Tensor_simpl2  by auto
have 5: "(i > (length y))
⟶((i <((length (z#zs))*(length y))))
= (i - (length y)< (length zs)*(length y))"
by auto
then have 6:
"∀i.((i<((length zs)*(length y)))
⟶ ((vec_vec_Tensor zs y)!i)
= f
(zs!(i div (length y)))
(y!(i mod (length y))))"
using Cons.hyps by auto
with 5 have "(i > (length y))
⟶ ((i<((length (z#zs))*(length y)))
⟶ ((vec_vec_Tensor zs y)!(i -(length y)))
= f
(zs!((i -(length y)) div (length y)))
(y!((i -(length y)) mod (length y))))
= ((i<((length zs)*(length y)))
⟶ ((vec_vec_Tensor zs y)!i)
= f
(zs!(i div (length y)))
(y!(i mod (length y))))"
by auto
with 6 have
"(i > (length y))
⟶((i<((length (z#zs))*(length y)))
⟶ ((vec_vec_Tensor zs y)!(i -(length y)))
= f
(zs!((i -(length y)) div (length y)))
(y!((i -(length y))  mod (length y))))"
by auto
with 2 3 4 have
"(i > (length y))
⟶((i<((length (z#zs))*(length y)))
⟶((vec_vec_Tensor (z#zs) y)!i)
=  f
((z#zs)!(i div (length y)))
(y!(i mod (length y))))"
by auto
then show ?thesis  by auto
qed
have "((length y) = i)
⟶ ((i < (length (z#zs)*(length y)))
⟶ ((vec_vec_Tensor (z#zs) y)!i)
= f
((z#zs)!(i div (length y)))
(y!(i mod (length y))))"
proof-
have 1:"(i = (length y))
⟶ ((vec_vec_Tensor (z#zs) y)!i)
= (vec_vec_Tensor zs y)!0"
using vec_vec_Tensor_simpl2   by auto
have 2:"(i = length y) ⟶ (i mod (length y)) = 0"
by auto
have 3:"(i = length y) ⟶ (i div (length y)) = 1"
using 4 assms div_self less_numeral_extra(3)
by auto
have 4: "(i = length y)
⟶ ((i < (length (z#zs))*(length y))
= (0 < (length zs)*(length y)))"
by auto
have "(z#zs)!1 = (zs!0)"
by auto
with 3 have 5:" (i = length y)
⟶ ((z#zs)!(i div (length y))) = (zs!0)"
by auto
have " ∀i.((i < (length zs)*(length y))
⟶((vec_vec_Tensor (zs) y)!i)
= f
((zs)!(i div (length y)))
(y!(i mod (length y))))"
using Cons.hyps by auto
with 4 have 6:"(i = length y)
⟶ ((0 < ((length zs)*(length y)))
⟶ (((vec_vec_Tensor (zs) y)!0)
= f ((zs)!0) (y!0)))
= ((i < ((length zs)*(length y)))
⟶(((vec_vec_Tensor zs y)!i)
= f
((zs)!(i div (length y)))
(y!(i mod (length y)))))"
by auto
have 7: "(0 div (length y)) = 0"
by auto
have 8: " (0 mod (length y)) = 0"
by auto
have 9: "(0 < ((length zs)*(length y)))
⟶ ((vec_vec_Tensor zs y)!0)
= f (zs!0) (y!0)"
using 7 8 Cons.hyps by auto
with  4 5 8 have "(i = length y)
⟶ ((i < (length (z#zs))*(length y))
⟶ (((vec_vec_Tensor (zs) y)!0)
= f ((zs)!0) (y!0)))"
by auto
with 1 2 5 have "(i = length y)
⟶ ((i < (length (z#zs))*(length y))
⟶ (((vec_vec_Tensor ((z#zs)) y)!i)
= f
((z#zs)!(i div (length y)))
(y!(i mod (length y)))))"
by auto
then show ?thesis by auto
qed
with step2 have step4:
"(i ≥ (length y))
⟶  ((i < (length (z#zs))*(length y))
⟶ (((vec_vec_Tensor ((z#zs)) y)!i)
= f
((z#zs)!(i div (length y)))
(y!(i mod (length y)))))"
by auto
have "(i < (length y)) ∨ (i ≥ (length y))"
by auto
with step1 step4 have
"((i < (length (z#zs))*(length y))
⟶ (((vec_vec_Tensor ((z#zs)) y)!i)
= f
((z#zs)!(i div (length y)))
(y!(i mod (length y)))))"
using logic by (metis "6" "7" 35)
then show ?case by auto
qed

text‹a few more results that will be used later on›

lemma nat_int:  "nat (int x + int y) = x + y"

lemma int_nat_equiv: "(x > 0) ⟶ (nat ((int x) + -1)+1) = x"
proof-
have "1 = nat (int 1)"
by auto
have "-1 = -int 1"
by auto
then have 1:"(nat ((int x) + -1)+1)
= (nat ((int x) + -1) + (nat (int 1)))"
by auto
then have 2:"(x > 0)
⟶ nat ((int x) + -1 ) + (nat (int 1))
=  (nat (((int x)  + -1) + (int 1)))"
have "(nat (((int x)  + -1) + (int 1))) = (nat ((int x) + -1 + (int 1)))"
by auto
then have "(nat (((int x)  + -1) + (int 1))) = (nat ((int x)))"
by auto
then have "(nat (((int x)  + -1) + (int 1))) = x"
by auto
with 1 2 have " (x > 0) ⟶ nat ((int x) + -1 ) + 1 = x"
by auto
then show ?thesis by auto
qed

lemma list_int_nat: "(k>0) ⟶ ((x#xs)!k = xs!(nat ((int k)+-1)))"
proof-
fix  j
have " ((x#xs)!(k+1) = xs!k)"
by auto
have "j = (k+1) ⟶ (nat ((int j)+-1)) = k"
by auto
moreover have "(nat ((int j)+-1)) = k
⟶ ((nat ((int j)+-1)) + 1) = (k +1)"
by auto
moreover have "(j>0)⟶(((nat ((int j)+-1)) + 1) = j)"
using  int_nat_equiv by (auto)
moreover have "(k>0) ⟶ ((x#xs)!k = xs!(nat ((int k)+-1)))"
using Suc_eq_plus1 int_nat_equiv nth_Cons_Suc by (metis)
from this show ?thesis by auto
qed

lemma row_length_eq:
"(mat  (row_length (a#b#N))  (length (a#b#N)) (a#b#N))
⟶
(row_length (a#b#N) = (row_length (b#N)))"
proof-
have "(mat  (row_length (a#b#N))  (length (a#b#N)) (a#b#N))
⟶ (b ∈ set (a#b#M))"
by auto
moreover have
"(mat  (row_length (a#b#N))  (length (a#b#N)) (a#b#N))
⟶ (Ball (set (a#b#N)) (vec (row_length (a#b#N))))"
using mat_def by metis
moreover have "(mat  (row_length (a#b#N))  (length (a#b#N)) (a#b#N))
⟶ (b ∈ (set (a#b#N)))
⟶ (vec (row_length (a#b#N)) b)"
by (metis calculation(2))
then have "(mat  (row_length (a#b#N))  (length (a#b#N)) (a#b#N))
⟶ (length b) = (row_length (a#b#N))"
using vec_def by auto
then have "(mat  (row_length (a#b#N))  (length (a#b#N)) (a#b#N))
⟶ (row_length (b#N))
= (row_length (a#b#N))"
using row_length_def by auto
then show ?thesis by auto
qed

text‹The following theorem tells us the relationship between entries of
vec\_mat\_Tensor v M and entries of v and M respectivety›

theorem vec_mat_Tensor_elements:
"∀i.∀j.
(((i<((length v)*(row_length M)))
∧(j < (length M)))
∧(mat (row_length M) (length M) M)
⟶ ((vec_mat_Tensor v M)!j!i)
= f (v!(i div (row_length M))) (M!j!(i mod (row_length M))))"
apply(rule allI)
apply(rule allI)
proof(induct M)
case Nil
have "row_length [] = 0"
using row_length_def by auto
from this
have "(length v)*(row_length []) = 0"
by auto
from this
have "((i<((length v)*(row_length [])))∧(j < (length []))) ⟶ False"
by auto
moreover have "vec_mat_Tensor v [] = []"
by auto
moreover have "(((i<((length v)*(row_length [])))∧(j < (length [])))
⟶ ((vec_mat_Tensor v [])!j!i)
= f (v!(i div (row_length []))) ([]!j!(i mod (row_length []))))"
by auto
from this
show ?case by auto
next
case (Cons a M)
have "(((i<((length v)*(row_length (a#M))))
∧(j < (length (a#M))))
∧(mat (row_length (a#M)) (length (a#M)) (a#M))
⟶ ((vec_mat_Tensor v (a#M))!j!i)
= f
(v!(i div (row_length (a#M))))
((a#M)!j!(i mod (row_length (a#M)))))"
proof(cases a)
case Nil
have "row_length ([]#M) = 0"
using row_length_def by auto
then have 1:"(length v)*(row_length ([]#M)) = 0"
by auto
then have "((i<((length v)*(row_length ([]#M))))
∧(j < (length ([]#M)))) ⟶ False"
by auto
moreover have
"(((i<((length v)*(row_length ([]#M))))
∧(j < (length ([]#M))))
⟶ ((vec_mat_Tensor v ([]#M))!j!i) =
f
(v!(i div (row_length ([]#M))))
([]!j!(i mod (row_length ([]#M)))))"
using calculation by auto
then show ?thesis using Nil 1 less_nat_zero_code by (metis )
next
case (Cons x xs)
have 1:"(a#M)!(j+1) = M!j" by auto
have "(((i<((length v)*(row_length M)))
∧(j < (length M)))
∧(mat (row_length M) (length M) M)
⟶ ((vec_mat_Tensor v M)!j!i) = f
(v!(i div (row_length M)))
(M!j!(i mod (row_length M))))"
using Cons.hyps by auto
have 2: "(row_length (a#M)) = (length a)"
using row_length_def by auto
then have 3:"(i< (row_length (a#M))*(length v))
= (i < (length a)*(length v))"
by auto
have "a ≠ []"
using Cons by auto
then have 4:
"∀i.((i < (length a)*(length v))
⟶  ((vec_vec_Tensor v a)!i) = f
(v!(i div (length a)))
(a!(i mod (length a))))"
using vec_vec_Tensor_elements Cons.hyps mult.commute
have "(vec_mat_Tensor v (a#M))!0 = (vec_vec_Tensor v a)"
using vec_mat_Tensor.simps(2) by auto
with 2 4 have 5:
"∀i.((i < (row_length (a#M))*(length v))
⟶  ((vec_mat_Tensor v (a#M))!0!i)
= f
(v!(i div (row_length (a#M))))
((a#M)!0!(i mod (row_length (a#M)))))"
by auto
have "length (a#M)>0"
by auto
with 5 have 6:
"(j = 0)⟶
((((i < (row_length (a#M))*(length v))
∧(j < (length (a#M))))
∧(mat (row_length (a#M)) (length (a#M)) (a#M))
⟶  ((vec_mat_Tensor v (a#M))!j!i)
= f
(v!(i div (row_length (a#M))))
((a#M)!j!(i mod (row_length (a#M))))))"
by auto
have "(((i < (row_length (a#M))*(length v))
∧(j < (length (a#M))))
∧(mat (row_length (a#M)) (length (a#M)) (a#M))
⟶
((vec_mat_Tensor v (a#M))!j!i) =
f
(v!(i div (row_length (a#M))))
((a#M)!j!(i mod (row_length (a#M)))))"
proof(cases M)
case Nil
have "(length (a#[])) = 1"
by auto
then have "(j<(length (a#[]))) = (j = 0)"
by auto
then have "((((i < (row_length (a#[]))*(length v))
∧(j < (length (a#[]))))
∧ (mat (row_length (a#[])) (length (a#[])) (a#[]))
⟶  ((vec_mat_Tensor v (a#[]))!j!i)
= f
(v!(i div (row_length (a#[]))))
((a#[])!j!(i mod (row_length (a#[]))))))"
using 6 Nil by auto
then show ?thesis using Nil by auto
next
case (Cons b N)
have 7:"(mat  (row_length (a#b#N))  (length (a#b#N)) (a#b#N))
⟶ row_length (a#b#N) = (row_length (b#N))"
using row_length_eq by metis
have 8: "(j>0)
⟶ ((vec_mat_Tensor v (b#N))!(nat ((int j)+-1)))
= (vec_mat_Tensor v (a#b#N))!j"
using vec_mat_Tensor.simps(2) using list_int_nat by metis
have 9: "(j>0)
⟶ (((i < (row_length (b#N))*(length v))
∧((nat ((int j)+-1)) < (length (b#N))))
∧(mat (row_length (b#N)) (length (b#N)) (b#N))
⟶
((vec_mat_Tensor v (b#N))!(nat ((int j)+-1))!i)
= f
(v!(i div (row_length (b#N))))
((b#N)!(nat ((int j)+-1))!(i mod (row_length (b#N)))))"
using Cons.hyps Cons mult.commute by metis
have "(j>0) ⟶ ((nat ((int j) + -1)) < (length (b#N)))
⟶ ((nat ((int j) + -1) + 1) < length (a#b#N))"
by auto
then have
"(j>0)
⟶ ((nat ((int j) + -1)) < (length (b#N))) = (j < length (a#b#N))"
by auto
then have
"(j>0)
⟶ (((i < (row_length (b#N))*(length v)) ∧ (j < length (a#b#N)))
∧(mat (row_length (b#N)) (length (b#N)) (b#N))   ⟶
((vec_mat_Tensor v (b#N))!(nat ((int j)+-1))!i)
= f
(v!(i div (row_length (b#N))))
((b#N)!(nat ((int j)+-1))!(i mod (row_length (b#N)))))"
using Cons.hyps Cons mult.commute by metis
with 8 have "(j>0)
⟶ (((i < (row_length (b#N))*(length v))
∧ (j < length (a#b#N)))
∧ (mat (row_length (b#N)) (length (b#N)) (b#N))
⟶
((vec_mat_Tensor v (a#b#N))!j!i)
= f
(v!(i div (row_length (b#N))))
((b#N)!(nat ((int j)+-1))!(i mod (row_length (b#N)))))"
by auto
also have "(j>0) ⟶ (b#N)!(nat ((int j)+-1)) = (a#b#N)!j"
using list_int_nat by metis
moreover have " (j>0) ⟶
(((i < (row_length (b#N))*(length v))
∧ (j < length (a#b#N)))
∧ (mat (row_length (b#N)) (length (b#N)) (b#N))
⟶
((vec_mat_Tensor v (a#b#N))!j!i)
= f
(v!(i div (row_length (b#N))))
((a#b#N)!j!(i mod (row_length (b#N)))))"
by (metis calculation(1) calculation(2))
then have
"(j>0)
⟶ (((i < (row_length (b#N))*(length v))
∧ (j < length (a#b#N)))
∧ (mat (row_length (a#b#N)) (length (a#b#N)) (a#b#N))
⟶
((vec_mat_Tensor v (a#b#N))!j!i)
= f
(v!(i div (row_length (b#N`