section ‹Very simple Quantum Hoare logic›

theory QHoare
  imports Quantum_Extra
begin

unbundle register_syntax
unbundle cblinfun_syntax
unbundle lattice_syntax
no_notation Order.top ("⊤ı")

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

definition "apply U R = R U" for R :: ‹'a update → 'mem update›
definition "ifthen R x = R (butterfly (ket x) (ket x))" for R :: ‹'a update → 'mem update›
definition "program S = fold (o_CL) 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 o_CL 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"
proof -
  from assms have ‹ψ ∈ space_as_set pre ==> R U *_V ψ ∈ space_as_set post› for ψ
    by (metis (no_types, lifting) cblinfun_image.rep_eq closure_subset imageI less_eq_ccsubspace.rep_eq subsetD)
  then show ?thesis
    by (auto simp: hoare_def program_def apply_def)
qed

lemma hoare_ifthen: 
  fixes R :: ‹'a update → 'mem update›
  assumes "R (selfbutter (ket x)) *_S pre ≤ post"
  shows "hoare pre [ifthen R x] post"
proof -
  from assms have ‹ψ ∈ space_as_set pre ==> R (vector_to_cblinfun (ket x) o_CL bra x) *_V ψ ∈ space_as_set post› for ψ
    by (metis butterfly_def_one_dim cblinfun_apply_in_image' less_eq_ccsubspace.rep_eq subsetD)
  then show ?thesis
    by (auto simp: hoare_def program_def ifthen_def butterfly_def)
qed
end

unbundle no register_syntax
unbundle no cblinfun_syntax
unbundle no lattice_syntax

end