[STATEMENT]
lemma mat_uniqueness:
 assumes "mat nr1 nc M"
 and "mat nr2 nc M" and "z = hd M" and "M \<noteq> []"
 shows "(\<forall>x\<in>(set M).(nr1 = nr2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set M. nr1 = nr2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x\<in>set M. nr1 = nr2
[PROOF STEP]
have A:"z \<in> set M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> set M
[PROOF STEP]
using assms(1) assms(3) assms(4) set_def mat_def
[PROOF STATE]
proof (prove)
using this:
mat nr1 nc M
z = hd M
M \<noteq> []
set \<equiv> ctor_fold_list (\<lambda>z. set1_pre_list z \<union> \<Union> (set2_pre_list z))
mat ?nr ?nc ?m = (length ?m = ?nc \<and> Ball (set ?m) (vec ?nr))

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

goal (1 subgoal):
 1. \<forall>x\<in>set M. nr1 = nr2
[PROOF STEP]
have "Ball (set M) (vec nr1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ball (set M) (vec nr1)
[PROOF STEP]
using mat_def assms(1)
[PROOF STATE]
proof (prove)
using this:
mat ?nr ?nc ?m = (length ?m = ?nc \<and> Ball (set ?m) (vec ?nr))
mat nr1 nc M

goal (1 subgoal):
 1. Ball (set M) (vec nr1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ball (set M) (vec nr1)

goal (1 subgoal):
 1. \<forall>x\<in>set M. nr1 = nr2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ball (set M) (vec nr1)
[PROOF STEP]
have step1: "((x \<in> (set M)) \<longrightarrow> (vec nr1 x))"
[PROOF STATE]
proof (prove)
using this:
Ball (set M) (vec nr1)

goal (1 subgoal):
 1. x \<in> set M \<longrightarrow> vec nr1 x
[PROOF STEP]
using Ball_def assms
[PROOF STATE]
proof (prove)
using this:
Ball (set M) (vec nr1)
Ball ?A ?P = (\<forall>x. x \<in> ?A \<longrightarrow> ?P x)
mat nr1 nc M
mat nr2 nc M
z = hd M
M \<noteq> []

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

goal (1 subgoal):
 1. \<forall>x\<in>set M. nr1 = nr2
[PROOF STEP]
have "Ball (set M) (vec nr2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ball (set M) (vec nr2)
[PROOF STEP]
using mat_def assms(2)
[PROOF STATE]
proof (prove)
using this:
mat ?nr ?nc ?m = (length ?m = ?nc \<and> Ball (set ?m) (vec ?nr))
mat nr2 nc M

goal (1 subgoal):
 1. Ball (set M) (vec nr2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ball (set M) (vec nr2)

goal (1 subgoal):
 1. \<forall>x\<in>set M. nr1 = nr2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ball (set M) (vec nr2)
[PROOF STEP]
have step2: "((x \<in> (set M)) \<longrightarrow> (vec nr2 x))"
[PROOF STATE]
proof (prove)
using this:
Ball (set M) (vec nr2)

goal (1 subgoal):
 1. x \<in> set M \<longrightarrow> vec nr2 x
[PROOF STEP]
using Ball_def assms
[PROOF STATE]
proof (prove)
using this:
Ball (set M) (vec nr2)
Ball ?A ?P = (\<forall>x. x \<in> ?A \<longrightarrow> ?P x)
mat nr1 nc M
mat nr2 nc M
z = hd M
M \<noteq> []

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

goal (1 subgoal):
 1. \<forall>x\<in>set M. nr1 = nr2
[PROOF STEP]
from step1 and step2
[PROOF STATE]
proof (chain)
picking this:
x \<in> set M \<longrightarrow> vec nr1 x
x \<in> set M \<longrightarrow> vec nr2 x
[PROOF STEP]
have step3:"\<forall>x.((x \<in> (set M))\<longrightarrow> ((vec nr1 x)\<and> (vec nr2 x)))"
[PROOF STATE]
proof (prove)
using this:
x \<in> set M \<longrightarrow> vec nr1 x
x \<in> set M \<longrightarrow> vec nr2 x

goal (1 subgoal):
 1. \<forall>x. x \<in> set M \<longrightarrow> vec nr1 x \<and> vec nr2 x
[PROOF STEP]
by (metis \<open>Ball (set M) (vec nr1)\<close> \<open>Ball (set M) (vec nr2)\<close>)
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<in> set M \<longrightarrow> vec nr1 x \<and> vec nr2 x

goal (1 subgoal):
 1. \<forall>x\<in>set M. nr1 = nr2
[PROOF STEP]
have "((vec nr1 x)\<and> (vec nr2 x)) \<longrightarrow> (nr1 = nr2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec nr1 x \<and> vec nr2 x \<longrightarrow> nr1 = nr2
[PROOF STEP]
using vec_uniqueness
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>vec ?m ?v; vec ?n ?v\<rbrakk> \<Longrightarrow> ?m = ?n

goal (1 subgoal):
 1. vec nr1 x \<and> vec nr2 x \<longrightarrow> nr1 = nr2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec nr1 x \<and> vec nr2 x \<longrightarrow> nr1 = nr2

goal (1 subgoal):
 1. \<forall>x\<in>set M. nr1 = nr2
[PROOF STEP]
with step3
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. x \<in> set M \<longrightarrow> vec nr1 x \<and> vec nr2 x
vec nr1 x \<and> vec nr2 x \<longrightarrow> nr1 = nr2
[PROOF STEP]
have "(\<forall>x.((x \<in> (set M)) \<longrightarrow>((nr1 = nr2))))"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> set M \<longrightarrow> vec nr1 x \<and> vec nr2 x
vec nr1 x \<and> vec nr2 x \<longrightarrow> nr1 = nr2

goal (1 subgoal):
 1. \<forall>x. x \<in> set M \<longrightarrow> nr1 = nr2
[PROOF STEP]
by (metis vec_uniqueness)
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<in> set M \<longrightarrow> nr1 = nr2

goal (1 subgoal):
 1. \<forall>x\<in>set M. nr1 = nr2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. x \<in> set M \<longrightarrow> nr1 = nr2
[PROOF STEP]
have "(\<forall>x\<in>(set M).(nr1 = nr2))"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> set M \<longrightarrow> nr1 = nr2

goal (1 subgoal):
 1. \<forall>x\<in>set M. nr1 = nr2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set M. nr1 = nr2

goal (1 subgoal):
 1. \<forall>x\<in>set M. nr1 = nr2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set M. nr1 = nr2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set M. nr1 = nr2

goal (1 subgoal):
 1. \<forall>x\<in>set M. nr1 = nr2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set M. nr1 = nr2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mat_empty_row_length: assumes "mat nr nc M" and "M = []"
shows "mat 0 nc M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat 0 nc M
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat 0 nc M
[PROOF STEP]
have "set M = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set M = {}
[PROOF STEP]
using mat_def assms  empty_set
[PROOF STATE]
proof (prove)
using this:
mat ?nr ?nc ?m = (length ?m = ?nc \<and> Ball (set ?m) (vec ?nr))
mat nr nc M
M = []
{} = set []

goal (1 subgoal):
 1. set M = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set M = {}

goal (1 subgoal):
 1. mat 0 nc M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set M = {}
[PROOF STEP]
have "Ball (set M) (vec 0)"
[PROOF STATE]
proof (prove)
using this:
set M = {}

goal (1 subgoal):
 1. Ball (set M) (vec 0)
[PROOF STEP]
using Ball_def
[PROOF STATE]
proof (prove)
using this:
set M = {}
Ball ?A ?P = (\<forall>x. x \<in> ?A \<longrightarrow> ?P x)

goal (1 subgoal):
 1. Ball (set M) (vec 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ball (set M) (vec 0)

goal (1 subgoal):
 1. mat 0 nc M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ball (set M) (vec 0)
[PROOF STEP]
have "mat 0 nc M"
[PROOF STATE]
proof (prove)
using this:
Ball (set M) (vec 0)

goal (1 subgoal):
 1. mat 0 nc M
[PROOF STEP]
using mat_def assms(1) assms(2) gen_length_code(1) length_code
[PROOF STATE]
proof (prove)
using this:
Ball (set M) (vec 0)
mat ?nr ?nc ?m = (length ?m = ?nc \<and> Ball (set ?m) (vec ?nr))
mat nr nc M
M = []
List.gen_length ?n [] = ?n
length = List.gen_length 0

goal (1 subgoal):
 1. mat 0 nc M
[PROOF STEP]
by (metis (full_types) )
[PROOF STATE]
proof (state)
this:
mat 0 nc M

goal (1 subgoal):
 1. mat 0 nc M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat 0 nc M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mat 0 nc M

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma null_mat:"null_matrix = [[]]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. null_matrix = null_matrix
[PROOF STEP]
by auto


[STATEMENT]
lemma zero_matrix:" mat 0 0 []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat 0 0 []
[PROOF STEP]
using mat_def in_set_insert insert_Nil list.size(3) not_Cons_self2
[PROOF STATE]
proof (prove)
using this:
mat ?nr ?nc ?m = (length ?m = ?nc \<and> Ball (set ?m) (vec ?nr))
?x \<in> set ?xs \<Longrightarrow> List.insert ?x ?xs = ?xs
List.insert ?x [] = [?x]
length [] = 0
?x # ?xs \<noteq> ?xs

goal (1 subgoal):
 1. mat 0 0 []
[PROOF STEP]
by (metis (full_types))


[STATEMENT]
lemma row_length_Nil:
 "row_length [] =0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_length [] = 0
[PROOF STEP]
using row_length_def
[PROOF STATE]
proof (prove)
using this:
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)

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


[STATEMENT]
lemma row_length_Null:
 "row_length [[]] =0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_length null_matrix = 0
[PROOF STEP]
using row_length_def
[PROOF STATE]
proof (prove)
using this:
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)

goal (1 subgoal):
 1. row_length null_matrix = 0
[PROOF STEP]
by auto


[STATEMENT]
lemma row_length_vect_mat:
 "row_length (vec_mat_Tensor v m)  = length v*(row_length m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_length (vec_mat_Tensor v m) = length v * row_length m
[PROOF STEP]
proof(induct m)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. row_length (vec_mat_Tensor v []) = length v * row_length []
 2. \<And>a m. row_length (vec_mat_Tensor v m) = length v * row_length m \<Longrightarrow> row_length (vec_mat_Tensor v (a # m)) = length v * row_length (a # m)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. row_length (vec_mat_Tensor v []) = length v * row_length []
 2. \<And>a m. row_length (vec_mat_Tensor v m) = length v * row_length m \<Longrightarrow> row_length (vec_mat_Tensor v (a # m)) = length v * row_length (a # m)
[PROOF STEP]
have "row_length [] = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_length [] = 0
[PROOF STEP]
using row_length_Nil
[PROOF STATE]
proof (prove)
using this:
row_length [] = 0

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

goal (2 subgoals):
 1. row_length (vec_mat_Tensor v []) = length v * row_length []
 2. \<And>a m. row_length (vec_mat_Tensor v m) = length v * row_length m \<Longrightarrow> row_length (vec_mat_Tensor v (a # m)) = length v * row_length (a # m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
row_length [] = 0

goal (2 subgoals):
 1. row_length (vec_mat_Tensor v []) = length v * row_length []
 2. \<And>a m. row_length (vec_mat_Tensor v m) = length v * row_length m \<Longrightarrow> row_length (vec_mat_Tensor v (a # m)) = length v * row_length (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)
[PROOF STATE]
proof (prove)
using this:
vec_mat_Tensor ?xs [] = []

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

goal (2 subgoals):
 1. row_length (vec_mat_Tensor v []) = length v * row_length []
 2. \<And>a m. row_length (vec_mat_Tensor v m) = length v * row_length m \<Longrightarrow> row_length (vec_mat_Tensor v (a # m)) = length v * row_length (a # m)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
row_length [] = 0
vec_mat_Tensor v [] = []
[PROOF STEP]
have
   "row_length (vec_mat_Tensor v [])  = length v*(row_length [])"
[PROOF STATE]
proof (prove)
using this:
row_length [] = 0
vec_mat_Tensor v [] = []

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

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

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

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

goal (1 subgoal):
 1. \<And>a m. row_length (vec_mat_Tensor v m) = length v * row_length m \<Longrightarrow> row_length (vec_mat_Tensor v (a # m)) = length v * row_length (a # m)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a m. row_length (vec_mat_Tensor v m) = length v * row_length m \<Longrightarrow> row_length (vec_mat_Tensor v (a # m)) = length v * row_length (a # m)
[PROOF STEP]
fix a m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a m. row_length (vec_mat_Tensor v m) = length v * row_length m \<Longrightarrow> row_length (vec_mat_Tensor v (a # m)) = length v * row_length (a # m)
[PROOF STEP]
assume A:"row_length (vec_mat_Tensor v m) = length v * row_length m"
[PROOF STATE]
proof (state)
this:
row_length (vec_mat_Tensor v m) = length v * row_length m

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

goal (1 subgoal):
 1. \<And>a m. row_length (vec_mat_Tensor v m) = length v * row_length m \<Longrightarrow> row_length (vec_mat_Tensor v (a # m)) = length v * row_length (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_def vec_mat_Tensor.simps(2)
[PROOF STATE]
proof (prove)
using this:
vec_mat_Tensor \<equiv> \<lambda>uu uua. rec_list (\<lambda>xs. []) (\<lambda>ys yss yssa xs. vec_vec_Tensor xs ys # yssa xs) uua uu
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>a m. row_length (vec_mat_Tensor v m) = length v * row_length m \<Longrightarrow> row_length (vec_mat_Tensor v (a # m)) = length v * row_length (a # m)
[PROOF STEP]
from this
[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
       "row_length (vec_mat_Tensor v (a#m)) = length (vec_vec_Tensor v a)"
[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. row_length (vec_mat_Tensor v (a # m)) = length (vec_vec_Tensor v a)
[PROOF STEP]
using row_length_def   list.distinct(1)  vec_mat_Tensor.simps(2)
[PROOF STATE]
proof (prove)
using this:
vec_mat_Tensor v (a # m) = vec_vec_Tensor v a # vec_mat_Tensor v m
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)
[] \<noteq> ?x21.0 # ?x22.0
vec_mat_Tensor ?xs (?ys # ?yss) = vec_vec_Tensor ?xs ?ys # vec_mat_Tensor ?xs ?yss

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

goal (1 subgoal):
 1. \<And>a m. row_length (vec_mat_Tensor v m) = length v * row_length m \<Longrightarrow> row_length (vec_mat_Tensor v (a # m)) = length v * row_length (a # m)
[PROOF STEP]
from this and vec_vec_Tensor_length
[PROOF STATE]
proof (chain)
picking this:
row_length (vec_mat_Tensor v (a # m)) = length (vec_vec_Tensor v a)
length (vec_vec_Tensor ?x ?y) = length ?x * length ?y
[PROOF STEP]
have
          "row_length (vec_mat_Tensor v (a#m)) = (length v)*(length a)"
[PROOF STATE]
proof (prove)
using this:
row_length (vec_mat_Tensor v (a # m)) = length (vec_vec_Tensor v a)
length (vec_vec_Tensor ?x ?y) = length ?x * length ?y

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

goal (1 subgoal):
 1. \<And>a m. row_length (vec_mat_Tensor v m) = length v * row_length m \<Longrightarrow> row_length (vec_mat_Tensor v (a # m)) = length v * row_length (a # m)
[PROOF STEP]
from this and A
[PROOF STATE]
proof (chain)
picking this:
row_length (vec_mat_Tensor v (a # m)) = length v * length a
row_length (a # m) = length a
[PROOF STEP]
have
         "row_length (vec_mat_Tensor v (a#m)) = (length v)*(row_length (a#m))"
[PROOF STATE]
proof (prove)
using this:
row_length (vec_mat_Tensor v (a # m)) = length v * length a
row_length (a # m) = length a

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

goal (1 subgoal):
 1. \<And>a m. row_length (vec_mat_Tensor v m) = length v * row_length m \<Longrightarrow> row_length (vec_mat_Tensor v (a # m)) = length v * row_length (a # m)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
row_length (vec_mat_Tensor v (a # m)) = length v * row_length (a # m)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
row_length (vec_mat_Tensor v (a # m)) = length v * row_length (a # m)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Tensor_null: "xs \<otimes>[] = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<otimes> [] = []
[PROOF STEP]
by(induction xs)(auto)


[STATEMENT]
lemma Tensor_left_id: "  [[id]] \<otimes> xs = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [[id]] \<otimes> xs = xs
[PROOF STEP]
by(induction xs)(auto simp add:times_scalar_id)


[STATEMENT]
lemma Tensor_right_id: "  xs \<otimes> [[id]] = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<otimes> [[id]] = xs
[PROOF STEP]
by(induction xs)(auto simp add: vec_vec_Tensor_right_id)


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

goal (2 subgoals):
 1. row_length ([] \<otimes> m2) = row_length [] * row_length m2
 2. \<And>a m1. row_length (m1 \<otimes> m2) = row_length m1 * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2
[PROOF STEP]
have "row_length ([]\<otimes>m2) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_length ([] \<otimes> m2) = 0
[PROOF STEP]
using Tensor.simps(1) row_length_def
[PROOF STATE]
proof (prove)
using this:
[] \<otimes> ?xs = []
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)

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

goal (2 subgoals):
 1. row_length ([] \<otimes> m2) = row_length [] * row_length m2
 2. \<And>a m1. row_length (m1 \<otimes> m2) = row_length m1 * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
row_length ([] \<otimes> m2) = 0
[PROOF STEP]
have "row_length ([]\<otimes>m2) = (row_length [])*(row_length m2)"
[PROOF STATE]
proof (prove)
using this:
row_length ([] \<otimes> m2) = 0

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

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

goal (2 subgoals):
 1. row_length ([] \<otimes> m2) = row_length [] * row_length m2
 2. \<And>a m1. row_length (m1 \<otimes> m2) = row_length m1 * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
row_length ([] \<otimes> m2) = row_length [] * row_length m2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
row_length ([] \<otimes> m2) = row_length [] * row_length m2

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

goal (1 subgoal):
 1. \<And>a m1. row_length (m1 \<otimes> m2) = row_length m1 * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a m1. row_length (m1 \<otimes> m2) = row_length m1 * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2
[PROOF STEP]
fix a m1
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a m1. row_length (m1 \<otimes> m2) = row_length m1 * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2
[PROOF STEP]
assume "row_length (m1 \<otimes> m2) = row_length m1 * row_length m2"
[PROOF STATE]
proof (state)
this:
row_length (m1 \<otimes> m2) = row_length m1 * row_length m2

goal (1 subgoal):
 1. \<And>a m1. row_length (m1 \<otimes> m2) = row_length m1 * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2
[PROOF STEP]
let ?case =
    "row_length ((a # m1) \<otimes> m2) = row_length (a # m1) * row_length m2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a m1. row_length (m1 \<otimes> m2) = row_length m1 * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2
[PROOF STEP]
have B: "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. row_length (m1 \<otimes> m2) = row_length m1 * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2
[PROOF STEP]
have "row_length ((a # m1) \<otimes> m2) = row_length (a # m1) * row_length m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2
[PROOF STEP]
proof(induct m2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. row_length (a # m1 \<otimes> []) = row_length (a # m1) * row_length []
 2. \<And>aa m2. row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> aa # m2) = row_length (a # m1) * row_length (aa # m2)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. row_length (a # m1 \<otimes> []) = row_length (a # m1) * row_length []
 2. \<And>aa m2. row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> aa # m2) = row_length (a # m1) * row_length (aa # m2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_length (a # m1 \<otimes> []) = row_length (a # m1) * row_length []
[PROOF STEP]
using Tensor_null row_length_def  mult_0_right
[PROOF STATE]
proof (prove)
using this:
?xs \<otimes> [] = []
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)
?m * 0 = 0

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

goal (1 subgoal):
 1. \<And>aa m2. row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> aa # m2) = row_length (a # m1) * row_length (aa # m2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa m2. row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> aa # m2) = row_length (a # m1) * row_length (aa # m2)
[PROOF STEP]
fix aa m2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa m2. row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> aa # m2) = row_length (a # m1) * row_length (aa # m2)
[PROOF STEP]
assume "row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2"
[PROOF STATE]
proof (state)
this:
row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2

goal (1 subgoal):
 1. \<And>aa m2. row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> aa # m2) = row_length (a # m1) * row_length (aa # m2)
[PROOF STEP]
let ?case=
      "row_length (a # m1 \<otimes> aa # m2)
                  = row_length (a # m1) * row_length (aa # m2)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa m2. row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> aa # m2) = row_length (a # m1) * row_length (aa # m2)
[PROOF STEP]
have "aa#m2 \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aa # m2 \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
aa # m2 \<noteq> []

goal (1 subgoal):
 1. \<And>aa m2. row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> aa # m2) = row_length (a # m1) * row_length (aa # m2)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
aa # m2 \<noteq> []
[PROOF STEP]
have non_zero:"(vec_mat_Tensor a (aa#m2)) \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
aa # m2 \<noteq> []

goal (1 subgoal):
 1. vec_mat_Tensor a (aa # m2) \<noteq> []
[PROOF STEP]
using vec_mat_Tensor_def
[PROOF STATE]
proof (prove)
using this:
aa # m2 \<noteq> []
vec_mat_Tensor \<equiv> \<lambda>uu uua. rec_list (\<lambda>xs. []) (\<lambda>ys yss yssa xs. vec_vec_Tensor xs ys # yssa xs) uua uu

goal (1 subgoal):
 1. vec_mat_Tensor a (aa # m2) \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec_mat_Tensor a (aa # m2) \<noteq> []

goal (1 subgoal):
 1. \<And>aa m2. row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> aa # m2) = row_length (a # m1) * row_length (aa # m2)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
vec_mat_Tensor a (aa # m2) \<noteq> []
[PROOF STEP]
have
            "hd ((vec_mat_Tensor a (aa#m2))@(m1\<otimes>m2))
                  = hd (vec_mat_Tensor a (aa#m2))"
[PROOF STATE]
proof (prove)
using this:
vec_mat_Tensor a (aa # m2) \<noteq> []

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

goal (1 subgoal):
 1. \<And>aa m2. row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> aa # m2) = row_length (a # m1) * row_length (aa # m2)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
hd (vec_mat_Tensor a (aa # m2) @ (m1 \<otimes> m2)) = hd (vec_mat_Tensor a (aa # m2))
[PROOF STEP]
have
            "hd ((a#m1)\<otimes>(aa#m2)) = hd (vec_mat_Tensor a (aa#m2))"
[PROOF STATE]
proof (prove)
using this:
hd (vec_mat_Tensor a (aa # m2) @ (m1 \<otimes> m2)) = hd (vec_mat_Tensor a (aa # m2))

goal (1 subgoal):
 1. hd (a # m1 \<otimes> aa # m2) = hd (vec_mat_Tensor a (aa # m2))
[PROOF STEP]
using Tensor.simps(2)
[PROOF STATE]
proof (prove)
using this:
hd (vec_mat_Tensor a (aa # m2) @ (m1 \<otimes> m2)) = hd (vec_mat_Tensor a (aa # m2))
?x # ?xs \<otimes> ?ys = vec_mat_Tensor ?x ?ys @ (?xs \<otimes> ?ys)

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

goal (1 subgoal):
 1. \<And>aa m2. row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> aa # m2) = row_length (a # m1) * row_length (aa # m2)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
hd (a # m1 \<otimes> aa # m2) = hd (vec_mat_Tensor a (aa # m2))
[PROOF STEP]
have s1: "row_length ((a#m1)\<otimes>(aa#m2))
                       = row_length (vec_mat_Tensor a (aa#m2))"
[PROOF STATE]
proof (prove)
using this:
hd (a # m1 \<otimes> aa # m2) = hd (vec_mat_Tensor a (aa # m2))

goal (1 subgoal):
 1. row_length (a # m1 \<otimes> aa # m2) = row_length (vec_mat_Tensor a (aa # m2))
[PROOF STEP]
using row_length_def  Nil_is_append_conv non_zero Tensor.simps(2)
[PROOF STATE]
proof (prove)
using this:
hd (a # m1 \<otimes> aa # m2) = hd (vec_mat_Tensor a (aa # m2))
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)
([] = ?xs @ ?ys) = (?xs = [] \<and> ?ys = [])
vec_mat_Tensor a (aa # m2) \<noteq> []
?x # ?xs \<otimes> ?ys = vec_mat_Tensor ?x ?ys @ (?xs \<otimes> ?ys)

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

goal (1 subgoal):
 1. \<And>aa m2. row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> aa # m2) = row_length (a # m1) * row_length (aa # m2)
[PROOF STEP]
have "row_length (vec_mat_Tensor a (aa#m2))
                    = (length a)*row_length(aa#m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_length (vec_mat_Tensor a (aa # m2)) = length a * row_length (aa # m2)
[PROOF STEP]
using row_length_vect_mat
[PROOF STATE]
proof (prove)
using this:
row_length (vec_mat_Tensor ?v ?m) = length ?v * row_length ?m

goal (1 subgoal):
 1. row_length (vec_mat_Tensor a (aa # m2)) = length a * row_length (aa # m2)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
row_length (vec_mat_Tensor a (aa # m2)) = length a * row_length (aa # m2)

goal (1 subgoal):
 1. \<And>aa m2. row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> aa # m2) = row_length (a # m1) * row_length (aa # m2)
[PROOF STEP]
from this and s1
[PROOF STATE]
proof (chain)
picking this:
row_length (vec_mat_Tensor a (aa # m2)) = length a * row_length (aa # m2)
row_length (a # m1 \<otimes> aa # m2) = row_length (vec_mat_Tensor a (aa # m2))
[PROOF STEP]
have "row_length (vec_mat_Tensor a (aa#m2))
                             = (length a)*row_length(aa#m2)"
[PROOF STATE]
proof (prove)
using this:
row_length (vec_mat_Tensor a (aa # m2)) = length a * row_length (aa # m2)
row_length (a # m1 \<otimes> aa # m2) = row_length (vec_mat_Tensor a (aa # m2))

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

goal (1 subgoal):
 1. \<And>aa m2. row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> aa # m2) = row_length (a # m1) * row_length (aa # m2)
[PROOF STEP]
from this and B
[PROOF STATE]
proof (chain)
picking this:
row_length (vec_mat_Tensor a (aa # m2)) = length a * row_length (aa # m2)
row_length (a # m1) = length a
[PROOF STEP]
have "row_length (vec_mat_Tensor a (aa#m2))
                           = (row_length (a#m1))*row_length(aa#m2)"
[PROOF STATE]
proof (prove)
using this:
row_length (vec_mat_Tensor a (aa # m2)) = length a * row_length (aa # m2)
row_length (a # m1) = length a

goal (1 subgoal):
 1. row_length (vec_mat_Tensor a (aa # m2)) = row_length (a # m1) * row_length (aa # m2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row_length (vec_mat_Tensor a (aa # m2)) = row_length (a # m1) * row_length (aa # m2)

goal (1 subgoal):
 1. \<And>aa m2. row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> aa # m2) = row_length (a # m1) * row_length (aa # m2)
[PROOF STEP]
from this  and s1
[PROOF STATE]
proof (chain)
picking this:
row_length (vec_mat_Tensor a (aa # m2)) = row_length (a # m1) * row_length (aa # m2)
row_length (a # m1 \<otimes> aa # m2) = row_length (vec_mat_Tensor a (aa # m2))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
row_length (vec_mat_Tensor a (aa # m2)) = row_length (a # m1) * row_length (aa # m2)
row_length (a # m1 \<otimes> aa # m2) = row_length (vec_mat_Tensor a (aa # m2))

goal (1 subgoal):
 1. row_length (a # m1 \<otimes> aa # m2) = row_length (a # m1) * row_length (aa # m2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row_length (a # m1 \<otimes> aa # m2) = row_length (a # m1) * row_length (aa # m2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2

goal (1 subgoal):
 1. \<And>a m1. row_length (m1 \<otimes> m2) = row_length m1 * row_length m2 \<Longrightarrow> row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
row_length (a # m1 \<otimes> m2) = row_length (a # m1) * row_length m2

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

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (2 subgoals):
 1. M = [] \<Longrightarrow> mat (row_length M) (length M) M
 2. \<And>a list. M = a # list \<Longrightarrow> mat (row_length M) (length M) M
[PROOF STEP]
have "row_length M= 0 "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_length M = 0
[PROOF STEP]
using row_length_def
[PROOF STATE]
proof (prove)
using this:
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)

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

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

goal (2 subgoals):
 1. M = [] \<Longrightarrow> mat (row_length M) (length M) M
 2. \<And>a list. M = a # list \<Longrightarrow> mat (row_length M) (length M) M
[PROOF STEP]
have "length M = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length M = 0
[PROOF STEP]
by (metis Nil list.size(3))
[PROOF STATE]
proof (state)
this:
length M = 0

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

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

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

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

goal (1 subgoal):
 1. mat (row_length M) (length M) M
[PROOF STEP]
using mat_empty_row_length row_length_def mat_def
[PROOF STATE]
proof (prove)
using this:
row_length M = 0
length M = 0
mat 0 0 M
\<lbrakk>mat ?nr ?nc ?M; ?M = []\<rbrakk> \<Longrightarrow> mat 0 ?nc ?M
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)
mat ?nr ?nc ?m = (length ?m = ?nc \<and> Ball (set ?m) (vec ?nr))

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

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

goal (1 subgoal):
 1. \<And>a list. M = a # list \<Longrightarrow> mat (row_length M) (length M) M
[PROOF STEP]
have 1: "mat nr nc (a#N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat nr nc (a # N)
[PROOF STEP]
using assms Cons
[PROOF STATE]
proof (prove)
using this:
mat nr nc M
M = a # N

goal (1 subgoal):
 1. mat nr nc (a # N)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat nr nc (a # N)

goal (1 subgoal):
 1. \<And>a list. M = a # list \<Longrightarrow> mat (row_length M) (length M) M
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
mat nr nc (a # N)
[PROOF STEP]
have "(x \<in> set (a #N)) \<longrightarrow> (x = a) \<or> (x \<in> (set N))"
[PROOF STATE]
proof (prove)
using this:
mat nr nc (a # N)

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

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

goal (1 subgoal):
 1. \<And>a list. M = a # list \<Longrightarrow> mat (row_length M) (length M) M
[PROOF STEP]
from this and 1
[PROOF STATE]
proof (chain)
picking this:
x \<in> set (a # N) \<longrightarrow> x = a \<or> x \<in> set N
mat nr nc (a # N)
[PROOF STEP]
have 2:"vec nr a"
[PROOF STATE]
proof (prove)
using this:
x \<in> set (a # N) \<longrightarrow> x = a \<or> x \<in> set N
mat nr nc (a # N)

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

goal (1 subgoal):
 1. vec nr a
[PROOF STEP]
by (metis Ball_set_list_all list_all_simps(1))
[PROOF STATE]
proof (state)
this:
vec nr a

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

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

goal (1 subgoal):
 1. \<And>a list. M = a # list \<Longrightarrow> mat (row_length M) (length M) M
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
row_length (a # N) = length a
[PROOF STEP]
have " vec (row_length (a#N)) a"
[PROOF STATE]
proof (prove)
using this:
row_length (a # N) = length a

goal (1 subgoal):
 1. vec (row_length (a # N)) a
[PROOF STEP]
using vec_def
[PROOF STATE]
proof (prove)
using this:
row_length (a # N) = length a
vec ?n ?x = (length ?x = ?n)

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

goal (1 subgoal):
 1. \<And>a list. M = a # list \<Longrightarrow> mat (row_length M) (length M) M
[PROOF STEP]
from this and 2
[PROOF STATE]
proof (chain)
picking this:
vec (row_length (a # N)) a
vec nr a
[PROOF STEP]
have 3:"(row_length M)  = nr"
[PROOF STATE]
proof (prove)
using this:
vec (row_length (a # N)) a
vec nr a

goal (1 subgoal):
 1. row_length M = nr
[PROOF STEP]
using vec_uniqueness Cons
[PROOF STATE]
proof (prove)
using this:
vec (row_length (a # N)) a
vec nr a
\<lbrakk>vec ?m ?v; vec ?n ?v\<rbrakk> \<Longrightarrow> ?m = ?n
M = a # N

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

goal (1 subgoal):
 1. \<And>a list. M = a # list \<Longrightarrow> mat (row_length M) (length M) M
[PROOF STEP]
have " nc = (length M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nc = length M
[PROOF STEP]
using 1 and mat_def and assms
[PROOF STATE]
proof (prove)
using this:
mat nr nc (a # N)
mat ?nr ?nc ?m = (length ?m = ?nc \<and> Ball (set ?m) (vec ?nr))
mat nr nc M

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

goal (1 subgoal):
 1. \<And>a list. M = a # list \<Longrightarrow> mat (row_length M) (length M) M
[PROOF STEP]
with 3
[PROOF STATE]
proof (chain)
picking this:
row_length M = nr
nc = length M
[PROOF STEP]
have "mat (row_length M) (length M) M"
[PROOF STATE]
proof (prove)
using this:
row_length M = nr
nc = length M

goal (1 subgoal):
 1. mat (row_length M) (length M) M
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
row_length M = nr
nc = length M
mat nr nc M

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

goal (1 subgoal):
 1. \<And>a list. M = a # list \<Longrightarrow> mat (row_length M) (length M) M
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
mat (row_length M) (length M) M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
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:
No subgoals!
[PROOF STEP]
qed


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

goal (2 subgoals):
 1. M = [] \<Longrightarrow> mat (row_length M) (length M) M
 2. \<And>a list. M = a # list \<Longrightarrow> mat (row_length M) (length M) M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length M) (length M) M
[PROOF STEP]
using row_length_def zero_matrix Nil  list.size(3)
[PROOF STATE]
proof (prove)
using this:
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)
mat 0 0 []
M = []
length [] = 0

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

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

goal (1 subgoal):
 1. \<And>a list. M = a # list \<Longrightarrow> mat (row_length M) (length M) M
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. M = a # list \<Longrightarrow> mat (row_length M) (length M) M
[PROOF STEP]
have 1: "b \<in> (set M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<in> set M
[PROOF STEP]
using set_def  Cons ListMem_iff elem
[PROOF STATE]
proof (prove)
using this:
set \<equiv> ctor_fold_list (\<lambda>z. set1_pre_list z \<union> \<Union> (set2_pre_list z))
M = b # N
ListMem ?x ?xs = (?x \<in> set ?xs)
ListMem ?x (?x # ?xs)

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>a list. M = a # list \<Longrightarrow> mat (row_length M) (length M) 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 assms
[PROOF STATE]
proof (prove)
using this:
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>a list. M = a # list \<Longrightarrow> mat (row_length M) (length M) 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> ((x = a) \<or> (x \<in> set M))"
[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> 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>a list. M = a # list \<Longrightarrow> mat (row_length M) (length M) M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set (a # M) \<longrightarrow> x = a \<or> x \<in> set M
[PROOF STEP]
have " (x \<in> (set (a#M))) \<longrightarrow> (vec (row_length (a#M)) x)"
[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> vec (row_length (a # M)) x
[PROOF STEP]
using mat_def Ball_def assms
[PROOF STATE]
proof (prove)
using this:
x \<in> set (a # M) \<longrightarrow> x = a \<or> x \<in> set 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)
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]
by metis
[PROOF STATE]
proof (state)
this:
x \<in> set (a # M) \<longrightarrow> vec (row_length (a # M)) x

goal (1 subgoal):
 1. \<And>a list. M = a # list \<Longrightarrow> mat (row_length M) (length M) 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>a list. M = a # list \<Longrightarrow> mat (row_length M) (length M) M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set (a # M) \<longrightarrow> vec (length a) x
[PROOF STEP]
have 2:"x \<in> (set M) \<longrightarrow> (vec (length a) x)"
[PROOF STATE]
proof (prove)
using this:
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>a list. M = a # list \<Longrightarrow> mat (row_length M) (length M) M
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
b \<in> set M
x \<in> set M \<longrightarrow> vec (length a) x
[PROOF STEP]
have 3:"(vec (length a) b)"
[PROOF STATE]
proof (prove)
using this:
b \<in> set M
x \<in> set M \<longrightarrow> vec (length a) x

goal (1 subgoal):
 1. vec (length a) b
[PROOF STEP]
using assms in_set_member mat_def member_rec(1) vec_def
[PROOF STATE]
proof (prove)
using this:
b \<in> set M
x \<in> set M \<longrightarrow> vec (length a) x
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>a list. M = a # list \<Longrightarrow> mat (row_length M) (length M) M
[PROOF STEP]
have 5: "(vec (length b) b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec (length b) b
[PROOF STEP]
using vec_def
[PROOF STATE]
proof (prove)
using this:
vec ?n ?x = (length ?x = ?n)

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

goal (1 subgoal):
 1. \<And>a list. M = a # list \<Longrightarrow> mat (row_length M) (length M) M
[PROOF STEP]
with 3
[PROOF STATE]
proof (chain)
picking this:
vec (length a) b
vec (length b) b
[PROOF STEP]
have "(length a) = (length b)"
[PROOF STATE]
proof (prove)
using this:
vec (length a) b
vec (length b) b

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<forall>x. x \<in> set M \<longrightarrow> vec (row_length M) x
[PROOF STEP]
using Cons 5 6 assms in_set_member mat_def member_rec(1)
         vec_uniqueness
[PROOF STATE]
proof (prove)
using this:
x \<in> set M \<longrightarrow> vec (row_length M) x
M = b # N
vec (length b) b
row_length M = length b
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)
\<lbrakk>vec ?m ?v; vec ?n ?v\<rbrakk> \<Longrightarrow> ?m = ?n

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>a list. M = a # list \<Longrightarrow> mat (row_length M) (length M) M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat (row_length M) (length M) M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
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:
No subgoals!
[PROOF STEP]
qed