123 apply (rule_tac [2] is_ub_thelub) |
123 apply (rule_tac [2] is_ub_thelub) |
124 prefer 2 apply (assumption) |
124 prefer 2 apply (assumption) |
125 apply assumption |
125 apply assumption |
126 done |
126 done |
127 |
127 |
|
128 lemma diag_lub: |
|
129 fixes Y :: "nat \<Rightarrow> nat \<Rightarrow> 'a::cpo" |
|
130 assumes 1: "\<And>j. chain (\<lambda>i. Y i j)" |
|
131 assumes 2: "\<And>i. chain (\<lambda>j. Y i j)" |
|
132 shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>i. Y i i)" |
|
133 proof (rule antisym_less) |
|
134 have 3: "chain (\<lambda>i. Y i i)" |
|
135 apply (rule chainI) |
|
136 apply (rule trans_less) |
|
137 apply (rule chainE [OF 1]) |
|
138 apply (rule chainE [OF 2]) |
|
139 done |
|
140 have 4: "chain (\<lambda>i. \<Squnion>j. Y i j)" |
|
141 apply (rule chainI) |
|
142 apply (rule lub_mono [OF 2 2, rule_format]) |
|
143 apply (rule chainE [OF 1]) |
|
144 done |
|
145 show "(\<Squnion>i. \<Squnion>j. Y i j) \<sqsubseteq> (\<Squnion>i. Y i i)" |
|
146 apply (rule is_lub_thelub [OF 4]) |
|
147 apply (rule ub_rangeI) |
|
148 apply (rule lub_mono3 [OF 2 3, rule_format]) |
|
149 apply (rule exI) |
|
150 apply (rule trans_less) |
|
151 apply (rule chain_mono3 [OF 1 le_maxI1]) |
|
152 apply (rule chain_mono3 [OF 2 le_maxI2]) |
|
153 done |
|
154 show "(\<Squnion>i. Y i i) \<sqsubseteq> (\<Squnion>i. \<Squnion>j. Y i j)" |
|
155 apply (rule lub_mono [OF 3 4, rule_format]) |
|
156 apply (rule is_ub_thelub [OF 2]) |
|
157 done |
|
158 qed |
|
159 |
|
160 lemma ex_lub: |
|
161 fixes Y :: "nat \<Rightarrow> nat \<Rightarrow> 'a::cpo" |
|
162 assumes 1: "\<And>j. chain (\<lambda>i. Y i j)" |
|
163 assumes 2: "\<And>i. chain (\<lambda>j. Y i j)" |
|
164 shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>j. \<Squnion>i. Y i j)" |
|
165 by (simp add: diag_lub 1 2) |
|
166 |
|
167 |
128 subsection {* Pointed cpos *} |
168 subsection {* Pointed cpos *} |
129 |
169 |
130 text {* The class pcpo of pointed cpos *} |
170 text {* The class pcpo of pointed cpos *} |
131 |
171 |
132 axclass pcpo < cpo |
172 axclass pcpo < cpo |
224 lemma flat_imp_chfin: |
264 lemma flat_imp_chfin: |
225 "ALL Y::nat=>'a::flat. chain Y --> (EX n. max_in_chain n Y)" |
265 "ALL Y::nat=>'a::flat. chain Y --> (EX n. max_in_chain n Y)" |
226 apply (unfold max_in_chain_def) |
266 apply (unfold max_in_chain_def) |
227 apply clarify |
267 apply clarify |
228 apply (case_tac "ALL i. Y (i) =UU") |
268 apply (case_tac "ALL i. Y (i) =UU") |
229 apply (rule_tac x = "0" in exI) |
|
230 apply simp |
269 apply simp |
231 apply simp |
270 apply simp |
232 apply (erule exE) |
271 apply (erule exE) |
233 apply (rule_tac x = "i" in exI) |
272 apply (rule_tac x = "i" in exI) |
234 apply clarify |
273 apply clarify |