Theory Pure_States

theory Pure_States
  imports Quantum_Extra2 "HOL-Eisbach.Eisbach"
begin

definition pure_state_target_vector F ηF = (if ket default  range (cblinfun_apply (F (butterfly ηF ηF)))
   then ket default
   else (SOME η'. norm η' = 1  η'  range (cblinfun_apply (F (butterfly ηF ηF)))))

lemma pure_state_target_vector_eqI:
  assumes F (butterfly ηF ηF) = G (butterfly ηG ηG)
  shows pure_state_target_vector F ηF = pure_state_target_vector G ηG
  by (simp add: assms pure_state_target_vector_def)

lemma pure_state_target_vector_ket_default: pure_state_target_vector F ηF = ket default if ket default  range (cblinfun_apply (F (butterfly ηF ηF)))
  by (simp add: pure_state_target_vector_def that)

lemma
  assumes [simp]: ηF  0 register F
  shows pure_state_target_vector_in_range: pure_state_target_vector F ηF  range ((*V) (F (selfbutter ηF))) (is ?range)
    and pure_state_target_vector_norm: norm (pure_state_target_vector F ηF) = 1 (is ?norm)
proof -
  from assms have selfbutter ηF  0
    by (metis butterfly_0_right complex_vector.scale_zero_right inj_selfbutter_upto_phase)
  then have F (selfbutter ηF)  0
    using register_inj[OF register F, THEN injD, where y=0]
    by (auto simp: complex_vector.linear_0)
  then obtain ψ' where ψ': F (selfbutter ηF) *V ψ'  0
    by (meson cblinfun_eq_0_on_UNIV_span complex_vector.span_UNIV)
  have ex: ψ. norm ψ = 1  ψ  range ((*V) (F (selfbutter ηF)))
    apply (rule exI[of _ (F (selfbutter ηF) *V ψ') /C norm (F (selfbutter ηF) *V ψ')])
    using ψ' apply (auto simp add: norm_inverse)
    by (metis cblinfun.scaleC_right rangeI)
  then show ?range
    by (metis (mono_tags, lifting) pure_state_target_vector_def verit_sko_ex')
  show ?norm
    apply (simp add: pure_state_target_vector_def)
    using ex by (metis (mono_tags, lifting) verit_sko_ex')
qed


lemma pure_state_target_vector_correct: 
  assumes [simp]: η  0 register F
  shows F (selfbutter η) *V pure_state_target_vector F η  0
proof -
  obtain ψ where ψ: F (selfbutter η) ψ = pure_state_target_vector F η
    apply atomize_elim
    using pure_state_target_vector_in_range[OF assms]
    by (smt (verit, best) image_iff top_ccsubspace.rep_eq top_set_def)

  define n where n = cinner η η
  then have n  0
    by auto

  have pure_state_target_vector_neq0: pure_state_target_vector F η  0
    using pure_state_target_vector_norm[OF assms]
    by auto

  have F (selfbutter η) *V pure_state_target_vector F η = F (selfbutter η) *V F (selfbutter η) *V ψ
    by (simp add: ψ)
  also have  = n *C F (selfbutter η) *V ψ
    by (simp flip: cblinfun_apply_cblinfun_compose add: register_mult register_scaleC n_def)
  also have  = n *C pure_state_target_vector F η
    by (simp add: ψ)
  also have   0
    using pure_state_target_vector_neq0 n  0
    by auto
  finally show ?thesis
    by -
qed

definition pure_state' F ψ ηF = F (butterfly ψ ηF) *V pure_state_target_vector F ηF

abbreviation pure_state F ψ  pure_state' F ψ (ket default)

nonterminal pure_tensor
syntax "_pure_tensor" :: 'a  'b  pure_tensor  pure_tensor ("_ _ p _" [1000, 0, 0] 1000)
syntax "_pure_tensor2" :: 'a  'b  'c  'd  pure_tensor ("_ _ p _ _" [1000, 0, 1000, 0] 1000)
syntax "_pure_tensor1" :: 'a  'b  pure_tensor
syntax "_pure_tensor_start" :: pure_tensor  'a ("'(_')")

translations
  "_pure_tensor2 F ψ G φ"  "CONST pure_state (F; G) (ψ s φ)"
  "_pure_tensor F ψ (CONST pure_state G φ)"  "CONST pure_state (F; G) (ψ s φ)"
  "_pure_tensor_start x"  "x"

  "_pure_tensor_start (_pure_tensor2 F ψ G φ)"  "CONST pure_state (F; G) (ψ s φ)"
  "_pure_tensor F ψ (_pure_tensor2 G φ H η)"  "_pure_tensor2 F ψ (G;H) (φ s η)"

term (F ψ p G φ p H z)
term pure_state (F; G) (a s b)

lemma register_pair_butterfly_tensor: (F; G) (butterfly (a s b) (c s d)) = F (butterfly a c) oCL G (butterfly b d)
  if [simp]: compatible F G
  by (auto simp: default_prod_def simp flip: tensor_ell2_ket tensor_butterfly register_pair_apply)

lemma pure_state_eqI:
  assumes F (selfbutter ηF) = G (selfbutter ηG)
  assumes F (butterfly ψ ηF) = G (butterfly φ ηG)
  shows pure_state' F ψ ηF = pure_state' G φ ηG
proof -
  from assms(1) have pure_state_target_vector F ηF = pure_state_target_vector G ηG
    by (rule pure_state_target_vector_eqI)
  with assms(2)
  show ?thesis
    unfolding pure_state'_def
    by simp
qed


definition regular_register F  register F  (a. (F; complement F) (selfbutterket default o a) = selfbutterket default)

lemma regular_registerI:
  assumes [simp]: register F
  assumes [simp]: complements F G
  assumes eq: (F; G) (selfbutterket default o a) = selfbutterket default
  shows regular_register F
proof -
  have [simp]: compatible F G
    using assms by (simp add: complements_def)
  from complements F G
  obtain I where cFI: complement F o I = G and iso_register I
    apply atomize_elim
    by (meson Laws_Complement_Quantum.complement_unique equivalent_registers_def equivalent_registers_sym)
  have (F; complement F) (selfbutterket default o I a) = (F; G) (selfbutterket default o a)
    using cFI by (auto simp: register_pair_apply)
  also have  = selfbutterket default
    by (rule eq)
  finally show ?thesis
    unfolding regular_register_def by auto
qed

lemma regular_register_pair:
  assumes [simp]: compatible F G
  assumes regular_register F and regular_register G
  shows regular_register (F;G)
proof -
  have [simp]: bij (F;complement F) bij (G;complement G)
    using assms(1) compatible_def complement_is_complement complements_def iso_register_bij by blast+
  have [simp]: bij ((F;G);complement (F;G))
    using assms(1) complement_is_complement complements_def iso_register_bij pair_is_register by blast
  have [simp]: register F register G
    using assms(1) unfolding compatible_def by auto

  obtain aF where [simp]: inv (F;complement F) (selfbutterket default) = selfbutterket default o aF
    by (metis assms(2) compatible_complement_right invI pair_is_register register_inj regular_register_def)
  obtain aG where [simp]: inv (G;complement G) (selfbutterket default) = selfbutterket default o aG
    by (metis assms(3) complement_is_complement complements_def inj_iff inv_f_f iso_register_inv_comp1 regular_register_def)
  define t1 where t1 = inv ((F;G); complement (F;G)) (selfbutterket default)
  define t2 where t2 = inv (F; (G; complement (F;G))) (selfbutterket default)
  define t3 where t3 = inv (G; (F; complement (F;G))) (selfbutterket default)


  have complements F (G; complement (F;G))
    apply (rule complements_complement_pair)
    by simp
  then have equivalent_registers (complement F) (G; complement (F;G))
    using Laws_Complement_Quantum.complement_unique equivalent_registers_sym by blast
  then obtain I where [simp]: iso_register I and I: (G; complement (F;G)) = complement F o I
    by (metis equivalent_registers_def)
  then have [simp]: register I
    by (meson iso_register_is_register)
  have [simp]: bij (id r I)
    by (rule iso_register_bij, simp)
  have [simp]: inv (id r I) = id r inv I
    by auto

  have t2 = (inv (id r I) o inv (F;complement F)) (selfbutterket default)
    unfolding t2_def I
    apply (subst o_inv_distrib[symmetric]) 
    by (auto simp: pair_o_tensor)
  also have  = (selfbutterket default o inv I aF)
    apply auto
    by (metis iso_register I id_def iso_register_def iso_register_inv register_id register_tensor_apply)
  finally have t2': t2 = selfbutterket default o inv I aF
    by simp

  have *: complements G (F; complement (F;G))
    apply (rule complements_complement_pair')
    by simp
  then have [simp]: compatible G (F; complement (F;G))
    using complements_def by blast
  from * have equivalent_registers (complement G) (F; complement (F;G))
    using complement_unique equivalent_registers_sym by blast
  then obtain J where [simp]: iso_register J and I: (F; complement (F;G)) = complement G o J
    by (metis equivalent_registers_def)
  then have [simp]: register J
    by (meson iso_register_is_register)
  have [simp]: bij (id r J)
    by (rule iso_register_bij, simp)
  have [simp]: inv (id r J) = id r inv J
    by auto

  have t3 = (inv (id r J) o inv (G;complement G)) (selfbutterket default)
    unfolding t3_def I
    apply (subst o_inv_distrib[symmetric]) 
    by (auto simp: pair_o_tensor)
  also have  = (selfbutterket default o inv J aG)
    apply auto
    by (metis iso_register J id_def iso_register_def iso_register_inv register_id register_tensor_apply)
  finally have t3': t3 = selfbutterket default o inv J aG
    by simp

  have *: ((F;G); complement (F;G)) o assoc' = (F; (G; complement (F;G)))
    apply (rule tensor_extensionality3)
    by (auto simp: register_pair_apply  compatible_complement_pair1 compatible_complement_pair2)
  have t2_t1: t2 = assoc t1
    unfolding t1_def t2_def *[symmetric] apply (subst o_inv_distrib)
    by auto

  have *: ((F;G); complement (F;G)) o (swap r id) o assoc' = (G; (F; complement (F;G)))
    apply (rule tensor_extensionality3)
      apply (auto intro!: register_comp register_tensor_is_register pair_is_register complements_complement_pair
        simp: register_pair_apply compatible_complement_pair1)
    by (metis assms(1) cblinfun_assoc_left(1) swap_registers_left)
  have t3_t1: t3 = assoc ((swap r id) t1)
    unfolding t1_def t3_def *[symmetric] apply (subst o_inv_distrib)
    by (auto intro!: bij_comp simp: iso_register_bij o_inv_distrib)

  from t2 = assoc t1 t3 = assoc ((swap r id) t1)
  have *: selfbutterket default o inv J aG =  assoc ((swap r id) (assoc' (selfbutterket default o inv I aF)))
    by (simp add: t2' t3')

  have selfbutterket default o swap (inv J aG) = (id r swap) (selfbutterket default o inv J aG)
    by auto
  also have  = ((id r swap) o assoc o (swap r id) o assoc') (selfbutterket default o inv I aF)
    by (simp add: *)
  also have  = (assoc o swap) (selfbutterket default o inv I aF)
    apply (rule fun_cong[where g=assoc o swap])
    apply (intro tensor_extensionality3 register_comp register_tensor_is_register)
    by auto
  also have  = assoc (inv I aF o selfbutterket default)
    by auto
  finally have *: selfbutterket default o swap (inv J aG) = assoc (inv I aF o selfbutterket default)
    by -

  obtain c where *: selfbutterket (default::'c) o swap (inv J aG) = selfbutterket default o c o selfbutterket default
    apply atomize_elim
    apply (rule overlapping_tensor)
    using * unfolding assoc_ell2_sandwich sandwich_def
    by auto

  have t1 = ((swap r id) o assoc') t3
    by (simp add: t3_t1 register_tensor_distrib[unfolded o_def, THEN fun_cong] flip: id_def)
  also have  = ((swap r id) o assoc' o (id r swap)) (selfbutterket (default::'c) o swap (inv J aG))
    unfolding t3' by auto
  also have  = ((swap r id) o assoc' o (id r swap)) (selfbutterket default o c o selfbutterket default)
    unfolding * by simp
  also have  = selfbutterket default o c
    apply (simp del: tensor_butterfly)
    by (simp add: default_prod_def)
  finally have t1 = selfbutterket default o c
    by -

  then show ?thesis
    apply (auto intro!: exI[of _ c] simp: regular_register_def t1_def)
    by (metis bij ((F;G);complement (F;G)) bij_inv_eq_iff)
qed

lemma regular_register_comp: regular_register (F o G) if regular_register F regular_register G
proof -
  have [simp]: register F register G
    using regular_register_def that by blast+
  from that obtain a where a: (F; complement F) (selfbutterket default o a) = selfbutterket default
    unfolding regular_register_def by metis
  from that obtain b where b: (G; complement G) (selfbutterket default o b) = selfbutterket default
    unfolding regular_register_def by metis
  have complements (F o G) (complement F; F o complement G)
    by (simp add: complements_chain)
  then have equivalent_registers (complement F; F o complement G) (complement (F o G))
    using complement_unique by blast
  then obtain J where [simp]: iso_register J and 1: (complement F; F o complement G) o J = (complement (F o G))
    using equivalent_registers_def by blast
  have [simp]: register J
    by (simp add: iso_register_is_register)

  define c where c = inv J (a o b)

  have ((F o G); complement (F o G)) (selfbutterket default o c) = ((F o G); (complement F; F o complement G)) (selfbutterket default o J c)
    by (auto simp flip: 1 simp: register_pair_apply)
  also have  = ((F o (G; complement G); complement F) o assoc' o (id r swap)) (selfbutterket default o J c)
    apply (subst register_comp_pair[symmetric])
      apply auto[2]
    apply (subst pair_o_assoc')
       apply auto[3]
    apply (subst pair_o_tensor)
    by auto
  also have  = ((F o (G; complement G); complement F) o assoc') (selfbutterket default o swap (J c))
    by auto
  also have  = ((F o (G; complement G); complement F) o assoc') (selfbutterket default o (b o a))
    unfolding c_def apply (subst surj_f_inv_f[where f=J])
     apply (meson iso_register J bij_betw_inv_into_right iso_register_inv_comp1 iso_register_inv_comp2 iso_tuple_UNIV_I o_bij surj_iff_all)
    by auto
  also have  = (F  (G;complement G);complement F) ((selfbutterket default o b) o a)
    by (simp add: assoc'_apply)
  also have  = (F; complement F) ((G;complement G) (selfbutterket default o b) o a)
    by (simp add: register_pair_apply')
  also have  = selfbutterket default
    by (auto simp: a b) 
  finally have (F  G;complement (F  G)) (selfbutterket default o c) = selfbutterket default
    by -
  then show ?thesis
    using register F register G register_comp regular_register_def by blast
qed

lemma regular_iso_register:
  assumes regular_register F
  assumes [register]: iso_register F
  shows F (selfbutterket default) = selfbutterket default
proof -
  from assms(1) obtain a where a: (F;complement F) (selfbutterket default o a) = selfbutterket default
    using regular_register_def by blast

  let ?u = empty_var :: (unit ell2 CL unit ell2)  _
  have is_unit_register ?u and is_unit_register (complement F)
    by auto
  then have equivalent_registers (complement F) ?u
    using unit_register_unique by blast
  then obtain I where iso_register I and complement F = ?u o I
    by (metis is_unit_register (complement F) equivalent_registers_def is_unit_register_empty_var unit_register_unique)
  have selfbutterket default = (F; ?u o I) (selfbutterket default o a)
    using complement F = empty_var  I a by presburger
  also have  = (F; ?u) (selfbutterket default o I a)
    by (metis Laws_Quantum.register_pair_apply complement F = empty_var  I equivalent_registers (complement F) empty_var assms(2) comp_apply complement_is_complement complements_def equivalent_complements iso_register_is_register)
  also have  = (F; ?u) (selfbutterket default o (one_dim_iso (I a) *C id_cblinfun))
    by simp
  also have  = one_dim_iso (I a) *C (F; ?u) (selfbutterket default o id_cblinfun)
    by (simp add: Axioms_Quantum.register_pair_apply empty_var_def iso_register_is_register)
  also have  = one_dim_iso (I a) *C F (selfbutterket default)
    by (auto simp: register_pair_apply iso_register_is_register simp del: id_cblinfun_eq_1)
  finally have F: one_dim_iso (I a) *C F (selfbutterket default) = selfbutterket default
    by simp

  from F have one_dim_iso (I a)  (0::complex)
    by (metis butterfly_apply butterfly_scaleC_left complex_vector.scale_eq_0_iff id_cblinfun_eq_1 id_cblinfun_not_0 cinner_ket_same ket_nonzero one_dim_iso_of_one one_dim_iso_of_zero')

  have selfbutterket default = one_dim_iso (I a) *C F (selfbutterket default)
    using F by simp
  also have  = one_dim_iso (I a) *C F (selfbutterket default oCL selfbutterket default)
    by auto
  also have  = one_dim_iso (I a) *C (F (selfbutterket default) oCL F (selfbutterket default))
    by (simp add: assms(2) iso_register_is_register register_mult)
  also have  = one_dim_iso (I a) *C ((selfbutterket default /C one_dim_iso (I a)) oCL (selfbutterket default /C one_dim_iso (I a)))
    by (metis (no_types, lifting) F one_dim_iso (I a)  0 complex_vector.scale_left_imp_eq inverse_1 left_inverse scaleC_scaleC zero_neq_one)
  also have  = one_dim_iso (I a) *C selfbutterket default
    by (smt (verit, best) butterfly_comp_butterfly calculation cblinfun_compose_scaleC_left cblinfun_compose_scaleC_right complex_vector.scale_cancel_left cinner_ket_same left_inverse scaleC_one scaleC_scaleC)
  finally have one_dim_iso (I a) = (1::complex)
    by (metis butterfly_0_left butterfly_apply complex_vector.scale_cancel_right cinner_ket_same ket_nonzero scaleC_one)
  with F show F (selfbutterket default) = selfbutterket default
    by simp
qed

lemma pure_state_nested:
  assumes [simp]: compatible F G
  assumes regular_register H
  assumes iso_register H
  shows pure_state (F;G) (pure_state H h s g) = pure_state ((F o H);G) (h s g)
proof -
  note [[simproc del: Laws_Quantum.compatibility_warn]]
  have [simp]: register H
    by (meson assms(3) iso_register_is_register)
  have [simp]: H (selfbutterket default) = selfbutterket default
    apply (rule regular_iso_register)
    using assms by auto
  have 1: pure_state_target_vector H (ket default) = ket default
    apply (rule pure_state_target_vector_ket_default)
    apply auto
    by (metis (no_types, lifting) cinner_ket_same rangeI scaleC_one)

  have butterfly (pure_state H h) (ket default) = butterfly (H (butterfly h (ket default)) *V ket default) (ket default)
    by (simp add: pure_state'_def 1)
  also have  = H (butterfly h (ket default)) oCL selfbutterket default
    by (metis (no_types, opaque_lifting) adj_cblinfun_compose butterfly_adjoint butterfly_comp_cblinfun double_adj)
  also have  = H (butterfly h (ket default)) oCL H (selfbutterket default)
    by simp
  also have  = H (butterfly h (ket default) oCL selfbutterket default)
    by (meson register H register_mult)
  also have  = H (butterfly h (ket default))
    by auto
  finally have 2: butterfly (pure_state H h) (ket default) = H (butterfly h (ket default))
    by simp

  show ?thesis
    apply (rule pure_state_eqI)
    using 1 2
    by (auto simp: register_pair_butterfly_tensor compatible_ac_rules default_prod_def simp flip: tensor_ell2_ket)
qed

lemma state_apply1: 
  assumes [register]: compatible F G
  shows F U *V (F ψ p G φ) = (F (U ψ) p G φ)
proof -
  have [register]: compatible F G
    using assms(1) complements_def by blast
  have F U *V (F ψ p G φ) = (F;G) (U o id_cblinfun) *V (F ψ p G φ)
    apply (subst register_pair_apply)
    by auto
  also have  = (F (U ψ) p G φ)
    unfolding pure_state'_def 
    by (auto simp: register_mult' cblinfun_comp_butterfly tensor_op_ell2)
  finally show ?thesis
    by -
qed

lemma Fst_regular[simp]: regular_register Fst
  apply (rule regular_registerI[where a=selfbutterket default and G=Snd])
  by (auto simp: pair_Fst_Snd default_prod_def)

lemma Snd_regular[simp]: regular_register Snd
  apply (rule regular_registerI[where a=selfbutterket default and G=Fst])
    apply auto[2]
  apply (auto simp only: default_prod_def swap_apply simp flip: swap_def)
  by auto

lemma id_regular[simp]: regular_register id
  apply (rule regular_registerI[where G=unit_register and a=id_cblinfun])
  by (auto simp: register_pair_apply)

lemma swap_regular[simp]: regular_register swap
  by (auto intro!: regular_register_pair simp: swap_def)

lemma assoc_regular[simp]: regular_register assoc
  by (auto intro!: regular_register_pair regular_register_comp simp: assoc_def)

lemma assoc'_regular[simp]: regular_register assoc'
  by (auto intro!: regular_register_pair regular_register_comp simp: assoc'_def)

lemma cspan_pure_state': 
  assumes iso_register F
  assumes cspan (g ` X) = UNIV
  assumes η_cond: F (selfbutter η) *V pure_state_target_vector F η  0
  shows cspan ((λz. pure_state' F (g z) η) ` X) = UNIV
proof -
  from iso_register_decomposition[of F]
  obtain U where [simp]: unitary U and F: F = sandwich U
    using assms(1) by blast

  define η' c where η' = pure_state_target_vector F η and c = cinner (U *V η) η'

  from η_cond
  have c  0
    by (simp add: η'_def F sandwich_def c_def cinner_adj_right)

  have cspan ((λz. pure_state' F (g z) η) ` X) = cspan ((λz. F (butterfly (g z) η) *V η') ` X)
    by (simp add: η'_def pure_state'_def)
  also have  = cspan ((λz. (butterfly (U *V g z) (U *V η)) *V η') ` X)
    by (simp add: F sandwich_def cinner_adj_right)
  also have  = cspan ((λz. c *C U *V g z) ` X)
    by (simp add: c_def)
  also have  = (λz. c *C U *V z) ` cspan (g ` X)
    apply (subst complex_vector.linear_span_image[symmetric])
    by (auto simp: image_image)
  also have  = (λz. c *C U *V z) ` UNIV
    using assms(2) by presburger
  also have  = UNIV
    apply (rule surjI[where f=λz. (U* *V z) /C c])
    using c  0 by (auto simp flip: cblinfun_apply_cblinfun_compose)
  finally show ?thesis
    by -
qed

lemma cspan_pure_state: 
  assumes [simp]: iso_register F
  assumes cspan (g ` X) = UNIV
  shows cspan ((λz. pure_state F (g z)) ` X) = UNIV
  apply (rule cspan_pure_state')
  using assms apply auto[2]
  apply (rule pure_state_target_vector_correct)
  by (auto simp: iso_register_is_register)

lemma pure_state_bounded_clinear:
  assumes [register]: compatible F G
  shows bounded_clinear (λψ. (F ψ p G φ))
proof -
  have [bounded_clinear]: bounded_clinear (F;G)
    using assms pair_is_register register_bounded_clinear by blast
  show ?thesis
    unfolding pure_state'_def
    by (auto intro!: bounded_linear_intros)
qed

lemma pure_state_bounded_clinear_right:
  assumes [register]: compatible F G
  shows bounded_clinear (λφ. (F ψ p G φ))
proof -
  have [bounded_clinear]: bounded_clinear (F;G)
    using assms pair_is_register register_bounded_clinear by blast
  show ?thesis
    unfolding pure_state'_def
    by (auto intro!: bounded_linear_intros)
qed

lemma pure_state_clinear:
  assumes [register]: compatible F G
  shows clinear (λψ. (F ψ p G φ))
  using assms bounded_clinear.clinear pure_state_bounded_clinear by blast

method pure_state_flatten_nested =
  (subst pure_state_nested, (auto; fail)[3])+

text The following method pure_state_eq› tries to solve a equality where both sides are of the form
  F11) ⊗p F22) ⊗p … ⊗p Fnn)› by reordering the registers and unfolding nested register pairs.
  (For the unfolding of nested pairs, it is necessary that the corresponding termcompatible F G facts are provable by the simplifier.)

  If the some of the pure states termψi themselves are p-tensors, they will be flattened if possible. 
  (If all necessary conditions can be proven, such as regular_register› etc.)

  The method may either succeed, fail, or reduce the equality to a hopefully simpler one.

method pure_state_eq =
  (pure_state_flatten_nested?,
    rule pure_state_eqI;
    auto simp: register_pair_butterfly_tensor compatible_ac_rules default_prod_def
    simp flip: tensor_ell2_ket)

lemma example:
  fixes F :: bit update  'c::{finite,default} update
    and G :: bit update  'c update
  assumes [register]: compatible F G
  shows  (F;G) CNOT oCL (G;F) CNOT oCL (F;G) CNOT = (F;G) swap_ell2
proof -
  define Z where Z = complement (F;G)
  then have [register]: compatible Z F compatible Z G
    using assms compatible_complement_pair1 compatible_complement_pair2 compatible_sym by blast+

  have [simp]: iso_register (F;(G;Z))
    using Z_def assms complements_complement_pair complements_def by blast

  have eq1: ((F;G) CNOT oCL (G;F) CNOT oCL (F;G) CNOT) *V (F(ket f) p G(ket g) p Z(ket z))
           = (F;G) swap_ell2 *V (F(ket f) p G(ket g) p Z(ket z)) for f g z
  proof -
    have (F(ket f) p G(ket g) p Z(ket z)) = ((F;G) (ket f s ket g) p Z(ket z))
      by pure_state_eq
    also have (F;G) CNOT *V  = ((F;G) (ket f s ket (g+f)) p Z(ket z))
      apply (subst state_apply1) by auto
    also have  = ((G;F) (ket (g+f) s ket f) p Z(ket z))
      by pure_state_eq
    also have (G;F) CNOT *V  = ((G;F) (ket (g+f) s ket g) p Z ket z)
      apply (subst state_apply1) by auto
    also have  = ((F;G) (ket g s ket (g+f)) p Z ket z)
      by pure_state_eq
    also have (F;G) CNOT *V  = ((F;G) ket g s ket f p Z ket z)
      apply (subst state_apply1)
      apply simp
      using add_right_imp_eq by fastforce
    also have  = (F(ket g) p G(ket f) p Z(ket z))
      by pure_state_eq
    finally have 1: ((F;G) CNOT oCL (G;F) CNOT oCL (F;G) CNOT) *V (F(ket f) p G(ket g) p Z(ket z)) = (F(ket g) p G(ket f) p Z(ket z))
      by auto

    have (F(ket f) p G(ket g) p Z(ket z)) = ((F;G) (ket f s ket g) p Z(ket z))
      by pure_state_eq
    also have (F;G) swap_ell2 *V  = ((F;G) (ket g s ket f) p Z(ket z))
      by (auto simp: state_apply1 swap_ell2_tensor simp del: tensor_ell2_ket)
    also have  = (F(ket g) p G(ket f) p Z(ket z))
      by pure_state_eq
    finally have 2: (F;G) swap_ell2 *V (F(ket f) p G(ket g) p Z(ket z)) = (F(ket g) p G(ket f) p Z(ket z))
      by -

    from 1 2 show ?thesis
      by simp
  qed

  then have eq1: ((F;G) CNOT oCL (G;F) CNOT oCL (F;G) CNOT) *V ψ
           = (F;G) swap_ell2 *V ψ if ψ  {(F(ket f) p G(ket g) p Z(ket z))| f g z. True} for ψ
    using that by auto

  moreover have cspan {(F(ket f) p G(ket g) p Z(ket z))| f g z. True} = UNIV
    apply (simp only: double_exists setcompr_eq_image full_SetCompr_eq)
    apply simp
    apply (rule cspan_pure_state)
    by auto

  ultimately show ?thesis
    using cblinfun_eq_on_UNIV_span by blast
qed

end