# HG changeset patch
# User nipkow
# Date 1637161980 -3600
# Node ID b61bd2c12de33999811106ae82bbc042e71b4bd6
# Parent  189248f76ed89614559db28e23076bb7a696e526
added lemmas

diff -r 189248f76ed8 -r b61bd2c12de3 src/HOL/List.thy
--- 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"
diff -r 189248f76ed8 -r b61bd2c12de3 src/HOL/Map.thy
--- 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"