src/HOL/IMP/Hoare.thy
author nipkow
Fri Mar 12 18:42:56 2010 +0100 (2010-03-12)
changeset 35754 8e7dba5f00f5
parent 35735 f139a9bb6501
child 41589 bbd861837ebc
permissions -rw-r--r--
Reorganized Hoare logic theories; added Hoare_Den
clasohm@1476
     1
(*  Title:      HOL/IMP/Hoare.thy
nipkow@938
     2
    ID:         $Id$
clasohm@1476
     3
    Author:     Tobias Nipkow
nipkow@936
     4
    Copyright   1995 TUM
nipkow@936
     5
*)
nipkow@936
     6
kleing@12431
     7
header "Inductive Definition of Hoare Logic"
kleing@12431
     8
nipkow@35754
     9
theory Hoare imports Natural begin
nipkow@1447
    10
kleing@12431
    11
types assn = "state => bool"
nipkow@1447
    12
berghofe@23746
    13
inductive
berghofe@23746
    14
  hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
berghofe@23746
    15
where
kleing@12431
    16
  skip: "|- {P}\<SKIP>{P}"
berghofe@23746
    17
| ass:  "|- {%s. P(s[x\<mapsto>a s])} x:==a {P}"
berghofe@23746
    18
| semi: "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
berghofe@23746
    19
| If: "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
kleing@12431
    20
      |- {P} \<IF> b \<THEN> c \<ELSE> d {Q}"
berghofe@23746
    21
| While: "|- {%s. P s & b s} c {P} ==>
kleing@12431
    22
         |- {P} \<WHILE> b \<DO> c {%s. P s & ~b s}"
berghofe@23746
    23
| conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
nipkow@1486
    24
          |- {P'}c{Q'}"
nipkow@1481
    25
nipkow@35735
    26
lemma strengthen_pre: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}"
nipkow@35735
    27
by (blast intro: conseq)
kleing@12431
    28
nipkow@35735
    29
lemma weaken_post: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}"
nipkow@35735
    30
by (blast intro: conseq)
kleing@12431
    31
nipkow@35754
    32
lemma While':
nipkow@35754
    33
assumes "|- {%s. P s & b s} c {P}" and "ALL s. P s & \<not> b s \<longrightarrow> Q s"
nipkow@35754
    34
shows "|- {P} \<WHILE> b \<DO> c {Q}"
nipkow@35754
    35
by(rule weaken_post[OF While[OF assms(1)] assms(2)])
nipkow@35735
    36
kleing@12431
    37
nipkow@35754
    38
lemmas [simp] = skip ass semi If
kleing@12431
    39
wenzelm@18372
    40
lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If
kleing@12431
    41
nipkow@939
    42
end