author  huffman 
Wed, 24 Oct 2012 18:43:25 +0200  
changeset 49975  faf4afed009f 
parent 49973  e84baadd4963 
child 51161  6ed12ae3b3e1 
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 

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

8 
imports Main 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 
49975
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
49973
diff
changeset

64 
 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

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

66 

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

67 
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

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

69 

29708  70 
subsection {* Properties *} 
71 

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

74 

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

76 
by transfer simp 

77 

78 
lemma lookup_empty: "lookup empty k = None" 

79 
by transfer simp 

80 

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

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

83 
by transfer (auto simp add: is_none_def) 
29708  84 

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

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

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

87 
by (induct ks) (auto simp add: tabulate_def restrict_map_def) 
29826  88 

29708  89 
lemma update_update: 
90 
"update k v (update k w m) = update k v m" 

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

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

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

96 
by transfer simp 
29708  97 

98 
lemma delete_update: 

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

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

101 
by (transfer, simp add: fun_upd_twist)+ 
29708  102 

35157  103 
lemma delete_empty [simp]: 
104 
"delete k empty = empty" 

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

105 
by transfer simp 
29708  106 

35157  107 
lemma replace_update: 
37052  108 
"k \<notin> keys m \<Longrightarrow> replace k v m = m" 
109 
"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

110 
by (transfer, auto simp add: replace_def fun_upd_twist)+ 
29708  111 

112 
lemma size_empty [simp]: 

113 
"size empty = 0" 

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

114 
unfolding size_def by transfer simp 
29708  115 

116 
lemma size_update: 

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

119 
unfolding size_def by transfer (auto simp add: insert_dom) 
29708  120 

121 
lemma size_delete: 

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

123 
unfolding size_def by transfer simp 
29708  124 

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

127 
unfolding size_def by transfer (auto simp add: tabulate_alt_def card_set comp_def) 
29708  128 

29831  129 
lemma bulkload_tabulate: 
29826  130 
"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

131 
by transfer (auto simp add: tabulate_alt_def) 
29826  132 

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

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

135 
unfolding is_empty_def by transfer simp 
37052  136 

137 
lemma is_empty_update [simp]: 

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

139 
unfolding is_empty_def by transfer simp 
37052  140 

141 
lemma is_empty_delete: 

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

143 
unfolding is_empty_def by transfer (auto simp del: dom_eq_empty_conv) 
37052  144 

145 
lemma is_empty_replace [simp]: 

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

147 
unfolding is_empty_def replace_def by transfer auto 
37052  148 

149 
lemma is_empty_default [simp]: 

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

151 
unfolding is_empty_def default_def by transfer auto 
37052  152 

153 
lemma is_empty_map_entry [simp]: 

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

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

156 
apply transfer by (case_tac "m k") auto 
37052  157 

158 
lemma is_empty_map_default [simp]: 

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

160 
by (simp add: map_default_def) 

161 

162 
lemma keys_empty [simp]: 

163 
"keys empty = {}" 

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

164 
by transfer simp 
37052  165 

166 
lemma keys_update [simp]: 

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

168 
by transfer simp 
37052  169 

170 
lemma keys_delete [simp]: 

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

172 
by transfer simp 
37052  173 

174 
lemma keys_replace [simp]: 

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

176 
unfolding replace_def by transfer (simp add: insert_absorb) 
37052  177 

178 
lemma keys_default [simp]: 

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

180 
unfolding default_def by transfer (simp add: insert_absorb) 
37052  181 

182 
lemma keys_map_entry [simp]: 

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

184 
apply transfer by (case_tac "m k") auto 
37052  185 

186 
lemma keys_map_default [simp]: 

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

188 
by (simp add: map_default_def) 

189 

190 
lemma keys_tabulate [simp]: 

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

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

192 
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

193 

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

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

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

197 

37052  198 
lemma distinct_ordered_keys [simp]: 
199 
"distinct (ordered_keys m)" 

200 
by (simp add: ordered_keys_def) 

201 

202 
lemma ordered_keys_infinite [simp]: 

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

204 
by (simp add: ordered_keys_def) 

205 

206 
lemma ordered_keys_empty [simp]: 

207 
"ordered_keys empty = []" 

208 
by (simp add: ordered_keys_def) 

209 

210 
lemma ordered_keys_update [simp]: 

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

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

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

214 

215 
lemma ordered_keys_delete [simp]: 

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

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

218 
case False then show ?thesis by simp 

219 
next 

220 
case True note fin = True 

221 
show ?thesis 

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

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

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

225 
next 

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

227 
qed 

228 
qed 

229 

230 
lemma ordered_keys_replace [simp]: 

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

232 
by (simp add: replace_def) 

233 

234 
lemma ordered_keys_default [simp]: 

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

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

237 
by (simp_all add: default_def) 

238 

239 
lemma ordered_keys_map_entry [simp]: 

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

241 
by (simp add: ordered_keys_def) 

242 

243 
lemma ordered_keys_map_default [simp]: 

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

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

246 
by (simp_all add: map_default_def) 

247 

248 
lemma ordered_keys_tabulate [simp]: 

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

250 
by (simp add: ordered_keys_def sorted_list_of_set_sort_remdups) 

251 

252 
lemma ordered_keys_bulkload [simp]: 

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

254 
by (simp add: ordered_keys_def) 

36110  255 

31459  256 

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

257 
subsection {* Code generator setup *} 
31459  258 

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

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

260 

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

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

262 
begin 
31459  263 

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

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

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

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

267 
qed(transfer, rule) 
31459  268 

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

269 
end 
31459  270 

35157  271 

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

272 
hide_const (open) empty is_empty rep lookup update delete ordered_keys keys size 
40605  273 
replace default map_entry map_default tabulate bulkload map 
35157  274 

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

275 
end 