Theory Cblinfun_Matrix

section Cblinfun_Matrix› -- Matrix representation of bounded operators›

theory Cblinfun_Matrix
  imports
    Complex_L2

    "Jordan_Normal_Form.Gram_Schmidt"
    "HOL-Analysis.Starlike"
    "Complex_Bounded_Operators.Extra_Jordan_Normal_Form"
begin

hide_const (open) Order.bottom Order.top
hide_type (open) Finite_Cartesian_Product.vec
hide_const (open) Finite_Cartesian_Product.mat
hide_fact (open) Finite_Cartesian_Product.mat_def
hide_const (open) Finite_Cartesian_Product.vec
hide_fact (open) Finite_Cartesian_Product.vec_def
hide_const (open) Finite_Cartesian_Product.row
hide_fact (open) Finite_Cartesian_Product.row_def
no_notation Finite_Cartesian_Product.vec_nth (infixl "$" 90)

unbundle jnf_notation
unbundle cblinfun_notation

subsection ‹Isomorphism between vectors›

text ‹We define the canonical isomorphism between vectors in some complex vector space
  typ'a::basis_enum and the complex termn-dimensional vectors 
  (where termn is the dimension of typ'a).
  This is possible if typ'a, typ'b are of class classbasis_enum
  since that class fixes a finite canonical basis. Vector are represented using
  the typcomplex vec type from sessionJordan_Normal_Form.
  (The isomorphism will be called termvec_of_onb_basis below.)›

definition vec_of_basis_enum :: 'a::basis_enum  complex vec where
  ― ‹Maps termv to a typ'a vec represented in basis constcanonical_basis
  vec_of_basis_enum v = vec_of_list (map (crepresentation (set canonical_basis) v) canonical_basis)

lemma dim_vec_of_basis_enum'[simp]:
  dim_vec (vec_of_basis_enum (v::'a)) = length (canonical_basis::'a::basis_enum list)
  unfolding vec_of_basis_enum_def
  by simp

definition basis_enum_of_vec :: complex vec  'a::basis_enum where
  basis_enum_of_vec v =
    (if dim_vec v = length (canonical_basis :: 'a list)
     then sum_list (map2 (*C) (list_of_vec v) (canonical_basis :: 'a list))
     else 0)

lemma vec_of_basis_enum_inverse[simp]:
  fixes ψ :: "'a::basis_enum"
  shows  "basis_enum_of_vec (vec_of_basis_enum ψ) = ψ"
  unfolding vec_of_basis_enum_def basis_enum_of_vec_def
  unfolding list_vec zip_map1 zip_same_conv_map map_map
  apply (simp add: o_def)
  apply (subst sum.distinct_set_conv_list[symmetric], simp)
  apply (rule complex_vector.sum_representation_eq)
  using  is_generator_set by auto

lemma basis_enum_of_vec_inverse[simp]:
  fixes v :: "complex vec"
  defines "n  length (canonical_basis :: 'a::basis_enum list)"
  assumes f1: "dim_vec v = n"
  shows "vec_of_basis_enum ((basis_enum_of_vec v)::'a) = v"
proof (rule eq_vecI)
  show dim_vec (vec_of_basis_enum (basis_enum_of_vec v :: 'a)) = dim_vec v
    by (auto simp: vec_of_basis_enum_def f1 n_def)
next
  fix j assume j_v: j < dim_vec v
  define w where "w = list_of_vec v"
  define basis where "basis = (canonical_basis::'a list)"
  have [simp]: "length w = n" "length basis = n" dim_vec v = n length (canonical_basis::'a list) = n
    j < n
    using j_v by (auto simp: f1 basis_def w_def n_def)
  have [simp]: cindependent (set basis) cspan (set basis) = UNIV
    by (auto simp: basis_def is_cindependent_set is_generator_set)

  have vec_of_basis_enum ((basis_enum_of_vec v)::'a) $ j
       = map (crepresentation (set basis) (sum_list (map2 (*C) w basis))) basis ! j
    by (auto simp: vec_of_list_index vec_of_basis_enum_def basis_enum_of_vec_def simp flip: w_def basis_def)
  also have  = crepresentation (set basis) (sum_list (map2 (*C) w basis)) (basis!j)
    by simp
  also have  = crepresentation (set basis) (i<n. (w!i) *C (basis!i)) (basis!j)
    by (auto simp: sum_list_sum_nth atLeast0LessThan)
  also have  = (i<n. (w!i) *C crepresentation (set basis) (basis!i) (basis!j))
    by (auto simp: complex_vector.representation_sum complex_vector.representation_scale)
  also have  = w!j
    apply (subst sum_single[where i=j])
      apply (auto simp: complex_vector.representation_basis)
    using j < n length basis = n basis_def distinct_canonical_basis nth_eq_iff_index_eq by blast
  also have  = v $ j
    by (simp add: w_def)
  finally show vec_of_basis_enum (basis_enum_of_vec v :: 'a) $ j = v $ j
    by -
qed

lemma basis_enum_eq_vec_of_basis_enumI:
  fixes a b :: "_::basis_enum"
  assumes "vec_of_basis_enum a = vec_of_basis_enum b"
  shows "a = b"
  by (metis assms vec_of_basis_enum_inverse)

lemma vec_of_basis_enum_carrier_vec[simp]: vec_of_basis_enum v  carrier_vec (canonical_basis_length TYPE('a)) for v :: 'a::basis_enum
  apply (simp only: dim_vec_of_basis_enum' carrier_vec_def vec_of_basis_enum_def)
  by (simp add: canonical_basis_length)

lemma vec_of_basis_enum_inj: "inj vec_of_basis_enum"
  by (simp add: basis_enum_eq_vec_of_basis_enumI injI)

lemma basis_enum_of_vec_inj: "inj_on (basis_enum_of_vec :: complex vec  'a)
      (carrier_vec (length (canonical_basis :: 'a::{basis_enum,complex_normed_vector} list)))"
  by (metis basis_enum_of_vec_inverse carrier_dim_vec inj_on_inverseI)

subsection ‹Operations on vectors›

lemma basis_enum_of_vec_add:
  assumes [simp]: dim_vec v1 = length (canonical_basis :: 'a::basis_enum list)
    dim_vec v2 = length (canonical_basis :: 'a list)
  shows ((basis_enum_of_vec (v1 + v2)) :: 'a) = basis_enum_of_vec v1 + basis_enum_of_vec v2
proof -
  have length (list_of_vec v1) = length (list_of_vec v2) and length (list_of_vec v2) = length (canonical_basis :: 'a list)
    by simp_all
  then have sum_list (map2 (*C) (map2 (+) (list_of_vec v1) (list_of_vec v2)) (canonical_basis::'a list))
    = sum_list (map2 (*C) (list_of_vec v1) canonical_basis) + sum_list (map2 (*C) (list_of_vec v2) canonical_basis)
    apply (induction rule: list_induct3)
    by (auto simp: scaleC_add_left)
  then show ?thesis
    using assms by (auto simp: basis_enum_of_vec_def list_of_vec_plus)
qed

lemma basis_enum_of_vec_mult:
  assumes [simp]: dim_vec v = length (canonical_basis :: 'a::basis_enum list)
  shows ((basis_enum_of_vec (c v v)) :: 'a) =  c *C basis_enum_of_vec v
proof -
  have *: monoid_add_hom ((*C) c :: 'a  _)
    by (simp add: monoid_add_hom_def plus_hom.intro scaleC_add_right semigroup_add_hom.intro zero_hom.intro)
  show ?thesis
    apply (auto simp: basis_enum_of_vec_def list_of_vec_mult map_zip_map
        monoid_add_hom.hom_sum_list[OF *])
    by (metis case_prod_unfold comp_apply scaleC_scaleC)
qed

lemma vec_of_basis_enum_add:
  vec_of_basis_enum (a + b) = vec_of_basis_enum a + vec_of_basis_enum b
  by (auto simp: vec_of_basis_enum_def complex_vector.representation_add)

lemma vec_of_basis_enum_scaleC:
  "vec_of_basis_enum (c *C b) = c v (vec_of_basis_enum b)"
  by (auto simp: vec_of_basis_enum_def complex_vector.representation_scale)

lemma vec_of_basis_enum_scaleR:
  "vec_of_basis_enum (r *R b) = complex_of_real r v (vec_of_basis_enum b)"
  by (simp add: scaleR_scaleC vec_of_basis_enum_scaleC)

lemma vec_of_basis_enum_uminus:
  "vec_of_basis_enum (- b2) = - vec_of_basis_enum b2"
  unfolding scaleC_minus1_left[symmetric, of b2]
  unfolding scaleC_minus1_left_vec[symmetric]
  by (rule vec_of_basis_enum_scaleC)

lemma vec_of_basis_enum_minus:
  "vec_of_basis_enum (b1 - b2) = vec_of_basis_enum b1 - vec_of_basis_enum b2"
  by (metis (mono_tags, opaque_lifting) carrier_vec_dim_vec diff_conv_add_uminus diff_zero index_add_vec(2) minus_add_uminus_vec vec_of_basis_enum_add vec_of_basis_enum_uminus)

lemma cinner_basis_enum_of_vec:
  defines "n  length (canonical_basis :: 'a::onb_enum list)"
  assumes [simp]: "dim_vec x = n" "dim_vec y = n"
  shows  "(basis_enum_of_vec x :: 'a) C basis_enum_of_vec y = y ∙c x"
proof -
  have (basis_enum_of_vec x :: 'a) C basis_enum_of_vec y
    = (i<n. x$i *C canonical_basis ! i :: 'a) C (i<n. y$i *C canonical_basis ! i)
    by (auto simp: basis_enum_of_vec_def sum_list_sum_nth atLeast0LessThan simp flip: n_def)
  also have  = (i<n. j<n. cnj (x$i) *C y$j *C ((canonical_basis ! i :: 'a) C (canonical_basis ! j)))
    apply (subst cinner_sum_left)
    apply (subst cinner_sum_right)
    by (auto simp: mult_ac)
  also have  = (i<n. j<n. cnj (x$i) *C y$j *C (if i=j then 1 else 0))
    apply (rule sum.cong[OF refl])
    apply (rule sum.cong[OF refl])
    by (auto simp: cinner_canonical_basis n_def)
  also have  = (i<n. cnj (x$i) *C y$i)
    apply (rule sum.cong[OF refl])
    apply (subst sum_single)
    by auto
  also have  = y ∙c x
    by (smt (z3) assms(2) complex_scaleC_def conjugate_complex_def dim_vec_conjugate lessThan_atLeast0 lessThan_iff mult.commute scalar_prod_def sum.cong vec_index_conjugate)
  finally show ?thesis
    by -
qed

lemma cscalar_prod_vec_of_basis_enum: "cscalar_prod (vec_of_basis_enum φ) (vec_of_basis_enum ψ) = cinner ψ φ"
  for ψ :: "'a::onb_enum"
  apply (subst cinner_basis_enum_of_vec[symmetric, where 'a='a])
  by simp_all

definition norm_vec ψ = sqrt ( i  {0 ..< dim_vec ψ}. let z = vec_index ψ i in (Re z)2 + (Im z)2)

lemma norm_vec_of_basis_enum: norm ψ = norm_vec (vec_of_basis_enum ψ) for ψ :: "'a::onb_enum"
proof -
  have "norm ψ = sqrt (cmod (i = 0..<dim_vec (vec_of_basis_enum ψ).
            vec_of_basis_enum ψ $ i * conjugate (vec_of_basis_enum ψ) $ i))"
    unfolding norm_eq_sqrt_cinner[where 'a='a] cscalar_prod_vec_of_basis_enum[symmetric] scalar_prod_def dim_vec_conjugate
    by rule
  also have " = sqrt (cmod (x = 0..<dim_vec (vec_of_basis_enum ψ).
                    let z = vec_of_basis_enum ψ $ x in (Re z)2 + (Im z)2))"
    apply (subst sum.cong, rule refl)
     apply (subst vec_index_conjugate)
    by (auto simp: Let_def complex_mult_cnj)
  also have " = norm_vec (vec_of_basis_enum ψ)"
    unfolding Let_def norm_of_real norm_vec_def
    apply (subst abs_of_nonneg)
     apply (rule sum_nonneg)
    by auto
  finally show ?thesis
    by -
qed

lemma basis_enum_of_vec_unit_vec:
  defines "basis  (canonical_basis::'a::basis_enum list)"
    and "n  length (canonical_basis :: 'a list)"
  assumes a3: "i < n"
  shows "basis_enum_of_vec (unit_vec n i) = basis!i"
proof-
  define L::"complex list" where "L = list_of_vec (unit_vec n i)"
  define I::"nat list" where "I = [0..<n]"
  have "length L = n"
    by (simp add: L_def)
  moreover have "length basis = n"
    by (simp add: basis_def n_def)
  ultimately have "map2 (*C) L basis = map (λj. L!j *C basis!j) I"
    by (simp add: I_def list_eq_iff_nth_eq)
  hence "sum_list (map2 (*C) L basis) = sum_list (map (λj. L!j *C basis!j) I)"
    by simp
  also have " = sum (λj. L!j *C basis!j) {0..n-1}"
  proof-
    have "set I = {0..n-1}"
      using I_def a3 by auto
    thus ?thesis
      using Groups_List.sum_code[where xs = I and g = "(λj. L!j *C basis!j)"]
      by (simp add: I_def)
  qed
  also have " = sum (λj. (list_of_vec (unit_vec n i))!j *C basis!j) {0..n-1}"
    unfolding L_def by blast
  finally have "sum_list (map2 (*C) (list_of_vec (unit_vec n i)) basis)
       = sum (λj. (list_of_vec (unit_vec n i))!j *C basis!j) {0..n-1}"
    using L_def by blast
  also have " = basis ! i"
  proof-
    have "(j = 0..n - 1. list_of_vec (unit_vec n i) ! j *C basis ! j) =
          (j  {0..n - 1}. list_of_vec (unit_vec n i) ! j *C basis ! j)"
      by simp
    also have " = list_of_vec (unit_vec n i) ! i *C basis ! i
               + (j  {0..n - 1}-{i}. list_of_vec (unit_vec n i) ! j *C basis ! j)"
    proof-
      define a where "a j = list_of_vec (unit_vec n i) ! j *C basis ! j" for j
      define S where "S = {0..n - 1}"
      have "finite S"
        by (simp add: S_def)
      hence "(j  insert i S. a j) = a i + (jS-{i}. a j)"
        using Groups_Big.comm_monoid_add_class.sum.insert_remove
        by auto
      moreover have "S-{i} = {0..n-1}-{i}"
        unfolding S_def
        by blast
      moreover have "insert i S = {0..n-1}"
        using S_def Suc_diff_1 a3 atLeastAtMost_iff diff_is_0_eq' le_SucE le_numeral_extra(4)
          less_imp_le not_gr_zero
        by fastforce
      ultimately show ?thesis
        using a  λj. list_of_vec (unit_vec n i) ! j *C basis ! j
        by simp
    qed
    also have " = list_of_vec (unit_vec n i) ! i *C basis ! i"
    proof-
      have "j  {0..n - 1}-{i}  list_of_vec (unit_vec n i) ! j = 0"
        for j
        using a3 atMost_atLeast0 atMost_iff diff_Suc_less index_unit_vec(1) le_less_trans
          list_of_vec_index member_remove zero_le by fastforce
      hence "j  {0..n - 1}-{i}  list_of_vec (unit_vec n i) ! j *C basis ! j = 0"
        for j
        by auto
      hence "(j  {0..n - 1}-{i}. list_of_vec (unit_vec n i) ! j *C basis ! j) = 0"
        by (simp add: j. j  {0..n - 1} - {i}  list_of_vec (unit_vec n i) ! j *C basis ! j = 0)
      thus ?thesis by simp
    qed
    also have " = basis ! i"
      by (simp add: a3)
    finally show ?thesis
      using (j = 0..n - 1. list_of_vec (unit_vec n i) ! j *C basis ! j)
             = list_of_vec (unit_vec n i) ! i *C basis ! i + (j{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *C basis ! j)
        list_of_vec (unit_vec n i) ! i *C basis ! i + (j{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *C basis ! j)
           = list_of_vec (unit_vec n i) ! i *C basis ! i
        list_of_vec (unit_vec n i) ! i *C basis ! i = basis ! i
      by auto
  qed
  finally have "sum_list (map2 (*C) (list_of_vec (unit_vec n i)) basis)
      = basis ! i"
    by (simp add: assms)
  hence "sum_list (map2 scaleC (list_of_vec (unit_vec n i)) (canonical_basis::'a list))
      = (canonical_basis::'a list) ! i"
    by (simp add: assms)
  thus ?thesis
    unfolding basis_enum_of_vec_def
    by (simp add: assms)
qed

lemma vec_of_basis_enum_ket:
  "vec_of_basis_enum (ket i) = unit_vec (CARD('a)) (enum_idx i)"
  for i::"'a::enum"
proof-
  have "dim_vec (vec_of_basis_enum (ket i))
      = dim_vec (unit_vec (CARD('a)) (enum_idx i))"
  proof-
    have "dim_vec (unit_vec (CARD('a)) (enum_idx i))
      = CARD('a)"
      by simp
    moreover have "dim_vec (vec_of_basis_enum (ket i)) = CARD('a)"
      unfolding vec_of_basis_enum_def vec_of_basis_enum_def by auto
    ultimately show ?thesis by simp
  qed
  moreover have "vec_of_basis_enum (ket i) $ j =
    (unit_vec (CARD('a)) (enum_idx i)) $ j"
    if "j < dim_vec (vec_of_basis_enum (ket i))"
    for j
  proof-
    have j_bound: "j < length (canonical_basis::'a ell2 list)"
      by (metis dim_vec_of_basis_enum' that)
    have y1: "cindependent (set (canonical_basis::'a ell2 list))"
      using is_cindependent_set by blast
    have y2: "canonical_basis ! j  set (canonical_basis::'a ell2 list)"
      using j_bound by auto
    have p1: "enum_class.enum ! enum_idx i = i"
      using enum_idx_correct by blast
    moreover have p2: "(canonical_basis::'a ell2 list) ! t  = ket ((enum_class.enum::'a list) ! t)"
      if "t < length (enum_class.enum::'a list)"
      for t
      unfolding canonical_basis_ell2_def
      using that by auto
    moreover have p3: "enum_idx i < length (enum_class.enum::'a list)"
    proof-
      have "set (enum_class.enum::'a list) = UNIV"
        using UNIV_enum by blast
      hence "i  set (enum_class.enum::'a list)"
        by blast
      thus ?thesis
        unfolding enum_idx_def
        by (metis index_of_bound length_greater_0_conv length_pos_if_in_set)
    qed
    ultimately have p4: "(canonical_basis::'a ell2 list) ! (enum_idx i)  = ket i"
      by auto
    have "enum_idx i < length (enum_class.enum::'a list)"
      using p3
      by auto
    moreover have "length (enum_class.enum::'a list) = dim_vec (vec_of_basis_enum (ket i))"
      unfolding vec_of_basis_enum_def canonical_basis_ell2_def
      using dim_vec_of_basis_enum'[where v = "ket i"]
      unfolding canonical_basis_ell2_def by simp
    ultimately have enum_i_dim_vec: "enum_idx i < dim_vec (unit_vec (CARD('a)) (enum_idx i))"
      using dim_vec (vec_of_basis_enum (ket i)) = dim_vec (unit_vec (CARD('a)) (enum_idx i)) by auto
    hence r1: "(unit_vec (CARD('a)) (enum_idx i)) $ j
        = (if enum_idx i = j then 1 else 0)"
      using dim_vec (vec_of_basis_enum (ket i)) = dim_vec (unit_vec (CARD('a)) (enum_idx i)) that by auto
    moreover have "vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)"
    proof(cases "enum_idx i = j")
      case True
      have "crepresentation (set (canonical_basis::'a ell2 list))
          ((canonical_basis::'a ell2 list) ! j) ((canonical_basis::'a ell2 list) ! j) = 1"
        using y1 y2 complex_vector.representation_basis[where
            basis = "set (canonical_basis::'a ell2 list)"
            and b = "(canonical_basis::'a ell2 list) ! j"]
        by smt

      hence "vec_of_basis_enum ((canonical_basis::'a ell2 list) ! j) $ j = 1"
        unfolding vec_of_basis_enum_def
        by (metis j_bound nth_map vec_of_list_index)
      hence "vec_of_basis_enum ((canonical_basis::'a ell2 list) ! (enum_idx i))
            $ enum_idx i = 1"
        using True by simp
      hence "vec_of_basis_enum (ket i) $ enum_idx i = 1"
        using p4
        by simp
      thus ?thesis using True unfolding vec_of_basis_enum_def by auto
    next
      case False
      have "crepresentation (set (canonical_basis::'a ell2 list))
          ((canonical_basis::'a ell2 list) ! (enum_idx i)) ((canonical_basis::'a ell2 list) ! j) = 0"
        using y1 y2 complex_vector.representation_basis[where
            basis = "set (canonical_basis::'a ell2 list)"
            and b = "(canonical_basis::'a ell2 list) ! j"]
        by (metis (mono_tags, opaque_lifting) False enum_i_dim_vec basis_enum_of_vec_inverse
            basis_enum_of_vec_unit_vec canonical_basis_length_ell2 index_unit_vec(3) j_bound
            list_of_vec_index list_vec nth_map r1 vec_of_basis_enum_def)
      hence "vec_of_basis_enum ((canonical_basis::'a ell2 list) ! (enum_idx i)) $ j = 0"
        unfolding vec_of_basis_enum_def by (smt j_bound nth_map vec_of_list_index)
      hence "vec_of_basis_enum ((canonical_basis::'a ell2 list) ! (enum_idx i)) $ j = 0"
        by auto
      hence "vec_of_basis_enum (ket i) $ j = 0"
        using p4
        by simp
      thus ?thesis using False unfolding vec_of_basis_enum_def by simp
    qed
    ultimately show ?thesis by auto
  qed
  ultimately show ?thesis
    using Matrix.eq_vecI
    by auto
qed

lemma vec_of_basis_enum_zero:
  defines "nA  length (canonical_basis :: 'a::basis_enum list)"
  shows "vec_of_basis_enum (0::'a) = 0v nA"
  by (metis assms carrier_vecI dim_vec_of_basis_enum' minus_cancel_vec right_minus_eq vec_of_basis_enum_minus)

lemma (in complex_vec_space) vec_of_basis_enum_cspan:
  fixes X :: "'a::basis_enum set"
  assumes "length (canonical_basis :: 'a list) = n"
  shows "vec_of_basis_enum ` cspan X = span (vec_of_basis_enum ` X)"
proof -
  have carrier: "vec_of_basis_enum ` X  carrier_vec n"
    by (metis assms carrier_vecI dim_vec_of_basis_enum' image_subsetI)
  have lincomb_sum: "lincomb c A = vec_of_basis_enum (bB. c' b *C b)"
    if B_def: "B = basis_enum_of_vec ` A" and finite A
      and AX: "A  vec_of_basis_enum ` X" and c'_def: "b. c' b = c (vec_of_basis_enum b)"
    for c c' A and B::"'a set"
    unfolding B_def using finite A AX
  proof induction
    case empty
    then show ?case
      by (simp add: assms vec_of_basis_enum_zero)
  next
    case (insert x F)
    then have IH: "lincomb c F = vec_of_basis_enum (bbasis_enum_of_vec ` F. c' b *C b)"
      (is "_ = ?sum")
      by simp
    have xx: "vec_of_basis_enum (basis_enum_of_vec x :: 'a) = x"
      apply (rule basis_enum_of_vec_inverse)
      using assms carrier carrier_vecD insert.prems by auto
    have "lincomb c (insert x F) = c x v x + lincomb c F"
      apply (rule lincomb_insert2)
      using insert.hyps insert.prems carrier by auto
    also have "c x v x = vec_of_basis_enum (c' (basis_enum_of_vec x) *C (basis_enum_of_vec x :: 'a))"
      by (simp add: xx vec_of_basis_enum_scaleC c'_def)
    also note IH
    also have
      "vec_of_basis_enum (c' (basis_enum_of_vec x) *C (basis_enum_of_vec x :: 'a)) + ?sum
          = vec_of_basis_enum (bbasis_enum_of_vec ` insert x F. c' b *C b)"
      apply simp apply (rule sym)
      apply (subst sum.insert)
      using finite F x  F dim_vec_of_basis_enum' insert.prems
        vec_of_basis_enum_add c'_def by auto
    finally show ?case
      by -
  qed

  show ?thesis
  proof auto
    fix x assume "x  local.span (vec_of_basis_enum ` X)"
    then obtain c A where xA: "x = lincomb c A" and "finite A" and AX: "A  vec_of_basis_enum ` X"
      unfolding span_def by auto
    define B::"'a set" and c' where "B = basis_enum_of_vec ` A"
      and "c' b = c (vec_of_basis_enum b)" for b::'a
    note xA
    also have "lincomb c A = vec_of_basis_enum (bB. c' b *C b)"
      using B_def finite A AX c'_def by (rule lincomb_sum)
    also have "  vec_of_basis_enum ` cspan X"
      unfolding complex_vector.span_explicit
      apply (rule imageI) apply (rule CollectI)
      apply (rule exI) apply (rule exI)
      using finite A AX by (auto simp: B_def)
    finally show "x  vec_of_basis_enum ` cspan X"
      by -
  next
    fix x assume "x  cspan X"
    then obtain c' B where x: "x = (bB. c' b *C b)" and "finite B" and BX: "B  X"
      unfolding complex_vector.span_explicit by auto
    define A and c where "A = vec_of_basis_enum ` B"
      and "c b = c' (basis_enum_of_vec b)" for b
    have "vec_of_basis_enum x = vec_of_basis_enum (bB. c' b *C b)"
      using x by simp
    also have " = lincomb c A"
      apply (rule lincomb_sum[symmetric])
      unfolding A_def c_def using BX finite B
      by (auto simp: image_image)
    also have "  span (vec_of_basis_enum ` X)"
      unfolding span_def apply (rule CollectI)
      apply (rule exI, rule exI)
      unfolding A_def using finite B BX by auto
    finally show "vec_of_basis_enum x  local.span (vec_of_basis_enum ` X)"
      by -
  qed
qed

lemma (in complex_vec_space) basis_enum_of_vec_span:
  assumes "length (canonical_basis :: 'a list) = n"
  assumes "Y  carrier_vec n"
  shows "basis_enum_of_vec ` local.span Y = cspan (basis_enum_of_vec ` Y :: 'a::basis_enum set)"
proof -
  define X::"'a set" where "X = basis_enum_of_vec ` Y"
  then have "cspan (basis_enum_of_vec ` Y :: 'a set) = basis_enum_of_vec ` vec_of_basis_enum ` cspan X"
    by (simp add: image_image)
  also have " = basis_enum_of_vec ` local.span (vec_of_basis_enum ` X)"
    apply (subst vec_of_basis_enum_cspan)
    using assms by simp_all
  also have "vec_of_basis_enum ` X = Y"
    unfolding X_def image_image
    apply (rule image_cong[where g=id and M=Y and N=Y, simplified])
    using assms(1) assms(2) by auto
  finally show ?thesis
    by simp
qed

lemma vec_of_basis_enum_canonical_basis:
  assumes "i < length (canonical_basis :: 'a list)"
  shows "vec_of_basis_enum (canonical_basis!i :: 'a)
       = unit_vec (length (canonical_basis :: 'a::basis_enum list)) i"
  by (metis assms basis_enum_of_vec_inverse basis_enum_of_vec_unit_vec index_unit_vec(3))

lemma vec_of_basis_enum_times:
  fixes ψ φ :: "'a::one_dim"
  shows "vec_of_basis_enum (ψ * φ)
   = vec_of_list [vec_index (vec_of_basis_enum ψ) 0 * vec_index (vec_of_basis_enum φ) 0]"
proof -
  have [simp]: crepresentation {1} x 1 = one_dim_iso x for x :: 'a
    apply (subst one_dim_scaleC_1[where x=x, symmetric])
    apply (subst complex_vector.representation_scale)
    by (auto simp add: complex_vector.span_base complex_vector.representation_basis)
  show ?thesis
    apply (rule eq_vecI)
    by (auto simp: vec_of_basis_enum_def)
qed

lemma vec_of_basis_enum_to_inverse:
  fixes ψ :: "'a::one_dim"
  shows "vec_of_basis_enum (inverse ψ) = vec_of_list [inverse (vec_index (vec_of_basis_enum ψ) 0)]"
proof -
  have [simp]: crepresentation {1} x 1 = one_dim_iso x for x :: 'a
    apply (subst one_dim_scaleC_1[where x=x, symmetric])
    apply (subst complex_vector.representation_scale)
    by (auto simp add: complex_vector.span_base complex_vector.representation_basis)
  show ?thesis
    apply (rule eq_vecI)
     apply (auto simp: vec_of_basis_enum_def)
    by (metis complex_vector.scale_cancel_right one_dim_inverse one_dim_scaleC_1 zero_neq_one)
qed

lemma vec_of_basis_enum_divide:
  fixes ψ φ :: "'a::one_dim"
  shows "vec_of_basis_enum (ψ / φ)
   = vec_of_list [vec_index (vec_of_basis_enum ψ) 0 / vec_index (vec_of_basis_enum φ) 0]"
  by (simp add: divide_inverse vec_of_basis_enum_to_inverse vec_of_basis_enum_times)

lemma vec_of_basis_enum_1: "vec_of_basis_enum (1 :: 'a::one_dim) = vec_of_list [1]"
proof -
  have [simp]: crepresentation {1} x 1 = one_dim_iso x for x :: 'a
    apply (subst one_dim_scaleC_1[where x=x, symmetric])
    apply (subst complex_vector.representation_scale)
    by (auto simp add: complex_vector.span_base complex_vector.representation_basis)
  show ?thesis
    apply (rule eq_vecI)
    by (auto simp: vec_of_basis_enum_def)
qed

lemma vec_of_basis_enum_ell2_component:
  fixes ψ :: 'a::enum ell2
  assumes [simp]: i < CARD('a)
  shows vec_of_basis_enum ψ $ i = Rep_ell2 ψ (Enum.enum ! i)
proof -
  let ?i = Enum.enum ! i
  have Rep_ell2 ψ (Enum.enum ! i) = ket ?i C ψ
    by (simp add: cinner_ket_left)
  also have  = vec_of_basis_enum ψ ∙c vec_of_basis_enum (ket ?i :: 'a ell2)
    by (rule cscalar_prod_vec_of_basis_enum[symmetric])
  also have  = vec_of_basis_enum ψ ∙c unit_vec (CARD('a)) i
    by (simp add: vec_of_basis_enum_ket enum_idx_enum)
  also have  = vec_of_basis_enum ψ  unit_vec (CARD('a)) i
    by (smt (verit, best) assms carrier_vecI conjugate_conjugate_sprod conjugate_id conjugate_vec_sprod_comm dim_vec_conjugate eq_vecI index_unit_vec(3) scalar_prod_left_unit vec_index_conjugate)
  also have  = vec_of_basis_enum ψ $ i
    by simp
  finally show ?thesis
    by simp
qed


lemma corthogonal_vec_of_basis_enum:
  fixes S :: "'a::onb_enum list"
  shows "corthogonal (map vec_of_basis_enum S)  is_ortho_set (set S)  distinct S"
proof auto
  assume assm: corthogonal (map vec_of_basis_enum S)
  then show is_ortho_set (set S)
    by (smt (verit, ccfv_SIG) cinner_eq_zero_iff corthogonal_def cscalar_prod_vec_of_basis_enum in_set_conv_nth is_ortho_set_def length_map nth_map)
  show distinct S
    using assm corthogonal_distinct distinct_map by blast
next
  assume is_ortho_set (set S) and distinct S
  then show corthogonal (map vec_of_basis_enum S)
    by (smt (verit, ccfv_threshold) cinner_eq_zero_iff corthogonalI cscalar_prod_vec_of_basis_enum is_ortho_set_def length_map length_map nth_eq_iff_index_eq nth_map nth_map nth_mem nth_mem)
qed

subsection ‹Isomorphism between bounded linear functions and matrices›


text ‹We define the canonical isomorphism between typ'a::basis_enum CL'b::basis_enum
  and the complex termn*m-matrices (where n,m are the dimensions of typ'a, typ'b,
  respectively). This is possible if typ'a, typ'b are of class classbasis_enum
  since that class fixes a finite canonical basis. Matrices are represented using
  the typcomplex mat type from sessionJordan_Normal_Form.
  (The isomorphism will be called termmat_of_cblinfun below.)›

definition mat_of_cblinfun :: 'a::{basis_enum,complex_normed_vector} CL'b::{basis_enum,complex_normed_vector}  complex mat where
  mat_of_cblinfun f =
    mat (length (canonical_basis :: 'b list)) (length (canonical_basis :: 'a list)) (
    λ (i, j). crepresentation (set (canonical_basis::'b list)) (f *V ((canonical_basis::'a list)!j)) ((canonical_basis::'b list)!i))
  for f

lift_definition cblinfun_of_mat :: complex mat  'a::{basis_enum,complex_normed_vector} CL'b::{basis_enum,complex_normed_vector} is
  λM. if Mcarrier_mat (length (canonical_basis :: 'b list)) (length (canonical_basis :: 'a list))
           then λv. basis_enum_of_vec (M *v vec_of_basis_enum v)
           else (λv. 0)
proof (intro bounded_clinear_finite_dim clinearI)
  fix M :: "complex mat"
  define m where "m = length (canonical_basis :: 'b list)"
  define n where "n = length (canonical_basis :: 'a list)"
  define f::"complex mat  'a  'b"
    where "f M = (if Mcarrier_mat m n
        then λv. basis_enum_of_vec (M *v vec_of_basis_enum (v::'a))
        else (λv. 0))"
    for M::"complex mat"

  show add: f M (b1 + b2) = f M b1 + f M b2 for b1 b2
    apply (auto simp: f_def)
    by (metis (mono_tags, lifting) carrier_matD(1) carrier_vec_dim_vec dim_mult_mat_vec dim_vec_of_basis_enum' m_def mult_add_distrib_mat_vec n_def basis_enum_of_vec_add vec_of_basis_enum_add)

  show scale: f M (c *C b) = c *C f M b for c b
    apply (auto simp: f_def)
    by (metis carrier_matD(1) carrier_vec_dim_vec dim_mult_mat_vec dim_vec_of_basis_enum' m_def mult_mat_vec n_def basis_enum_of_vec_mult vec_of_basis_enum_scaleC)
qed

lemma cblinfun_of_mat_invalid: 
  assumes M  carrier_mat (canonical_basis_length TYPE('b::{basis_enum,complex_normed_vector})) (canonical_basis_length TYPE('a::{basis_enum,complex_normed_vector}))
  shows (cblinfun_of_mat M :: 'a CL 'b) = 0
  apply (transfer fixing: M)
  using assms by (simp add: canonical_basis_length)

lemma dim_row_mat_of_cblinfun[simp]: dim_row (mat_of_cblinfun (a::'a::{basis_enum,complex_normed_vector} CL 'b::{basis_enum,complex_normed_vector})) = canonical_basis_length TYPE('b)
  by (simp add: mat_of_cblinfun_def canonical_basis_length)

lemma dim_col_mat_of_cblinfun[simp]: dim_col (mat_of_cblinfun (a::'a::{basis_enum,complex_normed_vector} CL 'b::{basis_enum,complex_normed_vector})) = canonical_basis_length TYPE('a)
  by (simp add: mat_of_cblinfun_def canonical_basis_length)

lemma mat_of_cblinfun_ell2_carrier[simp]: mat_of_cblinfun (a::'a::{basis_enum,complex_normed_vector} CL 'b::{basis_enum,complex_normed_vector})  carrier_mat (canonical_basis_length TYPE('b)) (canonical_basis_length TYPE('a))
  by (auto intro!: carrier_matI)

lemma basis_enum_of_vec_cblinfun_apply:
  fixes M :: "complex mat"
  defines "nA  length (canonical_basis :: 'a::{basis_enum,complex_normed_vector} list)"
    and "nB  length (canonical_basis :: 'b::{basis_enum,complex_normed_vector} list)"
  assumes "M  carrier_mat nB nA" and "dim_vec x = nA"
  shows "basis_enum_of_vec (M *v x) = (cblinfun_of_mat M :: 'a CL 'b) *V basis_enum_of_vec x"
  by (metis assms basis_enum_of_vec_inverse cblinfun_of_mat.rep_eq)

lemma mat_of_cblinfun_cblinfun_apply:
  vec_of_basis_enum (F *V u) = mat_of_cblinfun F *v vec_of_basis_enum u
  for F::"'a::{basis_enum,complex_normed_vector} CL 'b::{basis_enum,complex_normed_vector}" and u::'a
proof (rule eq_vecI)
  show dim_vec (vec_of_basis_enum (F *V u)) = dim_vec (mat_of_cblinfun F *v vec_of_basis_enum u)
    by (simp add: dim_vec_of_basis_enum' mat_of_cblinfun_def)
next
  fix i
  define BasisA where "BasisA = (canonical_basis::'a list)"
  define BasisB where "BasisB = (canonical_basis::'b list)"
  define nA where "nA = length (canonical_basis :: 'a list)"
  define nB where "nB = length (canonical_basis :: 'b list)"
  assume i < dim_vec (mat_of_cblinfun F *v vec_of_basis_enum u)
  then have [simp]: i < nB
    by (simp add: mat_of_cblinfun_def nB_def)
  define v where v = BasisB ! i

  have dim_row_F[simp]: dim_row (mat_of_cblinfun F) = nB
    by (simp add: mat_of_cblinfun_def nB_def)
  have [simp]: length BasisB = nB
    by (simp add: nB_def BasisB_def)
  have [simp]: length BasisA = nA
    using BasisA_def nA_def by auto
  have [simp]: cindependent (set BasisA)
    using BasisA_def is_cindependent_set by auto
  have [simp]: cindependent (set BasisB)
    using BasisB_def is_cindependent_set by blast
  have [simp]: cspan (set BasisB) = UNIV
    by (simp add: BasisB_def is_generator_set)
  have [simp]: cspan (set BasisA) = UNIV
    by (simp add: BasisA_def is_generator_set)

  have (mat_of_cblinfun F *v vec_of_basis_enum u) $ i =
          (j = 0..<nA. row (mat_of_cblinfun F) i $ j * crepresentation (set BasisA) u (vec_of_list BasisA $ j))
    using dim_row_F by (auto simp: mult_mat_vec_def vec_of_basis_enum_def scalar_prod_def simp flip: BasisA_def)
  also have  = (j = 0..<nA. crepresentation (set BasisB) (F *V BasisA ! j) v
                                 * crepresentation (set BasisA) u (BasisA ! j))
    apply (rule sum.cong[OF refl])
    by (auto simp: vec_of_list_index mat_of_cblinfun_def scalar_prod_def v_def simp flip: BasisA_def BasisB_def)
  also have  = crepresentation (set BasisB) (F *V u) v (is (j=_..<_. ?lhs v j) = _)
  proof (rule complex_vector.representation_eqI[symmetric, THEN fun_cong])
    show cindependent (set BasisB) F *V u  cspan (set BasisB)
      by simp_all
    show only_basis: (j = 0..<nA. ?lhs b j)  0  b  set BasisB for b
      by (metis (mono_tags, lifting) complex_vector.representation_ne_zero mult_not_zero sum.not_neutral_contains_not_neutral)
    then show finite {b. (j = 0..<nA. ?lhs b j)  0}
      by (smt (z3) List.finite_set finite_subset mem_Collect_eq subsetI)
    have (b | (j = 0..<nA. ?lhs b j)  0. (j = 0..<nA. ?lhs b j) *C b) =
            (bset BasisB. (j = 0..<nA. ?lhs b j) *C b)
      apply (rule sum.mono_neutral_left)
      using only_basis by auto
    also have  = (bset BasisB. (aset BasisA. crepresentation (set BasisB) (F *V a) b * crepresentation (set BasisA) u a) *C b)
      apply (subst sum.reindex_bij_betw[where h=nth BasisA and T=set BasisA])
       apply (metis BasisA_def length BasisA = nA atLeast0LessThan bij_betw_nth distinct_canonical_basis)
      by simp
    also have  = (aset BasisA. crepresentation (set BasisA) u a *C (bset BasisB. crepresentation (set BasisB) (F *V a) b *C b))
      apply (simp add: scaleC_sum_left scaleC_sum_right)
      apply (subst sum.swap)
      by (metis (no_types, lifting) mult.commute sum.cong)
    also have  = (aset BasisA. crepresentation (set BasisA) u a *C (F *V a))
      apply (subst complex_vector.sum_representation_eq)
      by auto
    also have  = F *V (aset BasisA. crepresentation (set BasisA) u a *C a)
      by (simp flip: cblinfun.scaleC_right cblinfun.sum_right)
    also have  = F *V u
      apply (subst complex_vector.sum_representation_eq)
      by auto
    finally show (b | (j = 0..<nA. ?lhs b j)  0. (j = 0..<nA. ?lhs b j) *C b) = F *V u
      by auto
  qed
  also have crepresentation (set BasisB) (F *V u) v = vec_of_basis_enum (F *V u) $ i
    by (auto simp: vec_of_list_index vec_of_basis_enum_def v_def simp flip: BasisB_def)
  finally show vec_of_basis_enum (F *V u) $ i = (mat_of_cblinfun F *v vec_of_basis_enum u) $ i
    by simp
qed

lemma mat_of_cblinfun_inverse:
  "cblinfun_of_mat (mat_of_cblinfun B) = B"
  for B::"'a::{basis_enum,complex_normed_vector}  CL 'b::{basis_enum,complex_normed_vector}"
proof (rule cblinfun_eqI)
  fix x :: 'a define y where y = vec_of_basis_enum x
  then have cblinfun_of_mat (mat_of_cblinfun B) *V x = ((cblinfun_of_mat (mat_of_cblinfun B) :: 'aCL'b) *V basis_enum_of_vec y)
    by simp
  also have  = basis_enum_of_vec (mat_of_cblinfun B *v vec_of_basis_enum (basis_enum_of_vec y :: 'a))
    apply (transfer fixing: B)
    by (simp add: mat_of_cblinfun_def)
  also have  = basis_enum_of_vec (vec_of_basis_enum (B *V x))
    by (simp add: mat_of_cblinfun_cblinfun_apply y_def)
  also have  = B *V x
    by simp
  finally show cblinfun_of_mat (mat_of_cblinfun B) *V x = B *V x
    by -
qed

lemma mat_of_cblinfun_inj: "inj mat_of_cblinfun"
  by (metis inj_on_def mat_of_cblinfun_inverse)

lemma cblinfun_of_mat_inverse:
  fixes M::"complex mat"
  defines "nA  length (canonical_basis :: 'a::{basis_enum,complex_normed_vector} list)"
    and "nB  length (canonical_basis :: 'b::{basis_enum,complex_normed_vector} list)"
  assumes "M  carrier_mat nB nA"
  shows "mat_of_cblinfun (cblinfun_of_mat M :: 'a CL 'b) = M"
  by (smt (verit) assms(3) basis_enum_of_vec_inverse carrier_matD(1) carrier_vecD cblinfun_of_mat.rep_eq dim_mult_mat_vec eq_mat_on_vecI mat_carrier mat_of_cblinfun_def mat_of_cblinfun_cblinfun_apply nA_def nB_def)

lemma cblinfun_of_mat_inj: "inj_on (cblinfun_of_mat::complex mat  'a CL 'b)
      (carrier_mat (length (canonical_basis :: 'b::{basis_enum,complex_normed_vector} list))
                   (length (canonical_basis :: 'a::{basis_enum,complex_normed_vector} list)))"
  using cblinfun_of_mat_inverse
  by (metis inj_onI)

lemma cblinfun_eq_mat_of_cblinfunI:
  assumes "mat_of_cblinfun a = mat_of_cblinfun b"
  shows "a = b"
  by (metis assms mat_of_cblinfun_inverse)

subsection ‹Operations on matrices›

lemma cblinfun_of_mat_plus:
  defines "nA  length (canonical_basis :: 'a::{basis_enum,complex_normed_vector} list)"
    and "nB  length (canonical_basis :: 'b::{basis_enum,complex_normed_vector} list)"
  assumes [simp,intro]: "M  carrier_mat nB nA" and [simp,intro]: "N  carrier_mat nB nA"
  shows "(cblinfun_of_mat (M + N) :: 'a CL 'b) = ((cblinfun_of_mat M + cblinfun_of_mat N))"
proof -
  have [simp]: vec_of_basis_enum (v :: 'a)  carrier_vec nA for v
    by (auto simp add: carrier_dim_vec dim_vec_of_basis_enum' nA_def)
  have [simp]: dim_row M = nB dim_row N = nB
    using carrier_matD(1) by auto
  show ?thesis
    apply (transfer fixing: M N)
    by (auto intro!: ext simp add: add_mult_distrib_mat_vec nA_def[symmetric] nB_def[symmetric]
        add_mult_distrib_mat_vec[where nr=nB and nc=nA] basis_enum_of_vec_add)
qed

lemma mat_of_cblinfun_zero:
  "mat_of_cblinfun (0 :: ('a::{basis_enum,complex_normed_vector}  CL 'b::{basis_enum,complex_normed_vector}))
  = 0m (length (canonical_basis :: 'b list)) (length (canonical_basis :: 'a list))"
  unfolding mat_of_cblinfun_def
  by (auto simp: complex_vector.representation_zero)

lemma mat_of_cblinfun_plus:
  "mat_of_cblinfun (F + G) = mat_of_cblinfun F + mat_of_cblinfun G"
  for F G::"'a::{basis_enum,complex_normed_vector} CL'b::{basis_enum,complex_normed_vector}"
  by (auto simp add: mat_of_cblinfun_def cblinfun.add_left complex_vector.representation_add)

lemma mat_of_cblinfun_id:
  "mat_of_cblinfun (id_cblinfun :: ('a::{basis_enum,complex_normed_vector} CL'a)) = 1m (length (canonical_basis :: 'a list))"
  apply (rule eq_matI)
  by (auto simp: mat_of_cblinfun_def complex_vector.representation_basis is_cindependent_set nth_eq_iff_index_eq)

lemma mat_of_cblinfun_1:
  "mat_of_cblinfun (1 :: ('a::one_dim CL'b::one_dim)) = 1m 1"
  apply (rule eq_matI)
  by (auto simp: mat_of_cblinfun_def complex_vector.representation_basis nth_eq_iff_index_eq)

lemma mat_of_cblinfun_uminus:
  "mat_of_cblinfun (- M) = - mat_of_cblinfun M"
  for M::"'a::{basis_enum,complex_normed_vector} CL'b::{basis_enum,complex_normed_vector}"
proof-
  define nA where "nA = length (canonical_basis :: 'a list)"
  define nB where "nB = length (canonical_basis :: 'b list)"
  have M1: "mat_of_cblinfun M  carrier_mat nB nA"
    unfolding nB_def nA_def
    by (metis add.right_neutral add_carrier_mat mat_of_cblinfun_plus mat_of_cblinfun_zero nA_def
        nB_def zero_carrier_mat)
  have M2: "mat_of_cblinfun (-M)  carrier_mat nB nA"
    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)
  have "mat_of_cblinfun (M - M) =  0m nB nA"
    unfolding nA_def nB_def
    by (simp add: mat_of_cblinfun_zero)
  moreover have "mat_of_cblinfun (M - M) = mat_of_cblinfun M + mat_of_cblinfun (- M)"
    by (metis mat_of_cblinfun_plus pth_2)
  ultimately have "mat_of_cblinfun M + mat_of_cblinfun (- M) = 0m nB nA"
    by simp
  thus ?thesis
    using M1 M2
    by (smt add_uminus_minus_mat assoc_add_mat comm_add_mat left_add_zero_mat minus_r_inv_mat
        uminus_carrier_mat)
qed

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} CL 'b::{basis_enum,complex_normed_vector}" and N::"'a CL'b"
  by (smt (z3) add_uminus_minus_mat mat_of_cblinfun_uminus mat_carrier mat_of_cblinfun_def mat_of_cblinfun_plus pth_2)

lemma cblinfun_of_mat_uminus:
  defines "nA  length (canonical_basis :: 'a::{basis_enum,complex_normed_vector} list)"
    and "nB  length (canonical_basis :: 'b::{basis_enum,complex_normed_vector} list)"
  assumes "M  carrier_mat nB nA"
  shows "(cblinfun_of_mat (-M) :: 'a CL 'b) = - cblinfun_of_mat M"
  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)

lemma cblinfun_of_mat_minus:
  fixes M::"complex mat"
  defines "nA  length (canonical_basis :: 'a::{basis_enum,complex_normed_vector} list)"
    and "nB  length (canonical_basis :: 'b::{basis_enum,complex_normed_vector} list)"
  assumes "M  carrier_mat nB nA" and "N  carrier_mat nB nA"
  shows "(cblinfun_of_mat (M - N) :: 'a CL 'b) = cblinfun_of_mat M - cblinfun_of_mat N"
  by (metis assms add_uminus_minus_mat cblinfun_of_mat_plus cblinfun_of_mat_uminus pth_2 uminus_carrier_mat)

lemma cblinfun_of_mat_times:
  fixes M N ::"complex mat"
  defines "nA  length (canonical_basis :: 'a::{basis_enum,complex_normed_vector} list)"
    and "nB  length (canonical_basis :: 'b::{basis_enum,complex_normed_vector} list)"
    and "nC  length (canonical_basis :: 'c::{basis_enum,complex_normed_vector} list)"
  assumes a1: "M  carrier_mat nC nB" and a2: "N  carrier_mat nB nA"
  shows  "cblinfun_of_mat (M * N) = ((cblinfun_of_mat M)::'b CL'c) oCL ((cblinfun_of_mat N)::'a CL'b)"
proof -
  have b1: "((cblinfun_of_mat M)::'b CL'c) v = basis_enum_of_vec (M *v vec_of_basis_enum v)"
    for v
    by (metis assms(4) cblinfun_of_mat.rep_eq nB_def nC_def)
  have b2: "((cblinfun_of_mat N)::'a CL'b) v = basis_enum_of_vec (N *v vec_of_basis_enum v)"
    for v
    by (metis assms(5) cblinfun_of_mat.rep_eq nA_def nB_def)
  have b3: "((cblinfun_of_mat (M * N))::'a CL'c) v
       = basis_enum_of_vec ((M * N) *v vec_of_basis_enum v)"
    for v
    by (metis assms(4) assms(5) cblinfun_of_mat.rep_eq mult_carrier_mat nA_def nC_def)
  have "(basis_enum_of_vec ((M * N) *v vec_of_basis_enum v)::'c)
      = (basis_enum_of_vec (M *v ( vec_of_basis_enum ( (basis_enum_of_vec (N *v vec_of_basis_enum v))::'b ))))"
    for v::'a
  proof-
    have c1: "vec_of_basis_enum (basis_enum_of_vec x :: 'b) = x"
      if "dim_vec x = nB"
      for x::"complex vec"
      using that unfolding nB_def
      by simp
    have c2: "vec_of_basis_enum v  carrier_vec nA"
      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)
    have "(M * N) *v vec_of_basis_enum v = M *v (N *v vec_of_basis_enum v)"
      using Matrix.assoc_mult_mat_vec a1 a2 c2 by blast
    hence "(basis_enum_of_vec ((M * N) *v vec_of_basis_enum v)::'c)
        = (basis_enum_of_vec (M *v (N *v vec_of_basis_enum v))::'c)"
      by simp
    also have " =
      (basis_enum_of_vec (M *v ( vec_of_basis_enum ( (basis_enum_of_vec (N *v vec_of_basis_enum v))::'b ))))"
      using c1 a2 by auto
    finally show ?thesis by simp
  qed
  thus ?thesis using b1 b2 b3
    by (simp add: cblinfun_eqI scaleC_cblinfun.rep_eq)
qed

lemma cblinfun_of_mat_adjoint:
  defines "nA  length (canonical_basis :: 'a::onb_enum list)"
    and "nB  length (canonical_basis :: 'b::onb_enum list)"
  fixes M:: "complex mat"
  assumes "M  carrier_mat nB nA"
  shows "((cblinfun_of_mat (mat_adjoint M)) :: 'b CL 'a) = (cblinfun_of_mat M)*"
proof (rule adjoint_eqI)
  show "(cblinfun_of_mat (mat_adjoint M) *V x) C y = x C (cblinfun_of_mat M *V y)"
    for x::'b and y::'a
  proof-
    define u where "u = vec_of_basis_enum x"
    define v where "v = vec_of_basis_enum y"
    have c1: "vec_of_basis_enum ((cblinfun_of_mat (mat_adjoint M) *V x)::'a) = (mat_adjoint M) *v u"
      unfolding u_def
      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)
    have c2: "(vec_of_basis_enum ((cblinfun_of_mat M *V y)::'b))
        = M *v v"
      by (metis assms(3) cblinfun_of_mat_inverse mat_of_cblinfun_cblinfun_apply nA_def nB_def v_def)
    have c3: "dim_vec v = nA"
      unfolding v_def nA_def vec_of_basis_enum_def
      by (simp add:)
    have c4: "dim_vec u = nB"
      unfolding u_def nB_def vec_of_basis_enum_def
      by (simp add:)
    have "v ∙c ((mat_adjoint M) *v u) = (M *v v) ∙c u"
      using c3 c4 cscalar_prod_adjoint assms(3) by blast
    hence "v ∙c (vec_of_basis_enum ((cblinfun_of_mat (mat_adjoint M) *V x)::'a))
        = (vec_of_basis_enum ((cblinfun_of_mat M *V y)::'b)) ∙c u"
      using c1 c2 by simp
    thus "(cblinfun_of_mat (mat_adjoint M) *V x) C y = x C (cblinfun_of_mat M *V y)"
      unfolding u_def v_def
      by (simp add: cscalar_prod_vec_of_basis_enum)
  qed
qed

lemma mat_of_cblinfun_compose:
  "mat_of_cblinfun (F oCL G) = mat_of_cblinfun F * mat_of_cblinfun G"
  for F::"'b::{basis_enum,complex_normed_vector} CL 'c::{basis_enum,complex_normed_vector}"
    and G::"'a::{basis_enum,complex_normed_vector}  CL 'b"
  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)

lemma mat_of_cblinfun_scaleC:
  "mat_of_cblinfun ((a::complex) *C F) = a m (mat_of_cblinfun F)"
  for F :: "'a::{basis_enum,complex_normed_vector} CL 'b::{basis_enum,complex_normed_vector}"
  by (auto simp add: complex_vector.representation_scale mat_of_cblinfun_def)

lemma mat_of_cblinfun_scaleR:
  "mat_of_cblinfun ((a::real) *R F) = (complex_of_real a) m (mat_of_cblinfun F)"
  unfolding scaleR_scaleC by (rule mat_of_cblinfun_scaleC)

lemma mat_of_cblinfun_adj:
  "mat_of_cblinfun (F*) = mat_adjoint (mat_of_cblinfun F)"
  for F :: "'a::onb_enum CL 'b::onb_enum"
  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)

lemma mat_of_cblinfun_vector_to_cblinfun:
  "mat_of_cblinfun (vector_to_cblinfun ψ)
       = mat_of_cols (length (canonical_basis :: 'a list)) [vec_of_basis_enum ψ]"
  for ψ::"'a::{basis_enum,complex_normed_vector}"
  by (auto simp: mat_of_cols_Cons_index_0 mat_of_cblinfun_def vec_of_basis_enum_def vec_of_list_index)

lemma mat_of_cblinfun_proj:
  fixes a::"'a::onb_enum"
  defines   "d  length (canonical_basis :: 'a list)"
    and "norm2  (vec_of_basis_enum a) ∙c (vec_of_basis_enum a)"
  shows  "mat_of_cblinfun (proj a) =
      1 / norm2 m (mat_of_cols d [vec_of_basis_enum a]
                 * mat_of_rows d [conjugate (vec_of_basis_enum a)])" (is _ = ?rhs)
proof (cases "a = 0")
  case False
  have norm2: norm2 = (norm a)2
    by (simp add: cscalar_prod_vec_of_basis_enum norm2_def cdot_square_norm[symmetric, simplified])
  have [simp]: vec_of_basis_enum a  carrier_vec d
    by (simp add: carrier_vecI d_def)

  have mat_of_cblinfun (proj a) = mat_of_cblinfun (proj (a /R norm a))
    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)
  also have  = mat_of_cblinfun (selfbutter (a /R norm a))
    apply (subst butterfly_eq_proj)
    by (auto simp add: False)
  also have  = 1/norm2 m mat_of_cblinfun (selfbutter a)
    apply (simp add: mat_of_cblinfun_scaleC norm2)
    by (simp add: inverse_eq_divide power2_eq_square)
  also have  = 1 / norm2 m (mat_of_cblinfun (vector_to_cblinfun a :: complex CL 'a) * mat_adjoint (mat_of_cblinfun (vector_to_cblinfun a :: complex CL 'a)))
    by (simp add: butterfly_def mat_of_cblinfun_compose mat_of_cblinfun_adj)
  also have  = ?rhs
    by (simp add: mat_of_cblinfun_vector_to_cblinfun mat_adjoint_def flip: d_def)
  finally show ?thesis
    by -
next
  case True
  show ?thesis
    apply (rule eq_matI)
    by (auto simp: True mat_of_cblinfun_zero vec_of_basis_enum_zero scalar_prod_def  mat_of_rows_index
        simp flip: d_def)
qed

lemma mat_of_cblinfun_ell2_component:
  fixes a :: 'a::enum ell2 CL 'b::enum ell2
  assumes [simp]: i < CARD('b) j < CARD('a)
  shows mat_of_cblinfun a $$ (i,j) = Rep_ell2 (a *V ket (Enum.enum ! j)) (Enum.enum ! i)
proof -
  let ?i = Enum.enum ! i and ?j = Enum.enum ! j and ?aj = a *V ket (Enum.enum ! j)
  have Rep_ell2 ?aj (Enum.enum ! i) = vec_of_basis_enum ?aj $ i
    by (rule vec_of_basis_enum_ell2_component[symmetric], simp)
  also have  = (mat_of_cblinfun a *v vec_of_basis_enum (ket (enum_class.enum ! j) :: 'a ell2)) $ i
    by (simp add: mat_of_cblinfun_cblinfun_apply)
  also have  = (mat_of_cblinfun a *v unit_vec CARD('a) j) $ i
    by (simp add: vec_of_basis_enum_ket enum_idx_enum)
  also have  = mat_of_cblinfun a $$ (i, j)
    apply (subst mat_entry_explicit[where m=CARD('b)])
    by (auto intro!: simp: canonical_basis_length)
  finally show ?thesis
    by auto
qed

lemma cblinfun_of_mat_mat:
  shows cblinfun_of_mat (mat (CARD('b)) (CARD('a)) f) = explicit_cblinfun (λ(r::'b::enum) (c::'a::enum). f (enum_idx r, enum_idx c))
  apply (intro equal_ket basis_enum_eq_vec_of_basis_enumI)
  by (auto intro!: eq_vecI simp: enum_idx_correct enum_idx_enum vec_of_basis_enum_ket
      mat_of_cblinfun_ell2_component canonical_basis_length cblinfun_of_mat_inverse index_row
      mat_of_cblinfun_cblinfun_apply)

lemma mat_of_cblinfun_explicit_cblinfun:
  fixes f :: 'a::enum  'b::enum  complex
  shows mat_of_cblinfun (explicit_cblinfun f) = mat (CARD('a)) (CARD('b)) (λ(r,c). f (Enum.enum!r) (Enum.enum!c))
  by (auto intro!: cblinfun_of_mat_inj[where 'a='b ell2 and 'b='a ell2, THEN inj_onD]
      simp: cblinfun_of_mat_mat canonical_basis_length enum_idx_correct mat_of_cblinfun_inverse)

lemma mat_of_cblinfun_classical_operator:
  fixes f::"'a::enum  'b::enum option"
  shows "mat_of_cblinfun (classical_operator f) = mat (CARD('b)) (CARD('a))
           (λ(r,c). if f (Enum.enum!c) = Some (Enum.enum!r) then 1 else 0)"
proof -
  define nA where "nA = CARD('a)"
  define nB where "nB = CARD('b)"
  define BasisA where "BasisA = (canonical_basis::'a ell2 list)"
  define BasisB where "BasisB = (canonical_basis::'b ell2 list)"
  have "mat_of_cblinfun (classical_operator f)  carrier_mat nB nA"
    by (auto simp: canonical_basis_length nA_def nB_def)
  moreover have "nA = CARD ('a)"
    unfolding nA_def
    by (simp add:)
  moreover have "nB = CARD ('b)"
    unfolding nB_def
    by (simp add:)
  ultimately have "mat_of_cblinfun (classical_operator f)  carrier_mat (CARD('b)) (CARD('a))"
    unfolding nA_def nB_def
    by simp
  moreover have "(mat_of_cblinfun (classical_operator f))$$(r,c)
  = (mat (CARD('b)) (CARD('a))
    (λ(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-
    have "CARD('a) = length (enum_class.enum::'a list)"
      using card_UNIV_length_enum[where 'a = 'a] .
    hence x1: "BasisA!c = ket ((Enum.enum::'a list)!c)"
      unfolding BasisA_def using a2 canonical_basis_ell2_def
        nth_map[where n = c and xs = "Enum.enum::'a list" and f = ket] by metis
    have cardb: "CARD('b) = length (enum_class.enum::'b list)"
      using card_UNIV_length_enum[where 'a = 'b] .
    hence x2: "BasisB!r = ket ((Enum.enum::'b list)!r)"
      unfolding BasisB_def using a1 canonical_basis_ell2_def
        nth_map[where n = r and xs = "Enum.enum::'b list" and f = ket] by metis
    have "inj (map (ket::'b _))"
      by (meson injI ket_injective list.inj_map)
    hence "length (Enum.enum::'b list) = length (map (ket::'b _) (Enum.enum::'b list))"
      by simp
    hence lengthBasisB: "CARD('b) = length BasisB"
      unfolding BasisB_def canonical_basis_ell2_def using cardb
      by smt
    have v1: "(mat_of_cblinfun (classical_operator f))$$(r,c) = 0"
      if c1: "f (Enum.enum!c) = None"
    proof-
      have "(classical_operator f) *V ket (Enum.enum!c)
          = (case f (Enum.enum!c) of None  0 | Some i  ket i)"
        using classical_operator_ket_finite .
      also have " = 0"
        using c1 by simp
      finally have "(classical_operator f) *V ket (Enum.enum!c) = 0" .
      hence *: "(classical_operator f) *V BasisA!c = 0"
        using x1 by simp
      hence "is_orthogonal (BasisB!r) (classical_operator f *V BasisA!c)"
        by simp
      thus ?thesis
        unfolding mat_of_cblinfun_def BasisA_def BasisB_def
        by (smt (verit, del_insts) BasisA_def * a1 a2 canonical_basis_length_ell2 complex_vector.representation_zero index_mat(1) old.prod.case)
    qed
    have v2: "(mat_of_cblinfun (classical_operator f))$$(r,c) = 0"
      if c1: "f (Enum.enum!c) = Some (Enum.enum!r')" and c2: "rr'"
        and c3: "r' < CARD('b)"
      for r'
    proof-
      have x3: "BasisB!r' = ket ((Enum.enum::'b list)!r')"
        unfolding BasisB_def using cardb c3 canonical_basis_ell2_def
          nth_map[where n = r' and xs = "Enum.enum::'b list" and f = ket]
        by smt
      have "distinct BasisB"
        unfolding BasisB_def
        by simp
      moreover have "r < length BasisB"
        using a1 lengthBasisB by simp
      moreover have "r' < length BasisB"
        using c3 lengthBasisB by simp
      ultimately have h1: "BasisB!r  BasisB!r'"
        using nth_eq_iff_index_eq[where xs = BasisB and i = r and j = r'] c2
        by blast
      have "(classical_operator f) *V ket (Enum.enum!c)
          = (case f (Enum.enum!c) of None  0 | Some i  ket i)"
        using classical_operator_ket_finite .
      also have " = ket (Enum.enum!r')"
        using c1 by simp
      finally have "(classical_operator f) *V ket (Enum.enum!c) = ket (Enum.enum!r')" .
      hence *: "(classical_operator f) *V BasisA!c = BasisB!r'"
        using x1 x3 by simp
      moreover have "is_orthogonal (BasisB!r) (BasisB!r')"
        using h1
        using BasisB_def r < length BasisB r' < length BasisB is_ortho_set_def is_orthonormal nth_mem
        by metis
      ultimately have "is_orthogonal (BasisB!r) (classical_operator f *V BasisA!c)"
        by simp
      thus ?thesis
        unfolding mat_of_cblinfun_def BasisA_def BasisB_def
        by (smt (z3) BasisA_def BasisB_def * r < length BasisB r' < length BasisB a2 canonical_basis_length_ell2 case_prod_conv complex_vector.representation_basis h1 index_mat(1) is_cindependent_set nth_mem)
    qed
    have "(mat_of_cblinfun (classical_operator f))$$(r,c) = 0"
      if b1: "f (Enum.enum!c)  Some (Enum.enum!r)"
    proof (cases "f (Enum.enum!c) = None")
      case True thus ?thesis using v1 by blast
    next
      case False
      hence "R. f (Enum.enum!c) = Some R"
        apply (induction "f (Enum.enum!c)")
         apply simp
        by simp
      then obtain R where R0: "f (Enum.enum!c) = Some R"
        by blast
      have "R  set (Enum.enum::'b list)"
        using UNIV_enum by blast
      hence "r'. R = (Enum.enum::'b list)!r'  r' < length (Enum.enum::'b list)"
        by (metis in_set_conv_nth)
      then obtain r' where u1: "R = (Enum.enum::'b list)!r'"
        and u2: "r' < length (Enum.enum::'b list)"
        by blast
      have R1: "f (Enum.enum!c) = Some (Enum.enum!r')"
        using R0 u1 by blast
      have "Some ((Enum.enum::'b list)!r')  Some ((Enum.enum::'b list)!r)"
      proof(rule classical)
        assume "¬(Some ((Enum.enum::'b list)!r')  Some ((Enum.enum::'b list)!r))"
        hence "Some ((Enum.enum::'b list)!r') = Some ((Enum.enum::'b list)!r)"
          by blast
        hence "f (Enum.enum!c) = Some ((Enum.enum::'b list)!r)"
          using R1 by auto
        thus ?thesis
          using b1 by blast
      qed
      hence "((Enum.enum::'b list)!r')  ((Enum.enum::'b list)!r)"
        by simp
      hence "r'  r"
        by blast
      moreover have "r' < CARD('b)"
        using u2 cardb by simp
      ultimately show ?thesis using R1 v2[where r' = r'] by blast
    qed
    moreover have "(mat_of_cblinfun (classical_operator f))$$(r,c) = 1"
      if b1: "f (Enum.enum!c) = Some (Enum.enum!r)"
    proof-
      have "CARD('b) = length (enum_class.enum::'b list)"
        using card_UNIV_length_enum[where 'a = 'b].
      hence "length (map (ket::'b_) enum_class.enum) = CARD('b)"
        by simp
      hence w0: "map (ket::'b_) enum_class.enum ! r = ket (enum_class.enum ! r)"
        by (simp add: a1)
      have "CARD('a) = length (enum_class.enum::'a list)"
        using card_UNIV_length_enum[where 'a = 'a].
      hence "length (map (ket::'a_) enum_class.enum) = CARD('a)"
        by simp
      hence "map (ket::'a_) enum_class.enum ! c = ket (enum_class.enum ! c)"
        by (simp add: a2)
      hence "(classical_operator f) *V (BasisA!c) = (classical_operator f) *V (ket (Enum.enum!c))"
        unfolding BasisA_def canonical_basis_ell2_def by simp
      also have "... = (case f (enum_class.enum ! c) of None  0 | Some x  ket x)"
        by (rule classical_operator_ket_finite)
      also have " = BasisB!r"
        using w0 b1 by (simp add: BasisB_def canonical_basis_ell2_def)
      finally have w1: "(classical_operator f) *V (BasisA!c) = BasisB!r"
        by simp
      have "(mat_of_cblinfun (classical_operator f))$$(r,c)
        = (BasisB!r) C (classical_operator f *V (BasisA!c))"
        unfolding BasisB_def BasisA_def mat_of_cblinfun_def
        using nA = CARD('a) nB = CARD('b) a1 a2 nA_def nB_def apply auto
        by (metis BasisA_def BasisB_def canonical_basis_length_ell2 cinner_canonical_basis complex_vector.representation_basis is_cindependent_set nth_mem w1)
      also have " = (BasisB!r) C (BasisB!r)"
        using w1 by simp
      also have " = 1"
        unfolding BasisB_def
        using nB = CARD('b) a1 nB_def
        by (simp add: cinner_canonical_basis)
      finally show ?thesis by blast
    qed
    ultimately show ?thesis
      by (simp add: a1 a2)
  qed
  ultimately show ?thesis
    apply (rule_tac eq_matI) by auto
qed


lemma mat_of_cblinfun_sandwich:
  fixes a :: "(_::onb_enum, _::onb_enum) cblinfun"
  shows mat_of_cblinfun (sandwich a *V b) = (let a' = mat_of_cblinfun a in a' * mat_of_cblinfun b * mat_adjoint a')
  by (simp add: mat_of_cblinfun_compose sandwich_apply Let_def mat_of_cblinfun_adj)

subsection ‹Operations on subspaces›

lemma ccspan_gram_schmidt0_invariant:
  defines "basis_enum  (basis_enum_of_vec :: _  'a::{basis_enum,complex_normed_vector})"
  defines "n  length (canonical_basis :: 'a list)"
  assumes "set ws  carrier_vec n"
  shows "ccspan (set (map basis_enum (gram_schmidt0 n ws))) = ccspan (set (map basis_enum ws))"
proof (transfer fixing: n ws basis_enum)
  interpret complex_vec_space.
  define gs where "gs = gram_schmidt0 n ws"
  have "closure (cspan (set (map basis_enum gs)))
     = cspan (set (map basis_enum gs))"
    apply (rule closure_finite_cspan)
    by simp
  also have " = cspan (basis_enum ` set gs)"
    by simp
  also have " = basis_enum ` span (set gs)"
    unfolding basis_enum_def
    apply (rule basis_enum_of_vec_span[symmetric])
    using n_def apply simp
    by (simp add: assms(3) cof_vec_space.gram_schmidt0_result(1) gs_def)
  also have " = basis_enum ` span (set ws)"
    unfolding gs_def
    apply (subst gram_schmidt0_result(4)[where ws=ws, symmetric])
    using assms by auto
  also have " = cspan (basis_enum ` set ws)"
    unfolding basis_enum_def
    apply (rule basis_enum_of_vec_span)
    using n_def apply simp
    by (simp add: assms(3))
  also have " = cspan (set (map basis_enum ws))"
    by simp
  also have " = closure (cspan (set (map basis_enum ws)))"
    apply (rule closure_finite_cspan[symmetric])
    by simp
  finally show "closure (cspan (set (map basis_enum gs)))
              = closure (cspan (set (map basis_enum ws)))".
qed

definition "is_subspace_of_vec_list n vs ws =
  (let ws' = gram_schmidt0 n ws in
     vset vs. adjuster n v ws' = - v)"

lemma ccspan_leq_using_vec:
  fixes A B :: 'a::{basis_enum,complex_normed_vector} list
  shows (ccspan (set A)  ccspan (set B)) 
    is_subspace_of_vec_list (length (canonical_basis :: 'a list))
      (map vec_of_basis_enum A) (map vec_of_basis_enum B)
proof -
  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"
  interpret complex_vec_space d.

  have Av_carrier: "set Av  carrier_vec d"
    unfolding Av_def apply auto
    by (simp add: carrier_vecI d_def dim_vec_of_basis_enum')
  have Bv_carrier: "set Bv  carrier_vec d"
    unfolding Bv_def apply auto
    by (simp add: carrier_vecI d_def dim_vec_of_basis_enum')
  have Bo_carrier: "set Bo  carrier_vec d"
    apply (simp add: Bo_def)
    using Bv_carrier by (rule gram_schmidt0_result(1))
  have orth_Bo: "corthogonal Bo"
    apply (simp add: Bo_def)
    using Bv_carrier by (rule gram_schmidt0_result(3))
  have distinct_Bo: "distinct Bo"
    apply (simp add: Bo_def)
    using Bv_carrier by (rule gram_schmidt0_result(2))

  have "ccspan (set A)  ccspan (set B)  cspan (set A)  cspan (set B)"
    apply (transfer fixing: A B)
    apply (subst closure_finite_cspan, simp)
    by (subst closure_finite_cspan, simp_all)
  also have "  span (set Av)  span (set Bv)"
    apply (simp add: Av_def Bv_def)
    apply (subst vec_of_basis_enum_cspan[symmetric], simp add: d_def)
    apply (subst vec_of_basis_enum_cspan[symmetric], simp add: d_def)
    by (metis inj_image_subset_iff inj_on_def vec_of_basis_enum_inverse)
  also have "  span (set Av)  span (set Bo)"
    unfolding Bo_def Av_def Bv_def
    apply (subst gram_schmidt0_result(4)[symmetric])
    by (simp_all add: carrier_dim_vec d_def dim_vec_of_basis_enum' image_subset_iff)
  also have "  (vset Av. adjuster d v Bo = - v)"
  proof (intro iffI ballI)
    fix v assume "v  set Av" and "span (set Av)  span (set Bo)"
    then have "v  span (set Bo)"
      using Av_carrier span_mem by auto
    have "adjuster d v Bo + v = 0v d"
      apply (rule adjuster_already_in_span)
      using Av_carrier v  set Av Bo_carrier orth_Bo
        v  span (set Bo) by simp_all
    then show "adjuster d v Bo = - v"
      using Av_carrier Bo_carrier v  set Av
      by (metis (no_types, lifting) add.inv_equality adjuster_carrier' local.vec_neg subsetD)
  next
    fix v
    assume adj_minusv: "vset Av. adjuster d v Bo = - v"
    have *: "adjuster d v Bo  span (set Bo)" if "v  set Av" for v
      apply (rule adjuster_in_span)
      using Bo_carrier that Av_carrier distinct_Bo by auto
    have "v  span (set Bo)" if "v  set Av" for v
      using *[OF that] adj_minusv[rule_format, OF that]
      apply auto
      by (metis (no_types, lifting) Av_carrier Bo_carrier adjust_nonzero distinct_Bo subsetD that uminus_l_inv_vec)
    then show "span (set Av)  span (set Bo)"
      apply auto
      by (meson Bo_carrier in_mono span_subsetI subsetI)
  qed
  also have " = is_subspace_of_vec_list d Av Bv"
    by (simp add: is_subspace_of_vec_list_def d_def Bo_def)
  finally show "ccspan (set A)  ccspan (set B)  is_subspace_of_vec_list d Av Bv"
    by simp
qed

lemma cblinfun_image_ccspan_using_vec:
  "A *S ccspan (set S) = ccspan (basis_enum_of_vec ` set (map ((*v) (mat_of_cblinfun A)) (map vec_of_basis_enum S)))"
  apply (auto simp: cblinfun_image_ccspan image_image)
  by (metis mat_of_cblinfun_cblinfun_apply vec_of_basis_enum_inverse)

text termmk_projector_orthog d L takes a list L of d-dimensional vectors
and returns the projector onto the span of L. (Assuming that all vectors in L are
orthogonal and nonzero.)›
fun mk_projector_orthog :: "nat  complex vec list  complex mat" where
  "mk_projector_orthog d [] = zero_mat d d"
| "mk_projector_orthog d [v] = (let norm2 = cscalar_prod v v in
                                smult_mat (1/norm2) (mat_of_cols d [v] * mat_of_rows d [conjugate v]))"
| "mk_projector_orthog d (v#vs) = (let norm2 = cscalar_prod v v in
                                   smult_mat (1/norm2) (mat_of_cols d [v] * mat_of_rows d [conjugate v])
                                        + mk_projector_orthog d vs)"

lemma mk_projector_orthog_correct:
  fixes S :: "'a::onb_enum list"
  defines "d  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 -
  define Snorm where "Snorm = map (λs. s /R norm s) S"

  have "distinct Snorm"
  proof (insert ortho distinct, unfold Snorm_def, induction S)
    case Nil
    show ?case by simp
  next
    case (Cons s S)
    then have "is_ortho_set (set S)" and "distinct S"
      unfolding is_ortho_set_def by auto
    note IH = Cons.IH[OF this]
    have "s /R norm s  (λs. s /R norm s) ` set S"
    proof auto
      fix s' assume "s'  set S" and same: "s /R norm s = s' /R norm s'"
      with Cons.prems have "s  s'" by auto
      have "s  0"
        by (metis Cons.prems(1) is_ortho_set_def list.set_intros(1))
      then have "0  (s /R norm s) C (s /R norm s)"
        by simp
      also have (s /R norm s) C (s /R norm s) = (s /R norm s) C (s' /R norm s')
        by (simp add: same)
      also have (s /R norm s) C (s' /R norm s') = (s C s') / (norm s * norm s')
        by (simp add: scaleR_scaleC divide_inverse_commute)
      also from s'  set S s  s' have " = 0"
        using Cons.prems unfolding is_ortho_set_def by simp
      finally show False
        by simp
    qed
    then show ?case
      using IH by simp
  qed

  have norm_Snorm: "norm s = 1" if "s  set Snorm" for s
    using that ortho unfolding Snorm_def is_ortho_set_def apply auto
    by (metis left_inverse norm_eq_zero)

  have ortho_Snorm: "is_ortho_set (set Snorm)"
    unfolding is_ortho_set_def
  proof (intro conjI ballI impI)
    fix x y
    show "0  set Snorm"
      using norm_Snorm[of 0] by auto
    assume "x  set Snorm" and "y  set Snorm" and "x  y"
    from x  set Snorm
    obtain x' where x: "x = x' /R norm x'" and x': "x'  set S"
      unfolding Snorm_def by auto
    from y  set Snorm
    obtain y' where y: "y = y' /R norm y'" and y': "y'  set S"
      unfolding Snorm_def by auto
    from x  y x y have x'  y' by auto
    with x' y' ortho have "cinner x' y' = 0"
      unfolding is_ortho_set_def by auto
    then show "cinner x y = 0"
      unfolding x y scaleR_scaleC by auto
  qed

  have inj_butter: "inj_on selfbutter (set Snorm)"
  proof (rule inj_onI)
    fix x y
    assume "x  set Snorm" and "y  set Snorm"
    assume "selfbutter x = selfbutter y"
    then obtain c where xcy: "x = c *C y" and "cmod c = 1"
      using inj_selfbutter_upto_phase by auto
    have "0  cmod (cinner x x)"
      using x  set Snorm norm_Snorm
      by force
    also have "cmod (cinner x x) = cmod (c * (x C y))"
      apply (subst (2) xcy) by simp
    also have " = cmod (x C y)"
      using cmod c = 1 by (simp add: norm_mult)
    finally have "(x C y)  0"
      by simp
    then show "x = y"
      using ortho_Snorm x  set Snorm y  set Snorm
      unfolding is_ortho_set_def by auto
  qed

  from distinct Snorm inj_butter
  have distinct': "distinct (map selfbutter Snorm)"
    unfolding distinct_map by simp

  have Span_Snorm: "ccspan (set Snorm) = ccspan (set S)"
    apply (transfer fixing: Snorm S)
    apply (simp add: scaleR_scaleC Snorm_def)
    apply (subst complex_vector.span_image_scale)
    using is_ortho_set_def ortho by fastforce+

  have "mk_projector_orthog d (map vec_of_basis_enum S)
      = mat_of_cblinfun (sum_list (map selfbutter Snorm))"
    unfolding Snorm_def
  proof (induction S)
    case Nil
    show ?case
      by (simp add: d_def mat_of_cblinfun_zero)
  next
    case (Cons a S)
    define sumS where "sumS = sum_list (map selfbutter (map (λs. s /R norm s) S))"
    with Cons have IH: "mk_projector_orthog d (map vec_of_basis_enum S)
                  = mat_of_cblinfun sumS"
      by simp

    define factor where "factor = inverse ((complex_of_real (norm a))2)"
    have factor': "factor = 1 / (vec_of_basis_enum a ∙c vec_of_basis_enum a)"
      unfolding factor_def cscalar_prod_vec_of_basis_enum
      by (simp add: inverse_eq_divide power2_norm_eq_cinner)

    have "mk_projector_orthog d (map vec_of_basis_enum (a # S))
          = factor m (mat_of_cols d [vec_of_basis_enum a]
                    * mat_of_rows d [conjugate (vec_of_basis_enum a)])
            + mat_of_cblinfun sumS"
      apply (cases S)
       apply (auto simp add: factor' sumS_def d_def mat_of_cblinfun_zero)[1]
      by (auto simp add: IH[symmetric] factor' d_def)

    also have " = factor 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"
      apply (rule arg_cong[where f="λx. _ m (_ * x) + _"])
      apply (rule mat_eq_iff[THEN iffD2])
      apply (auto simp add: mat_adjoint_def)
      apply (subst mat_of_rows_index) apply auto
      apply (subst mat_of_rows_index) apply auto
      apply (subst mat_of_cols_index) apply auto
      by (simp add: assms(1) dim_vec_of_basis_enum')
    also have " = mat_of_cblinfun (selfbutter (a /R norm a)) + mat_of_cblinfun sumS"
      apply (simp add: butterfly_scaleR_left butterfly_scaleR_right power_inverse mat_of_cblinfun_scaleR factor_def)
      apply (simp add: butterfly_def mat_of_cblinfun_compose
          mat_of_cblinfun_adj mat_of_cblinfun_vector_to_cblinfun d_def)
      by (simp add: mat_of_cblinfun_compose mat_of_cblinfun_adj mat_of_cblinfun_vector_to_cblinfun mat_of_cblinfun_scaleC power2_eq_square)
    finally show ?case
      by (simp add: mat_of_cblinfun_plus sumS_def)
  qed
  also have " = mat_of_cblinfun (sset Snorm. selfbutter s)"
    by (metis distinct' distinct_map sum.distinct_set_conv_list)
  also have " = mat_of_cblinfun (sset Snorm. proj s)"
    apply (rule arg_cong[where f="mat_of_cblinfun"])
    apply (rule sum.cong[OF refl])
    apply (rule butterfly_eq_proj)
    using norm_Snorm by simp
  also have " = mat_of_cblinfun (Proj (ccspan (set Snorm)))"
    apply (rule arg_cong[where f=mat_of_cblinfun])
    using ortho_Snorm distinct Snorm apply (induction Snorm)
     apply auto
    apply (subst Proj_orthog_ccspan_insert[where Y=set _])
    by (auto simp: is_ortho_set_def)
  also have " = mat_of_cblinfun (Proj (ccspan (set S)))"
    unfolding Span_Snorm by simp
  finally show ?thesis
    by -
qed

definition mk_projector d vs = mk_projector_orthog d (gram_schmidt0 d vs)

lemma mat_of_cblinfun_Proj_ccspan:
  fixes S :: 'a::onb_enum list
  shows mat_of_cblinfun (Proj (ccspan (set S))) = mk_projector (length (canonical_basis :: 'a list)) (map vec_of_basis_enum S)
proof-
  define d gs
    where "d = length (canonical_basis :: 'a list)"
      and "gs = gram_schmidt0 d (map vec_of_basis_enum S)"
  interpret complex_vec_space d.
  have gs_dim: "x  set gs  dim_vec x = d" for x
    by (smt carrier_vecD carrier_vec_dim_vec d_def dim_vec_of_basis_enum' ex_map_conv gram_schmidt0_result(1) gs_def subset_code(1))
  have ortho_gs: "is_ortho_set (set (map basis_enum_of_vec gs :: 'a list))"
    apply (subst corthogonal_vec_of_basis_enum[THEN iffD1], auto)
    by (smt carrier_dim_vec cof_vec_space.gram_schmidt0_result(1) d_def dim_vec_of_basis_enum' gram_schmidt0_result(3) gs_def imageE map_idI map_map o_apply set_map subset_code(1) basis_enum_of_vec_inverse)
  have distinct_gs: "distinct (map basis_enum_of_vec gs :: 'a list)"
    by (metis (mono_tags, opaque_lifting) carrier_vec_dim_vec cof_vec_space.gram_schmidt0_result(2) d_def dim_vec_of_basis_enum' distinct_map gs_def gs_dim image_iff inj_on_inverseI set_map subsetI basis_enum_of_vec_inverse)

  have "mk_projector_orthog d gs
      = mk_projector_orthog d (map vec_of_basis_enum (map basis_enum_of_vec gs :: 'a list))"
    apply simp
    apply (subst map_cong[where ys=gs and g=id], simp)
    using gs_dim by (auto intro!: vec_of_basis_enum_inverse simp: d_def)
  also have " = mat_of_cblinfun (Proj (ccspan (set (map basis_enum_of_vec gs :: 'a list))))"
    unfolding d_def
    apply (subst mk_projector_orthog_correct)
    using ortho_gs distinct_gs by auto
  also have " = mat_of_cblinfun (Proj (ccspan (set S)))"
    apply (rule arg_cong[where f="λx. mat_of_cblinfun (Proj x)"])
    unfolding gs_def d_def
    apply (subst ccspan_gram_schmidt0_invariant)
    by (auto simp add: carrier_vecI dim_vec_of_basis_enum')
  finally show ?thesis
    by (simp add: d_def gs_def mk_projector_def)
qed

unbundle no_jnf_notation
unbundle no_cblinfun_notation

end