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