# HG changeset patch
# User nipkow
# Date 1529260311 -7200
# Node ID b047339bd11cc85e2bfa9ada31064934a6d9028b
# Parent 517aa9076fc93bd3fe27e5fb0299c1eb1b8a3a3c
added simp rules
diff -r 517aa9076fc9 -r b047339bd11c src/HOL/Map.thy
--- a/src/HOL/Map.thy Sun Jun 17 13:10:14 2018 +0200
+++ b/src/HOL/Map.thy Sun Jun 17 20:31:51 2018 +0200
@@ -133,6 +133,10 @@
by (induction xys) simp_all
qed simp
+lemma empty_eq_map_of_iff [simp]:
+ "empty = map_of xys \ xys = []"
+by(subst eq_commute) simp
+
lemma map_of_eq_None_iff:
"(map_of xys x = None) = (x \ fst ` (set xys))"
by (induct xys) simp_all
diff -r 517aa9076fc9 -r b047339bd11c src/HOL/Option.thy
--- a/src/HOL/Option.thy Sun Jun 17 13:10:14 2018 +0200
+++ b/src/HOL/Option.thy Sun Jun 17 20:31:51 2018 +0200
@@ -36,6 +36,9 @@
lemma not_Some_eq [iff]: "(\y. x \ Some y) \ x = None"
by (induct x) auto
+lemma comp_the_Some[simp]: "the o Some = id"
+by auto
+
text \Although it may appear that both of these equalities are helpful
only when applied to assumptions, in practice it seems better to give
them the uniform iff attribute.\