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 CL '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 (iUNIV. P i) = id_cblinfun
    using sum_butterfly_ket P_butter by simp
  then have sumP'id: (iUNIV. 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 oCL P i) *V x') y'
      unfolding P'_def register_mult[OF register Φ, symmetric] by simp
    also have  = cinner (Φ (selfbutterket j oCL 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' = (iUNIV. 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 (iUNIV. 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 (iinsert j M. P' i) = P' j + (iM. P' i)
      by (meson insert.hyps(1) insert.hyps(2) sum.insert)
    also have  = Proj (ccspan (B j)) + Proj (ccspan (iM. B i))
      unfolding P'B insert.IH[symmetric] by simp
    also have  = Proj (ccspan (B j  (iM. B i)))
      apply (rule Proj_orthog_ccspan_union[symmetric])
      using orthoBiBj insert.hyps(2) by auto
    also have  = Proj (ccspan (iinsert 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  = (iUNIV. 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 ξ' oCL 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 α')
      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* oCL Φ (butterket ξ η) oCL 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* oCL Φ (butterket ξ η) oCL 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 ξ η oCL 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* oCL Φ (butterket ξ η) oCL U) *V ket ξ1α = (butterket ξ η o id_cblinfun) *V ket ξ1α
      by -
  qed
  then have 1: U* oCL Φ θ oCL 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 oCL (θ o id_cblinfun) oCL U* for θ
  proof -
    from unitary U
    have Φ θ = (U oCL U*) oCL Φ θ oCL (U oCL U*)
      by simp
    also have  = U oCL (U*  oCL Φ θ oCL U) oCL U*
      by (simp add: cblinfun_assoc_left)
    also have  = U oCL (θ o id_cblinfun) oCL 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 CL '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 CL _. 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 CL _

  from register_decomposition[OF register F]
  obtain V :: ('a × ('a, 'b) complement_domain) ell2 CL '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 CL '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 CL _ 
    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 oCL 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 oCL (butterfly x y o ?ida) oCL V* for x y
    by (simp add: Misc.sandwich_def FV)
  also have  x y = V oCL (butterfly (T x) (T y)) oCL V* for x y
    by (simp add: T γ γ = 1)
  also have  x y = U oCL (butterfly x y) oCL U* for x y
    by (simp add: U_def butterfly_comp_cblinfun cblinfun_comp_butterfly)
  finally have F_rep:  F a = U oCL a oCL 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 CL '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 oCL G b = G b oCL F a for a b
  proof -
    have F a oCL 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 oCL 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. yF. x oCL y = y oCL 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 oCL y = y oCL x)
    by (simp add: commutant_def)
  also have   (y  F ` X. G x oCL G y = G y oCL 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 oCL y = y oCL 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 CL ('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 oCL 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 CL ('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 oCL 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 oCL b) = I a oCL 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 oCL b) = J a oCL 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