author  wenzelm 
Sun, 07 Jun 2015 12:43:06 +0200  
changeset 60373  68eb60fd22a6 
parent 58881  b9556a055632 
child 60500  903bb1495239 
permissions  rwrr 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset

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

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

3 
*) 
43124  4 

58881  5 
section {* Implementation of mappings with RedBlack Trees *} 
43124  6 

7 
(*<*) 

8 
theory RBT_Mapping 

9 
imports RBT Mapping 

10 
begin 

11 

12 
subsection {* Implementation of mappings *} 

13 

56019  14 
context includes rbt.lifting begin 
15 
lift_definition Mapping :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) mapping" is RBT.lookup . 

16 
end 

43124  17 

18 
code_datatype Mapping 

19 

56019  20 
context includes rbt.lifting begin 
21 

43124  22 
lemma lookup_Mapping [simp, code]: 
56019  23 
"Mapping.lookup (Mapping t) = RBT.lookup t" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset

24 
by (transfer fixing: t) rule 
43124  25 

56019  26 
lemma empty_Mapping [code]: "Mapping.empty = Mapping RBT.empty" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset

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

28 
note RBT.empty.transfer[transfer_rule del] 
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset

29 
show ?thesis by transfer simp 
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset

30 
qed 
43124  31 

32 
lemma is_empty_Mapping [code]: 

56019  33 
"Mapping.is_empty (Mapping t) \<longleftrightarrow> RBT.is_empty t" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset

34 
unfolding is_empty_def by (transfer fixing: t) simp 
43124  35 

36 
lemma insert_Mapping [code]: 

56019  37 
"Mapping.update k v (Mapping t) = Mapping (RBT.insert k v t)" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset

38 
by (transfer fixing: t) simp 
43124  39 

40 
lemma delete_Mapping [code]: 

56019  41 
"Mapping.delete k (Mapping t) = Mapping (RBT.delete k t)" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset

42 
by (transfer fixing: t) simp 
43124  43 

44 
lemma map_entry_Mapping [code]: 

56019  45 
"Mapping.map_entry k f (Mapping t) = Mapping (RBT.map_entry k f t)" 
46 
apply (transfer fixing: t) by (case_tac "RBT.lookup t k") auto 

43124  47 

48 
lemma keys_Mapping [code]: 

56019  49 
"Mapping.keys (Mapping t) = set (RBT.keys t)" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset

50 
by (transfer fixing: t) (simp add: lookup_keys) 
43124  51 

52 
lemma ordered_keys_Mapping [code]: 

56019  53 
"Mapping.ordered_keys (Mapping t) = RBT.keys t" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset

54 
unfolding ordered_keys_def 
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset

55 
by (transfer fixing: t) (auto simp add: lookup_keys intro: sorted_distinct_set_unique) 
43124  56 

57 
lemma Mapping_size_card_keys: (*FIXME*) 

58 
"Mapping.size m = card (Mapping.keys m)" 

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

59 
unfolding size_def by transfer simp 
43124  60 

61 
lemma size_Mapping [code]: 

56019  62 
"Mapping.size (Mapping t) = length (RBT.keys t)" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset

63 
unfolding size_def 
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset

64 
by (transfer fixing: t) (simp add: lookup_keys distinct_card) 
43124  65 

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

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

67 
notes RBT.bulkload.transfer[transfer_rule del] 
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset

68 
begin 
60373  69 

70 
lemma tabulate_Mapping [code]: 

71 
"Mapping.tabulate ks f = Mapping (RBT.bulkload (List.map (\<lambda>k. (k, f k)) ks))" 

72 
by transfer (simp add: map_of_map_restrict) 

73 

74 
lemma bulkload_Mapping [code]: 

75 
"Mapping.bulkload vs = Mapping (RBT.bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))" 

76 
by transfer (simp add: map_of_map_restrict fun_eq_iff) 

77 

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

78 
end 
43124  79 

80 
lemma equal_Mapping [code]: 

56019  81 
"HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> RBT.entries t1 = RBT.entries t2" 
51161
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49929
diff
changeset

82 
by (transfer fixing: t1 t2) (simp add: entries_lookup) 
43124  83 

84 
lemma [code nbe]: 

85 
"HOL.equal (x :: (_, _) mapping) x \<longleftrightarrow> True" 

86 
by (fact equal_refl) 

87 

56019  88 
end 
43124  89 

90 
(*>*) 

91 

92 
text {* 

93 
This theory defines abstract redblack trees as an efficient 

94 
representation of finite maps, backed by the implementation 

95 
in @{theory RBT_Impl}. 

96 
*} 

97 

98 
subsection {* Data type and invariant *} 

99 

100 
text {* 

101 
The type @{typ "('k, 'v) RBT_Impl.rbt"} denotes redblack trees with 

102 
keys of type @{typ "'k"} and values of type @{typ "'v"}. To function 

103 
properly, the key type musorted belong to the @{text "linorder"} 

104 
class. 

105 

106 
A value @{term t} of this type is a valid redblack tree if it 

107 
satisfies the invariant @{text "is_rbt t"}. The abstract type @{typ 

108 
"('k, 'v) rbt"} always obeys this invariant, and for this reason you 

109 
should only use this in our application. Going back to @{typ "('k, 

110 
'v) RBT_Impl.rbt"} may be necessary in proofs if not yet proven 

111 
properties about the operations must be established. 

112 

113 
The interpretation function @{const "RBT.lookup"} returns the partial 

114 
map represented by a redblack tree: 

115 
@{term_type[display] "RBT.lookup"} 

116 

117 
This function should be used for reasoning about the semantics of the RBT 

118 
operations. Furthermore, it implements the lookup functionality for 

119 
the data structure: It is executable and the lookup is performed in 

120 
$O(\log n)$. 

121 
*} 

122 

123 
subsection {* Operations *} 

124 

125 
text {* 

126 
Currently, the following operations are supported: 

127 

128 
@{term_type [display] "RBT.empty"} 

129 
Returns the empty tree. $O(1)$ 

130 

131 
@{term_type [display] "RBT.insert"} 

132 
Updates the map at a given position. $O(\log n)$ 

133 

134 
@{term_type [display] "RBT.delete"} 

135 
Deletes a map entry at a given position. $O(\log n)$ 

136 

137 
@{term_type [display] "RBT.entries"} 

138 
Return a corresponding keyvalue list for a tree. 

139 

140 
@{term_type [display] "RBT.bulkload"} 

141 
Builds a tree from a keyvalue list. 

142 

143 
@{term_type [display] "RBT.map_entry"} 

144 
Maps a single entry in a tree. 

145 

146 
@{term_type [display] "RBT.map"} 

147 
Maps all values in a tree. $O(n)$ 

148 

149 
@{term_type [display] "RBT.fold"} 

150 
Folds over all entries in a tree. $O(n)$ 

151 
*} 

152 

153 

154 
subsection {* Invariant preservation *} 

155 

156 
text {* 

157 
\noindent 

158 
@{thm Empty_is_rbt}\hfill(@{text "Empty_is_rbt"}) 

159 

160 
\noindent 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
43124
diff
changeset

161 
@{thm rbt_insert_is_rbt}\hfill(@{text "rbt_insert_is_rbt"}) 
43124  162 

163 
\noindent 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
43124
diff
changeset

164 
@{thm rbt_delete_is_rbt}\hfill(@{text "delete_is_rbt"}) 
43124  165 

166 
\noindent 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
43124
diff
changeset

167 
@{thm rbt_bulkload_is_rbt}\hfill(@{text "bulkload_is_rbt"}) 
43124  168 

169 
\noindent 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
43124
diff
changeset

170 
@{thm rbt_map_entry_is_rbt}\hfill(@{text "map_entry_is_rbt"}) 
43124  171 

172 
\noindent 

173 
@{thm map_is_rbt}\hfill(@{text "map_is_rbt"}) 

174 

175 
\noindent 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
43124
diff
changeset

176 
@{thm rbt_union_is_rbt}\hfill(@{text "union_is_rbt"}) 
43124  177 
*} 
178 

179 

180 
subsection {* Map Semantics *} 

181 

182 
text {* 

183 
\noindent 

184 
\underline{@{text "lookup_empty"}} 

185 
@{thm [display] lookup_empty} 

186 
\vspace{1ex} 

187 

188 
\noindent 

189 
\underline{@{text "lookup_insert"}} 

190 
@{thm [display] lookup_insert} 

191 
\vspace{1ex} 

192 

193 
\noindent 

194 
\underline{@{text "lookup_delete"}} 

195 
@{thm [display] lookup_delete} 

196 
\vspace{1ex} 

197 

198 
\noindent 

199 
\underline{@{text "lookup_bulkload"}} 

200 
@{thm [display] lookup_bulkload} 

201 
\vspace{1ex} 

202 

203 
\noindent 

204 
\underline{@{text "lookup_map"}} 

205 
@{thm [display] lookup_map} 

206 
\vspace{1ex} 

207 
*} 

208 

209 
end 