author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 63649  e690d6f2185b 
child 68484  59793df7f853 
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 

60500  5 
section \<open>Implementation of mappings with RedBlack Trees\<close> 
43124  6 

7 
(*<*) 

8 
theory RBT_Mapping 

9 
imports RBT Mapping 

10 
begin 

11 

60500  12 
subsection \<open>Implementation of mappings\<close> 
43124  13 

56019  14 
context includes rbt.lifting begin 
61076  15 
lift_definition Mapping :: "('a::linorder, 'b) rbt \<Rightarrow> ('a, 'b) mapping" is RBT.lookup . 
56019  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)" 
63649  46 
apply (transfer fixing: t) 
47 
apply (case_tac "RBT.lookup t k") 

48 
apply auto 

49 
done 

43124  50 

51 
lemma keys_Mapping [code]: 

56019  52 
"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

53 
by (transfer fixing: t) (simp add: lookup_keys) 
43124  54 

55 
lemma ordered_keys_Mapping [code]: 

56019  56 
"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

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

58 
by (transfer fixing: t) (auto simp add: lookup_keys intro: sorted_distinct_set_unique) 
43124  59 

60 
lemma Mapping_size_card_keys: (*FIXME*) 

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

62 
unfolding size_def by transfer simp 
43124  63 

64 
lemma size_Mapping [code]: 

56019  65 
"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

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

67 
by (transfer fixing: t) (simp add: lookup_keys distinct_card) 
43124  68 

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

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

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

71 
begin 
60373  72 

73 
lemma tabulate_Mapping [code]: 

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

75 
by transfer (simp add: map_of_map_restrict) 

76 

77 
lemma bulkload_Mapping [code]: 

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

79 
by transfer (simp add: map_of_map_restrict fun_eq_iff) 

80 

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

81 
end 
43124  82 

63194  83 
lemma map_values_Mapping [code]: 
84 
"Mapping.map_values f (Mapping t) = Mapping (RBT.map f t)" 

85 
by (transfer fixing: t) (auto simp: fun_eq_iff) 

86 

87 
lemma filter_Mapping [code]: 

88 
"Mapping.filter P (Mapping t) = Mapping (RBT.filter P t)" 

89 
by (transfer' fixing: P t) (simp add: RBT.lookup_filter fun_eq_iff) 

90 

91 
lemma combine_with_key_Mapping [code]: 

92 
"Mapping.combine_with_key f (Mapping t1) (Mapping t2) = 

93 
Mapping (RBT.combine_with_key f t1 t2)" 

94 
by (transfer fixing: f t1 t2) (simp_all add: fun_eq_iff) 

95 

96 
lemma combine_Mapping [code]: 

97 
"Mapping.combine f (Mapping t1) (Mapping t2) = 

98 
Mapping (RBT.combine f t1 t2)" 

99 
by (transfer fixing: f t1 t2) (simp_all add: fun_eq_iff) 

100 

43124  101 
lemma equal_Mapping [code]: 
56019  102 
"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

103 
by (transfer fixing: t1 t2) (simp add: entries_lookup) 
43124  104 

105 
lemma [code nbe]: 

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

107 
by (fact equal_refl) 

108 

56019  109 
end 
43124  110 

111 
(*>*) 

112 

60500  113 
text \<open> 
43124  114 
This theory defines abstract redblack trees as an efficient 
115 
representation of finite maps, backed by the implementation 

116 
in @{theory RBT_Impl}. 

60500  117 
\<close> 
43124  118 

60500  119 
subsection \<open>Data type and invariant\<close> 
43124  120 

60500  121 
text \<open> 
43124  122 
The type @{typ "('k, 'v) RBT_Impl.rbt"} denotes redblack trees with 
123 
keys of type @{typ "'k"} and values of type @{typ "'v"}. To function 

61585  124 
properly, the key type musorted belong to the \<open>linorder\<close> 
43124  125 
class. 
126 

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

61585  128 
satisfies the invariant \<open>is_rbt t\<close>. The abstract type @{typ 
43124  129 
"('k, 'v) rbt"} always obeys this invariant, and for this reason you 
130 
should only use this in our application. Going back to @{typ "('k, 

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

132 
properties about the operations must be established. 

133 

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

135 
map represented by a redblack tree: 

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

137 

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

139 
operations. Furthermore, it implements the lookup functionality for 

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

141 
$O(\log n)$. 

60500  142 
\<close> 
43124  143 

60500  144 
subsection \<open>Operations\<close> 
43124  145 

60500  146 
text \<open> 
43124  147 
Currently, the following operations are supported: 
148 

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

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

151 

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

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

154 

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

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

157 

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

159 
Return a corresponding keyvalue list for a tree. 

160 

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

162 
Builds a tree from a keyvalue list. 

163 

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

165 
Maps a single entry in a tree. 

166 

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

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

169 

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

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

60500  172 
\<close> 
43124  173 

174 

60500  175 
subsection \<open>Invariant preservation\<close> 
43124  176 

60500  177 
text \<open> 
43124  178 
\noindent 
61585  179 
@{thm Empty_is_rbt}\hfill(\<open>Empty_is_rbt\<close>) 
43124  180 

181 
\noindent 

61585  182 
@{thm rbt_insert_is_rbt}\hfill(\<open>rbt_insert_is_rbt\<close>) 
43124  183 

184 
\noindent 

61585  185 
@{thm rbt_delete_is_rbt}\hfill(\<open>delete_is_rbt\<close>) 
43124  186 

187 
\noindent 

61585  188 
@{thm rbt_bulkload_is_rbt}\hfill(\<open>bulkload_is_rbt\<close>) 
43124  189 

190 
\noindent 

61585  191 
@{thm rbt_map_entry_is_rbt}\hfill(\<open>map_entry_is_rbt\<close>) 
43124  192 

193 
\noindent 

61585  194 
@{thm map_is_rbt}\hfill(\<open>map_is_rbt\<close>) 
43124  195 

196 
\noindent 

61585  197 
@{thm rbt_union_is_rbt}\hfill(\<open>union_is_rbt\<close>) 
60500  198 
\<close> 
43124  199 

200 

60500  201 
subsection \<open>Map Semantics\<close> 
43124  202 

60500  203 
text \<open> 
43124  204 
\noindent 
61585  205 
\underline{\<open>lookup_empty\<close>} 
43124  206 
@{thm [display] lookup_empty} 
207 
\vspace{1ex} 

208 

209 
\noindent 

61585  210 
\underline{\<open>lookup_insert\<close>} 
43124  211 
@{thm [display] lookup_insert} 
212 
\vspace{1ex} 

213 

214 
\noindent 

61585  215 
\underline{\<open>lookup_delete\<close>} 
43124  216 
@{thm [display] lookup_delete} 
217 
\vspace{1ex} 

218 

219 
\noindent 

61585  220 
\underline{\<open>lookup_bulkload\<close>} 
43124  221 
@{thm [display] lookup_bulkload} 
222 
\vspace{1ex} 

223 

224 
\noindent 

61585  225 
\underline{\<open>lookup_map\<close>} 
43124  226 
@{thm [display] lookup_map} 
227 
\vspace{1ex} 

60500  228 
\<close> 
43124  229 

62390  230 
end 