equal
deleted
inserted
replaced
146 \<Longrightarrow> range Y <<| Iup (\<Squnion>i. THE a. Iup a = Y(i + j))" |
146 \<Longrightarrow> range Y <<| Iup (\<Squnion>i. THE a. Iup a = Y(i + j))" |
147 apply (rule_tac j1 = j in is_lub_range_shift [THEN iffD1]) |
147 apply (rule_tac j1 = j in is_lub_range_shift [THEN iffD1]) |
148 apply assumption |
148 apply assumption |
149 apply (subst up_lemma5, assumption+) |
149 apply (subst up_lemma5, assumption+) |
150 apply (rule is_lub_Iup) |
150 apply (rule is_lub_Iup) |
151 apply (rule thelubE [OF _ refl]) |
151 apply (rule cpo_lubI) |
152 apply (erule (1) up_lemma4) |
152 apply (erule (1) up_lemma4) |
153 done |
153 done |
154 |
154 |
155 lemma up_chain_lemma: |
155 lemma up_chain_lemma: |
156 "chain Y \<Longrightarrow> |
156 "chain Y \<Longrightarrow> |
168 |
168 |
169 lemma cpo_up: "chain (Y::nat \<Rightarrow> 'a u) \<Longrightarrow> \<exists>x. range Y <<| x" |
169 lemma cpo_up: "chain (Y::nat \<Rightarrow> 'a u) \<Longrightarrow> \<exists>x. range Y <<| x" |
170 apply (frule up_chain_lemma, safe) |
170 apply (frule up_chain_lemma, safe) |
171 apply (rule_tac x="Iup (lub (range A))" in exI) |
171 apply (rule_tac x="Iup (lub (range A))" in exI) |
172 apply (erule_tac j="j" in is_lub_range_shift [THEN iffD1, standard]) |
172 apply (erule_tac j="j" in is_lub_range_shift [THEN iffD1, standard]) |
173 apply (simp add: is_lub_Iup thelubE) |
173 apply (simp add: is_lub_Iup cpo_lubI) |
174 apply (rule exI, rule lub_const) |
174 apply (rule exI, rule lub_const) |
175 done |
175 done |
176 |
176 |
177 instance u :: (cpo) cpo |
177 instance u :: (cpo) cpo |
178 by intro_classes (rule cpo_up) |
178 by intro_classes (rule cpo_up) |
196 text {* continuity for @{term Iup} *} |
196 text {* continuity for @{term Iup} *} |
197 |
197 |
198 lemma cont_Iup: "cont Iup" |
198 lemma cont_Iup: "cont Iup" |
199 apply (rule contI) |
199 apply (rule contI) |
200 apply (rule is_lub_Iup) |
200 apply (rule is_lub_Iup) |
201 apply (erule thelubE [OF _ refl]) |
201 apply (erule cpo_lubI) |
202 done |
202 done |
203 |
203 |
204 text {* continuity for @{term Ifup} *} |
204 text {* continuity for @{term Ifup} *} |
205 |
205 |
206 lemma cont_Ifup1: "cont (\<lambda>f. Ifup f x)" |
206 lemma cont_Ifup1: "cont (\<lambda>f. Ifup f x)" |