equal
deleted
inserted
replaced
793 |
793 |
794 lemma eval_map [simp]: |
794 lemma eval_map [simp]: |
795 "eval (map f P) = image f (eval P)" |
795 "eval (map f P) = image f (eval P)" |
796 by (auto simp add: map_def) |
796 by (auto simp add: map_def) |
797 |
797 |
798 type_lifting map |
798 type_lifting map: map |
799 by (auto intro!: pred_eqI simp add: image_image) |
799 by (auto intro!: pred_eqI simp add: fun_eq_iff image_compose) |
800 |
800 |
801 |
801 |
802 subsubsection {* Implementation *} |
802 subsubsection {* Implementation *} |
803 |
803 |
804 datatype 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq" |
804 datatype 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq" |