3981
|
1 |
(* Title: HOL/Map.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 1997 TU Muenchen
|
|
5 |
|
|
6 |
Map lemmas
|
|
7 |
*)
|
|
8 |
|
|
9 |
goalw thy [empty_def] "empty k = None";
|
|
10 |
by(Simp_tac 1);
|
|
11 |
qed "empty_def2";
|
|
12 |
Addsimps [empty_def2];
|
|
13 |
|
|
14 |
goalw thy [update_def] "(m[a|->b])x = (if x=a then Some b else m x)";
|
|
15 |
by(Simp_tac 1);
|
|
16 |
qed "update_def2";
|
|
17 |
Addsimps [update_def2];
|
|
18 |
|
|
19 |
section "++";
|
|
20 |
|
|
21 |
goalw thy [override_def] "m ++ empty = m";
|
|
22 |
by(Simp_tac 1);
|
|
23 |
qed "override_empty";
|
|
24 |
Addsimps [override_empty];
|
|
25 |
|
|
26 |
goalw thy [override_def] "empty ++ m = m";
|
|
27 |
by(Simp_tac 1);
|
|
28 |
br ext 1;
|
4071
|
29 |
by(split_tac [split_option_case] 1);
|
3981
|
30 |
by(Simp_tac 1);
|
|
31 |
qed "empty_override";
|
|
32 |
Addsimps [empty_override];
|
|
33 |
|
|
34 |
goalw thy [override_def]
|
|
35 |
"((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)";
|
4089
|
36 |
by(simp_tac (simpset() addsplits [split_option_case]) 1);
|
3981
|
37 |
qed_spec_mp "override_Some_iff";
|
|
38 |
|
|
39 |
bind_thm("override_SomeD", standard(override_Some_iff RS iffD1));
|
|
40 |
|
|
41 |
goalw thy [override_def]
|
|
42 |
"((m ++ n) k = None) = (n k = None & m k = None)";
|
4089
|
43 |
by(simp_tac (simpset() addsplits [split_option_case]) 1);
|
3981
|
44 |
qed "override_None";
|
|
45 |
AddIffs [override_None];
|
|
46 |
|
|
47 |
goalw thy [override_def] "map_of(xs@ys) = map_of ys ++ map_of xs";
|
|
48 |
by(induct_tac "xs" 1);
|
|
49 |
by(Simp_tac 1);
|
|
50 |
br ext 1;
|
4089
|
51 |
by(asm_simp_tac (simpset() addsplits [expand_if,split_option_case]) 1);
|
3981
|
52 |
qed "map_of_append";
|
|
53 |
Addsimps [map_of_append];
|
|
54 |
|
|
55 |
section "dom";
|
|
56 |
|
|
57 |
goalw thy [dom_def] "dom empty = {}";
|
|
58 |
by(Simp_tac 1);
|
|
59 |
qed "dom_empty";
|
|
60 |
Addsimps [dom_empty];
|
|
61 |
|
|
62 |
goalw thy [dom_def] "dom(m[a|->b]) = insert a (dom m)";
|
4089
|
63 |
by(simp_tac (simpset() addsplits [expand_if]) 1);
|
3981
|
64 |
by(Blast_tac 1);
|
|
65 |
qed "dom_update";
|
|
66 |
Addsimps [dom_update];
|
|
67 |
|
|
68 |
goalw thy [dom_def] "dom(m++n) = dom n Un dom m";
|
|
69 |
by(Blast_tac 1);
|
|
70 |
qed "dom_override";
|
|
71 |
Addsimps [dom_override];
|
|
72 |
|
|
73 |
section "ran";
|
|
74 |
|
|
75 |
goalw thy [ran_def] "ran empty = {}";
|
|
76 |
by(Simp_tac 1);
|
|
77 |
qed "ran_empty";
|
|
78 |
Addsimps [ran_empty];
|