equal
deleted
inserted
replaced
469 unfolding lower_join_def by simp |
469 unfolding lower_join_def by simp |
470 |
470 |
471 lemma lower_map_ident: "lower_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs" |
471 lemma lower_map_ident: "lower_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs" |
472 by (induct xs rule: lower_pd_induct, simp_all) |
472 by (induct xs rule: lower_pd_induct, simp_all) |
473 |
473 |
|
474 lemma lower_map_ID: "lower_map\<cdot>ID = ID" |
|
475 by (simp add: expand_cfun_eq ID_def lower_map_ident) |
|
476 |
474 lemma lower_map_map: |
477 lemma lower_map_map: |
475 "lower_map\<cdot>f\<cdot>(lower_map\<cdot>g\<cdot>xs) = lower_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs" |
478 "lower_map\<cdot>f\<cdot>(lower_map\<cdot>g\<cdot>xs) = lower_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs" |
476 by (induct xs rule: lower_pd_induct, simp_all) |
479 by (induct xs rule: lower_pd_induct, simp_all) |
477 |
480 |
478 lemma lower_join_map_unit: |
481 lemma lower_join_map_unit: |