22 |
22 |
23 "@LUB" :: "(('b::term) => 'a) => 'a" (binder "LUB " 10) |
23 "@LUB" :: "(('b::term) => 'a) => 'a" (binder "LUB " 10) |
24 |
24 |
25 translations |
25 translations |
26 |
26 |
27 "LUB x. t" == "lub(range(%x.t))" |
27 "LUB x. t" == "lub(range(%x. t))" |
28 |
28 |
29 syntax (symbols) |
29 syntax (symbols) |
30 |
30 |
31 "LUB " :: "[idts, 'a] => 'a" ("(3\\<Squnion>_./ _)"[0,10] 10) |
31 "LUB " :: "[idts, 'a] => 'a" ("(3\\<Squnion>_./ _)"[0,10] 10) |
32 |
32 |
33 defs |
33 defs |
34 |
34 |
35 (* class definitions *) |
35 (* class definitions *) |
36 is_ub "S <| x == ! y.y:S --> y<<x" |
36 is_ub "S <| x == ! y. y:S --> y<<x" |
37 is_lub "S <<| x == S <| x & (! u. S <| u --> x << u)" |
37 is_lub "S <<| x == S <| x & (! u. S <| u --> x << u)" |
38 |
38 |
39 (* Arbitrary chains are total orders *) |
39 (* Arbitrary chains are total orders *) |
40 is_tord "is_tord S == ! x y. x:S & y:S --> (x<<y | y<<x)" |
40 is_tord "is_tord S == ! x y. x:S & y:S --> (x<<y | y<<x)" |
41 |
41 |
42 (* Here we use countable chains and I prefer to code them as functions! *) |
42 (* Here we use countable chains and I prefer to code them as functions! *) |
43 is_chain "is_chain F == (! i.F(i) << F(Suc(i)))" |
43 is_chain "is_chain F == (! i. F(i) << F(Suc(i)))" |
44 |
44 |
45 (* finite chains, needed for monotony of continouous functions *) |
45 (* finite chains, needed for monotony of continouous functions *) |
46 max_in_chain_def "max_in_chain i C == ! j. i <= j --> C(i) = C(j)" |
46 max_in_chain_def "max_in_chain i C == ! j. i <= j --> C(i) = C(j)" |
47 finite_chain_def "finite_chain C == is_chain(C) & (? i. max_in_chain i C)" |
47 finite_chain_def "finite_chain C == is_chain(C) & (? i. max_in_chain i C)" |
48 |
48 |