equal
deleted
inserted
replaced
338 |
338 |
339 |
339 |
340 lemma cpo_cont_lemma: |
340 lemma cpo_cont_lemma: |
341 "[| monofun (f::'a::cpo => 'b::cpo); (!Y. chain Y --> f (lub(range Y)) << (LUB i. f (Y i))) |] ==> cont f" |
341 "[| monofun (f::'a::cpo => 'b::cpo); (!Y. chain Y --> f (lub(range Y)) << (LUB i. f (Y i))) |] ==> cont f" |
342 apply (rule monocontlub2cont, auto) |
342 apply (rule monocontlub2cont, auto) |
343 apply (simp add: contlub, auto) |
343 apply (simp add: contlub_def, auto) |
344 apply (erule_tac x="Y" in allE, auto) |
344 apply (erule_tac x="Y" in allE, auto) |
345 apply (simp add: po_eq_conv) |
345 apply (simp add: po_eq_conv) |
346 apply (frule cpo,auto) |
346 apply (frule cpo,auto) |
347 apply (frule is_lubD1) |
347 apply (frule is_lubD1) |
348 apply (frule ub2ub_monofun, auto) |
348 apply (frule ub2ub_monofun, auto) |