src/HOL/Map.ML
author paulson
Wed Mar 03 11:15:18 1999 +0100 (1999-03-03)
changeset 6301 08245f5a436d
parent 5444 ffc64812a70b
child 7958 f531589c9fc1
permissions -rw-r--r--
expandshort
nipkow@3981
     1
(*  Title:      HOL/Map.ML
nipkow@3981
     2
    ID:         $Id$
nipkow@3981
     3
    Author:     Tobias Nipkow
nipkow@3981
     4
    Copyright   1997 TU Muenchen
nipkow@3981
     5
nipkow@3981
     6
Map lemmas
nipkow@3981
     7
*)
nipkow@3981
     8
oheimb@5300
     9
section "empty";
oheimb@5300
    10
wenzelm@5069
    11
Goalw [empty_def] "empty k = None";
wenzelm@4423
    12
by (Simp_tac 1);
nipkow@3981
    13
qed "empty_def2";
nipkow@3981
    14
Addsimps [empty_def2];
nipkow@3981
    15
oheimb@5300
    16
oheimb@5300
    17
section "map_upd";
oheimb@5300
    18
oheimb@5300
    19
qed_goal "map_upd_triv" thy "!!X. t k = Some x ==> t(k|->x) = t"
oheimb@5300
    20
	(K [rtac ext 1, Asm_simp_tac 1]);
oheimb@5300
    21
(*Addsimps [map_upd_triv];*)
oheimb@5300
    22
oheimb@5300
    23
oheimb@5300
    24
section "map_upds";
nipkow@3981
    25
oheimb@5300
    26
Goal "a ~: set as --> (!m bs. (m(a|->b)(as[|->]bs)) = (m(as[|->]bs)(a|->b)))";
oheimb@5300
    27
by (induct_tac "as" 1);
oheimb@5300
    28
by  (auto_tac (claset(), simpset() delsimps[fun_upd_apply]));
oheimb@5300
    29
by (REPEAT(dtac spec 1));
oheimb@5300
    30
by (rotate_tac ~1 1);
oheimb@5300
    31
by (etac subst 1);
oheimb@5300
    32
by (etac (fun_upd_twist RS subst) 1);
oheimb@5300
    33
by (rtac refl 1);
oheimb@5300
    34
qed_spec_mp "map_upds_twist";
oheimb@5300
    35
Addsimps [map_upds_twist];
oheimb@5300
    36
oheimb@5300
    37
oheimb@5300
    38
section "chg_map";
oheimb@5300
    39
oheimb@5300
    40
qed_goalw "chg_map_new" thy [chg_map_def]
oheimb@5300
    41
	"!!s. m a = None   ==> chg_map f a m = m"          (K [Auto_tac]);
oheimb@5300
    42
qed_goalw "chg_map_upd" thy [chg_map_def]
oheimb@5300
    43
	"!!s. m a = Some b ==> chg_map f a m = m(a|->f b)" (K [Auto_tac]);
oheimb@5300
    44
Addsimps[chg_map_new, chg_map_upd];
oheimb@5300
    45
oheimb@4526
    46
oheimb@4990
    47
section "option_map";
oheimb@4990
    48
oheimb@4990
    49
qed_goal "option_map_o_empty" thy 
oheimb@4990
    50
         "option_map f o empty = empty" (K [rtac ext 1, Simp_tac 1]);
oheimb@4990
    51
nipkow@5195
    52
qed_goal "option_map_o_map_upd" thy 
oheimb@5300
    53
	 "option_map f o m(a|->b) = (option_map f o m)(a|->f b)" 
oheimb@4990
    54
	(K [rtac ext 1, Simp_tac 1]);
nipkow@5195
    55
Addsimps[option_map_o_empty, option_map_o_map_upd];
oheimb@4883
    56
oheimb@5300
    57
nipkow@3981
    58
section "++";
nipkow@3981
    59
wenzelm@5069
    60
Goalw [override_def] "m ++ empty = m";
wenzelm@4423
    61
by (Simp_tac 1);
nipkow@3981
    62
qed "override_empty";
nipkow@3981
    63
Addsimps [override_empty];
nipkow@3981
    64
wenzelm@5069
    65
Goalw [override_def] "empty ++ m = m";
wenzelm@4423
    66
by (Simp_tac 1);
wenzelm@4423
    67
by (rtac ext 1);
berghofe@5183
    68
by (split_tac [option.split] 1);
wenzelm@4423
    69
by (Simp_tac 1);
nipkow@3981
    70
qed "empty_override";
nipkow@3981
    71
Addsimps [empty_override];
nipkow@3981
    72
wenzelm@5069
    73
Goalw [override_def]
nipkow@3981
    74
 "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)";
berghofe@5183
    75
by (simp_tac (simpset() addsplits [option.split]) 1);
nipkow@3981
    76
qed_spec_mp "override_Some_iff";
nipkow@3981
    77
oheimb@4926
    78
bind_thm ("override_SomeD", standard(override_Some_iff RS iffD1));
oheimb@5444
    79
AddSDs[override_SomeD];
nipkow@3981
    80
oheimb@5444
    81
Goalw [override_def] "((m ++ n) k = None) = (n k = None & m k = None)";
berghofe@5183
    82
by (simp_tac (simpset() addsplits [option.split]) 1);
nipkow@3981
    83
qed "override_None";
nipkow@3981
    84
AddIffs [override_None];
nipkow@3981
    85
oheimb@5444
    86
Goalw [override_def] "map_of ys ++ map_of xs = map_of (xs@ys)";
oheimb@5444
    87
by (rtac sym 1);
wenzelm@4423
    88
by (induct_tac "xs" 1);
wenzelm@4423
    89
by (Simp_tac 1);
wenzelm@4423
    90
by (rtac ext 1);
berghofe@5183
    91
by (asm_simp_tac (simpset() addsplits [option.split]) 1);
oheimb@5444
    92
qed "map_of_override";
oheimb@5444
    93
Addsimps [map_of_override];
nipkow@3981
    94
wenzelm@5069
    95
Goal "map_of xs k = Some y --> (k,y):set xs";
berghofe@5183
    96
by (induct_tac "xs" 1);
oheimb@4526
    97
by  (Simp_tac 1);
oheimb@4838
    98
by (split_all_tac 1);
nipkow@4686
    99
by (Asm_simp_tac 1);
oheimb@4526
   100
qed_spec_mp "map_of_SomeD";
oheimb@4526
   101
oheimb@5300
   102
nipkow@3981
   103
section "dom";
nipkow@3981
   104
wenzelm@5069
   105
Goalw [dom_def] "dom empty = {}";
wenzelm@4423
   106
by (Simp_tac 1);
nipkow@3981
   107
qed "dom_empty";
nipkow@3981
   108
Addsimps [dom_empty];
nipkow@3981
   109
oheimb@5300
   110
Goalw [dom_def] "dom(m(a|->b)) = insert a (dom m)";
nipkow@4686
   111
by (Simp_tac 1);
wenzelm@4423
   112
by (Blast_tac 1);
nipkow@5195
   113
qed "dom_map_upd";
nipkow@5195
   114
Addsimps [dom_map_upd];
nipkow@3981
   115
oheimb@4883
   116
qed_goalw "finite_dom_map_of" Map.thy [dom_def] "finite (dom (map_of l))" (K[
berghofe@5183
   117
	induct_tac "l" 1,
oheimb@4883
   118
	 ALLGOALS Simp_tac,
oheimb@4883
   119
	stac (insert_Collect RS sym) 1,
oheimb@5444
   120
	Asm_full_simp_tac 1]);
oheimb@4883
   121
wenzelm@5069
   122
Goalw [dom_def] "dom(m++n) = dom n Un dom m";
paulson@6301
   123
by (Simp_tac 1);
wenzelm@4423
   124
by (Blast_tac 1);
nipkow@3981
   125
qed "dom_override";
nipkow@3981
   126
Addsimps [dom_override];
nipkow@3981
   127
nipkow@3981
   128
section "ran";
nipkow@3981
   129
wenzelm@5069
   130
Goalw [ran_def] "ran empty = {}";
wenzelm@4423
   131
by (Simp_tac 1);
nipkow@3981
   132
qed "ran_empty";
nipkow@3981
   133
Addsimps [ran_empty];
oheimb@4883
   134
oheimb@5300
   135
Goalw [ran_def] "m a = None ==> ran(m(a|->b)) = insert b (ran m)";
oheimb@4883
   136
by Auto_tac;
oheimb@4883
   137
by (subgoal_tac "~(aa = a)" 1);
oheimb@4883
   138
by Auto_tac;
nipkow@5195
   139
qed "ran_map_upd";
nipkow@5195
   140
Addsimps [ran_map_upd];