Theory Quantum

section ‹Quantum mechanics basics›

theory Quantum
  imports
    Finite_Tensor_Product
    "HOL-Library.Z2"
    Jordan_Normal_Form.Matrix_Impl 
    Real_Impl.Real_Impl
    "HOL-Library.Code_Target_Numeral"
begin

type_synonym ('a,'b) matrix = ‹('a ell2, 'b ell2) cblinfun›

subsection ‹Basic quantum states›

subsubsection ‹EPR pair›

definition "vector_β00 = vec_of_list [ 1/sqrt 2::complex, 0, 0, 1/sqrt 2 ]"
definition β00 :: ‹(bit×bit) ell2› where [code del]: "β00 = basis_enum_of_vec vector_β00"
lemma vec_of_basis_enum_β00[simp]: "vec_of_basis_enum β00 = vector_β00"
  by (auto simp add: β00_def vector_β00_def)
lemma vec_of_ell2_β00[simp, code]: "vec_of_ell2 β00 = vector_β00"
  by (simp add: vec_of_ell2_def)

lemma norm_β00[simp]: "norm β00 = 1"
  by eval

subsubsection ‹Ket plus›

definition "vector_ketplus = vec_of_list [ 1/sqrt 2::complex, 1/sqrt 2 ]"
definition ketplus :: ‹bit ell2› ("|+⟩") where [code del]: ‹ketplus = basis_enum_of_vec vector_ketplus›
lemma vec_of_basis_enum_ketplus[simp]: "vec_of_basis_enum ketplus = vector_ketplus"
  by (auto simp add: ketplus_def vector_ketplus_def)
lemma vec_of_ell2_ketplus[simp, code]: "vec_of_ell2 ketplus = vector_ketplus"
  by (simp add: vec_of_ell2_def)

subsection ‹Basic quantum gates›

subsubsection ‹Pauli X›

definition "matrix_pauliX = mat_of_rows_list 2 [ [0::complex, 1], [1, 0] ]"
definition pauliX :: ‹(bit, bit) matrix› where [code del]: "pauliX = cblinfun_of_mat matrix_pauliX"
lemma [simp, code]: "mat_of_cblinfun pauliX = matrix_pauliX"
  apply (auto simp add: pauliX_def matrix_pauliX_def)
  apply (subst cblinfun_of_mat_inverse)
  by (auto)

derive (eq) ceq bit

instantiation bit :: ccompare begin
definition "CCOMPARE(bit) = Some (λb1 b2. case (b1, b2) of (0, 0) ⇒ order.Eq | (0, 1) ⇒ order.Lt | (1, 0) ⇒ order.Gt | (1, 1) ⇒ order.Eq)"
instance 
  by intro_classes(unfold_locales; auto simp add: ccompare_bit_def split!: bit.splits)
end

derive (dlist) set_impl bit

lemma pauliX_adjoint[simp]: "pauliX* = pauliX"
  by eval
lemma pauliXX[simp]: "pauliX o⇩C⇩L pauliX = id_cblinfun"
  by eval

subsubsection ‹Pauli Z›

definition "matrix_pauliZ = mat_of_rows_list 2 [ [1::complex, 0], [0, -1] ]"
definition pauliZ :: ‹(bit, bit) matrix› where [code del]: "pauliZ = cblinfun_of_mat matrix_pauliZ"
lemma [simp, code]: "mat_of_cblinfun pauliZ = matrix_pauliZ"
  apply (auto simp add: pauliZ_def matrix_pauliZ_def)
  apply (subst cblinfun_of_mat_inverse)
  by (auto)
lemma pauliZ_adjoint[simp]: "pauliZ* = pauliZ"
  by eval
lemma pauliZZ[simp]: "pauliZ o⇩C⇩L pauliZ = id_cblinfun"
  by eval


subsubsection Hadamard

definition "matrix_hadamard = mat_of_rows_list 2 [ [1/sqrt 2::complex, 1/sqrt 2], [1/sqrt 2, -1/sqrt 2] ]"
definition hadamard :: ‹(bit,bit) matrix› where [code del]: "hadamard = cblinfun_of_mat matrix_hadamard"

lemma [simp, code]: "mat_of_cblinfun hadamard = matrix_hadamard"
  apply (auto simp add: hadamard_def matrix_hadamard_def)
  apply (subst cblinfun_of_mat_inverse)
  by (auto)

lemma hada_adj[simp]: "hadamard* = hadamard"
  by eval


subsubsection CNOT

definition "matrix_CNOT = mat_of_rows_list 4 [ [1::complex,0,0,0], [0,1,0,0], [0,0,0,1], [0,0,1,0] ]"
definition CNOT :: ‹(bit*bit, bit*bit) matrix› where [code del]: "CNOT = cblinfun_of_mat matrix_CNOT"

lemma [simp, code]: "mat_of_cblinfun CNOT = matrix_CNOT"
  apply (auto simp add: CNOT_def matrix_CNOT_def)
  apply (subst cblinfun_of_mat_inverse)
  by (auto)

lemma [simp]: "CNOT* = CNOT"
  by eval

lemma cnot_apply[simp]: ‹CNOT *⇩V ket (i,j) = ket (i,j+i)›
  apply (rule spec[where x=i], rule spec[where x=j])
  by eval

subsubsection ‹Qubit swap›


definition "matrix_Uswap = mat_of_rows_list 4 [ [1::complex, 0, 0, 0], [0,0,1,0], [0,1,0,0], [0,0,0,1] ]"
definition Uswap :: ‹(bit×bit, bit×bit) matrix› where
  [code del]: ‹Uswap = cblinfun_of_mat matrix_Uswap›

lemma mat_of_cblinfun_Uswap[simp, code]: "mat_of_cblinfun Uswap = matrix_Uswap"
  apply (auto simp add: Uswap_def matrix_Uswap_def)
  apply (subst cblinfun_of_mat_inverse)
  by (auto)

lemma dim_col_Uswap[simp]: "dim_col matrix_Uswap = 4"
  unfolding matrix_Uswap_def by simp
lemma dim_row_Uswap[simp]: "dim_row matrix_Uswap = 4"
  unfolding matrix_Uswap_def by simp
lemma Uswap_adjoint[simp]: "Uswap* = Uswap"
  by eval
lemma Uswap_involution[simp]: "Uswap o⇩C⇩L Uswap = id_cblinfun"
  by eval
lemma unitary_Uswap[simp]: "unitary Uswap"
  unfolding unitary_def by simp

lemma Uswap_apply[simp]: ‹Uswap *⇩V s ⊗⇩s t = t ⊗⇩s s›
  apply (rule clinear_equal_ket[where f=‹λs. Uswap *⇩V s ⊗⇩s t›, THEN fun_cong])
    apply (simp add: cblinfun.add_right clinearI tensor_ell2_add1 tensor_ell2_scaleC1)
   apply (simp add: clinear_tensor_ell21)
  apply (rule clinear_equal_ket[where f=‹λt. Uswap *⇩V _ ⊗⇩s t›, THEN fun_cong])
    apply (simp add: cblinfun.add_right clinearI tensor_ell2_add2 tensor_ell2_scaleC2)
   apply (simp add: clinear_tensor_ell22)
  apply (rule basis_enum_eq_vec_of_basis_enumI)
  apply (simp add: mat_of_cblinfun_cblinfun_apply vec_of_basis_enum_ket)
  by (case_tac i; case_tac ia; hypsubst_thin; normalization)

end