equal
deleted
inserted
replaced
124 (\<forall> x. (P1 x) \<longrightarrow> (P2 (f x))) \<longrightarrow> |
124 (\<forall> x. (P1 x) \<longrightarrow> (P2 (f x))) \<longrightarrow> |
125 (P2(k, v))" |
125 (P2(k, v))" |
126 by (induct xs,auto) |
126 by (induct xs,auto) |
127 |
127 |
128 lemma map_of_map2: "\<forall> x \<in> set xs. (fst (f x)) = (fst x) \<Longrightarrow> |
128 lemma map_of_map2: "\<forall> x \<in> set xs. (fst (f x)) = (fst x) \<Longrightarrow> |
129 map_of (map f xs) a = option_map (\<lambda> b. (snd (f (a, b)))) (map_of xs a)" |
129 map_of (map f xs) a = Option.map (\<lambda> b. (snd (f (a, b)))) (map_of xs a)" |
130 by (induct xs, auto) |
130 by (induct xs, auto) |
131 |
131 |
132 lemma option_map_of [simp]: "(option_map f (map_of xs k) = None) = ((map_of xs k) = None)" |
132 lemma option_map_of [simp]: "(Option.map f (map_of xs k) = None) = ((map_of xs k) = None)" |
133 by (simp add: option_map_def split: option.split) |
133 by (simp add: Option.map_def split: option.split) |
134 |
134 |
135 |
135 |
136 |
136 |
137 end |
137 end |