--- a/src/HOL/List.thy Tue Nov 16 21:53:09 2021 +0100
+++ b/src/HOL/List.thy Wed Nov 17 16:13:00 2021 +0100
@@ -4238,6 +4238,8 @@
case (Cons x xs) thus ?case by (fastforce split: if_splits)
qed
+lemmas find_None_iff2 = find_None_iff[THEN eq_iff_swap]
+
lemma find_Some_iff:
"List.find P xs = Some x \<longleftrightarrow>
(\<exists>i<length xs. P (xs!i) \<and> x = xs!i \<and> (\<forall>j<i. \<not> P (xs!j)))"
@@ -4249,6 +4251,8 @@
using diff_Suc_1[unfolded One_nat_def] less_Suc_eq_0_disj by fastforce
qed
+lemmas find_Some_iff2 = find_Some_iff[THEN eq_iff_swap]
+
lemma find_cong[fundef_cong]:
assumes "xs = ys" and "\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x"
shows "List.find P xs = List.find Q ys"
--- 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"