Theory Axioms_Complement_Quantum

section ‹Quantum instantiation of complements›

theory Axioms_Complement_Quantum
  imports Laws_Quantum Finite_Tensor_Product Quantum_Extra
begin

no_notation m_inv ("invı _" [81] 80)
no_notation Lattice.join (infixl "⊔ı" 65)

typedef ('a::finite,'b::finite) complement_domain = ‹{..< if CARD('b) div CARD('a) ≠ 0 then CARD('b) div CARD('a) else 1}›
  by auto

instance complement_domain :: (finite, finite) finite
proof intro_classes
  have ‹inj Rep_complement_domain›
    by (simp add: Rep_complement_domain_inject inj_on_def)
  moreover have ‹finite (range Rep_complement_domain)›
    by (metis finite_lessThan type_definition.Rep_range type_definition_complement_domain)
  ultimately show ‹finite (UNIV :: ('a,'b) complement_domain set)›
    using finite_image_iff by blast
qed

lemma CARD_complement_domain: 
  assumes ‹CARD('b::finite) = n * CARD('a::finite)›
  shows ‹CARD(('a,'b) complement_domain) = n›
proof -
  from assms have ‹n > 0›
    by (metis zero_less_card_finite zero_less_mult_pos2)
  have *: ‹inj Rep_complement_domain›
    by (simp add: Rep_complement_domain_inject inj_on_def)
  moreover have ‹card (range (Rep_complement_domain :: ('a,'b) complement_domain ⇒ _)) = n›
    apply (subst type_definition.Rep_range[OF type_definition_complement_domain])
    using assms ‹n > 0› by simp
  ultimately show ?thesis
    by (metis card_image)
qed


lemma register_decomposition:
  fixes Φ :: ‹'a::finite update ⇒ 'b::finite update›
  assumes [simp]: ‹register Φ›
  shows ‹∃U :: ('a × ('a, 'b) complement_domain) ell2 ⇒⇩C⇩L 'b ell2. unitary U ∧ 
              (∀θ. Φ θ = sandwich U (θ ⊗⇩o id_cblinfun))›
  ― ‹Proof based on \<^cite>‹daws21unitalanswer››
proof -
  note [[simproc del: compatibility_warn]]
  fix ξ0 :: 'a

  have [simp]: ‹clinear Φ›
    by simp

  define P where ‹P i = Proj (ccspan {ket i})› for i :: 'a
  have P_butter: ‹P i = selfbutterket i› for i
    by (simp add: P_def butterfly_eq_proj)

  define P' where ‹P' i = Φ (P i)› for i :: 'a
  have proj_P': ‹is_Proj (P' i)› for i
    by (simp add: P_def P'_def register_projector)
  have ‹(∑i∈UNIV. P i) = id_cblinfun›
    using sum_butterfly_ket P_butter by simp
  then have sumP'id: ‹(∑i∈UNIV. P' i) = id_cblinfun›
    unfolding P'_def 
    apply (subst complex_vector.linear_sum[OF ‹clinear Φ›, symmetric])
    by auto

  define S where ‹S i = P' i *⇩S ⊤› for i :: 'a
  have P'id: ‹P' i *⇩V ψ = ψ› if ‹ψ ∈ space_as_set (S i)› for i ψ
    using S_def that proj_P'
    by (metis cblinfun_fixes_range is_Proj_algebraic)

  obtain B0 where finiteB0: ‹finite (B0 i)› and cspanB0: ‹cspan (B0 i) = space_as_set (S i)› for i
    apply atomize_elim apply (simp flip: all_conj_distrib) apply (rule choice)
    by (meson cfinite_dim_finite_subspace_basis csubspace_space_as_set)

  obtain B where orthoB: ‹is_ortho_set (B i)›
    and normalB: ‹⋀b. b ∈ B i ⟹ norm b = 1›
    and cspanB: ‹cspan (B i) = cspan (B0 i)›
    and finiteB: ‹finite (B i)› for i
    apply atomize_elim apply (simp flip: all_conj_distrib) apply (rule choice)
    using orthonormal_basis_of_cspan[OF finiteB0] by blast

  from cspanB cspanB0 have cspanB: ‹cspan (B i) = space_as_set (S i)› for i
    by simp
  then have ccspanB: ‹ccspan (B i) = S i› for i
    by (metis ccspan.rep_eq closure_finite_cspan finiteB space_as_set_inject)
  from orthoB have indepB: ‹cindependent (B i)› for i
    by (simp add: Complex_Inner_Product.is_ortho_set_cindependent)

  have orthoBiBj: ‹is_orthogonal x y› if ‹x ∈ B i› and ‹y ∈ B j› and ‹i ≠ j› for x y i j
  proof -
    from ‹x ∈ B i› obtain x' where x: ‹x = P' i *⇩V x'›
      by (metis S_def cblinfun_fixes_range complex_vector.span_base cspanB is_Proj_idempotent proj_P')
    from ‹y ∈ B j› obtain y' where y: ‹y = P' j *⇩V y'›
      by (metis S_def cblinfun_fixes_range complex_vector.span_base cspanB is_Proj_idempotent proj_P')
    have ‹cinner x y = cinner (P' i *⇩V x') (P' j *⇩V  y')›
      using x y by simp
    also have ‹… = cinner (P' j *⇩V P' i *⇩V x') y'›
      by (metis cinner_adj_left is_Proj_algebraic proj_P')
    also have ‹… = cinner (Φ (P j o⇩C⇩L P i) *⇩V x') y'›
      unfolding P'_def register_mult[OF ‹register Φ›, symmetric] by simp
    also have ‹… = cinner (Φ (selfbutterket j o⇩C⇩L selfbutterket i) *⇩V x') y'›
      unfolding P_butter by simp
    also have ‹… = cinner (Φ 0 *⇩V x') y'›
      by (metis butterfly_comp_butterfly complex_vector.scale_eq_0_iff orthogonal_ket that(3))
    also have ‹… = 0›
      by (simp add: complex_vector.linear_0)
    finally show ?thesis
      by -
  qed


  define B' where ‹B' = (⋃i∈UNIV. B i)›

  have P'B: ‹P' i = Proj (ccspan (B i))› for i
    unfolding ccspanB S_def
    using proj_P' Proj_on_own_range'[symmetric] is_Proj_algebraic by blast

  have ‹(∑i∈UNIV. P' i) = Proj (ccspan B')›
  proof (unfold B'_def, use finite[of UNIV] in induction)
    case empty
    show ?case by auto
  next
    case (insert j M)
    have ‹(∑i∈insert j M. P' i) = P' j + (∑i∈M. P' i)›
      by (meson insert.hyps(1) insert.hyps(2) sum.insert)
    also have ‹… = Proj (ccspan (B j)) + Proj (ccspan (⋃i∈M. B i))›
      unfolding P'B insert.IH[symmetric] by simp
    also have ‹… = Proj (ccspan (B j ∪ (⋃i∈M. B i)))›
      apply (rule Proj_orthog_ccspan_union[symmetric])
      using orthoBiBj insert.hyps(2) by auto
    also have ‹… = Proj (ccspan (⋃i∈insert j M. B i))›
      by auto
    finally show ?case
      by simp
  qed

  with sumP'id 
  have ccspanB': ‹ccspan B' = ⊤›
    by (metis Proj_range cblinfun_image_id)
  hence cspanB': ‹cspan B' = UNIV›
    by (metis B'_def finiteB ccspan.rep_eq finite_UN_I finite_class.finite_UNIV closure_finite_cspan top_ccsubspace.rep_eq)

  from orthoBiBj orthoB have orthoB': ‹is_ortho_set B'›
    unfolding B'_def is_ortho_set_def by blast
  then have indepB': ‹cindependent B'›
    using is_ortho_set_cindependent by blast
  have cardB': ‹card B' = CARD('b)›
    apply (subst complex_vector.dim_span_eq_card_independent[symmetric])
     apply (rule indepB')
    apply (subst cspanB')
    using cdim_UNIV_ell2 by auto

  from orthoBiBj orthoB
  have Bdisj: ‹B i ∩ B j = {}› if ‹i ≠ j› for i j
    unfolding is_ortho_set_def
    apply auto by (metis cinner_eq_zero_iff that)

  have cardBsame: ‹card (B i) = card (B j)› for i j
  proof -
    define Si_to_Sj where ‹Si_to_Sj i j ψ = Φ (butterket j i) *⇩V ψ› for i j ψ
    have S2S2S: ‹Si_to_Sj j i (Si_to_Sj i j ψ) = ψ› if ‹ψ ∈ space_as_set (S i)› for i j ψ
      using that P'id
      by (simp add: Si_to_Sj_def cblinfun_apply_cblinfun_compose[symmetric] register_mult P_butter P'_def)
    also have lin[simp]: ‹clinear (Si_to_Sj i j)› for i j
      unfolding Si_to_Sj_def by simp
    have S2S: ‹Si_to_Sj i j x ∈ space_as_set (S j)› for i j x
    proof -
      have ‹Si_to_Sj i j x = P' j *⇩V Si_to_Sj i j x›
        by (simp add: Si_to_Sj_def cblinfun_apply_cblinfun_compose[symmetric] register_mult P_butter P'_def)
      also have ‹P' j *⇩V Si_to_Sj i j x ∈ space_as_set (S j)›
        by (simp add: S_def)
      finally show ?thesis by -
    qed
    have bij: ‹bij_betw (Si_to_Sj i j) (space_as_set (S i)) (space_as_set (S j))›
      apply (rule bij_betwI[where g=‹Si_to_Sj j i›])
      using S2S S2S2S by (auto intro!: funcsetI)
    have ‹cdim (space_as_set (S i)) = cdim (space_as_set (S j))›
      using lin apply (rule isomorphic_equal_cdim[where f=‹Si_to_Sj i j›])
      using bij apply (auto simp: bij_betw_def)
      by (metis complex_vector.span_span cspanB)
    then show ?thesis
      by (metis complex_vector.dim_span_eq_card_independent cspanB indepB)
  qed

  have CARD'b: ‹CARD('b) = card (B ξ0) * CARD('a)›
  proof -
    have ‹CARD('b) = card B'›
      using cardB' by simp
    also have ‹… = (∑i∈UNIV. card (B i))›
      unfolding B'_def apply (rule card_UN_disjoint)
      using finiteB Bdisj by auto
    also have ‹… = (∑(i::'a)∈UNIV. card (B ξ0))›
      using cardBsame by metis
    also have ‹… = card (B ξ0) * CARD('a)›
      by auto
    finally show ?thesis by -
  qed

  obtain f where bij_f: ‹bij_betw f (UNIV::('a,'b) complement_domain set) (B ξ0)›
    apply atomize_elim apply (rule finite_same_card_bij)
    using finiteB CARD_complement_domain[OF CARD'b] by auto

  define u where ‹u = (λ(ξ,α). Φ (butterket ξ ξ0) *⇩V f α)› for ξ :: 'a and α :: ‹('a,'b) complement_domain›
  obtain U where Uapply: ‹U *⇩V ket ξα = u ξα› for ξα
    apply atomize_elim
    apply (rule exI[of _ ‹cblinfun_extension (range ket) (λk. u (inv ket k))›])
    apply (subst cblinfun_extension_apply)
      apply (rule cblinfun_extension_exists_finite_dim)
    by (auto simp add: inj_ket cindependent_ket)

  define eqa where ‹eqa a b = (if a = b then 1 else 0 :: complex)› for a b :: 'a
  define eqc where ‹eqc a b = (if a = b then 1 else 0 :: complex)› for a b :: ‹('a,'b) complement_domain›
  define eqac where ‹eqac a b = (if a = b then 1 else 0 :: complex)› for a b :: ‹'a * ('a,'b) complement_domain›

  have ‹cinner (U *⇩V ket ξα) (U *⇩V ket ξ'α') = eqac ξα ξ'α'› for ξα ξ'α'
  proof -
    obtain ξ α ξ' α' where ξα: ‹ξα = (ξ,α)› and ξ'α': ‹ξ'α' = (ξ',α')›
      apply atomize_elim by auto
    have ‹cinner (U *⇩V ket (ξ,α)) (U *⇩V ket (ξ', α')) = cinner (Φ (butterket ξ ξ0) *⇩V f α) (Φ (butterket ξ' ξ0) *⇩V f α')›
      unfolding Uapply u_def by simp
    also have ‹… = cinner ((Φ (butterket ξ' ξ0))* *⇩V Φ (butterket ξ ξ0) *⇩V f α) (f α')›
      by (simp add: cinner_adj_left)
    also have ‹… = cinner (Φ (butterket ξ' ξ0 *) *⇩V Φ (butterket ξ ξ0) *⇩V f α) (f α')›
      by (metis (no_types, lifting) assms register_def)
    also have ‹… = cinner (Φ (butterket ξ0 ξ' o⇩C⇩L butterket ξ ξ0) *⇩V f α) (f α')›
      by (simp add: register_mult cblinfun_apply_cblinfun_compose[symmetric])
    also have ‹… = cinner (Φ (eqa ξ' ξ *⇩C selfbutterket ξ0) *⇩V f α) (f α')›
      by (simp add: eqa_def cinner_ket) 
    also have ‹… = eqa ξ' ξ * cinner (Φ (selfbutterket ξ0) *⇩V f α) (f α')›
      by (smt (verit, ccfv_threshold) ‹clinear Φ› eqa_def cblinfun.scaleC_left cinner_commute 
              cinner_scaleC_left cinner_zero_right complex_cnj_one complex_vector.linear_scale)
    also have ‹… = eqa ξ' ξ * cinner (P' ξ0 *⇩V f α) (f α')›
      using P_butter P'_def by simp
    also have ‹… = eqa ξ' ξ * cinner (f α) (f α')›
      apply (subst P'id)
       apply (metis bij_betw_imp_surj_on bij_f complex_vector.span_base cspanB rangeI)
      by simp
    also have ‹… = eqa ξ' ξ * eqc α α'›
      using bij_f orthoB normalB unfolding is_ortho_set_def eqc_def apply auto
       apply (metis bij_betw_imp_surj_on cnorm_eq_1 rangeI)
      by (smt (z3) bij_betw_iff_bijections iso_tuple_UNIV_I)
    finally show ?thesis
      by (simp add: eqa_def eqac_def eqc_def ξ'α' ξα)
  qed
  then have ‹isometry U›
    apply (rule_tac orthogonal_on_basis_is_isometry[where B=‹range ket›])
    using eqac_def by auto

  have ‹U* o⇩C⇩L Φ (butterket ξ η) o⇩C⇩L U = butterket ξ η ⊗⇩o id_cblinfun› for ξ η
  proof (rule equal_ket, rename_tac ξ1α)
    fix ξ1α obtain ξ1 :: 'a and α :: ‹('a,'b) complement_domain› where ξ1α: ‹ξ1α = (ξ1,α)› 
      apply atomize_elim by auto
    have ‹(U* o⇩C⇩L Φ (butterket ξ η) o⇩C⇩L U) *⇩V ket ξ1α = U* *⇩V Φ (butterket ξ η) *⇩V Φ (butterket ξ1 ξ0) *⇩V f α›
      unfolding cblinfun_apply_cblinfun_compose ξ1α Uapply u_def by simp
    also have ‹… = U* *⇩V Φ (butterket ξ η o⇩C⇩L butterket ξ1 ξ0) *⇩V f α›
      by (metis (no_types, lifting) assms butterfly_comp_butterfly lift_cblinfun_comp(4) register_mult)
    also have ‹… = U* *⇩V Φ (eqa η ξ1 *⇩C butterket ξ ξ0) *⇩V f α›
      by (simp add: eqa_def cinner_ket)
    also have ‹… = eqa η ξ1 *⇩C U* *⇩V Φ (butterket ξ ξ0) *⇩V f α›
      by (simp add: complex_vector.linear_scale)
    also have ‹… = eqa η ξ1 *⇩C U* *⇩V U *⇩V ket (ξ, α)›
      unfolding Uapply u_def by simp
    also from ‹isometry U› have ‹… = eqa η ξ1 *⇩C ket (ξ, α)›
      unfolding cblinfun_apply_cblinfun_compose[symmetric] by simp
    also have ‹… = (butterket ξ η *⇩V ket ξ1) ⊗⇩s ket α›
      by (simp add: eqa_def tensor_ell2_scaleC1)
    also have ‹… = (butterket ξ η ⊗⇩o id_cblinfun) *⇩V ket ξ1α›
      by (simp add: ξ1α tensor_op_ket)
    finally show ‹(U* o⇩C⇩L Φ (butterket ξ η) o⇩C⇩L U) *⇩V ket ξ1α = (butterket ξ η ⊗⇩o id_cblinfun) *⇩V ket ξ1α›
      by -
  qed
  then have 1: ‹U* o⇩C⇩L Φ θ o⇩C⇩L U = θ ⊗⇩o id_cblinfun› for θ
    apply (rule_tac clinear_eq_butterfly_ketI[THEN fun_cong, where x=θ])
    by (auto intro!: clinearI simp add: bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose complex_vector.linear_add complex_vector.linear_scale)

  have ‹unitary U›
  proof -
    have ‹Φ (butterket ξ ξ1) *⇩S ⊤ ≤ U *⇩S ⊤› for ξ ξ1
    proof -
      have *: ‹Φ (butterket ξ ξ0) *⇩V b ∈ space_as_set (U *⇩S ⊤)› if ‹b ∈ B ξ0› for b
        apply (subst asm_rl[of ‹Φ (butterket ξ ξ0) *⇩V b = u (ξ, inv f b)›])
         apply (simp add: u_def, metis bij_betw_inv_into_right bij_f that)
        by (metis Uapply cblinfun_apply_in_image)

      have ‹Φ (butterket ξ ξ1) *⇩S ⊤ = Φ (butterket ξ ξ0) *⇩S Φ (butterket ξ0 ξ0) *⇩S Φ (butterket ξ0 ξ1) *⇩S ⊤›
        unfolding cblinfun_compose_image[symmetric] register_mult[OF assms]
        by simp
      also have ‹… ≤ Φ (butterket ξ ξ0) *⇩S Φ (butterket ξ0 ξ0) *⇩S ⊤›
        by (meson cblinfun_image_mono top_greatest)
      also have ‹… = Φ (butterket ξ ξ0) *⇩S S ξ0›
        by (simp add: S_def P'_def P_butter)
      also have ‹… = Φ (butterket ξ ξ0) *⇩S ccspan (B ξ0)›
        by (simp add: ccspanB)
      also have ‹… = ccspan (Φ (butterket ξ ξ0) ` B ξ0)›
        by (meson cblinfun_image_ccspan)
      also have ‹… ≤ U *⇩S ⊤›
        by (rule ccspan_leqI, use * in auto)
      finally show ?thesis by -
    qed
    moreover have ‹Φ id_cblinfun *⇩S ⊤ ≤ (SUP ξ∈UNIV. Φ (selfbutterket ξ) *⇩S ⊤)›
      unfolding sum_butterfly_ket[symmetric]
      apply (subst complex_vector.linear_sum, simp)
      by (rule cblinfun_sum_image_distr)
    ultimately have ‹Φ id_cblinfun *⇩S ⊤ ≤ U *⇩S ⊤›
      apply auto by (meson SUP_le_iff order.trans)
    then have ‹U *⇩S ⊤ = ⊤›
      apply auto
      using top.extremum_unique by blast
    with ‹isometry U› show ‹unitary U›
      by (rule surj_isometry_is_unitary)
  qed

  have ‹Φ θ = U o⇩C⇩L (θ ⊗⇩o id_cblinfun) o⇩C⇩L U*› for θ
  proof -
    from ‹unitary U›
    have ‹Φ θ = (U o⇩C⇩L U*) o⇩C⇩L Φ θ o⇩C⇩L (U o⇩C⇩L U*)›
      by simp
    also have ‹… = U o⇩C⇩L (U*  o⇩C⇩L Φ θ o⇩C⇩L U) o⇩C⇩L U*›
      by (simp add: cblinfun_assoc_left)
    also have ‹… = U o⇩C⇩L (θ ⊗⇩o id_cblinfun) o⇩C⇩L U*›
      using 1 by simp
    finally show ?thesis
      by -
  qed

  with ‹unitary U› show ?thesis
    by (auto simp: sandwich_def)
qed

lemma register_decomposition_converse: 
  assumes ‹unitary U›
  shows ‹register (λx. sandwich U (id_cblinfun ⊗⇩o x))›
  using _ unitary_sandwich_register apply (rule register_comp[unfolded o_def])
  using assms by auto


lemma register_inj: ‹inj F› if ‹register F›
proof -
  obtain U :: ‹('a × ('a, 'b) complement_domain) ell2 ⇒⇩C⇩L 'b ell2›
    where ‹unitary U› and F: ‹F a = sandwich U (a ⊗⇩o id_cblinfun)› for a
    apply atomize_elim using ‹register F› by (rule register_decomposition)
  have ‹inj (sandwich U)›
    by (smt (verit, best) ‹unitary U› cblinfun_assoc_left inj_onI sandwich_def cblinfun_compose_id_right cblinfun_compose_id_left unitary_def)
  moreover have ‹inj (λa::'a::finite ell2 ⇒⇩C⇩L _. a ⊗⇩o id_cblinfun)›
    by (rule inj_tensor_left, simp)
  ultimately show ‹inj F›
    unfolding F
    by (smt (z3) inj_def) 
qed

lemma iso_register_decomposition:
  assumes [simp]: ‹iso_register F›
  shows ‹∃U. unitary U ∧ F = sandwich U›
proof -
  have [simp]: ‹register F›
    using assms iso_register_is_register by blast 

  let ?ida = ‹id_cblinfun :: ('a, 'b) complement_domain ell2 ⇒⇩C⇩L _›

  from register_decomposition[OF ‹register F›]
  obtain V :: ‹('a × ('a, 'b) complement_domain) ell2 ⇒⇩C⇩L 'b ell2› where ‹unitary V›
    and FV: ‹F θ = sandwich V (θ ⊗⇩o ?ida)› for θ
    by auto

  have ‹surj F›
    by (meson assms iso_register_inv_comp2 surj_iff)
  have surj_tensor: ‹surj (λa::'a ell2 ⇒⇩C⇩L 'a ell2. a ⊗⇩o ?ida)›
    apply (rule surj_from_comp[where g=‹sandwich V›])
    using ‹surj F› apply (auto simp: FV)
    by (meson ‹unitary V› register_inj unitary_sandwich_register)
  then obtain a :: ‹'a ell2 ⇒⇩C⇩L _› 
    where a: ‹a ⊗⇩o ?ida = selfbutterket undefined ⊗⇩o selfbutterket undefined›
    by (smt (verit, best) surjD)

  then have ‹a ≠ 0›
    apply auto
    by (metis butterfly_apply cblinfun.zero_left complex_vector.scale_eq_0_iff ket_nonzero orthogonal_ket)

  obtain γ where γ: ‹?ida = γ *⇩C selfbutterket undefined›
    apply atomize_elim
    using a ‹a ≠ 0› by (rule tensor_op_almost_injective)
  then have ‹?ida (ket undefined) = γ *⇩C (selfbutterket undefined *⇩V ket undefined)›
    by (simp add: ‹id_cblinfun = γ *⇩C selfbutterket undefined› scaleC_cblinfun.rep_eq)
  then have ‹ket undefined = γ *⇩C ket undefined›
    by (metis butterfly_apply cinner_scaleC_right id_cblinfun_apply cinner_ket_same mult.right_neutral scaleC_one)
  then have ‹γ = 1›
    by (smt (z3) γ butterfly_apply butterfly_scaleC_left cblinfun_id_cblinfun_apply complex_vector.scale_cancel_right cinner_ket_same ket_nonzero)

  define T U where ‹T = CBlinfun (λψ. ψ ⊗⇩s ket undefined)› and ‹U = V o⇩C⇩L T›
  have T: ‹T ψ = ψ ⊗⇩s ket undefined› for ψ
    unfolding T_def
    apply (subst bounded_clinear_CBlinfun_apply)
    by (auto intro!: bounded_clinear_finite_dim clinear_tensor_ell22)
  have sandwich_T: ‹sandwich T a = a ⊗⇩o ?ida› for a
    apply (rule fun_cong[where x=a])
    apply (rule clinear_eq_butterfly_ketI)
      apply auto
    by (metis (no_types, opaque_lifting) Misc.sandwich_def T γ ‹γ = 1› adj_cblinfun_compose butterfly_adjoint cblinfun_comp_butterfly scaleC_one tensor_butterfly)

  have ‹F (butterfly x y) = V o⇩C⇩L (butterfly x y ⊗⇩o ?ida) o⇩C⇩L V*› for x y
    by (simp add: Misc.sandwich_def FV)
  also have ‹… x y = V o⇩C⇩L (butterfly (T x) (T y)) o⇩C⇩L V*› for x y
    by (simp add: T γ ‹γ = 1›)
  also have ‹… x y = U o⇩C⇩L (butterfly x y) o⇩C⇩L U*› for x y
    by (simp add: U_def butterfly_comp_cblinfun cblinfun_comp_butterfly)
  finally have F_rep:  ‹F a = U o⇩C⇩L a o⇩C⇩L U*› for a
    apply (rule_tac fun_cong[where x=a])
    apply (rule_tac clinear_eq_butterfly_ketI)
      apply auto
    by (metis (no_types, lifting) cblinfun_apply_clinear clinear_iff sandwich_apply)

  have ‹isometry T›
    apply (rule orthogonal_on_basis_is_isometry[where B=‹range ket›])
    by (auto simp: T)
  moreover have ‹T *⇩S ⊤ = ⊤›
  proof -
    have 1: ‹φ ⊗⇩s ξ ∈ range ((*⇩V) T)› for φ ξ
    proof -
      have ‹T *⇩V (cinner (ket undefined) ξ *⇩C φ) = φ ⊗⇩s (cinner (ket undefined) ξ *⇩C ket undefined)›
        by (simp add: T tensor_ell2_scaleC2)
      also have ‹… = φ ⊗⇩s (selfbutterket undefined *⇩V ξ)›
        by simp
      also have ‹… = φ ⊗⇩s (?ida *⇩V ξ)›
        by (simp add: γ ‹γ = 1›)
      also have ‹… = φ ⊗⇩s ξ›
        by simp
      finally show ?thesis
        by (metis range_eqI)
    qed

    have ‹⊤ ≤ ccspan {ket x | x. True}›
      by (simp add: full_SetCompr_eq)
    also have ‹… ≤ ccspan {φ ⊗⇩s ξ | φ ξ. True}›
      apply (rule ccspan_mono)
      by (auto simp flip: tensor_ell2_ket)
    also from 1 have ‹… ≤ ccspan (range ((*⇩V) T))›
      by (auto intro!: ccspan_mono)
    also have ‹… = T *⇩S ⊤›
      by (metis (mono_tags, opaque_lifting) calculation cblinfun_image_ccspan cblinfun_image_mono eq_iff top_greatest)
    finally show ‹T *⇩S ⊤ = ⊤›
      using top.extremum_uniqueI by blast
  qed

  ultimately have ‹unitary T›
    by (rule surj_isometry_is_unitary)
  then have ‹unitary U›
    by (simp add: U_def ‹unitary V›)

  from F_rep ‹unitary U› show ?thesis
    by (auto simp: sandwich_def[abs_def])
qed

lemma complement_exists:
  fixes F :: ‹'a::finite update ⇒ 'b::finite update›
  assumes ‹register F›
  shows ‹∃G :: ('a, 'b) complement_domain update ⇒ 'b update. compatible F G ∧ iso_register (F;G)›
proof -
  note [[simproc del: Laws_Quantum.compatibility_warn]]
  obtain U :: ‹('a × ('a, 'b) complement_domain) ell2 ⇒⇩C⇩L 'b ell2›
    where [simp]: "unitary U" and F: ‹F a = sandwich U (a ⊗⇩o id_cblinfun)› for a
    apply atomize_elim using assms by (rule register_decomposition)
  define G :: ‹(('a, 'b) complement_domain) update ⇒ 'b update› where ‹G b = sandwich U (id_cblinfun ⊗⇩o b)› for b
  have [simp]: ‹register G›
    unfolding G_def apply (rule register_decomposition_converse) by simp
  have ‹F a o⇩C⇩L G b = G b o⇩C⇩L F a› for a b
  proof -
    have ‹F a o⇩C⇩L G b = sandwich U (a ⊗⇩o b)›
      apply (auto simp: F G_def sandwich_def)
      by (metis (no_types, lifting) ‹unitary U› isometryD cblinfun_assoc_left(1) comp_tensor_op cblinfun_compose_id_right cblinfun_compose_id_left unitary_isometry)
    moreover have ‹G b o⇩C⇩L F a = sandwich U (a ⊗⇩o b)›
      apply (auto simp: F G_def sandwich_def)
      by (metis (no_types, lifting) ‹unitary U› isometryD cblinfun_assoc_left(1) comp_tensor_op cblinfun_compose_id_right cblinfun_compose_id_left unitary_isometry)
    ultimately show ?thesis by simp
  qed
  then have [simp]: ‹compatible F G›
    by (auto simp: compatible_def ‹register F› ‹register G›)
  moreover have ‹iso_register (F;G)›
  proof -
    have ‹(F;G) (a ⊗⇩o b) = sandwich U (a ⊗⇩o b)› for a b
      apply (auto simp: register_pair_apply F G_def sandwich_def)
      by (metis (no_types, lifting) ‹unitary U› isometryD cblinfun_assoc_left(1) comp_tensor_op cblinfun_compose_id_right cblinfun_compose_id_left unitary_isometry)
    then have FG: ‹(F;G) = sandwich U›
      apply (rule tensor_extensionality[rotated -1])
      by (simp_all add: bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose bounded_cbilinear.add_right clinearI)
    define I where ‹I = sandwich (U*)› for x
    have [simp]: ‹register I›
      by (simp add: I_def unitary_sandwich_register)
    have ‹I o (F;G) = id› and FGI: ‹(F;G) o I = id›
       apply (auto intro!:ext simp: I_def[abs_def] FG sandwich_def)
       apply (metis (no_types, opaque_lifting) ‹unitary U› isometryD cblinfun_assoc_left(1) cblinfun_compose_id_right cblinfun_compose_id_left unitary_isometry)
      by (metis (no_types, lifting) ‹unitary U› cblinfun_assoc_left(1) cblinfun_compose_id_left cblinfun_compose_id_right unitaryD2)
    then show ‹iso_register (F;G)›
      by (auto intro!: iso_registerI)
  qed
  ultimately show ?thesis
    apply (rule_tac exI[of _ G]) by (auto)
qed

definition ‹commutant F = {x. ∀y∈F. x o⇩C⇩L y = y o⇩C⇩L x}›

lemma commutant_exchange:
  fixes F :: ‹'a::finite update ⇒ 'b::finite update›
  assumes ‹iso_register F›
  shows ‹commutant (F ` X) = F ` commutant X›
proof (rule Set.set_eqI)
  fix x :: ‹'b update›
  from assms
  obtain G where ‹F o G = id› and ‹G o F = id› and [simp]: ‹register G›
    using iso_register_def by blast
  from assms have [simp]: ‹register F›
    using iso_register_def by blast
  have ‹x ∈ commutant (F ` X) ⟷ (∀y ∈ F ` X. x o⇩C⇩L y = y o⇩C⇩L x)›
    by (simp add: commutant_def)
  also have ‹… ⟷ (∀y ∈ F ` X. G x o⇩C⇩L G y = G y o⇩C⇩L G x)›
    by (metis (no_types, opaque_lifting) ‹F ∘ G = id› ‹G o F = id› ‹register G› comp_def eq_id_iff register_def)
  also have ‹… ⟷ (∀y ∈ X. G x o⇩C⇩L y = y o⇩C⇩L G x)›
    by (simp add: ‹G ∘ F = id› pointfree_idE)
  also have ‹… ⟷ G x ∈ commutant X›
    by (simp add: commutant_def)
  also have ‹… ⟷ x ∈ F ` commutant X›
    by (metis (no_types, opaque_lifting) ‹G ∘ F = id› ‹F ∘ G = id› image_iff pointfree_idE)
  finally show ‹x ∈ commutant (F ` X) ⟷ x ∈ F ` commutant X›
    by -
qed

lemma commutant_tensor1: ‹commutant (range (λa. a ⊗⇩o id_cblinfun)) = range (λb. id_cblinfun ⊗⇩o b)›
proof (rule Set.set_eqI, rule iffI)
  fix x :: ‹('a × 'b) ell2 ⇒⇩C⇩L ('a × 'b) ell2›
  fix γ :: 'a
  assume ‹x ∈ commutant (range (λa. a ⊗⇩o id_cblinfun))›
  then have comm: ‹(a ⊗⇩o id_cblinfun) *⇩V x *⇩V ψ = x *⇩V (a ⊗⇩o id_cblinfun) *⇩V ψ› for a ψ
    by (metis (mono_tags, lifting) commutant_def mem_Collect_eq rangeI cblinfun_apply_cblinfun_compose)

  obtain x' where x': ‹cinner (ket j) (x' *⇩V ket l) = cinner (ket (γ,j)) (x *⇩V ket (γ,l))› for j l
  proof atomize_elim
    obtain ψ where ψ: ‹cinner (ket j) (ψ l) = cinner (ket (γ, j)) (x *⇩V ket (γ, l))› for l j
      apply (atomize_elim, rule choice, rule allI)
      apply (rule_tac x=‹Abs_ell2 (λj. cinner (ket (γ, j)) (x *⇩V ket (γ, l)))› in exI)
      by (simp add: cinner_ket_left Abs_ell2_inverse)
    obtain x' where ‹x' *⇩V ket l = ψ l› for l
      apply atomize_elim
      apply (rule exI[of _ ‹cblinfun_extension (range ket) (λl. ψ (inv ket l))›])
      apply (subst cblinfun_extension_apply)
        apply (rule cblinfun_extension_exists_finite_dim)
      by (auto simp add: inj_ket cindependent_ket)
    with ψ have ‹cinner (ket j) (x' *⇩V ket l) = cinner (ket (γ, j)) (x *⇩V ket (γ, l))› for j l
      by auto
    then show ‹∃x'. ∀j l. cinner (ket j) (x' *⇩V ket l) = cinner (ket (γ, j)) (x *⇩V ket (γ, l))›
      by auto
  qed

  have ‹cinner (ket (i,j)) (x *⇩V ket (k,l)) = cinner (ket (i,j)) ((id_cblinfun ⊗⇩o x') *⇩V ket (k,l))› for i j k l
  proof -
    have ‹cinner (ket (i,j)) (x *⇩V ket (k,l))
        = cinner ((butterket i γ ⊗⇩o id_cblinfun) *⇩V ket (γ,j)) (x *⇩V (butterket k γ ⊗⇩o id_cblinfun) *⇩V ket (γ,l))›
      by (auto simp: tensor_op_ket)
    also have ‹… = cinner (ket (γ,j)) ((butterket γ i ⊗⇩o id_cblinfun) *⇩V x *⇩V (butterket k γ ⊗⇩o id_cblinfun) *⇩V ket (γ,l))›
      by (metis (no_types, lifting) cinner_adj_left butterfly_adjoint id_cblinfun_adjoint tensor_op_adjoint)
    also have ‹… = cinner (ket (γ,j)) (x *⇩V (butterket γ i ⊗⇩o id_cblinfun o⇩C⇩L butterket k γ ⊗⇩o id_cblinfun) *⇩V ket (γ,l))›
      unfolding comm by (simp add: cblinfun_apply_cblinfun_compose)
    also have ‹… = cinner (ket i) (ket k) * cinner (ket (γ,j)) (x *⇩V ket (γ,l))›
      by (simp add: comp_tensor_op tensor_op_ket tensor_op_scaleC_left)
    also have ‹… = cinner (ket i) (ket k) * cinner (ket j) (x' *⇩V ket l)›
      by (simp add: x')
    also have ‹… = cinner (ket (i,j)) ((id_cblinfun ⊗⇩o x') *⇩V ket (k,l))›
      apply (simp add: tensor_op_ket)
      by (simp flip: tensor_ell2_ket)
    finally show ?thesis by -
  qed
  then have ‹x = (id_cblinfun ⊗⇩o x')›
    by (auto intro!: equal_ket cinner_ket_eqI)
  then show ‹x ∈ range (λb. id_cblinfun ⊗⇩o b)›
    by auto
next
  fix x :: ‹('a × 'b) ell2 ⇒⇩C⇩L ('a × 'b) ell2›
  assume ‹x ∈ range (λb. id_cblinfun ⊗⇩o b)›
  then obtain b where x: ‹x = id_cblinfun ⊗⇩o b›
    by auto
  then show ‹x ∈ commutant (range (λa. a ⊗⇩o id_cblinfun))›
    by (auto simp: x commutant_def comp_tensor_op)
qed

lemma complement_range:
  assumes [simp]: ‹compatible F G› and [simp]: ‹iso_register (F;G)›
  shows ‹range G = commutant (range F)›
proof -
  have [simp]: ‹register F› ‹register G›
    using assms compatible_def by metis+
  have [simp]: ‹(F;G) (a ⊗⇩o b) = F a o⇩C⇩L G b› for a b
    using Laws_Quantum.register_pair_apply assms by blast
  have [simp]: ‹range F = (F;G) ` range (λa. a ⊗⇩o id_cblinfun)›
    by force
  have [simp]: ‹range G = (F;G) ` range (λb. id_cblinfun ⊗⇩o b)›
    by force
  show ‹range G = commutant (range F)›
    by (simp add: commutant_exchange commutant_tensor1)
qed

lemma same_range_equivalent:
  fixes F :: ‹'a::finite update ⇒ 'c::finite update› and G :: ‹'b::finite update ⇒ 'c::finite update›
  assumes [simp]: ‹register F› and [simp]: ‹register G›
  assumes ‹range F = range G›
  shows ‹equivalent_registers F G›
proof -
  have G_rangeF[simp]: ‹G x ∈ range F› for x
    by (simp add: assms)
  have F_rangeG[simp]: ‹F x ∈ range G› for x
    by (simp add: assms(3)[symmetric])
  have [simp]: ‹inj F› and [simp]: ‹inj G›
    by (simp_all add: register_inj)
  have [simp]: ‹clinear F› ‹clinear G›
    by simp_all
  define I J where ‹I x = inv F (G x)› and ‹J y = inv G (F y)› for x y
  have addI: ‹I (x + y) = I x + I y› for x y
    unfolding I_def
    apply (rule injD[OF ‹inj F›])
    apply (subst complex_vector.linear_add[OF ‹clinear F›])
    apply (subst Hilbert_Choice.f_inv_into_f[where f=F], simp)+
    by (simp add: complex_vector.linear_add)
  have addJ: ‹J (x + y) = J x + J y› for x y
    unfolding J_def
    apply (rule injD[OF ‹inj G›])
    apply (subst complex_vector.linear_add[OF ‹clinear G›])
    apply (subst Hilbert_Choice.f_inv_into_f[where f=G], simp)+
    by (simp add: complex_vector.linear_add)
  have scaleI: ‹I (r *⇩C x) = r *⇩C I x› for r x
    unfolding I_def
    apply (rule injD[OF ‹inj F›])
    apply (subst complex_vector.linear_scale[OF ‹clinear F›])
    apply (subst Hilbert_Choice.f_inv_into_f[where f=F], simp)+
    by (simp add: complex_vector.linear_scale)
  have scaleJ: ‹J (r *⇩C x) = r *⇩C J x› for r x
    unfolding J_def
    apply (rule injD[OF ‹inj G›])
    apply (subst complex_vector.linear_scale[OF ‹clinear G›])
    apply (subst Hilbert_Choice.f_inv_into_f[where f=G], simp)+
    by (simp add: complex_vector.linear_scale)
  have unitalI: ‹I id_cblinfun = id_cblinfun›
    unfolding I_def
    apply (rule injD[OF ‹inj F›])
    apply (subst Hilbert_Choice.f_inv_into_f[where f=F])
     apply auto
    by (metis register_of_id G_rangeF assms(2))
  have unitalJ: ‹J id_cblinfun = id_cblinfun›
    unfolding J_def
    apply (rule injD[OF ‹inj G›])
    apply (subst Hilbert_Choice.f_inv_into_f[where f=G])
     apply auto
    by (metis register_of_id F_rangeG assms(1))
  have multI: ‹I (a o⇩C⇩L b) = I a o⇩C⇩L I b› for a b
    unfolding I_def
    apply (rule injD[OF ‹inj F›])
    apply (subst register_mult[symmetric, OF ‹register F›])
    apply (subst Hilbert_Choice.f_inv_into_f[where f=F], simp)+
    by (simp add: register_mult)
  have multJ: ‹J (a o⇩C⇩L b) = J a o⇩C⇩L J b› for a b
    unfolding J_def
    apply (rule injD[OF ‹inj G›])
    apply (subst register_mult[symmetric, OF ‹register G›])
    apply (subst Hilbert_Choice.f_inv_into_f[where f=G], simp)+
    by (simp add: register_mult)
  have adjI: ‹I (a*) = (I a)*› for a
    unfolding I_def
    apply (rule injD[OF ‹inj F›])
    apply (subst register_adjoint[OF ‹register F›])
    apply (subst Hilbert_Choice.f_inv_into_f[where f=F], simp)+
    using assms(2) register_adjoint by blast
  have adjJ: ‹J (a*) = (J a)*› for a
    unfolding J_def
    apply (rule injD[OF ‹inj G›])
    apply (subst register_adjoint[OF ‹register G›])
    apply (subst Hilbert_Choice.f_inv_into_f[where f=G], simp)+
    using assms(1) register_adjoint by blast

  from addI scaleI unitalI multI adjI
  have ‹register I›
    unfolding register_def by (auto intro!: clinearI)
  from addJ scaleJ unitalJ multJ adjJ
  have ‹register J›
    unfolding register_def by (auto intro!: clinearI)

  have ‹I o J = id›
    unfolding I_def J_def o_def
    apply (subst Hilbert_Choice.f_inv_into_f[where f=G], simp)
    apply (subst Hilbert_Choice.inv_f_f[OF ‹inj F›])
    by auto
  have ‹J o I = id›
    unfolding I_def J_def o_def
    apply (subst Hilbert_Choice.f_inv_into_f[where f=F], simp)
    apply (subst Hilbert_Choice.inv_f_f[OF ‹inj G›])
    by auto

  from ‹I o J = id› ‹J o I = id› ‹register I› ‹register J›
  have ‹iso_register I›
    using iso_register_def by blast

  have ‹F o I = G›
    unfolding I_def o_def
    by (subst Hilbert_Choice.f_inv_into_f[where f=F], auto)

  with ‹iso_register I› show ?thesis
    unfolding equivalent_registers_def by auto
qed

lemma complement_unique:
  assumes "compatible F G" and ‹iso_register (F;G)›
  assumes "compatible F H" and ‹iso_register (F;H)›
  shows ‹equivalent_registers G H›
  by (metis assms compatible_def complement_range same_range_equivalent)

end