19 (* Unions and limits *) |
19 (* Unions and limits *) |
20 |
20 |
21 goal thy "Inf (A Un B) = Inf A && Inf B"; |
21 goal thy "Inf (A Un B) = Inf A && Inf B"; |
22 br (Inf_uniq RS mp) 1; |
22 br (Inf_uniq RS mp) 1; |
23 by (rewtac is_Inf_def); |
23 by (rewtac is_Inf_def); |
24 by (safe_tac (!claset)); |
24 by (safe_tac (claset())); |
25 |
25 |
26 br (conjI RS (le_trans RS mp)) 1; |
26 br (conjI RS (le_trans RS mp)) 1; |
27 br inf_lb1 1; |
27 br inf_lb1 1; |
28 be Inf_lb 1; |
28 be Inf_lb 1; |
29 |
29 |
40 qed "Inf_Un_eq"; |
40 qed "Inf_Un_eq"; |
41 |
41 |
42 goal thy "Inf (UN i:A. B i) = Inf {Inf (B i) |i. i:A}"; |
42 goal thy "Inf (UN i:A. B i) = Inf {Inf (B i) |i. i:A}"; |
43 br (Inf_uniq RS mp) 1; |
43 br (Inf_uniq RS mp) 1; |
44 by (rewtac is_Inf_def); |
44 by (rewtac is_Inf_def); |
45 by (safe_tac (!claset)); |
45 by (safe_tac (claset())); |
46 (*level 3*) |
46 (*level 3*) |
47 br (conjI RS (le_trans RS mp)) 1; |
47 br (conjI RS (le_trans RS mp)) 1; |
48 be Inf_lb 2; |
48 be Inf_lb 2; |
49 br (sing_Inf_eq RS subst) 1; |
49 br (sing_Inf_eq RS subst) 1; |
50 br (Inf_subset_antimon RS mp) 1; |
50 br (Inf_subset_antimon RS mp) 1; |
51 by (Fast_tac 1); |
51 by (Fast_tac 1); |
52 (*level 8*) |
52 (*level 8*) |
53 by (stac le_Inf_eq 1); |
53 by (stac le_Inf_eq 1); |
54 by (safe_tac (!claset)); |
54 by (safe_tac (claset())); |
55 by (stac le_Inf_eq 1); |
55 by (stac le_Inf_eq 1); |
56 by (Fast_tac 1); |
56 by (Fast_tac 1); |
57 qed "Inf_UN_eq"; |
57 qed "Inf_UN_eq"; |
58 |
58 |
59 |
59 |
60 |
60 |
61 goal thy "Sup (A Un B) = Sup A || Sup B"; |
61 goal thy "Sup (A Un B) = Sup A || Sup B"; |
62 br (Sup_uniq RS mp) 1; |
62 br (Sup_uniq RS mp) 1; |
63 by (rewtac is_Sup_def); |
63 by (rewtac is_Sup_def); |
64 by (safe_tac (!claset)); |
64 by (safe_tac (claset())); |
65 |
65 |
66 br (conjI RS (le_trans RS mp)) 1; |
66 br (conjI RS (le_trans RS mp)) 1; |
67 be Sup_ub 1; |
67 be Sup_ub 1; |
68 br sup_ub1 1; |
68 br sup_ub1 1; |
69 |
69 |
80 qed "Sup_Un_eq"; |
80 qed "Sup_Un_eq"; |
81 |
81 |
82 goal thy "Sup (UN i:A. B i) = Sup {Sup (B i) |i. i:A}"; |
82 goal thy "Sup (UN i:A. B i) = Sup {Sup (B i) |i. i:A}"; |
83 br (Sup_uniq RS mp) 1; |
83 br (Sup_uniq RS mp) 1; |
84 by (rewtac is_Sup_def); |
84 by (rewtac is_Sup_def); |
85 by (safe_tac (!claset)); |
85 by (safe_tac (claset())); |
86 (*level 3*) |
86 (*level 3*) |
87 br (conjI RS (le_trans RS mp)) 1; |
87 br (conjI RS (le_trans RS mp)) 1; |
88 be Sup_ub 1; |
88 be Sup_ub 1; |
89 br (sing_Sup_eq RS subst) 1; |
89 br (sing_Sup_eq RS subst) 1; |
90 back(); |
90 back(); |
91 br (Sup_subset_mon RS mp) 1; |
91 br (Sup_subset_mon RS mp) 1; |
92 by (Fast_tac 1); |
92 by (Fast_tac 1); |
93 (*level 8*) |
93 (*level 8*) |
94 by (stac ge_Sup_eq 1); |
94 by (stac ge_Sup_eq 1); |
95 by (safe_tac (!claset)); |
95 by (safe_tac (claset())); |
96 by (stac ge_Sup_eq 1); |
96 by (stac ge_Sup_eq 1); |
97 by (Fast_tac 1); |
97 by (Fast_tac 1); |
98 qed "Sup_UN_eq"; |
98 qed "Sup_UN_eq"; |