equal
deleted
inserted
replaced
|
1 (* Title: HOLCF/fix.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 |
|
7 definitions for fixed point operator and admissibility |
|
8 |
|
9 *) |
|
10 |
|
11 Fix = Cfun3 + |
|
12 |
|
13 consts |
|
14 |
|
15 iterate :: "nat=>('a->'a)=>'a=>'a" |
|
16 Ifix :: "('a->'a)=>'a" |
|
17 fix :: "('a->'a)->'a" |
|
18 adm :: "('a=>bool)=>bool" |
|
19 admw :: "('a=>bool)=>bool" |
|
20 chain_finite :: "'a=>bool" |
|
21 flat :: "'a=>bool" |
|
22 |
|
23 rules |
|
24 |
|
25 iterate_def "iterate(n,F,c) == nat_rec(n,c,%n x.F[x])" |
|
26 Ifix_def "Ifix(F) == lub(range(%i.iterate(i,F,UU)))" |
|
27 fix_def "fix == (LAM f. Ifix(f))" |
|
28 |
|
29 adm_def "adm(P) == !Y. is_chain(Y) --> \ |
|
30 \ (!i.P(Y(i))) --> P(lub(range(Y)))" |
|
31 |
|
32 admw_def "admw(P)== (!F.((!n.P(iterate(n,F,UU)))-->\ |
|
33 \ P(lub(range(%i.iterate(i,F,UU))))))" |
|
34 |
|
35 chain_finite_def "chain_finite(x::'a)==\ |
|
36 \ !Y. is_chain(Y::nat=>'a) --> (? n.max_in_chain(n,Y))" |
|
37 |
|
38 flat_def "flat(x::'a) ==\ |
|
39 \ ! x y. x::'a << y --> (x = UU) | (x=y)" |
|
40 |
|
41 end |
|
42 |