Theory Pure_States

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

unbundle cblinfun_syntax
unbundle register_syntax

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 clinear_register)
  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 (simp add: norm_inverse cblinfun.scaleC_right)
    by (simp flip: cblinfun.scaleC_right)
  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) o⇩C⇩L 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) (selfbutter (ket default) ⊗⇩o a) = selfbutter (ket default))›

lemma regular_registerI:
  assumes [simp]: ‹register F›
  assumes [simp]: ‹complements F G›
  assumes eq: ‹(F; G) (selfbutter (ket default) ⊗⇩o a) = selfbutter (ket 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
    using complement_unique' equivalent_registers_def equivalent_registers_sym by blast
  have ‹(F; complement F) (selfbutter (ket default) ⊗⇩o I a) = (F; G) (selfbutter (ket default) ⊗⇩o a)›
    using cFI by (auto simp: register_pair_apply)
  also have ‹… = selfbutter (ket 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 bij_FGcFG[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) (selfbutter (ket default)) = selfbutter (ket 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) (selfbutter (ket default)) = selfbutter (ket 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)) (selfbutter (ket default))›
  define t2 where ‹t2 = inv (F; (G; complement (F;G))) (selfbutter (ket default))›
  define t3 where ‹t3 = inv (G; (F; complement (F;G))) (selfbutter (ket default))›


  have ‹complements F (G; complement (F;G))›
    apply (rule complements_complement_pair)
    by simp_all
  then have ‹equivalent_registers (complement F) (G; complement (F;G))›
    using 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)) (selfbutter (ket default))›
    unfolding t2_def I
    apply (subst o_inv_distrib[symmetric]) 
    by (auto simp: pair_o_tensor)
  also have ‹… = (selfbutter (ket default) ⊗⇩o inv I aF)›
    apply simp
    by (metis ‹iso_register I› id_def iso_register_def iso_register_inv register_id register_tensor_apply)
  finally have t2': ‹t2 = selfbutter (ket default) ⊗⇩o inv I aF›
    by simp

  have *: ‹complements G (F; complement (F;G))›
    apply (rule complements_complement_pair')
    by simp_all
  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)) (selfbutter (ket default))›
    unfolding t3_def I
    apply (subst o_inv_distrib[symmetric]) 
    by (auto simp: pair_o_tensor)
  also have ‹… = (selfbutter (ket default) ⊗⇩o inv J aG)›
    apply simp
    by (metis ‹iso_register J› id_def iso_register_def iso_register_inv register_id register_tensor_apply)
  finally have t3': ‹t3 = selfbutter (ket 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)
    by (auto intro!: register_comp register_tensor_is_register pair_is_register complements_complement_pair
        simp: register_pair_apply compatible_complement_pair1 
        lift_cblinfun_comp[OF swap_registers_left, of F G] cblinfun_assoc_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 *: ‹selfbutter (ket default) ⊗⇩o inv J aG =  assoc ((swap ⊗⇩r id) (assoc' (selfbutter (ket default) ⊗⇩o inv I aF)))›
    by (simp add: t2' t3')

  have ‹selfbutter (ket default) ⊗⇩o swap (inv J aG) = (id ⊗⇩r swap) (selfbutter (ket default) ⊗⇩o inv J aG)›
    by auto
  also have ‹… = ((id ⊗⇩r swap) o assoc o (swap ⊗⇩r id) o assoc') (selfbutter (ket default) ⊗⇩o inv I aF)›
    by (simp add: *)
  also have ‹… = (assoc o swap) (selfbutter (ket 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 selfbutter (ket default))›
    by auto
  finally have *: ‹selfbutter (ket default) ⊗⇩o swap (inv J aG) = assoc (inv I aF ⊗⇩o selfbutter (ket default))›
    by -

  obtain c where *: ‹butterfly (ket default :: 'c ell2) (ket default :: 'c ell2) ⊗⇩o swap (inv J aG) = selfbutter (ket default) ⊗⇩o c ⊗⇩o selfbutter (ket default)›
    apply atomize_elim
    apply (rule overlapping_tensor)
    using * unfolding assoc_ell2_sandwich sandwich_apply
    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)) (butterfly (ket default :: 'c ell2) (ket default :: 'c ell2) ⊗⇩o swap (inv J aG))›
    unfolding t3' by auto
  also have ‹… = ((swap ⊗⇩r id) o assoc' o (id ⊗⇩r swap)) (selfbutter (ket default) ⊗⇩o c ⊗⇩o selfbutter (ket default))›
    unfolding * by simp
  also have ‹… = selfbutter (ket default) ⊗⇩o c›
    apply simp
    by (simp add: default_prod_def tensor_butterfly tensor_ell2_ket)
  finally have ‹t1 = selfbutter (ket default) ⊗⇩o c›
    by -

  then show ?thesis
    by (auto intro!: exI[of _ c] simp: regular_register_def t1_def 
        simp flip: bij_inv_eq_iff[OF bij_FGcFG])
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) (selfbutter (ket default) ⊗⇩o a) = selfbutter (ket default)›
    unfolding regular_register_def by metis
  from that obtain b where b: ‹(G; complement G) (selfbutter (ket default) ⊗⇩o b) = selfbutter (ket 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)) (selfbutter (ket default) ⊗⇩o c) = ((F o G); (complement F; F o complement G)) (selfbutter (ket 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)) (selfbutter (ket 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') (selfbutter (ket default) ⊗⇩o swap (J c))›
    by auto
  also have ‹… = ((F o (G; complement G); complement F) o assoc') (selfbutter (ket 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) ((selfbutter (ket default) ⊗⇩o b) ⊗⇩o a)›
    by (simp add: assoc'_apply)
  also have ‹… = (F; complement F) ((G;complement G) (selfbutter (ket default) ⊗⇩o b) ⊗⇩o a)›
    by (simp add: register_pair_apply')
  also have ‹… = selfbutter (ket default)›
    by (auto simp: a b) 
  finally have ‹(F ∘ G;complement (F ∘ G)) (selfbutter (ket default) ⊗⇩o c) = selfbutter (ket 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 (selfbutter (ket default)) = selfbutter (ket default)›
proof -
  from assms(1) obtain a where a: ‹(F;complement F) (selfbutter (ket default) ⊗⇩o a) = selfbutter (ket default)›
    using regular_register_def by blast

  let ?u = ‹empty_var :: (unit ell2 ⇒⇩C⇩L 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 ‹selfbutter (ket default) = (F; ?u o I) (selfbutter (ket default) ⊗⇩o a)›
    using ‹complement F = empty_var ∘ I› a by presburger
  also have ‹… = (F; ?u) (selfbutter (ket 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) (selfbutter (ket default) ⊗⇩o (one_dim_iso (I a) *⇩C id_cblinfun))›
    by simp
  also have ‹… = one_dim_iso (I a) *⇩C (F; ?u) (selfbutter (ket 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 (selfbutter (ket 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 (selfbutter (ket default)) = selfbutter (ket 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 ‹selfbutter (ket default) = one_dim_iso (I a) *⇩C F (selfbutter (ket default))›
    using F by simp
  also have ‹… = one_dim_iso (I a) *⇩C F (selfbutter (ket default) o⇩C⇩L selfbutter (ket default))›
    by auto
  also have ‹… = one_dim_iso (I a) *⇩C (F (selfbutter (ket default)) o⇩C⇩L F (selfbutter (ket default)))›
    by (simp add: assms(2) iso_register_is_register register_mult)
  also have ‹… = one_dim_iso (I a) *⇩C ((selfbutter (ket default) /⇩C one_dim_iso (I a)) o⇩C⇩L (selfbutter (ket 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 selfbutter (ket 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 (selfbutter (ket default)) = selfbutter (ket 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 (selfbutter (ket default)) = selfbutter (ket 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 simp
    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)) o⇩C⇩L selfbutter (ket default)›
    by (metis (no_types, opaque_lifting) adj_cblinfun_compose butterfly_adjoint butterfly_comp_cblinfun double_adj)
  also have ‹… = H (butterfly h (ket default)) o⇩C⇩L H (selfbutter (ket default))›
    by simp
  also have ‹… = H (butterfly h (ket default) o⇩C⇩L selfbutter (ket 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=‹selfbutter (ket default)› and G=Snd])
  by (auto simp: pair_Fst_Snd default_prod_def tensor_ell2_ket tensor_butterfly)

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

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_apply c_def cinner_adj_right cblinfun.scaleC_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_apply cinner_adj_right cblinfun.scaleC_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 cblinfun.scaleC_right)
  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
  ‹F⇩1(ψ⇩1) ⊗⇩p F⇩2(ψ⇩2) ⊗⇩p … ⊗⇩p F⇩n(ψ⇩n)› by reordering the registers and unfolding nested register pairs.
  (For the unfolding of nested pairs, it is necessary that the corresponding \<^term>‹compatible 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 o⇩C⇩L (G;F) CNOT o⇩C⇩L (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 complement_is_complement complements_complement_pair complements_def pair_is_register by blast

  have eq1: ‹((F;G) CNOT o⇩C⇩L (G;F) CNOT o⇩C⇩L (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 simp: tensor_ell2_ket)
    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 simp: tensor_ell2_ket)
    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
      by (metis add_diff_cancel_left' cnot_apply minus_bit_def tensor_ell2_ket)
    also have ‹… = (F(ket g) ⊗⇩p G(ket f) ⊗⇩p Z(ket z))›
      by pure_state_eq
    finally have 1: ‹((F;G) CNOT o⇩C⇩L (G;F) CNOT o⇩C⇩L (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 o⇩C⇩L (G;F) CNOT o⇩C⇩L (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 simp: tensor_ell2_ket)

  ultimately show ?thesis
    using cblinfun_eq_on_UNIV_span by blast
qed

unbundle no cblinfun_syntax
unbundle no register_syntax

end