# HG changeset patch
# User bulwahn
# Date 1503809789 -7200
# Node ID ac183ddc9fefec52b801e125d6a2ebbe5a2e96a7
# Parent  2b49d4888cb8d4bc54f1f1458eafb9262ada3673
more facts on Map.ran

diff -r 2b49d4888cb8 -r ac183ddc9fef src/HOL/Map.thy
--- a/src/HOL/Map.thy	Sun Aug 27 06:27:01 2017 +0200
+++ b/src/HOL/Map.thy	Sun Aug 27 06:56:29 2017 +0200
@@ -619,6 +619,33 @@
  apply auto
 done
 
+lemma ran_map_add:
+  assumes "dom m1 \<inter> dom m2 = {}"
+  shows "ran (m1 ++ m2) = ran m1 \<union> ran m2"
+proof
+  show "ran (m1 ++ m2) \<subseteq> ran m1 \<union> ran m2"
+    unfolding ran_def by auto
+next
+  show "ran m1 \<union> ran m2 \<subseteq> ran (m1 ++ m2)"
+  proof -
+    have "(m1 ++ m2) x = Some y" if "m1 x = Some y" for x y
+      using assms map_add_comm that by fastforce
+    moreover have "(m1 ++ m2) x = Some y" if "m2 x = Some y" for x y
+      using assms that by auto
+    ultimately show ?thesis
+      unfolding ran_def by blast
+  qed
+qed
+
+lemma finite_ran:
+  assumes "finite (dom p)"
+  shows "finite (ran p)"
+proof -
+  have "ran p = (\<lambda>x. the (p x)) ` dom p"
+    unfolding ran_def by force
+  from this \<open>finite (dom p)\<close> show ?thesis by auto
+qed
+
 lemma ran_distinct:
   assumes dist: "distinct (map fst al)"
   shows "ran (map_of al) = snd ` set al"