src/HOL/Map.thy
changeset 17724 e969fc0a4925
parent 17399 56a3a4affedc
child 17782 b3846df9d643
     1.1 --- a/src/HOL/Map.thy	Thu Sep 29 15:50:46 2005 +0200
     1.2 +++ b/src/HOL/Map.thy	Thu Sep 29 17:02:57 2005 +0200
     1.3 @@ -202,7 +202,7 @@
     1.4   "distinct(map fst xys) \<Longrightarrow> (Some y = map_of xys x) = ((x,y) \<in> set xys)"
     1.5  by(auto simp del:map_of_eq_Some_iff simp add:map_of_eq_Some_iff[symmetric])
     1.6  
     1.7 -lemma [simp]: "\<lbrakk> distinct(map fst xys); (x,y) \<in> set xys \<rbrakk>
     1.8 +lemma map_of_is_SomeI [simp]: "\<lbrakk> distinct(map fst xys); (x,y) \<in> set xys \<rbrakk>
     1.9    \<Longrightarrow> map_of xys x = Some y"
    1.10  apply (induct xys)
    1.11   apply simp
    1.12 @@ -553,13 +553,13 @@
    1.13  lemma map_le_empty [simp]: "empty \<subseteq>\<^sub>m g"
    1.14  by(simp add:map_le_def)
    1.15  
    1.16 -lemma [simp]: "f(x := None) \<subseteq>\<^sub>m f"
    1.17 +lemma upd_None_map_le [simp]: "f(x := None) \<subseteq>\<^sub>m f"
    1.18  by(force simp add:map_le_def)
    1.19  
    1.20  lemma map_le_upd[simp]: "f \<subseteq>\<^sub>m g ==> f(a := b) \<subseteq>\<^sub>m g(a := b)"
    1.21  by(fastsimp simp add:map_le_def)
    1.22  
    1.23 -lemma [simp]: "m1 \<subseteq>\<^sub>m m2 \<Longrightarrow> m1(x := None) \<subseteq>\<^sub>m m2(x \<mapsto> y)"
    1.24 +lemma map_le_imp_upd_le [simp]: "m1 \<subseteq>\<^sub>m m2 \<Longrightarrow> m1(x := None) \<subseteq>\<^sub>m m2(x \<mapsto> y)"
    1.25  by(force simp add:map_le_def)
    1.26  
    1.27  lemma map_le_upds[simp]: