[STATEMENT]
theorem well_defined_Tensor:
 "(mat (row_length M1) (length M1) M1)
\<and> (mat (row_length M2) (length M2) M2)
\<Longrightarrow>(mat ((row_length M1)*(row_length M2)) ((length M1)*(length M2)) (M1\<otimes>M2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2)
[PROOF STEP]
proof(induct M1)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mat (row_length []) (length []) [] \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length [] * row_length M2) (length [] * length M2) ([] \<otimes> M2)
 2. \<And>a M1. \<lbrakk>mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2); mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2\<rbrakk> \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
mat (row_length []) (length []) [] \<and> mat (row_length M2) (length M2) M2

goal (2 subgoals):
 1. mat (row_length []) (length []) [] \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length [] * row_length M2) (length [] * length M2) ([] \<otimes> M2)
 2. \<And>a M1. \<lbrakk>mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2); mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2\<rbrakk> \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
have "(row_length []) * (row_length M2) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_length [] * row_length M2 = 0
[PROOF STEP]
using row_length_def  mult_zero_left
[PROOF STATE]
proof (prove)
using this:
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)
(0::?'a) * ?a = (0::?'a)

goal (1 subgoal):
 1. row_length [] * row_length M2 = 0
[PROOF STEP]
by (metis)
[PROOF STATE]
proof (state)
this:
row_length [] * row_length M2 = 0

goal (2 subgoals):
 1. mat (row_length []) (length []) [] \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length [] * row_length M2) (length [] * length M2) ([] \<otimes> M2)
 2. \<And>a M1. \<lbrakk>mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2); mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2\<rbrakk> \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
row_length [] * row_length M2 = 0

goal (2 subgoals):
 1. mat (row_length []) (length []) [] \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length [] * row_length M2) (length [] * length M2) ([] \<otimes> M2)
 2. \<And>a M1. \<lbrakk>mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2); mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2\<rbrakk> \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
have "(length []) * (length M2) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length [] * length M2 = 0
[PROOF STEP]
using  mult_zero_left list.size(3)
[PROOF STATE]
proof (prove)
using this:
(0::?'a) * ?a = (0::?'a)
length [] = 0

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

goal (2 subgoals):
 1. mat (row_length []) (length []) [] \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length [] * row_length M2) (length [] * length M2) ([] \<otimes> M2)
 2. \<And>a M1. \<lbrakk>mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2); mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2\<rbrakk> \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length [] * length M2 = 0

goal (2 subgoals):
 1. mat (row_length []) (length []) [] \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length [] * row_length M2) (length [] * length M2) ([] \<otimes> M2)
 2. \<And>a M1. \<lbrakk>mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2); mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2\<rbrakk> \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
have "[] \<otimes> M2 = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<otimes> M2 = []
[PROOF STEP]
using Tensor.simps(1)
[PROOF STATE]
proof (prove)
using this:
[] \<otimes> ?xs = []

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

goal (2 subgoals):
 1. mat (row_length []) (length []) [] \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length [] * row_length M2) (length [] * length M2) ([] \<otimes> M2)
 2. \<And>a M1. \<lbrakk>mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2); mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2\<rbrakk> \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
row_length [] * row_length M2 = 0
length [] * length M2 = 0
[] \<otimes> M2 = []
[PROOF STEP]
have
       "mat (row_length []*row_length M2) (length []*length M2) ([] \<otimes> M2)"
[PROOF STATE]
proof (prove)
using this:
row_length [] * row_length M2 = 0
length [] * length M2 = 0
[] \<otimes> M2 = []

goal (1 subgoal):
 1. mat (row_length [] * row_length M2) (length [] * length M2) ([] \<otimes> M2)
[PROOF STEP]
using zero_matrix
[PROOF STATE]
proof (prove)
using this:
row_length [] * row_length M2 = 0
length [] * length M2 = 0
[] \<otimes> M2 = []
mat 0 0 []

goal (1 subgoal):
 1. mat (row_length [] * row_length M2) (length [] * length M2) ([] \<otimes> M2)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
mat (row_length [] * row_length M2) (length [] * length M2) ([] \<otimes> M2)

goal (2 subgoals):
 1. mat (row_length []) (length []) [] \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length [] * row_length M2) (length [] * length M2) ([] \<otimes> M2)
 2. \<And>a M1. \<lbrakk>mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2); mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2\<rbrakk> \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat (row_length [] * row_length M2) (length [] * length M2) ([] \<otimes> M2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
mat (row_length [] * row_length M2) (length [] * length M2) ([] \<otimes> M2)

goal (1 subgoal):
 1. mat (row_length [] * row_length M2) (length [] * length M2) ([] \<otimes> M2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mat (row_length [] * row_length M2) (length [] * length M2) ([] \<otimes> M2)

goal (1 subgoal):
 1. \<And>a M1. \<lbrakk>mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2); mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2\<rbrakk> \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a M1. \<lbrakk>mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2); mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2\<rbrakk> \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
case (Cons a M1)
[PROOF STATE]
proof (state)
this:
mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2)
mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2

goal (1 subgoal):
 1. \<And>a M1. \<lbrakk>mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2); mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2\<rbrakk> \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
have step1: "mat (row_length (a # M1)) (length (a # M1)) (a # M1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length (a # M1)) (length (a # M1)) (a # M1)
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2

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

goal (1 subgoal):
 1. \<And>a M1. \<lbrakk>mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2); mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2\<rbrakk> \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat (row_length (a # M1)) (length (a # M1)) (a # M1)
[PROOF STEP]
have "mat (row_length (M1)) (length (M1)) (M1)"
[PROOF STATE]
proof (prove)
using this:
mat (row_length (a # M1)) (length (a # M1)) (a # M1)

goal (1 subgoal):
 1. mat (row_length M1) (length M1) M1
[PROOF STEP]
using reduct_matrix
[PROOF STATE]
proof (prove)
using this:
mat (row_length (a # M1)) (length (a # M1)) (a # M1)
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 M1) (length M1) M1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat (row_length M1) (length M1) M1

goal (1 subgoal):
 1. \<And>a M1. \<lbrakk>mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2); mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2\<rbrakk> \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mat (row_length M1) (length M1) M1

goal (1 subgoal):
 1. \<And>a M1. \<lbrakk>mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2); mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2\<rbrakk> \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
have "mat (row_length (M2)) (length (M2)) (M2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length M2) (length M2) M2
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2

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

goal (1 subgoal):
 1. \<And>a M1. \<lbrakk>mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2); mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2\<rbrakk> \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mat (row_length M1) (length M1) M1
mat (row_length M2) (length M2) M2
[PROOF STEP]
have step2:
      "mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2)"
[PROOF STATE]
proof (prove)
using this:
mat (row_length M1) (length M1) M1
mat (row_length M2) (length M2) M2

goal (1 subgoal):
 1. mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2)
[PROOF STEP]
using Cons.hyps
[PROOF STATE]
proof (prove)
using this:
mat (row_length M1) (length M1) M1
mat (row_length M2) (length M2) M2
mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2)

goal (1 subgoal):
 1. mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2)

goal (1 subgoal):
 1. \<And>a M1. \<lbrakk>mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2); mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2\<rbrakk> \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
have 0:"row_length (a#M1) = length a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_length (a # M1) = length a
[PROOF STEP]
using row_length_def  list.distinct(1)
[PROOF STATE]
proof (prove)
using this:
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)
[] \<noteq> ?x21.0 # ?x22.0

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

goal (1 subgoal):
 1. \<And>a M1. \<lbrakk>mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2); mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2\<rbrakk> \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
have "mat
           (row_length (a # M1)*row_length M2)
           (length (a # M1)*length M2)
                           (a # M1 \<otimes> M2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
proof(cases M1)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. M1 = [] \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
 2. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
M1 = []

goal (2 subgoals):
 1. M1 = [] \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
 2. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
have "(mat ((row_length M2)*(length a)) (length M2) (vec_mat_Tensor a M2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length M2 * length a) (length M2) (vec_mat_Tensor a M2)
[PROOF STEP]
using Cons.prems well_defined_vec_mat_Tensor
[PROOF STATE]
proof (prove)
using this:
mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2
mat (row_length ?M) (length ?M) ?M \<Longrightarrow> mat (row_length ?M * length ?v) (length ?M) (vec_mat_Tensor ?v ?M)

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

goal (2 subgoals):
 1. M1 = [] \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
 2. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mat (row_length M2 * length a) (length M2) (vec_mat_Tensor a M2)

goal (2 subgoals):
 1. M1 = [] \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
 2. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
have "(length (a # M1)) * (length M2) = length M2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (a # M1) * length M2 = length M2
[PROOF STEP]
using Nil
[PROOF STATE]
proof (prove)
using this:
M1 = []

goal (1 subgoal):
 1. length (a # M1) * length M2 = length M2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (a # M1) * length M2 = length M2

goal (2 subgoals):
 1. M1 = [] \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
 2. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length (a # M1) * length M2 = length M2

goal (2 subgoals):
 1. M1 = [] \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
 2. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
have "(a#M1)\<otimes>M2 = (vec_mat_Tensor a M2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a # M1 \<otimes> M2 = vec_mat_Tensor a M2
[PROOF STEP]
using Nil Tensor.simps append.simps(1)
[PROOF STATE]
proof (prove)
using this:
M1 = []
[] \<otimes> ?xs = []
?x # ?xs \<otimes> ?ys = vec_mat_Tensor ?x ?ys @ (?xs \<otimes> ?ys)
[] @ ?ys = ?ys

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

goal (2 subgoals):
 1. M1 = [] \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
 2. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mat (row_length M2 * length a) (length M2) (vec_mat_Tensor a M2)
length (a # M1) * length M2 = length M2
a # M1 \<otimes> M2 = vec_mat_Tensor a M2
[PROOF STEP]
have
        "(mat
            ((row_length M2)*(row_length (a#M1)))
            ((length (a # M1)) * (length M2))
               ((a#M1)\<otimes>M2))"
[PROOF STATE]
proof (prove)
using this:
mat (row_length M2 * length a) (length M2) (vec_mat_Tensor a M2)
length (a # M1) * length M2 = length M2
a # M1 \<otimes> M2 = vec_mat_Tensor a M2

goal (1 subgoal):
 1. mat (row_length M2 * row_length (a # M1)) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
mat (row_length M2 * length a) (length M2) (vec_mat_Tensor a M2)
length (a # M1) * length M2 = length M2
a # M1 \<otimes> M2 = vec_mat_Tensor a M2
row_length (a # M1) = length a

goal (1 subgoal):
 1. mat (row_length M2 * row_length (a # M1)) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat (row_length M2 * row_length (a # M1)) (length (a # M1) * length M2) (a # M1 \<otimes> M2)

goal (2 subgoals):
 1. M1 = [] \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
 2. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat (row_length M2 * row_length (a # M1)) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mat (row_length M2 * row_length (a # M1)) (length (a # M1) * length M2) (a # M1 \<otimes> M2)

goal (1 subgoal):
 1. mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
by (simp add: mult.commute)
[PROOF STATE]
proof (state)
this:
mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
case (Cons b N1)
[PROOF STATE]
proof (state)
this:
M1 = b # N1

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
have 1:"x \<in> (set (a#M1)) \<longrightarrow> ((x=a) \<or> (x \<in> (set M1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set (a # M1) \<longrightarrow> x = a \<or> x \<in> set M1
[PROOF STEP]
using hd_set
[PROOF STATE]
proof (prove)
using this:
?x \<in> set (?a # ?M) \<Longrightarrow> ?x = ?a \<or> ?x \<in> set ?M

goal (1 subgoal):
 1. x \<in> set (a # M1) \<longrightarrow> x = a \<or> x \<in> set M1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> set (a # M1) \<longrightarrow> x = a \<or> x \<in> set M1

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
have "mat (row_length (a#M1)) (length (a#M1)) (a#M1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length (a # M1)) (length (a # M1)) (a # M1)
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2

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

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat (row_length (a # M1)) (length (a # M1)) (a # M1)
[PROOF STEP]
have "x\<in> (set (a#M1)) \<longrightarrow> (vec (row_length (a#M1)) x)"
[PROOF STATE]
proof (prove)
using this:
mat (row_length (a # M1)) (length (a # M1)) (a # M1)

goal (1 subgoal):
 1. x \<in> set (a # M1) \<longrightarrow> vec (row_length (a # M1)) x
[PROOF STEP]
using mat_def Ball_def
[PROOF STATE]
proof (prove)
using this:
mat (row_length (a # M1)) (length (a # M1)) (a # M1)
mat ?nr ?nc ?m = (length ?m = ?nc \<and> Ball (set ?m) (vec ?nr))
Ball ?A ?P = (\<forall>x. x \<in> ?A \<longrightarrow> ?P x)

goal (1 subgoal):
 1. x \<in> set (a # M1) \<longrightarrow> vec (row_length (a # M1)) x
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
x \<in> set (a # M1) \<longrightarrow> vec (row_length (a # M1)) x

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set (a # M1) \<longrightarrow> vec (row_length (a # M1)) x
[PROOF STEP]
have "x\<in> (set (a#M1))\<longrightarrow> (vec (length a) x)"
[PROOF STATE]
proof (prove)
using this:
x \<in> set (a # M1) \<longrightarrow> vec (row_length (a # M1)) x

goal (1 subgoal):
 1. x \<in> set (a # M1) \<longrightarrow> vec (length a) x
[PROOF STEP]
using row_length_def  list.distinct(1)
[PROOF STATE]
proof (prove)
using this:
x \<in> set (a # M1) \<longrightarrow> vec (row_length (a # M1)) x
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)
[] \<noteq> ?x21.0 # ?x22.0

goal (1 subgoal):
 1. x \<in> set (a # M1) \<longrightarrow> vec (length a) x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> set (a # M1) \<longrightarrow> vec (length a) x

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
x \<in> set (a # M1) \<longrightarrow> x = a \<or> x \<in> set M1
x \<in> set (a # M1) \<longrightarrow> vec (length a) x
[PROOF STEP]
have "x\<in> (set M1)\<longrightarrow> (vec (length a) x)"
[PROOF STATE]
proof (prove)
using this:
x \<in> set (a # M1) \<longrightarrow> x = a \<or> x \<in> set M1
x \<in> set (a # M1) \<longrightarrow> vec (length a) x

goal (1 subgoal):
 1. x \<in> set M1 \<longrightarrow> vec (length a) x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> set M1 \<longrightarrow> vec (length a) x

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> set M1 \<longrightarrow> vec (length a) x

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
have " b \<in> (set M1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<in> set M1
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
M1 = b # N1

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

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> set M1 \<longrightarrow> vec (length a) x
b \<in> set M1
[PROOF STEP]
have "vec (length a) b"
[PROOF STATE]
proof (prove)
using this:
x \<in> set M1 \<longrightarrow> vec (length a) x
b \<in> set M1

goal (1 subgoal):
 1. vec (length a) b
[PROOF STEP]
using  Cons.prems in_set_member mat_def member_rec(1) vec_def
[PROOF STATE]
proof (prove)
using this:
x \<in> set M1 \<longrightarrow> vec (length a) x
b \<in> set M1
mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2
(?x \<in> set ?xs) = List.member ?xs ?x
mat ?nr ?nc ?m = (length ?m = ?nc \<and> Ball (set ?m) (vec ?nr))
List.member (?x # ?xs) ?y = (?x = ?y \<or> List.member ?xs ?y)
vec ?n ?x = (length ?x = ?n)

goal (1 subgoal):
 1. vec (length a) b
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
vec (length a) b

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vec (length a) b
[PROOF STEP]
have "(length b) = (length a)"
[PROOF STATE]
proof (prove)
using this:
vec (length a) b

goal (1 subgoal):
 1. length b = length a
[PROOF STEP]
using vec_def vec_uniqueness
[PROOF STATE]
proof (prove)
using this:
vec (length a) b
vec ?n ?x = (length ?x = ?n)
\<lbrakk>vec ?m ?v; vec ?n ?v\<rbrakk> \<Longrightarrow> ?m = ?n

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

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length b = length a
[PROOF STEP]
have 2:"row_length M1 = (length a)"
[PROOF STATE]
proof (prove)
using this:
length b = length a

goal (1 subgoal):
 1. row_length M1 = length a
[PROOF STEP]
using row_length_def Cons
[PROOF STATE]
proof (prove)
using this:
length b = length a
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)
M1 = b # N1

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

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
row_length M1 = length a
[PROOF STEP]
have "mat
                    ((length a) * row_length M2)
                    (length M1 * length M2)
                                    (M1 \<otimes> M2)"
[PROOF STATE]
proof (prove)
using this:
row_length M1 = length a

goal (1 subgoal):
 1. mat (length a * row_length M2) (length M1 * length M2) (M1 \<otimes> M2)
[PROOF STEP]
using step2
[PROOF STATE]
proof (prove)
using this:
row_length M1 = length a
mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2)

goal (1 subgoal):
 1. mat (length a * row_length M2) (length M1 * length M2) (M1 \<otimes> M2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat (length a * row_length M2) (length M1 * length M2) (M1 \<otimes> M2)

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat (length a * row_length M2) (length M1 * length M2) (M1 \<otimes> M2)
[PROOF STEP]
have "Ball (set (M1\<otimes>M2)) (vec ((length a)*(row_length M2))) "
[PROOF STATE]
proof (prove)
using this:
mat (length a * row_length M2) (length M1 * length M2) (M1 \<otimes> M2)

goal (1 subgoal):
 1. Ball (set (M1 \<otimes> M2)) (vec (length a * row_length M2))
[PROOF STEP]
using mat_def
[PROOF STATE]
proof (prove)
using this:
mat (length a * row_length M2) (length M1 * length M2) (M1 \<otimes> M2)
mat ?nr ?nc ?m = (length ?m = ?nc \<and> Ball (set ?m) (vec ?nr))

goal (1 subgoal):
 1. Ball (set (M1 \<otimes> M2)) (vec (length a * row_length M2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ball (set (M1 \<otimes> M2)) (vec (length a * row_length M2))

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
Ball (set (M1 \<otimes> M2)) (vec (length a * row_length M2))
[PROOF STEP]
have 3:
         "\<forall>x. x \<in> (set (M1 \<otimes> M2)) \<longrightarrow> (vec ((length a)*(row_length M2)) x)"
[PROOF STATE]
proof (prove)
using this:
Ball (set (M1 \<otimes> M2)) (vec (length a * row_length M2))

goal (1 subgoal):
 1. \<forall>x. x \<in> set (M1 \<otimes> M2) \<longrightarrow> vec (length a * row_length M2) x
[PROOF STEP]
using Ball_def
[PROOF STATE]
proof (prove)
using this:
Ball (set (M1 \<otimes> M2)) (vec (length a * row_length M2))
Ball ?A ?P = (\<forall>x. x \<in> ?A \<longrightarrow> ?P x)

goal (1 subgoal):
 1. \<forall>x. x \<in> set (M1 \<otimes> M2) \<longrightarrow> vec (length a * row_length M2) x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<in> set (M1 \<otimes> M2) \<longrightarrow> vec (length a * row_length M2) x

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
have "mat
              ((row_length M2)*(length a))
              (length M2)
                 (vec_mat_Tensor a M2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length M2 * length a) (length M2) (vec_mat_Tensor a M2)
[PROOF STEP]
using well_defined_vec_mat_Tensor Cons.prems
[PROOF STATE]
proof (prove)
using this:
mat (row_length ?M) (length ?M) ?M \<Longrightarrow> mat (row_length ?M * length ?v) (length ?M) (vec_mat_Tensor ?v ?M)
mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2

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

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat (row_length M2 * length a) (length M2) (vec_mat_Tensor a M2)
[PROOF STEP]
have "Ball
                    (set (vec_mat_Tensor a M2))
                    (vec ((row_length M2)*(length a)))"
[PROOF STATE]
proof (prove)
using this:
mat (row_length M2 * length a) (length M2) (vec_mat_Tensor a M2)

goal (1 subgoal):
 1. Ball (set (vec_mat_Tensor a M2)) (vec (row_length M2 * length a))
[PROOF STEP]
using mat_def
[PROOF STATE]
proof (prove)
using this:
mat (row_length M2 * length a) (length M2) (vec_mat_Tensor a M2)
mat ?nr ?nc ?m = (length ?m = ?nc \<and> Ball (set ?m) (vec ?nr))

goal (1 subgoal):
 1. Ball (set (vec_mat_Tensor a M2)) (vec (row_length M2 * length a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ball (set (vec_mat_Tensor a M2)) (vec (row_length M2 * length a))

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ball (set (vec_mat_Tensor a M2)) (vec (row_length M2 * length a))
[PROOF STEP]
have 4:
              "\<forall>x. x \<in> (set (vec_mat_Tensor a M2))
                        \<longrightarrow> (vec ((length a)*(row_length M2)) x)"
[PROOF STATE]
proof (prove)
using this:
Ball (set (vec_mat_Tensor a M2)) (vec (row_length M2 * length a))

goal (1 subgoal):
 1. \<forall>x. x \<in> set (vec_mat_Tensor a M2) \<longrightarrow> vec (length a * row_length M2) x
[PROOF STEP]
using mult.commute
[PROOF STATE]
proof (prove)
using this:
Ball (set (vec_mat_Tensor a M2)) (vec (row_length M2 * length a))
?a * ?b = ?b * ?a

goal (1 subgoal):
 1. \<forall>x. x \<in> set (vec_mat_Tensor a M2) \<longrightarrow> vec (length a * row_length M2) x
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<in> set (vec_mat_Tensor a M2) \<longrightarrow> vec (length a * row_length M2) x

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
with 3
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. x \<in> set (M1 \<otimes> M2) \<longrightarrow> vec (length a * row_length M2) x
\<forall>x. x \<in> set (vec_mat_Tensor a M2) \<longrightarrow> vec (length a * row_length M2) x
[PROOF STEP]
have 5: "\<forall>x. (x \<in> (set (vec_mat_Tensor a M2)))
                          \<or>(x \<in> (set (M1 \<otimes> M2)))
                                 \<longrightarrow> (vec ((length a)*(row_length M2)) x)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> set (M1 \<otimes> M2) \<longrightarrow> vec (length a * row_length M2) x
\<forall>x. x \<in> set (vec_mat_Tensor a M2) \<longrightarrow> vec (length a * row_length M2) x

goal (1 subgoal):
 1. \<forall>x. x \<in> set (vec_mat_Tensor a M2) \<or> x \<in> set (M1 \<otimes> M2) \<longrightarrow> vec (length a * row_length M2) x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<in> set (vec_mat_Tensor a M2) \<or> x \<in> set (M1 \<otimes> M2) \<longrightarrow> vec (length a * row_length M2) x

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
have 6:"(a # M1 \<otimes> M2) = (vec_mat_Tensor a M2)@(M1 \<otimes>M2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a # M1 \<otimes> M2 = vec_mat_Tensor a M2 @ (M1 \<otimes> M2)
[PROOF STEP]
using Tensor.simps(2)
[PROOF STATE]
proof (prove)
using this:
?x # ?xs \<otimes> ?ys = vec_mat_Tensor ?x ?ys @ (?xs \<otimes> ?ys)

goal (1 subgoal):
 1. a # M1 \<otimes> M2 = vec_mat_Tensor a M2 @ (M1 \<otimes> M2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a # M1 \<otimes> M2 = vec_mat_Tensor a M2 @ (M1 \<otimes> M2)

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a # M1 \<otimes> M2 = vec_mat_Tensor a M2 @ (M1 \<otimes> M2)
[PROOF STEP]
have "x \<in> (set (a # M1 \<otimes> M2))
                 \<longrightarrow> (x \<in> (set (vec_mat_Tensor a M2)))\<or>(x \<in> (set (M1 \<otimes> M2)))"
[PROOF STATE]
proof (prove)
using this:
a # M1 \<otimes> M2 = vec_mat_Tensor a M2 @ (M1 \<otimes> M2)

goal (1 subgoal):
 1. x \<in> set (a # M1 \<otimes> M2) \<longrightarrow> x \<in> set (vec_mat_Tensor a M2) \<or> x \<in> set (M1 \<otimes> M2)
[PROOF STEP]
using set_def append_def
[PROOF STATE]
proof (prove)
using this:
a # M1 \<otimes> M2 = vec_mat_Tensor a M2 @ (M1 \<otimes> M2)
set \<equiv> ctor_fold_list (\<lambda>z. set1_pre_list z \<union> \<Union> (set2_pre_list z))
(@) \<equiv> rec_list (\<lambda>ys. ys) (\<lambda>x xs xsa ys. x # xsa ys)

goal (1 subgoal):
 1. x \<in> set (a # M1 \<otimes> M2) \<longrightarrow> x \<in> set (vec_mat_Tensor a M2) \<or> x \<in> set (M1 \<otimes> M2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> set (a # M1 \<otimes> M2) \<longrightarrow> x \<in> set (vec_mat_Tensor a M2) \<or> x \<in> set (M1 \<otimes> M2)

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
with 5
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. x \<in> set (vec_mat_Tensor a M2) \<or> x \<in> set (M1 \<otimes> M2) \<longrightarrow> vec (length a * row_length M2) x
x \<in> set (a # M1 \<otimes> M2) \<longrightarrow> x \<in> set (vec_mat_Tensor a M2) \<or> x \<in> set (M1 \<otimes> M2)
[PROOF STEP]
have 7:"\<forall>x. (x \<in>  (set (a # M1 \<otimes> M2)))
                         \<longrightarrow> (vec ((length a)*(row_length M2)) x)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> set (vec_mat_Tensor a M2) \<or> x \<in> set (M1 \<otimes> M2) \<longrightarrow> vec (length a * row_length M2) x
x \<in> set (a # M1 \<otimes> M2) \<longrightarrow> x \<in> set (vec_mat_Tensor a M2) \<or> x \<in> set (M1 \<otimes> M2)

goal (1 subgoal):
 1. \<forall>x. x \<in> set (a # M1 \<otimes> M2) \<longrightarrow> vec (length a * row_length M2) x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<in> set (a # M1 \<otimes> M2) \<longrightarrow> vec (length a * row_length M2) x

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. x \<in> set (a # M1 \<otimes> M2) \<longrightarrow> vec (length a * row_length M2) x
[PROOF STEP]
have 8:
        "Ball (set (a # M1 \<otimes> M2)) (vec ((row_length (a#M1))*(row_length M2)))"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> set (a # M1 \<otimes> M2) \<longrightarrow> vec (length a * row_length M2) x

goal (1 subgoal):
 1. Ball (set (a # M1 \<otimes> M2)) (vec (row_length (a # M1) * row_length M2))
[PROOF STEP]
using Ball_def 0
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> set (a # M1 \<otimes> M2) \<longrightarrow> vec (length a * row_length M2) x
Ball ?A ?P = (\<forall>x. x \<in> ?A \<longrightarrow> ?P x)
row_length (a # M1) = length a

goal (1 subgoal):
 1. Ball (set (a # M1 \<otimes> M2)) (vec (row_length (a # M1) * row_length M2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ball (set (a # M1 \<otimes> M2)) (vec (row_length (a # M1) * row_length M2))

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
have "(length ((a#M1)\<otimes>M2)) = (length (a#M1))*(length M2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (a # M1 \<otimes> M2) = length (a # M1) * length M2
[PROOF STEP]
using length_Tensor
[PROOF STATE]
proof (prove)
using this:
length (?M1.0 \<otimes> ?M2.0) = length ?M1.0 * length ?M2.0

goal (1 subgoal):
 1. length (a # M1 \<otimes> M2) = length (a # M1) * length M2
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
length (a # M1 \<otimes> M2) = length (a # M1) * length M2

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
with 7 8
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. x \<in> set (a # M1 \<otimes> M2) \<longrightarrow> vec (length a * row_length M2) x
Ball (set (a # M1 \<otimes> M2)) (vec (row_length (a # M1) * row_length M2))
length (a # M1 \<otimes> M2) = length (a # M1) * length M2
[PROOF STEP]
have "mat
                     (row_length (a # M1) * row_length M2)
                       (length (a # M1) * length M2)
                                (a # M1 \<otimes> M2)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> set (a # M1 \<otimes> M2) \<longrightarrow> vec (length a * row_length M2) x
Ball (set (a # M1 \<otimes> M2)) (vec (row_length (a # M1) * row_length M2))
length (a # M1 \<otimes> M2) = length (a # M1) * length M2

goal (1 subgoal):
 1. mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
using mat_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> set (a # M1 \<otimes> M2) \<longrightarrow> vec (length a * row_length M2) x
Ball (set (a # M1 \<otimes> M2)) (vec (row_length (a # M1) * row_length M2))
length (a # M1 \<otimes> M2) = length (a # M1) * length M2
mat ?nr ?nc ?m = (length ?m = ?nc \<and> Ball (set ?m) (vec ?nr))

goal (1 subgoal):
 1. mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
by (metis "0"  length_Tensor)
[PROOF STATE]
proof (state)
this:
mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)

goal (1 subgoal):
 1. \<And>aa list. M1 = aa # list \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)

goal (1 subgoal):
 1. mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)

goal (1 subgoal):
 1. \<And>a M1. \<lbrakk>mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2); mat (row_length (a # M1)) (length (a # M1)) (a # M1) \<and> mat (row_length M2) (length M2) M2\<rbrakk> \<Longrightarrow> mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)

goal (1 subgoal):
 1. mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat (row_length (a # M1) * row_length M2) (length (a # M1) * length M2) (a # M1 \<otimes> M2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem effective_well_defined_Tensor:
 assumes "(mat (row_length M1) (length M1) M1)"
     and "(mat (row_length M2) (length M2) M2)"
 shows "mat
            ((row_length M1)*(row_length M2))
            ((length M1)*(length M2))
                               (M1\<otimes>M2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2)
[PROOF STEP]
using well_defined_Tensor assms
[PROOF STATE]
proof (prove)
using this:
mat (row_length ?M1.0) (length ?M1.0) ?M1.0 \<and> mat (row_length ?M2.0) (length ?M2.0) ?M2.0 \<Longrightarrow> mat (row_length ?M1.0 * row_length ?M2.0) (length ?M1.0 * length ?M2.0) (?M1.0 \<otimes> ?M2.0)
mat (row_length M1) (length M1) M1
mat (row_length M2) (length M2) M2

goal (1 subgoal):
 1. mat (row_length M1 * row_length M2) (length M1 * length M2) (M1 \<otimes> M2)
[PROOF STEP]
by auto


[STATEMENT]
theorem times_elements:
 "\<forall>i.((i<(length v)) \<longrightarrow> (times a v)!i = f a (v!i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<length v. local.times a v ! i = a * v ! i
[PROOF STEP]
apply(rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < length v \<longrightarrow> local.times a v ! i = a * v ! i
[PROOF STEP]
proof(induct v)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i < length [] \<longrightarrow> local.times a [] ! i = a * [] ! i
 2. \<And>aa v i. (\<And>i. i < length v \<longrightarrow> local.times a v ! i = a * v ! i) \<Longrightarrow> i < length (aa # v) \<longrightarrow> local.times a (aa # v) ! i = a * (aa # v) ! i
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>i. i < length [] \<longrightarrow> local.times a [] ! i = a * [] ! i
 2. \<And>aa v i. (\<And>i. i < length v \<longrightarrow> local.times a v ! i = a * v ! i) \<Longrightarrow> i < length (aa # v) \<longrightarrow> local.times a (aa # v) ! i = a * (aa # v) ! i
[PROOF STEP]
have "(length [] = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length [] = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length [] = 0

goal (2 subgoals):
 1. \<And>i. i < length [] \<longrightarrow> local.times a [] ! i = a * [] ! i
 2. \<And>aa v i. (\<And>i. i < length v \<longrightarrow> local.times a v ! i = a * v ! i) \<Longrightarrow> i < length (aa # v) \<longrightarrow> local.times a (aa # v) ! i = a * (aa # v) ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length [] = 0
[PROOF STEP]
have "i <(length []) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
using this:
length [] = 0

goal (1 subgoal):
 1. i < length [] \<Longrightarrow> False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length [] \<Longrightarrow> False

goal (2 subgoals):
 1. \<And>i. i < length [] \<longrightarrow> local.times a [] ! i = a * [] ! i
 2. \<And>aa v i. (\<And>i. i < length v \<longrightarrow> local.times a v ! i = a * v ! i) \<Longrightarrow> i < length (aa # v) \<longrightarrow> local.times a (aa # v) ! i = a * (aa # v) ! i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i < length [] \<Longrightarrow> False

goal (2 subgoals):
 1. \<And>i. i < length [] \<longrightarrow> local.times a [] ! i = a * [] ! i
 2. \<And>aa v i. (\<And>i. i < length v \<longrightarrow> local.times a v ! i = a * v ! i) \<Longrightarrow> i < length (aa # v) \<longrightarrow> local.times a (aa # v) ! i = a * (aa # v) ! i
[PROOF STEP]
have "(times a []) = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.times a [] = []
[PROOF STEP]
using times.simps(1)
[PROOF STATE]
proof (prove)
using this:
local.times ?n [] = []

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

goal (2 subgoals):
 1. \<And>i. i < length [] \<longrightarrow> local.times a [] ! i = a * [] ! i
 2. \<And>aa v i. (\<And>i. i < length v \<longrightarrow> local.times a v ! i = a * v ! i) \<Longrightarrow> i < length (aa # v) \<longrightarrow> local.times a (aa # v) ! i = a * (aa # v) ! i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i < length [] \<Longrightarrow> False
local.times a [] = []
[PROOF STEP]
have "(i<(length [])) \<longrightarrow> (times a [])!i = f a ([]!i)"
[PROOF STATE]
proof (prove)
using this:
i < length [] \<Longrightarrow> False
local.times a [] = []

goal (1 subgoal):
 1. i < length [] \<longrightarrow> local.times a [] ! i = a * [] ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length [] \<longrightarrow> local.times a [] ! i = a * [] ! i

goal (2 subgoals):
 1. \<And>i. i < length [] \<longrightarrow> local.times a [] ! i = a * [] ! i
 2. \<And>aa v i. (\<And>i. i < length v \<longrightarrow> local.times a v ! i = a * v ! i) \<Longrightarrow> i < length (aa # v) \<longrightarrow> local.times a (aa # v) ! i = a * (aa # v) ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length [] \<longrightarrow> local.times a [] ! i = a * [] ! i
[PROOF STEP]
have "\<forall>i. ((i<(length [])) \<longrightarrow> (times a [])!i = f a ([]!i))"
[PROOF STATE]
proof (prove)
using this:
i < length [] \<longrightarrow> local.times a [] ! i = a * [] ! i

goal (1 subgoal):
 1. \<forall>i<length []. local.times a [] ! i = a * [] ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i<length []. local.times a [] ! i = a * [] ! i

goal (2 subgoals):
 1. \<And>i. i < length [] \<longrightarrow> local.times a [] ! i = a * [] ! i
 2. \<And>aa v i. (\<And>i. i < length v \<longrightarrow> local.times a v ! i = a * v ! i) \<Longrightarrow> i < length (aa # v) \<longrightarrow> local.times a (aa # v) ! i = a * (aa # v) ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length []. local.times a [] ! i = a * [] ! i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length []. local.times a [] ! i = a * [] ! i

goal (1 subgoal):
 1. i < length [] \<longrightarrow> local.times a [] ! i = a * [] ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length [] \<longrightarrow> local.times a [] ! i = a * [] ! i

goal (1 subgoal):
 1. \<And>aa v i. (\<And>i. i < length v \<longrightarrow> local.times a v ! i = a * v ! i) \<Longrightarrow> i < length (aa # v) \<longrightarrow> local.times a (aa # v) ! i = a * (aa # v) ! i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa v i. (\<And>i. i < length v \<longrightarrow> local.times a v ! i = a * v ! i) \<Longrightarrow> i < length (aa # v) \<longrightarrow> local.times a (aa # v) ! i = a * (aa # v) ! i
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
?i < length xs \<longrightarrow> local.times a xs ! ?i = a * xs ! ?i

goal (1 subgoal):
 1. \<And>aa v i. (\<And>i. i < length v \<longrightarrow> local.times a v ! i = a * v ! i) \<Longrightarrow> i < length (aa # v) \<longrightarrow> local.times a (aa # v) ! i = a * (aa # v) ! i
[PROOF STEP]
have "\<forall>i.((x#xs)!(i+1) = (xs)!i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. (x # xs) ! (i + 1) = xs ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i. (x # xs) ! (i + 1) = xs ! i

goal (1 subgoal):
 1. \<And>aa v i. (\<And>i. i < length v \<longrightarrow> local.times a v ! i = a * v ! i) \<Longrightarrow> i < length (aa # v) \<longrightarrow> local.times a (aa # v) ! i = a * (aa # v) ! i
[PROOF STEP]
have 0:"((i<length (x#xs))\<longrightarrow> ((i<(length xs)) \<or> (i = (length xs))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length (x # xs) \<longrightarrow> i < length xs \<or> i = length xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length (x # xs) \<longrightarrow> i < length xs \<or> i = length xs

goal (1 subgoal):
 1. \<And>aa v i. (\<And>i. i < length v \<longrightarrow> local.times a v ! i = a * v ! i) \<Longrightarrow> i < length (aa # v) \<longrightarrow> local.times a (aa # v) ! i = a * (aa # v) ! i
[PROOF STEP]
have 1:" ((i<length xs) \<longrightarrow>((times a xs)!i = f a (xs!i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length xs \<longrightarrow> local.times a xs ! i = a * xs ! i
[PROOF STEP]
by (metis Cons.hyps)
[PROOF STATE]
proof (state)
this:
i < length xs \<longrightarrow> local.times a xs ! i = a * xs ! i

goal (1 subgoal):
 1. \<And>aa v i. (\<And>i. i < length v \<longrightarrow> local.times a v ! i = a * v ! i) \<Longrightarrow> i < length (aa # v) \<longrightarrow> local.times a (aa # v) ! i = a * (aa # v) ! i
[PROOF STEP]
have "\<forall>i.((x#xs)!(i+1) = (xs)!i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. (x # xs) ! (i + 1) = xs ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i. (x # xs) ! (i + 1) = xs ! i

goal (1 subgoal):
 1. \<And>aa v i. (\<And>i. i < length v \<longrightarrow> local.times a v ! i = a * v ! i) \<Longrightarrow> i < length (aa # v) \<longrightarrow> local.times a (aa # v) ! i = a * (aa # v) ! i
[PROOF STEP]
have "((i <length (x#xs)) \<longrightarrow>(times a (x#xs))!i = f a ((x#xs)!i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
proof(cases i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = 0 \<Longrightarrow> i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
 2. \<And>nat. i = Suc nat \<Longrightarrow> i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
i = 0

goal (2 subgoals):
 1. i = 0 \<Longrightarrow> i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
 2. \<And>nat. i = Suc nat \<Longrightarrow> i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
have "((times a (x#xs))!i) = f a x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.times a (x # xs) ! i = a * x
[PROOF STEP]
using 0 times.simps(2)
[PROOF STATE]
proof (prove)
using this:
i = 0
local.times ?n (?y # ?ys) = (?n * ?y) # local.times ?n ?ys

goal (1 subgoal):
 1. local.times a (x # xs) ! i = a * x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.times a (x # xs) ! i = a * x

goal (2 subgoals):
 1. i = 0 \<Longrightarrow> i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
 2. \<And>nat. i = Suc nat \<Longrightarrow> i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
local.times a (x # xs) ! i = a * x
[PROOF STEP]
have "(times a (x#xs))!i = f a ((x#xs)!i)"
[PROOF STATE]
proof (prove)
using this:
local.times a (x # xs) ! i = a * x

goal (1 subgoal):
 1. local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
local.times a (x # xs) ! i = a * x
i = 0

goal (1 subgoal):
 1. local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.times a (x # xs) ! i = a * (x # xs) ! i

goal (2 subgoals):
 1. i = 0 \<Longrightarrow> i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
 2. \<And>nat. i = Suc nat \<Longrightarrow> i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
local.times a (x # xs) ! i = a * (x # xs) ! i

goal (1 subgoal):
 1. i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i

goal (1 subgoal):
 1. \<And>nat. i = Suc nat \<Longrightarrow> i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. i = Suc nat \<Longrightarrow> i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
case (Suc j)
[PROOF STATE]
proof (state)
this:
i = Suc j

goal (1 subgoal):
 1. \<And>nat. i = Suc nat \<Longrightarrow> i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
have 1:"(times a (x#xs))!i = ((f a x)#(times a xs))!i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.times a (x # xs) ! i = ((a * x) # local.times a xs) ! i
[PROOF STEP]
using times.simps(2)
[PROOF STATE]
proof (prove)
using this:
local.times ?n (?y # ?ys) = (?n * ?y) # local.times ?n ?ys

goal (1 subgoal):
 1. local.times a (x # xs) ! i = ((a * x) # local.times a xs) ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.times a (x # xs) ! i = ((a * x) # local.times a xs) ! i

goal (1 subgoal):
 1. \<And>nat. i = Suc nat \<Longrightarrow> i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
have 2:"((f a x)#(times a xs))!i = (times a xs)!j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((a * x) # local.times a xs) ! i = local.times a xs ! j
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
i = Suc j

goal (1 subgoal):
 1. ((a * x) # local.times a xs) ! i = local.times a xs ! j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((a * x) # local.times a xs) ! i = local.times a xs ! j

goal (1 subgoal):
 1. \<And>nat. i = Suc nat \<Longrightarrow> i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
have 3:"(i <length (x#xs)) \<longrightarrow> (j<length xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length (x # xs) \<longrightarrow> j < length xs
[PROOF STEP]
using One_nat_def Suc Suc_eq_plus1 list.size(4) not_less_eq
[PROOF STATE]
proof (prove)
using this:
1 = Suc 0
i = Suc j
Suc ?n = ?n + 1
length (?x21.0 # ?x22.0) = length ?x22.0 + Suc 0
(\<not> ?m < ?n) = (?n < Suc ?m)

goal (1 subgoal):
 1. i < length (x # xs) \<longrightarrow> j < length xs
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i < length (x # xs) \<longrightarrow> j < length xs

goal (1 subgoal):
 1. \<And>nat. i = Suc nat \<Longrightarrow> i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
have 4:"(j<length xs) \<longrightarrow> ((times a xs)!j = (f a (xs!j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < length xs \<longrightarrow> local.times a xs ! j = a * xs ! j
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
local.times a (x # xs) ! i = ((a * x) # local.times a xs) ! i

goal (1 subgoal):
 1. j < length xs \<longrightarrow> local.times a xs ! j = a * xs ! j
[PROOF STEP]
by (metis Cons.hyps)
[PROOF STATE]
proof (state)
this:
j < length xs \<longrightarrow> local.times a xs ! j = a * xs ! j

goal (1 subgoal):
 1. \<And>nat. i = Suc nat \<Longrightarrow> i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
have 5:"(x#xs)!i = (xs!j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x # xs) ! i = xs ! j
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
i = Suc j

goal (1 subgoal):
 1. (x # xs) ! i = xs ! j
[PROOF STEP]
by (metis nth_Cons_Suc)
[PROOF STATE]
proof (state)
this:
(x # xs) ! i = xs ! j

goal (1 subgoal):
 1. \<And>nat. i = Suc nat \<Longrightarrow> i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
with 1 2 4
[PROOF STATE]
proof (chain)
picking this:
local.times a (x # xs) ! i = ((a * x) # local.times a xs) ! i
((a * x) # local.times a xs) ! i = local.times a xs ! j
j < length xs \<longrightarrow> local.times a xs ! j = a * xs ! j
(x # xs) ! i = xs ! j
[PROOF STEP]
have "(j<length xs)
                            \<longrightarrow> ((times a (x#xs))!i = (f a ((x#xs)!i)))"
[PROOF STATE]
proof (prove)
using this:
local.times a (x # xs) ! i = ((a * x) # local.times a xs) ! i
((a * x) # local.times a xs) ! i = local.times a xs ! j
j < length xs \<longrightarrow> local.times a xs ! j = a * xs ! j
(x # xs) ! i = xs ! j

goal (1 subgoal):
 1. j < length xs \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < length xs \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i

goal (1 subgoal):
 1. \<And>nat. i = Suc nat \<Longrightarrow> i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
with 3
[PROOF STATE]
proof (chain)
picking this:
i < length (x # xs) \<longrightarrow> j < length xs
j < length xs \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
have "(i <length (x#xs))
                            \<longrightarrow> ((times a (x#xs))!i = (f a ((x#xs)!i)))"
[PROOF STATE]
proof (prove)
using this:
i < length (x # xs) \<longrightarrow> j < length xs
j < length xs \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i

goal (1 subgoal):
 1. i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i

goal (1 subgoal):
 1. \<And>nat. i = Suc nat \<Longrightarrow> i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i

goal (1 subgoal):
 1. i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i

goal (1 subgoal):
 1. \<And>aa v i. (\<And>i. i < length v \<longrightarrow> local.times a v ! i = a * v ! i) \<Longrightarrow> i < length (aa # v) \<longrightarrow> local.times a (aa # v) ! i = a * (aa # v) ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i

goal (1 subgoal):
 1. i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length (x # xs) \<longrightarrow> local.times a (x # xs) ! i = a * (x # xs) ! i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma simpl_times_elements:
 assumes "(i<length xs)"
 shows "((i<(length v)) \<longrightarrow> (times a v)!i = f a (v!i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length v \<longrightarrow> local.times a v ! i = a * v ! i
[PROOF STEP]
using times_elements
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length ?v. local.times ?a ?v ! i = ?a * ?v ! i

goal (1 subgoal):
 1. i < length v \<longrightarrow> local.times a v ! i = a * v ! i
[PROOF STEP]
by auto


[STATEMENT]
lemma append_simpl: "i<(length xs) \<longrightarrow> (xs@ys)!i = (xs!i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length xs \<longrightarrow> (xs @ ys) ! i = xs ! i
[PROOF STEP]
using nth_append
[PROOF STATE]
proof (prove)
using this:
(?xs @ ?ys) ! ?n = (if ?n < length ?xs then ?xs ! ?n else ?ys ! (?n - length ?xs))

goal (1 subgoal):
 1. i < length xs \<longrightarrow> (xs @ ys) ! i = xs ! i
[PROOF STEP]
by metis


[STATEMENT]
lemma append_simpl2: "i \<ge>(length xs) \<longrightarrow> (xs@ys)!i = (ys!(i- (length xs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs \<le> i \<longrightarrow> (xs @ ys) ! i = ys ! (i - length xs)
[PROOF STEP]
using nth_append less_asym  leD
[PROOF STATE]
proof (prove)
using this:
(?xs @ ?ys) ! ?n = (if ?n < length ?xs then ?xs ! ?n else ?ys ! (?n - length ?xs))
\<lbrakk>?x < ?y; \<not> ?P \<Longrightarrow> ?y < ?x\<rbrakk> \<Longrightarrow> ?P
?y \<le> ?x \<Longrightarrow> \<not> ?x < ?y

goal (1 subgoal):
 1. length xs \<le> i \<longrightarrow> (xs @ ys) ! i = ys ! (i - length xs)
[PROOF STEP]
by metis


[STATEMENT]
lemma append_simpl3:
 assumes "i > (length y)"
 shows " (i <((length (z#zs))*(length y)))
                  \<longrightarrow> (i - (length y))< (length zs)*(length y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length (z # zs) * length y \<longrightarrow> i - length y < length zs * length y
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i < length (z # zs) * length y \<longrightarrow> i - length y < length zs * length y
[PROOF STEP]
have "length (z#zs) = (length zs)+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (z # zs) = length zs + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (z # zs) = length zs + 1

goal (1 subgoal):
 1. i < length (z # zs) * length y \<longrightarrow> i - length y < length zs * length y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (z # zs) = length zs + 1
[PROOF STEP]
have "i <((length (z#zs))*(length y))
                   \<longrightarrow> i <((length zs)+1)*(length y)"
[PROOF STATE]
proof (prove)
using this:
length (z # zs) = length zs + 1

goal (1 subgoal):
 1. i < length (z # zs) * length y \<longrightarrow> i < (length zs + 1) * length y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length (z # zs) * length y \<longrightarrow> i < (length zs + 1) * length y

goal (1 subgoal):
 1. i < length (z # zs) * length y \<longrightarrow> i - length y < length zs * length y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length (z # zs) * length y \<longrightarrow> i < (length zs + 1) * length y
[PROOF STEP]
have 1: "i <((length (z#zs))*(length y))
                  \<longrightarrow> (i <((length zs)*(length y)+ (length y)))"
[PROOF STATE]
proof (prove)
using this:
i < length (z # zs) * length y \<longrightarrow> i < (length zs + 1) * length y

goal (1 subgoal):
 1. i < length (z # zs) * length y \<longrightarrow> i < length zs * length y + length y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length (z # zs) * length y \<longrightarrow> i < length zs * length y + length y

goal (1 subgoal):
 1. i < length (z # zs) * length y \<longrightarrow> i - length y < length zs * length y
[PROOF STEP]
have "i <((length zs)*(length y)+ (length y))
                   = ((i - (length y)) <((length zs)*(length y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i < length zs * length y + length y) = (i - length y < length zs * length y)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length y < i

goal (1 subgoal):
 1. (i < length zs * length y + length y) = (i - length y < length zs * length y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(i < length zs * length y + length y) = (i - length y < length zs * length y)

goal (1 subgoal):
 1. i < length (z # zs) * length y \<longrightarrow> i - length y < length zs * length y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(i < length zs * length y + length y) = (i - length y < length zs * length y)
[PROOF STEP]
have "(i <((length (z#zs))*(length y)))
                  \<longrightarrow> ((i - (length y)) <((length zs)*(length y)))"
[PROOF STATE]
proof (prove)
using this:
(i < length zs * length y + length y) = (i - length y < length zs * length y)

goal (1 subgoal):
 1. i < length (z # zs) * length y \<longrightarrow> i - length y < length zs * length y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length (z # zs) * length y \<longrightarrow> i - length y < length zs * length y

goal (1 subgoal):
 1. i < length (z # zs) * length y \<longrightarrow> i - length y < length zs * length y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length (z # zs) * length y \<longrightarrow> i - length y < length zs * length y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i < length (z # zs) * length y \<longrightarrow> i - length y < length zs * length y

goal (1 subgoal):
 1. i < length (z # zs) * length y \<longrightarrow> i - length y < length zs * length y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length (z # zs) * length y \<longrightarrow> i - length y < length zs * length y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma append_simpl4:
"(i > (length y))
         \<longrightarrow> ((i <((length (z#zs))*(length y))))
                \<longrightarrow> ((i - (length y))< (length zs)*(length y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length y < i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> i - length y < length zs * length y
[PROOF STEP]
using append_simpl3
[PROOF STATE]
proof (prove)
using this:
length ?y < ?i \<Longrightarrow> ?i < length (?z # ?zs) * length ?y \<longrightarrow> ?i - length ?y < length ?zs * length ?y

goal (1 subgoal):
 1. length y < i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> i - length y < length zs * length y
[PROOF STEP]
by auto


[STATEMENT]
lemma vec_vec_Tensor_simpl:
   "i<(length y) \<longrightarrow> (vec_vec_Tensor (z#zs) y)!i = (times z y)!i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = local.times z y ! i
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i < length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = local.times z y ! i
[PROOF STEP]
have a: "vec_vec_Tensor (z#zs) y = (times z y)@(vec_vec_Tensor zs y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_vec_Tensor (z # zs) y = local.times z y @ vec_vec_Tensor zs y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec_vec_Tensor (z # zs) y = local.times z y @ vec_vec_Tensor zs y

goal (1 subgoal):
 1. i < length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = local.times z y ! i
[PROOF STEP]
have b: "length (times z y) = (length y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (local.times z y) = length y
[PROOF STEP]
using preserving_length
[PROOF STATE]
proof (prove)
using this:
length (local.times ?n ?y) = length ?y

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

goal (1 subgoal):
 1. i < length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = local.times z y ! i
[PROOF STEP]
have "i<(length (times z y))
          \<longrightarrow> ((times z y)@(vec_vec_Tensor zs y))!i = (times z y)!i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length (local.times z y) \<longrightarrow> (local.times z y @ vec_vec_Tensor zs y) ! i = local.times z y ! i
[PROOF STEP]
using append_simpl
[PROOF STATE]
proof (prove)
using this:
?i < length ?xs \<longrightarrow> (?xs @ ?ys) ! ?i = ?xs ! ?i

goal (1 subgoal):
 1. i < length (local.times z y) \<longrightarrow> (local.times z y @ vec_vec_Tensor zs y) ! i = local.times z y ! i
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i < length (local.times z y) \<longrightarrow> (local.times z y @ vec_vec_Tensor zs y) ! i = local.times z y ! i

goal (1 subgoal):
 1. i < length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = local.times z y ! i
[PROOF STEP]
with b
[PROOF STATE]
proof (chain)
picking this:
length (local.times z y) = length y
i < length (local.times z y) \<longrightarrow> (local.times z y @ vec_vec_Tensor zs y) ! i = local.times z y ! i
[PROOF STEP]
have "i<(length y)
          \<longrightarrow> ((times z y)@(vec_vec_Tensor zs y))!i = (times z y)!i"
[PROOF STATE]
proof (prove)
using this:
length (local.times z y) = length y
i < length (local.times z y) \<longrightarrow> (local.times z y @ vec_vec_Tensor zs y) ! i = local.times z y ! i

goal (1 subgoal):
 1. i < length y \<longrightarrow> (local.times z y @ vec_vec_Tensor zs y) ! i = local.times z y ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length y \<longrightarrow> (local.times z y @ vec_vec_Tensor zs y) ! i = local.times z y ! i

goal (1 subgoal):
 1. i < length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = local.times z y ! i
[PROOF STEP]
with  a
[PROOF STATE]
proof (chain)
picking this:
vec_vec_Tensor (z # zs) y = local.times z y @ vec_vec_Tensor zs y
i < length y \<longrightarrow> (local.times z y @ vec_vec_Tensor zs y) ! i = local.times z y ! i
[PROOF STEP]
have "i<(length y)
          \<longrightarrow> (vec_vec_Tensor (z#zs) y)!i = (times z y)!i"
[PROOF STATE]
proof (prove)
using this:
vec_vec_Tensor (z # zs) y = local.times z y @ vec_vec_Tensor zs y
i < length y \<longrightarrow> (local.times z y @ vec_vec_Tensor zs y) ! i = local.times z y ! i

goal (1 subgoal):
 1. i < length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = local.times z y ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = local.times z y ! i

goal (1 subgoal):
 1. i < length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = local.times z y ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = local.times z y ! i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i < length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = local.times z y ! i

goal (1 subgoal):
 1. i < length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = local.times z y ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = local.times z y ! i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vec_vec_Tensor_simpl2:
  "(i \<ge> (length y))
  \<longrightarrow> ((vec_vec_Tensor (z#zs) y)!i = (vec_vec_Tensor zs y)!(i- (length y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length y \<le> i \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = vec_vec_Tensor zs y ! (i - length y)
[PROOF STEP]
using vec_vec_Tensor.simps(2) append_simpl2  preserving_length
[PROOF STATE]
proof (prove)
using this:
vec_vec_Tensor (?x # ?xs) ?ys = local.times ?x ?ys @ vec_vec_Tensor ?xs ?ys
length ?xs \<le> ?i \<longrightarrow> (?xs @ ?ys) ! ?i = ?ys ! (?i - length ?xs)
length (local.times ?n ?y) = length ?y

goal (1 subgoal):
 1. length y \<le> i \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = vec_vec_Tensor zs y ! (i - length y)
[PROOF STEP]
by metis


[STATEMENT]
lemma division_product:
 assumes "(b::int)>0"
 and "a \<ge>b"
 shows " (a div b) = ((a - b) div b) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
fix c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
have "a -b \<ge>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> a - b
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
b \<le> a

goal (1 subgoal):
 1. 0 \<le> a - b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> a - b

goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
have 1: "a - b = a + (-1)*b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a - b = a + - 1 * b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a - b = a + - 1 * b

goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
have "(b \<noteq> 0) \<longrightarrow> ((a + b * (-1)) div b = (-1) + a div b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<noteq> 0 \<longrightarrow> (a + b * - 1) div b = - 1 + a div b
[PROOF STEP]
using div_mult_self2
[PROOF STATE]
proof (prove)
using this:
?b \<noteq> (0::?'a) \<Longrightarrow> (?a + ?b * ?c) div ?b = ?c + ?a div ?b

goal (1 subgoal):
 1. b \<noteq> 0 \<longrightarrow> (a + b * - 1) div b = - 1 + a div b
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
b \<noteq> 0 \<longrightarrow> (a + b * - 1) div b = - 1 + a div b

goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
with 1 assms(1)
[PROOF STATE]
proof (chain)
picking this:
a - b = a + - 1 * b
0 < b
b \<noteq> 0 \<longrightarrow> (a + b * - 1) div b = - 1 + a div b
[PROOF STEP]
have "((a - b) div b) = (-1) + a div b"
[PROOF STATE]
proof (prove)
using this:
a - b = a + - 1 * b
0 < b
b \<noteq> 0 \<longrightarrow> (a + b * - 1) div b = - 1 + a div b

goal (1 subgoal):
 1. (a - b) div b = - 1 + a div b
[PROOF STEP]
using less_int_code(1)
[PROOF STATE]
proof (prove)
using this:
a - b = a + - 1 * b
0 < b
b \<noteq> 0 \<longrightarrow> (a + b * - 1) div b = - 1 + a div b
(0 < 0) = False

goal (1 subgoal):
 1. (a - b) div b = - 1 + a div b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a - b) div b = - 1 + a div b

goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(a - b) div b = - 1 + a div b
[PROOF STEP]
have "(a div b) = ((a - b) div b) + 1"
[PROOF STATE]
proof (prove)
using this:
(a - b) div b = - 1 + a div b

goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a div b = (a - b) div b + 1

goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a div b = (a - b) div b + 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a div b = (a - b) div b + 1

goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a div b = (a - b) div b + 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma int_nat_div:
   "(int a) div (int b) = int ((a::nat) div b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int a div int b = int (a div b)
[PROOF STEP]
by (metis zdiv_int)


[STATEMENT]
lemma int_nat_eq:
 assumes "int (a::nat) = int b"
 shows "a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = b
[PROOF STEP]
using  assms of_nat_eq_iff
[PROOF STATE]
proof (prove)
using this:
int a = int b
(of_nat ?m = of_nat ?n) = (?m = ?n)

goal (1 subgoal):
 1. a = b
[PROOF STEP]
by auto


[STATEMENT]
lemma nat_div:
 assumes "(b::nat) > 0"
     and "a > b"
 shows "(a div b) = ((a - b) div b) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
have 1:"(int b)>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < int b
[PROOF STEP]
using assms(1) division_product
[PROOF STATE]
proof (prove)
using this:
0 < b
\<lbrakk>0 < ?b; ?b \<le> ?a\<rbrakk> \<Longrightarrow> ?a div ?b = (?a - ?b) div ?b + 1

goal (1 subgoal):
 1. 0 < int b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < int b

goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < int b

goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
have "(int a)>(int b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int b < int a
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
b < a

goal (1 subgoal):
 1. int b < int a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int b < int a

goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
0 < int b
int b < int a
[PROOF STEP]
have 2: "((int a) div (int b))
                   = (((int a) - (int b)) div (int b)) + 1"
[PROOF STATE]
proof (prove)
using this:
0 < int b
int b < int a

goal (1 subgoal):
 1. int a div int b = (int a - int b) div int b + 1
[PROOF STEP]
using division_product
[PROOF STATE]
proof (prove)
using this:
0 < int b
int b < int a
\<lbrakk>0 < ?b; ?b \<le> ?a\<rbrakk> \<Longrightarrow> ?a div ?b = (?a - ?b) div ?b + 1

goal (1 subgoal):
 1. int a div int b = (int a - int b) div int b + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int a div int b = (int a - int b) div int b + 1

goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
from int_nat_div
[PROOF STATE]
proof (chain)
picking this:
int ?a div int ?b = int (?a div ?b)
[PROOF STEP]
have 3: "((int a) div (int b)) = int ( a div b)"
[PROOF STATE]
proof (prove)
using this:
int ?a div int ?b = int (?a div ?b)

goal (1 subgoal):
 1. int a div int b = int (a div b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int a div int b = int (a div b)

goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
from int_nat_div assms(2)
[PROOF STATE]
proof (chain)
picking this:
int ?a div int ?b = int (?a div ?b)
b < a
[PROOF STEP]
have 4:
        "(((int a) - (int b)) div (int b)) = int ((a - b) div b)"
[PROOF STATE]
proof (prove)
using this:
int ?a div int ?b = int (?a div ?b)
b < a

goal (1 subgoal):
 1. (int a - int b) div int b = int ((a - b) div b)
[PROOF STEP]
by (metis (full_types) less_asym not_less of_nat_diff)
[PROOF STATE]
proof (state)
this:
(int a - int b) div int b = int ((a - b) div b)

goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
have "(int x) + 1 = int (x +1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int x + 1 = int (x + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int x + 1 = int (x + 1)

goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
with 2 3 4
[PROOF STATE]
proof (chain)
picking this:
int a div int b = (int a - int b) div int b + 1
int a div int b = int (a div b)
(int a - int b) div int b = int ((a - b) div b)
int x + 1 = int (x + 1)
[PROOF STEP]
have "int (a div b) = int (((a - b) div b) + 1)"
[PROOF STATE]
proof (prove)
using this:
int a div int b = (int a - int b) div int b + 1
int a div int b = int (a div b)
(int a - int b) div int b = int ((a - b) div b)
int x + 1 = int (x + 1)

goal (1 subgoal):
 1. int (a div b) = int ((a - b) div b + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int (a div b) = int ((a - b) div b + 1)

goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
with int_nat_eq
[PROOF STATE]
proof (chain)
picking this:
int ?a = int ?b \<Longrightarrow> ?a = ?b
int (a div b) = int ((a - b) div b + 1)
[PROOF STEP]
have "(a div b) = ((a - b) div b) + 1"
[PROOF STATE]
proof (prove)
using this:
int ?a = int ?b \<Longrightarrow> ?a = ?b
int (a div b) = int ((a - b) div b + 1)

goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a div b = (a - b) div b + 1

goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a div b = (a - b) div b + 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a div b = (a - b) div b + 1

goal (1 subgoal):
 1. a div b = (a - b) div b + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a div b = (a - b) div b + 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mod_eq:
 "(m::int) mod n = (m + (-1)*n) mod n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m mod n = (m + - 1 * n) mod n
[PROOF STEP]
using mod_mult_self1
[PROOF STATE]
proof (prove)
using this:
(?a + ?c * ?b) mod ?b = ?a mod ?b

goal (1 subgoal):
 1. m mod n = (m + - 1 * n) mod n
[PROOF STEP]
by metis


[STATEMENT]
lemma nat_mod_eq: "int m mod int n = int (m mod n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int m mod int n = int (m mod n)
[PROOF STEP]
by (simp add: of_nat_mod)


[STATEMENT]
lemma nat_mod:
 assumes  "(m::nat) > n"
 shows "(m::nat) mod n = (m -n) mod n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m mod n = (m - n) mod n
[PROOF STEP]
using assms mod_if not_less_iff_gr_or_eq
[PROOF STATE]
proof (prove)
using this:
n < m
?m mod ?n = (if ?m < ?n then ?m else (?m - ?n) mod ?n)
(\<not> ?x < ?y) = (?y < ?x \<or> ?x = ?y)

goal (1 subgoal):
 1. m mod n = (m - n) mod n
[PROOF STEP]
by auto


[STATEMENT]
lemma logic:
 assumes "A \<longrightarrow> B"
     and "\<not>A \<longrightarrow> B"
 shows "B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B
[PROOF STEP]
using assms(1) assms(2)
[PROOF STATE]
proof (prove)
using this:
A \<longrightarrow> B
\<not> A \<longrightarrow> B

goal (1 subgoal):
 1. B
[PROOF STEP]
by auto