[STATEMENT]
lemma tensor_mat_mult:
  assumes "m1 \<in> carrier_mat d1 d1"
    and "m2 \<in> carrier_mat d1 d1"
    and "m3 \<in> carrier_mat d2 d2"
    and "m4 \<in> carrier_mat d2 d2"
  shows "tensor_mat (m1 * m2) (m3 * m4) = tensor_mat m1 m3 * tensor_mat m2 m4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat (m1 * m2) (m3 * m4) = tensor_mat m1 m3 * tensor_mat m2 m4
[PROOF STEP]
proof (rule eq_matI, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = row (tensor_mat m1 m3) i \<bullet> col (tensor_mat m2 m4) j
[PROOF STEP]
fix i j :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = row (tensor_mat m1 m3) i \<bullet> col (tensor_mat m2 m4) j
[PROOF STEP]
assume i: "i < d" and j: "j < d"
[PROOF STATE]
proof (state)
this:
i < d
j < d

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = row (tensor_mat m1 m3) i \<bullet> col (tensor_mat m2 m4) j
[PROOF STEP]
let ?i1 = "encode1 i" and ?i2 = "encode2 i" and ?j1 = "encode1 j" and ?j2 = "encode2 j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = row (tensor_mat m1 m3) i \<bullet> col (tensor_mat m2 m4) j
[PROOF STEP]
have "tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = (m1 * m2) $$ (?i1, ?j1) * (m3 * m4) $$ (?i2, ?j2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = (m1 * m2) $$ (encode1 i, encode1 j) * (m3 * m4) $$ (encode2 i, encode2 j)
[PROOF STEP]
using i j
[PROOF STATE]
proof (prove)
using this:
i < d
j < d

goal (1 subgoal):
 1. tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = (m1 * m2) $$ (encode1 i, encode1 j) * (m3 * m4) $$ (encode2 i, encode2 j)
[PROOF STEP]
by (simp add: tensor_mat_eval)
[PROOF STATE]
proof (state)
this:
tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = (m1 * m2) $$ (encode1 i, encode1 j) * (m3 * m4) $$ (encode2 i, encode2 j)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = row (tensor_mat m1 m3) i \<bullet> col (tensor_mat m2 m4) j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = (m1 * m2) $$ (encode1 i, encode1 j) * (m3 * m4) $$ (encode2 i, encode2 j)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = row (tensor_mat m1 m3) i \<bullet> col (tensor_mat m2 m4) j
[PROOF STEP]
have "\<dots> = (row m1 ?i1 \<bullet> col m2 ?j1) * (row m3 ?i2 \<bullet> col m4 ?j2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (m1 * m2) $$ (encode1 i, encode1 j) * (m3 * m4) $$ (encode2 i, encode2 j) = row m1 (encode1 i) \<bullet> col m2 (encode1 j) * (row m3 (encode2 i) \<bullet> col m4 (encode2 j))
[PROOF STEP]
using assms i j
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d1 d1
m3 \<in> carrier_mat d2 d2
m4 \<in> carrier_mat d2 d2
i < d
j < d

goal (1 subgoal):
 1. (m1 * m2) $$ (encode1 i, encode1 j) * (m3 * m4) $$ (encode2 i, encode2 j) = row m1 (encode1 i) \<bullet> col m2 (encode1 j) * (row m3 (encode2 i) \<bullet> col m4 (encode2 j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(m1 * m2) $$ (encode1 i, encode1 j) * (m3 * m4) $$ (encode2 i, encode2 j) = row m1 (encode1 i) \<bullet> col m2 (encode1 j) * (row m3 (encode2 i) \<bullet> col m4 (encode2 j))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = row (tensor_mat m1 m3) i \<bullet> col (tensor_mat m2 m4) j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(m1 * m2) $$ (encode1 i, encode1 j) * (m3 * m4) $$ (encode2 i, encode2 j) = row m1 (encode1 i) \<bullet> col m2 (encode1 j) * (row m3 (encode2 i) \<bullet> col m4 (encode2 j))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = row (tensor_mat m1 m3) i \<bullet> col (tensor_mat m2 m4) j
[PROOF STEP]
have "\<dots> = (\<Sum>i = 0..<d1. m1 $$ (?i1, i) * m2 $$ (i, ?j1)) * (\<Sum>j = 0..<d2. m3 $$ (?i2, j) * m4 $$ (j, ?j2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row m1 (encode1 i) \<bullet> col m2 (encode1 j) * (row m3 (encode2 i) \<bullet> col m4 (encode2 j)) = (\<Sum>ia = 0..<d1. m1 $$ (encode1 i, ia) * m2 $$ (ia, encode1 j)) * (\<Sum>ja = 0..<d2. m3 $$ (encode2 i, ja) * m4 $$ (ja, encode2 j))
[PROOF STEP]
using assms i j
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d1 d1
m3 \<in> carrier_mat d2 d2
m4 \<in> carrier_mat d2 d2
i < d
j < d

goal (1 subgoal):
 1. row m1 (encode1 i) \<bullet> col m2 (encode1 j) * (row m3 (encode2 i) \<bullet> col m4 (encode2 j)) = (\<Sum>ia = 0..<d1. m1 $$ (encode1 i, ia) * m2 $$ (ia, encode1 j)) * (\<Sum>ja = 0..<d2. m3 $$ (encode2 i, ja) * m4 $$ (ja, encode2 j))
[PROOF STEP]
by (simp add: scalar_prod_def)
[PROOF STATE]
proof (state)
this:
row m1 (encode1 i) \<bullet> col m2 (encode1 j) * (row m3 (encode2 i) \<bullet> col m4 (encode2 j)) = (\<Sum>ia = 0..<d1. m1 $$ (encode1 i, ia) * m2 $$ (ia, encode1 j)) * (\<Sum>ja = 0..<d2. m3 $$ (encode2 i, ja) * m4 $$ (ja, encode2 j))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = row (tensor_mat m1 m3) i \<bullet> col (tensor_mat m2 m4) j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
row m1 (encode1 i) \<bullet> col m2 (encode1 j) * (row m3 (encode2 i) \<bullet> col m4 (encode2 j)) = (\<Sum>ia = 0..<d1. m1 $$ (encode1 i, ia) * m2 $$ (ia, encode1 j)) * (\<Sum>ja = 0..<d2. m3 $$ (encode2 i, ja) * m4 $$ (ja, encode2 j))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = row (tensor_mat m1 m3) i \<bullet> col (tensor_mat m2 m4) j
[PROOF STEP]
have "\<dots> = (\<Sum>i = 0..<d1. \<Sum>j = 0..<d2. (m1 $$ (?i1, i) * m2 $$ (i, ?j1)) * (m3 $$ (?i2, j) * m4 $$ (j, ?j2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia = 0..<d1. m1 $$ (encode1 i, ia) * m2 $$ (ia, encode1 j)) * (\<Sum>ja = 0..<d2. m3 $$ (encode2 i, ja) * m4 $$ (ja, encode2 j)) = (\<Sum>ia = 0..<d1. \<Sum>ja = 0..<d2. m1 $$ (encode1 i, ia) * m2 $$ (ia, encode1 j) * (m3 $$ (encode2 i, ja) * m4 $$ (ja, encode2 j)))
[PROOF STEP]
by (rule Groups_Big.sum_product)
[PROOF STATE]
proof (state)
this:
(\<Sum>ia = 0..<d1. m1 $$ (encode1 i, ia) * m2 $$ (ia, encode1 j)) * (\<Sum>ja = 0..<d2. m3 $$ (encode2 i, ja) * m4 $$ (ja, encode2 j)) = (\<Sum>ia = 0..<d1. \<Sum>ja = 0..<d2. m1 $$ (encode1 i, ia) * m2 $$ (ia, encode1 j) * (m3 $$ (encode2 i, ja) * m4 $$ (ja, encode2 j)))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = row (tensor_mat m1 m3) i \<bullet> col (tensor_mat m2 m4) j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>ia = 0..<d1. m1 $$ (encode1 i, ia) * m2 $$ (ia, encode1 j)) * (\<Sum>ja = 0..<d2. m3 $$ (encode2 i, ja) * m4 $$ (ja, encode2 j)) = (\<Sum>ia = 0..<d1. \<Sum>ja = 0..<d2. m1 $$ (encode1 i, ia) * m2 $$ (ia, encode1 j) * (m3 $$ (encode2 i, ja) * m4 $$ (ja, encode2 j)))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = row (tensor_mat m1 m3) i \<bullet> col (tensor_mat m2 m4) j
[PROOF STEP]
have "\<dots> = (\<Sum>i = 0..<d. (m1 $$ (?i1, encode1 i) * m2 $$ (encode1 i, ?j1)) * (m3 $$ (?i2, encode2 i) * m4 $$ (encode2 i, ?j2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia = 0..<d1. \<Sum>ja = 0..<d2. m1 $$ (encode1 i, ia) * m2 $$ (ia, encode1 j) * (m3 $$ (encode2 i, ja) * m4 $$ (ja, encode2 j))) = (\<Sum>ia = 0..<d. m1 $$ (encode1 i, encode1 ia) * m2 $$ (encode1 ia, encode1 j) * (m3 $$ (encode2 i, encode2 ia) * m4 $$ (encode2 ia, encode2 j)))
[PROOF STEP]
by (rule sum_encode)
[PROOF STATE]
proof (state)
this:
(\<Sum>ia = 0..<d1. \<Sum>ja = 0..<d2. m1 $$ (encode1 i, ia) * m2 $$ (ia, encode1 j) * (m3 $$ (encode2 i, ja) * m4 $$ (ja, encode2 j))) = (\<Sum>ia = 0..<d. m1 $$ (encode1 i, encode1 ia) * m2 $$ (encode1 ia, encode1 j) * (m3 $$ (encode2 i, encode2 ia) * m4 $$ (encode2 ia, encode2 j)))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = row (tensor_mat m1 m3) i \<bullet> col (tensor_mat m2 m4) j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>ia = 0..<d1. \<Sum>ja = 0..<d2. m1 $$ (encode1 i, ia) * m2 $$ (ia, encode1 j) * (m3 $$ (encode2 i, ja) * m4 $$ (ja, encode2 j))) = (\<Sum>ia = 0..<d. m1 $$ (encode1 i, encode1 ia) * m2 $$ (encode1 ia, encode1 j) * (m3 $$ (encode2 i, encode2 ia) * m4 $$ (encode2 ia, encode2 j)))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = row (tensor_mat m1 m3) i \<bullet> col (tensor_mat m2 m4) j
[PROOF STEP]
have "\<dots> = row (tensor_mat m1 m3) i \<bullet> col (tensor_mat m2 m4) j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia = 0..<d. m1 $$ (encode1 i, encode1 ia) * m2 $$ (encode1 ia, encode1 j) * (m3 $$ (encode2 i, encode2 ia) * m4 $$ (encode2 ia, encode2 j))) = row (tensor_mat m1 m3) i \<bullet> col (tensor_mat m2 m4) j
[PROOF STEP]
apply (simp add: scalar_prod_def tensor_mat_eval i j)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia = 0..<d. m1 $$ (encode1 i, encode1 ia) * m2 $$ (encode1 ia, encode1 j) * (m3 $$ (encode2 i, encode2 ia) * m4 $$ (encode2 ia, encode2 j))) = (\<Sum>ia = 0..<d. m1 $$ (encode1 i, encode1 ia) * m3 $$ (encode2 i, encode2 ia) * (m2 $$ (encode1 ia, encode1 j) * m4 $$ (encode2 ia, encode2 j)))
[PROOF STEP]
by (rule sum.cong, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>ia = 0..<d. m1 $$ (encode1 i, encode1 ia) * m2 $$ (encode1 ia, encode1 j) * (m3 $$ (encode2 i, encode2 ia) * m4 $$ (encode2 ia, encode2 j))) = row (tensor_mat m1 m3) i \<bullet> col (tensor_mat m2 m4) j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = row (tensor_mat m1 m3) i \<bullet> col (tensor_mat m2 m4) j
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = row (tensor_mat m1 m3) i \<bullet> col (tensor_mat m2 m4) j
[PROOF STEP]
show "tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = row (tensor_mat m1 m3) i \<bullet> col (tensor_mat m2 m4) j"
[PROOF STATE]
proof (prove)
using this:
tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = row (tensor_mat m1 m3) i \<bullet> col (tensor_mat m2 m4) j

goal (1 subgoal):
 1. tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = row (tensor_mat m1 m3) i \<bullet> col (tensor_mat m2 m4) j
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = row (tensor_mat m1 m3) i \<bullet> col (tensor_mat m2 m4) j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tensor_mat_adjoint:
  assumes "m1 \<in> carrier_mat d1 d1"
    and "m2 \<in> carrier_mat d2 d2"
  shows "adjoint (tensor_mat m1 m2) = tensor_mat (adjoint m1) (adjoint m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint (tensor_mat m1 m2) = tensor_mat (adjoint m1) (adjoint m2)
[PROOF STEP]
apply (rule eq_matI, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> adjoint (tensor_mat m1 m2) $$ (i, j) = tensor_mat (adjoint m1) (adjoint m2) $$ (i, j)
[PROOF STEP]
unfolding tensor_mat_def adjoint_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> mat (dim_col (mat d d (\<lambda>(i, j). m1 $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j)))) (dim_row (mat d d (\<lambda>(i, j). m1 $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j)))) (\<lambda>(i, j). conjugate (mat d d (\<lambda>(i, j). m1 $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j)) $$ (j, i))) $$ (i, j) = mat d d (\<lambda>(i, j). mat (dim_col m1) (dim_row m1) (\<lambda>(i, j). conjugate (m1 $$ (j, i))) $$ (encode1 i, encode1 j) * mat (dim_col m2) (dim_row m2) (\<lambda>(i, j). conjugate (m2 $$ (j, i))) $$ (encode2 i, encode2 j)) $$ (i, j)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> mat (dim_col (mat d d (\<lambda>(i, j). m1 $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j)))) (dim_row (mat d d (\<lambda>(i, j). m1 $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j)))) (\<lambda>(i, j). conjugate (mat d d (\<lambda>(i, j). m1 $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j)) $$ (j, i))) $$ (i, j) = mat d d (\<lambda>(i, j). mat (dim_col m1) (dim_row m1) (\<lambda>(i, j). conjugate (m1 $$ (j, i))) $$ (encode1 i, encode1 j) * mat (dim_col m2) (dim_row m2) (\<lambda>(i, j). conjugate (m2 $$ (j, i))) $$ (encode2 i, encode2 j)) $$ (i, j)
[PROOF STEP]
by (simp add: conjugate_dist_mul)


[STATEMENT]
lemma tensor_mat_hermitian:
  assumes "m1 \<in> carrier_mat d1 d1"
    and "m2 \<in> carrier_mat d2 d2"
    and "hermitian m1"
    and "hermitian m2"
  shows "hermitian (tensor_mat m1 m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hermitian (tensor_mat m1 m2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
hermitian m1
hermitian m2

goal (1 subgoal):
 1. hermitian (tensor_mat m1 m2)
[PROOF STEP]
by (metis hermitian_def tensor_mat_adjoint)


[STATEMENT]
lemma tensor_mat_unitary:
  assumes "m1 \<in> carrier_mat d1 d1"
    and "m2 \<in> carrier_mat d2 d2"
    and "unitary m1"
    and "unitary m2"
  shows "unitary (tensor_mat m1 m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unitary (tensor_mat m1 m2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
unitary m1
unitary m2

goal (1 subgoal):
 1. unitary (tensor_mat m1 m2)
[PROOF STEP]
apply (auto simp add: unitary_def tensor_mat_adjoint)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m1 \<in> carrier_mat d1 d1; m2 \<in> carrier_mat d2 d2; inverts_mat m1 (adjoint m1); inverts_mat m2 (adjoint m2)\<rbrakk> \<Longrightarrow> inverts_mat (tensor_mat m1 m2) (tensor_mat (adjoint m1) (adjoint m2))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
unitary m1
unitary m2

goal (1 subgoal):
 1. \<lbrakk>m1 \<in> carrier_mat d1 d1; m2 \<in> carrier_mat d2 d2; inverts_mat m1 (adjoint m1); inverts_mat m2 (adjoint m2)\<rbrakk> \<Longrightarrow> inverts_mat (tensor_mat m1 m2) (tensor_mat (adjoint m1) (adjoint m2))
[PROOF STEP]
unfolding inverts_mat_def
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
unitary m1
unitary m2

goal (1 subgoal):
 1. \<lbrakk>m1 \<in> carrier_mat d1 d1; m2 \<in> carrier_mat d2 d2; m1 * adjoint m1 = 1\<^sub>m (dim_row m1); m2 * adjoint m2 = 1\<^sub>m (dim_row m2)\<rbrakk> \<Longrightarrow> tensor_mat m1 m2 * tensor_mat (adjoint m1) (adjoint m2) = 1\<^sub>m (dim_row (tensor_mat m1 m2))
[PROOF STEP]
apply (subst tensor_mat_mult[symmetric], auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m1 \<in> carrier_mat d1 d1; m2 \<in> carrier_mat d2 d2; unitary m1; unitary m2\<rbrakk> \<Longrightarrow> tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) = 1\<^sub>m d
[PROOF STEP]
by (rule tensor_mat_id)


[STATEMENT]
lemma tensor_mat_positive:
  assumes "m1 \<in> carrier_mat d1 d1"
    and "m2 \<in> carrier_mat d2 d2"
    and "positive m1"
    and "positive m2"
  shows "positive (tensor_mat m1 m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive (tensor_mat m1 m2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. positive (tensor_mat m1 m2)
[PROOF STEP]
obtain M1 where M1: "m1 = M1 * adjoint M1" and dM1:"M1 \<in> carrier_mat d1 d1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>M1. \<lbrakk>m1 = M1 * adjoint M1; M1 \<in> carrier_mat d1 d1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using positive_only_if_decomp assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<in> carrier_mat ?n ?n; positive ?A\<rbrakk> \<Longrightarrow> \<exists>M\<in>carrier_mat ?n ?n. M * adjoint M = ?A
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2

goal (1 subgoal):
 1. (\<And>M1. \<lbrakk>m1 = M1 * adjoint M1; M1 \<in> carrier_mat d1 d1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m1 = M1 * adjoint M1
M1 \<in> carrier_mat d1 d1

goal (1 subgoal):
 1. positive (tensor_mat m1 m2)
[PROOF STEP]
obtain M2 where M2: "m2 = M2 * adjoint M2" and dM2:"M2 \<in> carrier_mat d2 d2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>M2. \<lbrakk>m2 = M2 * adjoint M2; M2 \<in> carrier_mat d2 d2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using positive_only_if_decomp assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<in> carrier_mat ?n ?n; positive ?A\<rbrakk> \<Longrightarrow> \<exists>M\<in>carrier_mat ?n ?n. M * adjoint M = ?A
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2

goal (1 subgoal):
 1. (\<And>M2. \<lbrakk>m2 = M2 * adjoint M2; M2 \<in> carrier_mat d2 d2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m2 = M2 * adjoint M2
M2 \<in> carrier_mat d2 d2

goal (1 subgoal):
 1. positive (tensor_mat m1 m2)
[PROOF STEP]
have "(adjoint (tensor_mat M1 M2)) = tensor_mat (adjoint M1) (adjoint M2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint (tensor_mat M1 M2) = tensor_mat (adjoint M1) (adjoint M2)
[PROOF STEP]
using tensor_mat_adjoint dM1 dM2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?m1.0 \<in> carrier_mat d1 d1; ?m2.0 \<in> carrier_mat d2 d2\<rbrakk> \<Longrightarrow> adjoint (tensor_mat ?m1.0 ?m2.0) = tensor_mat (adjoint ?m1.0) (adjoint ?m2.0)
M1 \<in> carrier_mat d1 d1
M2 \<in> carrier_mat d2 d2

goal (1 subgoal):
 1. adjoint (tensor_mat M1 M2) = tensor_mat (adjoint M1) (adjoint M2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
adjoint (tensor_mat M1 M2) = tensor_mat (adjoint M1) (adjoint M2)

goal (1 subgoal):
 1. positive (tensor_mat m1 m2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
adjoint (tensor_mat M1 M2) = tensor_mat (adjoint M1) (adjoint M2)
[PROOF STEP]
have "tensor_mat M1 M2 * (adjoint (tensor_mat M1 M2)) = tensor_mat (M1 * adjoint M1) (M2 * adjoint M2)"
[PROOF STATE]
proof (prove)
using this:
adjoint (tensor_mat M1 M2) = tensor_mat (adjoint M1) (adjoint M2)

goal (1 subgoal):
 1. tensor_mat M1 M2 * adjoint (tensor_mat M1 M2) = tensor_mat (M1 * adjoint M1) (M2 * adjoint M2)
[PROOF STEP]
using dM1 dM2 adjoint_dim[OF dM1] adjoint_dim[OF dM2]
[PROOF STATE]
proof (prove)
using this:
adjoint (tensor_mat M1 M2) = tensor_mat (adjoint M1) (adjoint M2)
M1 \<in> carrier_mat d1 d1
M2 \<in> carrier_mat d2 d2
adjoint M1 \<in> carrier_mat d1 d1
adjoint M2 \<in> carrier_mat d2 d2

goal (1 subgoal):
 1. tensor_mat M1 M2 * adjoint (tensor_mat M1 M2) = tensor_mat (M1 * adjoint M1) (M2 * adjoint M2)
[PROOF STEP]
by (auto simp add: tensor_mat_mult)
[PROOF STATE]
proof (state)
this:
tensor_mat M1 M2 * adjoint (tensor_mat M1 M2) = tensor_mat (M1 * adjoint M1) (M2 * adjoint M2)

goal (1 subgoal):
 1. positive (tensor_mat m1 m2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
tensor_mat M1 M2 * adjoint (tensor_mat M1 M2) = tensor_mat (M1 * adjoint M1) (M2 * adjoint M2)

goal (1 subgoal):
 1. positive (tensor_mat m1 m2)
[PROOF STEP]
have "\<dots> = tensor_mat m1 m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat (M1 * adjoint M1) (M2 * adjoint M2) = tensor_mat m1 m2
[PROOF STEP]
using M1 M2
[PROOF STATE]
proof (prove)
using this:
m1 = M1 * adjoint M1
m2 = M2 * adjoint M2

goal (1 subgoal):
 1. tensor_mat (M1 * adjoint M1) (M2 * adjoint M2) = tensor_mat m1 m2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tensor_mat (M1 * adjoint M1) (M2 * adjoint M2) = tensor_mat m1 m2

goal (1 subgoal):
 1. positive (tensor_mat m1 m2)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
tensor_mat M1 M2 * adjoint (tensor_mat M1 M2) = tensor_mat m1 m2
[PROOF STEP]
have "tensor_mat m1 m2 = tensor_mat M1 M2 * (adjoint (tensor_mat M1 M2))"
[PROOF STATE]
proof (prove)
using this:
tensor_mat M1 M2 * adjoint (tensor_mat M1 M2) = tensor_mat m1 m2

goal (1 subgoal):
 1. tensor_mat m1 m2 = tensor_mat M1 M2 * adjoint (tensor_mat M1 M2)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
tensor_mat m1 m2 = tensor_mat M1 M2 * adjoint (tensor_mat M1 M2)

goal (1 subgoal):
 1. positive (tensor_mat m1 m2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tensor_mat m1 m2 = tensor_mat M1 M2 * adjoint (tensor_mat M1 M2)
[PROOF STEP]
have "\<exists>M. M * adjoint M = tensor_mat m1 m2"
[PROOF STATE]
proof (prove)
using this:
tensor_mat m1 m2 = tensor_mat M1 M2 * adjoint (tensor_mat M1 M2)

goal (1 subgoal):
 1. \<exists>M. M * adjoint M = tensor_mat m1 m2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>M. M * adjoint M = tensor_mat m1 m2

goal (1 subgoal):
 1. positive (tensor_mat m1 m2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>M. M * adjoint M = tensor_mat m1 m2

goal (1 subgoal):
 1. positive (tensor_mat m1 m2)
[PROOF STEP]
have "tensor_mat m1 m2 \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat m1 m2 \<in> carrier_mat d d
[PROOF STEP]
using tensor_mat_carrier
[PROOF STATE]
proof (prove)
using this:
tensor_mat ?m1.0 ?m2.0 \<in> carrier_mat d d

goal (1 subgoal):
 1. tensor_mat m1 m2 \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tensor_mat m1 m2 \<in> carrier_mat d d

goal (1 subgoal):
 1. positive (tensor_mat m1 m2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>M. M * adjoint M = tensor_mat m1 m2
tensor_mat m1 m2 \<in> carrier_mat d d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>M. M * adjoint M = tensor_mat m1 m2
tensor_mat m1 m2 \<in> carrier_mat d d

goal (1 subgoal):
 1. positive (tensor_mat m1 m2)
[PROOF STEP]
using positive_if_decomp[of "tensor_mat m1 m2"]
[PROOF STATE]
proof (prove)
using this:
\<exists>M. M * adjoint M = tensor_mat m1 m2
tensor_mat m1 m2 \<in> carrier_mat d d
\<lbrakk>tensor_mat m1 m2 \<in> carrier_mat ?n ?n; \<exists>M. M * adjoint M = tensor_mat m1 m2\<rbrakk> \<Longrightarrow> positive (tensor_mat m1 m2)

goal (1 subgoal):
 1. positive (tensor_mat m1 m2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (tensor_mat m1 m2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tensor_mat_positive_le:
  assumes "m1 \<in> carrier_mat d1 d1"
    and "m2 \<in> carrier_mat d2 d2"
    and "positive m1"
    and "positive m2"
    and "m1 \<le>\<^sub>L A"
    and "m2 \<le>\<^sub>L B"
  shows "tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
have dA: "A \<in> carrier_mat d1 d1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> carrier_mat d1 d1
[PROOF STEP]
using assms lowner_le_def
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L A
m2 \<le>\<^sub>L B
(?A \<le>\<^sub>L ?B) = (dim_row ?A = dim_row ?B \<and> dim_col ?A = dim_col ?B \<and> positive (?B - ?A))

goal (1 subgoal):
 1. A \<in> carrier_mat d1 d1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<in> carrier_mat d1 d1

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
have pA: "positive A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive A
[PROOF STEP]
using assms dA lowner_le_trans_positiveI[of m1]
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L A
m2 \<le>\<^sub>L B
A \<in> carrier_mat d1 d1
\<lbrakk>m1 \<in> carrier_mat ?n ?n; positive m1; m1 \<le>\<^sub>L ?B\<rbrakk> \<Longrightarrow> positive ?B

goal (1 subgoal):
 1. positive A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive A

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
have dB: "B \<in> carrier_mat d2 d2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<in> carrier_mat d2 d2
[PROOF STEP]
using assms lowner_le_def
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L A
m2 \<le>\<^sub>L B
(?A \<le>\<^sub>L ?B) = (dim_row ?A = dim_row ?B \<and> dim_col ?A = dim_col ?B \<and> positive (?B - ?A))

goal (1 subgoal):
 1. B \<in> carrier_mat d2 d2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B \<in> carrier_mat d2 d2

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
have pB: "positive B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive B
[PROOF STEP]
using assms dB lowner_le_trans_positiveI[of m2]
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L A
m2 \<le>\<^sub>L B
B \<in> carrier_mat d2 d2
\<lbrakk>m2 \<in> carrier_mat ?n ?n; positive m2; m2 \<le>\<^sub>L ?B\<rbrakk> \<Longrightarrow> positive ?B

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

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
have "A - m1 = A + (- m1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A - m1 = A + - m1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L A
m2 \<le>\<^sub>L B

goal (1 subgoal):
 1. A - m1 = A + - m1
[PROOF STEP]
by (auto simp add: minus_add_uminus_mat)
[PROOF STATE]
proof (state)
this:
A - m1 = A + - m1

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A - m1 = A + - m1
[PROOF STEP]
have "positive (A + (- m1))"
[PROOF STATE]
proof (prove)
using this:
A - m1 = A + - m1

goal (1 subgoal):
 1. positive (A + - m1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A - m1 = A + - m1
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L A
m2 \<le>\<^sub>L B

goal (1 subgoal):
 1. positive (A + - m1)
[PROOF STEP]
unfolding lowner_le_def
[PROOF STATE]
proof (prove)
using this:
A - m1 = A + - m1
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
dim_row m1 = dim_row A \<and> dim_col m1 = dim_col A \<and> positive (A - m1)
dim_row m2 = dim_row B \<and> dim_col m2 = dim_col B \<and> positive (B - m2)

goal (1 subgoal):
 1. positive (A + - m1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (A + - m1)

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
positive (A + - m1)
[PROOF STEP]
have p1: "positive (tensor_mat (A + (- m1)) m2)"
[PROOF STATE]
proof (prove)
using this:
positive (A + - m1)

goal (1 subgoal):
 1. positive (tensor_mat (A + - m1) m2)
[PROOF STEP]
using assms tensor_mat_positive
[PROOF STATE]
proof (prove)
using this:
positive (A + - m1)
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L A
m2 \<le>\<^sub>L B
\<lbrakk>?m1.0 \<in> carrier_mat d1 d1; ?m2.0 \<in> carrier_mat d2 d2; positive ?m1.0; positive ?m2.0\<rbrakk> \<Longrightarrow> positive (tensor_mat ?m1.0 ?m2.0)

goal (1 subgoal):
 1. positive (tensor_mat (A + - m1) m2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (tensor_mat (A + - m1) m2)

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
positive (tensor_mat (A + - m1) m2)

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
have "tensor_mat (- m1) m2 = - tensor_mat m1 m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat (- m1) m2 = - tensor_mat m1 m2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L A
m2 \<le>\<^sub>L B

goal (1 subgoal):
 1. tensor_mat (- m1) m2 = - tensor_mat m1 m2
[PROOF STEP]
apply (subgoal_tac "- m1 = -1 \<cdot>\<^sub>m m1")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m1 \<in> carrier_mat d1 d1; m2 \<in> carrier_mat d2 d2; positive m1; positive m2; m1 \<le>\<^sub>L A; m2 \<le>\<^sub>L B; - m1 = - 1 \<cdot>\<^sub>m m1\<rbrakk> \<Longrightarrow> tensor_mat (- m1) m2 = - tensor_mat m1 m2
 2. \<lbrakk>m1 \<in> carrier_mat d1 d1; m2 \<in> carrier_mat d2 d2; positive m1; positive m2; m1 \<le>\<^sub>L A; m2 \<le>\<^sub>L B\<rbrakk> \<Longrightarrow> - m1 = - 1 \<cdot>\<^sub>m m1
[PROOF STEP]
by (auto simp add: tensor_mat_scale1)
[PROOF STATE]
proof (state)
this:
tensor_mat (- m1) m2 = - tensor_mat m1 m2

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
tensor_mat (- m1) m2 = - tensor_mat m1 m2

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
have "tensor_mat (A + (- m1)) m2 = tensor_mat A m2 + (tensor_mat (- m1) m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat (A + - m1) m2 = tensor_mat A m2 + tensor_mat (- m1) m2
[PROOF STEP]
using
      assms
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L A
m2 \<le>\<^sub>L B

goal (1 subgoal):
 1. tensor_mat (A + - m1) m2 = tensor_mat A m2 + tensor_mat (- m1) m2
[PROOF STEP]
by (auto simp add: tensor_mat_add1 dA)
[PROOF STATE]
proof (state)
this:
tensor_mat (A + - m1) m2 = tensor_mat A m2 + tensor_mat (- m1) m2

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
positive (tensor_mat (A + - m1) m2)
tensor_mat (- m1) m2 = - tensor_mat m1 m2
tensor_mat (A + - m1) m2 = tensor_mat A m2 + tensor_mat (- m1) m2
[PROOF STEP]
have "tensor_mat (A + (- m1)) m2 = tensor_mat A m2 - (tensor_mat m1 m2)"
[PROOF STATE]
proof (prove)
using this:
positive (tensor_mat (A + - m1) m2)
tensor_mat (- m1) m2 = - tensor_mat m1 m2
tensor_mat (A + - m1) m2 = tensor_mat A m2 + tensor_mat (- m1) m2

goal (1 subgoal):
 1. tensor_mat (A + - m1) m2 = tensor_mat A m2 - tensor_mat m1 m2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tensor_mat (A + - m1) m2 = tensor_mat A m2 - tensor_mat m1 m2

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
with p1
[PROOF STATE]
proof (chain)
picking this:
positive (tensor_mat (A + - m1) m2)
tensor_mat (A + - m1) m2 = tensor_mat A m2 - tensor_mat m1 m2
[PROOF STEP]
have le1: "tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A m2"
[PROOF STATE]
proof (prove)
using this:
positive (tensor_mat (A + - m1) m2)
tensor_mat (A + - m1) m2 = tensor_mat A m2 - tensor_mat m1 m2

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A m2
[PROOF STEP]
unfolding lowner_le_def
[PROOF STATE]
proof (prove)
using this:
positive (tensor_mat (A + - m1) m2)
tensor_mat (A + - m1) m2 = tensor_mat A m2 - tensor_mat m1 m2

goal (1 subgoal):
 1. dim_row (tensor_mat m1 m2) = dim_row (tensor_mat A m2) \<and> dim_col (tensor_mat m1 m2) = dim_col (tensor_mat A m2) \<and> positive (tensor_mat A m2 - tensor_mat m1 m2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A m2

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
have "B - m2 = B + (- m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B - m2 = B + - m2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L A
m2 \<le>\<^sub>L B

goal (1 subgoal):
 1. B - m2 = B + - m2
[PROOF STEP]
by (auto simp add: minus_add_uminus_mat)
[PROOF STATE]
proof (state)
this:
B - m2 = B + - m2

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B - m2 = B + - m2
[PROOF STEP]
have "positive (B + (- m2))"
[PROOF STATE]
proof (prove)
using this:
B - m2 = B + - m2

goal (1 subgoal):
 1. positive (B + - m2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
B - m2 = B + - m2
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L A
m2 \<le>\<^sub>L B

goal (1 subgoal):
 1. positive (B + - m2)
[PROOF STEP]
unfolding lowner_le_def
[PROOF STATE]
proof (prove)
using this:
B - m2 = B + - m2
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
dim_row m1 = dim_row A \<and> dim_col m1 = dim_col A \<and> positive (A - m1)
dim_row m2 = dim_row B \<and> dim_col m2 = dim_col B \<and> positive (B - m2)

goal (1 subgoal):
 1. positive (B + - m2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (B + - m2)

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
positive (B + - m2)
[PROOF STEP]
have p2: "positive (tensor_mat A (B + (- m2)))"
[PROOF STATE]
proof (prove)
using this:
positive (B + - m2)

goal (1 subgoal):
 1. positive (tensor_mat A (B + - m2))
[PROOF STEP]
using assms tensor_mat_positive positive_one dA dB pA
[PROOF STATE]
proof (prove)
using this:
positive (B + - m2)
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L A
m2 \<le>\<^sub>L B
\<lbrakk>?m1.0 \<in> carrier_mat d1 d1; ?m2.0 \<in> carrier_mat d2 d2; positive ?m1.0; positive ?m2.0\<rbrakk> \<Longrightarrow> positive (tensor_mat ?m1.0 ?m2.0)
positive (1\<^sub>m ?n)
A \<in> carrier_mat d1 d1
B \<in> carrier_mat d2 d2
positive A

goal (1 subgoal):
 1. positive (tensor_mat A (B + - m2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (tensor_mat A (B + - m2))

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
positive (tensor_mat A (B + - m2))

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
have "tensor_mat A (-m2) = - tensor_mat A m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat A (- m2) = - tensor_mat A m2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L A
m2 \<le>\<^sub>L B

goal (1 subgoal):
 1. tensor_mat A (- m2) = - tensor_mat A m2
[PROOF STEP]
apply (subgoal_tac "- m2 = -1 \<cdot>\<^sub>m m2")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m1 \<in> carrier_mat d1 d1; m2 \<in> carrier_mat d2 d2; positive m1; positive m2; m1 \<le>\<^sub>L A; m2 \<le>\<^sub>L B; - m2 = - 1 \<cdot>\<^sub>m m2\<rbrakk> \<Longrightarrow> tensor_mat A (- m2) = - tensor_mat A m2
 2. \<lbrakk>m1 \<in> carrier_mat d1 d1; m2 \<in> carrier_mat d2 d2; positive m1; positive m2; m1 \<le>\<^sub>L A; m2 \<le>\<^sub>L B\<rbrakk> \<Longrightarrow> - m2 = - 1 \<cdot>\<^sub>m m2
[PROOF STEP]
by (auto simp add: tensor_mat_scale2 dA)
[PROOF STATE]
proof (state)
this:
tensor_mat A (- m2) = - tensor_mat A m2

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
tensor_mat A (- m2) = - tensor_mat A m2

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
have "tensor_mat A (B + (- m2)) = tensor_mat A B + tensor_mat A (- m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat A (B + - m2) = tensor_mat A B + tensor_mat A (- m2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L A
m2 \<le>\<^sub>L B

goal (1 subgoal):
 1. tensor_mat A (B + - m2) = tensor_mat A B + tensor_mat A (- m2)
[PROOF STEP]
by (auto simp add: tensor_mat_add2 dA dB)
[PROOF STATE]
proof (state)
this:
tensor_mat A (B + - m2) = tensor_mat A B + tensor_mat A (- m2)

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
positive (tensor_mat A (B + - m2))
tensor_mat A (- m2) = - tensor_mat A m2
tensor_mat A (B + - m2) = tensor_mat A B + tensor_mat A (- m2)
[PROOF STEP]
have "tensor_mat A (B + (- m2)) = tensor_mat A B - tensor_mat A m2"
[PROOF STATE]
proof (prove)
using this:
positive (tensor_mat A (B + - m2))
tensor_mat A (- m2) = - tensor_mat A m2
tensor_mat A (B + - m2) = tensor_mat A B + tensor_mat A (- m2)

goal (1 subgoal):
 1. tensor_mat A (B + - m2) = tensor_mat A B - tensor_mat A m2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tensor_mat A (B + - m2) = tensor_mat A B - tensor_mat A m2

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
with p2
[PROOF STATE]
proof (chain)
picking this:
positive (tensor_mat A (B + - m2))
tensor_mat A (B + - m2) = tensor_mat A B - tensor_mat A m2
[PROOF STEP]
have le20: "tensor_mat A m2 \<le>\<^sub>L tensor_mat A B"
[PROOF STATE]
proof (prove)
using this:
positive (tensor_mat A (B + - m2))
tensor_mat A (B + - m2) = tensor_mat A B - tensor_mat A m2

goal (1 subgoal):
 1. tensor_mat A m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
unfolding lowner_le_def
[PROOF STATE]
proof (prove)
using this:
positive (tensor_mat A (B + - m2))
tensor_mat A (B + - m2) = tensor_mat A B - tensor_mat A m2

goal (1 subgoal):
 1. dim_row (tensor_mat A m2) = dim_row (tensor_mat A B) \<and> dim_col (tensor_mat A m2) = dim_col (tensor_mat A B) \<and> positive (tensor_mat A B - tensor_mat A m2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tensor_mat A m2 \<le>\<^sub>L tensor_mat A B

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B
[PROOF STEP]
apply (subst lowner_le_trans[of _ d "tensor_mat (A) m2"])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. tensor_mat m1 m2 \<in> carrier_mat d d
 2. tensor_mat A m2 \<in> carrier_mat d d
 3. tensor_mat A B \<in> carrier_mat d d
 4. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A m2
 5. tensor_mat A m2 \<le>\<^sub>L tensor_mat A B
 6. True
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat m1 m2 \<in> carrier_mat d d
[PROOF STEP]
using tensor_mat_carrier
[PROOF STATE]
proof (prove)
using this:
tensor_mat ?m1.0 ?m2.0 \<in> carrier_mat d d

goal (1 subgoal):
 1. tensor_mat m1 m2 \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. tensor_mat A m2 \<in> carrier_mat d d
 2. tensor_mat A B \<in> carrier_mat d d
 3. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A m2
 4. tensor_mat A m2 \<le>\<^sub>L tensor_mat A B
 5. True
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat A m2 \<in> carrier_mat d d
[PROOF STEP]
using tensor_mat_carrier
[PROOF STATE]
proof (prove)
using this:
tensor_mat ?m1.0 ?m2.0 \<in> carrier_mat d d

goal (1 subgoal):
 1. tensor_mat A m2 \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. tensor_mat A B \<in> carrier_mat d d
 2. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A m2
 3. tensor_mat A m2 \<le>\<^sub>L tensor_mat A B
 4. True
[PROOF STEP]
using le1 le20
[PROOF STATE]
proof (prove)
using this:
tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A m2
tensor_mat A m2 \<le>\<^sub>L tensor_mat A B

goal (4 subgoals):
 1. tensor_mat A B \<in> carrier_mat d d
 2. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A m2
 3. tensor_mat A m2 \<le>\<^sub>L tensor_mat A B
 4. True
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tensor_mat m1 m2 \<le>\<^sub>L tensor_mat A B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tensor_mat_le_one:
  assumes "m1 \<in> carrier_mat d1 d1"
    and "m2 \<in> carrier_mat d2 d2"
    and "positive m1"
    and "positive m2"
    and "m1 \<le>\<^sub>L 1\<^sub>m d1"
    and "m2 \<le>\<^sub>L 1\<^sub>m d2"
  shows "tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have "1\<^sub>m d1 - m1 = 1\<^sub>m d1 + (- m1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1\<^sub>m d1 - m1 = 1\<^sub>m d1 + - m1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L 1\<^sub>m d1
m2 \<le>\<^sub>L 1\<^sub>m d2

goal (1 subgoal):
 1. 1\<^sub>m d1 - m1 = 1\<^sub>m d1 + - m1
[PROOF STEP]
by (auto simp add: minus_add_uminus_mat)
[PROOF STATE]
proof (state)
this:
1\<^sub>m d1 - m1 = 1\<^sub>m d1 + - m1

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1\<^sub>m d1 - m1 = 1\<^sub>m d1 + - m1
[PROOF STEP]
have "positive (1\<^sub>m d1 + (- m1))"
[PROOF STATE]
proof (prove)
using this:
1\<^sub>m d1 - m1 = 1\<^sub>m d1 + - m1

goal (1 subgoal):
 1. positive (1\<^sub>m d1 + - m1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1\<^sub>m d1 - m1 = 1\<^sub>m d1 + - m1
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L 1\<^sub>m d1
m2 \<le>\<^sub>L 1\<^sub>m d2

goal (1 subgoal):
 1. positive (1\<^sub>m d1 + - m1)
[PROOF STEP]
unfolding lowner_le_def
[PROOF STATE]
proof (prove)
using this:
1\<^sub>m d1 - m1 = 1\<^sub>m d1 + - m1
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
dim_row m1 = dim_row (1\<^sub>m d1) \<and> dim_col m1 = dim_col (1\<^sub>m d1) \<and> positive (1\<^sub>m d1 - m1)
dim_row m2 = dim_row (1\<^sub>m d2) \<and> dim_col m2 = dim_col (1\<^sub>m d2) \<and> positive (1\<^sub>m d2 - m2)

goal (1 subgoal):
 1. positive (1\<^sub>m d1 + - m1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (1\<^sub>m d1 + - m1)

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
positive (1\<^sub>m d1 + - m1)
[PROOF STEP]
have p1: "positive (tensor_mat (1\<^sub>m d1 + (- m1)) m2)"
[PROOF STATE]
proof (prove)
using this:
positive (1\<^sub>m d1 + - m1)

goal (1 subgoal):
 1. positive (tensor_mat (1\<^sub>m d1 + - m1) m2)
[PROOF STEP]
using assms tensor_mat_positive
[PROOF STATE]
proof (prove)
using this:
positive (1\<^sub>m d1 + - m1)
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L 1\<^sub>m d1
m2 \<le>\<^sub>L 1\<^sub>m d2
\<lbrakk>?m1.0 \<in> carrier_mat d1 d1; ?m2.0 \<in> carrier_mat d2 d2; positive ?m1.0; positive ?m2.0\<rbrakk> \<Longrightarrow> positive (tensor_mat ?m1.0 ?m2.0)

goal (1 subgoal):
 1. positive (tensor_mat (1\<^sub>m d1 + - m1) m2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (tensor_mat (1\<^sub>m d1 + - m1) m2)

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
positive (tensor_mat (1\<^sub>m d1 + - m1) m2)

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have "tensor_mat (- m1) m2 = - tensor_mat m1 m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat (- m1) m2 = - tensor_mat m1 m2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L 1\<^sub>m d1
m2 \<le>\<^sub>L 1\<^sub>m d2

goal (1 subgoal):
 1. tensor_mat (- m1) m2 = - tensor_mat m1 m2
[PROOF STEP]
apply (subgoal_tac "- m1 = -1 \<cdot>\<^sub>m m1")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m1 \<in> carrier_mat d1 d1; m2 \<in> carrier_mat d2 d2; positive m1; positive m2; m1 \<le>\<^sub>L 1\<^sub>m d1; m2 \<le>\<^sub>L 1\<^sub>m d2; - m1 = - 1 \<cdot>\<^sub>m m1\<rbrakk> \<Longrightarrow> tensor_mat (- m1) m2 = - tensor_mat m1 m2
 2. \<lbrakk>m1 \<in> carrier_mat d1 d1; m2 \<in> carrier_mat d2 d2; positive m1; positive m2; m1 \<le>\<^sub>L 1\<^sub>m d1; m2 \<le>\<^sub>L 1\<^sub>m d2\<rbrakk> \<Longrightarrow> - m1 = - 1 \<cdot>\<^sub>m m1
[PROOF STEP]
by (auto simp add: tensor_mat_scale1)
[PROOF STATE]
proof (state)
this:
tensor_mat (- m1) m2 = - tensor_mat m1 m2

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
tensor_mat (- m1) m2 = - tensor_mat m1 m2

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have "tensor_mat (1\<^sub>m d1 + (- m1)) m2 = tensor_mat (1\<^sub>m d1) m2 + (tensor_mat (- m1) m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat (1\<^sub>m d1 + - m1) m2 = tensor_mat (1\<^sub>m d1) m2 + tensor_mat (- m1) m2
[PROOF STEP]
using
      assms
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L 1\<^sub>m d1
m2 \<le>\<^sub>L 1\<^sub>m d2

goal (1 subgoal):
 1. tensor_mat (1\<^sub>m d1 + - m1) m2 = tensor_mat (1\<^sub>m d1) m2 + tensor_mat (- m1) m2
[PROOF STEP]
by (auto simp add: tensor_mat_add1)
[PROOF STATE]
proof (state)
this:
tensor_mat (1\<^sub>m d1 + - m1) m2 = tensor_mat (1\<^sub>m d1) m2 + tensor_mat (- m1) m2

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
positive (tensor_mat (1\<^sub>m d1 + - m1) m2)
tensor_mat (- m1) m2 = - tensor_mat m1 m2
tensor_mat (1\<^sub>m d1 + - m1) m2 = tensor_mat (1\<^sub>m d1) m2 + tensor_mat (- m1) m2
[PROOF STEP]
have "tensor_mat (1\<^sub>m d1 + (- m1)) m2 = tensor_mat (1\<^sub>m d1) m2 - (tensor_mat m1 m2)"
[PROOF STATE]
proof (prove)
using this:
positive (tensor_mat (1\<^sub>m d1 + - m1) m2)
tensor_mat (- m1) m2 = - tensor_mat m1 m2
tensor_mat (1\<^sub>m d1 + - m1) m2 = tensor_mat (1\<^sub>m d1) m2 + tensor_mat (- m1) m2

goal (1 subgoal):
 1. tensor_mat (1\<^sub>m d1 + - m1) m2 = tensor_mat (1\<^sub>m d1) m2 - tensor_mat m1 m2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tensor_mat (1\<^sub>m d1 + - m1) m2 = tensor_mat (1\<^sub>m d1) m2 - tensor_mat m1 m2

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
with p1
[PROOF STATE]
proof (chain)
picking this:
positive (tensor_mat (1\<^sub>m d1 + - m1) m2)
tensor_mat (1\<^sub>m d1 + - m1) m2 = tensor_mat (1\<^sub>m d1) m2 - tensor_mat m1 m2
[PROOF STEP]
have le1: "(tensor_mat m1 m2) \<le>\<^sub>L tensor_mat (1\<^sub>m d1) m2"
[PROOF STATE]
proof (prove)
using this:
positive (tensor_mat (1\<^sub>m d1 + - m1) m2)
tensor_mat (1\<^sub>m d1 + - m1) m2 = tensor_mat (1\<^sub>m d1) m2 - tensor_mat m1 m2

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat (1\<^sub>m d1) m2
[PROOF STEP]
unfolding lowner_le_def
[PROOF STATE]
proof (prove)
using this:
positive (tensor_mat (1\<^sub>m d1 + - m1) m2)
tensor_mat (1\<^sub>m d1 + - m1) m2 = tensor_mat (1\<^sub>m d1) m2 - tensor_mat m1 m2

goal (1 subgoal):
 1. dim_row (tensor_mat m1 m2) = dim_row (tensor_mat (1\<^sub>m d1) m2) \<and> dim_col (tensor_mat m1 m2) = dim_col (tensor_mat (1\<^sub>m d1) m2) \<and> positive (tensor_mat (1\<^sub>m d1) m2 - tensor_mat m1 m2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tensor_mat m1 m2 \<le>\<^sub>L tensor_mat (1\<^sub>m d1) m2

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have "1\<^sub>m d2 - m2 = 1\<^sub>m d2 + (- m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1\<^sub>m d2 - m2 = 1\<^sub>m d2 + - m2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L 1\<^sub>m d1
m2 \<le>\<^sub>L 1\<^sub>m d2

goal (1 subgoal):
 1. 1\<^sub>m d2 - m2 = 1\<^sub>m d2 + - m2
[PROOF STEP]
by (auto simp add: minus_add_uminus_mat)
[PROOF STATE]
proof (state)
this:
1\<^sub>m d2 - m2 = 1\<^sub>m d2 + - m2

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1\<^sub>m d2 - m2 = 1\<^sub>m d2 + - m2
[PROOF STEP]
have "positive (1\<^sub>m d2 + (- m2))"
[PROOF STATE]
proof (prove)
using this:
1\<^sub>m d2 - m2 = 1\<^sub>m d2 + - m2

goal (1 subgoal):
 1. positive (1\<^sub>m d2 + - m2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1\<^sub>m d2 - m2 = 1\<^sub>m d2 + - m2
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L 1\<^sub>m d1
m2 \<le>\<^sub>L 1\<^sub>m d2

goal (1 subgoal):
 1. positive (1\<^sub>m d2 + - m2)
[PROOF STEP]
unfolding lowner_le_def
[PROOF STATE]
proof (prove)
using this:
1\<^sub>m d2 - m2 = 1\<^sub>m d2 + - m2
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
dim_row m1 = dim_row (1\<^sub>m d1) \<and> dim_col m1 = dim_col (1\<^sub>m d1) \<and> positive (1\<^sub>m d1 - m1)
dim_row m2 = dim_row (1\<^sub>m d2) \<and> dim_col m2 = dim_col (1\<^sub>m d2) \<and> positive (1\<^sub>m d2 - m2)

goal (1 subgoal):
 1. positive (1\<^sub>m d2 + - m2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (1\<^sub>m d2 + - m2)

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
positive (1\<^sub>m d2 + - m2)
[PROOF STEP]
have p2: "positive (tensor_mat (1\<^sub>m d1) (1\<^sub>m d2 + (- m2)))"
[PROOF STATE]
proof (prove)
using this:
positive (1\<^sub>m d2 + - m2)

goal (1 subgoal):
 1. positive (tensor_mat (1\<^sub>m d1) (1\<^sub>m d2 + - m2))
[PROOF STEP]
using assms tensor_mat_positive positive_one
[PROOF STATE]
proof (prove)
using this:
positive (1\<^sub>m d2 + - m2)
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L 1\<^sub>m d1
m2 \<le>\<^sub>L 1\<^sub>m d2
\<lbrakk>?m1.0 \<in> carrier_mat d1 d1; ?m2.0 \<in> carrier_mat d2 d2; positive ?m1.0; positive ?m2.0\<rbrakk> \<Longrightarrow> positive (tensor_mat ?m1.0 ?m2.0)
positive (1\<^sub>m ?n)

goal (1 subgoal):
 1. positive (tensor_mat (1\<^sub>m d1) (1\<^sub>m d2 + - m2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (tensor_mat (1\<^sub>m d1) (1\<^sub>m d2 + - m2))

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
positive (tensor_mat (1\<^sub>m d1) (1\<^sub>m d2 + - m2))

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have "tensor_mat (1\<^sub>m d1) (-m2) = - tensor_mat (1\<^sub>m d1) m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat (1\<^sub>m d1) (- m2) = - tensor_mat (1\<^sub>m d1) m2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L 1\<^sub>m d1
m2 \<le>\<^sub>L 1\<^sub>m d2

goal (1 subgoal):
 1. tensor_mat (1\<^sub>m d1) (- m2) = - tensor_mat (1\<^sub>m d1) m2
[PROOF STEP]
apply (subgoal_tac "- m2 = -1 \<cdot>\<^sub>m m2")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m1 \<in> carrier_mat d1 d1; m2 \<in> carrier_mat d2 d2; positive m1; positive m2; m1 \<le>\<^sub>L 1\<^sub>m d1; m2 \<le>\<^sub>L 1\<^sub>m d2; - m2 = - 1 \<cdot>\<^sub>m m2\<rbrakk> \<Longrightarrow> tensor_mat (1\<^sub>m d1) (- m2) = - tensor_mat (1\<^sub>m d1) m2
 2. \<lbrakk>m1 \<in> carrier_mat d1 d1; m2 \<in> carrier_mat d2 d2; positive m1; positive m2; m1 \<le>\<^sub>L 1\<^sub>m d1; m2 \<le>\<^sub>L 1\<^sub>m d2\<rbrakk> \<Longrightarrow> - m2 = - 1 \<cdot>\<^sub>m m2
[PROOF STEP]
by (auto simp add: tensor_mat_scale2)
[PROOF STATE]
proof (state)
this:
tensor_mat (1\<^sub>m d1) (- m2) = - tensor_mat (1\<^sub>m d1) m2

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
tensor_mat (1\<^sub>m d1) (- m2) = - tensor_mat (1\<^sub>m d1) m2

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have "tensor_mat (1\<^sub>m d1) (1\<^sub>m d2 + (- m2)) = tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) + (tensor_mat (1\<^sub>m d1) (- m2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat (1\<^sub>m d1) (1\<^sub>m d2 + - m2) = tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) + tensor_mat (1\<^sub>m d1) (- m2)
[PROOF STEP]
using
      assms
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
positive m1
positive m2
m1 \<le>\<^sub>L 1\<^sub>m d1
m2 \<le>\<^sub>L 1\<^sub>m d2

goal (1 subgoal):
 1. tensor_mat (1\<^sub>m d1) (1\<^sub>m d2 + - m2) = tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) + tensor_mat (1\<^sub>m d1) (- m2)
[PROOF STEP]
by (auto simp add: tensor_mat_add2)
[PROOF STATE]
proof (state)
this:
tensor_mat (1\<^sub>m d1) (1\<^sub>m d2 + - m2) = tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) + tensor_mat (1\<^sub>m d1) (- m2)

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
positive (tensor_mat (1\<^sub>m d1) (1\<^sub>m d2 + - m2))
tensor_mat (1\<^sub>m d1) (- m2) = - tensor_mat (1\<^sub>m d1) m2
tensor_mat (1\<^sub>m d1) (1\<^sub>m d2 + - m2) = tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) + tensor_mat (1\<^sub>m d1) (- m2)
[PROOF STEP]
have "tensor_mat (1\<^sub>m d1) (1\<^sub>m d2 + (- m2)) = tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) - (tensor_mat (1\<^sub>m d1) m2)"
[PROOF STATE]
proof (prove)
using this:
positive (tensor_mat (1\<^sub>m d1) (1\<^sub>m d2 + - m2))
tensor_mat (1\<^sub>m d1) (- m2) = - tensor_mat (1\<^sub>m d1) m2
tensor_mat (1\<^sub>m d1) (1\<^sub>m d2 + - m2) = tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) + tensor_mat (1\<^sub>m d1) (- m2)

goal (1 subgoal):
 1. tensor_mat (1\<^sub>m d1) (1\<^sub>m d2 + - m2) = tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) - tensor_mat (1\<^sub>m d1) m2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tensor_mat (1\<^sub>m d1) (1\<^sub>m d2 + - m2) = tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) - tensor_mat (1\<^sub>m d1) m2

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
with p2
[PROOF STATE]
proof (chain)
picking this:
positive (tensor_mat (1\<^sub>m d1) (1\<^sub>m d2 + - m2))
tensor_mat (1\<^sub>m d1) (1\<^sub>m d2 + - m2) = tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) - tensor_mat (1\<^sub>m d1) m2
[PROOF STEP]
have le20: "tensor_mat (1\<^sub>m d1) m2 \<le>\<^sub>L tensor_mat (1\<^sub>m d1) (1\<^sub>m d2)"
[PROOF STATE]
proof (prove)
using this:
positive (tensor_mat (1\<^sub>m d1) (1\<^sub>m d2 + - m2))
tensor_mat (1\<^sub>m d1) (1\<^sub>m d2 + - m2) = tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) - tensor_mat (1\<^sub>m d1) m2

goal (1 subgoal):
 1. tensor_mat (1\<^sub>m d1) m2 \<le>\<^sub>L tensor_mat (1\<^sub>m d1) (1\<^sub>m d2)
[PROOF STEP]
unfolding lowner_le_def
[PROOF STATE]
proof (prove)
using this:
positive (tensor_mat (1\<^sub>m d1) (1\<^sub>m d2 + - m2))
tensor_mat (1\<^sub>m d1) (1\<^sub>m d2 + - m2) = tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) - tensor_mat (1\<^sub>m d1) m2

goal (1 subgoal):
 1. dim_row (tensor_mat (1\<^sub>m d1) m2) = dim_row (tensor_mat (1\<^sub>m d1) (1\<^sub>m d2)) \<and> dim_col (tensor_mat (1\<^sub>m d1) m2) = dim_col (tensor_mat (1\<^sub>m d1) (1\<^sub>m d2)) \<and> positive (tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) - tensor_mat (1\<^sub>m d1) m2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tensor_mat (1\<^sub>m d1) m2 \<le>\<^sub>L tensor_mat (1\<^sub>m d1) (1\<^sub>m d2)

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tensor_mat (1\<^sub>m d1) m2 \<le>\<^sub>L tensor_mat (1\<^sub>m d1) (1\<^sub>m d2)
[PROOF STEP]
have le2: "tensor_mat (1\<^sub>m d1) m2 \<le>\<^sub>L 1\<^sub>m d"
[PROOF STATE]
proof (prove)
using this:
tensor_mat (1\<^sub>m d1) m2 \<le>\<^sub>L tensor_mat (1\<^sub>m d1) (1\<^sub>m d2)

goal (1 subgoal):
 1. tensor_mat (1\<^sub>m d1) m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
apply (subst tensor_mat_id[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat (1\<^sub>m d1) m2 \<le>\<^sub>L tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) \<Longrightarrow> tensor_mat (1\<^sub>m d1) m2 \<le>\<^sub>L tensor_mat (1\<^sub>m d1) (1\<^sub>m d2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tensor_mat (1\<^sub>m d1) m2 \<le>\<^sub>L 1\<^sub>m d

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have "tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) = 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) = 1\<^sub>m d
[PROOF STEP]
using tensor_mat_id
[PROOF STATE]
proof (prove)
using this:
tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) = 1\<^sub>m d

goal (1 subgoal):
 1. tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) = 1\<^sub>m d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) = 1\<^sub>m d

goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
apply (subst lowner_le_trans[of _ d "tensor_mat (1\<^sub>m d1) m2"])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. tensor_mat m1 m2 \<in> carrier_mat d d
 2. tensor_mat (1\<^sub>m d1) m2 \<in> carrier_mat d d
 3. 1\<^sub>m d \<in> carrier_mat d d
 4. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat (1\<^sub>m d1) m2
 5. tensor_mat (1\<^sub>m d1) m2 \<le>\<^sub>L 1\<^sub>m d
 6. True
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat m1 m2 \<in> carrier_mat d d
[PROOF STEP]
using tensor_mat_carrier
[PROOF STATE]
proof (prove)
using this:
tensor_mat ?m1.0 ?m2.0 \<in> carrier_mat d d

goal (1 subgoal):
 1. tensor_mat m1 m2 \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. tensor_mat (1\<^sub>m d1) m2 \<in> carrier_mat d d
 2. 1\<^sub>m d \<in> carrier_mat d d
 3. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat (1\<^sub>m d1) m2
 4. tensor_mat (1\<^sub>m d1) m2 \<le>\<^sub>L 1\<^sub>m d
 5. True
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat (1\<^sub>m d1) m2 \<in> carrier_mat d d
[PROOF STEP]
using tensor_mat_carrier
[PROOF STATE]
proof (prove)
using this:
tensor_mat ?m1.0 ?m2.0 \<in> carrier_mat d d

goal (1 subgoal):
 1. tensor_mat (1\<^sub>m d1) m2 \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. 1\<^sub>m d \<in> carrier_mat d d
 2. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat (1\<^sub>m d1) m2
 3. tensor_mat (1\<^sub>m d1) m2 \<le>\<^sub>L 1\<^sub>m d
 4. True
[PROOF STEP]
using le1 le2
[PROOF STATE]
proof (prove)
using this:
tensor_mat m1 m2 \<le>\<^sub>L tensor_mat (1\<^sub>m d1) m2
tensor_mat (1\<^sub>m d1) m2 \<le>\<^sub>L 1\<^sub>m d

goal (4 subgoals):
 1. 1\<^sub>m d \<in> carrier_mat d d
 2. tensor_mat m1 m2 \<le>\<^sub>L tensor_mat (1\<^sub>m d1) m2
 3. tensor_mat (1\<^sub>m d1) m2 \<le>\<^sub>L 1\<^sub>m d
 4. True
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tensor_mat m1 m2 \<le>\<^sub>L 1\<^sub>m d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mat_extension_carrier:
  "mat_extension m \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_extension m \<in> carrier_mat d d
[PROOF STEP]
by (simp add: mat_extension_def tensor_mat_carrier)


[STATEMENT]
lemma mat_extension_add:
  assumes "m1 \<in> carrier_mat d1 d1"
    and "m2 \<in> carrier_mat d1 d1"
  shows "mat_extension (m1 + m2) = mat_extension m1 + mat_extension m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_extension (m1 + m2) = mat_extension m1 + mat_extension m2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d1 d1

goal (1 subgoal):
 1. mat_extension (m1 + m2) = mat_extension m1 + mat_extension m2
[PROOF STEP]
by (simp add: mat_extension_def tensor_mat_add1)


[STATEMENT]
lemma mat_extension_trace:
  assumes "m \<in> carrier_mat d1 d1"
  shows "trace (mat_extension m) = d2 * trace m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (mat_extension m) = int d2 * trace m
[PROOF STEP]
unfolding mat_extension_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (tensor_mat m (1\<^sub>m d2)) = int d2 * trace m
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m \<in> carrier_mat d1 d1

goal (1 subgoal):
 1. trace (tensor_mat m (1\<^sub>m d2)) = int d2 * trace m
[PROOF STEP]
by (simp add: tensor_mat_trace)


[STATEMENT]
lemma mat_extension_id:
  "mat_extension (1\<^sub>m d1) = 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_extension (1\<^sub>m d1) = 1\<^sub>m d
[PROOF STEP]
unfolding mat_extension_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) = 1\<^sub>m d
[PROOF STEP]
by (rule tensor_mat_id)


[STATEMENT]
lemma mat_extension_mult:
  assumes "m1 \<in> carrier_mat d1 d1"
    and "m2 \<in> carrier_mat d1 d1"
  shows "mat_extension (m1 * m2) = mat_extension m1 * mat_extension m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_extension (m1 * m2) = mat_extension m1 * mat_extension m2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d1 d1

goal (1 subgoal):
 1. mat_extension (m1 * m2) = mat_extension m1 * mat_extension m2
[PROOF STEP]
by (simp add: mat_extension_def tensor_mat_mult[symmetric])


[STATEMENT]
lemma mat_extension_hermitian:
  assumes "m \<in> carrier_mat d1 d1"
    and "hermitian m"
  shows "hermitian (mat_extension m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hermitian (mat_extension m)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m \<in> carrier_mat d1 d1
hermitian m

goal (1 subgoal):
 1. hermitian (mat_extension m)
[PROOF STEP]
by (simp add: hermitian_one mat_extension_def tensor_mat_hermitian)


[STATEMENT]
lemma mat_extension_unitary:
  assumes "m \<in> carrier_mat d1 d1"
    and "unitary m"
  shows "unitary (mat_extension m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unitary (mat_extension m)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m \<in> carrier_mat d1 d1
unitary m

goal (1 subgoal):
 1. unitary (mat_extension m)
[PROOF STEP]
by (simp add: mat_extension_def tensor_mat_unitary unitary_one)


[STATEMENT]
lemma tensor_mat_comm:
  assumes "vars1 \<inter> vars2 = {}"
    and "{0..<length dims} \<subseteq> vars1 \<union> vars2"
    and "m1 \<in> carrier_mat (prod_list (nths dims vars1)) (prod_list (nths dims vars1))"
    and "m2 \<in> carrier_mat (prod_list (nths dims vars2)) (prod_list (nths dims vars2))"
  shows "tensor_mat dims vars1 m1 m2 = tensor_mat dims vars2 m2 m1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat dims vars1 m1 m2 = tensor_mat dims vars2 m2 m1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. tensor_mat dims vars1 m1 m2 = tensor_mat dims vars2 m2 m1
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. tensor_mat dims vars1 m1 m2 = tensor_mat dims vars2 m2 m1
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. tensor_mat dims vars1 m1 m2 = tensor_mat dims vars2 m2 m1
[PROOF STEP]
have "nths dims (- vars2) = nths dims vars1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths dims (- vars2) = nths dims vars1
[PROOF STEP]
using nths_split_complement_eq[symmetric] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<inter> ?B = {}; {0..<length ?xs} \<subseteq> ?A \<union> ?B\<rbrakk> \<Longrightarrow> nths ?xs (- ?B) = nths ?xs ?A
vars1 \<inter> vars2 = {}
{0..<length dims} \<subseteq> vars1 \<union> vars2
m1 \<in> carrier_mat (prod_list (nths dims vars1)) (prod_list (nths dims vars1))
m2 \<in> carrier_mat (prod_list (nths dims vars2)) (prod_list (nths dims vars2))

goal (1 subgoal):
 1. nths dims (- vars2) = nths dims vars1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths dims (- vars2) = nths dims vars1

goal (1 subgoal):
 1. tensor_mat dims vars1 m1 m2 = tensor_mat dims vars2 m2 m1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths dims (- vars2) = nths dims vars1
[PROOF STEP]
have eq2211: "partial_state.dims2 dims vars2 = partial_state.dims1 dims vars1"
[PROOF STATE]
proof (prove)
using this:
nths dims (- vars2) = nths dims vars1

goal (1 subgoal):
 1. partial_state.dims2 dims vars2 = partial_state.dims1 dims vars1
[PROOF STEP]
unfolding partial_state.dims2_def partial_state.dims1_def
[PROOF STATE]
proof (prove)
using this:
nths dims (- vars2) = nths dims vars1

goal (1 subgoal):
 1. nths dims (- vars2) = nths dims vars1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_state.dims2 dims vars2 = partial_state.dims1 dims vars1

goal (1 subgoal):
 1. tensor_mat dims vars1 m1 m2 = tensor_mat dims vars2 m2 m1
[PROOF STEP]
have "nths dims (- vars1) = nths dims vars2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths dims (- vars1) = nths dims vars2
[PROOF STEP]
using nths_split_complement_eq[symmetric, of vars2] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>vars2 \<inter> ?B = {}; {0..<length ?xs} \<subseteq> vars2 \<union> ?B\<rbrakk> \<Longrightarrow> nths ?xs (- ?B) = nths ?xs vars2
vars1 \<inter> vars2 = {}
{0..<length dims} \<subseteq> vars1 \<union> vars2
m1 \<in> carrier_mat (prod_list (nths dims vars1)) (prod_list (nths dims vars1))
m2 \<in> carrier_mat (prod_list (nths dims vars2)) (prod_list (nths dims vars2))

goal (1 subgoal):
 1. nths dims (- vars1) = nths dims vars2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths dims (- vars1) = nths dims vars2

goal (1 subgoal):
 1. tensor_mat dims vars1 m1 m2 = tensor_mat dims vars2 m2 m1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths dims (- vars1) = nths dims vars2
[PROOF STEP]
have eq2112: "partial_state.dims2 dims vars1 = partial_state.dims1 dims vars2"
[PROOF STATE]
proof (prove)
using this:
nths dims (- vars1) = nths dims vars2

goal (1 subgoal):
 1. partial_state.dims2 dims vars1 = partial_state.dims1 dims vars2
[PROOF STEP]
unfolding partial_state.dims2_def partial_state.dims1_def
[PROOF STATE]
proof (prove)
using this:
nths dims (- vars1) = nths dims vars2

goal (1 subgoal):
 1. nths dims (- vars1) = nths dims vars2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_state.dims2 dims vars1 = partial_state.dims1 dims vars2

goal (1 subgoal):
 1. tensor_mat dims vars1 m1 m2 = tensor_mat dims vars2 m2 m1
[PROOF STEP]
have "vars1 \<union> vars2 - vars2 = vars1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars1 \<union> vars2 - vars2 = vars1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vars1 \<inter> vars2 = {}
{0..<length dims} \<subseteq> vars1 \<union> vars2
m1 \<in> carrier_mat (prod_list (nths dims vars1)) (prod_list (nths dims vars1))
m2 \<in> carrier_mat (prod_list (nths dims vars2)) (prod_list (nths dims vars2))

goal (1 subgoal):
 1. vars1 \<union> vars2 - vars2 = vars1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars1 \<union> vars2 - vars2 = vars1

goal (1 subgoal):
 1. tensor_mat dims vars1 m1 m2 = tensor_mat dims vars2 m2 m1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vars1 \<union> vars2 - vars2 = vars1
[PROOF STEP]
have e1:"partial_state.encode2 dims vars2 i = partial_state.encode1 dims (vars1) i"
[PROOF STATE]
proof (prove)
using this:
vars1 \<union> vars2 - vars2 = vars1

goal (1 subgoal):
 1. partial_state.encode2 dims vars2 i = partial_state.encode1 dims vars1 i
[PROOF STEP]
using assms(2) partial_state.encode2_alter[of dims "vars1 \<union> vars2" vars2]
[PROOF STATE]
proof (prove)
using this:
vars1 \<union> vars2 - vars2 = vars1
{0..<length dims} \<subseteq> vars1 \<union> vars2
{0..<length dims} \<subseteq> vars1 \<union> vars2 \<Longrightarrow> partial_state.encode2 dims vars2 ?i = digit_decode (partial_state.dims2 dims vars2) (nths (digit_encode dims ?i) (vars1 \<union> vars2 - vars2))

goal (1 subgoal):
 1. partial_state.encode2 dims vars2 i = partial_state.encode1 dims vars1 i
[PROOF STEP]
unfolding partial_state.encode2_def partial_state.encode1_def
[PROOF STATE]
proof (prove)
using this:
vars1 \<union> vars2 - vars2 = vars1
{0..<length dims} \<subseteq> vars1 \<union> vars2
{0..<length dims} \<subseteq> vars1 \<union> vars2 \<Longrightarrow> digit_decode (partial_state.dims2 dims vars2) (nths (digit_encode dims ?i) (- vars2)) = digit_decode (partial_state.dims2 dims vars2) (nths (digit_encode dims ?i) (vars1 \<union> vars2 - vars2))

goal (1 subgoal):
 1. digit_decode (partial_state.dims2 dims vars2) (nths (digit_encode dims i) (- vars2)) = digit_decode (partial_state.dims1 dims vars1) (nths (digit_encode dims i) vars1)
[PROOF STEP]
apply (subst eq2211[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vars1 \<union> vars2 - vars2 = vars1; {0..<length dims} \<subseteq> vars1 \<union> vars2; \<And>i. {0..<length dims} \<subseteq> vars1 \<union> vars2 \<Longrightarrow> digit_decode (partial_state.dims2 dims vars2) (nths (digit_encode dims i) (- vars2)) = digit_decode (partial_state.dims2 dims vars2) (nths (digit_encode dims i) (vars1 \<union> vars2 - vars2))\<rbrakk> \<Longrightarrow> digit_decode (partial_state.dims2 dims vars2) (nths (digit_encode dims i) (- vars2)) = digit_decode (partial_state.dims2 dims vars2) (nths (digit_encode dims i) vars1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_state.encode2 dims vars2 i = partial_state.encode1 dims vars1 i

goal (1 subgoal):
 1. tensor_mat dims vars1 m1 m2 = tensor_mat dims vars2 m2 m1
[PROOF STEP]
have "vars1 \<union> vars2 - vars1 = vars2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars1 \<union> vars2 - vars1 = vars2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vars1 \<inter> vars2 = {}
{0..<length dims} \<subseteq> vars1 \<union> vars2
m1 \<in> carrier_mat (prod_list (nths dims vars1)) (prod_list (nths dims vars1))
m2 \<in> carrier_mat (prod_list (nths dims vars2)) (prod_list (nths dims vars2))

goal (1 subgoal):
 1. vars1 \<union> vars2 - vars1 = vars2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars1 \<union> vars2 - vars1 = vars2

goal (1 subgoal):
 1. tensor_mat dims vars1 m1 m2 = tensor_mat dims vars2 m2 m1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vars1 \<union> vars2 - vars1 = vars2
[PROOF STEP]
have e2:"partial_state.encode2 dims vars1 i = partial_state.encode1 dims (vars2) i"
[PROOF STATE]
proof (prove)
using this:
vars1 \<union> vars2 - vars1 = vars2

goal (1 subgoal):
 1. partial_state.encode2 dims vars1 i = partial_state.encode1 dims vars2 i
[PROOF STEP]
using assms(2) partial_state.encode2_alter[of dims "vars1 \<union> vars2" vars1]
[PROOF STATE]
proof (prove)
using this:
vars1 \<union> vars2 - vars1 = vars2
{0..<length dims} \<subseteq> vars1 \<union> vars2
{0..<length dims} \<subseteq> vars1 \<union> vars2 \<Longrightarrow> partial_state.encode2 dims vars1 ?i = digit_decode (partial_state.dims2 dims vars1) (nths (digit_encode dims ?i) (vars1 \<union> vars2 - vars1))

goal (1 subgoal):
 1. partial_state.encode2 dims vars1 i = partial_state.encode1 dims vars2 i
[PROOF STEP]
unfolding partial_state.encode2_def partial_state.encode1_def
[PROOF STATE]
proof (prove)
using this:
vars1 \<union> vars2 - vars1 = vars2
{0..<length dims} \<subseteq> vars1 \<union> vars2
{0..<length dims} \<subseteq> vars1 \<union> vars2 \<Longrightarrow> digit_decode (partial_state.dims2 dims vars1) (nths (digit_encode dims ?i) (- vars1)) = digit_decode (partial_state.dims2 dims vars1) (nths (digit_encode dims ?i) (vars1 \<union> vars2 - vars1))

goal (1 subgoal):
 1. digit_decode (partial_state.dims2 dims vars1) (nths (digit_encode dims i) (- vars1)) = digit_decode (partial_state.dims1 dims vars2) (nths (digit_encode dims i) vars2)
[PROOF STEP]
apply (subst eq2112[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vars1 \<union> vars2 - vars1 = vars2; {0..<length dims} \<subseteq> vars1 \<union> vars2; \<And>i. {0..<length dims} \<subseteq> vars1 \<union> vars2 \<Longrightarrow> digit_decode (partial_state.dims2 dims vars1) (nths (digit_encode dims i) (- vars1)) = digit_decode (partial_state.dims2 dims vars1) (nths (digit_encode dims i) (vars1 \<union> vars2 - vars1))\<rbrakk> \<Longrightarrow> digit_decode (partial_state.dims2 dims vars1) (nths (digit_encode dims i) (- vars1)) = digit_decode (partial_state.dims2 dims vars1) (nths (digit_encode dims i) vars2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_state.encode2 dims vars1 i = partial_state.encode1 dims vars2 i

goal (1 subgoal):
 1. tensor_mat dims vars1 m1 m2 = tensor_mat dims vars2 m2 m1
[PROOF STEP]
note e1 e2
[PROOF STATE]
proof (state)
this:
partial_state.encode2 dims vars2 i = partial_state.encode1 dims vars1 i
partial_state.encode2 dims vars1 i = partial_state.encode1 dims vars2 i

goal (1 subgoal):
 1. tensor_mat dims vars1 m1 m2 = tensor_mat dims vars2 m2 m1
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
partial_state.encode2 dims vars2 ?i2 = partial_state.encode1 dims vars1 ?i2
partial_state.encode2 dims vars1 ?i2 = partial_state.encode1 dims vars2 ?i2

goal (1 subgoal):
 1. tensor_mat dims vars1 m1 m2 = tensor_mat dims vars2 m2 m1
[PROOF STEP]
note e = this
[PROOF STATE]
proof (state)
this:
partial_state.encode2 dims vars2 ?i2 = partial_state.encode1 dims vars1 ?i2
partial_state.encode2 dims vars1 ?i2 = partial_state.encode1 dims vars2 ?i2

goal (1 subgoal):
 1. tensor_mat dims vars1 m1 m2 = tensor_mat dims vars2 m2 m1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat dims vars1 m1 m2 = tensor_mat dims vars2 m2 m1
[PROOF STEP]
unfolding partial_state.tensor_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat d d (\<lambda>(i, j). m1 $$ (partial_state.encode1 dims vars1 i, partial_state.encode1 dims vars1 j) * m2 $$ (partial_state.encode2 dims vars1 i, partial_state.encode2 dims vars1 j)) = mat d d (\<lambda>(i, j). m2 $$ (partial_state.encode1 dims vars2 i, partial_state.encode1 dims vars2 j) * m1 $$ (partial_state.encode2 dims vars2 i, partial_state.encode2 dims vars2 j))
[PROOF STEP]
apply (rule cong_mat, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> m1 $$ (partial_state.encode1 dims vars1 i, partial_state.encode1 dims vars1 j) * m2 $$ (partial_state.encode2 dims vars1 i, partial_state.encode2 dims vars1 j) = m2 $$ (partial_state.encode1 dims vars2 i, partial_state.encode1 dims vars2 j) * m1 $$ (partial_state.encode2 dims vars2 i, partial_state.encode2 dims vars2 j)
[PROOF STEP]
unfolding partial_state.dims1_def partial_state.dims2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> m1 $$ (partial_state.encode1 dims vars1 i, partial_state.encode1 dims vars1 j) * m2 $$ (partial_state.encode2 dims vars1 i, partial_state.encode2 dims vars1 j) = m2 $$ (partial_state.encode1 dims vars2 i, partial_state.encode1 dims vars2 j) * m1 $$ (partial_state.encode2 dims vars2 i, partial_state.encode2 dims vars2 j)
[PROOF STEP]
using e
[PROOF STATE]
proof (prove)
using this:
partial_state.encode2 dims vars2 ?i2 = partial_state.encode1 dims vars1 ?i2
partial_state.encode2 dims vars1 ?i2 = partial_state.encode1 dims vars2 ?i2

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> m1 $$ (partial_state.encode1 dims vars1 i, partial_state.encode1 dims vars1 j) * m2 $$ (partial_state.encode2 dims vars1 i, partial_state.encode2 dims vars1 j) = m2 $$ (partial_state.encode1 dims vars2 i, partial_state.encode1 dims vars2 j) * m1 $$ (partial_state.encode2 dims vars2 i, partial_state.encode2 dims vars2 j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tensor_mat dims vars1 m1 m2 = tensor_mat dims vars2 m2 m1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dims_product:
  "d0 = d1 * d2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d0 = d1 * d2
[PROOF STEP]
unfolding d0_def d1_def d2_def dims0_def dims1_def dims2_def vars0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_list (nths dims (vars1 \<union> vars2)) = prod_list (nths dims vars1) * prod_list (nths dims vars2)
[PROOF STEP]
using disjoint nths_prod_list_split[of vars1 "vars1 \<union> vars2" dims]
[PROOF STATE]
proof (prove)
using this:
vars1 \<inter> vars2 = {}
vars1 \<subseteq> vars1 \<union> vars2 \<Longrightarrow> prod_list (nths dims (vars1 \<union> vars2)) = prod_list (nths dims vars1) * prod_list (nths dims (vars1 \<union> vars2 - vars1))

goal (1 subgoal):
 1. prod_list (nths dims (vars1 \<union> vars2)) = prod_list (nths dims vars1) * prod_list (nths dims vars2)
[PROOF STEP]
apply (subgoal_tac "vars1 \<union> vars2 - vars1 = vars2")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>vars1 \<inter> vars2 = {}; vars1 \<subseteq> vars1 \<union> vars2 \<Longrightarrow> prod_list (nths dims (vars1 \<union> vars2)) = prod_list (nths dims vars1) * prod_list (nths dims (vars1 \<union> vars2 - vars1)); vars1 \<union> vars2 - vars1 = vars2\<rbrakk> \<Longrightarrow> prod_list (nths dims (vars1 \<union> vars2)) = prod_list (nths dims vars1) * prod_list (nths dims vars2)
 2. \<lbrakk>vars1 \<inter> vars2 = {}; vars1 \<subseteq> vars1 \<union> vars2 \<Longrightarrow> prod_list (nths dims (vars1 \<union> vars2)) = prod_list (nths dims vars1) * prod_list (nths dims (vars1 \<union> vars2 - vars1))\<rbrakk> \<Longrightarrow> vars1 \<union> vars2 - vars1 = vars2
[PROOF STEP]
by auto


[STATEMENT]
lemma vars1'I:
  "x \<in> vars1 \<Longrightarrow> card {y\<in>vars0. y < x} \<in> vars1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> vars1 \<Longrightarrow> card {y \<in> vars0. y < x} \<in> vars1'
[PROOF STEP]
unfolding vars1'_def ind_in_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> vars1 \<Longrightarrow> card {y \<in> vars0. y < x} \<in> (\<lambda>x. card {i \<in> vars0. i < x}) ` vars1
[PROOF STEP]
by auto


[STATEMENT]
lemma vars1'D:
  "i \<in> vars1' \<Longrightarrow> \<exists>x\<in>vars1. card {y\<in>vars0. y < x} = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<in> vars1' \<Longrightarrow> \<exists>x\<in>vars1. card {y \<in> vars0. y < x} = i
[PROOF STEP]
unfolding vars1'_def ind_in_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<in> (\<lambda>x. card {i \<in> vars0. i < x}) ` vars1 \<Longrightarrow> \<exists>x\<in>vars1. card {y \<in> vars0. y < x} = i
[PROOF STEP]
by auto


[STATEMENT]
lemma ind_in_set_bij:
  "bij_betw (ind_in_set vars0) ({0..<length dims} \<inter> vars0) {0..<card ({0..<length dims} \<inter> vars0)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (ind_in_set vars0) ({0..<length dims} \<inter> vars0) {0..<card ({0..<length dims} \<inter> vars0)}
[PROOF STEP]
using bij_ind_in_set_bound
[PROOF STATE]
proof (prove)
using this:
(\<And>x. ?f x = card {y \<in> ?v0.0. y < x}) \<Longrightarrow> bij_betw ?f ({0..<?M} \<inter> ?v0.0) {0..<card ({0..<?M} \<inter> ?v0.0)}

goal (1 subgoal):
 1. bij_betw (ind_in_set vars0) ({0..<length dims} \<inter> vars0) {0..<card ({0..<length dims} \<inter> vars0)}
[PROOF STEP]
unfolding ind_in_set_def
[PROOF STATE]
proof (prove)
using this:
(\<And>x. ?f x = card {y \<in> ?v0.0. y < x}) \<Longrightarrow> bij_betw ?f ({0..<?M} \<inter> ?v0.0) {0..<card ({0..<?M} \<inter> ?v0.0)}

goal (1 subgoal):
 1. bij_betw (\<lambda>x. card {i \<in> vars0. i < x}) ({0..<length dims} \<inter> vars0) {0..<card ({0..<length dims} \<inter> vars0)}
[PROOF STEP]
by auto


[STATEMENT]
lemma length_dims0:
  "length dims0 = card ({0..<length dims} \<inter> vars0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length dims0 = card ({0..<length dims} \<inter> vars0)
[PROOF STEP]
unfolding dims0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (nths dims vars0) = card ({0..<length dims} \<inter> vars0)
[PROOF STEP]
using length_nths[of dims vars0]
[PROOF STATE]
proof (prove)
using this:
length (nths dims vars0) = card {i. i < length dims \<and> i \<in> vars0}

goal (1 subgoal):
 1. length (nths dims vars0) = card ({0..<length dims} \<inter> vars0)
[PROOF STEP]
apply (subgoal_tac "{i. i < length dims \<and> i \<in> vars0}= {0..<length dims} \<inter> vars0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length (nths dims vars0) = card {i. i < length dims \<and> i \<in> vars0}; {i. i < length dims \<and> i \<in> vars0} = {0..<length dims} \<inter> vars0\<rbrakk> \<Longrightarrow> length (nths dims vars0) = card ({0..<length dims} \<inter> vars0)
 2. length (nths dims vars0) = card {i. i < length dims \<and> i \<in> vars0} \<Longrightarrow> {i. i < length dims \<and> i \<in> vars0} = {0..<length dims} \<inter> vars0
[PROOF STEP]
by auto


[STATEMENT]
lemma length_dims0_minus_vars2'_is_vars1':
  "{0..<length dims0} - vars2' = {0..<length dims0} \<inter> vars1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..<length dims0} - vars2' = {0..<length dims0} \<inter> vars1'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {0..<length dims0} - vars2' = {0..<length dims0} \<inter> vars1'
[PROOF STEP]
have sub20: "vars2 \<subseteq> vars0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars2 \<subseteq> vars0
[PROOF STEP]
unfolding vars0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars2 \<subseteq> vars1 \<union> vars2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars2 \<subseteq> vars0

goal (1 subgoal):
 1. {0..<length dims0} - vars2' = {0..<length dims0} \<inter> vars1'
[PROOF STEP]
have sub1: "vars1 = vars0 - vars2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars1 = vars0 - vars2
[PROOF STEP]
unfolding vars0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars1 = vars1 \<union> vars2 - vars2
[PROOF STEP]
using disjoint
[PROOF STATE]
proof (prove)
using this:
vars1 \<inter> vars2 = {}

goal (1 subgoal):
 1. vars1 = vars1 \<union> vars2 - vars2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars1 = vars0 - vars2

goal (1 subgoal):
 1. {0..<length dims0} - vars2' = {0..<length dims0} \<inter> vars1'
[PROOF STEP]
have eq: "{0..<length dims0} = ind_in_set vars0 ` ({0..<length dims} \<inter> vars0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..<length dims0} = ind_in_set vars0 ` ({0..<length dims} \<inter> vars0)
[PROOF STEP]
using ind_in_set_bij length_dims0 bij_betw_imp_surj_on[of "ind_in_set vars0"]
[PROOF STATE]
proof (prove)
using this:
bij_betw (ind_in_set vars0) ({0..<length dims} \<inter> vars0) {0..<card ({0..<length dims} \<inter> vars0)}
length dims0 = card ({0..<length dims} \<inter> vars0)
bij_betw (ind_in_set vars0) ?A ?B \<Longrightarrow> ind_in_set vars0 ` ?A = ?B

goal (1 subgoal):
 1. {0..<length dims0} = ind_in_set vars0 ` ({0..<length dims} \<inter> vars0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{0..<length dims0} = ind_in_set vars0 ` ({0..<length dims} \<inter> vars0)

goal (1 subgoal):
 1. {0..<length dims0} - vars2' = {0..<length dims0} \<inter> vars1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..<length dims0} - vars2' = {0..<length dims0} \<inter> vars1'
[PROOF STEP]
unfolding vars2'_def vars1'_def eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set vars0 ` ({0..<length dims} \<inter> vars0) - ind_in_set vars0 ` vars2 = ind_in_set vars0 ` ({0..<length dims} \<inter> vars0) \<inter> ind_in_set vars0 ` vars1
[PROOF STEP]
using ind_in_set_minus_subset_bound[OF sub20] sub1
[PROOF STATE]
proof (prove)
using this:
ind_in_set vars0 ` ({0..<?M} \<inter> vars0) - ind_in_set vars0 ` vars2 = ind_in_set vars0 ` ({0..<?M} \<inter> vars0) \<inter> ind_in_set vars0 ` (vars0 - vars2)
vars1 = vars0 - vars2

goal (1 subgoal):
 1. ind_in_set vars0 ` ({0..<length dims} \<inter> vars0) - ind_in_set vars0 ` vars2 = ind_in_set vars0 ` ({0..<length dims} \<inter> vars0) \<inter> ind_in_set vars0 ` vars1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{0..<length dims0} - vars2' = {0..<length dims0} \<inter> vars1'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma length_dims0_minus_vars1'_is_vars2':
  "{0..<length dims0} - vars1' = {0..<length dims0} \<inter> vars2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..<length dims0} - vars1' = {0..<length dims0} \<inter> vars2'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {0..<length dims0} - vars1' = {0..<length dims0} \<inter> vars2'
[PROOF STEP]
have sub10: "vars1 \<subseteq> vars0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars1 \<subseteq> vars0
[PROOF STEP]
unfolding vars0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars1 \<subseteq> vars1 \<union> vars2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars1 \<subseteq> vars0

goal (1 subgoal):
 1. {0..<length dims0} - vars1' = {0..<length dims0} \<inter> vars2'
[PROOF STEP]
have sub2: "vars2 = vars0 - vars1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars2 = vars0 - vars1
[PROOF STEP]
unfolding vars0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars2 = vars1 \<union> vars2 - vars1
[PROOF STEP]
using disjoint
[PROOF STATE]
proof (prove)
using this:
vars1 \<inter> vars2 = {}

goal (1 subgoal):
 1. vars2 = vars1 \<union> vars2 - vars1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars2 = vars0 - vars1

goal (1 subgoal):
 1. {0..<length dims0} - vars1' = {0..<length dims0} \<inter> vars2'
[PROOF STEP]
have eq: "{0..<length dims0} = ind_in_set vars0 ` ({0..<length dims} \<inter> vars0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..<length dims0} = ind_in_set vars0 ` ({0..<length dims} \<inter> vars0)
[PROOF STEP]
using ind_in_set_bij length_dims0 bij_betw_imp_surj_on[of "ind_in_set vars0"]
[PROOF STATE]
proof (prove)
using this:
bij_betw (ind_in_set vars0) ({0..<length dims} \<inter> vars0) {0..<card ({0..<length dims} \<inter> vars0)}
length dims0 = card ({0..<length dims} \<inter> vars0)
bij_betw (ind_in_set vars0) ?A ?B \<Longrightarrow> ind_in_set vars0 ` ?A = ?B

goal (1 subgoal):
 1. {0..<length dims0} = ind_in_set vars0 ` ({0..<length dims} \<inter> vars0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{0..<length dims0} = ind_in_set vars0 ` ({0..<length dims} \<inter> vars0)

goal (1 subgoal):
 1. {0..<length dims0} - vars1' = {0..<length dims0} \<inter> vars2'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..<length dims0} - vars1' = {0..<length dims0} \<inter> vars2'
[PROOF STEP]
unfolding vars2'_def vars1'_def eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set vars0 ` ({0..<length dims} \<inter> vars0) - ind_in_set vars0 ` vars1 = ind_in_set vars0 ` ({0..<length dims} \<inter> vars0) \<inter> ind_in_set vars0 ` vars2
[PROOF STEP]
using ind_in_set_minus_subset_bound[OF sub10] sub2
[PROOF STATE]
proof (prove)
using this:
ind_in_set vars0 ` ({0..<?M} \<inter> vars0) - ind_in_set vars0 ` vars1 = ind_in_set vars0 ` ({0..<?M} \<inter> vars0) \<inter> ind_in_set vars0 ` (vars0 - vars1)
vars2 = vars0 - vars1

goal (1 subgoal):
 1. ind_in_set vars0 ` ({0..<length dims} \<inter> vars0) - ind_in_set vars0 ` vars1 = ind_in_set vars0 ` ({0..<length dims} \<inter> vars0) \<inter> ind_in_set vars0 ` vars2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{0..<length dims0} - vars1' = {0..<length dims0} \<inter> vars2'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nths_vars1':
  "nths dims0 vars1' = dims1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths dims0 vars1' = dims1
[PROOF STEP]
using nths_reencode_eq[of vars1 vars0 dims]
[PROOF STATE]
proof (prove)
using this:
vars1 \<subseteq> vars0 \<Longrightarrow> nths (nths dims vars0) (ind_in_set vars0 ` vars1) = nths dims vars1

goal (1 subgoal):
 1. nths dims0 vars1' = dims1
[PROOF STEP]
using nths_reencode_eq_comp[of vars1 vars0 dims]
[PROOF STATE]
proof (prove)
using this:
vars1 \<subseteq> vars0 \<Longrightarrow> nths (nths dims vars0) (ind_in_set vars0 ` vars1) = nths dims vars1
vars1 \<subseteq> vars0 \<Longrightarrow> nths (nths dims vars0) (- ind_in_set vars0 ` vars1) = nths dims (vars0 - vars1)

goal (1 subgoal):
 1. nths dims0 vars1' = dims1
[PROOF STEP]
unfolding vars0_def ind_in_set_def vars1'_def dims1_def dims0_def
[PROOF STATE]
proof (prove)
using this:
vars1 \<subseteq> vars1 \<union> vars2 \<Longrightarrow> nths (nths dims (vars1 \<union> vars2)) ((\<lambda>x. card {i \<in> vars1 \<union> vars2. i < x}) ` vars1) = nths dims vars1
vars1 \<subseteq> vars1 \<union> vars2 \<Longrightarrow> nths (nths dims (vars1 \<union> vars2)) (- (\<lambda>x. card {i \<in> vars1 \<union> vars2. i < x}) ` vars1) = nths dims (vars1 \<union> vars2 - vars1)

goal (1 subgoal):
 1. nths (nths dims (vars1 \<union> vars2)) ((\<lambda>x. card {i \<in> vars1 \<union> vars2. i < x}) ` vars1) = nths dims vars1
[PROOF STEP]
by auto


[STATEMENT]
lemma nths_vars1'_comp:
  "nths dims0 (-vars2') = dims1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths dims0 (- vars2') = dims1
[PROOF STEP]
using nths_reencode_eq_comp[of vars2 vars0 dims] disjoint
[PROOF STATE]
proof (prove)
using this:
vars2 \<subseteq> vars0 \<Longrightarrow> nths (nths dims vars0) (- ind_in_set vars0 ` vars2) = nths dims (vars0 - vars2)
vars1 \<inter> vars2 = {}

goal (1 subgoal):
 1. nths dims0 (- vars2') = dims1
[PROOF STEP]
unfolding vars0_def ind_in_set_def vars2'_def dims1_def dims0_def
[PROOF STATE]
proof (prove)
using this:
vars2 \<subseteq> vars1 \<union> vars2 \<Longrightarrow> nths (nths dims (vars1 \<union> vars2)) (- (\<lambda>x. card {i \<in> vars1 \<union> vars2. i < x}) ` vars2) = nths dims (vars1 \<union> vars2 - vars2)
vars1 \<inter> vars2 = {}

goal (1 subgoal):
 1. nths (nths dims (vars1 \<union> vars2)) (- (\<lambda>x. card {i \<in> vars1 \<union> vars2. i < x}) ` vars2) = nths dims vars1
[PROOF STEP]
apply (subgoal_tac "(vars1 \<union> vars2 - vars2) = vars1")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>vars2 \<subseteq> vars1 \<union> vars2 \<Longrightarrow> nths (nths dims (vars1 \<union> vars2)) (- (\<lambda>x. card {i \<in> vars1 \<union> vars2. i < x}) ` vars2) = nths dims (vars1 \<union> vars2 - vars2); vars1 \<inter> vars2 = {}; vars1 \<union> vars2 - vars2 = vars1\<rbrakk> \<Longrightarrow> nths (nths dims (vars1 \<union> vars2)) (- (\<lambda>x. card {i \<in> vars1 \<union> vars2. i < x}) ` vars2) = nths dims vars1
 2. \<lbrakk>vars2 \<subseteq> vars1 \<union> vars2 \<Longrightarrow> nths (nths dims (vars1 \<union> vars2)) (- (\<lambda>x. card {i \<in> vars1 \<union> vars2. i < x}) ` vars2) = nths dims (vars1 \<union> vars2 - vars2); vars1 \<inter> vars2 = {}\<rbrakk> \<Longrightarrow> vars1 \<union> vars2 - vars2 = vars1
[PROOF STEP]
by auto


[STATEMENT]
lemma nths_vars2':
  "nths dims0 (-vars1') = dims2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths dims0 (- vars1') = dims2
[PROOF STEP]
using nths_reencode_eq_comp[of vars1 vars0 dims] disjoint
[PROOF STATE]
proof (prove)
using this:
vars1 \<subseteq> vars0 \<Longrightarrow> nths (nths dims vars0) (- ind_in_set vars0 ` vars1) = nths dims (vars0 - vars1)
vars1 \<inter> vars2 = {}

goal (1 subgoal):
 1. nths dims0 (- vars1') = dims2
[PROOF STEP]
unfolding vars0_def ind_in_set_def vars1'_def dims2_def dims0_def
[PROOF STATE]
proof (prove)
using this:
vars1 \<subseteq> vars1 \<union> vars2 \<Longrightarrow> nths (nths dims (vars1 \<union> vars2)) (- (\<lambda>x. card {i \<in> vars1 \<union> vars2. i < x}) ` vars1) = nths dims (vars1 \<union> vars2 - vars1)
vars1 \<inter> vars2 = {}

goal (1 subgoal):
 1. nths (nths dims (vars1 \<union> vars2)) (- (\<lambda>x. card {i \<in> vars1 \<union> vars2. i < x}) ` vars1) = nths dims vars2
[PROOF STEP]
apply (subgoal_tac "(vars1 \<union> vars2 - vars1) = vars2")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>vars1 \<subseteq> vars1 \<union> vars2 \<Longrightarrow> nths (nths dims (vars1 \<union> vars2)) (- (\<lambda>x. card {i \<in> vars1 \<union> vars2. i < x}) ` vars1) = nths dims (vars1 \<union> vars2 - vars1); vars1 \<inter> vars2 = {}; vars1 \<union> vars2 - vars1 = vars2\<rbrakk> \<Longrightarrow> nths (nths dims (vars1 \<union> vars2)) (- (\<lambda>x. card {i \<in> vars1 \<union> vars2. i < x}) ` vars1) = nths dims vars2
 2. \<lbrakk>vars1 \<subseteq> vars1 \<union> vars2 \<Longrightarrow> nths (nths dims (vars1 \<union> vars2)) (- (\<lambda>x. card {i \<in> vars1 \<union> vars2. i < x}) ` vars1) = nths dims (vars1 \<union> vars2 - vars1); vars1 \<inter> vars2 = {}\<rbrakk> \<Longrightarrow> vars1 \<union> vars2 - vars1 = vars2
[PROOF STEP]
by auto


[STATEMENT]
lemma nths_vars2'_comp:
  "nths dims0 (vars2') = dims2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths dims0 vars2' = dims2
[PROOF STEP]
using nths_reencode_eq[of vars2 vars0 dims]
[PROOF STATE]
proof (prove)
using this:
vars2 \<subseteq> vars0 \<Longrightarrow> nths (nths dims vars0) (ind_in_set vars0 ` vars2) = nths dims vars2

goal (1 subgoal):
 1. nths dims0 vars2' = dims2
[PROOF STEP]
unfolding vars0_def ind_in_set_def vars2'_def dims2_def dims0_def
[PROOF STATE]
proof (prove)
using this:
vars2 \<subseteq> vars1 \<union> vars2 \<Longrightarrow> nths (nths dims (vars1 \<union> vars2)) ((\<lambda>x. card {i \<in> vars1 \<union> vars2. i < x}) ` vars2) = nths dims vars2

goal (1 subgoal):
 1. nths (nths dims (vars1 \<union> vars2)) ((\<lambda>x. card {i \<in> vars1 \<union> vars2. i < x}) ` vars2) = nths dims vars2
[PROOF STEP]
by auto