54 |
54 |
55 val prems = goalw thy [Inf_def] "x:A ==> Inf A [= x"; |
55 val prems = goalw thy [Inf_def] "x:A ==> Inf A [= x"; |
56 by (cut_facts_tac prems 1); |
56 by (cut_facts_tac prems 1); |
57 br selectI2 1; |
57 br selectI2 1; |
58 br Inf_is_Inf 1; |
58 br Inf_is_Inf 1; |
59 by (rewrite_goals_tac [is_Inf_def]); |
59 by (rewtac is_Inf_def); |
60 by (fast_tac set_cs 1); |
60 by (fast_tac set_cs 1); |
61 qed "Inf_lb"; |
61 qed "Inf_lb"; |
62 |
62 |
63 val [prem] = goalw thy [Inf_def] "(!!x. x:A ==> z [= x) ==> z [= Inf A"; |
63 val [prem] = goalw thy [Inf_def] "(!!x. x:A ==> z [= x) ==> z [= Inf A"; |
64 br selectI2 1; |
64 br selectI2 1; |
65 br Inf_is_Inf 1; |
65 br Inf_is_Inf 1; |
66 by (rewrite_goals_tac [is_Inf_def]); |
66 by (rewtac is_Inf_def); |
67 by (step_tac HOL_cs 1); |
67 by (step_tac HOL_cs 1); |
68 by (step_tac HOL_cs 1); |
68 by (step_tac HOL_cs 1); |
69 be mp 1; |
69 be mp 1; |
70 br ballI 1; |
70 br ballI 1; |
71 be prem 1; |
71 be prem 1; |
74 |
74 |
75 val prems = goalw thy [Sup_def] "x:A ==> x [= Sup A"; |
75 val prems = goalw thy [Sup_def] "x:A ==> x [= Sup A"; |
76 by (cut_facts_tac prems 1); |
76 by (cut_facts_tac prems 1); |
77 br selectI2 1; |
77 br selectI2 1; |
78 br Sup_is_Sup 1; |
78 br Sup_is_Sup 1; |
79 by (rewrite_goals_tac [is_Sup_def]); |
79 by (rewtac is_Sup_def); |
80 by (fast_tac set_cs 1); |
80 by (fast_tac set_cs 1); |
81 qed "Sup_ub"; |
81 qed "Sup_ub"; |
82 |
82 |
83 val [prem] = goalw thy [Sup_def] "(!!x. x:A ==> x [= z) ==> Sup A [= z"; |
83 val [prem] = goalw thy [Sup_def] "(!!x. x:A ==> x [= z) ==> Sup A [= z"; |
84 br selectI2 1; |
84 br selectI2 1; |
85 br Sup_is_Sup 1; |
85 br Sup_is_Sup 1; |
86 by (rewrite_goals_tac [is_Sup_def]); |
86 by (rewtac is_Sup_def); |
87 by (step_tac HOL_cs 1); |
87 by (step_tac HOL_cs 1); |
88 by (step_tac HOL_cs 1); |
88 by (step_tac HOL_cs 1); |
89 be mp 1; |
89 be mp 1; |
90 br ballI 1; |
90 br ballI 1; |
91 be prem 1; |
91 be prem 1; |
124 (** Subsets and limits **) |
124 (** Subsets and limits **) |
125 |
125 |
126 goal thy "A <= B --> Inf B [= Inf A"; |
126 goal thy "A <= B --> Inf B [= Inf A"; |
127 br impI 1; |
127 br impI 1; |
128 by (stac le_Inf_eq 1); |
128 by (stac le_Inf_eq 1); |
129 by (rewrite_goals_tac [Ball_def]); |
129 by (rewtac Ball_def); |
130 by (safe_tac set_cs); |
130 by (safe_tac set_cs); |
131 bd subsetD 1; |
131 bd subsetD 1; |
132 ba 1; |
132 ba 1; |
133 be Inf_lb 1; |
133 be Inf_lb 1; |
134 qed "Inf_subset_antimon"; |
134 qed "Inf_subset_antimon"; |
135 |
135 |
136 goal thy "A <= B --> Sup A [= Sup B"; |
136 goal thy "A <= B --> Sup A [= Sup B"; |
137 br impI 1; |
137 br impI 1; |
138 by (stac ge_Sup_eq 1); |
138 by (stac ge_Sup_eq 1); |
139 by (rewrite_goals_tac [Ball_def]); |
139 by (rewtac Ball_def); |
140 by (safe_tac set_cs); |
140 by (safe_tac set_cs); |
141 bd subsetD 1; |
141 bd subsetD 1; |
142 ba 1; |
142 ba 1; |
143 be Sup_ub 1; |
143 be Sup_ub 1; |
144 qed "Sup_subset_mon"; |
144 qed "Sup_subset_mon"; |
146 |
146 |
147 (** singleton / empty limits **) |
147 (** singleton / empty limits **) |
148 |
148 |
149 goal thy "Inf {x} = x"; |
149 goal thy "Inf {x} = x"; |
150 br (Inf_uniq RS mp) 1; |
150 br (Inf_uniq RS mp) 1; |
151 by (rewrite_goals_tac [is_Inf_def]); |
151 by (rewtac is_Inf_def); |
152 by (safe_tac set_cs); |
152 by (safe_tac set_cs); |
153 br le_refl 1; |
153 br le_refl 1; |
154 by (fast_tac set_cs 1); |
154 by (fast_tac set_cs 1); |
155 qed "sing_Inf_eq"; |
155 qed "sing_Inf_eq"; |
156 |
156 |
157 goal thy "Sup {x} = x"; |
157 goal thy "Sup {x} = x"; |
158 br (Sup_uniq RS mp) 1; |
158 br (Sup_uniq RS mp) 1; |
159 by (rewrite_goals_tac [is_Sup_def]); |
159 by (rewtac is_Sup_def); |
160 by (safe_tac set_cs); |
160 by (safe_tac set_cs); |
161 br le_refl 1; |
161 br le_refl 1; |
162 by (fast_tac set_cs 1); |
162 by (fast_tac set_cs 1); |
163 qed "sing_Sup_eq"; |
163 qed "sing_Sup_eq"; |
164 |
164 |
165 |
165 |
166 goal thy "Inf {} = Sup {x. True}"; |
166 goal thy "Inf {} = Sup {x. True}"; |
167 br (Inf_uniq RS mp) 1; |
167 br (Inf_uniq RS mp) 1; |
168 by (rewrite_goals_tac [is_Inf_def]); |
168 by (rewtac is_Inf_def); |
169 by (safe_tac set_cs); |
169 by (safe_tac set_cs); |
170 br (sing_Sup_eq RS subst) 1; |
170 br (sing_Sup_eq RS subst) 1; |
171 back(); |
171 back(); |
172 br (Sup_subset_mon RS mp) 1; |
172 br (Sup_subset_mon RS mp) 1; |
173 by (fast_tac set_cs 1); |
173 by (fast_tac set_cs 1); |
174 qed "empty_Inf_eq"; |
174 qed "empty_Inf_eq"; |
175 |
175 |
176 goal thy "Sup {} = Inf {x. True}"; |
176 goal thy "Sup {} = Inf {x. True}"; |
177 br (Sup_uniq RS mp) 1; |
177 br (Sup_uniq RS mp) 1; |
178 by (rewrite_goals_tac [is_Sup_def]); |
178 by (rewtac is_Sup_def); |
179 by (safe_tac set_cs); |
179 by (safe_tac set_cs); |
180 br (sing_Inf_eq RS subst) 1; |
180 br (sing_Inf_eq RS subst) 1; |
181 br (Inf_subset_antimon RS mp) 1; |
181 br (Inf_subset_antimon RS mp) 1; |
182 by (fast_tac set_cs 1); |
182 by (fast_tac set_cs 1); |
183 qed "empty_Sup_eq"; |
183 qed "empty_Sup_eq"; |