src/HOLCF/Ssum.thy
 changeset 26962 c8b20f615d6c parent 26046 1624b3304bb9 child 27310 d0229bc6c461
equal inserted replaced
26961:290e1571c829 26962:c8b20f615d6c
214 apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff)
214 apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff)
215 done
215 done
216
216
217 subsection {* Strict sum is a bifinite domain *}
217 subsection {* Strict sum is a bifinite domain *}
218
218
219 instance "++" :: (bifinite, bifinite) approx ..
219 instantiation "++" :: (bifinite, bifinite) bifinite
220
220 begin
221

222 definition
222   approx_ssum_def:
223   approx_ssum_def:
223     "approx \<equiv> \<lambda>n. sscase\<cdot>(\<Lambda> x. sinl\<cdot>(approx n\<cdot>x))\<cdot>(\<Lambda> y. sinr\<cdot>(approx n\<cdot>y))"
224     "approx = (\<lambda>n. sscase\<cdot>(\<Lambda> x. sinl\<cdot>(approx n\<cdot>x))\<cdot>(\<Lambda> y. sinr\<cdot>(approx n\<cdot>y)))"
224
225
225 lemma approx_sinl [simp]: "approx i\<cdot>(sinl\<cdot>x) = sinl\<cdot>(approx i\<cdot>x)"
226 lemma approx_sinl [simp]: "approx i\<cdot>(sinl\<cdot>x) = sinl\<cdot>(approx i\<cdot>x)"
226 unfolding approx_ssum_def by (cases "x = \<bottom>") simp_all
227 unfolding approx_ssum_def by (cases "x = \<bottom>") simp_all
227
228
228 lemma approx_sinr [simp]: "approx i\<cdot>(sinr\<cdot>x) = sinr\<cdot>(approx i\<cdot>x)"
229 lemma approx_sinr [simp]: "approx i\<cdot>(sinr\<cdot>x) = sinr\<cdot>(approx i\<cdot>x)"
229 unfolding approx_ssum_def by (cases "x = \<bottom>") simp_all
230 unfolding approx_ssum_def by (cases "x = \<bottom>") simp_all
230
231
231 instance "++" :: (bifinite, bifinite) bifinite
232 instance proof
232 proof

233   fix i :: nat and x :: "'a \<oplus> 'b"
233   fix i :: nat and x :: "'a \<oplus> 'b"
234   show "chain (\<lambda>i. approx i\<cdot>x)"
234   show "chain (\<lambda>i. approx i\<cdot>x)"
235     unfolding approx_ssum_def by simp
235     unfolding approx_ssum_def by simp
236   show "(\<Squnion>i. approx i\<cdot>x) = x"
236   show "(\<Squnion>i. approx i\<cdot>x) = x"
237     unfolding approx_ssum_def
237     unfolding approx_ssum_def
246     by (rule finite_subset,
246     by (rule finite_subset,
247         intro finite_UnI finite_imageI finite_fixes_approx)
247         intro finite_UnI finite_imageI finite_fixes_approx)
248 qed
248 qed
249
249
250 end
250 end

251

252 end