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_syntax
unbundle cblinfun_syntax

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)])
    by (simp add: cblinfun_compose_image cblinfun_image_mono)
  moreover have "((R a o⇩C⇩L S b) *⇩S ⊤) ≤ (R a *⇩S ⊤)"
    by (simp add: cblinfun_compose_image cblinfun_image_mono)
  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 ψ›
      by (simp add: cblinfun_apply_cblinfun_compose)
    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)
  by (simp add: assms(2) assms(3) is_proj_selfadj register_projector)

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)
  by (simp add: lift_cblinfun_comp(2))

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 (simp_all add: unitary_sandwich_register)[2]
  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 (simp_all add: unitary_sandwich_register)[2]
  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›
  by (simp add: assms complex_vector.linear_scale)

lemma register_bounded_clinear: ‹register F ⟹ bounded_clinear F›
  using bounded_clinear_finite_dim register_def by blast

lemma register_adjoint: "F (a*) = (F a)*" if ‹register F›
  using register_def that by blast

end