# 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 (o⇩C⇩L) S id_cblinfun" for S :: ‹'mem update list›

definition hoare :: ‹'mem ell2 ccsubspace ⇒ ('mem ell2 ⇒⇩C⇩L '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"

lemma program_seq: "program (p1@p2) = program p2 o⇩C⇩L program p1"
apply (induction p2 rule:rev_induct)
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
```