src/HOL/Map.ML
author nipkow
Sat Feb 08 14:46:22 2003 +0100 (2003-02-08)
changeset 13811 f39f67982854
parent 11015 55d95834c815
child 13890 90611b4e0054
permissions -rw-r--r--
adjusted dom rules
     1 (*  Title:      HOL/Map.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1997 TU Muenchen
     5 
     6 Map lemmas.
     7 *)
     8 
     9 section "empty";
    10 
    11 Goalw [empty_def] "empty k = None";
    12 by (Simp_tac 1);
    13 qed "empty_def2";
    14 Addsimps [empty_def2];
    15 
    16 Goal "empty(x := None) = empty";
    17 by (rtac ext 1);
    18 by (Simp_tac 1);
    19 qed "empty_upd_none";
    20 Addsimps [empty_upd_none];
    21 
    22 Goal "sum_case empty empty = empty";
    23 by (rtac ext 1);
    24 by (simp_tac (simpset() addsplits [sum.split]) 1);
    25 qed "sum_case_empty_empty";
    26 Addsimps [sum_case_empty_empty];
    27 
    28 
    29 section "map_upd";
    30 
    31 Goal "t k = Some x ==> t(k|->x) = t";
    32 by (rtac ext 1);
    33 by (Asm_simp_tac 1);
    34 qed "map_upd_triv";
    35 
    36 Goal "t(k|->x) ~= empty";
    37 by Safe_tac;
    38 by (dres_inst_tac [("x","k")] fun_cong 1);
    39 by (Full_simp_tac 1);
    40 qed "map_upd_nonempty";
    41 Addsimps[map_upd_nonempty];
    42 
    43 Goalw [image_def] "finite (range f) ==> finite (range (f(a|->b)))";
    44 by (full_simp_tac (simpset() addsimps [full_SetCompr_eq]) 1);
    45 by (rtac finite_subset 1);
    46 by (assume_tac 2);
    47 by Auto_tac;
    48 qed "finite_range_updI";
    49 
    50 
    51 section "sum_case and empty/map_upd";
    52 
    53 Goal "sum_case (m(k|->y)) empty =  (sum_case m empty)(Inl k|->y)";
    54 by (rtac ext 1);
    55 by (simp_tac (simpset() addsplits [sum.split]) 1);
    56 qed "sum_case_map_upd_empty";
    57 Addsimps[sum_case_map_upd_empty];
    58 
    59 Goal "sum_case empty (m(k|->y)) =  (sum_case empty m)(Inr k|->y)";
    60 by (rtac ext 1);
    61 by (simp_tac (simpset() addsplits [sum.split]) 1);
    62 qed "sum_case_empty_map_upd";
    63 Addsimps[sum_case_empty_map_upd];
    64 
    65 Goal "sum_case (m1(k1|->y1)) (m2(k2|->y2)) = (sum_case (m1(k1|->y1)) m2)(Inr k2|->y2)";
    66 by (rtac ext 1);
    67 by (simp_tac (simpset() addsplits [sum.split]) 1);
    68 qed "sum_case_map_upd_map_upd";
    69 Addsimps[sum_case_map_upd_map_upd];
    70 
    71 
    72 section "map_upds";
    73 
    74 Goal "a ~: set as --> (!m bs. (m(a|->b)(as[|->]bs)) = (m(as[|->]bs)(a|->b)))";
    75 by (induct_tac "as" 1);
    76 by  (auto_tac (claset(), simpset() delsimps[fun_upd_apply]));
    77 by (REPEAT(dtac spec 1));
    78 by (rotate_tac ~1 1);
    79 by (etac subst 1);
    80 by (etac (fun_upd_twist RS subst) 1);
    81 by (rtac refl 1);
    82 qed_spec_mp "map_upds_twist";
    83 Addsimps [map_upds_twist];
    84 
    85 
    86 section "chg_map";
    87 
    88 Goalw [chg_map_def] "m a = None   ==> chg_map f a m = m";
    89 by Auto_tac;
    90 qed "chg_map_new";
    91 
    92 Goalw [chg_map_def] "m a = Some b ==> chg_map f a m = m(a|->f b)";
    93 by Auto_tac;
    94 qed "chg_map_upd";
    95 
    96 Addsimps[chg_map_new, chg_map_upd];
    97 
    98 
    99 section "map_of";
   100 
   101 Goal "map_of xs k = Some y --> (k,y):set xs";
   102 by (induct_tac "xs" 1);
   103 by  Auto_tac;
   104 qed_spec_mp "map_of_SomeD";
   105 
   106 Goal "inj f ==> map_of t k = Some x --> \
   107 \  map_of (map (split (%k. Pair (f k))) t) (f k) = Some x";
   108 by (induct_tac "t" 1);
   109 by  (auto_tac (claset(),simpset()addsimps[inj_eq]));
   110 qed_spec_mp "map_of_mapk_SomeI";
   111 
   112 Goal "(k, x) : set l --> (? x. map_of l k = Some x)";
   113 by (induct_tac "l" 1);
   114 by  Auto_tac;
   115 qed_spec_mp "weak_map_of_SomeI";
   116 
   117 Goal 
   118 "[| map_of xs k = Some z; P k z |] ==> map_of (filter (split P) xs) k = Some z";
   119 by (rtac mp 1);
   120 by (atac 2);
   121 by (etac thin_rl 1);
   122 by (induct_tac "xs" 1);
   123 by  Auto_tac;
   124 qed "map_of_filter_in";
   125 
   126 Goal "finite (range (map_of l))";
   127 by (induct_tac "l" 1);
   128 by  (ALLGOALS (simp_tac (simpset() addsimps [image_constant])));
   129 by (rtac finite_subset 1);
   130 by (assume_tac 2);
   131 by Auto_tac;
   132 qed "finite_range_map_of";
   133 
   134 Goal "map_of (map (%(a,b). (a,f b)) xs) x = option_map f (map_of xs x)";
   135 by (induct_tac "xs" 1);
   136 by Auto_tac;
   137 qed "map_of_map";
   138 
   139 
   140 section "option_map related";
   141 
   142 Goal "option_map f o empty = empty";
   143 by (rtac ext 1);
   144 by (Simp_tac 1);
   145 qed "option_map_o_empty";
   146 
   147 Goal "option_map f o m(a|->b) = (option_map f o m)(a|->f b)";
   148 by (rtac ext 1);
   149 by (Simp_tac 1);
   150 qed "option_map_o_map_upd";
   151 
   152 Addsimps[option_map_o_empty, option_map_o_map_upd];
   153 
   154 
   155 section "++";
   156 
   157 Goalw [override_def] "m ++ empty = m";
   158 by (Simp_tac 1);
   159 qed "override_empty";
   160 Addsimps [override_empty];
   161 
   162 Goalw [override_def] "empty ++ m = m";
   163 by (Simp_tac 1);
   164 by (rtac ext 1);
   165 by (split_tac [option.split] 1);
   166 by (Simp_tac 1);
   167 qed "empty_override";
   168 Addsimps [empty_override];
   169 
   170 Goalw [override_def]
   171  "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)";
   172 by (simp_tac (simpset() addsplits [option.split]) 1);
   173 qed_spec_mp "override_Some_iff";
   174 
   175 bind_thm ("override_SomeD", standard(override_Some_iff RS iffD1));
   176 AddSDs[override_SomeD];
   177 
   178 Goal "!!xx. n k = Some xx ==> (m ++ n) k = Some xx";
   179 by (stac override_Some_iff 1);
   180 by (Fast_tac 1);
   181 qed "override_find_right";
   182 Addsimps[override_find_right];
   183 
   184 Goalw [override_def] "((m ++ n) k = None) = (n k = None & m k = None)";
   185 by (simp_tac (simpset() addsplits [option.split]) 1);
   186 qed "override_None";
   187 AddIffs [override_None];
   188 
   189 Goalw [override_def] "f ++ g(x|->y) = (f ++ g)(x|->y)";
   190 by (rtac ext 1);
   191 by Auto_tac;
   192 qed "override_upd";
   193 Addsimps[override_upd];
   194 
   195 Goalw [override_def] "map_of ys ++ map_of xs = map_of (xs@ys)";
   196 by (rtac sym 1);
   197 by (induct_tac "xs" 1);
   198 by (Simp_tac 1);
   199 by (rtac ext 1);
   200 by (asm_simp_tac (simpset() addsplits [option.split]) 1);
   201 qed "map_of_override";
   202 Addsimps [map_of_override];
   203 
   204 Delsimps[fun_upd_apply];
   205 Goal "finite (range f) ==> finite (range (f ++ map_of l))";
   206 by (induct_tac "l" 1);
   207 by  Auto_tac;
   208 by  (fold_goals_tac [empty_def]);
   209 by  (Asm_simp_tac 1);
   210 by (etac finite_range_updI 1);
   211 qed "finite_range_map_of_override";
   212 Addsimps [fun_upd_apply];
   213 
   214 
   215 section "dom";
   216 
   217 Goalw [dom_def] "m a = Some b ==> a : dom m";
   218 by Auto_tac;
   219 qed "domI";
   220 
   221 Goalw [dom_def] "a : dom m ==> ? b. m a = Some b";
   222 by Auto_tac;
   223 qed "domD";
   224 
   225 Goalw [dom_def] "(a : dom m) = (m a ~= None)";
   226 by Auto_tac;
   227 qed "domIff";
   228 AddIffs [domIff];
   229 Delsimps [domIff];
   230 
   231 Goalw [dom_def] "dom empty = {}";
   232 by (Simp_tac 1);
   233 qed "dom_empty";
   234 Addsimps [dom_empty];
   235 
   236 Goalw [dom_def] "dom(m(a|->b)) = insert a (dom m)";
   237 by (Simp_tac 1);
   238 by (Blast_tac 1);
   239 qed "dom_map_upd";
   240 Addsimps [dom_map_upd];
   241 
   242 Goalw [dom_def] "finite (dom (map_of l))";
   243 by (induct_tac "l" 1);
   244 by (auto_tac (claset(),
   245               simpset() addsimps [insert_Collect RS sym]));
   246 qed "finite_dom_map_of";
   247 
   248 Goalw [dom_def] "dom(m++n) = dom n Un dom m";
   249 by Auto_tac;
   250 qed "dom_override";
   251 Addsimps [dom_override];
   252 
   253 section "ran";
   254 
   255 Goalw [ran_def] "ran empty = {}";
   256 by (Simp_tac 1);
   257 qed "ran_empty";
   258 Addsimps [ran_empty];
   259 
   260 Goalw [ran_def] "ran (%u. None) = {}";
   261 by Auto_tac;
   262 qed "ran_empty'";
   263 Addsimps[ran_empty'];
   264 
   265 Goalw [ran_def] "m a = None ==> ran(m(a|->b)) = insert b (ran m)";
   266 by Auto_tac;
   267 by (subgoal_tac "~(aa = a)" 1);
   268 by Auto_tac;
   269 qed "ran_map_upd";
   270 Addsimps [ran_map_upd];