|
3664
|
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
|