author  kuncar 
Thu, 18 Oct 2012 15:52:33 +0200  
changeset 49929  70300f1b6835 
parent 49834  b27bbb021df1 
child 49939  eb8b434158c8 
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 

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

8 
imports Main "~~/src/HOL/Library/Quotient_Option" 
29708  9 
begin 
10 

11 
subsection {* Type definition and primitive operations *} 

12 

49834  13 
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

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

15 

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

16 
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

17 

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

18 
lift_definition empty :: "('a, 'b) mapping" is "(\<lambda>_. None)" . 
37700
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

19 

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

20 
lift_definition lookup :: "('a, 'b) mapping \<Rightarrow> 'a \<Rightarrow> 'b option" is "\<lambda>m k. m k" . 
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

21 

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

22 
lift_definition update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" is "\<lambda>k v m. m(k \<mapsto> v)" . 
37700
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

23 

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

24 
lift_definition delete :: "'a \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" is "\<lambda>k m. m(k := None)" . 
39380
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset

25 

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

26 
lift_definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set" is dom . 
29708  27 

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

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

29 
"\<lambda>ks f. (map_of (List.map (\<lambda>k. (k, f k)) ks))" . 
29708  30 

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

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

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

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

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

35 
"\<lambda>f g m. (Option.map g \<circ> m \<circ> f)" . 
29708  36 

40605  37 
subsection {* Functorial structure *} 
38 

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

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

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

29708  42 
subsection {* Derived operations *} 
43 

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

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

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

37052  51 
"size m = (if finite (keys m) then card (keys m) else 0)" 
35157  52 

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

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

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

56 
definition default :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where 
37052  57 
"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

58 

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

59 
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

60 
"\<lambda>k f m. (case m k of None \<Rightarrow> m 
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

61 
 Some v \<Rightarrow> m (k \<mapsto> (f v)))" . 
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

62 

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

63 
lemma map_entry_code [code]: "map_entry k f m = (case lookup m k of None \<Rightarrow> m 
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
49834
diff
changeset

64 
 Some v \<Rightarrow> update k (f v) m)" by transfer rule 
37026
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

65 

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

66 
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

67 
"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

68 

29708  69 
subsection {* Properties *} 
70 

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

71 
lemma keys_is_none_rep [code_unfold]: 
37052  72 
"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

73 
by transfer (auto simp add: is_none_def) 
29708  74 

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

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

76 
"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

77 
by (induct ks) (auto simp add: tabulate_def restrict_map_def) 
29826  78 

29708  79 
lemma update_update: 
80 
"update k v (update k w m) = update k v m" 

81 
"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

82 
by (transfer, simp add: fun_upd_twist)+ 
29708  83 

35157  84 
lemma update_delete [simp]: 
85 
"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

86 
by transfer simp 
29708  87 

88 
lemma delete_update: 

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

90 
"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

91 
by (transfer, simp add: fun_upd_twist)+ 
29708  92 

35157  93 
lemma delete_empty [simp]: 
94 
"delete k empty = empty" 

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

95 
by transfer simp 
29708  96 

35157  97 
lemma replace_update: 
37052  98 
"k \<notin> keys m \<Longrightarrow> replace k v m = m" 
99 
"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

100 
by (transfer, auto simp add: replace_def fun_upd_twist)+ 
29708  101 

102 
lemma size_empty [simp]: 

103 
"size empty = 0" 

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

104 
unfolding size_def by transfer simp 
29708  105 

106 
lemma size_update: 

37052  107 
"finite (keys m) \<Longrightarrow> size (update k v m) = 
108 
(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

109 
unfolding size_def by transfer (auto simp add: insert_dom) 
29708  110 

111 
lemma size_delete: 

37052  112 
"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

113 
unfolding size_def by transfer simp 
29708  114 

37052  115 
lemma size_tabulate [simp]: 
29708  116 
"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

117 
unfolding size_def by transfer (auto simp add: tabulate_alt_def card_set comp_def) 
29708  118 

29831  119 
lemma bulkload_tabulate: 
29826  120 
"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

121 
by transfer (auto simp add: tabulate_alt_def) 
29826  122 

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

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

125 
unfolding is_empty_def by transfer simp 
37052  126 

127 
lemma is_empty_update [simp]: 

128 
"\<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

129 
unfolding is_empty_def by transfer simp 
37052  130 

131 
lemma is_empty_delete: 

132 
"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

133 
unfolding is_empty_def by transfer (auto simp del: dom_eq_empty_conv) 
37052  134 

135 
lemma is_empty_replace [simp]: 

136 
"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

137 
unfolding is_empty_def replace_def by transfer auto 
37052  138 

139 
lemma is_empty_default [simp]: 

140 
"\<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

141 
unfolding is_empty_def default_def by transfer auto 
37052  142 

143 
lemma is_empty_map_entry [simp]: 

144 
"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

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

146 
apply transfer by (case_tac "m k") auto 
37052  147 

148 
lemma is_empty_map_default [simp]: 

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

150 
by (simp add: map_default_def) 

151 

152 
lemma keys_empty [simp]: 

153 
"keys empty = {}" 

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

154 
by transfer simp 
37052  155 

156 
lemma keys_update [simp]: 

157 
"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

158 
by transfer simp 
37052  159 

160 
lemma keys_delete [simp]: 

161 
"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

162 
by transfer simp 
37052  163 

164 
lemma keys_replace [simp]: 

165 
"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

166 
unfolding replace_def by transfer (simp add: insert_absorb) 
37052  167 

168 
lemma keys_default [simp]: 

169 
"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

170 
unfolding default_def by transfer (simp add: insert_absorb) 
37052  171 

172 
lemma keys_map_entry [simp]: 

173 
"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

174 
apply transfer by (case_tac "m k") auto 
37052  175 

176 
lemma keys_map_default [simp]: 

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

178 
by (simp add: map_default_def) 

179 

180 
lemma keys_tabulate [simp]: 

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

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

182 
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

183 

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

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

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

187 

37052  188 
lemma distinct_ordered_keys [simp]: 
189 
"distinct (ordered_keys m)" 

190 
by (simp add: ordered_keys_def) 

191 

192 
lemma ordered_keys_infinite [simp]: 

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

194 
by (simp add: ordered_keys_def) 

195 

196 
lemma ordered_keys_empty [simp]: 

197 
"ordered_keys empty = []" 

198 
by (simp add: ordered_keys_def) 

199 

200 
lemma ordered_keys_update [simp]: 

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

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

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

204 

205 
lemma ordered_keys_delete [simp]: 

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

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

208 
case False then show ?thesis by simp 

209 
next 

210 
case True note fin = True 

211 
show ?thesis 

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

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

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

215 
next 

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

217 
qed 

218 
qed 

219 

220 
lemma ordered_keys_replace [simp]: 

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

222 
by (simp add: replace_def) 

223 

224 
lemma ordered_keys_default [simp]: 

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

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

227 
by (simp_all add: default_def) 

228 

229 
lemma ordered_keys_map_entry [simp]: 

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

231 
by (simp add: ordered_keys_def) 

232 

233 
lemma ordered_keys_map_default [simp]: 

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

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

236 
by (simp_all add: map_default_def) 

237 

238 
lemma ordered_keys_tabulate [simp]: 

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

240 
by (simp add: ordered_keys_def sorted_list_of_set_sort_remdups) 

241 

242 
lemma ordered_keys_bulkload [simp]: 

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

244 
by (simp add: ordered_keys_def) 

36110  245 

31459  246 

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

247 
subsection {* Code generator setup *} 
31459  248 

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

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

250 

38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37701
diff
changeset

251 
instantiation mapping :: (type, type) equal 
37700
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

252 
begin 
31459  253 

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

254 
lift_definition equal_mapping :: "('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping \<Rightarrow> bool" is "op=" . 
31459  255 

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

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

257 
qed(transfer, rule) 
31459  258 

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

259 
end 
31459  260 

35157  261 

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

262 
hide_const (open) empty is_empty rep lookup update delete ordered_keys keys size 
40605  263 
replace default map_entry map_default tabulate bulkload map 
35157  264 

29708  265 
end 