src/HOL/Map.ML
author wenzelm
Mon, 03 Nov 1997 12:13:18 +0100
changeset 4089 96fba19bcbe2
parent 4071 4747aefbbc52
child 4423 a129b817b58a
permissions -rw-r--r--
isatool fixclasimp;
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
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
     6
Map lemmas
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
     7
*)
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
     8
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
     9
goalw thy [empty_def] "empty k = None";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    10
by(Simp_tac 1);
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    11
qed "empty_def2";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    12
Addsimps [empty_def2];
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    13
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    14
goalw thy [update_def] "(m[a|->b])x = (if x=a then Some b else m x)";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    15
by(Simp_tac 1);
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    16
qed "update_def2";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    17
Addsimps [update_def2];
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    18
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    19
section "++";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    20
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    21
goalw thy [override_def] "m ++ empty = m";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    22
by(Simp_tac 1);
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    23
qed "override_empty";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    24
Addsimps [override_empty];
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    25
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    26
goalw thy [override_def] "empty ++ m = m";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    27
by(Simp_tac 1);
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    28
br ext 1;
4071
4747aefbbc52 expand_option_case -> split_option_case
nipkow
parents: 3981
diff changeset
    29
by(split_tac [split_option_case] 1);
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    30
by(Simp_tac 1);
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    31
qed "empty_override";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    32
Addsimps [empty_override];
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    33
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    34
goalw thy [override_def]
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    35
 "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4071
diff changeset
    36
by(simp_tac (simpset() addsplits [split_option_case]) 1);
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    37
qed_spec_mp "override_Some_iff";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    38
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    39
bind_thm("override_SomeD", standard(override_Some_iff RS iffD1));
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    40
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    41
goalw thy [override_def]
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    42
 "((m ++ n) k = None) = (n k = None & m k = None)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4071
diff changeset
    43
by(simp_tac (simpset() addsplits [split_option_case]) 1);
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    44
qed "override_None";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    45
AddIffs [override_None];
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    46
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    47
goalw thy [override_def] "map_of(xs@ys) = map_of ys ++ map_of xs";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    48
by(induct_tac "xs" 1);
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    49
by(Simp_tac 1);
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    50
br ext 1;
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4071
diff changeset
    51
by(asm_simp_tac (simpset() addsplits [expand_if,split_option_case]) 1);
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    52
qed "map_of_append";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    53
Addsimps [map_of_append];
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    54
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    55
section "dom";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    56
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    57
goalw thy [dom_def] "dom empty = {}";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    58
by(Simp_tac 1);
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    59
qed "dom_empty";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    60
Addsimps [dom_empty];
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    61
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    62
goalw thy [dom_def] "dom(m[a|->b]) = insert a (dom m)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4071
diff changeset
    63
by(simp_tac (simpset() addsplits [expand_if]) 1);
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    64
by(Blast_tac 1);
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    65
qed "dom_update";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    66
Addsimps [dom_update];
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    67
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    68
goalw thy [dom_def] "dom(m++n) = dom n Un dom m";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    69
by(Blast_tac 1);
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    70
qed "dom_override";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    71
Addsimps [dom_override];
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    72
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    73
section "ran";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    74
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    75
goalw thy [ran_def] "ran empty = {}";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    76
by(Simp_tac 1);
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    77
qed "ran_empty";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    78
Addsimps [ran_empty];