equal
deleted
inserted
replaced
746 apply (simp add: chain_in cpo_lub [THEN islub_in] lub_const) |
746 apply (simp add: chain_in cpo_lub [THEN islub_in] lub_const) |
747 done |
747 done |
748 |
748 |
749 lemma cf_least: |
749 lemma cf_least: |
750 "[|cpo(D); pcpo(E); y \<in> cont(D,E)|]==>rel(cf(D,E),(\<lambda>x \<in> set(D).bot(E)),y)" |
750 "[|cpo(D); pcpo(E); y \<in> cont(D,E)|]==>rel(cf(D,E),(\<lambda>x \<in> set(D).bot(E)),y)" |
751 apply (rule rel_cfI, simp) |
751 apply (rule rel_cfI, simp, typecheck) |
752 apply typecheck |
|
753 done |
752 done |
754 |
753 |
755 lemma pcpo_cf: |
754 lemma pcpo_cf: |
756 "[|cpo(D); pcpo(E)|] ==> pcpo(cf(D,E))" |
755 "[|cpo(D); pcpo(E)|] ==> pcpo(cf(D,E))" |
757 apply (rule pcpoI) |
756 apply (rule pcpoI) |