src/HOL/Map.thy
changeset 29622 2eeb09477ed3
parent 28790 2efba7b18c5b
child 30235 58d147683393
     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>