179 (etac (inst_up_pcpo RS ssubst) 1), |
179 (etac (inst_up_pcpo RS ssubst) 1), |
180 (resolve_tac (tl prems) 1), |
180 (resolve_tac (tl prems) 1), |
181 (asm_simp_tac (Up0_ss addsimps [cont_Iup]) 1) |
181 (asm_simp_tac (Up0_ss addsimps [cont_Iup]) 1) |
182 ]); |
182 ]); |
183 |
183 |
|
184 val tac = (simp_tac (!simpset addsimps [cont_Iup,cont_Ifup1, |
|
185 cont_Ifup2,cont2cont_CF1L]) 1); |
184 |
186 |
185 qed_goalw "fup1" Up3.thy [up_def,fup_def] "fup`f`UU=UU" |
187 qed_goalw "fup1" Up3.thy [up_def,fup_def] "fup`f`UU=UU" |
186 (fn prems => |
188 (fn prems => |
187 [ |
189 [ |
188 (stac inst_up_pcpo 1), |
190 (stac inst_up_pcpo 1), |
189 (stac beta_cfun 1), |
191 (stac beta_cfun 1), |
190 (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, |
192 tac, |
191 cont_Ifup2,cont2cont_CF1L]) 1)), |
193 (stac beta_cfun 1), |
192 (stac beta_cfun 1), |
194 tac, |
193 (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, |
|
194 cont_Ifup2,cont2cont_CF1L]) 1)), |
|
195 (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1) |
195 (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1) |
196 ]); |
196 ]); |
197 |
197 |
198 qed_goalw "fup2" Up3.thy [up_def,fup_def] "fup`f`(up`x)=f`x" |
198 qed_goalw "fup2" Up3.thy [up_def,fup_def] "fup`f`(up`x)=f`x" |
199 (fn prems => |
199 (fn prems => |
200 [ |
200 [ |
201 (stac beta_cfun 1), |
201 (stac beta_cfun 1), |
202 (rtac cont_Iup 1), |
202 (rtac cont_Iup 1), |
203 (stac beta_cfun 1), |
203 (stac beta_cfun 1), |
204 (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, |
204 tac, |
205 cont_Ifup2,cont2cont_CF1L]) 1)), |
|
206 (stac beta_cfun 1), |
205 (stac beta_cfun 1), |
207 (rtac cont_Ifup2 1), |
206 (rtac cont_Ifup2 1), |
208 (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1) |
207 (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1) |
209 ]); |
208 ]); |
210 |
209 |
228 \ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))" |
227 \ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))" |
229 (fn prems => |
228 (fn prems => |
230 [ |
229 [ |
231 (cut_facts_tac prems 1), |
230 (cut_facts_tac prems 1), |
232 (stac beta_cfun 1), |
231 (stac beta_cfun 1), |
233 (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, |
232 tac, |
234 cont_Ifup2,cont2cont_CF1L]) 1)), |
233 (stac beta_cfun 1), |
235 (stac beta_cfun 1), |
234 tac, |
236 (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, |
|
237 cont_Ifup2,cont2cont_CF1L]) 1)), |
|
238 |
|
239 (stac (beta_cfun RS ext) 1), |
235 (stac (beta_cfun RS ext) 1), |
240 (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, |
236 tac, |
241 cont_Ifup2,cont2cont_CF1L]) 1)), |
|
242 (rtac thelub_up1a 1), |
237 (rtac thelub_up1a 1), |
243 (atac 1), |
238 (atac 1), |
244 (etac exE 1), |
239 (etac exE 1), |
245 (etac exE 1), |
240 (etac exE 1), |
246 (rtac exI 1), |
241 (rtac exI 1), |