equal
deleted
inserted
replaced
322 by (rule stream_reach2) |
322 by (rule stream_reach2) |
323 |
323 |
324 |
324 |
325 lemma cpo_cont_lemma: |
325 lemma cpo_cont_lemma: |
326 "[| monofun (f::'a::cpo => 'b::cpo); (!Y. chain Y --> f (lub(range Y)) << (LUB i. f (Y i))) |] ==> cont f" |
326 "[| monofun (f::'a::cpo => 'b::cpo); (!Y. chain Y --> f (lub(range Y)) << (LUB i. f (Y i))) |] ==> cont f" |
327 apply (rule monocontlub2cont, auto) |
327 by (erule contI2, simp) |
328 apply (simp add: contlub_def, auto) |
|
329 apply (erule_tac x="Y" in allE, auto) |
|
330 apply (simp add: po_eq_conv) |
|
331 apply (frule cpo,auto) |
|
332 apply (frule is_lubD1) |
|
333 apply (frule ub2ub_monofun, auto) |
|
334 apply (drule thelubI, auto) |
|
335 apply (rule is_lub_thelub, auto) |
|
336 by (erule ch2ch_monofun, simp) |
|
337 |
328 |
338 end |
329 end |