# Theory Quantum_Extra

```section ‹Derived facts about quantum registers›

theory Quantum_Extra
imports
Laws_Quantum
Quantum
begin

no_notation meet (infixl "⊓ı" 70)
no_notation Group.mult (infixl "⊗ı" 70)
no_notation Order.top ("⊤ı")
unbundle lattice_syntax
unbundle register_notation
unbundle cblinfun_notation

lemma zero_not_register[simp]: ‹~ register (λ_. 0)›
unfolding register_def by simp

lemma register_pair_is_register_converse:
‹register (F;G) ⟹ register F› ‹register (F;G) ⟹ register G›
using [[simproc del: Laws_Quantum.compatibility_warn]]
apply (cases ‹register F›)
apply (auto simp: register_pair_def)[2]
apply (cases ‹register G›)
by (auto simp: register_pair_def)[2]

lemma register_id'[simp]: ‹register (λx. x)›
using register_id by (simp add: id_def)

lemma register_projector:
assumes "register F"
assumes "is_Proj a"
shows "is_Proj (F a)"
using assms unfolding register_def is_Proj_algebraic by metis

lemma register_unitary:
assumes "register F"
assumes "unitary a"
shows "unitary (F a)"
using assms by (smt (verit, best) register_def unitary_def)

lemma compatible_proj_intersect:
(* I think this also holds without is_Proj premises, but my proof ideas use the Penrose-Moore
pseudoinverse or simultaneous diagonalization and we do not have an existence theorem for either. *)
assumes "compatible R S" and "is_Proj a" and "is_Proj b"
shows "(R a *⇩S ⊤) ⊓ (S b *⇩S ⊤) = ((R a o⇩C⇩L S b) *⇩S ⊤)"
proof (rule antisym)
have "((R a o⇩C⇩L S b) *⇩S ⊤) ≤ (S b *⇩S ⊤)"
apply (subst swap_registers[OF assms(1)])
moreover have "((R a o⇩C⇩L S b) *⇩S ⊤) ≤ (R a *⇩S ⊤)"
ultimately show ‹((R a o⇩C⇩L S b) *⇩S ⊤) ≤ (R a *⇩S ⊤) ⊓ (S b *⇩S ⊤)›
by auto

have "is_Proj (R a)"
using assms(1) assms(2) compatible_register1 register_projector by blast
have "is_Proj (S b)"
using assms(1) assms(3) compatible_register2 register_projector by blast
show ‹(R a *⇩S ⊤) ⊓ (S b *⇩S ⊤) ≤ (R a o⇩C⇩L S b) *⇩S ⊤›
proof (unfold less_eq_ccsubspace.rep_eq, rule)
fix ψ
assume asm: ‹ψ ∈ space_as_set ((R a *⇩S ⊤) ⊓ (S b *⇩S ⊤))›
then have ‹ψ ∈ space_as_set (R a *⇩S ⊤)›
by auto
then have R: ‹R a *⇩V ψ = ψ›
using ‹is_Proj (R a)› cblinfun_fixes_range is_Proj_algebraic by blast
from asm have ‹ψ ∈ space_as_set (S b *⇩S ⊤)›
by auto
then have S: ‹S b *⇩V ψ = ψ›
using ‹is_Proj (S b)› cblinfun_fixes_range is_Proj_algebraic by blast
from R S have ‹ψ = (R a o⇩C⇩L S b) *⇩V ψ›
also have ‹… ∈ space_as_set ((R a o⇩C⇩L S b) *⇩S ⊤)›
apply simp by (metis R S calculation cblinfun_apply_in_image)
finally show ‹ψ ∈ space_as_set ((R a o⇩C⇩L S b) *⇩S ⊤)›
by -
qed
qed

lemma compatible_proj_mult:
assumes "compatible R S" and "is_Proj a" and "is_Proj b"
shows "is_Proj (R a o⇩C⇩L S b)"
using [[simproc del: Laws_Quantum.compatibility_warn]]
using assms unfolding is_Proj_algebraic compatible_def
apply auto
apply (metis (no_types, lifting) cblinfun_compose_assoc register_mult)

lemma unitary_sandwich_register: ‹unitary a ⟹ register (sandwich a)›
unfolding register_def
apply (auto simp: sandwich_def)
apply (metis (no_types, lifting) cblinfun_assoc_left(1) cblinfun_compose_id_right unitaryD1)

lemma sandwich_tensor:
fixes a :: ‹'a::finite ell2 ⇒⇩C⇩L 'a ell2› and b :: ‹'b::finite ell2 ⇒⇩C⇩L 'b ell2›
assumes ‹unitary a› ‹unitary b›
shows "sandwich (a ⊗⇩o b) = sandwich a ⊗⇩r sandwich b"
apply (rule tensor_extensionality)
by (auto simp: unitary_sandwich_register assms sandwich_def register_tensor_is_register comp_tensor_op tensor_op_adjoint)

lemma sandwich_grow_left:
fixes a :: ‹'a::finite ell2 ⇒⇩C⇩L 'a ell2›
assumes "unitary a"
shows "sandwich a ⊗⇩r id = sandwich (a ⊗⇩o id_cblinfun)"
by (simp add: unitary_sandwich_register assms sandwich_tensor sandwich_id)

lemma register_sandwich: ‹register F ⟹ F (sandwich a b) = sandwich (F a) (F b)›
by (smt (verit, del_insts) register_def sandwich_def)

lemma assoc_ell2_sandwich: ‹assoc = sandwich assoc_ell2›
apply (rule tensor_extensionality3')
apply (rule equal_ket)
apply (case_tac x)
by (simp add: sandwich_def assoc_apply cblinfun_apply_cblinfun_compose tensor_op_ell2 assoc_ell2_tensor assoc_ell2'_tensor
flip: tensor_ell2_ket)

lemma assoc_ell2'_sandwich: ‹assoc' = sandwich assoc_ell2'›
apply (rule tensor_extensionality3)
apply (rule equal_ket)
apply (case_tac x)
by (simp add: sandwich_def assoc'_apply cblinfun_apply_cblinfun_compose tensor_op_ell2 assoc_ell2_tensor assoc_ell2'_tensor
flip: tensor_ell2_ket)

lemma swap_sandwich: "swap = sandwich Uswap"
apply (rule tensor_extensionality)
apply (auto simp: sandwich_def)[2]
apply (rule tensor_ell2_extensionality)
by (simp add: sandwich_def cblinfun_apply_cblinfun_compose tensor_op_ell2)

lemma id_tensor_sandwich:
fixes a :: "'a::finite ell2 ⇒⇩C⇩L 'b::finite ell2"
assumes "unitary a"
shows "id ⊗⇩r sandwich a = sandwich (id_cblinfun ⊗⇩o a)"
apply (rule tensor_extensionality)
using assms by (auto simp: register_tensor_is_register comp_tensor_op sandwich_def tensor_op_adjoint unitary_sandwich_register)

lemma compatible_selfbutter_join:
assumes [register]: "compatible R S"
shows "R (selfbutter ψ) o⇩C⇩L S (selfbutter φ) = (R; S) (selfbutter (ψ ⊗⇩s φ))"
apply (subst register_pair_apply[symmetric, where F=R and G=S])
using assms by auto

lemma register_mult':
assumes ‹register F›
shows ‹F a *⇩V F b *⇩V c = F (a o⇩C⇩L b) *⇩V c›
by (simp add: assms lift_cblinfun_comp(4) register_mult)

lemma register_scaleC:
assumes ‹register F› shows ‹F (c *⇩C a) = c *⇩C F a›