[STATEMENT]
lemma scalar_product_distributivity:
"\<forall>v1 v2 w1 w2.((length v1 = length v2)\<and>(length v1 = n)\<and> (length w1 = length w2)
           \<longrightarrow>  (scalar_product v1 v2)*(scalar_product w1 w2)
      = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v1. \<forall>v2 w1 w2. length v1 = length v2 \<and> length v1 = n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v1 v2. \<forall>w1 w2. length v1 = length v2 \<and> length v1 = n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v1 v2 w1. \<forall>w2. length v1 = length v2 \<and> length v1 = n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
proof(induct "n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
 2. \<And>n v1 v2 w1 w2. (\<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)) \<Longrightarrow> length v1 = length v2 \<and> length v1 = Suc n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
 2. \<And>n v1 v2 w1 w2. (\<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)) \<Longrightarrow> length v1 = length v2 \<and> length v1 = Suc n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
have "((length v1 = length v2)\<and>(length v1 = 0)\<and> (length w1 = length w2))
           \<longrightarrow>length v1 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> length v1 = 0
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> length v1 = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> length v1 = 0

goal (2 subgoals):
 1. \<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
 2. \<And>n v1 v2 w1 w2. (\<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)) \<Longrightarrow> length v1 = length v2 \<and> length v1 = Suc n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> length v1 = 0
[PROOF STEP]
have 1:"((length v1 = length v2)
                 \<and>(length v1 = 0)
                 \<and>(length w1 = length w2))
                        \<longrightarrow>v1 = []"
[PROOF STATE]
proof (prove)
using this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> length v1 = 0

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> v1 = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> v1 = []

goal (2 subgoals):
 1. \<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
 2. \<And>n v1 v2 w1 w2. (\<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)) \<Longrightarrow> length v1 = length v2 \<and> length v1 = Suc n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> v1 = []

goal (2 subgoals):
 1. \<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
 2. \<And>n v1 v2 w1 w2. (\<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)) \<Longrightarrow> length v1 = length v2 \<and> length v1 = Suc n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
have "((length v1 = length v2)
                   \<and>(length v1 = 0)
                   \<and>(length w1 = length w2))
           \<longrightarrow>length v2 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> length v2 = 0
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> length v2 = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> length v2 = 0

goal (2 subgoals):
 1. \<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
 2. \<And>n v1 v2 w1 w2. (\<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)) \<Longrightarrow> length v1 = length v2 \<and> length v1 = Suc n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> length v2 = 0

goal (2 subgoals):
 1. \<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
 2. \<And>n v1 v2 w1 w2. (\<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)) \<Longrightarrow> length v1 = length v2 \<and> length v1 = Suc n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> length v2 = 0
[PROOF STEP]
have 2:"((length v1 = length v2)
                          \<and>(length v1 = 0)
                          \<and>(length w1 = length w2))
                                    \<longrightarrow>v2 = []"
[PROOF STATE]
proof (prove)
using this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> length v2 = 0

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> v2 = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> v2 = []

goal (2 subgoals):
 1. \<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
 2. \<And>n v1 v2 w1 w2. (\<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)) \<Longrightarrow> length v1 = length v2 \<and> length v1 = Suc n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> v1 = []
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> length v2 = 0
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> v2 = []
[PROOF STEP]
have 3:
         "((length v1 = length v2)\<and>(length v1 = 0)\<and> (length w1 = length w2))
           \<longrightarrow>scalar_product v1 v2 = zer"
[PROOF STATE]
proof (prove)
using this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> v1 = []
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> length v2 = 0
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> v2 = []

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 = zer
[PROOF STEP]
unfolding scalar_product_def scalar_prodI_def
[PROOF STATE]
proof (prove)
using this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> v1 = []
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> length v2 = 0
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> v2 = []

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> foldr (\<lambda>(x, y). (+) (x * y)) (zip v1 v2) zer = zer
[PROOF STEP]
using zip_Nil
[PROOF STATE]
proof (prove)
using this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> v1 = []
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> length v2 = 0
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> v2 = []
zip [] [] = []

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> foldr (\<lambda>(x, y). (+) (x * y)) (zip v1 v2) zer = zer
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 = zer

goal (2 subgoals):
 1. \<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
 2. \<And>n v1 v2 w1 w2. (\<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)) \<Longrightarrow> length v1 = length v2 \<and> length v1 = Suc n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 = zer
[PROOF STEP]
have 4:"f zer (scalar_product w1 w2) = zer"
[PROOF STATE]
proof (prove)
using this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 = zer

goal (1 subgoal):
 1. zer * scalar_product w1 w2 = zer
[PROOF STEP]
using zer_left_mult
[PROOF STATE]
proof (prove)
using this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 = zer
zer * ?x = zer

goal (1 subgoal):
 1. zer * scalar_product w1 w2 = zer
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
zer * scalar_product w1 w2 = zer

goal (2 subgoals):
 1. \<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
 2. \<And>n v1 v2 w1 w2. (\<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)) \<Longrightarrow> length v1 = length v2 \<and> length v1 = Suc n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
have "((length v1 = length v2)\<and>(length v1 = 0)\<and> (length w1 = length w2))
           \<longrightarrow>vec_vec_Tensor v1 w1 = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> vec_vec_Tensor v1 w1 = []
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> v1 = []

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> vec_vec_Tensor v1 w1 = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> vec_vec_Tensor v1 w1 = []

goal (2 subgoals):
 1. \<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
 2. \<And>n v1 v2 w1 w2. (\<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)) \<Longrightarrow> length v1 = length v2 \<and> length v1 = Suc n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> vec_vec_Tensor v1 w1 = []

goal (2 subgoals):
 1. \<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
 2. \<And>n v1 v2 w1 w2. (\<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)) \<Longrightarrow> length v1 = length v2 \<and> length v1 = Suc n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
have "((length v1 = length v2)
                   \<and>(length v1 = 0)
                   \<and>(length w1 = length w2))
                    \<longrightarrow>vec_vec_Tensor v2 w2 = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> vec_vec_Tensor v2 w2 = []
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> v2 = []

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> vec_vec_Tensor v2 w2 = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> vec_vec_Tensor v2 w2 = []

goal (2 subgoals):
 1. \<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
 2. \<And>n v1 v2 w1 w2. (\<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)) \<Longrightarrow> length v1 = length v2 \<and> length v1 = Suc n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> vec_vec_Tensor v1 w1 = []
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> vec_vec_Tensor v2 w2 = []
[PROOF STEP]
have "((length v1 = length v2)
                      \<and>(length v1 = 0)
                      \<and>(length w1 = length w2))
                         \<longrightarrow> scalar_product
                                 (vec_vec_Tensor v1 w1)
                                 (vec_vec_Tensor v2 w2)  = zer"
[PROOF STATE]
proof (prove)
using this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> vec_vec_Tensor v1 w1 = []
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> vec_vec_Tensor v2 w2 = []

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2) = zer
[PROOF STEP]
unfolding scalar_product_def scalar_prodI_def
[PROOF STATE]
proof (prove)
using this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> vec_vec_Tensor v1 w1 = []
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> vec_vec_Tensor v2 w2 = []

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> foldr (\<lambda>(x, y). (+) (x * y)) (zip (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)) zer = zer
[PROOF STEP]
using zip_Nil
[PROOF STATE]
proof (prove)
using this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> vec_vec_Tensor v1 w1 = []
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> vec_vec_Tensor v2 w2 = []
zip [] [] = []

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> foldr (\<lambda>(x, y). (+) (x * y)) (zip (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)) zer = zer
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2) = zer

goal (2 subgoals):
 1. \<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
 2. \<And>n v1 v2 w1 w2. (\<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)) \<Longrightarrow> length v1 = length v2 \<and> length v1 = Suc n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
with 3 4
[PROOF STATE]
proof (chain)
picking this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 = zer
zer * scalar_product w1 w2 = zer
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2) = zer
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 = zer
zer * scalar_product w1 w2 = zer
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2) = zer

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length v1 = length v2 \<and> length v1 = 0 \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)

goal (1 subgoal):
 1. \<And>n v1 v2 w1 w2. (\<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)) \<Longrightarrow> length v1 = length v2 \<and> length v1 = Suc n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n v1 v2 w1 w2. (\<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)) \<Longrightarrow> length v1 = length v2 \<and> length v1 = Suc n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
length ?v1.0 = length ?v2.0 \<and> length ?v1.0 = k \<and> length ?w1.0 = length ?w2.0 \<longrightarrow> scalar_product ?v1.0 ?v2.0 * scalar_product ?w1.0 ?w2.0 = scalar_product (vec_vec_Tensor ?v1.0 ?w1.0) (vec_vec_Tensor ?v2.0 ?w2.0)

goal (1 subgoal):
 1. \<And>n v1 v2 w1 w2. (\<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)) \<Longrightarrow> length v1 = length v2 \<and> length v1 = Suc n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
have "((length v1 = length v2)\<and>(length v1 = Suc k)
                    \<and> (length w1 = length w2))
           \<Longrightarrow>  f (scalar_product v1 v2) (scalar_product w1 w2)
      = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
assume assms:"((length v1 = length v2)\<and>(length v1 = Suc k)
                    \<and> (length w1 = length w2))"
[PROOF STATE]
proof (state)
this:
length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
have "length v1 = Suc k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length v1 = Suc k
[PROOF STEP]
using Suc assms
[PROOF STATE]
proof (prove)
using this:
length ?v1.0 = length ?v2.0 \<and> length ?v1.0 = k \<and> length ?w1.0 = length ?w2.0 \<longrightarrow> scalar_product ?v1.0 ?v2.0 * scalar_product ?w1.0 ?w2.0 = scalar_product (vec_vec_Tensor ?v1.0 ?w1.0) (vec_vec_Tensor ?v2.0 ?w2.0)
length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2

goal (1 subgoal):
 1. length v1 = Suc k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length v1 = Suc k

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length v1 = Suc k
[PROOF STEP]
have "(\<exists>a1 u1.(v1 = a1#u1)\<and>(length u1 = k))"
[PROOF STATE]
proof (prove)
using this:
length v1 = Suc k

goal (1 subgoal):
 1. \<exists>a1 u1. v1 = a1 # u1 \<and> length u1 = k
[PROOF STEP]
using assms Suc_length_conv
[PROOF STATE]
proof (prove)
using this:
length v1 = Suc k
length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2
(Suc ?n = length ?xs) = (\<exists>y ys. ?xs = y # ys \<and> length ys = ?n)

goal (1 subgoal):
 1. \<exists>a1 u1. v1 = a1 # u1 \<and> length u1 = k
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>a1 u1. v1 = a1 # u1 \<and> length u1 = k

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a1 u1. v1 = a1 # u1 \<and> length u1 = k
[PROOF STEP]
obtain a1 u1 where "(v1 = a1#u1)\<and>(length u1 = k)"
[PROOF STATE]
proof (prove)
using this:
\<exists>a1 u1. v1 = a1 # u1 \<and> length u1 = k

goal (1 subgoal):
 1. (\<And>a1 u1. v1 = a1 # u1 \<and> length u1 = k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<exists>a1 u1. v1 = a1 # u1 \<and> length u1 = k
length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2

goal (1 subgoal):
 1. (\<And>a1 u1. v1 = a1 # u1 \<and> length u1 = k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v1 = a1 # u1 \<and> length u1 = k

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v1 = a1 # u1 \<and> length u1 = k
[PROOF STEP]
have Cons_1:"(v1 = a1#u1)\<and>(length u1 = k)"
[PROOF STATE]
proof (prove)
using this:
v1 = a1 # u1 \<and> length u1 = k

goal (1 subgoal):
 1. v1 = a1 # u1 \<and> length u1 = k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v1 = a1 # u1 \<and> length u1 = k

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v1 = a1 # u1 \<and> length u1 = k

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
have "length v2 = Suc k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length v2 = Suc k
[PROOF STEP]
using assms Suc
[PROOF STATE]
proof (prove)
using this:
length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2
length ?v1.0 = length ?v2.0 \<and> length ?v1.0 = k \<and> length ?w1.0 = length ?w2.0 \<longrightarrow> scalar_product ?v1.0 ?v2.0 * scalar_product ?w1.0 ?w2.0 = scalar_product (vec_vec_Tensor ?v1.0 ?w1.0) (vec_vec_Tensor ?v2.0 ?w2.0)

goal (1 subgoal):
 1. length v2 = Suc k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length v2 = Suc k

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length v2 = Suc k
[PROOF STEP]
have "(\<exists>a2 u2.(v2 = a2#u2)\<and>(length u2 = k))"
[PROOF STATE]
proof (prove)
using this:
length v2 = Suc k

goal (1 subgoal):
 1. \<exists>a2 u2. v2 = a2 # u2 \<and> length u2 = k
[PROOF STEP]
using  Suc_length_conv
[PROOF STATE]
proof (prove)
using this:
length v2 = Suc k
(Suc ?n = length ?xs) = (\<exists>y ys. ?xs = y # ys \<and> length ys = ?n)

goal (1 subgoal):
 1. \<exists>a2 u2. v2 = a2 # u2 \<and> length u2 = k
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>a2 u2. v2 = a2 # u2 \<and> length u2 = k

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a2 u2. v2 = a2 # u2 \<and> length u2 = k
[PROOF STEP]
obtain a2 u2 where "(v2 = a2#u2)\<and>(length u2 = k)"
[PROOF STATE]
proof (prove)
using this:
\<exists>a2 u2. v2 = a2 # u2 \<and> length u2 = k

goal (1 subgoal):
 1. (\<And>a2 u2. v2 = a2 # u2 \<and> length u2 = k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v2 = a2 # u2 \<and> length u2 = k

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v2 = a2 # u2 \<and> length u2 = k
[PROOF STEP]
have Cons_2: "(v2 = a2#u2)\<and>(length u2 = k)"
[PROOF STATE]
proof (prove)
using this:
v2 = a2 # u2 \<and> length u2 = k

goal (1 subgoal):
 1. v2 = a2 # u2 \<and> length u2 = k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v2 = a2 # u2 \<and> length u2 = k

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v2 = a2 # u2 \<and> length u2 = k
[PROOF STEP]
have "length u1 = length u2"
[PROOF STATE]
proof (prove)
using this:
v2 = a2 # u2 \<and> length u2 = k

goal (1 subgoal):
 1. length u1 = length u2
[PROOF STEP]
using Cons_1
[PROOF STATE]
proof (prove)
using this:
v2 = a2 # u2 \<and> length u2 = k
v1 = a1 # u1 \<and> length u1 = k

goal (1 subgoal):
 1. length u1 = length u2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length u1 = length u2

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length u1 = length u2
[PROOF STEP]
have Cons_3:"(scalar_product u1 u2) * scalar_product w1 w2 =
         scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)"
[PROOF STATE]
proof (prove)
using this:
length u1 = length u2

goal (1 subgoal):
 1. scalar_product u1 u2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)
[PROOF STEP]
using Suc Cons_1 Cons_2 assms
[PROOF STATE]
proof (prove)
using this:
length u1 = length u2
length ?v1.0 = length ?v2.0 \<and> length ?v1.0 = k \<and> length ?w1.0 = length ?w2.0 \<longrightarrow> scalar_product ?v1.0 ?v2.0 * scalar_product ?w1.0 ?w2.0 = scalar_product (vec_vec_Tensor ?v1.0 ?w1.0) (vec_vec_Tensor ?v2.0 ?w2.0)
v1 = a1 # u1 \<and> length u1 = k
v2 = a2 # u2 \<and> length u2 = k
length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2

goal (1 subgoal):
 1. scalar_product u1 u2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
scalar_product u1 u2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
scalar_product u1 u2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)
[PROOF STEP]
have "zip v1 v2 = (a1,a2)#(zip u1 u2)"
[PROOF STATE]
proof (prove)
using this:
scalar_product u1 u2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)

goal (1 subgoal):
 1. zip v1 v2 = (a1, a2) # zip u1 u2
[PROOF STEP]
using  zip_Cons Cons_1 Cons_2
[PROOF STATE]
proof (prove)
using this:
scalar_product u1 u2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)
length ?v = length ?w \<Longrightarrow> zip (?a # ?v) (?b # ?w) = (?a, ?b) # zip ?v ?w
v1 = a1 # u1 \<and> length u1 = k
v2 = a2 # u2 \<and> length u2 = k

goal (1 subgoal):
 1. zip v1 v2 = (a1, a2) # zip u1 u2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
zip v1 v2 = (a1, a2) # zip u1 u2

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zip v1 v2 = (a1, a2) # zip u1 u2
[PROOF STEP]
have Cons_4:"scalar_product v1 v2 =  (a1*a2)+ (scalar_product u1 u2)"
[PROOF STATE]
proof (prove)
using this:
zip v1 v2 = (a1, a2) # zip u1 u2

goal (1 subgoal):
 1. scalar_product v1 v2 = a1 * a2 + scalar_product u1 u2
[PROOF STEP]
unfolding scalar_product_def scalar_prodI_def
[PROOF STATE]
proof (prove)
using this:
zip v1 v2 = (a1, a2) # zip u1 u2

goal (1 subgoal):
 1. foldr (\<lambda>(x, y). (+) (x * y)) (zip v1 v2) zer = a1 * a2 + foldr (\<lambda>(x, y). (+) (x * y)) (zip u1 u2) zer
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
scalar_product v1 v2 = a1 * a2 + scalar_product u1 u2

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
scalar_product v1 v2 = a1 * a2 + scalar_product u1 u2
[PROOF STEP]
have "f (scalar_product v1 v2) (scalar_product w1 w2)
                      = ((a1*a2)+ (scalar_product u1 u2))*(scalar_product w1 w2)"
[PROOF STATE]
proof (prove)
using this:
scalar_product v1 v2 = a1 * a2 + scalar_product u1 u2

goal (1 subgoal):
 1. scalar_product v1 v2 * scalar_product w1 w2 = a1 * a2 + scalar_product u1 u2 * scalar_product w1 w2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
scalar_product v1 v2 * scalar_product w1 w2 = a1 * a2 + scalar_product u1 u2 * scalar_product w1 w2

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
scalar_product v1 v2 * scalar_product w1 w2 = a1 * a2 + scalar_product u1 u2 * scalar_product w1 w2
[PROOF STEP]
have "... = ((a1*a2)*(scalar_product w1 w2))
                                     + ((scalar_product u1 u2)*(scalar_product w1 w2))"
[PROOF STATE]
proof (prove)
using this:
scalar_product v1 v2 * scalar_product w1 w2 = a1 * a2 + scalar_product u1 u2 * scalar_product w1 w2

goal (1 subgoal):
 1. a1 * a2 + scalar_product u1 u2 * scalar_product w1 w2 = a1 * a2 * scalar_product w1 w2 + (scalar_product u1 u2 * scalar_product w1 w2)
[PROOF STEP]
using plus_right_distributivity
[PROOF STATE]
proof (prove)
using this:
scalar_product v1 v2 * scalar_product w1 w2 = a1 * a2 + scalar_product u1 u2 * scalar_product w1 w2
?a + ?b * ?c = ?a * ?c + (?b * ?c)

goal (1 subgoal):
 1. a1 * a2 + scalar_product u1 u2 * scalar_product w1 w2 = a1 * a2 * scalar_product w1 w2 + (scalar_product u1 u2 * scalar_product w1 w2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a1 * a2 + scalar_product u1 u2 * scalar_product w1 w2 = a1 * a2 * scalar_product w1 w2 + (scalar_product u1 u2 * scalar_product w1 w2)

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a1 * a2 + scalar_product u1 u2 * scalar_product w1 w2 = a1 * a2 * scalar_product w1 w2 + (scalar_product u1 u2 * scalar_product w1 w2)
[PROOF STEP]
have Cons_5:"... = ((a1*a2)*(scalar_product w1 w2))
                       + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)"
[PROOF STATE]
proof (prove)
using this:
a1 * a2 + scalar_product u1 u2 * scalar_product w1 w2 = a1 * a2 * scalar_product w1 w2 + (scalar_product u1 u2 * scalar_product w1 w2)

goal (1 subgoal):
 1. a1 * a2 * scalar_product w1 w2 + (scalar_product u1 u2 * scalar_product w1 w2) = a1 * a2 * scalar_product w1 w2 + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)
[PROOF STEP]
using Cons_3
[PROOF STATE]
proof (prove)
using this:
a1 * a2 + scalar_product u1 u2 * scalar_product w1 w2 = a1 * a2 * scalar_product w1 w2 + (scalar_product u1 u2 * scalar_product w1 w2)
scalar_product u1 u2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)

goal (1 subgoal):
 1. a1 * a2 * scalar_product w1 w2 + (scalar_product u1 u2 * scalar_product w1 w2) = a1 * a2 * scalar_product w1 w2 + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a1 * a2 * scalar_product w1 w2 + (scalar_product u1 u2 * scalar_product w1 w2) = a1 * a2 * scalar_product w1 w2 + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a1 * a2 * scalar_product w1 w2 + (scalar_product u1 u2 * scalar_product w1 w2) = a1 * a2 * scalar_product w1 w2 + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)
[PROOF STEP]
have Cons_6:"... = (scalar_product (times a1 w1) (times a2 w2))
                    +  scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)"
[PROOF STATE]
proof (prove)
using this:
a1 * a2 * scalar_product w1 w2 + (scalar_product u1 u2 * scalar_product w1 w2) = a1 * a2 * scalar_product w1 w2 + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)

goal (1 subgoal):
 1. a1 * a2 * scalar_product w1 w2 + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2) = scalar_product (local.times a1 w1) (local.times a2 w2) + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)
[PROOF STEP]
using assms effective_scalar_product_times
[PROOF STATE]
proof (prove)
using this:
a1 * a2 * scalar_product w1 w2 + (scalar_product u1 u2 * scalar_product w1 w2) = a1 * a2 * scalar_product w1 w2 + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)
length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2
length ?w1.0 = length ?w2.0 \<Longrightarrow> ?x * ?y * scalar_product ?w1.0 ?w2.0 = scalar_product (local.times ?x ?w1.0) (local.times ?y ?w2.0)

goal (1 subgoal):
 1. a1 * a2 * scalar_product w1 w2 + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2) = scalar_product (local.times a1 w1) (local.times a2 w2) + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a1 * a2 * scalar_product w1 w2 + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2) = scalar_product (local.times a1 w1) (local.times a2 w2) + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a1 * a2 * scalar_product w1 w2 + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2) = scalar_product (local.times a1 w1) (local.times a2 w2) + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)
[PROOF STEP]
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)"
[PROOF STATE]
proof (prove)
using this:
a1 * a2 * scalar_product w1 w2 + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2) = scalar_product (local.times a1 w1) (local.times a2 w2) + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)

goal (1 subgoal):
 1. 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)
[PROOF STEP]
using Cons_1 Cons_2
[PROOF STATE]
proof (prove)
using this:
a1 * a2 * scalar_product w1 w2 + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2) = scalar_product (local.times a1 w1) (local.times a2 w2) + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)
v1 = a1 # u1 \<and> length u1 = k
v2 = a2 # u2 \<and> length u2 = k

goal (1 subgoal):
 1. 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)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
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)

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
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)

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
have "(vec_vec_Tensor (a1#u1) w1) = (times a1 w1)@(vec_vec_Tensor u1 w1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_vec_Tensor (a1 # u1) w1 = local.times a1 w1 @ vec_vec_Tensor u1 w1
[PROOF STEP]
using vec_vec_Tensor.simps
[PROOF STATE]
proof (prove)
using this:
vec_vec_Tensor [] ?ys = []
vec_vec_Tensor (?x # ?xs) ?ys = local.times ?x ?ys @ vec_vec_Tensor ?xs ?ys

goal (1 subgoal):
 1. vec_vec_Tensor (a1 # u1) w1 = local.times a1 w1 @ vec_vec_Tensor u1 w1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec_vec_Tensor (a1 # u1) w1 = local.times a1 w1 @ vec_vec_Tensor u1 w1

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vec_vec_Tensor (a1 # u1) w1 = local.times a1 w1 @ vec_vec_Tensor u1 w1

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
have "(vec_vec_Tensor (a2#u2) w2) = (times a2 w2)@(vec_vec_Tensor u2 w2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_vec_Tensor (a2 # u2) w2 = local.times a2 w2 @ vec_vec_Tensor u2 w2
[PROOF STEP]
using vec_vec_Tensor.simps
[PROOF STATE]
proof (prove)
using this:
vec_vec_Tensor [] ?ys = []
vec_vec_Tensor (?x # ?xs) ?ys = local.times ?x ?ys @ vec_vec_Tensor ?xs ?ys

goal (1 subgoal):
 1. vec_vec_Tensor (a2 # u2) w2 = local.times a2 w2 @ vec_vec_Tensor u2 w2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec_vec_Tensor (a2 # u2) w2 = local.times a2 w2 @ vec_vec_Tensor u2 w2

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
v1 = a1 # u1 \<and> length u1 = k
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)
vec_vec_Tensor (a1 # u1) w1 = local.times a1 w1 @ vec_vec_Tensor u1 w1
vec_vec_Tensor (a2 # u2) w2 = local.times a2 w2 @ vec_vec_Tensor u2 w2
[PROOF STEP]
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))"
[PROOF STATE]
proof (prove)
using this:
v1 = a1 # u1 \<and> length u1 = k
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)
vec_vec_Tensor (a1 # u1) w1 = local.times a1 w1 @ vec_vec_Tensor u1 w1
vec_vec_Tensor (a2 # u2) w2 = local.times a2 w2 @ vec_vec_Tensor u2 w2

goal (1 subgoal):
 1. scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2) = scalar_product (local.times a1 w1 @ vec_vec_Tensor u1 w1) (local.times a2 w2 @ vec_vec_Tensor u2 w2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2) = scalar_product (local.times a1 w1 @ vec_vec_Tensor u1 w1) (local.times a2 w2 @ vec_vec_Tensor u2 w2)

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2) = scalar_product (local.times a1 w1 @ vec_vec_Tensor u1 w1) (local.times a2 w2 @ vec_vec_Tensor u2 w2)

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
have "length (vec_vec_Tensor u2 w2) = length (vec_vec_Tensor u1 w1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (vec_vec_Tensor u2 w2) = length (vec_vec_Tensor u1 w1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2

goal (1 subgoal):
 1. length (vec_vec_Tensor u2 w2) = length (vec_vec_Tensor u1 w1)
[PROOF STEP]
by (metis Cons_1 Cons_2 vec_vec_Tensor_length)
[PROOF STATE]
proof (state)
this:
length (vec_vec_Tensor u2 w2) = length (vec_vec_Tensor u1 w1)

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length (vec_vec_Tensor u2 w2) = length (vec_vec_Tensor u1 w1)

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
have "length (times a1 w1) = (length (times a2 w2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (local.times a1 w1) = length (local.times a2 w2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2

goal (1 subgoal):
 1. length (local.times a1 w1) = length (local.times a2 w2)
[PROOF STEP]
by (metis preserving_length)
[PROOF STATE]
proof (state)
this:
length (local.times a1 w1) = length (local.times a2 w2)

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2) = scalar_product (local.times a1 w1 @ vec_vec_Tensor u1 w1) (local.times a2 w2 @ vec_vec_Tensor u2 w2)
length (vec_vec_Tensor u2 w2) = length (vec_vec_Tensor u1 w1)
length (local.times a1 w1) = length (local.times a2 w2)
[PROOF STEP]
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)"
[PROOF STATE]
proof (prove)
using this:
scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2) = scalar_product (local.times a1 w1 @ vec_vec_Tensor u1 w1) (local.times a2 w2 @ vec_vec_Tensor u2 w2)
length (vec_vec_Tensor u2 w2) = length (vec_vec_Tensor u1 w1)
length (local.times a1 w1) = length (local.times a2 w2)

goal (1 subgoal):
 1. scalar_product (local.times a1 w1 @ vec_vec_Tensor u1 w1) (local.times a2 w2 @ vec_vec_Tensor u2 w2) = scalar_product (local.times a1 w1) (local.times a2 w2) + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)
[PROOF STEP]
using effective_scalar_product_append
[PROOF STATE]
proof (prove)
using this:
scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2) = scalar_product (local.times a1 w1 @ vec_vec_Tensor u1 w1) (local.times a2 w2 @ vec_vec_Tensor u2 w2)
length (vec_vec_Tensor u2 w2) = length (vec_vec_Tensor u1 w1)
length (local.times a1 w1) = length (local.times a2 w2)
\<lbrakk>length ?zs = length ?ws; length ?xs = length ?ys\<rbrakk> \<Longrightarrow> scalar_product (?xs @ ?zs) (?ys @ ?ws) = scalar_product ?xs ?ys + scalar_product ?zs ?ws

goal (1 subgoal):
 1. scalar_product (local.times a1 w1 @ vec_vec_Tensor u1 w1) (local.times a2 w2 @ vec_vec_Tensor u2 w2) = scalar_product (local.times a1 w1) (local.times a2 w2) + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
scalar_product (local.times a1 w1 @ vec_vec_Tensor u1 w1) (local.times a2 w2 @ vec_vec_Tensor u2 w2) = scalar_product (local.times a1 w1) (local.times a2 w2) + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
scalar_product (local.times a1 w1 @ vec_vec_Tensor u1 w1) (local.times a2 w2 @ vec_vec_Tensor u2 w2) = scalar_product (local.times a1 w1) (local.times a2 w2) + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
scalar_product (local.times a1 w1 @ vec_vec_Tensor u1 w1) (local.times a2 w2 @ vec_vec_Tensor u2 w2) = scalar_product (local.times a1 w1) (local.times a2 w2) + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)

goal (1 subgoal):
 1. scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
using Cons_6 Cons_7 \<open>a1 * a2 + scalar_product u1 u2 * scalar_product w1 w2
                 = a1 * a2 * scalar_product w1 w2
                  + (scalar_product u1 u2 * scalar_product w1 w2)\<close>
[PROOF STATE]
proof (prove)
using this:
scalar_product (local.times a1 w1 @ vec_vec_Tensor u1 w1) (local.times a2 w2 @ vec_vec_Tensor u2 w2) = scalar_product (local.times a1 w1) (local.times a2 w2) + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)
a1 * a2 * scalar_product w1 w2 + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2) = scalar_product (local.times a1 w1) (local.times a2 w2) + scalar_product (vec_vec_Tensor u1 w1) (vec_vec_Tensor u2 w2)
scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2) = scalar_product (local.times a1 w1 @ vec_vec_Tensor u1 w1) (local.times a2 w2 @ vec_vec_Tensor u2 w2)
a1 * a2 + scalar_product u1 u2 * scalar_product w1 w2 = a1 * a2 * scalar_product w1 w2 + (scalar_product u1 u2 * scalar_product w1 w2)

goal (1 subgoal):
 1. scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
by (metis Cons_3 Cons_4 )
[PROOF STATE]
proof (state)
this:
scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)

goal (1 subgoal):
 1. \<And>n v1 v2 w1 w2. (\<And>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)) \<Longrightarrow> length v1 = length v2 \<and> length v1 = Suc n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<Longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)

goal (1 subgoal):
 1. length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length v1 = length v2 \<and> length v1 = Suc k \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
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) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
using assms scalar_product_distributivity
[PROOF STATE]
proof (prove)
using this:
length v1 = length v2
length w1 = length w2
\<forall>v1 v2 w1 w2. length v1 = length v2 \<and> length v1 = ?n \<and> length w1 = length w2 \<longrightarrow> scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)

goal (1 subgoal):
 1. scalar_product v1 v2 * scalar_product w1 w2 = scalar_product (vec_vec_Tensor v1 w1) (vec_vec_Tensor v2 w2)
[PROOF STEP]
by auto


[STATEMENT]
lemma row_length_constant:assumes "mat nr nc A" and "j < length A"
         shows "length (A!j) = (row_length A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (A ! j) = row_length A
[PROOF STEP]
proof(cases A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A = [] \<Longrightarrow> length (A ! j) = row_length A
 2. \<And>a list. A = a # list \<Longrightarrow> length (A ! j) = row_length A
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
A = []

goal (2 subgoals):
 1. A = [] \<Longrightarrow> length (A ! j) = row_length A
 2. \<And>a list. A = a # list \<Longrightarrow> length (A ! j) = row_length A
[PROOF STEP]
have "length (A!j) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (A ! j) = 0
[PROOF STEP]
using assms(2) Nil
[PROOF STATE]
proof (prove)
using this:
j < length A
A = []

goal (1 subgoal):
 1. length (A ! j) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (A ! j) = 0

goal (2 subgoals):
 1. A = [] \<Longrightarrow> length (A ! j) = row_length A
 2. \<And>a list. A = a # list \<Longrightarrow> length (A ! j) = row_length A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (A ! j) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length (A ! j) = 0

goal (1 subgoal):
 1. length (A ! j) = row_length A
[PROOF STEP]
using assms(2) Nil row_length_Nil
[PROOF STATE]
proof (prove)
using this:
length (A ! j) = 0
j < length A
A = []
row_length [] = 0

goal (1 subgoal):
 1. length (A ! j) = row_length A
[PROOF STEP]
by (metis)
[PROOF STATE]
proof (state)
this:
length (A ! j) = row_length A

goal (1 subgoal):
 1. \<And>a list. A = a # list \<Longrightarrow> length (A ! j) = row_length A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. A = a # list \<Longrightarrow> length (A ! j) = row_length A
[PROOF STEP]
case (Cons v B)
[PROOF STATE]
proof (state)
this:
A = v # B

goal (1 subgoal):
 1. \<And>a list. A = a # list \<Longrightarrow> length (A ! j) = row_length A
[PROOF STEP]
have 1:"\<forall>x. ((x \<in> set A) \<longrightarrow> length x = nr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. x \<in> set A \<longrightarrow> length x = nr
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mat nr nc A
j < length A

goal (1 subgoal):
 1. \<forall>x. x \<in> set A \<longrightarrow> length x = nr
[PROOF STEP]
unfolding mat_def Ball_def vec_def
[PROOF STATE]
proof (prove)
using this:
length A = nc \<and> (\<forall>x. x \<in> set A \<longrightarrow> length x = nr)
j < length A

goal (1 subgoal):
 1. \<forall>x. x \<in> set A \<longrightarrow> length x = nr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<in> set A \<longrightarrow> length x = nr

goal (1 subgoal):
 1. \<And>a list. A = a # list \<Longrightarrow> length (A ! j) = row_length A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<in> set A \<longrightarrow> length x = nr

goal (1 subgoal):
 1. \<And>a list. A = a # list \<Longrightarrow> length (A ! j) = row_length A
[PROOF STEP]
have "(A!j) \<in> set A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A ! j \<in> set A
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
j < length A

goal (1 subgoal):
 1. A ! j \<in> set A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A ! j \<in> set A

goal (1 subgoal):
 1. \<And>a list. A = a # list \<Longrightarrow> length (A ! j) = row_length A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. x \<in> set A \<longrightarrow> length x = nr
A ! j \<in> set A
[PROOF STEP]
have 2:"length (A!j) = nr"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> set A \<longrightarrow> length x = nr
A ! j \<in> set A

goal (1 subgoal):
 1. length (A ! j) = nr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (A ! j) = nr

goal (1 subgoal):
 1. \<And>a list. A = a # list \<Longrightarrow> length (A ! j) = row_length A
[PROOF STEP]
have "hd A \<in> set A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd A \<in> set A
[PROOF STEP]
using hd_def Cons
[PROOF STATE]
proof (prove)
using this:
hd ?list = (case ?list of x21 # x22 \<Rightarrow> x21)
A = v # B

goal (1 subgoal):
 1. hd A \<in> set A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hd A \<in> set A

goal (1 subgoal):
 1. \<And>a list. A = a # list \<Longrightarrow> length (A ! j) = row_length A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hd A \<in> set A
[PROOF STEP]
have "row_length A = nr"
[PROOF STATE]
proof (prove)
using this:
hd A \<in> set A

goal (1 subgoal):
 1. row_length A = nr
[PROOF STEP]
using row_length_def 1
[PROOF STATE]
proof (prove)
using this:
hd A \<in> set A
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)
\<forall>x. x \<in> set A \<longrightarrow> length x = nr

goal (1 subgoal):
 1. row_length A = nr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row_length A = nr

goal (1 subgoal):
 1. \<And>a list. A = a # list \<Longrightarrow> length (A ! j) = row_length A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
row_length A = nr
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
row_length A = nr

goal (1 subgoal):
 1. length (A ! j) = row_length A
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
row_length A = nr
length (A ! j) = nr

goal (1 subgoal):
 1. length (A ! j) = row_length A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (A ! j) = row_length A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
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 \<noteq> [])\<and>(A2 \<noteq> [])\<and>(B1 \<noteq> [])\<and>(B2 \<noteq> [])"
    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 STATE]
proof (prove)
goal (1 subgoal):
 1. length (row A1 (i div row_length B1)) = length (col A2 (j div length B2)) &&& length (row B1 (i mod row_length B1)) = length (col B2 (j mod length B2))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length (row A1 (i div row_length B1)) = length (col A2 (j div length B2))
 2. length (row B1 (i mod row_length B1)) = length (col B2 (j mod length B2))
[PROOF STEP]
have "i div (row_length B1) < row_length  A1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i div row_length B1 < row_length A1
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < row_length A1 * row_length B1

goal (1 subgoal):
 1. i div row_length B1 < row_length A1
[PROOF STEP]
by (metis div_left_ineq)
[PROOF STATE]
proof (state)
this:
i div row_length B1 < row_length A1

goal (2 subgoals):
 1. length (row A1 (i div row_length B1)) = length (col A2 (j div length B2))
 2. length (row B1 (i mod row_length B1)) = length (col B2 (j mod length B2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i div row_length B1 < row_length A1
[PROOF STEP]
have 1:"length (row A1 (i div (row_length B1))) = length A1"
[PROOF STATE]
proof (prove)
using this:
i div row_length B1 < row_length A1

goal (1 subgoal):
 1. length (row A1 (i div row_length B1)) = length A1
[PROOF STEP]
unfolding row_def
[PROOF STATE]
proof (prove)
using this:
i div row_length B1 < row_length A1

goal (1 subgoal):
 1. length (map (\<lambda>w. w ! (i div row_length B1)) A1) = length A1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (row A1 (i div row_length B1)) = length A1

goal (2 subgoals):
 1. length (row A1 (i div row_length B1)) = length (col A2 (j div length B2))
 2. length (row B1 (i mod row_length B1)) = length (col B2 (j mod length B2))
[PROOF STEP]
have "j div (length B2)< length A2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j div length B2 < length A2
[PROOF STEP]
using j
[PROOF STATE]
proof (prove)
using this:
j < length A2 * length B2

goal (1 subgoal):
 1. j div length B2 < length A2
[PROOF STEP]
by (metis div_left_ineq)
[PROOF STATE]
proof (state)
this:
j div length B2 < length A2

goal (2 subgoals):
 1. length (row A1 (i div row_length B1)) = length (col A2 (j div length B2))
 2. length (row B1 (i mod row_length B1)) = length (col B2 (j mod length B2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j div length B2 < length A2
[PROOF STEP]
have 2:"length (col A2  (j div (length B2))) = row_length A2"
[PROOF STATE]
proof (prove)
using this:
j div length B2 < length A2

goal (1 subgoal):
 1. length (col A2 (j div length B2)) = row_length A2
[PROOF STEP]
using row_length_constant wf2
[PROOF STATE]
proof (prove)
using this:
j div length B2 < length A2
\<lbrakk>mat ?nr ?nc ?A; ?j < length ?A\<rbrakk> \<Longrightarrow> length (?A ! ?j) = row_length ?A
mat (row_length A2) (length A2) A2

goal (1 subgoal):
 1. length (col A2 (j div length B2)) = row_length A2
[PROOF STEP]
unfolding col_def
[PROOF STATE]
proof (prove)
using this:
j div length B2 < length A2
\<lbrakk>mat ?nr ?nc ?A; ?j < length ?A\<rbrakk> \<Longrightarrow> length (?A ! ?j) = row_length ?A
mat (row_length A2) (length A2) A2

goal (1 subgoal):
 1. length (A2 ! (j div length B2)) = row_length A2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (col A2 (j div length B2)) = row_length A2

goal (2 subgoals):
 1. length (row A1 (i div row_length B1)) = length (col A2 (j div length B2))
 2. length (row B1 (i mod row_length B1)) = length (col B2 (j mod length B2))
[PROOF STEP]
with 1 matchAA
[PROOF STATE]
proof (chain)
picking this:
length (row A1 (i div row_length B1)) = length A1
length A1 = row_length A2
length (col A2 (j div length B2)) = row_length A2
[PROOF STEP]
show "length (row A1 (i div (row_length B1)))=length (col A2  (j div (length B2)))"
[PROOF STATE]
proof (prove)
using this:
length (row A1 (i div row_length B1)) = length A1
length A1 = row_length A2
length (col A2 (j div length B2)) = row_length A2

goal (1 subgoal):
 1. length (row A1 (i div row_length B1)) = length (col A2 (j div length B2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (row A1 (i div row_length B1)) = length (col A2 (j div length B2))

goal (1 subgoal):
 1. length (row B1 (i mod row_length B1)) = length (col B2 (j mod length B2))
[PROOF STEP]
have "i mod (row_length B1) < row_length B1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i mod row_length B1 < row_length B1
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < row_length A1 * row_length B1

goal (1 subgoal):
 1. i mod row_length B1 < row_length B1
[PROOF STEP]
by (metis less_nat_zero_code mod_less_divisor mult_is_0 neq0_conv)
[PROOF STATE]
proof (state)
this:
i mod row_length B1 < row_length B1

goal (1 subgoal):
 1. length (row B1 (i mod row_length B1)) = length (col B2 (j mod length B2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i mod row_length B1 < row_length B1
[PROOF STEP]
have 2:"length (row B1 (i mod (row_length B1))) = length B1"
[PROOF STATE]
proof (prove)
using this:
i mod row_length B1 < row_length B1

goal (1 subgoal):
 1. length (row B1 (i mod row_length B1)) = length B1
[PROOF STEP]
unfolding row_def
[PROOF STATE]
proof (prove)
using this:
i mod row_length B1 < row_length B1

goal (1 subgoal):
 1. length (map (\<lambda>w. w ! (i mod row_length B1)) B1) = length B1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (row B1 (i mod row_length B1)) = length B1

goal (1 subgoal):
 1. length (row B1 (i mod row_length B1)) = length (col B2 (j mod length B2))
[PROOF STEP]
have "j mod (length B2) < length B2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j mod length B2 < length B2
[PROOF STEP]
using j
[PROOF STATE]
proof (prove)
using this:
j < length A2 * length B2

goal (1 subgoal):
 1. j mod length B2 < length B2
[PROOF STEP]
by (metis less_nat_zero_code mod_less_divisor mult_is_0 neq0_conv)
[PROOF STATE]
proof (state)
this:
j mod length B2 < length B2

goal (1 subgoal):
 1. length (row B1 (i mod row_length B1)) = length (col B2 (j mod length B2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j mod length B2 < length B2
[PROOF STEP]
have "length (col B2 (j mod (length B2))) = row_length B2"
[PROOF STATE]
proof (prove)
using this:
j mod length B2 < length B2

goal (1 subgoal):
 1. length (col B2 (j mod length B2)) = row_length B2
[PROOF STEP]
using row_length_constant wf4
[PROOF STATE]
proof (prove)
using this:
j mod length B2 < length B2
\<lbrakk>mat ?nr ?nc ?A; ?j < length ?A\<rbrakk> \<Longrightarrow> length (?A ! ?j) = row_length ?A
mat (row_length B2) (length B2) B2

goal (1 subgoal):
 1. length (col B2 (j mod length B2)) = row_length B2
[PROOF STEP]
unfolding col_def
[PROOF STATE]
proof (prove)
using this:
j mod length B2 < length B2
\<lbrakk>mat ?nr ?nc ?A; ?j < length ?A\<rbrakk> \<Longrightarrow> length (?A ! ?j) = row_length ?A
mat (row_length B2) (length B2) B2

goal (1 subgoal):
 1. length (B2 ! (j mod length B2)) = row_length B2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (col B2 (j mod length B2)) = row_length B2

goal (1 subgoal):
 1. length (row B1 (i mod row_length B1)) = length (col B2 (j mod length B2))
[PROOF STEP]
with 2 matchBB
[PROOF STATE]
proof (chain)
picking this:
length (row B1 (i mod row_length B1)) = length B1
length B1 = row_length B2
length (col B2 (j mod length B2)) = row_length B2
[PROOF STEP]
show "length (row B1 (i mod (row_length B1))) = length (col B2 (j mod (length B2)))"
[PROOF STATE]
proof (prove)
using this:
length (row B1 (i mod row_length B1)) = length B1
length B1 = row_length B2
length (col B2 (j mod length B2)) = row_length B2

goal (1 subgoal):
 1. length (row B1 (i mod row_length B1)) = length (col B2 (j mod length B2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (row B1 (i mod row_length B1)) = length (col B2 (j mod length B2))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma effective_row_col_match: assumes "matrix_match A1 A2 B1 B2"
 shows "\<forall>i j. ((i<(row_length A1)*(row_length B1))\<and>(j<(length A2)*(length B2)))
       \<longrightarrow>length (row A1 (i div (row_length B1))) = length (col A2  (j div (length B2)))"
  "\<forall>i j. ((i<(row_length A1)*(row_length B1))\<and>(j<(length A2)*(length B2)))
           \<longrightarrow>length (row B1 (i mod (row_length B1))) = length (col B2 (j mod (length B2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> length (row A1 (i div row_length B1)) = length (col A2 (j div length B2)) &&& \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> length (row B1 (i mod row_length B1)) = length (col B2 (j mod length B2))
[PROOF STEP]
using assms row_col_match
[PROOF STATE]
proof (prove)
using this:
matrix_match A1 A2 B1 B2
\<lbrakk>mat (row_length ?A1.0) (length ?A1.0) ?A1.0; mat (row_length ?A2.0) (length ?A2.0) ?A2.0; mat (row_length ?B1.0) (length ?B1.0) ?B1.0; mat (row_length ?B2.0) (length ?B2.0) ?B2.0; length ?A1.0 = row_length ?A2.0; length ?B1.0 = row_length ?B2.0; ?A1.0 \<noteq> [] \<and> ?A2.0 \<noteq> [] \<and> ?B1.0 \<noteq> [] \<and> ?B2.0 \<noteq> []; ?i < row_length ?A1.0 * row_length ?B1.0; ?j < length ?A2.0 * length ?B2.0\<rbrakk> \<Longrightarrow> length (row ?A1.0 (?i div row_length ?B1.0)) = length (col ?A2.0 (?j div length ?B2.0))
\<lbrakk>mat (row_length ?A1.0) (length ?A1.0) ?A1.0; mat (row_length ?A2.0) (length ?A2.0) ?A2.0; mat (row_length ?B1.0) (length ?B1.0) ?B1.0; mat (row_length ?B2.0) (length ?B2.0) ?B2.0; length ?A1.0 = row_length ?A2.0; length ?B1.0 = row_length ?B2.0; ?A1.0 \<noteq> [] \<and> ?A2.0 \<noteq> [] \<and> ?B1.0 \<noteq> [] \<and> ?B2.0 \<noteq> []; ?i < row_length ?A1.0 * row_length ?B1.0; ?j < length ?A2.0 * length ?B2.0\<rbrakk> \<Longrightarrow> length (row ?B1.0 (?i mod row_length ?B1.0)) = length (col ?B2.0 (?j mod length ?B2.0))

goal (1 subgoal):
 1. \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> length (row A1 (i div row_length B1)) = length (col A2 (j div length B2)) &&& \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> length (row B1 (i mod row_length B1)) = length (col B2 (j mod length B2))
[PROOF STEP]
unfolding matrix_match_def
[PROOF STATE]
proof (prove)
using this:
mat (row_length A1) (length A1) A1 \<and> mat (row_length A2) (length A2) A2 \<and> mat (row_length B1) (length B1) B1 \<and> mat (row_length B2) (length B2) B2 \<and> length A1 = row_length A2 \<and> length B1 = row_length B2 \<and> A1 \<noteq> [] \<and> A2 \<noteq> [] \<and> B1 \<noteq> [] \<and> B2 \<noteq> []
\<lbrakk>mat (row_length ?A1.0) (length ?A1.0) ?A1.0; mat (row_length ?A2.0) (length ?A2.0) ?A2.0; mat (row_length ?B1.0) (length ?B1.0) ?B1.0; mat (row_length ?B2.0) (length ?B2.0) ?B2.0; length ?A1.0 = row_length ?A2.0; length ?B1.0 = row_length ?B2.0; ?A1.0 \<noteq> [] \<and> ?A2.0 \<noteq> [] \<and> ?B1.0 \<noteq> [] \<and> ?B2.0 \<noteq> []; ?i < row_length ?A1.0 * row_length ?B1.0; ?j < length ?A2.0 * length ?B2.0\<rbrakk> \<Longrightarrow> length (row ?A1.0 (?i div row_length ?B1.0)) = length (col ?A2.0 (?j div length ?B2.0))
\<lbrakk>mat (row_length ?A1.0) (length ?A1.0) ?A1.0; mat (row_length ?A2.0) (length ?A2.0) ?A2.0; mat (row_length ?B1.0) (length ?B1.0) ?B1.0; mat (row_length ?B2.0) (length ?B2.0) ?B2.0; length ?A1.0 = row_length ?A2.0; length ?B1.0 = row_length ?B2.0; ?A1.0 \<noteq> [] \<and> ?A2.0 \<noteq> [] \<and> ?B1.0 \<noteq> [] \<and> ?B2.0 \<noteq> []; ?i < row_length ?A1.0 * row_length ?B1.0; ?j < length ?A2.0 * length ?B2.0\<rbrakk> \<Longrightarrow> length (row ?B1.0 (?i mod row_length ?B1.0)) = length (col ?B2.0 (?j mod length ?B2.0))

goal (1 subgoal):
 1. \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> length (row A1 (i div row_length B1)) = length (col A2 (j div length B2)) &&& \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> length (row B1 (i mod row_length B1)) = length (col B2 (j mod length B2))
[PROOF STEP]
by auto


[STATEMENT]
theorem prelim_element_match:
 "matrix_match A1 A2 B1 B2 \<Longrightarrow> (\<forall>i j.((i<(row_length A1)*(row_length B1))
                              \<and>(j<(length A2)*(length B2)))
         \<longrightarrow>
  (((A1 \<circ> A2)\<otimes>(B1 \<circ>  B2))!j!i
                  = ((A1 \<otimes> B1)\<circ>(A2 \<otimes> B2))!j!i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_match A1 A2 B1 B2 \<Longrightarrow> \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matrix_match A1 A2 B1 B2 \<Longrightarrow> \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i
[PROOF STEP]
assume assms:"matrix_match A1 A2 B1 B2 "
[PROOF STATE]
proof (state)
this:
matrix_match A1 A2 B1 B2

goal (1 subgoal):
 1. matrix_match A1 A2 B1 B2 \<Longrightarrow> \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i
[PROOF STEP]
have 1:"matrix_match A1 A2 B1 B2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_match A1 A2 B1 B2
[PROOF STEP]
using assms matrix_compose_cond_def
[PROOF STATE]
proof (prove)
using this:
matrix_match A1 A2 B1 B2
matrix_compose_cond ?A1.0 ?A2.0 ?B1.0 ?B2.0 ?i ?j \<equiv> mat (row_length ?A1.0) (length ?A1.0) ?A1.0 \<and> mat (row_length ?A2.0) (length ?A2.0) ?A2.0 \<and> mat (row_length ?B1.0) (length ?B1.0) ?B1.0 \<and> mat (row_length ?B2.0) (length ?B2.0) ?B2.0 \<and> length ?A1.0 = row_length ?A2.0 \<and> length ?B1.0 = row_length ?B2.0 \<and> ?A1.0 \<noteq> [] \<and> ?A2.0 \<noteq> [] \<and> ?B1.0 \<noteq> [] \<and> ?B2.0 \<noteq> [] \<and> ?i < row_length ?A1.0 * row_length ?B1.0 \<and> ?j < length ?A2.0 * length ?B2.0

goal (1 subgoal):
 1. matrix_match A1 A2 B1 B2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_match A1 A2 B1 B2

goal (1 subgoal):
 1. matrix_match A1 A2 B1 B2 \<Longrightarrow> \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
matrix_match A1 A2 B1 B2
[PROOF STEP]
have 2:
    "\<forall>i j. ((i<(row_length A1)*(row_length B1))\<and>(j<(length A2)*(length B2)))
     \<longrightarrow>
      (((A1 \<circ> A2)\<otimes>(B1 \<circ>  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)))))"
[PROOF STATE]
proof (prove)
using this:
matrix_match A1 A2 B1 B2

goal (1 subgoal):
 1. \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> 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))
[PROOF STEP]
using effective_matrix_match_condn_1 assms
[PROOF STATE]
proof (prove)
using this:
matrix_match A1 A2 B1 B2
matrix_match ?A1.0 ?A2.0 ?B1.0 ?B2.0 \<Longrightarrow> \<forall>i j. i < row_length ?A1.0 * row_length ?B1.0 \<and> j < length ?A2.0 * length ?B2.0 \<longrightarrow> (?A1.0 \<circ> ?A2.0 \<otimes> ?B1.0 \<circ> ?B2.0) ! j ! i = scalar_product (row ?A1.0 (i div row_length ?B1.0)) (col ?A2.0 (j div length ?B2.0)) * scalar_product (row ?B1.0 (i mod row_length ?B1.0)) (col ?B2.0 (j mod length ?B2.0))
matrix_match A1 A2 B1 B2

goal (1 subgoal):
 1. \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> 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))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> 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))

goal (1 subgoal):
 1. matrix_match A1 A2 B1 B2 \<Longrightarrow> \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> 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))

goal (1 subgoal):
 1. matrix_match A1 A2 B1 B2 \<Longrightarrow> \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
matrix_match A1 A2 B1 B2
[PROOF STEP]
have 3:"\<forall>i j. ((i<(row_length A1)*(row_length B1))\<and>(j<(length A2)*(length B2))) \<longrightarrow>
           ((A1 \<otimes> B1)\<circ>(A2 \<otimes> 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 STATE]
proof (prove)
using this:
matrix_match A1 A2 B1 B2

goal (1 subgoal):
 1. \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> ((A1 \<otimes> B1) \<circ> (A2 \<otimes> 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 STEP]
using effective_matrix_match_condn_2
[PROOF STATE]
proof (prove)
using this:
matrix_match A1 A2 B1 B2
matrix_match ?A1.0 ?A2.0 ?B1.0 ?B2.0 \<Longrightarrow> \<forall>i j. i < row_length ?A1.0 * row_length ?B1.0 \<and> j < length ?A2.0 * length ?B2.0 \<longrightarrow> ((?A1.0 \<otimes> ?B1.0) \<circ> (?A2.0 \<otimes> ?B2.0)) ! j ! i = scalar_product (vec_vec_Tensor (row ?A1.0 (i div row_length ?B1.0)) (row ?B1.0 (i mod row_length ?B1.0))) (vec_vec_Tensor (col ?A2.0 (j div length ?B2.0)) (col ?B2.0 (j mod length ?B2.0)))

goal (1 subgoal):
 1. \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> ((A1 \<otimes> B1) \<circ> (A2 \<otimes> 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 STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> ((A1 \<otimes> B1) \<circ> (A2 \<otimes> 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)))

goal (1 subgoal):
 1. matrix_match A1 A2 B1 B2 \<Longrightarrow> \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i
[PROOF STEP]
have  "\<forall>i j. ((i<(row_length A1)*(row_length B1))\<and>(j<(length A2)*(length B2)))
         \<longrightarrow>length (row A1 (i div (row_length B1)))
                           = length (col A2  (j div (length B2)))"
 and "\<forall>i j. ((i<(row_length A1)*(row_length B1))\<and>(j<(length A2)*(length B2)))
           \<longrightarrow> length (row B1 (i mod (row_length B1)))
                             = length (col B2 (j mod (length B2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> length (row A1 (i div row_length B1)) = length (col A2 (j div length B2)) &&& \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> length (row B1 (i mod row_length B1)) = length (col B2 (j mod length B2))
[PROOF STEP]
using assms effective_row_col_match
[PROOF STATE]
proof (prove)
using this:
matrix_match A1 A2 B1 B2
matrix_match ?A1.0 ?A2.0 ?B1.0 ?B2.0 \<Longrightarrow> \<forall>i j. i < row_length ?A1.0 * row_length ?B1.0 \<and> j < length ?A2.0 * length ?B2.0 \<longrightarrow> length (row ?A1.0 (i div row_length ?B1.0)) = length (col ?A2.0 (j div length ?B2.0))
matrix_match ?A1.0 ?A2.0 ?B1.0 ?B2.0 \<Longrightarrow> \<forall>i j. i < row_length ?A1.0 * row_length ?B1.0 \<and> j < length ?A2.0 * length ?B2.0 \<longrightarrow> length (row ?B1.0 (i mod row_length ?B1.0)) = length (col ?B2.0 (j mod length ?B2.0))

goal (1 subgoal):
 1. \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> length (row A1 (i div row_length B1)) = length (col A2 (j div length B2)) &&& \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> length (row B1 (i mod row_length B1)) = length (col B2 (j mod length B2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> length (row A1 (i div row_length B1)) = length (col A2 (j div length B2))
\<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> length (row B1 (i mod row_length B1)) = length (col B2 (j mod length B2))

goal (1 subgoal):
 1. matrix_match A1 A2 B1 B2 \<Longrightarrow> \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> length (row A1 (i div row_length B1)) = length (col A2 (j div length B2))
\<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> length (row B1 (i mod row_length B1)) = length (col B2 (j mod length B2))
[PROOF STEP]
have " \<forall>i j. ((i<(row_length A1)*(row_length B1))\<and>(j<(length A2)*(length B2)))
           \<longrightarrow>
           (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)))"
[PROOF STATE]
proof (prove)
using this:
\<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> length (row A1 (i div row_length B1)) = length (col A2 (j div length B2))
\<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> length (row B1 (i mod row_length B1)) = length (col B2 (j mod length B2))

goal (1 subgoal):
 1. \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> 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)))
[PROOF STEP]
using effective_scalar_product_distributivity
[PROOF STATE]
proof (prove)
using this:
\<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> length (row A1 (i div row_length B1)) = length (col A2 (j div length B2))
\<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> length (row B1 (i mod row_length B1)) = length (col B2 (j mod length B2))
\<lbrakk>length ?v1.0 = length ?v2.0; length ?w1.0 = length ?w2.0\<rbrakk> \<Longrightarrow> scalar_product ?v1.0 ?v2.0 * scalar_product ?w1.0 ?w2.0 = scalar_product (vec_vec_Tensor ?v1.0 ?w1.0) (vec_vec_Tensor ?v2.0 ?w2.0)

goal (1 subgoal):
 1. \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> 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)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> 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)))

goal (1 subgoal):
 1. matrix_match A1 A2 B1 B2 \<Longrightarrow> \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> 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)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> 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)))

goal (1 subgoal):
 1. \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i
[PROOF STEP]
using 2 3
[PROOF STATE]
proof (prove)
using this:
\<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> 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)))
\<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> 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))
\<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> ((A1 \<otimes> B1) \<circ> (A2 \<otimes> 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)))

goal (1 subgoal):
 1. \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem element_match:
 "matrix_match A1 A2 B1 B2 \<Longrightarrow>(\<forall>i<((row_length A1)*(row_length B1)).
                              \<forall>j<((length A2)*(length B2)).
(((A1 \<circ> A2)\<otimes>(B1 \<circ>  B2))!j!i
                  = ((A1 \<otimes> B1)\<circ>(A2 \<otimes> B2))!j!i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_match A1 A2 B1 B2 \<Longrightarrow> \<forall>i<row_length A1 * row_length B1. \<forall>j<length A2 * length B2. (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i
[PROOF STEP]
using prelim_element_match
[PROOF STATE]
proof (prove)
using this:
matrix_match ?A1.0 ?A2.0 ?B1.0 ?B2.0 \<Longrightarrow> \<forall>i j. i < row_length ?A1.0 * row_length ?B1.0 \<and> j < length ?A2.0 * length ?B2.0 \<longrightarrow> (?A1.0 \<circ> ?A2.0 \<otimes> ?B1.0 \<circ> ?B2.0) ! j ! i = ((?A1.0 \<otimes> ?B1.0) \<circ> (?A2.0 \<otimes> ?B2.0)) ! j ! i

goal (1 subgoal):
 1. matrix_match A1 A2 B1 B2 \<Longrightarrow> \<forall>i<row_length A1 * row_length B1. \<forall>j<length A2 * length B2. (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i
[PROOF STEP]
by auto


[STATEMENT]
lemma application: fixes m1 m2
shows "\<forall>m1 m2.(mat nr nc m1)
              \<and>(mat nr nc m2)
              \<and>(\<forall> j < nc. \<forall> i < nr. m1 ! j ! i = m2 ! j ! i)
                  \<longrightarrow> (m1 = m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m1 m2. mat nr nc m1 \<and> mat nr nc m2 \<and> (\<forall>j<nc. \<forall>i<nr. m1 ! j ! i = m2 ! j ! i) \<longrightarrow> m1 = m2
[PROOF STEP]
using mat_eqI
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mat ?nr ?nc ?m1.0; mat ?nr ?nc ?m2.0; \<And>i j. \<lbrakk>i < ?nc; j < ?nr\<rbrakk> \<Longrightarrow> ?m1.0 ! i ! j = ?m2.0 ! i ! j\<rbrakk> \<Longrightarrow> ?m1.0 = ?m2.0

goal (1 subgoal):
 1. \<forall>m1 m2. mat nr nc m1 \<and> mat nr nc m2 \<and> (\<forall>j<nc. \<forall>i<nr. m1 ! j ! i = m2 ! j ! i) \<longrightarrow> m1 = m2
[PROOF STEP]
by blast


[STATEMENT]
theorem tensor_compose_condn:
assumes wf1:"mat nr nc ((A1\<circ>A2)\<otimes>(B1\<circ>B2))"
   and wf2:"mat nr nc ((A1 \<otimes> B1)\<circ>(A2 \<otimes> B2))"
   and wf3:"\<forall>j<nc.\<forall>i<nr.(((A1 \<circ> A2)\<otimes>(B1 \<circ>B2))!j!i
                              = ((A1 \<otimes> B1)\<circ>(A2 \<otimes> B2))!j!i)"
 shows "((A1 \<circ> A2) \<otimes> (B1 \<circ> B2))
                              = ((A1 \<otimes> B1)\<circ>(A2 \<otimes> B2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A1 \<circ> A2 \<otimes> B1 \<circ> B2 = (A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)
[PROOF STEP]
using application wf1 wf2 wf3
[PROOF STATE]
proof (prove)
using this:
\<forall>m1 m2. mat ?nr ?nc m1 \<and> mat ?nr ?nc m2 \<and> (\<forall>j<?nc. \<forall>i<?nr. m1 ! j ! i = m2 ! j ! i) \<longrightarrow> m1 = m2
mat nr nc (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
mat nr nc ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2))
\<forall>j<nc. \<forall>i<nr. (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i

goal (1 subgoal):
 1. A1 \<circ> A2 \<otimes> B1 \<circ> B2 = (A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)
[PROOF STEP]
by blast