[STATEMENT]
theorem vec_vec_Tensor_elements:
 assumes " (y \<noteq> [])"
 shows
   "\<forall>i.((i<((length x)*(length y)))
       \<longrightarrow> ((vec_vec_Tensor x y)!i)
             = f (x!(i div (length y))) (y!(i mod (length y))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<length x * length y. vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
apply(rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
proof(induct x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i < length [] * length y \<longrightarrow> vec_vec_Tensor [] y ! i = [] ! (i div length y) * y ! (i mod length y)
 2. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

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

goal (2 subgoals):
 1. \<And>i. i < length [] * length y \<longrightarrow> vec_vec_Tensor [] y ! i = [] ! (i div length y) * y ! (i mod length y)
 2. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length [] = 0

goal (2 subgoals):
 1. \<And>i. i < length [] * length y \<longrightarrow> vec_vec_Tensor [] y ! i = [] ! (i div length y) * y ! (i mod length y)
 2. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have "length (vec_vec_Tensor [] y) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (vec_vec_Tensor [] y) = 0
[PROOF STEP]
using vec_vec_Tensor.simps(1)
[PROOF STATE]
proof (prove)
using this:
vec_vec_Tensor [] ?ys = []

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

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

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

goal (2 subgoals):
 1. \<And>i. i < length [] * length y \<longrightarrow> vec_vec_Tensor [] y ! i = [] ! (i div length y) * y ! (i mod length y)
 2. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i < length (vec_vec_Tensor [] y) \<Longrightarrow> False

goal (2 subgoals):
 1. \<And>i. i < length [] * length y \<longrightarrow> vec_vec_Tensor [] y ! i = [] ! (i div length y) * y ! (i mod length y)
 2. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have "(vec_vec_Tensor [] y) = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_vec_Tensor [] y = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec_vec_Tensor [] y = []

goal (2 subgoals):
 1. \<And>i. i < length [] * length y \<longrightarrow> vec_vec_Tensor [] y ! i = [] ! (i div length y) * y ! (i mod length y)
 2. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vec_vec_Tensor [] y = []

goal (2 subgoals):
 1. \<And>i. i < length [] * length y \<longrightarrow> vec_vec_Tensor [] y ! i = [] ! (i div length y) * y ! (i mod length y)
 2. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have
   "(i<(length (vec_vec_Tensor [] y))) \<longrightarrow>
   ((vec_vec_Tensor x y)!i) = f (x!(i div (length y))) (y!(i mod (length y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length (vec_vec_Tensor [] y) \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length (vec_vec_Tensor [] y) \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)

goal (2 subgoals):
 1. \<And>i. i < length [] * length y \<longrightarrow> vec_vec_Tensor [] y ! i = [] ! (i div length y) * y ! (i mod length y)
 2. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length (vec_vec_Tensor [] y) \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i < length (vec_vec_Tensor [] y) \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)

goal (1 subgoal):
 1. i < length [] * length y \<longrightarrow> vec_vec_Tensor [] y ! i = [] ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length [] * length y \<longrightarrow> vec_vec_Tensor [] y ! i = [] ! (i div length y) * y ! (i mod length y)

goal (1 subgoal):
 1. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
case (Cons z zs)
[PROOF STATE]
proof (state)
this:
?i < length zs * length y \<longrightarrow> vec_vec_Tensor zs y ! ?i = zs ! (?i div length y) * y ! (?i mod length y)

goal (1 subgoal):
 1. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have 1:"vec_vec_Tensor (z#zs) y = (times z y)@(vec_vec_Tensor zs y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_vec_Tensor (z # zs) y = local.times z y @ vec_vec_Tensor zs y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec_vec_Tensor (z # zs) y = local.times z y @ vec_vec_Tensor zs y

goal (1 subgoal):
 1. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have 2:"i<(length y)\<longrightarrow>((times z y)!i = f z (y!i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length y \<longrightarrow> local.times z y ! i = z * y ! i
[PROOF STEP]
using times_elements
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length ?v. local.times ?a ?v ! i = ?a * ?v ! i

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

goal (1 subgoal):
 1. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i < length y \<longrightarrow> local.times z y ! i = z * y ! i

goal (1 subgoal):
 1. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have 3:
        "i<(length y)
           \<longrightarrow> (vec_vec_Tensor (z#zs) y)!i = (times z y)!i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = local.times z y ! i
[PROOF STEP]
using vec_vec_Tensor_simpl
[PROOF STATE]
proof (prove)
using this:
?i < length ?y \<longrightarrow> vec_vec_Tensor (?z # ?zs) ?y ! ?i = local.times ?z ?y ! ?i

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

goal (1 subgoal):
 1. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i < length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = local.times z y ! i

goal (1 subgoal):
 1. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have 35:
           "i<(length y) \<longrightarrow> (vec_vec_Tensor (z#zs) y)!i = f z (y!i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = z * y ! i
[PROOF STEP]
using calculation(1) calculation(2)
[PROOF STATE]
proof (prove)
using this:
i < length y \<longrightarrow> local.times z y ! i = z * y ! i
i < length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = local.times z y ! i

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

goal (1 subgoal):
 1. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have 4:"(y \<noteq> []) \<longrightarrow> (length y) >0 "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<noteq> [] \<longrightarrow> 0 < length y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<noteq> [] \<longrightarrow> 0 < length y

goal (1 subgoal):
 1. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have "(i <(length y)) \<longrightarrow>  ((i div (length y)) = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length y \<longrightarrow> i div length y = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length y \<longrightarrow> i div length y = 0

goal (1 subgoal):
 1. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length y \<longrightarrow> i div length y = 0
[PROOF STEP]
have  6:"(i <(length y)) \<longrightarrow> (z#zs)!(i div (length y)) = z"
[PROOF STATE]
proof (prove)
using this:
i < length y \<longrightarrow> i div length y = 0

goal (1 subgoal):
 1. i < length y \<longrightarrow> (z # zs) ! (i div length y) = z
[PROOF STEP]
using nth_Cons_0
[PROOF STATE]
proof (prove)
using this:
i < length y \<longrightarrow> i div length y = 0
(?x # ?xs) ! 0 = ?x

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

goal (1 subgoal):
 1. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length y \<longrightarrow> (z # zs) ! (i div length y) = z
[PROOF STEP]
have 7:"(i <(length y)) \<longrightarrow> (i mod (length y)) = i"
[PROOF STATE]
proof (prove)
using this:
i < length y \<longrightarrow> (z # zs) ! (i div length y) = z

goal (1 subgoal):
 1. i < length y \<longrightarrow> i mod length y = i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length y \<longrightarrow> i mod length y = i

goal (1 subgoal):
 1. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
with 2 6
[PROOF STATE]
proof (chain)
picking this:
i < length y \<longrightarrow> local.times z y ! i = z * y ! i
i < length y \<longrightarrow> (z # zs) ! (i div length y) = z
i < length y \<longrightarrow> i mod length y = i
[PROOF STEP]
have "(i < (length y))
        \<longrightarrow> (times z y)!i
                 = f  ((z#zs)!(i div (length y))) (y! (i mod (length y)))"
[PROOF STATE]
proof (prove)
using this:
i < length y \<longrightarrow> local.times z y ! i = z * y ! i
i < length y \<longrightarrow> (z # zs) ! (i div length y) = z
i < length y \<longrightarrow> i mod length y = i

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

goal (1 subgoal):
 1. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
with 3
[PROOF STATE]
proof (chain)
picking this:
i < length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = local.times z y ! i
i < length y \<longrightarrow> local.times z y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have step1:
      "((i < (length y))
          \<longrightarrow> ((i<((length x)*(length y))
          \<longrightarrow> ((vec_vec_Tensor (z#zs) y)!i
                      =  f
                             ((z#zs)!(i div (length y)))
                              (y! (i mod (length y)))))))"
[PROOF STATE]
proof (prove)
using this:
i < length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = local.times z y ! i
i < length y \<longrightarrow> local.times z y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)

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

goal (1 subgoal):
 1. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have "((length y) \<le> i) \<longrightarrow> (i - (length y)) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length y \<le> i \<longrightarrow> 0 \<le> i - length y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length y \<le> i \<longrightarrow> 0 \<le> i - length y

goal (1 subgoal):
 1. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have step2:
        "((length y) < i)
           \<longrightarrow> ((i < (length (z#zs)*(length y)))
           \<longrightarrow>((vec_vec_Tensor (z#zs) y)!i)
                          = f
                              ((z#zs)!(i div (length y)))
                              (y!(i mod (length y))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length y < i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length y < i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have "(length y)>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < length y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
y \<noteq> []

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

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

goal (1 subgoal):
 1. length y < i \<longrightarrow> i div length y = (i - length y) div length y + 1
[PROOF STEP]
using nat_div
[PROOF STATE]
proof (prove)
using this:
0 < length y
\<lbrakk>0 < ?b; ?b < ?a\<rbrakk> \<Longrightarrow> ?a div ?b = (?a - ?b) div ?b + 1

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

goal (1 subgoal):
 1. length y < i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have "zs!j = (z#zs)!(j+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zs ! j = (z # zs) ! (j + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
zs ! j = (z # zs) ! (j + 1)

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

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

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

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

goal (1 subgoal):
 1. length y < i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have "(i > (length y))
               \<longrightarrow>((i mod (length y))
                                 = ((i - (length y)) mod (length y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length y < i \<longrightarrow> i mod length y = (i - length y) mod length y
[PROOF STEP]
using nat_mod
[PROOF STATE]
proof (prove)
using this:
?n < ?m \<Longrightarrow> ?m mod ?n = (?m - ?n) mod ?n

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

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

goal (1 subgoal):
 1. length y < i \<longrightarrow> y ! (i mod length y) = y ! ((i - length y) mod length y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length y < i \<longrightarrow> y ! (i mod length y) = y ! ((i - length y) mod length y)

goal (1 subgoal):
 1. length y < i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have 4:"(i > (length y))
                       \<longrightarrow>(vec_vec_Tensor (z#zs) y)!i
                                = (vec_vec_Tensor zs y)!(i- (length y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length y < i \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = vec_vec_Tensor zs y ! (i - length y)
[PROOF STEP]
using vec_vec_Tensor_simpl2
[PROOF STATE]
proof (prove)
using this:
length ?y \<le> ?i \<longrightarrow> vec_vec_Tensor (?z # ?zs) ?y ! ?i = vec_vec_Tensor ?zs ?y ! (?i - length ?y)

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

goal (1 subgoal):
 1. length y < i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have 5: "(i > (length y))
                 \<longrightarrow>((i <((length (z#zs))*(length y))))
                          = (i - (length y)< (length zs)*(length y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length y < i \<longrightarrow> (i < length (z # zs) * length y) = (i - length y < length zs * length y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length y < i \<longrightarrow> (i < length (z # zs) * length y) = (i - length y < length zs * length y)

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

goal (1 subgoal):
 1. \<forall>i<length zs * length y. vec_vec_Tensor zs y ! i = zs ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
using Cons.hyps
[PROOF STATE]
proof (prove)
using this:
length y < i \<longrightarrow> (i < length (z # zs) * length y) = (i - length y < length zs * length y)
?i < length zs * length y \<longrightarrow> vec_vec_Tensor zs y ! ?i = zs ! (?i div length y) * y ! (?i mod length y)

goal (1 subgoal):
 1. \<forall>i<length zs * length y. vec_vec_Tensor zs y ! i = zs ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i<length zs * length y. vec_vec_Tensor zs y ! i = zs ! (i div length y) * y ! (i mod length y)

goal (1 subgoal):
 1. length y < i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
with 5
[PROOF STATE]
proof (chain)
picking this:
length y < i \<longrightarrow> (i < length (z # zs) * length y) = (i - length y < length zs * length y)
\<forall>i<length zs * length y. vec_vec_Tensor zs y ! i = zs ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have "(i > (length y))
                       \<longrightarrow> ((i<((length (z#zs))*(length y)))
                       \<longrightarrow> ((vec_vec_Tensor zs y)!(i -(length y)))
                               = f
                                  (zs!((i -(length y)) div (length y)))
                                  (y!((i -(length y)) mod (length y))))
                                   = ((i<((length zs)*(length y)))
                                      \<longrightarrow> ((vec_vec_Tensor zs y)!i)
                                                = f
                                                    (zs!(i div (length y)))
                                                    (y!(i mod (length y))))"
[PROOF STATE]
proof (prove)
using this:
length y < i \<longrightarrow> (i < length (z # zs) * length y) = (i - length y < length zs * length y)
\<forall>i<length zs * length y. vec_vec_Tensor zs y ! i = zs ! (i div length y) * y ! (i mod length y)

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

goal (1 subgoal):
 1. length y < i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
with 6
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length zs * length y. vec_vec_Tensor zs y ! i = zs ! (i div length y) * y ! (i mod length y)
length y < i \<longrightarrow> (i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor zs y ! (i - length y) = zs ! ((i - length y) div length y) * y ! ((i - length y) mod length y)) = (i < length zs * length y \<longrightarrow> vec_vec_Tensor zs y ! i = zs ! (i div length y) * y ! (i mod length y))
[PROOF STEP]
have
           "(i > (length y))
                \<longrightarrow>((i<((length (z#zs))*(length y)))
                \<longrightarrow> ((vec_vec_Tensor zs y)!(i -(length y)))
                            = f
                               (zs!((i -(length y)) div (length y)))
                               (y!((i -(length y))  mod (length y))))"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length zs * length y. vec_vec_Tensor zs y ! i = zs ! (i div length y) * y ! (i mod length y)
length y < i \<longrightarrow> (i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor zs y ! (i - length y) = zs ! ((i - length y) div length y) * y ! ((i - length y) mod length y)) = (i < length zs * length y \<longrightarrow> vec_vec_Tensor zs y ! i = zs ! (i div length y) * y ! (i mod length y))

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

goal (1 subgoal):
 1. length y < i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
with 2 3 4
[PROOF STATE]
proof (chain)
picking this:
length y < i \<longrightarrow> zs ! ((i - length y) div length y) = (z # zs) ! (i div length y)
length y < i \<longrightarrow> y ! (i mod length y) = y ! ((i - length y) mod length y)
length y < i \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = vec_vec_Tensor zs y ! (i - length y)
length y < i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor zs y ! (i - length y) = zs ! ((i - length y) div length y) * y ! ((i - length y) mod length y)
[PROOF STEP]
have
            "(i > (length y))
                \<longrightarrow>((i<((length (z#zs))*(length y)))
                \<longrightarrow>((vec_vec_Tensor (z#zs) y)!i)
                         =  f
                               ((z#zs)!(i div (length y)))
                               (y!(i mod (length y))))"
[PROOF STATE]
proof (prove)
using this:
length y < i \<longrightarrow> zs ! ((i - length y) div length y) = (z # zs) ! (i div length y)
length y < i \<longrightarrow> y ! (i mod length y) = y ! ((i - length y) mod length y)
length y < i \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = vec_vec_Tensor zs y ! (i - length y)
length y < i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor zs y ! (i - length y) = zs ! ((i - length y) div length y) * y ! ((i - length y) mod length y)

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length y < i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)

goal (1 subgoal):
 1. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have "((length y) = i)
                     \<longrightarrow> ((i < (length (z#zs)*(length y)))
                     \<longrightarrow> ((vec_vec_Tensor (z#zs) y)!i)
                                          = f
                                              ((z#zs)!(i div (length y)))
                                              (y!(i mod (length y))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length y = i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length y = i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have 1:"(i = (length y))
                  \<longrightarrow> ((vec_vec_Tensor (z#zs) y)!i)
                                        = (vec_vec_Tensor zs y)!0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = vec_vec_Tensor zs y ! 0
[PROOF STEP]
using vec_vec_Tensor_simpl2
[PROOF STATE]
proof (prove)
using this:
length ?y \<le> ?i \<longrightarrow> vec_vec_Tensor (?z # ?zs) ?y ! ?i = vec_vec_Tensor ?zs ?y ! (?i - length ?y)

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

goal (1 subgoal):
 1. length y = i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have 2:"(i = length y) \<longrightarrow> (i mod (length y)) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = length y \<longrightarrow> i mod length y = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i = length y \<longrightarrow> i mod length y = 0

goal (1 subgoal):
 1. length y = i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have 3:"(i = length y) \<longrightarrow> (i div (length y)) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = length y \<longrightarrow> i div length y = 1
[PROOF STEP]
using 4 assms div_self less_numeral_extra(3)
[PROOF STATE]
proof (prove)
using this:
y \<noteq> [] \<longrightarrow> 0 < length y
y \<noteq> []
?a \<noteq> (0::?'a) \<Longrightarrow> ?a div ?a = (1::?'a)
\<not> (0::?'a) < (0::?'a)

goal (1 subgoal):
 1. i = length y \<longrightarrow> i div length y = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i = length y \<longrightarrow> i div length y = 1

goal (1 subgoal):
 1. length y = i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have 4: "(i = length y)
                  \<longrightarrow> ((i < (length (z#zs))*(length y))
                               = (0 < (length zs)*(length y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = length y \<longrightarrow> (i < length (z # zs) * length y) = (0 < length zs * length y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i = length y \<longrightarrow> (i < length (z # zs) * length y) = (0 < length zs * length y)

goal (1 subgoal):
 1. length y = i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have "(z#zs)!1 = (zs!0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z # zs) ! 1 = zs ! 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(z # zs) ! 1 = zs ! 0

goal (1 subgoal):
 1. length y = i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
with 3
[PROOF STATE]
proof (chain)
picking this:
i = length y \<longrightarrow> i div length y = 1
(z # zs) ! 1 = zs ! 0
[PROOF STEP]
have 5:" (i = length y)
                              \<longrightarrow> ((z#zs)!(i div (length y))) = (zs!0)"
[PROOF STATE]
proof (prove)
using this:
i = length y \<longrightarrow> i div length y = 1
(z # zs) ! 1 = zs ! 0

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

goal (1 subgoal):
 1. length y = i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have " \<forall>i.((i < (length zs)*(length y))
                               \<longrightarrow>((vec_vec_Tensor (zs) y)!i)
                                             = f
                                                 ((zs)!(i div (length y)))
                                                 (y!(i mod (length y))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<length zs * length y. vec_vec_Tensor zs y ! i = zs ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
using Cons.hyps
[PROOF STATE]
proof (prove)
using this:
?i < length zs * length y \<longrightarrow> vec_vec_Tensor zs y ! ?i = zs ! (?i div length y) * y ! (?i mod length y)

goal (1 subgoal):
 1. \<forall>i<length zs * length y. vec_vec_Tensor zs y ! i = zs ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i<length zs * length y. vec_vec_Tensor zs y ! i = zs ! (i div length y) * y ! (i mod length y)

goal (1 subgoal):
 1. length y = i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
with 4
[PROOF STATE]
proof (chain)
picking this:
i = length y \<longrightarrow> (i < length (z # zs) * length y) = (0 < length zs * length y)
\<forall>i<length zs * length y. vec_vec_Tensor zs y ! i = zs ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have 6:"(i = length y)
                           \<longrightarrow> ((0 < ((length zs)*(length y)))
                              \<longrightarrow> (((vec_vec_Tensor (zs) y)!0)
                                       = f ((zs)!0) (y!0)))
                                         = ((i < ((length zs)*(length y)))
                                               \<longrightarrow>(((vec_vec_Tensor zs y)!i)
                                                = f
                                                    ((zs)!(i div (length y)))
                                                    (y!(i mod (length y)))))"
[PROOF STATE]
proof (prove)
using this:
i = length y \<longrightarrow> (i < length (z # zs) * length y) = (0 < length zs * length y)
\<forall>i<length zs * length y. vec_vec_Tensor zs y ! i = zs ! (i div length y) * y ! (i mod length y)

goal (1 subgoal):
 1. i = length y \<longrightarrow> (0 < length zs * length y \<longrightarrow> vec_vec_Tensor zs y ! 0 = zs ! 0 * y ! 0) = (i < length zs * length y \<longrightarrow> vec_vec_Tensor zs y ! i = zs ! (i div length y) * y ! (i mod length y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i = length y \<longrightarrow> (0 < length zs * length y \<longrightarrow> vec_vec_Tensor zs y ! 0 = zs ! 0 * y ! 0) = (i < length zs * length y \<longrightarrow> vec_vec_Tensor zs y ! i = zs ! (i div length y) * y ! (i mod length y))

goal (1 subgoal):
 1. length y = i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have 7: "(0 div (length y)) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 div length y = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 div length y = 0

goal (1 subgoal):
 1. length y = i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have 8: " (0 mod (length y)) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 mod length y = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 mod length y = 0

goal (1 subgoal):
 1. length y = i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have 9: "(0 < ((length zs)*(length y)))
                       \<longrightarrow> ((vec_vec_Tensor zs y)!0)
                                           = f (zs!0) (y!0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < length zs * length y \<longrightarrow> vec_vec_Tensor zs y ! 0 = zs ! 0 * y ! 0
[PROOF STEP]
using 7 8 Cons.hyps
[PROOF STATE]
proof (prove)
using this:
0 div length y = 0
0 mod length y = 0
?i < length zs * length y \<longrightarrow> vec_vec_Tensor zs y ! ?i = zs ! (?i div length y) * y ! (?i mod length y)

goal (1 subgoal):
 1. 0 < length zs * length y \<longrightarrow> vec_vec_Tensor zs y ! 0 = zs ! 0 * y ! 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < length zs * length y \<longrightarrow> vec_vec_Tensor zs y ! 0 = zs ! 0 * y ! 0

goal (1 subgoal):
 1. length y = i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
with  4 5 8
[PROOF STATE]
proof (chain)
picking this:
i = length y \<longrightarrow> (i < length (z # zs) * length y) = (0 < length zs * length y)
i = length y \<longrightarrow> (z # zs) ! (i div length y) = zs ! 0
0 mod length y = 0
0 < length zs * length y \<longrightarrow> vec_vec_Tensor zs y ! 0 = zs ! 0 * y ! 0
[PROOF STEP]
have "(i = length y)
                            \<longrightarrow> ((i < (length (z#zs))*(length y))
                                     \<longrightarrow> (((vec_vec_Tensor (zs) y)!0)
                                             = f ((zs)!0) (y!0)))"
[PROOF STATE]
proof (prove)
using this:
i = length y \<longrightarrow> (i < length (z # zs) * length y) = (0 < length zs * length y)
i = length y \<longrightarrow> (z # zs) ! (i div length y) = zs ! 0
0 mod length y = 0
0 < length zs * length y \<longrightarrow> vec_vec_Tensor zs y ! 0 = zs ! 0 * y ! 0

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

goal (1 subgoal):
 1. length y = i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
with 1 2 5
[PROOF STATE]
proof (chain)
picking this:
i = length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = vec_vec_Tensor zs y ! 0
i = length y \<longrightarrow> i mod length y = 0
i = length y \<longrightarrow> (z # zs) ! (i div length y) = zs ! 0
i = length y \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor zs y ! 0 = zs ! 0 * y ! 0
[PROOF STEP]
have "(i = length y)
                             \<longrightarrow> ((i < (length (z#zs))*(length y))
                                 \<longrightarrow> (((vec_vec_Tensor ((z#zs)) y)!i)
                                            = f
                                                 ((z#zs)!(i div (length y)))
                                                 (y!(i mod (length y)))))"
[PROOF STATE]
proof (prove)
using this:
i = length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = vec_vec_Tensor zs y ! 0
i = length y \<longrightarrow> i mod length y = 0
i = length y \<longrightarrow> (z # zs) ! (i div length y) = zs ! 0
i = length y \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor zs y ! 0 = zs ! 0 * y ! 0

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length y = i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)

goal (1 subgoal):
 1. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
with step2
[PROOF STATE]
proof (chain)
picking this:
length y < i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
length y = i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have step4:
            "(i \<ge> (length y))
                      \<longrightarrow>  ((i < (length (z#zs))*(length y))
                       \<longrightarrow> (((vec_vec_Tensor ((z#zs)) y)!i)
                                    = f
                                         ((z#zs)!(i div (length y)))
                                         (y!(i mod (length y)))))"
[PROOF STATE]
proof (prove)
using this:
length y < i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
length y = i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)

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

goal (1 subgoal):
 1. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
have "(i < (length y)) \<or> (i \<ge> (length y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length y \<or> length y \<le> i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length y \<or> length y \<le> i

goal (1 subgoal):
 1. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
with step1 step4
[PROOF STATE]
proof (chain)
picking this:
i < length y \<longrightarrow> i < length x * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
length y \<le> i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
i < length y \<or> length y \<le> i
[PROOF STEP]
have
            "((i < (length (z#zs))*(length y))
                       \<longrightarrow> (((vec_vec_Tensor ((z#zs)) y)!i)
                                = f
                                    ((z#zs)!(i div (length y)))
                                     (y!(i mod (length y)))))"
[PROOF STATE]
proof (prove)
using this:
i < length y \<longrightarrow> i < length x * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
length y \<le> i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
i < length y \<or> length y \<le> i

goal (1 subgoal):
 1. i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
using logic
[PROOF STATE]
proof (prove)
using this:
i < length y \<longrightarrow> i < length x * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
length y \<le> i \<longrightarrow> i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
i < length y \<or> length y \<le> i
\<lbrakk>?A \<longrightarrow> ?B; \<not> ?A \<longrightarrow> ?B\<rbrakk> \<Longrightarrow> ?B

goal (1 subgoal):
 1. i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
by (metis "6" "7" 35)
[PROOF STATE]
proof (state)
this:
i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)

goal (1 subgoal):
 1. \<And>a x i. (\<And>i. i < length x * length y \<longrightarrow> vec_vec_Tensor x y ! i = x ! (i div length y) * y ! (i mod length y)) \<Longrightarrow> i < length (a # x) * length y \<longrightarrow> vec_vec_Tensor (a # x) y ! i = (a # x) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i < length (z # zs) * length y \<longrightarrow> vec_vec_Tensor (z # zs) y ! i = (z # zs) ! (i div length y) * y ! (i mod length y)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nat_int:  "nat (int x + int y) = x + y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat (int x + int y) = x + y
[PROOF STEP]
using nat_int of_nat_add
[PROOF STATE]
proof (prove)
using this:
nat (int ?n) = ?n
of_nat (?m + ?n) = of_nat ?m + of_nat ?n

goal (1 subgoal):
 1. nat (int x + int y) = x + y
[PROOF STEP]
by auto


[STATEMENT]
lemma int_nat_equiv: "(x > 0) \<longrightarrow> (nat ((int x) + -1)+1) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < x \<longrightarrow> nat (int x + - 1) + 1 = x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < x \<longrightarrow> nat (int x + - 1) + 1 = x
[PROOF STEP]
have "1 = nat (int 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 = nat (int 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 = nat (int 1)

goal (1 subgoal):
 1. 0 < x \<longrightarrow> nat (int x + - 1) + 1 = x
[PROOF STEP]
have "-1 = -int 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - 1 = - int 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- 1 = - int 1

goal (1 subgoal):
 1. 0 < x \<longrightarrow> nat (int x + - 1) + 1 = x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
- 1 = - int 1
[PROOF STEP]
have 1:"(nat ((int x) + -1)+1)
                      = (nat ((int x) + -1) + (nat (int 1)))"
[PROOF STATE]
proof (prove)
using this:
- 1 = - int 1

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

goal (1 subgoal):
 1. 0 < x \<longrightarrow> nat (int x + - 1) + 1 = x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nat (int x + - 1) + 1 = nat (int x + - 1) + nat (int 1)
[PROOF STEP]
have 2:"(x > 0)
                 \<longrightarrow> nat ((int x) + -1 ) + (nat (int 1))
                                 =  (nat (((int x)  + -1) + (int 1)))"
[PROOF STATE]
proof (prove)
using this:
nat (int x + - 1) + 1 = nat (int x + - 1) + nat (int 1)

goal (1 subgoal):
 1. 0 < x \<longrightarrow> nat (int x + - 1) + nat (int 1) = nat (int x + - 1 + int 1)
[PROOF STEP]
using of_nat_add nat_int
[PROOF STATE]
proof (prove)
using this:
nat (int x + - 1) + 1 = nat (int x + - 1) + nat (int 1)
of_nat (?m + ?n) = of_nat ?m + of_nat ?n
nat (int ?x + int ?y) = ?x + ?y

goal (1 subgoal):
 1. 0 < x \<longrightarrow> nat (int x + - 1) + nat (int 1) = nat (int x + - 1 + int 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < x \<longrightarrow> nat (int x + - 1) + nat (int 1) = nat (int x + - 1 + int 1)

goal (1 subgoal):
 1. 0 < x \<longrightarrow> nat (int x + - 1) + 1 = x
[PROOF STEP]
have "(nat (((int x)  + -1) + (int 1))) = (nat ((int x) + -1 + (int 1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat (int x + - 1 + int 1) = nat (int x + - 1 + int 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat (int x + - 1 + int 1) = nat (int x + - 1 + int 1)

goal (1 subgoal):
 1. 0 < x \<longrightarrow> nat (int x + - 1) + 1 = x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nat (int x + - 1 + int 1) = nat (int x + - 1 + int 1)
[PROOF STEP]
have "(nat (((int x)  + -1) + (int 1))) = (nat ((int x)))"
[PROOF STATE]
proof (prove)
using this:
nat (int x + - 1 + int 1) = nat (int x + - 1 + int 1)

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

goal (1 subgoal):
 1. 0 < x \<longrightarrow> nat (int x + - 1) + 1 = x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nat (int x + - 1 + int 1) = nat (int x)
[PROOF STEP]
have "(nat (((int x)  + -1) + (int 1))) = x"
[PROOF STATE]
proof (prove)
using this:
nat (int x + - 1 + int 1) = nat (int x)

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

goal (1 subgoal):
 1. 0 < x \<longrightarrow> nat (int x + - 1) + 1 = x
[PROOF STEP]
with 1 2
[PROOF STATE]
proof (chain)
picking this:
nat (int x + - 1) + 1 = nat (int x + - 1) + nat (int 1)
0 < x \<longrightarrow> nat (int x + - 1) + nat (int 1) = nat (int x + - 1 + int 1)
nat (int x + - 1 + int 1) = x
[PROOF STEP]
have " (x > 0) \<longrightarrow> nat ((int x) + -1 ) + 1 = x"
[PROOF STATE]
proof (prove)
using this:
nat (int x + - 1) + 1 = nat (int x + - 1) + nat (int 1)
0 < x \<longrightarrow> nat (int x + - 1) + nat (int 1) = nat (int x + - 1 + int 1)
nat (int x + - 1 + int 1) = x

goal (1 subgoal):
 1. 0 < x \<longrightarrow> nat (int x + - 1) + 1 = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < x \<longrightarrow> nat (int x + - 1) + 1 = x

goal (1 subgoal):
 1. 0 < x \<longrightarrow> nat (int x + - 1) + 1 = x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < x \<longrightarrow> nat (int x + - 1) + 1 = x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < x \<longrightarrow> nat (int x + - 1) + 1 = x

goal (1 subgoal):
 1. 0 < x \<longrightarrow> nat (int x + - 1) + 1 = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < x \<longrightarrow> nat (int x + - 1) + 1 = x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_int_nat: "(k>0) \<longrightarrow> ((x#xs)!k = xs!(nat ((int k)+-1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<longrightarrow> (x # xs) ! k = xs ! nat (int k + - 1)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < k \<longrightarrow> (x # xs) ! k = xs ! nat (int k + - 1)
[PROOF STEP]
fix  j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < k \<longrightarrow> (x # xs) ! k = xs ! nat (int k + - 1)
[PROOF STEP]
have " ((x#xs)!(k+1) = xs!k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x # xs) ! (k + 1) = xs ! k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x # xs) ! (k + 1) = xs ! k

goal (1 subgoal):
 1. 0 < k \<longrightarrow> (x # xs) ! k = xs ! nat (int k + - 1)
[PROOF STEP]
have "j = (k+1) \<longrightarrow> (nat ((int j)+-1)) = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j = k + 1 \<longrightarrow> nat (int j + - 1) = k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j = k + 1 \<longrightarrow> nat (int j + - 1) = k

goal (1 subgoal):
 1. 0 < k \<longrightarrow> (x # xs) ! k = xs ! nat (int k + - 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j = k + 1 \<longrightarrow> nat (int j + - 1) = k

goal (1 subgoal):
 1. 0 < k \<longrightarrow> (x # xs) ! k = xs ! nat (int k + - 1)
[PROOF STEP]
have "(nat ((int j)+-1)) = k
                  \<longrightarrow> ((nat ((int j)+-1)) + 1) = (k +1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat (int j + - 1) = k \<longrightarrow> nat (int j + - 1) + 1 = k + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat (int j + - 1) = k \<longrightarrow> nat (int j + - 1) + 1 = k + 1

goal (1 subgoal):
 1. 0 < k \<longrightarrow> (x # xs) ! k = xs ! nat (int k + - 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nat (int j + - 1) = k \<longrightarrow> nat (int j + - 1) + 1 = k + 1

goal (1 subgoal):
 1. 0 < k \<longrightarrow> (x # xs) ! k = xs ! nat (int k + - 1)
[PROOF STEP]
have "(j>0)\<longrightarrow>(((nat ((int j)+-1)) + 1) = j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < j \<longrightarrow> nat (int j + - 1) + 1 = j
[PROOF STEP]
using  int_nat_equiv
[PROOF STATE]
proof (prove)
using this:
0 < ?x \<longrightarrow> nat (int ?x + - 1) + 1 = ?x

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

goal (1 subgoal):
 1. 0 < k \<longrightarrow> (x # xs) ! k = xs ! nat (int k + - 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < j \<longrightarrow> nat (int j + - 1) + 1 = j

goal (1 subgoal):
 1. 0 < k \<longrightarrow> (x # xs) ! k = xs ! nat (int k + - 1)
[PROOF STEP]
have "(k>0) \<longrightarrow> ((x#xs)!k = xs!(nat ((int k)+-1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<longrightarrow> (x # xs) ! k = xs ! nat (int k + - 1)
[PROOF STEP]
using Suc_eq_plus1 int_nat_equiv nth_Cons_Suc
[PROOF STATE]
proof (prove)
using this:
Suc ?n = ?n + 1
0 < ?x \<longrightarrow> nat (int ?x + - 1) + 1 = ?x
(?x # ?xs) ! Suc ?n = ?xs ! ?n

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

goal (1 subgoal):
 1. 0 < k \<longrightarrow> (x # xs) ! k = xs ! nat (int k + - 1)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
0 < k \<longrightarrow> (x # xs) ! k = xs ! nat (int k + - 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < k \<longrightarrow> (x # xs) ! k = xs ! nat (int k + - 1)

goal (1 subgoal):
 1. 0 < k \<longrightarrow> (x # xs) ! k = xs ! nat (int k + - 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < k \<longrightarrow> (x # xs) ! k = xs ! nat (int k + - 1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma row_length_eq:
 "(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]
proof-
[PROOF STATE]
proof (state)
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]
have "(mat  (row_length (a#b#N))  (length (a#b#N)) (a#b#N))
                        \<longrightarrow> (b \<in> set (a#b#M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> b \<in> set (a # b # M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> b \<in> set (a # b # M)

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]
moreover
[PROOF STATE]
proof (state)
this:
mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> b \<in> set (a # b # M)

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]
have
         "(mat  (row_length (a#b#N))  (length (a#b#N)) (a#b#N))
                 \<longrightarrow> (Ball (set (a#b#N)) (vec (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> Ball (set (a # b # N)) (vec (row_length (a # b # N)))
[PROOF STEP]
using mat_def
[PROOF STATE]
proof (prove)
using this:
mat ?nr ?nc ?m = (length ?m = ?nc \<and> Ball (set ?m) (vec ?nr))

goal (1 subgoal):
 1. mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> Ball (set (a # b # N)) (vec (row_length (a # 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> Ball (set (a # b # N)) (vec (row_length (a # 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]
moreover
[PROOF STATE]
proof (state)
this:
mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> Ball (set (a # b # N)) (vec (row_length (a # 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]
have "(mat  (row_length (a#b#N))  (length (a#b#N)) (a#b#N))
                  \<longrightarrow> (b \<in> (set (a#b#N)))
                    \<longrightarrow> (vec (row_length (a#b#N)) b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> b \<in> set (a # b # N) \<longrightarrow> vec (row_length (a # b # N)) b
[PROOF STEP]
by (metis calculation(2))
[PROOF STATE]
proof (state)
this:
mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> b \<in> set (a # b # N) \<longrightarrow> vec (row_length (a # b # N)) b

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]
then
[PROOF STATE]
proof (chain)
picking this:
mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> b \<in> set (a # b # N) \<longrightarrow> vec (row_length (a # b # N)) b
[PROOF STEP]
have "(mat  (row_length (a#b#N))  (length (a#b#N)) (a#b#N))
                         \<longrightarrow> (length b) = (row_length (a#b#N))"
[PROOF STATE]
proof (prove)
using this:
mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> b \<in> set (a # b # N) \<longrightarrow> vec (row_length (a # b # N)) b

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

goal (1 subgoal):
 1. mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> length b = row_length (a # b # N)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> length b = row_length (a # 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]
then
[PROOF STATE]
proof (chain)
picking this:
mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> length b = row_length (a # b # N)
[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)
using this:
mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> length b = row_length (a # b # N)

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]
using row_length_def
[PROOF STATE]
proof (prove)
using this:
mat (row_length (a # b # N)) (length (a # b # N)) (a # b # N) \<longrightarrow> length b = row_length (a # b # N)
row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)

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 auto
[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. 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]
then
[PROOF STATE]
proof (chain)
picking this:
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]
show ?thesis
[PROOF STATE]
proof (prove)
using 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. 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 auto
[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:
No subgoals!
[PROOF STEP]
qed