src/HOL/Library/RBT.thy
changeset 37027 98bfff1d159d
parent 36245 af5fe3a72087
child 37053 a89b47a94b19
     1.1 --- a/src/HOL/Library/RBT.thy	Thu May 20 17:29:43 2010 +0200
     1.2 +++ b/src/HOL/Library/RBT.thy	Thu May 20 17:29:43 2010 +0200
     1.3 @@ -136,7 +136,7 @@
     1.4  
     1.5  lemma lookup_map_entry [simp]:
     1.6    "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
     1.7 -  by (simp add: map_entry_def lookup_RBT lookup_map_entry lookup_impl_of)
     1.8 +  by (simp add: map_entry_def lookup_RBT RBT_Impl.lookup_map_entry lookup_impl_of)
     1.9  
    1.10  lemma lookup_map [simp]:
    1.11    "lookup (map f t) k = Option.map (f k) (lookup t k)"
    1.12 @@ -191,7 +191,11 @@
    1.13    by (rule mapping_eqI) simp
    1.14  
    1.15  lemma delete_Mapping [code]:
    1.16 -  "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
    1.17 +  "Mapping.delete k (Mapping t) = Mapping (delete k t)"
    1.18 +  by (rule mapping_eqI) simp
    1.19 +
    1.20 +lemma map_entry_Mapping [code]:
    1.21 +  "Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)"
    1.22    by (rule mapping_eqI) simp
    1.23  
    1.24  lemma keys_Mapping [code]: