| author | paulson |
| Tue, 16 Jul 1996 15:49:46 +0200 | |
| changeset 1868 | 836950047d85 |
| parent 1479 | 21eb5e156d91 |
| child 2570 | 24d7e8fb8261 |
| permissions | -rw-r--r-- |
| 1479 | 1 |
(* Title: HOLCF/ex/Fix2.thy |
| 1274 | 2 |
ID: $Id$ |
| 1479 | 3 |
Author: Franz Regensburger |
4 |
Copyright 1995 Technische Universitaet Muenchen |
|
| 1274 | 5 |
|
6 |
Show that fix is the unique least fixed-point operator. |
|
7 |
From axioms gix1_def,gix2_def it follows that fix = gix |
|
8 |
||
9 |
*) |
|
10 |
||
11 |
Fix2 = Fix + |
|
12 |
||
13 |
consts |
|
14 |
||
15 |
gix :: "('a->'a)->'a"
|
|
16 |
||
17 |
rules |
|
18 |
||
19 |
gix1_def "F`(gix`F) = gix`F" |
|
20 |
gix2_def "F`y=y ==> gix`F << y" |
|
21 |
||
22 |
end |
|
23 |
||
24 |
||
25 |
||
26 |
||
27 |
||
28 |
||
29 |
||
30 |
||
31 |
||
32 |
||
33 |
||
34 |
||
35 |
||
36 |
||
37 |
||
38 |