|
1479
|
1 |
(* Title: HOLCF/ex/Fix2.thy
|
|
1274
|
2 |
ID: $Id$
|
|
1479
|
3 |
Author: Franz Regensburger
|
|
1274
|
4 |
|
|
17291
|
5 |
Show that fix is the unique least fixed-point operator.
|
|
12036
|
6 |
From axioms gix1_def,gix2_def it follows that fix = gix
|
|
1274
|
7 |
*)
|
|
|
8 |
|
|
17291
|
9 |
theory Fix2
|
|
|
10 |
imports HOLCF
|
|
|
11 |
begin
|
|
1274
|
12 |
|
|
|
13 |
consts
|
|
17291
|
14 |
gix :: "('a->'a)->'a"
|
|
1274
|
15 |
|
|
17291
|
16 |
axioms
|
|
|
17 |
gix1_def: "F$(gix$F) = gix$F"
|
|
|
18 |
gix2_def: "F$y=y ==> gix$F << y"
|
|
1274
|
19 |
|
|
19742
|
20 |
|
|
|
21 |
lemma lemma1: "fix = gix"
|
|
|
22 |
apply (rule ext_cfun)
|
|
|
23 |
apply (rule antisym_less)
|
|
|
24 |
apply (rule fix_least)
|
|
|
25 |
apply (rule gix1_def)
|
|
|
26 |
apply (rule gix2_def)
|
|
|
27 |
apply (rule fix_eq [symmetric])
|
|
|
28 |
done
|
|
|
29 |
|
|
|
30 |
lemma lemma2: "gix$F=lub(range(%i. iterate i$F$UU))"
|
|
|
31 |
apply (rule lemma1 [THEN subst])
|
|
|
32 |
apply (rule fix_def2)
|
|
|
33 |
done
|
|
1274
|
34 |
|
|
|
35 |
end
|