src/HOLCF/IMP/HoareEx.thy
author wenzelm
Tue, 28 Jul 1998 17:05:34 +0200
changeset 5210 54aaa779b6b4
parent 3664 2dced1ac2d8e
child 10835 f4745d77e620
permissions -rw-r--r--
removed global_names flag;

(*  Title:      HOLCF/IMP/HoareEx.thy
    ID:         $Id$
    Author:     Tobias Nipkow, TUM
    Copyright   1997 TUM

An example from the HOLCF paper by Mueller, Nipkow, Oheimb, Slotosch.
It demonstrates fixpoint reasoning by showing the correctness of the Hoare
rule for while-loops.
*)

HoareEx = Denotational +

types assn = state => bool

constdefs hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50)
 "|= {A} c {B} == !s t. A s & D c `(Discr s) = Def t --> B t"

end