more facts on Map.ran
authorbulwahn
Sun Aug 27 06:56:29 2017 +0200 (20 months ago)
changeset 66583ac183ddc9fef
parent 66582 2b49d4888cb8
child 66584 acb02fa48ef3
more facts on Map.ran
src/HOL/Map.thy
     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.7 +lemma ran_map_add:
     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"