author | wenzelm |
Fri, 12 Oct 2001 12:11:39 +0200 | |
changeset 11734 | 7a21bf539412 |
parent 10835 | f4745d77e620 |
child 12431 | 07ec657249e5 |
permissions | -rw-r--r-- |
(* 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