author  kuncar 
Fri, 08 Mar 2013 13:21:58 +0100  
changeset 51379  6dd83e007f56 
parent 51375  d9e62d9c98de 
child 53013  3fbcfa911863 
permissions  rwrr 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

1 
(* Title: HOL/Library/Mapping.thy 
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

2 
Author: Florian Haftmann and Ondrej Kuncar 
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

3 
*) 
29708  4 

5 
header {* An abstract view on maps for code generation. *} 

6 

7 
theory Mapping 

51375
d9e62d9c98de
patch Isabelle ditribution to conform to changes regarding the parametricity
kuncar
parents:
51161
diff
changeset

8 
imports Main Quotient_Option Quotient_List 
29708  9 
begin 
10 

51379  11 
subsection {* Parametricity transfer rules *} 
12 

13 
lemma empty_transfer: "(A ===> option_rel B) Map.empty Map.empty" by transfer_prover 

14 

15 
lemma lookup_transfer: "((A ===> B) ===> A ===> B) (\<lambda>m k. m k) (\<lambda>m k. m k)" by transfer_prover 

16 

17 
lemma update_transfer: 

18 
assumes [transfer_rule]: "bi_unique A" 

19 
shows "(A ===> B ===> (A ===> option_rel B) ===> A ===> option_rel B) 

20 
(\<lambda>k v m. m(k \<mapsto> v)) (\<lambda>k v m. m(k \<mapsto> v))" 

21 
by transfer_prover 

22 

23 
lemma delete_transfer: 

24 
assumes [transfer_rule]: "bi_unique A" 

25 
shows "(A ===> (A ===> option_rel B) ===> A ===> option_rel B) 

26 
(\<lambda>k m. m(k := None)) (\<lambda>k m. m(k := None))" 

27 
by transfer_prover 

28 

29 
definition equal_None :: "'a option \<Rightarrow> bool" where "equal_None x \<equiv> x = None" 

30 

31 
lemma [transfer_rule]: "(option_rel A ===> op=) equal_None equal_None" 

32 
unfolding fun_rel_def option_rel_unfold equal_None_def by (auto split: option.split) 

33 

34 
lemma dom_transfer: 

35 
assumes [transfer_rule]: "bi_total A" 

36 
shows "((A ===> option_rel B) ===> set_rel A) dom dom" 

37 
unfolding dom_def[abs_def] equal_None_def[symmetric] 

38 
by transfer_prover 

39 

40 
lemma map_of_transfer [transfer_rule]: 

41 
assumes [transfer_rule]: "bi_unique R1" 

42 
shows "(list_all2 (prod_rel R1 R2) ===> R1 ===> option_rel R2) map_of map_of" 

43 
unfolding map_of_def by transfer_prover 

44 

45 
lemma tabulate_transfer: 

46 
assumes [transfer_rule]: "bi_unique A" 

47 
shows "(list_all2 A ===> (A ===> B) ===> A ===> option_rel B) 

48 
(\<lambda>ks f. (map_of (List.map (\<lambda>k. (k, f k)) ks))) (\<lambda>ks f. (map_of (List.map (\<lambda>k. (k, f k)) ks)))" 

49 
by transfer_prover 

50 

51 
lemma bulkload_transfer: 

52 
"(list_all2 A ===> op= ===> option_rel A) 

53 
(\<lambda>xs k. if k < length xs then Some (xs ! k) else None) (\<lambda>xs k. if k < length xs then Some (xs ! k) else None)" 

54 
unfolding fun_rel_def 

55 
apply clarsimp 

56 
apply (erule list_all2_induct) 

57 
apply simp 

58 
apply (case_tac xa) 

59 
apply simp 

60 
by (auto dest: list_all2_lengthD list_all2_nthD) 

61 

62 
lemma map_transfer: 

63 
"((A ===> B) ===> (C ===> D) ===> (B ===> option_rel C) ===> A ===> option_rel D) 

64 
(\<lambda>f g m. (Option.map g \<circ> m \<circ> f)) (\<lambda>f g m. (Option.map g \<circ> m \<circ> f))" 

65 
by transfer_prover 

66 

67 
lemma map_entry_transfer: 

68 
assumes [transfer_rule]: "bi_unique A" 

69 
shows "(A ===> (B ===> B) ===> (A ===> option_rel B) ===> A ===> option_rel B) 

70 
(\<lambda>k f m. (case m k of None \<Rightarrow> m 

71 
 Some v \<Rightarrow> m (k \<mapsto> (f v)))) (\<lambda>k f m. (case m k of None \<Rightarrow> m 

72 
 Some v \<Rightarrow> m (k \<mapsto> (f v))))" 

73 
by transfer_prover 

74 

29708  75 
subsection {* Type definition and primitive operations *} 
76 

49834  77 
typedef ('a, 'b) mapping = "UNIV :: ('a \<rightharpoonup> 'b) set" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

78 
morphisms rep Mapping .. 
37700
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

79 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

80 
setup_lifting(no_code) type_definition_mapping 
37700
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

81 

51379  82 
lift_definition empty :: "('a, 'b) mapping" is Map.empty parametric empty_transfer . 
37700
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

83 

51379  84 
lift_definition lookup :: "('a, 'b) mapping \<Rightarrow> 'a \<Rightarrow> 'b option" is "\<lambda>m k. m k" 
85 
parametric lookup_transfer . 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

86 

51379  87 
lift_definition update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" is "\<lambda>k v m. m(k \<mapsto> v)" 
88 
parametric update_transfer . 

37700
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

89 

51379  90 
lift_definition delete :: "'a \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" is "\<lambda>k m. m(k := None)" 
91 
parametric delete_transfer . 

39380
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset

92 

51379  93 
lift_definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set" is dom parametric dom_transfer . 
29708  94 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

95 
lift_definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping" is 
51379  96 
"\<lambda>ks f. (map_of (List.map (\<lambda>k. (k, f k)) ks))" parametric tabulate_transfer . 
29708  97 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

98 
lift_definition bulkload :: "'a list \<Rightarrow> (nat, 'a) mapping" is 
51379  99 
"\<lambda>xs k. if k < length xs then Some (xs ! k) else None" parametric bulkload_transfer . 
29708  100 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

101 
lift_definition map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('c, 'd) mapping" is 
51379  102 
"\<lambda>f g m. (Option.map g \<circ> m \<circ> f)" parametric map_transfer . 
29708  103 

51161
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset

104 

40605  105 
subsection {* Functorial structure *} 
106 

41505
6d19301074cf
"enriched_type" replaces less specific "type_lifting"
haftmann
parents:
41372
diff
changeset

107 
enriched_type map: map 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

108 
by (transfer, auto simp add: fun_eq_iff Option.map.compositionality Option.map.id)+ 
40605  109 

51161
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset

110 

29708  111 
subsection {* Derived operations *} 
112 

35194  113 
definition ordered_keys :: "('a\<Colon>linorder, 'b) mapping \<Rightarrow> 'a list" where 
37052  114 
"ordered_keys m = (if finite (keys m) then sorted_list_of_set (keys m) else [])" 
35194  115 

35157  116 
definition is_empty :: "('a, 'b) mapping \<Rightarrow> bool" where 
37052  117 
"is_empty m \<longleftrightarrow> keys m = {}" 
35157  118 

119 
definition size :: "('a, 'b) mapping \<Rightarrow> nat" where 

37052  120 
"size m = (if finite (keys m) then card (keys m) else 0)" 
35157  121 

122 
definition replace :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where 

37052  123 
"replace k v m = (if k \<in> keys m then update k v m else m)" 
29814  124 

37026
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

125 
definition default :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where 
37052  126 
"default k v m = (if k \<in> keys m then m else update k v m)" 
37026
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

127 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

128 
lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" is 
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

129 
"\<lambda>k f m. (case m k of None \<Rightarrow> m 
51379  130 
 Some v \<Rightarrow> m (k \<mapsto> (f v)))" parametric map_entry_transfer . 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

131 

70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

132 
lemma map_entry_code [code]: "map_entry k f m = (case lookup m k of None \<Rightarrow> m 
49975
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
49973
diff
changeset

133 
 Some v \<Rightarrow> update k (f v) m)" 
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
49973
diff
changeset

134 
by transfer rule 
37026
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

135 

7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

136 
definition map_default :: "'a \<Rightarrow> 'b \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where 
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

137 
"map_default k v f m = map_entry k f (default k v m)" 
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

138 

51379  139 
lift_definition assoc_list_to_mapping :: "('k \<times> 'v) list \<Rightarrow> ('k, 'v) mapping" 
140 
is map_of parametric map_of_transfer . 

141 

142 
lemma assoc_list_to_mapping_code [code]: 

143 
"assoc_list_to_mapping xs = foldr (\<lambda>(k, v) m. update k v m) xs empty" 

144 
by transfer(simp add: map_add_map_of_foldr[symmetric]) 

145 

51161
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset

146 
instantiation mapping :: (type, type) equal 
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset

147 
begin 
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset

148 

6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset

149 
definition 
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset

150 
"HOL.equal m1 m2 \<longleftrightarrow> (\<forall>k. lookup m1 k = lookup m2 k)" 
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset

151 

6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset

152 
instance proof 
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset

153 
qed (unfold equal_mapping_def, transfer, auto) 
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset

154 

6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset

155 
end 
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset

156 

6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset

157 
lemma [transfer_rule]: 
51379  158 
assumes [transfer_rule]: "bi_total A" 
159 
assumes [transfer_rule]: "bi_unique B" 

160 
shows "fun_rel (pcr_mapping A B) (fun_rel (pcr_mapping A B) HOL.iff) HOL.eq HOL.equal" 

161 
by (unfold equal) transfer_prover 

51161
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset

162 

6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset

163 

29708  164 
subsection {* Properties *} 
165 

49973  166 
lemma lookup_update: "lookup (update k v m) k = Some v" 
167 
by transfer simp 

168 

169 
lemma lookup_update_neq: "k \<noteq> k' \<Longrightarrow> lookup (update k v m) k' = lookup m k'" 

170 
by transfer simp 

171 

172 
lemma lookup_empty: "lookup empty k = None" 

173 
by transfer simp 

174 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

175 
lemma keys_is_none_rep [code_unfold]: 
37052  176 
"k \<in> keys m \<longleftrightarrow> \<not> (Option.is_none (lookup m k))" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

177 
by transfer (auto simp add: is_none_def) 
29708  178 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

179 
lemma tabulate_alt_def: 
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

180 
"map_of (List.map (\<lambda>k. (k, f k)) ks) = (Some o f) ` set ks" 
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

181 
by (induct ks) (auto simp add: tabulate_def restrict_map_def) 
29826  182 

29708  183 
lemma update_update: 
184 
"update k v (update k w m) = update k v m" 

185 
"k \<noteq> l \<Longrightarrow> update k v (update l w m) = update l w (update k v m)" 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

186 
by (transfer, simp add: fun_upd_twist)+ 
29708  187 

35157  188 
lemma update_delete [simp]: 
189 
"update k v (delete k m) = update k v m" 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

190 
by transfer simp 
29708  191 

192 
lemma delete_update: 

193 
"delete k (update k v m) = delete k m" 

194 
"k \<noteq> l \<Longrightarrow> delete k (update l v m) = update l v (delete k m)" 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

195 
by (transfer, simp add: fun_upd_twist)+ 
29708  196 

35157  197 
lemma delete_empty [simp]: 
198 
"delete k empty = empty" 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

199 
by transfer simp 
29708  200 

35157  201 
lemma replace_update: 
37052  202 
"k \<notin> keys m \<Longrightarrow> replace k v m = m" 
203 
"k \<in> keys m \<Longrightarrow> replace k v m = update k v m" 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

204 
by (transfer, auto simp add: replace_def fun_upd_twist)+ 
29708  205 

206 
lemma size_empty [simp]: 

207 
"size empty = 0" 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

208 
unfolding size_def by transfer simp 
29708  209 

210 
lemma size_update: 

37052  211 
"finite (keys m) \<Longrightarrow> size (update k v m) = 
212 
(if k \<in> keys m then size m else Suc (size m))" 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

213 
unfolding size_def by transfer (auto simp add: insert_dom) 
29708  214 

215 
lemma size_delete: 

37052  216 
"size (delete k m) = (if k \<in> keys m then size m  1 else size m)" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

217 
unfolding size_def by transfer simp 
29708  218 

37052  219 
lemma size_tabulate [simp]: 
29708  220 
"size (tabulate ks f) = length (remdups ks)" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

221 
unfolding size_def by transfer (auto simp add: tabulate_alt_def card_set comp_def) 
29708  222 

29831  223 
lemma bulkload_tabulate: 
29826  224 
"bulkload xs = tabulate [0..<length xs] (nth xs)" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

225 
by transfer (auto simp add: tabulate_alt_def) 
29826  226 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

227 
lemma is_empty_empty [simp]: 
37052  228 
"is_empty empty" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

229 
unfolding is_empty_def by transfer simp 
37052  230 

231 
lemma is_empty_update [simp]: 

232 
"\<not> is_empty (update k v m)" 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

233 
unfolding is_empty_def by transfer simp 
37052  234 

235 
lemma is_empty_delete: 

236 
"is_empty (delete k m) \<longleftrightarrow> is_empty m \<or> keys m = {k}" 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

237 
unfolding is_empty_def by transfer (auto simp del: dom_eq_empty_conv) 
37052  238 

239 
lemma is_empty_replace [simp]: 

240 
"is_empty (replace k v m) \<longleftrightarrow> is_empty m" 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

241 
unfolding is_empty_def replace_def by transfer auto 
37052  242 

243 
lemma is_empty_default [simp]: 

244 
"\<not> is_empty (default k v m)" 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

245 
unfolding is_empty_def default_def by transfer auto 
37052  246 

247 
lemma is_empty_map_entry [simp]: 

248 
"is_empty (map_entry k f m) \<longleftrightarrow> is_empty m" 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

249 
unfolding is_empty_def 
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

250 
apply transfer by (case_tac "m k") auto 
37052  251 

252 
lemma is_empty_map_default [simp]: 

253 
"\<not> is_empty (map_default k v f m)" 

254 
by (simp add: map_default_def) 

255 

256 
lemma keys_empty [simp]: 

257 
"keys empty = {}" 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

258 
by transfer simp 
37052  259 

260 
lemma keys_update [simp]: 

261 
"keys (update k v m) = insert k (keys m)" 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

262 
by transfer simp 
37052  263 

264 
lemma keys_delete [simp]: 

265 
"keys (delete k m) = keys m  {k}" 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

266 
by transfer simp 
37052  267 

268 
lemma keys_replace [simp]: 

269 
"keys (replace k v m) = keys m" 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

270 
unfolding replace_def by transfer (simp add: insert_absorb) 
37052  271 

272 
lemma keys_default [simp]: 

273 
"keys (default k v m) = insert k (keys m)" 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

274 
unfolding default_def by transfer (simp add: insert_absorb) 
37052  275 

276 
lemma keys_map_entry [simp]: 

277 
"keys (map_entry k f m) = keys m" 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

278 
apply transfer by (case_tac "m k") auto 
37052  279 

280 
lemma keys_map_default [simp]: 

281 
"keys (map_default k v f m) = insert k (keys m)" 

282 
by (simp add: map_default_def) 

283 

284 
lemma keys_tabulate [simp]: 

37026
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

285 
"keys (tabulate ks f) = set ks" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

286 
by transfer (simp add: map_of_map_restrict o_def) 
37026
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

287 

37052  288 
lemma keys_bulkload [simp]: 
37026
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

289 
"keys (bulkload xs) = {0..<length xs}" 
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

290 
by (simp add: keys_tabulate bulkload_tabulate) 
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

291 

37052  292 
lemma distinct_ordered_keys [simp]: 
293 
"distinct (ordered_keys m)" 

294 
by (simp add: ordered_keys_def) 

295 

296 
lemma ordered_keys_infinite [simp]: 

297 
"\<not> finite (keys m) \<Longrightarrow> ordered_keys m = []" 

298 
by (simp add: ordered_keys_def) 

299 

300 
lemma ordered_keys_empty [simp]: 

301 
"ordered_keys empty = []" 

302 
by (simp add: ordered_keys_def) 

303 

304 
lemma ordered_keys_update [simp]: 

305 
"k \<in> keys m \<Longrightarrow> ordered_keys (update k v m) = ordered_keys m" 

306 
"finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow> ordered_keys (update k v m) = insort k (ordered_keys m)" 

307 
by (simp_all add: ordered_keys_def) (auto simp only: sorted_list_of_set_insert [symmetric] insert_absorb) 

308 

309 
lemma ordered_keys_delete [simp]: 

310 
"ordered_keys (delete k m) = remove1 k (ordered_keys m)" 

311 
proof (cases "finite (keys m)") 

312 
case False then show ?thesis by simp 

313 
next 

314 
case True note fin = True 

315 
show ?thesis 

316 
proof (cases "k \<in> keys m") 

317 
case False with fin have "k \<notin> set (sorted_list_of_set (keys m))" by simp 

318 
with False show ?thesis by (simp add: ordered_keys_def remove1_idem) 

319 
next 

320 
case True with fin show ?thesis by (simp add: ordered_keys_def sorted_list_of_set_remove) 

321 
qed 

322 
qed 

323 

324 
lemma ordered_keys_replace [simp]: 

325 
"ordered_keys (replace k v m) = ordered_keys m" 

326 
by (simp add: replace_def) 

327 

328 
lemma ordered_keys_default [simp]: 

329 
"k \<in> keys m \<Longrightarrow> ordered_keys (default k v m) = ordered_keys m" 

330 
"finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow> ordered_keys (default k v m) = insort k (ordered_keys m)" 

331 
by (simp_all add: default_def) 

332 

333 
lemma ordered_keys_map_entry [simp]: 

334 
"ordered_keys (map_entry k f m) = ordered_keys m" 

335 
by (simp add: ordered_keys_def) 

336 

337 
lemma ordered_keys_map_default [simp]: 

338 
"k \<in> keys m \<Longrightarrow> ordered_keys (map_default k v f m) = ordered_keys m" 

339 
"finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow> ordered_keys (map_default k v f m) = insort k (ordered_keys m)" 

340 
by (simp_all add: map_default_def) 

341 

342 
lemma ordered_keys_tabulate [simp]: 

343 
"ordered_keys (tabulate ks f) = sort (remdups ks)" 

344 
by (simp add: ordered_keys_def sorted_list_of_set_sort_remdups) 

345 

346 
lemma ordered_keys_bulkload [simp]: 

347 
"ordered_keys (bulkload ks) = [0..<length ks]" 

348 
by (simp add: ordered_keys_def) 

36110  349 

31459  350 

37700
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

351 
subsection {* Code generator setup *} 
31459  352 

37701
411717732710
explicit code_datatype declaration prevents multiple instantiations later on
haftmann
parents:
37700
diff
changeset

353 
code_datatype empty update 
411717732710
explicit code_datatype declaration prevents multiple instantiations later on
haftmann
parents:
37700
diff
changeset

354 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

355 
hide_const (open) empty is_empty rep lookup update delete ordered_keys keys size 
40605  356 
replace default map_entry map_default tabulate bulkload map 
35157  357 

49975
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
49973
diff
changeset

358 
end 
51161
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49975
diff
changeset

359 

51379  360 