src/HOL/HOLCF/ConvexPD.thy
changeset 41286 3d7685a4a5ff
parent 41111 b497cc48e563
child 41287 029a6fc1bfb8
     1.1 --- a/src/HOL/HOLCF/ConvexPD.thy	Sun Dec 19 04:06:02 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/ConvexPD.thy	Sun Dec 19 05:15:31 2010 -0800
     1.3 @@ -468,6 +468,19 @@
     1.4  
     1.5  subsection {* Convex powerdomain is a domain *}
     1.6  
     1.7 +lemma approx_chain_convex_map:
     1.8 +  assumes "approx_chain a"
     1.9 +  shows "approx_chain (\<lambda>i. convex_map\<cdot>(a i))"
    1.10 +  using assms unfolding approx_chain_def
    1.11 +  by (simp add: lub_APP convex_map_ID finite_deflation_convex_map)
    1.12 +
    1.13 +instance convex_pd :: ("domain") bifinite
    1.14 +proof
    1.15 +  show "\<exists>(a::nat \<Rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd). approx_chain a"
    1.16 +    using bifinite [where 'a='a]
    1.17 +    by (fast intro!: approx_chain_convex_map)
    1.18 +qed
    1.19 +
    1.20  definition
    1.21    convex_approx :: "nat \<Rightarrow> udom convex_pd \<rightarrow> udom convex_pd"
    1.22  where