renamed map_of to lookup
authornipkow
Sun Jan 17 17:56:33 2016 +0100 (2016-01-17)
changeset 6219666fb3d1767f2
parent 62195 799a5306e2ed
child 62197 f354900ac0ea
renamed map_of to lookup
src/HOL/Data_Structures/Map_by_Ordered.thy
     1.1 --- a/src/HOL/Data_Structures/Map_by_Ordered.thy	Sun Jan 17 00:14:45 2016 +0100
     1.2 +++ b/src/HOL/Data_Structures/Map_by_Ordered.thy	Sun Jan 17 17:56:33 2016 +0100
     1.3 @@ -10,11 +10,11 @@
     1.4  fixes empty :: "'m"
     1.5  fixes update :: "'a \<Rightarrow> 'b \<Rightarrow> 'm \<Rightarrow> 'm"
     1.6  fixes delete :: "'a \<Rightarrow> 'm \<Rightarrow> 'm"
     1.7 -fixes map_of :: "'m \<Rightarrow> 'a \<Rightarrow> 'b option"
     1.8 +fixes lookup :: "'m \<Rightarrow> 'a \<Rightarrow> 'b option"
     1.9  fixes invar :: "'m \<Rightarrow> bool"
    1.10 -assumes map_empty: "map_of empty = (\<lambda>_. None)"
    1.11 -and map_update: "invar m \<Longrightarrow> map_of(update a b m) = (map_of m)(a := Some b)"
    1.12 -and map_delete: "invar m \<Longrightarrow> map_of(delete a m) = (map_of m)(a := None)"
    1.13 +assumes map_empty: "lookup empty = (\<lambda>_. None)"
    1.14 +and map_update: "invar m \<Longrightarrow> lookup(update a b m) = (lookup m)(a := Some b)"
    1.15 +and map_delete: "invar m \<Longrightarrow> lookup(delete a m) = (lookup m)(a := None)"
    1.16  and invar_empty: "invar empty"
    1.17  and invar_update: "invar m \<Longrightarrow> invar(update a b m)"
    1.18  and invar_delete: "invar m \<Longrightarrow> invar(delete a m)"