equal
deleted
inserted
replaced
109 assume S: "chain S" |
109 assume S: "chain S" |
110 thus "\<exists>x. range (\<lambda>i. S i) <<| x" |
110 thus "\<exists>x. range (\<lambda>i. S i) <<| x" |
111 proof (rule up_chain_lemma) |
111 proof (rule up_chain_lemma) |
112 assume "\<forall>i. S i = Ibottom" |
112 assume "\<forall>i. S i = Ibottom" |
113 hence "range (\<lambda>i. S i) <<| Ibottom" |
113 hence "range (\<lambda>i. S i) <<| Ibottom" |
114 by (simp add: lub_const) |
114 by (simp add: is_lub_const) |
115 thus ?thesis .. |
115 thus ?thesis .. |
116 next |
116 next |
117 fix A :: "nat \<Rightarrow> 'a" |
117 fix A :: "nat \<Rightarrow> 'a" |
118 assume "range S <<| Iup (\<Squnion>i. A i)" |
118 assume "range S <<| Iup (\<Squnion>i. A i)" |
119 thus ?thesis .. |
119 thus ?thesis .. |
158 proof (rule up_chain_lemma) |
158 proof (rule up_chain_lemma) |
159 fix A and k |
159 fix A and k |
160 assume A: "\<forall>i. Iup (A i) = Y (i + k)" |
160 assume A: "\<forall>i. Iup (A i) = Y (i + k)" |
161 assume "chain A" and "range Y <<| Iup (\<Squnion>i. A i)" |
161 assume "chain A" and "range Y <<| Iup (\<Squnion>i. A i)" |
162 hence "Ifup f (\<Squnion>i. Y i) = (\<Squnion>i. Ifup f (Iup (A i)))" |
162 hence "Ifup f (\<Squnion>i. Y i) = (\<Squnion>i. Ifup f (Iup (A i)))" |
163 by (simp add: thelubI contlub_cfun_arg) |
163 by (simp add: lub_eqI contlub_cfun_arg) |
164 also have "\<dots> = (\<Squnion>i. Ifup f (Y (i + k)))" |
164 also have "\<dots> = (\<Squnion>i. Ifup f (Y (i + k)))" |
165 by (simp add: A) |
165 by (simp add: A) |
166 also have "\<dots> = (\<Squnion>i. Ifup f (Y i))" |
166 also have "\<dots> = (\<Squnion>i. Ifup f (Y i))" |
167 using Y' by (rule lub_range_shift) |
167 using Y' by (rule lub_range_shift) |
168 finally show ?thesis by simp |
168 finally show ?thesis by simp |
221 |
221 |
222 lemma up_chain_cases: |
222 lemma up_chain_cases: |
223 assumes Y: "chain Y" obtains "\<forall>i. Y i = \<bottom>" |
223 assumes Y: "chain Y" obtains "\<forall>i. Y i = \<bottom>" |
224 | A k where "\<forall>i. up\<cdot>(A i) = Y (i + k)" and "chain A" and "(\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i)" |
224 | A k where "\<forall>i. up\<cdot>(A i) = Y (i + k)" and "chain A" and "(\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i)" |
225 apply (rule up_chain_lemma [OF Y]) |
225 apply (rule up_chain_lemma [OF Y]) |
226 apply (simp_all add: inst_up_pcpo up_def cont_Iup thelubI) |
226 apply (simp_all add: inst_up_pcpo up_def cont_Iup lub_eqI) |
227 done |
227 done |
228 |
228 |
229 lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)" |
229 lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)" |
230 apply (rule compactI2) |
230 apply (rule compactI2) |
231 apply (erule up_chain_cases) |
231 apply (erule up_chain_cases) |