Theory Hoare

(* Author: Tobias Nipkow *)

section "Hoare Logic"

subsection "Hoare Logic for Partial Correctness"

theory Hoare imports Big_Step begin

type_synonym assn = "state  bool"

hoare_valid :: "assn  com  assn  bool" (" {(1_)}/ (_)/ {(1_)}" 50) where
" {P}c{Q} = (s t. P s  (c,s)  t    Q t)"

abbreviation state_subst :: "state  aexp  vname  state"
  ("_[_'/_]" [1000,0,0] 999)
where "s[a/x] == s(x := aval a s)"

  hoare :: "assn  com  assn  bool" (" ({(1_)}/ (_)/ {(1_)})" 50)
Skip: " {P} SKIP {P}"  |

Assign:  " {λs. P(s[a/x])} x::=a {P}"  |

Seq: "  {P} c1 {Q};   {Q} c2 {R} 
        {P} c1;;c2 {R}"  |

If: "  {λs. P s  bval b s} c1 {Q};   {λs. P s  ¬ bval b s} c2 {Q} 
       {P} IF b THEN c1 ELSE c2 {Q}"  |

While: " {λs. P s  bval b s} c {P} 
         {P} WHILE b DO c {λs. P s  ¬ bval b s}"  |

conseq: " s. P' s  P s;   {P} c {Q};  s. Q s  Q' s 
          {P'} c {Q'}"

lemmas [simp] = hoare.Skip hoare.Assign hoare.Seq If

lemmas [intro!] = hoare.Skip hoare.Assign hoare.Seq hoare.If

lemma strengthen_pre:
  " s. P' s  P s;   {P} c {Q}    {P'} c {Q}"
by (blast intro: conseq)

lemma weaken_post:
  "  {P} c {Q};  s. Q s  Q' s     {P} c {Q'}"
by (blast intro: conseq)

text‹The assignment and While rule are awkward to use in actual proofs
because their pre and postcondition are of a very special form and the actual
goal would have to match this form exactly. Therefore we derive two variants
with arbitrary pre and postconditions.›

lemma Assign': "s. P s  Q(s[a/x])   {P} x ::= a {Q}"
by (simp add: strengthen_pre[OF _ Assign])

lemma While':
assumes " {λs. P s  bval b s} c {P}" and "s. P s  ¬ bval b s  Q s"
shows " {P} WHILE b DO c {Q}"
by(rule weaken_post[OF While[OF assms(1)] assms(2)])