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;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3664
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
     1
(*  Title:      HOLCF/IMP/HoareEx.thy
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow, TUM
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
     4
    Copyright   1997 TUM
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
     5
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
     6
An example from the HOLCF paper by Mueller, Nipkow, Oheimb, Slotosch.
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
     7
It demonstrates fixpoint reasoning by showing the correctness of the Hoare
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
     8
rule for while-loops.
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
     9
*)
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
    10
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
    11
HoareEx = Denotational +
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
    12
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
    13
types assn = state => bool
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
    14
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
    15
constdefs hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50)
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
    16
 "|= {A} c {B} == !s t. A s & D c `(Discr s) = Def t --> B t"
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
    17
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
    18
end