author  berghofe 
Tue, 30 May 2000 18:02:49 +0200  
changeset 9001  93af64f54bf2 
parent 8529  4656e8312ba9 
child 9018  b16bc0b5ad21 
permissions  rwrr 
3981  1 
(* Title: HOL/Map.ML 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow 

4 
Copyright 1997 TU Muenchen 

5 

6 
Map lemmas 

7 
*) 

8 

5300  9 
section "empty"; 
10 

5069  11 
Goalw [empty_def] "empty k = None"; 
4423  12 
by (Simp_tac 1); 
3981  13 
qed "empty_def2"; 
14 
Addsimps [empty_def2]; 

15 

5300  16 

17 
section "map_upd"; 

18 

8529  19 
Goal "t k = Some x ==> t(k>x) = t"; 
20 
by (rtac ext 1); 

21 
by (Asm_simp_tac 1); 

22 
qed "map_upd_triv"; 

5300  23 

8160
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

24 
Goalw [image_def] "finite (range f) ==> finite (range (f(a>b)))"; 
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

25 
by (full_simp_tac (simpset() addsimps [full_SetCompr_eq]) 1); 
8254  26 
by (rtac finite_subset 1); 
27 
by (assume_tac 2); 

8160
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

28 
by Auto_tac; 
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

29 
qed "finite_range_updI"; 
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

30 

5300  31 

32 
section "map_upds"; 

3981  33 

5300  34 
Goal "a ~: set as > (!m bs. (m(a>b)(as[>]bs)) = (m(as[>]bs)(a>b)))"; 
35 
by (induct_tac "as" 1); 

36 
by (auto_tac (claset(), simpset() delsimps[fun_upd_apply])); 

37 
by (REPEAT(dtac spec 1)); 

38 
by (rotate_tac ~1 1); 

39 
by (etac subst 1); 

40 
by (etac (fun_upd_twist RS subst) 1); 

41 
by (rtac refl 1); 

42 
qed_spec_mp "map_upds_twist"; 

43 
Addsimps [map_upds_twist]; 

44 

45 

46 
section "chg_map"; 

47 

8529  48 
Goalw [chg_map_def] "m a = None ==> chg_map f a m = m"; 
49 
by Auto_tac; 

50 
qed "chg_map_new"; 

51 

52 
Goalw [chg_map_def] "m a = Some b ==> chg_map f a m = m(a>f b)"; 

53 
by Auto_tac; 

54 
qed "chg_map_upd"; 

55 

5300  56 
Addsimps[chg_map_new, chg_map_upd]; 
57 

4526
6be35399125a
added update_same, update_other, update_triv, and map_of_SomeD
oheimb
parents:
4423
diff
changeset

58 

7958  59 
section "map_of"; 
60 

61 
Goal "map_of xs k = Some y > (k,y):set xs"; 

62 
by (induct_tac "xs" 1); 

63 
by (Simp_tac 1); 

64 
by (split_all_tac 1); 

65 
by (Asm_simp_tac 1); 

66 
qed_spec_mp "map_of_SomeD"; 

67 

68 
Goal "[ map_of xs k = Some z; P z ] ==> map_of [(k,z):xs . P z] k = Some z"; 

7961  69 
by (rtac mp 1); 
70 
by (assume_tac 2); 

7958  71 
by (etac thin_rl 1); 
72 
by (induct_tac "xs" 1); 

73 
by Auto_tac; 

74 
qed "map_of_filter_in"; 

75 

8160
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

76 
Goal "finite (range (map_of l))"; 
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

77 
by (induct_tac "l" 1); 
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

78 
by (ALLGOALS (simp_tac (simpset() addsimps [image_constant]))); 
8254  79 
by (rtac finite_subset 1); 
80 
by (assume_tac 2); 

8160
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

81 
by Auto_tac; 
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

82 
qed "finite_range_map_of"; 
7958  83 

84 
section "option_map related"; 

4990  85 

8529  86 
Goal "option_map f o empty = empty"; 
87 
by (rtac ext 1); 

88 
by (Simp_tac 1); 

89 
qed "option_map_o_empty"; 

4990  90 

8529  91 
Goal "option_map f o m(a>b) = (option_map f o m)(a>f b)"; 
92 
by (rtac ext 1); 

93 
by (Simp_tac 1); 

94 
qed "option_map_o_map_upd"; 

95 

5195  96 
Addsimps[option_map_o_empty, option_map_o_map_upd]; 
4883  97 

3981  98 
section "++"; 
99 

5069  100 
Goalw [override_def] "m ++ empty = m"; 
4423  101 
by (Simp_tac 1); 
3981  102 
qed "override_empty"; 
103 
Addsimps [override_empty]; 

104 

5069  105 
Goalw [override_def] "empty ++ m = m"; 
4423  106 
by (Simp_tac 1); 
107 
by (rtac ext 1); 

5183  108 
by (split_tac [option.split] 1); 
4423  109 
by (Simp_tac 1); 
3981  110 
qed "empty_override"; 
111 
Addsimps [empty_override]; 

112 

5069  113 
Goalw [override_def] 
3981  114 
"((m ++ n) k = Some x) = (n k = Some x  n k = None & m k = Some x)"; 
5183  115 
by (simp_tac (simpset() addsplits [option.split]) 1); 
3981  116 
qed_spec_mp "override_Some_iff"; 
117 

4926  118 
bind_thm ("override_SomeD", standard(override_Some_iff RS iffD1)); 
5444  119 
AddSDs[override_SomeD]; 
3981  120 

7958  121 
Goal "!!xx. n k = Some xx ==> (m ++ n) k = Some xx"; 
122 
by (stac override_Some_iff 1); 

123 
by (Fast_tac 1); 

124 
qed "override_find_right"; 

125 
Addsimps[override_find_right]; 

126 

5444  127 
Goalw [override_def] "((m ++ n) k = None) = (n k = None & m k = None)"; 
5183  128 
by (simp_tac (simpset() addsplits [option.split]) 1); 
3981  129 
qed "override_None"; 
130 
AddIffs [override_None]; 

131 

8160
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

132 
Goalw [override_def] "f ++ g(x>y) = (f ++ g)(x>y)"; 
8254  133 
by (rtac ext 1); 
8160
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

134 
by (auto_tac (claset_of Map.thy, simpset_of Map.thy)); 
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

135 
qed "override_upd"; 
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

136 
Addsimps[override_upd]; 
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

137 

5444  138 
Goalw [override_def] "map_of ys ++ map_of xs = map_of (xs@ys)"; 
139 
by (rtac sym 1); 

4423  140 
by (induct_tac "xs" 1); 
141 
by (Simp_tac 1); 

142 
by (rtac ext 1); 

5183  143 
by (asm_simp_tac (simpset() addsplits [option.split]) 1); 
5444  144 
qed "map_of_override"; 
145 
Addsimps [map_of_override]; 

3981  146 

8160
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

147 
Delsimps[fun_upd_apply]; 
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

148 
Goal "finite (range f) ==> finite (range (f ++ map_of l))"; 
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

149 
by (induct_tac "l" 1); 
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

150 
by Auto_tac; 
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

151 
by (fold_goals_tac [empty_def]); 
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

152 
by (Asm_simp_tac 1); 
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

153 
by (etac finite_range_updI 1); 
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

154 
qed "finite_range_map_of_override"; 
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

155 
Addsimps [fun_upd_apply]; 
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

156 

5300  157 

3981  158 
section "dom"; 
159 

8259  160 
Goalw [dom_def] "m a = Some b ==> a : dom m"; 
161 
by Auto_tac; 

162 
qed "domI"; 

163 

164 
Goalw [dom_def] "a : dom m ==> ? b. m a = Some b"; 

165 
by Auto_tac; 

166 
qed "domD"; 

167 
AddSDs [domD]; 

168 

5069  169 
Goalw [dom_def] "dom empty = {}"; 
4423  170 
by (Simp_tac 1); 
3981  171 
qed "dom_empty"; 
172 
Addsimps [dom_empty]; 

173 

5300  174 
Goalw [dom_def] "dom(m(a>b)) = insert a (dom m)"; 
4686  175 
by (Simp_tac 1); 
4423  176 
by (Blast_tac 1); 
5195  177 
qed "dom_map_upd"; 
178 
Addsimps [dom_map_upd]; 

3981  179 

8529  180 
Goalw [dom_def] "finite (dom (map_of l))"; 
181 
by (induct_tac "l" 1); 

182 
by (auto_tac (claset(), 

183 
simpset() addsimps [insert_Collect RS sym])); 

184 
qed "finite_dom_map_of"; 

4883  185 

5069  186 
Goalw [dom_def] "dom(m++n) = dom n Un dom m"; 
8529  187 
by Auto_tac; 
3981  188 
qed "dom_override"; 
189 
Addsimps [dom_override]; 

190 

191 
section "ran"; 

192 

5069  193 
Goalw [ran_def] "ran empty = {}"; 
4423  194 
by (Simp_tac 1); 
3981  195 
qed "ran_empty"; 
196 
Addsimps [ran_empty]; 

4883  197 

8160
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

198 
Goalw [ran_def] "ran (%u. None) = {}"; 
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

199 
by Auto_tac; 
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

200 
qed "ran_empty'"; 
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

201 
Addsimps[ran_empty']; 
837a6b515005
added finite_range_updI, finite_range_map_of, finite_range_map_of_override
oheimb
parents:
7961
diff
changeset

202 

5300  203 
Goalw [ran_def] "m a = None ==> ran(m(a>b)) = insert b (ran m)"; 
4883  204 
by Auto_tac; 
205 
by (subgoal_tac "~(aa = a)" 1); 

206 
by Auto_tac; 

5195  207 
qed "ran_map_upd"; 
208 
Addsimps [ran_map_upd]; 