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 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 oCL S b) *S ⊤)"
proof (rule antisym)
  have "((R a oCL 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 oCL S b) *S ⊤) ≤ (R a *S ⊤)"
    by (simp add: cblinfun_compose_image cblinfun_image_mono)
  ultimately show ‹((R a oCL 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 oCL S b) *S ⊤›
  proof (unfold less_eq_ccsubspace.rep_eq, rule subsetI)
    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 oCL S b) *V ψ›
      by (simp add: cblinfun_apply_cblinfun_compose)
    also have ‹… ∈ space_as_set ((R a oCL S b) *S ⊤)›
      apply simp by (metis R S calculation cblinfun_apply_in_image)
    finally show ‹ψ ∈ space_as_set ((R a oCL 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 oCL S b)"
proof -
  have aux: ‹∀a b. R a oCL S b = S b oCL R a ⟹ S b oCL R a oCL (S b oCL R a) = S b oCL R a›
    using assms
    by (metis (no_types, lifting) cblinfun_compose_assoc register_mult is_Proj_algebraic compatible_def)
  show ?thesis
    using [[simproc del: Laws_Quantum.compatibility_warn]]
    using assms unfolding is_Proj_algebraic compatible_def
    by (auto simp add: assms is_proj_selfadj register_projector aux)
qed

lemma sandwich_tensor: 
  fixes a :: ‹'a ell2 ⇒CL 'a ell2› and b :: ‹'b ell2 ⇒CL 'b ell2› 
  assumes [simp]: ‹unitary a› ‹unitary b›
  shows "(*V) (sandwich (a ⊗o b)) = sandwich a ⊗r sandwich b"
  apply (rule tensor_extensionality)
  by (auto simp: unitary_sandwich_register sandwich_apply register_tensor_is_register
      comp_tensor_op tensor_op_adjoint unitary_tensor_op intro!: register_preregister unitary_sandwich_register)

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

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

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_apply 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_apply 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_apply unitary_sandwich_register)[2]
  apply (rule tensor_ell2_extensionality)
  by (simp add: sandwich_apply cblinfun_apply_cblinfun_compose tensor_op_ell2)

lemma id_tensor_sandwich: 
  fixes a :: "'a::finite ell2 ⇒CL '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_apply tensor_op_adjoint unitary_sandwich_register
      intro!: register_preregister unitary_sandwich_register unitary_tensor_op)

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

lemma register_mult':
  assumes ‹register F›
  shows ‹F a *V F b *V c = F (a oCL 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›
  using assms [[simproc del: Laws_Quantum.compatibility_warn]] 
  unfolding register_def
  by (simp add: bounded_clinear.clinear clinear.scaleC)

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

lemma register_finite_dim: ‹register F ⟷ clinear F ∧ F id_cblinfun = id_cblinfun ∧ (∀a b. F (a oCL b) = F a oCL F b) ∧ (∀a. F (a*) = F a*)›
  for F :: ‹'a::finite update ⇒ 'b::finite update›
    (* I conjecture that this holds even when only 'a is finite. *)
proof
  assume ‹register F›
  then show ‹clinear F ∧ F id_cblinfun = id_cblinfun ∧ (∀a b. F (a oCL b) = F a oCL F b) ∧ (∀a. F (a*) = F a*)›
    unfolding register_def
    by (auto simp add: bounded_clinear_def)
next
  assume asm: ‹clinear F ∧ F id_cblinfun = id_cblinfun ∧ (∀a b. F (a oCL b) = F a oCL F b) ∧ (∀a. F (a*) = F a*)›
  then have ‹clinear F›
    by simp
  then have ‹bounded_clinear F›
    by simp
  then have ‹continuous_map euclidean euclidean F›
    by (auto intro!: continuous_at_imp_continuous_on clinear_continuous_at)
  then have wstar: ‹continuous_map weak_star_topology weak_star_topology F›
    by simp
  from asm ‹bounded_clinear F› wstar
  show ‹register F›
    unfolding register_def by simp
qed

unbundle no lattice_syntax
unbundle no register_syntax
unbundle no cblinfun_syntax

end