# HG changeset patch # User haftmann # Date 1226649008 -3600 # Node ID 2efba7b18c5b28d29913bce7d72f392795bcfe2d # Parent 5a404273ea8f7a37a3769d0507b384b45682ccd5 lemmas about dom and minus / insert diff -r 5a404273ea8f -r 2efba7b18c5b src/HOL/Map.thy --- a/src/HOL/Map.thy Fri Nov 14 08:50:07 2008 +0100 +++ b/src/HOL/Map.thy Fri Nov 14 08:50:08 2008 +0100 @@ -509,6 +509,15 @@ \x. f x = None" by(bestsimp dest:ex_new_if_finite) +lemma dom_minus: + "f x = None \ dom f - insert x A = dom f - A" + unfolding dom_def by simp + +lemma insert_dom: + "f x = Some y \ insert x (dom f) = dom f" + unfolding dom_def by auto + + subsection {* @{term [source] ran} *} lemma ranI: "m a = Some b ==> b : ran m"