src/HOL/Map.ML
changeset 13908 4bdfa9f77254
parent 13907 2bc462b99e70
child 13909 a5247a49c85e
     1.1 --- a/src/HOL/Map.ML	Wed Apr 09 12:52:45 2003 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,267 +0,0 @@
     1.4 -(*  Title:      HOL/Map.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Tobias Nipkow
     1.7 -    Copyright   1997 TU Muenchen
     1.8 -
     1.9 -Map lemmas.
    1.10 -*)
    1.11 -
    1.12 -section "empty";
    1.13 -
    1.14 -Goal "empty(x := None) = empty";
    1.15 -by (rtac ext 1);
    1.16 -by (Simp_tac 1);
    1.17 -qed "empty_upd_none";
    1.18 -Addsimps [empty_upd_none];
    1.19 -
    1.20 -(* FIXME: what is this sum_case nonsense?? *)
    1.21 -Goal "sum_case empty empty = empty";
    1.22 -by (rtac ext 1);
    1.23 -by (simp_tac (simpset() addsplits [sum.split]) 1);
    1.24 -qed "sum_case_empty_empty";
    1.25 -Addsimps [sum_case_empty_empty];
    1.26 -
    1.27 -
    1.28 -section "map_upd";
    1.29 -
    1.30 -Goal "t k = Some x ==> t(k|->x) = t";
    1.31 -by (rtac ext 1);
    1.32 -by (Asm_simp_tac 1);
    1.33 -qed "map_upd_triv";
    1.34 -
    1.35 -Goal "t(k|->x) ~= empty";
    1.36 -by Safe_tac;
    1.37 -by (dres_inst_tac [("x","k")] fun_cong 1);
    1.38 -by (Full_simp_tac 1);
    1.39 -qed "map_upd_nonempty";
    1.40 -Addsimps[map_upd_nonempty];
    1.41 -
    1.42 -Goalw [image_def] "finite (range f) ==> finite (range (f(a|->b)))";
    1.43 -by (full_simp_tac (simpset() addsimps [full_SetCompr_eq]) 1);
    1.44 -by (rtac finite_subset 1);
    1.45 -by (assume_tac 2);
    1.46 -by Auto_tac;
    1.47 -qed "finite_range_updI";
    1.48 -
    1.49 -
    1.50 -(* FIXME: what is this sum_case nonsense?? *)
    1.51 -section "sum_case and empty/map_upd";
    1.52 -
    1.53 -Goal "sum_case (m(k|->y)) empty =  (sum_case m empty)(Inl k|->y)";
    1.54 -by (rtac ext 1);
    1.55 -by (simp_tac (simpset() addsplits [sum.split]) 1);
    1.56 -qed "sum_case_map_upd_empty";
    1.57 -Addsimps[sum_case_map_upd_empty];
    1.58 -
    1.59 -Goal "sum_case empty (m(k|->y)) =  (sum_case empty m)(Inr k|->y)";
    1.60 -by (rtac ext 1);
    1.61 -by (simp_tac (simpset() addsplits [sum.split]) 1);
    1.62 -qed "sum_case_empty_map_upd";
    1.63 -Addsimps[sum_case_empty_map_upd];
    1.64 -
    1.65 -Goal "sum_case (m1(k1|->y1)) (m2(k2|->y2)) = (sum_case (m1(k1|->y1)) m2)(Inr k2|->y2)";
    1.66 -by (rtac ext 1);
    1.67 -by (simp_tac (simpset() addsplits [sum.split]) 1);
    1.68 -qed "sum_case_map_upd_map_upd";
    1.69 -Addsimps[sum_case_map_upd_map_upd];
    1.70 -
    1.71 -
    1.72 -section "map_upds";
    1.73 -
    1.74 -Goal "a ~: set as --> (!m bs. (m(a|->b)(as[|->]bs)) = (m(as[|->]bs)(a|->b)))";
    1.75 -by (induct_tac "as" 1);
    1.76 -by  (auto_tac (claset(), simpset() delsimps[fun_upd_apply]));
    1.77 -by (REPEAT(dtac spec 1));
    1.78 -by (rotate_tac ~1 1);
    1.79 -by (etac subst 1);
    1.80 -by (etac (fun_upd_twist RS subst) 1);
    1.81 -by (rtac refl 1);
    1.82 -qed_spec_mp "map_upds_twist";
    1.83 -Addsimps [map_upds_twist];
    1.84 -
    1.85 -
    1.86 -section "chg_map";
    1.87 -
    1.88 -Goalw [chg_map_def] "m a = None   ==> chg_map f a m = m";
    1.89 -by Auto_tac;
    1.90 -qed "chg_map_new";
    1.91 -
    1.92 -Goalw [chg_map_def] "m a = Some b ==> chg_map f a m = m(a|->f b)";
    1.93 -by Auto_tac;
    1.94 -qed "chg_map_upd";
    1.95 -
    1.96 -Addsimps[chg_map_new, chg_map_upd];
    1.97 -
    1.98 -
    1.99 -section "map_of";
   1.100 -
   1.101 -Goal "map_of xs k = Some y --> (k,y):set xs";
   1.102 -by (induct_tac "xs" 1);
   1.103 -by  Auto_tac;
   1.104 -qed_spec_mp "map_of_SomeD";
   1.105 -
   1.106 -Goal "inj f ==> map_of t k = Some x --> \
   1.107 -\  map_of (map (split (%k. Pair (f k))) t) (f k) = Some x";
   1.108 -by (induct_tac "t" 1);
   1.109 -by  (auto_tac (claset(),simpset()addsimps[inj_eq]));
   1.110 -qed_spec_mp "map_of_mapk_SomeI";
   1.111 -
   1.112 -Goal "(k, x) : set l --> (? x. map_of l k = Some x)";
   1.113 -by (induct_tac "l" 1);
   1.114 -by  Auto_tac;
   1.115 -qed_spec_mp "weak_map_of_SomeI";
   1.116 -
   1.117 -Goal 
   1.118 -"[| map_of xs k = Some z; P k z |] ==> map_of (filter (split P) xs) k = Some z";
   1.119 -by (rtac mp 1);
   1.120 -by (atac 2);
   1.121 -by (etac thin_rl 1);
   1.122 -by (induct_tac "xs" 1);
   1.123 -by  Auto_tac;
   1.124 -qed "map_of_filter_in";
   1.125 -
   1.126 -Goal "finite (range (map_of l))";
   1.127 -by (induct_tac "l" 1);
   1.128 -by  (ALLGOALS (simp_tac (simpset() addsimps [image_constant])));
   1.129 -by (rtac finite_subset 1);
   1.130 -by (assume_tac 2);
   1.131 -by Auto_tac;
   1.132 -qed "finite_range_map_of";
   1.133 -
   1.134 -Goal "map_of (map (%(a,b). (a,f b)) xs) x = option_map f (map_of xs x)";
   1.135 -by (induct_tac "xs" 1);
   1.136 -by Auto_tac;
   1.137 -qed "map_of_map";
   1.138 -
   1.139 -
   1.140 -section "option_map related";
   1.141 -
   1.142 -Goal "option_map f o empty = empty";
   1.143 -by (rtac ext 1);
   1.144 -by (Simp_tac 1);
   1.145 -qed "option_map_o_empty";
   1.146 -
   1.147 -Goal "option_map f o m(a|->b) = (option_map f o m)(a|->f b)";
   1.148 -by (rtac ext 1);
   1.149 -by (Simp_tac 1);
   1.150 -qed "option_map_o_map_upd";
   1.151 -
   1.152 -Addsimps[option_map_o_empty, option_map_o_map_upd];
   1.153 -
   1.154 -
   1.155 -section "++";
   1.156 -
   1.157 -Goalw [override_def] "m ++ empty = m";
   1.158 -by (Simp_tac 1);
   1.159 -qed "override_empty";
   1.160 -Addsimps [override_empty];
   1.161 -
   1.162 -Goalw [override_def] "empty ++ m = m";
   1.163 -by (Simp_tac 1);
   1.164 -by (rtac ext 1);
   1.165 -by (split_tac [option.split] 1);
   1.166 -by (Simp_tac 1);
   1.167 -qed "empty_override";
   1.168 -Addsimps [empty_override];
   1.169 -
   1.170 -Goalw [override_def]
   1.171 - "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)";
   1.172 -by (simp_tac (simpset() addsplits [option.split]) 1);
   1.173 -qed_spec_mp "override_Some_iff";
   1.174 -
   1.175 -bind_thm ("override_SomeD", standard(override_Some_iff RS iffD1));
   1.176 -AddSDs[override_SomeD];
   1.177 -
   1.178 -Goal "!!xx. n k = Some xx ==> (m ++ n) k = Some xx";
   1.179 -by (stac override_Some_iff 1);
   1.180 -by (Fast_tac 1);
   1.181 -qed "override_find_right";
   1.182 -Addsimps[override_find_right];
   1.183 -
   1.184 -Goalw [override_def] "((m ++ n) k = None) = (n k = None & m k = None)";
   1.185 -by (simp_tac (simpset() addsplits [option.split]) 1);
   1.186 -qed "override_None";
   1.187 -AddIffs [override_None];
   1.188 -
   1.189 -Goalw [override_def] "f ++ g(x|->y) = (f ++ g)(x|->y)";
   1.190 -by (rtac ext 1);
   1.191 -by Auto_tac;
   1.192 -qed "override_upd";
   1.193 -Addsimps[override_upd];
   1.194 -
   1.195 -Goalw [override_def] "map_of ys ++ map_of xs = map_of (xs@ys)";
   1.196 -by (rtac sym 1);
   1.197 -by (induct_tac "xs" 1);
   1.198 -by (Simp_tac 1);
   1.199 -by (rtac ext 1);
   1.200 -by (asm_simp_tac (simpset() addsplits [option.split]) 1);
   1.201 -qed "map_of_override";
   1.202 -Addsimps [map_of_override];
   1.203 -
   1.204 -Delsimps[fun_upd_apply];
   1.205 -Goal "finite (range f) ==> finite (range (f ++ map_of l))";
   1.206 -by (induct_tac "l" 1);
   1.207 -by  Auto_tac;
   1.208 -by  (fold_goals_tac [empty_def]);
   1.209 -by  (Asm_simp_tac 1);
   1.210 -by (etac finite_range_updI 1);
   1.211 -qed "finite_range_map_of_override";
   1.212 -Addsimps [fun_upd_apply];
   1.213 -
   1.214 -
   1.215 -section "dom";
   1.216 -
   1.217 -Goalw [dom_def] "m a = Some b ==> a : dom m";
   1.218 -by Auto_tac;
   1.219 -qed "domI";
   1.220 -
   1.221 -Goalw [dom_def] "a : dom m ==> ? b. m a = Some b";
   1.222 -by Auto_tac;
   1.223 -qed "domD";
   1.224 -
   1.225 -Goalw [dom_def] "(a : dom m) = (m a ~= None)";
   1.226 -by Auto_tac;
   1.227 -qed "domIff";
   1.228 -AddIffs [domIff];
   1.229 -Delsimps [domIff];
   1.230 -
   1.231 -Goalw [dom_def] "dom empty = {}";
   1.232 -by (Simp_tac 1);
   1.233 -qed "dom_empty";
   1.234 -Addsimps [dom_empty];
   1.235 -
   1.236 -Goalw [dom_def] "dom(m(a|->b)) = insert a (dom m)";
   1.237 -by (Simp_tac 1);
   1.238 -by (Blast_tac 1);
   1.239 -qed "dom_map_upd";
   1.240 -Addsimps [dom_map_upd];
   1.241 -
   1.242 -Goalw [dom_def] "finite (dom (map_of l))";
   1.243 -by (induct_tac "l" 1);
   1.244 -by (auto_tac (claset(),
   1.245 -              simpset() addsimps [insert_Collect RS sym]));
   1.246 -qed "finite_dom_map_of";
   1.247 -
   1.248 -Goalw [dom_def] "dom(m++n) = dom n Un dom m";
   1.249 -by Auto_tac;
   1.250 -qed "dom_override";
   1.251 -Addsimps [dom_override];
   1.252 -
   1.253 -section "ran";
   1.254 -
   1.255 -Goalw [ran_def] "ran empty = {}";
   1.256 -by (Simp_tac 1);
   1.257 -qed "ran_empty";
   1.258 -Addsimps [ran_empty];
   1.259 -
   1.260 -Goalw [ran_def] "ran (%u. None) = {}";
   1.261 -by Auto_tac;
   1.262 -qed "ran_empty'";
   1.263 -Addsimps[ran_empty'];
   1.264 -
   1.265 -Goalw [ran_def] "m a = None ==> ran(m(a|->b)) = insert b (ran m)";
   1.266 -by Auto_tac;
   1.267 -by (subgoal_tac "~(aa = a)" 1);
   1.268 -by Auto_tac;
   1.269 -qed "ran_map_upd";
   1.270 -Addsimps [ran_map_upd];