(* 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" by(induction v)(auto simp add:left_id) lemma times_vector_id: "times v [id] = [v]" by(simp add:right_id) 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" by(induction v)(auto simp add:left_id) lemma vec_vec_Tensor_right_id: "vec_vec_Tensor v [id] = v" by(induction v)(auto simp add:right_id) theorem vec_vec_Tensor_length : "(length(vec_vec_Tensor x y)) = (length x)*(length y)" by(induction x)(auto simp add: preserving_length) theorem vec_length: assumes "vec m x" and "vec n y" shows "vec (m*n) (vec_vec_Tensor x y)" apply(simp add:vec_def) apply(simp add:vec_vec_Tensor_length) 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" by(induction v)(auto simp add: times_scalar_id) lemma vec_mat_Tensor_matrix_id: "vec_mat_Tensor v [[id]] = [v]" by(induction v)(auto simp add: right_id) 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" by(induction xs)(auto simp add:times_scalar_id) lemma Tensor_right_id: " xs ⊗ [[id]] = xs" by(induction xs)(auto simp add: vec_vec_Tensor_right_id) 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)" by (simp add: of_nat_mod) 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" using nat_int of_nat_add by auto 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)))" using of_nat_add nat_int by auto 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 by (simp add: mult.commute vec_vec_Tensor_elements) 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)))) ((a#b#N)!j!(i mod (row_length (b#N)))))" using reduct_matrix by (metis) moreover have "(mat (row_length (a#b#N)) (length (a#b#N)) (a#b#N)) ⟶(row_length (b#N)) = (row_length (a#b#N))" by (metis "7" Cons) moreover have 10:"(j>0) ⟶ (((i < (row_length (a#b#N))*(length v)) ∧(j < length (a#b#N))) ∧