src/HOL/Product_Type.thy
changeset 41505 6d19301074cf
parent 41372 551eb49a6e91
child 41792 ff3cb0c418b7
equal deleted inserted replaced
41503:a7462e442e35 41505:6d19301074cf
   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: map_pair
   837 enriched_type map_pair: map_pair
   838   by (auto simp add: split_paired_all intro: ext)
   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