equal
deleted
inserted
replaced
79 apply (induct xs) |
79 apply (induct xs) |
80 apply simp |
80 apply simp |
81 apply (rule allI) |
81 apply (rule allI) |
82 apply (drule_tac x="a # ys" in spec) |
82 apply (drule_tac x="a # ys" in spec) |
83 apply (simp only: rev.simps append_assoc append_Cons append_Nil |
83 apply (simp only: rev.simps append_assoc append_Cons append_Nil |
84 map.simps map_of.simps map_upds.simps hd.simps tl.simps) |
84 map.simps map_of.simps map_upds_Cons hd.simps tl.simps) |
85 done |
85 done |
86 |
86 |
87 lemma map_of_as_map_upds: "map_of (rev xs) = empty ((map fst xs) [\<mapsto>] (map snd xs))" |
87 lemma map_of_as_map_upds: "map_of (rev xs) = empty ((map fst xs) [\<mapsto>] (map snd xs))" |
88 by (rule map_of_append [of _ "[]", simplified]) |
88 by (rule map_of_append [of _ "[]", simplified]) |
89 |
89 |
90 lemma map_of_rev: "unique xs \<Longrightarrow> map_of (rev xs) = map_of xs" |
90 lemma map_of_rev: "unique xs \<Longrightarrow> map_of (rev xs) = map_of xs" |
91 apply (induct xs) |
91 apply (induct xs) |
92 apply simp |
92 apply simp |
93 apply (simp add: unique_def map_of_append map_of_as_map_upds [THEN sym]) |
93 apply (simp add: unique_def map_of_append map_of_as_map_upds [THEN sym] |
|
94 Map.map_of_append[symmetric] del:Map.map_of_append) |
94 done |
95 done |
95 |
96 |
96 lemma map_upds_rev [rule_format]: "\<forall> xs. (distinct ks \<longrightarrow> length ks = length xs |
97 lemma map_upds_rev [rule_format]: "\<forall> xs. (distinct ks \<longrightarrow> length ks = length xs |
97 \<longrightarrow> m (rev ks [\<mapsto>] rev xs) = m (ks [\<mapsto>] xs))" |
98 \<longrightarrow> m (rev ks [\<mapsto>] rev xs) = m (ks [\<mapsto>] xs))" |
98 apply (induct ks) |
99 apply (induct ks) |