equal
deleted
inserted
replaced
13 consts |
13 consts |
14 |
14 |
15 iterate :: "nat=>('a->'a)=>'a=>'a" |
15 iterate :: "nat=>('a->'a)=>'a=>'a" |
16 Ifix :: "('a->'a)=>'a" |
16 Ifix :: "('a->'a)=>'a" |
17 fix :: "('a->'a)->'a" |
17 fix :: "('a->'a)->'a" |
18 adm :: "('a=>bool)=>bool" |
18 adm :: "('a::cpo=>bool)=>bool" |
19 admw :: "('a=>bool)=>bool" |
19 admw :: "('a=>bool)=>bool" |
20 chain_finite :: "'a=>bool" |
20 chain_finite :: "'a::cpo=>bool" |
21 flat :: "'a=>bool" (* should be called flat, for consistency *) |
21 flat :: "'a=>bool" |
22 |
22 |
23 defs |
23 defs |
24 |
24 |
25 iterate_def "iterate n F c == nat_rec c (%n x.F`x) n" |
25 iterate_def "iterate n F c == nat_rec c (%n x.F`x) n" |
26 Ifix_def "Ifix F == lub(range(%i.iterate i F UU))" |
26 Ifix_def "Ifix F == lub(range(%i.iterate i F UU))" |
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::cpo)== |
36 !Y. is_chain (Y::nat=>'a) --> (? n.max_in_chain n Y)" |
36 !Y. is_chain (Y::nat=>'a::cpo) --> (? 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 *) |
40 (* further useful class for HOLCF *) |
41 |
41 |