| author | wenzelm |
| Mon, 02 Nov 1998 21:22:03 +0100 | |
| changeset 5791 | 96ab3e097732 |
| parent 244 | 929fc2c63bd0 |
| permissions | -rw-r--r-- |
| 244 | 1 |
(* Title: HOLCF/ex/loop.thy |
2 |
ID: $Id$ |
|
3 |
Author: Franz Regensburger |
|
4 |
Copyright 1993 Technische Universitaet Muenchen |
|
5 |
||
6 |
Theory for a loop primitive like while |
|
7 |
*) |
|
8 |
||
9 |
Loop = Tr2 + |
|
10 |
||
11 |
consts |
|
12 |
||
13 |
step :: "('a -> tr)->('a -> 'a)->'a->'a"
|
|
14 |
while :: "('a -> tr)->('a -> 'a)->'a->'a"
|
|
15 |
||
16 |
rules |
|
17 |
||
18 |
step_def "step == (LAM b g x. If b[x] then g[x] else x fi)" |
|
19 |
while_def "while == (LAM b g. fix[LAM f x.\ |
|
20 |
\ If b[x] then f[g[x]] else x fi])" |
|
21 |
||
22 |
||
23 |
end |
|
24 |