--- a/src/HOL/Map.thy Tue Nov 16 21:53:09 2021 +0100
+++ b/src/HOL/Map.thy Wed Nov 17 16:13:00 2021 +0100
@@ -667,6 +667,10 @@
lemma fun_upd_None_if_notin_dom[simp]: "k \<notin> dom m \<Longrightarrow> m(k := None) = m"
by auto
+lemma ran_map_upd_Some:
+ "\<lbrakk> m x = Some y; inj_on m (dom m); z \<notin> ran m \<rbrakk> \<Longrightarrow> ran(m(x := Some z)) = ran m - {y} \<union> {z}"
+by(force simp add: ran_def domI inj_onD)
+
lemma ran_map_add:
assumes "dom m1 \<inter> dom m2 = {}"
shows "ran (m1 ++ m2) = ran m1 \<union> ran m2"