src/HOL/Map.thy
changeset 68460 b047339bd11c
parent 68454 f35aa0e7255d
child 69593 3dda49e08b9d
equal deleted inserted replaced
68457:517aa9076fc9 68460:b047339bd11c
   130   "map_of xys = empty \<longleftrightarrow> xys = []"
   130   "map_of xys = empty \<longleftrightarrow> xys = []"
   131 proof
   131 proof
   132   show "map_of xys = empty \<Longrightarrow> xys = []"
   132   show "map_of xys = empty \<Longrightarrow> xys = []"
   133     by (induction xys) simp_all
   133     by (induction xys) simp_all
   134 qed simp
   134 qed simp
       
   135 
       
   136 lemma empty_eq_map_of_iff [simp]:
       
   137   "empty = map_of xys \<longleftrightarrow> xys = []"
       
   138 by(subst eq_commute) simp
   135 
   139 
   136 lemma map_of_eq_None_iff:
   140 lemma map_of_eq_None_iff:
   137   "(map_of xys x = None) = (x \<notin> fst ` (set xys))"
   141   "(map_of xys x = None) = (x \<notin> fst ` (set xys))"
   138 by (induct xys) simp_all
   142 by (induct xys) simp_all
   139 
   143