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

goal (2 subgoals):
 1. \<And>w1 w2. length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
 2. \<And>n w1 w2. (\<And>w1 w2. length w1 = length w2 \<and> length w1 = n \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)) \<Longrightarrow> length w1 = length w2 \<and> length w1 = Suc n \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
have "(length w1 = length w2) \<and>(length w1 = 0)  \<Longrightarrow> ?case"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length w1 = length w2 \<and> length w1 = 0 \<Longrightarrow> length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length w1 = length w2 \<and> length w1 = 0 \<Longrightarrow> length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
assume assms:"(length w1 = length w2) \<and>(length w1 = 0)"
[PROOF STATE]
proof (state)
this:
length w1 = length w2 \<and> length w1 = 0

goal (1 subgoal):
 1. length w1 = length w2 \<and> length w1 = 0 \<Longrightarrow> length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
have 1:" w1 = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w1 = []
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length w1 = length w2 \<and> length w1 = 0

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

goal (1 subgoal):
 1. length w1 = length w2 \<and> length w1 = 0 \<Longrightarrow> length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
w1 = []

goal (1 subgoal):
 1. length w1 = length w2 \<and> length w1 = 0 \<Longrightarrow> length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
have 2:"(length w1 = length w2) \<and>(length w1 = 0) \<longrightarrow> w2 = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> w2 = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> w2 = []

goal (1 subgoal):
 1. length w1 = length w2 \<and> length w1 = 0 \<Longrightarrow> length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
w1 = []
length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> w2 = []
[PROOF STEP]
have "(length w1 = length w2) \<and>(length w1 = 0)
                                   \<longrightarrow> scalar_product w1 w2 = zer"
[PROOF STATE]
proof (prove)
using this:
w1 = []
length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> w2 = []

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

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

goal (1 subgoal):
 1. length w1 = length w2 \<and> length w1 = 0 \<Longrightarrow> length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> scalar_product w1 w2 = zer
[PROOF STEP]
have 3:"(length w1 = length w2) \<and>(length w1 = 0)
                                   \<longrightarrow> (f (x*y) (scalar_product w1 w2)) = zer"
[PROOF STATE]
proof (prove)
using this:
length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> scalar_product w1 w2 = zer

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

goal (1 subgoal):
 1. length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> x * y * scalar_product w1 w2 = zer
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> x * y * scalar_product w1 w2 = zer

goal (1 subgoal):
 1. length w1 = length w2 \<and> length w1 = 0 \<Longrightarrow> length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> x * y * scalar_product w1 w2 = zer
[PROOF STEP]
have "times x w1 = []"
[PROOF STATE]
proof (prove)
using this:
length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> x * y * scalar_product w1 w2 = zer

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

goal (1 subgoal):
 1. local.times x w1 = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.times x w1 = []

goal (1 subgoal):
 1. length w1 = length w2 \<and> length w1 = 0 \<Longrightarrow> length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
local.times x w1 = []

goal (1 subgoal):
 1. length w1 = length w2 \<and> length w1 = 0 \<Longrightarrow> length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
have "times y w2 = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.times y w2 = []
[PROOF STEP]
using 2 assms
[PROOF STATE]
proof (prove)
using this:
length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> w2 = []
length w1 = length w2 \<and> length w1 = 0

goal (1 subgoal):
 1. local.times y w2 = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.times y w2 = []

goal (1 subgoal):
 1. length w1 = length w2 \<and> length w1 = 0 \<Longrightarrow> length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
local.times x w1 = []
local.times y w2 = []
[PROOF STEP]
have "(scalar_product (times x w1) ( times y w2)) = zer"
[PROOF STATE]
proof (prove)
using this:
local.times x w1 = []
local.times y w2 = []

goal (1 subgoal):
 1. scalar_product (local.times x w1) (local.times y w2) = zer
[PROOF STEP]
unfolding scalar_product_def scalar_prodI_def
[PROOF STATE]
proof (prove)
using this:
local.times x w1 = []
local.times y w2 = []

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

goal (1 subgoal):
 1. length w1 = length w2 \<and> length w1 = 0 \<Longrightarrow> length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
with 3
[PROOF STATE]
proof (chain)
picking this:
length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> x * y * scalar_product w1 w2 = zer
scalar_product (local.times x w1) (local.times y w2) = zer
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> x * y * scalar_product w1 w2 = zer
scalar_product (local.times x w1) (local.times y w2) = zer

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length w1 = length w2 \<and> length w1 = 0 \<Longrightarrow> length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)

goal (2 subgoals):
 1. \<And>w1 w2. length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
 2. \<And>n w1 w2. (\<And>w1 w2. length w1 = length w2 \<and> length w1 = n \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)) \<Longrightarrow> length w1 = length w2 \<and> length w1 = Suc n \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length w1 = length w2 \<and> length w1 = 0 \<Longrightarrow> length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length w1 = length w2 \<and> length w1 = 0 \<Longrightarrow> length w1 = length w2 \<and> length w1 = 0 \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)

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

goal (1 subgoal):
 1. \<And>n w1 w2. (\<And>w1 w2. length w1 = length w2 \<and> length w1 = n \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)) \<Longrightarrow> length w1 = length w2 \<and> length w1 = Suc n \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n w1 w2. (\<And>w1 w2. length w1 = length w2 \<and> length w1 = n \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)) \<Longrightarrow> length w1 = length w2 \<and> length w1 = Suc n \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
length ?w1.0 = length ?w2.0 \<and> length ?w1.0 = k \<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. \<And>n w1 w2. (\<And>w1 w2. length w1 = length w2 \<and> length w1 = n \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)) \<Longrightarrow> length w1 = length w2 \<and> length w1 = Suc n \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
have "(length w1 = length w2) \<and>(length w1 = (Suc k))  \<Longrightarrow> ?case"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length w1 = length w2 \<and> length w1 = Suc k \<Longrightarrow> length w1 = length w2 \<and> length w1 = Suc k \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length w1 = length w2 \<and> length w1 = Suc k \<Longrightarrow> length w1 = length w2 \<and> length w1 = Suc k \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
assume assms:"(length w1 = length w2) \<and>(length w1 = (Suc k))"
[PROOF STATE]
proof (state)
this:
length w1 = length w2 \<and> length w1 = Suc k

goal (1 subgoal):
 1. length w1 = length w2 \<and> length w1 = Suc k \<Longrightarrow> length w1 = length w2 \<and> length w1 = Suc k \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
have "\<exists>a1 u1.(w1 = a1#u1)\<and>(length u1 = k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a1 u1. w1 = a1 # u1 \<and> length u1 = k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length w1 = length w2 \<and> length w1 = Suc k

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<exists>a2 u2. w2 = a2 # u2 \<and> length u2 = k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length w2 = Suc k
length w1 = length w2 \<and> length w1 = Suc k

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. x * y * scalar_product u1 u2 = scalar_product (local.times x u1) (local.times y u2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x * y * scalar_product u1 u2 = scalar_product (local.times x u1) (local.times y u2)

goal (1 subgoal):
 1. length w1 = length w2 \<and> length w1 = Suc k \<Longrightarrow> length w1 = length w2 \<and> length w1 = Suc k \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
have "scalar_product (a1#u1) (a2#u2) = (a1*a2) + (scalar_product u1 u2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. scalar_product (a1 # u1) (a2 # u2) = a1 * a2 + scalar_product u1 u2
[PROOF STEP]
unfolding scalar_product_def scalar_prodI_def zip_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>(x, y). (+) (x * y)) (rec_list (\<lambda>xs. []) (\<lambda>y ys ysa. case_list [] (\<lambda>z zs. (z, y) # ysa zs)) (a2 # u2) (a1 # u1)) zer = a1 * a2 + foldr (\<lambda>(x, y). (+) (x * y)) (rec_list (\<lambda>xs. []) (\<lambda>y ys ysa. case_list [] (\<lambda>z zs. (z, y) # ysa zs)) u2 u1) zer
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
scalar_product (a1 # u1) (a2 # u2) = a1 * a2 + scalar_product u1 u2

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

goal (1 subgoal):
 1. scalar_product w1 w2 = a1 * a2 + scalar_product u1 u2
[PROOF STEP]
using Cons_1 Cons_2
[PROOF STATE]
proof (prove)
using this:
scalar_product (a1 # u1) (a2 # u2) = a1 * a2 + scalar_product u1 u2
w1 = a1 # u1 \<and> length u1 = k
w2 = a2 # u2 \<and> length u2 = k

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. length w1 = length w2 \<and> length w1 = Suc k \<Longrightarrow> length w1 = length w2 \<and> length w1 = Suc k \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
local.times x w1 = (x * a1) # local.times x u1
local.times y w2 = (y * a2) # local.times y u2
[PROOF STEP]
have Cons_5:"scalar_product (times x w1) (times y w2)
                            = scalar_product
                                  ((x*a1)#(times x u1))
                                  ((y*a2)#(times y u2))"
[PROOF STATE]
proof (prove)
using this:
local.times x w1 = (x * a1) # local.times x u1
local.times y w2 = (y * a2) # local.times y u2

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

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

goal (1 subgoal):
 1. scalar_product ((x * a1) # local.times x u1) ((y * a2) # local.times y u2) = x * a1 * (y * a2) + scalar_product (local.times x u1) (local.times y u2)
[PROOF STEP]
unfolding scalar_product_def scalar_prodI_def zip_def
[PROOF STATE]
proof (prove)
using this:
foldr (\<lambda>(x, y). (+) (x * y)) (rec_list (\<lambda>xs. []) (\<lambda>y ys ysa. case_list [] (\<lambda>z zs. (z, y) # ysa zs)) (local.times y w2) (local.times x w1)) zer = foldr (\<lambda>(x, y). (+) (x * y)) (rec_list (\<lambda>xs. []) (\<lambda>y ys ysa. case_list [] (\<lambda>z zs. (z, y) # ysa zs)) ((y * a2) # local.times y u2) ((x * a1) # local.times x u1)) zer

goal (1 subgoal):
 1. foldr (\<lambda>(x, y). (+) (x * y)) (rec_list (\<lambda>xs. []) (\<lambda>y ys ysa. case_list [] (\<lambda>z zs. (z, y) # ysa zs)) ((y * a2) # local.times y u2) ((x * a1) # local.times x u1)) zer = x * a1 * (y * a2) + foldr (\<lambda>(x, y). (+) (x * y)) (rec_list (\<lambda>xs. []) (\<lambda>y ys ysa. case_list [] (\<lambda>z zs. (z, y) # ysa zs)) (local.times y u2) (local.times x u1)) zer
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
scalar_product ((x * a1) # local.times x u1) ((y * a2) # local.times y u2) = x * a1 * (y * a2) + scalar_product (local.times x u1) (local.times y u2)

goal (1 subgoal):
 1. length w1 = length w2 \<and> length w1 = Suc k \<Longrightarrow> length w1 = length w2 \<and> length w1 = Suc k \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
with Cons_3 Cons_4 Cons_5
[PROOF STATE]
proof (chain)
picking this:
x * y * scalar_product u1 u2 = scalar_product (local.times x u1) (local.times y u2)
x * y * scalar_product w1 w2 = x * a1 * y * a2 + (x * y * scalar_product u1 u2)
scalar_product (local.times x w1) (local.times y w2) = scalar_product ((x * a1) # local.times x u1) ((y * a2) # local.times y u2)
scalar_product ((x * a1) # local.times x u1) ((y * a2) # local.times y u2) = x * a1 * (y * a2) + scalar_product (local.times x u1) (local.times y u2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x * y * scalar_product u1 u2 = scalar_product (local.times x u1) (local.times y u2)
x * y * scalar_product w1 w2 = x * a1 * y * a2 + (x * y * scalar_product u1 u2)
scalar_product (local.times x w1) (local.times y w2) = scalar_product ((x * a1) # local.times x u1) ((y * a2) # local.times y u2)
scalar_product ((x * a1) # local.times x u1) ((y * a2) # local.times y u2) = x * a1 * (y * a2) + scalar_product (local.times x u1) (local.times y u2)

goal (1 subgoal):
 1. length w1 = length w2 \<and> length w1 = Suc k \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
using assoc
[PROOF STATE]
proof (prove)
using this:
x * y * scalar_product u1 u2 = scalar_product (local.times x u1) (local.times y u2)
x * y * scalar_product w1 w2 = x * a1 * y * a2 + (x * y * scalar_product u1 u2)
scalar_product (local.times x w1) (local.times y w2) = scalar_product ((x * a1) # local.times x u1) ((y * a2) # local.times y u2)
scalar_product ((x * a1) # local.times x u1) ((y * a2) # local.times y u2) = x * a1 * (y * a2) + scalar_product (local.times x u1) (local.times y u2)
?a * ?b * ?c = ?a * (?b * ?c)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length w1 = length w2 \<and> length w1 = Suc k \<Longrightarrow> length w1 = length w2 \<and> length w1 = Suc k \<longrightarrow> x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma effective_scalar_product_times:
 assumes "(length w1 = length w2)"
 shows "(f (x*y) (scalar_product w1 w2))
                       = (scalar_product (times x w1) ( times y w2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
using scalar_product_times assms
[PROOF STATE]
proof (prove)
using this:
\<forall>w1 w2. length w1 = length w2 \<and> length w1 = ?n \<longrightarrow> ?x * ?y * scalar_product w1 w2 = scalar_product (local.times ?x w1) (local.times ?y w2)
length w1 = length w2

goal (1 subgoal):
 1. x * y * scalar_product w1 w2 = scalar_product (local.times x w1) (local.times y w2)
[PROOF STEP]
by auto


[STATEMENT]
lemma zip_append:"(length zs = length ws)\<and>(length xs = length ys)
                       \<Longrightarrow> (zip (xs@zs) (ys@ws)) = (zip xs ys)@(zip zs ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<Longrightarrow> zip (xs @ zs) (ys @ ws) = zip xs ys @ zip zs ws
[PROOF STEP]
using zip_append1 zip_append2
[PROOF STATE]
proof (prove)
using this:
zip (?xs @ ?ys) ?zs = zip ?xs (take (length ?xs) ?zs) @ zip ?ys (drop (length ?xs) ?zs)
zip ?xs (?ys @ ?zs) = zip (take (length ?ys) ?xs) ?ys @ zip (drop (length ?ys) ?xs) ?zs

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<Longrightarrow> zip (xs @ zs) (ys @ ws) = zip xs ys @ zip zs ws
[PROOF STEP]
by auto


[STATEMENT]
lemma scalar_product_append:
 "\<forall>xs ys zs ws.(length zs = length ws)
               \<and>(length xs = length ys)
               \<and>(length xs = n)  \<longrightarrow>
                     (scalar_product (xs@zs) (ys@ws))
                                   = (scalar_product xs ys)
                                         +(scalar_product zs ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs ys zs ws. length zs = length ws \<and> length xs = length ys \<and> length xs = n \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
apply(rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<forall>ys zs ws. length zs = length ws \<and> length xs = length ys \<and> length xs = n \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
apply(rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs ys. \<forall>zs ws. length zs = length ws \<and> length xs = length ys \<and> length xs = n \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
apply(rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs ys zs. \<forall>ws. length zs = length ws \<and> length xs = length ys \<and> length xs = n \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
apply(rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs ys zs ws. length zs = length ws \<and> length xs = length ys \<and> length xs = n \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
proof(induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs ys zs ws. length zs = length ws \<and> length xs = length ys \<and> length xs = 0 \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
 2. \<And>n xs ys zs ws. (\<And>xs ys zs ws. length zs = length ws \<and> length xs = length ys \<and> length xs = n \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws) \<Longrightarrow> length zs = length ws \<and> length xs = length ys \<and> length xs = Suc n \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>xs ys zs ws. length zs = length ws \<and> length xs = length ys \<and> length xs = 0 \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
 2. \<And>n xs ys zs ws. (\<And>xs ys zs ws. length zs = length ws \<and> length xs = length ys \<and> length xs = n \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws) \<Longrightarrow> length zs = length ws \<and> length xs = length ys \<and> length xs = Suc n \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
have "(length zs = length ws) \<and>(length xs = length ys) \<and>(length xs = 0)
          \<Longrightarrow>
           (scalar_product (xs@zs) (ys@ws))
                                   = (scalar_product xs ys)
                                          +(scalar_product zs ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = 0 \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = 0 \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
assume assms:"(length zs = length ws)\<and>(length xs = length ys)
                                        \<and>(length xs = 0)"
[PROOF STATE]
proof (state)
this:
length zs = length ws \<and> length xs = length ys \<and> length xs = 0

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = 0 \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
have 1:"xs = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = []
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length zs = length ws \<and> length xs = length ys \<and> length xs = 0

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

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = 0 \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xs = []

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = 0 \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
have 2:"ys = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ys = []
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length zs = length ws \<and> length xs = length ys \<and> length xs = 0

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

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = 0 \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
xs = []
ys = []
[PROOF STEP]
have "scalar_product xs ys = zer"
[PROOF STATE]
proof (prove)
using this:
xs = []
ys = []

goal (1 subgoal):
 1. scalar_product xs ys = zer
[PROOF STEP]
unfolding scalar_product_def scalar_prodI_def zip_def
[PROOF STATE]
proof (prove)
using this:
xs = []
ys = []

goal (1 subgoal):
 1. foldr (\<lambda>(x, y). (+) (x * y)) (rec_list (\<lambda>xs. []) (\<lambda>y ys ysa. case_list [] (\<lambda>z zs. (z, y) # ysa zs)) ys xs) zer = zer
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
scalar_product xs ys = zer

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = 0 \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
scalar_product xs ys = zer
[PROOF STEP]
have "(scalar_product xs ys)+(scalar_product zs ws)
                                       = (scalar_product zs ws)"
[PROOF STATE]
proof (prove)
using this:
scalar_product xs ys = zer

goal (1 subgoal):
 1. scalar_product xs ys + scalar_product zs ws = scalar_product zs ws
[PROOF STEP]
using plus_left_id
[PROOF STATE]
proof (prove)
using this:
scalar_product xs ys = zer
zer + ?x = ?x

goal (1 subgoal):
 1. scalar_product xs ys + scalar_product zs ws = scalar_product zs ws
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
scalar_product xs ys + scalar_product zs ws = scalar_product zs ws

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = 0 \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
scalar_product xs ys + scalar_product zs ws = scalar_product zs ws

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = 0 \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
have "(scalar_product (xs@zs) (ys@ws)) = (scalar_product zs ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. scalar_product (xs @ zs) (ys @ ws) = scalar_product zs ws
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
xs = []
ys = []

goal (1 subgoal):
 1. scalar_product (xs @ zs) (ys @ ws) = scalar_product zs ws
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
scalar_product (xs @ zs) (ys @ ws) = scalar_product zs ws

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = 0 \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
scalar_product xs ys + scalar_product zs ws = scalar_product zs ws
scalar_product (xs @ zs) (ys @ ws) = scalar_product zs ws
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
scalar_product xs ys + scalar_product zs ws = scalar_product zs ws
scalar_product (xs @ zs) (ys @ ws) = scalar_product zs ws

goal (1 subgoal):
 1. scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length zs = length ws \<and> length xs = length ys \<and> length xs = 0 \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws

goal (2 subgoals):
 1. \<And>xs ys zs ws. length zs = length ws \<and> length xs = length ys \<and> length xs = 0 \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
 2. \<And>n xs ys zs ws. (\<And>xs ys zs ws. length zs = length ws \<and> length xs = length ys \<and> length xs = n \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws) \<Longrightarrow> length zs = length ws \<and> length xs = length ys \<and> length xs = Suc n \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length zs = length ws \<and> length xs = length ys \<and> length xs = 0 \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length zs = length ws \<and> length xs = length ys \<and> length xs = 0 \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = 0 \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length zs = length ws \<and> length xs = length ys \<and> length xs = 0 \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws

goal (1 subgoal):
 1. \<And>n xs ys zs ws. (\<And>xs ys zs ws. length zs = length ws \<and> length xs = length ys \<and> length xs = n \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws) \<Longrightarrow> length zs = length ws \<and> length xs = length ys \<and> length xs = Suc n \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n xs ys zs ws. (\<And>xs ys zs ws. length zs = length ws \<and> length xs = length ys \<and> length xs = n \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws) \<Longrightarrow> length zs = length ws \<and> length xs = length ys \<and> length xs = Suc n \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
length ?zs = length ?ws \<and> length ?xs = length ?ys \<and> length ?xs = k \<longrightarrow> scalar_product (?xs @ ?zs) (?ys @ ?ws) = scalar_product ?xs ?ys + scalar_product ?zs ?ws

goal (1 subgoal):
 1. \<And>n xs ys zs ws. (\<And>xs ys zs ws. length zs = length ws \<and> length xs = length ys \<and> length xs = n \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws) \<Longrightarrow> length zs = length ws \<and> length xs = length ys \<and> length xs = Suc n \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
have "(length zs = length ws)\<and>(length xs = length ys)\<and>(length xs = (Suc k))  \<Longrightarrow>
        (scalar_product (xs@zs) (ys@ws))
                                   = (scalar_product xs ys)
                                      +(scalar_product zs ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
assume assms:"(length zs = length ws)
                   \<and>(length xs = length ys)
                   \<and>(length xs = (Suc k))"
[PROOF STATE]
proof (state)
this:
length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
have "\<exists>x xss.(xs = x#xss)\<and>(length xss = k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x xss. xs = x # xss \<and> length xss = k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k

goal (1 subgoal):
 1. \<exists>x xss. xs = x # xss \<and> length xss = k
[PROOF STEP]
by (metis Suc_length_conv)
[PROOF STATE]
proof (state)
this:
\<exists>x xss. xs = x # xss \<and> length xss = k

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x xss. xs = x # xss \<and> length xss = k
[PROOF STEP]
obtain x xss where "(xs = x#xss)\<and>(length xss = k)"
[PROOF STATE]
proof (prove)
using this:
\<exists>x xss. xs = x # xss \<and> length xss = k

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

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs = x # xss \<and> length xss = k
[PROOF STEP]
have 1:"(xs = x#xss)\<and>(length xss = k)"
[PROOF STATE]
proof (prove)
using this:
xs = x # xss \<and> length xss = k

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

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
have "\<exists>y yss.(ys = y#yss)\<and>(length yss = k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y yss. ys = y # yss \<and> length yss = k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k

goal (1 subgoal):
 1. \<exists>y yss. ys = y # yss \<and> length yss = k
[PROOF STEP]
by (metis Suc_length_conv)
[PROOF STATE]
proof (state)
this:
\<exists>y yss. ys = y # yss \<and> length yss = k

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>y yss. ys = y # yss \<and> length yss = k
[PROOF STEP]
obtain y yss where "(ys = y#yss)\<and>(length yss = k)"
[PROOF STATE]
proof (prove)
using this:
\<exists>y yss. ys = y # yss \<and> length yss = k

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

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ys = y # yss \<and> length yss = k
[PROOF STEP]
have 2:"(ys = y#yss)\<and>(length yss = k)"
[PROOF STATE]
proof (prove)
using this:
ys = y # yss \<and> length yss = k

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

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
xs = x # xss \<and> length xss = k
ys = y # yss \<and> length yss = k
[PROOF STEP]
have "length xss = length yss \<and> length xss = k"
[PROOF STATE]
proof (prove)
using this:
xs = x # xss \<and> length xss = k
ys = y # yss \<and> length yss = k

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

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xss = length yss \<and> length xss = k
[PROOF STEP]
have 3:"(scalar_product (xss@zs) (yss@ws))
                                   = (scalar_product xss yss)
                                    +(scalar_product zs ws)"
[PROOF STATE]
proof (prove)
using this:
length xss = length yss \<and> length xss = k

goal (1 subgoal):
 1. scalar_product (xss @ zs) (yss @ ws) = scalar_product xss yss + scalar_product zs ws
[PROOF STEP]
using 1 2 assms Suc
[PROOF STATE]
proof (prove)
using this:
length xss = length yss \<and> length xss = k
xs = x # xss \<and> length xss = k
ys = y # yss \<and> length yss = k
length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k
length ?zs = length ?ws \<and> length ?xs = length ?ys \<and> length ?xs = k \<longrightarrow> scalar_product (?xs @ ?zs) (?ys @ ?ws) = scalar_product ?xs ?ys + scalar_product ?zs ?ws

goal (1 subgoal):
 1. scalar_product (xss @ zs) (yss @ ws) = scalar_product xss yss + scalar_product zs ws
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
scalar_product (xss @ zs) (yss @ ws) = scalar_product xss yss + scalar_product zs ws

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
scalar_product (xss @ zs) (yss @ ws) = scalar_product xss yss + scalar_product zs ws
[PROOF STEP]
have 4:"(scalar_product ((x#xss)@zs) ((y#yss)@ws)) =
                        (scalar_product (x#(xss@zs)) (y#(yss@ws)))"
[PROOF STATE]
proof (prove)
using this:
scalar_product (xss @ zs) (yss @ ws) = scalar_product xss yss + scalar_product zs ws

goal (1 subgoal):
 1. scalar_product ((x # xss) @ zs) ((y # yss) @ ws) = scalar_product (x # xss @ zs) (y # yss @ ws)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
scalar_product ((x # xss) @ zs) ((y # yss) @ ws) = scalar_product (x # xss @ zs) (y # yss @ ws)

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
scalar_product ((x # xss) @ zs) ((y # yss) @ ws) = scalar_product (x # xss @ zs) (y # yss @ ws)
[PROOF STEP]
have "... =  (x*y) + (scalar_product (xss@zs) (yss@ws))"
[PROOF STATE]
proof (prove)
using this:
scalar_product ((x # xss) @ zs) ((y # yss) @ ws) = scalar_product (x # xss @ zs) (y # yss @ ws)

goal (1 subgoal):
 1. scalar_product (x # xss @ zs) (y # yss @ ws) = x * y + scalar_product (xss @ zs) (yss @ ws)
[PROOF STEP]
unfolding scalar_product_def scalar_prodI_def
[PROOF STATE]
proof (prove)
using this:
foldr (\<lambda>(x, y). (+) (x * y)) (zip ((x # xss) @ zs) ((y # yss) @ ws)) zer = foldr (\<lambda>(x, y). (+) (x * y)) (zip (x # xss @ zs) (y # yss @ ws)) zer

goal (1 subgoal):
 1. foldr (\<lambda>(x, y). (+) (x * y)) (zip (x # xss @ zs) (y # yss @ ws)) zer = x * y + foldr (\<lambda>(x, y). (+) (x * y)) (zip (xss @ zs) (yss @ ws)) zer
[PROOF STEP]
using zip_Cons  scalar_prodI_def scalar_prod_cons
[PROOF STATE]
proof (prove)
using this:
foldr (\<lambda>(x, y). (+) (x * y)) (zip ((x # xss) @ zs) ((y # yss) @ ws)) zer = foldr (\<lambda>(x, y). (+) (x * y)) (zip (x # xss @ zs) (y # yss @ ws)) zer
length ?v = length ?w \<Longrightarrow> zip (?a # ?v) (?b # ?w) = (?a, ?b) # zip ?v ?w
scalar_prodI ?ze ?pl ?ti ?v ?w = foldr (\<lambda>(x, y). ?pl (?ti x y)) (zip ?v ?w) ?ze
scalar_prodI ?ze ?pl ?ti (?a # ?as) (?b # ?bs) = ?pl (?ti ?a ?b) (scalar_prodI ?ze ?pl ?ti ?as ?bs)

goal (1 subgoal):
 1. foldr (\<lambda>(x, y). (+) (x * y)) (zip (x # xss @ zs) (y # yss @ ws)) zer = x * y + foldr (\<lambda>(x, y). (+) (x * y)) (zip (xss @ zs) (yss @ ws)) zer
[PROOF STEP]
by (metis)
[PROOF STATE]
proof (state)
this:
scalar_product (x # xss @ zs) (y # yss @ ws) = x * y + scalar_product (xss @ zs) (yss @ ws)

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
with 4
[PROOF STATE]
proof (chain)
picking this:
scalar_product ((x # xss) @ zs) ((y # yss) @ ws) = scalar_product (x # xss @ zs) (y # yss @ ws)
scalar_product (x # xss @ zs) (y # yss @ ws) = x * y + scalar_product (xss @ zs) (yss @ ws)
[PROOF STEP]
have 5:"(scalar_product (xs@zs) ((ys)@ws))
                       =  (x*y) + (scalar_product (xss@zs) (yss@ws))"
[PROOF STATE]
proof (prove)
using this:
scalar_product ((x # xss) @ zs) ((y # yss) @ ws) = scalar_product (x # xss @ zs) (y # yss @ ws)
scalar_product (x # xss @ zs) (y # yss @ ws) = x * y + scalar_product (xss @ zs) (yss @ ws)

goal (1 subgoal):
 1. scalar_product (xs @ zs) (ys @ ws) = x * y + scalar_product (xss @ zs) (yss @ ws)
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
scalar_product ((x # xss) @ zs) ((y # yss) @ ws) = scalar_product (x # xss @ zs) (y # yss @ ws)
scalar_product (x # xss @ zs) (y # yss @ ws) = x * y + scalar_product (xss @ zs) (yss @ ws)
xs = x # xss \<and> length xss = k
ys = y # yss \<and> length yss = k

goal (1 subgoal):
 1. scalar_product (xs @ zs) (ys @ ws) = x * y + scalar_product (xss @ zs) (yss @ ws)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
scalar_product (xs @ zs) (ys @ ws) = x * y + scalar_product (xss @ zs) (yss @ ws)

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
scalar_product (xs @ zs) (ys @ ws) = x * y + scalar_product (xss @ zs) (yss @ ws)

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
have "(scalar_product xs ys) = (x*y) + (scalar_product xss yss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. scalar_product xs ys = x * y + scalar_product xss yss
[PROOF STEP]
unfolding scalar_product_def scalar_prodI_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>(x, y). (+) (x * y)) (zip xs ys) zer = x * y + foldr (\<lambda>(x, y). (+) (x * y)) (zip xss yss) zer
[PROOF STEP]
using zip_Cons
[PROOF STATE]
proof (prove)
using this:
length ?v = length ?w \<Longrightarrow> zip (?a # ?v) (?b # ?w) = (?a, ?b) # zip ?v ?w

goal (1 subgoal):
 1. foldr (\<lambda>(x, y). (+) (x * y)) (zip xs ys) zer = x * y + foldr (\<lambda>(x, y). (+) (x * y)) (zip xss yss) zer
[PROOF STEP]
by (metis "1" "2" scalar_prodI_def scalar_prod_cons)
[PROOF STATE]
proof (state)
this:
scalar_product xs ys = x * y + scalar_product xss yss

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
scalar_product xs ys = x * y + scalar_product xss yss

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
scalar_product xs ys = x * y + scalar_product xss yss
[PROOF STEP]
have "(scalar_product xs ys)+(scalar_product zs ws)
                               =  (x*y)
                                       + (scalar_product xss yss)
                                       + (scalar_product zs ws)"
[PROOF STATE]
proof (prove)
using this:
scalar_product xs ys = x * y + scalar_product xss yss

goal (1 subgoal):
 1. scalar_product xs ys + scalar_product zs ws = x * y + scalar_product xss yss + scalar_product zs ws
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
scalar_product xs ys + scalar_product zs ws = x * y + scalar_product xss yss + scalar_product zs ws

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
scalar_product (xs @ zs) (ys @ ws) = x * y + scalar_product (xss @ zs) (yss @ ws)
scalar_product xs ys = x * y + scalar_product xss yss
scalar_product xs ys + scalar_product zs ws = x * y + scalar_product xss yss + scalar_product zs ws
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
scalar_product (xs @ zs) (ys @ ws) = x * y + scalar_product (xss @ zs) (yss @ ws)
scalar_product xs ys = x * y + scalar_product xss yss
scalar_product xs ys + scalar_product zs ws = x * y + scalar_product xss yss + scalar_product zs ws

goal (1 subgoal):
 1. scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
using 3 plus_assoc
[PROOF STATE]
proof (prove)
using this:
scalar_product (xs @ zs) (ys @ ws) = x * y + scalar_product (xss @ zs) (yss @ ws)
scalar_product xs ys = x * y + scalar_product xss yss
scalar_product xs ys + scalar_product zs ws = x * y + scalar_product xss yss + scalar_product zs ws
scalar_product (xss @ zs) (yss @ ws) = scalar_product xss yss + scalar_product zs ws
?a + ?b + ?c = ?a + (?b + ?c)

goal (1 subgoal):
 1. scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws

goal (1 subgoal):
 1. \<And>n xs ys zs ws. (\<And>xs ys zs ws. length zs = length ws \<and> length xs = length ys \<and> length xs = n \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws) \<Longrightarrow> length zs = length ws \<and> length xs = length ys \<and> length xs = Suc n \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k \<Longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws

goal (1 subgoal):
 1. length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length zs = length ws \<and> length xs = length ys \<and> length xs = Suc k \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma effective_scalar_product_append:
assumes "length zs = length ws" and  "(length xs = length ys)"
 shows "(scalar_product (xs@zs) (ys@ws)) = (scalar_product xs ys)+(scalar_product zs ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
using scalar_product_append assms
[PROOF STATE]
proof (prove)
using this:
\<forall>xs ys zs ws. length zs = length ws \<and> length xs = length ys \<and> length xs = ?n \<longrightarrow> scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
length zs = length ws
length xs = length ys

goal (1 subgoal):
 1. scalar_product (xs @ zs) (ys @ ws) = scalar_product xs ys + scalar_product zs ws
[PROOF STEP]
by auto