equal
deleted
inserted
replaced
1 (* Title: HOLCF/fix.thy |
1 (* Title: HOLCF/fix.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Franz Regensburger |
3 Author: Franz Regensburger |
4 Copyright 1993 Technische Universitaet Muenchen |
4 Copyright 1993 Technische Universitaet Muenchen |
5 |
5 |
6 |
6 |
7 definitions for fixed point operator and admissibility |
7 definitions for fixed point operator and admissibility |
8 |
8 |
28 |
28 |
29 adm_def "adm P == !Y. is_chain(Y) --> |
29 adm_def "adm P == !Y. is_chain(Y) --> |
30 (!i.P(Y i)) --> P(lub(range Y))" |
30 (!i.P(Y i)) --> P(lub(range Y))" |
31 |
31 |
32 admw_def "admw P == !F. (!n.P (iterate n F UU)) --> |
32 admw_def "admw P == !F. (!n.P (iterate n F UU)) --> |
33 P (lub(range (%i. iterate i F UU)))" |
33 P (lub(range (%i. iterate i F UU)))" |
34 |
34 |
35 chain_finite_def "chain_finite (x::'a)== |
35 chain_finite_def "chain_finite (x::'a)== |
36 !Y. is_chain (Y::nat=>'a) --> (? n.max_in_chain n Y)" |
36 !Y. is_chain (Y::nat=>'a) --> (? n.max_in_chain n Y)" |
37 |
37 |
38 is_flat_def "is_flat (x::'a) == |
38 is_flat_def "is_flat (x::'a) == |