lemmas dom_const, dom_if
authorhaftmann
Fri Jan 23 19:51:48 2009 +0100 (2009-01-23)
changeset 296222eeb09477ed3
parent 29619 82054da94a74
child 29623 1219985d24b5
lemmas dom_const, dom_if
src/HOL/Map.thy
     1.1 --- a/src/HOL/Map.thy	Fri Jan 23 10:21:48 2009 +0100
     1.2 +++ b/src/HOL/Map.thy	Fri Jan 23 19:51:48 2009 +0100
     1.3 @@ -503,6 +503,15 @@
     1.4  lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
     1.5  by (rule ext) (force simp: map_add_def dom_def split: option.split)
     1.6  
     1.7 +lemma dom_const [simp]:
     1.8 +  "dom (\<lambda>x. Some y) = UNIV"
     1.9 +  by auto
    1.10 +
    1.11 +lemma dom_if:
    1.12 +  "dom (\<lambda>x. if P x then f x else g x) = dom f \<inter> {x. P x} \<union> dom g \<inter> {x. \<not> P x}"
    1.13 +  by (auto split: if_splits)
    1.14 +
    1.15 +
    1.16  (* Due to John Matthews - could be rephrased with dom *)
    1.17  lemma finite_map_freshness:
    1.18    "finite (dom (f :: 'a \<rightharpoonup> 'b)) \<Longrightarrow> \<not> finite (UNIV :: 'a set) \<Longrightarrow>