src/HOLCF/IMP/HoareEx.thy
author nipkow
Tue Jan 09 15:36:30 2001 +0100 (2001-01-09)
changeset 10835 f4745d77e620
parent 3664 2dced1ac2d8e
child 12431 07ec657249e5
permissions -rw-r--r--
` -> $
     1 (*  Title:      HOLCF/IMP/HoareEx.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, TUM
     4     Copyright   1997 TUM
     5 
     6 An example from the HOLCF paper by Mueller, Nipkow, Oheimb, Slotosch.
     7 It demonstrates fixpoint reasoning by showing the correctness of the Hoare
     8 rule for while-loops.
     9 *)
    10 
    11 HoareEx = Denotational +
    12 
    13 types assn = state => bool
    14 
    15 constdefs hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50)
    16  "|= {A} c {B} == !s t. A s & D c $(Discr s) = Def t --> B t"
    17 
    18 end