lemmas about dom and minus / insert
authorhaftmann
Fri Nov 14 08:50:08 2008 +0100 (2008-11-14)
changeset 287902efba7b18c5b
parent 28789 5a404273ea8f
child 28791 cc16be808796
lemmas about dom and minus / insert
src/HOL/Map.thy
     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"