Theory StdLogic

section "A standard total correctness Hoare logic"

theory StdLogic imports WhileLang begin

(* -- inference rules for a standard total-correctness Hoare logic -- *)

inductive hoare :: "(state ⇒ bool) ⇒ prog ⇒ (state ⇒ bool) ⇒ bool" where
  h_skip[simp,intro!]: "hoare P Skip P"
| h_assign[simp,intro!]: "hoare (λs. Q (subst n x s)) (Assign n x) Q"
| h_print[simp,intro!]: "hoare (λs. Q (print x s)) (Print x) Q"
| h_seq[intro]: "hoare P p M ⟹ hoare M q Q ⟹ hoare P (Seq p q) Q"
| h_if[intro!]    : "hoare (λs. P s ∧  guard x s) p Q
        ⟹ hoare (λs. P s ∧ ~guard x s) q Q ⟹ hoare P (If x p q) Q"
| h_while : "(⋀s0. hoare (λs. P s ∧ guard x s ∧ s = s0) p (λs. P s ∧ R s s0))
        ⟹ wfP R ⟹ hoare P (While x p) (λs. P s ∧ ~guard x s)"
| h_weaken: "(⋀s. P s ⟹ P' s) ⟹ hoare P' p Q' ⟹ (⋀s. Q' s ⟹ Q s) ⟹ hoare P p Q"

(* -- semantics -- *)

definition hoare_sem :: "(state ⇒ bool) ⇒ prog ⇒ (state ⇒ bool) ⇒ bool" where
  "hoare_sem P p Q ≡
    (∀s. P s ⟶ (∃t. terminates s p t ∧ Q t))"

end