author bulwahn Sun Aug 27 06:56:29 2017 +0200 (22 months ago) changeset 66583 ac183ddc9fef parent 66582 2b49d4888cb8 child 66584 acb02fa48ef3
more facts on Map.ran
 src/HOL/Map.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Map.thy	Sun Aug 27 06:27:01 2017 +0200
1.2 +++ b/src/HOL/Map.thy	Sun Aug 27 06:56:29 2017 +0200
1.3 @@ -619,6 +619,33 @@
1.4   apply auto
1.5  done
1.6
1.8 +  assumes "dom m1 \<inter> dom m2 = {}"
1.9 +  shows "ran (m1 ++ m2) = ran m1 \<union> ran m2"
1.10 +proof
1.11 +  show "ran (m1 ++ m2) \<subseteq> ran m1 \<union> ran m2"
1.12 +    unfolding ran_def by auto
1.13 +next
1.14 +  show "ran m1 \<union> ran m2 \<subseteq> ran (m1 ++ m2)"
1.15 +  proof -
1.16 +    have "(m1 ++ m2) x = Some y" if "m1 x = Some y" for x y
1.17 +      using assms map_add_comm that by fastforce
1.18 +    moreover have "(m1 ++ m2) x = Some y" if "m2 x = Some y" for x y
1.19 +      using assms that by auto
1.20 +    ultimately show ?thesis
1.21 +      unfolding ran_def by blast
1.22 +  qed
1.23 +qed
1.24 +
1.25 +lemma finite_ran:
1.26 +  assumes "finite (dom p)"
1.27 +  shows "finite (ran p)"
1.28 +proof -
1.29 +  have "ran p = (\<lambda>x. the (p x)) ` dom p"
1.30 +    unfolding ran_def by force
1.31 +  from this \<open>finite (dom p)\<close> show ?thesis by auto
1.32 +qed
1.33 +
1.34  lemma ran_distinct:
1.35    assumes dist: "distinct (map fst al)"
1.36    shows "ran (map_of al) = snd ` set al"
```