equal
deleted
inserted
replaced
25 |
25 |
26 rules |
26 rules |
27 |
27 |
28 monofun "monofun(f) == ! x y. x << y --> f(x) << f(y)" |
28 monofun "monofun(f) == ! x y. x << y --> f(x) << f(y)" |
29 |
29 |
30 contlub "contlub(f) == ! Y. is_chain(Y) --> \ |
30 contlub "contlub(f) == ! Y. is_chain(Y) --> |
31 \ f(lub(range(Y))) = lub(range(% i.f(Y(i))))" |
31 f(lub(range(Y))) = lub(range(% i.f(Y(i))))" |
32 |
32 |
33 contX "contX(f) == ! Y. is_chain(Y) --> \ |
33 contX "contX(f) == ! Y. is_chain(Y) --> |
34 \ range(% i.f(Y(i))) <<| f(lub(range(Y)))" |
34 range(% i.f(Y(i))) <<| f(lub(range(Y)))" |
35 |
35 |
36 (* ------------------------------------------------------------------------ *) |
36 (* ------------------------------------------------------------------------ *) |
37 (* the main purpose of cont.thy is to show: *) |
37 (* the main purpose of cont.thy is to show: *) |
38 (* monofun(f) & contlub(f) <==> contX(f) *) |
38 (* monofun(f) & contlub(f) <==> contX(f) *) |
39 (* ------------------------------------------------------------------------ *) |
39 (* ------------------------------------------------------------------------ *) |