[STATEMENT]
lemma mat_of_cblinfun_uminus:
  "mat_of_cblinfun (- M) = - mat_of_cblinfun M"
  for M::"'a::{basis_enum,complex_normed_vector} \<Rightarrow>\<^sub>C\<^sub>L'b::{basis_enum,complex_normed_vector}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (- M) = - mat_of_cblinfun M
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat_of_cblinfun (- M) = - mat_of_cblinfun M
[PROOF STEP]
define nA where "nA = length (canonical_basis :: 'a list)"
[PROOF STATE]
proof (state)
this:
nA = length canonical_basis

goal (1 subgoal):
 1. mat_of_cblinfun (- M) = - mat_of_cblinfun M
[PROOF STEP]
define nB where "nB = length (canonical_basis :: 'b list)"
[PROOF STATE]
proof (state)
this:
nB = length canonical_basis

goal (1 subgoal):
 1. mat_of_cblinfun (- M) = - mat_of_cblinfun M
[PROOF STEP]
have M1: "mat_of_cblinfun M \<in> carrier_mat nB nA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun M \<in> carrier_mat nB nA
[PROOF STEP]
unfolding nB_def nA_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun M \<in> carrier_mat (length canonical_basis) (length canonical_basis)
[PROOF STEP]
by (metis add.right_neutral add_carrier_mat mat_of_cblinfun_plus mat_of_cblinfun_zero nA_def
        nB_def zero_carrier_mat)
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun M \<in> carrier_mat nB nA

goal (1 subgoal):
 1. mat_of_cblinfun (- M) = - mat_of_cblinfun M
[PROOF STEP]
have M2: "mat_of_cblinfun (-M) \<in> carrier_mat nB nA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (- M) \<in> carrier_mat nB nA
[PROOF STEP]
by (metis add_carrier_mat mat_of_cblinfun_plus mat_of_cblinfun_zero diff_0 nA_def nB_def
        uminus_add_conv_diff zero_carrier_mat)
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (- M) \<in> carrier_mat nB nA

goal (1 subgoal):
 1. mat_of_cblinfun (- M) = - mat_of_cblinfun M
[PROOF STEP]
have "mat_of_cblinfun (M - M) =  0\<^sub>m nB nA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (M - M) = 0\<^sub>m nB nA
[PROOF STEP]
unfolding nA_def nB_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (M - M) = 0\<^sub>m (length canonical_basis) (length canonical_basis)
[PROOF STEP]
by (simp add: mat_of_cblinfun_zero)
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (M - M) = 0\<^sub>m nB nA

goal (1 subgoal):
 1. mat_of_cblinfun (- M) = - mat_of_cblinfun M
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (M - M) = 0\<^sub>m nB nA

goal (1 subgoal):
 1. mat_of_cblinfun (- M) = - mat_of_cblinfun M
[PROOF STEP]
have "mat_of_cblinfun (M - M) = mat_of_cblinfun M + mat_of_cblinfun (- M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (M - M) = mat_of_cblinfun M + mat_of_cblinfun (- M)
[PROOF STEP]
by (metis mat_of_cblinfun_plus pth_2)
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (M - M) = mat_of_cblinfun M + mat_of_cblinfun (- M)

goal (1 subgoal):
 1. mat_of_cblinfun (- M) = - mat_of_cblinfun M
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mat_of_cblinfun (M - M) = 0\<^sub>m nB nA
mat_of_cblinfun (M - M) = mat_of_cblinfun M + mat_of_cblinfun (- M)
[PROOF STEP]
have "mat_of_cblinfun M + mat_of_cblinfun (- M) = 0\<^sub>m nB nA"
[PROOF STATE]
proof (prove)
using this:
mat_of_cblinfun (M - M) = 0\<^sub>m nB nA
mat_of_cblinfun (M - M) = mat_of_cblinfun M + mat_of_cblinfun (- M)

goal (1 subgoal):
 1. mat_of_cblinfun M + mat_of_cblinfun (- M) = 0\<^sub>m nB nA
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun M + mat_of_cblinfun (- M) = 0\<^sub>m nB nA

goal (1 subgoal):
 1. mat_of_cblinfun (- M) = - mat_of_cblinfun M
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
mat_of_cblinfun M + mat_of_cblinfun (- M) = 0\<^sub>m nB nA

goal (1 subgoal):
 1. mat_of_cblinfun (- M) = - mat_of_cblinfun M
[PROOF STEP]
using M1 M2
[PROOF STATE]
proof (prove)
using this:
mat_of_cblinfun M + mat_of_cblinfun (- M) = 0\<^sub>m nB nA
mat_of_cblinfun M \<in> carrier_mat nB nA
mat_of_cblinfun (- M) \<in> carrier_mat nB nA

goal (1 subgoal):
 1. mat_of_cblinfun (- M) = - mat_of_cblinfun M
[PROOF STEP]
by (smt add_uminus_minus_mat assoc_add_mat comm_add_mat left_add_zero_mat minus_r_inv_mat
        uminus_carrier_mat)
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (- M) = - mat_of_cblinfun M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mat_of_cblinfun_minus:
  "mat_of_cblinfun (M - N) = mat_of_cblinfun M - mat_of_cblinfun N"
  for M::"'a::{basis_enum,complex_normed_vector} \<Rightarrow>\<^sub>C\<^sub>L 'b::{basis_enum,complex_normed_vector}" and N::"'a \<Rightarrow>\<^sub>C\<^sub>L'b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (M - N) = mat_of_cblinfun M - mat_of_cblinfun N
[PROOF STEP]
by (smt (z3) add_uminus_minus_mat mat_of_cblinfun_uminus mat_carrier mat_of_cblinfun_def mat_of_cblinfun_plus pth_2)


[STATEMENT]
lemma cblinfun_of_mat_uminus:
  defines "nA \<equiv> length (canonical_basis :: 'a::{basis_enum,complex_normed_vector} list)"
    and "nB \<equiv> length (canonical_basis :: 'b::{basis_enum,complex_normed_vector} list)"
  assumes "M \<in> carrier_mat nB nA"
  shows "(cblinfun_of_mat (-M) :: 'a \<Rightarrow>\<^sub>C\<^sub>L 'b) = - cblinfun_of_mat M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cblinfun_of_mat (- M) = - cblinfun_of_mat M
[PROOF STEP]
by (smt assms add.group_axioms add.right_neutral add_minus_cancel add_uminus_minus_mat
      cblinfun_of_mat_plus group.inverse_inverse mat_of_cblinfun_inverse mat_of_cblinfun_zero
      minus_r_inv_mat uminus_carrier_mat)


[STATEMENT]
lemma cblinfun_of_mat_minus:
  fixes M::"complex mat"
  defines "nA \<equiv> length (canonical_basis :: 'a::{basis_enum,complex_normed_vector} list)"
    and "nB \<equiv> length (canonical_basis :: 'b::{basis_enum,complex_normed_vector} list)"
  assumes "M \<in> carrier_mat nB nA" and "N \<in> carrier_mat nB nA"
  shows "(cblinfun_of_mat (M - N) :: 'a \<Rightarrow>\<^sub>C\<^sub>L 'b) = cblinfun_of_mat M - cblinfun_of_mat N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cblinfun_of_mat (M - N) = cblinfun_of_mat M - cblinfun_of_mat N
[PROOF STEP]
by (metis assms add_uminus_minus_mat cblinfun_of_mat_plus cblinfun_of_mat_uminus pth_2 uminus_carrier_mat)


[STATEMENT]
lemma cblinfun_of_mat_times:
  fixes M N ::"complex mat"
  defines "nA \<equiv> length (canonical_basis :: 'a::{basis_enum,complex_normed_vector} list)"
    and "nB \<equiv> length (canonical_basis :: 'b::{basis_enum,complex_normed_vector} list)"
    and "nC \<equiv> length (canonical_basis :: 'c::{basis_enum,complex_normed_vector} list)"
  assumes a1: "M \<in> carrier_mat nC nB" and a2: "N \<in> carrier_mat nB nA"
  shows  "cblinfun_of_mat (M * N) = ((cblinfun_of_mat M)::'b \<Rightarrow>\<^sub>C\<^sub>L'c) o\<^sub>C\<^sub>L ((cblinfun_of_mat N)::'a \<Rightarrow>\<^sub>C\<^sub>L'b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cblinfun_of_mat (M * N) = cblinfun_of_mat M o\<^sub>C\<^sub>L cblinfun_of_mat N
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cblinfun_of_mat (M * N) = cblinfun_of_mat M o\<^sub>C\<^sub>L cblinfun_of_mat N
[PROOF STEP]
have b1: "((cblinfun_of_mat M)::'b \<Rightarrow>\<^sub>C\<^sub>L'c) v = basis_enum_of_vec (M *\<^sub>v vec_of_basis_enum v)"
    for v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cblinfun_of_mat M *\<^sub>V v = basis_enum_of_vec (M *\<^sub>v vec_of_basis_enum v)
[PROOF STEP]
by (metis assms(4) cblinfun_of_mat.rep_eq nB_def nC_def)
[PROOF STATE]
proof (state)
this:
cblinfun_of_mat M *\<^sub>V ?v = basis_enum_of_vec (M *\<^sub>v vec_of_basis_enum ?v)

goal (1 subgoal):
 1. cblinfun_of_mat (M * N) = cblinfun_of_mat M o\<^sub>C\<^sub>L cblinfun_of_mat N
[PROOF STEP]
have b2: "((cblinfun_of_mat N)::'a \<Rightarrow>\<^sub>C\<^sub>L'b) v = basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum v)"
    for v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cblinfun_of_mat N *\<^sub>V v = basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum v)
[PROOF STEP]
by (metis assms(5) cblinfun_of_mat.rep_eq nA_def nB_def)
[PROOF STATE]
proof (state)
this:
cblinfun_of_mat N *\<^sub>V ?v = basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum ?v)

goal (1 subgoal):
 1. cblinfun_of_mat (M * N) = cblinfun_of_mat M o\<^sub>C\<^sub>L cblinfun_of_mat N
[PROOF STEP]
have b3: "((cblinfun_of_mat (M * N))::'a \<Rightarrow>\<^sub>C\<^sub>L'c) v
       = basis_enum_of_vec ((M * N) *\<^sub>v vec_of_basis_enum v)"
    for v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cblinfun_of_mat (M * N) *\<^sub>V v = basis_enum_of_vec (M * N *\<^sub>v vec_of_basis_enum v)
[PROOF STEP]
by (metis assms(4) assms(5) cblinfun_of_mat.rep_eq mult_carrier_mat nA_def nC_def)
[PROOF STATE]
proof (state)
this:
cblinfun_of_mat (M * N) *\<^sub>V ?v = basis_enum_of_vec (M * N *\<^sub>v vec_of_basis_enum ?v)

goal (1 subgoal):
 1. cblinfun_of_mat (M * N) = cblinfun_of_mat M o\<^sub>C\<^sub>L cblinfun_of_mat N
[PROOF STEP]
have "(basis_enum_of_vec ((M * N) *\<^sub>v vec_of_basis_enum v)::'c)
      = (basis_enum_of_vec (M *\<^sub>v ( vec_of_basis_enum ( (basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum v))::'b ))))"
    for v::'a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_enum_of_vec (M * N *\<^sub>v vec_of_basis_enum v) = basis_enum_of_vec (M *\<^sub>v vec_of_basis_enum (basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum v)))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. basis_enum_of_vec (M * N *\<^sub>v vec_of_basis_enum v) = basis_enum_of_vec (M *\<^sub>v vec_of_basis_enum (basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum v)))
[PROOF STEP]
have c1: "vec_of_basis_enum (basis_enum_of_vec x :: 'b) = x"
      if "dim_vec x = nB"
      for x::"complex vec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (basis_enum_of_vec x) = x
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
dim_vec x = nB

goal (1 subgoal):
 1. vec_of_basis_enum (basis_enum_of_vec x) = x
[PROOF STEP]
unfolding nB_def
[PROOF STATE]
proof (prove)
using this:
dim_vec x = length canonical_basis

goal (1 subgoal):
 1. vec_of_basis_enum (basis_enum_of_vec x) = x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_vec ?x = nB \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec ?x) = ?x

goal (1 subgoal):
 1. basis_enum_of_vec (M * N *\<^sub>v vec_of_basis_enum v) = basis_enum_of_vec (M *\<^sub>v vec_of_basis_enum (basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum v)))
[PROOF STEP]
have c2: "vec_of_basis_enum v \<in> carrier_vec nA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum v \<in> carrier_vec nA
[PROOF STEP]
by (metis (mono_tags, opaque_lifting) add.commute carrier_vec_dim_vec index_add_vec(2)
          index_zero_vec(2) nA_def vec_of_basis_enum_add basis_enum_of_vec_inverse)
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum v \<in> carrier_vec nA

goal (1 subgoal):
 1. basis_enum_of_vec (M * N *\<^sub>v vec_of_basis_enum v) = basis_enum_of_vec (M *\<^sub>v vec_of_basis_enum (basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum v)))
[PROOF STEP]
have "(M * N) *\<^sub>v vec_of_basis_enum v = M *\<^sub>v (N *\<^sub>v vec_of_basis_enum v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M * N *\<^sub>v vec_of_basis_enum v = M *\<^sub>v (N *\<^sub>v vec_of_basis_enum v)
[PROOF STEP]
using Matrix.assoc_mult_mat_vec a1 a2 c2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<in> carrier_mat ?n\<^sub>1 ?n\<^sub>2; ?B \<in> carrier_mat ?n\<^sub>2 ?n\<^sub>3; ?v \<in> carrier_vec ?n\<^sub>3\<rbrakk> \<Longrightarrow> ?A * ?B *\<^sub>v ?v = ?A *\<^sub>v (?B *\<^sub>v ?v)
M \<in> carrier_mat nC nB
N \<in> carrier_mat nB nA
vec_of_basis_enum v \<in> carrier_vec nA

goal (1 subgoal):
 1. M * N *\<^sub>v vec_of_basis_enum v = M *\<^sub>v (N *\<^sub>v vec_of_basis_enum v)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
M * N *\<^sub>v vec_of_basis_enum v = M *\<^sub>v (N *\<^sub>v vec_of_basis_enum v)

goal (1 subgoal):
 1. basis_enum_of_vec (M * N *\<^sub>v vec_of_basis_enum v) = basis_enum_of_vec (M *\<^sub>v vec_of_basis_enum (basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum v)))
[PROOF STEP]
hence "(basis_enum_of_vec ((M * N) *\<^sub>v vec_of_basis_enum v)::'c)
        = (basis_enum_of_vec (M *\<^sub>v (N *\<^sub>v vec_of_basis_enum v))::'c)"
[PROOF STATE]
proof (prove)
using this:
M * N *\<^sub>v vec_of_basis_enum v = M *\<^sub>v (N *\<^sub>v vec_of_basis_enum v)

goal (1 subgoal):
 1. basis_enum_of_vec (M * N *\<^sub>v vec_of_basis_enum v) = basis_enum_of_vec (M *\<^sub>v (N *\<^sub>v vec_of_basis_enum v))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
basis_enum_of_vec (M * N *\<^sub>v vec_of_basis_enum v) = basis_enum_of_vec (M *\<^sub>v (N *\<^sub>v vec_of_basis_enum v))

goal (1 subgoal):
 1. basis_enum_of_vec (M * N *\<^sub>v vec_of_basis_enum v) = basis_enum_of_vec (M *\<^sub>v vec_of_basis_enum (basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum v)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
basis_enum_of_vec (M * N *\<^sub>v vec_of_basis_enum v) = basis_enum_of_vec (M *\<^sub>v (N *\<^sub>v vec_of_basis_enum v))

goal (1 subgoal):
 1. basis_enum_of_vec (M * N *\<^sub>v vec_of_basis_enum v) = basis_enum_of_vec (M *\<^sub>v vec_of_basis_enum (basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum v)))
[PROOF STEP]
have "\<dots> =
      (basis_enum_of_vec (M *\<^sub>v ( vec_of_basis_enum ( (basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum v))::'b ))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_enum_of_vec (M *\<^sub>v (N *\<^sub>v vec_of_basis_enum v)) = basis_enum_of_vec (M *\<^sub>v vec_of_basis_enum (basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum v)))
[PROOF STEP]
using c1 a2
[PROOF STATE]
proof (prove)
using this:
dim_vec ?x = nB \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec ?x) = ?x
N \<in> carrier_mat nB nA

goal (1 subgoal):
 1. basis_enum_of_vec (M *\<^sub>v (N *\<^sub>v vec_of_basis_enum v)) = basis_enum_of_vec (M *\<^sub>v vec_of_basis_enum (basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum v)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
basis_enum_of_vec (M *\<^sub>v (N *\<^sub>v vec_of_basis_enum v)) = basis_enum_of_vec (M *\<^sub>v vec_of_basis_enum (basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum v)))

goal (1 subgoal):
 1. basis_enum_of_vec (M * N *\<^sub>v vec_of_basis_enum v) = basis_enum_of_vec (M *\<^sub>v vec_of_basis_enum (basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum v)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
basis_enum_of_vec (M * N *\<^sub>v vec_of_basis_enum v) = basis_enum_of_vec (M *\<^sub>v vec_of_basis_enum (basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum v)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
basis_enum_of_vec (M * N *\<^sub>v vec_of_basis_enum v) = basis_enum_of_vec (M *\<^sub>v vec_of_basis_enum (basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum v)))

goal (1 subgoal):
 1. basis_enum_of_vec (M * N *\<^sub>v vec_of_basis_enum v) = basis_enum_of_vec (M *\<^sub>v vec_of_basis_enum (basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum v)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
basis_enum_of_vec (M * N *\<^sub>v vec_of_basis_enum v) = basis_enum_of_vec (M *\<^sub>v vec_of_basis_enum (basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum v)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
basis_enum_of_vec (M * N *\<^sub>v vec_of_basis_enum ?v) = basis_enum_of_vec (M *\<^sub>v vec_of_basis_enum (basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum ?v)))

goal (1 subgoal):
 1. cblinfun_of_mat (M * N) = cblinfun_of_mat M o\<^sub>C\<^sub>L cblinfun_of_mat N
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
basis_enum_of_vec (M * N *\<^sub>v vec_of_basis_enum ?v) = basis_enum_of_vec (M *\<^sub>v vec_of_basis_enum (basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum ?v)))

goal (1 subgoal):
 1. cblinfun_of_mat (M * N) = cblinfun_of_mat M o\<^sub>C\<^sub>L cblinfun_of_mat N
[PROOF STEP]
using b1 b2 b3
[PROOF STATE]
proof (prove)
using this:
basis_enum_of_vec (M * N *\<^sub>v vec_of_basis_enum ?v) = basis_enum_of_vec (M *\<^sub>v vec_of_basis_enum (basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum ?v)))
cblinfun_of_mat M *\<^sub>V ?v = basis_enum_of_vec (M *\<^sub>v vec_of_basis_enum ?v)
cblinfun_of_mat N *\<^sub>V ?v = basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum ?v)
cblinfun_of_mat (M * N) *\<^sub>V ?v = basis_enum_of_vec (M * N *\<^sub>v vec_of_basis_enum ?v)

goal (1 subgoal):
 1. cblinfun_of_mat (M * N) = cblinfun_of_mat M o\<^sub>C\<^sub>L cblinfun_of_mat N
[PROOF STEP]
by (simp add: cblinfun_eqI scaleC_cblinfun.rep_eq)
[PROOF STATE]
proof (state)
this:
cblinfun_of_mat (M * N) = cblinfun_of_mat M o\<^sub>C\<^sub>L cblinfun_of_mat N

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cblinfun_of_mat_adjoint:
  defines "nA \<equiv> length (canonical_basis :: 'a::onb_enum list)"
    and "nB \<equiv> length (canonical_basis :: 'b::onb_enum list)"
  fixes M:: "complex mat"
  assumes "M \<in> carrier_mat nB nA"
  shows "((cblinfun_of_mat (mat_adjoint M)) :: 'b \<Rightarrow>\<^sub>C\<^sub>L 'a) = (cblinfun_of_mat M)*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cblinfun_of_mat (mat_adjoint M) = cblinfun_of_mat M*
[PROOF STEP]
proof (rule adjoint_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. (cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) \<bullet>\<^sub>C y = x \<bullet>\<^sub>C (cblinfun_of_mat M *\<^sub>V y)
[PROOF STEP]
show "(cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) \<bullet>\<^sub>C y = x \<bullet>\<^sub>C (cblinfun_of_mat M *\<^sub>V y)"
    for x::'b and y::'a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) \<bullet>\<^sub>C y = x \<bullet>\<^sub>C (cblinfun_of_mat M *\<^sub>V y)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) \<bullet>\<^sub>C y = x \<bullet>\<^sub>C (cblinfun_of_mat M *\<^sub>V y)
[PROOF STEP]
define u where "u = vec_of_basis_enum x"
[PROOF STATE]
proof (state)
this:
u = vec_of_basis_enum x

goal (1 subgoal):
 1. (cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) \<bullet>\<^sub>C y = x \<bullet>\<^sub>C (cblinfun_of_mat M *\<^sub>V y)
[PROOF STEP]
define v where "v = vec_of_basis_enum y"
[PROOF STATE]
proof (state)
this:
v = vec_of_basis_enum y

goal (1 subgoal):
 1. (cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) \<bullet>\<^sub>C y = x \<bullet>\<^sub>C (cblinfun_of_mat M *\<^sub>V y)
[PROOF STEP]
have c1: "vec_of_basis_enum ((cblinfun_of_mat (mat_adjoint M) *\<^sub>V x)::'a) = (mat_adjoint M) *\<^sub>v u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) = mat_adjoint M *\<^sub>v u
[PROOF STEP]
unfolding u_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) = mat_adjoint M *\<^sub>v vec_of_basis_enum x
[PROOF STEP]
by (metis (mono_tags, lifting) assms(3) cblinfun_of_mat_inverse map_carrier_mat mat_adjoint_def' mat_of_cblinfun_cblinfun_apply nA_def nB_def transpose_carrier_mat)
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) = mat_adjoint M *\<^sub>v u

goal (1 subgoal):
 1. (cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) \<bullet>\<^sub>C y = x \<bullet>\<^sub>C (cblinfun_of_mat M *\<^sub>V y)
[PROOF STEP]
have c2: "(vec_of_basis_enum ((cblinfun_of_mat M *\<^sub>V y)::'b))
        = M *\<^sub>v v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (cblinfun_of_mat M *\<^sub>V y) = M *\<^sub>v v
[PROOF STEP]
by (metis assms(3) cblinfun_of_mat_inverse mat_of_cblinfun_cblinfun_apply nA_def nB_def v_def)
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (cblinfun_of_mat M *\<^sub>V y) = M *\<^sub>v v

goal (1 subgoal):
 1. (cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) \<bullet>\<^sub>C y = x \<bullet>\<^sub>C (cblinfun_of_mat M *\<^sub>V y)
[PROOF STEP]
have c3: "dim_vec v = nA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec v = nA
[PROOF STEP]
unfolding v_def nA_def vec_of_basis_enum_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (vec_of_list (map (crepresentation (set canonical_basis) y) canonical_basis)) = length canonical_basis
[PROOF STEP]
by (simp add:)
[PROOF STATE]
proof (state)
this:
dim_vec v = nA

goal (1 subgoal):
 1. (cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) \<bullet>\<^sub>C y = x \<bullet>\<^sub>C (cblinfun_of_mat M *\<^sub>V y)
[PROOF STEP]
have c4: "dim_vec u = nB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec u = nB
[PROOF STEP]
unfolding u_def nB_def vec_of_basis_enum_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (vec_of_list (map (crepresentation (set canonical_basis) x) canonical_basis)) = length canonical_basis
[PROOF STEP]
by (simp add:)
[PROOF STATE]
proof (state)
this:
dim_vec u = nB

goal (1 subgoal):
 1. (cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) \<bullet>\<^sub>C y = x \<bullet>\<^sub>C (cblinfun_of_mat M *\<^sub>V y)
[PROOF STEP]
have "v \<bullet>c ((mat_adjoint M) *\<^sub>v u) = (M *\<^sub>v v) \<bullet>c u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<bullet>c (mat_adjoint M *\<^sub>v u) = (M *\<^sub>v v) \<bullet>c u
[PROOF STEP]
using c3 c4 cscalar_prod_adjoint assms(3)
[PROOF STATE]
proof (prove)
using this:
dim_vec v = nA
dim_vec u = nB
\<lbrakk>?M \<in> carrier_mat ?nB ?nA; dim_vec ?v = ?nA; dim_vec ?u = ?nB\<rbrakk> \<Longrightarrow> ?v \<bullet>c (mat_adjoint ?M *\<^sub>v ?u) = (?M *\<^sub>v ?v) \<bullet>c ?u
M \<in> carrier_mat nB nA

goal (1 subgoal):
 1. v \<bullet>c (mat_adjoint M *\<^sub>v u) = (M *\<^sub>v v) \<bullet>c u
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v \<bullet>c (mat_adjoint M *\<^sub>v u) = (M *\<^sub>v v) \<bullet>c u

goal (1 subgoal):
 1. (cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) \<bullet>\<^sub>C y = x \<bullet>\<^sub>C (cblinfun_of_mat M *\<^sub>V y)
[PROOF STEP]
hence "v \<bullet>c (vec_of_basis_enum ((cblinfun_of_mat (mat_adjoint M) *\<^sub>V x)::'a))
        = (vec_of_basis_enum ((cblinfun_of_mat M *\<^sub>V y)::'b)) \<bullet>c u"
[PROOF STATE]
proof (prove)
using this:
v \<bullet>c (mat_adjoint M *\<^sub>v u) = (M *\<^sub>v v) \<bullet>c u

goal (1 subgoal):
 1. v \<bullet>c vec_of_basis_enum (cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) = vec_of_basis_enum (cblinfun_of_mat M *\<^sub>V y) \<bullet>c u
[PROOF STEP]
using c1 c2
[PROOF STATE]
proof (prove)
using this:
v \<bullet>c (mat_adjoint M *\<^sub>v u) = (M *\<^sub>v v) \<bullet>c u
vec_of_basis_enum (cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) = mat_adjoint M *\<^sub>v u
vec_of_basis_enum (cblinfun_of_mat M *\<^sub>V y) = M *\<^sub>v v

goal (1 subgoal):
 1. v \<bullet>c vec_of_basis_enum (cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) = vec_of_basis_enum (cblinfun_of_mat M *\<^sub>V y) \<bullet>c u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v \<bullet>c vec_of_basis_enum (cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) = vec_of_basis_enum (cblinfun_of_mat M *\<^sub>V y) \<bullet>c u

goal (1 subgoal):
 1. (cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) \<bullet>\<^sub>C y = x \<bullet>\<^sub>C (cblinfun_of_mat M *\<^sub>V y)
[PROOF STEP]
thus "(cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) \<bullet>\<^sub>C y = x \<bullet>\<^sub>C (cblinfun_of_mat M *\<^sub>V y)"
[PROOF STATE]
proof (prove)
using this:
v \<bullet>c vec_of_basis_enum (cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) = vec_of_basis_enum (cblinfun_of_mat M *\<^sub>V y) \<bullet>c u

goal (1 subgoal):
 1. (cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) \<bullet>\<^sub>C y = x \<bullet>\<^sub>C (cblinfun_of_mat M *\<^sub>V y)
[PROOF STEP]
unfolding u_def v_def
[PROOF STATE]
proof (prove)
using this:
vec_of_basis_enum y \<bullet>c vec_of_basis_enum (cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) = vec_of_basis_enum (cblinfun_of_mat M *\<^sub>V y) \<bullet>c vec_of_basis_enum x

goal (1 subgoal):
 1. (cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) \<bullet>\<^sub>C y = x \<bullet>\<^sub>C (cblinfun_of_mat M *\<^sub>V y)
[PROOF STEP]
by (simp add: cscalar_prod_vec_of_basis_enum)
[PROOF STATE]
proof (state)
this:
(cblinfun_of_mat (mat_adjoint M) *\<^sub>V x) \<bullet>\<^sub>C y = x \<bullet>\<^sub>C (cblinfun_of_mat M *\<^sub>V y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(cblinfun_of_mat (mat_adjoint M) *\<^sub>V ?x) \<bullet>\<^sub>C ?y = ?x \<bullet>\<^sub>C (cblinfun_of_mat M *\<^sub>V ?y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mat_of_cblinfun_classical_operator:
  fixes f::"'a::enum \<Rightarrow> 'b::enum option"
  shows "mat_of_cblinfun (classical_operator f) = mat (CARD('b)) (CARD('a))
           (\<lambda>(r,c). if f (Enum.enum!c) = Some (Enum.enum!r) then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0)
[PROOF STEP]
define nA where "nA = CARD('a)"
[PROOF STATE]
proof (state)
this:
nA = CARD('a)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0)
[PROOF STEP]
define nB where "nB = CARD('b)"
[PROOF STATE]
proof (state)
this:
nB = CARD('b)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0)
[PROOF STEP]
define BasisA where "BasisA = (canonical_basis::'a ell2 list)"
[PROOF STATE]
proof (state)
this:
BasisA = canonical_basis

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0)
[PROOF STEP]
define BasisB where "BasisB = (canonical_basis::'b ell2 list)"
[PROOF STATE]
proof (state)
this:
BasisB = canonical_basis

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0)
[PROOF STEP]
have "mat_of_cblinfun (classical_operator f) \<in> carrier_mat nB nA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) \<in> carrier_mat nB nA
[PROOF STEP]
unfolding nA_def nB_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) \<in> carrier_mat CARD('b) CARD('a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (classical_operator f) \<in> carrier_mat nB nA

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (classical_operator f) \<in> carrier_mat nB nA

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0)
[PROOF STEP]
have "nA = CARD ('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nA = CARD('a)
[PROOF STEP]
unfolding nA_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD('a) = CARD('a)
[PROOF STEP]
by (simp add:)
[PROOF STATE]
proof (state)
this:
nA = CARD('a)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nA = CARD('a)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0)
[PROOF STEP]
have "nB = CARD ('b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nB = CARD('b)
[PROOF STEP]
unfolding nB_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD('b) = CARD('b)
[PROOF STEP]
by (simp add:)
[PROOF STATE]
proof (state)
this:
nB = CARD('b)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mat_of_cblinfun (classical_operator f) \<in> carrier_mat nB nA
nA = CARD('a)
nB = CARD('b)
[PROOF STEP]
have "mat_of_cblinfun (classical_operator f) \<in> carrier_mat (CARD('b)) (CARD('a))"
[PROOF STATE]
proof (prove)
using this:
mat_of_cblinfun (classical_operator f) \<in> carrier_mat nB nA
nA = CARD('a)
nB = CARD('b)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) \<in> carrier_mat CARD('b) CARD('a)
[PROOF STEP]
unfolding nA_def nB_def
[PROOF STATE]
proof (prove)
using this:
mat_of_cblinfun (classical_operator f) \<in> carrier_mat CARD('b) CARD('a)
CARD('a) = CARD('a)
CARD('b) = CARD('b)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) \<in> carrier_mat CARD('b) CARD('a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (classical_operator f) \<in> carrier_mat CARD('b) CARD('a)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (classical_operator f) \<in> carrier_mat CARD('b) CARD('a)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0)
[PROOF STEP]
have "(mat_of_cblinfun (classical_operator f))$$(r,c)
  = (mat (CARD('b)) (CARD('a))
    (\<lambda>(r,c). if f (Enum.enum!c) = Some (Enum.enum!r) then 1 else 0))$$(r,c)"
    if a1: "r < CARD('b)" and a2: "c < CARD('a)"
    for r c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0) $$ (r, c)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0) $$ (r, c)
[PROOF STEP]
have "CARD('a) = length (enum_class.enum::'a list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD('a) = length enum_class.enum
[PROOF STEP]
using card_UNIV_length_enum[where 'a = 'a]
[PROOF STATE]
proof (prove)
using this:
CARD('a) = length enum_class.enum

goal (1 subgoal):
 1. CARD('a) = length enum_class.enum
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
CARD('a) = length enum_class.enum

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0) $$ (r, c)
[PROOF STEP]
hence x1: "BasisA!c = ket ((Enum.enum::'a list)!c)"
[PROOF STATE]
proof (prove)
using this:
CARD('a) = length enum_class.enum

goal (1 subgoal):
 1. BasisA ! c = ket (enum_class.enum ! c)
[PROOF STEP]
unfolding BasisA_def
[PROOF STATE]
proof (prove)
using this:
CARD('a) = length enum_class.enum

goal (1 subgoal):
 1. canonical_basis ! c = ket (enum_class.enum ! c)
[PROOF STEP]
using a2 canonical_basis_ell2_def
        nth_map[where n = c and xs = "Enum.enum::'a list" and f = ket]
[PROOF STATE]
proof (prove)
using this:
CARD('a) = length enum_class.enum
c < CARD('a)
canonical_basis = map ket enum_class.enum
c < length enum_class.enum \<Longrightarrow> map ket enum_class.enum ! c = ket (enum_class.enum ! c)

goal (1 subgoal):
 1. canonical_basis ! c = ket (enum_class.enum ! c)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
BasisA ! c = ket (enum_class.enum ! c)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0) $$ (r, c)
[PROOF STEP]
have cardb: "CARD('b) = length (enum_class.enum::'b list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD('b) = length enum_class.enum
[PROOF STEP]
using card_UNIV_length_enum[where 'a = 'b]
[PROOF STATE]
proof (prove)
using this:
CARD('b) = length enum_class.enum

goal (1 subgoal):
 1. CARD('b) = length enum_class.enum
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
CARD('b) = length enum_class.enum

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0) $$ (r, c)
[PROOF STEP]
hence x2: "BasisB!r = ket ((Enum.enum::'b list)!r)"
[PROOF STATE]
proof (prove)
using this:
CARD('b) = length enum_class.enum

goal (1 subgoal):
 1. BasisB ! r = ket (enum_class.enum ! r)
[PROOF STEP]
unfolding BasisB_def
[PROOF STATE]
proof (prove)
using this:
CARD('b) = length enum_class.enum

goal (1 subgoal):
 1. canonical_basis ! r = ket (enum_class.enum ! r)
[PROOF STEP]
using a1 canonical_basis_ell2_def
        nth_map[where n = r and xs = "Enum.enum::'b list" and f = ket]
[PROOF STATE]
proof (prove)
using this:
CARD('b) = length enum_class.enum
r < CARD('b)
canonical_basis = map ket enum_class.enum
r < length enum_class.enum \<Longrightarrow> map ket enum_class.enum ! r = ket (enum_class.enum ! r)

goal (1 subgoal):
 1. canonical_basis ! r = ket (enum_class.enum ! r)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
BasisB ! r = ket (enum_class.enum ! r)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0) $$ (r, c)
[PROOF STEP]
have "inj (map (ket::'b \<Rightarrow>_))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj (map ket)
[PROOF STEP]
by (meson injI ket_injective list.inj_map)
[PROOF STATE]
proof (state)
this:
inj (map ket)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0) $$ (r, c)
[PROOF STEP]
hence "length (Enum.enum::'b list) = length (map (ket::'b \<Rightarrow>_) (Enum.enum::'b list))"
[PROOF STATE]
proof (prove)
using this:
inj (map ket)

goal (1 subgoal):
 1. length enum_class.enum = length (map ket enum_class.enum)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length enum_class.enum = length (map ket enum_class.enum)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0) $$ (r, c)
[PROOF STEP]
hence lengthBasisB: "CARD('b) = length BasisB"
[PROOF STATE]
proof (prove)
using this:
length enum_class.enum = length (map ket enum_class.enum)

goal (1 subgoal):
 1. CARD('b) = length BasisB
[PROOF STEP]
unfolding BasisB_def canonical_basis_ell2_def
[PROOF STATE]
proof (prove)
using this:
length enum_class.enum = length (map ket enum_class.enum)

goal (1 subgoal):
 1. CARD('b) = length (map ket enum_class.enum)
[PROOF STEP]
using cardb
[PROOF STATE]
proof (prove)
using this:
length enum_class.enum = length (map ket enum_class.enum)
CARD('b) = length enum_class.enum

goal (1 subgoal):
 1. CARD('b) = length (map ket enum_class.enum)
[PROOF STEP]
by smt
[PROOF STATE]
proof (state)
this:
CARD('b) = length BasisB

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0) $$ (r, c)
[PROOF STEP]
have v1: "(mat_of_cblinfun (classical_operator f))$$(r,c) = 0"
      if c1: "f (Enum.enum!c) = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
have "(classical_operator f) *\<^sub>V ket (Enum.enum!c)
          = (case f (Enum.enum!c) of None \<Rightarrow> 0 | Some i \<Rightarrow> ket i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. classical_operator f *\<^sub>V ket (enum_class.enum ! c) = (case f (enum_class.enum ! c) of None \<Rightarrow> 0 | Some i \<Rightarrow> ket i)
[PROOF STEP]
using classical_operator_ket_finite
[PROOF STATE]
proof (prove)
using this:
classical_operator ?\<pi> *\<^sub>V ket ?x = (case ?\<pi> ?x of None \<Rightarrow> 0 | Some i \<Rightarrow> ket i)

goal (1 subgoal):
 1. classical_operator f *\<^sub>V ket (enum_class.enum ! c) = (case f (enum_class.enum ! c) of None \<Rightarrow> 0 | Some i \<Rightarrow> ket i)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
classical_operator f *\<^sub>V ket (enum_class.enum ! c) = (case f (enum_class.enum ! c) of None \<Rightarrow> 0 | Some i \<Rightarrow> ket i)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
classical_operator f *\<^sub>V ket (enum_class.enum ! c) = (case f (enum_class.enum ! c) of None \<Rightarrow> 0 | Some i \<Rightarrow> ket i)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
have "\<dots> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case f (enum_class.enum ! c) of None \<Rightarrow> 0 | Some i \<Rightarrow> ket i) = 0
[PROOF STEP]
using c1
[PROOF STATE]
proof (prove)
using this:
f (enum_class.enum ! c) = None

goal (1 subgoal):
 1. (case f (enum_class.enum ! c) of None \<Rightarrow> 0 | Some i \<Rightarrow> ket i) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(case f (enum_class.enum ! c) of None \<Rightarrow> 0 | Some i \<Rightarrow> ket i) = 0

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
classical_operator f *\<^sub>V ket (enum_class.enum ! c) = 0
[PROOF STEP]
have "(classical_operator f) *\<^sub>V ket (Enum.enum!c) = 0"
[PROOF STATE]
proof (prove)
using this:
classical_operator f *\<^sub>V ket (enum_class.enum ! c) = 0

goal (1 subgoal):
 1. classical_operator f *\<^sub>V ket (enum_class.enum ! c) = 0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
classical_operator f *\<^sub>V ket (enum_class.enum ! c) = 0

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
hence *: "(classical_operator f) *\<^sub>V BasisA!c = 0"
[PROOF STATE]
proof (prove)
using this:
classical_operator f *\<^sub>V ket (enum_class.enum ! c) = 0

goal (1 subgoal):
 1. classical_operator f *\<^sub>V BasisA ! c = 0
[PROOF STEP]
using x1
[PROOF STATE]
proof (prove)
using this:
classical_operator f *\<^sub>V ket (enum_class.enum ! c) = 0
BasisA ! c = ket (enum_class.enum ! c)

goal (1 subgoal):
 1. classical_operator f *\<^sub>V BasisA ! c = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
classical_operator f *\<^sub>V BasisA ! c = 0

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
hence "is_orthogonal (BasisB!r) (classical_operator f *\<^sub>V BasisA!c)"
[PROOF STATE]
proof (prove)
using this:
classical_operator f *\<^sub>V BasisA ! c = 0

goal (1 subgoal):
 1. is_orthogonal (BasisB ! r) (classical_operator f *\<^sub>V BasisA ! c)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_orthogonal (BasisB ! r) (classical_operator f *\<^sub>V BasisA ! c)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
is_orthogonal (BasisB ! r) (classical_operator f *\<^sub>V BasisA ! c)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
unfolding mat_of_cblinfun_def BasisA_def BasisB_def
[PROOF STATE]
proof (prove)
using this:
is_orthogonal (canonical_basis ! r) (classical_operator f *\<^sub>V canonical_basis ! c)

goal (1 subgoal):
 1. mat (length canonical_basis) (length canonical_basis) (\<lambda>(i, j). crepresentation (set canonical_basis) (classical_operator f *\<^sub>V canonical_basis ! j) (canonical_basis ! i)) $$ (r, c) = 0
[PROOF STEP]
by (smt (verit, del_insts) BasisA_def * a1 a2 canonical_basis_length_ell2 complex_vector.representation_zero index_mat(1) old.prod.case)
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (classical_operator f) $$ (r, c) = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f (enum_class.enum ! c) = None \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0) $$ (r, c)
[PROOF STEP]
have v2: "(mat_of_cblinfun (classical_operator f))$$(r,c) = 0"
      if c1: "f (Enum.enum!c) = Some (Enum.enum!r')" and c2: "r\<noteq>r'"
        and c3: "r' < CARD('b)"
      for r'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
have x3: "BasisB!r' = ket ((Enum.enum::'b list)!r')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BasisB ! r' = ket (enum_class.enum ! r')
[PROOF STEP]
unfolding BasisB_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. canonical_basis ! r' = ket (enum_class.enum ! r')
[PROOF STEP]
using cardb c3 canonical_basis_ell2_def
          nth_map[where n = r' and xs = "Enum.enum::'b list" and f = ket]
[PROOF STATE]
proof (prove)
using this:
CARD('b) = length enum_class.enum
r' < CARD('b)
canonical_basis = map ket enum_class.enum
r' < length enum_class.enum \<Longrightarrow> map ket enum_class.enum ! r' = ket (enum_class.enum ! r')

goal (1 subgoal):
 1. canonical_basis ! r' = ket (enum_class.enum ! r')
[PROOF STEP]
by smt
[PROOF STATE]
proof (state)
this:
BasisB ! r' = ket (enum_class.enum ! r')

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
have "distinct BasisB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct BasisB
[PROOF STEP]
unfolding BasisB_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct canonical_basis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct BasisB

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct BasisB

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
have "r < length BasisB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r < length BasisB
[PROOF STEP]
using a1 lengthBasisB
[PROOF STATE]
proof (prove)
using this:
r < CARD('b)
CARD('b) = length BasisB

goal (1 subgoal):
 1. r < length BasisB
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r < length BasisB

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r < length BasisB

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
have "r' < length BasisB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r' < length BasisB
[PROOF STEP]
using c3 lengthBasisB
[PROOF STATE]
proof (prove)
using this:
r' < CARD('b)
CARD('b) = length BasisB

goal (1 subgoal):
 1. r' < length BasisB
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r' < length BasisB

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
distinct BasisB
r < length BasisB
r' < length BasisB
[PROOF STEP]
have h1: "BasisB!r \<noteq> BasisB!r'"
[PROOF STATE]
proof (prove)
using this:
distinct BasisB
r < length BasisB
r' < length BasisB

goal (1 subgoal):
 1. BasisB ! r \<noteq> BasisB ! r'
[PROOF STEP]
using nth_eq_iff_index_eq[where xs = BasisB and i = r and j = r'] c2
[PROOF STATE]
proof (prove)
using this:
distinct BasisB
r < length BasisB
r' < length BasisB
\<lbrakk>distinct BasisB; r < length BasisB; r' < length BasisB\<rbrakk> \<Longrightarrow> (BasisB ! r = BasisB ! r') = (r = r')
r \<noteq> r'

goal (1 subgoal):
 1. BasisB ! r \<noteq> BasisB ! r'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
BasisB ! r \<noteq> BasisB ! r'

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
have "(classical_operator f) *\<^sub>V ket (Enum.enum!c)
          = (case f (Enum.enum!c) of None \<Rightarrow> 0 | Some i \<Rightarrow> ket i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. classical_operator f *\<^sub>V ket (enum_class.enum ! c) = (case f (enum_class.enum ! c) of None \<Rightarrow> 0 | Some i \<Rightarrow> ket i)
[PROOF STEP]
using classical_operator_ket_finite
[PROOF STATE]
proof (prove)
using this:
classical_operator ?\<pi> *\<^sub>V ket ?x = (case ?\<pi> ?x of None \<Rightarrow> 0 | Some i \<Rightarrow> ket i)

goal (1 subgoal):
 1. classical_operator f *\<^sub>V ket (enum_class.enum ! c) = (case f (enum_class.enum ! c) of None \<Rightarrow> 0 | Some i \<Rightarrow> ket i)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
classical_operator f *\<^sub>V ket (enum_class.enum ! c) = (case f (enum_class.enum ! c) of None \<Rightarrow> 0 | Some i \<Rightarrow> ket i)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
classical_operator f *\<^sub>V ket (enum_class.enum ! c) = (case f (enum_class.enum ! c) of None \<Rightarrow> 0 | Some i \<Rightarrow> ket i)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
have "\<dots> = ket (Enum.enum!r')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case f (enum_class.enum ! c) of None \<Rightarrow> 0 | Some i \<Rightarrow> ket i) = ket (enum_class.enum ! r')
[PROOF STEP]
using c1
[PROOF STATE]
proof (prove)
using this:
f (enum_class.enum ! c) = Some (enum_class.enum ! r')

goal (1 subgoal):
 1. (case f (enum_class.enum ! c) of None \<Rightarrow> 0 | Some i \<Rightarrow> ket i) = ket (enum_class.enum ! r')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(case f (enum_class.enum ! c) of None \<Rightarrow> 0 | Some i \<Rightarrow> ket i) = ket (enum_class.enum ! r')

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
classical_operator f *\<^sub>V ket (enum_class.enum ! c) = ket (enum_class.enum ! r')
[PROOF STEP]
have "(classical_operator f) *\<^sub>V ket (Enum.enum!c) = ket (Enum.enum!r')"
[PROOF STATE]
proof (prove)
using this:
classical_operator f *\<^sub>V ket (enum_class.enum ! c) = ket (enum_class.enum ! r')

goal (1 subgoal):
 1. classical_operator f *\<^sub>V ket (enum_class.enum ! c) = ket (enum_class.enum ! r')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
classical_operator f *\<^sub>V ket (enum_class.enum ! c) = ket (enum_class.enum ! r')

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
hence *: "(classical_operator f) *\<^sub>V BasisA!c = BasisB!r'"
[PROOF STATE]
proof (prove)
using this:
classical_operator f *\<^sub>V ket (enum_class.enum ! c) = ket (enum_class.enum ! r')

goal (1 subgoal):
 1. classical_operator f *\<^sub>V BasisA ! c = BasisB ! r'
[PROOF STEP]
using x1 x3
[PROOF STATE]
proof (prove)
using this:
classical_operator f *\<^sub>V ket (enum_class.enum ! c) = ket (enum_class.enum ! r')
BasisA ! c = ket (enum_class.enum ! c)
BasisB ! r' = ket (enum_class.enum ! r')

goal (1 subgoal):
 1. classical_operator f *\<^sub>V BasisA ! c = BasisB ! r'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
classical_operator f *\<^sub>V BasisA ! c = BasisB ! r'

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
classical_operator f *\<^sub>V BasisA ! c = BasisB ! r'

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
have "is_orthogonal (BasisB!r) (BasisB!r')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_orthogonal (BasisB ! r) (BasisB ! r')
[PROOF STEP]
using h1
[PROOF STATE]
proof (prove)
using this:
BasisB ! r \<noteq> BasisB ! r'

goal (1 subgoal):
 1. is_orthogonal (BasisB ! r) (BasisB ! r')
[PROOF STEP]
using BasisB_def \<open>r < length BasisB\<close> \<open>r' < length BasisB\<close> is_ortho_set_def is_orthonormal nth_mem
[PROOF STATE]
proof (prove)
using this:
BasisB ! r \<noteq> BasisB ! r'
BasisB = canonical_basis
r < length BasisB
r' < length BasisB
is_ortho_set ?S = ((\<forall>x\<in>?S. \<forall>y\<in>?S. x \<noteq> y \<longrightarrow> is_orthogonal x y) \<and> (0::?'a) \<notin> ?S)
is_ortho_set (set canonical_basis)
?n < length ?xs \<Longrightarrow> ?xs ! ?n \<in> set ?xs

goal (1 subgoal):
 1. is_orthogonal (BasisB ! r) (BasisB ! r')
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
is_orthogonal (BasisB ! r) (BasisB ! r')

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
classical_operator f *\<^sub>V BasisA ! c = BasisB ! r'
is_orthogonal (BasisB ! r) (BasisB ! r')
[PROOF STEP]
have "is_orthogonal (BasisB!r) (classical_operator f *\<^sub>V BasisA!c)"
[PROOF STATE]
proof (prove)
using this:
classical_operator f *\<^sub>V BasisA ! c = BasisB ! r'
is_orthogonal (BasisB ! r) (BasisB ! r')

goal (1 subgoal):
 1. is_orthogonal (BasisB ! r) (classical_operator f *\<^sub>V BasisA ! c)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_orthogonal (BasisB ! r) (classical_operator f *\<^sub>V BasisA ! c)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
is_orthogonal (BasisB ! r) (classical_operator f *\<^sub>V BasisA ! c)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
unfolding mat_of_cblinfun_def BasisA_def BasisB_def
[PROOF STATE]
proof (prove)
using this:
is_orthogonal (canonical_basis ! r) (classical_operator f *\<^sub>V canonical_basis ! c)

goal (1 subgoal):
 1. mat (length canonical_basis) (length canonical_basis) (\<lambda>(i, j). crepresentation (set canonical_basis) (classical_operator f *\<^sub>V canonical_basis ! j) (canonical_basis ! i)) $$ (r, c) = 0
[PROOF STEP]
by (smt (z3) BasisA_def BasisB_def * \<open>r < length BasisB\<close> \<open>r' < length BasisB\<close> a2 canonical_basis_length_ell2 case_prod_conv complex_vector.representation_basis h1 index_mat(1) is_cindependent_set nth_mem)
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (classical_operator f) $$ (r, c) = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>f (enum_class.enum ! c) = Some (enum_class.enum ! ?r'); r \<noteq> ?r'; ?r' < CARD('b)\<rbrakk> \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0) $$ (r, c)
[PROOF STEP]
have "(mat_of_cblinfun (classical_operator f))$$(r,c) = 0"
      if b1: "f (Enum.enum!c) \<noteq> Some (Enum.enum!r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
proof (cases "f (Enum.enum!c) = None")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f (enum_class.enum ! c) = None \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
 2. f (enum_class.enum ! c) \<noteq> None \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
f (enum_class.enum ! c) = None

goal (2 subgoals):
 1. f (enum_class.enum ! c) = None \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
 2. f (enum_class.enum ! c) \<noteq> None \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f (enum_class.enum ! c) = None

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
using v1
[PROOF STATE]
proof (prove)
using this:
f (enum_class.enum ! c) = None
f (enum_class.enum ! c) = None \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (classical_operator f) $$ (r, c) = 0

goal (1 subgoal):
 1. f (enum_class.enum ! c) \<noteq> None \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f (enum_class.enum ! c) \<noteq> None \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
f (enum_class.enum ! c) \<noteq> None

goal (1 subgoal):
 1. f (enum_class.enum ! c) \<noteq> None \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
hence "\<exists>R. f (Enum.enum!c) = Some R"
[PROOF STATE]
proof (prove)
using this:
f (enum_class.enum ! c) \<noteq> None

goal (1 subgoal):
 1. \<exists>R. f (enum_class.enum ! c) = Some R
[PROOF STEP]
apply (induction "f (Enum.enum!c)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>None = f (enum_class.enum ! c); f (enum_class.enum ! c) \<noteq> None\<rbrakk> \<Longrightarrow> \<exists>R. f (enum_class.enum ! c) = Some R
 2. \<And>option. \<lbrakk>Some option = f (enum_class.enum ! c); f (enum_class.enum ! c) \<noteq> None\<rbrakk> \<Longrightarrow> \<exists>R. f (enum_class.enum ! c) = Some R
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>option. \<lbrakk>Some option = f (enum_class.enum ! c); f (enum_class.enum ! c) \<noteq> None\<rbrakk> \<Longrightarrow> \<exists>R. f (enum_class.enum ! c) = Some R
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>R. f (enum_class.enum ! c) = Some R

goal (1 subgoal):
 1. f (enum_class.enum ! c) \<noteq> None \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>R. f (enum_class.enum ! c) = Some R
[PROOF STEP]
obtain R where R0: "f (Enum.enum!c) = Some R"
[PROOF STATE]
proof (prove)
using this:
\<exists>R. f (enum_class.enum ! c) = Some R

goal (1 subgoal):
 1. (\<And>R. f (enum_class.enum ! c) = Some R \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f (enum_class.enum ! c) = Some R

goal (1 subgoal):
 1. f (enum_class.enum ! c) \<noteq> None \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
have "R \<in> set (Enum.enum::'b list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<in> set enum_class.enum
[PROOF STEP]
using UNIV_enum
[PROOF STATE]
proof (prove)
using this:
UNIV = set enum_class.enum

goal (1 subgoal):
 1. R \<in> set enum_class.enum
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
R \<in> set enum_class.enum

goal (1 subgoal):
 1. f (enum_class.enum ! c) \<noteq> None \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
hence "\<exists>r'. R = (Enum.enum::'b list)!r' \<and> r' < length (Enum.enum::'b list)"
[PROOF STATE]
proof (prove)
using this:
R \<in> set enum_class.enum

goal (1 subgoal):
 1. \<exists>r'. R = enum_class.enum ! r' \<and> r' < length enum_class.enum
[PROOF STEP]
by (metis in_set_conv_nth)
[PROOF STATE]
proof (state)
this:
\<exists>r'. R = enum_class.enum ! r' \<and> r' < length enum_class.enum

goal (1 subgoal):
 1. f (enum_class.enum ! c) \<noteq> None \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>r'. R = enum_class.enum ! r' \<and> r' < length enum_class.enum
[PROOF STEP]
obtain r' where u1: "R = (Enum.enum::'b list)!r'"
        and u2: "r' < length (Enum.enum::'b list)"
[PROOF STATE]
proof (prove)
using this:
\<exists>r'. R = enum_class.enum ! r' \<and> r' < length enum_class.enum

goal (1 subgoal):
 1. (\<And>r'. \<lbrakk>R = enum_class.enum ! r'; r' < length enum_class.enum\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
R = enum_class.enum ! r'
r' < length enum_class.enum

goal (1 subgoal):
 1. f (enum_class.enum ! c) \<noteq> None \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
have R1: "f (Enum.enum!c) = Some (Enum.enum!r')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (enum_class.enum ! c) = Some (enum_class.enum ! r')
[PROOF STEP]
using R0 u1
[PROOF STATE]
proof (prove)
using this:
f (enum_class.enum ! c) = Some R
R = enum_class.enum ! r'

goal (1 subgoal):
 1. f (enum_class.enum ! c) = Some (enum_class.enum ! r')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f (enum_class.enum ! c) = Some (enum_class.enum ! r')

goal (1 subgoal):
 1. f (enum_class.enum ! c) \<noteq> None \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
have "Some ((Enum.enum::'b list)!r') \<noteq> Some ((Enum.enum::'b list)!r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some (enum_class.enum ! r') \<noteq> Some (enum_class.enum ! r)
[PROOF STEP]
proof(rule classical)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Some (enum_class.enum ! r') \<noteq> Some (enum_class.enum ! r) \<Longrightarrow> Some (enum_class.enum ! r') \<noteq> Some (enum_class.enum ! r)
[PROOF STEP]
assume "\<not>(Some ((Enum.enum::'b list)!r') \<noteq> Some ((Enum.enum::'b list)!r))"
[PROOF STATE]
proof (state)
this:
\<not> Some (enum_class.enum ! r') \<noteq> Some (enum_class.enum ! r)

goal (1 subgoal):
 1. \<not> Some (enum_class.enum ! r') \<noteq> Some (enum_class.enum ! r) \<Longrightarrow> Some (enum_class.enum ! r') \<noteq> Some (enum_class.enum ! r)
[PROOF STEP]
hence "Some ((Enum.enum::'b list)!r') = Some ((Enum.enum::'b list)!r)"
[PROOF STATE]
proof (prove)
using this:
\<not> Some (enum_class.enum ! r') \<noteq> Some (enum_class.enum ! r)

goal (1 subgoal):
 1. Some (enum_class.enum ! r') = Some (enum_class.enum ! r)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Some (enum_class.enum ! r') = Some (enum_class.enum ! r)

goal (1 subgoal):
 1. \<not> Some (enum_class.enum ! r') \<noteq> Some (enum_class.enum ! r) \<Longrightarrow> Some (enum_class.enum ! r') \<noteq> Some (enum_class.enum ! r)
[PROOF STEP]
hence "f (Enum.enum!c) = Some ((Enum.enum::'b list)!r)"
[PROOF STATE]
proof (prove)
using this:
Some (enum_class.enum ! r') = Some (enum_class.enum ! r)

goal (1 subgoal):
 1. f (enum_class.enum ! c) = Some (enum_class.enum ! r)
[PROOF STEP]
using R1
[PROOF STATE]
proof (prove)
using this:
Some (enum_class.enum ! r') = Some (enum_class.enum ! r)
f (enum_class.enum ! c) = Some (enum_class.enum ! r')

goal (1 subgoal):
 1. f (enum_class.enum ! c) = Some (enum_class.enum ! r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (enum_class.enum ! c) = Some (enum_class.enum ! r)

goal (1 subgoal):
 1. \<not> Some (enum_class.enum ! r') \<noteq> Some (enum_class.enum ! r) \<Longrightarrow> Some (enum_class.enum ! r') \<noteq> Some (enum_class.enum ! r)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f (enum_class.enum ! c) = Some (enum_class.enum ! r)

goal (1 subgoal):
 1. Some (enum_class.enum ! r') \<noteq> Some (enum_class.enum ! r)
[PROOF STEP]
using b1
[PROOF STATE]
proof (prove)
using this:
f (enum_class.enum ! c) = Some (enum_class.enum ! r)
f (enum_class.enum ! c) \<noteq> Some (enum_class.enum ! r)

goal (1 subgoal):
 1. Some (enum_class.enum ! r') \<noteq> Some (enum_class.enum ! r)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Some (enum_class.enum ! r') \<noteq> Some (enum_class.enum ! r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Some (enum_class.enum ! r') \<noteq> Some (enum_class.enum ! r)

goal (1 subgoal):
 1. f (enum_class.enum ! c) \<noteq> None \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
hence "((Enum.enum::'b list)!r') \<noteq> ((Enum.enum::'b list)!r)"
[PROOF STATE]
proof (prove)
using this:
Some (enum_class.enum ! r') \<noteq> Some (enum_class.enum ! r)

goal (1 subgoal):
 1. enum_class.enum ! r' \<noteq> enum_class.enum ! r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
enum_class.enum ! r' \<noteq> enum_class.enum ! r

goal (1 subgoal):
 1. f (enum_class.enum ! c) \<noteq> None \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
hence "r' \<noteq> r"
[PROOF STATE]
proof (prove)
using this:
enum_class.enum ! r' \<noteq> enum_class.enum ! r

goal (1 subgoal):
 1. r' \<noteq> r
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r' \<noteq> r

goal (1 subgoal):
 1. f (enum_class.enum ! c) \<noteq> None \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r' \<noteq> r

goal (1 subgoal):
 1. f (enum_class.enum ! c) \<noteq> None \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
have "r' < CARD('b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r' < CARD('b)
[PROOF STEP]
using u2 cardb
[PROOF STATE]
proof (prove)
using this:
r' < length enum_class.enum
CARD('b) = length enum_class.enum

goal (1 subgoal):
 1. r' < CARD('b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r' < CARD('b)

goal (1 subgoal):
 1. f (enum_class.enum ! c) \<noteq> None \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r' \<noteq> r
r' < CARD('b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r' \<noteq> r
r' < CARD('b)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
using R1 v2[where r' = r']
[PROOF STATE]
proof (prove)
using this:
r' \<noteq> r
r' < CARD('b)
f (enum_class.enum ! c) = Some (enum_class.enum ! r')
\<lbrakk>f (enum_class.enum ! c) = Some (enum_class.enum ! r'); r \<noteq> r'; r' < CARD('b)\<rbrakk> \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (classical_operator f) $$ (r, c) = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f (enum_class.enum ! c) \<noteq> Some (enum_class.enum ! r) \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0) $$ (r, c)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f (enum_class.enum ! c) \<noteq> Some (enum_class.enum ! r) \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0) $$ (r, c)
[PROOF STEP]
have "(mat_of_cblinfun (classical_operator f))$$(r,c) = 1"
      if b1: "f (Enum.enum!c) = Some (Enum.enum!r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 1
[PROOF STEP]
have "CARD('b) = length (enum_class.enum::'b list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD('b) = length enum_class.enum
[PROOF STEP]
using card_UNIV_length_enum[where 'a = 'b]
[PROOF STATE]
proof (prove)
using this:
CARD('b) = length enum_class.enum

goal (1 subgoal):
 1. CARD('b) = length enum_class.enum
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
CARD('b) = length enum_class.enum

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 1
[PROOF STEP]
hence "length (map (ket::'b\<Rightarrow>_) enum_class.enum) = CARD('b)"
[PROOF STATE]
proof (prove)
using this:
CARD('b) = length enum_class.enum

goal (1 subgoal):
 1. length (map ket enum_class.enum) = CARD('b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (map ket enum_class.enum) = CARD('b)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 1
[PROOF STEP]
hence w0: "map (ket::'b\<Rightarrow>_) enum_class.enum ! r = ket (enum_class.enum ! r)"
[PROOF STATE]
proof (prove)
using this:
length (map ket enum_class.enum) = CARD('b)

goal (1 subgoal):
 1. map ket enum_class.enum ! r = ket (enum_class.enum ! r)
[PROOF STEP]
by (simp add: a1)
[PROOF STATE]
proof (state)
this:
map ket enum_class.enum ! r = ket (enum_class.enum ! r)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 1
[PROOF STEP]
have "CARD('a) = length (enum_class.enum::'a list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD('a) = length enum_class.enum
[PROOF STEP]
using card_UNIV_length_enum[where 'a = 'a]
[PROOF STATE]
proof (prove)
using this:
CARD('a) = length enum_class.enum

goal (1 subgoal):
 1. CARD('a) = length enum_class.enum
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
CARD('a) = length enum_class.enum

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 1
[PROOF STEP]
hence "length (map (ket::'a\<Rightarrow>_) enum_class.enum) = CARD('a)"
[PROOF STATE]
proof (prove)
using this:
CARD('a) = length enum_class.enum

goal (1 subgoal):
 1. length (map ket enum_class.enum) = CARD('a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (map ket enum_class.enum) = CARD('a)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 1
[PROOF STEP]
hence "map (ket::'a\<Rightarrow>_) enum_class.enum ! c = ket (enum_class.enum ! c)"
[PROOF STATE]
proof (prove)
using this:
length (map ket enum_class.enum) = CARD('a)

goal (1 subgoal):
 1. map ket enum_class.enum ! c = ket (enum_class.enum ! c)
[PROOF STEP]
by (simp add: a2)
[PROOF STATE]
proof (state)
this:
map ket enum_class.enum ! c = ket (enum_class.enum ! c)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 1
[PROOF STEP]
hence "(classical_operator f) *\<^sub>V (BasisA!c) = (classical_operator f) *\<^sub>V (ket (Enum.enum!c))"
[PROOF STATE]
proof (prove)
using this:
map ket enum_class.enum ! c = ket (enum_class.enum ! c)

goal (1 subgoal):
 1. classical_operator f *\<^sub>V BasisA ! c = classical_operator f *\<^sub>V ket (enum_class.enum ! c)
[PROOF STEP]
unfolding BasisA_def canonical_basis_ell2_def
[PROOF STATE]
proof (prove)
using this:
map ket enum_class.enum ! c = ket (enum_class.enum ! c)

goal (1 subgoal):
 1. classical_operator f *\<^sub>V map ket enum_class.enum ! c = classical_operator f *\<^sub>V ket (enum_class.enum ! c)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
classical_operator f *\<^sub>V BasisA ! c = classical_operator f *\<^sub>V ket (enum_class.enum ! c)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
classical_operator f *\<^sub>V BasisA ! c = classical_operator f *\<^sub>V ket (enum_class.enum ! c)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 1
[PROOF STEP]
have "... = (case f (enum_class.enum ! c) of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. classical_operator f *\<^sub>V ket (enum_class.enum ! c) = (case f (enum_class.enum ! c) of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x)
[PROOF STEP]
by (rule classical_operator_ket_finite)
[PROOF STATE]
proof (state)
this:
classical_operator f *\<^sub>V ket (enum_class.enum ! c) = (case f (enum_class.enum ! c) of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
classical_operator f *\<^sub>V ket (enum_class.enum ! c) = (case f (enum_class.enum ! c) of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 1
[PROOF STEP]
have "\<dots> = BasisB!r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case f (enum_class.enum ! c) of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x) = BasisB ! r
[PROOF STEP]
using w0 b1
[PROOF STATE]
proof (prove)
using this:
map ket enum_class.enum ! r = ket (enum_class.enum ! r)
f (enum_class.enum ! c) = Some (enum_class.enum ! r)

goal (1 subgoal):
 1. (case f (enum_class.enum ! c) of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x) = BasisB ! r
[PROOF STEP]
by (simp add: BasisB_def canonical_basis_ell2_def)
[PROOF STATE]
proof (state)
this:
(case f (enum_class.enum ! c) of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x) = BasisB ! r

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
classical_operator f *\<^sub>V BasisA ! c = BasisB ! r
[PROOF STEP]
have w1: "(classical_operator f) *\<^sub>V (BasisA!c) = BasisB!r"
[PROOF STATE]
proof (prove)
using this:
classical_operator f *\<^sub>V BasisA ! c = BasisB ! r

goal (1 subgoal):
 1. classical_operator f *\<^sub>V BasisA ! c = BasisB ! r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
classical_operator f *\<^sub>V BasisA ! c = BasisB ! r

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 1
[PROOF STEP]
have "(mat_of_cblinfun (classical_operator f))$$(r,c)
        = (BasisB!r) \<bullet>\<^sub>C (classical_operator f *\<^sub>V (BasisA!c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = BasisB ! r \<bullet>\<^sub>C (classical_operator f *\<^sub>V BasisA ! c)
[PROOF STEP]
unfolding BasisB_def BasisA_def mat_of_cblinfun_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (length canonical_basis) (length canonical_basis) (\<lambda>(i, j). crepresentation (set canonical_basis) (classical_operator f *\<^sub>V canonical_basis ! j) (canonical_basis ! i)) $$ (r, c) = canonical_basis ! r \<bullet>\<^sub>C (classical_operator f *\<^sub>V canonical_basis ! c)
[PROOF STEP]
using \<open>nA = CARD('a)\<close> \<open>nB = CARD('b)\<close> a1 a2 nA_def nB_def
[PROOF STATE]
proof (prove)
using this:
nA = CARD('a)
nB = CARD('b)
r < CARD('b)
c < CARD('a)
nA = CARD('a)
nB = CARD('b)

goal (1 subgoal):
 1. mat (length canonical_basis) (length canonical_basis) (\<lambda>(i, j). crepresentation (set canonical_basis) (classical_operator f *\<^sub>V canonical_basis ! j) (canonical_basis ! i)) $$ (r, c) = canonical_basis ! r \<bullet>\<^sub>C (classical_operator f *\<^sub>V canonical_basis ! c)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r < CARD('b); c < CARD('a); nA = CARD('a); nB = CARD('b)\<rbrakk> \<Longrightarrow> crepresentation (set canonical_basis) (classical_operator f *\<^sub>V canonical_basis ! c) (canonical_basis ! r) = canonical_basis ! r \<bullet>\<^sub>C (classical_operator f *\<^sub>V canonical_basis ! c)
[PROOF STEP]
by (metis BasisA_def BasisB_def canonical_basis_length_ell2 cinner_canonical_basis complex_vector.representation_basis is_cindependent_set nth_mem w1)
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (classical_operator f) $$ (r, c) = BasisB ! r \<bullet>\<^sub>C (classical_operator f *\<^sub>V BasisA ! c)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (classical_operator f) $$ (r, c) = BasisB ! r \<bullet>\<^sub>C (classical_operator f *\<^sub>V BasisA ! c)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 1
[PROOF STEP]
have "\<dots> = (BasisB!r) \<bullet>\<^sub>C (BasisB!r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BasisB ! r \<bullet>\<^sub>C (classical_operator f *\<^sub>V BasisA ! c) = BasisB ! r \<bullet>\<^sub>C BasisB ! r
[PROOF STEP]
using w1
[PROOF STATE]
proof (prove)
using this:
classical_operator f *\<^sub>V BasisA ! c = BasisB ! r

goal (1 subgoal):
 1. BasisB ! r \<bullet>\<^sub>C (classical_operator f *\<^sub>V BasisA ! c) = BasisB ! r \<bullet>\<^sub>C BasisB ! r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
BasisB ! r \<bullet>\<^sub>C (classical_operator f *\<^sub>V BasisA ! c) = BasisB ! r \<bullet>\<^sub>C BasisB ! r

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
BasisB ! r \<bullet>\<^sub>C (classical_operator f *\<^sub>V BasisA ! c) = BasisB ! r \<bullet>\<^sub>C BasisB ! r

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 1
[PROOF STEP]
have "\<dots> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BasisB ! r \<bullet>\<^sub>C BasisB ! r = 1
[PROOF STEP]
unfolding BasisB_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. canonical_basis ! r \<bullet>\<^sub>C canonical_basis ! r = 1
[PROOF STEP]
using \<open>nB = CARD('b)\<close> a1 nB_def
[PROOF STATE]
proof (prove)
using this:
nB = CARD('b)
r < CARD('b)
nB = CARD('b)

goal (1 subgoal):
 1. canonical_basis ! r \<bullet>\<^sub>C canonical_basis ! r = 1
[PROOF STEP]
by (simp add: cinner_canonical_basis)
[PROOF STATE]
proof (state)
this:
BasisB ! r \<bullet>\<^sub>C BasisB ! r = 1

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mat_of_cblinfun (classical_operator f) $$ (r, c) = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mat_of_cblinfun (classical_operator f) $$ (r, c) = 1

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = 1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (classical_operator f) $$ (r, c) = 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f (enum_class.enum ! c) = Some (enum_class.enum ! r) \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 1

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0) $$ (r, c)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f (enum_class.enum ! c) \<noteq> Some (enum_class.enum ! r) \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
f (enum_class.enum ! c) = Some (enum_class.enum ! r) \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f (enum_class.enum ! c) \<noteq> Some (enum_class.enum ! r) \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 0
f (enum_class.enum ! c) = Some (enum_class.enum ! r) \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = 1

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) $$ (r, c) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0) $$ (r, c)
[PROOF STEP]
by (simp add: a1 a2)
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (classical_operator f) $$ (r, c) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0) $$ (r, c)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?r < CARD('b); ?c < CARD('a)\<rbrakk> \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (?r, ?c) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0) $$ (?r, ?c)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mat_of_cblinfun (classical_operator f) \<in> carrier_mat CARD('b) CARD('a)
\<lbrakk>?r < CARD('b); ?c < CARD('a)\<rbrakk> \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (?r, ?c) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0) $$ (?r, ?c)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mat_of_cblinfun (classical_operator f) \<in> carrier_mat CARD('b) CARD('a)
\<lbrakk>?r < CARD('b); ?c < CARD('a)\<rbrakk> \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (?r, ?c) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0) $$ (?r, ?c)

goal (1 subgoal):
 1. mat_of_cblinfun (classical_operator f) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0)
[PROOF STEP]
apply (rule_tac eq_matI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>mat_of_cblinfun (classical_operator f) \<in> carrier_mat CARD('b) CARD('a); \<And>r c. \<lbrakk>r < CARD('b); c < CARD('a)\<rbrakk> \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0) $$ (r, c); i < dim_row (mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0)); j < dim_col (mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0))\<rbrakk> \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (i, j) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0) $$ (i, j)
 2. \<lbrakk>mat_of_cblinfun (classical_operator f) \<in> carrier_mat CARD('b) CARD('a); \<And>r c. \<lbrakk>r < CARD('b); c < CARD('a)\<rbrakk> \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0) $$ (r, c)\<rbrakk> \<Longrightarrow> dim_row (mat_of_cblinfun (classical_operator f)) = dim_row (mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0))
 3. \<lbrakk>mat_of_cblinfun (classical_operator f) \<in> carrier_mat CARD('b) CARD('a); \<And>r c. \<lbrakk>r < CARD('b); c < CARD('a)\<rbrakk> \<Longrightarrow> mat_of_cblinfun (classical_operator f) $$ (r, c) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0) $$ (r, c)\<rbrakk> \<Longrightarrow> dim_col (mat_of_cblinfun (classical_operator f)) = dim_col (mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (classical_operator f) = mat CARD('b) CARD('a) (\<lambda>(r, c). if f (enum_class.enum ! c) = Some (enum_class.enum ! r) then 1 else 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mat_of_cblinfun_compose:
  "mat_of_cblinfun (F o\<^sub>C\<^sub>L G) = mat_of_cblinfun F * mat_of_cblinfun G"
  for F::"'b::{basis_enum,complex_normed_vector} \<Rightarrow>\<^sub>C\<^sub>L 'c::{basis_enum,complex_normed_vector}"
    and G::"'a::{basis_enum,complex_normed_vector}  \<Rightarrow>\<^sub>C\<^sub>L 'b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (F o\<^sub>C\<^sub>L G) = mat_of_cblinfun F * mat_of_cblinfun G
[PROOF STEP]
by (smt (verit, del_insts) cblinfun_of_mat_inverse mat_carrier mat_of_cblinfun_def mat_of_cblinfun_inverse cblinfun_of_mat_times mult_carrier_mat)


[STATEMENT]
lemma mat_of_cblinfun_scaleC:
  "mat_of_cblinfun ((a::complex) *\<^sub>C F) = a \<cdot>\<^sub>m (mat_of_cblinfun F)"
  for F :: "'a::{basis_enum,complex_normed_vector} \<Rightarrow>\<^sub>C\<^sub>L 'b::{basis_enum,complex_normed_vector}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (a *\<^sub>C F) = a \<cdot>\<^sub>m mat_of_cblinfun F
[PROOF STEP]
by (auto simp add: complex_vector.representation_scale mat_of_cblinfun_def)


[STATEMENT]
lemma mat_of_cblinfun_scaleR:
  "mat_of_cblinfun ((a::real) *\<^sub>R F) = (complex_of_real a) \<cdot>\<^sub>m (mat_of_cblinfun F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (a *\<^sub>R F) = complex_of_real a \<cdot>\<^sub>m mat_of_cblinfun F
[PROOF STEP]
unfolding scaleR_scaleC
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (complex_of_real a *\<^sub>C F) = complex_of_real a \<cdot>\<^sub>m mat_of_cblinfun F
[PROOF STEP]
by (rule mat_of_cblinfun_scaleC)


[STATEMENT]
lemma mat_of_cblinfun_adj:
  "mat_of_cblinfun (F*) = mat_adjoint (mat_of_cblinfun F)"
  for F :: "'a::onb_enum \<Rightarrow>\<^sub>C\<^sub>L 'b::onb_enum"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (F*) = mat_adjoint (mat_of_cblinfun F)
[PROOF STEP]
by (metis (no_types, lifting) cblinfun_of_mat_inverse map_carrier_mat mat_adjoint_def' mat_carrier cblinfun_of_mat_adjoint mat_of_cblinfun_def mat_of_cblinfun_inverse transpose_carrier_mat)


[STATEMENT]
lemma mat_of_cblinfun_vector_to_cblinfun:
  "mat_of_cblinfun (vector_to_cblinfun \<psi>)
       = mat_of_cols (length (canonical_basis :: 'a list)) [vec_of_basis_enum \<psi>]"
  for \<psi>::"'a::{basis_enum,complex_normed_vector}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (vector_to_cblinfun \<psi>) = mat_of_cols (length canonical_basis) [vec_of_basis_enum \<psi>]
[PROOF STEP]
by (auto simp: mat_of_cols_Cons_index_0 mat_of_cblinfun_def vec_of_basis_enum_def vec_of_list_index)


[STATEMENT]
lemma mat_of_cblinfun_proj:
  fixes a::"'a::onb_enum"
  defines   "d \<equiv> length (canonical_basis :: 'a list)"
    and "norm2 \<equiv> (vec_of_basis_enum a) \<bullet>c (vec_of_basis_enum a)"
  shows  "mat_of_cblinfun (proj a) =
      1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a]
                 * mat_of_rows d [conjugate (vec_of_basis_enum a)])" (is \<open>_ = ?rhs\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
[PROOF STEP]
proof (cases "a = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
 2. a \<noteq> (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<noteq> (0::'a)

goal (2 subgoals):
 1. a = (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
 2. a \<noteq> (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
[PROOF STEP]
have norm2: \<open>norm2 = (norm a)\<^sup>2\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm2 = complex_of_real ((norm a)\<^sup>2)
[PROOF STEP]
by (simp add: cscalar_prod_vec_of_basis_enum norm2_def cdot_square_norm[symmetric, simplified])
[PROOF STATE]
proof (state)
this:
norm2 = complex_of_real ((norm a)\<^sup>2)

goal (2 subgoals):
 1. a = (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
 2. a \<noteq> (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
[PROOF STEP]
have [simp]: \<open>vec_of_basis_enum a \<in> carrier_vec d\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum a \<in> carrier_vec d
[PROOF STEP]
by (simp add: carrier_vecI d_def)
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum a \<in> carrier_vec d

goal (2 subgoals):
 1. a = (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
 2. a \<noteq> (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
[PROOF STEP]
have \<open>mat_of_cblinfun (proj a) = mat_of_cblinfun (proj (a /\<^sub>R norm a))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (proj a) = mat_of_cblinfun (proj (a /\<^sub>R norm a))
[PROOF STEP]
by (metis (mono_tags, opaque_lifting) ccspan_singleton_scaleC complex_vector.scale_eq_0_iff
        nonzero_imp_inverse_nonzero norm_eq_zero scaleR_scaleC scale_left_imp_eq)
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (proj a) = mat_of_cblinfun (proj (a /\<^sub>R norm a))

goal (2 subgoals):
 1. a = (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
 2. a \<noteq> (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (proj a) = mat_of_cblinfun (proj (a /\<^sub>R norm a))

goal (2 subgoals):
 1. a = (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
 2. a \<noteq> (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
[PROOF STEP]
have \<open>\<dots> = mat_of_cblinfun (selfbutter (a /\<^sub>R norm a))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (proj (a /\<^sub>R norm a)) = mat_of_cblinfun (selfbutter (a /\<^sub>R norm a))
[PROOF STEP]
apply (subst butterfly_eq_proj)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. norm (a /\<^sub>R norm a) = 1
 2. mat_of_cblinfun (proj (a /\<^sub>R norm a)) = mat_of_cblinfun (proj (a /\<^sub>R norm a))
[PROOF STEP]
by (auto simp add: False)
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (proj (a /\<^sub>R norm a)) = mat_of_cblinfun (selfbutter (a /\<^sub>R norm a))

goal (2 subgoals):
 1. a = (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
 2. a \<noteq> (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (proj (a /\<^sub>R norm a)) = mat_of_cblinfun (selfbutter (a /\<^sub>R norm a))

goal (2 subgoals):
 1. a = (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
 2. a \<noteq> (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
[PROOF STEP]
have \<open>\<dots> = 1/norm2 \<cdot>\<^sub>m mat_of_cblinfun (selfbutter a)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (selfbutter (a /\<^sub>R norm a)) = 1 / norm2 \<cdot>\<^sub>m mat_of_cblinfun (selfbutter a)
[PROOF STEP]
apply (simp add: mat_of_cblinfun_scaleC norm2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (complex_of_real (norm a)) * inverse (complex_of_real (norm a)) \<cdot>\<^sub>m mat_of_cblinfun (selfbutter a) = 1 / (complex_of_real (norm a))\<^sup>2 \<cdot>\<^sub>m mat_of_cblinfun (selfbutter a)
[PROOF STEP]
by (simp add: inverse_eq_divide power2_eq_square)
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (selfbutter (a /\<^sub>R norm a)) = 1 / norm2 \<cdot>\<^sub>m mat_of_cblinfun (selfbutter a)

goal (2 subgoals):
 1. a = (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
 2. a \<noteq> (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (selfbutter (a /\<^sub>R norm a)) = 1 / norm2 \<cdot>\<^sub>m mat_of_cblinfun (selfbutter a)

goal (2 subgoals):
 1. a = (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
 2. a \<noteq> (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
[PROOF STEP]
have \<open>\<dots> = 1 / norm2 \<cdot>\<^sub>m (mat_of_cblinfun (vector_to_cblinfun a :: complex \<Rightarrow>\<^sub>C\<^sub>L 'a) * mat_adjoint (mat_of_cblinfun (vector_to_cblinfun a :: complex \<Rightarrow>\<^sub>C\<^sub>L 'a)))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / norm2 \<cdot>\<^sub>m mat_of_cblinfun (selfbutter a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cblinfun (vector_to_cblinfun a) * mat_adjoint (mat_of_cblinfun (vector_to_cblinfun a)))
[PROOF STEP]
by (simp add: butterfly_def mat_of_cblinfun_compose mat_of_cblinfun_adj)
[PROOF STATE]
proof (state)
this:
1 / norm2 \<cdot>\<^sub>m mat_of_cblinfun (selfbutter a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cblinfun (vector_to_cblinfun a) * mat_adjoint (mat_of_cblinfun (vector_to_cblinfun a)))

goal (2 subgoals):
 1. a = (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
 2. a \<noteq> (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 / norm2 \<cdot>\<^sub>m mat_of_cblinfun (selfbutter a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cblinfun (vector_to_cblinfun a) * mat_adjoint (mat_of_cblinfun (vector_to_cblinfun a)))

goal (2 subgoals):
 1. a = (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
 2. a \<noteq> (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
[PROOF STEP]
have \<open>\<dots> = ?rhs\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / norm2 \<cdot>\<^sub>m (mat_of_cblinfun (vector_to_cblinfun a) * mat_adjoint (mat_of_cblinfun (vector_to_cblinfun a))) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
[PROOF STEP]
by (simp add: mat_of_cblinfun_vector_to_cblinfun mat_adjoint_def flip: d_def)
[PROOF STATE]
proof (state)
this:
1 / norm2 \<cdot>\<^sub>m (mat_of_cblinfun (vector_to_cblinfun a) * mat_adjoint (mat_of_cblinfun (vector_to_cblinfun a))) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])

goal (2 subgoals):
 1. a = (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
 2. a \<noteq> (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])

goal (1 subgoal):
 1. mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])

goal (1 subgoal):
 1. a = (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a = (0::'a)

goal (1 subgoal):
 1. a = (0::'a) \<Longrightarrow> mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])
[PROOF STEP]
apply (rule eq_matI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])); j < dim_col (1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)]))\<rbrakk> \<Longrightarrow> mat_of_cblinfun (proj a) $$ (i, j) = (1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])) $$ (i, j)
 2. dim_row (mat_of_cblinfun (proj a)) = dim_row (1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)]))
 3. dim_col (mat_of_cblinfun (proj a)) = dim_col (1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)]))
[PROOF STEP]
by (auto simp: True mat_of_cblinfun_zero vec_of_basis_enum_zero scalar_prod_def  mat_of_rows_index
        simp flip: d_def)
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (proj a) = 1 / norm2 \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)])

goal:
No subgoals!
[PROOF STEP]
qed