Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
implement Mapping.map_entry
authorhaftmann
Thu, 20 May 2010 17:29:43 +0200
changeset 37027 98bfff1d159d
parent 37026 7e8979a155ae
child 37028 a6e0696d7110
implement Mapping.map_entry
src/HOL/Library/RBT.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/RBT.thy	Thu May 20 17:29:43 2010 +0200
+++ b/src/HOL/Library/RBT.thy	Thu May 20 17:29:43 2010 +0200
@@ -136,7 +136,7 @@
 
 lemma lookup_map_entry [simp]:
   "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
-  by (simp add: map_entry_def lookup_RBT lookup_map_entry lookup_impl_of)
+  by (simp add: map_entry_def lookup_RBT RBT_Impl.lookup_map_entry lookup_impl_of)
 
 lemma lookup_map [simp]:
   "lookup (map f t) k = Option.map (f k) (lookup t k)"
@@ -191,7 +191,11 @@
   by (rule mapping_eqI) simp
 
 lemma delete_Mapping [code]:
-  "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
+  "Mapping.delete k (Mapping t) = Mapping (delete k t)"
+  by (rule mapping_eqI) simp
+
+lemma map_entry_Mapping [code]:
+  "Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)"
   by (rule mapping_eqI) simp
 
 lemma keys_Mapping [code]:
isabelle