src/HOL/IMP/Hoare.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 35754 8e7dba5f00f5
child 41589 bbd861837ebc
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
     1 (*  Title:      HOL/IMP/Hoare.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1995 TUM
     5 *)
     6 
     7 header "Inductive Definition of Hoare Logic"
     8 
     9 theory Hoare imports Natural begin
    10 
    11 types assn = "state => bool"
    12 
    13 inductive
    14   hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
    15 where
    16   skip: "|- {P}\<SKIP>{P}"
    17 | ass:  "|- {%s. P(s[x\<mapsto>a s])} x:==a {P}"
    18 | semi: "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
    19 | If: "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
    20       |- {P} \<IF> b \<THEN> c \<ELSE> d {Q}"
    21 | While: "|- {%s. P s & b s} c {P} ==>
    22          |- {P} \<WHILE> b \<DO> c {%s. P s & ~b s}"
    23 | conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
    24           |- {P'}c{Q'}"
    25 
    26 lemma strengthen_pre: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}"
    27 by (blast intro: conseq)
    28 
    29 lemma weaken_post: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}"
    30 by (blast intro: conseq)
    31 
    32 lemma While':
    33 assumes "|- {%s. P s & b s} c {P}" and "ALL s. P s & \<not> b s \<longrightarrow> Q s"
    34 shows "|- {P} \<WHILE> b \<DO> c {Q}"
    35 by(rule weaken_post[OF While[OF assms(1)] assms(2)])
    36 
    37 
    38 lemmas [simp] = skip ass semi If
    39 
    40 lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If
    41 
    42 end