35 structure. |
35 structure. |
36 *}; |
36 *}; |
37 |
37 |
38 theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a"; |
38 theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a"; |
39 proof; |
39 proof; |
40 let ??H = "{u. f u <= u}"; |
40 let ?H = "{u. f u <= u}"; |
41 let ??a = "Inter ??H"; |
41 let ?a = "Inter ?H"; |
42 |
42 |
43 assume mono: "mono f"; |
43 assume mono: "mono f"; |
44 show "f ??a = ??a"; |
44 show "f ?a = ?a"; |
45 proof -; |
45 proof -; |
46 {{; |
46 {{; |
47 fix x; |
47 fix x; |
48 assume mem: "x : ??H"; |
48 assume mem: "x : ?H"; |
49 hence "??a <= x"; by (rule Inter_lower); |
49 hence "?a <= x"; by (rule Inter_lower); |
50 with mono; have "f ??a <= f x"; ..; |
50 with mono; have "f ?a <= f x"; ..; |
51 also; from mem; have "... <= x"; ..; |
51 also; from mem; have "... <= x"; ..; |
52 finally; have "f ??a <= x"; .; |
52 finally; have "f ?a <= x"; .; |
53 }}; |
53 }}; |
54 hence ge: "f ??a <= ??a"; by (rule Inter_greatest); |
54 hence ge: "f ?a <= ?a"; by (rule Inter_greatest); |
55 {{; |
55 {{; |
56 also; presume "... <= f ??a"; |
56 also; presume "... <= f ?a"; |
57 finally (order_antisym); show ??thesis; .; |
57 finally (order_antisym); show ?thesis; .; |
58 }}; |
58 }}; |
59 from mono ge; have "f (f ??a) <= f ??a"; ..; |
59 from mono ge; have "f (f ?a) <= f ?a"; ..; |
60 hence "f ??a : ??H"; ..; |
60 hence "f ?a : ?H"; ..; |
61 thus "??a <= f ??a"; by (rule Inter_lower); |
61 thus "?a <= f ?a"; by (rule Inter_lower); |
62 qed; |
62 qed; |
63 qed; |
63 qed; |
64 |
64 |
65 |
65 |
66 end; |
66 end; |