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

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


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

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


[STATEMENT]
lemma div_left_ineq:
 assumes "(x::nat) < y*z"
 shows " (x div z) < y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x div z < y
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x div z < y \<Longrightarrow> False
[PROOF STEP]
assume 0: " \<not>((x div z) < y)"
[PROOF STATE]
proof (state)
this:
\<not> x div z < y

goal (1 subgoal):
 1. \<not> x div z < y \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> x div z < y
[PROOF STEP]
have 1:" x div z \<ge> y"
[PROOF STATE]
proof (prove)
using this:
\<not> x div z < y

goal (1 subgoal):
 1. y \<le> x div z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<le> x div z

goal (1 subgoal):
 1. \<not> x div z < y \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<le> x div z
[PROOF STEP]
have 2:"(x div z)*z \<ge> y*z"
[PROOF STATE]
proof (prove)
using this:
y \<le> x div z

goal (1 subgoal):
 1. y * z \<le> x div z * z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y * z \<le> x div z * z

goal (1 subgoal):
 1. \<not> x div z < y \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y * z \<le> x div z * z
[PROOF STEP]
have 3:"(x div z)*z + (x mod z) = z"
[PROOF STATE]
proof (prove)
using this:
y * z \<le> x div z * z

goal (1 subgoal):
 1. x div z * z + x mod z = z
[PROOF STEP]
using div_mult_mod_eq
          add_leD1 assms minus_mod_eq_div_mult [symmetric] le_diff_conv2 mod_less_eq_dividend not_less
[PROOF STATE]
proof (prove)
using this:
y * z \<le> x div z * z
?a div ?b * ?b + ?a mod ?b = ?a
?m + ?k \<le> ?n \<Longrightarrow> ?m \<le> ?n
x < y * z
?a div ?b * ?b = ?a - ?a mod ?b
?k \<le> ?j \<Longrightarrow> (?i \<le> ?j - ?k) = (?i + ?k \<le> ?j)
?m mod ?n \<le> ?m
(\<not> ?x < ?y) = (?y \<le> ?x)

goal (1 subgoal):
 1. x div z * z + x mod z = z
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
x div z * z + x mod z = z

goal (1 subgoal):
 1. \<not> x div z < y \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x div z * z + x mod z = z
[PROOF STEP]
have 4:"(x div z)*z \<le> z"
[PROOF STATE]
proof (prove)
using this:
x div z * z + x mod z = z

goal (1 subgoal):
 1. x div z * z \<le> z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x div z * z \<le> z

goal (1 subgoal):
 1. \<not> x div z < y \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x div z * z \<le> z
[PROOF STEP]
have 5:"z \<ge> y*z"
[PROOF STATE]
proof (prove)
using this:
x div z * z \<le> z

goal (1 subgoal):
 1. y * z \<le> z
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
x div z * z \<le> z
y * z \<le> x div z * z

goal (1 subgoal):
 1. y * z \<le> z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y * z \<le> z

goal (1 subgoal):
 1. \<not> x div z < y \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y * z \<le> z
[PROOF STEP]
have 6:"z div z \<ge> (y*z) div z"
[PROOF STATE]
proof (prove)
using this:
y * z \<le> z

goal (1 subgoal):
 1. y * z div z \<le> z div z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y * z div z \<le> z div z

goal (1 subgoal):
 1. \<not> x div z < y \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y * z div z \<le> z div z
[PROOF STEP]
have "(y*z) div z \<le> 1"
[PROOF STATE]
proof (prove)
using this:
y * z div z \<le> z div z

goal (1 subgoal):
 1. y * z div z \<le> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y * z div z \<le> 1

goal (1 subgoal):
 1. \<not> x div z < y \<Longrightarrow> False
[PROOF STEP]
with 6
[PROOF STATE]
proof (chain)
picking this:
y * z div z \<le> z div z
y * z div z \<le> 1
[PROOF STEP]
have "1 \<ge> y"
[PROOF STATE]
proof (prove)
using this:
y * z div z \<le> z div z
y * z div z \<le> 1

goal (1 subgoal):
 1. y \<le> 1
[PROOF STEP]
using 1 3 assms div_self less_nat_zero_code mult_zero_left
          mult.commute mod_div_mult_eq
[PROOF STATE]
proof (prove)
using this:
y * z div z \<le> z div z
y * z div z \<le> 1
y \<le> x div z
x div z * z + x mod z = z
x < y * z
?a \<noteq> (0::?'a) \<Longrightarrow> ?a div ?a = (1::?'a)
(?n < 0) = False
(0::?'a) * ?a = (0::?'a)
?a * ?b = ?b * ?a
?a mod ?b + ?a div ?b * ?b = ?a

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

goal (1 subgoal):
 1. \<not> x div z < y \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<le> 1
[PROOF STEP]
have 7:"(y = 0) \<or> (y = 1)"
[PROOF STATE]
proof (prove)
using this:
y \<le> 1

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

goal (1 subgoal):
 1. \<not> x div z < y \<Longrightarrow> False
[PROOF STEP]
have "(y = 0 ) \<Longrightarrow> x<0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = 0 \<Longrightarrow> x < 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x < y * z

goal (1 subgoal):
 1. y = 0 \<Longrightarrow> x < 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y = 0 \<Longrightarrow> x < 0

goal (1 subgoal):
 1. \<not> x div z < y \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y = 0 \<Longrightarrow> x < 0

goal (1 subgoal):
 1. \<not> x div z < y \<Longrightarrow> False
[PROOF STEP]
have "x \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> x

goal (1 subgoal):
 1. \<not> x div z < y \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<le> x
[PROOF STEP]
have 8:"(y = 0) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
using this:
0 \<le> x

goal (1 subgoal):
 1. y = 0 \<Longrightarrow> False
[PROOF STEP]
using calculation  less_nat_zero_code
[PROOF STATE]
proof (prove)
using this:
0 \<le> x
y = 0 \<Longrightarrow> x < 0
(?n < 0) = False

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

goal (1 subgoal):
 1. \<not> x div z < y \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y = 0 \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> x div z < y \<Longrightarrow> False
[PROOF STEP]
have "(y = 1) \<Longrightarrow> ( x < z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = 1 \<Longrightarrow> x < z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x < y * z

goal (1 subgoal):
 1. y = 1 \<Longrightarrow> x < z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y = 1 \<Longrightarrow> x < z

goal (1 subgoal):
 1. \<not> x div z < y \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y = 1 \<Longrightarrow> x < z
[PROOF STEP]
have "(y = 1) \<Longrightarrow> (x div z) = 0"
[PROOF STATE]
proof (prove)
using this:
y = 1 \<Longrightarrow> x < z

goal (1 subgoal):
 1. y = 1 \<Longrightarrow> x div z = 0
[PROOF STEP]
by (metis div_less)
[PROOF STATE]
proof (state)
this:
y = 1 \<Longrightarrow> x div z = 0

goal (1 subgoal):
 1. \<not> x div z < y \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y = 1 \<Longrightarrow> x div z = 0
[PROOF STEP]
have "(y = 1) \<Longrightarrow>(x div z) < y"
[PROOF STATE]
proof (prove)
using this:
y = 1 \<Longrightarrow> x div z = 0

goal (1 subgoal):
 1. y = 1 \<Longrightarrow> x div z < y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y = 1 \<Longrightarrow> x div z < y

goal (1 subgoal):
 1. \<not> x div z < y \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y = 1 \<Longrightarrow> x div z < y
[PROOF STEP]
have "(y = 1) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
using this:
y = 1 \<Longrightarrow> x div z < y

goal (1 subgoal):
 1. y = 1 \<Longrightarrow> False
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
y = 1 \<Longrightarrow> x div z < y
\<not> x div z < y

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

goal (1 subgoal):
 1. \<not> x div z < y \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y = 1 \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
y = 1 \<Longrightarrow> False

goal (1 subgoal):
 1. False
[PROOF STEP]
using 7 8
[PROOF STATE]
proof (prove)
using this:
y = 1 \<Longrightarrow> False
y = 0 \<or> y = 1
y = 0 \<Longrightarrow> False

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma div_right_ineq:
 assumes "(x::nat) < y*z"
 shows " (x div y) < z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x div y < z
[PROOF STEP]
using assms div_left_ineq mult.commute
[PROOF STATE]
proof (prove)
using this:
x < y * z
?x < ?y * ?z \<Longrightarrow> ?x div ?z < ?y
?a * ?b = ?b * ?a

goal (1 subgoal):
 1. x div y < z
[PROOF STEP]
by (metis)


[STATEMENT]
lemma col_vec_mat_Tensor_prelim:
 " \<forall>j.(j < (length M)
     \<longrightarrow>
      col (vec_mat_Tensor v M) j = vec_vec_Tensor v (col M j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j<length M. col (vec_mat_Tensor v M) j = vec_vec_Tensor v (col M j)
[PROOF STEP]
unfolding col_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j<length M. vec_mat_Tensor v M ! j = vec_vec_Tensor v (M ! j)
[PROOF STEP]
apply(rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. j < length M \<longrightarrow> vec_mat_Tensor v M ! j = vec_vec_Tensor v (M ! j)
[PROOF STEP]
proof(induct M)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>j. j < length [] \<longrightarrow> vec_mat_Tensor v [] ! j = vec_vec_Tensor v ([] ! j)
 2. \<And>a M j. (\<And>j. j < length M \<longrightarrow> vec_mat_Tensor v M ! j = vec_vec_Tensor v (M ! j)) \<Longrightarrow> j < length (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j = vec_vec_Tensor v ((a # M) ! j)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>j. j < length [] \<longrightarrow> vec_mat_Tensor v [] ! j = vec_vec_Tensor v ([] ! j)
 2. \<And>a M j. (\<And>j. j < length M \<longrightarrow> vec_mat_Tensor v M ! j = vec_vec_Tensor v (M ! j)) \<Longrightarrow> j < length (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j = vec_vec_Tensor v ((a # M) ! j)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < length [] \<longrightarrow> vec_mat_Tensor v [] ! j = vec_vec_Tensor v ([] ! j)
[PROOF STEP]
using Nil
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < length [] \<longrightarrow> vec_mat_Tensor v [] ! j = vec_vec_Tensor v ([] ! j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < length [] \<longrightarrow> vec_mat_Tensor v [] ! j = vec_vec_Tensor v ([] ! j)

goal (1 subgoal):
 1. \<And>a M j. (\<And>j. j < length M \<longrightarrow> vec_mat_Tensor v M ! j = vec_vec_Tensor v (M ! j)) \<Longrightarrow> j < length (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j = vec_vec_Tensor v ((a # M) ! j)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a M j. (\<And>j. j < length M \<longrightarrow> vec_mat_Tensor v M ! j = vec_vec_Tensor v (M ! j)) \<Longrightarrow> j < length (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j = vec_vec_Tensor v ((a # M) ! j)
[PROOF STEP]
case (Cons w N)
[PROOF STATE]
proof (state)
this:
?j < length N \<longrightarrow> vec_mat_Tensor v N ! ?j = vec_vec_Tensor v (N ! ?j)

goal (1 subgoal):
 1. \<And>a M j. (\<And>j. j < length M \<longrightarrow> vec_mat_Tensor v M ! j = vec_vec_Tensor v (M ! j)) \<Longrightarrow> j < length (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j = vec_vec_Tensor v ((a # M) ! j)
[PROOF STEP]
have Cons_1:"vec_mat_Tensor v (w#N)
                        = (vec_vec_Tensor v w)#(vec_mat_Tensor v N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_mat_Tensor v (w # N) = vec_vec_Tensor v w # vec_mat_Tensor v N
[PROOF STEP]
using vec_mat_Tensor.simps Cons
[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
?j < length N \<longrightarrow> vec_mat_Tensor v N ! ?j = vec_vec_Tensor v (N ! ?j)

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

goal (1 subgoal):
 1. \<And>a M j. (\<And>j. j < length M \<longrightarrow> vec_mat_Tensor v M ! j = vec_vec_Tensor v (M ! j)) \<Longrightarrow> j < length (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j = vec_vec_Tensor v ((a # M) ! j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vec_mat_Tensor v (w # N) = vec_vec_Tensor v w # vec_mat_Tensor v N
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
vec_mat_Tensor v (w # N) = vec_vec_Tensor v w # vec_mat_Tensor v N

goal (1 subgoal):
 1. j < length (w # N) \<longrightarrow> vec_mat_Tensor v (w # N) ! j = vec_vec_Tensor v ((w # N) ! j)
[PROOF STEP]
proof(cases j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>vec_mat_Tensor v (w # N) = vec_vec_Tensor v w # vec_mat_Tensor v N; j = 0\<rbrakk> \<Longrightarrow> j < length (w # N) \<longrightarrow> vec_mat_Tensor v (w # N) ! j = vec_vec_Tensor v ((w # N) ! j)
 2. \<And>nat. \<lbrakk>vec_mat_Tensor v (w # N) = vec_vec_Tensor v w # vec_mat_Tensor v N; j = Suc nat\<rbrakk> \<Longrightarrow> j < length (w # N) \<longrightarrow> vec_mat_Tensor v (w # N) ! j = vec_vec_Tensor v ((w # N) ! j)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
j = 0

goal (2 subgoals):
 1. \<lbrakk>vec_mat_Tensor v (w # N) = vec_vec_Tensor v w # vec_mat_Tensor v N; j = 0\<rbrakk> \<Longrightarrow> j < length (w # N) \<longrightarrow> vec_mat_Tensor v (w # N) ! j = vec_vec_Tensor v ((w # N) ! j)
 2. \<And>nat. \<lbrakk>vec_mat_Tensor v (w # N) = vec_vec_Tensor v w # vec_mat_Tensor v N; j = Suc nat\<rbrakk> \<Longrightarrow> j < length (w # N) \<longrightarrow> vec_mat_Tensor v (w # N) ! j = vec_vec_Tensor v ((w # N) ! j)
[PROOF STEP]
have "vec_mat_Tensor v (w#N)!0 =  (vec_vec_Tensor v w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_mat_Tensor v (w # N) ! 0 = vec_vec_Tensor v w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec_mat_Tensor v (w # N) ! 0 = vec_vec_Tensor v w

goal (2 subgoals):
 1. \<lbrakk>vec_mat_Tensor v (w # N) = vec_vec_Tensor v w # vec_mat_Tensor v N; j = 0\<rbrakk> \<Longrightarrow> j < length (w # N) \<longrightarrow> vec_mat_Tensor v (w # N) ! j = vec_vec_Tensor v ((w # N) ! j)
 2. \<And>nat. \<lbrakk>vec_mat_Tensor v (w # N) = vec_vec_Tensor v w # vec_mat_Tensor v N; j = Suc nat\<rbrakk> \<Longrightarrow> j < length (w # N) \<longrightarrow> vec_mat_Tensor v (w # N) ! j = vec_vec_Tensor v ((w # N) ! j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vec_mat_Tensor v (w # N) ! 0 = vec_vec_Tensor v w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vec_mat_Tensor v (w # N) ! 0 = vec_vec_Tensor v w

goal (1 subgoal):
 1. j < length (w # N) \<longrightarrow> vec_mat_Tensor v (w # N) ! j = vec_vec_Tensor v ((w # N) ! j)
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
vec_mat_Tensor v (w # N) ! 0 = vec_vec_Tensor v w
j = 0

goal (1 subgoal):
 1. j < length (w # N) \<longrightarrow> vec_mat_Tensor v (w # N) ! j = vec_vec_Tensor v ((w # N) ! j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < length (w # N) \<longrightarrow> vec_mat_Tensor v (w # N) ! j = vec_vec_Tensor v ((w # N) ! j)

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>vec_mat_Tensor v (w # N) = vec_vec_Tensor v w # vec_mat_Tensor v N; j = Suc nat\<rbrakk> \<Longrightarrow> j < length (w # N) \<longrightarrow> vec_mat_Tensor v (w # N) ! j = vec_vec_Tensor v ((w # N) ! j)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>vec_mat_Tensor v (w # N) = vec_vec_Tensor v w # vec_mat_Tensor v N; j = Suc nat\<rbrakk> \<Longrightarrow> j < length (w # N) \<longrightarrow> vec_mat_Tensor v (w # N) ! j = vec_vec_Tensor v ((w # N) ! j)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
j = Suc k

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>vec_mat_Tensor v (w # N) = vec_vec_Tensor v w # vec_mat_Tensor v N; j = Suc nat\<rbrakk> \<Longrightarrow> j < length (w # N) \<longrightarrow> vec_mat_Tensor v (w # N) ! j = vec_vec_Tensor v ((w # N) ! j)
[PROOF STEP]
have " vec_mat_Tensor v (w#N)!j = (vec_mat_Tensor v N)!(k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_mat_Tensor v (w # N) ! j = vec_mat_Tensor v N ! k
[PROOF STEP]
using Cons_1 Suc
[PROOF STATE]
proof (prove)
using this:
vec_mat_Tensor v (w # N) = vec_vec_Tensor v w # vec_mat_Tensor v N
j = Suc k

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

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>vec_mat_Tensor v (w # N) = vec_vec_Tensor v w # vec_mat_Tensor v N; j = Suc nat\<rbrakk> \<Longrightarrow> j < length (w # N) \<longrightarrow> vec_mat_Tensor v (w # N) ! j = vec_vec_Tensor v ((w # N) ! j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vec_mat_Tensor v (w # N) ! j = vec_mat_Tensor v N ! k

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>vec_mat_Tensor v (w # N) = vec_vec_Tensor v w # vec_mat_Tensor v N; j = Suc nat\<rbrakk> \<Longrightarrow> j < length (w # N) \<longrightarrow> vec_mat_Tensor v (w # N) ! j = vec_vec_Tensor v ((w # N) ! j)
[PROOF STEP]
have "j < length (w#N) \<Longrightarrow> k < length N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < length (w # N) \<Longrightarrow> k < length N
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
j = Suc k

goal (1 subgoal):
 1. j < length (w # N) \<Longrightarrow> k < length N
[PROOF STEP]
by (metis length_Suc_conv not_less_eq)
[PROOF STATE]
proof (state)
this:
j < length (w # N) \<Longrightarrow> k < length N

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>vec_mat_Tensor v (w # N) = vec_vec_Tensor v w # vec_mat_Tensor v N; j = Suc nat\<rbrakk> \<Longrightarrow> j < length (w # N) \<longrightarrow> vec_mat_Tensor v (w # N) ! j = vec_vec_Tensor v ((w # N) ! j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j < length (w # N) \<Longrightarrow> k < length N

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>vec_mat_Tensor v (w # N) = vec_vec_Tensor v w # vec_mat_Tensor v N; j = Suc nat\<rbrakk> \<Longrightarrow> j < length (w # N) \<longrightarrow> vec_mat_Tensor v (w # N) ! j = vec_vec_Tensor v ((w # N) ! j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j < length (w # N) \<Longrightarrow> k < length N
[PROOF STEP]
have "k < length (N)
                  \<Longrightarrow> (vec_mat_Tensor v N)!k =   vec_vec_Tensor v (N!k)"
[PROOF STATE]
proof (prove)
using this:
j < length (w # N) \<Longrightarrow> k < length N

goal (1 subgoal):
 1. k < length N \<Longrightarrow> vec_mat_Tensor v N ! k = vec_vec_Tensor v (N ! k)
[PROOF STEP]
using Cons.hyps
[PROOF STATE]
proof (prove)
using this:
j < length (w # N) \<Longrightarrow> k < length N
?j < length N \<longrightarrow> vec_mat_Tensor v N ! ?j = vec_vec_Tensor v (N ! ?j)

goal (1 subgoal):
 1. k < length N \<Longrightarrow> vec_mat_Tensor v N ! k = vec_vec_Tensor v (N ! k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k < length N \<Longrightarrow> vec_mat_Tensor v N ! k = vec_vec_Tensor v (N ! k)

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>vec_mat_Tensor v (w # N) = vec_vec_Tensor v w # vec_mat_Tensor v N; j = Suc nat\<rbrakk> \<Longrightarrow> j < length (w # N) \<longrightarrow> vec_mat_Tensor v (w # N) ! j = vec_vec_Tensor v ((w # N) ! j)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
vec_mat_Tensor v (w # N) ! j = vec_mat_Tensor v N ! k
j < length (w # N) \<Longrightarrow> k < length N
k < length N \<Longrightarrow> vec_mat_Tensor v N ! k = vec_vec_Tensor v (N ! k)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vec_mat_Tensor v (w # N) ! j = vec_mat_Tensor v N ! k
j < length (w # N) \<Longrightarrow> k < length N
k < length N \<Longrightarrow> vec_mat_Tensor v N ! k = vec_vec_Tensor v (N ! k)

goal (1 subgoal):
 1. j < length (w # N) \<longrightarrow> vec_mat_Tensor v (w # N) ! j = vec_vec_Tensor v ((w # N) ! j)
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
vec_mat_Tensor v (w # N) ! j = vec_mat_Tensor v N ! k
j < length (w # N) \<Longrightarrow> k < length N
k < length N \<Longrightarrow> vec_mat_Tensor v N ! k = vec_vec_Tensor v (N ! k)
j = Suc k

goal (1 subgoal):
 1. j < length (w # N) \<longrightarrow> vec_mat_Tensor v (w # N) ! j = vec_vec_Tensor v ((w # N) ! j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < length (w # N) \<longrightarrow> vec_mat_Tensor v (w # N) ! j = vec_vec_Tensor v ((w # N) ! j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
j < length (w # N) \<longrightarrow> vec_mat_Tensor v (w # N) ! j = vec_vec_Tensor v ((w # N) ! j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma col_vec_mat_Tensor:fixes j M v
 assumes "j < (length M)"
 shows "col (vec_mat_Tensor v M) j = vec_vec_Tensor v (col M j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (vec_mat_Tensor v M) j = vec_vec_Tensor v (col M j)
[PROOF STEP]
using col_vec_mat_Tensor_prelim assms
[PROOF STATE]
proof (prove)
using this:
\<forall>j<length ?M. col (vec_mat_Tensor ?v ?M) j = vec_vec_Tensor ?v (col ?M j)
j < length M

goal (1 subgoal):
 1. col (vec_mat_Tensor v M) j = vec_vec_Tensor v (col M j)
[PROOF STEP]
by auto


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

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

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

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

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

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

goal (1 subgoal):
 1. j < length (v # M) * length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> col (v # M \<otimes> M2) j = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
have "j < (1+ length M)*(length M2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < (1 + length M) * length M2
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
j < length (v # M) * length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2

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

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

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

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

goal (1 subgoal):
 1. length M2 \<le> j \<Longrightarrow> j - length M2 < length M * length M2
[PROOF STEP]
using add_0_iff add_diff_inverse diff_is_0_eq
                   less_diff_conv less_imp_le linorder_cases add.commute
                   neq0_conv
[PROOF STATE]
proof (prove)
using this:
j < length M2 + length M * length M2
(?b = ?b + ?a) = (?a = (0::?'a))
\<not> ?a < ?b \<Longrightarrow> ?b + (?a - ?b) = ?a
(?m - ?n = 0) = (?m \<le> ?n)
(?i < ?j - ?k) = (?i + ?k < ?j)
?x < ?y \<Longrightarrow> ?x \<le> ?y
\<lbrakk>?x < ?y \<Longrightarrow> ?P; ?x = ?y \<Longrightarrow> ?P; ?y < ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
?a + ?b = ?b + ?a
(?n \<noteq> 0) = (0 < ?n)

goal (1 subgoal):
 1. length M2 \<le> j \<Longrightarrow> j - length M2 < length M * length M2
[PROOF STEP]
by (metis (opaque_lifting, no_types))
[PROOF STATE]
proof (state)
this:
length M2 \<le> j \<Longrightarrow> j - length M2 < length M * length M2

goal (1 subgoal):
 1. j < length (v # M) * length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> col (v # M \<otimes> M2) j = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
have 3:"(v#M)\<otimes>M2 = (vec_mat_Tensor v M2)@(M \<otimes> M2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v # M \<otimes> M2 = vec_mat_Tensor v M2 @ (M \<otimes> M2)
[PROOF STEP]
using Tensor.simps
[PROOF STATE]
proof (prove)
using this:
[] \<otimes> ?xs = []
?x # ?xs \<otimes> ?ys = vec_mat_Tensor ?x ?ys @ (?xs \<otimes> ?ys)

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

goal (1 subgoal):
 1. j < length (v # M) * length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> col (v # M \<otimes> M2) j = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
have "(col ((v#M)\<otimes>M2) j) = (col ((vec_mat_Tensor v M2)@(M \<otimes> M2)) j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (v # M \<otimes> M2) j = col (vec_mat_Tensor v M2 @ (M \<otimes> M2)) j
[PROOF STEP]
using col_def
[PROOF STATE]
proof (prove)
using this:
col ?m ?i \<equiv> ?m ! ?i

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

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

goal (1 subgoal):
 1. j < length (vec_mat_Tensor v M2) \<Longrightarrow> col (v # M \<otimes> M2) j = col (vec_mat_Tensor v M2) j
[PROOF STEP]
unfolding col_def
[PROOF STATE]
proof (prove)
using this:
(v # M \<otimes> M2) ! j = (vec_mat_Tensor v M2 @ (M \<otimes> M2)) ! j

goal (1 subgoal):
 1. j < length (vec_mat_Tensor v M2) \<Longrightarrow> (v # M \<otimes> M2) ! j = vec_mat_Tensor v M2 ! j
[PROOF STEP]
using append_simpl
[PROOF STATE]
proof (prove)
using this:
(v # M \<otimes> M2) ! j = (vec_mat_Tensor v M2 @ (M \<otimes> M2)) ! j
?i < length ?xs \<longrightarrow> (?xs @ ?ys) ! ?i = ?xs ! ?i

goal (1 subgoal):
 1. j < length (vec_mat_Tensor v M2) \<Longrightarrow> (v # M \<otimes> M2) ! j = vec_mat_Tensor v M2 ! j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < length (vec_mat_Tensor v M2) \<Longrightarrow> col (v # M \<otimes> M2) j = col (vec_mat_Tensor v M2) j

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

goal (1 subgoal):
 1. j < length M2 \<Longrightarrow> col (v # M \<otimes> M2) j = col (vec_mat_Tensor v M2) j
[PROOF STEP]
using vec_mat_Tensor_length
[PROOF STATE]
proof (prove)
using this:
j < length (vec_mat_Tensor v M2) \<Longrightarrow> col (v # M \<otimes> M2) j = col (vec_mat_Tensor v M2) j
length (vec_mat_Tensor ?xs ?ys) = length ?ys

goal (1 subgoal):
 1. j < length M2 \<Longrightarrow> col (v # M \<otimes> M2) j = col (vec_mat_Tensor v M2) j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
j < length M2 \<Longrightarrow> col (v # M \<otimes> M2) j = col (vec_mat_Tensor v M2) j

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

goal (1 subgoal):
 1. j < length M2 \<Longrightarrow> col (vec_mat_Tensor v M2) j = vec_vec_Tensor v (col M2 j)
[PROOF STEP]
using col_vec_mat_Tensor
[PROOF STATE]
proof (prove)
using this:
j < length M2 \<Longrightarrow> col (v # M \<otimes> M2) j = col (vec_mat_Tensor v M2) j
?j < length ?M \<Longrightarrow> col (vec_mat_Tensor ?v ?M) ?j = vec_vec_Tensor ?v (col ?M ?j)

goal (1 subgoal):
 1. j < length M2 \<Longrightarrow> col (vec_mat_Tensor v M2) j = vec_vec_Tensor v (col M2 j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < length M2 \<Longrightarrow> col (vec_mat_Tensor v M2) j = vec_vec_Tensor v (col M2 j)

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

goal (1 subgoal):
 1. j < length M2 \<Longrightarrow> col (vec_mat_Tensor v M2) j = vec_vec_Tensor ((v # M) ! (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < length M2 \<Longrightarrow> col (vec_mat_Tensor v M2) j = vec_vec_Tensor ((v # M) ! (j div length M2)) (col M2 (j mod length M2))

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

goal (1 subgoal):
 1. j < length M2 \<Longrightarrow> col (v # M \<otimes> M2) j = vec_vec_Tensor ((v # M) ! (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
j < length M2 \<Longrightarrow> col (vec_mat_Tensor v M2) j = vec_vec_Tensor ((v # M) ! (j div length M2)) (col M2 (j mod length M2))
j < length M2 \<Longrightarrow> col (v # M \<otimes> M2) j = col (vec_mat_Tensor v M2) j

goal (1 subgoal):
 1. j < length M2 \<Longrightarrow> col (v # M \<otimes> M2) j = vec_vec_Tensor ((v # M) ! (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < length M2 \<Longrightarrow> col (v # M \<otimes> M2) j = vec_vec_Tensor ((v # M) ! (j div length M2)) (col M2 (j mod length M2))

goal (1 subgoal):
 1. j < length (v # M) * length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> col (v # M \<otimes> M2) j = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
have 4:"j \<ge> length M2
                  \<Longrightarrow> (col ((v#M)\<otimes>M2) j)= (M \<otimes> M2)!(j- (length M2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length M2 \<le> j \<Longrightarrow> col (v # M \<otimes> M2) j = (M \<otimes> M2) ! (j - length M2)
[PROOF STEP]
unfolding col_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length M2 \<le> j \<Longrightarrow> (v # M \<otimes> M2) ! j = (M \<otimes> M2) ! (j - length M2)
[PROOF STEP]
using 3 append_simpl2 vec_mat_Tensor_length
[PROOF STATE]
proof (prove)
using this:
v # M \<otimes> M2 = vec_mat_Tensor v M2 @ (M \<otimes> M2)
length ?xs \<le> ?i \<longrightarrow> (?xs @ ?ys) ! ?i = ?ys ! (?i - length ?xs)
length (vec_mat_Tensor ?xs ?ys) = length ?ys

goal (1 subgoal):
 1. length M2 \<le> j \<Longrightarrow> (v # M \<otimes> M2) ! j = (M \<otimes> M2) ! (j - length M2)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
length M2 \<le> j \<Longrightarrow> col (v # M \<otimes> M2) j = (M \<otimes> M2) ! (j - length M2)

goal (1 subgoal):
 1. j < length (v # M) * length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> col (v # M \<otimes> M2) j = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length M2 \<le> j \<Longrightarrow> col (v # M \<otimes> M2) j = (M \<otimes> M2) ! (j - length M2)
[PROOF STEP]
have 5:
         "j \<ge> length M2 \<Longrightarrow>
              col (M \<otimes> M2) (j-length M2)
                     = vec_vec_Tensor
                                (col M ((j-length M2) div length M2))
                                (col M2 ((j- length M2) mod length M2))"
[PROOF STATE]
proof (prove)
using this:
length M2 \<le> j \<Longrightarrow> col (v # M \<otimes> M2) j = (M \<otimes> M2) ! (j - length M2)

goal (1 subgoal):
 1. length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col M ((j - length M2) div length M2)) (col M2 ((j - length M2) mod length M2))
[PROOF STEP]
using 1 0 2 Cons
[PROOF STATE]
proof (prove)
using this:
length M2 \<le> j \<Longrightarrow> col (v # M \<otimes> M2) j = (M \<otimes> M2) ! (j - length M2)
mat (row_length M) (length M) M
j < length (v # M) * length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2
length M2 \<le> j \<Longrightarrow> j - length M2 < length M * length M2
?j < length M * length M2 \<and> mat (row_length M) (length M) M \<and> mat (row_length M2) (length M2) M2 \<longrightarrow> col (M \<otimes> M2) ?j = vec_vec_Tensor (col M (?j div length M2)) (col M2 (?j mod length M2))

goal (1 subgoal):
 1. length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col M ((j - length M2) div length M2)) (col M2 ((j - length M2) mod length M2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col M ((j - length M2) div length M2)) (col M2 ((j - length M2) mod length M2))

goal (1 subgoal):
 1. j < length (v # M) * length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> col (v # M \<otimes> M2) j = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col M ((j - length M2) div length M2)) (col M2 ((j - length M2) mod length M2))
[PROOF STEP]
have 6:
         "j \<ge> length M2 \<Longrightarrow>
                 (j - length M2) div (length M2) + 1 = j div (length M2)"
[PROOF STATE]
proof (prove)
using this:
length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col M ((j - length M2) div length M2)) (col M2 ((j - length M2) mod length M2))

goal (1 subgoal):
 1. length M2 \<le> j \<Longrightarrow> (j - length M2) div length M2 + 1 = j div length M2
[PROOF STEP]
using 2  div_0 div_self
                   le_neq_implies_less less_nat_zero_code
                   monoid_add_class.add.right_neutral mult_0 mult_cancel2
                   add.commute nat_div neq0_conv div_add_self1 le_add_diff_inverse
[PROOF STATE]
proof (prove)
using this:
length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col M ((j - length M2) div length M2)) (col M2 ((j - length M2) mod length M2))
length M2 \<le> j \<Longrightarrow> j - length M2 < length M * length M2
(0::?'a) div ?a = (0::?'a)
?a \<noteq> (0::?'a) \<Longrightarrow> ?a div ?a = (1::?'a)
\<lbrakk>?m \<le> ?n; ?m \<noteq> ?n\<rbrakk> \<Longrightarrow> ?m < ?n
(?n < 0) = False
?a + (0::?'a) = ?a
0 * ?n = 0
(?m * ?k = ?n * ?k) = (?m = ?n \<or> ?k = 0)
?a + ?b = ?b + ?a
\<lbrakk>0 < ?b; ?b < ?a\<rbrakk> \<Longrightarrow> ?a div ?b = (?a - ?b) div ?b + 1
(?n \<noteq> 0) = (0 < ?n)
?b \<noteq> (0::?'a) \<Longrightarrow> (?b + ?a) div ?b = ?a div ?b + (1::?'a)
?b \<le> ?a \<Longrightarrow> ?b + (?a - ?b) = ?a

goal (1 subgoal):
 1. length M2 \<le> j \<Longrightarrow> (j - length M2) div length M2 + 1 = j div length M2
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
length M2 \<le> j \<Longrightarrow> (j - length M2) div length M2 + 1 = j div length M2

goal (1 subgoal):
 1. j < length (v # M) * length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> col (v # M \<otimes> M2) j = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length M2 \<le> j \<Longrightarrow> (j - length M2) div length M2 + 1 = j div length M2
[PROOF STEP]
have
           "j \<ge> length M2 \<Longrightarrow>
                    ((j- length M2) mod length M2) = j mod (length M2)"
[PROOF STATE]
proof (prove)
using this:
length M2 \<le> j \<Longrightarrow> (j - length M2) div length M2 + 1 = j div length M2

goal (1 subgoal):
 1. length M2 \<le> j \<Longrightarrow> (j - length M2) mod length M2 = j mod length M2
[PROOF STEP]
using le_mod_geq
[PROOF STATE]
proof (prove)
using this:
length M2 \<le> j \<Longrightarrow> (j - length M2) div length M2 + 1 = j div length M2
?n \<le> ?m \<Longrightarrow> ?m mod ?n = (?m - ?n) mod ?n

goal (1 subgoal):
 1. length M2 \<le> j \<Longrightarrow> (j - length M2) mod length M2 = j mod length M2
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
length M2 \<le> j \<Longrightarrow> (j - length M2) mod length M2 = j mod length M2

goal (1 subgoal):
 1. j < length (v # M) * length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> col (v # M \<otimes> M2) j = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
with 6
[PROOF STATE]
proof (chain)
picking this:
length M2 \<le> j \<Longrightarrow> (j - length M2) div length M2 + 1 = j div length M2
length M2 \<le> j \<Longrightarrow> (j - length M2) mod length M2 = j mod length M2
[PROOF STEP]
have 7:
         "j \<ge> length M2 \<Longrightarrow>
              col (M \<otimes> M2) (j-length M2)
                     = vec_vec_Tensor (col M ((j-length M2) div length M2))
                                (col M2 (j mod length M2))"
[PROOF STATE]
proof (prove)
using this:
length M2 \<le> j \<Longrightarrow> (j - length M2) div length M2 + 1 = j div length M2
length M2 \<le> j \<Longrightarrow> (j - length M2) mod length M2 = j mod length M2

goal (1 subgoal):
 1. length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col M ((j - length M2) div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
using 5
[PROOF STATE]
proof (prove)
using this:
length M2 \<le> j \<Longrightarrow> (j - length M2) div length M2 + 1 = j div length M2
length M2 \<le> j \<Longrightarrow> (j - length M2) mod length M2 = j mod length M2
length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col M ((j - length M2) div length M2)) (col M2 ((j - length M2) mod length M2))

goal (1 subgoal):
 1. length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col M ((j - length M2) div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col M ((j - length M2) div length M2)) (col M2 (j mod length M2))

goal (1 subgoal):
 1. j < length (v # M) * length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> col (v # M \<otimes> M2) j = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col M ((j - length M2) div length M2)) (col M2 (j mod length M2))

goal (1 subgoal):
 1. j < length (v # M) * length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> col (v # M \<otimes> M2) j = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
have "k<(length M) \<Longrightarrow> (col M k) = (col (v#M) (k+1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < length M \<Longrightarrow> col M k = col (v # M) (k + 1)
[PROOF STEP]
unfolding col_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < length M \<Longrightarrow> M ! k = (v # M) ! (k + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k < length M \<Longrightarrow> col M k = col (v # M) (k + 1)

goal (1 subgoal):
 1. j < length (v # M) * length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> col (v # M \<otimes> M2) j = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col M ((j - length M2) div length M2)) (col M2 (j mod length M2))
k < length M \<Longrightarrow> col M k = col (v # M) (k + 1)
[PROOF STEP]
have "j \<ge> length M2 \<Longrightarrow>
              col (M \<otimes> M2) (j-length M2)
                     = vec_vec_Tensor (col (v#M) (j div length M2))
                                (col M2 (j mod length M2))"
[PROOF STATE]
proof (prove)
using this:
length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col M ((j - length M2) div length M2)) (col M2 (j mod length M2))
k < length M \<Longrightarrow> col M k = col (v # M) (k + 1)

goal (1 subgoal):
 1. length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>length M2 \<le> j; length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col M ((j - length M2) div length M2)) (col M2 (j mod length M2)); k < length M \<Longrightarrow> col M k = col (v # M) (k + 1)\<rbrakk> \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
assume temp:"j \<ge> length M2 "
[PROOF STATE]
proof (state)
this:
length M2 \<le> j

goal (1 subgoal):
 1. \<lbrakk>length M2 \<le> j; length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col M ((j - length M2) div length M2)) (col M2 (j mod length M2)); k < length M \<Longrightarrow> col M k = col (v # M) (k + 1)\<rbrakk> \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
have " j- (length M2) < (length M)*(length M2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j - length M2 < length M * length M2
[PROOF STEP]
using 2 temp
[PROOF STATE]
proof (prove)
using this:
length M2 \<le> j \<Longrightarrow> j - length M2 < length M * length M2
length M2 \<le> j

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

goal (1 subgoal):
 1. \<lbrakk>length M2 \<le> j; length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col M ((j - length M2) div length M2)) (col M2 (j mod length M2)); k < length M \<Longrightarrow> col M k = col (v # M) (k + 1)\<rbrakk> \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j - length M2 < length M * length M2
[PROOF STEP]
have "(j- (length M2)) div (length M2) < (length M)"
[PROOF STATE]
proof (prove)
using this:
j - length M2 < length M * length M2

goal (1 subgoal):
 1. (j - length M2) div length M2 < length M
[PROOF STEP]
using div_right_ineq mult.commute
[PROOF STATE]
proof (prove)
using this:
j - length M2 < length M * length M2
?x < ?y * ?z \<Longrightarrow> ?x div ?y < ?z
?a * ?b = ?b * ?a

goal (1 subgoal):
 1. (j - length M2) div length M2 < length M
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(j - length M2) div length M2 < length M

goal (1 subgoal):
 1. \<lbrakk>length M2 \<le> j; length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col M ((j - length M2) div length M2)) (col M2 (j mod length M2)); k < length M \<Longrightarrow> col M k = col (v # M) (k + 1)\<rbrakk> \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(j - length M2) div length M2 < length M

goal (1 subgoal):
 1. \<lbrakk>length M2 \<le> j; length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col M ((j - length M2) div length M2)) (col M2 (j mod length M2)); k < length M \<Longrightarrow> col M k = col (v # M) (k + 1)\<rbrakk> \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
have
                 "((j- (length M2)) div (length M2)<(length M)
                     \<longrightarrow> (col M ((j- (length M2)) div (length M2)))
                          = (col (v#M) ((j- (length M2)) div (length M2)+1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (j - length M2) div length M2 < length M \<longrightarrow> col M ((j - length M2) div length M2) = col (v # M) ((j - length M2) div length M2 + 1)
[PROOF STEP]
unfolding col_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (j - length M2) div length M2 < length M \<longrightarrow> M ! ((j - length M2) div length M2) = (v # M) ! ((j - length M2) div length M2 + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(j - length M2) div length M2 < length M \<longrightarrow> col M ((j - length M2) div length M2) = col (v # M) ((j - length M2) div length M2 + 1)

goal (1 subgoal):
 1. \<lbrakk>length M2 \<le> j; length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col M ((j - length M2) div length M2)) (col M2 (j mod length M2)); k < length M \<Longrightarrow> col M k = col (v # M) (k + 1)\<rbrakk> \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(j - length M2) div length M2 < length M
(j - length M2) div length M2 < length M \<longrightarrow> col M ((j - length M2) div length M2) = col (v # M) ((j - length M2) div length M2 + 1)
[PROOF STEP]
have temp1:
                      "(col (v#M) (((j-length M2) div length M2)+1))
                                  = (col M (((j-length M2) div length M2)))"
[PROOF STATE]
proof (prove)
using this:
(j - length M2) div length M2 < length M
(j - length M2) div length M2 < length M \<longrightarrow> col M ((j - length M2) div length M2) = col (v # M) ((j - length M2) div length M2 + 1)

goal (1 subgoal):
 1. col (v # M) ((j - length M2) div length M2 + 1) = col M ((j - length M2) div length M2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
col (v # M) ((j - length M2) div length M2 + 1) = col M ((j - length M2) div length M2)

goal (1 subgoal):
 1. \<lbrakk>length M2 \<le> j; length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col M ((j - length M2) div length M2)) (col M2 (j mod length M2)); k < length M \<Longrightarrow> col M k = col (v # M) (k + 1)\<rbrakk> \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
col (v # M) ((j - length M2) div length M2 + 1) = col M ((j - length M2) div length M2)
[PROOF STEP]
have "(col (v#M) (((j-length M2) div length M2)+1))
                                   = (col (v#M) (j div length M2))"
[PROOF STATE]
proof (prove)
using this:
col (v # M) ((j - length M2) div length M2 + 1) = col M ((j - length M2) div length M2)

goal (1 subgoal):
 1. col (v # M) ((j - length M2) div length M2 + 1) = col (v # M) (j div length M2)
[PROOF STEP]
using 6 temp
[PROOF STATE]
proof (prove)
using this:
col (v # M) ((j - length M2) div length M2 + 1) = col M ((j - length M2) div length M2)
length M2 \<le> j \<Longrightarrow> (j - length M2) div length M2 + 1 = j div length M2
length M2 \<le> j

goal (1 subgoal):
 1. col (v # M) ((j - length M2) div length M2 + 1) = col (v # M) (j div length M2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
col (v # M) ((j - length M2) div length M2 + 1) = col (v # M) (j div length M2)

goal (1 subgoal):
 1. \<lbrakk>length M2 \<le> j; length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col M ((j - length M2) div length M2)) (col M2 (j mod length M2)); k < length M \<Longrightarrow> col M k = col (v # M) (k + 1)\<rbrakk> \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
col (v # M) ((j - length M2) div length M2 + 1) = col (v # M) (j div length M2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
col (v # M) ((j - length M2) div length M2 + 1) = col (v # M) (j div length M2)

goal (1 subgoal):
 1. col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
using temp1 7
[PROOF STATE]
proof (prove)
using this:
col (v # M) ((j - length M2) div length M2 + 1) = col (v # M) (j div length M2)
col (v # M) ((j - length M2) div length M2 + 1) = col M ((j - length M2) div length M2)
length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col M ((j - length M2) div length M2)) (col M2 (j mod length M2))

goal (1 subgoal):
 1. col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
by (metis temp)
[PROOF STATE]
proof (state)
this:
col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))

goal (1 subgoal):
 1. j < length (v # M) * length M2 \<and> mat (row_length (v # M)) (length (v # M)) (v # M) \<and> mat (row_length M2) (length M2) M2 \<Longrightarrow> col (v # M \<otimes> M2) j = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
have "j \<ge> length M2 \<Longrightarrow>
              col ((v#M) \<otimes> M2) j
                     = vec_vec_Tensor (col (v#M) (j div length M2))
                                (col M2 (j mod length M2))"
[PROOF STATE]
proof (prove)
using this:
length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))

goal (1 subgoal):
 1. length M2 \<le> j \<Longrightarrow> col (v # M \<otimes> M2) j = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
using col_def 4
[PROOF STATE]
proof (prove)
using this:
length M2 \<le> j \<Longrightarrow> col (M \<otimes> M2) (j - length M2) = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
col ?m ?i \<equiv> ?m ! ?i
length M2 \<le> j \<Longrightarrow> col (v # M \<otimes> M2) j = (M \<otimes> M2) ! (j - length M2)

goal (1 subgoal):
 1. length M2 \<le> j \<Longrightarrow> col (v # M \<otimes> M2) j = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
length M2 \<le> j \<Longrightarrow> col (v # M \<otimes> M2) j = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))

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

goal (1 subgoal):
 1. col (v # M \<otimes> M2) j = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
[PROOF STEP]
using step_1  col_def le_refl nat_less_le nat_neq_iff
[PROOF STATE]
proof (prove)
using this:
length M2 \<le> j \<Longrightarrow> col (v # M \<otimes> M2) j = vec_vec_Tensor (col (v # M) (j div length M2)) (col M2 (j mod length M2))
j < length M2 \<Longrightarrow> col (v # M \<otimes> M2) j = vec_vec_Tensor ((v # M) ! (j div length M2)) (col M2 (j mod length M2))
col ?m ?i \<equiv> ?m ! ?i
?n \<le> ?n
(?m < ?n) = (?m \<le> ?n \<and> ?m \<noteq> ?n)
(?m \<noteq> ?n) = (?m < ?n \<or> ?n < ?m)

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma row_Cons:"row (v#M) i = (v!i)#(row M i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (v # M) i = v ! i # row M i
[PROOF STEP]
unfolding row_def map_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>w. w ! i) (v # M) = v ! i # map (\<lambda>w. w ! i) M
[PROOF STEP]
by auto


[STATEMENT]
lemma row_append:"row (A@B)i = (row A i)@(row B i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (A @ B) i = row A i @ row B i
[PROOF STEP]
unfolding row_def map_append
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>w. w ! i) A @ map (\<lambda>w. w ! i) B = map (\<lambda>w. w ! i) A @ map (\<lambda>w. w ! i) B
[PROOF STEP]
by auto


[STATEMENT]
lemma row_empty:"row [] i = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row [] i = []
[PROOF STEP]
unfolding row_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>w. w ! i) [] = []
[PROOF STEP]
by auto


[STATEMENT]
lemma vec_vec_Tensor_right_empty:"vec_vec_Tensor x [] = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_vec_Tensor x [] = []
[PROOF STEP]
using vec_vec_Tensor.simps times.simps  length_0_conv mult_0_right vec_vec_Tensor_length
[PROOF STATE]
proof (prove)
using this:
vec_vec_Tensor [] ?ys = []
vec_vec_Tensor (?x # ?xs) ?ys = local.times ?x ?ys @ vec_vec_Tensor ?xs ?ys
local.times ?n [] = []
local.times ?n (?y # ?ys) = (?n * ?y) # local.times ?n ?ys
(length ?xs = 0) = (?xs = [])
?m * 0 = 0
length (vec_vec_Tensor ?x ?y) = length ?x * length ?y

goal (1 subgoal):
 1. vec_vec_Tensor x [] = []
[PROOF STEP]
by (metis)


[STATEMENT]
lemma "vec_mat_Tensor v ([]#[]) = [[]] "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_mat_Tensor v null_matrix = null_matrix
[PROOF STEP]
using vec_mat_Tensor.simps
[PROOF STATE]
proof (prove)
using this:
vec_mat_Tensor ?xs [] = []
vec_mat_Tensor ?xs (?ys # ?yss) = vec_vec_Tensor ?xs ?ys # vec_mat_Tensor ?xs ?yss

goal (1 subgoal):
 1. vec_mat_Tensor v null_matrix = null_matrix
[PROOF STEP]
by (metis vec_vec_Tensor_right_empty)