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