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 |
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 flat_def "flat (x::'a) == ! x y. (x::'a) << y --> (x = UU) | (x=y)" |
38 flat_def "flat (x::'a) == ! x y. (x::'a) << y --> (x = UU) | (x=y)" |
39 |
39 |
|
40 (* further useful class for HOLCF *) |
|
41 |
|
42 axclass chfin<pcpo |
|
43 |
|
44 ax_chfin "!Y.is_chain Y-->(? n.max_in_chain n Y)" |
|
45 |
|
46 axclass flat<pcpo |
|
47 |
|
48 ax_flat "! x y.x << y --> (x = UU) | (x=y)" |
|
49 |
40 end |
50 end |
41 |
51 |