1 (* Author: Lukas Bulwahn, TU Muenchen *)
3 header {* Lifting operations of RBT trees *}
6 imports Main "~~/src/HOL/Library/RBT_Impl"
9 definition inv :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
10 where [simp]: "inv R = (\<lambda>x y. R x \<and> x = y)"
12 subsection {* Type definition *}
14 quotient_type ('a, 'b) rbt = "('a\<Colon>linorder, 'b) RBT_Impl.rbt" / "inv is_rbt" morphisms impl_of RBT
19 "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2"
20 by (simp add: impl_of_inject)
23 "impl_of t1 = impl_of t2 \<Longrightarrow> t1 = t2"
24 by (simp add: rbt_eq_iff)
26 lemma is_rbt_impl_of [simp, intro]:
28 using impl_of [of t] by simp
30 lemma RBT_impl_of [simp, code abstype]:
32 by (simp add: impl_of_inverse)
35 subsection {* Primitive operations *}
37 quotient_definition lookup where "lookup :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup"
40 declare lookup_def[unfolded map_fun_def comp_def id_def, code]
42 (* FIXME: quotient_definition at the moment requires that types variables match exactly,
43 i.e., sort constraints must be annotated to the constant being lifted.
44 But, it should be possible to infer the necessary sort constraints, making the explicit
45 sort constraints unnecessary.
47 Hence this unannotated quotient_definition fails:
49 quotient_definition empty where "empty :: ('a\<Colon>linorder, 'b) rbt"
52 Similar issue for quotient_definition for entries, keys, map, and fold.
55 quotient_definition empty where "empty :: ('a\<Colon>linorder, 'b) rbt"
56 is "(RBT_Impl.Empty :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt)" done
58 lemma impl_of_empty [code abstract]:
59 "impl_of empty = RBT_Impl.Empty"
60 by (simp add: empty_def RBT_inverse)
62 quotient_definition insert where "insert :: 'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
63 is "RBT_Impl.insert" done
65 lemma impl_of_insert [code abstract]:
66 "impl_of (insert k v t) = RBT_Impl.insert k v (impl_of t)"
67 by (simp add: insert_def RBT_inverse)
69 quotient_definition delete where "delete :: 'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
70 is "RBT_Impl.delete" done
72 lemma impl_of_delete [code abstract]:
73 "impl_of (delete k t) = RBT_Impl.delete k (impl_of t)"
74 by (simp add: delete_def RBT_inverse)
76 (* FIXME: unnecessary type annotations *)
77 quotient_definition "entries :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list"
78 is "RBT_Impl.entries :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a \<times> 'b) list" done
80 lemma [code]: "entries t = RBT_Impl.entries (impl_of t)"
81 unfolding entries_def map_fun_def comp_def id_def ..
83 (* FIXME: unnecessary type annotations *)
84 quotient_definition "keys :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list"
85 is "RBT_Impl.keys :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a list" done
87 quotient_definition "bulkload :: ('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt"
88 is "RBT_Impl.bulkload" done
90 lemma impl_of_bulkload [code abstract]:
91 "impl_of (bulkload xs) = RBT_Impl.bulkload xs"
92 by (simp add: bulkload_def RBT_inverse)
94 quotient_definition "map_entry :: 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
95 is "RBT_Impl.map_entry" done
97 lemma impl_of_map_entry [code abstract]:
98 "impl_of (map_entry k f t) = RBT_Impl.map_entry k f (impl_of t)"
99 by (simp add: map_entry_def RBT_inverse)
101 (* FIXME: unnecesary type annotations *)
102 quotient_definition map where "map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
103 is "RBT_Impl.map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a, 'b) RBT_Impl.rbt"
106 lemma impl_of_map [code abstract]:
107 "impl_of (map f t) = RBT_Impl.map f (impl_of t)"
108 by (simp add: map_def RBT_inverse)
110 (* FIXME: unnecessary type annotations *)
111 quotient_definition fold where "fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"
112 is "RBT_Impl.fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'c \<Rightarrow> 'c" done
114 lemma [code]: "fold f t = RBT_Impl.fold f (impl_of t)"
115 unfolding fold_def map_fun_def comp_def id_def ..
118 subsection {* Derived operations *}
120 definition is_empty :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> bool" where
121 [code]: "is_empty t = (case impl_of t of RBT_Impl.Empty \<Rightarrow> True | _ \<Rightarrow> False)"
124 subsection {* Abstract lookup properties *}
126 (* TODO: obtain the following lemmas by lifting existing theorems. *)
129 "is_rbt t \<Longrightarrow> lookup (RBT t) = RBT_Impl.lookup t"
130 by (simp add: lookup_def RBT_inverse)
132 lemma lookup_impl_of:
133 "RBT_Impl.lookup (impl_of t) = lookup t"
134 by (simp add: lookup_def)
136 lemma entries_impl_of:
137 "RBT_Impl.entries (impl_of t) = entries t"
138 by (simp add: entries_def)
141 "RBT_Impl.keys (impl_of t) = keys t"
142 by (simp add: keys_def)
144 lemma lookup_empty [simp]:
145 "lookup empty = Map.empty"
146 by (simp add: empty_def lookup_RBT fun_eq_iff)
148 lemma lookup_insert [simp]:
149 "lookup (insert k v t) = (lookup t)(k \<mapsto> v)"
150 by (simp add: insert_def lookup_RBT lookup_insert lookup_impl_of)
152 lemma lookup_delete [simp]:
153 "lookup (delete k t) = (lookup t)(k := None)"
154 by (simp add: delete_def lookup_RBT RBT_Impl.lookup_delete lookup_impl_of restrict_complement_singleton_eq)
156 lemma map_of_entries [simp]:
157 "map_of (entries t) = lookup t"
158 by (simp add: entries_def map_of_entries lookup_impl_of)
160 lemma entries_lookup:
161 "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
162 by (simp add: entries_def lookup_def entries_lookup)
164 lemma lookup_bulkload [simp]:
165 "lookup (bulkload xs) = map_of xs"
166 by (simp add: bulkload_def lookup_RBT RBT_Impl.lookup_bulkload)
168 lemma lookup_map_entry [simp]:
169 "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
170 by (simp add: map_entry_def lookup_RBT RBT_Impl.lookup_map_entry lookup_impl_of)
172 lemma lookup_map [simp]:
173 "lookup (map f t) k = Option.map (f k) (lookup t k)"
174 by (simp add: map_def lookup_RBT RBT_Impl.lookup_map lookup_impl_of)
177 "fold f t = List.fold (prod_case f) (entries t)"
178 by (simp add: fold_def fun_eq_iff RBT_Impl.fold_def entries_impl_of)
180 lemma is_empty_empty [simp]:
181 "is_empty t \<longleftrightarrow> t = empty"
182 by (simp add: rbt_eq_iff is_empty_def impl_of_empty split: rbt.split)
184 lemma RBT_lookup_empty [simp]: (*FIXME*)
185 "RBT_Impl.lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
186 by (cases t) (auto simp add: fun_eq_iff)
188 lemma lookup_empty_empty [simp]:
189 "lookup t = Map.empty \<longleftrightarrow> t = empty"
190 by (cases t) (simp add: empty_def lookup_def RBT_inject RBT_inverse)
192 lemma sorted_keys [iff]:
194 by (simp add: keys_def RBT_Impl.keys_def sorted_entries)
196 lemma distinct_keys [iff]:
198 by (simp add: keys_def RBT_Impl.keys_def distinct_entries)