src/HOL/IMP/Hoare.thy
author oheimb
Tue Jul 04 10:54:46 2000 +0200 (2000-07-04)
changeset 9241 f961c1fdff50
parent 5102 8c782c25a11e
child 12431 07ec657249e5
permissions -rw-r--r--
disambiguated := ; added Examples (factorial)
     1 (*  Title:      HOL/IMP/Hoare.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1995 TUM
     5 
     6 Inductive definition of Hoare logic
     7 *)
     8 
     9 Hoare = Denotation + Inductive +
    10 
    11 types assn = state => bool
    12 
    13 constdefs hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50)
    14           "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t"
    15 
    16 consts hoare :: "(assn * com * assn) set"
    17 syntax "@hoare" :: [bool,com,bool] => bool ("|- ({(1_)}/ (_)/ {(1_)})" 50)
    18 translations "|- {P}c{Q}" == "(P,c,Q) : hoare"
    19 
    20 inductive hoare
    21 intrs
    22   skip "|- {P}SKIP{P}"
    23   ass  "|- {%s. P(s[x::=a s])} x:==a {P}"
    24   semi "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
    25   If "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
    26       |- {P} IF b THEN c ELSE d {Q}"
    27   While "|- {%s. P s & b s} c {P} ==>
    28          |- {P} WHILE b DO c {%s. P s & ~b s}"
    29   conseq "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
    30           |- {P'}c{Q'}"
    31 
    32 constdefs wp :: com => assn => assn
    33           "wp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
    34 
    35 end