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

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

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
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 ψ›
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 η›
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) (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)))›

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

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)›
also have ‹… = (F; complement F) ((G;complement G) (selfbutterket default ⊗⇩o b) ⊗⇩o a)›
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 ⇒⇩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 ‹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 o⇩C⇩L selfbutterket default)›
by auto
also have ‹… = one_dim_iso (I a) *⇩C (F (selfbutterket default) o⇩C⇩L 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)) o⇩C⇩L (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)›
also have ‹… = H (butterfly h (ket default)) o⇩C⇩L selfbutterket default›
also have ‹… = H (butterfly h (ket default)) o⇩C⇩L H (selfbutterket default)›
by simp
also have ‹… = H (butterfly h (ket default) o⇩C⇩L 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›

have ‹cspan ((λz. pure_state' F (g z) η) ` X) = cspan ((λz. F (butterfly (g z) η) *⇩V η') ` X)›
also have ‹… = cspan ((λz. (butterfly (U *⇩V g z) (U *⇩V η)) *⇩V η') ` X)›
also have ‹… = cspan ((λz. c *⇩C U *⇩V g z) ` X)›
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
‹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 complements_complement_pair complements_def 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
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
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

ultimately show ?thesis
using cblinfun_eq_on_UNIV_span by blast
qed

end
```