[STATEMENT]
lemma row_vec_mat_Tensor_prelim:
 "\<forall>i.
     ((i < (length v)*(row_length M))\<and>(mat nr (length M) M)
      \<longrightarrow> row (vec_mat_Tensor v M) i
            = times (v!(i div row_length M)) (row M (i mod row_length M)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. i < length v * row_length M \<and> mat nr (length M) M \<longrightarrow> row (vec_mat_Tensor v M) i = local.times (v ! (i div row_length M)) (row M (i mod row_length M))
[PROOF STEP]
apply(rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < length v * row_length M \<and> mat nr (length M) M \<longrightarrow> row (vec_mat_Tensor v M) i = local.times (v ! (i div row_length M)) (row M (i mod row_length M))
[PROOF STEP]
proof(induct M)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i < length v * row_length [] \<and> mat nr (length []) [] \<longrightarrow> row (vec_mat_Tensor v []) i = local.times (v ! (i div row_length [])) (row [] (i mod row_length []))
 2. \<And>a M i. (\<And>i. i < length v * row_length M \<and> mat nr (length M) M \<longrightarrow> row (vec_mat_Tensor v M) i = local.times (v ! (i div row_length M)) (row M (i mod row_length M))) \<Longrightarrow> i < length v * row_length (a # M) \<and> mat nr (length (a # M)) (a # M) \<longrightarrow> row (vec_mat_Tensor v (a # M)) i = local.times (v ! (i div row_length (a # M))) (row (a # M) (i mod row_length (a # M)))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>i. i < length v * row_length [] \<and> mat nr (length []) [] \<longrightarrow> row (vec_mat_Tensor v []) i = local.times (v ! (i div row_length [])) (row [] (i mod row_length []))
 2. \<And>a M i. (\<And>i. i < length v * row_length M \<and> mat nr (length M) M \<longrightarrow> row (vec_mat_Tensor v M) i = local.times (v ! (i div row_length M)) (row M (i mod row_length M))) \<Longrightarrow> i < length v * row_length (a # M) \<and> mat nr (length (a # M)) (a # M) \<longrightarrow> row (vec_mat_Tensor v (a # M)) i = local.times (v ! (i div row_length (a # M))) (row (a # M) (i mod row_length (a # M)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length v * row_length [] \<and> mat nr (length []) [] \<longrightarrow> row (vec_mat_Tensor v []) i = local.times (v ! (i div row_length [])) (row [] (i mod row_length []))
[PROOF STEP]
using Nil
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length v * row_length [] \<and> mat nr (length []) [] \<longrightarrow> row (vec_mat_Tensor v []) i = local.times (v ! (i div row_length [])) (row [] (i mod row_length []))
[PROOF STEP]
by (metis less_nat_zero_code mult_0_right row_length_Nil)
[PROOF STATE]
proof (state)
this:
i < length v * row_length [] \<and> mat nr (length []) [] \<longrightarrow> row (vec_mat_Tensor v []) i = local.times (v ! (i div row_length [])) (row [] (i mod row_length []))

goal (1 subgoal):
 1. \<And>a M i. (\<And>i. i < length v * row_length M \<and> mat nr (length M) M \<longrightarrow> row (vec_mat_Tensor v M) i = local.times (v ! (i div row_length M)) (row M (i mod row_length M))) \<Longrightarrow> i < length v * row_length (a # M) \<and> mat nr (length (a # M)) (a # M) \<longrightarrow> row (vec_mat_Tensor v (a # M)) i = local.times (v ! (i div row_length (a # M))) (row (a # M) (i mod row_length (a # M)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a M i. (\<And>i. i < length v * row_length M \<and> mat nr (length M) M \<longrightarrow> row (vec_mat_Tensor v M) i = local.times (v ! (i div row_length M)) (row M (i mod row_length M))) \<Longrightarrow> i < length v * row_length (a # M) \<and> mat nr (length (a # M)) (a # M) \<longrightarrow> row (vec_mat_Tensor v (a # M)) i = local.times (v ! (i div row_length (a # M))) (row (a # M) (i mod row_length (a # M)))
[PROOF STEP]
case (Cons w N)
[PROOF STATE]
proof (state)
this:
?i < length v * row_length N \<and> mat nr (length N) N \<longrightarrow> row (vec_mat_Tensor v N) ?i = local.times (v ! (?i div row_length N)) (row N (?i mod row_length N))

goal (1 subgoal):
 1. \<And>a M i. (\<And>i. i < length v * row_length M \<and> mat nr (length M) M \<longrightarrow> row (vec_mat_Tensor v M) i = local.times (v ! (i div row_length M)) (row M (i mod row_length M))) \<Longrightarrow> i < length v * row_length (a # M) \<and> mat nr (length (a # M)) (a # M) \<longrightarrow> row (vec_mat_Tensor v (a # M)) i = local.times (v ! (i div row_length (a # M))) (row (a # M) (i mod row_length (a # M)))
[PROOF STEP]
have "row (vec_mat_Tensor v (w#N)) i
                      =  row ((vec_vec_Tensor v w)#(vec_mat_Tensor v N)) i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (vec_mat_Tensor v (w # N)) i = row (vec_vec_Tensor v w # vec_mat_Tensor v N) i
[PROOF STEP]
using vec_mat_Tensor.simps
[PROOF STATE]
proof (prove)
using this:
vec_mat_Tensor ?xs [] = []
vec_mat_Tensor ?xs (?ys # ?yss) = vec_vec_Tensor ?xs ?ys # vec_mat_Tensor ?xs ?yss

goal (1 subgoal):
 1. row (vec_mat_Tensor v (w # N)) i = row (vec_vec_Tensor v w # vec_mat_Tensor v N) i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row (vec_mat_Tensor v (w # N)) i = row (vec_vec_Tensor v w # vec_mat_Tensor v N) i

goal (1 subgoal):
 1. \<And>a M i. (\<And>i. i < length v * row_length M \<and> mat nr (length M) M \<longrightarrow> row (vec_mat_Tensor v M) i = local.times (v ! (i div row_length M)) (row M (i mod row_length M))) \<Longrightarrow> i < length v * row_length (a # M) \<and> mat nr (length (a # M)) (a # M) \<longrightarrow> row (vec_mat_Tensor v (a # M)) i = local.times (v ! (i div row_length (a # M))) (row (a # M) (i mod row_length (a # M)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
row (vec_mat_Tensor v (w # N)) i = row (vec_vec_Tensor v w # vec_mat_Tensor v N) i
[PROOF STEP]
have 1:"...   = ((vec_vec_Tensor v w)!i)#(row (vec_mat_Tensor v N) i)"
[PROOF STATE]
proof (prove)
using this:
row (vec_mat_Tensor v (w # N)) i = row (vec_vec_Tensor v w # vec_mat_Tensor v N) i

goal (1 subgoal):
 1. row (vec_vec_Tensor v w # vec_mat_Tensor v N) i = vec_vec_Tensor v w ! i # row (vec_mat_Tensor v N) i
[PROOF STEP]
using row_Cons
[PROOF STATE]
proof (prove)
using this:
row (vec_mat_Tensor v (w # N)) i = row (vec_vec_Tensor v w # vec_mat_Tensor v N) i
row (?v # ?M) ?i = ?v ! ?i # row ?M ?i

goal (1 subgoal):
 1. row (vec_vec_Tensor v w # vec_mat_Tensor v N) i = vec_vec_Tensor v w ! i # row (vec_mat_Tensor v N) i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row (vec_vec_Tensor v w # vec_mat_Tensor v N) i = vec_vec_Tensor v w ! i # row (vec_mat_Tensor v N) i

goal (1 subgoal):
 1. \<And>a M i. (\<And>i. i < length v * row_length M \<and> mat nr (length M) M \<longrightarrow> row (vec_mat_Tensor v M) i = local.times (v ! (i div row_length M)) (row M (i mod row_length M))) \<Longrightarrow> i < length v * row_length (a # M) \<and> mat nr (length (a # M)) (a # M) \<longrightarrow> row (vec_mat_Tensor v (a # M)) i = local.times (v ! (i div row_length (a # M))) (row (a # M) (i mod row_length (a # M)))
[PROOF STEP]
have 2:"row_length (w#N) = length w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_length (w # N) = length w
[PROOF STEP]
using row_length_def
[PROOF STATE]
proof (prove)
using this:
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)

goal (1 subgoal):
 1. row_length (w # N) = length w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row_length (w # N) = length w

goal (1 subgoal):
 1. \<And>a M i. (\<And>i. i < length v * row_length M \<and> mat nr (length M) M \<longrightarrow> row (vec_mat_Tensor v M) i = local.times (v ! (i div row_length M)) (row M (i mod row_length M))) \<Longrightarrow> i < length v * row_length (a # M) \<and> mat nr (length (a # M)) (a # M) \<longrightarrow> row (vec_mat_Tensor v (a # M)) i = local.times (v ! (i div row_length (a # M))) (row (a # M) (i mod row_length (a # M)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
row_length (w # N) = length w
[PROOF STEP]
have 3:"(mat nr (length (w#N)) (w#N)) \<Longrightarrow> nr = length w"
[PROOF STATE]
proof (prove)
using this:
row_length (w # N) = length w

goal (1 subgoal):
 1. mat nr (length (w # N)) (w # N) \<Longrightarrow> nr = length w
[PROOF STEP]
using hd_in_set list.distinct(1) mat_uniqueness matrix_row_length
[PROOF STATE]
proof (prove)
using this:
row_length (w # N) = length w
?xs \<noteq> [] \<Longrightarrow> hd ?xs \<in> set ?xs
[] \<noteq> ?x21.0 # ?x22.0
\<lbrakk>mat ?nr1.0 ?nc ?M; mat ?nr2.0 ?nc ?M; ?z = hd ?M; ?M \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ?M. ?nr1.0 = ?nr2.0
mat ?nr ?nc ?M \<Longrightarrow> mat (row_length ?M) (length ?M) ?M

goal (1 subgoal):
 1. mat nr (length (w # N)) (w # N) \<Longrightarrow> nr = length w
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
mat nr (length (w # N)) (w # N) \<Longrightarrow> nr = length w

goal (1 subgoal):
 1. \<And>a M i. (\<And>i. i < length v * row_length M \<and> mat nr (length M) M \<longrightarrow> row (vec_mat_Tensor v M) i = local.times (v ! (i div row_length M)) (row M (i mod row_length M))) \<Longrightarrow> i < length v * row_length (a # M) \<and> mat nr (length (a # M)) (a # M) \<longrightarrow> row (vec_mat_Tensor v (a # M)) i = local.times (v ! (i div row_length (a # M))) (row (a # M) (i mod row_length (a # M)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat nr (length (w # N)) (w # N) \<Longrightarrow> nr = length w
[PROOF STEP]
have   "((i < (length v)*(row_length (w#N)))
               \<and> (mat nr (length (w#N)) (w#N))
                 \<Longrightarrow> row (vec_mat_Tensor v (w#N)) i
                           = times
                                 (v!(i div row_length (w#N)))
                                 (row (w#N) (i mod row_length (w#N))))"
[PROOF STATE]
proof (prove)
using this:
mat nr (length (w # N)) (w # N) \<Longrightarrow> nr = length w

goal (1 subgoal):
 1. i < length v * row_length (w # N) \<and> mat nr (length (w # N)) (w # N) \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>i < length v * row_length (w # N) \<and> mat nr (length (w # N)) (w # N); mat nr (length (w # N)) (w # N) \<Longrightarrow> nr = length w\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
assume assms: "i < (length v)*(row_length (w#N))
                     \<and> (mat nr (length (w#N)) (w#N))"
[PROOF STATE]
proof (state)
this:
i < length v * row_length (w # N) \<and> mat nr (length (w # N)) (w # N)

goal (1 subgoal):
 1. \<lbrakk>i < length v * row_length (w # N) \<and> mat nr (length (w # N)) (w # N); mat nr (length (w # N)) (w # N) \<Longrightarrow> nr = length w\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
proof(cases N)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. N = [] \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
 2. \<And>a list. N = a # list \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
N = []

goal (2 subgoals):
 1. N = [] \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
 2. \<And>a list. N = a # list \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
have "row (vec_mat_Tensor v (w#N)) i = [(vec_vec_Tensor v w)!i]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]
[PROOF STEP]
using 1 vec_mat_Tensor.simps  Nil row_empty
[PROOF STATE]
proof (prove)
using this:
row (vec_vec_Tensor v w # vec_mat_Tensor v N) i = vec_vec_Tensor v w ! i # row (vec_mat_Tensor v N) i
vec_mat_Tensor ?xs [] = []
vec_mat_Tensor ?xs (?ys # ?yss) = vec_vec_Tensor ?xs ?ys # vec_mat_Tensor ?xs ?yss
N = []
row [] ?i = []

goal (1 subgoal):
 1. row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]

goal (2 subgoals):
 1. N = [] \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
 2. \<And>a list. N = a # list \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]

goal (1 subgoal):
 1. row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
proof(cases w)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]; w = []\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
 2. \<And>a list. \<lbrakk>row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]; w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
w = []

goal (2 subgoals):
 1. \<lbrakk>row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]; w = []\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
 2. \<And>a list. \<lbrakk>row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]; w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
have "(vec_vec_Tensor v w) = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_vec_Tensor v w = []
[PROOF STEP]
using Nil vec_vec_Tensor_right_empty
[PROOF STATE]
proof (prove)
using this:
w = []
vec_vec_Tensor ?x [] = []

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

goal (2 subgoals):
 1. \<lbrakk>row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]; w = []\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
 2. \<And>a list. \<lbrakk>row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]; w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vec_vec_Tensor v w = []

goal (2 subgoals):
 1. \<lbrakk>row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]; w = []\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
 2. \<And>a list. \<lbrakk>row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]; w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
have " (length v)*(row_length (w#N)) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length v * row_length (w # N) = 0
[PROOF STEP]
using Nil row_length_def
[PROOF STATE]
proof (prove)
using this:
w = []
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)

goal (1 subgoal):
 1. length v * row_length (w # N) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length v * row_length (w # N) = 0

goal (2 subgoals):
 1. \<lbrakk>row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]; w = []\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
 2. \<And>a list. \<lbrakk>row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]; w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length v * row_length (w # N) = 0
[PROOF STEP]
have " [(vec_vec_Tensor v [])!i] = []"
[PROOF STATE]
proof (prove)
using this:
length v * row_length (w # N) = 0

goal (1 subgoal):
 1. [vec_vec_Tensor v [] ! i] = []
[PROOF STEP]
using assms less_nat_zero_code
[PROOF STATE]
proof (prove)
using this:
length v * row_length (w # N) = 0
i < length v * row_length (w # N) \<and> mat nr (length (w # N)) (w # N)
(?n < 0) = False

goal (1 subgoal):
 1. [vec_vec_Tensor v [] ! i] = []
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
[vec_vec_Tensor v [] ! i] = []

goal (2 subgoals):
 1. \<lbrakk>row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]; w = []\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
 2. \<And>a list. \<lbrakk>row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]; w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
vec_vec_Tensor v w = []
[vec_vec_Tensor v [] ! i] = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vec_vec_Tensor v w = []
[vec_vec_Tensor v [] ! i] = []

goal (1 subgoal):
 1. row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
using vec_vec_Tensor.simps row_empty Nil assms list.distinct(1)
[PROOF STATE]
proof (prove)
using this:
vec_vec_Tensor v w = []
[vec_vec_Tensor v [] ! i] = []
vec_vec_Tensor [] ?ys = []
vec_vec_Tensor (?x # ?xs) ?ys = local.times ?x ?ys @ vec_vec_Tensor ?xs ?ys
row [] ?i = []
w = []
i < length v * row_length (w # N) \<and> mat nr (length (w # N)) (w # N)
[] \<noteq> ?x21.0 # ?x22.0

goal (1 subgoal):
 1. row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
by (metis)
[PROOF STATE]
proof (state)
this:
row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]; w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]; w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
case (Cons a w1)
[PROOF STATE]
proof (state)
this:
w = a # w1

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]; w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
have 1:"w \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<noteq> []
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
w = a # w1

goal (1 subgoal):
 1. w \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<noteq> []

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]; w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<noteq> []
[PROOF STEP]
have "i < (length v)*(length w)"
[PROOF STATE]
proof (prove)
using this:
w \<noteq> []

goal (1 subgoal):
 1. i < length v * length w
[PROOF STEP]
using assms row_length_def
[PROOF STATE]
proof (prove)
using this:
w \<noteq> []
i < length v * row_length (w # N) \<and> mat nr (length (w # N)) (w # N)
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)

goal (1 subgoal):
 1. i < length v * length w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length v * length w

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]; w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length v * length w
[PROOF STEP]
have "(vec_vec_Tensor v w)!i
                                       = f
                                           (v!(i div (length w)))
                                           (w!(i mod (length w)))"
[PROOF STATE]
proof (prove)
using this:
i < length v * length w

goal (1 subgoal):
 1. vec_vec_Tensor v w ! i = v ! (i div length w) * w ! (i mod length w)
[PROOF STEP]
using vec_vec_Tensor_elements 1 allI
[PROOF STATE]
proof (prove)
using this:
i < length v * length w
?y \<noteq> [] \<Longrightarrow> \<forall>i<length ?x * length ?y. vec_vec_Tensor ?x ?y ! i = ?x ! (i div length ?y) * ?y ! (i mod length ?y)
w \<noteq> []
(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x

goal (1 subgoal):
 1. vec_vec_Tensor v w ! i = v ! (i div length w) * w ! (i mod length w)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec_vec_Tensor v w ! i = v ! (i div length w) * w ! (i mod length w)

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]; w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vec_vec_Tensor v w ! i = v ! (i div length w) * w ! (i mod length w)
[PROOF STEP]
have "(row (vec_mat_Tensor v (w#N)) i)
                                = times
                                      (v!(i div row_length (w#N)))
                                      (row (w#N) (i mod (length w)))"
[PROOF STATE]
proof (prove)
using this:
vec_vec_Tensor v w ! i = v ! (i div length w) * w ! (i mod length w)

goal (1 subgoal):
 1. row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod length w))
[PROOF STEP]
using Cons vec_mat_Tensor.simps row_def  row_length_def 2 Nil row_Cons
                   row_empty times.simps(1) times.simps(2)
[PROOF STATE]
proof (prove)
using this:
vec_vec_Tensor v w ! i = v ! (i div length w) * w ! (i mod length w)
w = a # w1
vec_mat_Tensor ?xs [] = []
vec_mat_Tensor ?xs (?ys # ?yss) = vec_vec_Tensor ?xs ?ys # vec_mat_Tensor ?xs ?yss
row ?m ?i \<equiv> map (\<lambda>w. w ! ?i) ?m
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)
row_length (w # N) = length w
N = []
row (?v # ?M) ?i = ?v ! ?i # row ?M ?i
row [] ?i = []
local.times ?n [] = []
local.times ?n (?y # ?ys) = (?n * ?y) # local.times ?n ?ys

goal (1 subgoal):
 1. row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod length w))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod length w))

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v (w # N)) i = [vec_vec_Tensor v w ! i]; w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod length w))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod length w))

goal (1 subgoal):
 1. row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
using row_def 2
[PROOF STATE]
proof (prove)
using this:
row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod length w))
row ?m ?i \<equiv> map (\<lambda>w. w ! ?i) ?m
row_length (w # N) = length w

goal (1 subgoal):
 1. row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))

goal (1 subgoal):
 1. \<And>a list. N = a # list \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. N = a # list \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
case (Cons w1 N1)
[PROOF STATE]
proof (state)
this:
N = w1 # N1

goal (1 subgoal):
 1. \<And>a list. N = a # list \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
have Cons_0:"row_length N = length w1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_length N = length w1
[PROOF STEP]
using Cons row_length_def
[PROOF STATE]
proof (prove)
using this:
N = w1 # N1
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)

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

goal (1 subgoal):
 1. \<And>a list. N = a # list \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
have "mat nr (length (w#w1#N1)) (w#w1#N1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat nr (length (w # w1 # N1)) (w # w1 # N1)
[PROOF STEP]
using assms Cons
[PROOF STATE]
proof (prove)
using this:
i < length v * row_length (w # N) \<and> mat nr (length (w # N)) (w # N)
N = w1 # N1

goal (1 subgoal):
 1. mat nr (length (w # w1 # N1)) (w # w1 # N1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat nr (length (w # w1 # N1)) (w # w1 # N1)

goal (1 subgoal):
 1. \<And>a list. N = a # list \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat nr (length (w # w1 # N1)) (w # w1 # N1)
[PROOF STEP]
have Cons_1:
                     "mat (row_length (w#w1#N1)) (length (w#w1#N1)) (w#w1#N1)"
[PROOF STATE]
proof (prove)
using this:
mat nr (length (w # w1 # N1)) (w # w1 # N1)

goal (1 subgoal):
 1. mat (row_length (w # w1 # N1)) (length (w # w1 # N1)) (w # w1 # N1)
[PROOF STEP]
by (metis matrix_row_length)
[PROOF STATE]
proof (state)
this:
mat (row_length (w # w1 # N1)) (length (w # w1 # N1)) (w # w1 # N1)

goal (1 subgoal):
 1. \<And>a list. N = a # list \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat (row_length (w # w1 # N1)) (length (w # w1 # N1)) (w # w1 # N1)
[PROOF STEP]
have Cons_2:
                     "mat (row_length (w1#N1)) (length (w1#N1)) (w1#N1)"
[PROOF STATE]
proof (prove)
using this:
mat (row_length (w # w1 # N1)) (length (w # w1 # N1)) (w # w1 # N1)

goal (1 subgoal):
 1. mat (row_length (w1 # N1)) (length (w1 # N1)) (w1 # N1)
[PROOF STEP]
by (metis reduct_matrix)
[PROOF STATE]
proof (state)
this:
mat (row_length (w1 # N1)) (length (w1 # N1)) (w1 # N1)

goal (1 subgoal):
 1. \<And>a list. N = a # list \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat (row_length (w1 # N1)) (length (w1 # N1)) (w1 # N1)
[PROOF STEP]
have Cons_3:"(length w1 = length w)"
[PROOF STATE]
proof (prove)
using this:
mat (row_length (w1 # N1)) (length (w1 # N1)) (w1 # N1)

goal (1 subgoal):
 1. length w1 = length w
[PROOF STEP]
using Cons_1
[PROOF STATE]
proof (prove)
using this:
mat (row_length (w1 # N1)) (length (w1 # N1)) (w1 # N1)
mat (row_length (w # w1 # N1)) (length (w # w1 # N1)) (w # w1 # N1)

goal (1 subgoal):
 1. length w1 = length w
[PROOF STEP]
unfolding mat_def row_length_def Ball_def vec_def
[PROOF STATE]
proof (prove)
using this:
length (w1 # N1) = length (w1 # N1) \<and> (\<forall>x. x \<in> set (w1 # N1) \<longrightarrow> length x = (if w1 # N1 = [] then 0 else length (hd (w1 # N1))))
length (w # w1 # N1) = length (w # w1 # N1) \<and> (\<forall>x. x \<in> set (w # w1 # N1) \<longrightarrow> length x = (if w # w1 # N1 = [] then 0 else length (hd (w # w1 # N1))))

goal (1 subgoal):
 1. length w1 = length w
[PROOF STEP]
by (metis "2" Cons_0 Cons_1 local.Cons row_length_eq)
[PROOF STATE]
proof (state)
this:
length w1 = length w

goal (1 subgoal):
 1. \<And>a list. N = a # list \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length w1 = length w
[PROOF STEP]
have Cons_4:"mat nr (length (w1#N1)) (w1#N1)"
[PROOF STATE]
proof (prove)
using this:
length w1 = length w

goal (1 subgoal):
 1. mat nr (length (w1 # N1)) (w1 # N1)
[PROOF STEP]
using 3 Cons_2 assms hd_conv_nth list.distinct(1) nth_Cons_0 row_length_def
[PROOF STATE]
proof (prove)
using this:
length w1 = length w
mat nr (length (w # N)) (w # N) \<Longrightarrow> nr = length w
mat (row_length (w1 # N1)) (length (w1 # N1)) (w1 # N1)
i < length v * row_length (w # N) \<and> mat nr (length (w # N)) (w # N)
?xs \<noteq> [] \<Longrightarrow> hd ?xs = ?xs ! 0
[] \<noteq> ?x21.0 # ?x22.0
(?x # ?xs) ! 0 = ?x
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)

goal (1 subgoal):
 1. mat nr (length (w1 # N1)) (w1 # N1)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
mat nr (length (w1 # N1)) (w1 # N1)

goal (1 subgoal):
 1. \<And>a list. N = a # list \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mat nr (length (w1 # N1)) (w1 # N1)

goal (1 subgoal):
 1. \<And>a list. N = a # list \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
have "i < (length v)*(row_length (w1#N1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length v * row_length (w1 # N1)
[PROOF STEP]
using assms Cons_3 row_length_def
[PROOF STATE]
proof (prove)
using this:
i < length v * row_length (w # N) \<and> mat nr (length (w # N)) (w # N)
length w1 = length w
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)

goal (1 subgoal):
 1. i < length v * row_length (w1 # N1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length v * row_length (w1 # N1)

goal (1 subgoal):
 1. \<And>a list. N = a # list \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mat nr (length (w1 # N1)) (w1 # N1)
i < length v * row_length (w1 # N1)
[PROOF STEP]
have Cons_5:"row (vec_mat_Tensor v N) i
                                  = times
                                      (v ! (i div row_length N))
                                      (row N (i mod row_length N))"
[PROOF STATE]
proof (prove)
using this:
mat nr (length (w1 # N1)) (w1 # N1)
i < length v * row_length (w1 # N1)

goal (1 subgoal):
 1. row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N))
[PROOF STEP]
using Cons  Cons.hyps
[PROOF STATE]
proof (prove)
using this:
mat nr (length (w1 # N1)) (w1 # N1)
i < length v * row_length (w1 # N1)
N = w1 # N1
?i < length v * row_length N \<and> mat nr (length N) N \<longrightarrow> row (vec_mat_Tensor v N) ?i = local.times (v ! (?i div row_length N)) (row N (?i mod row_length N))

goal (1 subgoal):
 1. row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N))

goal (1 subgoal):
 1. \<And>a list. N = a # list \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N))

goal (1 subgoal):
 1. row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
proof(cases w)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N)); w = []\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
 2. \<And>a list. \<lbrakk>row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N)); w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
w = []

goal (2 subgoals):
 1. \<lbrakk>row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N)); w = []\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
 2. \<And>a list. \<lbrakk>row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N)); w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
have "(vec_vec_Tensor v w) = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_vec_Tensor v w = []
[PROOF STEP]
using Nil vec_vec_Tensor_right_empty
[PROOF STATE]
proof (prove)
using this:
w = []
vec_vec_Tensor ?x [] = []

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

goal (2 subgoals):
 1. \<lbrakk>row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N)); w = []\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
 2. \<And>a list. \<lbrakk>row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N)); w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vec_vec_Tensor v w = []

goal (2 subgoals):
 1. \<lbrakk>row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N)); w = []\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
 2. \<And>a list. \<lbrakk>row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N)); w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
have " (length v)*(row_length (w#N)) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length v * row_length (w # N) = 0
[PROOF STEP]
using Nil row_length_def
[PROOF STATE]
proof (prove)
using this:
w = []
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)

goal (1 subgoal):
 1. length v * row_length (w # N) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length v * row_length (w # N) = 0

goal (2 subgoals):
 1. \<lbrakk>row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N)); w = []\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
 2. \<And>a list. \<lbrakk>row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N)); w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length v * row_length (w # N) = 0
[PROOF STEP]
have " [(vec_vec_Tensor v [])!i] = []"
[PROOF STATE]
proof (prove)
using this:
length v * row_length (w # N) = 0

goal (1 subgoal):
 1. [vec_vec_Tensor v [] ! i] = []
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length v * row_length (w # N) = 0
i < length v * row_length (w # N) \<and> mat nr (length (w # N)) (w # N)

goal (1 subgoal):
 1. [vec_vec_Tensor v [] ! i] = []
[PROOF STEP]
by (metis less_nat_zero_code)
[PROOF STATE]
proof (state)
this:
[vec_vec_Tensor v [] ! i] = []

goal (2 subgoals):
 1. \<lbrakk>row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N)); w = []\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
 2. \<And>a list. \<lbrakk>row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N)); w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
vec_vec_Tensor v w = []
[vec_vec_Tensor v [] ! i] = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vec_vec_Tensor v w = []
[vec_vec_Tensor v [] ! i] = []

goal (1 subgoal):
 1. row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
using vec_vec_Tensor.simps row_empty Nil assms
[PROOF STATE]
proof (prove)
using this:
vec_vec_Tensor v w = []
[vec_vec_Tensor v [] ! i] = []
vec_vec_Tensor [] ?ys = []
vec_vec_Tensor (?x # ?xs) ?ys = local.times ?x ?ys @ vec_vec_Tensor ?xs ?ys
row [] ?i = []
w = []
i < length v * row_length (w # N) \<and> mat nr (length (w # N)) (w # N)

goal (1 subgoal):
 1. row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
by (metis list.distinct(1))
[PROOF STATE]
proof (state)
this:
row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N)); w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N)); w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
case (Cons a w2)
[PROOF STATE]
proof (state)
this:
w = a # w2

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N)); w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
have 1:"w \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<noteq> []
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
w = a # w2

goal (1 subgoal):
 1. w \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<noteq> []

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N)); w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<noteq> []
[PROOF STEP]
have "i < (length v)*(length w)"
[PROOF STATE]
proof (prove)
using this:
w \<noteq> []

goal (1 subgoal):
 1. i < length v * length w
[PROOF STEP]
using assms row_length_def
[PROOF STATE]
proof (prove)
using this:
w \<noteq> []
i < length v * row_length (w # N) \<and> mat nr (length (w # N)) (w # N)
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)

goal (1 subgoal):
 1. i < length v * length w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length v * length w

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N)); w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length v * length w
[PROOF STEP]
have ConsCons_2:
                     "(vec_vec_Tensor v w)!i = f
                                                 (v!(i div (length w)))
                                                 (w!(i mod (length w)))"
[PROOF STATE]
proof (prove)
using this:
i < length v * length w

goal (1 subgoal):
 1. vec_vec_Tensor v w ! i = v ! (i div length w) * w ! (i mod length w)
[PROOF STEP]
using vec_vec_Tensor_elements 1 allI
[PROOF STATE]
proof (prove)
using this:
i < length v * length w
?y \<noteq> [] \<Longrightarrow> \<forall>i<length ?x * length ?y. vec_vec_Tensor ?x ?y ! i = ?x ! (i div length ?y) * ?y ! (i mod length ?y)
w \<noteq> []
(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x

goal (1 subgoal):
 1. vec_vec_Tensor v w ! i = v ! (i div length w) * w ! (i mod length w)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec_vec_Tensor v w ! i = v ! (i div length w) * w ! (i mod length w)

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N)); w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vec_vec_Tensor v w ! i = v ! (i div length w) * w ! (i mod length w)

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N)); w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
have
                      "times
                              (v!(i div row_length (w#N)))
                              (row (w#N) (i mod row_length (w#N)))
                             = (f
                                 (v!(i div (length w)))
                                 (w!(i mod (length w))))
                                  #(times (v ! (i div row_length N))
                                          (row N (i mod row_length N)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N))) = (v ! (i div length w) * w ! (i mod length w)) # local.times (v ! (i div row_length N)) (row N (i mod row_length N))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N))) = (v ! (i div length w) * w ! (i mod length w)) # local.times (v ! (i div row_length N)) (row N (i mod row_length N))
[PROOF STEP]
have temp:"row_length (w#N) = (row_length N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_length (w # N) = row_length N
[PROOF STEP]
using row_length_def 2 Cons_3 Cons_0
[PROOF STATE]
proof (prove)
using this:
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)
row_length (w # N) = length w
length w1 = length w
row_length N = length w1

goal (1 subgoal):
 1. row_length (w # N) = row_length N
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row_length (w # N) = row_length N

goal (1 subgoal):
 1. local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N))) = (v ! (i div length w) * w ! (i mod length w)) # local.times (v ! (i div row_length N)) (row N (i mod row_length N))
[PROOF STEP]
have "(row (w#N) (i mod row_length (w#N)))
                              = (w!(i mod (row_length (w#N))))
                                       #(row N (i mod row_length (w#N)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (w # N) (i mod row_length (w # N)) = w ! (i mod row_length (w # N)) # row N (i mod row_length (w # N))
[PROOF STEP]
unfolding row_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>wa. wa ! (i mod row_length (w # N))) (w # N) = w ! (i mod row_length (w # N)) # map (\<lambda>wa. wa ! (i mod row_length (w # N))) N
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row (w # N) (i mod row_length (w # N)) = w ! (i mod row_length (w # N)) # row N (i mod row_length (w # N))

goal (1 subgoal):
 1. local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N))) = (v ! (i div length w) * w ! (i mod length w)) # local.times (v ! (i div row_length N)) (row N (i mod row_length N))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
row (w # N) (i mod row_length (w # N)) = w ! (i mod row_length (w # N)) # row N (i mod row_length (w # N))
[PROOF STEP]
have "...
                              = (w!(i mod (length w)))
                                        #(row N (i mod row_length N))"
[PROOF STATE]
proof (prove)
using this:
row (w # N) (i mod row_length (w # N)) = w ! (i mod row_length (w # N)) # row N (i mod row_length (w # N))

goal (1 subgoal):
 1. w ! (i mod row_length (w # N)) # row N (i mod row_length (w # N)) = w ! (i mod length w) # row N (i mod row_length N)
[PROOF STEP]
using Cons_3 3 assms 2 neq_Nil_conv row_Cons row_empty
                           row_length_eq
[PROOF STATE]
proof (prove)
using this:
row (w # N) (i mod row_length (w # N)) = w ! (i mod row_length (w # N)) # row N (i mod row_length (w # N))
length w1 = length w
mat nr (length (w # N)) (w # N) \<Longrightarrow> nr = length w
i < length v * row_length (w # N) \<and> mat nr (length (w # N)) (w # N)
row_length (w # N) = length w
(?xs \<noteq> []) = (\<exists>y ys. ?xs = y # ys)
row (?v # ?M) ?i = ?v ! ?i # row ?M ?i
row [] ?i = []
mat (row_length (?a # ?b # ?N)) (length (?a # ?b # ?N)) (?a # ?b # ?N) \<longrightarrow> row_length (?a # ?b # ?N) = row_length (?b # ?N)

goal (1 subgoal):
 1. w ! (i mod row_length (w # N)) # row N (i mod row_length (w # N)) = w ! (i mod length w) # row N (i mod row_length N)
[PROOF STEP]
by (metis (opaque_lifting, no_types))
[PROOF STATE]
proof (state)
this:
w ! (i mod row_length (w # N)) # row N (i mod row_length (w # N)) = w ! (i mod length w) # row N (i mod row_length N)

goal (1 subgoal):
 1. local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N))) = (v ! (i div length w) * w ! (i mod length w)) # local.times (v ! (i div row_length N)) (row N (i mod row_length N))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w ! (i mod row_length (w # N)) # row N (i mod row_length (w # N)) = w ! (i mod length w) # row N (i mod row_length N)
[PROOF STEP]
have "times
                           (v!(i div row_length (w#N)))
                           ((w!(i mod (length w)))
                             #(row N (i mod row_length N)))
                               = (f
                                     (v!(i div row_length (w#N)))
                                     (w!(i mod (length w))))
                                         #(times  (v!(i div row_length (w#N)))
                                                      (row N (i mod row_length N)))"
[PROOF STATE]
proof (prove)
using this:
w ! (i mod row_length (w # N)) # row N (i mod row_length (w # N)) = w ! (i mod length w) # row N (i mod row_length N)

goal (1 subgoal):
 1. local.times (v ! (i div row_length (w # N))) (w ! (i mod length w) # row N (i mod row_length N)) = (v ! (i div row_length (w # N)) * w ! (i mod length w)) # local.times (v ! (i div row_length (w # N))) (row N (i mod row_length N))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.times (v ! (i div row_length (w # N))) (w ! (i mod length w) # row N (i mod row_length N)) = (v ! (i div row_length (w # N)) * w ! (i mod length w)) # local.times (v ! (i div row_length (w # N))) (row N (i mod row_length N))

goal (1 subgoal):
 1. local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N))) = (v ! (i div length w) * w ! (i mod length w)) # local.times (v ! (i div row_length N)) (row N (i mod row_length N))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
local.times (v ! (i div row_length (w # N))) (w ! (i mod length w) # row N (i mod row_length N)) = (v ! (i div row_length (w # N)) * w ! (i mod length w)) # local.times (v ! (i div row_length (w # N))) (row N (i mod row_length N))
[PROOF STEP]
have "... =  (f
                                       (v!(i div length w))
                                       (w!(i mod (length w))))
                                         #(times  (v!(i div row_length N))
                                                  (row N (i mod row_length N)))"
[PROOF STATE]
proof (prove)
using this:
local.times (v ! (i div row_length (w # N))) (w ! (i mod length w) # row N (i mod row_length N)) = (v ! (i div row_length (w # N)) * w ! (i mod length w)) # local.times (v ! (i div row_length (w # N))) (row N (i mod row_length N))

goal (1 subgoal):
 1. (v ! (i div row_length (w # N)) * w ! (i mod length w)) # local.times (v ! (i div row_length (w # N))) (row N (i mod row_length N)) = (v ! (i div length w) * w ! (i mod length w)) # local.times (v ! (i div row_length N)) (row N (i mod row_length N))
[PROOF STEP]
using 3 Cons_3 assms temp row_length_def
[PROOF STATE]
proof (prove)
using this:
local.times (v ! (i div row_length (w # N))) (w ! (i mod length w) # row N (i mod row_length N)) = (v ! (i div row_length (w # N)) * w ! (i mod length w)) # local.times (v ! (i div row_length (w # N))) (row N (i mod row_length N))
mat nr (length (w # N)) (w # N) \<Longrightarrow> nr = length w
length w1 = length w
i < length v * row_length (w # N) \<and> mat nr (length (w # N)) (w # N)
row_length (w # N) = row_length N
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)

goal (1 subgoal):
 1. (v ! (i div row_length (w # N)) * w ! (i mod length w)) # local.times (v ! (i div row_length (w # N))) (row N (i mod row_length N)) = (v ! (i div length w) * w ! (i mod length w)) # local.times (v ! (i div row_length N)) (row N (i mod row_length N))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(v ! (i div row_length (w # N)) * w ! (i mod length w)) # local.times (v ! (i div row_length (w # N))) (row N (i mod row_length N)) = (v ! (i div length w) * w ! (i mod length w)) # local.times (v ! (i div row_length N)) (row N (i mod row_length N))

goal (1 subgoal):
 1. local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N))) = (v ! (i div length w) * w ! (i mod length w)) # local.times (v ! (i div row_length N)) (row N (i mod row_length N))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(v ! (i div row_length (w # N)) * w ! (i mod length w)) # local.times (v ! (i div row_length (w # N))) (row N (i mod row_length N)) = (v ! (i div length w) * w ! (i mod length w)) # local.times (v ! (i div row_length N)) (row N (i mod row_length N))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(v ! (i div row_length (w # N)) * w ! (i mod length w)) # local.times (v ! (i div row_length (w # N))) (row N (i mod row_length N)) = (v ! (i div length w) * w ! (i mod length w)) # local.times (v ! (i div row_length N)) (row N (i mod row_length N))

goal (1 subgoal):
 1. local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N))) = (v ! (i div length w) * w ! (i mod length w)) # local.times (v ! (i div row_length N)) (row N (i mod row_length N))
[PROOF STEP]
using times.simps 2 row_Cons temp
[PROOF STATE]
proof (prove)
using this:
(v ! (i div row_length (w # N)) * w ! (i mod length w)) # local.times (v ! (i div row_length (w # N))) (row N (i mod row_length N)) = (v ! (i div length w) * w ! (i mod length w)) # local.times (v ! (i div row_length N)) (row N (i mod row_length N))
local.times ?n [] = []
local.times ?n (?y # ?ys) = (?n * ?y) # local.times ?n ?ys
row_length (w # N) = length w
row (?v # ?M) ?i = ?v ! ?i # row ?M ?i
row_length (w # N) = row_length N

goal (1 subgoal):
 1. local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N))) = (v ! (i div length w) * w ! (i mod length w)) # local.times (v ! (i div row_length N)) (row N (i mod row_length N))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N))) = (v ! (i div length w) * w ! (i mod length w)) # local.times (v ! (i div row_length N)) (row N (i mod row_length N))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N))) = (v ! (i div length w) * w ! (i mod length w)) # local.times (v ! (i div row_length N)) (row N (i mod row_length N))

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N)); w = a # list\<rbrakk> \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N))) = (v ! (i div length w) * w ! (i mod length w)) # local.times (v ! (i div row_length N)) (row N (i mod row_length N))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N))) = (v ! (i div length w) * w ! (i mod length w)) # local.times (v ! (i div row_length N)) (row N (i mod row_length N))

goal (1 subgoal):
 1. row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
using Cons_5 ConsCons_2 1
                                row_Cons vec_mat_Tensor.simps(2)
[PROOF STATE]
proof (prove)
using this:
local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N))) = (v ! (i div length w) * w ! (i mod length w)) # local.times (v ! (i div row_length N)) (row N (i mod row_length N))
row (vec_mat_Tensor v N) i = local.times (v ! (i div row_length N)) (row N (i mod row_length N))
vec_vec_Tensor v w ! i = v ! (i div length w) * w ! (i mod length w)
w \<noteq> []
row (?v # ?M) ?i = ?v ! ?i # row ?M ?i
vec_mat_Tensor ?xs (?ys # ?yss) = vec_vec_Tensor ?xs ?ys # vec_mat_Tensor ?xs ?yss

goal (1 subgoal):
 1. row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
by (metis)
[PROOF STATE]
proof (state)
this:
row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i < length v * row_length (w # N) \<and> mat nr (length (w # N)) (w # N) \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))

goal (1 subgoal):
 1. \<And>a M i. (\<And>i. i < length v * row_length M \<and> mat nr (length M) M \<longrightarrow> row (vec_mat_Tensor v M) i = local.times (v ! (i div row_length M)) (row M (i mod row_length M))) \<Longrightarrow> i < length v * row_length (a # M) \<and> mat nr (length (a # M)) (a # M) \<longrightarrow> row (vec_mat_Tensor v (a # M)) i = local.times (v ! (i div row_length (a # M))) (row (a # M) (i mod row_length (a # M)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length v * row_length (w # N) \<and> mat nr (length (w # N)) (w # N) \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i < length v * row_length (w # N) \<and> mat nr (length (w # N)) (w # N) \<Longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))

goal (1 subgoal):
 1. i < length v * row_length (w # N) \<and> mat nr (length (w # N)) (w # N) \<longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length v * row_length (w # N) \<and> mat nr (length (w # N)) (w # N) \<longrightarrow> row (vec_mat_Tensor v (w # N)) i = local.times (v ! (i div row_length (w # N))) (row (w # N) (i mod row_length (w # N)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma  row_formula:
 fixes M1 and M2
 shows "\<forall>i.((i < (row_length M1)*(row_length M2))
          \<and>(mat (row_length M1) (length M1) M1)
          \<and>(mat (row_length M2) (length M2) M2)
             \<longrightarrow> row (M1 \<otimes> M2) i
                        =  vec_vec_Tensor
                                 (row M1 (i div row_length M2))
                                 (row M2 (i mod row_length M2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. i < row_length M1 * row_length M2 \<and> mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> row (M1 \<otimes> M2) i = vec_vec_Tensor (row M1 (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
apply(rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < row_length M1 * row_length M2 \<and> mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> row (M1 \<otimes> M2) i = vec_vec_Tensor (row M1 (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
proof(induct M1)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i < row_length [] * row_length M2 \<and> mat (row_length []) (length []) [] \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> row ([] \<otimes> M2) i = vec_vec_Tensor (row [] (i div row_length M2)) (row M2 (i mod row_length M2))
 2. \<And>a M1 i. (\<And>i. i < row_length M1 * row_length M2 \<and> mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> row (M1 \<otimes> M2) i = vec_vec_Tensor (row M1 (i div row_length M2)) (row M2 (i mod row_length M2))) \<Longrightarrow> i < row_length (a # M1) * row_length M2 \<and> mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> row (a # M1 \<otimes> M2) i = vec_vec_Tensor (row (a # M1) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>i. i < row_length [] * row_length M2 \<and> mat (row_length []) (length []) [] \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> row ([] \<otimes> M2) i = vec_vec_Tensor (row [] (i div row_length M2)) (row M2 (i mod row_length M2))
 2. \<And>a M1 i. (\<And>i. i < row_length M1 * row_length M2 \<and> mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> row (M1 \<otimes> M2) i = vec_vec_Tensor (row M1 (i div row_length M2)) (row M2 (i mod row_length M2))) \<Longrightarrow> i < row_length (a # M1) * row_length M2 \<and> mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> row (a # M1 \<otimes> M2) i = vec_vec_Tensor (row (a # M1) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < row_length [] * row_length M2 \<and> mat (row_length []) (length []) [] \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> row ([] \<otimes> M2) i = vec_vec_Tensor (row [] (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
using Nil
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < row_length [] * row_length M2 \<and> mat (row_length []) (length []) [] \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> row ([] \<otimes> M2) i = vec_vec_Tensor (row [] (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
by (metis less_nat_zero_code mult_0 row_length_Nil)
[PROOF STATE]
proof (state)
this:
i < row_length [] * row_length M2 \<and> mat (row_length []) (length []) [] \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> row ([] \<otimes> M2) i = vec_vec_Tensor (row [] (i div row_length M2)) (row M2 (i mod row_length M2))

goal (1 subgoal):
 1. \<And>a M1 i. (\<And>i. i < row_length M1 * row_length M2 \<and> mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> row (M1 \<otimes> M2) i = vec_vec_Tensor (row M1 (i div row_length M2)) (row M2 (i mod row_length M2))) \<Longrightarrow> i < row_length (a # M1) * row_length M2 \<and> mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> row (a # M1 \<otimes> M2) i = vec_vec_Tensor (row (a # M1) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a M1 i. (\<And>i. i < row_length M1 * row_length M2 \<and> mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> row (M1 \<otimes> M2) i = vec_vec_Tensor (row M1 (i div row_length M2)) (row M2 (i mod row_length M2))) \<Longrightarrow> i < row_length (a # M1) * row_length M2 \<and> mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> row (a # M1 \<otimes> M2) i = vec_vec_Tensor (row (a # M1) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
case (Cons v M)
[PROOF STATE]
proof (state)
this:
?i < row_length M * row_length M2 \<and> mat (row_length M) (length M) M \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> row (M \<otimes> M2) ?i = vec_vec_Tensor (row M (?i div row_length M2)) (row M2 (?i mod row_length M2))

goal (1 subgoal):
 1. \<And>a M1 i. (\<And>i. i < row_length M1 * row_length M2 \<and> mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> row (M1 \<otimes> M2) i = vec_vec_Tensor (row M1 (i div row_length M2)) (row M2 (i mod row_length M2))) \<Longrightarrow> i < row_length (a # M1) * row_length M2 \<and> mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> row (a # M1 \<otimes> M2) i = vec_vec_Tensor (row (a # M1) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
have
    "((i < (row_length (v#M))*(row_length M2))
    \<and> (mat (row_length (v#M)) (length (v#M)) (v#M))
    \<and> (mat (row_length M2) (length M2) M2)
     \<Longrightarrow> row ((v#M) \<otimes> M2) i =  vec_vec_Tensor
                                    (row (v#M) (i div row_length M2))
                                    (row M2 (i mod row_length M2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < row_length (v # M) * row_length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i < row_length (v # M) * row_length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
assume assms:
                 "(i < (row_length (v#M))*(row_length M2))
                 \<and>(mat (row_length (v#M)) (length (v#M)) (v#M))
                 \<and>(mat (row_length M2) (length M2) M2)"
[PROOF STATE]
proof (state)
this:
i < row_length (v # M) * row_length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2

goal (1 subgoal):
 1. i < row_length (v # M) * row_length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
have 0:"i < (length v)*(row_length M2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length v * row_length M2
[PROOF STEP]
using assms row_length_def
[PROOF STATE]
proof (prove)
using this:
i < row_length (v # M) * row_length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)

goal (1 subgoal):
 1. i < length v * row_length M2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length v * row_length M2

goal (1 subgoal):
 1. i < row_length (v # M) * row_length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
have 1:"mat (row_length M) (length M) M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length M) (length M) M
[PROOF STEP]
using assms  reduct_matrix
[PROOF STATE]
proof (prove)
using this:
i < row_length (v # M) * row_length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2
mat (row_length (?a # ?M)) (length (?a # ?M)) (?a # ?M) \<Longrightarrow> mat (row_length ?M) (length ?M) ?M

goal (1 subgoal):
 1. mat (row_length M) (length M) M
[PROOF STEP]
by (metis)
[PROOF STATE]
proof (state)
this:
mat (row_length M) (length M) M

goal (1 subgoal):
 1. i < row_length (v # M) * row_length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
have "row ((v#M)\<otimes>M2) i = row ((vec_mat_Tensor v M2)@(M \<otimes> M2)) i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (v # M \<otimes> M2) i = row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row (v # M \<otimes> M2) i = row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i

goal (1 subgoal):
 1. i < row_length (v # M) * row_length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
row (v # M \<otimes> M2) i = row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i
[PROOF STEP]
have 2:"... = (row (vec_mat_Tensor v M2) i)@(row (M \<otimes> M2) i)"
[PROOF STATE]
proof (prove)
using this:
row (v # M \<otimes> M2) i = row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i

goal (1 subgoal):
 1. row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i
[PROOF STEP]
using row_append
[PROOF STATE]
proof (prove)
using this:
row (v # M \<otimes> M2) i = row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i
row (?A @ ?B) ?i = row ?A ?i @ row ?B ?i

goal (1 subgoal):
 1. row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i

goal (1 subgoal):
 1. i < row_length (v # M) * row_length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i

goal (1 subgoal):
 1. row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
proof(cases M)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = []\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
 2. \<And>a list. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = a # list\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
M = []

goal (2 subgoals):
 1. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = []\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
 2. \<And>a list. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = a # list\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
have "row ((v#M)\<otimes>M2) i = (row (vec_mat_Tensor v M2) i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (v # M \<otimes> M2) i = row (vec_mat_Tensor v M2) i
[PROOF STEP]
using Nil 2
[PROOF STATE]
proof (prove)
using this:
M = []
row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i

goal (1 subgoal):
 1. row (v # M \<otimes> M2) i = row (vec_mat_Tensor v M2) i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row (v # M \<otimes> M2) i = row (vec_mat_Tensor v M2) i

goal (2 subgoals):
 1. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = []\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
 2. \<And>a list. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = a # list\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
row (v # M \<otimes> M2) i = row (vec_mat_Tensor v M2) i

goal (2 subgoals):
 1. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = []\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
 2. \<And>a list. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = a # list\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
have "row (vec_mat_Tensor v M2) i =  times
                                                (v!(i div row_length M2))
                                                (row M2 (i mod row_length M2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (vec_mat_Tensor v M2) i = local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
using row_vec_mat_Tensor_prelim assms 0
[PROOF STATE]
proof (prove)
using this:
\<forall>i. i < length ?v * row_length ?M \<and> mat ?nr (length ?M) ?M \<longrightarrow> row (vec_mat_Tensor ?v ?M) i = local.times (?v ! (i div row_length ?M)) (row ?M (i mod row_length ?M))
i < row_length (v # M) * row_length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2
i < length v * row_length M2

goal (1 subgoal):
 1. row (vec_mat_Tensor v M2) i = local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row (vec_mat_Tensor v M2) i = local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2))

goal (2 subgoals):
 1. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = []\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
 2. \<And>a list. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = a # list\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
row (v # M \<otimes> M2) i = row (vec_mat_Tensor v M2) i
row (vec_mat_Tensor v M2) i = local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
row (v # M \<otimes> M2) i = row (vec_mat_Tensor v M2) i
row (vec_mat_Tensor v M2) i = local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2))

goal (1 subgoal):
 1. row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
using vec_vec_Tensor_def
             Nil append_Nil2 vec_vec_Tensor.simps(1)
             vec_vec_Tensor.simps(2) row_Cons row_empty
[PROOF STATE]
proof (prove)
using this:
row (v # M \<otimes> M2) i = row (vec_mat_Tensor v M2) i
row (vec_mat_Tensor v M2) i = local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2))
vec_vec_Tensor \<equiv> rec_list (\<lambda>ys. []) (\<lambda>x xs xsa ys. local.times x ys @ xsa ys)
M = []
?xs @ [] = ?xs
vec_vec_Tensor [] ?ys = []
vec_vec_Tensor (?x # ?xs) ?ys = local.times ?x ?ys @ vec_vec_Tensor ?xs ?ys
row (?v # ?M) ?i = ?v ! ?i # row ?M ?i
row [] ?i = []

goal (1 subgoal):
 1. row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
by (metis)
[PROOF STATE]
proof (state)
this:
row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = a # list\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = a # list\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
case (Cons w N)
[PROOF STATE]
proof (state)
this:
M = w # N

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = a # list\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
have Cons_Cons_1:"mat (row_length M) (length M) M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length M) (length M) M
[PROOF STEP]
using assms reduct_matrix
[PROOF STATE]
proof (prove)
using this:
i < row_length (v # M) * row_length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2
mat (row_length (?a # ?M)) (length (?a # ?M)) (?a # ?M) \<Longrightarrow> mat (row_length ?M) (length ?M) ?M

goal (1 subgoal):
 1. mat (row_length M) (length M) M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat (row_length M) (length M) M

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = a # list\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat (row_length M) (length M) M
[PROOF STEP]
have "row_length (w#N) = row_length (v#M)"
[PROOF STATE]
proof (prove)
using this:
mat (row_length M) (length M) M

goal (1 subgoal):
 1. row_length (w # N) = row_length (v # M)
[PROOF STEP]
using assms Cons
[PROOF STATE]
proof (prove)
using this:
mat (row_length M) (length M) M
i < row_length (v # M) * row_length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2
M = w # N

goal (1 subgoal):
 1. row_length (w # N) = row_length (v # M)
[PROOF STEP]
unfolding mat_def Ball_def vec_def
[PROOF STATE]
proof (prove)
using this:
length M = length M \<and> (\<forall>x. x \<in> set M \<longrightarrow> length x = row_length M)
i < row_length (v # M) * row_length M2 \<and> (length (v # M) = length (v # M) \<and> (\<forall>x. x \<in> set (v # M) \<longrightarrow> length x = row_length (v # M))) \<and> length M2 = length M2 \<and> (\<forall>x. x \<in> set M2 \<longrightarrow> length x = row_length M2)
M = w # N

goal (1 subgoal):
 1. row_length (w # N) = row_length (v # M)
[PROOF STEP]
using append_Cons  hd_in_set list.distinct(1)
                        rotate1.simps(2) set_rotate1
[PROOF STATE]
proof (prove)
using this:
length M = length M \<and> (\<forall>x. x \<in> set M \<longrightarrow> length x = row_length M)
i < row_length (v # M) * row_length M2 \<and> (length (v # M) = length (v # M) \<and> (\<forall>x. x \<in> set (v # M) \<longrightarrow> length x = row_length (v # M))) \<and> length M2 = length M2 \<and> (\<forall>x. x \<in> set M2 \<longrightarrow> length x = row_length M2)
M = w # N
(?x # ?xs) @ ?ys = ?x # ?xs @ ?ys
?xs \<noteq> [] \<Longrightarrow> hd ?xs \<in> set ?xs
[] \<noteq> ?x21.0 # ?x22.0
rotate1 (?x # ?xs) = ?xs @ [?x]
set (rotate1 ?xs) = set ?xs

goal (1 subgoal):
 1. row_length (w # N) = row_length (v # M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row_length (w # N) = row_length (v # M)

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = a # list\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
row_length (w # N) = row_length (v # M)
[PROOF STEP]
have Cons_Cons_2:"i < (row_length M)*(row_length M2)"
[PROOF STATE]
proof (prove)
using this:
row_length (w # N) = row_length (v # M)

goal (1 subgoal):
 1. i < row_length M * row_length M2
[PROOF STEP]
using assms Cons
[PROOF STATE]
proof (prove)
using this:
row_length (w # N) = row_length (v # M)
i < row_length (v # M) * row_length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2
M = w # N

goal (1 subgoal):
 1. i < row_length M * row_length M2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < row_length M * row_length M2

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = a # list\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < row_length M * row_length M2
[PROOF STEP]
have Cons_Cons_3:"(row (M \<otimes> M2) i) =  vec_vec_Tensor
                                          (row M (i div row_length M2))
                                           (row M2 (i mod row_length M2))"
[PROOF STATE]
proof (prove)
using this:
i < row_length M * row_length M2

goal (1 subgoal):
 1. row (M \<otimes> M2) i = vec_vec_Tensor (row M (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
using Cons.hyps Cons_Cons_1 assms
[PROOF STATE]
proof (prove)
using this:
i < row_length M * row_length M2
?i < row_length M * row_length M2 \<and> mat (row_length M) (length M) M \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> row (M \<otimes> M2) ?i = vec_vec_Tensor (row M (?i div row_length M2)) (row M2 (?i mod row_length M2))
mat (row_length M) (length M) M
i < row_length (v # M) * row_length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2

goal (1 subgoal):
 1. row (M \<otimes> M2) i = vec_vec_Tensor (row M (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row (M \<otimes> M2) i = vec_vec_Tensor (row M (i div row_length M2)) (row M2 (i mod row_length M2))

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = a # list\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
row (M \<otimes> M2) i = vec_vec_Tensor (row M (i div row_length M2)) (row M2 (i mod row_length M2))

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = a # list\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
have "row (vec_mat_Tensor v M2) i
                                            =  times
                                               (v!(i div row_length M2))
                                               (row M2 (i mod row_length M2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (vec_mat_Tensor v M2) i = local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
using row_vec_mat_Tensor_prelim assms 0
[PROOF STATE]
proof (prove)
using this:
\<forall>i. i < length ?v * row_length ?M \<and> mat ?nr (length ?M) ?M \<longrightarrow> row (vec_mat_Tensor ?v ?M) i = local.times (?v ! (i div row_length ?M)) (row ?M (i mod row_length ?M))
i < row_length (v # M) * row_length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2
i < length v * row_length M2

goal (1 subgoal):
 1. row (vec_mat_Tensor v M2) i = local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row (vec_mat_Tensor v M2) i = local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2))

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = a # list\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
row (vec_mat_Tensor v M2) i = local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
have "row ((v#M)\<otimes>M2) i =
                           (times
                                   (v!(i div row_length M2))
                                    (row M2 (i mod row_length M2)))
                                      @(vec_vec_Tensor
                                          (row M (i div row_length M2))
                                           (row M2 (i mod row_length M2)))"
[PROOF STATE]
proof (prove)
using this:
row (vec_mat_Tensor v M2) i = local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2))

goal (1 subgoal):
 1. row (v # M \<otimes> M2) i = local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2)) @ vec_vec_Tensor (row M (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
using 2 Cons_Cons_3
[PROOF STATE]
proof (prove)
using this:
row (vec_mat_Tensor v M2) i = local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2))
row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i
row (M \<otimes> M2) i = vec_vec_Tensor (row M (i div row_length M2)) (row M2 (i mod row_length M2))

goal (1 subgoal):
 1. row (v # M \<otimes> M2) i = local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2)) @ vec_vec_Tensor (row M (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row (v # M \<otimes> M2) i = local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2)) @ vec_vec_Tensor (row M (i div row_length M2)) (row M2 (i mod row_length M2))

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = a # list\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
row (v # M \<otimes> M2) i = local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2)) @ vec_vec_Tensor (row M (i div row_length M2)) (row M2 (i mod row_length M2))

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = a # list\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
have "... = (vec_vec_Tensor
                                        ((v!(i div row_length M2))
                                             #(row M (i div row_length M2)))
                                        (row M2 (i mod row_length M2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2)) @ vec_vec_Tensor (row M (i div row_length M2)) (row M2 (i mod row_length M2)) = vec_vec_Tensor (v ! (i div row_length M2) # row M (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
using vec_vec_Tensor.simps(2)
[PROOF STATE]
proof (prove)
using this:
vec_vec_Tensor (?x # ?xs) ?ys = local.times ?x ?ys @ vec_vec_Tensor ?xs ?ys

goal (1 subgoal):
 1. local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2)) @ vec_vec_Tensor (row M (i div row_length M2)) (row M2 (i mod row_length M2)) = vec_vec_Tensor (v ! (i div row_length M2) # row M (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2)) @ vec_vec_Tensor (row M (i div row_length M2)) (row M2 (i mod row_length M2)) = vec_vec_Tensor (v ! (i div row_length M2) # row M (i div row_length M2)) (row M2 (i mod row_length M2))

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = a # list\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2)) @ vec_vec_Tensor (row M (i div row_length M2)) (row M2 (i mod row_length M2)) = vec_vec_Tensor (v ! (i div row_length M2) # row M (i div row_length M2)) (row M2 (i mod row_length M2))

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = a # list\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
have "... = (vec_vec_Tensor (row (v#M) (i div row_length M2))
                                           (row M2 (i mod row_length M2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_vec_Tensor (v ! (i div row_length M2) # row M (i div row_length M2)) (row M2 (i mod row_length M2)) = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
using row_Cons
[PROOF STATE]
proof (prove)
using this:
row (?v # ?M) ?i = ?v ! ?i # row ?M ?i

goal (1 subgoal):
 1. vec_vec_Tensor (v ! (i div row_length M2) # row M (i div row_length M2)) (row M2 (i mod row_length M2)) = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
vec_vec_Tensor (v ! (i div row_length M2) # row M (i div row_length M2)) (row M2 (i mod row_length M2)) = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>row (vec_mat_Tensor v M2 @ (M \<otimes> M2)) i = row (vec_mat_Tensor v M2) i @ row (M \<otimes> M2) i; M = a # list\<rbrakk> \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
row (M \<otimes> M2) i = vec_vec_Tensor (row M (i div row_length M2)) (row M2 (i mod row_length M2))
row (v # M \<otimes> M2) i = local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2)) @ vec_vec_Tensor (row M (i div row_length M2)) (row M2 (i mod row_length M2))
local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2)) @ vec_vec_Tensor (row M (i div row_length M2)) (row M2 (i mod row_length M2)) = vec_vec_Tensor (v ! (i div row_length M2) # row M (i div row_length M2)) (row M2 (i mod row_length M2))
vec_vec_Tensor (v ! (i div row_length M2) # row M (i div row_length M2)) (row M2 (i mod row_length M2)) = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
row (M \<otimes> M2) i = vec_vec_Tensor (row M (i div row_length M2)) (row M2 (i mod row_length M2))
row (v # M \<otimes> M2) i = local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2)) @ vec_vec_Tensor (row M (i div row_length M2)) (row M2 (i mod row_length M2))
local.times (v ! (i div row_length M2)) (row M2 (i mod row_length M2)) @ vec_vec_Tensor (row M (i div row_length M2)) (row M2 (i mod row_length M2)) = vec_vec_Tensor (v ! (i div row_length M2) # row M (i div row_length M2)) (row M2 (i mod row_length M2))
vec_vec_Tensor (v ! (i div row_length M2) # row M (i div row_length M2)) (row M2 (i mod row_length M2)) = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))

goal (1 subgoal):
 1. row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i < row_length (v # M) * row_length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))

goal (1 subgoal):
 1. \<And>a M1 i. (\<And>i. i < row_length M1 * row_length M2 \<and> mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> row (M1 \<otimes> M2) i = vec_vec_Tensor (row M1 (i div row_length M2)) (row M2 (i mod row_length M2))) \<Longrightarrow> i < row_length (a # M1) * row_length M2 \<and> mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> row (a # M1 \<otimes> M2) i = vec_vec_Tensor (row (a # M1) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < row_length (v # M) * row_length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i < row_length (v # M) * row_length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))

goal (1 subgoal):
 1. i < row_length (v # M) * row_length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < row_length (v # M) * row_length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> row (v # M \<otimes> M2) i = vec_vec_Tensor (row (v # M) (i div row_length M2)) (row M2 (i mod row_length M2))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma  effective_row_formula:
 fixes M1 and M2
 assumes "i < (row_length M1)*(row_length M2)"
     and "(mat (row_length M1) (length M1) M1)"
     and "(mat (row_length M2) (length M2) M2)"
 shows "row (M1 \<otimes> M2) i
               =  vec_vec_Tensor
                       (row M1 (i div row_length M2))
                       (row M2 (i mod row_length M2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (M1 \<otimes> M2) i = vec_vec_Tensor (row M1 (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
using assms row_formula
[PROOF STATE]
proof (prove)
using this:
i < row_length M1 * row_length M2
mat (row_length M1) (length M1) M1
mat (row_length M2) (length M2) M2
\<forall>i. i < row_length ?M1.0 * row_length ?M2.0 \<and> mat (row_length ?M1.0) (length ?M1.0) ?M1.0 \<and> mat (row_length ?M2.0) (length ?M2.0) ?M2.0 \<longrightarrow> row (?M1.0 \<otimes> ?M2.0) i = vec_vec_Tensor (row ?M1.0 (i div row_length ?M2.0)) (row ?M2.0 (i mod row_length ?M2.0))

goal (1 subgoal):
 1. row (M1 \<otimes> M2) i = vec_vec_Tensor (row M1 (i div row_length M2)) (row M2 (i mod row_length M2))
[PROOF STEP]
by auto


[STATEMENT]
lemma alt_effective_matrix_tensor_elements:
 " (((i<((row_length M2)*(row_length M3)))
 \<and>(j < (length M2)*(length M3)))
 \<and>(mat (row_length M2) (length M2) M2)
 \<and>(mat (row_length M3) (length M3) M3)
 \<Longrightarrow> ((M2 \<otimes> M3)!j!i) = f (M2!(j div (length M3))!(i div (row_length M3)))
(M3!(j mod length M3)!(i mod (row_length M3))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i < row_length M2 * row_length M3 \<and> j < length M2 * length M3) \<and> mat (row_length M2) (length M2) M2 \<and> mat (row_length M3) (length M3) M3 \<Longrightarrow> (M2 \<otimes> M3) ! j ! i = M2 ! (j div length M3) ! (i div row_length M3) * M3 ! (j mod length M3) ! (i mod row_length M3)
[PROOF STEP]
using matrix_Tensor_elements
[PROOF STATE]
proof (prove)
using this:
\<forall>i j. (i < row_length ?M1.0 * row_length ?M2.0 \<and> j < length ?M1.0 * length ?M2.0) \<and> mat (row_length ?M1.0) (length ?M1.0) ?M1.0 \<and> mat (row_length ?M2.0) (length ?M2.0) ?M2.0 \<longrightarrow> (?M1.0 \<otimes> ?M2.0) ! j ! i = ?M1.0 ! (j div length ?M2.0) ! (i div row_length ?M2.0) * ?M2.0 ! (j mod length ?M2.0) ! (i mod row_length ?M2.0)

goal (1 subgoal):
 1. (i < row_length M2 * row_length M3 \<and> j < length M2 * length M3) \<and> mat (row_length M2) (length M2) M2 \<and> mat (row_length M3) (length M3) M3 \<Longrightarrow> (M2 \<otimes> M3) ! j ! i = M2 ! (j div length M3) ! (i div row_length M3) * M3 ! (j mod length M3) ! (i mod row_length M3)
[PROOF STEP]
by auto


[STATEMENT]
lemma trans_impl:"(\<forall> i j.(P i j \<longrightarrow> Q i j))\<and>(\<forall> i j. (Q i j \<longrightarrow> R i j))
        \<Longrightarrow> (\<forall> i j. (P i j \<longrightarrow> R i j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i j. P i j \<longrightarrow> Q i j) \<and> (\<forall>i j. Q i j \<longrightarrow> R i j) \<Longrightarrow> \<forall>i j. P i j \<longrightarrow> R i j
[PROOF STEP]
by auto