446 convex_approx :: "nat \<Rightarrow> udom convex_pd \<rightarrow> udom convex_pd" |
446 convex_approx :: "nat \<Rightarrow> udom convex_pd \<rightarrow> udom convex_pd" |
447 where |
447 where |
448 "convex_approx = (\<lambda>i. convex_map\<cdot>(udom_approx i))" |
448 "convex_approx = (\<lambda>i. convex_map\<cdot>(udom_approx i))" |
449 |
449 |
450 lemma convex_approx: "approx_chain convex_approx" |
450 lemma convex_approx: "approx_chain convex_approx" |
451 proof (rule approx_chain.intro) |
451 using convex_map_ID finite_deflation_convex_map |
452 show "chain (\<lambda>i. convex_approx i)" |
452 unfolding convex_approx_def by (rule approx_chain_lemma1) |
453 unfolding convex_approx_def by simp |
|
454 show "(\<Squnion>i. convex_approx i) = ID" |
|
455 unfolding convex_approx_def |
|
456 by (simp add: lub_distribs convex_map_ID) |
|
457 show "\<And>i. finite_deflation (convex_approx i)" |
|
458 unfolding convex_approx_def |
|
459 by (intro finite_deflation_convex_map finite_deflation_udom_approx) |
|
460 qed |
|
461 |
453 |
462 definition convex_defl :: "defl \<rightarrow> defl" |
454 definition convex_defl :: "defl \<rightarrow> defl" |
463 where "convex_defl = defl_fun1 convex_approx convex_map" |
455 where "convex_defl = defl_fun1 convex_approx convex_map" |
464 |
456 |
465 lemma cast_convex_defl: |
457 lemma cast_convex_defl: |
466 "cast\<cdot>(convex_defl\<cdot>A) = |
458 "cast\<cdot>(convex_defl\<cdot>A) = |
467 udom_emb convex_approx oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj convex_approx" |
459 udom_emb convex_approx oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj convex_approx" |
468 unfolding convex_defl_def |
460 using convex_approx finite_deflation_convex_map |
469 apply (rule cast_defl_fun1 [OF convex_approx]) |
461 unfolding convex_defl_def by (rule cast_defl_fun1) |
470 apply (erule finite_deflation_convex_map) |
|
471 done |
|
472 |
462 |
473 instantiation convex_pd :: (bifinite) bifinite |
463 instantiation convex_pd :: (bifinite) bifinite |
474 begin |
464 begin |
475 |
465 |
476 definition |
466 definition |