equal
deleted
inserted
replaced
832 |
832 |
833 lemma map_pair_simp [simp, code]: |
833 lemma map_pair_simp [simp, code]: |
834 "map_pair f g (a, b) = (f a, g b)" |
834 "map_pair f g (a, b) = (f a, g b)" |
835 by (simp add: map_pair_def) |
835 by (simp add: map_pair_def) |
836 |
836 |
837 type_lifting map_pair |
837 type_lifting map_pair: map_pair |
838 by (simp_all add: split_paired_all) |
838 by (auto simp add: split_paired_all intro: ext) |
839 |
839 |
840 lemma fst_map_pair [simp]: |
840 lemma fst_map_pair [simp]: |
841 "fst (map_pair f g x) = f (fst x)" |
841 "fst (map_pair f g x) = f (fst x)" |
842 by (cases x) simp_all |
842 by (cases x) simp_all |
843 |
843 |