# HG changeset patch
# User nipkow
# Date 1529125997 -7200
# Node ID f35aa0e7255d3629915073ce885a376824bda65d
# Parent  febbf8f2881d0e8cc83081a5eec2aa340cf49bff
moved lemmas from AFP

diff -r febbf8f2881d -r f35aa0e7255d src/HOL/Map.thy
--- a/src/HOL/Map.thy	Fri Jun 15 13:52:05 2018 +0100
+++ b/src/HOL/Map.thy	Sat Jun 16 07:13:17 2018 +0200
@@ -126,6 +126,13 @@
 
 subsection \<open>@{term [source] map_of}\<close>
 
+lemma map_of_eq_empty_iff [simp]:
+  "map_of xys = empty \<longleftrightarrow> xys = []"
+proof
+  show "map_of xys = empty \<Longrightarrow> xys = []"
+    by (induction xys) simp_all
+qed simp
+
 lemma map_of_eq_None_iff:
   "(map_of xys x = None) = (x \<notin> fst ` (set xys))"
 by (induct xys) simp_all
@@ -761,6 +768,14 @@
   qed
 qed
 
+lemma map_add_eq_empty_iff[simp]:
+  "(f++g = empty) \<longleftrightarrow> f = empty \<and> g = empty"
+by (metis map_add_None)
+
+lemma empty_eq_map_add_iff[simp]:
+  "(empty = f++g) \<longleftrightarrow> f = empty \<and> g = empty"
+by(subst map_add_eq_empty_iff[symmetric])(rule eq_commute)
+
 
 subsection \<open>Various\<close>