author | huffman |
Wed, 24 Mar 2010 07:50:21 -0700 | |
changeset 35948 | 5e7909f0346b |
parent 35174 | e15040ae75d7 |
child 40002 | c5b5f7a3a3b1 |
permissions | -rw-r--r-- |
1479 | 1 |
(* Title: HOLCF/ex/Fix2.thy |
2 |
Author: Franz Regensburger |
|
1274 | 3 |
|
17291 | 4 |
Show that fix is the unique least fixed-point operator. |
12036 | 5 |
From axioms gix1_def,gix2_def it follows that fix = gix |
1274 | 6 |
*) |
7 |
||
17291 | 8 |
theory Fix2 |
9 |
imports HOLCF |
|
10 |
begin |
|
1274 | 11 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19742
diff
changeset
|
12 |
axiomatization |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19742
diff
changeset
|
13 |
gix :: "('a->'a)->'a" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19742
diff
changeset
|
14 |
gix1_def: "F$(gix$F) = gix$F" and |
17291 | 15 |
gix2_def: "F$y=y ==> gix$F << y" |
1274 | 16 |
|
19742 | 17 |
|
18 |
lemma lemma1: "fix = gix" |
|
19 |
apply (rule ext_cfun) |
|
20 |
apply (rule antisym_less) |
|
21 |
apply (rule fix_least) |
|
22 |
apply (rule gix1_def) |
|
23 |
apply (rule gix2_def) |
|
24 |
apply (rule fix_eq [symmetric]) |
|
25 |
done |
|
26 |
||
27 |
lemma lemma2: "gix$F=lub(range(%i. iterate i$F$UU))" |
|
28 |
apply (rule lemma1 [THEN subst]) |
|
29 |
apply (rule fix_def2) |
|
30 |
done |
|
1274 | 31 |
|
32 |
end |