24 Addsimps [override_empty]; |
24 Addsimps [override_empty]; |
25 |
25 |
26 goalw thy [override_def] "empty ++ m = m"; |
26 goalw thy [override_def] "empty ++ m = m"; |
27 by(Simp_tac 1); |
27 by(Simp_tac 1); |
28 br ext 1; |
28 br ext 1; |
29 by(split_tac [expand_option_case] 1); |
29 by(split_tac [split_option_case] 1); |
30 by(Simp_tac 1); |
30 by(Simp_tac 1); |
31 qed "empty_override"; |
31 qed "empty_override"; |
32 Addsimps [empty_override]; |
32 Addsimps [empty_override]; |
33 |
33 |
34 goalw thy [override_def] |
34 goalw thy [override_def] |
35 "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)"; |
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); |
36 by(simp_tac (!simpset addsplits [split_option_case]) 1); |
37 qed_spec_mp "override_Some_iff"; |
37 qed_spec_mp "override_Some_iff"; |
38 |
38 |
39 bind_thm("override_SomeD", standard(override_Some_iff RS iffD1)); |
39 bind_thm("override_SomeD", standard(override_Some_iff RS iffD1)); |
40 |
40 |
41 goalw thy [override_def] |
41 goalw thy [override_def] |
42 "((m ++ n) k = None) = (n k = None & m k = None)"; |
42 "((m ++ n) k = None) = (n k = None & m k = None)"; |
43 by(simp_tac (!simpset addsplits [expand_option_case]) 1); |
43 by(simp_tac (!simpset addsplits [split_option_case]) 1); |
44 qed "override_None"; |
44 qed "override_None"; |
45 AddIffs [override_None]; |
45 AddIffs [override_None]; |
46 |
46 |
47 goalw thy [override_def] "map_of(xs@ys) = map_of ys ++ map_of xs"; |
47 goalw thy [override_def] "map_of(xs@ys) = map_of ys ++ map_of xs"; |
48 by(induct_tac "xs" 1); |
48 by(induct_tac "xs" 1); |
49 by(Simp_tac 1); |
49 by(Simp_tac 1); |
50 br ext 1; |
50 br ext 1; |
51 by(asm_simp_tac (!simpset addsplits [expand_if,expand_option_case]) 1); |
51 by(asm_simp_tac (!simpset addsplits [expand_if,split_option_case]) 1); |
52 qed "map_of_append"; |
52 qed "map_of_append"; |
53 Addsimps [map_of_append]; |
53 Addsimps [map_of_append]; |
54 |
54 |
55 section "dom"; |
55 section "dom"; |
56 |
56 |