src/HOL/Map.thy
changeset 14208 144f45277d5a
parent 14187 26dfcd0ac436
child 14300 bf8b8c9425c3
     1.1 --- a/src/HOL/Map.thy	Fri Sep 26 10:34:28 2003 +0200
     1.2 +++ b/src/HOL/Map.thy	Fri Sep 26 10:34:57 2003 +0200
     1.3 @@ -111,7 +111,7 @@
     1.4  
     1.5  lemma map_upd_nonempty[simp]: "t(k|->x) ~= empty"
     1.6  apply safe
     1.7 -apply (drule_tac x = "k" in fun_cong)
     1.8 +apply (drule_tac x = k in fun_cong)
     1.9  apply (simp (no_asm_use))
    1.10  done
    1.11  
    1.12 @@ -126,7 +126,7 @@
    1.13  apply (unfold image_def)
    1.14  apply (simp (no_asm_use) add: full_SetCompr_eq)
    1.15  apply (rule finite_subset)
    1.16 -prefer 2 apply (assumption)
    1.17 +prefer 2 apply assumption
    1.18  apply auto
    1.19  done
    1.20  
    1.21 @@ -156,22 +156,16 @@
    1.22  subsection {* @{term chg_map} *}
    1.23  
    1.24  lemma chg_map_new[simp]: "m a = None   ==> chg_map f a m = m"
    1.25 -apply (unfold chg_map_def)
    1.26 -apply auto
    1.27 -done
    1.28 +by (unfold chg_map_def, auto)
    1.29  
    1.30  lemma chg_map_upd[simp]: "m a = Some b ==> chg_map f a m = m(a|->f b)"
    1.31 -apply (unfold chg_map_def)
    1.32 -apply auto
    1.33 -done
    1.34 +by (unfold chg_map_def, auto)
    1.35  
    1.36  
    1.37  subsection {* @{term map_of} *}
    1.38  
    1.39  lemma map_of_SomeD [rule_format (no_asm)]: "map_of xs k = Some y --> (k,y):set xs"
    1.40 -apply (induct_tac "xs")
    1.41 -apply  auto
    1.42 -done
    1.43 +by (induct_tac "xs", auto)
    1.44  
    1.45  lemma map_of_mapk_SomeI [rule_format (no_asm)]: "inj f ==> map_of t k = Some x -->  
    1.46     map_of (map (split (%k. Pair (f k))) t) (f k) = Some x"
    1.47 @@ -180,31 +174,26 @@
    1.48  done
    1.49  
    1.50  lemma weak_map_of_SomeI [rule_format (no_asm)]: "(k, x) : set l --> (? x. map_of l k = Some x)"
    1.51 -apply (induct_tac "l")
    1.52 -apply  auto
    1.53 -done
    1.54 +by (induct_tac "l", auto)
    1.55  
    1.56  lemma map_of_filter_in: 
    1.57  "[| map_of xs k = Some z; P k z |] ==> map_of (filter (split P) xs) k = Some z"
    1.58  apply (rule mp)
    1.59 -prefer 2 apply (assumption)
    1.60 +prefer 2 apply assumption
    1.61  apply (erule thin_rl)
    1.62 -apply (induct_tac "xs")
    1.63 -apply  auto
    1.64 +apply (induct_tac "xs", auto)
    1.65  done
    1.66  
    1.67  lemma finite_range_map_of: "finite (range (map_of l))"
    1.68  apply (induct_tac "l")
    1.69  apply  (simp_all (no_asm) add: image_constant)
    1.70  apply (rule finite_subset)
    1.71 -prefer 2 apply (assumption)
    1.72 +prefer 2 apply assumption
    1.73  apply auto
    1.74  done
    1.75  
    1.76  lemma map_of_map: "map_of (map (%(a,b). (a,f b)) xs) x = option_map f (map_of xs x)"
    1.77 -apply (induct_tac "xs")
    1.78 -apply auto
    1.79 -done
    1.80 +by (induct_tac "xs", auto)
    1.81  
    1.82  
    1.83  subsection {* @{term option_map} related *}
    1.84 @@ -249,9 +238,7 @@
    1.85  declare map_add_SomeD [dest!]
    1.86  
    1.87  lemma map_add_find_right[simp]: "!!xx. n k = Some xx ==> (m ++ n) k = Some xx"
    1.88 -apply (subst map_add_Some_iff)
    1.89 -apply fast
    1.90 -done
    1.91 +by (subst map_add_Some_iff, fast)
    1.92  
    1.93  lemma map_add_None [iff]: "((m ++ n) k = None) = (n k = None & m k = None)"
    1.94  apply (unfold map_add_def)
    1.95 @@ -260,8 +247,7 @@
    1.96  
    1.97  lemma map_add_upd[simp]: "f ++ g(x|->y) = (f ++ g)(x|->y)"
    1.98  apply (unfold map_add_def)
    1.99 -apply (rule ext)
   1.100 -apply auto
   1.101 +apply (rule ext, auto)
   1.102  done
   1.103  
   1.104  lemma map_add_upds[simp]: "m1 ++ (m2(xs[\<mapsto>]ys)) = (m1++m2)(xs[\<mapsto>]ys)"
   1.105 @@ -278,8 +264,7 @@
   1.106  declare fun_upd_apply [simp del]
   1.107  lemma finite_range_map_of_map_add:
   1.108   "finite (range f) ==> finite (range (f ++ map_of l))"
   1.109 -apply (induct_tac "l")
   1.110 -apply  auto
   1.111 +apply (induct_tac "l", auto)
   1.112  apply (erule finite_range_updI)
   1.113  done
   1.114  declare fun_upd_apply [simp]
   1.115 @@ -351,18 +336,14 @@
   1.116    m(xs@[x] [\<mapsto>] ys) = m(xs [\<mapsto>] ys)(x \<mapsto> ys!size xs)"
   1.117  apply(induct xs)
   1.118   apply(clarsimp simp add:neq_Nil_conv)
   1.119 -apply(case_tac ys)
   1.120 - apply simp
   1.121 -apply simp
   1.122 +apply (case_tac ys, simp, simp)
   1.123  done
   1.124  
   1.125  lemma map_upds_list_update2_drop[simp]:
   1.126   "\<And>m ys i. \<lbrakk>size xs \<le> i; i < size ys\<rbrakk>
   1.127       \<Longrightarrow> m(xs[\<mapsto>]ys[i:=y]) = m(xs[\<mapsto>]ys)"
   1.128 -apply(induct xs)
   1.129 - apply simp
   1.130 -apply(case_tac ys)
   1.131 - apply simp
   1.132 +apply (induct xs, simp)
   1.133 +apply (case_tac ys, simp)
   1.134  apply(simp split:nat.split)
   1.135  done
   1.136  
   1.137 @@ -370,8 +351,7 @@
   1.138   (f(x|->y))(xs [|->] ys) =
   1.139   (if x : set(take (length ys) xs) then f(xs [|->] ys)
   1.140                                    else (f(xs [|->] ys))(x|->y))"
   1.141 -apply(induct xs)
   1.142 - apply simp
   1.143 +apply (induct xs, simp)
   1.144  apply(case_tac ys)
   1.145   apply(auto split:split_if simp:fun_upd_twist)
   1.146  done
   1.147 @@ -384,8 +364,7 @@
   1.148  
   1.149  lemma map_upds_apply_nontin[simp]:
   1.150   "!!ys. x ~: set xs ==> (f(xs[|->]ys)) x = f x"
   1.151 -apply(induct xs)
   1.152 - apply simp
   1.153 +apply (induct xs, simp)
   1.154  apply(case_tac ys)
   1.155   apply(auto simp: map_upd_upds_conv_if)
   1.156  done
   1.157 @@ -393,10 +372,8 @@
   1.158  lemma restrict_map_upds[simp]: "!!m ys.
   1.159   \<lbrakk> length xs = length ys; set xs \<subseteq> D \<rbrakk>
   1.160   \<Longrightarrow> m(xs [\<mapsto>] ys)\<lfloor>D = (m\<lfloor>(D - set xs))(xs [\<mapsto>] ys)"
   1.161 -apply(induct xs)
   1.162 - apply simp
   1.163 -apply(case_tac ys)
   1.164 - apply simp
   1.165 +apply (induct xs, simp)
   1.166 +apply (case_tac ys, simp)
   1.167  apply(simp add:Diff_insert[symmetric] insert_absorb)
   1.168  apply(simp add: map_upd_upds_conv_if)
   1.169  done
   1.170 @@ -415,20 +392,14 @@
   1.171  subsection {* @{term dom} *}
   1.172  
   1.173  lemma domI: "m a = Some b ==> a : dom m"
   1.174 -apply (unfold dom_def)
   1.175 -apply auto
   1.176 -done
   1.177 +by (unfold dom_def, auto)
   1.178  (* declare domI [intro]? *)
   1.179  
   1.180  lemma domD: "a : dom m ==> ? b. m a = Some b"
   1.181 -apply (unfold dom_def)
   1.182 -apply auto
   1.183 -done
   1.184 +by (unfold dom_def, auto)
   1.185  
   1.186  lemma domIff[iff]: "(a : dom m) = (m a ~= None)"
   1.187 -apply (unfold dom_def)
   1.188 -apply auto
   1.189 -done
   1.190 +by (unfold dom_def, auto)
   1.191  declare domIff [simp del]
   1.192  
   1.193  lemma dom_empty[simp]: "dom empty = {}"
   1.194 @@ -453,16 +424,12 @@
   1.195  
   1.196  lemma dom_map_upds[simp]:
   1.197   "!!m ys. dom(m(xs[|->]ys)) = set(take (length ys) xs) Un dom m"
   1.198 -apply(induct xs)
   1.199 - apply simp
   1.200 -apply(case_tac ys)
   1.201 - apply auto
   1.202 +apply (induct xs, simp)
   1.203 +apply (case_tac ys, auto)
   1.204  done
   1.205  
   1.206  lemma dom_map_add[simp]: "dom(m++n) = dom n Un dom m"
   1.207 -apply (unfold dom_def)
   1.208 -apply auto
   1.209 -done
   1.210 +by (unfold dom_def, auto)
   1.211  
   1.212  lemma dom_overwrite[simp]:
   1.213   "dom(f(g|A)) = (dom f  - {a. a : A - dom g}) Un {a. a : A Int dom g}"
   1.214 @@ -485,8 +452,7 @@
   1.215  done
   1.216  
   1.217  lemma ran_map_upd[simp]: "m a = None ==> ran(m(a|->b)) = insert b (ran m)"
   1.218 -apply (unfold ran_def)
   1.219 -apply auto
   1.220 +apply (unfold ran_def, auto)
   1.221  apply (subgoal_tac "~ (aa = a) ")
   1.222  apply auto
   1.223  done
   1.224 @@ -507,10 +473,8 @@
   1.225  
   1.226  lemma map_le_upds[simp]:
   1.227   "!!f g bs. f \<subseteq>\<^sub>m g ==> f(as [|->] bs) \<subseteq>\<^sub>m g(as [|->] bs)"
   1.228 -apply(induct as)
   1.229 - apply simp
   1.230 -apply(case_tac bs)
   1.231 - apply auto
   1.232 +apply (induct as, simp)
   1.233 +apply (case_tac bs, auto)
   1.234  done
   1.235  
   1.236  lemma map_le_implies_dom_le: "(f \<subseteq>\<^sub>m g) \<Longrightarrow> (dom f \<subseteq> dom g)"
   1.237 @@ -525,11 +489,8 @@
   1.238  lemma map_le_antisym: "\<lbrakk> f \<subseteq>\<^sub>m g; g \<subseteq>\<^sub>m f \<rbrakk> \<Longrightarrow> f = g"
   1.239    apply (unfold map_le_def)
   1.240    apply (rule ext)
   1.241 -  apply (case_tac "x \<in> dom f")
   1.242 -    apply simp
   1.243 -  apply (case_tac "x \<in> dom g")
   1.244 -    apply simp
   1.245 -  apply fastsimp
   1.246 +  apply (case_tac "x \<in> dom f", simp)
   1.247 +  apply (case_tac "x \<in> dom g", simp, fastsimp)
   1.248  done
   1.249  
   1.250  lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m (g ++ f)"