# HG changeset patch
# User kuncar
# Date 1350938834 -7200
# Node ID e84baadd4963aa97214a2aee8d563c4fe448509f
# Parent  f11f8905d9fddc96c1d4b86e93f84b73deb179f0
new theorems

diff -r f11f8905d9fd -r e84baadd4963 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Mon Oct 22 22:24:34 2012 +0200
+++ b/src/HOL/Library/Mapping.thy	Mon Oct 22 22:47:14 2012 +0200
@@ -71,6 +71,15 @@
 
 subsection {* Properties *}
 
+lemma lookup_update: "lookup (update k v m) k = Some v" 
+  by transfer simp
+
+lemma lookup_update_neq: "k \<noteq> k' \<Longrightarrow> lookup (update k v m) k' = lookup m k'" 
+  by transfer simp
+
+lemma lookup_empty: "lookup empty k = None" 
+  by transfer simp
+
 lemma keys_is_none_rep [code_unfold]:
   "k \<in> keys m \<longleftrightarrow> \<not> (Option.is_none (lookup m k))"
   by transfer (auto simp add: is_none_def)