Theory Matrix_Tensor

(*  Title:       Tensor Product of Matrices
    Author:      T. V. H. Prathamesh (prathamesh@imsc.res.in)
    Maintainer:  T. V. H. Prathamesh
*)

text‹
We define Tensor Product of Matrics and prove properties such as associativity and mixed product 
property(distributivity) of the tensor product.›

section‹Tensor Product of Matrices›

theory Matrix_Tensor
imports Matrix.Utility Matrix.Matrix_Legacy
begin


subsection‹Defining the Tensor Product›



text‹We define a multiplicative locale here - mult, 
where the multiplication satisfies commutativity, 
associativity and contains a left and right identity›

locale mult = 
 fixes id::"'a"
 fixes f::" 'a  'a  'a " (infixl "*" 60)
 assumes comm:" f a  b = f b  a "
 assumes assoc:" (f (f a b) c) = (f a (f b c))"
 assumes left_id:" f id x = x"
 assumes right_id:"f x id = x"
 
context mult
begin   


text‹times a v , gives us the product of the vector v with 
multiplied pointwise with a›

primrec times:: "'a  'a vec  'a vec"
where
"times n [] = []"|
"times n (y#ys) = (f n y)#(times n ys)"

lemma times_scalar_id: "times id v = v"
 by(induction v)(auto simp add:left_id)

lemma times_vector_id: "times v [id] = [v]"
 by(simp add:right_id)

lemma preserving_length: "length (times n y) = (length y)"
 by(induction y)(auto)

text‹vec$\_$vec$\_$Tensor is the tensor product of two vectors. It is 
illustrated by the following relation
 
$vec\_vec\_Tensor (v_1,v_2,...v_n) (w_1,w_2,...w_m) 
                 = (v_1 \cdot w_1,...,v_1 \cdot w_m,...
                          , v_n \cdot w_1 , ..., v_n \cdot w_m)$›

primrec vec_vec_Tensor:: "'a vec  'a vec  'a vec"
where
"vec_vec_Tensor [] ys = []"|
"vec_vec_Tensor (x#xs) ys = (times x ys)@(vec_vec_Tensor xs ys)"


lemma vec_vec_Tensor_left_id: "vec_vec_Tensor [id] v = v"
 by(induction v)(auto simp add:left_id)

lemma vec_vec_Tensor_right_id: "vec_vec_Tensor v [id] = v"
 by(induction v)(auto simp add:right_id)

theorem vec_vec_Tensor_length : 
 "(length(vec_vec_Tensor x y)) = (length x)*(length y)"
 by(induction x)(auto simp add: preserving_length)

theorem vec_length: assumes "vec m x" and "vec n y"
shows "vec (m*n) (vec_vec_Tensor x y)"
 apply(simp add:vec_def)
 apply(simp add:vec_vec_Tensor_length)
 apply (metis assms(1) assms(2) vec_def)
 done


text‹vec$\_$mat$\_$Tensor is the tensor product of two vectors. It is 
illusstrated by the following relation
 
vec\_mat\_Tensor ($v_1,v_2,...v_n) (C_1,C_2,...C_m) 
                 = (v_1 \cdot C_1,...,v_n \cdot C_1,
                               ...,v_1 \cdot C_m , ..., v_n \cdot C_m$)›


primrec vec_mat_Tensor::"'a vec  'a mat 'a mat"
where
"vec_mat_Tensor xs []  = []"|
"vec_mat_Tensor xs (ys#yss) = (vec_vec_Tensor xs ys)#(vec_mat_Tensor xs yss)"


lemma vec_mat_Tensor_vector_id: "vec_mat_Tensor [id] v = v"
 by(induction v)(auto simp add: times_scalar_id)

lemma vec_mat_Tensor_matrix_id: "vec_mat_Tensor  v [[id]] = [v]"
 by(induction v)(auto simp add: right_id)

theorem vec_mat_Tensor_length: 
 "length(vec_mat_Tensor xs ys) = length ys"
 by(induction ys)(auto)

theorem length_matrix: 
 assumes "mat nr nc (y#ys)" and "length v = k"
     and "(vec_mat_Tensor v (y#ys) = x#xs)" 
 shows "(vec (nr*k) x)" 
proof-
 have "vec_mat_Tensor v (y#ys) = (vec_vec_Tensor v y)#(vec_mat_Tensor v ys)"  
       using vec_mat_Tensor_def assms by auto
 also have "(vec_vec_Tensor v y) = x" using assms by auto
 also have "length y = nr" using assms mat_def 
       by (metis in_set_member member_rec(1) vec_def)
 from this
   have "length (vec_vec_Tensor v y) = nr*k" 
       using assms vec_vec_Tensor_length  by auto
 from this 
   have "length x = nr*k" by (simp add: vec_vec_Tensor v y = x)
 from this 
   have "vec (nr*k) x" using vec_def by auto
 from this 
   show ?thesis by auto
qed

lemma matrix_set_list: 
 assumes "mat nr nc M" 
     and "length v = k"
     and " x  set M" 
 shows "ys.zs.(ys@x#zs = M)" 
 using assms set_def in_set_conv_decomp by metis

primrec reduct :: "'a mat  'a mat"
where
"reduct [] = []"
|"reduct (x#xs) = xs"

lemma length_reduct: 
 assumes "m  []"
 shows "length (reduct m) +1  = (length m)"
 apply(auto)
 by (metis One_nat_def Suc_eq_plus1 assms list.size(4) neq_Nil_conv reduct.simps(2))

lemma mat_empty_column_length: assumes "mat nr nc M" and "M = []"
shows "nc = 0" 
proof-
 have "(length M = nc)" using mat_def assms by metis
 from this 
   have "nc = 0" using assms by auto
 from this 
   show ?thesis by simp
qed

lemma vec_uniqueness: 
 assumes "vec m v" 
     and "vec n v" 
 shows "m = n"
 using vec_def assms(1) assms(2)  by metis

lemma mat_uniqueness: 
 assumes "mat nr1 nc M" 
 and "mat nr2 nc M" and "z = hd M" and "M  []"
 shows "(x(set M).(nr1 = nr2))" 
proof-
 have A:"z  set M" using assms(1) assms(3) assms(4) set_def mat_def 
           by (metis hd_in_set)
 have "Ball (set M) (vec nr1)" using mat_def assms(1) by auto 
 then have step1: "((x  (set M))  (vec nr1 x))" using Ball_def assms by auto
 have "Ball (set M) (vec nr2)" using mat_def assms(2) by auto
 then have step2: "((x  (set M))  (vec nr2 x))" using Ball_def assms by auto
 from step1 and step2 
   have step3:"x.((x  (set M)) ((vec nr1 x) (vec nr2 x)))"
   by (metis Ball (set M) (vec nr1) Ball (set M) (vec nr2))
 have "((vec nr1 x) (vec nr2 x))  (nr1 = nr2)" using vec_uniqueness by auto
 with step3  
   have "(x.((x  (set M)) ((nr1 = nr2))))" by (metis vec_uniqueness) 
 then
   have "(x(set M).(nr1 = nr2))" by auto 
 then 
     show ?thesis by auto
qed

 
lemma mat_empty_row_length: assumes "mat nr nc M" and "M = []"
shows "mat 0 nc M" 
proof-
 have "set M = {}" using mat_def assms  empty_set  by auto
 then have "Ball (set M) (vec 0)" using Ball_def by auto
 then have "mat 0 nc M" using mat_def assms(1) assms(2) gen_length_code(1) length_code
 by (metis (full_types) )
 then show ?thesis by auto
qed

abbreviation null_matrix::"'a list list"
where
"null_matrix  [Nil] "

lemma null_mat:"null_matrix = [[]]"
 by auto

lemma zero_matrix:" mat 0 0 []" using mat_def in_set_insert insert_Nil list.size(3) not_Cons_self2
 by (metis (full_types))

text‹row\_length gives the length of the first row of a matrix. For a `valid'
matrix, it is equal to the number of rows›

definition row_length:: "'a mat  nat"
where
"row_length xs  if (xs = []) then 0 else (length (hd xs))"

lemma row_length_Nil: 
 "row_length [] =0" 
 using row_length_def by (metis )

lemma row_length_Null: 
 "row_length [[]] =0" 
 using row_length_def by auto

lemma row_length_vect_mat: 
 "row_length (vec_mat_Tensor v m)  = length v*(row_length m)"
proof(induct m)
 case Nil
  have "row_length [] = 0" 
       using row_length_Nil by simp
  moreover have "vec_mat_Tensor v [] = []" 
       using vec_mat_Tensor.simps(1) by auto 
  ultimately have 
   "row_length (vec_mat_Tensor v [])  = length v*(row_length [])" 
       using mult_0_right by (metis )
  then show ?case by metis
 next  
  fix a m
  assume A:"row_length (vec_mat_Tensor v m) = length v * row_length m"
  let ?case = 
         "row_length (vec_mat_Tensor v (a#m)) = (length v)*(row_length (a#m))" 
  have A:"row_length (a # m) = length a" 
              using row_length_def   list.distinct(1)
              by auto
  have "(vec_mat_Tensor v  (a#m)) = (vec_vec_Tensor v a)#(vec_mat_Tensor v m)" 
              using vec_mat_Tensor_def vec_mat_Tensor.simps(2)
              by auto
  from this have 
       "row_length (vec_mat_Tensor v (a#m)) = length (vec_vec_Tensor v a)" 
              using row_length_def   list.distinct(1)  vec_mat_Tensor.simps(2)
              by auto
  from this and vec_vec_Tensor_length have 
          "row_length (vec_mat_Tensor v (a#m)) = (length v)*(length a)" 
              by auto
  from this and A  have 
         "row_length (vec_mat_Tensor v (a#m)) = (length v)*(row_length (a#m))"
              by auto
  from this show ?case by auto
qed

text‹Tensor is the tensor product of matrices›

primrec Tensor::" 'a mat  'a mat 'a mat" (infixl "" 63)
where
"Tensor [] xs = []"|
"Tensor (x#xs) ys = (vec_mat_Tensor x ys)@(Tensor xs ys)"

lemma Tensor_null: "xs [] = []" 
 by(induction xs)(auto)

text‹Tensor commutes with left and right identity›

lemma Tensor_left_id: "  [[id]]  xs = xs"
 by(induction xs)(auto simp add:times_scalar_id)

lemma Tensor_right_id: "  xs  [[id]] = xs"
 by(induction xs)(auto simp add: vec_vec_Tensor_right_id)

text‹row$\_$length of tensor product of matrices is the product of 
their respective row lengths›

lemma row_length_mat: 
    "(row_length (m1m2)) = (row_length m1)*(row_length m2)"
proof(induct m1)
 case Nil
  have "row_length ([]m2) = 0" 
    using Tensor.simps(1) row_length_def 
    by metis
  from this 
   have "row_length ([]m2) = (row_length [])*(row_length m2)" 
    using  row_length_Nil   
    by auto
   then show ?case by metis
 next
  fix a m1 
  assume "row_length (m1  m2) = row_length m1 * row_length m2"
  let ?case = 
    "row_length ((a # m1)  m2) = row_length (a # m1) * row_length m2"
  have B: "row_length (a#m1) = length a" 
    using row_length_def   list.distinct(1)
    by auto
  have "row_length ((a # m1)  m2) = row_length (a # m1) * row_length m2"
  proof(induct m2)
   case Nil
       show ?case using Tensor_null row_length_def  mult_0_right by (metis)
   next
    fix aa m2
    assume "row_length (a # m1  m2) = row_length (a # m1) * row_length m2"
     let ?case= 
      "row_length (a # m1  aa # m2) 
                  = row_length (a # m1) * row_length (aa # m2)"
     have "aa#m2  []" 
          by auto
     from this have non_zero:"(vec_mat_Tensor a (aa#m2))  []" 
          using vec_mat_Tensor_def by auto
     from this have 
            "hd ((vec_mat_Tensor a (aa#m2))@(m1m2))
                  = hd (vec_mat_Tensor a (aa#m2))" 
          by auto
     from this have 
            "hd ((a#m1)(aa#m2)) = hd (vec_mat_Tensor a (aa#m2))" 
          using Tensor.simps(2) by auto
     from this have s1: "row_length ((a#m1)(aa#m2)) 
                       = row_length (vec_mat_Tensor a (aa#m2))" 
          using row_length_def  Nil_is_append_conv non_zero Tensor.simps(2)
          by auto
     have "row_length (vec_mat_Tensor a (aa#m2)) 
                    = (length a)*row_length(aa#m2)" 
          using row_length_vect_mat by metis   
     from this and s1  
     have "row_length (vec_mat_Tensor a (aa#m2)) 
                             = (length a)*row_length(aa#m2)"
          by auto
     from this and B 
             have "row_length (vec_mat_Tensor a (aa#m2)) 
                           = (row_length (a#m1))*row_length(aa#m2)"    
          by auto
     from this  and s1 show ?case  by auto
  qed
  from this show ?case by auto
 qed


lemma hd_set:assumes "x  set (a#M)" shows "(x = a)  (x(set M))"
 using set_def assms set_ConsD  by auto

text‹for every valid matrix can also be written in the following form›

theorem matrix_row_length: 
 assumes "mat nr nc M" 
 shows "mat (row_length M) (length M) M"
proof(cases M)
 case Nil
  have "row_length M= 0 " 
       using row_length_def by (metis Nil)
  moreover have "length M = 0" 
       by (metis Nil list.size(3))
  moreover  have "mat 0 0 M" 
       using zero_matrix Nil by auto 
  ultimately show ?thesis  
       using mat_empty_row_length row_length_def mat_def  by metis
 next
 case (Cons a N) 
  have 1: "mat nr nc (a#N)" 
       using assms Cons by auto
  from this have "(x  set (a #N))  (x = a)  (x  (set N))" 
       using hd_set by auto
  from this and 1 have 2:"vec nr a" 
       using mat_def by (metis Ball_set_list_all list_all_simps(1))
  have "row_length (a#N) = length a" 
       using row_length_def Cons  list.distinct(1) by auto
  from this have " vec (row_length (a#N)) a" 
        using vec_def by auto
  from this and 2 have 3:"(row_length M)  = nr" 
        using vec_uniqueness Cons by auto
  have " nc = (length M)" 
        using 1 and mat_def and assms by metis
  with 3 
        have "mat (row_length M) (length M) M" 
        using assms by auto 
  from this show ?thesis by auto
qed


lemma reduct_matrix: 
 assumes "mat (row_length (a#M)) (length (a#M)) (a#M)"
 shows "mat (row_length M) (length M) M"
proof(cases M)
 case Nil
   show ?thesis 
         using row_length_def zero_matrix Nil  list.size(3)  by (metis)
 next   
 case (Cons b N)
  fix x
  have 1: "b  (set M)" 
         using set_def  Cons ListMem_iff elem  by auto
  have "mat (row_length (a#M)) (length (a#M)) (a#M)" 
         using assms by auto
  then have "(x  (set (a#M)))  ((x = a)  (x  set M))" 
         by auto
  then have " (x  (set (a#M)))  (vec (row_length (a#M)) x)" 
         using mat_def Ball_def assms 
         by metis
  then have "(x  (set (a#M)))  (vec (length a) x)" 
         using row_length_def  list.distinct(1) 
         by auto
  then have 2:"x  (set M)  (vec (length a) x)" 
         by auto
  with 1 have 3:"(vec (length a) b)"
         using assms in_set_member mat_def member_rec(1) vec_def
         by metis 
  have 5: "(vec (length b) b)" 
         using vec_def by auto
  with 3 have "(length a) = (length b)" 
         using vec_uniqueness by auto
  with 2 have 4: "x  (set M)  (vec (length b) x)" 
         by auto
  have 6: "row_length M = (length b)" 
         using row_length_def   Cons list.distinct(1)
         by auto
  with 4 have "x  (set M)  (vec (row_length M) x)" 
         by auto
  then have "(x. (x  (set M)  (vec (row_length M) x)))" 
         using Cons 5 6 assms in_set_member mat_def member_rec(1) 
         vec_uniqueness
         by metis
  then have "Ball (set M) (vec (row_length M))" 
         using Ball_def by auto
  then have "(mat (row_length M) (length M) M)" 
         using mat_def by auto
  then show ?thesis by auto
 qed 


theorem well_defined_vec_mat_Tensor:
"(mat (row_length M) (length M) M) 
                  (mat 
                    ((row_length M)*(length v)) 
                    (length M) 
                           (vec_mat_Tensor v M))"
proof(induct M) 
 case Nil
  have "(vec_mat_Tensor v []) = []" 
      using vec_mat_Tensor.simps(1) Nil  
      by simp
  moreover have "(row_length [] = 0)"  
      using row_length_def Nil 
      by metis
  moreover have "(length []) = 0" 
      using Nil by simp
  ultimately have 
       "mat ((row_length [])*(length v)) (length []) (vec_mat_Tensor v [])" 
      using zero_matrix by (metis mult_zero_left)
  then show ?case by simp
 next
 fix a M
 assume hyp :
   "(mat (row_length M) (length M) M 
            mat (row_length M * length v) (length M) (vec_mat_Tensor v M))"
   "mat (row_length (a#M)) (length (a#M)) (a#M)"                      
  let ?case = 
   "mat (row_length (a#M) * length v) (length (a#M)) (vec_mat_Tensor v (a#M))"
  have step1: "mat (row_length M) (length M) M" 
          using hyp(2) reduct_matrix by auto
  then have step2:
    "mat (row_length M * length v) (length M) (vec_mat_Tensor v M)" 
          using hyp(1) by auto 
  have 
   "mat 
        (row_length (a#M) * length v) 
        (length (a#M)) 
             (vec_mat_Tensor v (a#M))" 
  proof (cases M)
   case Nil 
    fix x
    have 1:"(vec_mat_Tensor v (a#M)) = [vec_vec_Tensor v a]" 
           using vec_mat_Tensor.simps Nil by auto
    have   "(x  (set [vec_vec_Tensor v a]))   x = (vec_vec_Tensor v a)" 
           using set_def by auto
    then have 2:
        "(x  (set [vec_vec_Tensor v a])) 
                     (vec (length (vec_vec_Tensor v a)) x)" 
           using vec_def by metis 
    have 3:"length (vec_vec_Tensor v a) = (length v)*(length a)" 
           using vec_vec_Tensor_length by auto 
    then have 4:
        "length (vec_vec_Tensor v a) = (length v)*(row_length (a#M))" 
           using row_length_def  list.distinct(1) 
           by auto
    have 6: "length (vec_mat_Tensor v (a#M)) = (length (a#M))" 
           using vec_mat_Tensor_length by auto
    hence "mat (length (vec_vec_Tensor v a)) (length (a # M)) [vec_vec_Tensor v a]"
      by (simp add: Nil mat_def vec_def)
    hence
        "mat (row_length (a#M) * length v) 
             (length (vec_mat_Tensor v (a#M))) 
             (vec_mat_Tensor v (a#M))"
      using 1 4 6 by (simp add: mult.commute)
    then show ?thesis using 6 by auto
   next 
   case (Cons b L)
    fix x
    have 1:"x  (set (a#M))  ((x=a)  (x  (set M)))" 
           using hd_set by auto
    have "mat (row_length (a#M)) (length (a#M)) (a#M)" 
           using hyp by auto
    then have "x (set (a#M))  (vec (row_length (a#M)) x)" 
           using mat_def Ball_def by metis
    then have "x (set (a#M)) (vec (length a) x)" 
           using row_length_def  list.distinct(1)
           by auto
    with 1 have "x (set M) (vec (length a) x)" 
           by auto
    moreover have " b  (set M)" 
           using Cons by auto
    ultimately have "vec (length a) b"
           using  hyp(2) in_set_member mat_def member_rec(1) vec_def  by (metis) 
    then have "(length b) = (length a)" 
           using vec_def vec_uniqueness by auto
    then have 2:"row_length M = (length a)" 
           using row_length_def   Cons list.distinct(1) by auto     
    have "mat (row_length M * length v) (length M) (vec_mat_Tensor v M)" 
           using step2 by auto 
    then have 3:
          "Ball (set (vec_mat_Tensor v M)) (vec ((row_length M)*(length v)))" 
           using mat_def by auto
    then have "(x  set (vec_mat_Tensor v M)) 
                         (vec ((row_length M)*(length v)) x)" 
           using mat_def Ball_def by auto
    then have 4:"(x  set (vec_mat_Tensor v M)) 
                           (vec ((length a)*(length v)) x)" 
           using 2 by auto  
    have 5:"length (vec_vec_Tensor v a) = (length a)*(length v)" 
           using   vec_vec_Tensor_length by auto  
    then have 6:" vec ((length a)*(length v)) (vec_vec_Tensor v a)" 
           using vec_vec_Tensor_length vec_def by (metis (full_types))
    have 7:"(length a) = (row_length (a#M))" 
           using row_length_def   list.distinct(1) by auto 
    have "vec_mat_Tensor v (a#M) 
                   = (vec_vec_Tensor v a)#(vec_mat_Tensor v M)" 
           using vec_mat_Tensor.simps(2) by auto
    then have "(x  set (vec_mat_Tensor v (a#M)))
                       ((x = (vec_vec_Tensor v a)) 
                            (x  (set (vec_mat_Tensor v M))))"
           using  hd_set by auto
    with 4 6 have "(x  set (vec_mat_Tensor v (a#M)))
                               vec ((length a)*(length v)) x" 
           by auto
    with 7 have "(x  set (vec_mat_Tensor v (a#M)))
                                  vec ((row_length (a#M))*(length v)) x" 
           by auto
    then have "x.((x  set (vec_mat_Tensor v (a#M)))
                                  vec ((row_length (a#M))*(length v)) x)"
           using "2" "3" "6" "7" hd_set vec_mat_Tensor.simps(2) by auto
    then have 7: 
      "Ball 
            (set (vec_mat_Tensor v (a#M))) 
            (vec ((row_length (a#M))*(length v)))" 
           using Ball_def  by auto
    have 8: "length (vec_mat_Tensor v (a#M)) = length (a#M)" 
           using vec_mat_Tensor_length by auto   
    with 6  7 have 
               "mat 
                 ((row_length (a#M))*(length v)) 
                 (length (a#M)) 
                           (vec_mat_Tensor v (a#M))"
           using mat_def  "5" length_code
           by (metis (opaque_lifting, no_types))
    then show ?thesis by auto
    qed
    with  hyp  show ?case by auto  
 qed

text‹The following theorem  gives length of tensor product of two matrices›

lemma length_Tensor:" (length (M1M2)) = (length M1)*(length M2)"
proof(induct M1)
 case Nil
  show ?case by auto
 next
 case (Cons a M1)
  have "((a # M1)  M2) = (vec_mat_Tensor a M2)@(M1  M2)" 
               using Tensor.simps(2) by auto
  then have 1:
          "length ((a # M1)  M2) = length ((vec_mat_Tensor a M2)@(M1  M2))" 
               by auto
  have 2:"length ((vec_mat_Tensor a M2)@(M1  M2)) 
              = length (vec_mat_Tensor a M2)+ length (M1  M2)" 
               using append_def
               by auto
  have 3:"(length (vec_mat_Tensor a M2)) = length M2" 
               using vec_mat_Tensor_length by (auto)
  have 4:"length (M1  M2) = (length M1)*(length M2)" 
               using  Cons.hyps by auto
  with 2 3 have "length ((vec_mat_Tensor a M2)@(M1  M2)) 
                              = (length M2) + (length M1)*(length M2)"
               by auto
  then have 5:
    "length ((vec_mat_Tensor a M2)@(M1  M2)) = (1 + (length M1))*(length M2)" 
               by auto
  with 1  have "length ((a # M1)  M2) = ((length (a # M1)) * (length M2))" 
          by auto
  then show ?case by auto
qed



lemma append_reduct_matrix: 
"(mat (row_length (M1@M2)) (length (M1@M2)) (M1@M2))
(mat (row_length M2) (length M2) M2)"
proof(induct M1)
 case Nil
  show ?thesis using Nil append.simps(1) by auto
 next
 case (Cons a M1)
  have "mat (row_length (M1 @ M2)) (length (M1 @ M2)) (M1 @ M2)" 
    using reduct_matrix Cons.prems append_Cons by metis
  from this have "(mat (row_length M2) (length M2) M2)" 
    using Cons.hyps by auto
  from this show?thesis by simp
qed

text‹The following theorem proves that tensor product of two valid matrices
is a valid matrix›

theorem well_defined_Tensor:
 "(mat (row_length M1) (length M1) M1) 
 (mat (row_length M2) (length M2) M2)
(mat ((row_length M1)*(row_length M2)) ((length M1)*(length M2)) (M1M2))"
proof(induct M1)
 case Nil
   have "(row_length []) * (row_length M2) = 0" 
            using row_length_def  mult_zero_left  by (metis)
   moreover have "(length []) * (length M2) = 0" 
            using  mult_zero_left list.size(3) by auto 
   moreover have "[]  M2 = []" 
            using Tensor.simps(1) by auto
   ultimately have 
       "mat (row_length []*row_length M2) (length []*length M2) ([]  M2)"
            using zero_matrix by metis
   then show ?case by simp
 next
 case (Cons a M1)
  have step1: "mat (row_length (a # M1)) (length (a # M1)) (a # M1)" 
             using Cons.prems by auto
  then have "mat (row_length (M1)) (length (M1)) (M1)" 
             using reduct_matrix by auto
  moreover have "mat (row_length (M2)) (length (M2)) (M2)" 
             using Cons.prems by auto
  ultimately have step2:
      "mat (row_length M1 * row_length M2) (length M1 * length M2) (M1  M2)"
             using Cons.hyps by auto
  have 0:"row_length (a#M1) = length a" 
             using row_length_def  list.distinct(1) by auto
  have "mat 
           (row_length (a # M1)*row_length M2) 
           (length (a # M1)*length M2) 
                           (a # M1  M2)"
  proof(cases M1)
   case Nil 
    have "(mat ((row_length M2)*(length a)) (length M2) (vec_mat_Tensor a M2))" 
          using Cons.prems well_defined_vec_mat_Tensor by auto
    moreover have "(length (a # M1)) * (length M2) = length M2" 
          using Nil by auto
    moreover have "(a#M1)M2 = (vec_mat_Tensor a M2)" 
          using Nil Tensor.simps append.simps(1) by auto
    ultimately have 
        "(mat 
            ((row_length M2)*(row_length (a#M1))) 
            ((length (a # M1)) * (length M2))
               ((a#M1)M2))" 
          using 0 by auto
    then show ?thesis by (simp add: mult.commute)
   next
   case (Cons b N1)
    fix x
    have 1:"x  (set (a#M1))  ((x=a)  (x  (set M1)))" 
               using hd_set by auto
    have "mat (row_length (a#M1)) (length (a#M1)) (a#M1)" 
               using Cons.prems by auto
    then have "x (set (a#M1))  (vec (row_length (a#M1)) x)" 
               using mat_def Ball_def by metis
    then have "x (set (a#M1)) (vec (length a) x)" 
               using row_length_def  list.distinct(1)
               by auto 
    with 1 have "x (set M1) (vec (length a) x)" 
               by auto
    moreover have " b  (set M1)" 
               using Cons by auto
    ultimately have "vec (length a) b" 
               using  Cons.prems in_set_member mat_def member_rec(1) vec_def
               by metis
    then have "(length b) = (length a)" 
               using vec_def vec_uniqueness by auto
    then have 2:"row_length M1 = (length a)" 
               using row_length_def Cons by auto 
    then have "mat 
                    ((length a) * row_length M2) 
                    (length M1 * length M2) 
                                    (M1  M2)" 
                using step2 by auto
    then have "Ball (set (M1M2)) (vec ((length a)*(row_length M2))) " 
                using mat_def by auto     
    from this have 3:
         "x. x  (set (M1  M2))  (vec ((length a)*(row_length M2)) x)" 
                using Ball_def by auto    
    have "mat 
              ((row_length M2)*(length a)) 
              (length M2) 
                 (vec_mat_Tensor a M2)" 
                 using well_defined_vec_mat_Tensor Cons.prems 
                 by auto
    then have "Ball 
                    (set (vec_mat_Tensor a M2)) 
                    (vec ((row_length M2)*(length a)))" 
                 using mat_def
                 by auto
    then have 4:
              "x. x  (set (vec_mat_Tensor a M2)) 
                         (vec ((length a)*(row_length M2)) x)"
                 using mult.commute by metis

    with 3 have 5: "x. (x  (set (vec_mat_Tensor a M2)))
                          (x  (set (M1  M2))) 
                                  (vec ((length a)*(row_length M2)) x)"  
                  by auto  
    have 6:"(a # M1  M2) = (vec_mat_Tensor a M2)@(M1 M2)" 
                  using Tensor.simps(2) by auto 
    then have "x  (set (a # M1  M2)) 
                  (x  (set (vec_mat_Tensor a M2)))(x  (set (M1  M2)))"
                  using set_def append_def by auto
    with 5 have 7:"x. (x   (set (a # M1  M2)))
                          (vec ((length a)*(row_length M2)) x)" 
                  by auto
    then have 8:
        "Ball (set (a # M1  M2)) (vec ((row_length (a#M1))*(row_length M2)))" 
                  using Ball_def 0 by auto   
    have "(length ((a#M1)M2)) = (length (a#M1))*(length M2)" 
                  using length_Tensor by metis
    with 7 8
       have "mat 
                     (row_length (a # M1) * row_length M2) 
                       (length (a # M1) * length M2) 
                                (a # M1  M2)"
                  using mat_def by (metis "0"  length_Tensor)
    then show ?thesis by auto
  qed
 then show ?case by auto
qed

theorem effective_well_defined_Tensor:
 assumes "(mat (row_length M1) (length M1) M1)" 
     and "(mat (row_length M2) (length M2) M2)"
 shows "mat 
            ((row_length M1)*(row_length M2)) 
            ((length M1)*(length M2)) 
                               (M1M2)"
 using well_defined_Tensor assms by auto


definition natmod::"nat  nat  nat" (infixl "nmod" 50)
where
 "natmod x y = nat ((int x) mod (int y))"

theorem times_elements:
 "i.((i<(length v))  (times a v)!i = f a (v!i))"
 apply(rule allI)
 proof(induct v)
  case Nil
   have "(length [] = 0)" 
          by auto
   then have "i <(length [])  False" 
          by auto
   moreover have "(times a []) = []" 
          using times.simps(1) by auto 
   ultimately have "(i<(length []))  (times a [])!i = f a ([]!i)" 
          by auto
   then have "i. ((i<(length []))  (times a [])!i = f a ([]!i))" 
          by auto
   then show ?case  by auto
  next   
  case (Cons x xs)
   have "i.((x#xs)!(i+1) = (xs)!i)" 
          by auto
   have 0:"((i<length (x#xs)) ((i<(length xs))  (i = (length xs))))" 
          by auto
   have 1:" ((i<length xs) ((times a xs)!i = f a (xs!i)))" 
         by (metis Cons.hyps)
   have "i.((x#xs)!(i+1) = (xs)!i)" by auto
   have "((i <length (x#xs)) (times a (x#xs))!i = f a ((x#xs)!i))"  
   proof(cases i)
    case 0
     have "((times a (x#xs))!i) = f a x" 
          using 0 times.simps(2) by auto
     then have "(times a (x#xs))!i = f a ((x#xs)!i)" 
          using 0 by auto
     then show ?thesis by auto
    next
    case (Suc j)
     have 1:"(times a (x#xs))!i = ((f a x)#(times a xs))!i" 
          using times.simps(2) by auto 
     have 2:"((f a x)#(times a xs))!i = (times a xs)!j" 
          using Suc by auto
     have 3:"(i <length (x#xs))  (j<length xs)" 
          using One_nat_def Suc Suc_eq_plus1 list.size(4) not_less_eq 
          by metis
     have 4:"(j<length xs)  ((times a xs)!j = (f a (xs!j)))" 
          using 1 by (metis Cons.hyps)
     have 5:"(x#xs)!i = (xs!j)" 
          using Suc by (metis nth_Cons_Suc)
     with 1 2 4  have "(j<length xs) 
                             ((times a (x#xs))!i = (f a ((x#xs)!i)))" 
          by auto
     with 3 have "(i <length (x#xs)) 
                             ((times a (x#xs))!i = (f a ((x#xs)!i)))" 
          by auto
     then show ?thesis  by auto
   qed
   then show ?case by auto
 qed

lemma simpl_times_elements:
 assumes "(i<length xs)" 
 shows "((i<(length v))  (times a v)!i = f a (v!i))"
 using times_elements by auto

(*some lemmas which are used to prove theorems*)
lemma append_simpl: "i<(length xs)  (xs@ys)!i = (xs!i)" 
 using nth_append  by metis

lemma append_simpl2: "i (length xs)  (xs@ys)!i = (ys!(i- (length xs)))" 
 using nth_append less_asym  leD  by metis

lemma append_simpl3: 
 assumes "i > (length y)"
 shows " (i <((length (z#zs))*(length y))) 
                   (i - (length y))< (length zs)*(length y)"
proof-
 have "length (z#zs) = (length zs)+1" 
       by auto
 then have "i <((length (z#zs))*(length y)) 
                    i <((length zs)+1)*(length y)"
       by auto
 then have 1: "i <((length (z#zs))*(length y)) 
                   (i <((length zs)*(length y)+ (length y)))" 
       by auto
 have "i <((length zs)*(length y)+ (length y)) 
                   = ((i - (length y)) <((length zs)*(length y)))"
       using assms by auto
 then have "(i <((length (z#zs))*(length y))) 
                   ((i - (length y)) <((length zs)*(length y)))"
       by auto
 then show ?thesis by auto
qed

lemma append_simpl4: 
"(i > (length y))
          ((i <((length (z#zs))*(length y)))) 
                 ((i - (length y))< (length zs)*(length y))"
    using append_simpl3 by auto

lemma vec_vec_Tensor_simpl: 
   "i<(length y)  (vec_vec_Tensor (z#zs) y)!i = (times z y)!i" 
proof-
 have a: "vec_vec_Tensor (z#zs) y = (times z y)@(vec_vec_Tensor zs y)" 
      by auto
 have b: "length (times z y) = (length y)" using preserving_length by auto
 have "i<(length (times z y)) 
           ((times z y)@(vec_vec_Tensor zs y))!i = (times z y)!i" 
      using append_simpl by metis
 with b have "i<(length y) 
           ((times z y)@(vec_vec_Tensor zs y))!i = (times z y)!i" 
      by auto
 with  a have "i<(length y) 
           (vec_vec_Tensor (z#zs) y)!i = (times z y)!i" 
      by auto
 then show ?thesis by auto
qed


lemma vec_vec_Tensor_simpl2: 
  "(i  (length y)) 
   ((vec_vec_Tensor (z#zs) y)!i = (vec_vec_Tensor zs y)!(i- (length y)))" 
 using vec_vec_Tensor.simps(2) append_simpl2  preserving_length 
 by metis

lemma division_product: 
 assumes "(b::int)>0"
 and "a b"
 shows " (a div b) = ((a - b) div b) + 1"
proof-
 fix c
 have "a -b 0" 
     using assms(2) by auto
 have 1: "a - b = a + (-1)*b" 
     by auto
 have "(b  0)  ((a + b * (-1)) div b = (-1) + a div b)" 
     using div_mult_self2 by metis
 with 1 assms(1) have "((a - b) div b) = (-1) + a div b" 
     using less_int_code(1) by auto
 then  have "(a div b) = ((a - b) div b) + 1" 
     by auto
 then show ?thesis 
     by auto
qed

lemma int_nat_div: 
   "(int a) div (int b) = int ((a::nat) div b)"
 by (metis zdiv_int)

lemma int_nat_eq: 
 assumes "int (a::nat) = int b"
 shows "a = b" 
 using  assms of_nat_eq_iff by auto

lemma nat_div: 
 assumes "(b::nat) > 0" 
     and "a > b"
 shows "(a div b) = ((a - b) div b) + 1"
proof-
 fix x
 have 1:"(int b)>0" 
      using assms(1) division_product by auto
 moreover have "(int a)>(int b)" 
      using assms(2) by auto
 with 1 have 2: "((int a) div (int b)) 
                   = (((int a) - (int b)) div (int b)) + 1" 
      using division_product by auto
 from int_nat_div have 3: "((int a) div (int b)) = int ( a div b)" 
      by auto
 from int_nat_div assms(2) have 4: 
        "(((int a) - (int b)) div (int b)) = int ((a - b) div b)" 
      by (metis (full_types) less_asym not_less of_nat_diff)
 have "(int x) + 1 = int (x +1)" 
      by auto
 with 2 3 4 have "int (a div b) = int (((a - b) div b) + 1)" 
      by auto
 with int_nat_eq have "(a div b) = ((a - b) div b) + 1" 
      by auto 
 then show ?thesis by auto
qed

lemma mod_eq:
 "(m::int) mod n = (m + (-1)*n) mod n"
 using mod_mult_self1 by metis

lemma nat_mod_eq: "int m mod int n = int (m mod n)"
  by (simp add: of_nat_mod)

lemma nat_mod: 
 assumes  "(m::nat) > n"
 shows "(m::nat) mod n = (m -n) mod n"
 using assms mod_if not_less_iff_gr_or_eq by auto 

lemma logic: 
 assumes "A  B" 
     and "¬A  B" 
 shows "B" 
 using assms(1) assms(2) by auto

theorem vec_vec_Tensor_elements:
 assumes " (y  [])"
 shows 
   "i.((i<((length x)*(length y)))
        ((vec_vec_Tensor x y)!i) 
             = f (x!(i div (length y))) (y!(i mod (length y))))"
 apply(rule allI)
 proof(induct x)
 case Nil
  have "(length [] = 0)" 
      by auto
  also have "length (vec_vec_Tensor [] y) = 0" 
      using vec_vec_Tensor.simps(1) by auto
  then have "i <(length (vec_vec_Tensor [] y))  False" 
      by auto
  moreover have "(vec_vec_Tensor [] y) = []" 
      by auto 
  moreover have 
   "(i<(length (vec_vec_Tensor [] y)))  
   ((vec_vec_Tensor x y)!i) = f (x!(i div (length y))) (y!(i mod (length y)))"  
      by auto
  then show ?case  
      by auto
 next
 case (Cons z zs)
  have 1:"vec_vec_Tensor (z#zs) y = (times z y)@(vec_vec_Tensor zs y)" 
      by auto
  have 2:"i<(length y)((times z y)!i = f z (y!i))" 
      using times_elements by auto
  moreover have 3:
        "i<(length y) 
            (vec_vec_Tensor (z#zs) y)!i = (times z y)!i" 
      using vec_vec_Tensor_simpl by auto
  moreover  have 35:
           "i<(length y)  (vec_vec_Tensor (z#zs) y)!i = f z (y!i)" 
      using calculation(1) calculation(2) by metis 
  have 4:"(y  [])  (length y) >0 " 
      by auto 
  have "(i <(length y))   ((i div (length y)) = 0)" 
      by auto
  then have  6:"(i <(length y))  (z#zs)!(i div (length y)) = z" 
      using nth_Cons_0 by auto
  then have 7:"(i <(length y))  (i mod (length y)) = i" 
      by auto
  with 2 6  
     have "(i < (length y)) 
         (times z y)!i 
                 = f  ((z#zs)!(i div (length y))) (y! (i mod (length y)))" 
      by auto 
  with 3 have step1:
      "((i < (length y)) 
           ((i<((length x)*(length y)) 
           ((vec_vec_Tensor (z#zs) y)!i 
                      =  f  
                             ((z#zs)!(i div (length y))) 
                              (y! (i mod (length y)))))))"
      by auto
  have "((length y)  i)  (i - (length y))  0" 
      by auto
  have step2: 
        "((length y) < i) 
            ((i < (length (z#zs)*(length y)))
           ((vec_vec_Tensor (z#zs) y)!i) 
                          = f 
                              ((z#zs)!(i div (length y))) 
                              (y!(i mod (length y))))"
  proof-
   have "(length y)>0" 
       using assms by auto
   then have 1: 
           "(i > (length y))
               (i div (length y)) = ((i-(length y)) div (length y)) + 1" 
       using nat_div by auto
   have "zs!j = (z#zs)!(j+1)" 
       by auto
   then have 
            "(zs!((i - (length y)) div (length y))) 
                     = (z#zs)!(((i - (length y)) div (length y))+1)"
       by auto
   with 1 have 2: 
           "(i > (length y))
               (zs!((i - (length y)) div (length y)) 
                     = (z#zs)!(i div (length y)))"
       by auto
   have "(i > (length y))
               ((i mod (length y)) 
                                 = ((i - (length y)) mod (length y)))" 
       using nat_mod by auto
   then have 3:
          "(i > (length y))
                  ((y! (i mod (length y))) 
                                = (y! ((i - (length y)) mod (length y))))" 
       by auto
   have 4:"(i > (length y))
                       (vec_vec_Tensor (z#zs) y)!i 
                                = (vec_vec_Tensor zs y)!(i- (length y))" 
       using vec_vec_Tensor_simpl2  by auto
   have 5: "(i > (length y)) 
                 ((i <((length (z#zs))*(length y)))) 
                          = (i - (length y)< (length zs)*(length y))"
       by auto
   then have 6:
             "i.((i<((length zs)*(length y)))
                        ((vec_vec_Tensor zs y)!i) 
                                 = f 
                                    (zs!(i div (length y))) 
                                    (y!(i mod (length y))))" 
       using Cons.hyps by auto
   with 5 have "(i > (length y))
                        ((i<((length (z#zs))*(length y)))
                        ((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)))
                                       ((vec_vec_Tensor zs y)!i) 
                                                = f 
                                                    (zs!(i div (length y))) 
                                                    (y!(i mod (length y))))"
       by auto
   with 6 have 
           "(i > (length y))
                ((i<((length (z#zs))*(length y)))
                 ((vec_vec_Tensor zs y)!(i -(length y))) 
                            = f 
                               (zs!((i -(length y)) div (length y))) 
                               (y!((i -(length y))  mod (length y))))" 
       by auto
   with 2 3 4 have  
            "(i > (length y))
                ((i<((length (z#zs))*(length y)))
                ((vec_vec_Tensor (z#zs) y)!i) 
                         =  f 
                               ((z#zs)!(i div (length y))) 
                               (y!(i mod (length y))))"
       by auto
    then show ?thesis  by auto
  qed
  have "((length y) = i) 
                      ((i < (length (z#zs)*(length y)))
                      ((vec_vec_Tensor (z#zs) y)!i) 
                                          = f 
                                              ((z#zs)!(i div (length y))) 
                                              (y!(i mod (length y))))"
  proof-
    have 1:"(i = (length y)) 
                   ((vec_vec_Tensor (z#zs) y)!i) 
                                        = (vec_vec_Tensor zs y)!0" 
           using vec_vec_Tensor_simpl2   by auto
    have 2:"(i = length y)  (i mod (length y)) = 0" 
           by auto
    have 3:"(i = length y)  (i div (length y)) = 1" 
           using 4 assms div_self less_numeral_extra(3)
           by auto
    have 4: "(i = length y) 
                   ((i < (length (z#zs))*(length y)) 
                               = (0 < (length zs)*(length y)))" 
           by auto
    have "(z#zs)!1 = (zs!0)" 
           by auto
    with 3 have 5:" (i = length y) 
                               ((z#zs)!(i div (length y))) = (zs!0)" 
           by auto 
    have " i.((i < (length zs)*(length y))
                               ((vec_vec_Tensor (zs) y)!i) 
                                             = f 
                                                 ((zs)!(i div (length y))) 
                                                 (y!(i mod (length y))))" 
           using Cons.hyps by auto  
    with 4 have 6:"(i = length y) 
                            ((0 < ((length zs)*(length y)))
                               (((vec_vec_Tensor (zs) y)!0) 
                                       = f ((zs)!0) (y!0))) 
                                         = ((i < ((length zs)*(length y)))
                                               (((vec_vec_Tensor zs y)!i) 
                                                = f 
                                                    ((zs)!(i div (length y)))
                                                    (y!(i mod (length y)))))" 
           by auto
    have 7: "(0 div (length y)) = 0" 
           by auto
    have 8: " (0 mod (length y)) = 0" 
           by auto
    have 9: "(0 < ((length zs)*(length y))) 
                        ((vec_vec_Tensor zs y)!0) 
                                           = f (zs!0) (y!0)" 
           using 7 8 Cons.hyps by auto
    with  4 5 8 have "(i = length y) 
                             ((i < (length (z#zs))*(length y)) 
                                      (((vec_vec_Tensor (zs) y)!0) 
                                             = f ((zs)!0) (y!0)))" 
           by auto
    with 1 2 5 have "(i = length y) 
                              ((i < (length (z#zs))*(length y)) 
                                  (((vec_vec_Tensor ((z#zs)) y)!i) 
                                            = f 
                                                 ((z#zs)!(i div (length y))) 
                                                 (y!(i mod (length y)))))" 
           by auto
    then show ?thesis by auto
  qed
  with step2 have step4: 
            "(i  (length y)) 
                        ((i < (length (z#zs))*(length y)) 
                        (((vec_vec_Tensor ((z#zs)) y)!i) 
                                    = f 
                                         ((z#zs)!(i div (length y))) 
                                         (y!(i mod (length y)))))" 
         by auto
  have "(i < (length y))  (i  (length y))" 
         by auto
  with step1 step4 have 
            "((i < (length (z#zs))*(length y)) 
                        (((vec_vec_Tensor ((z#zs)) y)!i) 
                                = f 
                                    ((z#zs)!(i div (length y))) 
                                     (y!(i mod (length y)))))" 
         using logic by (metis "6" "7" 35) 
  then show ?case by auto
qed

text‹a few more results that will be used later on›

lemma nat_int:  "nat (int x + int y) = x + y"
 using nat_int of_nat_add by auto

lemma int_nat_equiv: "(x > 0)  (nat ((int x) + -1)+1) = x"
proof-
 have "1 = nat (int 1)" 
   by auto
 have "-1 = -int 1" 
   by auto
 then have 1:"(nat ((int x) + -1)+1) 
                      = (nat ((int x) + -1) + (nat (int 1)))" 
   by auto
 then have 2:"(x > 0) 
                  nat ((int x) + -1 ) + (nat (int 1)) 
                                 =  (nat (((int x)  + -1) + (int 1)))" 
   using of_nat_add nat_int by auto
 have "(nat (((int x)  + -1) + (int 1))) = (nat ((int x) + -1 + (int 1)))" 
   by auto
 then have "(nat (((int x)  + -1) + (int 1))) = (nat ((int x)))" 
   by auto
 then have "(nat (((int x)  + -1) + (int 1))) = x" 
   by auto
 with 1 2 have " (x > 0)  nat ((int x) + -1 ) + 1 = x" 
   by auto
 then show ?thesis by auto
qed 

lemma list_int_nat: "(k>0)  ((x#xs)!k = xs!(nat ((int k)+-1)))"  
proof-
 fix  j
 have " ((x#xs)!(k+1) = xs!k)" 
      by auto
 have "j = (k+1)  (nat ((int j)+-1)) = k" 
      by auto
 moreover have "(nat ((int j)+-1)) = k 
                   ((nat ((int j)+-1)) + 1) = (k +1)" 
      by auto
 moreover have "(j>0)(((nat ((int j)+-1)) + 1) = j)" 
      using  int_nat_equiv by (auto)
 moreover have "(k>0)  ((x#xs)!k = xs!(nat ((int k)+-1)))" 
      using Suc_eq_plus1 int_nat_equiv nth_Cons_Suc by (metis)
  from this show ?thesis by auto
qed



lemma row_length_eq:
 "(mat  (row_length (a#b#N))  (length (a#b#N)) (a#b#N)) 
    
    (row_length (a#b#N) = (row_length (b#N)))" 
proof-
 have "(mat  (row_length (a#b#N))  (length (a#b#N)) (a#b#N)) 
                         (b  set (a#b#M))" 
           by auto
 moreover have 
         "(mat  (row_length (a#b#N))  (length (a#b#N)) (a#b#N)) 
                  (Ball (set (a#b#N)) (vec (row_length (a#b#N))))"
           using mat_def by metis
 moreover have "(mat  (row_length (a#b#N))  (length (a#b#N)) (a#b#N)) 
                   (b  (set (a#b#N)))
                     (vec (row_length (a#b#N)) b)"  
           by (metis calculation(2))
 then have "(mat  (row_length (a#b#N))  (length (a#b#N)) (a#b#N)) 
                          (length b) = (row_length (a#b#N))" 
            using vec_def by auto
 then have "(mat  (row_length (a#b#N))  (length (a#b#N)) (a#b#N)) 
                           (row_length (b#N)) 
                                       = (row_length (a#b#N))" 
            using row_length_def by auto
 then show ?thesis by auto
qed

text‹The following theorem tells us the relationship between entries of 
vec\_mat\_Tensor v M and entries of v and M respectivety›

theorem vec_mat_Tensor_elements: 
 "i.j.
  (((i<((length v)*(row_length M)))
  (j < (length M)))
  (mat (row_length M) (length M) M)
    ((vec_mat_Tensor v M)!j!i) 
               = f (v!(i div (row_length M))) (M!j!(i mod (row_length M))))"
 apply(rule allI)
 apply(rule allI)
 proof(induct M)
  case Nil
   have "row_length [] = 0" 
       using row_length_def by auto
   from this 
      have "(length v)*(row_length []) = 0" 
       by auto
   from this 
      have "((i<((length v)*(row_length [])))(j < (length [])))  False" 
       by auto
   moreover have "vec_mat_Tensor v [] = []" 
       by auto 
   moreover have "(((i<((length v)*(row_length [])))(j < (length [])))
                   ((vec_mat_Tensor v [])!j!i) 
                                = f (v!(i div (row_length []))) ([]!j!(i mod (row_length []))))"
       by auto
   from this 
       show ?case by auto
  next
  case (Cons a M)
   have "(((i<((length v)*(row_length (a#M))))
       (j < (length (a#M))))
       (mat (row_length (a#M)) (length (a#M)) (a#M))
            ((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(cases a)
    case Nil
     have "row_length ([]#M) = 0" 
          using row_length_def by auto
     then have 1:"(length v)*(row_length ([]#M)) = 0" 
          by auto
     then have "((i<((length v)*(row_length ([]#M))))
                (j < (length ([]#M))))  False" 
          by auto
     moreover have 
                 "(((i<((length v)*(row_length ([]#M))))
                  (j < (length ([]#M))))
                      ((vec_mat_Tensor v ([]#M))!j!i) = 
                                   f 
                                        (v!(i div (row_length ([]#M)))) 
                                        ([]!j!(i mod (row_length ([]#M)))))"
          using calculation by auto 
     then show ?thesis using Nil 1 less_nat_zero_code by (metis )
    next
    case (Cons x xs)
     have 1:"(a#M)!(j+1) = M!j" by auto
     have "(((i<((length v)*(row_length M)))
           (j < (length M)))
           (mat (row_length M) (length M) M)
              ((vec_mat_Tensor v M)!j!i) = f 
                                               (v!(i div (row_length M))) 
                                               (M!j!(i mod (row_length M))))" 
          using Cons.hyps by auto
     have 2: "(row_length (a#M)) = (length a)" 
          using row_length_def by auto
     then have 3:"(i< (row_length (a#M))*(length v)) 
                              = (i < (length a)*(length v))" 
          by auto
     have "a  []" 
          using Cons by auto
     then have 4:
         "i.((i < (length a)*(length v)) 
                ((vec_vec_Tensor v a)!i) = f 
                                               (v!(i div (length a))) 
                                               (a!(i mod (length a))))" 
          using vec_vec_Tensor_elements Cons.hyps mult.commute 
          by (simp add: mult.commute vec_vec_Tensor_elements)
     have "(vec_mat_Tensor v (a#M))!0 = (vec_vec_Tensor v a)" 
          using vec_mat_Tensor.simps(2) by auto
     with 2 4 have 5: 
       "i.((i < (row_length (a#M))*(length v)) 
            ((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)))))" 
          by auto 
     have "length (a#M)>0" 
          by auto
     with 5 have 6: 
       "(j = 0)
                    ((((i < (row_length (a#M))*(length v)) 
                    (j < (length (a#M))))
                    (mat (row_length (a#M)) (length (a#M)) (a#M))  
                           ((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))))))" 
          by auto 
     have "(((i < (row_length (a#M))*(length v))
         (j < (length (a#M))))
         (mat (row_length (a#M)) (length (a#M)) (a#M)) 
            
           ((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(cases M)
      case Nil
       have "(length (a#[])) = 1" 
              by auto
       then have "(j<(length (a#[]))) = (j = 0)" 
              by auto
       then have "((((i < (row_length (a#[]))*(length v)) 
               (j < (length (a#[]))))
                (mat (row_length (a#[])) (length (a#[])) (a#[]))   
                    ((vec_mat_Tensor v (a#[]))!j!i) 
                                 = f 
                                    (v!(i div (row_length (a#[])))) 
                                     ((a#[])!j!(i mod (row_length (a#[]))))))" 
              using 6 Nil by auto
       then show ?thesis using Nil by auto 
      next
      case (Cons b N)
       have 7:"(mat  (row_length (a#b#N))  (length (a#b#N)) (a#b#N)) 
                row_length (a#b#N) = (row_length (b#N))" 
              using row_length_eq by metis
       have 8: "(j>0) 
             ((vec_mat_Tensor v (b#N))!(nat ((int j)+-1))) 
                                  = (vec_mat_Tensor v (a#b#N))!j"
              using vec_mat_Tensor.simps(2) using list_int_nat by metis
       have 9: "(j>0) 
                  (((i < (row_length (b#N))*(length v))
                    ((nat ((int j)+-1)) < (length (b#N))))
                    (mat (row_length (b#N)) (length (b#N)) (b#N)) 
                        
             ((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)))))"
              using Cons.hyps Cons mult.commute by metis
       have "(j>0)  ((nat ((int j) + -1)) < (length (b#N))) 
                            ((nat ((int j) + -1) + 1) < length (a#b#N))"
              by auto
       then have 
           "(j>0) 
                  ((nat ((int j) + -1)) < (length (b#N))) = (j < length (a#b#N))"
              by auto
       then have  
         "(j>0) 
           (((i < (row_length (b#N))*(length v))  (j < length (a#b#N)))
              (mat (row_length (b#N)) (length (b#N)) (b#N))     
                    ((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)))))"
              using Cons.hyps Cons mult.commute by metis
       with 8 have "(j>0) 
                  (((i < (row_length (b#N))*(length v)) 
                      (j < length (a#b#N)))
                      (mat (row_length (b#N)) (length (b#N)) (b#N))   
                        
         ((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)))))"
              by auto
       also have "(j>0)  (b#N)!(nat ((int j)+-1)) = (a#b#N)!j" 
              using list_int_nat by metis
       moreover have " (j>0)  
                    (((i < (row_length (b#N))*(length v)) 
                    (j < length (a#b#N)))
                    (mat (row_length (b#N)) (length (b#N)) (b#N))   
                       
                         ((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)))))"
              by (metis calculation(1) calculation(2))
       then have  
           "(j>0) 
              (((i < (row_length (b#N))*(length v)) 
                  (j < length (a#b#N)))
                  (mat (row_length (a#b#N)) (length (a#b#N)) (a#b#N))   
                   
                        ((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)))))"
              using reduct_matrix by (metis)
       moreover  have "(mat (row_length (a#b#N)) (length (a#b#N)) (a#b#N))
                   (row_length (b#N)) = (row_length (a#b#N))" 
              by (metis "7" Cons)
       moreover have 10:"(j>0) 
                      (((i < (row_length (a#b#N))*(length v)) 
                        (j < length (a#b#N)))
                        (mat (row_length (a