22 |
22 |
23 Goal "Iup(x) ~= UU"; |
23 Goal "Iup(x) ~= UU"; |
24 by (stac inst_up_pcpo 1); |
24 by (stac inst_up_pcpo 1); |
25 by (rtac defined_Iup 1); |
25 by (rtac defined_Iup 1); |
26 qed "defined_Iup2"; |
26 qed "defined_Iup2"; |
|
27 AddIffs [defined_Iup2]; |
27 |
28 |
28 (* ------------------------------------------------------------------------ *) |
29 (* ------------------------------------------------------------------------ *) |
29 (* continuity for Iup *) |
30 (* continuity for Iup *) |
30 (* ------------------------------------------------------------------------ *) |
31 (* ------------------------------------------------------------------------ *) |
31 |
32 |
47 Goal "cont(Iup)"; |
48 Goal "cont(Iup)"; |
48 by (rtac monocontlub2cont 1); |
49 by (rtac monocontlub2cont 1); |
49 by (rtac monofun_Iup 1); |
50 by (rtac monofun_Iup 1); |
50 by (rtac contlub_Iup 1); |
51 by (rtac contlub_Iup 1); |
51 qed "cont_Iup"; |
52 qed "cont_Iup"; |
52 |
53 AddIffs [cont_Iup]; |
53 |
54 |
54 (* ------------------------------------------------------------------------ *) |
55 (* ------------------------------------------------------------------------ *) |
55 (* continuity for Ifup *) |
56 (* continuity for Ifup *) |
56 (* ------------------------------------------------------------------------ *) |
57 (* ------------------------------------------------------------------------ *) |
57 |
58 |
130 |
131 |
131 (* ------------------------------------------------------------------------ *) |
132 (* ------------------------------------------------------------------------ *) |
132 (* continuous versions of lemmas for ('a)u *) |
133 (* continuous versions of lemmas for ('a)u *) |
133 (* ------------------------------------------------------------------------ *) |
134 (* ------------------------------------------------------------------------ *) |
134 |
135 |
135 Goalw [up_def] "z = UU | (? x. z = up`x)"; |
136 Goalw [up_def] "z = UU | (EX x. z = up`x)"; |
136 by (simp_tac (Up0_ss addsimps [cont_Iup]) 1); |
137 by (simp_tac (Up0_ss addsimps [cont_Iup]) 1); |
137 by (stac inst_up_pcpo 1); |
138 by (stac inst_up_pcpo 1); |
138 by (rtac Exh_Up 1); |
139 by (rtac Exh_Up 1); |
139 qed "Exh_Up1"; |
140 qed "Exh_Up1"; |
140 |
141 |
141 Goalw [up_def] "up`x=up`y ==> x=y"; |
142 Goalw [up_def] "up`x=up`y ==> x=y"; |
142 by (rtac inject_Iup 1); |
143 by (rtac inject_Iup 1); |
143 by (etac box_equals 1); |
144 by Auto_tac; |
144 by (simp_tac (Up0_ss addsimps [cont_Iup]) 1); |
|
145 by (simp_tac (Up0_ss addsimps [cont_Iup]) 1); |
|
146 qed "inject_up"; |
145 qed "inject_up"; |
147 |
146 |
148 Goalw [up_def] " up`x ~= UU"; |
147 Goalw [up_def] " up`x ~= UU"; |
149 by (simp_tac (Up0_ss addsimps [cont_Iup]) 1); |
148 by Auto_tac; |
150 by (rtac defined_Iup2 1); |
|
151 qed "defined_up"; |
149 qed "defined_up"; |
152 |
150 |
153 val prems = Goalw [up_def] |
151 val prems = Goalw [up_def] |
154 "[| p=UU ==> Q; !!x. p=up`x==>Q|] ==>Q"; |
152 "[| p=UU ==> Q; !!x. p=up`x==>Q|] ==>Q"; |
155 by (rtac upE 1); |
153 by (rtac upE 1); |
191 by (simp_tac (Up0_ss addsimps [cont_Iup]) 1); |
189 by (simp_tac (Up0_ss addsimps [cont_Iup]) 1); |
192 by (rtac less_up2c 1); |
190 by (rtac less_up2c 1); |
193 qed "less_up4c"; |
191 qed "less_up4c"; |
194 |
192 |
195 Goalw [up_def,fup_def] |
193 Goalw [up_def,fup_def] |
196 "[| chain(Y); ? i x. Y(i) = up`x |] ==>\ |
194 "[| chain(Y); EX i x. Y(i) = up`x |] ==>\ |
197 \ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"; |
195 \ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"; |
198 by (stac beta_cfun 1); |
196 by (stac beta_cfun 1); |
199 by tac; |
197 by tac; |
200 by (stac beta_cfun 1); |
198 by (stac beta_cfun 1); |
201 by tac; |
199 by tac; |
220 by (rtac thelub_up1b 1); |
218 by (rtac thelub_up1b 1); |
221 by (atac 1); |
219 by (atac 1); |
222 by (strip_tac 1); |
220 by (strip_tac 1); |
223 by (dtac spec 1); |
221 by (dtac spec 1); |
224 by (dtac spec 1); |
222 by (dtac spec 1); |
225 by (rtac swap 1); |
223 by (asm_full_simp_tac (Up0_ss addsimps [cont_Iup]) 1); |
226 by (atac 1); |
|
227 by (dtac notnotD 1); |
|
228 by (etac box_equals 1); |
|
229 by (rtac refl 1); |
|
230 by (simp_tac (Up0_ss addsimps [cont_Iup]) 1); |
|
231 qed "thelub_up2b"; |
224 qed "thelub_up2b"; |
232 |
225 |
233 |
226 |
234 Goal "(? x. z = up`x) = (z~=UU)"; |
227 Goal "(EX x. z = up`x) = (z~=UU)"; |
235 by (rtac iffI 1); |
228 by (rtac iffI 1); |
236 by (etac exE 1); |
229 by (etac exE 1); |
237 by (hyp_subst_tac 1); |
230 by (hyp_subst_tac 1); |
238 by (rtac defined_up 1); |
231 by (rtac defined_up 1); |
239 by (res_inst_tac [("p","z")] upE1 1); |
232 by (res_inst_tac [("p","z")] upE1 1); |
241 by (atac 1); |
234 by (atac 1); |
242 by (etac exI 1); |
235 by (etac exI 1); |
243 qed "up_lemma2"; |
236 qed "up_lemma2"; |
244 |
237 |
245 |
238 |
246 Goal "[| chain(Y); lub(range(Y)) = up`x |] ==> ? i x. Y(i) = up`x"; |
239 Goal "[| chain(Y); lub(range(Y)) = up`x |] ==> EX i x. Y(i) = up`x"; |
247 by (rtac exE 1); |
240 by (rtac exE 1); |
248 by (rtac chain_UU_I_inverse2 1); |
241 by (rtac chain_UU_I_inverse2 1); |
249 by (rtac (up_lemma2 RS iffD1) 1); |
242 by (rtac (up_lemma2 RS iffD1) 1); |
250 by (etac exI 1); |
243 by (etac exI 1); |
251 by (rtac exI 1); |
244 by (rtac exI 1); |
252 by (rtac (up_lemma2 RS iffD2) 1); |
245 by (rtac (up_lemma2 RS iffD2) 1); |
253 by (atac 1); |
246 by (atac 1); |
254 qed "thelub_up2a_rev"; |
247 qed "thelub_up2a_rev"; |
255 |
248 |
256 Goal "[| chain(Y); lub(range(Y)) = UU |] ==> ! i x. Y(i) ~= up`x"; |
249 Goal "[| chain(Y); lub(range(Y)) = UU |] ==> ! i x. Y(i) ~= up`x"; |
257 by (rtac allI 1); |
250 by (blast_tac (claset() addSDs [chain_UU_I RS spec, |
258 by (rtac (not_ex RS iffD1) 1); |
251 exI RS (up_lemma2 RS iffD1)]) 1); |
259 by (rtac contrapos 1); |
|
260 by (etac (up_lemma2 RS iffD1) 2); |
|
261 by (fast_tac (HOL_cs addSDs [chain_UU_I RS spec]) 1); |
|
262 qed "thelub_up2b_rev"; |
252 qed "thelub_up2b_rev"; |
263 |
253 |
264 |
254 |
265 Goal "chain(Y) ==> lub(range(Y)) = UU | \ |
255 Goal "chain(Y) ==> lub(range(Y)) = UU | \ |
266 \ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"; |
256 \ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"; |