equal
deleted
inserted
replaced
412 lemma convex_map_bind: |
412 lemma convex_map_bind: |
413 "convex_map\<cdot>f\<cdot>(convex_bind\<cdot>xs\<cdot>g) = convex_bind\<cdot>xs\<cdot>(\<Lambda> x. convex_map\<cdot>f\<cdot>(g\<cdot>x))" |
413 "convex_map\<cdot>f\<cdot>(convex_bind\<cdot>xs\<cdot>g) = convex_bind\<cdot>xs\<cdot>(\<Lambda> x. convex_map\<cdot>f\<cdot>(g\<cdot>x))" |
414 by (simp add: convex_map_def convex_bind_bind) |
414 by (simp add: convex_map_def convex_bind_bind) |
415 |
415 |
416 lemma ep_pair_convex_map: "ep_pair e p \<Longrightarrow> ep_pair (convex_map\<cdot>e) (convex_map\<cdot>p)" |
416 lemma ep_pair_convex_map: "ep_pair e p \<Longrightarrow> ep_pair (convex_map\<cdot>e) (convex_map\<cdot>p)" |
417 apply default |
417 apply standard |
418 apply (induct_tac x rule: convex_pd_induct, simp_all add: ep_pair.e_inverse) |
418 apply (induct_tac x rule: convex_pd_induct, simp_all add: ep_pair.e_inverse) |
419 apply (induct_tac y rule: convex_pd_induct) |
419 apply (induct_tac y rule: convex_pd_induct) |
420 apply (simp_all add: ep_pair.e_p_below monofun_cfun) |
420 apply (simp_all add: ep_pair.e_p_below monofun_cfun) |
421 done |
421 done |
422 |
422 |
423 lemma deflation_convex_map: "deflation d \<Longrightarrow> deflation (convex_map\<cdot>d)" |
423 lemma deflation_convex_map: "deflation d \<Longrightarrow> deflation (convex_map\<cdot>d)" |
424 apply default |
424 apply standard |
425 apply (induct_tac x rule: convex_pd_induct, simp_all add: deflation.idem) |
425 apply (induct_tac x rule: convex_pd_induct, simp_all add: deflation.idem) |
426 apply (induct_tac x rule: convex_pd_induct) |
426 apply (induct_tac x rule: convex_pd_induct) |
427 apply (simp_all add: deflation.below monofun_cfun) |
427 apply (simp_all add: deflation.below monofun_cfun) |
428 done |
428 done |
429 |
429 |