src/HOL/Map.thy
 changeset 46588 4895d7f1be42 parent 44921 58eef4843641 child 53015 a1119cf551e8
1.1 --- a/src/HOL/Map.thy	Wed Feb 22 09:35:01 2012 +0100
1.2 +++ b/src/HOL/Map.thy	Wed Feb 22 12:30:01 2012 +0100
1.3 @@ -422,8 +422,7 @@
1.4  done
1.6  lemma map_upds_list_update2_drop [simp]:
1.7 -  "\<lbrakk>size xs \<le> i; i < size ys\<rbrakk>
1.8 -    \<Longrightarrow> m(xs[\<mapsto>]ys[i:=y]) = m(xs[\<mapsto>]ys)"
1.9 +  "size xs \<le> i \<Longrightarrow> m(xs[\<mapsto>]ys[i:=y]) = m(xs[\<mapsto>]ys)"
1.10  apply (induct xs arbitrary: m ys i)
1.11   apply simp
1.12  apply (case_tac ys)
1.13 @@ -512,9 +511,8 @@
1.14    "dom (map_of xys) = fst ` set xys"
1.15    by (induct xys) (auto simp add: dom_if)
1.17 -lemma dom_map_of_zip [simp]: "[| length xs = length ys; distinct xs |] ==>
1.18 -  dom(map_of(zip xs ys)) = set xs"
1.19 -by (induct rule: list_induct2) simp_all
1.20 +lemma dom_map_of_zip [simp]: "length xs = length ys ==> dom (map_of (zip xs ys)) = set xs"
1.21 +by (induct rule: list_induct2) (auto simp add: dom_if)
1.23  lemma finite_dom_map_of: "finite (dom (map_of l))"
1.24  by (induct l) (auto simp add: dom_def insert_Collect [symmetric])
1.25 @@ -669,7 +667,7 @@
1.26  lemma map_add_le_mapE: "f++g \<subseteq>\<^sub>m h \<Longrightarrow> g \<subseteq>\<^sub>m h"