src/HOL/Map.ML
author nipkow
Fri, 24 Jul 1998 17:18:15 +0200
changeset 5195 277831ae7eac
parent 5183 89f162de39cf
child 5300 2b1ca524ace8
permissions -rw-r--r--
Map.update -> map_upd, Unpdate.update -> fun_upd Problem: macros get confused about two updates.
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
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4990
diff changeset
     9
Goalw [empty_def] "empty k = None";
4423
a129b817b58a expandshort;
wenzelm
parents: 4089
diff changeset
    10
by (Simp_tac 1);
3981
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
5195
277831ae7eac Map.update -> map_upd, Unpdate.update -> fun_upd
nipkow
parents: 5183
diff changeset
    14
Goalw [map_upd_def] "(m[a|->b])x = (if x=a then Some b else m x)";
4423
a129b817b58a expandshort;
wenzelm
parents: 4089
diff changeset
    15
by (Simp_tac 1);
5195
277831ae7eac Map.update -> map_upd, Unpdate.update -> fun_upd
nipkow
parents: 5183
diff changeset
    16
qed "map_upd_def2";
277831ae7eac Map.update -> map_upd, Unpdate.update -> fun_upd
nipkow
parents: 5183
diff changeset
    17
Addsimps [map_upd_def2];
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    18
5195
277831ae7eac Map.update -> map_upd, Unpdate.update -> fun_upd
nipkow
parents: 5183
diff changeset
    19
qed_goal "map_upd_same" thy "(t[k|->x]) k = Some x" 
4526
6be35399125a added update_same, update_other, update_triv, and map_of_SomeD
oheimb
parents: 4423
diff changeset
    20
	(K [Simp_tac 1]);
5195
277831ae7eac Map.update -> map_upd, Unpdate.update -> fun_upd
nipkow
parents: 5183
diff changeset
    21
qed_goal "map_upd_other" thy "!!X. l~=k ==> (t[k|->x]) l = t l"
4526
6be35399125a added update_same, update_other, update_triv, and map_of_SomeD
oheimb
parents: 4423
diff changeset
    22
	(K [Asm_simp_tac 1]);
5195
277831ae7eac Map.update -> map_upd, Unpdate.update -> fun_upd
nipkow
parents: 5183
diff changeset
    23
qed_goal "map_upd_triv" thy "!!X. t k = Some x ==> t[k|->x] = t"
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4526
diff changeset
    24
	(K [rtac ext 1, Asm_simp_tac 1]);
5195
277831ae7eac Map.update -> map_upd, Unpdate.update -> fun_upd
nipkow
parents: 5183
diff changeset
    25
(*Addsimps [map_upd_same, map_upd_other, map_upd_triv];*)
4526
6be35399125a added update_same, update_other, update_triv, and map_of_SomeD
oheimb
parents: 4423
diff changeset
    26
4990
25da60d0a20b added option_map_o_empty
oheimb
parents: 4926
diff changeset
    27
section "option_map";
25da60d0a20b added option_map_o_empty
oheimb
parents: 4926
diff changeset
    28
25da60d0a20b added option_map_o_empty
oheimb
parents: 4926
diff changeset
    29
qed_goal "option_map_o_empty" thy 
25da60d0a20b added option_map_o_empty
oheimb
parents: 4926
diff changeset
    30
         "option_map f o empty = empty" (K [rtac ext 1, Simp_tac 1]);
25da60d0a20b added option_map_o_empty
oheimb
parents: 4926
diff changeset
    31
5195
277831ae7eac Map.update -> map_upd, Unpdate.update -> fun_upd
nipkow
parents: 5183
diff changeset
    32
qed_goal "option_map_o_map_upd" thy 
4990
25da60d0a20b added option_map_o_empty
oheimb
parents: 4926
diff changeset
    33
	 "option_map f o m[a|->b] = (option_map f o m)[a|->f b]" 
25da60d0a20b added option_map_o_empty
oheimb
parents: 4926
diff changeset
    34
	(K [rtac ext 1, Simp_tac 1]);
5195
277831ae7eac Map.update -> map_upd, Unpdate.update -> fun_upd
nipkow
parents: 5183
diff changeset
    35
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
    36
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    37
section "++";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    38
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4990
diff changeset
    39
Goalw [override_def] "m ++ empty = m";
4423
a129b817b58a expandshort;
wenzelm
parents: 4089
diff changeset
    40
by (Simp_tac 1);
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    41
qed "override_empty";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    42
Addsimps [override_empty];
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    43
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4990
diff changeset
    44
Goalw [override_def] "empty ++ m = m";
4423
a129b817b58a expandshort;
wenzelm
parents: 4089
diff changeset
    45
by (Simp_tac 1);
a129b817b58a expandshort;
wenzelm
parents: 4089
diff changeset
    46
by (rtac ext 1);
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5143
diff changeset
    47
by (split_tac [option.split] 1);
4423
a129b817b58a expandshort;
wenzelm
parents: 4089
diff changeset
    48
by (Simp_tac 1);
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    49
qed "empty_override";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    50
Addsimps [empty_override];
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    51
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4990
diff changeset
    52
Goalw [override_def]
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    53
 "((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
    54
by (simp_tac (simpset() addsplits [option.split]) 1);
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    55
qed_spec_mp "override_Some_iff";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    56
4926
0fd0b3f3bc25 added option_map_o_update
oheimb
parents: 4883
diff changeset
    57
bind_thm ("override_SomeD", standard(override_Some_iff RS iffD1));
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    58
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4990
diff changeset
    59
Goalw [override_def]
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    60
 "((m ++ n) k = None) = (n k = None & m k = None)";
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5143
diff changeset
    61
by (simp_tac (simpset() addsplits [option.split]) 1);
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    62
qed "override_None";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    63
AddIffs [override_None];
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    64
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4990
diff changeset
    65
Goalw [override_def] "map_of(xs@ys) = map_of ys ++ map_of xs";
4423
a129b817b58a expandshort;
wenzelm
parents: 4089
diff changeset
    66
by (induct_tac "xs" 1);
a129b817b58a expandshort;
wenzelm
parents: 4089
diff changeset
    67
by (Simp_tac 1);
a129b817b58a expandshort;
wenzelm
parents: 4089
diff changeset
    68
by (rtac ext 1);
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5143
diff changeset
    69
by (asm_simp_tac (simpset() addsplits [option.split]) 1);
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    70
qed "map_of_append";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    71
Addsimps [map_of_append];
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    72
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4990
diff changeset
    73
Goal "map_of xs k = Some y --> (k,y):set xs";
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5143
diff changeset
    74
by (induct_tac "xs" 1);
4526
6be35399125a added update_same, update_other, update_triv, and map_of_SomeD
oheimb
parents: 4423
diff changeset
    75
by  (Simp_tac 1);
4838
196100237656 cleanup for split_all_tac as wrapper in claset()
oheimb
parents: 4686
diff changeset
    76
by (split_all_tac 1);
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4526
diff changeset
    77
by (Asm_simp_tac 1);
4526
6be35399125a added update_same, update_other, update_triv, and map_of_SomeD
oheimb
parents: 4423
diff changeset
    78
qed_spec_mp "map_of_SomeD";
6be35399125a added update_same, update_other, update_triv, and map_of_SomeD
oheimb
parents: 4423
diff changeset
    79
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    80
section "dom";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    81
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4990
diff changeset
    82
Goalw [dom_def] "dom empty = {}";
4423
a129b817b58a expandshort;
wenzelm
parents: 4089
diff changeset
    83
by (Simp_tac 1);
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    84
qed "dom_empty";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    85
Addsimps [dom_empty];
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    86
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4990
diff changeset
    87
Goalw [dom_def] "dom(m[a|->b]) = insert a (dom m)";
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4526
diff changeset
    88
by (Simp_tac 1);
4423
a129b817b58a expandshort;
wenzelm
parents: 4089
diff changeset
    89
by (Blast_tac 1);
5195
277831ae7eac Map.update -> map_upd, Unpdate.update -> fun_upd
nipkow
parents: 5183
diff changeset
    90
qed "dom_map_upd";
277831ae7eac Map.update -> map_upd, Unpdate.update -> fun_upd
nipkow
parents: 5183
diff changeset
    91
Addsimps [dom_map_upd];
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    92
4883
c1aec06d1dca added finite_dom_map_of and ran_update
oheimb
parents: 4838
diff changeset
    93
qed_goalw "finite_dom_map_of" Map.thy [dom_def] "finite (dom (map_of l))" (K[
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5143
diff changeset
    94
	induct_tac "l" 1,
4883
c1aec06d1dca added finite_dom_map_of and ran_update
oheimb
parents: 4838
diff changeset
    95
	 ALLGOALS Simp_tac,
c1aec06d1dca added finite_dom_map_of and ran_update
oheimb
parents: 4838
diff changeset
    96
	stac (insert_Collect RS sym) 1,
c1aec06d1dca added finite_dom_map_of and ran_update
oheimb
parents: 4838
diff changeset
    97
	Asm_simp_tac 1]);
c1aec06d1dca added finite_dom_map_of and ran_update
oheimb
parents: 4838
diff changeset
    98
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4990
diff changeset
    99
Goalw [dom_def] "dom(m++n) = dom n Un dom m";
4423
a129b817b58a expandshort;
wenzelm
parents: 4089
diff changeset
   100
by (Blast_tac 1);
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
   101
qed "dom_override";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
   102
Addsimps [dom_override];
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
   103
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
   104
section "ran";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
   105
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4990
diff changeset
   106
Goalw [ran_def] "ran empty = {}";
4423
a129b817b58a expandshort;
wenzelm
parents: 4089
diff changeset
   107
by (Simp_tac 1);
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
   108
qed "ran_empty";
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
   109
Addsimps [ran_empty];
4883
c1aec06d1dca added finite_dom_map_of and ran_update
oheimb
parents: 4838
diff changeset
   110
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   111
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
   112
by Auto_tac;
c1aec06d1dca added finite_dom_map_of and ran_update
oheimb
parents: 4838
diff changeset
   113
by (subgoal_tac "~(aa = a)" 1);
c1aec06d1dca added finite_dom_map_of and ran_update
oheimb
parents: 4838
diff changeset
   114
by Auto_tac;
5195
277831ae7eac Map.update -> map_upd, Unpdate.update -> fun_upd
nipkow
parents: 5183
diff changeset
   115
qed "ran_map_upd";
277831ae7eac Map.update -> map_upd, Unpdate.update -> fun_upd
nipkow
parents: 5183
diff changeset
   116
Addsimps [ran_map_upd];