[STATEMENT]
lemma " \<And>(a::nat) b.(times  a  b) =(times  b  a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. a * b = b * a
[PROOF STEP]
by auto


[STATEMENT]
lemma fixes M1 M2 M3
      shows "(mat (row_length M1) (length M1) M1)
            \<and>(mat (row_length M2) (length M2) M2)
            \<and>(mat (row_length M3) (length M3) M3)
             \<Longrightarrow> (M1 \<otimes> (M2 \<otimes> M3)) = ((M1 \<otimes> M2) \<otimes> M3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<and> mat (row_length M3) (length M3) M3 \<Longrightarrow> M1 \<otimes> (M2 \<otimes> M3) = M1 \<otimes> M2 \<otimes> M3
[PROOF STEP]
using associativity
[PROOF STATE]
proof (prove)
using this:
mat (row_length ?M1.0) (length ?M1.0) ?M1.0 \<and> mat (row_length ?M2.0) (length ?M2.0) ?M2.0 \<and> mat (row_length ?M3.0) (length ?M3.0) ?M3.0 \<Longrightarrow> ?M1.0 \<otimes> (?M2.0 \<otimes> ?M3.0) = ?M1.0 \<otimes> ?M2.0 \<otimes> ?M3.0

goal (1 subgoal):
 1. mat (row_length M1) (length M1) M1 \<and> mat (row_length M2) (length M2) M2 \<and> mat (row_length M3) (length M3) M3 \<Longrightarrow> M1 \<otimes> (M2 \<otimes> M3) = M1 \<otimes> M2 \<otimes> M3
[PROOF STEP]
by auto


[STATEMENT]
lemma ma :
 assumes wf1: "mat nr n m1"
     and wf2: "mat n nc m2"
        and i: "i < nr"
        and j: "j < nc"
 shows "mat_multI zer g f nr m1 m2 ! j ! i
                  = scalar_prodI zer g f (row m1 i) (col m2 j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_multI zer (+) (*) nr m1 m2 ! j ! i = scalar_prodI zer (+) (*) (row m1 i) (col m2 j)
[PROOF STEP]
using mat_mult_index i j wf1 wf2
[PROOF STATE]
proof (prove)
using this:
\<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)
i < nr
j < nc
mat nr n m1
mat n nc m2

goal (1 subgoal):
 1. mat_multI zer (+) (*) nr m1 m2 ! j ! i = scalar_prodI zer (+) (*) (row m1 i) (col m2 j)
[PROOF STEP]
by metis


[STATEMENT]
lemma matrix_index:
  assumes wf1: "mat (row_length m1) n m1"
      and wf2: "mat n nc m2"
        and i: "i < (row_length m1)"
        and j: "j < nc"
 shows  "matrix_mult  m1 m2 ! j ! i
                 = scalar_product  (row m1 i) (col m2 j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (m1 \<circ> m2) ! j ! i = scalar_product (row m1 i) (col m2 j)
[PROOF STEP]
using wf1 wf2 i j ma scalar_product_def
[PROOF STATE]
proof (prove)
using this:
mat (row_length m1) n m1
mat n nc m2
i < row_length m1
j < nc
\<lbrakk>mat ?nr ?n ?m1.0; mat ?n ?nc ?m2.0; ?i < ?nr; ?j < ?nc\<rbrakk> \<Longrightarrow> mat_multI zer (+) (*) ?nr ?m1.0 ?m2.0 ! ?j ! ?i = scalar_prodI zer (+) (*) (row ?m1.0 ?i) (col ?m2.0 ?j)
scalar_product ?v ?w = scalar_prodI zer (+) (*) ?v ?w

goal (1 subgoal):
 1. (m1 \<circ> m2) ! j ! i = scalar_product (row m1 i) (col m2 j)
[PROOF STEP]
by auto


[STATEMENT]
lemma unique_row_col:
 assumes "mat nr1 nc1 M" and "mat nr2 nc2 M" and "M \<noteq> []"
 shows "nr1 = nr2" and "nc1 = nc2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nr1 = nr2 &&& nc1 = nc2
[PROOF STEP]
proof(cases M)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. M = [] \<Longrightarrow> nr1 = nr2
 2. \<And>a list. M = a # list \<Longrightarrow> nr1 = nr2
 3. nc1 = nc2
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
M = []

goal (3 subgoals):
 1. M = [] \<Longrightarrow> nr1 = nr2
 2. \<And>a list. M = a # list \<Longrightarrow> nr1 = nr2
 3. nc1 = nc2
[PROOF STEP]
show "nr1 = nr2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nr1 = nr2
[PROOF STEP]
using assms(3) Nil
[PROOF STATE]
proof (prove)
using this:
M \<noteq> []
M = []

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

goal (2 subgoals):
 1. \<And>a list. M = a # list \<Longrightarrow> nr1 = nr2
 2. nc1 = nc2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a list. M = a # list \<Longrightarrow> nr1 = nr2
 2. nc1 = nc2
[PROOF STEP]
case (Cons v M)
[PROOF STATE]
proof (state)
this:
M = v # M

goal (2 subgoals):
 1. \<And>a list. M = a # list \<Longrightarrow> nr1 = nr2
 2. nc1 = nc2
[PROOF STEP]
have 1:"v \<in> set (v#M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> set (v # M)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
M = v # M

goal (1 subgoal):
 1. v \<in> set (v # M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> set (v # M)

goal (2 subgoals):
 1. \<And>a list. M = a # list \<Longrightarrow> nr1 = nr2
 2. nc1 = nc2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> set (v # M)
[PROOF STEP]
have "length v = nr1"
[PROOF STATE]
proof (prove)
using this:
v \<in> set (v # M)

goal (1 subgoal):
 1. length v = nr1
[PROOF STEP]
using assms(1) mat_def Ball_def vec_def  Cons
[PROOF STATE]
proof (prove)
using this:
v \<in> set (v # M)
mat nr1 nc1 M
mat ?nr ?nc ?m = (length ?m = ?nc \<and> Ball (set ?m) (vec ?nr))
Ball ?A ?P = (\<forall>x. x \<in> ?A \<longrightarrow> ?P x)
vec ?n ?x = (length ?x = ?n)
M = v # M

goal (1 subgoal):
 1. length v = nr1
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
length v = nr1

goal (2 subgoals):
 1. \<And>a list. M = a # list \<Longrightarrow> nr1 = nr2
 2. nc1 = nc2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length v = nr1

goal (2 subgoals):
 1. \<And>a list. M = a # list \<Longrightarrow> nr1 = nr2
 2. nc1 = nc2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length v = nr1
[PROOF STEP]
have "length v = nr2"
[PROOF STATE]
proof (prove)
using this:
length v = nr1

goal (1 subgoal):
 1. length v = nr2
[PROOF STEP]
using 1 assms(2) mat_def Ball_def vec_def  Cons
[PROOF STATE]
proof (prove)
using this:
length v = nr1
v \<in> set (v # M)
mat nr2 nc2 M
mat ?nr ?nc ?m = (length ?m = ?nc \<and> Ball (set ?m) (vec ?nr))
Ball ?A ?P = (\<forall>x. x \<in> ?A \<longrightarrow> ?P x)
vec ?n ?x = (length ?x = ?n)
M = v # M

goal (1 subgoal):
 1. length v = nr2
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
length v = nr2

goal (2 subgoals):
 1. \<And>a list. M = a # list \<Longrightarrow> nr1 = nr2
 2. nc1 = nc2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length v = nr1
length v = nr2
[PROOF STEP]
show "nr1 = nr2"
[PROOF STATE]
proof (prove)
using this:
length v = nr1
length v = nr2

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

goal (1 subgoal):
 1. nc1 = nc2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nc1 = nc2
[PROOF STEP]
have "length M = nc1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length M = nc1
[PROOF STEP]
using mat_def assms(1)
[PROOF STATE]
proof (prove)
using this:
mat ?nr ?nc ?m = (length ?m = ?nc \<and> Ball (set ?m) (vec ?nr))
mat nr1 nc1 M

goal (1 subgoal):
 1. length M = nc1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length M = nc1

goal (1 subgoal):
 1. nc1 = nc2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length M = nc1

goal (1 subgoal):
 1. nc1 = nc2
[PROOF STEP]
have "length M = nc2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length M = nc2
[PROOF STEP]
using mat_def assms(2)
[PROOF STATE]
proof (prove)
using this:
mat ?nr ?nc ?m = (length ?m = ?nc \<and> Ball (set ?m) (vec ?nr))
mat nr2 nc2 M

goal (1 subgoal):
 1. length M = nc2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length M = nc2

goal (1 subgoal):
 1. nc1 = nc2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length M = nc1
length M = nc2
[PROOF STEP]
show "nc1 = nc2"
[PROOF STATE]
proof (prove)
using this:
length M = nc1
length M = nc2

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matrix_mult_index:
 assumes "m1 \<noteq> []"
  and  wf1: "mat nr n m1"
  and wf2: "mat n nc m2"
    and i: "i < nr"
    and j: "j < nc"
 shows  "matrix_mult  m1 m2 ! j ! i = scalar_product  (row m1 i) (col m2 j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (m1 \<circ> m2) ! j ! i = scalar_product (row m1 i) (col m2 j)
[PROOF STEP]
using matrix_index unique_row_col assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mat (row_length ?m1.0) ?n ?m1.0; mat ?n ?nc ?m2.0; ?i < row_length ?m1.0; ?j < ?nc\<rbrakk> \<Longrightarrow> (?m1.0 \<circ> ?m2.0) ! ?j ! ?i = scalar_product (row ?m1.0 ?i) (col ?m2.0 ?j)
\<lbrakk>mat ?nr1.0 ?nc1.0 ?M; mat ?nr2.0 ?nc2.0 ?M; ?M \<noteq> []\<rbrakk> \<Longrightarrow> ?nr1.0 = ?nr2.0
\<lbrakk>mat ?nr1.0 ?nc1.0 ?M; mat ?nr2.0 ?nc2.0 ?M; ?M \<noteq> []\<rbrakk> \<Longrightarrow> ?nc1.0 = ?nc2.0
m1 \<noteq> []
mat nr n m1
mat n nc m2
i < nr
j < nc

goal (1 subgoal):
 1. (m1 \<circ> m2) ! j ! i = scalar_product (row m1 i) (col m2 j)
[PROOF STEP]
by (metis matrix_row_length)


[STATEMENT]
lemma non_empty_mat_mult:
 assumes wf1:"mat nr n A"
     and wf2:"mat n nc B"
         and "A \<noteq> []" and " B \<noteq> []"
 shows  "A \<circ> B \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<circ> B \<noteq> []
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<circ> B \<noteq> []
[PROOF STEP]
have "mat nr nc (A \<circ> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat nr nc (A \<circ> B)
[PROOF STEP]
using assms(1) assms(2) mat_mult  assms(3) matrix_row_length unique_row_col(1)
[PROOF STATE]
proof (prove)
using this:
mat nr n A
mat n nc B
\<lbrakk>mat ?nr ?n ?m1.0; mat ?n ?nc ?m2.0\<rbrakk> \<Longrightarrow> mat ?nr ?nc (mat_multI ?ze ?pl ?ti ?nr ?m1.0 ?m2.0)
A \<noteq> []
mat ?nr ?nc ?M \<Longrightarrow> mat (row_length ?M) (length ?M) ?M
\<lbrakk>mat ?nr1.0 ?nc1.0 ?M; mat ?nr2.0 ?nc2.0 ?M; ?M \<noteq> []\<rbrakk> \<Longrightarrow> ?nr1.0 = ?nr2.0

goal (1 subgoal):
 1. mat nr nc (A \<circ> B)
[PROOF STEP]
by (metis)
[PROOF STATE]
proof (state)
this:
mat nr nc (A \<circ> B)

goal (1 subgoal):
 1. A \<circ> B \<noteq> []
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat nr nc (A \<circ> B)
[PROOF STEP]
have "length (A \<circ> B) = nc"
[PROOF STATE]
proof (prove)
using this:
mat nr nc (A \<circ> B)

goal (1 subgoal):
 1. length (A \<circ> B) = nc
[PROOF STEP]
using mat_def
[PROOF STATE]
proof (prove)
using this:
mat nr nc (A \<circ> B)
mat ?nr ?nc ?m = (length ?m = ?nc \<and> Ball (set ?m) (vec ?nr))

goal (1 subgoal):
 1. length (A \<circ> B) = nc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (A \<circ> B) = nc

goal (1 subgoal):
 1. A \<circ> B \<noteq> []
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length (A \<circ> B) = nc

goal (1 subgoal):
 1. A \<circ> B \<noteq> []
[PROOF STEP]
have "nc > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < nc
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < nc
[PROOF STEP]
have "length B = nc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length B = nc
[PROOF STEP]
using assms(2) mat_def
[PROOF STATE]
proof (prove)
using this:
mat n nc B
mat ?nr ?nc ?m = (length ?m = ?nc \<and> Ball (set ?m) (vec ?nr))

goal (1 subgoal):
 1. length B = nc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length B = nc

goal (1 subgoal):
 1. 0 < nc
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length B = nc
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length B = nc

goal (1 subgoal):
 1. 0 < nc
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
length B = nc
B \<noteq> []

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < nc

goal (1 subgoal):
 1. A \<circ> B \<noteq> []
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < nc

goal (1 subgoal):
 1. A \<circ> B \<noteq> []
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < nc
[PROOF STEP]
have "length (A \<circ> B) > 0"
[PROOF STATE]
proof (prove)
using this:
0 < nc

goal (1 subgoal):
 1. 0 < length (A \<circ> B)
[PROOF STEP]
by (metis calculation(1))
[PROOF STATE]
proof (state)
this:
0 < length (A \<circ> B)

goal (1 subgoal):
 1. A \<circ> B \<noteq> []
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < length (A \<circ> B)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < length (A \<circ> B)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tensor_compose_distribution1:
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> [])"
 shows "mat ((row_length A1)*(row_length B1))
            ((length A2)*(length B2))
                    ((A1\<circ>A2)\<otimes>(B1\<circ>B2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length A1 * row_length B1) (length A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat (row_length A1 * row_length B1) (length A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
[PROOF STEP]
have 0:"mat (row_length A1) (length A2) (matrix_mult A1 A2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length A1) (length A2) (A1 \<circ> A2)
[PROOF STEP]
using wf1 wf2  mat_mult matchAA
[PROOF STATE]
proof (prove)
using this:
mat (row_length A1) (length A1) A1
mat (row_length A2) (length A2) A2
\<lbrakk>mat ?nr ?n ?m1.0; mat ?n ?nc ?m2.0\<rbrakk> \<Longrightarrow> mat ?nr ?nc (mat_multI ?ze ?pl ?ti ?nr ?m1.0 ?m2.0)
length A1 = row_length A2

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

goal (1 subgoal):
 1. mat (row_length A1 * row_length B1) (length A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat (row_length A1) (length A2) (A1 \<circ> A2)
[PROOF STEP]
have 1:"mat (row_length (A1 \<circ> A2)) (length (A1 \<circ> A2)) (matrix_mult A1 A2)"
[PROOF STATE]
proof (prove)
using this:
mat (row_length A1) (length A2) (A1 \<circ> A2)

goal (1 subgoal):
 1. mat (row_length (A1 \<circ> A2)) (length (A1 \<circ> A2)) (A1 \<circ> A2)
[PROOF STEP]
by (metis matrix_row_length)
[PROOF STATE]
proof (state)
this:
mat (row_length (A1 \<circ> A2)) (length (A1 \<circ> A2)) (A1 \<circ> A2)

goal (1 subgoal):
 1. mat (row_length A1 * row_length B1) (length A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat (row_length (A1 \<circ> A2)) (length (A1 \<circ> A2)) (A1 \<circ> A2)
[PROOF STEP]
have 2: "(row_length (A1 \<circ> A2)) = (row_length A1)" and "length (A1 \<circ> A2) = length A2"
[PROOF STATE]
proof (prove)
using this:
mat (row_length (A1 \<circ> A2)) (length (A1 \<circ> A2)) (A1 \<circ> A2)

goal (1 subgoal):
 1. row_length (A1 \<circ> A2) = row_length A1 &&& length (A1 \<circ> A2) = length A2
[PROOF STEP]
using non_empty_mat_mult unique_row_col 0
[PROOF STATE]
proof (prove)
using this:
mat (row_length (A1 \<circ> A2)) (length (A1 \<circ> A2)) (A1 \<circ> A2)
\<lbrakk>mat ?nr ?n ?A; mat ?n ?nc ?B; ?A \<noteq> []; ?B \<noteq> []\<rbrakk> \<Longrightarrow> ?A \<circ> ?B \<noteq> []
\<lbrakk>mat ?nr1.0 ?nc1.0 ?M; mat ?nr2.0 ?nc2.0 ?M; ?M \<noteq> []\<rbrakk> \<Longrightarrow> ?nr1.0 = ?nr2.0
\<lbrakk>mat ?nr1.0 ?nc1.0 ?M; mat ?nr2.0 ?nc2.0 ?M; ?M \<noteq> []\<rbrakk> \<Longrightarrow> ?nc1.0 = ?nc2.0
mat (row_length A1) (length A2) (A1 \<circ> A2)

goal (1 subgoal):
 1. row_length (A1 \<circ> A2) = row_length A1 &&& length (A1 \<circ> A2) = length A2
[PROOF STEP]
apply (metis length_0_conv mat_empty_column_length non_Nil)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (A1 \<circ> A2) = length A2
[PROOF STEP]
by (metis "0" "1" mat_empty_column_length unique_row_col(2))
[PROOF STATE]
proof (state)
this:
row_length (A1 \<circ> A2) = row_length A1
length (A1 \<circ> A2) = length A2

goal (1 subgoal):
 1. mat (row_length A1 * row_length B1) (length A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
row_length (A1 \<circ> A2) = row_length A1
length (A1 \<circ> A2) = length A2

goal (1 subgoal):
 1. mat (row_length A1 * row_length B1) (length A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
[PROOF STEP]
have 3:"mat (row_length B1) (length B2) (matrix_mult B1 B2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length B1) (length B2) (B1 \<circ> B2)
[PROOF STEP]
using wf3 wf4 matchBB mat_mult
[PROOF STATE]
proof (prove)
using this:
mat (row_length B1) (length B1) B1
mat (row_length B2) (length B2) B2
length B1 = row_length B2
\<lbrakk>mat ?nr ?n ?m1.0; mat ?n ?nc ?m2.0\<rbrakk> \<Longrightarrow> mat ?nr ?nc (mat_multI ?ze ?pl ?ti ?nr ?m1.0 ?m2.0)

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

goal (1 subgoal):
 1. mat (row_length A1 * row_length B1) (length A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat (row_length B1) (length B2) (B1 \<circ> B2)
[PROOF STEP]
have 4:"mat (row_length (B1 \<circ> B2)) (length (B1 \<circ> B2)) (matrix_mult B1 B2)"
[PROOF STATE]
proof (prove)
using this:
mat (row_length B1) (length B2) (B1 \<circ> B2)

goal (1 subgoal):
 1. mat (row_length (B1 \<circ> B2)) (length (B1 \<circ> B2)) (B1 \<circ> B2)
[PROOF STEP]
by (metis matrix_row_length)
[PROOF STATE]
proof (state)
this:
mat (row_length (B1 \<circ> B2)) (length (B1 \<circ> B2)) (B1 \<circ> B2)

goal (1 subgoal):
 1. mat (row_length A1 * row_length B1) (length A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat (row_length (B1 \<circ> B2)) (length (B1 \<circ> B2)) (B1 \<circ> B2)
[PROOF STEP]
have 5: "(row_length (B1 \<circ> B2)) = (row_length B1)" and "length (B1 \<circ> B2) = length B2"
[PROOF STATE]
proof (prove)
using this:
mat (row_length (B1 \<circ> B2)) (length (B1 \<circ> B2)) (B1 \<circ> B2)

goal (1 subgoal):
 1. row_length (B1 \<circ> B2) = row_length B1 &&& length (B1 \<circ> B2) = length B2
[PROOF STEP]
using non_empty_mat_mult unique_row_col 3
[PROOF STATE]
proof (prove)
using this:
mat (row_length (B1 \<circ> B2)) (length (B1 \<circ> B2)) (B1 \<circ> B2)
\<lbrakk>mat ?nr ?n ?A; mat ?n ?nc ?B; ?A \<noteq> []; ?B \<noteq> []\<rbrakk> \<Longrightarrow> ?A \<circ> ?B \<noteq> []
\<lbrakk>mat ?nr1.0 ?nc1.0 ?M; mat ?nr2.0 ?nc2.0 ?M; ?M \<noteq> []\<rbrakk> \<Longrightarrow> ?nr1.0 = ?nr2.0
\<lbrakk>mat ?nr1.0 ?nc1.0 ?M; mat ?nr2.0 ?nc2.0 ?M; ?M \<noteq> []\<rbrakk> \<Longrightarrow> ?nc1.0 = ?nc2.0
mat (row_length B1) (length B2) (B1 \<circ> B2)

goal (1 subgoal):
 1. row_length (B1 \<circ> B2) = row_length B1 &&& length (B1 \<circ> B2) = length B2
[PROOF STEP]
apply (metis length_0_conv mat_empty_column_length non_Nil)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (B1 \<circ> B2) = length B2
[PROOF STEP]
by (metis "3" "4" mat_empty_column_length unique_row_col(2))
[PROOF STATE]
proof (state)
this:
row_length (B1 \<circ> B2) = row_length B1
length (B1 \<circ> B2) = length B2

goal (1 subgoal):
 1. mat (row_length A1 * row_length B1) (length A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
row_length (B1 \<circ> B2) = row_length B1
length (B1 \<circ> B2) = length B2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
row_length (B1 \<circ> B2) = row_length B1
length (B1 \<circ> B2) = length B2

goal (1 subgoal):
 1. mat (row_length A1 * row_length B1) (length A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
[PROOF STEP]
using 1 4 5 well_defined_Tensor
[PROOF STATE]
proof (prove)
using this:
row_length (B1 \<circ> B2) = row_length B1
length (B1 \<circ> B2) = length B2
mat (row_length (A1 \<circ> A2)) (length (A1 \<circ> A2)) (A1 \<circ> A2)
mat (row_length (B1 \<circ> B2)) (length (B1 \<circ> B2)) (B1 \<circ> B2)
row_length (B1 \<circ> B2) = row_length 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 A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
[PROOF STEP]
by (metis "2" calculation(2))
[PROOF STATE]
proof (state)
this:
mat (row_length A1 * row_length B1) (length A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma effective_tensor_compose_distribution1:
 "matrix_match A1 A2 B1 B2 \<Longrightarrow> mat ((row_length A1)*(row_length B1))
            ((length A2)*(length B2))
                    ((A1\<circ>A2)\<otimes>(B1\<circ>B2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_match A1 A2 B1 B2 \<Longrightarrow> mat (row_length A1 * row_length B1) (length A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
[PROOF STEP]
using tensor_compose_distribution1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mat (row_length ?A1.0) (length ?A1.0) ?A1.0; mat (row_length ?A2.0) (length ?A2.0) ?A2.0; mat (row_length ?B1.0) (length ?B1.0) ?B1.0; mat (row_length ?B2.0) (length ?B2.0) ?B2.0; length ?A1.0 = row_length ?A2.0; length ?B1.0 = row_length ?B2.0; ?A1.0 \<noteq> [] \<and> ?A2.0 \<noteq> [] \<and> ?B1.0 \<noteq> [] \<and> ?B2.0 \<noteq> []\<rbrakk> \<Longrightarrow> mat (row_length ?A1.0 * row_length ?B1.0) (length ?A2.0 * length ?B2.0) (?A1.0 \<circ> ?A2.0 \<otimes> ?B1.0 \<circ> ?B2.0)

goal (1 subgoal):
 1. matrix_match A1 A2 B1 B2 \<Longrightarrow> mat (row_length A1 * row_length B1) (length A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
[PROOF STEP]
unfolding matrix_match_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mat (row_length ?A1.0) (length ?A1.0) ?A1.0; mat (row_length ?A2.0) (length ?A2.0) ?A2.0; mat (row_length ?B1.0) (length ?B1.0) ?B1.0; mat (row_length ?B2.0) (length ?B2.0) ?B2.0; length ?A1.0 = row_length ?A2.0; length ?B1.0 = row_length ?B2.0; ?A1.0 \<noteq> [] \<and> ?A2.0 \<noteq> [] \<and> ?B1.0 \<noteq> [] \<and> ?B2.0 \<noteq> []\<rbrakk> \<Longrightarrow> mat (row_length ?A1.0 * row_length ?B1.0) (length ?A2.0 * length ?B2.0) (?A1.0 \<circ> ?A2.0 \<otimes> ?B1.0 \<circ> ?B2.0)

goal (1 subgoal):
 1. mat (row_length A1) (length A1) A1 \<and> mat (row_length A2) (length A2) A2 \<and> mat (row_length B1) (length B1) B1 \<and> mat (row_length B2) (length B2) B2 \<and> length A1 = row_length A2 \<and> length B1 = row_length B2 \<and> A1 \<noteq> [] \<and> A2 \<noteq> [] \<and> B1 \<noteq> [] \<and> B2 \<noteq> [] \<Longrightarrow> mat (row_length A1 * row_length B1) (length A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
[PROOF STEP]
by auto


[STATEMENT]
lemma tensor_compose_distribution2:
 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> [])"
 shows "mat ((row_length A1)*(row_length B1))
            ((length A2)*(length B2))
                    ((A1 \<otimes> B1) \<circ>(A2 \<otimes>B2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length A1 * row_length B1) (length A2 * length B2) ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat (row_length A1 * row_length B1) (length A2 * length B2) ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2))
[PROOF STEP]
have "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. mat (row_length A1 * row_length B1) (length A2 * length B2) ((A1 \<otimes> B1) \<circ> (A2 \<otimes> 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. mat (row_length A1 * row_length B1) (length A2 * length B2) ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2))
[PROOF STEP]
have "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. mat (row_length A1 * row_length B1) (length A2 * length B2) ((A1 \<otimes> B1) \<circ> (A2 \<otimes> 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. mat (row_length A1 * row_length B1) (length A2 * length B2) ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2))
[PROOF STEP]
have "((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. mat (row_length A1 * row_length B1) (length A2 * length B2) ((A1 \<otimes> B1) \<circ> (A2 \<otimes> 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]
show ?thesis
[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. mat (row_length A1 * row_length B1) (length A2 * length B2) ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2))
[PROOF STEP]
using mat_mult row_length_mat
[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
\<lbrakk>mat ?nr ?n ?m1.0; mat ?n ?nc ?m2.0\<rbrakk> \<Longrightarrow> mat ?nr ?nc (mat_multI ?ze ?pl ?ti ?nr ?m1.0 ?m2.0)
row_length (?m1.0 \<otimes> ?m2.0) = row_length ?m1.0 * row_length ?m2.0

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem tensor_non_empty: assumes "A \<noteq> []" and "B \<noteq> []"
 shows "A \<otimes> B \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<otimes> B \<noteq> []
[PROOF STEP]
using  assms(1) assms(2) length_0_conv length_Tensor mult_is_0
[PROOF STATE]
proof (prove)
using this:
A \<noteq> []
B \<noteq> []
(length ?xs = 0) = (?xs = [])
length (?M1.0 \<otimes> ?M2.0) = length ?M1.0 * length ?M2.0
(?m * ?n = 0) = (?m = 0 \<or> ?n = 0)

goal (1 subgoal):
 1. A \<otimes> B \<noteq> []
[PROOF STEP]
by metis


[STATEMENT]
theorem non_empty_distribution:
 assumes "mat nr1 n1 A1"
     and "mat n1 nc1 A2"
     and "mat nr2 n2 B1"
     and "mat n2 nc2 B2"
     and "A1 \<noteq> []" and "B1 \<noteq> []" and "A2 \<noteq> []" and "B2 \<noteq> []"
 shows "((A1\<circ>A2)\<otimes>(B1\<circ>B2)) \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A1 \<circ> A2 \<otimes> B1 \<circ> B2 \<noteq> []
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A1 \<circ> A2 \<otimes> B1 \<circ> B2 \<noteq> []
[PROOF STEP]
have "A1 \<circ> A2 \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A1 \<circ> A2 \<noteq> []
[PROOF STEP]
using assms  non_empty_mat_mult
[PROOF STATE]
proof (prove)
using this:
mat nr1 n1 A1
mat n1 nc1 A2
mat nr2 n2 B1
mat n2 nc2 B2
A1 \<noteq> []
B1 \<noteq> []
A2 \<noteq> []
B2 \<noteq> []
\<lbrakk>mat ?nr ?n ?A; mat ?n ?nc ?B; ?A \<noteq> []; ?B \<noteq> []\<rbrakk> \<Longrightarrow> ?A \<circ> ?B \<noteq> []

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

goal (1 subgoal):
 1. A1 \<circ> A2 \<otimes> B1 \<circ> B2 \<noteq> []
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A1 \<circ> A2 \<noteq> []

goal (1 subgoal):
 1. A1 \<circ> A2 \<otimes> B1 \<circ> B2 \<noteq> []
[PROOF STEP]
have "B1 \<circ> B2 \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B1 \<circ> B2 \<noteq> []
[PROOF STEP]
using assms  non_empty_mat_mult
[PROOF STATE]
proof (prove)
using this:
mat nr1 n1 A1
mat n1 nc1 A2
mat nr2 n2 B1
mat n2 nc2 B2
A1 \<noteq> []
B1 \<noteq> []
A2 \<noteq> []
B2 \<noteq> []
\<lbrakk>mat ?nr ?n ?A; mat ?n ?nc ?B; ?A \<noteq> []; ?B \<noteq> []\<rbrakk> \<Longrightarrow> ?A \<circ> ?B \<noteq> []

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

goal (1 subgoal):
 1. A1 \<circ> A2 \<otimes> B1 \<circ> B2 \<noteq> []
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A1 \<circ> A2 \<noteq> []
B1 \<circ> B2 \<noteq> []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A1 \<circ> A2 \<noteq> []
B1 \<circ> B2 \<noteq> []

goal (1 subgoal):
 1. A1 \<circ> A2 \<otimes> B1 \<circ> B2 \<noteq> []
[PROOF STEP]
using tensor_non_empty
[PROOF STATE]
proof (prove)
using this:
A1 \<circ> A2 \<noteq> []
B1 \<circ> B2 \<noteq> []
\<lbrakk>?A \<noteq> []; ?B \<noteq> []\<rbrakk> \<Longrightarrow> ?A \<otimes> ?B \<noteq> []

goal (1 subgoal):
 1. A1 \<circ> A2 \<otimes> B1 \<circ> B2 \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A1 \<circ> A2 \<otimes> B1 \<circ> B2 \<noteq> []

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma effective_tensor_compose_distribution2:"matrix_match A1 A2 B1 B2 \<Longrightarrow>
   mat ((row_length A1)*(row_length B1))
            ((length A2)*(length B2))
                    ((A1 \<otimes> B1) \<circ>(A2 \<otimes>B2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_match A1 A2 B1 B2 \<Longrightarrow> mat (row_length A1 * row_length B1) (length A2 * length B2) ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2))
[PROOF STEP]
using tensor_compose_distribution2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mat (row_length ?A1.0) (length ?A1.0) ?A1.0; mat (row_length ?A2.0) (length ?A2.0) ?A2.0; mat (row_length ?B1.0) (length ?B1.0) ?B1.0; mat (row_length ?B2.0) (length ?B2.0) ?B2.0; length ?A1.0 = row_length ?A2.0; length ?B1.0 = row_length ?B2.0; ?A1.0 \<noteq> [] \<and> ?A2.0 \<noteq> [] \<and> ?B1.0 \<noteq> [] \<and> ?B2.0 \<noteq> []\<rbrakk> \<Longrightarrow> mat (row_length ?A1.0 * row_length ?B1.0) (length ?A2.0 * length ?B2.0) ((?A1.0 \<otimes> ?B1.0) \<circ> (?A2.0 \<otimes> ?B2.0))

goal (1 subgoal):
 1. matrix_match A1 A2 B1 B2 \<Longrightarrow> mat (row_length A1 * row_length B1) (length A2 * length B2) ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2))
[PROOF STEP]
unfolding matrix_match_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mat (row_length ?A1.0) (length ?A1.0) ?A1.0; mat (row_length ?A2.0) (length ?A2.0) ?A2.0; mat (row_length ?B1.0) (length ?B1.0) ?B1.0; mat (row_length ?B2.0) (length ?B2.0) ?B2.0; length ?A1.0 = row_length ?A2.0; length ?B1.0 = row_length ?B2.0; ?A1.0 \<noteq> [] \<and> ?A2.0 \<noteq> [] \<and> ?B1.0 \<noteq> [] \<and> ?B2.0 \<noteq> []\<rbrakk> \<Longrightarrow> mat (row_length ?A1.0 * row_length ?B1.0) (length ?A2.0 * length ?B2.0) ((?A1.0 \<otimes> ?B1.0) \<circ> (?A2.0 \<otimes> ?B2.0))

goal (1 subgoal):
 1. mat (row_length A1) (length A1) A1 \<and> mat (row_length A2) (length A2) A2 \<and> mat (row_length B1) (length B1) B1 \<and> mat (row_length B2) (length B2) B2 \<and> length A1 = row_length A2 \<and> length B1 = row_length B2 \<and> A1 \<noteq> [] \<and> A2 \<noteq> [] \<and> B1 \<noteq> [] \<and> B2 \<noteq> [] \<Longrightarrow> mat (row_length A1 * row_length B1) (length A2 * length B2) ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2))
[PROOF STEP]
by auto


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

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


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

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


[STATEMENT]
theorem elements_matrix_distribution_1:
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<(row_length A1)*(row_length B1)" and "j< (length A2)*(length B2)"
shows
"((matrix_mult A1  A2)\<otimes>(matrix_mult B1  B2))!j!i
  =  f (scalar_product (row A1 (i div (row_length B1)))
                        (col A2  (j div (length B2))))
       (scalar_product (row B1 (i mod (row_length B1)))
                       (col B2 (j mod (length B2))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = scalar_product (row A1 (i div row_length B1)) (col A2 (j div length B2)) * scalar_product (row B1 (i mod row_length B1)) (col B2 (j mod length B2))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = scalar_product (row A1 (i div row_length B1)) (col A2 (j div length B2)) * scalar_product (row B1 (i mod row_length B1)) (col B2 (j mod length B2))
[PROOF STEP]
have 0:"((matrix_mult A1  A2)\<otimes>(matrix_mult B1  B2)) \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A1 \<circ> A2 \<otimes> B1 \<circ> B2 \<noteq> []
[PROOF STEP]
using non_empty_distribution assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mat ?nr1.0 ?n1.0 ?A1.0; mat ?n1.0 ?nc1.0 ?A2.0; mat ?nr2.0 ?n2.0 ?B1.0; mat ?n2.0 ?nc2.0 ?B2.0; ?A1.0 \<noteq> []; ?B1.0 \<noteq> []; ?A2.0 \<noteq> []; ?B2.0 \<noteq> []\<rbrakk> \<Longrightarrow> ?A1.0 \<circ> ?A2.0 \<otimes> ?B1.0 \<circ> ?B2.0 \<noteq> []
mat (row_length A1) (length A1) A1
mat (row_length A2) (length A2) A2
mat (row_length B1) (length B1) B1
mat (row_length B2) (length B2) B2
length A1 = row_length A2
length B1 = row_length B2
A1 \<noteq> [] \<and> A2 \<noteq> [] \<and> B1 \<noteq> [] \<and> B2 \<noteq> []
i < row_length A1 * row_length B1
j < length A2 * length B2

goal (1 subgoal):
 1. A1 \<circ> A2 \<otimes> B1 \<circ> B2 \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A1 \<circ> A2 \<otimes> B1 \<circ> B2 \<noteq> []

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

goal (1 subgoal):
 1. mat (row_length A1 * row_length B1) (length A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
[PROOF STEP]
using tensor_compose_distribution1 assms
[PROOF STATE]
proof (prove)
using this:
A1 \<circ> A2 \<otimes> B1 \<circ> B2 \<noteq> []
\<lbrakk>mat (row_length ?A1.0) (length ?A1.0) ?A1.0; mat (row_length ?A2.0) (length ?A2.0) ?A2.0; mat (row_length ?B1.0) (length ?B1.0) ?B1.0; mat (row_length ?B2.0) (length ?B2.0) ?B2.0; length ?A1.0 = row_length ?A2.0; length ?B1.0 = row_length ?B2.0; ?A1.0 \<noteq> [] \<and> ?A2.0 \<noteq> [] \<and> ?B1.0 \<noteq> [] \<and> ?B2.0 \<noteq> []\<rbrakk> \<Longrightarrow> mat (row_length ?A1.0 * row_length ?B1.0) (length ?A2.0 * length ?B2.0) (?A1.0 \<circ> ?A2.0 \<otimes> ?B1.0 \<circ> ?B2.0)
mat (row_length A1) (length A1) A1
mat (row_length A2) (length A2) A2
mat (row_length B1) (length B1) B1
mat (row_length B2) (length B2) B2
length A1 = row_length A2
length B1 = row_length B2
A1 \<noteq> [] \<and> A2 \<noteq> [] \<and> B1 \<noteq> [] \<and> B2 \<noteq> []
i < row_length A1 * row_length B1
j < length A2 * length B2

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

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

goal (1 subgoal):
 1. mat (row_length (A1 \<circ> A2 \<otimes> B1 \<circ> B2)) (length (A1 \<circ> A2 \<otimes> B1 \<circ> B2)) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
[PROOF STEP]
by (metis matrix_row_length)
[PROOF STATE]
proof (state)
this:
mat (row_length (A1 \<circ> A2 \<otimes> B1 \<circ> B2)) (length (A1 \<circ> A2 \<otimes> B1 \<circ> B2)) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)

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

goal (1 subgoal):
 1. row_length A1 * row_length B1 = row_length (A1 \<circ> A2 \<otimes> B1 \<circ> B2) &&& length A2 * length B2 = length (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
[PROOF STEP]
using 0 1 unique_row_col
[PROOF STATE]
proof (prove)
using this:
mat (row_length (A1 \<circ> A2 \<otimes> B1 \<circ> B2)) (length (A1 \<circ> A2 \<otimes> B1 \<circ> B2)) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
A1 \<circ> A2 \<otimes> B1 \<circ> B2 \<noteq> []
mat (row_length A1 * row_length B1) (length A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
\<lbrakk>mat ?nr1.0 ?nc1.0 ?M; mat ?nr2.0 ?nc2.0 ?M; ?M \<noteq> []\<rbrakk> \<Longrightarrow> ?nr1.0 = ?nr2.0
\<lbrakk>mat ?nr1.0 ?nc1.0 ?M; mat ?nr2.0 ?nc2.0 ?M; ?M \<noteq> []\<rbrakk> \<Longrightarrow> ?nc1.0 = ?nc2.0

goal (1 subgoal):
 1. row_length A1 * row_length B1 = row_length (A1 \<circ> A2 \<otimes> B1 \<circ> B2) &&& length A2 * length B2 = length (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
[PROOF STEP]
apply metis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length A2 * length B2 = length (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
[PROOF STEP]
using 0 1 2 unique_row_col
[PROOF STATE]
proof (prove)
using this:
A1 \<circ> A2 \<otimes> B1 \<circ> B2 \<noteq> []
mat (row_length A1 * row_length B1) (length A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
mat (row_length (A1 \<circ> A2 \<otimes> B1 \<circ> B2)) (length (A1 \<circ> A2 \<otimes> B1 \<circ> B2)) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
\<lbrakk>mat ?nr1.0 ?nc1.0 ?M; mat ?nr2.0 ?nc2.0 ?M; ?M \<noteq> []\<rbrakk> \<Longrightarrow> ?nr1.0 = ?nr2.0
\<lbrakk>mat ?nr1.0 ?nc1.0 ?M; mat ?nr2.0 ?nc2.0 ?M; ?M \<noteq> []\<rbrakk> \<Longrightarrow> ?nc1.0 = ?nc2.0

goal (1 subgoal):
 1. length A2 * length B2 = length (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
row_length A1 * row_length B1 = row_length (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
length A2 * length B2 = length (A1 \<circ> A2 \<otimes> B1 \<circ> B2)

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

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

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

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

goal (1 subgoal):
 1. (j < length A2 * length B2) = (j < length (A1 \<circ> A2 \<otimes> B1 \<circ> B2))
[PROOF STEP]
by (metis)
[PROOF STATE]
proof (state)
this:
(j < length A2 * length B2) = (j < length (A1 \<circ> A2 \<otimes> B1 \<circ> B2))

goal (1 subgoal):
 1. (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = scalar_product (row A1 (i div row_length B1)) (col A2 (j div length B2)) * scalar_product (row B1 (i mod row_length B1)) (col B2 (j mod length B2))
[PROOF STEP]
have 4:"mat (row_length A1) (length A2) (A1 \<circ> A2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length A1) (length A2) (A1 \<circ> A2)
[PROOF STEP]
using assms mat_mult
[PROOF STATE]
proof (prove)
using this:
mat (row_length A1) (length A1) A1
mat (row_length A2) (length A2) A2
mat (row_length B1) (length B1) B1
mat (row_length B2) (length B2) B2
length A1 = row_length A2
length B1 = row_length B2
A1 \<noteq> [] \<and> A2 \<noteq> [] \<and> B1 \<noteq> [] \<and> B2 \<noteq> []
i < row_length A1 * row_length B1
j < length A2 * length B2
\<lbrakk>mat ?nr ?n ?m1.0; mat ?n ?nc ?m2.0\<rbrakk> \<Longrightarrow> mat ?nr ?nc (mat_multI ?ze ?pl ?ti ?nr ?m1.0 ?m2.0)

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

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

goal (1 subgoal):
 1. mat (row_length (A1 \<circ> A2)) (length (A1 \<circ> A2)) (A1 \<circ> A2)
[PROOF STEP]
using  matrix_row_length
[PROOF STATE]
proof (prove)
using this:
mat (row_length A1) (length A2) (A1 \<circ> A2)
mat ?nr ?nc ?M \<Longrightarrow> mat (row_length ?M) (length ?M) ?M

goal (1 subgoal):
 1. mat (row_length (A1 \<circ> A2)) (length (A1 \<circ> A2)) (A1 \<circ> A2)
[PROOF STEP]
by (metis)
[PROOF STATE]
proof (state)
this:
mat (row_length (A1 \<circ> A2)) (length (A1 \<circ> A2)) (A1 \<circ> A2)

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

goal (1 subgoal):
 1. row_length A1 = row_length (A1 \<circ> A2)
[PROOF STEP]
by (metis "0" Tensor.simps(1) unique_row_col(1))
[PROOF STATE]
proof (state)
this:
row_length A1 = row_length (A1 \<circ> A2)

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

goal (1 subgoal):
 1. length A2 = length (A1 \<circ> A2)
[PROOF STEP]
by (metis  mat_empty_column_length unique_row_col(2))
[PROOF STATE]
proof (state)
this:
length A2 = length (A1 \<circ> A2)

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

goal (1 subgoal):
 1. mat (row_length B1) (length B2) (B1 \<circ> B2)
[PROOF STEP]
using assms mat_mult
[PROOF STATE]
proof (prove)
using this:
length A2 = length (A1 \<circ> A2)
mat (row_length A1) (length A1) A1
mat (row_length A2) (length A2) A2
mat (row_length B1) (length B1) B1
mat (row_length B2) (length B2) B2
length A1 = row_length A2
length B1 = row_length B2
A1 \<noteq> [] \<and> A2 \<noteq> [] \<and> B1 \<noteq> [] \<and> B2 \<noteq> []
i < row_length A1 * row_length B1
j < length A2 * length B2
\<lbrakk>mat ?nr ?n ?m1.0; mat ?n ?nc ?m2.0\<rbrakk> \<Longrightarrow> mat ?nr ?nc (mat_multI ?ze ?pl ?ti ?nr ?m1.0 ?m2.0)

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

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

goal (1 subgoal):
 1. mat (row_length (B1 \<circ> B2)) (length (B1 \<circ> B2)) (B1 \<circ> B2)
[PROOF STEP]
using  matrix_row_length
[PROOF STATE]
proof (prove)
using this:
mat (row_length B1) (length B2) (B1 \<circ> B2)
mat ?nr ?nc ?M \<Longrightarrow> mat (row_length ?M) (length ?M) ?M

goal (1 subgoal):
 1. mat (row_length (B1 \<circ> B2)) (length (B1 \<circ> B2)) (B1 \<circ> B2)
[PROOF STEP]
by (metis)
[PROOF STATE]
proof (state)
this:
mat (row_length (B1 \<circ> B2)) (length (B1 \<circ> B2)) (B1 \<circ> B2)

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

goal (1 subgoal):
 1. row_length B1 = row_length (B1 \<circ> B2)
[PROOF STEP]
by (metis "3" "6" assms(8) less_nat_zero_code mult_cancel2 mult_is_0 mult.commute row_length_mat)
[PROOF STATE]
proof (state)
this:
row_length B1 = row_length (B1 \<circ> B2)

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

goal (1 subgoal):
 1. length B2 = length (B1 \<circ> B2)
[PROOF STEP]
by (metis  mat_empty_column_length unique_row_col(2))
[PROOF STATE]
proof (state)
this:
length B2 = length (B1 \<circ> B2)

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

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

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

goal (1 subgoal):
 1. i < row_length (A1 \<circ> A2) * row_length (B1 \<circ> B2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(i < row_length A1 * row_length B1) = (i < row_length (A1 \<circ> A2) * row_length (B1 \<circ> B2))
mat (row_length A1) (length A1) A1
mat (row_length A2) (length A2) A2
mat (row_length B1) (length B1) B1
mat (row_length B2) (length B2) B2
length A1 = row_length A2
length B1 = row_length B2
A1 \<noteq> [] \<and> A2 \<noteq> [] \<and> B1 \<noteq> [] \<and> B2 \<noteq> []
i < row_length A1 * row_length B1
j < length A2 * length B2

goal (1 subgoal):
 1. i < row_length (A1 \<circ> A2) * row_length (B1 \<circ> B2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < row_length (A1 \<circ> A2) * row_length (B1 \<circ> B2)

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

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

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

goal (1 subgoal):
 1. j < length (A1 \<circ> A2) * length (B1 \<circ> B2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(j < length A2 * length B2) = (j < length (A1 \<circ> A2) * length (B1 \<circ> B2))
mat (row_length A1) (length A1) A1
mat (row_length A2) (length A2) A2
mat (row_length B1) (length B1) B1
mat (row_length B2) (length B2) B2
length A1 = row_length A2
length B1 = row_length B2
A1 \<noteq> [] \<and> A2 \<noteq> [] \<and> B1 \<noteq> [] \<and> B2 \<noteq> []
i < row_length A1 * row_length B1
j < length A2 * length B2

goal (1 subgoal):
 1. j < length (A1 \<circ> A2) * length (B1 \<circ> B2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < length (A1 \<circ> A2) * length (B1 \<circ> B2)

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

goal (1 subgoal):
 1. (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = (A1 \<circ> A2) ! (j div length (B1 \<circ> B2)) ! (i div row_length (B1 \<circ> B2)) * (B1 \<circ> B2) ! (j mod length (B1 \<circ> B2)) ! (i mod row_length (B1 \<circ> B2))
[PROOF STEP]
using 5 9 13 15 effective_matrix_Tensor_elements
[PROOF STATE]
proof (prove)
using this:
j < length (A1 \<circ> A2) * length (B1 \<circ> B2)
mat (row_length (A1 \<circ> A2)) (length (A1 \<circ> A2)) (A1 \<circ> A2)
mat (row_length (B1 \<circ> B2)) (length (B1 \<circ> B2)) (B1 \<circ> B2)
i < row_length (A1 \<circ> A2) * row_length (B1 \<circ> B2)
j < length (A1 \<circ> A2) * length (B1 \<circ> B2)
\<lbrakk>?i < row_length ?M1.0 * row_length ?M2.0; ?j < length ?M1.0 * 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> (?M1.0 \<otimes> ?M2.0) ! ?j ! ?i = ?M1.0 ! (?j div length ?M2.0) ! (?i div row_length ?M2.0) * ?M2.0 ! (?j mod length ?M2.0) ! (?i mod row_length ?M2.0)

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

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

goal (1 subgoal):
 1. (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = (A1 \<circ> A2) ! (j div length B2) ! (i div row_length B1) * (B1 \<circ> B2) ! (j mod length B2) ! (i mod row_length B1)
[PROOF STEP]
using 10 11
[PROOF STATE]
proof (prove)
using this:
(A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = (A1 \<circ> A2) ! (j div length (B1 \<circ> B2)) ! (i div row_length (B1 \<circ> B2)) * (B1 \<circ> B2) ! (j mod length (B1 \<circ> B2)) ! (i mod row_length (B1 \<circ> B2))
row_length B1 = row_length (B1 \<circ> B2)
length B2 = length (B1 \<circ> B2)

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

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

goal (1 subgoal):
 1. (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = scalar_product (row A1 (i div row_length B1)) (col A2 (j div length B2)) * scalar_product (row B1 (i mod row_length B1)) (col B2 (j mod length B2))
[PROOF STEP]
have " ((A1\<circ>A2)!(j div (length B2))!(i div (row_length B1)))
               = (scalar_product (row A1 (i div (row_length B1)) ) (col A2 (j div (length B2)) ))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A1 \<circ> A2) ! (j div length B2) ! (i div row_length B1) = scalar_product (row A1 (i div row_length B1)) (col A2 (j div length B2))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (A1 \<circ> A2) ! (j div length B2) ! (i div row_length B1) = scalar_product (row A1 (i div row_length B1)) (col A2 (j div length B2))
[PROOF STEP]
have "j div (length B2) < (length A2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j div length B2 < length A2
[PROOF STEP]
using div_left_ineq assms
[PROOF STATE]
proof (prove)
using this:
?x < ?y * ?z \<Longrightarrow> ?x div ?z < ?y
mat (row_length A1) (length A1) A1
mat (row_length A2) (length A2) A2
mat (row_length B1) (length B1) B1
mat (row_length B2) (length B2) B2
length A1 = row_length A2
length B1 = row_length B2
A1 \<noteq> [] \<and> A2 \<noteq> [] \<and> B1 \<noteq> [] \<and> B2 \<noteq> []
i < row_length A1 * row_length B1
j < length A2 * length B2

goal (1 subgoal):
 1. j div length B2 < length A2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j div length B2 < length A2

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

goal (1 subgoal):
 1. (A1 \<circ> A2) ! (j div length B2) ! (i div row_length B1) = scalar_product (row A1 (i div row_length B1)) (col A2 (j div length B2))
[PROOF STEP]
have "i div (row_length B1) < (row_length A1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i div row_length B1 < row_length A1
[PROOF STEP]
using assms div_left_ineq
[PROOF STATE]
proof (prove)
using this:
mat (row_length A1) (length A1) A1
mat (row_length A2) (length A2) A2
mat (row_length B1) (length B1) B1
mat (row_length B2) (length B2) B2
length A1 = row_length A2
length B1 = row_length B2
A1 \<noteq> [] \<and> A2 \<noteq> [] \<and> B1 \<noteq> [] \<and> B2 \<noteq> []
i < row_length A1 * row_length B1
j < length A2 * length B2
?x < ?y * ?z \<Longrightarrow> ?x div ?z < ?y

goal (1 subgoal):
 1. i div row_length B1 < row_length A1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i div row_length B1 < row_length A1

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

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

goal (1 subgoal):
 1. mat (length A1) (length A2) A2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat (length A1) (length A2) A2

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

goal (1 subgoal):
 1. (A1 \<circ> A2) ! (j div length B2) ! (i div row_length B1) = scalar_product (row A1 (i div row_length B1)) (col A2 (j div length B2))
[PROOF STEP]
using wf1  non_Nil matrix_mult_index
[PROOF STATE]
proof (prove)
using this:
j div length B2 < length A2
i div row_length B1 < row_length A1
mat (length A1) (length A2) A2
mat (row_length A1) (length A1) A1
A1 \<noteq> [] \<and> A2 \<noteq> [] \<and> B1 \<noteq> [] \<and> B2 \<noteq> []
\<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)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(A1 \<circ> A2) ! (j div length B2) ! (i div row_length B1) = scalar_product (row A1 (i div row_length B1)) (col A2 (j div length B2))

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

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

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

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

goal (1 subgoal):
 1. j mod length B2 < length B2
[PROOF STEP]
by (metis calculation less_nat_zero_code mod_less_divisor mult_is_0 neq0_conv)
[PROOF STATE]
proof (state)
this:
j mod length B2 < length B2

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

goal (1 subgoal):
 1. (B1 \<circ> B2) ! (j mod length B2) ! (i mod row_length B1) = scalar_product (row B1 (i mod row_length B1)) (col B2 (j mod length B2))
[PROOF STEP]
have "i mod (row_length B1) < (row_length B1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i mod row_length B1 < row_length B1
[PROOF STEP]
by (metis assms(8) less_nat_zero_code mod_less_divisor mult_is_0 neq0_conv)
[PROOF STATE]
proof (state)
this:
i mod row_length B1 < row_length B1

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

goal (1 subgoal):
 1. (B1 \<circ> B2) ! (j mod length B2) ! (i mod row_length B1) = scalar_product (row B1 (i mod row_length B1)) (col B2 (j mod length B2))
[PROOF STEP]
have "mat (length B1) (length B2) B2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (length B1) (length B2) B2
[PROOF STEP]
using wf4 matchBB
[PROOF STATE]
proof (prove)
using this:
mat (row_length B2) (length B2) B2
length B1 = row_length B2

goal (1 subgoal):
 1. mat (length B1) (length B2) B2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat (length B1) (length B2) B2

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

goal (1 subgoal):
 1. (B1 \<circ> B2) ! (j mod length B2) ! (i mod row_length B1) = scalar_product (row B1 (i mod row_length B1)) (col B2 (j mod length B2))
[PROOF STEP]
using wf3 non_Nil matrix_mult_index
[PROOF STATE]
proof (prove)
using this:
j mod length B2 < length B2
i mod row_length B1 < row_length B1
mat (length B1) (length B2) B2
mat (row_length B1) (length B1) B1
A1 \<noteq> [] \<and> A2 \<noteq> [] \<and> B1 \<noteq> [] \<and> B2 \<noteq> []
\<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)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(B1 \<circ> B2) ! (j mod length B2) ! (i mod row_length B1) = scalar_product (row B1 (i mod row_length B1)) (col B2 (j mod length B2))

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma effective_elements_matrix_distribution1:
 "matrix_compose_cond A1 A2 B1 B2 i j \<Longrightarrow>
 ((matrix_mult A1  A2)\<otimes>(matrix_mult B1  B2))!j!i
  =  f (scalar_product (row A1 (i div (row_length B1))) (col A2  (j div (length B2))))
       (scalar_product (row B1 (i mod (row_length B1))) (col B2 (j mod (length B2))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_compose_cond A1 A2 B1 B2 i j \<Longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = scalar_product (row A1 (i div row_length B1)) (col A2 (j div length B2)) * scalar_product (row B1 (i mod row_length B1)) (col B2 (j mod length B2))
[PROOF STEP]
using  elements_matrix_distribution_1 matrix_compose_cond_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mat (row_length ?A1.0) (length ?A1.0) ?A1.0; mat (row_length ?A2.0) (length ?A2.0) ?A2.0; mat (row_length ?B1.0) (length ?B1.0) ?B1.0; mat (row_length ?B2.0) (length ?B2.0) ?B2.0; length ?A1.0 = row_length ?A2.0; length ?B1.0 = row_length ?B2.0; ?A1.0 \<noteq> [] \<and> ?A2.0 \<noteq> [] \<and> ?B1.0 \<noteq> [] \<and> ?B2.0 \<noteq> []; ?i < row_length ?A1.0 * row_length ?B1.0; ?j < length ?A2.0 * length ?B2.0\<rbrakk> \<Longrightarrow> (?A1.0 \<circ> ?A2.0 \<otimes> ?B1.0 \<circ> ?B2.0) ! ?j ! ?i = scalar_product (row ?A1.0 (?i div row_length ?B1.0)) (col ?A2.0 (?j div length ?B2.0)) * scalar_product (row ?B1.0 (?i mod row_length ?B1.0)) (col ?B2.0 (?j mod length ?B2.0))
matrix_compose_cond ?A1.0 ?A2.0 ?B1.0 ?B2.0 ?i ?j \<equiv> mat (row_length ?A1.0) (length ?A1.0) ?A1.0 \<and> mat (row_length ?A2.0) (length ?A2.0) ?A2.0 \<and> mat (row_length ?B1.0) (length ?B1.0) ?B1.0 \<and> mat (row_length ?B2.0) (length ?B2.0) ?B2.0 \<and> length ?A1.0 = row_length ?A2.0 \<and> length ?B1.0 = row_length ?B2.0 \<and> ?A1.0 \<noteq> [] \<and> ?A2.0 \<noteq> [] \<and> ?B1.0 \<noteq> [] \<and> ?B2.0 \<noteq> [] \<and> ?i < row_length ?A1.0 * row_length ?B1.0 \<and> ?j < length ?A2.0 * length ?B2.0

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


[STATEMENT]
lemma matrix_match_condn_1:
"matrix_match A1 A2 B1 B2
      \<and>((i<(row_length A1)*(row_length B1))
      \<and>(j<(length A2)*(length B2)))
       \<Longrightarrow>  ((matrix_mult A1  A2)\<otimes>(matrix_mult B1  B2))!j!i
  =  f
       (scalar_product
                 (row A1 (i div (row_length B1)))
                 (col A2  (j div (length B2))))
       (scalar_product
                 (row B1 (i mod (row_length B1)))
                 (col B2 (j mod (length B2))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_match A1 A2 B1 B2 \<and> i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<Longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = scalar_product (row A1 (i div row_length B1)) (col A2 (j div length B2)) * scalar_product (row B1 (i mod row_length B1)) (col B2 (j mod length B2))
[PROOF STEP]
using elements_matrix_distribution_1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mat (row_length ?A1.0) (length ?A1.0) ?A1.0; mat (row_length ?A2.0) (length ?A2.0) ?A2.0; mat (row_length ?B1.0) (length ?B1.0) ?B1.0; mat (row_length ?B2.0) (length ?B2.0) ?B2.0; length ?A1.0 = row_length ?A2.0; length ?B1.0 = row_length ?B2.0; ?A1.0 \<noteq> [] \<and> ?A2.0 \<noteq> [] \<and> ?B1.0 \<noteq> [] \<and> ?B2.0 \<noteq> []; ?i < row_length ?A1.0 * row_length ?B1.0; ?j < length ?A2.0 * length ?B2.0\<rbrakk> \<Longrightarrow> (?A1.0 \<circ> ?A2.0 \<otimes> ?B1.0 \<circ> ?B2.0) ! ?j ! ?i = scalar_product (row ?A1.0 (?i div row_length ?B1.0)) (col ?A2.0 (?j div length ?B2.0)) * scalar_product (row ?B1.0 (?i mod row_length ?B1.0)) (col ?B2.0 (?j mod length ?B2.0))

goal (1 subgoal):
 1. matrix_match A1 A2 B1 B2 \<and> i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<Longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = scalar_product (row A1 (i div row_length B1)) (col A2 (j div length B2)) * scalar_product (row B1 (i mod row_length B1)) (col B2 (j mod length B2))
[PROOF STEP]
unfolding matrix_match_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mat (row_length ?A1.0) (length ?A1.0) ?A1.0; mat (row_length ?A2.0) (length ?A2.0) ?A2.0; mat (row_length ?B1.0) (length ?B1.0) ?B1.0; mat (row_length ?B2.0) (length ?B2.0) ?B2.0; length ?A1.0 = row_length ?A2.0; length ?B1.0 = row_length ?B2.0; ?A1.0 \<noteq> [] \<and> ?A2.0 \<noteq> [] \<and> ?B1.0 \<noteq> [] \<and> ?B2.0 \<noteq> []; ?i < row_length ?A1.0 * row_length ?B1.0; ?j < length ?A2.0 * length ?B2.0\<rbrakk> \<Longrightarrow> (?A1.0 \<circ> ?A2.0 \<otimes> ?B1.0 \<circ> ?B2.0) ! ?j ! ?i = scalar_product (row ?A1.0 (?i div row_length ?B1.0)) (col ?A2.0 (?j div length ?B2.0)) * scalar_product (row ?B1.0 (?i mod row_length ?B1.0)) (col ?B2.0 (?j mod length ?B2.0))

goal (1 subgoal):
 1. (mat (row_length A1) (length A1) A1 \<and> mat (row_length A2) (length A2) A2 \<and> mat (row_length B1) (length B1) B1 \<and> mat (row_length B2) (length B2) B2 \<and> length A1 = row_length A2 \<and> length B1 = row_length B2 \<and> A1 \<noteq> [] \<and> A2 \<noteq> [] \<and> B1 \<noteq> [] \<and> B2 \<noteq> []) \<and> i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<Longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = scalar_product (row A1 (i div row_length B1)) (col A2 (j div length B2)) * scalar_product (row B1 (i mod row_length B1)) (col B2 (j mod length B2))
[PROOF STEP]
by auto


[STATEMENT]
lemma effective_matrix_match_condn_1:
 assumes "(matrix_match A1 A2 B1 B2) "
 shows "\<forall>i j.((i<(row_length A1)*(row_length B1))
             \<and>(j<(length A2)*(length B2))
              \<longrightarrow>   ((A1 \<circ>  A2)\<otimes>(B1 \<circ> B2))!j!i
                        =  f
                            (scalar_product
                                  (row A1 (i div (row_length B1)))
                                  (col A2  (j div (length B2))))
                            (scalar_product
                                  (row B1 (i mod (row_length B1)))
                                  (col B2 (j mod (length B2)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = scalar_product (row A1 (i div row_length B1)) (col A2 (j div length B2)) * scalar_product (row B1 (i mod row_length B1)) (col B2 (j mod length B2))
[PROOF STEP]
using assms matrix_match_condn_1
[PROOF STATE]
proof (prove)
using this:
matrix_match A1 A2 B1 B2
matrix_match ?A1.0 ?A2.0 ?B1.0 ?B2.0 \<and> ?i < row_length ?A1.0 * row_length ?B1.0 \<and> ?j < length ?A2.0 * length ?B2.0 \<Longrightarrow> (?A1.0 \<circ> ?A2.0 \<otimes> ?B1.0 \<circ> ?B2.0) ! ?j ! ?i = scalar_product (row ?A1.0 (?i div row_length ?B1.0)) (col ?A2.0 (?j div length ?B2.0)) * scalar_product (row ?B1.0 (?i mod row_length ?B1.0)) (col ?B2.0 (?j mod length ?B2.0))

goal (1 subgoal):
 1. \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = scalar_product (row A1 (i div row_length B1)) (col A2 (j div length B2)) * scalar_product (row B1 (i mod row_length B1)) (col B2 (j mod length B2))
[PROOF STEP]
unfolding matrix_match_def
[PROOF STATE]
proof (prove)
using this:
mat (row_length A1) (length A1) A1 \<and> mat (row_length A2) (length A2) A2 \<and> mat (row_length B1) (length B1) B1 \<and> mat (row_length B2) (length B2) B2 \<and> length A1 = row_length A2 \<and> length B1 = row_length B2 \<and> A1 \<noteq> [] \<and> A2 \<noteq> [] \<and> B1 \<noteq> [] \<and> B2 \<noteq> []
(mat (row_length ?A1.0) (length ?A1.0) ?A1.0 \<and> mat (row_length ?A2.0) (length ?A2.0) ?A2.0 \<and> mat (row_length ?B1.0) (length ?B1.0) ?B1.0 \<and> mat (row_length ?B2.0) (length ?B2.0) ?B2.0 \<and> length ?A1.0 = row_length ?A2.0 \<and> length ?B1.0 = row_length ?B2.0 \<and> ?A1.0 \<noteq> [] \<and> ?A2.0 \<noteq> [] \<and> ?B1.0 \<noteq> [] \<and> ?B2.0 \<noteq> []) \<and> ?i < row_length ?A1.0 * row_length ?B1.0 \<and> ?j < length ?A2.0 * length ?B2.0 \<Longrightarrow> (?A1.0 \<circ> ?A2.0 \<otimes> ?B1.0 \<circ> ?B2.0) ! ?j ! ?i = scalar_product (row ?A1.0 (?i div row_length ?B1.0)) (col ?A2.0 (?j div length ?B2.0)) * scalar_product (row ?B1.0 (?i mod row_length ?B1.0)) (col ?B2.0 (?j mod length ?B2.0))

goal (1 subgoal):
 1. \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = scalar_product (row A1 (i div row_length B1)) (col A2 (j div length B2)) * scalar_product (row B1 (i mod row_length B1)) (col B2 (j mod length B2))
[PROOF STEP]
by auto


[STATEMENT]
lemma matrix_match_condn_2:
"matrix_match A1 A2 B1 B2
 \<and>((i<(row_length A1)*(row_length B1))
 \<and>(j<(length A2)*(length B2)))
  \<Longrightarrow> ((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. matrix_match A1 A2 B1 B2 \<and> i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<Longrightarrow> ((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]
using elements_matrix_distribution2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mat (row_length ?A1.0) (length ?A1.0) ?A1.0; mat (row_length ?A2.0) (length ?A2.0) ?A2.0; mat (row_length ?B1.0) (length ?B1.0) ?B1.0; mat (row_length ?B2.0) (length ?B2.0) ?B2.0; length ?A1.0 = row_length ?A2.0; length ?B1.0 = row_length ?B2.0; ?A1.0 \<noteq> [] \<and> ?A2.0 \<noteq> [] \<and> ?B1.0 \<noteq> [] \<and> ?B2.0 \<noteq> []; ?i < row_length ?A1.0 * row_length ?B1.0; ?j < length ?A2.0 * length ?B2.0\<rbrakk> \<Longrightarrow> ((?A1.0 \<otimes> ?B1.0) \<circ> (?A2.0 \<otimes> ?B2.0)) ! ?j ! ?i = scalar_product (vec_vec_Tensor (row ?A1.0 (?i div row_length ?B1.0)) (row ?B1.0 (?i mod row_length ?B1.0))) (vec_vec_Tensor (col ?A2.0 (?j div length ?B2.0)) (col ?B2.0 (?j mod length ?B2.0)))

goal (1 subgoal):
 1. matrix_match A1 A2 B1 B2 \<and> i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<Longrightarrow> ((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]
unfolding matrix_match_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mat (row_length ?A1.0) (length ?A1.0) ?A1.0; mat (row_length ?A2.0) (length ?A2.0) ?A2.0; mat (row_length ?B1.0) (length ?B1.0) ?B1.0; mat (row_length ?B2.0) (length ?B2.0) ?B2.0; length ?A1.0 = row_length ?A2.0; length ?B1.0 = row_length ?B2.0; ?A1.0 \<noteq> [] \<and> ?A2.0 \<noteq> [] \<and> ?B1.0 \<noteq> [] \<and> ?B2.0 \<noteq> []; ?i < row_length ?A1.0 * row_length ?B1.0; ?j < length ?A2.0 * length ?B2.0\<rbrakk> \<Longrightarrow> ((?A1.0 \<otimes> ?B1.0) \<circ> (?A2.0 \<otimes> ?B2.0)) ! ?j ! ?i = scalar_product (vec_vec_Tensor (row ?A1.0 (?i div row_length ?B1.0)) (row ?B1.0 (?i mod row_length ?B1.0))) (vec_vec_Tensor (col ?A2.0 (?j div length ?B2.0)) (col ?B2.0 (?j mod length ?B2.0)))

goal (1 subgoal):
 1. (mat (row_length A1) (length A1) A1 \<and> mat (row_length A2) (length A2) A2 \<and> mat (row_length B1) (length B1) B1 \<and> mat (row_length B2) (length B2) B2 \<and> length A1 = row_length A2 \<and> length B1 = row_length B2 \<and> A1 \<noteq> [] \<and> A2 \<noteq> [] \<and> B1 \<noteq> [] \<and> B2 \<noteq> []) \<and> i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<Longrightarrow> ((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


[STATEMENT]
lemma effective_matrix_match_condn_2:
 assumes "(matrix_match A1 A2 B1 B2) "
 shows "\<forall>i j.((i<(row_length A1)*(row_length B1))
         \<and>(j<(length A2)*(length B2))
            \<longrightarrow> ((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. \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> ((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]
using assms matrix_match_condn_2
[PROOF STATE]
proof (prove)
using this:
matrix_match A1 A2 B1 B2
matrix_match ?A1.0 ?A2.0 ?B1.0 ?B2.0 \<and> ?i < row_length ?A1.0 * row_length ?B1.0 \<and> ?j < length ?A2.0 * length ?B2.0 \<Longrightarrow> ((?A1.0 \<otimes> ?B1.0) \<circ> (?A2.0 \<otimes> ?B2.0)) ! ?j ! ?i = scalar_product (vec_vec_Tensor (row ?A1.0 (?i div row_length ?B1.0)) (row ?B1.0 (?i mod row_length ?B1.0))) (vec_vec_Tensor (col ?A2.0 (?j div length ?B2.0)) (col ?B2.0 (?j mod length ?B2.0)))

goal (1 subgoal):
 1. \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> ((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]
unfolding matrix_match_def
[PROOF STATE]
proof (prove)
using this:
mat (row_length A1) (length A1) A1 \<and> mat (row_length A2) (length A2) A2 \<and> mat (row_length B1) (length B1) B1 \<and> mat (row_length B2) (length B2) B2 \<and> length A1 = row_length A2 \<and> length B1 = row_length B2 \<and> A1 \<noteq> [] \<and> A2 \<noteq> [] \<and> B1 \<noteq> [] \<and> B2 \<noteq> []
(mat (row_length ?A1.0) (length ?A1.0) ?A1.0 \<and> mat (row_length ?A2.0) (length ?A2.0) ?A2.0 \<and> mat (row_length ?B1.0) (length ?B1.0) ?B1.0 \<and> mat (row_length ?B2.0) (length ?B2.0) ?B2.0 \<and> length ?A1.0 = row_length ?A2.0 \<and> length ?B1.0 = row_length ?B2.0 \<and> ?A1.0 \<noteq> [] \<and> ?A2.0 \<noteq> [] \<and> ?B1.0 \<noteq> [] \<and> ?B2.0 \<noteq> []) \<and> ?i < row_length ?A1.0 * row_length ?B1.0 \<and> ?j < length ?A2.0 * length ?B2.0 \<Longrightarrow> ((?A1.0 \<otimes> ?B1.0) \<circ> (?A2.0 \<otimes> ?B2.0)) ! ?j ! ?i = scalar_product (vec_vec_Tensor (row ?A1.0 (?i div row_length ?B1.0)) (row ?B1.0 (?i mod row_length ?B1.0))) (vec_vec_Tensor (col ?A2.0 (?j div length ?B2.0)) (col ?B2.0 (?j mod length ?B2.0)))

goal (1 subgoal):
 1. \<forall>i j. i < row_length A1 * row_length B1 \<and> j < length A2 * length B2 \<longrightarrow> ((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


[STATEMENT]
lemma zip_Nil:"zip [] [] = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zip [] [] = []
[PROOF STEP]
using zip_def
[PROOF STATE]
proof (prove)
using this:
zip \<equiv> \<lambda>uu uua. rec_list (\<lambda>xs. []) (\<lambda>y ys ysa xs. case xs of [] \<Rightarrow> [] | z # zs \<Rightarrow> (z, y) # ysa zs) uua uu

goal (1 subgoal):
 1. zip [] [] = []
[PROOF STEP]
by auto


[STATEMENT]
lemma zer_left_mult:"f zer x = zer"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zer * x = zer
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. zer * x = zer
[PROOF STEP]
have "g zer zer = zer"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zer + zer = zer
[PROOF STEP]
using plus_left_id
[PROOF STATE]
proof (prove)
using this:
zer + ?x = ?x

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

goal (1 subgoal):
 1. zer * x = zer
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zer + zer = zer
[PROOF STEP]
have "f zer x = f (g zer zer) x"
[PROOF STATE]
proof (prove)
using this:
zer + zer = zer

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

goal (1 subgoal):
 1. zer * x = zer
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zer * x = zer + zer * x
[PROOF STEP]
have "f zer x = (f zer x) + (f zer x)"
[PROOF STATE]
proof (prove)
using this:
zer * x = zer + zer * x

goal (1 subgoal):
 1. zer * x = zer * x + (zer * x)
[PROOF STEP]
using  plus_right_distributivity
[PROOF STATE]
proof (prove)
using this:
zer * x = zer + zer * x
?a + ?b * ?c = ?a * ?c + (?b * ?c)

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

goal (1 subgoal):
 1. zer * x = zer
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zer * x = zer * x + (zer * x)
[PROOF STEP]
have "(f zer x) + (inver (f zer x)) = (f zer x) + (f zer x) + (inver (f zer x))"
[PROOF STATE]
proof (prove)
using this:
zer * x = zer * x + (zer * x)

goal (1 subgoal):
 1. zer * x + inver (zer * x) = zer * x + (zer * x) + inver (zer * x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
zer * x + inver (zer * x) = zer * x + (zer * x) + inver (zer * x)

goal (1 subgoal):
 1. zer * x = zer
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zer * x + inver (zer * x) = zer * x + (zer * x) + inver (zer * x)
[PROOF STEP]
have "zer = (f zer x) + zer"
[PROOF STATE]
proof (prove)
using this:
zer * x + inver (zer * x) = zer * x + (zer * x) + inver (zer * x)

goal (1 subgoal):
 1. zer = zer * x + zer
[PROOF STEP]
using plus_left_inverse  plus_assoc
[PROOF STATE]
proof (prove)
using this:
zer * x + inver (zer * x) = zer * x + (zer * x) + inver (zer * x)
?x + inver ?x = zer
?a + ?b + ?c = ?a + (?b + ?c)

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

goal (1 subgoal):
 1. zer * x = zer
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zer = zer * x + zer
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
zer = zer * x + zer

goal (1 subgoal):
 1. zer * x = zer
[PROOF STEP]
using plus_right_id
[PROOF STATE]
proof (prove)
using this:
zer = zer * x + zer
?x + zer = ?x

goal (1 subgoal):
 1. zer * x = zer
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
zer * x = zer

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma zip_Cons:"(length v = length w) \<Longrightarrow> zip (a#v) (b#w) = (a,b)#(zip v w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length v = length w \<Longrightarrow> zip (a # v) (b # w) = (a, b) # zip v w
[PROOF STEP]
unfolding zip_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length v = length w \<Longrightarrow> rec_list (\<lambda>xs. []) (\<lambda>y ys ysa. case_list [] (\<lambda>z zs. (z, y) # ysa zs)) (b # w) (a # v) = (a, b) # rec_list (\<lambda>xs. []) (\<lambda>y ys ysa. case_list [] (\<lambda>z zs. (z, y) # ysa zs)) w v
[PROOF STEP]
by auto