src/HOL/IMP/Hoare.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 53015 a1119cf551e8
child 67406 23307fd33906
permissions -rw-r--r--
modernized header uniformly as section;
kleing@43158
     1
(* Author: Tobias Nipkow *)
kleing@43158
     2
wenzelm@58889
     3
section "Hoare Logic"
kleing@43158
     4
kleing@43158
     5
theory Hoare imports Big_Step begin
kleing@43158
     6
kleing@43158
     7
subsection "Hoare Logic for Partial Correctness"
kleing@43158
     8
kleing@43158
     9
type_synonym assn = "state \<Rightarrow> bool"
kleing@43158
    10
nipkow@52165
    11
definition
nipkow@52165
    12
hoare_valid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where
nipkow@52167
    13
"\<Turnstile> {P}c{Q} = (\<forall>s t. P s \<and> (c,s) \<Rightarrow> t  \<longrightarrow>  Q t)"
nipkow@52165
    14
nipkow@45212
    15
abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> vname \<Rightarrow> state"
kleing@43158
    16
  ("_[_'/_]" [1000,0,0] 999)
kleing@43158
    17
where "s[a/x] == s(x := aval a s)"
kleing@43158
    18
kleing@43158
    19
inductive
kleing@43158
    20
  hoare :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile> ({(1_)}/ (_)/ {(1_)})" 50)
kleing@43158
    21
where
kleing@43158
    22
Skip: "\<turnstile> {P} SKIP {P}"  |
kleing@43158
    23
kleing@43158
    24
Assign:  "\<turnstile> {\<lambda>s. P(s[a/x])} x::=a {P}"  |
kleing@43158
    25
wenzelm@53015
    26
Seq: "\<lbrakk> \<turnstile> {P} c\<^sub>1 {Q};  \<turnstile> {Q} c\<^sub>2 {R} \<rbrakk>
wenzelm@53015
    27
      \<Longrightarrow> \<turnstile> {P} c\<^sub>1;;c\<^sub>2 {R}"  |
kleing@43158
    28
wenzelm@53015
    29
If: "\<lbrakk> \<turnstile> {\<lambda>s. P s \<and> bval b s} c\<^sub>1 {Q};  \<turnstile> {\<lambda>s. P s \<and> \<not> bval b s} c\<^sub>2 {Q} \<rbrakk>
wenzelm@53015
    30
     \<Longrightarrow> \<turnstile> {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}"  |
kleing@43158
    31
kleing@43158
    32
While: "\<turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow>
kleing@43158
    33
        \<turnstile> {P} WHILE b DO c {\<lambda>s. P s \<and> \<not> bval b s}"  |
kleing@43158
    34
kleing@43158
    35
conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile> {P} c {Q};  \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk>
kleing@43158
    36
        \<Longrightarrow> \<turnstile> {P'} c {Q'}"
kleing@43158
    37
nipkow@47818
    38
lemmas [simp] = hoare.Skip hoare.Assign hoare.Seq If
kleing@43158
    39
nipkow@47818
    40
lemmas [intro!] = hoare.Skip hoare.Assign hoare.Seq hoare.If
kleing@43158
    41
kleing@43158
    42
lemma strengthen_pre:
kleing@43158
    43
  "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile> {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile> {P'} c {Q}"
kleing@43158
    44
by (blast intro: conseq)
kleing@43158
    45
kleing@43158
    46
lemma weaken_post:
kleing@43158
    47
  "\<lbrakk> \<turnstile> {P} c {Q};  \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow>  \<turnstile> {P} c {Q'}"
kleing@43158
    48
by (blast intro: conseq)
kleing@43158
    49
kleing@43158
    50
text{* The assignment and While rule are awkward to use in actual proofs
kleing@43158
    51
because their pre and postcondition are of a very special form and the actual
kleing@43158
    52
goal would have to match this form exactly. Therefore we derive two variants
kleing@43158
    53
with arbitrary pre and postconditions. *}
kleing@43158
    54
kleing@43158
    55
lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile> {P} x ::= a {Q}"
kleing@43158
    56
by (simp add: strengthen_pre[OF _ Assign])
kleing@43158
    57
kleing@43158
    58
lemma While':
kleing@43158
    59
assumes "\<turnstile> {\<lambda>s. P s \<and> bval b s} c {P}" and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s"
kleing@43158
    60
shows "\<turnstile> {P} WHILE b DO c {Q}"
kleing@43158
    61
by(rule weaken_post[OF While[OF assms(1)] assms(2)])
kleing@43158
    62
kleing@43158
    63
end