equal
deleted
inserted
replaced
106 \<Longrightarrow> k \<in> (set (xs @ map fst m))" |
106 \<Longrightarrow> k \<in> (set (xs @ map fst m))" |
107 by (auto dest: map_upds_SomeD map_of_SomeD fst_in_set_lemma) |
107 by (auto dest: map_upds_SomeD map_of_SomeD fst_in_set_lemma) |
108 |
108 |
109 lemma map_of_map_prop: |
109 lemma map_of_map_prop: |
110 "\<lbrakk>map_of (map f xs) k = Some v; \<forall>x \<in> set xs. P1 x; \<forall>x. P1 x \<longrightarrow> P2 (f x)\<rbrakk> \<Longrightarrow> P2 (k, v)" |
110 "\<lbrakk>map_of (map f xs) k = Some v; \<forall>x \<in> set xs. P1 x; \<forall>x. P1 x \<longrightarrow> P2 (f x)\<rbrakk> \<Longrightarrow> P2 (k, v)" |
111 by (induct xs) (auto split: split_if_asm) |
111 by (induct xs) (auto split: if_split_asm) |
112 |
112 |
113 lemma map_of_map2: "\<forall>x \<in> set xs. (fst (f x)) = (fst x) \<Longrightarrow> |
113 lemma map_of_map2: "\<forall>x \<in> set xs. (fst (f x)) = (fst x) \<Longrightarrow> |
114 map_of (map f xs) a = map_option (\<lambda> b. (snd (f (a, b)))) (map_of xs a)" |
114 map_of (map f xs) a = map_option (\<lambda> b. (snd (f (a, b)))) (map_of xs a)" |
115 by (induct xs, auto) |
115 by (induct xs, auto) |
116 |
116 |