src/HOL/IMP/Hoare.thy
author nipkow
Wed Nov 24 12:12:36 1999 +0100 (1999-11-24)
changeset 8029 05446a898852
parent 5102 8c782c25a11e
child 9241 f961c1fdff50
permissions -rw-r--r--
Basis now Main.
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@1447
     6
Inductive definition of Hoare logic
nipkow@936
     7
*)
nipkow@936
     8
berghofe@5102
     9
Hoare = Denotation + Inductive +
nipkow@1447
    10
nipkow@1447
    11
types assn = state => bool
nipkow@1447
    12
nipkow@1696
    13
constdefs hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50)
nipkow@1696
    14
          "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t"
nipkow@939
    15
nipkow@1696
    16
consts hoare :: "(assn * com * assn) set"
nipkow@1696
    17
syntax "@hoare" :: [bool,com,bool] => bool ("|- ({(1_)}/ (_)/ {(1_)})" 50)
nipkow@1486
    18
translations "|- {P}c{Q}" == "(P,c,Q) : hoare"
nipkow@939
    19
paulson@1789
    20
inductive hoare
nipkow@1447
    21
intrs
nipkow@1696
    22
  skip "|- {P}SKIP{P}"
nipkow@4897
    23
  ass  "|- {%s. P(s[x:=a s])} x:=a {P}"
nipkow@1486
    24
  semi "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
nipkow@1696
    25
  If "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
nipkow@1486
    26
      |- {P} IF b THEN c ELSE d {Q}"
nipkow@1696
    27
  While "|- {%s. P s & b s} c {P} ==>
nipkow@1696
    28
         |- {P} WHILE b DO c {%s. P s & ~b s}"
nipkow@1486
    29
  conseq "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
nipkow@1486
    30
          |- {P'}c{Q'}"
nipkow@1481
    31
nipkow@2810
    32
constdefs wp :: com => assn => assn
nipkow@2810
    33
          "wp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
nipkow@939
    34
nipkow@939
    35
end