Theory Hoare

(*  Title:       Inductive definition of Hoare logic
    Author:      Tobias Nipkow, 2001/2006
    Maintainer:  Tobias Nipkow
*)

theory Hoare imports Lang begin

subsection‹Hoare logic for partial correctness›

text‹We continue our semantic approach by modelling assertions just
like boolean expressions, i.e.\ as functions:›

type_synonym assn = "state ⇒ bool"

text‹Hoare triples are triples of the form ‹{P} c {Q}›, where
the assertions ‹P› and ‹Q› are the so-called pre and
postconditions. Such a triple is \emph{valid} (denoted by ‹⊨›)
iff every (terminating) execution starting in a state satisfying ‹P›
ends up in a state satisfying ‹Q›:›

definition
 hoare_valid :: "assn ⇒ com ⇒ assn ⇒ bool" (‹⊨ {(1_)}/ (_)/ {(1_)}› 50) where
 "⊨ {P}c{Q} ⟷ (∀s t. s -c→ t ⟶ P s ⟶ Q t)"

text‹\noindent
This notion of validity is called \emph{partial correctness} because
it does not require termination of @{term c}.

Provability in Hoare logic is indicated by ‹⊢› and defined
inductively:›

inductive
  hoare :: "assn ⇒ com ⇒ assn ⇒ bool" (‹⊢ ({(1_)}/ (_)/ {(1_)})› 50)
where
  (*<*)Do:(*>*)"⊢ {λs. ∀t ∈ f s. P t} Do f {P}"

| (*<*)Semi:(*>*)"⟦ ⊢ {P}c1{Q};  ⊢ {Q}c2{R} ⟧  ⟹  ⊢ {P} c1;c2 {R}"

| (*<*)If:(*>*)"⟦ ⊢ {λs. P s ∧ b s} c1 {Q};  ⊢ {λs. P s ∧ ¬b s} c2 {Q} ⟧
  ⟹ ⊢ {P} IF b THEN c1 ELSE c2 {Q}"

| (*<*)While:(*>*)"⊢ {λs. P s ∧ b s} c {P}  ⟹  ⊢ {P} WHILE b DO c {λs. P s ∧ ¬b s}"

| (*<*)Conseq:(*>*)"⟦ ∀s. P' s ⟶ P s;  ⊢ {P}c{Q};  ∀s. Q s ⟶ Q' s  ⟧  ⟹  ⊢ {P'}c{Q'}"

| (*<*)Local:(*>*) "⟦ ⋀s. P s ⟹ P' s (f s); ∀s. ⊢ {P' s} c {Q ∘ (g s)} ⟧ ⟹
        ⊢ {P} LOCAL f;c;g {Q}"

text‹Soundness is proved by induction on the derivation of @{prop"⊢
{P} c {Q}"}:›

theorem hoare_sound: "⊢ {P}c{Q}  ⟹  ⊨ {P}c{Q}"
apply(unfold hoare_valid_def)
apply(erule hoare.induct)
      apply blast
     apply blast
    apply clarsimp
   apply clarify
   apply(drule while_rule)
   prefer 3
   apply (assumption, assumption, blast)
  apply blast
apply clarify
apply(erule allE)
apply clarify
apply(erule allE)
apply(erule allE)
apply(erule impE)
apply assumption
apply simp
apply(erule mp)
apply(simp)
done

text‹
Completeness is not quite as straightforward, but still easy. The
proof is best explained in terms of the \emph{weakest precondition}:›

definition
 wp :: "com ⇒ assn ⇒ assn" where
 "wp c Q = (λs. ∀t. s -c→ t ⟶ Q t)"

text‹\noindent Dijkstra calls this the weakest \emph{liberal}
precondition to emphasize that it corresponds to partial
correctness. We use ``weakest precondition'' all the time and let the
context determine if we talk about partial or total correctness ---
the latter is introduced further below.

The following lemmas about @{term wp} are easily derived:
›

lemma [simp]: "wp (Do f) Q = (λs. ∀t ∈ f s. Q(t))"
apply(unfold wp_def)
apply(rule ext)
apply blast
done

lemma [simp]: "wp (c⇩1;c⇩2) R = wp c⇩1 (wp c⇩2 R)"
apply(unfold wp_def)
apply(rule ext)
apply blast
done

lemma [simp]:
 "wp (IF b THEN c⇩1 ELSE c⇩2) Q = (λs. wp (if b s then c⇩1 else c⇩2) Q s)"
apply(unfold wp_def)
apply(rule ext)
apply auto
done

lemma wp_while:
 "wp (WHILE b DO c) Q =
           (λs. if b s then wp (c;WHILE b DO c) Q s else Q s)"
apply(rule ext)
apply(unfold wp_def)
apply auto
apply(blast intro:exec.intros)
apply(simp add:unfold_while)
apply(blast intro:exec.intros)
apply(simp add:unfold_while)
done

lemma [simp]:
 "wp (LOCAL f;c;g) Q = (λs. wp c (Q o (g s)) (f s))"
apply(unfold wp_def)
apply(rule ext)
apply auto
done

lemma strengthen_pre: "⟦ ∀s. P' s ⟶ P s; ⊢ {P}c{Q}  ⟧ ⟹ ⊢ {P'}c{Q}"
by(erule hoare.Conseq, assumption, blast)

lemma weaken_post: "⟦ ⊢ {P}c{Q}; ∀s. Q s ⟶ Q' s  ⟧ ⟹ ⊢ {P}c{Q'}"
apply(rule hoare.Conseq)
apply(fast, assumption, assumption)
done

text‹By induction on @{term c} one can easily prove›

lemma wp_is_pre[rule_format]: "⊢ {wp c Q} c {Q}"
apply (induct c arbitrary: Q)
apply simp_all

apply(blast intro:hoare.Do hoare.Conseq)

apply(blast intro:hoare.Semi hoare.Conseq)

apply(blast intro:hoare.If hoare.Conseq)

apply(rule weaken_post)
apply(rule hoare.While)
apply(rule strengthen_pre)
prefer 2
apply blast
apply(clarify)
apply(drule fun_eq_iff[THEN iffD1, OF wp_while, THEN spec, THEN iffD1])
apply simp
apply(clarify)
apply(drule fun_eq_iff[THEN iffD1, OF wp_while, THEN spec, THEN iffD1])
apply(simp split:if_split_asm)

apply(fast intro!: hoare.Local)
done

text‹\noindent
from which completeness follows more or less directly via the
rule of consequence:›

theorem hoare_relative_complete: "⊨ {P}c{Q}  ⟹  ⊢ {P}c{Q}"
apply (rule strengthen_pre[OF _ wp_is_pre])
apply(unfold hoare_valid_def wp_def)
apply blast
done

end