equal
deleted
inserted
replaced
79 |
79 |
80 lemma map_map_upds [simp]: |
80 lemma map_map_upds [simp]: |
81 "(\<forall>y\<in>set ys. y \<notin> set xs) \<Longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) xs = map (the \<circ> f) xs" |
81 "(\<forall>y\<in>set ys. y \<notin> set xs) \<Longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) xs = map (the \<circ> f) xs" |
82 apply (induct xs arbitrary: f vs) |
82 apply (induct xs arbitrary: f vs) |
83 apply simp |
83 apply simp |
84 apply fastsimp |
84 apply fastforce |
85 done |
85 done |
86 |
86 |
87 lemma map_upds_distinct [simp]: |
87 lemma map_upds_distinct [simp]: |
88 "distinct ys \<Longrightarrow> length ys = length vs \<Longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) ys = vs" |
88 "distinct ys \<Longrightarrow> length ys = length vs \<Longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) ys = vs" |
89 apply (induct ys arbitrary: f vs) |
89 apply (induct ys arbitrary: f vs) |