src/HOL/Map.thy
changeset 60841 144523e0678e
parent 60839 422ec7a3c18a
child 61032 b57df8eecad6
     1.1 --- a/src/HOL/Map.thy	Tue Aug 04 15:00:58 2015 +0200
     1.2 +++ b/src/HOL/Map.thy	Tue Aug 04 23:11:16 2015 +0200
     1.3 @@ -137,12 +137,6 @@
     1.4    "(map_of xys x = None) = (x \<notin> fst ` (set xys))"
     1.5  by (induct xys) simp_all
     1.6  
     1.7 -lemma map_of_is_SomeD: "map_of xys x = Some y \<Longrightarrow> (x,y) \<in> set xys"
     1.8 -apply (induct xys)
     1.9 - apply simp
    1.10 -apply (clarsimp split: if_splits)
    1.11 -done
    1.12 -
    1.13  lemma map_of_eq_Some_iff [simp]:
    1.14    "distinct(map fst xys) \<Longrightarrow> (map_of xys x = Some y) = ((x,y) \<in> set xys)"
    1.15  apply (induct xys)
    1.16 @@ -229,7 +223,7 @@
    1.17  done
    1.18  
    1.19  lemma map_of_SomeD: "map_of xs k = Some y \<Longrightarrow> (k, y) \<in> set xs"
    1.20 -by (induct xs) (simp, atomize (full), auto)
    1.21 +  by (induct xs) (auto split: if_splits)
    1.22  
    1.23  lemma map_of_mapk_SomeI:
    1.24    "inj f \<Longrightarrow> map_of t k = Some x \<Longrightarrow>