Theory QHoare

section Very simple Quantum Hoare logic

theory QHoare
  imports Quantum_Extra
begin

no_notation Order.top ("ı")

locale qhoare =
  fixes memory_type :: "'mem::finite itself"
begin

definition "apply U R = R U" for R :: 'a update  'mem update
definition "ifthen R x = R (butterket x x)" for R :: 'a update  'mem update
definition "program S = fold (oCL) S id_cblinfun" for S :: 'mem update list


definition hoare :: 'mem ell2 ccsubspace  ('mem ell2 CL 'mem ell2) list  'mem ell2 ccsubspace  bool where
  "hoare C p D  (ψspace_as_set C. program p *V ψ  space_as_set D)" for C p D

definition EQ :: "('a update  'mem update)  'a ell2  'mem ell2 ccsubspace" (infix "=q" 75) where
  "EQ R ψ = R (selfbutter ψ) *S "

lemma program_skip[simp]: "program [] = id_cblinfun"
  by (simp add: qhoare.program_def)

lemma program_seq: "program (p1@p2) = program p2 oCL program p1"
  apply (induction p2 rule:rev_induct)
   apply (simp_all add: program_def)
  by (meson cblinfun_assoc_left(1))

lemma hoare_seq[trans]: "hoare C p1 D  hoare D p2 E  hoare C (p1@p2) E"
  by (auto simp: program_seq hoare_def)

lemma hoare_weaken_left[trans]: A  B  hoare B p C  hoare A p C
  unfolding hoare_def
  by (meson in_mono less_eq_ccsubspace.rep_eq) 

lemma hoare_weaken_right[trans]: hoare A p B  B  C  hoare A p C
  unfolding hoare_def 
  by (meson in_mono less_eq_ccsubspace.rep_eq) 

lemma hoare_skip: "C  D  hoare C [] D"
  by (auto simp: program_def hoare_def in_mono less_eq_ccsubspace.rep_eq)

lemma hoare_apply: 
  assumes "R U *S pre  post"
  shows "hoare pre [apply U R] post"
  using assms 
  apply (auto simp: hoare_def program_def apply_def)
  by (metis (no_types, lifting) cblinfun_image.rep_eq closure_subset imageI less_eq_ccsubspace.rep_eq subsetD)

lemma hoare_ifthen: 
  fixes R :: 'a update  'mem update
  assumes "R (selfbutter (ket x)) *S pre  post"
  shows "hoare pre [ifthen R x] post"
  using assms 
  apply (auto simp: hoare_def program_def ifthen_def butterfly_def)
  by (metis (no_types, lifting) cblinfun_image.rep_eq closure_subset imageI less_eq_ccsubspace.rep_eq subsetD)

end

end