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 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)
    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)"
  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 CL 'a ell2 and b :: 'b::finite ell2 CL '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 CL '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 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_def tensor_op_adjoint unitary_sandwich_register)

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

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