[STATEMENT]
theorem well_defined_vec_mat_Tensor:
"(mat (row_length M) (length M) M) \<Longrightarrow>
                  (mat
                    ((row_length M)*(length v))
                    (length M)
                           (vec_mat_Tensor v M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length M) (length M) M \<Longrightarrow> mat (row_length M * length v) (length M) (vec_mat_Tensor v M)
[PROOF STEP]
proof(induct M)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mat (row_length []) (length []) [] \<Longrightarrow> mat (row_length [] * length v) (length []) (vec_mat_Tensor v [])
 2. \<And>a M. \<lbrakk>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 # M)) (length (a # M)) (a # M)\<rbrakk> \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
mat (row_length []) (length []) []

goal (2 subgoals):
 1. mat (row_length []) (length []) [] \<Longrightarrow> mat (row_length [] * length v) (length []) (vec_mat_Tensor v [])
 2. \<And>a M. \<lbrakk>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 # M)) (length (a # M)) (a # M)\<rbrakk> \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
have "(vec_mat_Tensor v []) = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_mat_Tensor v [] = []
[PROOF STEP]
using vec_mat_Tensor.simps(1) Nil
[PROOF STATE]
proof (prove)
using this:
vec_mat_Tensor ?xs [] = []
mat (row_length []) (length []) []

goal (1 subgoal):
 1. vec_mat_Tensor v [] = []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vec_mat_Tensor v [] = []

goal (2 subgoals):
 1. mat (row_length []) (length []) [] \<Longrightarrow> mat (row_length [] * length v) (length []) (vec_mat_Tensor v [])
 2. \<And>a M. \<lbrakk>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 # M)) (length (a # M)) (a # M)\<rbrakk> \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vec_mat_Tensor v [] = []

goal (2 subgoals):
 1. mat (row_length []) (length []) [] \<Longrightarrow> mat (row_length [] * length v) (length []) (vec_mat_Tensor v [])
 2. \<And>a M. \<lbrakk>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 # M)) (length (a # M)) (a # M)\<rbrakk> \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
have "(row_length [] = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_length [] = 0
[PROOF STEP]
using row_length_def Nil
[PROOF STATE]
proof (prove)
using this:
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)
mat (row_length []) (length []) []

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

goal (2 subgoals):
 1. mat (row_length []) (length []) [] \<Longrightarrow> mat (row_length [] * length v) (length []) (vec_mat_Tensor v [])
 2. \<And>a M. \<lbrakk>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 # M)) (length (a # M)) (a # M)\<rbrakk> \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
row_length [] = 0

goal (2 subgoals):
 1. mat (row_length []) (length []) [] \<Longrightarrow> mat (row_length [] * length v) (length []) (vec_mat_Tensor v [])
 2. \<And>a M. \<lbrakk>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 # M)) (length (a # M)) (a # M)\<rbrakk> \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
have "(length []) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length [] = 0
[PROOF STEP]
using Nil
[PROOF STATE]
proof (prove)
using this:
mat (row_length []) (length []) []

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

goal (2 subgoals):
 1. mat (row_length []) (length []) [] \<Longrightarrow> mat (row_length [] * length v) (length []) (vec_mat_Tensor v [])
 2. \<And>a M. \<lbrakk>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 # M)) (length (a # M)) (a # M)\<rbrakk> \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
vec_mat_Tensor v [] = []
row_length [] = 0
length [] = 0
[PROOF STEP]
have
       "mat ((row_length [])*(length v)) (length []) (vec_mat_Tensor v [])"
[PROOF STATE]
proof (prove)
using this:
vec_mat_Tensor v [] = []
row_length [] = 0
length [] = 0

goal (1 subgoal):
 1. mat (row_length [] * length v) (length []) (vec_mat_Tensor v [])
[PROOF STEP]
using zero_matrix
[PROOF STATE]
proof (prove)
using this:
vec_mat_Tensor v [] = []
row_length [] = 0
length [] = 0
mat 0 0 []

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

goal (2 subgoals):
 1. mat (row_length []) (length []) [] \<Longrightarrow> mat (row_length [] * length v) (length []) (vec_mat_Tensor v [])
 2. \<And>a M. \<lbrakk>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 # M)) (length (a # M)) (a # M)\<rbrakk> \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat (row_length [] * length v) (length []) (vec_mat_Tensor v [])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
mat (row_length [] * length v) (length []) (vec_mat_Tensor v [])

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

goal (1 subgoal):
 1. \<And>a M. \<lbrakk>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 # M)) (length (a # M)) (a # M)\<rbrakk> \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a M. \<lbrakk>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 # M)) (length (a # M)) (a # M)\<rbrakk> \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
fix a M
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a M. \<lbrakk>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 # M)) (length (a # M)) (a # M)\<rbrakk> \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
assume hyp :
   "(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#M)) (length (a#M)) (a#M)"
[PROOF STATE]
proof (state)
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 # M)) (length (a # M)) (a # M)

goal (1 subgoal):
 1. \<And>a M. \<lbrakk>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 # M)) (length (a # M)) (a # M)\<rbrakk> \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
let ?case =
   "mat (row_length (a#M) * length v) (length (a#M)) (vec_mat_Tensor v (a#M))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a M. \<lbrakk>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 # M)) (length (a # M)) (a # M)\<rbrakk> \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
have step1: "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 hyp(2) reduct_matrix
[PROOF STATE]
proof (prove)
using this:
mat (row_length (a # M)) (length (a # M)) (a # M)
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 M. \<lbrakk>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 # M)) (length (a # M)) (a # M)\<rbrakk> \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat (row_length M) (length M) M
[PROOF STEP]
have step2:
    "mat (row_length M * length v) (length M) (vec_mat_Tensor v M)"
[PROOF STATE]
proof (prove)
using this:
mat (row_length M) (length M) M

goal (1 subgoal):
 1. mat (row_length M * length v) (length M) (vec_mat_Tensor v M)
[PROOF STEP]
using hyp(1)
[PROOF STATE]
proof (prove)
using this:
mat (row_length M) (length M) M
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 M * length v) (length M) (vec_mat_Tensor v M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat (row_length M * length v) (length M) (vec_mat_Tensor v M)

goal (1 subgoal):
 1. \<And>a M. \<lbrakk>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 # M)) (length (a # M)) (a # M)\<rbrakk> \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
have
   "mat
        (row_length (a#M) * length v)
        (length (a#M))
             (vec_mat_Tensor v (a#M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
proof (cases M)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. M = [] \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
 2. \<And>aa list. M = aa # list \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
M = []

goal (2 subgoals):
 1. M = [] \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
 2. \<And>aa list. M = aa # list \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. M = [] \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
 2. \<And>aa list. M = aa # list \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
have 1:"(vec_mat_Tensor v (a#M)) = [vec_vec_Tensor v a]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_mat_Tensor v (a # M) = [vec_vec_Tensor v a]
[PROOF STEP]
using vec_mat_Tensor.simps Nil
[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
M = []

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

goal (2 subgoals):
 1. M = [] \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
 2. \<And>aa list. M = aa # list \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
have   "(x \<in> (set [vec_vec_Tensor v a])) \<longrightarrow>  x = (vec_vec_Tensor v a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set [vec_vec_Tensor v a] \<longrightarrow> x = vec_vec_Tensor v a
[PROOF STEP]
using set_def
[PROOF STATE]
proof (prove)
using this:
set \<equiv> ctor_fold_list (\<lambda>z. set1_pre_list z \<union> \<Union> (set2_pre_list z))

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

goal (2 subgoals):
 1. M = [] \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
 2. \<And>aa list. M = aa # list \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set [vec_vec_Tensor v a] \<longrightarrow> x = vec_vec_Tensor v a
[PROOF STEP]
have 2:
        "(x \<in> (set [vec_vec_Tensor v a]))
                    \<longrightarrow> (vec (length (vec_vec_Tensor v a)) x)"
[PROOF STATE]
proof (prove)
using this:
x \<in> set [vec_vec_Tensor v a] \<longrightarrow> x = vec_vec_Tensor v a

goal (1 subgoal):
 1. x \<in> set [vec_vec_Tensor v a] \<longrightarrow> vec (length (vec_vec_Tensor v a)) x
[PROOF STEP]
using vec_def
[PROOF STATE]
proof (prove)
using this:
x \<in> set [vec_vec_Tensor v a] \<longrightarrow> x = vec_vec_Tensor v a
vec ?n ?x = (length ?x = ?n)

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

goal (2 subgoals):
 1. M = [] \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
 2. \<And>aa list. M = aa # list \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
have 3:"length (vec_vec_Tensor v a) = (length v)*(length a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (vec_vec_Tensor v a) = length v * length a
[PROOF STEP]
using vec_vec_Tensor_length
[PROOF STATE]
proof (prove)
using this:
length (vec_vec_Tensor ?x ?y) = length ?x * length ?y

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

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

goal (1 subgoal):
 1. length (vec_vec_Tensor v a) = length v * row_length (a # M)
[PROOF STEP]
using row_length_def  list.distinct(1)
[PROOF STATE]
proof (prove)
using this:
length (vec_vec_Tensor v a) = length v * length a
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)
[] \<noteq> ?x21.0 # ?x22.0

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

goal (2 subgoals):
 1. M = [] \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
 2. \<And>aa list. M = aa # list \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
have 6: "length (vec_mat_Tensor v (a#M)) = (length (a#M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (vec_mat_Tensor v (a # M)) = length (a # M)
[PROOF STEP]
using vec_mat_Tensor_length
[PROOF STATE]
proof (prove)
using this:
length (vec_mat_Tensor ?xs ?ys) = length ?ys

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

goal (2 subgoals):
 1. M = [] \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
 2. \<And>aa list. M = aa # list \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
hence "mat (length (vec_vec_Tensor v a)) (length (a # M)) [vec_vec_Tensor v a]"
[PROOF STATE]
proof (prove)
using this:
length (vec_mat_Tensor v (a # M)) = length (a # M)

goal (1 subgoal):
 1. mat (length (vec_vec_Tensor v a)) (length (a # M)) [vec_vec_Tensor v a]
[PROOF STEP]
by (simp add: Nil mat_def vec_def)
[PROOF STATE]
proof (state)
this:
mat (length (vec_vec_Tensor v a)) (length (a # M)) [vec_vec_Tensor v a]

goal (2 subgoals):
 1. M = [] \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
 2. \<And>aa list. M = aa # list \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
hence
        "mat (row_length (a#M) * length v)
             (length (vec_mat_Tensor v (a#M)))
             (vec_mat_Tensor v (a#M))"
[PROOF STATE]
proof (prove)
using this:
mat (length (vec_vec_Tensor v a)) (length (a # M)) [vec_vec_Tensor v a]

goal (1 subgoal):
 1. mat (row_length (a # M) * length v) (length (vec_mat_Tensor v (a # M))) (vec_mat_Tensor v (a # M))
[PROOF STEP]
using 1 4 6
[PROOF STATE]
proof (prove)
using this:
mat (length (vec_vec_Tensor v a)) (length (a # M)) [vec_vec_Tensor v a]
vec_mat_Tensor v (a # M) = [vec_vec_Tensor v a]
length (vec_vec_Tensor v a) = length v * row_length (a # M)
length (vec_mat_Tensor v (a # M)) = length (a # M)

goal (1 subgoal):
 1. mat (row_length (a # M) * length v) (length (vec_mat_Tensor v (a # M))) (vec_mat_Tensor v (a # M))
[PROOF STEP]
by (simp add: mult.commute)
[PROOF STATE]
proof (state)
this:
mat (row_length (a # M) * length v) (length (vec_mat_Tensor v (a # M))) (vec_mat_Tensor v (a # M))

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

goal (1 subgoal):
 1. mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
using 6
[PROOF STATE]
proof (prove)
using this:
mat (row_length (a # M) * length v) (length (vec_mat_Tensor v (a # M))) (vec_mat_Tensor v (a # M))
length (vec_mat_Tensor v (a # M)) = length (a # M)

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

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

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
have 1:"x \<in> (set (a#M)) \<longrightarrow> ((x=a) \<or> (x \<in> (set M)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set (a # M) \<longrightarrow> x = a \<or> x \<in> set M
[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 # M) \<longrightarrow> x = a \<or> x \<in> set M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> set (a # M) \<longrightarrow> x = a \<or> x \<in> set M

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
have "mat (row_length (a#M)) (length (a#M)) (a#M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length (a # M)) (length (a # M)) (a # M)
[PROOF STEP]
using hyp
[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 # M)) (length (a # M)) (a # M)

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

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

goal (1 subgoal):
 1. x \<in> set (a # M) \<longrightarrow> vec (row_length (a # M)) x
[PROOF STEP]
using mat_def Ball_def
[PROOF STATE]
proof (prove)
using this:
mat (row_length (a # M)) (length (a # M)) (a # M)
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 # M) \<longrightarrow> vec (row_length (a # M)) x
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
x \<in> set (a # M) \<longrightarrow> vec (row_length (a # M)) x

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

goal (1 subgoal):
 1. x \<in> set (a # M) \<longrightarrow> vec (length a) x
[PROOF STEP]
using row_length_def  list.distinct(1)
[PROOF STATE]
proof (prove)
using this:
x \<in> set (a # M) \<longrightarrow> vec (row_length (a # M)) 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 # M) \<longrightarrow> vec (length a) x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> set (a # M) \<longrightarrow> vec (length a) x

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

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

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

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

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

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

goal (1 subgoal):
 1. vec (length a) b
[PROOF STEP]
using  hyp(2) in_set_member mat_def member_rec(1) vec_def
[PROOF STATE]
proof (prove)
using this:
x \<in> set M \<longrightarrow> vec (length a) x
b \<in> set M
mat (row_length (a # M)) (length (a # M)) (a # M)
(?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. M = aa # list \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[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. M = aa # list \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length b = length a
[PROOF STEP]
have 2:"row_length M = (length a)"
[PROOF STATE]
proof (prove)
using this:
length b = length a

goal (1 subgoal):
 1. row_length M = length a
[PROOF STEP]
using row_length_def   Cons list.distinct(1)
[PROOF STATE]
proof (prove)
using this:
length b = length a
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)
M = b # L
[] \<noteq> ?x21.0 # ?x22.0

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

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
have "mat (row_length M * length v) (length M) (vec_mat_Tensor v M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length M * length v) (length M) (vec_mat_Tensor v M)
[PROOF STEP]
using step2
[PROOF STATE]
proof (prove)
using this:
mat (row_length M * length v) (length M) (vec_mat_Tensor v M)

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

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

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

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

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

goal (1 subgoal):
 1. x \<in> set (vec_mat_Tensor v M) \<longrightarrow> vec (row_length M * length v) x
[PROOF STEP]
using mat_def Ball_def
[PROOF STATE]
proof (prove)
using this:
Ball (set (vec_mat_Tensor v M)) (vec (row_length M * length v))
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 (vec_mat_Tensor v M) \<longrightarrow> vec (row_length M * length v) x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> set (vec_mat_Tensor v M) \<longrightarrow> vec (row_length M * length v) x

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

goal (1 subgoal):
 1. x \<in> set (vec_mat_Tensor v M) \<longrightarrow> vec (length a * length v) x
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
x \<in> set (vec_mat_Tensor v M) \<longrightarrow> vec (row_length M * length v) x
row_length M = length a

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

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
have 5:"length (vec_vec_Tensor v a) = (length a)*(length v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (vec_vec_Tensor v a) = length a * length v
[PROOF STEP]
using   vec_vec_Tensor_length
[PROOF STATE]
proof (prove)
using this:
length (vec_vec_Tensor ?x ?y) = length ?x * length ?y

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

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

goal (1 subgoal):
 1. vec (length a * length v) (vec_vec_Tensor v a)
[PROOF STEP]
using vec_vec_Tensor_length vec_def
[PROOF STATE]
proof (prove)
using this:
length (vec_vec_Tensor v a) = length a * length v
length (vec_vec_Tensor ?x ?y) = length ?x * length ?y
vec ?n ?x = (length ?x = ?n)

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

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
have 7:"(length a) = (row_length (a#M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length a = row_length (a # M)
[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. length a = row_length (a # M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length a = row_length (a # M)

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
have "vec_mat_Tensor v (a#M)
                   = (vec_vec_Tensor v a)#(vec_mat_Tensor v M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_mat_Tensor v (a # M) = vec_vec_Tensor v a # vec_mat_Tensor v M
[PROOF STEP]
using vec_mat_Tensor.simps(2)
[PROOF STATE]
proof (prove)
using this:
vec_mat_Tensor ?xs (?ys # ?yss) = vec_vec_Tensor ?xs ?ys # vec_mat_Tensor ?xs ?yss

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

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

goal (1 subgoal):
 1. x \<in> set (vec_mat_Tensor v (a # M)) \<longrightarrow> x = vec_vec_Tensor v a \<or> x \<in> set (vec_mat_Tensor v M)
[PROOF STEP]
using  hd_set
[PROOF STATE]
proof (prove)
using this:
vec_mat_Tensor v (a # M) = vec_vec_Tensor v a # vec_mat_Tensor v M
?x \<in> set (?a # ?M) \<Longrightarrow> ?x = ?a \<or> ?x \<in> set ?M

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

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

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

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

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

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

goal (1 subgoal):
 1. \<forall>x. x \<in> set (vec_mat_Tensor v (a # M)) \<longrightarrow> vec (row_length (a # M) * length v) x
[PROOF STEP]
using "2" "3" "6" "7" hd_set vec_mat_Tensor.simps(2)
[PROOF STATE]
proof (prove)
using this:
x \<in> set (vec_mat_Tensor v (a # M)) \<longrightarrow> vec (row_length (a # M) * length v) x
row_length M = length a
Ball (set (vec_mat_Tensor v M)) (vec (row_length M * length v))
vec (length a * length v) (vec_vec_Tensor v a)
length a = row_length (a # M)
?x \<in> set (?a # ?M) \<Longrightarrow> ?x = ?a \<or> ?x \<in> set ?M
vec_mat_Tensor ?xs (?ys # ?yss) = vec_vec_Tensor ?xs ?ys # vec_mat_Tensor ?xs ?yss

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

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

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

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

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
have 8: "length (vec_mat_Tensor v (a#M)) = length (a#M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (vec_mat_Tensor v (a # M)) = length (a # M)
[PROOF STEP]
using vec_mat_Tensor_length
[PROOF STATE]
proof (prove)
using this:
length (vec_mat_Tensor ?xs ?ys) = length ?ys

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

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
with 6  7
[PROOF STATE]
proof (chain)
picking this:
vec (length a * length v) (vec_vec_Tensor v a)
Ball (set (vec_mat_Tensor v (a # M))) (vec (row_length (a # M) * length v))
length (vec_mat_Tensor v (a # M)) = length (a # M)
[PROOF STEP]
have
               "mat
                 ((row_length (a#M))*(length v))
                 (length (a#M))
                           (vec_mat_Tensor v (a#M))"
[PROOF STATE]
proof (prove)
using this:
vec (length a * length v) (vec_vec_Tensor v a)
Ball (set (vec_mat_Tensor v (a # M))) (vec (row_length (a # M) * length v))
length (vec_mat_Tensor v (a # M)) = length (a # M)

goal (1 subgoal):
 1. mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
using mat_def  "5" length_code
[PROOF STATE]
proof (prove)
using this:
vec (length a * length v) (vec_vec_Tensor v a)
Ball (set (vec_mat_Tensor v (a # M))) (vec (row_length (a # M) * length v))
length (vec_mat_Tensor v (a # M)) = length (a # M)
mat ?nr ?nc ?m = (length ?m = ?nc \<and> Ball (set ?m) (vec ?nr))
length (vec_vec_Tensor v a) = length a * length v
length = List.gen_length 0

goal (1 subgoal):
 1. mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
by (metis (opaque_lifting, no_types))
[PROOF STATE]
proof (state)
this:
mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))

goal (1 subgoal):
 1. \<And>a M. \<lbrakk>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 # M)) (length (a # M)) (a # M)\<rbrakk> \<Longrightarrow> mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
with  hyp
[PROOF STATE]
proof (chain)
picking 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 # M)) (length (a # M)) (a # M)
mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))
[PROOF STEP]
show ?case
[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 # M)) (length (a # M)) (a # M)
mat (row_length (a # M) * length v) (length (a # M)) (vec_mat_Tensor v (a # M))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma length_Tensor:" (length (M1\<otimes>M2)) = (length M1)*(length M2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (M1 \<otimes> M2) = length M1 * length M2
[PROOF STEP]
proof(induct M1)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length ([] \<otimes> M2) = length [] * length M2
 2. \<And>a M1. length (M1 \<otimes> M2) = length M1 * length M2 \<Longrightarrow> length (a # M1 \<otimes> M2) = length (a # M1) * length M2
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. length ([] \<otimes> M2) = length [] * length M2
 2. \<And>a M1. length (M1 \<otimes> M2) = length M1 * length M2 \<Longrightarrow> length (a # M1 \<otimes> M2) = length (a # M1) * length M2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ([] \<otimes> M2) = length [] * length M2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length ([] \<otimes> M2) = length [] * length M2

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

goal (1 subgoal):
 1. \<And>a M1. length (M1 \<otimes> M2) = length M1 * length M2 \<Longrightarrow> length (a # M1 \<otimes> M2) = length (a # M1) * length M2
[PROOF STEP]
have "((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>a M1. length (M1 \<otimes> M2) = length M1 * length M2 \<Longrightarrow> length (a # M1 \<otimes> M2) = length (a # M1) * length 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 1:
          "length ((a # M1) \<otimes> M2) = length ((vec_mat_Tensor a M2)@(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. length (a # M1 \<otimes> M2) = length (vec_mat_Tensor a M2 @ (M1 \<otimes> M2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (a # M1 \<otimes> M2) = length (vec_mat_Tensor a M2 @ (M1 \<otimes> M2))

goal (1 subgoal):
 1. \<And>a M1. length (M1 \<otimes> M2) = length M1 * length M2 \<Longrightarrow> length (a # M1 \<otimes> M2) = length (a # M1) * length M2
[PROOF STEP]
have 2:"length ((vec_mat_Tensor a M2)@(M1 \<otimes> M2))
              = length (vec_mat_Tensor a M2)+ length (M1 \<otimes> M2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (vec_mat_Tensor a M2 @ (M1 \<otimes> M2)) = length (vec_mat_Tensor a M2) + length (M1 \<otimes> M2)
[PROOF STEP]
using append_def
[PROOF STATE]
proof (prove)
using this:
(@) \<equiv> rec_list (\<lambda>ys. ys) (\<lambda>x xs xsa ys. x # xsa ys)

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

goal (1 subgoal):
 1. \<And>a M1. length (M1 \<otimes> M2) = length M1 * length M2 \<Longrightarrow> length (a # M1 \<otimes> M2) = length (a # M1) * length M2
[PROOF STEP]
have 3:"(length (vec_mat_Tensor a M2)) = length M2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (vec_mat_Tensor a M2) = length M2
[PROOF STEP]
using vec_mat_Tensor_length
[PROOF STATE]
proof (prove)
using this:
length (vec_mat_Tensor ?xs ?ys) = length ?ys

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

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

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

goal (1 subgoal):
 1. \<And>a M1. length (M1 \<otimes> M2) = length M1 * length M2 \<Longrightarrow> length (a # M1 \<otimes> M2) = length (a # M1) * length M2
[PROOF STEP]
with 2 3
[PROOF STATE]
proof (chain)
picking this:
length (vec_mat_Tensor a M2 @ (M1 \<otimes> M2)) = length (vec_mat_Tensor a M2) + length (M1 \<otimes> M2)
length (vec_mat_Tensor a M2) = length M2
length (M1 \<otimes> M2) = length M1 * length M2
[PROOF STEP]
have "length ((vec_mat_Tensor a M2)@(M1 \<otimes> M2))
                              = (length M2) + (length M1)*(length M2)"
[PROOF STATE]
proof (prove)
using this:
length (vec_mat_Tensor a M2 @ (M1 \<otimes> M2)) = length (vec_mat_Tensor a M2) + length (M1 \<otimes> M2)
length (vec_mat_Tensor a M2) = length M2
length (M1 \<otimes> M2) = length M1 * length M2

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

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

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

goal (1 subgoal):
 1. \<And>a M1. length (M1 \<otimes> M2) = length M1 * length M2 \<Longrightarrow> length (a # M1 \<otimes> M2) = length (a # M1) * length M2
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
length (a # M1 \<otimes> M2) = length (vec_mat_Tensor a M2 @ (M1 \<otimes> M2))
length (vec_mat_Tensor a M2 @ (M1 \<otimes> M2)) = (1 + length M1) * length M2
[PROOF STEP]
have "length ((a # M1) \<otimes> M2) = ((length (a # M1)) * (length M2))"
[PROOF STATE]
proof (prove)
using this:
length (a # M1 \<otimes> M2) = length (vec_mat_Tensor a M2 @ (M1 \<otimes> M2))
length (vec_mat_Tensor a M2 @ (M1 \<otimes> M2)) = (1 + length M1) * length M2

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (2 subgoals):
 1. mat (row_length ([] @ M2)) (length ([] @ M2)) ([] @ M2) \<Longrightarrow> mat (row_length M2) (length M2) M2
 2. \<And>a M1. \<lbrakk>mat (row_length (M1 @ M2)) (length (M1 @ M2)) (M1 @ M2) \<Longrightarrow> mat (row_length M2) (length M2) M2; mat (row_length ((a # M1) @ M2)) (length ((a # M1) @ M2)) ((a # M1) @ M2)\<rbrakk> \<Longrightarrow> mat (row_length M2) (length M2) M2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length M2) (length M2) M2
[PROOF STEP]
using Nil append.simps(1)
[PROOF STATE]
proof (prove)
using this:
mat (row_length ([] @ M2)) (length ([] @ M2)) ([] @ M2)
[] @ ?ys = ?ys

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 @ M2)) (length (M1 @ M2)) (M1 @ M2) \<Longrightarrow> mat (row_length M2) (length M2) M2; mat (row_length ((a # M1) @ M2)) (length ((a # M1) @ M2)) ((a # M1) @ M2)\<rbrakk> \<Longrightarrow> mat (row_length M2) (length M2) M2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a M1. \<lbrakk>mat (row_length (M1 @ M2)) (length (M1 @ M2)) (M1 @ M2) \<Longrightarrow> mat (row_length M2) (length M2) M2; mat (row_length ((a # M1) @ M2)) (length ((a # M1) @ M2)) ((a # M1) @ M2)\<rbrakk> \<Longrightarrow> mat (row_length M2) (length M2) M2
[PROOF STEP]
case (Cons a M1)
[PROOF STATE]
proof (state)
this:
mat (row_length (M1 @ M2)) (length (M1 @ M2)) (M1 @ M2) \<Longrightarrow> mat (row_length M2) (length M2) M2
mat (row_length ((a # M1) @ M2)) (length ((a # M1) @ M2)) ((a # M1) @ M2)

goal (1 subgoal):
 1. \<And>a M1. \<lbrakk>mat (row_length (M1 @ M2)) (length (M1 @ M2)) (M1 @ M2) \<Longrightarrow> mat (row_length M2) (length M2) M2; mat (row_length ((a # M1) @ M2)) (length ((a # M1) @ M2)) ((a # M1) @ M2)\<rbrakk> \<Longrightarrow> mat (row_length M2) (length M2) M2
[PROOF STEP]
have "mat (row_length (M1 @ M2)) (length (M1 @ M2)) (M1 @ M2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length (M1 @ M2)) (length (M1 @ M2)) (M1 @ M2)
[PROOF STEP]
using reduct_matrix Cons.prems append_Cons
[PROOF STATE]
proof (prove)
using this:
mat (row_length (?a # ?M)) (length (?a # ?M)) (?a # ?M) \<Longrightarrow> mat (row_length ?M) (length ?M) ?M
mat (row_length ((a # M1) @ M2)) (length ((a # M1) @ M2)) ((a # M1) @ M2)
(?x # ?xs) @ ?ys = ?x # ?xs @ ?ys

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

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

goal (1 subgoal):
 1. mat (row_length M2) (length M2) M2
[PROOF STEP]
using Cons.hyps
[PROOF STATE]
proof (prove)
using this:
mat (row_length (M1 @ M2)) (length (M1 @ M2)) (M1 @ M2)
mat (row_length (M1 @ M2)) (length (M1 @ M2)) (M1 @ M2) \<Longrightarrow> 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 @ M2)) (length (M1 @ M2)) (M1 @ M2) \<Longrightarrow> mat (row_length M2) (length M2) M2; mat (row_length ((a # M1) @ M2)) (length ((a # M1) @ M2)) ((a # M1) @ M2)\<rbrakk> \<Longrightarrow> mat (row_length M2) (length M2) M2
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
mat (row_length M2) (length M2) M2
[PROOF STEP]
show?thesis
[PROOF STATE]
proof (prove)
using this:
mat (row_length M2) (length M2) M2

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

goal:
No subgoals!
[PROOF STEP]
qed