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

goal (2 subgoals):
 1. \<And>i j. (i < length v * row_length [] \<and> j < length []) \<and> mat (row_length []) (length []) [] \<longrightarrow> vec_mat_Tensor v [] ! j ! i = v ! (i div row_length []) * [] ! j ! (i mod row_length [])
 2. \<And>a M i j. (\<And>i j. (i < length v * row_length M \<and> j < length M) \<and> mat (row_length M) (length M) M \<longrightarrow> vec_mat_Tensor v M ! j ! i = v ! (i div row_length M) * M ! j ! (i mod row_length M)) \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod 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_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 auto
[PROOF STATE]
proof (state)
this:
row_length [] = 0

goal (2 subgoals):
 1. \<And>i j. (i < length v * row_length [] \<and> j < length []) \<and> mat (row_length []) (length []) [] \<longrightarrow> vec_mat_Tensor v [] ! j ! i = v ! (i div row_length []) * [] ! j ! (i mod row_length [])
 2. \<And>a M i j. (\<And>i j. (i < length v * row_length M \<and> j < length M) \<and> mat (row_length M) (length M) M \<longrightarrow> vec_mat_Tensor v M ! j ! i = v ! (i div row_length M) * M ! j ! (i mod row_length M)) \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
row_length [] = 0
[PROOF STEP]
have "(length v)*(row_length []) = 0"
[PROOF STATE]
proof (prove)
using this:
row_length [] = 0

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

goal (2 subgoals):
 1. \<And>i j. (i < length v * row_length [] \<and> j < length []) \<and> mat (row_length []) (length []) [] \<longrightarrow> vec_mat_Tensor v [] ! j ! i = v ! (i div row_length []) * [] ! j ! (i mod row_length [])
 2. \<And>a M i j. (\<And>i j. (i < length v * row_length M \<and> j < length M) \<and> mat (row_length M) (length M) M \<longrightarrow> vec_mat_Tensor v M ! j ! i = v ! (i div row_length M) * M ! j ! (i mod row_length M)) \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
length v * row_length [] = 0
[PROOF STEP]
have "((i<((length v)*(row_length [])))\<and>(j < (length []))) \<longrightarrow> False"
[PROOF STATE]
proof (prove)
using this:
length v * row_length [] = 0

goal (1 subgoal):
 1. i < length v * row_length [] \<and> j < length [] \<longrightarrow> False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length v * row_length [] \<and> j < length [] \<longrightarrow> False

goal (2 subgoals):
 1. \<And>i j. (i < length v * row_length [] \<and> j < length []) \<and> mat (row_length []) (length []) [] \<longrightarrow> vec_mat_Tensor v [] ! j ! i = v ! (i div row_length []) * [] ! j ! (i mod row_length [])
 2. \<And>a M i j. (\<And>i j. (i < length v * row_length M \<and> j < length M) \<and> mat (row_length M) (length M) M \<longrightarrow> vec_mat_Tensor v M ! j ! i = v ! (i div row_length M) * M ! j ! (i mod row_length M)) \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i < length v * row_length [] \<and> j < length [] \<longrightarrow> False

goal (2 subgoals):
 1. \<And>i j. (i < length v * row_length [] \<and> j < length []) \<and> mat (row_length []) (length []) [] \<longrightarrow> vec_mat_Tensor v [] ! j ! i = v ! (i div row_length []) * [] ! j ! (i mod row_length [])
 2. \<And>a M i j. (\<And>i j. (i < length v * row_length M \<and> j < length M) \<and> mat (row_length M) (length M) M \<longrightarrow> vec_mat_Tensor v M ! j ! i = v ! (i div row_length M) * M ! j ! (i mod row_length M)) \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod 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]
by auto
[PROOF STATE]
proof (state)
this:
vec_mat_Tensor v [] = []

goal (2 subgoals):
 1. \<And>i j. (i < length v * row_length [] \<and> j < length []) \<and> mat (row_length []) (length []) [] \<longrightarrow> vec_mat_Tensor v [] ! j ! i = v ! (i div row_length []) * [] ! j ! (i mod row_length [])
 2. \<And>a M i j. (\<And>i j. (i < length v * row_length M \<and> j < length M) \<and> mat (row_length M) (length M) M \<longrightarrow> vec_mat_Tensor v M ! j ! i = v ! (i div row_length M) * M ! j ! (i mod row_length M)) \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vec_mat_Tensor v [] = []

goal (2 subgoals):
 1. \<And>i j. (i < length v * row_length [] \<and> j < length []) \<and> mat (row_length []) (length []) [] \<longrightarrow> vec_mat_Tensor v [] ! j ! i = v ! (i div row_length []) * [] ! j ! (i mod row_length [])
 2. \<And>a M i j. (\<And>i j. (i < length v * row_length M \<and> j < length M) \<and> mat (row_length M) (length M) M \<longrightarrow> vec_mat_Tensor v M ! j ! i = v ! (i div row_length M) * M ! j ! (i mod row_length M)) \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
have "(((i<((length v)*(row_length [])))\<and>(j < (length [])))
                  \<longrightarrow> ((vec_mat_Tensor v [])!j!i)
                                = f (v!(i div (row_length []))) ([]!j!(i mod (row_length []))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length v * row_length [] \<and> j < length [] \<longrightarrow> vec_mat_Tensor v [] ! j ! i = v ! (i div row_length []) * [] ! j ! (i mod row_length [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length v * row_length [] \<and> j < length [] \<longrightarrow> vec_mat_Tensor v [] ! j ! i = v ! (i div row_length []) * [] ! j ! (i mod row_length [])

goal (2 subgoals):
 1. \<And>i j. (i < length v * row_length [] \<and> j < length []) \<and> mat (row_length []) (length []) [] \<longrightarrow> vec_mat_Tensor v [] ! j ! i = v ! (i div row_length []) * [] ! j ! (i mod row_length [])
 2. \<And>a M i j. (\<And>i j. (i < length v * row_length M \<and> j < length M) \<and> mat (row_length M) (length M) M \<longrightarrow> vec_mat_Tensor v M ! j ! i = v ! (i div row_length M) * M ! j ! (i mod row_length M)) \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
i < length v * row_length [] \<and> j < length [] \<longrightarrow> vec_mat_Tensor v [] ! j ! i = v ! (i div row_length []) * [] ! j ! (i mod row_length [])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i < length v * row_length [] \<and> j < length [] \<longrightarrow> vec_mat_Tensor v [] ! j ! i = v ! (i div row_length []) * [] ! j ! (i mod row_length [])

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

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

goal (1 subgoal):
 1. \<And>a M i j. (\<And>i j. (i < length v * row_length M \<and> j < length M) \<and> mat (row_length M) (length M) M \<longrightarrow> vec_mat_Tensor v M ! j ! i = v ! (i div row_length M) * M ! j ! (i mod row_length M)) \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
have "(((i<((length v)*(row_length (a#M))))
       \<and>(j < (length (a#M))))
       \<and>(mat (row_length (a#M)) (length (a#M)) (a#M))
           \<longrightarrow> ((vec_mat_Tensor v (a#M))!j!i)
                  = f
                      (v!(i div (row_length (a#M))))
                      ((a#M)!j!(i mod (row_length (a#M)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
proof(cases a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = [] \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
 2. \<And>aa list. a = aa # list \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
a = []

goal (2 subgoals):
 1. a = [] \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
 2. \<And>aa list. a = aa # list \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # 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 auto
[PROOF STATE]
proof (state)
this:
row_length ([] # M) = 0

goal (2 subgoals):
 1. a = [] \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
 2. \<And>aa list. a = aa # list \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
row_length ([] # M) = 0
[PROOF STEP]
have 1:"(length v)*(row_length ([]#M)) = 0"
[PROOF STATE]
proof (prove)
using this:
row_length ([] # M) = 0

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

goal (2 subgoals):
 1. a = [] \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
 2. \<And>aa list. a = aa # list \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length v * row_length ([] # M) = 0
[PROOF STEP]
have "((i<((length v)*(row_length ([]#M))))
                \<and>(j < (length ([]#M)))) \<longrightarrow> False"
[PROOF STATE]
proof (prove)
using this:
length v * row_length ([] # M) = 0

goal (1 subgoal):
 1. i < length v * row_length ([] # M) \<and> j < length ([] # M) \<longrightarrow> False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length v * row_length ([] # M) \<and> j < length ([] # M) \<longrightarrow> False

goal (2 subgoals):
 1. a = [] \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
 2. \<And>aa list. a = aa # list \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i < length v * row_length ([] # M) \<and> j < length ([] # M) \<longrightarrow> False

goal (2 subgoals):
 1. a = [] \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
 2. \<And>aa list. a = aa # list \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
have
                 "(((i<((length v)*(row_length ([]#M))))
                  \<and>(j < (length ([]#M))))
                     \<longrightarrow> ((vec_mat_Tensor v ([]#M))!j!i) =
                                   f
                                        (v!(i div (row_length ([]#M))))
                                        ([]!j!(i mod (row_length ([]#M)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length v * row_length ([] # M) \<and> j < length ([] # M) \<longrightarrow> vec_mat_Tensor v ([] # M) ! j ! i = v ! (i div row_length ([] # M)) * [] ! j ! (i mod row_length ([] # M))
[PROOF STEP]
using calculation
[PROOF STATE]
proof (prove)
using this:
i < length v * row_length ([] # M) \<and> j < length ([] # M) \<longrightarrow> False

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

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

goal (1 subgoal):
 1. (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
using Nil 1 less_nat_zero_code
[PROOF STATE]
proof (prove)
using this:
i < length v * row_length ([] # M) \<and> j < length ([] # M) \<longrightarrow> vec_mat_Tensor v ([] # M) ! j ! i = v ! (i div row_length ([] # M)) * [] ! j ! (i mod row_length ([] # M))
a = []
length v * row_length ([] # M) = 0
(?n < 0) = False

goal (1 subgoal):
 1. (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
by (metis )
[PROOF STATE]
proof (state)
this:
(i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))

goal (1 subgoal):
 1. \<And>aa list. a = aa # list \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa list. a = aa # list \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
a = x # xs

goal (1 subgoal):
 1. \<And>aa list. a = aa # list \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
have 1:"(a#M)!(j+1) = M!j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a # M) ! (j + 1) = M ! j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a # M) ! (j + 1) = M ! j

goal (1 subgoal):
 1. \<And>aa list. a = aa # list \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
have "(((i<((length v)*(row_length M)))
           \<and>(j < (length M)))
           \<and>(mat (row_length M) (length M) M)
             \<longrightarrow> ((vec_mat_Tensor v M)!j!i) = f
                                               (v!(i div (row_length M)))
                                               (M!j!(i mod (row_length M))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i < length v * row_length M \<and> j < length M) \<and> mat (row_length M) (length M) M \<longrightarrow> vec_mat_Tensor v M ! j ! i = v ! (i div row_length M) * M ! j ! (i mod row_length M)
[PROOF STEP]
using Cons.hyps
[PROOF STATE]
proof (prove)
using this:
(?i < length v * row_length M \<and> ?j < length M) \<and> mat (row_length M) (length M) M \<longrightarrow> vec_mat_Tensor v M ! ?j ! ?i = v ! (?i div row_length M) * M ! ?j ! (?i mod row_length M)

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

goal (1 subgoal):
 1. \<And>aa list. a = aa # list \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
have 2: "(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
[PROOF STATE]
proof (prove)
using this:
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)

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>aa list. a = aa # list \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
row_length (a # M) = length a
[PROOF STEP]
have 3:"(i< (row_length (a#M))*(length v))
                              = (i < (length a)*(length v))"
[PROOF STATE]
proof (prove)
using this:
row_length (a # M) = length a

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

goal (1 subgoal):
 1. \<And>aa list. a = aa # list \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
have "a \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> []
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
a = x # xs

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

goal (1 subgoal):
 1. \<And>aa list. a = aa # list \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> []
[PROOF STEP]
have 4:
         "\<forall>i.((i < (length a)*(length v))
              \<longrightarrow>  ((vec_vec_Tensor v a)!i) = f
                                               (v!(i div (length a)))
                                               (a!(i mod (length a))))"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> []

goal (1 subgoal):
 1. \<forall>i<length a * length v. vec_vec_Tensor v a ! i = v ! (i div length a) * a ! (i mod length a)
[PROOF STEP]
using vec_vec_Tensor_elements Cons.hyps mult.commute
[PROOF STATE]
proof (prove)
using this:
a \<noteq> []
?y \<noteq> [] \<Longrightarrow> \<forall>i<length ?x * length ?y. vec_vec_Tensor ?x ?y ! i = ?x ! (i div length ?y) * ?y ! (i mod length ?y)
(?i < length v * row_length M \<and> ?j < length M) \<and> mat (row_length M) (length M) M \<longrightarrow> vec_mat_Tensor v M ! ?j ! ?i = v ! (?i div row_length M) * M ! ?j ! (?i mod row_length M)
?a * ?b = ?b * ?a

goal (1 subgoal):
 1. \<forall>i<length a * length v. vec_vec_Tensor v a ! i = v ! (i div length a) * a ! (i mod length a)
[PROOF STEP]
by (simp add: mult.commute vec_vec_Tensor_elements)
[PROOF STATE]
proof (state)
this:
\<forall>i<length a * length v. vec_vec_Tensor v a ! i = v ! (i div length a) * a ! (i mod length a)

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

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

goal (1 subgoal):
 1. \<And>aa list. a = aa # list \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
with 2 4
[PROOF STATE]
proof (chain)
picking this:
row_length (a # M) = length a
\<forall>i<length a * length v. vec_vec_Tensor v a ! i = v ! (i div length a) * a ! (i mod length a)
vec_mat_Tensor v (a # M) ! 0 = vec_vec_Tensor v a
[PROOF STEP]
have 5:
       "\<forall>i.((i < (row_length (a#M))*(length v))
          \<longrightarrow>  ((vec_mat_Tensor v (a#M))!0!i)
                                   = f
                                       (v!(i div (row_length (a#M))))
                                       ((a#M)!0!(i mod (row_length (a#M)))))"
[PROOF STATE]
proof (prove)
using this:
row_length (a # M) = length a
\<forall>i<length a * length v. vec_vec_Tensor v a ! i = v ! (i div length a) * a ! (i mod length a)
vec_mat_Tensor v (a # M) ! 0 = vec_vec_Tensor v a

goal (1 subgoal):
 1. \<forall>i<row_length (a # M) * length v. vec_mat_Tensor v (a # M) ! 0 ! i = v ! (i div row_length (a # M)) * (a # M) ! 0 ! (i mod row_length (a # M))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i<row_length (a # M) * length v. vec_mat_Tensor v (a # M) ! 0 ! i = v ! (i div row_length (a # M)) * (a # M) ! 0 ! (i mod row_length (a # M))

goal (1 subgoal):
 1. \<And>aa list. a = aa # list \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
have "length (a#M)>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < length (a # M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < length (a # M)

goal (1 subgoal):
 1. \<And>aa list. a = aa # list \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
with 5
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<row_length (a # M) * length v. vec_mat_Tensor v (a # M) ! 0 ! i = v ! (i div row_length (a # M)) * (a # M) ! 0 ! (i mod row_length (a # M))
0 < length (a # M)
[PROOF STEP]
have 6:
       "(j = 0)\<longrightarrow>
                    ((((i < (row_length (a#M))*(length v))
                    \<and>(j < (length (a#M))))
                    \<and>(mat (row_length (a#M)) (length (a#M)) (a#M))
                         \<longrightarrow>  ((vec_mat_Tensor v (a#M))!j!i)
                               = f
                                    (v!(i div (row_length (a#M))))
                                    ((a#M)!j!(i mod (row_length (a#M))))))"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<row_length (a # M) * length v. vec_mat_Tensor v (a # M) ! 0 ! i = v ! (i div row_length (a # M)) * (a # M) ! 0 ! (i mod row_length (a # M))
0 < length (a # M)

goal (1 subgoal):
 1. j = 0 \<longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j = 0 \<longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))

goal (1 subgoal):
 1. \<And>aa list. a = aa # list \<Longrightarrow> (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
have "(((i < (row_length (a#M))*(length v))
         \<and>(j < (length (a#M))))
         \<and>(mat (row_length (a#M)) (length (a#M)) (a#M))
          \<longrightarrow>
           ((vec_mat_Tensor v (a#M))!j!i) =
                                f
                                         (v!(i div (row_length (a#M))))
                                         ((a#M)!j!(i mod (row_length (a#M)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
proof(cases M)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. M = [] \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
 2. \<And>aa list. M = aa # list \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
M = []

goal (2 subgoals):
 1. M = [] \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
 2. \<And>aa list. M = aa # list \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
have "(length (a#[])) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length [a] = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length [a] = 1

goal (2 subgoals):
 1. M = [] \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
 2. \<And>aa list. M = aa # list \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length [a] = 1
[PROOF STEP]
have "(j<(length (a#[]))) = (j = 0)"
[PROOF STATE]
proof (prove)
using this:
length [a] = 1

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

goal (2 subgoals):
 1. M = [] \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
 2. \<And>aa list. M = aa # list \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(j < length [a]) = (j = 0)
[PROOF STEP]
have "((((i < (row_length (a#[]))*(length v))
               \<and>(j < (length (a#[]))))
               \<and> (mat (row_length (a#[])) (length (a#[])) (a#[]))
                  \<longrightarrow>  ((vec_mat_Tensor v (a#[]))!j!i)
                                 = f
                                    (v!(i div (row_length (a#[]))))
                                     ((a#[])!j!(i mod (row_length (a#[]))))))"
[PROOF STATE]
proof (prove)
using this:
(j < length [a]) = (j = 0)

goal (1 subgoal):
 1. (i < row_length [a] * length v \<and> j < length [a]) \<and> mat (row_length [a]) (length [a]) [a] \<longrightarrow> vec_mat_Tensor v [a] ! j ! i = v ! (i div row_length [a]) * [a] ! j ! (i mod row_length [a])
[PROOF STEP]
using 6 Nil
[PROOF STATE]
proof (prove)
using this:
(j < length [a]) = (j = 0)
j = 0 \<longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
M = []

goal (1 subgoal):
 1. (i < row_length [a] * length v \<and> j < length [a]) \<and> mat (row_length [a]) (length [a]) [a] \<longrightarrow> vec_mat_Tensor v [a] ! j ! i = v ! (i div row_length [a]) * [a] ! j ! (i mod row_length [a])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(i < row_length [a] * length v \<and> j < length [a]) \<and> mat (row_length [a]) (length [a]) [a] \<longrightarrow> vec_mat_Tensor v [a] ! j ! i = v ! (i div row_length [a]) * [a] ! j ! (i mod row_length [a])

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

goal (1 subgoal):
 1. (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
using Nil
[PROOF STATE]
proof (prove)
using this:
(i < row_length [a] * length v \<and> j < length [a]) \<and> mat (row_length [a]) (length [a]) [a] \<longrightarrow> vec_mat_Tensor v [a] ! j ! i = v ! (i div row_length [a]) * [a] ! j ! (i mod row_length [a])
M = []

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

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

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
have 7:"(mat  (row_length (a#b#N))  (length (a#b#N)) (a#b#N))
               \<longrightarrow> row_length (a#b#N) = (row_length (b#N))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> row_length (a # b # N) = row_length (b # N)
[PROOF STEP]
using row_length_eq
[PROOF STATE]
proof (prove)
using this:
mat (row_length (?a # ?b # ?N)) (length (?a # ?b # ?N)) (?a # ?b # ?N) \<longrightarrow> row_length (?a # ?b # ?N) = row_length (?b # ?N)

goal (1 subgoal):
 1. mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> row_length (a # b # N) = row_length (b # N)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> row_length (a # b # N) = row_length (b # N)

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
have 8: "(j>0)
            \<longrightarrow> ((vec_mat_Tensor v (b#N))!(nat ((int j)+-1)))
                                  = (vec_mat_Tensor v (a#b#N))!j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < j \<longrightarrow> vec_mat_Tensor v (b # N) ! nat (int j + - 1) = vec_mat_Tensor v (a # b # N) ! j
[PROOF STEP]
using vec_mat_Tensor.simps(2)
[PROOF STATE]
proof (prove)
using this:
vec_mat_Tensor ?xs (?ys # ?yss) = vec_vec_Tensor ?xs ?ys # vec_mat_Tensor ?xs ?yss

goal (1 subgoal):
 1. 0 < j \<longrightarrow> vec_mat_Tensor v (b # N) ! nat (int j + - 1) = vec_mat_Tensor v (a # b # N) ! j
[PROOF STEP]
using list_int_nat
[PROOF STATE]
proof (prove)
using this:
vec_mat_Tensor ?xs (?ys # ?yss) = vec_vec_Tensor ?xs ?ys # vec_mat_Tensor ?xs ?yss
0 < ?k \<longrightarrow> (?x # ?xs) ! ?k = ?xs ! nat (int ?k + - 1)

goal (1 subgoal):
 1. 0 < j \<longrightarrow> vec_mat_Tensor v (b # N) ! nat (int j + - 1) = vec_mat_Tensor v (a # b # N) ! j
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
0 < j \<longrightarrow> vec_mat_Tensor v (b # N) ! nat (int j + - 1) = vec_mat_Tensor v (a # b # N) ! j

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
have 9: "(j>0)
                 \<longrightarrow> (((i < (row_length (b#N))*(length v))
                    \<and>((nat ((int j)+-1)) < (length (b#N))))
                    \<and>(mat (row_length (b#N)) (length (b#N)) (b#N))
                      \<longrightarrow>
             ((vec_mat_Tensor v (b#N))!(nat ((int j)+-1))!i)
                    = f
                      (v!(i div (row_length (b#N))))
                      ((b#N)!(nat ((int j)+-1))!(i mod (row_length (b#N)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < j \<longrightarrow> (i < row_length (b # N) * length v \<and> nat (int j + - 1) < length (b # N)) \<and> mat (row_length (b # N)) (length (b # N)) (b # N) \<longrightarrow> vec_mat_Tensor v (b # N) ! nat (int j + - 1) ! i = v ! (i div row_length (b # N)) * (b # N) ! nat (int j + - 1) ! (i mod row_length (b # N))
[PROOF STEP]
using Cons.hyps Cons mult.commute
[PROOF STATE]
proof (prove)
using this:
(?i < length v * row_length M \<and> ?j < length M) \<and> mat (row_length M) (length M) M \<longrightarrow> vec_mat_Tensor v M ! ?j ! ?i = v ! (?i div row_length M) * M ! ?j ! (?i mod row_length M)
M = b # N
?a * ?b = ?b * ?a

goal (1 subgoal):
 1. 0 < j \<longrightarrow> (i < row_length (b # N) * length v \<and> nat (int j + - 1) < length (b # N)) \<and> mat (row_length (b # N)) (length (b # N)) (b # N) \<longrightarrow> vec_mat_Tensor v (b # N) ! nat (int j + - 1) ! i = v ! (i div row_length (b # N)) * (b # N) ! nat (int j + - 1) ! (i mod row_length (b # N))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
0 < j \<longrightarrow> (i < row_length (b # N) * length v \<and> nat (int j + - 1) < length (b # N)) \<and> mat (row_length (b # N)) (length (b # N)) (b # N) \<longrightarrow> vec_mat_Tensor v (b # N) ! nat (int j + - 1) ! i = v ! (i div row_length (b # N)) * (b # N) ! nat (int j + - 1) ! (i mod row_length (b # N))

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
have "(j>0) \<longrightarrow> ((nat ((int j) + -1)) < (length (b#N)))
                           \<longrightarrow> ((nat ((int j) + -1) + 1) < length (a#b#N))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < j \<longrightarrow> nat (int j + - 1) < length (b # N) \<longrightarrow> nat (int j + - 1) + 1 < length (a # b # N)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < j \<longrightarrow> nat (int j + - 1) < length (b # N) \<longrightarrow> nat (int j + - 1) + 1 < length (a # b # N)

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < j \<longrightarrow> nat (int j + - 1) < length (b # N) \<longrightarrow> nat (int j + - 1) + 1 < length (a # b # N)
[PROOF STEP]
have
           "(j>0)
                 \<longrightarrow> ((nat ((int j) + -1)) < (length (b#N))) = (j < length (a#b#N))"
[PROOF STATE]
proof (prove)
using this:
0 < j \<longrightarrow> nat (int j + - 1) < length (b # N) \<longrightarrow> nat (int j + - 1) + 1 < length (a # b # N)

goal (1 subgoal):
 1. 0 < j \<longrightarrow> (nat (int j + - 1) < length (b # N)) = (j < length (a # b # N))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < j \<longrightarrow> (nat (int j + - 1) < length (b # N)) = (j < length (a # b # N))

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < j \<longrightarrow> (nat (int j + - 1) < length (b # N)) = (j < length (a # b # N))
[PROOF STEP]
have
         "(j>0)
          \<longrightarrow> (((i < (row_length (b#N))*(length v)) \<and> (j < length (a#b#N)))
              \<and>(mat (row_length (b#N)) (length (b#N)) (b#N))   \<longrightarrow>
                    ((vec_mat_Tensor v (b#N))!(nat ((int j)+-1))!i)
            = f
                (v!(i div (row_length (b#N))))
                ((b#N)!(nat ((int j)+-1))!(i mod (row_length (b#N)))))"
[PROOF STATE]
proof (prove)
using this:
0 < j \<longrightarrow> (nat (int j + - 1) < length (b # N)) = (j < length (a # b # N))

goal (1 subgoal):
 1. 0 < j \<longrightarrow> (i < row_length (b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (b # N)) (length (b # N)) (b # N) \<longrightarrow> vec_mat_Tensor v (b # N) ! nat (int j + - 1) ! i = v ! (i div row_length (b # N)) * (b # N) ! nat (int j + - 1) ! (i mod row_length (b # N))
[PROOF STEP]
using Cons.hyps Cons mult.commute
[PROOF STATE]
proof (prove)
using this:
0 < j \<longrightarrow> (nat (int j + - 1) < length (b # N)) = (j < length (a # b # N))
(?i < length v * row_length M \<and> ?j < length M) \<and> mat (row_length M) (length M) M \<longrightarrow> vec_mat_Tensor v M ! ?j ! ?i = v ! (?i div row_length M) * M ! ?j ! (?i mod row_length M)
M = b # N
?a * ?b = ?b * ?a

goal (1 subgoal):
 1. 0 < j \<longrightarrow> (i < row_length (b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (b # N)) (length (b # N)) (b # N) \<longrightarrow> vec_mat_Tensor v (b # N) ! nat (int j + - 1) ! i = v ! (i div row_length (b # N)) * (b # N) ! nat (int j + - 1) ! (i mod row_length (b # N))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
0 < j \<longrightarrow> (i < row_length (b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (b # N)) (length (b # N)) (b # N) \<longrightarrow> vec_mat_Tensor v (b # N) ! nat (int j + - 1) ! i = v ! (i div row_length (b # N)) * (b # N) ! nat (int j + - 1) ! (i mod row_length (b # N))

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
with 8
[PROOF STATE]
proof (chain)
picking this:
0 < j \<longrightarrow> vec_mat_Tensor v (b # N) ! nat (int j + - 1) = vec_mat_Tensor v (a # b # N) ! j
0 < j \<longrightarrow> (i < row_length (b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (b # N)) (length (b # N)) (b # N) \<longrightarrow> vec_mat_Tensor v (b # N) ! nat (int j + - 1) ! i = v ! (i div row_length (b # N)) * (b # N) ! nat (int j + - 1) ! (i mod row_length (b # N))
[PROOF STEP]
have "(j>0)
                 \<longrightarrow> (((i < (row_length (b#N))*(length v))
                     \<and> (j < length (a#b#N)))
                     \<and> (mat (row_length (b#N)) (length (b#N)) (b#N))
                      \<longrightarrow>
         ((vec_mat_Tensor v (a#b#N))!j!i)
                = f
                    (v!(i div (row_length (b#N))))
                    ((b#N)!(nat ((int j)+-1))!(i mod (row_length (b#N)))))"
[PROOF STATE]
proof (prove)
using this:
0 < j \<longrightarrow> vec_mat_Tensor v (b # N) ! nat (int j + - 1) = vec_mat_Tensor v (a # b # N) ! j
0 < j \<longrightarrow> (i < row_length (b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (b # N)) (length (b # N)) (b # N) \<longrightarrow> vec_mat_Tensor v (b # N) ! nat (int j + - 1) ! i = v ! (i div row_length (b # N)) * (b # N) ! nat (int j + - 1) ! (i mod row_length (b # N))

goal (1 subgoal):
 1. 0 < j \<longrightarrow> (i < row_length (b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (b # N)) (length (b # N)) (b # N) \<longrightarrow> vec_mat_Tensor v (a # b # N) ! j ! i = v ! (i div row_length (b # N)) * (b # N) ! nat (int j + - 1) ! (i mod row_length (b # N))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < j \<longrightarrow> (i < row_length (b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (b # N)) (length (b # N)) (b # N) \<longrightarrow> vec_mat_Tensor v (a # b # N) ! j ! i = v ! (i div row_length (b # N)) * (b # N) ! nat (int j + - 1) ! (i mod row_length (b # N))

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 < j \<longrightarrow> (i < row_length (b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (b # N)) (length (b # N)) (b # N) \<longrightarrow> vec_mat_Tensor v (a # b # N) ! j ! i = v ! (i div row_length (b # N)) * (b # N) ! nat (int j + - 1) ! (i mod row_length (b # N))

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
have "(j>0) \<longrightarrow> (b#N)!(nat ((int j)+-1)) = (a#b#N)!j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < j \<longrightarrow> (b # N) ! nat (int j + - 1) = (a # b # N) ! j
[PROOF STEP]
using list_int_nat
[PROOF STATE]
proof (prove)
using this:
0 < ?k \<longrightarrow> (?x # ?xs) ! ?k = ?xs ! nat (int ?k + - 1)

goal (1 subgoal):
 1. 0 < j \<longrightarrow> (b # N) ! nat (int j + - 1) = (a # b # N) ! j
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
0 < j \<longrightarrow> (b # N) ! nat (int j + - 1) = (a # b # N) ! j

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < j \<longrightarrow> (b # N) ! nat (int j + - 1) = (a # b # N) ! j

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
have " (j>0) \<longrightarrow>
                    (((i < (row_length (b#N))*(length v))
                   \<and> (j < length (a#b#N)))
                   \<and> (mat (row_length (b#N)) (length (b#N)) (b#N))
                     \<longrightarrow>
                         ((vec_mat_Tensor v (a#b#N))!j!i)
                                  = f
                                      (v!(i div (row_length (b#N))))
                                      ((a#b#N)!j!(i mod (row_length (b#N)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < j \<longrightarrow> (i < row_length (b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (b # N)) (length (b # N)) (b # N) \<longrightarrow> vec_mat_Tensor v (a # b # N) ! j ! i = v ! (i div row_length (b # N)) * (a # b # N) ! j ! (i mod row_length (b # N))
[PROOF STEP]
by (metis calculation(1) calculation(2))
[PROOF STATE]
proof (state)
this:
0 < j \<longrightarrow> (i < row_length (b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (b # N)) (length (b # N)) (b # N) \<longrightarrow> vec_mat_Tensor v (a # b # N) ! j ! i = v ! (i div row_length (b # N)) * (a # b # N) ! j ! (i mod row_length (b # N))

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < j \<longrightarrow> (i < row_length (b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (b # N)) (length (b # N)) (b # N) \<longrightarrow> vec_mat_Tensor v (a # b # N) ! j ! i = v ! (i div row_length (b # N)) * (a # b # N) ! j ! (i mod row_length (b # N))
[PROOF STEP]
have
           "(j>0)
             \<longrightarrow> (((i < (row_length (b#N))*(length v))
                 \<and> (j < length (a#b#N)))
                 \<and> (mat (row_length (a#b#N)) (length (a#b#N)) (a#b#N))
                 \<longrightarrow>
                        ((vec_mat_Tensor v (a#b#N))!j!i)
                              = f
                                    (v!(i div (row_length (b#N))))
                                    ((a#b#N)!j!(i mod (row_length (b#N)))))"
[PROOF STATE]
proof (prove)
using this:
0 < j \<longrightarrow> (i < row_length (b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (b # N)) (length (b # N)) (b # N) \<longrightarrow> vec_mat_Tensor v (a # b # N) ! j ! i = v ! (i div row_length (b # N)) * (a # b # N) ! j ! (i mod row_length (b # N))

goal (1 subgoal):
 1. 0 < j \<longrightarrow> (i < row_length (b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> vec_mat_Tensor v (a # b # N) ! j ! i = v ! (i div row_length (b # N)) * (a # b # N) ! j ! (i mod row_length (b # N))
[PROOF STEP]
using reduct_matrix
[PROOF STATE]
proof (prove)
using this:
0 < j \<longrightarrow> (i < row_length (b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (b # N)) (length (b # N)) (b # N) \<longrightarrow> vec_mat_Tensor v (a # b # N) ! j ! i = v ! (i div row_length (b # N)) * (a # b # N) ! j ! (i mod row_length (b # N))
mat (row_length (?a # ?M)) (length (?a # ?M)) (?a # ?M) \<Longrightarrow> mat (row_length ?M) (length ?M) ?M

goal (1 subgoal):
 1. 0 < j \<longrightarrow> (i < row_length (b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> vec_mat_Tensor v (a # b # N) ! j ! i = v ! (i div row_length (b # N)) * (a # b # N) ! j ! (i mod row_length (b # N))
[PROOF STEP]
by (metis)
[PROOF STATE]
proof (state)
this:
0 < j \<longrightarrow> (i < row_length (b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> vec_mat_Tensor v (a # b # N) ! j ! i = v ! (i div row_length (b # N)) * (a # b # N) ! j ! (i mod row_length (b # N))

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < j \<longrightarrow> (i < row_length (b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> vec_mat_Tensor v (a # b # N) ! j ! i = v ! (i div row_length (b # N)) * (a # b # N) ! j ! (i mod row_length (b # N))

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
have "(mat (row_length (a#b#N)) (length (a#b#N)) (a#b#N))
                   \<longrightarrow>(row_length (b#N)) = (row_length (a#b#N))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> row_length (b # N) = row_length (a # b # N)
[PROOF STEP]
by (metis "7" Cons)
[PROOF STATE]
proof (state)
this:
mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> row_length (b # N) = row_length (a # b # N)

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> row_length (b # N) = row_length (a # b # N)

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
have 10:"(j>0)
                     \<longrightarrow> (((i < (row_length (a#b#N))*(length v))
                        \<and>(j < length (a#b#N)))
                        \<and>(mat (row_length (a#b#N)) (length (a#b#N)) (a#b#N))   \<longrightarrow>
                         ((vec_mat_Tensor v (a#b#N))!j!i)
                                = f (v!(i div (row_length (a#b#N))))
                                    ((a#b#N)!j!(i mod (row_length (a#b#N)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < j \<longrightarrow> (i < row_length (a # b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> vec_mat_Tensor v (a # b # N) ! j ! i = v ! (i div row_length (a # b # N)) * (a # b # N) ! j ! (i mod row_length (a # b # N))
[PROOF STEP]
by (metis calculation(3) calculation(4))
[PROOF STATE]
proof (state)
this:
0 < j \<longrightarrow> (i < row_length (a # b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> vec_mat_Tensor v (a # b # N) ! j ! i = v ! (i div row_length (a # b # N)) * (a # b # N) ! j ! (i mod row_length (a # b # N))

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
have "(j = 0) \<or> (j > 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j = 0 \<or> 0 < j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j = 0 \<or> 0 < j

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
with 6 10 logic
[PROOF STATE]
proof (chain)
picking this:
j = 0 \<longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
0 < j \<longrightarrow> (i < row_length (a # b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> vec_mat_Tensor v (a # b # N) ! j ! i = v ! (i div row_length (a # b # N)) * (a # b # N) ! j ! (i mod row_length (a # b # N))
\<lbrakk>?A \<longrightarrow> ?B; \<not> ?A \<longrightarrow> ?B\<rbrakk> \<Longrightarrow> ?B
j = 0 \<or> 0 < j
[PROOF STEP]
have
            "(((i < (row_length (a#b#N))*(length v))
            \<and> (j < length (a#b#N)))
            \<and> (mat (row_length (a#b#N)) (length (a#b#N)) (a#b#N))
            \<longrightarrow>
                ((vec_mat_Tensor v (a#b#N))!j!i)
                      = f
                          (v!(i div (row_length (a#b#N))))
                          ((a#b#N)!j!(i mod (row_length (a#b#N)))))"
[PROOF STATE]
proof (prove)
using this:
j = 0 \<longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
0 < j \<longrightarrow> (i < row_length (a # b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> vec_mat_Tensor v (a # b # N) ! j ! i = v ! (i div row_length (a # b # N)) * (a # b # N) ! j ! (i mod row_length (a # b # N))
\<lbrakk>?A \<longrightarrow> ?B; \<not> ?A \<longrightarrow> ?B\<rbrakk> \<Longrightarrow> ?B
j = 0 \<or> 0 < j

goal (1 subgoal):
 1. (i < row_length (a # b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> vec_mat_Tensor v (a # b # N) ! j ! i = v ! (i div row_length (a # b # N)) * (a # b # N) ! j ! (i mod row_length (a # b # N))
[PROOF STEP]
using  Cons
[PROOF STATE]
proof (prove)
using this:
j = 0 \<longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
0 < j \<longrightarrow> (i < row_length (a # b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> vec_mat_Tensor v (a # b # N) ! j ! i = v ! (i div row_length (a # b # N)) * (a # b # N) ! j ! (i mod row_length (a # b # N))
\<lbrakk>?A \<longrightarrow> ?B; \<not> ?A \<longrightarrow> ?B\<rbrakk> \<Longrightarrow> ?B
j = 0 \<or> 0 < j
M = b # N

goal (1 subgoal):
 1. (i < row_length (a # b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> vec_mat_Tensor v (a # b # N) ! j ! i = v ! (i div row_length (a # b # N)) * (a # b # N) ! j ! (i mod row_length (a # b # N))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(i < row_length (a # b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> vec_mat_Tensor v (a # b # N) ! j ! i = v ! (i div row_length (a # b # N)) * (a # b # N) ! j ! (i mod row_length (a # b # N))

goal (1 subgoal):
 1. \<And>aa list. M = aa # list \<Longrightarrow> (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(i < row_length (a # b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> vec_mat_Tensor v (a # b # N) ! j ! i = v ! (i div row_length (a # b # N)) * (a # b # N) ! j ! (i mod row_length (a # b # N))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(i < row_length (a # b # N) * length v \<and> j < length (a # b # N)) \<and> mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> vec_mat_Tensor v (a # b # N) ! j ! i = v ! (i div row_length (a # b # N)) * (a # b # N) ! j ! (i mod row_length (a # b # N))

goal (1 subgoal):
 1. (i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
by (metis Cons)
[PROOF STATE]
proof (state)
this:
(i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(i < row_length (a # M) * length v \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))

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

goal (1 subgoal):
 1. (i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))
[PROOF STEP]
by (metis mult.commute)
[PROOF STATE]
proof (state)
this:
(i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(i < length v * row_length (a # M) \<and> j < length (a # M)) \<and> mat (row_length (a # M)) (length (a # M)) (a # M) \<longrightarrow> vec_mat_Tensor v (a # M) ! j ! i = v ! (i div row_length (a # M)) * (a # M) ! j ! (i mod row_length (a # M))

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

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

goal:
No subgoals!
[PROOF STEP]
qed