|
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; |
|
29 by(split_tac [expand_option_case] 1); |
|
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)"; |
|
36 by(simp_tac (!simpset addsplits [expand_option_case]) 1); |
|
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)"; |
|
43 by(simp_tac (!simpset addsplits [expand_option_case]) 1); |
|
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; |
|
51 by(asm_simp_tac (!simpset addsplits [expand_if,expand_option_case]) 1); |
|
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)"; |
|
63 by(simp_tac (!simpset addsplits [expand_if]) 1); |
|
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]; |