1461
|
1 |
(* Title: HOLCF/ex/Fix2.ML
|
1274
|
2 |
ID: $Id$
|
1461
|
3 |
Author: Franz Regensburger
|
|
4 |
Copyright 1995 Technische Universitaet Muenchen
|
1274
|
5 |
*)
|
|
6 |
|
|
7 |
open Fix2;
|
|
8 |
|
|
9 |
val lemma1 = prove_goal Fix2.thy "fix = gix"
|
|
10 |
(fn prems =>
|
1461
|
11 |
[
|
|
12 |
(rtac ext_cfun 1),
|
|
13 |
(rtac antisym_less 1),
|
|
14 |
(rtac fix_least 1),
|
|
15 |
(rtac gix1_def 1),
|
|
16 |
(rtac gix2_def 1),
|
|
17 |
(rtac (fix_eq RS sym) 1)
|
|
18 |
]);
|
1274
|
19 |
|
|
20 |
|
|
21 |
val lemma2 = prove_goal Fix2.thy "gix`F=lub(range(%i. iterate i F UU))"
|
|
22 |
(fn prems =>
|
1461
|
23 |
[
|
|
24 |
(rtac (lemma1 RS subst) 1),
|
|
25 |
(rtac fix_def2 1)
|
|
26 |
]);
|
1274
|
27 |
|
|
28 |
|