author  kuncar 
Fri, 08 Mar 2013 13:21:58 +0100  
changeset 51379  6dd83e007f56 
parent 51161  6ed12ae3b3e1 
child 51438  a614e456870b 
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 

5 
header {* Implementation of mappings with RedBlack Trees *} 

6 

7 
(*<*) 

8 
theory RBT_Mapping 

9 
imports RBT Mapping 

10 
begin 

11 

12 
subsection {* Implementation of mappings *} 

13 

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

14 
lift_definition Mapping :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) mapping" is lookup . 
43124  15 

16 
code_datatype Mapping 

17 

18 
lemma lookup_Mapping [simp, code]: 

19 
"Mapping.lookup (Mapping t) = lookup t" 

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

20 
by (transfer fixing: t) rule 
43124  21 

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

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

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

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

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

26 
qed 
43124  27 

28 
lemma is_empty_Mapping [code]: 

29 
"Mapping.is_empty (Mapping t) \<longleftrightarrow> is_empty t" 

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

30 
unfolding is_empty_def by (transfer fixing: t) simp 
43124  31 

32 
lemma insert_Mapping [code]: 

33 
"Mapping.update k v (Mapping t) = Mapping (insert k v t)" 

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

34 
by (transfer fixing: t) simp 
43124  35 

36 
lemma delete_Mapping [code]: 

37 
"Mapping.delete k (Mapping t) = Mapping (delete k 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 map_entry_Mapping [code]: 

41 
"Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)" 

51379  42 
by (transfer fixing: t, case_tac "lookup t k") auto 
43124  43 

44 
lemma keys_Mapping [code]: 

45 
"Mapping.keys (Mapping t) = set (keys t)" 

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

46 
by (transfer fixing: t) (simp add: lookup_keys) 
43124  47 

48 
lemma ordered_keys_Mapping [code]: 

49 
"Mapping.ordered_keys (Mapping t) = keys t" 

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

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

51 
by (transfer fixing: t) (auto simp add: lookup_keys intro: sorted_distinct_set_unique) 
43124  52 

53 
lemma Mapping_size_card_keys: (*FIXME*) 

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

55 
unfolding size_def by transfer simp 
43124  56 

57 
lemma size_Mapping [code]: 

58 
"Mapping.size (Mapping t) = length (keys t)" 

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

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

60 
by (transfer fixing: t) (simp add: lookup_keys distinct_card) 
43124  61 

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

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

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

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

65 
lemma tabulate_Mapping [code]: 
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset

66 
"Mapping.tabulate ks f = Mapping (bulkload (List.map (\<lambda>k. (k, f k)) ks))" 
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset

67 
by transfer (simp add: map_of_map_restrict) 
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset

68 

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

69 
lemma bulkload_Mapping [code]: 
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset

70 
"Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))" 
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset

71 
by transfer (simp add: map_of_map_restrict fun_eq_iff) 
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset

72 
end 
43124  73 

74 
lemma equal_Mapping [code]: 

75 
"HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2" 

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

76 
by (transfer fixing: t1 t2) (simp add: entries_lookup) 
43124  77 

78 
lemma [code nbe]: 

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

80 
by (fact equal_refl) 

81 

82 

83 
hide_const (open) impl_of lookup empty insert delete 

84 
entries keys bulkload map_entry map fold 

85 
(*>*) 

86 

87 
text {* 

88 
This theory defines abstract redblack trees as an efficient 

89 
representation of finite maps, backed by the implementation 

90 
in @{theory RBT_Impl}. 

91 
*} 

92 

93 
subsection {* Data type and invariant *} 

94 

95 
text {* 

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

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

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

99 
class. 

100 

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

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

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

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

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

106 
properties about the operations must be established. 

107 

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

109 
map represented by a redblack tree: 

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

111 

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

113 
operations. Furthermore, it implements the lookup functionality for 

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

115 
$O(\log n)$. 

116 
*} 

117 

118 
subsection {* Operations *} 

119 

120 
text {* 

121 
Currently, the following operations are supported: 

122 

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

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

125 

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

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

128 

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

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

131 

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

133 
Return a corresponding keyvalue list for a tree. 

134 

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

136 
Builds a tree from a keyvalue list. 

137 

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

139 
Maps a single entry in a tree. 

140 

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

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

143 

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

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

146 
*} 

147 

148 

149 
subsection {* Invariant preservation *} 

150 

151 
text {* 

152 
\noindent 

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

154 

155 
\noindent 

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

156 
@{thm rbt_insert_is_rbt}\hfill(@{text "rbt_insert_is_rbt"}) 
43124  157 

158 
\noindent 

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

159 
@{thm rbt_delete_is_rbt}\hfill(@{text "delete_is_rbt"}) 
43124  160 

161 
\noindent 

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

162 
@{thm rbt_bulkload_is_rbt}\hfill(@{text "bulkload_is_rbt"}) 
43124  163 

164 
\noindent 

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

165 
@{thm rbt_map_entry_is_rbt}\hfill(@{text "map_entry_is_rbt"}) 
43124  166 

167 
\noindent 

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

169 

170 
\noindent 

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

171 
@{thm rbt_union_is_rbt}\hfill(@{text "union_is_rbt"}) 
43124  172 
*} 
173 

174 

175 
subsection {* Map Semantics *} 

176 

177 
text {* 

178 
\noindent 

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

180 
@{thm [display] lookup_empty} 

181 
\vspace{1ex} 

182 

183 
\noindent 

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

185 
@{thm [display] lookup_insert} 

186 
\vspace{1ex} 

187 

188 
\noindent 

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

190 
@{thm [display] lookup_delete} 

191 
\vspace{1ex} 

192 

193 
\noindent 

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

195 
@{thm [display] lookup_bulkload} 

196 
\vspace{1ex} 

197 

198 
\noindent 

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

200 
@{thm [display] lookup_map} 

201 
\vspace{1ex} 

202 
*} 

203 

204 
end 