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