equal
deleted
inserted
replaced
13 |
13 |
14 text {* The class cpo of chain complete partial orders *} |
14 text {* The class cpo of chain complete partial orders *} |
15 |
15 |
16 axclass cpo < po |
16 axclass cpo < po |
17 -- {* class axiom: *} |
17 -- {* class axiom: *} |
18 cpo: "chain S \<Longrightarrow> \<exists>x. range S <<| x" |
18 cpo: "chain S \<Longrightarrow> \<exists>x. range S <<| x" |
19 |
19 |
20 text {* in cpo's everthing equal to THE lub has lub properties for every chain *} |
20 text {* in cpo's everthing equal to THE lub has lub properties for every chain *} |
21 |
21 |
22 lemma cpo_lubI: "chain (S::nat \<Rightarrow> 'a::cpo) \<Longrightarrow> range S <<| lub (range S)" |
22 lemma cpo_lubI: "chain (S::nat \<Rightarrow> 'a::cpo) \<Longrightarrow> range S <<| (\<Squnion>i. S i)" |
23 by (fast dest: cpo elim: lubI) |
23 by (fast dest: cpo elim: lubI) |
24 |
24 |
25 lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = (l::'a::cpo)\<rbrakk> \<Longrightarrow> range S <<| l" |
25 lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = (l::'a::cpo)\<rbrakk> \<Longrightarrow> range S <<| l" |
26 by (blast dest: cpo intro: lubI) |
26 by (blast dest: cpo intro: lubI) |
27 |
27 |