src/HOL/Map.thy
changeset 28790 2efba7b18c5b
parent 28562 4e74209f113e
child 29622 2eeb09477ed3
     1.1 --- a/src/HOL/Map.thy	Fri Nov 14 08:50:07 2008 +0100
     1.2 +++ b/src/HOL/Map.thy	Fri Nov 14 08:50:08 2008 +0100
     1.3 @@ -509,6 +509,15 @@
     1.4     \<exists>x. f x = None"
     1.5  by(bestsimp dest:ex_new_if_finite)
     1.6  
     1.7 +lemma dom_minus:
     1.8 +  "f x = None \<Longrightarrow> dom f - insert x A = dom f - A"
     1.9 +  unfolding dom_def by simp
    1.10 +
    1.11 +lemma insert_dom:
    1.12 +  "f x = Some y \<Longrightarrow> insert x (dom f) = dom f"
    1.13 +  unfolding dom_def by auto
    1.14 +
    1.15 +
    1.16  subsection {* @{term [source] ran} *}
    1.17  
    1.18  lemma ranI: "m a = Some b ==> b : ran m"