[STATEMENT]
theorem elements_matrix_distribution2:
fixes A1 A2 B1 B2 i j
assumes wf1:"mat (row_length A1) (length A1) A1"
   and wf2:"mat (row_length A2) (length A2) A2"
   and wf3:"mat (row_length B1) (length B1) B1"
   and wf4:"mat (row_length B2) (length B2) B2"
   and matchAA:"length A1 = row_length A2"
   and matchBB:"length B1 = row_length B2"
   and non_Nil:"(A1 \<noteq> [])\<and>(A2 \<noteq> [])\<and>(B1 \<noteq> [])\<and>(B2 \<noteq> [])"    
         and i:"i<(row_length A1)*(row_length B1)" and j:"j< (length A2)*(length B2)" 
shows
"((A1 \<otimes> B1)\<circ>(A2 \<otimes> B2))!j!i
  =  scalar_product 
          (vec_vec_Tensor 
                    (row A1 (i div row_length B1)) 
                    (row B1 (i mod row_length B1))) 
          (vec_vec_Tensor 
                    (col A2 (j div length B2)) 
                    (col B2 (j mod length B2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
have 1:"mat 
              ((row_length A1)*(row_length B1)) 
              ((length A1)*(length B1)) 
                                   (A1 \<otimes> B1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length A1 * row_length B1) (length A1 * length B1) (A1 \<otimes> B1)
[PROOF STEP]
using wf1 wf3 well_defined_Tensor
[PROOF STATE]
proof (prove)
using this:
mat (row_length A1) (length A1) A1
mat (row_length B1) (length B1) B1
mat (row_length ?M1.0) (length ?M1.0) ?M1.0 \<and> mat (row_length ?M2.0) (length ?M2.0) ?M2.0 \<Longrightarrow> mat (row_length ?M1.0 * row_length ?M2.0) (length ?M1.0 * length ?M2.0) (?M1.0 \<otimes> ?M2.0)

goal (1 subgoal):
 1. mat (row_length A1 * row_length B1) (length A1 * length B1) (A1 \<otimes> B1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat (row_length A1 * row_length B1) (length A1 * length B1) (A1 \<otimes> B1)

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mat (row_length A1 * row_length B1) (length A1 * length B1) (A1 \<otimes> B1)

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
have 2:"mat 
                   ((row_length A2)*(row_length B2)) 
                   ((length A2)*(length B2)) 
                                   (A2 \<otimes> B2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length A2 * row_length B2) (length A2 * length B2) (A2 \<otimes> B2)
[PROOF STEP]
using wf2 wf4 well_defined_Tensor
[PROOF STATE]
proof (prove)
using this:
mat (row_length A2) (length A2) A2
mat (row_length B2) (length B2) B2
mat (row_length ?M1.0) (length ?M1.0) ?M1.0 \<and> mat (row_length ?M2.0) (length ?M2.0) ?M2.0 \<Longrightarrow> mat (row_length ?M1.0 * row_length ?M2.0) (length ?M1.0 * length ?M2.0) (?M1.0 \<otimes> ?M2.0)

goal (1 subgoal):
 1. mat (row_length A2 * row_length B2) (length A2 * length B2) (A2 \<otimes> B2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat (row_length A2 * row_length B2) (length A2 * length B2) (A2 \<otimes> B2)

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mat (row_length A2 * row_length B2) (length A2 * length B2) (A2 \<otimes> B2)

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
have 3:"((length A1)*(length B1)) 
                           = ((row_length A2)*(row_length B2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length A1 * length B1 = row_length A2 * row_length B2
[PROOF STEP]
using matchAA matchBB
[PROOF STATE]
proof (prove)
using this:
length A1 = row_length A2
length B1 = row_length B2

goal (1 subgoal):
 1. length A1 * length B1 = row_length A2 * row_length B2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length A1 * length B1 = row_length A2 * row_length B2

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mat (row_length A1 * row_length B1) (length A1 * length B1) (A1 \<otimes> B1)
mat (row_length A2 * row_length B2) (length A2 * length B2) (A2 \<otimes> B2)
length A1 * length B1 = row_length A2 * row_length B2
[PROOF STEP]
have 4:"((A1\<otimes>B1)\<circ>(A2\<otimes>B2))!j!i 
                        = scalar_product (row (A1 \<otimes> B1) i) (col (A2 \<otimes> B2) j)"
[PROOF STATE]
proof (prove)
using this:
mat (row_length A1 * row_length B1) (length A1 * length B1) (A1 \<otimes> B1)
mat (row_length A2 * row_length B2) (length A2 * length B2) (A2 \<otimes> B2)
length A1 * length B1 = row_length A2 * row_length B2

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (row (A1 \<otimes> B1) i) (col (A2 \<otimes> B2) j)
[PROOF STEP]
using i j matrix_mult_index non_Nil mat_mult_index 
                    row_length_mat scalar_product_def
[PROOF STATE]
proof (prove)
using this:
mat (row_length A1 * row_length B1) (length A1 * length B1) (A1 \<otimes> B1)
mat (row_length A2 * row_length B2) (length A2 * length B2) (A2 \<otimes> B2)
length A1 * length B1 = row_length A2 * row_length B2
i < row_length A1 * row_length B1
j < length A2 * length B2
\<lbrakk>?m1.0 \<noteq> []; mat ?nr ?n ?m1.0; mat ?n ?nc ?m2.0; ?i < ?nr; ?j < ?nc\<rbrakk> \<Longrightarrow> (?m1.0 \<circ> ?m2.0) ! ?j ! ?i = scalar_product (row ?m1.0 ?i) (col ?m2.0 ?j)
A1 \<noteq> [] \<and> A2 \<noteq> [] \<and> B1 \<noteq> [] \<and> B2 \<noteq> []
\<lbrakk>mat ?nr ?n ?m1.0; mat ?n ?nc ?m2.0; ?i < ?nr; ?j < ?nc\<rbrakk> \<Longrightarrow> mat_multI ?ze ?pl ?ti ?nr ?m1.0 ?m2.0 ! ?j ! ?i = scalar_prodI ?ze ?pl ?ti (row ?m1.0 ?i) (col ?m2.0 ?j)
row_length (?m1.0 \<otimes> ?m2.0) = row_length ?m1.0 * row_length ?m2.0
scalar_product ?v ?w = scalar_prodI zer (+) (*) ?v ?w

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (row (A1 \<otimes> B1) i) (col (A2 \<otimes> B2) j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (row (A1 \<otimes> B1) i) (col (A2 \<otimes> B2) j)

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (row (A1 \<otimes> B1) i) (col (A2 \<otimes> B2) j)

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
have "(row (A1 \<otimes> B1) i)
                  =  vec_vec_Tensor 
                           (row A1 (i div row_length B1)) 
                           (row B1 (i mod row_length B1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (A1 \<otimes> B1) i = vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))
[PROOF STEP]
using  wf1 wf3 i effective_row_formula
[PROOF STATE]
proof (prove)
using this:
mat (row_length A1) (length A1) A1
mat (row_length B1) (length B1) B1
i < row_length A1 * row_length B1
\<lbrakk>?i < row_length ?M1.0 * row_length ?M2.0; mat (row_length ?M1.0) (length ?M1.0) ?M1.0; mat (row_length ?M2.0) (length ?M2.0) ?M2.0\<rbrakk> \<Longrightarrow> row (?M1.0 \<otimes> ?M2.0) ?i = vec_vec_Tensor (row ?M1.0 (?i div row_length ?M2.0)) (row ?M2.0 (?i mod row_length ?M2.0))

goal (1 subgoal):
 1. row (A1 \<otimes> B1) i = vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row (A1 \<otimes> B1) i = vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
row (A1 \<otimes> B1) i = vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
have " col (A2 \<otimes> B2) j =  vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (A2 \<otimes> B2) j = vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2))
[PROOF STEP]
using wf2 wf4 j col_formula
[PROOF STATE]
proof (prove)
using this:
mat (row_length A2) (length A2) A2
mat (row_length B2) (length B2) B2
j < length A2 * length B2
\<forall>j. j < length ?M1.0 * length ?M2.0 \<and> mat (row_length ?M1.0) (length ?M1.0) ?M1.0 \<and> mat (row_length ?M2.0) (length ?M2.0) ?M2.0 \<longrightarrow> col (?M1.0 \<otimes> ?M2.0) j = vec_vec_Tensor (col ?M1.0 (j div length ?M2.0)) (col ?M2.0 (j mod length ?M2.0))

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

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (row (A1 \<otimes> B1) i) (col (A2 \<otimes> B2) j)
row (A1 \<otimes> B1) i = vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))
col (A2 \<otimes> B2) j = vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (row (A1 \<otimes> B1) i) (col (A2 \<otimes> B2) j)
row (A1 \<otimes> B1) i = vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))
col (A2 \<otimes> B2) j = vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2))

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))

goal:
No subgoals!
[PROOF STEP]
qed