equal
deleted
inserted
replaced
493 unfolding convex_join_def by simp |
493 unfolding convex_join_def by simp |
494 |
494 |
495 lemma convex_map_ident: "convex_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs" |
495 lemma convex_map_ident: "convex_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs" |
496 by (induct xs rule: convex_pd_induct, simp_all) |
496 by (induct xs rule: convex_pd_induct, simp_all) |
497 |
497 |
|
498 lemma convex_map_ID: "convex_map\<cdot>ID = ID" |
|
499 by (simp add: expand_cfun_eq ID_def convex_map_ident) |
|
500 |
498 lemma convex_map_map: |
501 lemma convex_map_map: |
499 "convex_map\<cdot>f\<cdot>(convex_map\<cdot>g\<cdot>xs) = convex_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs" |
502 "convex_map\<cdot>f\<cdot>(convex_map\<cdot>g\<cdot>xs) = convex_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs" |
500 by (induct xs rule: convex_pd_induct, simp_all) |
503 by (induct xs rule: convex_pd_induct, simp_all) |
501 |
504 |
502 lemma convex_join_map_unit: |
505 lemma convex_join_map_unit: |