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.5  
     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.16  
    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.22  
    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"
    1.27  by (fastforce simp add: map_le_def map_add_def dom_def)
    1.28  
    1.29 -lemma map_add_le_mapI: "\<lbrakk> f \<subseteq>\<^sub>m h; g \<subseteq>\<^sub>m h; f \<subseteq>\<^sub>m f++g \<rbrakk> \<Longrightarrow> f++g \<subseteq>\<^sub>m h"
    1.30 +lemma map_add_le_mapI: "\<lbrakk> f \<subseteq>\<^sub>m h; g \<subseteq>\<^sub>m h \<rbrakk> \<Longrightarrow> f++g \<subseteq>\<^sub>m h"
    1.31  by (clarsimp simp add: map_le_def map_add_def dom_def split: option.splits)
    1.32  
    1.33  lemma dom_eq_singleton_conv: "dom f = {x} \<longleftrightarrow> (\<exists>v. f = [x \<mapsto> v])"