equal
deleted
inserted
replaced
98 |
98 |
99 lemma option_map_comp: |
99 lemma option_map_comp: |
100 "map f (map g opt) = map (f o g) opt" |
100 "map f (map g opt) = map (f o g) opt" |
101 by (simp add: map_def split add: option.split) |
101 by (simp add: map_def split add: option.split) |
102 |
102 |
103 lemma option_map_o_sum_case [simp]: |
103 lemma option_map_o_case_sum [simp]: |
104 "map f o sum_case g h = sum_case (map f o g) (map f o h)" |
104 "map f o case_sum g h = case_sum (map f o g) (map f o h)" |
105 by (rule ext) (simp split: sum.split) |
105 by (rule ext) (simp split: sum.split) |
106 |
106 |
107 lemma map_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> map f x = map g y" |
107 lemma map_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> map f x = map g y" |
108 by (cases x) auto |
108 by (cases x) auto |
109 |
109 |