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›
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›
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

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

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'›
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›
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)›
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 α')›
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 α')›
also have ‹… = cinner (Φ (eqa ξ' ξ *⇩C selfbutterket ξ0) *⇩V f α) (f α')›
apply simp by (metis 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 α›
also have ‹… = eqa η ξ1 *⇩C U* *⇩V Φ (butterket ξ ξ0) *⇩V f α›
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 α›
also have ‹… = (butterket ξ η ⊗⇩o id_cblinfun) *⇩V ket ξ1α›
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=θ])

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)›
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*›
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
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)›
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}›
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])
define I where ‹I = sandwich (U*)› for x
have [simp]: ‹register I›
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)›
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›
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)
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))›
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)›
also have ‹… = cinner (ket (i,j)) ((id_cblinfun ⊗⇩o x') *⇩V ket (k,l))›
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)›
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
have F_rangeG[simp]: ‹F x ∈ range G› for x
have [simp]: ‹inj F› and [simp]: ‹inj G›
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 Hilbert_Choice.f_inv_into_f[where f=F], simp)+
have addJ: ‹J (x + y) = J x + J y› for x y
unfolding J_def
apply (rule injD[OF ‹inj G›])
apply (subst Hilbert_Choice.f_inv_into_f[where f=G], simp)+
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)+
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)+
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)+
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)+
have adjI: ‹I (a*) = (I a)*› for a
unfolding I_def
apply (rule injD[OF ‹inj F›])
apply (subst Hilbert_Choice.f_inv_into_f[where f=F], simp)+
have adjJ: ‹J (a*) = (J a)*› for a
unfolding J_def
apply (rule injD[OF ‹inj G›])
apply (subst Hilbert_Choice.f_inv_into_f[where f=G], simp)+

have ‹register I›
unfolding register_def by (auto intro!: clinearI)
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
```