[STATEMENT]
lemma mat_of_cblinfun_ell2_component:
  fixes a :: \<open>'a::enum ell2 \<Rightarrow>\<^sub>C\<^sub>L 'b::enum ell2\<close>
  assumes [simp]: \<open>i < CARD('b)\<close> \<open>j < CARD('a)\<close>
  shows \<open>mat_of_cblinfun a $$ (i,j) = Rep_ell2 (a *\<^sub>V ket (Enum.enum ! j)) (Enum.enum ! i)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun a $$ (i, j) = Rep_ell2 (a *\<^sub>V ket (enum_class.enum ! j)) (enum_class.enum ! i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat_of_cblinfun a $$ (i, j) = Rep_ell2 (a *\<^sub>V ket (enum_class.enum ! j)) (enum_class.enum ! i)
[PROOF STEP]
let ?i = \<open>Enum.enum ! i\<close> and ?j = \<open>Enum.enum ! j\<close> and ?aj = \<open>a *\<^sub>V ket (Enum.enum ! j)\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat_of_cblinfun a $$ (i, j) = Rep_ell2 (a *\<^sub>V ket (enum_class.enum ! j)) (enum_class.enum ! i)
[PROOF STEP]
have \<open>Rep_ell2 ?aj (Enum.enum ! i) = vec_of_basis_enum ?aj $ i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_ell2 (a *\<^sub>V ket (enum_class.enum ! j)) (enum_class.enum ! i) = vec_of_basis_enum (a *\<^sub>V ket (enum_class.enum ! j)) $ i
[PROOF STEP]
by (rule vec_of_basis_enum_ell2_component[symmetric], simp)
[PROOF STATE]
proof (state)
this:
Rep_ell2 (a *\<^sub>V ket (enum_class.enum ! j)) (enum_class.enum ! i) = vec_of_basis_enum (a *\<^sub>V ket (enum_class.enum ! j)) $ i

goal (1 subgoal):
 1. mat_of_cblinfun a $$ (i, j) = Rep_ell2 (a *\<^sub>V ket (enum_class.enum ! j)) (enum_class.enum ! i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Rep_ell2 (a *\<^sub>V ket (enum_class.enum ! j)) (enum_class.enum ! i) = vec_of_basis_enum (a *\<^sub>V ket (enum_class.enum ! j)) $ i

goal (1 subgoal):
 1. mat_of_cblinfun a $$ (i, j) = Rep_ell2 (a *\<^sub>V ket (enum_class.enum ! j)) (enum_class.enum ! i)
[PROOF STEP]
have \<open>\<dots> = (mat_of_cblinfun a *\<^sub>v vec_of_basis_enum (ket (enum_class.enum ! j) :: 'a ell2)) $ i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (a *\<^sub>V ket (enum_class.enum ! j)) $ i = (mat_of_cblinfun a *\<^sub>v vec_of_basis_enum (ket (enum_class.enum ! j))) $ i
[PROOF STEP]
by (simp add: mat_of_cblinfun_cblinfun_apply)
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (a *\<^sub>V ket (enum_class.enum ! j)) $ i = (mat_of_cblinfun a *\<^sub>v vec_of_basis_enum (ket (enum_class.enum ! j))) $ i

goal (1 subgoal):
 1. mat_of_cblinfun a $$ (i, j) = Rep_ell2 (a *\<^sub>V ket (enum_class.enum ! j)) (enum_class.enum ! i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (a *\<^sub>V ket (enum_class.enum ! j)) $ i = (mat_of_cblinfun a *\<^sub>v vec_of_basis_enum (ket (enum_class.enum ! j))) $ i

goal (1 subgoal):
 1. mat_of_cblinfun a $$ (i, j) = Rep_ell2 (a *\<^sub>V ket (enum_class.enum ! j)) (enum_class.enum ! i)
[PROOF STEP]
have \<open>\<dots> = (mat_of_cblinfun a *\<^sub>v unit_vec CARD('a) j) $ i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mat_of_cblinfun a *\<^sub>v vec_of_basis_enum (ket (enum_class.enum ! j))) $ i = (mat_of_cblinfun a *\<^sub>v unit_vec CARD('a) j) $ i
[PROOF STEP]
by (simp add: vec_of_basis_enum_ket enum_idx_enum)
[PROOF STATE]
proof (state)
this:
(mat_of_cblinfun a *\<^sub>v vec_of_basis_enum (ket (enum_class.enum ! j))) $ i = (mat_of_cblinfun a *\<^sub>v unit_vec CARD('a) j) $ i

goal (1 subgoal):
 1. mat_of_cblinfun a $$ (i, j) = Rep_ell2 (a *\<^sub>V ket (enum_class.enum ! j)) (enum_class.enum ! i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(mat_of_cblinfun a *\<^sub>v vec_of_basis_enum (ket (enum_class.enum ! j))) $ i = (mat_of_cblinfun a *\<^sub>v unit_vec CARD('a) j) $ i

goal (1 subgoal):
 1. mat_of_cblinfun a $$ (i, j) = Rep_ell2 (a *\<^sub>V ket (enum_class.enum ! j)) (enum_class.enum ! i)
[PROOF STEP]
have \<open>\<dots> = mat_of_cblinfun a $$ (i, j)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mat_of_cblinfun a *\<^sub>v unit_vec CARD('a) j) $ i = mat_of_cblinfun a $$ (i, j)
[PROOF STEP]
apply (subst mat_entry_explicit[where m=\<open>CARD('b)\<close>])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. mat_of_cblinfun a \<in> carrier_mat CARD('b) CARD('a)
 2. i < CARD('b)
 3. j < CARD('a)
 4. mat_of_cblinfun a $$ (i, j) = mat_of_cblinfun a $$ (i, j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(mat_of_cblinfun a *\<^sub>v unit_vec CARD('a) j) $ i = mat_of_cblinfun a $$ (i, j)

goal (1 subgoal):
 1. mat_of_cblinfun a $$ (i, j) = Rep_ell2 (a *\<^sub>V ket (enum_class.enum ! j)) (enum_class.enum ! i)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Rep_ell2 (a *\<^sub>V ket (enum_class.enum ! j)) (enum_class.enum ! i) = mat_of_cblinfun a $$ (i, j)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Rep_ell2 (a *\<^sub>V ket (enum_class.enum ! j)) (enum_class.enum ! i) = mat_of_cblinfun a $$ (i, j)

goal (1 subgoal):
 1. mat_of_cblinfun a $$ (i, j) = Rep_ell2 (a *\<^sub>V ket (enum_class.enum ! j)) (enum_class.enum ! i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun a $$ (i, j) = Rep_ell2 (a *\<^sub>V ket (enum_class.enum ! j)) (enum_class.enum ! i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mat_of_cblinfun_sandwich:
  fixes a :: "(_::onb_enum, _::onb_enum) cblinfun"
  shows \<open>mat_of_cblinfun (sandwich a *\<^sub>V b) = (let a' = mat_of_cblinfun a in a' * mat_of_cblinfun b * mat_adjoint a')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (sandwich a *\<^sub>V b) = (let a' = mat_of_cblinfun a in a' * mat_of_cblinfun b * mat_adjoint a')
[PROOF STEP]
by (simp add: mat_of_cblinfun_compose sandwich_apply Let_def mat_of_cblinfun_adj)


[STATEMENT]
lemma ccspan_gram_schmidt0_invariant:
  defines "basis_enum \<equiv> (basis_enum_of_vec :: _ \<Rightarrow> 'a::{basis_enum,complex_normed_vector})"
  defines "n \<equiv> length (canonical_basis :: 'a list)"
  assumes "set ws \<subseteq> carrier_vec n"
  shows "ccspan (set (map basis_enum (gram_schmidt0 n ws))) = ccspan (set (map basis_enum ws))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccspan (set (map basis_enum (gram_schmidt0 n ws))) = ccspan (set (map basis_enum ws))
[PROOF STEP]
proof (transfer fixing: n ws basis_enum)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. closure (cspan (set (map basis_enum (gram_schmidt0 n ws)))) = closure (cspan (set (map basis_enum ws)))
[PROOF STEP]
interpret complex_vec_space
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. closure (cspan (set (map basis_enum (gram_schmidt0 n ws)))) = closure (cspan (set (map basis_enum ws)))
[PROOF STEP]
define gs where "gs = gram_schmidt0 n ws"
[PROOF STATE]
proof (state)
this:
gs = gram_schmidt0 n ws

goal (1 subgoal):
 1. closure (cspan (set (map basis_enum (gram_schmidt0 n ws)))) = closure (cspan (set (map basis_enum ws)))
[PROOF STEP]
have "closure (cspan (set (map basis_enum gs)))
     = cspan (set (map basis_enum gs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure (cspan (set (map basis_enum gs))) = cspan (set (map basis_enum gs))
[PROOF STEP]
apply (rule closure_finite_cspan)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set (map basis_enum gs))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
closure (cspan (set (map basis_enum gs))) = cspan (set (map basis_enum gs))

goal (1 subgoal):
 1. closure (cspan (set (map basis_enum (gram_schmidt0 n ws)))) = closure (cspan (set (map basis_enum ws)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
closure (cspan (set (map basis_enum gs))) = cspan (set (map basis_enum gs))

goal (1 subgoal):
 1. closure (cspan (set (map basis_enum (gram_schmidt0 n ws)))) = closure (cspan (set (map basis_enum ws)))
[PROOF STEP]
have "\<dots> = cspan (basis_enum ` set gs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cspan (set (map basis_enum gs)) = cspan (basis_enum ` set gs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cspan (set (map basis_enum gs)) = cspan (basis_enum ` set gs)

goal (1 subgoal):
 1. closure (cspan (set (map basis_enum (gram_schmidt0 n ws)))) = closure (cspan (set (map basis_enum ws)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cspan (set (map basis_enum gs)) = cspan (basis_enum ` set gs)

goal (1 subgoal):
 1. closure (cspan (set (map basis_enum (gram_schmidt0 n ws)))) = closure (cspan (set (map basis_enum ws)))
[PROOF STEP]
have "\<dots> = basis_enum ` span (set gs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cspan (basis_enum ` set gs) = basis_enum ` local.span (set gs)
[PROOF STEP]
unfolding basis_enum_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cspan (basis_enum_of_vec ` set gs) = basis_enum_of_vec ` local.span (set gs)
[PROOF STEP]
apply (rule basis_enum_of_vec_span[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length canonical_basis = n
 2. set gs \<subseteq> carrier_vec n
[PROOF STEP]
using n_def
[PROOF STATE]
proof (prove)
using this:
n \<equiv> length canonical_basis

goal (2 subgoals):
 1. length canonical_basis = n
 2. set gs \<subseteq> carrier_vec n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set gs \<subseteq> carrier_vec n
[PROOF STEP]
by (simp add: assms(3) cof_vec_space.gram_schmidt0_result(1) gs_def)
[PROOF STATE]
proof (state)
this:
cspan (basis_enum ` set gs) = basis_enum ` local.span (set gs)

goal (1 subgoal):
 1. closure (cspan (set (map basis_enum (gram_schmidt0 n ws)))) = closure (cspan (set (map basis_enum ws)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cspan (basis_enum ` set gs) = basis_enum ` local.span (set gs)

goal (1 subgoal):
 1. closure (cspan (set (map basis_enum (gram_schmidt0 n ws)))) = closure (cspan (set (map basis_enum ws)))
[PROOF STEP]
have "\<dots> = basis_enum ` span (set ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_enum ` local.span (set gs) = basis_enum ` local.span (set ws)
[PROOF STEP]
unfolding gs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_enum ` local.span (set (gram_schmidt0 n ws)) = basis_enum ` local.span (set ws)
[PROOF STEP]
apply (subst gram_schmidt0_result(4)[where ws=ws, symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. set ws \<subseteq> carrier_vec n
 2. basis_enum ` local.span (set ws) = basis_enum ` local.span (set ws)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
basis_enum \<equiv> basis_enum_of_vec
n \<equiv> length canonical_basis
set ws \<subseteq> carrier_vec n

goal (2 subgoals):
 1. set ws \<subseteq> carrier_vec n
 2. basis_enum ` local.span (set ws) = basis_enum ` local.span (set ws)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
basis_enum ` local.span (set gs) = basis_enum ` local.span (set ws)

goal (1 subgoal):
 1. closure (cspan (set (map basis_enum (gram_schmidt0 n ws)))) = closure (cspan (set (map basis_enum ws)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
basis_enum ` local.span (set gs) = basis_enum ` local.span (set ws)

goal (1 subgoal):
 1. closure (cspan (set (map basis_enum (gram_schmidt0 n ws)))) = closure (cspan (set (map basis_enum ws)))
[PROOF STEP]
have "\<dots> = cspan (basis_enum ` set ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_enum ` local.span (set ws) = cspan (basis_enum ` set ws)
[PROOF STEP]
unfolding basis_enum_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_enum_of_vec ` local.span (set ws) = cspan (basis_enum_of_vec ` set ws)
[PROOF STEP]
apply (rule basis_enum_of_vec_span)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length canonical_basis = n
 2. set ws \<subseteq> carrier_vec n
[PROOF STEP]
using n_def
[PROOF STATE]
proof (prove)
using this:
n \<equiv> length canonical_basis

goal (2 subgoals):
 1. length canonical_basis = n
 2. set ws \<subseteq> carrier_vec n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set ws \<subseteq> carrier_vec n
[PROOF STEP]
by (simp add: assms(3))
[PROOF STATE]
proof (state)
this:
basis_enum ` local.span (set ws) = cspan (basis_enum ` set ws)

goal (1 subgoal):
 1. closure (cspan (set (map basis_enum (gram_schmidt0 n ws)))) = closure (cspan (set (map basis_enum ws)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
basis_enum ` local.span (set ws) = cspan (basis_enum ` set ws)

goal (1 subgoal):
 1. closure (cspan (set (map basis_enum (gram_schmidt0 n ws)))) = closure (cspan (set (map basis_enum ws)))
[PROOF STEP]
have "\<dots> = cspan (set (map basis_enum ws))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cspan (basis_enum ` set ws) = cspan (set (map basis_enum ws))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cspan (basis_enum ` set ws) = cspan (set (map basis_enum ws))

goal (1 subgoal):
 1. closure (cspan (set (map basis_enum (gram_schmidt0 n ws)))) = closure (cspan (set (map basis_enum ws)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cspan (basis_enum ` set ws) = cspan (set (map basis_enum ws))

goal (1 subgoal):
 1. closure (cspan (set (map basis_enum (gram_schmidt0 n ws)))) = closure (cspan (set (map basis_enum ws)))
[PROOF STEP]
have "\<dots> = closure (cspan (set (map basis_enum ws)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cspan (set (map basis_enum ws)) = closure (cspan (set (map basis_enum ws)))
[PROOF STEP]
apply (rule closure_finite_cspan[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set (map basis_enum ws))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cspan (set (map basis_enum ws)) = closure (cspan (set (map basis_enum ws)))

goal (1 subgoal):
 1. closure (cspan (set (map basis_enum (gram_schmidt0 n ws)))) = closure (cspan (set (map basis_enum ws)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
closure (cspan (set (map basis_enum gs))) = closure (cspan (set (map basis_enum ws)))
[PROOF STEP]
show "closure (cspan (set (map basis_enum gs)))
              = closure (cspan (set (map basis_enum ws)))"
[PROOF STATE]
proof (prove)
using this:
closure (cspan (set (map basis_enum gs))) = closure (cspan (set (map basis_enum ws)))

goal (1 subgoal):
 1. closure (cspan (set (map basis_enum gs))) = closure (cspan (set (map basis_enum ws)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
closure (cspan (set (map basis_enum gs))) = closure (cspan (set (map basis_enum ws)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ccspan_leq_using_vec:
  fixes A B :: "'a::{basis_enum,complex_normed_vector} list"
  shows "(ccspan (set A) \<le> ccspan (set B)) \<longleftrightarrow>
    is_subspace_of_vec_list (length (canonical_basis :: 'a list))
      (map vec_of_basis_enum A) (map vec_of_basis_enum B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ccspan (set A) \<le> ccspan (set B)) = is_subspace_of_vec_list (length canonical_basis) (map vec_of_basis_enum A) (map vec_of_basis_enum B)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (ccspan (set A) \<le> ccspan (set B)) = is_subspace_of_vec_list (length canonical_basis) (map vec_of_basis_enum A) (map vec_of_basis_enum B)
[PROOF STEP]
define d Av Bv Bo
    where "d = length (canonical_basis :: 'a list)"
      and "Av = map vec_of_basis_enum A"
      and "Bv = map vec_of_basis_enum B"
      and "Bo = gram_schmidt0 d Bv"
[PROOF STATE]
proof (state)
this:
d = length canonical_basis
Av = map vec_of_basis_enum A
Bv = map vec_of_basis_enum B
Bo = gram_schmidt0 d Bv

goal (1 subgoal):
 1. (ccspan (set A) \<le> ccspan (set B)) = is_subspace_of_vec_list (length canonical_basis) (map vec_of_basis_enum A) (map vec_of_basis_enum B)
[PROOF STEP]
interpret complex_vec_space d
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (ccspan (set A) \<le> ccspan (set B)) = is_subspace_of_vec_list (length canonical_basis) (map vec_of_basis_enum A) (map vec_of_basis_enum B)
[PROOF STEP]
have Av_carrier: "set Av \<subseteq> carrier_vec d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set Av \<subseteq> carrier_vec d
[PROOF STEP]
unfolding Av_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map vec_of_basis_enum A) \<subseteq> carrier_vec d
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> set A \<Longrightarrow> vec_of_basis_enum xa \<in> carrier_vec d
[PROOF STEP]
by (simp add: carrier_vecI d_def dim_vec_of_basis_enum')
[PROOF STATE]
proof (state)
this:
set Av \<subseteq> carrier_vec d

goal (1 subgoal):
 1. (ccspan (set A) \<le> ccspan (set B)) = is_subspace_of_vec_list (length canonical_basis) (map vec_of_basis_enum A) (map vec_of_basis_enum B)
[PROOF STEP]
have Bv_carrier: "set Bv \<subseteq> carrier_vec d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set Bv \<subseteq> carrier_vec d
[PROOF STEP]
unfolding Bv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map vec_of_basis_enum B) \<subseteq> carrier_vec d
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> set B \<Longrightarrow> vec_of_basis_enum xa \<in> carrier_vec d
[PROOF STEP]
by (simp add: carrier_vecI d_def dim_vec_of_basis_enum')
[PROOF STATE]
proof (state)
this:
set Bv \<subseteq> carrier_vec d

goal (1 subgoal):
 1. (ccspan (set A) \<le> ccspan (set B)) = is_subspace_of_vec_list (length canonical_basis) (map vec_of_basis_enum A) (map vec_of_basis_enum B)
[PROOF STEP]
have Bo_carrier: "set Bo \<subseteq> carrier_vec d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set Bo \<subseteq> carrier_vec d
[PROOF STEP]
apply (simp add: Bo_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (gram_schmidt0 d Bv) \<subseteq> carrier_vec d
[PROOF STEP]
using Bv_carrier
[PROOF STATE]
proof (prove)
using this:
set Bv \<subseteq> carrier_vec d

goal (1 subgoal):
 1. set (gram_schmidt0 d Bv) \<subseteq> carrier_vec d
[PROOF STEP]
by (rule gram_schmidt0_result(1))
[PROOF STATE]
proof (state)
this:
set Bo \<subseteq> carrier_vec d

goal (1 subgoal):
 1. (ccspan (set A) \<le> ccspan (set B)) = is_subspace_of_vec_list (length canonical_basis) (map vec_of_basis_enum A) (map vec_of_basis_enum B)
[PROOF STEP]
have orth_Bo: "corthogonal Bo"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. corthogonal Bo
[PROOF STEP]
apply (simp add: Bo_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. corthogonal (gram_schmidt0 d Bv)
[PROOF STEP]
using Bv_carrier
[PROOF STATE]
proof (prove)
using this:
set Bv \<subseteq> carrier_vec d

goal (1 subgoal):
 1. corthogonal (gram_schmidt0 d Bv)
[PROOF STEP]
by (rule gram_schmidt0_result(3))
[PROOF STATE]
proof (state)
this:
corthogonal Bo

goal (1 subgoal):
 1. (ccspan (set A) \<le> ccspan (set B)) = is_subspace_of_vec_list (length canonical_basis) (map vec_of_basis_enum A) (map vec_of_basis_enum B)
[PROOF STEP]
have distinct_Bo: "distinct Bo"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct Bo
[PROOF STEP]
apply (simp add: Bo_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (gram_schmidt0 d Bv)
[PROOF STEP]
using Bv_carrier
[PROOF STATE]
proof (prove)
using this:
set Bv \<subseteq> carrier_vec d

goal (1 subgoal):
 1. distinct (gram_schmidt0 d Bv)
[PROOF STEP]
by (rule gram_schmidt0_result(2))
[PROOF STATE]
proof (state)
this:
distinct Bo

goal (1 subgoal):
 1. (ccspan (set A) \<le> ccspan (set B)) = is_subspace_of_vec_list (length canonical_basis) (map vec_of_basis_enum A) (map vec_of_basis_enum B)
[PROOF STEP]
have "ccspan (set A) \<le> ccspan (set B) \<longleftrightarrow> cspan (set A) \<subseteq> cspan (set B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ccspan (set A) \<le> ccspan (set B)) = (cspan (set A) \<subseteq> cspan (set B))
[PROOF STEP]
apply (transfer fixing: A B)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (closure (cspan (set A)) \<subseteq> closure (cspan (set B))) = (cspan (set A) \<subseteq> cspan (set B))
[PROOF STEP]
apply (subst closure_finite_cspan, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cspan (set A) \<subseteq> closure (cspan (set B))) = (cspan (set A) \<subseteq> cspan (set B))
[PROOF STEP]
by (subst closure_finite_cspan, simp_all)
[PROOF STATE]
proof (state)
this:
(ccspan (set A) \<le> ccspan (set B)) = (cspan (set A) \<subseteq> cspan (set B))

goal (1 subgoal):
 1. (ccspan (set A) \<le> ccspan (set B)) = is_subspace_of_vec_list (length canonical_basis) (map vec_of_basis_enum A) (map vec_of_basis_enum B)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(ccspan (set A) \<le> ccspan (set B)) = (cspan (set A) \<subseteq> cspan (set B))

goal (1 subgoal):
 1. (ccspan (set A) \<le> ccspan (set B)) = is_subspace_of_vec_list (length canonical_basis) (map vec_of_basis_enum A) (map vec_of_basis_enum B)
[PROOF STEP]
have "\<dots> \<longleftrightarrow> span (set Av) \<subseteq> span (set Bv)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cspan (set A) \<subseteq> cspan (set B)) = (local.span (set Av) \<subseteq> local.span (set Bv))
[PROOF STEP]
apply (simp add: Av_def Bv_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cspan (set A) \<subseteq> cspan (set B)) = (local.span (vec_of_basis_enum ` set A) \<subseteq> local.span (vec_of_basis_enum ` set B))
[PROOF STEP]
apply (subst vec_of_basis_enum_cspan[symmetric], simp add: d_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cspan (set A) \<subseteq> cspan (set B)) = (vec_of_basis_enum ` cspan (set A) \<subseteq> local.span (vec_of_basis_enum ` set B))
[PROOF STEP]
apply (subst vec_of_basis_enum_cspan[symmetric], simp add: d_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cspan (set A) \<subseteq> cspan (set B)) = (vec_of_basis_enum ` cspan (set A) \<subseteq> vec_of_basis_enum ` cspan (set B))
[PROOF STEP]
by (metis inj_image_subset_iff inj_on_def vec_of_basis_enum_inverse)
[PROOF STATE]
proof (state)
this:
(cspan (set A) \<subseteq> cspan (set B)) = (local.span (set Av) \<subseteq> local.span (set Bv))

goal (1 subgoal):
 1. (ccspan (set A) \<le> ccspan (set B)) = is_subspace_of_vec_list (length canonical_basis) (map vec_of_basis_enum A) (map vec_of_basis_enum B)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(cspan (set A) \<subseteq> cspan (set B)) = (local.span (set Av) \<subseteq> local.span (set Bv))

goal (1 subgoal):
 1. (ccspan (set A) \<le> ccspan (set B)) = is_subspace_of_vec_list (length canonical_basis) (map vec_of_basis_enum A) (map vec_of_basis_enum B)
[PROOF STEP]
have "\<dots> \<longleftrightarrow> span (set Av) \<subseteq> span (set Bo)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (local.span (set Av) \<subseteq> local.span (set Bv)) = (local.span (set Av) \<subseteq> local.span (set Bo))
[PROOF STEP]
unfolding Bo_def Av_def Bv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (local.span (set (map vec_of_basis_enum A)) \<subseteq> local.span (set (map vec_of_basis_enum B))) = (local.span (set (map vec_of_basis_enum A)) \<subseteq> local.span (set (gram_schmidt0 d (map vec_of_basis_enum B))))
[PROOF STEP]
apply (subst gram_schmidt0_result(4)[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. set (map vec_of_basis_enum B) \<subseteq> carrier_vec d
 2. (local.span (set (map vec_of_basis_enum A)) \<subseteq> local.span (set (map vec_of_basis_enum B))) = (local.span (set (map vec_of_basis_enum A)) \<subseteq> local.span (set (map vec_of_basis_enum B)))
[PROOF STEP]
by (simp_all add: carrier_dim_vec d_def dim_vec_of_basis_enum' image_subset_iff)
[PROOF STATE]
proof (state)
this:
(local.span (set Av) \<subseteq> local.span (set Bv)) = (local.span (set Av) \<subseteq> local.span (set Bo))

goal (1 subgoal):
 1. (ccspan (set A) \<le> ccspan (set B)) = is_subspace_of_vec_list (length canonical_basis) (map vec_of_basis_enum A) (map vec_of_basis_enum B)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(local.span (set Av) \<subseteq> local.span (set Bv)) = (local.span (set Av) \<subseteq> local.span (set Bo))

goal (1 subgoal):
 1. (ccspan (set A) \<le> ccspan (set B)) = is_subspace_of_vec_list (length canonical_basis) (map vec_of_basis_enum A) (map vec_of_basis_enum B)
[PROOF STEP]
have "\<dots> \<longleftrightarrow> (\<forall>v\<in>set Av. adjuster d v Bo = - v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (local.span (set Av) \<subseteq> local.span (set Bo)) = (\<forall>v\<in>set Av. adjuster d v Bo = - v)
[PROOF STEP]
proof (intro iffI ballI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v. \<lbrakk>local.span (set Av) \<subseteq> local.span (set Bo); v \<in> set Av\<rbrakk> \<Longrightarrow> adjuster d v Bo = - v
 2. \<forall>v\<in>set Av. adjuster d v Bo = - v \<Longrightarrow> local.span (set Av) \<subseteq> local.span (set Bo)
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v. \<lbrakk>local.span (set Av) \<subseteq> local.span (set Bo); v \<in> set Av\<rbrakk> \<Longrightarrow> adjuster d v Bo = - v
 2. \<forall>v\<in>set Av. adjuster d v Bo = - v \<Longrightarrow> local.span (set Av) \<subseteq> local.span (set Bo)
[PROOF STEP]
assume "v \<in> set Av" and "span (set Av) \<subseteq> span (set Bo)"
[PROOF STATE]
proof (state)
this:
v \<in> set Av
local.span (set Av) \<subseteq> local.span (set Bo)

goal (2 subgoals):
 1. \<And>v. \<lbrakk>local.span (set Av) \<subseteq> local.span (set Bo); v \<in> set Av\<rbrakk> \<Longrightarrow> adjuster d v Bo = - v
 2. \<forall>v\<in>set Av. adjuster d v Bo = - v \<Longrightarrow> local.span (set Av) \<subseteq> local.span (set Bo)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> set Av
local.span (set Av) \<subseteq> local.span (set Bo)
[PROOF STEP]
have "v \<in> span (set Bo)"
[PROOF STATE]
proof (prove)
using this:
v \<in> set Av
local.span (set Av) \<subseteq> local.span (set Bo)

goal (1 subgoal):
 1. v \<in> local.span (set Bo)
[PROOF STEP]
using Av_carrier span_mem
[PROOF STATE]
proof (prove)
using this:
v \<in> set Av
local.span (set Av) \<subseteq> local.span (set Bo)
set Av \<subseteq> carrier_vec d
\<lbrakk>?E \<subseteq> carrier_vec d; ?u \<in> ?E\<rbrakk> \<Longrightarrow> ?u \<in> local.span ?E

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

goal (2 subgoals):
 1. \<And>v. \<lbrakk>local.span (set Av) \<subseteq> local.span (set Bo); v \<in> set Av\<rbrakk> \<Longrightarrow> adjuster d v Bo = - v
 2. \<forall>v\<in>set Av. adjuster d v Bo = - v \<Longrightarrow> local.span (set Av) \<subseteq> local.span (set Bo)
[PROOF STEP]
have "adjuster d v Bo + v = 0\<^sub>v d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjuster d v Bo + v = 0\<^sub>v d
[PROOF STEP]
apply (rule adjuster_already_in_span)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. v \<in> carrier_vec d
 2. set Bo \<subseteq> carrier_vec d
 3. corthogonal Bo
 4. v \<in> local.span (set Bo)
[PROOF STEP]
using Av_carrier \<open>v \<in> set Av\<close> Bo_carrier orth_Bo
        \<open>v \<in> span (set Bo)\<close>
[PROOF STATE]
proof (prove)
using this:
set Av \<subseteq> carrier_vec d
v \<in> set Av
set Bo \<subseteq> carrier_vec d
corthogonal Bo
v \<in> local.span (set Bo)

goal (4 subgoals):
 1. v \<in> carrier_vec d
 2. set Bo \<subseteq> carrier_vec d
 3. corthogonal Bo
 4. v \<in> local.span (set Bo)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
adjuster d v Bo + v = 0\<^sub>v d

goal (2 subgoals):
 1. \<And>v. \<lbrakk>local.span (set Av) \<subseteq> local.span (set Bo); v \<in> set Av\<rbrakk> \<Longrightarrow> adjuster d v Bo = - v
 2. \<forall>v\<in>set Av. adjuster d v Bo = - v \<Longrightarrow> local.span (set Av) \<subseteq> local.span (set Bo)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
adjuster d v Bo + v = 0\<^sub>v d
[PROOF STEP]
show "adjuster d v Bo = - v"
[PROOF STATE]
proof (prove)
using this:
adjuster d v Bo + v = 0\<^sub>v d

goal (1 subgoal):
 1. adjuster d v Bo = - v
[PROOF STEP]
using Av_carrier Bo_carrier \<open>v \<in> set Av\<close>
[PROOF STATE]
proof (prove)
using this:
adjuster d v Bo + v = 0\<^sub>v d
set Av \<subseteq> carrier_vec d
set Bo \<subseteq> carrier_vec d
v \<in> set Av

goal (1 subgoal):
 1. adjuster d v Bo = - v
[PROOF STEP]
by (metis (no_types, lifting) add.inv_equality adjuster_carrier' local.vec_neg subsetD)
[PROOF STATE]
proof (state)
this:
adjuster d v Bo = - v

goal (1 subgoal):
 1. \<forall>v\<in>set Av. adjuster d v Bo = - v \<Longrightarrow> local.span (set Av) \<subseteq> local.span (set Bo)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>v\<in>set Av. adjuster d v Bo = - v \<Longrightarrow> local.span (set Av) \<subseteq> local.span (set Bo)
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>v\<in>set Av. adjuster d v Bo = - v \<Longrightarrow> local.span (set Av) \<subseteq> local.span (set Bo)
[PROOF STEP]
assume adj_minusv: "\<forall>v\<in>set Av. adjuster d v Bo = - v"
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>set Av. adjuster d v Bo = - v

goal (1 subgoal):
 1. \<forall>v\<in>set Av. adjuster d v Bo = - v \<Longrightarrow> local.span (set Av) \<subseteq> local.span (set Bo)
[PROOF STEP]
have *: "adjuster d v Bo \<in> span (set Bo)" if "v \<in> set Av" for v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjuster d v Bo \<in> local.span (set Bo)
[PROOF STEP]
apply (rule adjuster_in_span)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. v \<in> carrier_vec d
 2. set Bo \<subseteq> carrier_vec d
 3. distinct Bo
[PROOF STEP]
using Bo_carrier that Av_carrier distinct_Bo
[PROOF STATE]
proof (prove)
using this:
set Bo \<subseteq> carrier_vec d
v \<in> set Av
set Av \<subseteq> carrier_vec d
distinct Bo

goal (3 subgoals):
 1. v \<in> carrier_vec d
 2. set Bo \<subseteq> carrier_vec d
 3. distinct Bo
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?v1 \<in> set Av \<Longrightarrow> adjuster d ?v1 Bo \<in> local.span (set Bo)

goal (1 subgoal):
 1. \<forall>v\<in>set Av. adjuster d v Bo = - v \<Longrightarrow> local.span (set Av) \<subseteq> local.span (set Bo)
[PROOF STEP]
have "v \<in> span (set Bo)" if "v \<in> set Av" for v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> local.span (set Bo)
[PROOF STEP]
using *[OF that] adj_minusv[rule_format, OF that]
[PROOF STATE]
proof (prove)
using this:
adjuster d v Bo \<in> local.span (set Bo)
adjuster d v Bo = - v

goal (1 subgoal):
 1. v \<in> local.span (set Bo)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>- v \<in> local.span (set Bo); adjuster d v Bo = - v\<rbrakk> \<Longrightarrow> v \<in> local.span (set Bo)
[PROOF STEP]
by (metis (no_types, lifting) Av_carrier Bo_carrier adjust_nonzero distinct_Bo subsetD that uminus_l_inv_vec)
[PROOF STATE]
proof (state)
this:
?v1 \<in> set Av \<Longrightarrow> ?v1 \<in> local.span (set Bo)

goal (1 subgoal):
 1. \<forall>v\<in>set Av. adjuster d v Bo = - v \<Longrightarrow> local.span (set Av) \<subseteq> local.span (set Bo)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?v1 \<in> set Av \<Longrightarrow> ?v1 \<in> local.span (set Bo)
[PROOF STEP]
show "span (set Av) \<subseteq> span (set Bo)"
[PROOF STATE]
proof (prove)
using this:
?v1 \<in> set Av \<Longrightarrow> ?v1 \<in> local.span (set Bo)

goal (1 subgoal):
 1. local.span (set Av) \<subseteq> local.span (set Bo)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>v. v \<in> set Av \<Longrightarrow> v \<in> local.span (set Bo); x \<in> local.span (set Av)\<rbrakk> \<Longrightarrow> x \<in> local.span (set Bo)
[PROOF STEP]
by (meson Bo_carrier in_mono span_subsetI subsetI)
[PROOF STATE]
proof (state)
this:
local.span (set Av) \<subseteq> local.span (set Bo)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(local.span (set Av) \<subseteq> local.span (set Bo)) = (\<forall>v\<in>set Av. adjuster d v Bo = - v)

goal (1 subgoal):
 1. (ccspan (set A) \<le> ccspan (set B)) = is_subspace_of_vec_list (length canonical_basis) (map vec_of_basis_enum A) (map vec_of_basis_enum B)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(local.span (set Av) \<subseteq> local.span (set Bo)) = (\<forall>v\<in>set Av. adjuster d v Bo = - v)

goal (1 subgoal):
 1. (ccspan (set A) \<le> ccspan (set B)) = is_subspace_of_vec_list (length canonical_basis) (map vec_of_basis_enum A) (map vec_of_basis_enum B)
[PROOF STEP]
have "\<dots> = is_subspace_of_vec_list d Av Bv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>v\<in>set Av. adjuster d v Bo = - v) = is_subspace_of_vec_list d Av Bv
[PROOF STEP]
by (simp add: is_subspace_of_vec_list_def d_def Bo_def)
[PROOF STATE]
proof (state)
this:
(\<forall>v\<in>set Av. adjuster d v Bo = - v) = is_subspace_of_vec_list d Av Bv

goal (1 subgoal):
 1. (ccspan (set A) \<le> ccspan (set B)) = is_subspace_of_vec_list (length canonical_basis) (map vec_of_basis_enum A) (map vec_of_basis_enum B)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(ccspan (set A) \<le> ccspan (set B)) = is_subspace_of_vec_list d Av Bv
[PROOF STEP]
show "ccspan (set A) \<le> ccspan (set B) \<longleftrightarrow> is_subspace_of_vec_list d Av Bv"
[PROOF STATE]
proof (prove)
using this:
(ccspan (set A) \<le> ccspan (set B)) = is_subspace_of_vec_list d Av Bv

goal (1 subgoal):
 1. (ccspan (set A) \<le> ccspan (set B)) = is_subspace_of_vec_list d Av Bv
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(ccspan (set A) \<le> ccspan (set B)) = is_subspace_of_vec_list d Av Bv

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cblinfun_apply_ccspan_using_vec:
  "A *\<^sub>S ccspan (set S) = ccspan (basis_enum_of_vec ` set (map ((*\<^sub>v) (mat_of_cblinfun A)) (map vec_of_basis_enum S)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>S ccspan (set S) = ccspan (basis_enum_of_vec ` set (map ((*\<^sub>v) (mat_of_cblinfun A)) (map vec_of_basis_enum S)))
[PROOF STEP]
apply (auto simp: cblinfun_image_ccspan image_image)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccspan ((*\<^sub>V) A ` set S) = ccspan ((\<lambda>x. basis_enum_of_vec (mat_of_cblinfun A *\<^sub>v vec_of_basis_enum x)) ` set S)
[PROOF STEP]
by (metis mat_of_cblinfun_cblinfun_apply vec_of_basis_enum_inverse)


[STATEMENT]
lemma mk_projector_orthog_correct:
  fixes S :: "'a::onb_enum list"
  defines "d \<equiv> length (canonical_basis :: 'a list)"
  assumes ortho: "is_ortho_set (set S)" and distinct: "distinct S"
  shows "mk_projector_orthog d (map vec_of_basis_enum S)
       = mat_of_cblinfun (Proj (ccspan (set S)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
define Snorm where "Snorm = map (\<lambda>s. s /\<^sub>R norm s) S"
[PROOF STATE]
proof (state)
this:
Snorm = map (\<lambda>s. s /\<^sub>R norm s) S

goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
have "distinct Snorm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct Snorm
[PROOF STEP]
proof (insert ortho distinct, unfold Snorm_def, induction S)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>is_ortho_set (set []); distinct []\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>s. s /\<^sub>R norm s) [])
 2. \<And>a S. \<lbrakk>\<lbrakk>is_ortho_set (set S); distinct S\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>s. s /\<^sub>R norm s) S); is_ortho_set (set (a # S)); distinct (a # S)\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>s. s /\<^sub>R norm s) (a # S))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
is_ortho_set (set [])
distinct []

goal (2 subgoals):
 1. \<lbrakk>is_ortho_set (set []); distinct []\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>s. s /\<^sub>R norm s) [])
 2. \<And>a S. \<lbrakk>\<lbrakk>is_ortho_set (set S); distinct S\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>s. s /\<^sub>R norm s) S); is_ortho_set (set (a # S)); distinct (a # S)\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>s. s /\<^sub>R norm s) (a # S))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map (\<lambda>s. s /\<^sub>R norm s) [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (map (\<lambda>s. s /\<^sub>R norm s) [])

goal (1 subgoal):
 1. \<And>a S. \<lbrakk>\<lbrakk>is_ortho_set (set S); distinct S\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>s. s /\<^sub>R norm s) S); is_ortho_set (set (a # S)); distinct (a # S)\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>s. s /\<^sub>R norm s) (a # S))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a S. \<lbrakk>\<lbrakk>is_ortho_set (set S); distinct S\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>s. s /\<^sub>R norm s) S); is_ortho_set (set (a # S)); distinct (a # S)\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>s. s /\<^sub>R norm s) (a # S))
[PROOF STEP]
case (Cons s S)
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_ortho_set (set S); distinct S\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>s. s /\<^sub>R norm s) S)
is_ortho_set (set (s # S))
distinct (s # S)

goal (1 subgoal):
 1. \<And>a S. \<lbrakk>\<lbrakk>is_ortho_set (set S); distinct S\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>s. s /\<^sub>R norm s) S); is_ortho_set (set (a # S)); distinct (a # S)\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>s. s /\<^sub>R norm s) (a # S))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>is_ortho_set (set S); distinct S\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>s. s /\<^sub>R norm s) S)
is_ortho_set (set (s # S))
distinct (s # S)
[PROOF STEP]
have "is_ortho_set (set S)" and "distinct S"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_ortho_set (set S); distinct S\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>s. s /\<^sub>R norm s) S)
is_ortho_set (set (s # S))
distinct (s # S)

goal (1 subgoal):
 1. is_ortho_set (set S) &&& distinct S
[PROOF STEP]
unfolding is_ortho_set_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(\<forall>x\<in>set S. \<forall>y\<in>set S. x \<noteq> y \<longrightarrow> is_orthogonal x y) \<and> (0::'a) \<notin> set S; distinct S\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>s. s /\<^sub>R norm s) S)
(\<forall>x\<in>set (s # S). \<forall>y\<in>set (s # S). x \<noteq> y \<longrightarrow> is_orthogonal x y) \<and> (0::'a) \<notin> set (s # S)
distinct (s # S)

goal (1 subgoal):
 1. (\<forall>x\<in>set S. \<forall>y\<in>set S. x \<noteq> y \<longrightarrow> is_orthogonal x y) \<and> (0::'a) \<notin> set S &&& distinct S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_ortho_set (set S)
distinct S

goal (1 subgoal):
 1. \<And>a S. \<lbrakk>\<lbrakk>is_ortho_set (set S); distinct S\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>s. s /\<^sub>R norm s) S); is_ortho_set (set (a # S)); distinct (a # S)\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>s. s /\<^sub>R norm s) (a # S))
[PROOF STEP]
note IH = Cons.IH[OF this]
[PROOF STATE]
proof (state)
this:
distinct (map (\<lambda>s. s /\<^sub>R norm s) S)

goal (1 subgoal):
 1. \<And>a S. \<lbrakk>\<lbrakk>is_ortho_set (set S); distinct S\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>s. s /\<^sub>R norm s) S); is_ortho_set (set (a # S)); distinct (a # S)\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>s. s /\<^sub>R norm s) (a # S))
[PROOF STEP]
have "s /\<^sub>R norm s \<notin> (\<lambda>s. s /\<^sub>R norm s) ` set S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s /\<^sub>R norm s \<notin> (\<lambda>s. s /\<^sub>R norm s) ` set S
[PROOF STEP]
proof auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>s /\<^sub>R norm s = sa /\<^sub>R norm sa; sa \<in> set S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix s'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>s /\<^sub>R norm s = sa /\<^sub>R norm sa; sa \<in> set S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "s' \<in> set S" and same: "s /\<^sub>R norm s = s' /\<^sub>R norm s'"
[PROOF STATE]
proof (state)
this:
s' \<in> set S
s /\<^sub>R norm s = s' /\<^sub>R norm s'

goal (1 subgoal):
 1. \<And>sa. \<lbrakk>s /\<^sub>R norm s = sa /\<^sub>R norm sa; sa \<in> set S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with Cons.prems
[PROOF STATE]
proof (chain)
picking this:
is_ortho_set (set (s # S))
distinct (s # S)
s' \<in> set S
s /\<^sub>R norm s = s' /\<^sub>R norm s'
[PROOF STEP]
have "s \<noteq> s'"
[PROOF STATE]
proof (prove)
using this:
is_ortho_set (set (s # S))
distinct (s # S)
s' \<in> set S
s /\<^sub>R norm s = s' /\<^sub>R norm s'

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

goal (1 subgoal):
 1. \<And>sa. \<lbrakk>s /\<^sub>R norm s = sa /\<^sub>R norm sa; sa \<in> set S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "s \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<noteq> (0::'a)
[PROOF STEP]
by (metis Cons.prems(1) is_ortho_set_def list.set_intros(1))
[PROOF STATE]
proof (state)
this:
s \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>sa. \<lbrakk>s /\<^sub>R norm s = sa /\<^sub>R norm sa; sa \<in> set S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<noteq> (0::'a)
[PROOF STEP]
have "0 \<noteq> (s /\<^sub>R norm s) \<bullet>\<^sub>C (s /\<^sub>R norm s)"
[PROOF STATE]
proof (prove)
using this:
s \<noteq> (0::'a)

goal (1 subgoal):
 1. 0 \<noteq> (s /\<^sub>R norm s) \<bullet>\<^sub>C (s /\<^sub>R norm s)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<noteq> (s /\<^sub>R norm s) \<bullet>\<^sub>C (s /\<^sub>R norm s)

goal (1 subgoal):
 1. \<And>sa. \<lbrakk>s /\<^sub>R norm s = sa /\<^sub>R norm sa; sa \<in> set S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 \<noteq> (s /\<^sub>R norm s) \<bullet>\<^sub>C (s /\<^sub>R norm s)

goal (1 subgoal):
 1. \<And>sa. \<lbrakk>s /\<^sub>R norm s = sa /\<^sub>R norm sa; sa \<in> set S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have \<open>(s /\<^sub>R norm s) \<bullet>\<^sub>C (s /\<^sub>R norm s) = (s /\<^sub>R norm s) \<bullet>\<^sub>C (s' /\<^sub>R norm s')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s /\<^sub>R norm s) \<bullet>\<^sub>C (s /\<^sub>R norm s) = (s /\<^sub>R norm s) \<bullet>\<^sub>C (s' /\<^sub>R norm s')
[PROOF STEP]
by (simp add: same)
[PROOF STATE]
proof (state)
this:
(s /\<^sub>R norm s) \<bullet>\<^sub>C (s /\<^sub>R norm s) = (s /\<^sub>R norm s) \<bullet>\<^sub>C (s' /\<^sub>R norm s')

goal (1 subgoal):
 1. \<And>sa. \<lbrakk>s /\<^sub>R norm s = sa /\<^sub>R norm sa; sa \<in> set S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(s /\<^sub>R norm s) \<bullet>\<^sub>C (s /\<^sub>R norm s) = (s /\<^sub>R norm s) \<bullet>\<^sub>C (s' /\<^sub>R norm s')

goal (1 subgoal):
 1. \<And>sa. \<lbrakk>s /\<^sub>R norm s = sa /\<^sub>R norm sa; sa \<in> set S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have \<open>(s /\<^sub>R norm s) \<bullet>\<^sub>C (s' /\<^sub>R norm s') = (s \<bullet>\<^sub>C s') / (norm s * norm s')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s /\<^sub>R norm s) \<bullet>\<^sub>C (s' /\<^sub>R norm s') = s \<bullet>\<^sub>C s' / complex_of_real (norm s * norm s')
[PROOF STEP]
by (simp add: scaleR_scaleC divide_inverse_commute)
[PROOF STATE]
proof (state)
this:
(s /\<^sub>R norm s) \<bullet>\<^sub>C (s' /\<^sub>R norm s') = s \<bullet>\<^sub>C s' / complex_of_real (norm s * norm s')

goal (1 subgoal):
 1. \<And>sa. \<lbrakk>s /\<^sub>R norm s = sa /\<^sub>R norm sa; sa \<in> set S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(s /\<^sub>R norm s) \<bullet>\<^sub>C (s' /\<^sub>R norm s') = s \<bullet>\<^sub>C s' / complex_of_real (norm s * norm s')

goal (1 subgoal):
 1. \<And>sa. \<lbrakk>s /\<^sub>R norm s = sa /\<^sub>R norm sa; sa \<in> set S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from \<open>s' \<in> set S\<close> \<open>s \<noteq> s'\<close>
[PROOF STATE]
proof (chain)
picking this:
s' \<in> set S
s \<noteq> s'
[PROOF STEP]
have "\<dots> = 0"
[PROOF STATE]
proof (prove)
using this:
s' \<in> set S
s \<noteq> s'

goal (1 subgoal):
 1. s \<bullet>\<^sub>C s' / complex_of_real (norm s * norm s') = 0
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
s' \<in> set S
s \<noteq> s'
is_ortho_set (set (s # S))
distinct (s # S)

goal (1 subgoal):
 1. s \<bullet>\<^sub>C s' / complex_of_real (norm s * norm s') = 0
[PROOF STEP]
unfolding is_ortho_set_def
[PROOF STATE]
proof (prove)
using this:
s' \<in> set S
s \<noteq> s'
(\<forall>x\<in>set (s # S). \<forall>y\<in>set (s # S). x \<noteq> y \<longrightarrow> is_orthogonal x y) \<and> (0::'a) \<notin> set (s # S)
distinct (s # S)

goal (1 subgoal):
 1. s \<bullet>\<^sub>C s' / complex_of_real (norm s * norm s') = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s \<bullet>\<^sub>C s' / complex_of_real (norm s * norm s') = 0

goal (1 subgoal):
 1. \<And>sa. \<lbrakk>s /\<^sub>R norm s = sa /\<^sub>R norm sa; sa \<in> set S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 \<noteq> 0
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
0 \<noteq> 0

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s /\<^sub>R norm s \<notin> (\<lambda>s. s /\<^sub>R norm s) ` set S

goal (1 subgoal):
 1. \<And>a S. \<lbrakk>\<lbrakk>is_ortho_set (set S); distinct S\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>s. s /\<^sub>R norm s) S); is_ortho_set (set (a # S)); distinct (a # S)\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>s. s /\<^sub>R norm s) (a # S))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s /\<^sub>R norm s \<notin> (\<lambda>s. s /\<^sub>R norm s) ` set S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
s /\<^sub>R norm s \<notin> (\<lambda>s. s /\<^sub>R norm s) ` set S

goal (1 subgoal):
 1. distinct (map (\<lambda>s. s /\<^sub>R norm s) (s # S))
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
s /\<^sub>R norm s \<notin> (\<lambda>s. s /\<^sub>R norm s) ` set S
distinct (map (\<lambda>s. s /\<^sub>R norm s) S)

goal (1 subgoal):
 1. distinct (map (\<lambda>s. s /\<^sub>R norm s) (s # S))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (map (\<lambda>s. s /\<^sub>R norm s) (s # S))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
distinct Snorm

goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
have norm_Snorm: "norm s = 1" if "s \<in> set Snorm" for s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm s = 1
[PROOF STEP]
using that ortho
[PROOF STATE]
proof (prove)
using this:
s \<in> set Snorm
is_ortho_set (set S)

goal (1 subgoal):
 1. norm s = 1
[PROOF STEP]
unfolding Snorm_def is_ortho_set_def
[PROOF STATE]
proof (prove)
using this:
s \<in> set (map (\<lambda>s. s /\<^sub>R norm s) S)
(\<forall>x\<in>set S. \<forall>y\<in>set S. x \<noteq> y \<longrightarrow> is_orthogonal x y) \<and> (0::'a) \<notin> set S

goal (1 subgoal):
 1. norm s = 1
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>sa \<in> set S; s = sa /\<^sub>R norm sa; \<forall>x\<in>set S. \<forall>y\<in>set S. x \<noteq> y \<longrightarrow> is_orthogonal x y; (0::'a) \<notin> set S\<rbrakk> \<Longrightarrow> inverse (norm sa) * norm sa = 1
[PROOF STEP]
by (metis left_inverse norm_eq_zero)
[PROOF STATE]
proof (state)
this:
?s \<in> set Snorm \<Longrightarrow> norm ?s = 1

goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
have ortho_Snorm: "is_ortho_set (set Snorm)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_ortho_set (set Snorm)
[PROOF STEP]
unfolding is_ortho_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>set Snorm. \<forall>y\<in>set Snorm. x \<noteq> y \<longrightarrow> is_orthogonal x y) \<and> (0::'a) \<notin> set Snorm
[PROOF STEP]
proof (intro conjI ballI impI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> set Snorm; y \<in> set Snorm; x \<noteq> y\<rbrakk> \<Longrightarrow> is_orthogonal x y
 2. (0::'a) \<notin> set Snorm
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> set Snorm; y \<in> set Snorm; x \<noteq> y\<rbrakk> \<Longrightarrow> is_orthogonal x y
 2. (0::'a) \<notin> set Snorm
[PROOF STEP]
show "0 \<notin> set Snorm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<notin> set Snorm
[PROOF STEP]
using norm_Snorm[of 0]
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<in> set Snorm \<Longrightarrow> norm (0::'a) = 1

goal (1 subgoal):
 1. (0::'a) \<notin> set Snorm
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(0::'a) \<notin> set Snorm

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set Snorm; y \<in> set Snorm; x \<noteq> y\<rbrakk> \<Longrightarrow> is_orthogonal x y
[PROOF STEP]
assume "x \<in> set Snorm" and "y \<in> set Snorm" and "x \<noteq> y"
[PROOF STATE]
proof (state)
this:
x \<in> set Snorm
y \<in> set Snorm
x \<noteq> y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set Snorm; y \<in> set Snorm; x \<noteq> y\<rbrakk> \<Longrightarrow> is_orthogonal x y
[PROOF STEP]
from \<open>x \<in> set Snorm\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> set Snorm
[PROOF STEP]
obtain x' where x: "x = x' /\<^sub>R norm x'" and x': "x' \<in> set S"
[PROOF STATE]
proof (prove)
using this:
x \<in> set Snorm

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>x = x' /\<^sub>R norm x'; x' \<in> set S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding Snorm_def
[PROOF STATE]
proof (prove)
using this:
x \<in> set (map (\<lambda>s. s /\<^sub>R norm s) S)

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>x = x' /\<^sub>R norm x'; x' \<in> set S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = x' /\<^sub>R norm x'
x' \<in> set S

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set Snorm; y \<in> set Snorm; x \<noteq> y\<rbrakk> \<Longrightarrow> is_orthogonal x y
[PROOF STEP]
from \<open>y \<in> set Snorm\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> set Snorm
[PROOF STEP]
obtain y' where y: "y = y' /\<^sub>R norm y'" and y': "y' \<in> set S"
[PROOF STATE]
proof (prove)
using this:
y \<in> set Snorm

goal (1 subgoal):
 1. (\<And>y'. \<lbrakk>y = y' /\<^sub>R norm y'; y' \<in> set S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding Snorm_def
[PROOF STATE]
proof (prove)
using this:
y \<in> set (map (\<lambda>s. s /\<^sub>R norm s) S)

goal (1 subgoal):
 1. (\<And>y'. \<lbrakk>y = y' /\<^sub>R norm y'; y' \<in> set S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y = y' /\<^sub>R norm y'
y' \<in> set S

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set Snorm; y \<in> set Snorm; x \<noteq> y\<rbrakk> \<Longrightarrow> is_orthogonal x y
[PROOF STEP]
from \<open>x \<noteq> y\<close> x y
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> y
x = x' /\<^sub>R norm x'
y = y' /\<^sub>R norm y'
[PROOF STEP]
have \<open>x' \<noteq> y'\<close>
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
x = x' /\<^sub>R norm x'
y = y' /\<^sub>R norm y'

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set Snorm; y \<in> set Snorm; x \<noteq> y\<rbrakk> \<Longrightarrow> is_orthogonal x y
[PROOF STEP]
with x' y' ortho
[PROOF STATE]
proof (chain)
picking this:
x' \<in> set S
y' \<in> set S
is_ortho_set (set S)
x' \<noteq> y'
[PROOF STEP]
have "cinner x' y' = 0"
[PROOF STATE]
proof (prove)
using this:
x' \<in> set S
y' \<in> set S
is_ortho_set (set S)
x' \<noteq> y'

goal (1 subgoal):
 1. is_orthogonal x' y'
[PROOF STEP]
unfolding is_ortho_set_def
[PROOF STATE]
proof (prove)
using this:
x' \<in> set S
y' \<in> set S
(\<forall>x\<in>set S. \<forall>y\<in>set S. x \<noteq> y \<longrightarrow> is_orthogonal x y) \<and> (0::'a) \<notin> set S
x' \<noteq> y'

goal (1 subgoal):
 1. is_orthogonal x' y'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_orthogonal x' y'

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set Snorm; y \<in> set Snorm; x \<noteq> y\<rbrakk> \<Longrightarrow> is_orthogonal x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_orthogonal x' y'
[PROOF STEP]
show "cinner x y = 0"
[PROOF STATE]
proof (prove)
using this:
is_orthogonal x' y'

goal (1 subgoal):
 1. is_orthogonal x y
[PROOF STEP]
unfolding x y scaleR_scaleC
[PROOF STATE]
proof (prove)
using this:
is_orthogonal x' y'

goal (1 subgoal):
 1. is_orthogonal (complex_of_real (inverse (norm x')) *\<^sub>C x') (complex_of_real (inverse (norm y')) *\<^sub>C y')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_orthogonal x y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_ortho_set (set Snorm)

goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
have inj_butter: "inj_on selfbutter (set Snorm)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on selfbutter (set Snorm)
[PROOF STEP]
proof (rule inj_onI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set Snorm; y \<in> set Snorm; selfbutter x = selfbutter y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set Snorm; y \<in> set Snorm; selfbutter x = selfbutter y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume "x \<in> set Snorm" and "y \<in> set Snorm"
[PROOF STATE]
proof (state)
this:
x \<in> set Snorm
y \<in> set Snorm

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set Snorm; y \<in> set Snorm; selfbutter x = selfbutter y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume "selfbutter x = selfbutter y"
[PROOF STATE]
proof (state)
this:
selfbutter x = selfbutter y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set Snorm; y \<in> set Snorm; selfbutter x = selfbutter y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
selfbutter x = selfbutter y
[PROOF STEP]
obtain c where xcy: "x = c *\<^sub>C y" and "cmod c = 1"
[PROOF STATE]
proof (prove)
using this:
selfbutter x = selfbutter y

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>x = c *\<^sub>C y; cmod c = 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using inj_selfbutter_upto_phase
[PROOF STATE]
proof (prove)
using this:
selfbutter x = selfbutter y
selfbutter ?x = selfbutter ?y \<Longrightarrow> \<exists>c. cmod c = 1 \<and> ?x = c *\<^sub>C ?y

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>x = c *\<^sub>C y; cmod c = 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = c *\<^sub>C y
cmod c = 1

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set Snorm; y \<in> set Snorm; selfbutter x = selfbutter y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "0 \<noteq> cmod (cinner x x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<noteq> cmod (x \<bullet>\<^sub>C x)
[PROOF STEP]
using \<open>x \<in> set Snorm\<close> norm_Snorm
[PROOF STATE]
proof (prove)
using this:
x \<in> set Snorm
?s \<in> set Snorm \<Longrightarrow> norm ?s = 1

goal (1 subgoal):
 1. 0 \<noteq> cmod (x \<bullet>\<^sub>C x)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
0 \<noteq> cmod (x \<bullet>\<^sub>C x)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set Snorm; y \<in> set Snorm; selfbutter x = selfbutter y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 \<noteq> cmod (x \<bullet>\<^sub>C x)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set Snorm; y \<in> set Snorm; selfbutter x = selfbutter y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "cmod (cinner x x) = cmod (c * (x \<bullet>\<^sub>C y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (x \<bullet>\<^sub>C x) = cmod (c * (x \<bullet>\<^sub>C y))
[PROOF STEP]
apply (subst (2) xcy)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (x \<bullet>\<^sub>C c *\<^sub>C y) = cmod (c * (x \<bullet>\<^sub>C y))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cmod (x \<bullet>\<^sub>C x) = cmod (c * (x \<bullet>\<^sub>C y))

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set Snorm; y \<in> set Snorm; selfbutter x = selfbutter y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cmod (x \<bullet>\<^sub>C x) = cmod (c * (x \<bullet>\<^sub>C y))

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set Snorm; y \<in> set Snorm; selfbutter x = selfbutter y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "\<dots> = cmod (x \<bullet>\<^sub>C y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (c * (x \<bullet>\<^sub>C y)) = cmod (x \<bullet>\<^sub>C y)
[PROOF STEP]
using \<open>cmod c = 1\<close>
[PROOF STATE]
proof (prove)
using this:
cmod c = 1

goal (1 subgoal):
 1. cmod (c * (x \<bullet>\<^sub>C y)) = cmod (x \<bullet>\<^sub>C y)
[PROOF STEP]
by (simp add: norm_mult)
[PROOF STATE]
proof (state)
this:
cmod (c * (x \<bullet>\<^sub>C y)) = cmod (x \<bullet>\<^sub>C y)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set Snorm; y \<in> set Snorm; selfbutter x = selfbutter y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 \<noteq> cmod (x \<bullet>\<^sub>C y)
[PROOF STEP]
have "(x \<bullet>\<^sub>C y) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
0 \<noteq> cmod (x \<bullet>\<^sub>C y)

goal (1 subgoal):
 1. x \<bullet>\<^sub>C y \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<bullet>\<^sub>C y \<noteq> 0

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set Snorm; y \<in> set Snorm; selfbutter x = selfbutter y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<bullet>\<^sub>C y \<noteq> 0
[PROOF STEP]
show "x = y"
[PROOF STATE]
proof (prove)
using this:
x \<bullet>\<^sub>C y \<noteq> 0

goal (1 subgoal):
 1. x = y
[PROOF STEP]
using ortho_Snorm \<open>x \<in> set Snorm\<close> \<open>y \<in> set Snorm\<close>
[PROOF STATE]
proof (prove)
using this:
x \<bullet>\<^sub>C y \<noteq> 0
is_ortho_set (set Snorm)
x \<in> set Snorm
y \<in> set Snorm

goal (1 subgoal):
 1. x = y
[PROOF STEP]
unfolding is_ortho_set_def
[PROOF STATE]
proof (prove)
using this:
x \<bullet>\<^sub>C y \<noteq> 0
(\<forall>x\<in>set Snorm. \<forall>y\<in>set Snorm. x \<noteq> y \<longrightarrow> is_orthogonal x y) \<and> (0::'a) \<notin> set Snorm
x \<in> set Snorm
y \<in> set Snorm

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj_on selfbutter (set Snorm)

goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
from \<open>distinct Snorm\<close> inj_butter
[PROOF STATE]
proof (chain)
picking this:
distinct Snorm
inj_on selfbutter (set Snorm)
[PROOF STEP]
have distinct': "distinct (map selfbutter Snorm)"
[PROOF STATE]
proof (prove)
using this:
distinct Snorm
inj_on selfbutter (set Snorm)

goal (1 subgoal):
 1. distinct (map selfbutter Snorm)
[PROOF STEP]
unfolding distinct_map
[PROOF STATE]
proof (prove)
using this:
distinct Snorm
inj_on selfbutter (set Snorm)

goal (1 subgoal):
 1. distinct Snorm \<and> inj_on selfbutter (set Snorm)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (map selfbutter Snorm)

goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
have Span_Snorm: "ccspan (set Snorm) = ccspan (set S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccspan (set Snorm) = ccspan (set S)
[PROOF STEP]
apply (transfer fixing: Snorm S)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure (cspan (set Snorm)) = closure (cspan (set S))
[PROOF STEP]
apply (simp add: scaleR_scaleC Snorm_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cspan ((\<lambda>s. s /\<^sub>C complex_of_real (norm s)) ` set S) = cspan (set S)
[PROOF STEP]
apply (subst complex_vector.span_image_scale)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite (set S)
 2. \<And>x. x \<in> set S \<Longrightarrow> inverse (complex_of_real (norm x)) \<noteq> 0
 3. cspan (set S) = cspan (set S)
[PROOF STEP]
using is_ortho_set_def ortho
[PROOF STATE]
proof (prove)
using this:
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 S)

goal (3 subgoals):
 1. finite (set S)
 2. \<And>x. x \<in> set S \<Longrightarrow> inverse (complex_of_real (norm x)) \<noteq> 0
 3. cspan (set S) = cspan (set S)
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
ccspan (set Snorm) = ccspan (set S)

goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
have "mk_projector_orthog d (map vec_of_basis_enum S)
      = mat_of_cblinfun (sum_list (map selfbutter Snorm))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (sum_list (map selfbutter Snorm))
[PROOF STEP]
unfolding Snorm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) S)))
[PROOF STEP]
proof (induction S)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mk_projector_orthog d (map vec_of_basis_enum []) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) [])))
 2. \<And>a S. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) S))) \<Longrightarrow> mk_projector_orthog d (map vec_of_basis_enum (a # S)) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) (a # S))))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. mk_projector_orthog d (map vec_of_basis_enum []) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) [])))
 2. \<And>a S. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) S))) \<Longrightarrow> mk_projector_orthog d (map vec_of_basis_enum (a # S)) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) (a # S))))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum []) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) [])))
[PROOF STEP]
by (simp add: d_def mat_of_cblinfun_zero)
[PROOF STATE]
proof (state)
this:
mk_projector_orthog d (map vec_of_basis_enum []) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) [])))

goal (1 subgoal):
 1. \<And>a S. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) S))) \<Longrightarrow> mk_projector_orthog d (map vec_of_basis_enum (a # S)) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) (a # S))))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a S. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) S))) \<Longrightarrow> mk_projector_orthog d (map vec_of_basis_enum (a # S)) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) (a # S))))
[PROOF STEP]
case (Cons a S)
[PROOF STATE]
proof (state)
this:
mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) S)))

goal (1 subgoal):
 1. \<And>a S. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) S))) \<Longrightarrow> mk_projector_orthog d (map vec_of_basis_enum (a # S)) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) (a # S))))
[PROOF STEP]
define sumS where "sumS = sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) S))"
[PROOF STATE]
proof (state)
this:
sumS = sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) S))

goal (1 subgoal):
 1. \<And>a S. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) S))) \<Longrightarrow> mk_projector_orthog d (map vec_of_basis_enum (a # S)) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) (a # S))))
[PROOF STEP]
with Cons
[PROOF STATE]
proof (chain)
picking this:
mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) S)))
sumS = sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) S))
[PROOF STEP]
have IH: "mk_projector_orthog d (map vec_of_basis_enum S)
                  = mat_of_cblinfun sumS"
[PROOF STATE]
proof (prove)
using this:
mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) S)))
sumS = sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) S))

goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun sumS
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun sumS

goal (1 subgoal):
 1. \<And>a S. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) S))) \<Longrightarrow> mk_projector_orthog d (map vec_of_basis_enum (a # S)) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) (a # S))))
[PROOF STEP]
define factor where "factor = inverse ((complex_of_real (norm a))\<^sup>2)"
[PROOF STATE]
proof (state)
this:
factor = inverse ((complex_of_real (norm a))\<^sup>2)

goal (1 subgoal):
 1. \<And>a S. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) S))) \<Longrightarrow> mk_projector_orthog d (map vec_of_basis_enum (a # S)) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) (a # S))))
[PROOF STEP]
have factor': "factor = 1 / (vec_of_basis_enum a \<bullet>c vec_of_basis_enum a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. factor = 1 / (vec_of_basis_enum a \<bullet>c vec_of_basis_enum a)
[PROOF STEP]
unfolding factor_def cscalar_prod_vec_of_basis_enum
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse ((complex_of_real (norm a))\<^sup>2) = 1 / (a \<bullet>\<^sub>C a)
[PROOF STEP]
by (simp add: inverse_eq_divide power2_norm_eq_cinner)
[PROOF STATE]
proof (state)
this:
factor = 1 / (vec_of_basis_enum a \<bullet>c vec_of_basis_enum a)

goal (1 subgoal):
 1. \<And>a S. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) S))) \<Longrightarrow> mk_projector_orthog d (map vec_of_basis_enum (a # S)) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) (a # S))))
[PROOF STEP]
have "mk_projector_orthog d (map vec_of_basis_enum (a # S))
          = factor \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a]
                    * mat_of_rows d [conjugate (vec_of_basis_enum a)])
            + mat_of_cblinfun sumS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum (a # S)) = factor \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)]) + mat_of_cblinfun sumS
[PROOF STEP]
apply (cases S)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. S = [] \<Longrightarrow> mk_projector_orthog d (map vec_of_basis_enum (a # S)) = factor \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)]) + mat_of_cblinfun sumS
 2. \<And>aa list. S = aa # list \<Longrightarrow> mk_projector_orthog d (map vec_of_basis_enum (a # S)) = factor \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)]) + mat_of_cblinfun sumS
[PROOF STEP]
apply (auto simp add: factor' sumS_def d_def mat_of_cblinfun_zero)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa list. S = aa # list \<Longrightarrow> mk_projector_orthog d (map vec_of_basis_enum (a # S)) = factor \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)]) + mat_of_cblinfun sumS
[PROOF STEP]
by (auto simp add: IH[symmetric] factor' d_def)
[PROOF STATE]
proof (state)
this:
mk_projector_orthog d (map vec_of_basis_enum (a # S)) = factor \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)]) + mat_of_cblinfun sumS

goal (1 subgoal):
 1. \<And>a S. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) S))) \<Longrightarrow> mk_projector_orthog d (map vec_of_basis_enum (a # S)) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) (a # S))))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mk_projector_orthog d (map vec_of_basis_enum (a # S)) = factor \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)]) + mat_of_cblinfun sumS

goal (1 subgoal):
 1. \<And>a S. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) S))) \<Longrightarrow> mk_projector_orthog d (map vec_of_basis_enum (a # S)) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) (a # S))))
[PROOF STEP]
have "\<dots> = factor \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] *
         mat_adjoint (mat_of_cols d [vec_of_basis_enum a])) + mat_of_cblinfun sumS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. factor \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)]) + mat_of_cblinfun sumS = factor \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_adjoint (mat_of_cols d [vec_of_basis_enum a])) + mat_of_cblinfun sumS
[PROOF STEP]
apply (rule arg_cong[where f="\<lambda>x. _ \<cdot>\<^sub>m (_ * x) + _"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_rows d [conjugate (vec_of_basis_enum a)] = mat_adjoint (mat_of_cols d [vec_of_basis_enum a])
[PROOF STEP]
apply (rule mat_eq_iff[THEN iffD2])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (mat_of_rows d [conjugate (vec_of_basis_enum a)]) = dim_row (mat_adjoint (mat_of_cols d [vec_of_basis_enum a])) \<and> dim_col (mat_of_rows d [conjugate (vec_of_basis_enum a)]) = dim_col (mat_adjoint (mat_of_cols d [vec_of_basis_enum a])) \<and> (\<forall>i j. i < dim_row (mat_adjoint (mat_of_cols d [vec_of_basis_enum a])) \<longrightarrow> j < dim_col (mat_adjoint (mat_of_cols d [vec_of_basis_enum a])) \<longrightarrow> mat_of_rows d [conjugate (vec_of_basis_enum a)] $$ (i, j) = mat_adjoint (mat_of_cols d [vec_of_basis_enum a]) $$ (i, j))
[PROOF STEP]
apply (auto simp add: mat_adjoint_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. j < d \<Longrightarrow> mat_of_rows d [conjugate (vec_of_basis_enum a)] $$ (0, j) = mat_of_rows d (map conjugate (cols (mat_of_cols d [vec_of_basis_enum a]))) $$ (0, j)
[PROOF STEP]
apply (subst mat_of_rows_index)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>j. j < d \<Longrightarrow> 0 < length [conjugate (vec_of_basis_enum a)]
 2. \<And>j. j < d \<Longrightarrow> j < d
 3. \<And>j. j < d \<Longrightarrow> [conjugate (vec_of_basis_enum a)] ! 0 $ j = mat_of_rows d (map conjugate (cols (mat_of_cols d [vec_of_basis_enum a]))) $$ (0, j)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. j < d \<Longrightarrow> conjugate (vec_of_basis_enum a) $ j = mat_of_rows d (map conjugate (cols (mat_of_cols d [vec_of_basis_enum a]))) $$ (0, j)
[PROOF STEP]
apply (subst mat_of_rows_index)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>j. j < d \<Longrightarrow> 0 < length (map conjugate (cols (mat_of_cols d [vec_of_basis_enum a])))
 2. \<And>j. j < d \<Longrightarrow> j < d
 3. \<And>j. j < d \<Longrightarrow> conjugate (vec_of_basis_enum a) $ j = map conjugate (cols (mat_of_cols d [vec_of_basis_enum a])) ! 0 $ j
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. j < d \<Longrightarrow> conjugate (vec_of_basis_enum a) $ j = cnj (mat_of_cols d [vec_of_basis_enum a] $$ (j, 0))
[PROOF STEP]
apply (subst mat_of_cols_index)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>j. j < d \<Longrightarrow> j < d
 2. \<And>j. j < d \<Longrightarrow> 0 < length [vec_of_basis_enum a]
 3. \<And>j. j < d \<Longrightarrow> conjugate (vec_of_basis_enum a) $ j = cnj ([vec_of_basis_enum a] ! 0 $ j)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. j < d \<Longrightarrow> conjugate (vec_of_basis_enum a) $ j = cnj (vec_of_basis_enum a $ j)
[PROOF STEP]
by (simp add: assms(1) dim_vec_of_basis_enum')
[PROOF STATE]
proof (state)
this:
factor \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)]) + mat_of_cblinfun sumS = factor \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_adjoint (mat_of_cols d [vec_of_basis_enum a])) + mat_of_cblinfun sumS

goal (1 subgoal):
 1. \<And>a S. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) S))) \<Longrightarrow> mk_projector_orthog d (map vec_of_basis_enum (a # S)) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) (a # S))))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
factor \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_of_rows d [conjugate (vec_of_basis_enum a)]) + mat_of_cblinfun sumS = factor \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_adjoint (mat_of_cols d [vec_of_basis_enum a])) + mat_of_cblinfun sumS

goal (1 subgoal):
 1. \<And>a S. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) S))) \<Longrightarrow> mk_projector_orthog d (map vec_of_basis_enum (a # S)) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) (a # S))))
[PROOF STEP]
have "\<dots> = mat_of_cblinfun (selfbutter (a /\<^sub>R norm a)) + mat_of_cblinfun sumS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. factor \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_adjoint (mat_of_cols d [vec_of_basis_enum a])) + mat_of_cblinfun sumS = mat_of_cblinfun (selfbutter (a /\<^sub>R norm a)) + mat_of_cblinfun sumS
[PROOF STEP]
apply (simp add: butterfly_scaleR_left butterfly_scaleR_right power_inverse mat_of_cblinfun_scaleR factor_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse ((complex_of_real (norm a))\<^sup>2) \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_adjoint (mat_of_cols d [vec_of_basis_enum a])) + mat_of_cblinfun sumS = mat_of_cblinfun ((inverse (complex_of_real (norm a)) * inverse (complex_of_real (norm a))) *\<^sub>C selfbutter a) + mat_of_cblinfun sumS
[PROOF STEP]
apply (simp add: butterfly_def mat_of_cblinfun_compose
          mat_of_cblinfun_adj mat_of_cblinfun_vector_to_cblinfun d_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse ((complex_of_real (norm a))\<^sup>2) \<cdot>\<^sub>m (mat_of_cols (length canonical_basis) [vec_of_basis_enum a] * mat_adjoint (mat_of_cols (length canonical_basis) [vec_of_basis_enum a])) + mat_of_cblinfun sumS = mat_of_cblinfun ((inverse (complex_of_real (norm a)) * inverse (complex_of_real (norm a))) *\<^sub>C (vector_to_cblinfun a o\<^sub>C\<^sub>L vector_to_cblinfun a*)) + mat_of_cblinfun sumS
[PROOF STEP]
by (simp add: mat_of_cblinfun_compose mat_of_cblinfun_adj mat_of_cblinfun_vector_to_cblinfun mat_of_cblinfun_scaleC power2_eq_square)
[PROOF STATE]
proof (state)
this:
factor \<cdot>\<^sub>m (mat_of_cols d [vec_of_basis_enum a] * mat_adjoint (mat_of_cols d [vec_of_basis_enum a])) + mat_of_cblinfun sumS = mat_of_cblinfun (selfbutter (a /\<^sub>R norm a)) + mat_of_cblinfun sumS

goal (1 subgoal):
 1. \<And>a S. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) S))) \<Longrightarrow> mk_projector_orthog d (map vec_of_basis_enum (a # S)) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) (a # S))))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mk_projector_orthog d (map vec_of_basis_enum (a # S)) = mat_of_cblinfun (selfbutter (a /\<^sub>R norm a)) + mat_of_cblinfun sumS
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
mk_projector_orthog d (map vec_of_basis_enum (a # S)) = mat_of_cblinfun (selfbutter (a /\<^sub>R norm a)) + mat_of_cblinfun sumS

goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum (a # S)) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) (a # S))))
[PROOF STEP]
by (simp add: mat_of_cblinfun_plus sumS_def)
[PROOF STATE]
proof (state)
this:
mk_projector_orthog d (map vec_of_basis_enum (a # S)) = mat_of_cblinfun (sum_list (map selfbutter (map (\<lambda>s. s /\<^sub>R norm s) (a # S))))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (sum_list (map selfbutter Snorm))

goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (sum_list (map selfbutter Snorm))

goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
have "\<dots> = mat_of_cblinfun (\<Sum>s\<in>set Snorm. selfbutter s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (sum_list (map selfbutter Snorm)) = mat_of_cblinfun (sum selfbutter (set Snorm))
[PROOF STEP]
by (metis distinct' distinct_map sum.distinct_set_conv_list)
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (sum_list (map selfbutter Snorm)) = mat_of_cblinfun (sum selfbutter (set Snorm))

goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (sum_list (map selfbutter Snorm)) = mat_of_cblinfun (sum selfbutter (set Snorm))

goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
have "\<dots> = mat_of_cblinfun (\<Sum>s\<in>set Snorm. proj s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (sum selfbutter (set Snorm)) = mat_of_cblinfun (sum proj (set Snorm))
[PROOF STEP]
apply (rule arg_cong[where f="mat_of_cblinfun"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum selfbutter (set Snorm) = sum proj (set Snorm)
[PROOF STEP]
apply (rule sum.cong[OF refl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set Snorm \<Longrightarrow> selfbutter x = proj x
[PROOF STEP]
apply (rule butterfly_eq_proj)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set Snorm \<Longrightarrow> norm x = 1
[PROOF STEP]
using norm_Snorm
[PROOF STATE]
proof (prove)
using this:
?s \<in> set Snorm \<Longrightarrow> norm ?s = 1

goal (1 subgoal):
 1. \<And>x. x \<in> set Snorm \<Longrightarrow> norm x = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (sum selfbutter (set Snorm)) = mat_of_cblinfun (sum proj (set Snorm))

goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (sum selfbutter (set Snorm)) = mat_of_cblinfun (sum proj (set Snorm))

goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
have "\<dots> = mat_of_cblinfun (Proj (ccspan (set Snorm)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (sum proj (set Snorm)) = mat_of_cblinfun (Proj (ccspan (set Snorm)))
[PROOF STEP]
apply (rule arg_cong[of _ _ mat_of_cblinfun])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum proj (set Snorm) = Proj (ccspan (set Snorm))
[PROOF STEP]
proof (insert ortho_Snorm, insert \<open>distinct Snorm\<close>, induction Snorm)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>is_ortho_set (set []); distinct []\<rbrakk> \<Longrightarrow> sum proj (set []) = Proj (ccspan (set []))
 2. \<And>a Snorm. \<lbrakk>\<lbrakk>is_ortho_set (set Snorm); distinct Snorm\<rbrakk> \<Longrightarrow> sum proj (set Snorm) = Proj (ccspan (set Snorm)); is_ortho_set (set (a # Snorm)); distinct (a # Snorm)\<rbrakk> \<Longrightarrow> sum proj (set (a # Snorm)) = Proj (ccspan (set (a # Snorm)))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
is_ortho_set (set [])
distinct []

goal (2 subgoals):
 1. \<lbrakk>is_ortho_set (set []); distinct []\<rbrakk> \<Longrightarrow> sum proj (set []) = Proj (ccspan (set []))
 2. \<And>a Snorm. \<lbrakk>\<lbrakk>is_ortho_set (set Snorm); distinct Snorm\<rbrakk> \<Longrightarrow> sum proj (set Snorm) = Proj (ccspan (set Snorm)); is_ortho_set (set (a # Snorm)); distinct (a # Snorm)\<rbrakk> \<Longrightarrow> sum proj (set (a # Snorm)) = Proj (ccspan (set (a # Snorm)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum proj (set []) = Proj (ccspan (set []))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum proj (set []) = Proj (ccspan (set []))

goal (1 subgoal):
 1. \<And>a Snorm. \<lbrakk>\<lbrakk>is_ortho_set (set Snorm); distinct Snorm\<rbrakk> \<Longrightarrow> sum proj (set Snorm) = Proj (ccspan (set Snorm)); is_ortho_set (set (a # Snorm)); distinct (a # Snorm)\<rbrakk> \<Longrightarrow> sum proj (set (a # Snorm)) = Proj (ccspan (set (a # Snorm)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a Snorm. \<lbrakk>\<lbrakk>is_ortho_set (set Snorm); distinct Snorm\<rbrakk> \<Longrightarrow> sum proj (set Snorm) = Proj (ccspan (set Snorm)); is_ortho_set (set (a # Snorm)); distinct (a # Snorm)\<rbrakk> \<Longrightarrow> sum proj (set (a # Snorm)) = Proj (ccspan (set (a # Snorm)))
[PROOF STEP]
case (Cons a Snorm)
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_ortho_set (set Snorm); distinct Snorm\<rbrakk> \<Longrightarrow> sum proj (set Snorm) = Proj (ccspan (set Snorm))
is_ortho_set (set (a # Snorm))
distinct (a # Snorm)

goal (1 subgoal):
 1. \<And>a Snorm. \<lbrakk>\<lbrakk>is_ortho_set (set Snorm); distinct Snorm\<rbrakk> \<Longrightarrow> sum proj (set Snorm) = Proj (ccspan (set Snorm)); is_ortho_set (set (a # Snorm)); distinct (a # Snorm)\<rbrakk> \<Longrightarrow> sum proj (set (a # Snorm)) = Proj (ccspan (set (a # Snorm)))
[PROOF STEP]
from Cons.prems
[PROOF STATE]
proof (chain)
picking this:
is_ortho_set (set (a # Snorm))
distinct (a # Snorm)
[PROOF STEP]
have [simp]: "a \<notin> set Snorm"
[PROOF STATE]
proof (prove)
using this:
is_ortho_set (set (a # Snorm))
distinct (a # Snorm)

goal (1 subgoal):
 1. a \<notin> set Snorm
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a \<notin> set Snorm

goal (1 subgoal):
 1. \<And>a Snorm. \<lbrakk>\<lbrakk>is_ortho_set (set Snorm); distinct Snorm\<rbrakk> \<Longrightarrow> sum proj (set Snorm) = Proj (ccspan (set Snorm)); is_ortho_set (set (a # Snorm)); distinct (a # Snorm)\<rbrakk> \<Longrightarrow> sum proj (set (a # Snorm)) = Proj (ccspan (set (a # Snorm)))
[PROOF STEP]
have "sum proj (set (a # Snorm))
        = proj a + sum proj (set Snorm)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum proj (set (a # Snorm)) = proj a + sum proj (set Snorm)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum proj (set (a # Snorm)) = proj a + sum proj (set Snorm)

goal (1 subgoal):
 1. \<And>a Snorm. \<lbrakk>\<lbrakk>is_ortho_set (set Snorm); distinct Snorm\<rbrakk> \<Longrightarrow> sum proj (set Snorm) = Proj (ccspan (set Snorm)); is_ortho_set (set (a # Snorm)); distinct (a # Snorm)\<rbrakk> \<Longrightarrow> sum proj (set (a # Snorm)) = Proj (ccspan (set (a # Snorm)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum proj (set (a # Snorm)) = proj a + sum proj (set Snorm)

goal (1 subgoal):
 1. \<And>a Snorm. \<lbrakk>\<lbrakk>is_ortho_set (set Snorm); distinct Snorm\<rbrakk> \<Longrightarrow> sum proj (set Snorm) = Proj (ccspan (set Snorm)); is_ortho_set (set (a # Snorm)); distinct (a # Snorm)\<rbrakk> \<Longrightarrow> sum proj (set (a # Snorm)) = Proj (ccspan (set (a # Snorm)))
[PROOF STEP]
have "\<dots> = proj a + Proj (ccspan (set Snorm))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj a + sum proj (set Snorm) = proj a + Proj (ccspan (set Snorm))
[PROOF STEP]
apply (subst Cons.IH)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. is_ortho_set (set Snorm)
 2. distinct Snorm
 3. proj a + Proj (ccspan (set Snorm)) = proj a + Proj (ccspan (set Snorm))
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
is_ortho_set (set (a # Snorm))
distinct (a # Snorm)

goal (3 subgoals):
 1. is_ortho_set (set Snorm)
 2. distinct Snorm
 3. proj a + Proj (ccspan (set Snorm)) = proj a + Proj (ccspan (set Snorm))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_ortho_set (insert a (set Snorm)); distinct Snorm\<rbrakk> \<Longrightarrow> is_ortho_set (set Snorm)
[PROOF STEP]
by (meson Cons.prems(1) is_ortho_set_antimono set_subset_Cons)
[PROOF STATE]
proof (state)
this:
proj a + sum proj (set Snorm) = proj a + Proj (ccspan (set Snorm))

goal (1 subgoal):
 1. \<And>a Snorm. \<lbrakk>\<lbrakk>is_ortho_set (set Snorm); distinct Snorm\<rbrakk> \<Longrightarrow> sum proj (set Snorm) = Proj (ccspan (set Snorm)); is_ortho_set (set (a # Snorm)); distinct (a # Snorm)\<rbrakk> \<Longrightarrow> sum proj (set (a # Snorm)) = Proj (ccspan (set (a # Snorm)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
proj a + sum proj (set Snorm) = proj a + Proj (ccspan (set Snorm))

goal (1 subgoal):
 1. \<And>a Snorm. \<lbrakk>\<lbrakk>is_ortho_set (set Snorm); distinct Snorm\<rbrakk> \<Longrightarrow> sum proj (set Snorm) = Proj (ccspan (set Snorm)); is_ortho_set (set (a # Snorm)); distinct (a # Snorm)\<rbrakk> \<Longrightarrow> sum proj (set (a # Snorm)) = Proj (ccspan (set (a # Snorm)))
[PROOF STEP]
have "\<dots> = Proj (ccspan ({a} \<union> set Snorm))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj a + Proj (ccspan (set Snorm)) = Proj (ccspan ({a} \<union> set Snorm))
[PROOF STEP]
apply (rule Proj_orthog_ccspan_union[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> {a}; y \<in> set Snorm\<rbrakk> \<Longrightarrow> is_orthogonal x y
[PROOF STEP]
by (metis Cons.prems(1) \<open>a \<notin> set Snorm\<close> is_ortho_set_def list.set_intros(1) list.set_intros(2) singleton_iff)
[PROOF STATE]
proof (state)
this:
proj a + Proj (ccspan (set Snorm)) = Proj (ccspan ({a} \<union> set Snorm))

goal (1 subgoal):
 1. \<And>a Snorm. \<lbrakk>\<lbrakk>is_ortho_set (set Snorm); distinct Snorm\<rbrakk> \<Longrightarrow> sum proj (set Snorm) = Proj (ccspan (set Snorm)); is_ortho_set (set (a # Snorm)); distinct (a # Snorm)\<rbrakk> \<Longrightarrow> sum proj (set (a # Snorm)) = Proj (ccspan (set (a # Snorm)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum proj (set (a # Snorm)) = Proj (ccspan ({a} \<union> set Snorm))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sum proj (set (a # Snorm)) = Proj (ccspan ({a} \<union> set Snorm))

goal (1 subgoal):
 1. sum proj (set (a # Snorm)) = Proj (ccspan (set (a # Snorm)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum proj (set (a # Snorm)) = Proj (ccspan (set (a # Snorm)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (sum proj (set Snorm)) = mat_of_cblinfun (Proj (ccspan (set Snorm)))

goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (sum proj (set Snorm)) = mat_of_cblinfun (Proj (ccspan (set Snorm)))

goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
have "\<dots> = mat_of_cblinfun (Proj (ccspan (set S)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (Proj (ccspan (set Snorm))) = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
unfolding Span_Snorm
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (Proj (ccspan (set S))) = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (Proj (ccspan (set Snorm))) = mat_of_cblinfun (Proj (ccspan (set S)))

goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (Proj (ccspan (set S)))

goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
mk_projector_orthog d (map vec_of_basis_enum S) = mat_of_cblinfun (Proj (ccspan (set S)))

goal:
No subgoals!
[PROOF STEP]
qed