| author | huffman |
| Fri, 08 Jul 2005 03:09:32 +0200 | |
| changeset 16757 | b8bfd086f7d4 |
| parent 14981 | e73f8140af78 |
| child 17291 | 94f6113fe9ed |
| permissions | -rw-r--r-- |
| 1479 | 1 |
(* Title: HOLCF/ex/Fix2.thy |
| 1274 | 2 |
ID: $Id$ |
| 1479 | 3 |
Author: Franz Regensburger |
| 1274 | 4 |
|
| 12036 | 5 |
Show that fix is the unique least fixed-point operator. |
6 |
From axioms gix1_def,gix2_def it follows that fix = gix |
|
| 1274 | 7 |
*) |
8 |
||
9 |
Fix2 = Fix + |
|
10 |
||
11 |
consts |
|
12 |
||
13 |
gix :: "('a->'a)->'a"
|
|
14 |
||
15 |
rules |
|
16 |
||
| 10835 | 17 |
gix1_def "F$(gix$F) = gix$F" |
18 |
gix2_def "F$y=y ==> gix$F << y" |
|
| 1274 | 19 |
|
20 |
end |