Theory Matrix_Tensor.Matrix_Tensor
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
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)))
∧(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 (a#b#N))))
((a#b#N)!j!(i mod (row_length (a#b#N)))))"
by (metis calculation(3) calculation(4))
have "(j = 0) ∨ (j > 0)"
by auto
with 6 10 logic have
"(((i < (row_length (a#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 (a#b#N))))
((a#b#N)!j!(i mod (row_length (a#b#N)))))"
using Cons by metis
from this show ?thesis by (metis Cons)
qed
from this show ?thesis by (metis mult.commute)
qed
from this show ?case by auto
qed
text‹The following theorem tells us about the relationship between
entries of tensor products of two matrices and the entries of matrices›
theorem matrix_Tensor_elements:
fixes M1 M2
shows
"∀i.∀j.(((i<((row_length M1)*(row_length M2)))
∧(j < (length M1)*(length M2)))
∧(mat (row_length M1) (length M1) M1)
∧(mat (row_length M2) (length M2) M2)
⟶ ((M1 ⊗ M2)!j!i) =
f
(M1!(j div (length M2))!(i div (row_length M2)))
(M2!(j mod length M2)!(i mod (row_length M2))))"
apply(rule allI)
apply(rule allI)
proof(induct M1)
case Nil
have "(row_length []) = 0"
using row_length_def by auto
then have "(i< ((row_length [])*(row_length M2))) ⟶ False"
by auto
from this have "((i<((row_length [])*(row_length M2)))
∧(j < (length [])*(length M2)))
∧(mat (row_length []) (length []) [])
∧(mat (row_length M2) (length M2) M2)
⟶ False"
by auto
moreover have "([] ⊗ M2) = []"
by auto
moreover have
"((i<((row_length [])*(row_length M2)))
∧(j < (length [])*(length M2)))
∧(mat (row_length []) (length []) [])
∧(mat (row_length M2) (length M2) M2)
⟶ (([] ⊗ M2)!j!i) =
f
([]!(j div (length []))!(i div (row_length M2)))
(M2!(j mod length [])!(i mod (row_length M2)))"
by auto
then show ?case by auto
next
case (Cons v M)
fix a
have 0:"(v#M) ⊗ M2 = (vec_mat_Tensor v M2)@(Tensor M M2)"
by auto
then have 1:
"(j<(length M2)) ⟶ ( ((v#M) ⊗ M2)!j = (vec_mat_Tensor v M2)!j)"
using append_simpl vec_mat_Tensor_length by metis
have " (((i<((length a)*(row_length M2)))
∧(j < (length M2)))∧(mat (row_length M2) (length M2) M2)
⟶ ((vec_mat_Tensor a M2)!j!i) = f (a!(i div (row_length M2))) (M2!j!(i mod (row_length M2))))"
using vec_mat_Tensor_elements by auto
have "(j < (length M2)) ⟶ (j div (length M2)) = 0"
by auto
then have 2:"(j < (length M2)) ⟶ (v#M)!(j div (length M2)) = v"
by auto
have "(j < (length M2)) ⟶ (j mod (length M2)) = j"
by auto
moreover have "(j < (length M2)) ⟶ (v#M)!(j mod (length M2)) = (v#M)!j"
by auto
have step0:
"(j < (length M2)) ⟶
(((i<((length v)*(row_length M2)))
∧(j < (length M2) * (length (v#M))))
∧(mat (row_length M2) (length M2) M2)
⟶ ((Tensor (v#M) M2)!j!i)
= f
((v#M)!(j div (length M2))!(i div (row_length M2)))
(M2!(j mod (length M2))!(i mod (row_length M2))))"
using 2 1 calculation(1) vec_mat_Tensor_elements by auto
have step1:
"(j < (length M2))
⟶ (((i<((row_length (v#M))*(row_length M2)))
∧(j < (length (v#M))*(length M2)))
∧(mat (row_length (v#M)) (length (v#M)) (v#M))
∧(mat (row_length M2) (length M2) M2)
⟶ ((Tensor (v#M) M2)!j!i) =
f
((v#M)!(j div (length M2))!(i div (row_length M2)))
(M2!(j mod (length M2))!(i mod (row_length M2))))"
using row_length_def step0 by auto
from 0 have 3:
"(j ≥ (length M2)) ⟶ ((v#M) ⊗ M2)!j = (M ⊗ M2)!(j - (length M2))"
using vec_mat_Tensor_length add.commute append_simpl2 by metis
have 4:
"(j ≥ (length M2)) ⟶
(((i<((row_length M)*(row_length M2)))
∧((j-(length M2)) < (length M)*(length M2)))
∧(mat (row_length M) (length M) M)
∧(mat (row_length M2) (length M2) M2)
⟶ ((M ⊗ M2)!(j-(length M2))!i)
= f
(M!((j-(length M2)) div (length M2))!(i div (row_length M2)))
(M2!((j-(length M2)) mod length M2)!(i mod (row_length M2))))"
using Cons.hyps by auto
moreover have "(mat (row_length (v#M)) (length (v#M)) (v#M))
⟶(mat (row_length M) (length M) M)"
using reduct_matrix by auto
moreover have 5:
"(j ≥ (length M2))
⟶ (((i<((row_length M)*(row_length M2)))
∧((j-(length M2)) < (length M)*(length M2)))
∧(mat (row_length (v#M)) (length (v#M)) (v#M))
∧(mat (row_length M2) (length M2) M2)
⟶ ((M ⊗ M2)!(j-(length M2))!i)
= f
(M!((j-(length M2)) div (length M2))!(i div (row_length M2)))
(M2!((j-(length M2)) mod length M2)!(i mod (row_length M2))))"
using 4 calculation(3) by metis
have "(((j-(length M2)) < (length M)*(length M2)))
⟶ (j < ((length M)+1)*(length M2))"
by auto
then have 6:
"(((j-(length M2)) < (length M)*(length M2)))
⟶
(j < ((length (v#M))*(length M2)))"
by auto
have 7:
"(j ≥ (length M2))
⟶
((j-(length M2)) div (length M2)) = ((j div (length M2)) - 1)"
using add_diff_cancel_left' div_add_self1 div_by_0
le_imp_diff_is_add add.commute zero_diff
by metis
then have 8:
"(j ≥ (length M2))
⟶
M!((j-(length M2)) div (length M2))
= M!((j div (length M2)) - 1)"
by auto
have step2:
"(j ≥ (length M2))
⟶
(((i<((row_length (v#M))*(row_length M2)))
∧(j < (length (v#M))*(length M2)))
∧(mat (row_length (v#M)) (length (v#M)) (v#M))
∧(mat (row_length M2) (length M2) M2))
⟶(((v#M) ⊗ M2)!j!i) =
f
((v#M)!(j div (length M2))!(i div (row_length M2)))
(M2!(j mod length M2)!(i mod (row_length M2)))"
proof(cases M2)
case Nil
have "(0 = ((row_length (v#M))*(row_length M2)))"
using row_length_def Nil mult_0_right by auto
then have "(i < ((row_length (v#M))*(row_length M2))) ⟶ False"
by auto
then have " (j ≥ (length M2))
⟶(((i<((row_length (v#M))*(row_length M2)))
∧(j < (length (v#M))*(length M2)))
∧(mat (row_length (v#M)) (length (v#M)) (v#M))
∧(mat (row_length M2) (length M2) M2))
⟶ False"
by auto
then show ?thesis by auto
next
case (Cons w N)
fix k
have "(k < (length M))∧ (k ≥ 1) ⟶ M!(k - 1) = (v#M)!k"
using not_one_le_zero nth_Cons' by auto
have "(j ≥ (length (w#N))) ⟶ (j div (length (w#N))) ≥ 1"
using div_le_mono div_self length_0_conv neq_Nil_conv by metis
moreover have "(j ≥ (length (w#N))) ⟶ (j div (length (w#N)))- 1 ≥ 0"
by auto
moreover have "(j ≥ (length (w#N)))
⟶ M!((j div (length (w#N)))- 1 )
= (v#M)!(j div (length (w#N)))"
using calculation(1) not_one_le_zero nth_Cons' by auto
from this 7 have 9:" (j ≥ (length (w#N)))
⟶ M!((j-(length (w#N))) div (length (w#N)))
= (v#M)!(j div (length (w#N)))"
using Cons by auto
have 10: "(j ≥ (length (w#N)))
⟶ ((j-(length (w#N))) mod (length (w#N)))
= (j mod(length (w#N)))"
using mod_if not_less by auto
with 5 9 have
"(j ≥ (length (w#N))) ⟶
((i<((row_length M)*(row_length (w#N))))
∧((j-(length (w#N))) < (length M)*(length (w#N)))
∧(mat (row_length (v#M)) (length (v#M)) (v#M))
∧(mat (row_length (w#N)) (length (w#N)) (w#N)))
⟶ (((M ⊗ (w#N))!(j-(length (w#N)))!i)
= f
((v#M)!(j div (length (w#N)))!(i div (row_length (w#N))))
((w#N)!(j mod length (w#N))!(i mod (row_length (w#N)))))"
using Cons by auto
then have
"(j ≥ (length (w#N))) ⟶
((i<((row_length M)*(row_length (w#N))))
∧(j <(length (v#M))*(length (w#N)))
∧(mat (row_length (v#M)) (length (v#M)) (v#M))
∧(mat (row_length (w#N)) (length (w#N)) (w#N)))
⟶ (((M ⊗ (w#N))!(j-(length (w#N)))!i)
= f
((v#M)!(j div (length (w#N)))!(i div (row_length (w#N))))
((w#N)!(j mod length (w#N))!(i mod (row_length (w#N)))))"
using 6 by auto
then have 11:
"(j ≥ (length (w#N))) ⟶
((i<((row_length M)*(row_length (w#N))))
∧(j <(length (v#M))*(length (w#N)))
∧(mat (row_length (v#M)) (length (v#M)) (v#M))
∧(mat (row_length (w#N)) (length (w#N)) (w#N)))
⟶ (((v#M) ⊗ (w#N))!j!i) =
f
((v#M)!(j div (length (w#N)))!(i div (row_length (w#N))))
((w#N)!(j mod length (w#N))!(i mod (row_length (w#N))))"
using 3 Cons by auto
have
"(j ≥ (length (w#N))) ⟶
((i<((row_length (v#M))*(row_length (w#N))))
∧(j <(length (v#M))*(length (w#N)))
∧(mat (row_length (v#M)) (length (v#M)) (v#M))
∧(mat (row_length (w#N)) (length (w#N)) (w#N)))
⟶ (((v#M) ⊗ (w#N))!j!i)
= f
((v#M)!(j div (length (w#N)))!(i div (row_length (w#N))))
((w#N)!(j mod length (w#N))!(i mod (row_length (w#N))))"
proof(cases M)
case Nil
have Nil0:"(length (v#[])) = 1"
by auto
then have Nil1:
"(j <(length (v#[]))*(length (w#N))) = (j< (length (w#N)))"
by (metis Nil nat_mult_1)
have
"row_length (v#[]) = (length v)"
using row_length_def by auto
then have Nil2:
"(i<((row_length (v#M))*(row_length (w#N))))
= (i<((length v)*(row_length (w#N))))"
using Nil by auto
then have "(j< (length (w#N))) ⟶ (j div (length (w#N))) = 0"
by auto
from this have Nil3:
"(j< (length (w#N))) ⟶ (v#M)!(j div (length (w#N))) = v"
using Nil by auto
then have Nil4:
"(j< (length (w#N))) ⟶ (j mod (length (w#N))) = j"
by auto
then have Nil5:"(v#M) ⊗ (w#N) = vec_mat_Tensor v (w#N)"
using Nil Tensor.simps(2) Tensor.simps(1)
by auto
from vec_mat_Tensor_elements have
"(((i<((length v)*(row_length (w#N))))
∧(j < (length (w#N))))
∧(mat (row_length (w#N)) (length (w#N)) (w#N))
⟶ ((vec_mat_Tensor v (w#N))!j!i)
= f
(v!(i div (row_length (w#N))))
((w#N)!j!(i mod (row_length (w#N)))))"
by metis
then have
"((i<((row_length (v#M))*(row_length (w#N))))
∧(j < ((length (v#M))*(length (w#N))))
∧(mat (row_length (w#N)) (length (w#N)) (w#N))
⟶ ((vec_mat_Tensor v (w#N))!j!i)
= f (v!(i div (row_length (w#N))))
((w#N)!j!(i mod (row_length (w#N)))))"
using Nil1 Nil2 Nil by auto
then have
"((i<((row_length (v#M))*(row_length (w#N))))
∧(j < ((length (v#M))*(length (w#N))))
∧(mat (row_length (w#N)) (length (w#N)) (w#N))
⟶ (((v#M)⊗(w#N))!j!i)
= f
((v#M)!(j div (length (w#N)))!(i div (row_length (w#N))))
((w#N)!(j mod (length (w#N)))!(i mod (row_length (w#N)))))"
using Nil3 Nil4 Nil5 Nil by auto
then have
"((i<((row_length (v#M))*(row_length (w#N))))
∧(j < ((length (v#M))*(length (w#N))))
∧(mat (row_length (v#M)) (length (v#M)) (v#M))
∧(mat (row_length (w#N)) (length (w#N)) (w#N))
⟶ (((v#M)⊗(w#N))!j!i)
= f
((v#M)!(j div (length (w#N)))!(i div (row_length (w#N))))
((w#N)!(j mod (length (w#N)))!(i mod (row_length (w#N)))))" by auto
from this show ?thesis by auto
next
case (Cons u P)
have "(mat (row_length (v#M)) (length (v#M)) (v#M)) ⟶ (row_length (v#M)) = (row_length M)"
using Cons row_length_eq by metis
from this 11 show ?thesis by auto
qed
from this show ?thesis using Cons by auto
qed
have "(j<(length M2)) ∨ (j ≥ (length M2))" by auto
from this step1 step2 logic have
"(((i<((row_length (v#M))*(row_length M2)))
∧(j < (length M2) * (length (v#M))))
∧(mat (row_length (v#M)) (length (v#M)) (v#M))
∧(mat (row_length M2) (length M2) M2)
⟶ ( ((v#M) ⊗ M2)!j!i)
= f
((v#M)!(j div (length M2))!(i div (row_length M2)))
(M2!(j mod (length M2))!(i mod (row_length M2))))"
using mult.commute by metis
from this show ?case by (metis mult.commute)
qed
text‹we restate the theorem in two different forms for convenience
of reuse›
theorem effective_matrix_tensor_elements:
" (((i<((row_length M1)*(row_length M2)))
∧(j < (length M1)*(length M2)))
∧(mat (row_length M1) (length M1) M1)
∧(mat (row_length M2) (length M2) M2)
⟹ ((M1 ⊗ M2)!j!i)
= f (M1!(j div (length M2))!(i div (row_length M2)))
(M2!(j mod length M2)!(i mod (row_length M2))))"
using matrix_Tensor_elements by auto
theorem effective_matrix_tensor_elements2:
assumes " i<(row_length M1)*(row_length M2)"
and "j < (length M1)*(length M2)"
and "mat (row_length M1) (length M1) M1"
and "mat (row_length M2) (length M2) M2"
shows "(M1 ⊗ M2)!j!i =
(M1!(j div (length M2))!(i div (row_length M2)))
* (M2!(j mod length M2)!(i mod (row_length M2)))"
using assms matrix_Tensor_elements by auto
text‹the following lemmas are useful in proving associativity of tensor
products›
lemma div_left_ineq:
assumes "(x::nat) < y*z"
shows " (x div z) < y"
proof(rule ccontr)
assume 0: " ¬((x div z) < y)"
then have 1:" x div z ≥ y"
by auto
then have 2:"(x div z)*z ≥ y*z"
by auto
then have 3:"(x div z)*z + (x mod z) = z"
using div_mult_mod_eq
add_leD1 assms minus_mod_eq_div_mult [symmetric] le_diff_conv2 mod_less_eq_dividend not_less
by metis
then have 4:"(x div z)*z ≤ z"
by auto
then have 5:"z ≥ y*z"
using 2 by auto
then have 6:"z div z ≥ (y*z) div z"
by auto
then have "(y*z) div z ≤ 1"
by auto
with 6 have "1 ≥ y"
using 1 3 assms div_self less_nat_zero_code mult_zero_left
mult.commute mod_div_mult_eq
by auto
then have 7:"(y = 0) ∨ (y = 1)"
by auto
have "(y = 0 ) ⟹ x<0"
using assms by auto
moreover have "x ≥ 0"
by auto
then have 8:"(y = 0) ⟹ False"
using calculation less_nat_zero_code by auto
moreover have "(y = 1) ⟹ ( x < z)"
using assms by auto
then have "(y = 1) ⟹ (x div z) = 0"
by (metis div_less)
then have "(y = 1) ⟹(x div z) < y"
by auto
then have "(y = 1) ⟹ False"
using 0 by auto
then show False using 7 8 by auto
qed
lemma div_right_ineq:
assumes "(x::nat) < y*z"
shows " (x div y) < z"
using assms div_left_ineq mult.commute by (metis)
text‹In the following theorem, we obtain columns of vec$\_$mat$\_$Tensor of
a vector v and a matrix M in terms of the vector v and columns of the
matrix M›
lemma col_vec_mat_Tensor_prelim:
" ∀j.(j < (length M)
⟶
col (vec_mat_Tensor v M) j = vec_vec_Tensor v (col M j))"
unfolding col_def
apply(rule allI)
proof(induct M)
case Nil
show ?case using Nil by auto
next
case (Cons w N)
have Cons_1:"vec_mat_Tensor v (w#N)
= (vec_vec_Tensor v w)#(vec_mat_Tensor v N)"
using vec_mat_Tensor.simps Cons by auto
then show ?case
proof(cases j)
case 0
have "vec_mat_Tensor v (w#N)!0 = (vec_vec_Tensor v w)"
by auto
then show ?thesis using 0 by auto
next
case (Suc k)
have " vec_mat_Tensor v (w#N)!j = (vec_mat_Tensor v N)!(k)"
using Cons_1 Suc by auto
moreover have "j < length (w#N) ⟹ k < length N"
using Suc by (metis length_Suc_conv not_less_eq)
moreover then have "k < length (N)
⟹ (vec_mat_Tensor v N)!k = vec_vec_Tensor v (N!k)"
using Cons.hyps by auto
ultimately show ?thesis using Suc by auto
qed
qed
lemma col_vec_mat_Tensor:fixes j M v
assumes "j < (length M)"
shows "col (vec_mat_Tensor v M) j = vec_vec_Tensor v (col M j)"
using col_vec_mat_Tensor_prelim assms by auto
lemma col_formula:
fixes M1 and M2
shows "∀j.((j < (length M1)*(length M2))
∧ (mat (row_length M1) (length M1) M1)
∧ (mat (row_length M2) (length M2) M2)
⟶ col (M1 ⊗ M2) j
= vec_vec_Tensor
(col M1 (j div length M2))
(col M2 (j mod length M2)))"
apply (rule allI)
proof(induct M1)
case Nil
show ?case using Nil by auto
next
case (Cons v M)
have "j < (length (v#M))*(length M2)
∧ mat (row_length (v # M)) (length (v # M)) (v # M)
∧ mat (row_length M2) (length M2) M2 ⟹
(col (v # M ⊗ M2) j
= vec_vec_Tensor
(col (v # M) (j div length M2))
(col M2 (j mod length M2)))"
proof-
fix k
assume 0:"j < (length (v#M))*(length M2)
∧ mat (row_length (v # M)) (length (v # M)) (v # M)
∧ mat (row_length M2) (length M2) M2"
then have 1:"mat (row_length M) (length M) M"
by (metis reduct_matrix)
have "j < (1+ length M)*(length M2)"
using 0 by auto
then have "j < (length M2)+ (length M)*(length M2)"
by auto
then have 2:"j ≥ (length M2)
⟹ j- (length M2) < (length M)*(length M2)"
using add_0_iff add_diff_inverse diff_is_0_eq
less_diff_conv less_imp_le linorder_cases add.commute
neq0_conv
by (metis (opaque_lifting, no_types))
have 3:"(v#M)⊗M2 = (vec_mat_Tensor v M2)@(M ⊗ M2)"
using Tensor.simps by auto
have "(col ((v#M)⊗M2) j) = (col ((vec_mat_Tensor v M2)@(M ⊗ M2)) j)"
using col_def by auto
then have "j < length (vec_mat_Tensor v M2)
⟹ (col ((v#M)⊗M2) j) = (col (vec_mat_Tensor v M2) j)"
unfolding col_def using append_simpl by auto
then have 4:"j < length M2 ⟹
(col ((v#M)⊗M2) j) = (col (vec_mat_Tensor v M2) j)"
using vec_mat_Tensor_length by simp
then have "j < length M2 ⟹
(col (vec_mat_Tensor v M2) j)
= vec_vec_Tensor v (col M2 j)"
using col_vec_mat_Tensor by auto
then have
"j< length M2 ⟹
(col (vec_mat_Tensor v M2) j)
= vec_vec_Tensor
((v#M)!(j div length M2))
(col M2 (j mod (length M2)))"
by auto
then have step_1:"j< length M2 ⟹
(col ((v#M)⊗ M2) j)
= vec_vec_Tensor
((v#M)!(j div length M2))
(col M2 (j mod (length M2)))"
using 4 by auto
have 4:"j ≥ length M2
⟹ (col ((v#M)⊗M2) j)= (M ⊗ M2)!(j- (length M2))"
unfolding col_def using 3 append_simpl2 vec_mat_Tensor_length
by metis
then have 5:
"j ≥ length M2 ⟹
col (M ⊗ M2) (j-length M2)
= vec_vec_Tensor
(col M ((j-length M2) div length M2))
(col M2 ((j- length M2) mod length M2))"
using 1 0 2 Cons by auto
then have 6:
"j ≥ length M2 ⟹
(j - length M2) div (length M2) + 1 = j div (length M2)"
using 2 div_0 div_self
le_neq_implies_less less_nat_zero_code
monoid_add_class.add.right_neutral mult_0 mult_cancel2
add.commute nat_div neq0_conv div_add_self1 le_add_diff_inverse
by metis
then have
"j ≥ length M2 ⟹
((j- length M2) mod length M2) = j mod (length M2)"
using le_mod_geq by metis
with 6 have 7:
"j ≥ length M2 ⟹
col (M ⊗ M2) (j-length M2)
= vec_vec_Tensor (col M ((j-length M2) div length M2))
(col M2 (j mod length M2))"
using 5 by auto
moreover have "k<(length M) ⟹ (col M k) = (col (v#M) (k+1))"
unfolding col_def by auto
ultimately have "j ≥ length M2 ⟹
col (M ⊗ M2) (j-length M2)
= vec_vec_Tensor (col (v#M) (j div length M2))
(col M2 (j mod length M2))"
proof-
assume temp:"j ≥ length M2 "
have " j- (length M2) < (length M)*(length M2)"
using 2 temp by auto
then have "(j- (length M2)) div (length M2) < (length M)"
using div_right_ineq mult.commute by metis
moreover have
"((j- (length M2)) div (length M2)<(length M)
⟶ (col M ((j- (length M2)) div (length M2)))
= (col (v#M) ((j- (length M2)) div (length M2)+1)))"
unfolding col_def by auto
ultimately have temp1:
"(col (v#M) (((j-length M2) div length M2)+1))
= (col M (((j-length M2) div length M2)))"
by auto
then have "(col (v#M) (((j-length M2) div length M2)+1))
= (col (v#M) (j div length M2))"
using 6 temp by auto
then show ?thesis using temp1 7 by (metis temp)
qed
then have "j ≥ length M2 ⟹
col ((v#M) ⊗ M2) j
= vec_vec_Tensor (col (v#M) (j div length M2))
(col M2 (j mod length M2))"
using col_def 4 by metis
then show ?thesis
using step_1 col_def le_refl nat_less_le nat_neq_iff
by (metis)
qed
then show ?case by auto
qed
lemma row_Cons:"row (v#M) i = (v!i)#(row M i)"
unfolding row_def map_def by auto
lemma row_append:"row (A@B)i = (row A i)@(row B i)"
unfolding row_def map_append by auto
lemma row_empty:"row [] i = []"
unfolding row_def by auto
lemma vec_vec_Tensor_right_empty:"vec_vec_Tensor x [] = []"
using vec_vec_Tensor.simps times.simps length_0_conv mult_0_right vec_vec_Tensor_length
by (metis)
lemma "vec_mat_Tensor v ([]#[]) = [[]] "
using vec_mat_Tensor.simps by (metis vec_vec_Tensor_right_empty)
lemma "i<0 ⟶ [[]!i] = []"
by auto
lemma row_vec_mat_Tensor_prelim:
"∀i.
((i < (length v)*(row_length M))∧(mat nr (length M) M)
⟶ row (vec_mat_Tensor v M) i
= times (v!(i div row_length M)) (row M (i mod row_length M)))"
apply(rule allI)
proof(induct M)
case Nil
show ?case using Nil by (metis less_nat_zero_code mult_0_right row_length_Nil)
next
case (Cons w N)
have "row (vec_mat_Tensor v (w#N)) i
= row ((vec_vec_Tensor v w)#(vec_mat_Tensor v N)) i"
using vec_mat_Tensor.simps by auto
then have 1:"... = ((vec_vec_Tensor v w)!i)#(row (vec_mat_Tensor v N) i)"
using row_Cons by auto
have 2:"row_length (w#N) = length w"
using row_length_def by auto
then have 3:"(mat nr (length (w#N)) (w#N)) ⟹ nr = length w"
using hd_in_set list.distinct(1) mat_uniqueness matrix_row_length by metis
then have "((i < (length v)*(row_length (w#N)))
∧ (mat nr (length (w#N)) (w#N))
⟹ row (vec_mat_Tensor v (w#N)) i
= times
(v!(i div row_length (w#N)))
(row (w#N) (i mod row_length (w#N))))"
proof-
assume assms: "i < (length v)*(row_length (w#N))
∧ (mat nr (length (w#N)) (w#N))"
show ?thesis
proof(cases N)
case Nil
have "row (vec_mat_Tensor v (w#N)) i = [(vec_vec_Tensor v w)!i]"
using 1 vec_mat_Tensor.simps Nil row_empty by auto
then show ?thesis
proof(cases w)
case Nil
have "(vec_vec_Tensor v w) = []"
using Nil vec_vec_Tensor_right_empty by auto
moreover have " (length v)*(row_length (w#N)) = 0"
using Nil row_length_def by auto
then have " [(vec_vec_Tensor v [])!i] = []"
using assms less_nat_zero_code by metis
ultimately show ?thesis
using vec_vec_Tensor.simps row_empty Nil assms list.distinct(1) by (metis)
next
case (Cons a w1)
have 1:"w ≠ []"
using Cons by auto
then have "i < (length v)*(length w)"
using assms row_length_def by auto
then have "(vec_vec_Tensor v w)!i
= f
(v!(i div (length w)))
(w!(i mod (length w)))"
using vec_vec_Tensor_elements 1 allI by auto
then have "(row (vec_mat_Tensor v (w#N)) i)
= times
(v!(i div row_length (w#N)))
(row (w#N) (i mod (length w)))"
using Cons vec_mat_Tensor.simps row_def row_length_def 2 Nil row_Cons
row_empty times.simps(1) times.simps(2) by metis
then show ?thesis using row_def 2 by metis
qed
next
case (Cons w1 N1)
have Cons_0:"row_length N = length w1"
using Cons row_length_def by auto
have "mat nr (length (w#w1#N1)) (w#w1#N1)"
using assms Cons by auto
then have Cons_1:
"mat (row_length (w#w1#N1)) (length (w#w1#N1)) (w#w1#N1)"
by (metis matrix_row_length)
then have Cons_2:
"mat (row_length (w1#N1)) (length (w1#N1)) (w1#N1)"
by (metis reduct_matrix)
then have Cons_3:"(length w1 = length w)"
using Cons_1
unfolding mat_def row_length_def Ball_def vec_def
by (metis "2" Cons_0 Cons_1 local.Cons row_length_eq)
then have Cons_4:"mat nr (length (w1#N1)) (w1#N1)"
using 3 Cons_2 assms hd_conv_nth list.distinct(1) nth_Cons_0 row_length_def
by metis
moreover have "i < (length v)*(row_length (w1#N1))"
using assms Cons_3 row_length_def by auto
ultimately have Cons_5:"row (vec_mat_Tensor v N) i
= times
(v ! (i div row_length N))
(row N (i mod row_length N))"
using Cons Cons.hyps by auto
then show ?thesis
proof(cases w)
case Nil
have "(vec_vec_Tensor v w) = []"
using Nil vec_vec_Tensor_right_empty by auto
moreover have " (length v)*(row_length (w#N)) = 0"
using Nil row_length_def by auto
then have " [(vec_vec_Tensor v [])!i] = []"
using assms by (metis less_nat_zero_code)
ultimately show ?thesis
using vec_vec_Tensor.simps row_empty Nil assms
by (metis list.distinct(1))
next
case (Cons a w2)
have 1:"w ≠ []"
using Cons by auto
then have "i < (length v)*(length w)"
using assms row_length_def by auto
then have ConsCons_2:
"(vec_vec_Tensor v w)!i = f
(v!(i div (length w)))
(w!(i mod (length w)))"
using vec_vec_Tensor_elements 1 allI by auto
moreover have
"times
(v!(i div row_length (w#N)))
(row (w#N) (i mod row_length (w#N)))
= (f
(v!(i div (length w)))
(w!(i mod (length w))))
#(times (v ! (i div row_length N))
(row N (i mod row_length N)))"
proof-
have temp:"row_length (w#N) = (row_length N)"
using row_length_def 2 Cons_3 Cons_0 by auto
have "(row (w#N) (i mod row_length (w#N)))
= (w!(i mod (row_length (w#N))))
#(row N (i mod row_length (w#N)))"
unfolding row_def by auto
then have "...
= (w!(i mod (length w)))
#(row N (i mod row_length N))"
using Cons_3 3 assms 2 neq_Nil_conv row_Cons row_empty
row_length_eq by (metis (opaque_lifting, no_types))
then have "times
(v!(i div row_length (w#N)))
((w!(i mod (length w)))
#(row N (i mod row_length N)))
= (f
(v!(i div row_length (w#N)))
(w!(i mod (length w))))
#(times (v!(i div row_length (w#N)))
(row N (i mod row_length N)))"
by auto
then have "... = (f
(v!(i div length w))
(w!(i mod (length w))))
#(times (v!(i div row_length N))
(row N (i mod row_length N)))"
using 3 Cons_3 assms temp row_length_def by auto
then show ?thesis using times.simps 2 row_Cons temp by metis
qed
then show ?thesis using Cons_5 ConsCons_2 1
row_Cons vec_mat_Tensor.simps(2) by (metis)
qed
qed
qed
then show ?case by auto
qed
text‹The following lemma gives us a formula for the row of a tensor of
two matrices›
lemma row_formula:
fixes M1 and M2
shows "∀i.((i < (row_length M1)*(row_length M2))
∧(mat (row_length M1) (length M1) M1)
∧(mat (row_length M2) (length M2) M2)
⟶ row (M1 ⊗ M2) i
= vec_vec_Tensor
(row M1 (i div row_length M2))
(row M2 (i mod row_length M2)))"
apply(rule allI)
proof(induct M1)
case Nil
show ?case using Nil by (metis less_nat_zero_code mult_0 row_length_Nil)
next
case (Cons v M)
have
"((i < (row_length (v#M))*(row_length M2))
∧ (mat (row_length (v#M)) (length (v#M)) (v#M))
∧ (mat (row_length M2) (length M2) M2)
⟹ row ((v#M) ⊗ M2) i = vec_vec_Tensor
(row (v#M) (i div row_length M2))
(row M2 (i mod row_length M2)))"
proof-
assume assms:
"(i < (row_length (v#M))*(row_length M2))
∧(mat (row_length (v#M)) (length (v#M)) (v#M))
∧(mat (row_length M2) (length M2) M2)"
have 0:"i < (length v)*(row_length M2)"
using assms row_length_def by auto
have 1:"mat (row_length M) (length M) M"
using assms reduct_matrix by (metis)
have "row ((v#M)⊗M2) i = row ((vec_mat_Tensor v M2)@(M ⊗ M2)) i"
by auto
then have 2:"... = (row (vec_mat_Tensor v M2) i)@(row (M ⊗ M2) i)"
using row_append by auto
then show ?thesis
proof(cases M)
case Nil
have "row ((v#M)⊗M2) i = (row (vec_mat_Tensor v M2) i)"
using Nil 2 by auto
moreover have "row (vec_mat_Tensor v M2) i = times
(v!(i div row_length M2))
(row M2 (i mod row_length M2))"
using row_vec_mat_Tensor_prelim assms 0 by auto
ultimately show ?thesis using vec_vec_Tensor_def
Nil append_Nil2 vec_vec_Tensor.simps(1)
vec_vec_Tensor.simps(2) row_Cons row_empty by (metis)
next
case (Cons w N)
have Cons_Cons_1:"mat (row_length M) (length M) M"
using assms reduct_matrix by auto
then have "row_length (w#N) = row_length (v#M)"
using assms Cons unfolding mat_def Ball_def vec_def
using append_Cons hd_in_set list.distinct(1)
rotate1.simps(2) set_rotate1
by auto
then have Cons_Cons_2:"i < (row_length M)*(row_length M2)"
using assms Cons by auto
then have Cons_Cons_3:"(row (M ⊗ M2) i) = vec_vec_Tensor
(row M (i div row_length M2))
(row M2 (i mod row_length M2))"
using Cons.hyps Cons_Cons_1 assms by auto
moreover have "row (vec_mat_Tensor v M2) i
= times
(v!(i div row_length M2))
(row M2 (i mod row_length M2))"
using row_vec_mat_Tensor_prelim assms 0 by auto
then have "row ((v#M)⊗M2) i =
(times
(v!(i div row_length M2))
(row M2 (i mod row_length M2)))
@(vec_vec_Tensor
(row M (i div row_length M2))
(row M2 (i mod row_length M2)))"
using 2 Cons_Cons_3 by auto
moreover have "... = (vec_vec_Tensor
((v!(i div row_length M2))
#(row M (i div row_length M2)))
(row M2 (i mod row_length M2)))"
using vec_vec_Tensor.simps(2) by auto
moreover have "... = (vec_vec_Tensor (row (v#M) (i div row_length M2))
(row M2 (i mod row_length M2)))"
using row_Cons by metis
ultimately show ?thesis by metis
qed
qed
then show ?case by auto
qed
lemma effective_row_formula:
fixes M1 and M2
assumes "i < (row_length M1)*(row_length M2)"
and "(mat (row_length M1) (length M1) M1)"
and "(mat (row_length M2) (length M2) M2)"
shows "row (M1 ⊗ M2) i
= vec_vec_Tensor
(row M1 (i div row_length M2))
(row M2 (i mod row_length M2))"
using assms row_formula by auto
lemma alt_effective_matrix_tensor_elements:
" (((i<((row_length M2)*(row_length M3)))
∧(j < (length M2)*(length M3)))
∧(mat (row_length M2) (length M2) M2)
∧(mat (row_length M3) (length M3) M3)
⟹ ((M2 ⊗ M3)!j!i) = f (M2!(j div (length M3))!(i div (row_length M3)))
(M3!(j mod length M3)!(i mod (row_length M3))))"
using matrix_Tensor_elements by auto
lemma trans_impl:"(∀ i j.(P i j ⟶ Q i j))∧(∀ i j. (Q i j ⟶ R i j))
⟹ (∀ i j. (P i j ⟶ R i j))"
by auto
lemma "((x::nat) div y) div z = (x div (y*z))"
using div_mult2_eq by auto
lemma "(¬((a::nat) < b)) ⟹ (a ≥ b)"
by auto
lemma not_null: "xs ≠ [] ⟹ ∃y ys. xs = y#ys"
by (metis neq_Nil_conv)
lemma "(y::nat) ≠ 0 ⟹ (x mod y) < y"
using mod_less_divisor by auto
lemma mod_prop1:"((a::nat) mod (b*c)) mod c = (a mod c)"
proof(cases "c = 0")
case True
have "b*c = 0"
by (metis True mult_0_right)
then have "(a::nat) mod (b*c) = a"
by auto
then have "((a::nat) mod (b*c)) mod c = a mod c"
by auto
then show ?thesis by auto
next
case False
let ?x = "(a::nat) mod (b*c)"
let ?z = "?x mod c"
have "∃m. a = m*(b*c) + ?x"
by (metis div_mult_mod_eq)
then obtain m1 where "a = m1*(b*c) + ?x"
by auto
then have "?x = (a - m1*(b*c))"
by auto
then have "∃m.( ?x = m*c + ?z)"
using mod_div_decomp by blast
then obtain m where "( ?x = m*c + ?z)"
by auto
then have "(a - m1*(b*c)) = m*c + ?z"
using ‹a mod (b * c) = a - m1 * (b * c)› by (metis)
then have "a = m1*b*c + m*c + ?z"
using ‹a = m1 * (b * c) + a mod (b * c)› ‹a mod (b * c)
= m * c + a mod (b * c) mod c›
by (metis ab_semigroup_add_class.add_ac(1)
ab_semigroup_mult_class.mult_ac(1))
then have 1:"a = (m1*b + m)*c + ?z"
by (metis add_mult_distrib2 mult.commute)
let ?y = "(a mod c)"
have "∃n. a = n*(c) + ?y"
by (metis "1" ‹a mod (b * c) = m * c + a mod (b * c) mod c› mod_mult_self3)
then obtain n where "a = n*(c) + ?y"
by auto
with 1 have "(m1*b + m)*c + ?z = n*c + ?y"
by auto
then have "(m1*b + m)*c - (n*c) = ?y - ?z"
by auto
then have "(m1*b + m - n)*c = (?y - ?z)"
by (metis diff_mult_distrib2 mult.commute)
then have "c dvd (?y - ?z)"
by (metis dvd_triv_right)
moreover have "?y < c"
using mod_less_divisor False by auto
moreover have "?z < c"
using mod_less_divisor False by auto
moreover have "?y - ?z < c"
using calculation(2) less_imp_diff_less by blast
ultimately have "?y - ?z = 0"
by (metis dvd_imp_mod_0 mod_less)
then show ?thesis using False
by (metis "1" mod_add_right_eq mod_mult_self2 add.commute mult.commute)
qed
lemma mod_div_relation:"((a::nat) mod (b*c)) div c = (a div c) mod b"
proof(cases "b*c = 0")
case True
have T_1:"(b = 0)∨(c = 0)"
using True by auto
show ?thesis
proof(cases "(b = 0)")
case True
have "a mod (b*c) = a"
using True by auto
then show ?thesis using True by auto
next
case False
have "c = 0"
using T_1 False by auto
then show ?thesis by auto
qed
next
case False
have F_1:"(b > 0)∧ (c > 0)"
using False by auto
have "∃x. a = x*(b*c) + (a mod (b*c))"
using mod_div_decomp by blast
then obtain x where "a = x*(b*c) + (a mod (b*c))"
by auto
then have "a div c = ((x*(b*c)) div c) + ((a mod (b*c)) div c)"
using div_add1_eq mod_add_self1 mod_add_self2
mod_by_0 mod_div_trivial mod_prop1 mod_self
by (metis)
then have "a div c = (((x*b)*c) div c) + ((a mod (b*c)) div c)"
by auto
then have F_2:"a div c = (x*b) + ((a mod (b*c)) div c)"
by (metis F_1 nonzero_mult_div_cancel_left mult.commute neq0_conv)
have "∃y. a div c = (y*b) + ((a div c) mod b)"
by (metis add.commute mod_div_mult_eq)
then obtain y where "a div c = (y*b) + ((a div c) mod b)"
by auto
with F_2 have F_3:" (x*b) + ((a mod (b*c)) div c) = (y*b) + ((a div c) mod b)"
by auto
then have "(x*b) - (y * b) = ((a div c) mod b) - ((a mod (b*c)) div c) "
by auto
then have "(x - y) * b = ((a div c) mod b) - ((a mod (b*c)) div c)"
by (metis diff_mult_distrib2 mult.commute)
then have F_4:"b dvd (((a div c) mod b) - ((a mod (b*c)) div c))"
by (metis dvd_eq_mod_eq_0 mod_mult_self1_is_0 mult.commute)
have F_5:"b > ((a div c) mod b)"
by (metis F_1 mod_less_divisor)
have "b*c > (a mod (b*c))"
by (metis False mod_less_divisor neq0_conv)
moreover then have "(b*c) div c > (a mod (b*c)) div c"
by (metis F_1 div_left_ineq nonzero_mult_div_cancel_right neq0_conv)
then have "b > (a mod (b*c)) div c"
by (metis calculation div_right_ineq mult.commute)
with F_4 F_5
have F_6:"((a div c) mod b)-((a mod (b*c)) div c) = 0"
using less_imp_diff_less nat_dvd_not_less by blast
from F_3 have "(y * b) - (x*b)
= ((a mod (b*c)) div c) - ((a div c) mod b) "
by auto
then have "(y - x) * b = ((a mod (b*c)) div c) - ((a div c) mod b)"
by (metis diff_mult_distrib2 mult.commute)
then have F_7:"b dvd (((a mod (b*c)) div c) - ((a div c) mod b))"
by (metis dvd_eq_mod_eq_0 mod_mult_self1_is_0 mult.commute)
have F_8:"b > ((a div c) mod b)"
by (metis F_1 mod_less_divisor)
have "b*c > (a mod (b*c))"
by (metis False mod_less_divisor neq0_conv)
moreover then have "(b*c) div c > (a mod (b*c)) div c"
by (metis F_1 div_left_ineq nonzero_mult_div_cancel_right neq0_conv)
then have "b > (a mod (b*c)) div c"
by (metis calculation div_right_ineq mult.commute)
with F_7 F_8
have "((a mod (b*c)) div c) - ((a div c) mod b) = 0"
by (metis F_2 cancel_comm_monoid_add_class.diff_cancel mod_if mod_mult_self3)
with F_6 have "((a mod (b*c)) div c) = ((a div c) mod b)"
by auto
then show ?thesis using False by auto
qed
text‹The following lemma proves that the tensor product of matrices
is associative›
lemma associativity:
fixes M1 M2 M3
shows
" (mat (row_length M1) (length M1) M1)
∧ (mat (row_length M2) (length M2) M2)
∧ (mat (row_length M3) (length M3) M3)
⟹
M1 ⊗ (M2 ⊗ M3) = (M1 ⊗ M2) ⊗ M3" (is "?x ⟹?l = ?r")
proof-
fix j
assume 0:" (mat (row_length M1) (length M1) M1)
∧ (mat (row_length M2) (length M2) M2)
∧ (mat (row_length M3) (length M3) M3)"
have 1:"length ((M1 ⊗ M2) ⊗ M3)
= (length M1)*(length M2)* (length M3)"
proof-
have "length (M2 ⊗ M3) = (length M2)* (length M3)"
by (metis length_Tensor)
then have "length (M1 ⊗ (M2 ⊗ M3))
= (length M1)*(length M2)* (length M3)"
using mult.assoc length_Tensor by auto
moreover have " length (M1 ⊗ M2) = (length M1)* (length M2)"
by (metis length_Tensor)
ultimately show ?thesis using mult.assoc length_Tensor by auto
qed
have 2:"row_length ((M1 ⊗ M2) ⊗ M3)
= (row_length M1)*(row_length M2)* (row_length M3)"
proof-
have "row_length (M2 ⊗ M3) = (row_length M2)* (row_length M3)"
using row_length_mat assoc by auto
then have "row_length (M1 ⊗ (M2 ⊗ M3))
= (row_length M1)*(row_length M2)* (row_length M3)"
using row_length_mat assoc by auto
moreover have " row_length (M1 ⊗ M2)
= (row_length M1)* (row_length M2)"
using row_length_mat by auto
ultimately show ?thesis using row_length_mat assoc by auto
qed
have 3:
"∀i.∀j.(((i<((row_length M1)*(row_length M2)*(row_length M3)))
∧(j < (length M1)*(length M2)*(length M3)))
⟶
(((M1 ⊗ M2) ⊗ M3)!j!i)
= f
((M1 ⊗ M2)!(j div (length M3))!(i div (row_length M3)))
(M3!(j mod length M3)!(i mod (row_length M3))))"
using 0 matrix_Tensor_elements 1 2 effective_well_defined_Tensor
length_Tensor row_length_mat
by auto
moreover have
"∀j.(j < (length M1)*(length M2)*(length M3))
⟶ (j div (length M3)) < (length M1)*(length M2)"
apply(rule allI)
apply(simp add:div_left_ineq)
done
moreover have "∀i.(i < (row_length M1)*(row_length M2)*(row_length M3))
⟶ (i div (row_length M3))
< (row_length M1)*(row_length M2)"
apply(rule allI)
apply(simp add:div_left_ineq)
done
ultimately have 4:"∀i.∀j.(((i<((row_length M1)*(row_length M2)*(row_length M3)))
∧(j < (length M1)*(length M2)*(length M3)))
⟶
((i div (row_length M3)) < (row_length M1)*(row_length M2))
∧ ((j div (length M3)) < (length M1)*(length M2)))"
using allI 0 by auto
have " (mat (row_length M1) (length M1) M1)
∧ (mat (row_length M2) (length M2) M2)"
using 0 by auto
then have "∀i.∀j.(((i div (row_length M3)) < (row_length M1)*(row_length M2))
∧ ((j div (length M3)) < (length M1)*(length M2))
⟶
(((M1 ⊗ M2))!(j div (length M3))!(i div row_length M3))
= f
((M1)!((j div (length M3)) div (length M2))
!((i div (row_length M3)) div (row_length M2)))
(M2!((j div (length M3)) mod (length M2))
!((i div (row_length M3)) mod (row_length M2))))"
using effective_matrix_tensor_elements by auto
with 4 have 5:"∀i j.(((i<((row_length M1)*(row_length M2)*(row_length M3)))
∧(j < (length M1)*(length M2)*(length M3)))
⟶ (((M1 ⊗ M2))!(j div (length M3))!(i div row_length M3))
= f
((M1)!((j div (length M3)) div (length M2))
!((i div (row_length M3)) div (row_length M2)))
(M2!((j div (length M3)) mod (length M2))
!((i div (row_length M3)) mod (row_length M2))))"
by auto
with 3 have 6:
"∀i.∀j.(((i<((row_length M1)*(row_length M2)*(row_length M3)))
∧(j < (length M1)*(length M2)*(length M3)))
⟶
(((M1 ⊗ M2) ⊗ M3)!j!i)
= f
(f
((M1)!((j div (length M3)) div (length M2))
!((i div (row_length M3)) div (row_length M2)))
(M2!((j div (length M3)) mod (length M2))
!((i div (row_length M3)) mod (row_length M2))))
(M3!(j mod length M3)!(i mod (row_length M3))))"
by auto
have "(j div (length M3))div (length M2) = (j div ((length M3)*(length M2)))"
using div_mult2_eq by auto
moreover have "((i div (row_length M3)) div (row_length M2)) = (i div ((row_length M3)*(row_length M2)))"
using div_mult2_eq by auto
ultimately have step1:"∀i.∀j.(((i<((row_length M1)*(row_length M2)*(row_length M3)))
∧(j < (length M1)*(length M2)*(length M3)))
⟶
(((M1 ⊗ M2) ⊗ M3)!j!i)
= f
(f
((M1)!(j div ((length M3)*(length M2)))! (i div ((row_length M3)*(row_length M2))))
(M2!((j div (length M3)) mod (length M2))!((i div (row_length M3)) mod (row_length M2))))
(M3!(j mod length M3)!(i mod (row_length M3))))"
using 6 by (metis "3" "5" div_mult2_eq)
then have step1:"∀i j.(((i<((row_length M1)*(row_length M2)*(row_length M3)))
∧(j < (length M1)*(length M2)*(length M3)))
⟶
(((M1 ⊗ M2) ⊗ M3)!j!i)
= f
(f
((M1)!(j div ((length M2)*(length M3)))! (i div ((row_length M2)*(row_length M3))))
(M2!((j div (length M3)) mod (length M2))!((i div (row_length M3)) mod (row_length M2))))
(M3!(j mod length M3)!(i mod (row_length M3))))"
by (metis mult.commute)
have 7:
"∀i.∀j.(((i<((row_length M1)*(row_length M2)*(row_length M3)))
∧(j < (length M1)*(length M2)*(length M3)))
⟶
((M1 ⊗ (M2 ⊗ M3))!j!i)
= f
((M1)!(j div (length (M2 ⊗ M3)))!(i div (row_length (M2 ⊗ M3))))
((M2 ⊗ M3)!(j mod length (M2 ⊗M3))!(i mod (row_length (M2 ⊗ M3)))))"
using 0 matrix_Tensor_elements 1 2 effective_well_defined_Tensor
length_Tensor row_length_mat
by auto
then have
"∀i.∀j.(((i<((row_length M1)*(row_length M2)*(row_length M3)))
∧(j < (length M1)*(length M2)*(length M3)))
⟶
((M1 ⊗ (M2 ⊗ M3))!j!i)
= f
((M1)!(j div ((length M2)*(length M3)))!(i div ((row_length M2)*(row_length M3))))
((M2 ⊗ M3)!(j mod length (M2 ⊗M3))!(i mod (row_length (M2 ⊗ M3)))))"
using length_Tensor row_length_mat by auto
then have
"∀i.∀j.(((i<((row_length M1)*(row_length M2)*(row_length M3)))
∧(j < (length M1)*(length M2)*(length M3)))
⟶
((M1 ⊗ (M2 ⊗ M3))!j!i)
= f
((M1)!(j div ((length M3)*(length M2)))
!(i div ((row_length M3)*(row_length M2))))
((M2 ⊗ M3)!(j mod length (M2 ⊗M3))
!(i mod (row_length (M2 ⊗ M3)))))"
using mult.commute by (metis)
have 8:
"∀j.((j < (length M1)*(length M2)*(length M3)))
⟶ (j mod (length (M2 ⊗ M3))) < (length (M2 ⊗ M3))"
proof(cases "length (M2 ⊗ M3) = 0")
case True
have "(length M2)*(length M3) = 0"
using length_Tensor True by auto
then have "(length M1)*(length M2)*(length M3) = 0"
by auto
then show ?thesis by (metis less_nat_zero_code)
next
case False
have "length (M2 ⊗ M3) > 0"
using False by auto
then show ?thesis using mod_less_divisor by auto
qed
then have 9:
"∀i.((i < (row_length M1)*(row_length M2)*(row_length M3)))
⟶ (i mod (row_length (M2 ⊗ M3))) < (row_length (M2 ⊗ M3))"
proof(cases "row_length (M2 ⊗ M3) = 0")
case True
have "(row_length M2)*(row_length M3) = 0"
using True by (metis row_length_mat)
then have "(row_length M1)*(row_length M2)*(row_length M3) = 0"
by auto
then show ?thesis by (metis less_nat_zero_code)
next
case False
have "row_length (M2 ⊗ M3) > 0"
using False by auto
then show ?thesis using mod_less_divisor by auto
qed
with 8 have 10:"∀i.∀j.(((i<((row_length M1)*(row_length M2)*(row_length M3)))
∧(j < (length M1)*(length M2)*(length M3)))
⟶
(i mod (row_length (M2 ⊗ M3))) < (row_length (M2 ⊗ M3))
∧ (j mod (length (M2 ⊗ M3))) < (length (M2 ⊗ M3)))"
by auto
then have 11:"∀ i j.(((i<((row_length M1)*(row_length M2)*(row_length M3)))
∧(j < (length M1)*(length M2)*(length M3)))
⟶
(i mod (row_length (M2 ⊗ M3)))
< (row_length M2)*(row_length M3)
∧(j mod (length (M2 ⊗ M3))) < (length M2)*(length M3))"
using length_Tensor row_length_mat by auto
have "(mat (row_length M2) (length M2) M2)
∧ (mat (row_length M3) (length M3) M3)"
using 0 by auto
then have "∀ i j.(((i mod (row_length (M2 ⊗ M3)))
< (row_length M2)*(row_length M3))
∧((j mod (length (M2⊗M3))) < (length M2)*(length M3))
⟶
(((M2 ⊗ M3))!(j mod (length (M2 ⊗ M3)))!(i mod row_length (M2 ⊗ M3)))
= f
((M2)!((j mod (length (M2 ⊗ M3))) div (length M3))
!((i mod (row_length (M2 ⊗ M3))) div (row_length M3)))
(M3!((j mod (length (M2 ⊗ M3))) mod (length M3))
!((i mod (row_length (M2 ⊗ M3))) mod (row_length M3))))"
using matrix_Tensor_elements by auto
then have "∀ i j.
((i < (row_length M1)*(row_length M2)*(row_length M3))
∧(j < (length M1)*(length M2)*(length M3) )
⟶
(((M2 ⊗ M3))!(j mod (length (M2 ⊗ M3)))
!(i mod row_length (M2 ⊗ M3)))
=
f
((M2)!((j mod (length (M2 ⊗ M3))) div (length M3))
!((i mod (row_length (M2 ⊗ M3))) div (row_length M3)))
(M3!((j mod (length (M2 ⊗ M3))) mod (length M3))
!((i mod (row_length (M2 ⊗ M3))) mod (row_length M3))))"
using 11 by auto
moreover then have "∀j.(j mod (length (M2 ⊗ M3))) mod (length M3)
= j mod (length M3)"
proof
have "∀j.((j mod (length (M2 ⊗ M3)))
= (j mod ((length M2) *(length M3))))"
using length_Tensor by auto
moreover have
"∀j.((j mod ((length M2) *(length M3))) mod (length M3)
= (j mod (length M3)))"
using mod_prop1 by auto
ultimately show ?thesis by auto
qed
moreover then have "∀i.(i mod (row_length (M2 ⊗ M3))) mod (row_length M3)
= i mod (row_length M3)"
proof
have "∀i.((i mod (row_length (M2 ⊗ M3)))
= (i mod ((row_length M2) *(row_length M3))))"
using row_length_mat by auto
moreover have "∀i.((i mod ((row_length M2)*(row_length M3)))
mod (row_length M3)
= (i mod (row_length M3)))"
using mod_prop1 by auto
ultimately show ?thesis by auto
qed
ultimately have 12:"∀ i j.((i < (row_length M1)
*(row_length M2)
*(row_length M3))
∧(j < (length M1)*(length M2)*(length M3) )
⟶
(((M2 ⊗ M3))!(j mod (length (M2 ⊗ M3)))
!(i mod row_length (M2 ⊗ M3)))
= f
((M2)!((j mod (length (M2 ⊗ M3))) div (length M3))
!((i mod (row_length (M2 ⊗ M3))) div (row_length M3)))
(M3!(j mod (length M3))!(i mod (row_length M3))))"
by auto
moreover have "∀j.(j mod (length (M2 ⊗ M3))) div (length M3)
= (j div (length M3)) mod (length M2)"
proof-
have "∀j.((j mod (length (M2 ⊗ M3)))
= (j mod ((length M2)*(length M3))))"
using length_Tensor by auto
then show ?thesis using mod_div_relation by auto
qed
moreover have "∀i.(i mod (row_length (M2 ⊗ M3))) div (row_length M3)
= (i div (row_length M3)) mod (row_length M2)"
proof-
have "∀i.((i mod (row_length (M2 ⊗ M3)))
= (i mod ((row_length M2)*(row_length M3))))"
using row_length_mat by auto
then show ?thesis using mod_div_relation by auto
qed
ultimately have "∀ i j.
((i < (row_length M1)*(row_length M2)*(row_length M3))
∧(j < (length M1)*(length M2)*(length M3) )
⟶
(((M2 ⊗ M3))!(j mod (length (M2 ⊗ M3)))
!(i mod row_length (M2 ⊗ M3)))
= f
((M2)!((j div (length M3)) mod (length M2))
!((i div (row_length M3)) mod (row_length M2)))
(M3!(j mod (length M3))!(i mod (row_length M3))))"
by auto
with 7 have 13:"∀i j.(((i<((row_length M1)*(row_length M2)*(row_length M3)))
∧(j < (length M1)*(length M2)*(length M3)))
⟶
((M1 ⊗ (M2 ⊗ M3))!j!i)
= f
((M1)!(j div ((length M2)*(length M3)))
!(i div ((row_length M2)*(row_length M3))))
(f
((M2)!((j div (length M3)) mod (length M2))!((i div (row_length M3)) mod (row_length M2)))
(M3!(j mod (length M3))
!(i mod (row_length M3)))))"
using length_Tensor row_length_mat by auto
moreover have "∀ i j.( f
((M1)!(j div ((length M2)*(length M3)))
!(i div ((row_length M2)*(row_length M3))))
(f
((M2)!((j div (length M3)) mod (length M2))!((i div (row_length M3)) mod (row_length M2)))
(M3!(j mod (length M3))
!(i mod (row_length M3)))))
= f (f
((M1)!(j div ((length M2)*(length M3)))
!(i div ((row_length M2)*(row_length M3))))
((M2)!((j div (length M3)) mod (length M2))
!((i div (row_length M3)) mod (row_length M2))))
(M3!(j mod (length M3))
!(i mod (row_length M3)))"
using assoc by auto
with 13 have "∀i j.(((i<((row_length M1)*(row_length M2)*(row_length M3)))
∧(j < (length M1)*(length M2)*(length M3)))
⟶
((M1 ⊗ (M2 ⊗ M3))!j!i)
= f (f
((M1)!(j div ((length M2)*(length M3)))
!(i div ((row_length M2)*(row_length M3))))
((M2)!((j div (length M3)) mod (length M2))
!((i div (row_length M3)) mod (row_length M2))))
(M3!(j mod (length M3))
!(i mod (row_length M3))))"
by auto
with step1 have step2:
"∀i j.(((i<((row_length M1)*(row_length M2)*(row_length M3)))
∧(j < (length M1)*(length M2)*(length M3)))
⟶
((M1 ⊗ (M2 ⊗ M3))!j!i) = (((M1 ⊗ M2) ⊗ M3)!j!i))"
by auto
moreover have "mat ((row_length M1)*(row_length M2)*(row_length M3))
((length M1)*(length M2)*(length M3))
(M1 ⊗ (M2 ⊗ M3))"
proof-
have "mat ((row_length M2)*(row_length M3)) ((length M2)*(length M3)) (M2 ⊗ M3)"
using 0 effective_well_defined_Tensor row_length_mat length_Tensor
by auto
moreover have "mat ((row_length M1)*((row_length (M2 ⊗ M3))))
((length M1)*((length (M2 ⊗ M3))))
(M1 ⊗ (M2 ⊗ M3))"
using 0 effective_well_defined_Tensor row_length_mat length_Tensor
by metis
ultimately show ?thesis using row_length_mat length_Tensor mult.assoc
by (simp add: length_Tensor row_length_mat semigroup_mult_class.mult.assoc)
qed
moreover have "mat ((row_length M1)*(row_length M2)*(row_length M3))
((length M1)*(length M2)*(length M3))
((M1 ⊗ M2) ⊗ M3)"
proof-
have "mat ((row_length M1)*(row_length M2)) ((length M1)*(length M2)) (M1 ⊗ M2)"
using 0 effective_well_defined_Tensor row_length_mat length_Tensor by auto
moreover have "mat ((row_length (M1 ⊗ M2))*(row_length M3))
((length (M1 ⊗ M2))*(length M3))
((M1 ⊗ M2 )⊗ M3)"
using 0 effective_well_defined_Tensor row_length_mat length_Tensor by metis
ultimately show ?thesis using row_length_mat length_Tensor by (metis mult.assoc)
qed
ultimately show ?thesis using mat_eqI by blast
qed
end
lemma " ⋀(a::nat) b.(times a b) =(times b a)"
by auto
subsection‹Associativity and Distributive properties›
locale plus_mult =
mult +
fixes zer::"'a"
fixes g::" 'a ⇒ 'a ⇒ 'a " (infixl "+" 60)
fixes inver::"'a ⇒ 'a"
assumes plus_comm:" g a b = g b a "
assumes plus_assoc:" (g (g a b) c) = (g a (g b c))"
assumes plus_left_id:" g zer x = x"
assumes plus_right_id:"g x zer = x"
assumes plus_left_distributivity: "f a (g b c) = g (f a b) (f a c)"
assumes plus_right_distributivity: "f (g a b) c = g (f a c) (f b c)"
assumes plus_left_inverse: "(g x (inver x)) = zer"
assumes plus_right_inverse: "(g (inver x) x) = zer"
context plus_mult
begin
lemma fixes M1 M2 M3
shows "(mat (row_length M1) (length M1) M1)
∧(mat (row_length M2) (length M2) M2)
∧(mat (row_length M3) (length M3) M3)
⟹ (M1 ⊗ (M2 ⊗ M3)) = ((M1 ⊗ M2) ⊗ M3)"
using associativity by auto
text‹matrix$\_$mult refers to multiplication of matrices in the locale
plus\_mult›
abbreviation matrix_mult::"'a mat ⇒ 'a mat ⇒ 'a mat" (infixl "∘" 65)
where
"matrix_mult M1 M2 ≡ (mat_multI zer g f (row_length M1) M1 M2)"
definition scalar_product :: "'a vec ⇒ 'a vec ⇒ 'a" where
"scalar_product v w = scalar_prodI zer g f v w"
lemma ma :
assumes wf1: "mat nr n m1"
and wf2: "mat n nc m2"
and i: "i < nr"
and j: "j < nc"
shows "mat_multI zer g f nr m1 m2 ! j ! i
= scalar_prodI zer g f (row m1 i) (col m2 j)"
using mat_mult_index i j wf1 wf2 by metis
lemma matrix_index:
assumes wf1: "mat (row_length m1) n m1"
and wf2: "mat n nc m2"
and i: "i < (row_length m1)"
and j: "j < nc"
shows "matrix_mult m1 m2 ! j ! i
= scalar_product (row m1 i) (col m2 j)"
using wf1 wf2 i j ma scalar_product_def by auto
lemma unique_row_col:
assumes "mat nr1 nc1 M" and "mat nr2 nc2 M" and "M ≠ []"
shows "nr1 = nr2" and "nc1 = nc2"
proof(cases M)
case Nil
show "nr1 = nr2" using assms(3) Nil by auto
next
case (Cons v M)
have 1:"v ∈ set (v#M)"
using Cons by auto
then have "length v = nr1"
using assms(1) mat_def Ball_def vec_def Cons by metis
moreover then have "length v = nr2"
using 1 assms(2) mat_def Ball_def vec_def Cons by metis
ultimately show "nr1 = nr2"
by auto
next
have "length M = nc1"
using mat_def assms(1) by auto
moreover have "length M = nc2"
using mat_def assms(2) by auto
ultimately show "nc1 = nc2"
by auto
qed
lemma matrix_mult_index:
assumes "m1 ≠ []"
and wf1: "mat nr n m1"
and wf2: "mat n nc m2"
and i: "i < nr"
and j: "j < nc"
shows "matrix_mult m1 m2 ! j ! i = scalar_product (row m1 i) (col m2 j)"
using matrix_index unique_row_col assms by (metis matrix_row_length)
text‹the following definition checks if the given four matrices
are such that the compositions in the mixed-product property which
will be proved, hold true. It further checks that the matrices are
non empty and valid›
definition matrix_match::"'a mat ⇒ 'a mat ⇒'a mat ⇒ 'a mat ⇒ bool"
where
"matrix_match A1 A2 B1 B2 ≡
(mat (row_length A1) (length A1) A1)
∧(mat (row_length A2) (length A2) A2)
∧(mat (row_length B1) (length B1) B1)
∧(mat (row_length B2) (length B2) B2)
∧ (length A1 = row_length A2)
∧ (length B1 = row_length B2)
∧(A1 ≠ [])∧(A2 ≠ [])∧(B1 ≠ [])∧(B2 ≠ [])"
lemma non_empty_mat_mult:
assumes wf1:"mat nr n A"
and wf2:"mat n nc B"
and "A ≠ []" and " B ≠ []"
shows "A ∘ B ≠ []"
proof-
have "mat nr nc (A ∘ B)"
using assms(1) assms(2) mat_mult assms(3) matrix_row_length unique_row_col(1) by (metis)
then have "length (A ∘ B) = nc"
using mat_def by auto
moreover have "nc > 0"
proof-
have "length B = nc"
using assms(2) mat_def by auto
then show ?thesis using assms(4) by auto
qed
moreover then have "length (A ∘ B) > 0"
by (metis calculation(1))
then show ?thesis by auto
qed
lemma tensor_compose_distribution1:
assumes wf1:"mat (row_length A1) (length A1) A1"
and wf2:"mat (row_length A2) (length A2) A2"
and wf3:"mat (row_length B1) (length B1) B1"
and wf4:"mat (row_length B2) (length B2) B2"
and matchAA:"length A1 = row_length A2"
and matchBB:"length B1 = row_length B2"
and non_Nil:"(A1 ≠ [])∧(A2 ≠ [])∧(B1 ≠ [])∧(B2 ≠ [])"
shows "mat ((row_length A1)*(row_length B1))
((length A2)*(length B2))
((A1∘A2)⊗(B1∘B2))"
proof-
have 0:"mat (row_length A1) (length A2) (matrix_mult A1 A2)"
using wf1 wf2 mat_mult matchAA by auto
then have 1:"mat (row_length (A1 ∘ A2)) (length (A1 ∘ A2)) (matrix_mult A1 A2)"
by (metis matrix_row_length)
then have 2: "(row_length (A1 ∘ A2)) = (row_length A1)" and "length (A1 ∘ A2) = length A2"
using non_empty_mat_mult unique_row_col 0
apply (metis length_0_conv mat_empty_column_length non_Nil)
by (metis "0" "1" mat_empty_column_length unique_row_col(2))
moreover have 3:"mat (row_length B1) (length B2) (matrix_mult B1 B2)"
using wf3 wf4 matchBB mat_mult by auto
then have 4:"mat (row_length (B1 ∘ B2)) (length (B1 ∘ B2)) (matrix_mult B1 B2)"
by (metis matrix_row_length)
then have 5: "(row_length (B1 ∘ B2)) = (row_length B1)" and "length (B1 ∘ B2) = length B2"
using non_empty_mat_mult unique_row_col 3
apply (metis length_0_conv mat_empty_column_length non_Nil)
by (metis "3" "4" mat_empty_column_length unique_row_col(2))
then show ?thesis using 1 4 5 well_defined_Tensor
by (metis "2" calculation(2))
qed
lemma effective_tensor_compose_distribution1:
"matrix_match A1 A2 B1 B2 ⟹ mat ((row_length A1)*(row_length B1))
((length A2)*(length B2))
((A1∘A2)⊗(B1∘B2))"
using tensor_compose_distribution1 unfolding matrix_match_def by auto
lemma tensor_compose_distribution2:
assumes wf1:"mat (row_length A1) (length A1) A1"
and wf2:"mat (row_length A2) (length A2) A2"
and wf3:"mat (row_length B1) (length B1) B1"
and wf4:"mat (row_length B2) (length B2) B2"
and matchAA:"length A1 = row_length A2"
and matchBB:"length B1 = row_length B2"
and non_Nil:"(A1 ≠ [])∧(A2 ≠ [])∧(B1 ≠ [])∧(B2 ≠ [])"
shows "mat ((row_length A1)*(row_length B1))
((length A2)*(length B2))
((A1 ⊗ B1) ∘(A2 ⊗B2))"
proof-
have "mat
((row_length A1)*(row_length B1))
((length A1)*(length B1))
(A1 ⊗ B1)"
using wf1 wf3 well_defined_Tensor by auto
moreover have "mat
((row_length A2)*(row_length B2))
((length A2)*(length B2))
(A2⊗ B2)"
using wf2 wf4 well_defined_Tensor by auto
moreover have "((length A1)*(length B1))
= ((row_length A2)*(row_length B2))"
using matchAA matchBB by auto
ultimately show ?thesis using mat_mult row_length_mat by simp
qed
theorem tensor_non_empty: assumes "A ≠ []" and "B ≠ []"
shows "A ⊗ B ≠ []"
using assms(1) assms(2) length_0_conv length_Tensor mult_is_0 by metis
theorem non_empty_distribution:
assumes "mat nr1 n1 A1"
and "mat n1 nc1 A2"
and "mat nr2 n2 B1"
and "mat n2 nc2 B2"
and "A1 ≠ []" and "B1 ≠ []" and "A2 ≠ []" and "B2 ≠ []"
shows "((A1∘A2)⊗(B1∘B2)) ≠ []"
proof-
have "A1 ∘ A2 ≠ []"
using assms non_empty_mat_mult by auto
moreover have "B1 ∘ B2 ≠ []"
using assms non_empty_mat_mult by auto
ultimately show ?thesis using tensor_non_empty by auto
qed
lemma effective_tensor_compose_distribution2:"matrix_match A1 A2 B1 B2 ⟹
mat ((row_length A1)*(row_length B1))
((length A2)*(length B2))
((A1 ⊗ B1) ∘(A2 ⊗B2))"
using tensor_compose_distribution2 unfolding matrix_match_def by auto
theorem effective_matrix_Tensor_elements:
fixes M1 M2 i j
assumes "i<((row_length M1)*(row_length M2))"
and "j < (length M1)*(length M2)"
and "mat (row_length M1) (length M1) M1"
and "mat (row_length M2) (length M2) M2"
shows
"((M1 ⊗ M2)!j!i) = f (M1!(j div (length M2))!(i div (row_length M2)))
(M2!(j mod length M2)!(i mod (row_length M2)))"
using matrix_Tensor_elements assms by auto
theorem effective_matrix_Tensor_elements2:
fixes M1 M2
assumes "mat (row_length M1) (length M1) M1"
and "mat (row_length M2) (length M2) M2"
shows
"(∀i <((row_length M1)*(row_length M2)).
∀j < ((length M1)*(length M2))
.((M1 ⊗ M2)!j!i) = f (M1!(j div (length M2))!(i div (row_length M2)))
(M2!(j mod length M2)!(i mod (row_length M2))))"
using matrix_Tensor_elements assms by auto
definition matrix_compose_cond::"'a mat ⇒ 'a mat ⇒'a mat ⇒ 'a mat ⇒ nat ⇒ nat ⇒ bool"
where
"matrix_compose_cond A1 A2 B1 B2 i j ≡
(mat (row_length A1) (length A1) A1)
∧(mat (row_length A2) (length A2) A2)
∧(mat (row_length B1) (length B1) B1)
∧(mat (row_length B2) (length B2) B2)
∧ (length A1 = row_length A2)
∧ (length B1 = row_length B2)
∧(A1 ≠ [])∧(A2 ≠ [])∧(B1 ≠ [])∧(B2 ≠ [])
∧(i<(row_length A1)*(row_length B1))∧(j< (length A2)*(length B2))"
theorem elements_matrix_distribution_1:
assumes wf1:"mat (row_length A1) (length A1) A1"
and wf2:"mat (row_length A2) (length A2) A2"
and wf3:"mat (row_length B1) (length B1) B1"
and wf4:"mat (row_length B2) (length B2) B2"
and matchAA:"length A1 = row_length A2"
and matchBB:"length B1 = row_length B2"
and non_Nil:"(A1 ≠ [])∧(A2 ≠ [])∧(B1 ≠ [])∧(B2 ≠ [])"
and "i<(row_length A1)*(row_length B1)" and "j< (length A2)*(length B2)"
shows
"((matrix_mult A1 A2)⊗(matrix_mult B1 B2))!j!i
= f (scalar_product (row A1 (i div (row_length B1)))
(col A2 (j div (length B2))))
(scalar_product (row B1 (i mod (row_length B1)))
(col B2 (j mod (length B2))))"
proof-
have 0:"((matrix_mult A1 A2)⊗(matrix_mult B1 B2)) ≠ []"
using non_empty_distribution assms by auto
then have 1:"mat ((row_length A1)*(row_length B1))
((length A2)*(length B2))
((A1∘A2)⊗(B1∘B2))"
using tensor_compose_distribution1 assms by auto
then have 2:"mat (row_length ((A1∘A2)⊗(B1∘B2)))
(length ((A1∘A2)⊗(B1∘B2)))
((A1∘A2)⊗(B1∘B2))"
by (metis matrix_row_length)
then have 3:"((row_length A1)*(row_length B1))
= (row_length ((A1∘A2)⊗(B1∘B2))) "
and "((length A2)*(length B2)) = (length ((A1∘A2)⊗(B1∘B2)))"
using 0 1 unique_row_col
apply metis
using 0 1 2 unique_row_col by metis
then have i:"(i < ((row_length A1)*(row_length B1)))
= (i < (row_length ((A1∘A2)⊗(B1∘B2))))"
by auto
moreover have j:"(j < ((length A2)*(length B2)))
= (j < (length ((A1∘A2)⊗(B1∘B2))))"
using 3 ‹length A2 * length B2 = length (A1 ∘ A2 ⊗ B1 ∘ B2)›
by (metis)
have 4:"mat (row_length A1) (length A2) (A1 ∘ A2)"
using assms mat_mult by auto
then have 5:"mat (row_length (A1 ∘ A2)) (length (A1 ∘ A2)) (A1 ∘ A2)"
using matrix_row_length by (metis)
with 4 have 6:"row_length A1 = row_length (A1 ∘ A2)"
by (metis "0" Tensor.simps(1) unique_row_col(1))
with 4 5 have 7:"length A2 = length (A1 ∘ A2)"
by (metis mat_empty_column_length unique_row_col(2))
then have 8:"mat (row_length B1) (length B2) (B1 ∘ B2)"
using assms mat_mult by auto
then have 9:"mat (row_length (B1 ∘ B2)) (length (B1 ∘ B2)) (B1 ∘ B2)"
using matrix_row_length by (metis)
with 7 8 have 10:"row_length B1 = row_length (B1 ∘ B2)"
by (metis "3" "6" assms(8) less_nat_zero_code mult_cancel2 mult_is_0 mult.commute row_length_mat)
with 7 8 9 have 11:"length B2 = length (B1 ∘ B2)"
by (metis mat_empty_column_length unique_row_col(2))
from 6 10 have 12:
"(i < ((row_length A1)*(row_length B1)))
= (i < (row_length (A1∘A2))*(row_length (B1∘B2)))"
by auto
then have 13:" (i < (row_length (A1∘A2))*(row_length (B1∘B2)))"
using assms by auto
from 7 11 have 14:
"(j < ((length A2)*(length B2)))
= (j < (length (A1∘A2))*(length (B1∘B2)))"
by auto
then have 15:"(j < (length (A1∘A2))*(length (B1∘B2)))"
using assms by auto
then have step_1:"((A1∘A2)⊗(B1∘B2))!j!i
= f ((A1∘A2)!(j div (length (B1∘B2)))
!(i div (row_length (B1∘B2))))
((B1∘B2)!(j mod length (B1∘B2))
!(i mod (row_length (B1∘B2))))"
using 5 9 13 15 effective_matrix_Tensor_elements by auto
then have "((A1∘A2)⊗(B1∘B2))!j!i
= f ((A1∘A2)!(j div (length B2))!(i div (row_length B1)))
((B1∘B2)!(j mod length B2)!(i mod (row_length B1)))"
using 10 11 by auto
moreover have " ((A1∘A2)!(j div (length B2))!(i div (row_length B1)))
= (scalar_product (row A1 (i div (row_length B1)) ) (col A2 (j div (length B2)) ))"
proof-
have "j div (length B2) < (length A2)"
using div_left_ineq assms by auto
moreover have "i div (row_length B1) < (row_length A1)"
using assms div_left_ineq by auto
moreover have "mat (length A1) (length A2) A2"
using wf2 matchAA by auto
ultimately show ?thesis using wf1 non_Nil matrix_mult_index by blast
qed
moreover have " ((B1∘B2)!(j mod (length B2))!(i mod (row_length B1)))
= (scalar_product
(row B1 (i mod (row_length B1)) )
(col B2 (j mod (length B2))))"
proof-
have "j <(length A2)*(length B2)"
using assms by auto
then have "j mod (length B2) < (length B2)"
by (metis calculation less_nat_zero_code mod_less_divisor mult_is_0 neq0_conv)
moreover have "i mod (row_length B1) < (row_length B1)"
by (metis assms(8) less_nat_zero_code mod_less_divisor mult_is_0 neq0_conv)
moreover have "mat (length B1) (length B2) B2"
using wf4 matchBB by auto
ultimately show ?thesis
using wf3 non_Nil matrix_mult_index by blast
qed
ultimately show ?thesis by auto
qed
lemma effective_elements_matrix_distribution1:
"matrix_compose_cond A1 A2 B1 B2 i j ⟹
((matrix_mult A1 A2)⊗(matrix_mult B1 B2))!j!i
= f (scalar_product (row A1 (i div (row_length B1))) (col A2 (j div (length B2))))
(scalar_product (row B1 (i mod (row_length B1))) (col B2 (j mod (length B2))))"
using elements_matrix_distribution_1 matrix_compose_cond_def by auto
lemma matrix_match_condn_1:
"matrix_match A1 A2 B1 B2
∧((i<(row_length A1)*(row_length B1))
∧(j<(length A2)*(length B2)))
⟹ ((matrix_mult A1 A2)⊗(matrix_mult B1 B2))!j!i
= f
(scalar_product
(row A1 (i div (row_length B1)))
(col A2 (j div (length B2))))
(scalar_product
(row B1 (i mod (row_length B1)))
(col B2 (j mod (length B2))))"
using elements_matrix_distribution_1 unfolding matrix_match_def by auto
lemma effective_matrix_match_condn_1:
assumes "(matrix_match A1 A2 B1 B2) "
shows "∀i j.((i<(row_length A1)*(row_length B1))
∧(j<(length A2)*(length B2))
⟶ ((A1 ∘ A2)⊗(B1 ∘ B2))!j!i
= f
(scalar_product
(row A1 (i div (row_length B1)))
(col A2 (j div (length B2))))
(scalar_product
(row B1 (i mod (row_length B1)))
(col B2 (j mod (length B2)))))"
using assms matrix_match_condn_1 unfolding matrix_match_def
by auto
theorem elements_matrix_distribution2:
fixes A1 A2 B1 B2 i j
assumes wf1:"mat (row_length A1) (length A1) A1"
and wf2:"mat (row_length A2) (length A2) A2"
and wf3:"mat (row_length B1) (length B1) B1"
and wf4:"mat (row_length B2) (length B2) B2"
and matchAA:"length A1 = row_length A2"
and matchBB:"length B1 = row_length B2"
and non_Nil:"(A1 ≠ [])∧(A2 ≠ [])∧(B1 ≠ [])∧(B2 ≠ [])"
and i:"i<(row_length A1)*(row_length B1)" and j:"j< (length A2)*(length B2)"
shows
"((A1 ⊗ B1)∘(A2 ⊗ B2))!j!i
= scalar_product
(vec_vec_Tensor
(row A1 (i div row_length B1))
(row B1 (i mod row_length B1)))
(vec_vec_Tensor
(col A2 (j div length B2))
(col B2 (j mod length B2)))"
proof-
have 1:"mat
((row_length A1)*(row_length B1))
((length A1)*(length B1))
(A1 ⊗ B1)"
using wf1 wf3 well_defined_Tensor by auto
moreover have 2:"mat
((row_length A2)*(row_length B2))
((length A2)*(length B2))
(A2 ⊗ B2)"
using wf2 wf4 well_defined_Tensor by auto
moreover have 3:"((length A1)*(length B1))
= ((row_length A2)*(row_length B2))"
using matchAA matchBB by auto
ultimately have 4:"((A1⊗B1)∘(A2⊗B2))!j!i
= scalar_product (row (A1 ⊗ B1) i) (col (A2 ⊗ B2) j)"
using i j matrix_mult_index non_Nil mat_mult_index
row_length_mat scalar_product_def
by auto
moreover have "(row (A1 ⊗ B1) i)
= vec_vec_Tensor
(row A1 (i div row_length B1))
(row B1 (i mod row_length B1))"
using wf1 wf3 i effective_row_formula by auto
moreover have " col (A2 ⊗ B2) j = vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2))"
using wf2 wf4 j col_formula by auto
ultimately show ?thesis by auto
qed
lemma matrix_match_condn_2:
"matrix_match A1 A2 B1 B2
∧((i<(row_length A1)*(row_length B1))
∧(j<(length A2)*(length B2)))
⟹ ((A1 ⊗ B1)∘(A2 ⊗ B2))!j!i
= scalar_product
(vec_vec_Tensor
(row A1 (i div row_length B1))
(row B1 (i mod row_length B1)))
(vec_vec_Tensor
(col A2 (j div length B2))
(col B2 (j mod length B2)))"
using elements_matrix_distribution2 unfolding matrix_match_def by auto
lemma effective_matrix_match_condn_2:
assumes "(matrix_match A1 A2 B1 B2) "
shows "∀i j.((i<(row_length A1)*(row_length B1))
∧(j<(length A2)*(length B2))
⟶ ((A1 ⊗ B1)∘(A2 ⊗ B2))!j!i
= scalar_product
(vec_vec_Tensor
(row A1 (i div row_length B1))
(row B1 (i mod row_length B1)))
(vec_vec_Tensor
(col A2 (j div length B2))
(col B2 (j mod length B2))))"
using assms matrix_match_condn_2 unfolding matrix_match_def by auto
lemma zip_Nil:"zip [] [] = []"
using zip_def by auto
lemma zer_left_mult:"f zer x = zer"
proof-
have "g zer zer = zer"
using plus_left_id by auto
then have "f zer x = f (g zer zer) x"
by auto
then have "f zer x = (f zer x) + (f zer x)"
using plus_right_distributivity by auto
then have "(f zer x) + (inver (f zer x)) = (f zer x) + (f zer x) + (inver (f zer x))"
by auto
then have "zer = (f zer x) + zer"
using plus_left_inverse plus_assoc by (metis)
then show ?thesis
using plus_right_id by simp
qed
lemma zip_Cons:"(length v = length w) ⟹ zip (a#v) (b#w) = (a,b)#(zip v w)"
unfolding zip_def by auto
lemma scalar_product_times:
"∀w1 w2.(length w1 = length w2) ∧(length w1 = n) ⟶
(f (x*y) (scalar_product w1 w2))
= (scalar_product
(times x w1)
(times y w2))"
apply(rule allI)
apply (rule allI)
proof(induct n)
case 0
have "(length w1 = length w2) ∧(length w1 = 0) ⟹ ?case"
proof-
assume assms:"(length w1 = length w2) ∧(length w1 = 0)"
have 1:" w1 = []"
using assms by auto
moreover have 2:"(length w1 = length w2) ∧(length w1 = 0) ⟶ w2 = []"
by auto
ultimately have "(length w1 = length w2) ∧(length w1 = 0)
⟶ scalar_product w1 w2 = zer"
unfolding scalar_product_def scalar_prodI_def by auto
then have 3:"(length w1 = length w2) ∧(length w1 = 0)
⟶ (f (x*y) (scalar_product w1 w2)) = zer"
using comm zer_left_mult by metis
then have "times x w1 = []"
using 1 by auto
moreover have "times y w2 = []"
using 2 assms by auto
ultimately have "(scalar_product (times x w1) ( times y w2)) = zer"
unfolding scalar_product_def scalar_prodI_def by auto
with 3 show ?thesis by auto
qed
then show ?case by auto
next
case (Suc k)
have "(length w1 = length w2) ∧(length w1 = (Suc k)) ⟹ ?case"
proof-
assume assms:"(length w1 = length w2) ∧(length w1 = (Suc k))"
have "∃a1 u1.(w1 = a1#u1)∧(length u1 = k)"
using assms by (metis length_Suc_conv)
then obtain a1 u1 where "(w1 = a1#u1)∧(length u1 = k)"
by auto
then have Cons_1:"(w1 = a1#u1)∧(length u1 = k)"
by auto
have "length w2 = (Suc k)"
using assms by auto
then have "∃a2 u2.(w2 = a2#u2)∧(length u2 = k)"
using assms by (metis length_Suc_conv)
then obtain a2 u2 where "(w2 = a2#u2)∧(length u2 = k)"
by auto
then have Cons_2:"(w2 = a2#u2)∧(length u2 = k)"
by auto
then have "(length u1 = length u2)∧(length u1 = k)"
using Cons_1 by auto
then have Cons_3:"x * y * scalar_product u1 u2
= scalar_product (times x u1) (times y u2)"
using Suc assms by auto
have "scalar_product (a1#u1) (a2#u2) = (a1*a2) + (scalar_product u1 u2)"
unfolding scalar_product_def scalar_prodI_def zip_def by auto
then have "scalar_product w1 w2 = (a1*a2) + (scalar_product u1 u2)"
using Cons_1 Cons_2 by auto
then have "(x*y)*(scalar_product w1 w2)
= ((x*y)*(a1*a2)) + ((x*y)*(scalar_product u1 u2))"
using plus_right_distributivity by (metis plus_left_distributivity)
then have Cons_4:"(x*y)*(scalar_product w1 w2)
= (x*a1*y*a2)+ ((x*y)*(scalar_product u1 u2))"
using comm assoc by metis
have "(times x w1) = (x*a1)#(times x u1)"
using times.simps Cons_1 by auto
moreover have "(times y w2) = (y*a2)#(times y u2)"
using times.simps Cons_2 by auto
ultimately have Cons_5:"scalar_product (times x w1) (times y w2)
= scalar_product
((x*a1)#(times x u1))
((y*a2)#(times y u2))"
by auto
then have "... = ((x*a1)*(y*a2))
+ scalar_product (times x u1) (times y u2)"
unfolding scalar_product_def scalar_prodI_def zip_def by auto
with Cons_3 Cons_4 Cons_5 show ?thesis using assoc by auto
qed
then show ?case by auto
qed
lemma effective_scalar_product_times:
assumes "(length w1 = length w2)"
shows "(f (x*y) (scalar_product w1 w2))
= (scalar_product (times x w1) ( times y w2))"
using scalar_product_times assms by auto
lemma zip_append:"(length zs = length ws)∧(length xs = length ys)
⟹ (zip (xs@zs) (ys@ws)) = (zip xs ys)@(zip zs ws)"
using zip_append1 zip_append2 by auto
lemma scalar_product_append:
"∀xs ys zs ws.(length zs = length ws)
∧(length xs = length ys)
∧(length xs = n) ⟶
(scalar_product (xs@zs) (ys@ws))
= (scalar_product xs ys)
+(scalar_product zs ws)"
apply(rule allI)
apply(rule allI)
apply(rule allI)
apply(rule allI)
proof(induct n)
case 0
have "(length zs = length ws) ∧(length xs = length ys) ∧(length xs = 0)
⟹
(scalar_product (xs@zs) (ys@ws))
= (scalar_product xs ys)
+(scalar_product zs ws)"
proof-
assume assms:"(length zs = length ws)∧(length xs = length ys)
∧(length xs = 0)"
have 1:"xs = []"
using assms by auto
moreover have 2:"ys = []"
using assms by auto
ultimately have "scalar_product xs ys = zer"
unfolding scalar_product_def scalar_prodI_def zip_def by auto
then have "(scalar_product xs ys)+(scalar_product zs ws)
= (scalar_product zs ws)"
using plus_left_id by auto
moreover have "(scalar_product (xs@zs) (ys@ws)) = (scalar_product zs ws)"
using 1 2 by auto
ultimately show ?thesis by auto
qed
then show ?case by auto
next
case (Suc k)
have "(length zs = length ws)∧(length xs = length ys)∧(length xs = (Suc k)) ⟹
(scalar_product (xs@zs) (ys@ws))
= (scalar_product xs ys)
+(scalar_product zs ws)"
proof-
assume assms:"(length zs = length ws)
∧(length xs = length ys)
∧(length xs = (Suc k))"
have "∃x xss.(xs = x#xss)∧(length xss = k)"
using assms by (metis Suc_length_conv)
then obtain x xss where "(xs = x#xss)∧(length xss = k)"
by auto
then have 1:"(xs = x#xss)∧(length xss = k)"
by auto
have "∃y yss.(ys = y#yss)∧(length yss = k)"
using assms by (metis Suc_length_conv)
then obtain y yss where "(ys = y#yss)∧(length yss = k)"
by auto
then have 2:"(ys = y#yss)∧(length yss = k)"
by auto
with 1 have "length xss = length yss ∧ length xss = k"
by auto
then have 3:"(scalar_product (xss@zs) (yss@ws))
= (scalar_product xss yss)
+(scalar_product zs ws)"
using 1 2 assms Suc by auto
then have 4:"(scalar_product ((x#xss)@zs) ((y#yss)@ws)) =
(scalar_product (x#(xss@zs)) (y#(yss@ws)))"
by auto
then have "... = (x*y) + (scalar_product (xss@zs) (yss@ws))"
unfolding scalar_product_def scalar_prodI_def
using zip_Cons scalar_prodI_def scalar_prod_cons
by (metis)
with 4 have 5:"(scalar_product (xs@zs) ((ys)@ws))
= (x*y) + (scalar_product (xss@zs) (yss@ws))"
using 1 2 by auto
moreover have "(scalar_product xs ys) = (x*y) + (scalar_product xss yss)"
unfolding scalar_product_def scalar_prodI_def
using zip_Cons
by (metis "1" "2" scalar_prodI_def scalar_prod_cons)
moreover then have "(scalar_product xs ys)+(scalar_product zs ws)
= (x*y)
+ (scalar_product xss yss)
+ (scalar_product zs ws)"
by auto
ultimately show ?thesis using 3 plus_assoc by auto
qed
then show ?case by auto
qed
lemma effective_scalar_product_append:
assumes "length zs = length ws" and "(length xs = length ys)"
shows "(scalar_product (xs@zs) (ys@ws)) = (scalar_product xs ys)+(scalar_product zs ws)"
using scalar_product_append assms by auto
lemma scalar_product_distributivity:
"∀v1 v2 w1 w2.((length v1 = length v2)∧(length v1 = n)∧ (length w1 = length w2)
⟶ (scalar_product v1 v2)*(scalar_product w1 w2)
= scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)) "
apply (rule allI)
apply (rule allI)
apply (rule allI)
apply (rule allI)
proof(induct "n")
case 0
have "((length v1 = length v2)∧(length v1 = 0)∧ (length w1 = length w2))
⟶length v1 = 0"
using 0 by auto
then have 1:"((length v1 = length v2)
∧(length v1 = 0)
∧(length w1 = length w2))
⟶v1 = []"
by auto
moreover have "((length v1 = length v2)
∧(length v1 = 0)
∧(length w1 = length w2))
⟶length v2 = 0"
using 0 by auto
moreover then have 2:"((length v1 = length v2)
∧(length v1 = 0)
∧(length w1 = length w2))
⟶v2 = []"
by auto
ultimately have 3:
"((length v1 = length v2)∧(length v1 = 0)∧ (length w1 = length w2))
⟶scalar_product v1 v2 = zer"
unfolding scalar_product_def scalar_prodI_def using zip_Nil by auto
then have 4:"f zer (scalar_product w1 w2) = zer"
using zer_left_mult by auto
have "((length v1 = length v2)∧(length v1 = 0)∧ (length w1 = length w2))
⟶vec_vec_Tensor v1 w1 = []"
using 1 by auto
moreover have "((length v1 = length v2)
∧(length v1 = 0)
∧(length w1 = length w2))
⟶vec_vec_Tensor v2 w2 = []"
using 2 by auto
ultimately have "((length v1 = length v2)
∧(length v1 = 0)
∧(length w1 = length w2))
⟶ scalar_product
(vec_vec_Tensor v1 w1)
(vec_vec_Tensor v2 w2) = zer"
unfolding scalar_product_def scalar_prodI_def using zip_Nil by auto
with 3 4 show ?case by auto
next
case (Suc k)
have "((length v1 = length v2)∧(length v1 = Suc k)
∧ (length w1 = length w2))
⟹ f (scalar_product v1 v2) (scalar_product w1 w2)
= scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)"
proof-
assume assms:"((length v1 = length v2)∧(length v1 = Suc k)
∧ (length w1 = length w2))"
have "length v1 = Suc k"
using Suc assms by auto
then have "(∃a1 u1.(v1 = a1#u1)∧(length u1 = k))"
using assms Suc_length_conv by metis
then obtain a1 u1 where "(v1 = a1#u1)∧(length u1 = k)"
using assms by auto
then have Cons_1:"(v1 = a1#u1)∧(length u1 = k)"
by auto
moreover have "length v2 = Suc k"
using assms Suc by auto
then have "(∃a2 u2.(v2 = a2#u2)∧(length u2 = k))"
using Suc_length_conv by metis
then obtain a2 u2 where "(v2 = a2#u2)∧(length u2 = k)"
by auto
then have Cons_2: "(v2 = a2#u2)∧(length u2 = k)"
by simp
then have "length u1 = length u2"
using Cons_1 by auto
then have Cons_3:"(scalar_product u1 u2) * scalar_product w1 w2 =
scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)"
using Suc Cons_1 Cons_2 assms by auto
then have "zip v1 v2 = (a1,a2)#(zip u1 u2)"
using zip_Cons Cons_1 Cons_2 by auto
then have Cons_4:"scalar_product v1 v2 = (a1*a2)+ (scalar_product u1 u2)"
unfolding scalar_product_def scalar_prodI_def by auto
then have "f (scalar_product v1 v2) (scalar_product w1 w2)
= ((a1*a2)+ (scalar_product u1 u2))*(scalar_product w1 w2)"
by auto
then have "... = ((a1*a2)*(scalar_product w1 w2))
+ ((scalar_product u1 u2)*(scalar_product w1 w2))"
using plus_right_distributivity by auto
then have Cons_5:"... = ((a1*a2)*(scalar_product w1 w2))
+ scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)"
using Cons_3 by auto
then have Cons_6:"... = (scalar_product (times a1 w1) (times a2 w2))
+ scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)"
using assms effective_scalar_product_times by auto
then have "scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
= scalar_product (vec_vec_Tensor (a1#u1) w1) (vec_vec_Tensor (a2#u2) w2)"
using Cons_1 Cons_2 by auto
moreover have "(vec_vec_Tensor (a1#u1) w1) = (times a1 w1)@(vec_vec_Tensor u1 w1)"
using vec_vec_Tensor.simps by auto
moreover have "(vec_vec_Tensor (a2#u2) w2) = (times a2 w2)@(vec_vec_Tensor u2 w2)"
using vec_vec_Tensor.simps by auto
ultimately have Cons_7:"scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
= scalar_product ((times a1 w1)@(vec_vec_Tensor u1 w1))
((times a2 w2)@(vec_vec_Tensor u2 w2))"
by auto
moreover have "length (vec_vec_Tensor u2 w2) = length (vec_vec_Tensor u1 w1)"
using assms by (metis Cons_1 Cons_2 vec_vec_Tensor_length)
moreover have "length (times a1 w1) = (length (times a2 w2))"
using assms by (metis preserving_length)
ultimately have "scalar_product ((times a1 w1)@(vec_vec_Tensor u1 w1))
((times a2 w2)@(vec_vec_Tensor u2 w2)) =
(scalar_product (times a1 w1) (times a2 w2))
+ scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)"
using effective_scalar_product_append by auto
then show ?thesis
using Cons_6 Cons_7 ‹a1 * a2 + scalar_product u1 u2 * scalar_product w1 w2
= a1 * a2 * scalar_product w1 w2
+ (scalar_product u1 u2 * scalar_product w1 w2)›
by (metis Cons_3 Cons_4 )
qed
then show ?case by auto
qed
lemma effective_scalar_product_distributivity:
assumes "length v1 = length v2" and "length w1 = length w2"
shows "(scalar_product v1 v2)*(scalar_product w1 w2)
= scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2) "
using assms scalar_product_distributivity by auto
lemma row_length_constant:assumes "mat nr nc A" and "j < length A"
shows "length (A!j) = (row_length A)"
proof(cases A)
case Nil
have "length (A!j) = 0"
using assms(2) Nil by auto
then show ?thesis using assms(2) Nil row_length_Nil by (metis)
next
case (Cons v B)
have 1:"∀x. ((x ∈ set A) ⟶ length x = nr)"
using assms unfolding mat_def Ball_def vec_def by auto
moreover have "(A!j) ∈ set A"
using assms(2) by auto
ultimately have 2:"length (A!j) = nr"
by auto
have "hd A ∈ set A"
using hd_def Cons by auto
then have "row_length A = nr"
using row_length_def 1 by auto
then show ?thesis using 2 by auto
qed
theorem row_col_match:
fixes A1 A2 B1 B2 i j
assumes wf1:"mat (row_length A1) (length A1) A1"
and wf2:"mat (row_length A2) (length A2) A2"
and wf3:"mat (row_length B1) (length B1) B1"
and wf4:"mat (row_length B2) (length B2) B2"
and matchAA:"length A1 = row_length A2"
and matchBB:"length B1 = row_length B2"
and non_Nil:"(A1 ≠ [])∧(A2 ≠ [])∧(B1 ≠ [])∧(B2 ≠ [])"
and i:"i<(row_length A1)*(row_length B1)" and j:"j< (length A2)*(length B2)"
shows "length (row A1 (i div (row_length B1)))
= length (col A2 (j div (length B2)))"
and "length (row B1 (i mod (row_length B1)))
= length (col B2 (j mod (length B2)))"
proof-
have "i div (row_length B1) < row_length A1"
using i by (metis div_left_ineq)
then have 1:"length (row A1 (i div (row_length B1))) = length A1"
unfolding row_def by auto
have "j div (length B2)< length A2"
using j by (metis div_left_ineq)
then have 2:"length (col A2 (j div (length B2))) = row_length A2"
using row_length_constant wf2 unfolding col_def by auto
with 1 matchAA show "length (row A1 (i div (row_length B1)))=length (col A2 (j div (length B2)))"
by auto
have "i mod (row_length B1) < row_length B1"
using i by (metis less_nat_zero_code mod_less_divisor mult_is_0 neq0_conv)
then have 2:"length (row B1 (i mod (row_length B1))) = length B1"
unfolding row_def by auto
have "j mod (length B2) < length B2"
using j by (metis less_nat_zero_code mod_less_divisor mult_is_0 neq0_conv)
then have "length (col B2 (j mod (length B2))) = row_length B2"
using row_length_constant wf4 unfolding col_def by auto
with 2 matchBB show "length (row B1 (i mod (row_length B1))) = length (col B2 (j mod (length B2)))"
by auto
qed
lemma effective_row_col_match: assumes "matrix_match A1 A2 B1 B2"
shows "∀i j. ((i<(row_length A1)*(row_length B1))∧(j<(length A2)*(length B2)))
⟶length (row A1 (i div (row_length B1))) = length (col A2 (j div (length B2)))"
"∀i j. ((i<(row_length A1)*(row_length B1))∧(j<(length A2)*(length B2)))
⟶length (row B1 (i mod (row_length B1))) = length (col B2 (j mod (length B2)))"
using assms row_col_match unfolding matrix_match_def by auto
theorem prelim_element_match:
"matrix_match A1 A2 B1 B2 ⟹ (∀i j.((i<(row_length A1)*(row_length B1))
∧(j<(length A2)*(length B2)))
⟶
(((A1 ∘ A2)⊗(B1 ∘ B2))!j!i
= ((A1 ⊗ B1)∘(A2 ⊗ B2))!j!i))"
proof-
assume assms:"matrix_match A1 A2 B1 B2 "
have 1:"matrix_match A1 A2 B1 B2"
using assms matrix_compose_cond_def by auto
then have 2:
"∀i j. ((i<(row_length A1)*(row_length B1))∧(j<(length A2)*(length B2)))
⟶
(((A1 ∘ A2)⊗(B1 ∘ B2))!j!i
= (scalar_product
(row A1 (i div (row_length B1))) (col A2 (j div (length B2))))
*(scalar_product
(row B1 (i mod (row_length B1))) (col B2 (j mod (length B2)))))"
using effective_matrix_match_condn_1 assms by metis
moreover from 1 have 3:"∀i j. ((i<(row_length A1)*(row_length B1))∧(j<(length A2)*(length B2))) ⟶
((A1 ⊗ B1)∘(A2 ⊗ B2))!j!i =
scalar_product
(vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1)))
(vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))"
using effective_matrix_match_condn_2 by auto
have "∀i j. ((i<(row_length A1)*(row_length B1))∧(j<(length A2)*(length B2)))
⟶length (row A1 (i div (row_length B1)))
= length (col A2 (j div (length B2)))"
and "∀i j. ((i<(row_length A1)*(row_length B1))∧(j<(length A2)*(length B2)))
⟶ length (row B1 (i mod (row_length B1)))
= length (col B2 (j mod (length B2)))"
using assms effective_row_col_match by auto
then have " ∀i j. ((i<(row_length A1)*(row_length B1))∧(j<(length A2)*(length B2)))
⟶
(scalar_product (row A1 (i div (row_length B1))) (col A2 (j div (length B2))))
*(scalar_product (row B1 (i mod (row_length B1))) (col B2 (j mod (length B2))))
= scalar_product
(vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1)))
(vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))"
using effective_scalar_product_distributivity by auto
then show ?thesis using 2 3 by auto
qed
theorem element_match:
"matrix_match A1 A2 B1 B2 ⟹(∀i<((row_length A1)*(row_length B1)).
∀j<((length A2)*(length B2)).
(((A1 ∘ A2)⊗(B1 ∘ B2))!j!i
= ((A1 ⊗ B1)∘(A2 ⊗ B2))!j!i))"
using prelim_element_match by auto
lemma application: fixes m1 m2
shows "∀m1 m2.(mat nr nc m1)
∧(mat nr nc m2)
∧(∀ j < nc. ∀ i < nr. m1 ! j ! i = m2 ! j ! i)
⟶ (m1 = m2)"
using mat_eqI by blast
theorem tensor_compose_condn:
assumes wf1:"mat nr nc ((A1∘A2)⊗(B1∘B2))"
and wf2:"mat nr nc ((A1 ⊗ B1)∘(A2 ⊗ B2))"
and wf3:"∀j<nc.∀i<nr.(((A1 ∘ A2)⊗(B1 ∘B2))!j!i
= ((A1 ⊗ B1)∘(A2 ⊗ B2))!j!i)"
shows "((A1 ∘ A2) ⊗ (B1 ∘ B2))
= ((A1 ⊗ B1)∘(A2 ⊗ B2))"
using application wf1 wf2 wf3 by blast
text‹The following theorem gives us the distributivity relation of tensor
product with matrix multiplication›
theorem distributivity:
assumes "matrix_match A1 A2 B1 B2"
shows "((A1 ∘ A2)⊗(B1∘B2)) = ((A1 ⊗ B1)∘(A2 ⊗ B2))"
proof-
let ?nr = " ((row_length A1)*(row_length B1))"
let ?nc = "((length A2)*(length B2))"
have "mat ?nr ?nc ((A1∘A2)⊗(B1∘B2))"
by (metis assms effective_tensor_compose_distribution1)
moreover have "mat ?nr ?nc ((A1 ⊗ B1)∘(A2 ⊗ B2))"
using assms by (metis effective_tensor_compose_distribution2)
moreover have "∀j<?nc.∀i<?nr.
(((A1 ∘ A2)⊗(B1 ∘B2))!j!i
= ((A1 ⊗ B1)∘(A2 ⊗ B2))!j!i)"
using element_match assms by auto
ultimately show ?thesis
using application by blast
qed
end
end