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