kuncar@49638
|
1 |
(* Title: HOL/Library/RBT_Set.thy
|
kuncar@49638
|
2 |
Author: Ondrej Kuncar
|
kuncar@49638
|
3 |
*)
|
kuncar@49638
|
4 |
|
kuncar@49638
|
5 |
header {* Implementation of sets using RBT trees *}
|
kuncar@49638
|
6 |
|
kuncar@49638
|
7 |
theory RBT_Set
|
haftmann@52252
|
8 |
imports RBT Product_Lexorder
|
kuncar@49638
|
9 |
begin
|
kuncar@49638
|
10 |
|
kuncar@49638
|
11 |
(*
|
kuncar@49638
|
12 |
Users should be aware that by including this file all code equations
|
kuncar@49638
|
13 |
outside of List.thy using 'a list as an implenentation of sets cannot be
|
kuncar@49638
|
14 |
used for code generation. If such equations are not needed, they can be
|
kuncar@49638
|
15 |
deleted from the code generator. Otherwise, a user has to provide their
|
kuncar@49638
|
16 |
own equations using RBT trees.
|
kuncar@49638
|
17 |
*)
|
kuncar@49638
|
18 |
|
kuncar@49638
|
19 |
section {* Definition of code datatype constructors *}
|
kuncar@49638
|
20 |
|
kuncar@49638
|
21 |
definition Set :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set"
|
kuncar@49638
|
22 |
where "Set t = {x . lookup t x = Some ()}"
|
kuncar@49638
|
23 |
|
kuncar@49638
|
24 |
definition Coset :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set"
|
kuncar@49638
|
25 |
where [simp]: "Coset t = - Set t"
|
kuncar@49638
|
26 |
|
kuncar@49638
|
27 |
|
kuncar@49638
|
28 |
section {* Deletion of already existing code equations *}
|
kuncar@49638
|
29 |
|
kuncar@49638
|
30 |
lemma [code, code del]:
|
kuncar@49638
|
31 |
"Set.empty = Set.empty" ..
|
kuncar@49638
|
32 |
|
kuncar@49638
|
33 |
lemma [code, code del]:
|
kuncar@49638
|
34 |
"Set.is_empty = Set.is_empty" ..
|
kuncar@49638
|
35 |
|
kuncar@49638
|
36 |
lemma [code, code del]:
|
kuncar@49638
|
37 |
"uminus_set_inst.uminus_set = uminus_set_inst.uminus_set" ..
|
kuncar@49638
|
38 |
|
kuncar@49638
|
39 |
lemma [code, code del]:
|
kuncar@49638
|
40 |
"Set.member = Set.member" ..
|
kuncar@49638
|
41 |
|
kuncar@49638
|
42 |
lemma [code, code del]:
|
kuncar@49638
|
43 |
"Set.insert = Set.insert" ..
|
kuncar@49638
|
44 |
|
kuncar@49638
|
45 |
lemma [code, code del]:
|
kuncar@49638
|
46 |
"Set.remove = Set.remove" ..
|
kuncar@49638
|
47 |
|
kuncar@49638
|
48 |
lemma [code, code del]:
|
kuncar@49638
|
49 |
"UNIV = UNIV" ..
|
kuncar@49638
|
50 |
|
kuncar@49638
|
51 |
lemma [code, code del]:
|
kuncar@50772
|
52 |
"Set.filter = Set.filter" ..
|
kuncar@49638
|
53 |
|
kuncar@49638
|
54 |
lemma [code, code del]:
|
kuncar@49638
|
55 |
"image = image" ..
|
kuncar@49638
|
56 |
|
kuncar@49638
|
57 |
lemma [code, code del]:
|
kuncar@49638
|
58 |
"Set.subset_eq = Set.subset_eq" ..
|
kuncar@49638
|
59 |
|
kuncar@49638
|
60 |
lemma [code, code del]:
|
kuncar@49638
|
61 |
"Ball = Ball" ..
|
kuncar@49638
|
62 |
|
kuncar@49638
|
63 |
lemma [code, code del]:
|
kuncar@49638
|
64 |
"Bex = Bex" ..
|
kuncar@49638
|
65 |
|
haftmann@50963
|
66 |
lemma [code, code del]:
|
haftmann@50963
|
67 |
"can_select = can_select" ..
|
haftmann@50963
|
68 |
|
kuncar@49638
|
69 |
lemma [code, code del]:
|
kuncar@49638
|
70 |
"Set.union = Set.union" ..
|
kuncar@49638
|
71 |
|
kuncar@49638
|
72 |
lemma [code, code del]:
|
kuncar@49638
|
73 |
"minus_set_inst.minus_set = minus_set_inst.minus_set" ..
|
kuncar@49638
|
74 |
|
kuncar@49638
|
75 |
lemma [code, code del]:
|
kuncar@49638
|
76 |
"Set.inter = Set.inter" ..
|
kuncar@49638
|
77 |
|
kuncar@49638
|
78 |
lemma [code, code del]:
|
kuncar@49638
|
79 |
"card = card" ..
|
kuncar@49638
|
80 |
|
kuncar@49638
|
81 |
lemma [code, code del]:
|
kuncar@49638
|
82 |
"the_elem = the_elem" ..
|
kuncar@49638
|
83 |
|
kuncar@49638
|
84 |
lemma [code, code del]:
|
kuncar@49638
|
85 |
"Pow = Pow" ..
|
kuncar@49638
|
86 |
|
kuncar@49638
|
87 |
lemma [code, code del]:
|
kuncar@49638
|
88 |
"setsum = setsum" ..
|
kuncar@49638
|
89 |
|
kuncar@49638
|
90 |
lemma [code, code del]:
|
kuncar@49638
|
91 |
"Product_Type.product = Product_Type.product" ..
|
kuncar@49638
|
92 |
|
kuncar@49638
|
93 |
lemma [code, code del]:
|
kuncar@49638
|
94 |
"Id_on = Id_on" ..
|
kuncar@49638
|
95 |
|
kuncar@49638
|
96 |
lemma [code, code del]:
|
kuncar@49638
|
97 |
"Image = Image" ..
|
kuncar@49638
|
98 |
|
kuncar@49638
|
99 |
lemma [code, code del]:
|
kuncar@49638
|
100 |
"trancl = trancl" ..
|
kuncar@49638
|
101 |
|
kuncar@49638
|
102 |
lemma [code, code del]:
|
kuncar@49638
|
103 |
"relcomp = relcomp" ..
|
kuncar@49638
|
104 |
|
kuncar@49638
|
105 |
lemma [code, code del]:
|
kuncar@49638
|
106 |
"wf = wf" ..
|
kuncar@49638
|
107 |
|
kuncar@49638
|
108 |
lemma [code, code del]:
|
kuncar@49638
|
109 |
"Min = Min" ..
|
kuncar@49638
|
110 |
|
kuncar@49638
|
111 |
lemma [code, code del]:
|
kuncar@49638
|
112 |
"Inf_fin = Inf_fin" ..
|
kuncar@49638
|
113 |
|
kuncar@49638
|
114 |
lemma [code, code del]:
|
kuncar@49638
|
115 |
"INFI = INFI" ..
|
kuncar@49638
|
116 |
|
kuncar@49638
|
117 |
lemma [code, code del]:
|
kuncar@49638
|
118 |
"Max = Max" ..
|
kuncar@49638
|
119 |
|
kuncar@49638
|
120 |
lemma [code, code del]:
|
kuncar@49638
|
121 |
"Sup_fin = Sup_fin" ..
|
kuncar@49638
|
122 |
|
kuncar@49638
|
123 |
lemma [code, code del]:
|
kuncar@49638
|
124 |
"SUPR = SUPR" ..
|
kuncar@49638
|
125 |
|
kuncar@49638
|
126 |
lemma [code, code del]:
|
kuncar@49638
|
127 |
"(Inf :: 'a set set \<Rightarrow> 'a set) = Inf" ..
|
kuncar@49638
|
128 |
|
kuncar@49638
|
129 |
lemma [code, code del]:
|
kuncar@49638
|
130 |
"(Sup :: 'a set set \<Rightarrow> 'a set) = Sup" ..
|
kuncar@49638
|
131 |
|
kuncar@49638
|
132 |
lemma [code, code del]:
|
kuncar@49638
|
133 |
"sorted_list_of_set = sorted_list_of_set" ..
|
kuncar@49638
|
134 |
|
kuncar@49638
|
135 |
lemma [code, code del]:
|
kuncar@49638
|
136 |
"List.map_project = List.map_project" ..
|
kuncar@49638
|
137 |
|
nipkow@55092
|
138 |
lemma [code, code del]:
|
nipkow@55092
|
139 |
"List.Bleast = List.Bleast" ..
|
nipkow@55092
|
140 |
|
kuncar@49638
|
141 |
section {* Lemmas *}
|
kuncar@49638
|
142 |
|
kuncar@49638
|
143 |
|
kuncar@49638
|
144 |
subsection {* Auxiliary lemmas *}
|
kuncar@49638
|
145 |
|
kuncar@49638
|
146 |
lemma [simp]: "x \<noteq> Some () \<longleftrightarrow> x = None"
|
kuncar@49638
|
147 |
by (auto simp: not_Some_eq[THEN iffD1])
|
kuncar@49638
|
148 |
|
kuncar@50943
|
149 |
lemma Set_set_keys: "Set x = dom (lookup x)"
|
kuncar@50943
|
150 |
by (auto simp: Set_def)
|
kuncar@50943
|
151 |
|
kuncar@49638
|
152 |
lemma finite_Set [simp, intro!]: "finite (Set x)"
|
kuncar@50943
|
153 |
by (simp add: Set_set_keys)
|
kuncar@49638
|
154 |
|
kuncar@49638
|
155 |
lemma set_keys: "Set t = set(keys t)"
|
kuncar@50943
|
156 |
by (simp add: Set_set_keys lookup_keys)
|
kuncar@49638
|
157 |
|
kuncar@49638
|
158 |
subsection {* fold and filter *}
|
kuncar@49638
|
159 |
|
kuncar@49638
|
160 |
lemma finite_fold_rbt_fold_eq:
|
kuncar@49638
|
161 |
assumes "comp_fun_commute f"
|
kuncar@49638
|
162 |
shows "Finite_Set.fold f A (set(entries t)) = fold (curry f) t A"
|
kuncar@49638
|
163 |
proof -
|
kuncar@49638
|
164 |
have *: "remdups (entries t) = entries t"
|
kuncar@49638
|
165 |
using distinct_entries distinct_map by (auto intro: distinct_remdups_id)
|
kuncar@49638
|
166 |
show ?thesis using assms by (auto simp: fold_def_alt comp_fun_commute.fold_set_fold_remdups *)
|
kuncar@49638
|
167 |
qed
|
kuncar@49638
|
168 |
|
kuncar@49638
|
169 |
definition fold_keys :: "('a :: linorder \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, _) rbt \<Rightarrow> 'b \<Rightarrow> 'b"
|
kuncar@49638
|
170 |
where [code_unfold]:"fold_keys f t A = fold (\<lambda>k _ t. f k t) t A"
|
kuncar@49638
|
171 |
|
kuncar@49638
|
172 |
lemma fold_keys_def_alt:
|
kuncar@49638
|
173 |
"fold_keys f t s = List.fold f (keys t) s"
|
kuncar@49638
|
174 |
by (auto simp: fold_map o_def split_def fold_def_alt keys_def_alt fold_keys_def)
|
kuncar@49638
|
175 |
|
kuncar@49638
|
176 |
lemma finite_fold_fold_keys:
|
kuncar@49638
|
177 |
assumes "comp_fun_commute f"
|
kuncar@49638
|
178 |
shows "Finite_Set.fold f A (Set t) = fold_keys f t A"
|
kuncar@49638
|
179 |
using assms
|
kuncar@49638
|
180 |
proof -
|
kuncar@49638
|
181 |
interpret comp_fun_commute f by fact
|
kuncar@49638
|
182 |
have "set (keys t) = fst ` (set (entries t))" by (auto simp: fst_eq_Domain keys_entries)
|
kuncar@49638
|
183 |
moreover have "inj_on fst (set (entries t))" using distinct_entries distinct_map by auto
|
kuncar@49638
|
184 |
ultimately show ?thesis
|
kuncar@49638
|
185 |
by (auto simp add: set_keys fold_keys_def curry_def fold_image finite_fold_rbt_fold_eq
|
kuncar@49638
|
186 |
comp_comp_fun_commute)
|
kuncar@49638
|
187 |
qed
|
kuncar@49638
|
188 |
|
kuncar@49638
|
189 |
definition rbt_filter :: "('a :: linorder \<Rightarrow> bool) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'a set" where
|
kuncar@49638
|
190 |
"rbt_filter P t = fold (\<lambda>k _ A'. if P k then Set.insert k A' else A') t {}"
|
kuncar@49638
|
191 |
|
kuncar@50773
|
192 |
lemma Set_filter_rbt_filter:
|
kuncar@50773
|
193 |
"Set.filter P (Set t) = rbt_filter P t"
|
kuncar@50773
|
194 |
by (simp add: fold_keys_def Set_filter_fold rbt_filter_def
|
kuncar@49638
|
195 |
finite_fold_fold_keys[OF comp_fun_commute_filter_fold])
|
kuncar@49638
|
196 |
|
kuncar@49638
|
197 |
|
kuncar@49638
|
198 |
subsection {* foldi and Ball *}
|
kuncar@49638
|
199 |
|
kuncar@49638
|
200 |
lemma Ball_False: "RBT_Impl.fold (\<lambda>k v s. s \<and> P k) t False = False"
|
kuncar@49638
|
201 |
by (induction t) auto
|
kuncar@49638
|
202 |
|
kuncar@49638
|
203 |
lemma rbt_foldi_fold_conj:
|
kuncar@49638
|
204 |
"RBT_Impl.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t val = RBT_Impl.fold (\<lambda>k v s. s \<and> P k) t val"
|
kuncar@49638
|
205 |
proof (induction t arbitrary: val)
|
kuncar@49638
|
206 |
case (Branch c t1) then show ?case
|
kuncar@49638
|
207 |
by (cases "RBT_Impl.fold (\<lambda>k v s. s \<and> P k) t1 True") (simp_all add: Ball_False)
|
kuncar@49638
|
208 |
qed simp
|
kuncar@49638
|
209 |
|
kuncar@49638
|
210 |
lemma foldi_fold_conj: "foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t val = fold_keys (\<lambda>k s. s \<and> P k) t val"
|
kuncar@49638
|
211 |
unfolding fold_keys_def by transfer (rule rbt_foldi_fold_conj)
|
kuncar@49638
|
212 |
|
kuncar@49638
|
213 |
|
kuncar@49638
|
214 |
subsection {* foldi and Bex *}
|
kuncar@49638
|
215 |
|
kuncar@49638
|
216 |
lemma Bex_True: "RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t True = True"
|
kuncar@49638
|
217 |
by (induction t) auto
|
kuncar@49638
|
218 |
|
kuncar@49638
|
219 |
lemma rbt_foldi_fold_disj:
|
kuncar@49638
|
220 |
"RBT_Impl.foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t val = RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t val"
|
kuncar@49638
|
221 |
proof (induction t arbitrary: val)
|
kuncar@49638
|
222 |
case (Branch c t1) then show ?case
|
kuncar@49638
|
223 |
by (cases "RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t1 False") (simp_all add: Bex_True)
|
kuncar@49638
|
224 |
qed simp
|
kuncar@49638
|
225 |
|
kuncar@49638
|
226 |
lemma foldi_fold_disj: "foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t val = fold_keys (\<lambda>k s. s \<or> P k) t val"
|
kuncar@49638
|
227 |
unfolding fold_keys_def by transfer (rule rbt_foldi_fold_disj)
|
kuncar@49638
|
228 |
|
kuncar@49638
|
229 |
|
kuncar@49638
|
230 |
subsection {* folding over non empty trees and selecting the minimal and maximal element *}
|
kuncar@49638
|
231 |
|
kuncar@49638
|
232 |
(** concrete **)
|
kuncar@49638
|
233 |
|
kuncar@49638
|
234 |
(* The concrete part is here because it's probably not general enough to be moved to RBT_Impl *)
|
kuncar@49638
|
235 |
|
kuncar@49638
|
236 |
definition rbt_fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a"
|
kuncar@49638
|
237 |
where "rbt_fold1_keys f t = List.fold f (tl(RBT_Impl.keys t)) (hd(RBT_Impl.keys t))"
|
kuncar@49638
|
238 |
|
kuncar@49638
|
239 |
(* minimum *)
|
kuncar@49638
|
240 |
|
kuncar@49638
|
241 |
definition rbt_min :: "('a::linorder, unit) RBT_Impl.rbt \<Rightarrow> 'a"
|
kuncar@49638
|
242 |
where "rbt_min t = rbt_fold1_keys min t"
|
kuncar@49638
|
243 |
|
kuncar@49638
|
244 |
lemma key_le_right: "rbt_sorted (Branch c lt k v rt) \<Longrightarrow> (\<And>x. x \<in>set (RBT_Impl.keys rt) \<Longrightarrow> k \<le> x)"
|
kuncar@49638
|
245 |
by (auto simp: rbt_greater_prop less_imp_le)
|
kuncar@49638
|
246 |
|
kuncar@49638
|
247 |
lemma left_le_key: "rbt_sorted (Branch c lt k v rt) \<Longrightarrow> (\<And>x. x \<in>set (RBT_Impl.keys lt) \<Longrightarrow> x \<le> k)"
|
kuncar@49638
|
248 |
by (auto simp: rbt_less_prop less_imp_le)
|
kuncar@49638
|
249 |
|
kuncar@49638
|
250 |
lemma fold_min_triv:
|
kuncar@49638
|
251 |
fixes k :: "_ :: linorder"
|
kuncar@49638
|
252 |
shows "(\<forall>x\<in>set xs. k \<le> x) \<Longrightarrow> List.fold min xs k = k"
|
kuncar@49638
|
253 |
by (induct xs) (auto simp add: min_def)
|
kuncar@49638
|
254 |
|
kuncar@49638
|
255 |
lemma rbt_min_simps:
|
kuncar@49638
|
256 |
"is_rbt (Branch c RBT_Impl.Empty k v rt) \<Longrightarrow> rbt_min (Branch c RBT_Impl.Empty k v rt) = k"
|
kuncar@49638
|
257 |
by (auto intro: fold_min_triv dest: key_le_right is_rbt_rbt_sorted simp: rbt_fold1_keys_def rbt_min_def)
|
kuncar@49638
|
258 |
|
kuncar@49638
|
259 |
fun rbt_min_opt where
|
kuncar@49638
|
260 |
"rbt_min_opt (Branch c RBT_Impl.Empty k v rt) = k" |
|
kuncar@49638
|
261 |
"rbt_min_opt (Branch c (Branch lc llc lk lv lrt) k v rt) = rbt_min_opt (Branch lc llc lk lv lrt)"
|
kuncar@49638
|
262 |
|
kuncar@49638
|
263 |
lemma rbt_min_opt_Branch:
|
kuncar@49638
|
264 |
"t1 \<noteq> rbt.Empty \<Longrightarrow> rbt_min_opt (Branch c t1 k () t2) = rbt_min_opt t1"
|
kuncar@49638
|
265 |
by (cases t1) auto
|
kuncar@49638
|
266 |
|
kuncar@49638
|
267 |
lemma rbt_min_opt_induct [case_names empty left_empty left_non_empty]:
|
kuncar@49638
|
268 |
fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
|
kuncar@49638
|
269 |
assumes "P rbt.Empty"
|
kuncar@49638
|
270 |
assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t1 = rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
|
kuncar@49638
|
271 |
assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t1 \<noteq> rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
|
kuncar@49638
|
272 |
shows "P t"
|
kuncar@49638
|
273 |
using assms
|
kuncar@49638
|
274 |
apply (induction t)
|
kuncar@49638
|
275 |
apply simp
|
kuncar@49638
|
276 |
apply (case_tac "t1 = rbt.Empty")
|
kuncar@49638
|
277 |
apply simp_all
|
kuncar@49638
|
278 |
done
|
kuncar@49638
|
279 |
|
kuncar@49638
|
280 |
lemma rbt_min_opt_in_set:
|
kuncar@49638
|
281 |
fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
|
kuncar@49638
|
282 |
assumes "t \<noteq> rbt.Empty"
|
kuncar@49638
|
283 |
shows "rbt_min_opt t \<in> set (RBT_Impl.keys t)"
|
kuncar@49638
|
284 |
using assms by (induction t rule: rbt_min_opt.induct) (auto)
|
kuncar@49638
|
285 |
|
kuncar@49638
|
286 |
lemma rbt_min_opt_is_min:
|
kuncar@49638
|
287 |
fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
|
kuncar@49638
|
288 |
assumes "rbt_sorted t"
|
kuncar@49638
|
289 |
assumes "t \<noteq> rbt.Empty"
|
kuncar@49638
|
290 |
shows "\<And>y. y \<in> set (RBT_Impl.keys t) \<Longrightarrow> y \<ge> rbt_min_opt t"
|
kuncar@49638
|
291 |
using assms
|
kuncar@49638
|
292 |
proof (induction t rule: rbt_min_opt_induct)
|
kuncar@49638
|
293 |
case empty
|
kuncar@49638
|
294 |
then show ?case by simp
|
kuncar@49638
|
295 |
next
|
kuncar@49638
|
296 |
case left_empty
|
kuncar@49638
|
297 |
then show ?case by (auto intro: key_le_right simp del: rbt_sorted.simps)
|
kuncar@49638
|
298 |
next
|
kuncar@49638
|
299 |
case (left_non_empty c t1 k v t2 y)
|
kuncar@49638
|
300 |
then have "y = k \<or> y \<in> set (RBT_Impl.keys t1) \<or> y \<in> set (RBT_Impl.keys t2)" by auto
|
kuncar@49638
|
301 |
with left_non_empty show ?case
|
kuncar@49638
|
302 |
proof(elim disjE)
|
kuncar@49638
|
303 |
case goal1 then show ?case
|
kuncar@49638
|
304 |
by (auto simp add: rbt_min_opt_Branch intro: left_le_key rbt_min_opt_in_set)
|
kuncar@49638
|
305 |
next
|
kuncar@49638
|
306 |
case goal2 with left_non_empty show ?case by (auto simp add: rbt_min_opt_Branch)
|
kuncar@49638
|
307 |
next
|
kuncar@49638
|
308 |
case goal3 show ?case
|
kuncar@49638
|
309 |
proof -
|
kuncar@49638
|
310 |
from goal3 have "rbt_min_opt t1 \<le> k" by (simp add: left_le_key rbt_min_opt_in_set)
|
kuncar@49638
|
311 |
moreover from goal3 have "k \<le> y" by (simp add: key_le_right)
|
kuncar@49638
|
312 |
ultimately show ?thesis using goal3 by (simp add: rbt_min_opt_Branch)
|
kuncar@49638
|
313 |
qed
|
kuncar@49638
|
314 |
qed
|
kuncar@49638
|
315 |
qed
|
kuncar@49638
|
316 |
|
kuncar@49638
|
317 |
lemma rbt_min_eq_rbt_min_opt:
|
kuncar@49638
|
318 |
assumes "t \<noteq> RBT_Impl.Empty"
|
kuncar@49638
|
319 |
assumes "is_rbt t"
|
kuncar@49638
|
320 |
shows "rbt_min t = rbt_min_opt t"
|
kuncar@49638
|
321 |
proof -
|
haftmann@52626
|
322 |
from assms have "hd (RBT_Impl.keys t) # tl (RBT_Impl.keys t) = RBT_Impl.keys t" by (cases t) simp_all
|
haftmann@52626
|
323 |
with assms show ?thesis
|
haftmann@52626
|
324 |
by (simp add: rbt_min_def rbt_fold1_keys_def rbt_min_opt_is_min
|
haftmann@52677
|
325 |
Min.set_eq_fold [symmetric] Min_eqI rbt_min_opt_in_set)
|
kuncar@49638
|
326 |
qed
|
kuncar@49638
|
327 |
|
kuncar@49638
|
328 |
(* maximum *)
|
kuncar@49638
|
329 |
|
kuncar@49638
|
330 |
definition rbt_max :: "('a::linorder, unit) RBT_Impl.rbt \<Rightarrow> 'a"
|
kuncar@49638
|
331 |
where "rbt_max t = rbt_fold1_keys max t"
|
kuncar@49638
|
332 |
|
kuncar@49638
|
333 |
lemma fold_max_triv:
|
kuncar@49638
|
334 |
fixes k :: "_ :: linorder"
|
kuncar@49638
|
335 |
shows "(\<forall>x\<in>set xs. x \<le> k) \<Longrightarrow> List.fold max xs k = k"
|
kuncar@49638
|
336 |
by (induct xs) (auto simp add: max_def)
|
kuncar@49638
|
337 |
|
kuncar@49638
|
338 |
lemma fold_max_rev_eq:
|
kuncar@49638
|
339 |
fixes xs :: "('a :: linorder) list"
|
kuncar@49638
|
340 |
assumes "xs \<noteq> []"
|
kuncar@49638
|
341 |
shows "List.fold max (tl xs) (hd xs) = List.fold max (tl (rev xs)) (hd (rev xs))"
|
haftmann@52677
|
342 |
using assms by (simp add: Max.set_eq_fold [symmetric])
|
kuncar@49638
|
343 |
|
kuncar@49638
|
344 |
lemma rbt_max_simps:
|
kuncar@49638
|
345 |
assumes "is_rbt (Branch c lt k v RBT_Impl.Empty)"
|
kuncar@49638
|
346 |
shows "rbt_max (Branch c lt k v RBT_Impl.Empty) = k"
|
kuncar@49638
|
347 |
proof -
|
kuncar@49638
|
348 |
have "List.fold max (tl (rev(RBT_Impl.keys lt @ [k]))) (hd (rev(RBT_Impl.keys lt @ [k]))) = k"
|
kuncar@49638
|
349 |
using assms by (auto intro!: fold_max_triv dest!: left_le_key is_rbt_rbt_sorted)
|
kuncar@49638
|
350 |
then show ?thesis by (auto simp add: rbt_max_def rbt_fold1_keys_def fold_max_rev_eq)
|
kuncar@49638
|
351 |
qed
|
kuncar@49638
|
352 |
|
kuncar@49638
|
353 |
fun rbt_max_opt where
|
kuncar@49638
|
354 |
"rbt_max_opt (Branch c lt k v RBT_Impl.Empty) = k" |
|
kuncar@49638
|
355 |
"rbt_max_opt (Branch c lt k v (Branch rc rlc rk rv rrt)) = rbt_max_opt (Branch rc rlc rk rv rrt)"
|
kuncar@49638
|
356 |
|
kuncar@49638
|
357 |
lemma rbt_max_opt_Branch:
|
kuncar@49638
|
358 |
"t2 \<noteq> rbt.Empty \<Longrightarrow> rbt_max_opt (Branch c t1 k () t2) = rbt_max_opt t2"
|
kuncar@49638
|
359 |
by (cases t2) auto
|
kuncar@49638
|
360 |
|
kuncar@49638
|
361 |
lemma rbt_max_opt_induct [case_names empty right_empty right_non_empty]:
|
kuncar@49638
|
362 |
fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
|
kuncar@49638
|
363 |
assumes "P rbt.Empty"
|
kuncar@49638
|
364 |
assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t2 = rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
|
kuncar@49638
|
365 |
assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t2 \<noteq> rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
|
kuncar@49638
|
366 |
shows "P t"
|
kuncar@49638
|
367 |
using assms
|
kuncar@49638
|
368 |
apply (induction t)
|
kuncar@49638
|
369 |
apply simp
|
kuncar@49638
|
370 |
apply (case_tac "t2 = rbt.Empty")
|
kuncar@49638
|
371 |
apply simp_all
|
kuncar@49638
|
372 |
done
|
kuncar@49638
|
373 |
|
kuncar@49638
|
374 |
lemma rbt_max_opt_in_set:
|
kuncar@49638
|
375 |
fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
|
kuncar@49638
|
376 |
assumes "t \<noteq> rbt.Empty"
|
kuncar@49638
|
377 |
shows "rbt_max_opt t \<in> set (RBT_Impl.keys t)"
|
kuncar@49638
|
378 |
using assms by (induction t rule: rbt_max_opt.induct) (auto)
|
kuncar@49638
|
379 |
|
kuncar@49638
|
380 |
lemma rbt_max_opt_is_max:
|
kuncar@49638
|
381 |
fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
|
kuncar@49638
|
382 |
assumes "rbt_sorted t"
|
kuncar@49638
|
383 |
assumes "t \<noteq> rbt.Empty"
|
kuncar@49638
|
384 |
shows "\<And>y. y \<in> set (RBT_Impl.keys t) \<Longrightarrow> y \<le> rbt_max_opt t"
|
kuncar@49638
|
385 |
using assms
|
kuncar@49638
|
386 |
proof (induction t rule: rbt_max_opt_induct)
|
kuncar@49638
|
387 |
case empty
|
kuncar@49638
|
388 |
then show ?case by simp
|
kuncar@49638
|
389 |
next
|
kuncar@49638
|
390 |
case right_empty
|
kuncar@49638
|
391 |
then show ?case by (auto intro: left_le_key simp del: rbt_sorted.simps)
|
kuncar@49638
|
392 |
next
|
kuncar@49638
|
393 |
case (right_non_empty c t1 k v t2 y)
|
kuncar@49638
|
394 |
then have "y = k \<or> y \<in> set (RBT_Impl.keys t2) \<or> y \<in> set (RBT_Impl.keys t1)" by auto
|
kuncar@49638
|
395 |
with right_non_empty show ?case
|
kuncar@49638
|
396 |
proof(elim disjE)
|
kuncar@49638
|
397 |
case goal1 then show ?case
|
kuncar@49638
|
398 |
by (auto simp add: rbt_max_opt_Branch intro: key_le_right rbt_max_opt_in_set)
|
kuncar@49638
|
399 |
next
|
kuncar@49638
|
400 |
case goal2 with right_non_empty show ?case by (auto simp add: rbt_max_opt_Branch)
|
kuncar@49638
|
401 |
next
|
kuncar@49638
|
402 |
case goal3 show ?case
|
kuncar@49638
|
403 |
proof -
|
kuncar@49638
|
404 |
from goal3 have "rbt_max_opt t2 \<ge> k" by (simp add: key_le_right rbt_max_opt_in_set)
|
kuncar@49638
|
405 |
moreover from goal3 have "y \<le> k" by (simp add: left_le_key)
|
kuncar@49638
|
406 |
ultimately show ?thesis using goal3 by (simp add: rbt_max_opt_Branch)
|
kuncar@49638
|
407 |
qed
|
kuncar@49638
|
408 |
qed
|
kuncar@49638
|
409 |
qed
|
kuncar@49638
|
410 |
|
kuncar@49638
|
411 |
lemma rbt_max_eq_rbt_max_opt:
|
kuncar@49638
|
412 |
assumes "t \<noteq> RBT_Impl.Empty"
|
kuncar@49638
|
413 |
assumes "is_rbt t"
|
kuncar@49638
|
414 |
shows "rbt_max t = rbt_max_opt t"
|
kuncar@49638
|
415 |
proof -
|
haftmann@52626
|
416 |
from assms have "hd (RBT_Impl.keys t) # tl (RBT_Impl.keys t) = RBT_Impl.keys t" by (cases t) simp_all
|
haftmann@52626
|
417 |
with assms show ?thesis
|
haftmann@52626
|
418 |
by (simp add: rbt_max_def rbt_fold1_keys_def rbt_max_opt_is_max
|
haftmann@52677
|
419 |
Max.set_eq_fold [symmetric] Max_eqI rbt_max_opt_in_set)
|
kuncar@49638
|
420 |
qed
|
kuncar@49638
|
421 |
|
kuncar@49638
|
422 |
|
kuncar@49638
|
423 |
(** abstract **)
|
kuncar@49638
|
424 |
|
kuncar@49638
|
425 |
lift_definition fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> 'a"
|
kuncar@49638
|
426 |
is rbt_fold1_keys by simp
|
kuncar@49638
|
427 |
|
kuncar@49638
|
428 |
lemma fold1_keys_def_alt:
|
kuncar@49638
|
429 |
"fold1_keys f t = List.fold f (tl(keys t)) (hd(keys t))"
|
kuncar@49638
|
430 |
by transfer (simp add: rbt_fold1_keys_def)
|
kuncar@49638
|
431 |
|
kuncar@49638
|
432 |
lemma finite_fold1_fold1_keys:
|
haftmann@52626
|
433 |
assumes "semilattice f"
|
haftmann@52626
|
434 |
assumes "\<not> is_empty t"
|
haftmann@52626
|
435 |
shows "semilattice_set.F f (Set t) = fold1_keys f t"
|
kuncar@49638
|
436 |
proof -
|
haftmann@52626
|
437 |
from `semilattice f` interpret semilattice_set f by (rule semilattice_set.intro)
|
kuncar@49638
|
438 |
show ?thesis using assms
|
haftmann@52626
|
439 |
by (auto simp: fold1_keys_def_alt set_keys fold_def_alt non_empty_keys set_eq_fold [symmetric])
|
kuncar@49638
|
440 |
qed
|
kuncar@49638
|
441 |
|
kuncar@49638
|
442 |
(* minimum *)
|
kuncar@49638
|
443 |
|
kuncar@49638
|
444 |
lift_definition r_min :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min by simp
|
kuncar@49638
|
445 |
|
kuncar@49638
|
446 |
lift_definition r_min_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min_opt by simp
|
kuncar@49638
|
447 |
|
kuncar@49638
|
448 |
lemma r_min_alt_def: "r_min t = fold1_keys min t"
|
kuncar@49638
|
449 |
by transfer (simp add: rbt_min_def)
|
kuncar@49638
|
450 |
|
kuncar@49638
|
451 |
lemma r_min_eq_r_min_opt:
|
kuncar@49638
|
452 |
assumes "\<not> (is_empty t)"
|
kuncar@49638
|
453 |
shows "r_min t = r_min_opt t"
|
kuncar@49638
|
454 |
using assms unfolding is_empty_empty by transfer (auto intro: rbt_min_eq_rbt_min_opt)
|
kuncar@49638
|
455 |
|
kuncar@49638
|
456 |
lemma fold_keys_min_top_eq:
|
kuncar@49638
|
457 |
fixes t :: "('a :: {linorder, bounded_lattice_top}, unit) rbt"
|
kuncar@49638
|
458 |
assumes "\<not> (is_empty t)"
|
kuncar@49638
|
459 |
shows "fold_keys min t top = fold1_keys min t"
|
kuncar@49638
|
460 |
proof -
|
kuncar@49638
|
461 |
have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold min (RBT_Impl.keys t) top =
|
kuncar@49638
|
462 |
List.fold min (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) top"
|
kuncar@49638
|
463 |
by (simp add: hd_Cons_tl[symmetric])
|
kuncar@49638
|
464 |
{ fix x :: "_ :: {linorder, bounded_lattice_top}" and xs
|
kuncar@49638
|
465 |
have "List.fold min (x#xs) top = List.fold min xs x"
|
kuncar@49638
|
466 |
by (simp add: inf_min[symmetric])
|
kuncar@49638
|
467 |
} note ** = this
|
kuncar@49638
|
468 |
show ?thesis using assms
|
kuncar@49638
|
469 |
unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
|
kuncar@49638
|
470 |
apply transfer
|
kuncar@49638
|
471 |
apply (case_tac t)
|
kuncar@49638
|
472 |
apply simp
|
kuncar@49638
|
473 |
apply (subst *)
|
kuncar@49638
|
474 |
apply simp
|
kuncar@49638
|
475 |
apply (subst **)
|
kuncar@49638
|
476 |
apply simp
|
kuncar@49638
|
477 |
done
|
kuncar@49638
|
478 |
qed
|
kuncar@49638
|
479 |
|
kuncar@49638
|
480 |
(* maximum *)
|
kuncar@49638
|
481 |
|
kuncar@49638
|
482 |
lift_definition r_max :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max by simp
|
kuncar@49638
|
483 |
|
kuncar@49638
|
484 |
lift_definition r_max_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max_opt by simp
|
kuncar@49638
|
485 |
|
kuncar@49638
|
486 |
lemma r_max_alt_def: "r_max t = fold1_keys max t"
|
kuncar@49638
|
487 |
by transfer (simp add: rbt_max_def)
|
kuncar@49638
|
488 |
|
kuncar@49638
|
489 |
lemma r_max_eq_r_max_opt:
|
kuncar@49638
|
490 |
assumes "\<not> (is_empty t)"
|
kuncar@49638
|
491 |
shows "r_max t = r_max_opt t"
|
kuncar@49638
|
492 |
using assms unfolding is_empty_empty by transfer (auto intro: rbt_max_eq_rbt_max_opt)
|
kuncar@49638
|
493 |
|
kuncar@49638
|
494 |
lemma fold_keys_max_bot_eq:
|
kuncar@49638
|
495 |
fixes t :: "('a :: {linorder, bounded_lattice_bot}, unit) rbt"
|
kuncar@49638
|
496 |
assumes "\<not> (is_empty t)"
|
kuncar@49638
|
497 |
shows "fold_keys max t bot = fold1_keys max t"
|
kuncar@49638
|
498 |
proof -
|
kuncar@49638
|
499 |
have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold max (RBT_Impl.keys t) bot =
|
kuncar@49638
|
500 |
List.fold max (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) bot"
|
kuncar@49638
|
501 |
by (simp add: hd_Cons_tl[symmetric])
|
kuncar@49638
|
502 |
{ fix x :: "_ :: {linorder, bounded_lattice_bot}" and xs
|
kuncar@49638
|
503 |
have "List.fold max (x#xs) bot = List.fold max xs x"
|
kuncar@49638
|
504 |
by (simp add: sup_max[symmetric])
|
kuncar@49638
|
505 |
} note ** = this
|
kuncar@49638
|
506 |
show ?thesis using assms
|
kuncar@49638
|
507 |
unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
|
kuncar@49638
|
508 |
apply transfer
|
kuncar@49638
|
509 |
apply (case_tac t)
|
kuncar@49638
|
510 |
apply simp
|
kuncar@49638
|
511 |
apply (subst *)
|
kuncar@49638
|
512 |
apply simp
|
kuncar@49638
|
513 |
apply (subst **)
|
kuncar@49638
|
514 |
apply simp
|
kuncar@49638
|
515 |
done
|
kuncar@49638
|
516 |
qed
|
kuncar@49638
|
517 |
|
kuncar@49638
|
518 |
|
kuncar@49638
|
519 |
section {* Code equations *}
|
kuncar@49638
|
520 |
|
kuncar@49638
|
521 |
code_datatype Set Coset
|
kuncar@49638
|
522 |
|
kuncar@52178
|
523 |
declare set.simps[code]
|
kuncar@52178
|
524 |
|
kuncar@49638
|
525 |
lemma empty_Set [code]:
|
kuncar@49638
|
526 |
"Set.empty = Set RBT.empty"
|
kuncar@49638
|
527 |
by (auto simp: Set_def)
|
kuncar@49638
|
528 |
|
kuncar@49638
|
529 |
lemma UNIV_Coset [code]:
|
kuncar@49638
|
530 |
"UNIV = Coset RBT.empty"
|
kuncar@49638
|
531 |
by (auto simp: Set_def)
|
kuncar@49638
|
532 |
|
kuncar@49638
|
533 |
lemma is_empty_Set [code]:
|
kuncar@49638
|
534 |
"Set.is_empty (Set t) = RBT.is_empty t"
|
kuncar@49638
|
535 |
unfolding Set.is_empty_def by (auto simp: fun_eq_iff Set_def intro: lookup_empty_empty[THEN iffD1])
|
kuncar@49638
|
536 |
|
kuncar@49638
|
537 |
lemma compl_code [code]:
|
kuncar@49638
|
538 |
"- Set xs = Coset xs"
|
kuncar@49638
|
539 |
"- Coset xs = Set xs"
|
kuncar@49638
|
540 |
by (simp_all add: Set_def)
|
kuncar@49638
|
541 |
|
kuncar@49638
|
542 |
lemma member_code [code]:
|
kuncar@49638
|
543 |
"x \<in> (Set t) = (RBT.lookup t x = Some ())"
|
kuncar@49638
|
544 |
"x \<in> (Coset t) = (RBT.lookup t x = None)"
|
kuncar@49638
|
545 |
by (simp_all add: Set_def)
|
kuncar@49638
|
546 |
|
kuncar@49638
|
547 |
lemma insert_code [code]:
|
kuncar@49638
|
548 |
"Set.insert x (Set t) = Set (RBT.insert x () t)"
|
kuncar@49638
|
549 |
"Set.insert x (Coset t) = Coset (RBT.delete x t)"
|
kuncar@49638
|
550 |
by (auto simp: Set_def)
|
kuncar@49638
|
551 |
|
kuncar@49638
|
552 |
lemma remove_code [code]:
|
kuncar@49638
|
553 |
"Set.remove x (Set t) = Set (RBT.delete x t)"
|
kuncar@49638
|
554 |
"Set.remove x (Coset t) = Coset (RBT.insert x () t)"
|
kuncar@49638
|
555 |
by (auto simp: Set_def)
|
kuncar@49638
|
556 |
|
kuncar@49638
|
557 |
lemma union_Set [code]:
|
kuncar@49638
|
558 |
"Set t \<union> A = fold_keys Set.insert t A"
|
kuncar@49638
|
559 |
proof -
|
kuncar@49638
|
560 |
interpret comp_fun_idem Set.insert
|
kuncar@49638
|
561 |
by (fact comp_fun_idem_insert)
|
kuncar@49638
|
562 |
from finite_fold_fold_keys[OF `comp_fun_commute Set.insert`]
|
kuncar@49638
|
563 |
show ?thesis by (auto simp add: union_fold_insert)
|
kuncar@49638
|
564 |
qed
|
kuncar@49638
|
565 |
|
kuncar@49638
|
566 |
lemma inter_Set [code]:
|
kuncar@49638
|
567 |
"A \<inter> Set t = rbt_filter (\<lambda>k. k \<in> A) t"
|
kuncar@50773
|
568 |
by (simp add: inter_Set_filter Set_filter_rbt_filter)
|
kuncar@49638
|
569 |
|
kuncar@49638
|
570 |
lemma minus_Set [code]:
|
kuncar@49638
|
571 |
"A - Set t = fold_keys Set.remove t A"
|
kuncar@49638
|
572 |
proof -
|
kuncar@49638
|
573 |
interpret comp_fun_idem Set.remove
|
kuncar@49638
|
574 |
by (fact comp_fun_idem_remove)
|
kuncar@49638
|
575 |
from finite_fold_fold_keys[OF `comp_fun_commute Set.remove`]
|
kuncar@49638
|
576 |
show ?thesis by (auto simp add: minus_fold_remove)
|
kuncar@49638
|
577 |
qed
|
kuncar@49638
|
578 |
|
kuncar@49638
|
579 |
lemma union_Coset [code]:
|
kuncar@49638
|
580 |
"Coset t \<union> A = - rbt_filter (\<lambda>k. k \<notin> A) t"
|
kuncar@49638
|
581 |
proof -
|
kuncar@49638
|
582 |
have *: "\<And>A B. (-A \<union> B) = -(-B \<inter> A)" by blast
|
kuncar@49638
|
583 |
show ?thesis by (simp del: boolean_algebra_class.compl_inf add: * inter_Set)
|
kuncar@49638
|
584 |
qed
|
kuncar@49638
|
585 |
|
kuncar@49638
|
586 |
lemma union_Set_Set [code]:
|
kuncar@49638
|
587 |
"Set t1 \<union> Set t2 = Set (union t1 t2)"
|
kuncar@49638
|
588 |
by (auto simp add: lookup_union map_add_Some_iff Set_def)
|
kuncar@49638
|
589 |
|
kuncar@49638
|
590 |
lemma inter_Coset [code]:
|
kuncar@49638
|
591 |
"A \<inter> Coset t = fold_keys Set.remove t A"
|
kuncar@49638
|
592 |
by (simp add: Diff_eq [symmetric] minus_Set)
|
kuncar@49638
|
593 |
|
kuncar@49638
|
594 |
lemma inter_Coset_Coset [code]:
|
kuncar@49638
|
595 |
"Coset t1 \<inter> Coset t2 = Coset (union t1 t2)"
|
kuncar@49638
|
596 |
by (auto simp add: lookup_union map_add_Some_iff Set_def)
|
kuncar@49638
|
597 |
|
kuncar@49638
|
598 |
lemma minus_Coset [code]:
|
kuncar@49638
|
599 |
"A - Coset t = rbt_filter (\<lambda>k. k \<in> A) t"
|
kuncar@49638
|
600 |
by (simp add: inter_Set[simplified Int_commute])
|
kuncar@49638
|
601 |
|
kuncar@50772
|
602 |
lemma filter_Set [code]:
|
kuncar@50772
|
603 |
"Set.filter P (Set t) = (rbt_filter P t)"
|
kuncar@50773
|
604 |
by (auto simp add: Set_filter_rbt_filter)
|
kuncar@49638
|
605 |
|
kuncar@49638
|
606 |
lemma image_Set [code]:
|
kuncar@49638
|
607 |
"image f (Set t) = fold_keys (\<lambda>k A. Set.insert (f k) A) t {}"
|
kuncar@49638
|
608 |
proof -
|
kuncar@49638
|
609 |
have "comp_fun_commute (\<lambda>k. Set.insert (f k))" by default auto
|
kuncar@49638
|
610 |
then show ?thesis by (auto simp add: image_fold_insert intro!: finite_fold_fold_keys)
|
kuncar@49638
|
611 |
qed
|
kuncar@49638
|
612 |
|
kuncar@49638
|
613 |
lemma Ball_Set [code]:
|
kuncar@49638
|
614 |
"Ball (Set t) P \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t True"
|
kuncar@49638
|
615 |
proof -
|
kuncar@49638
|
616 |
have "comp_fun_commute (\<lambda>k s. s \<and> P k)" by default auto
|
kuncar@49638
|
617 |
then show ?thesis
|
kuncar@49638
|
618 |
by (simp add: foldi_fold_conj[symmetric] Ball_fold finite_fold_fold_keys)
|
kuncar@49638
|
619 |
qed
|
kuncar@49638
|
620 |
|
kuncar@49638
|
621 |
lemma Bex_Set [code]:
|
kuncar@49638
|
622 |
"Bex (Set t) P \<longleftrightarrow> foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t False"
|
kuncar@49638
|
623 |
proof -
|
kuncar@49638
|
624 |
have "comp_fun_commute (\<lambda>k s. s \<or> P k)" by default auto
|
kuncar@49638
|
625 |
then show ?thesis
|
kuncar@49638
|
626 |
by (simp add: foldi_fold_disj[symmetric] Bex_fold finite_fold_fold_keys)
|
kuncar@49638
|
627 |
qed
|
kuncar@49638
|
628 |
|
kuncar@49638
|
629 |
lemma subset_code [code]:
|
kuncar@49638
|
630 |
"Set t \<le> B \<longleftrightarrow> (\<forall>x\<in>Set t. x \<in> B)"
|
kuncar@49638
|
631 |
"A \<le> Coset t \<longleftrightarrow> (\<forall>y\<in>Set t. y \<notin> A)"
|
kuncar@49638
|
632 |
by auto
|
kuncar@49638
|
633 |
|
kuncar@49638
|
634 |
lemma subset_Coset_empty_Set_empty [code]:
|
kuncar@49638
|
635 |
"Coset t1 \<le> Set t2 \<longleftrightarrow> (case (impl_of t1, impl_of t2) of
|
kuncar@49638
|
636 |
(rbt.Empty, rbt.Empty) => False |
|
Andreas@54882
|
637 |
(_, _) => Code.abort (STR ''non_empty_trees'') (\<lambda>_. Coset t1 \<le> Set t2))"
|
kuncar@49638
|
638 |
proof -
|
kuncar@49638
|
639 |
have *: "\<And>t. impl_of t = rbt.Empty \<Longrightarrow> t = RBT rbt.Empty"
|
kuncar@49638
|
640 |
by (subst(asm) RBT_inverse[symmetric]) (auto simp: impl_of_inject)
|
kuncar@49638
|
641 |
have **: "Lifting.invariant is_rbt rbt.Empty rbt.Empty" unfolding Lifting.invariant_def by simp
|
kuncar@49638
|
642 |
show ?thesis
|
Andreas@54882
|
643 |
by (auto simp: Set_def lookup.abs_eq[OF **] dest!: * split: rbt.split)
|
kuncar@49638
|
644 |
qed
|
kuncar@49638
|
645 |
|
kuncar@49638
|
646 |
text {* A frequent case – avoid intermediate sets *}
|
kuncar@49638
|
647 |
lemma [code_unfold]:
|
kuncar@49638
|
648 |
"Set t1 \<subseteq> Set t2 \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> k \<in> Set t2) t1 True"
|
kuncar@49638
|
649 |
by (simp add: subset_code Ball_Set)
|
kuncar@49638
|
650 |
|
kuncar@49638
|
651 |
lemma card_Set [code]:
|
kuncar@49638
|
652 |
"card (Set t) = fold_keys (\<lambda>_ n. n + 1) t 0"
|
haftmann@52626
|
653 |
by (auto simp add: card.eq_fold intro: finite_fold_fold_keys comp_fun_commute_const)
|
kuncar@49638
|
654 |
|
kuncar@49638
|
655 |
lemma setsum_Set [code]:
|
kuncar@49638
|
656 |
"setsum f (Set xs) = fold_keys (plus o f) xs 0"
|
kuncar@49638
|
657 |
proof -
|
kuncar@49638
|
658 |
have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: add_ac)
|
kuncar@49638
|
659 |
then show ?thesis
|
haftmann@52626
|
660 |
by (auto simp add: setsum.eq_fold finite_fold_fold_keys o_def)
|
kuncar@49638
|
661 |
qed
|
kuncar@49638
|
662 |
|
kuncar@49638
|
663 |
lemma the_elem_set [code]:
|
kuncar@49638
|
664 |
fixes t :: "('a :: linorder, unit) rbt"
|
kuncar@49638
|
665 |
shows "the_elem (Set t) = (case impl_of t of
|
kuncar@49638
|
666 |
(Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty) \<Rightarrow> x
|
Andreas@54882
|
667 |
| _ \<Rightarrow> Code.abort (STR ''not_a_singleton_tree'') (\<lambda>_. the_elem (Set t)))"
|
kuncar@49638
|
668 |
proof -
|
kuncar@49638
|
669 |
{
|
kuncar@49638
|
670 |
fix x :: "'a :: linorder"
|
kuncar@49638
|
671 |
let ?t = "Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty"
|
kuncar@49638
|
672 |
have *:"?t \<in> {t. is_rbt t}" unfolding is_rbt_def by auto
|
kuncar@49638
|
673 |
then have **:"Lifting.invariant is_rbt ?t ?t" unfolding Lifting.invariant_def by auto
|
kuncar@49638
|
674 |
|
kuncar@49638
|
675 |
have "impl_of t = ?t \<Longrightarrow> the_elem (Set t) = x"
|
kuncar@49638
|
676 |
by (subst(asm) RBT_inverse[symmetric, OF *])
|
kuncar@49638
|
677 |
(auto simp: Set_def the_elem_def lookup.abs_eq[OF **] impl_of_inject)
|
kuncar@49638
|
678 |
}
|
Andreas@54882
|
679 |
then show ?thesis
|
kuncar@49638
|
680 |
by(auto split: rbt.split unit.split color.split)
|
kuncar@49638
|
681 |
qed
|
kuncar@49638
|
682 |
|
kuncar@49638
|
683 |
lemma Pow_Set [code]:
|
kuncar@49638
|
684 |
"Pow (Set t) = fold_keys (\<lambda>x A. A \<union> Set.insert x ` A) t {{}}"
|
kuncar@49638
|
685 |
by (simp add: Pow_fold finite_fold_fold_keys[OF comp_fun_commute_Pow_fold])
|
kuncar@49638
|
686 |
|
kuncar@49638
|
687 |
lemma product_Set [code]:
|
kuncar@49638
|
688 |
"Product_Type.product (Set t1) (Set t2) =
|
kuncar@49638
|
689 |
fold_keys (\<lambda>x A. fold_keys (\<lambda>y. Set.insert (x, y)) t2 A) t1 {}"
|
kuncar@49638
|
690 |
proof -
|
kuncar@49638
|
691 |
have *:"\<And>x. comp_fun_commute (\<lambda>y. Set.insert (x, y))" by default auto
|
kuncar@49638
|
692 |
show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_product_fold, of "Set t2" "{}" "t1"]
|
kuncar@49638
|
693 |
by (simp add: product_fold Product_Type.product_def finite_fold_fold_keys[OF *])
|
kuncar@49638
|
694 |
qed
|
kuncar@49638
|
695 |
|
kuncar@49638
|
696 |
lemma Id_on_Set [code]:
|
kuncar@49638
|
697 |
"Id_on (Set t) = fold_keys (\<lambda>x. Set.insert (x, x)) t {}"
|
kuncar@49638
|
698 |
proof -
|
kuncar@49638
|
699 |
have "comp_fun_commute (\<lambda>x. Set.insert (x, x))" by default auto
|
kuncar@49638
|
700 |
then show ?thesis
|
kuncar@49638
|
701 |
by (auto simp add: Id_on_fold intro!: finite_fold_fold_keys)
|
kuncar@49638
|
702 |
qed
|
kuncar@49638
|
703 |
|
kuncar@49638
|
704 |
lemma Image_Set [code]:
|
kuncar@49638
|
705 |
"(Set t) `` S = fold_keys (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A) t {}"
|
kuncar@49638
|
706 |
by (auto simp add: Image_fold finite_fold_fold_keys[OF comp_fun_commute_Image_fold])
|
kuncar@49638
|
707 |
|
kuncar@49638
|
708 |
lemma trancl_set_ntrancl [code]:
|
kuncar@49638
|
709 |
"trancl (Set t) = ntrancl (card (Set t) - 1) (Set t)"
|
kuncar@49638
|
710 |
by (simp add: finite_trancl_ntranl)
|
kuncar@49638
|
711 |
|
kuncar@49638
|
712 |
lemma relcomp_Set[code]:
|
kuncar@49638
|
713 |
"(Set t1) O (Set t2) = fold_keys
|
kuncar@49638
|
714 |
(\<lambda>(x,y) A. fold_keys (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') t2 A) t1 {}"
|
kuncar@49638
|
715 |
proof -
|
kuncar@49638
|
716 |
interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
|
kuncar@49638
|
717 |
have *: "\<And>x y. comp_fun_commute (\<lambda>(w, z) A'. if y = w then Set.insert (x, z) A' else A')"
|
kuncar@49638
|
718 |
by default (auto simp add: fun_eq_iff)
|
kuncar@49638
|
719 |
show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_relcomp_fold, of "Set t2" "{}" t1]
|
kuncar@49638
|
720 |
by (simp add: relcomp_fold finite_fold_fold_keys[OF *])
|
kuncar@49638
|
721 |
qed
|
kuncar@49638
|
722 |
|
kuncar@49638
|
723 |
lemma wf_set [code]:
|
kuncar@49638
|
724 |
"wf (Set t) = acyclic (Set t)"
|
kuncar@49638
|
725 |
by (simp add: wf_iff_acyclic_if_finite)
|
kuncar@49638
|
726 |
|
kuncar@49638
|
727 |
lemma Min_fin_set_fold [code]:
|
Andreas@54882
|
728 |
"Min (Set t) =
|
Andreas@54882
|
729 |
(if is_empty t
|
Andreas@54882
|
730 |
then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Min (Set t))
|
Andreas@54882
|
731 |
else r_min_opt t)"
|
kuncar@49638
|
732 |
proof -
|
haftmann@52626
|
733 |
have *: "semilattice (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" ..
|
haftmann@52626
|
734 |
with finite_fold1_fold1_keys [OF *, folded Min_def]
|
kuncar@49638
|
735 |
show ?thesis
|
Andreas@54882
|
736 |
by (simp add: r_min_alt_def r_min_eq_r_min_opt [symmetric])
|
kuncar@49638
|
737 |
qed
|
kuncar@49638
|
738 |
|
kuncar@49638
|
739 |
lemma Inf_fin_set_fold [code]:
|
kuncar@49638
|
740 |
"Inf_fin (Set t) = Min (Set t)"
|
kuncar@49638
|
741 |
by (simp add: inf_min Inf_fin_def Min_def)
|
kuncar@49638
|
742 |
|
kuncar@49638
|
743 |
lemma Inf_Set_fold:
|
kuncar@49638
|
744 |
fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
|
kuncar@49638
|
745 |
shows "Inf (Set t) = (if is_empty t then top else r_min_opt t)"
|
kuncar@49638
|
746 |
proof -
|
kuncar@49638
|
747 |
have "comp_fun_commute (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
|
kuncar@49638
|
748 |
then have "t \<noteq> empty \<Longrightarrow> Finite_Set.fold min top (Set t) = fold1_keys min t"
|
kuncar@49638
|
749 |
by (simp add: finite_fold_fold_keys fold_keys_min_top_eq)
|
kuncar@49638
|
750 |
then show ?thesis
|
kuncar@49638
|
751 |
by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric] r_min_eq_r_min_opt[symmetric] r_min_alt_def)
|
kuncar@49638
|
752 |
qed
|
kuncar@49638
|
753 |
|
kuncar@49638
|
754 |
definition Inf' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Inf' x = Inf x"
|
kuncar@49638
|
755 |
declare Inf'_def[symmetric, code_unfold]
|
kuncar@49638
|
756 |
declare Inf_Set_fold[folded Inf'_def, code]
|
kuncar@49638
|
757 |
|
kuncar@49638
|
758 |
lemma INFI_Set_fold [code]:
|
hoelzl@55715
|
759 |
fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
|
hoelzl@55715
|
760 |
shows "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
|
kuncar@49638
|
761 |
proof -
|
kuncar@49638
|
762 |
have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)"
|
kuncar@49638
|
763 |
by default (auto simp add: fun_eq_iff ac_simps)
|
kuncar@49638
|
764 |
then show ?thesis
|
kuncar@49638
|
765 |
by (auto simp: INF_fold_inf finite_fold_fold_keys)
|
kuncar@49638
|
766 |
qed
|
kuncar@49638
|
767 |
|
kuncar@49638
|
768 |
lemma Max_fin_set_fold [code]:
|
Andreas@54882
|
769 |
"Max (Set t) =
|
Andreas@54882
|
770 |
(if is_empty t
|
Andreas@54882
|
771 |
then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Max (Set t))
|
Andreas@54882
|
772 |
else r_max_opt t)"
|
kuncar@49638
|
773 |
proof -
|
haftmann@52626
|
774 |
have *: "semilattice (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" ..
|
haftmann@52626
|
775 |
with finite_fold1_fold1_keys [OF *, folded Max_def]
|
kuncar@49638
|
776 |
show ?thesis
|
Andreas@54882
|
777 |
by (simp add: r_max_alt_def r_max_eq_r_max_opt [symmetric])
|
kuncar@49638
|
778 |
qed
|
kuncar@49638
|
779 |
|
kuncar@49638
|
780 |
lemma Sup_fin_set_fold [code]:
|
kuncar@49638
|
781 |
"Sup_fin (Set t) = Max (Set t)"
|
kuncar@49638
|
782 |
by (simp add: sup_max Sup_fin_def Max_def)
|
kuncar@49638
|
783 |
|
kuncar@49638
|
784 |
lemma Sup_Set_fold:
|
kuncar@49638
|
785 |
fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
|
kuncar@49638
|
786 |
shows "Sup (Set t) = (if is_empty t then bot else r_max_opt t)"
|
kuncar@49638
|
787 |
proof -
|
kuncar@49638
|
788 |
have "comp_fun_commute (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
|
kuncar@49638
|
789 |
then have "t \<noteq> empty \<Longrightarrow> Finite_Set.fold max bot (Set t) = fold1_keys max t"
|
kuncar@49638
|
790 |
by (simp add: finite_fold_fold_keys fold_keys_max_bot_eq)
|
kuncar@49638
|
791 |
then show ?thesis
|
kuncar@49638
|
792 |
by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric] r_max_eq_r_max_opt[symmetric] r_max_alt_def)
|
kuncar@49638
|
793 |
qed
|
kuncar@49638
|
794 |
|
kuncar@49638
|
795 |
definition Sup' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Sup' x = Sup x"
|
kuncar@49638
|
796 |
declare Sup'_def[symmetric, code_unfold]
|
kuncar@49638
|
797 |
declare Sup_Set_fold[folded Sup'_def, code]
|
kuncar@49638
|
798 |
|
kuncar@49638
|
799 |
lemma SUPR_Set_fold [code]:
|
hoelzl@55715
|
800 |
fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
|
hoelzl@55715
|
801 |
shows "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
|
kuncar@49638
|
802 |
proof -
|
kuncar@49638
|
803 |
have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)"
|
kuncar@49638
|
804 |
by default (auto simp add: fun_eq_iff ac_simps)
|
kuncar@49638
|
805 |
then show ?thesis
|
kuncar@49638
|
806 |
by (auto simp: SUP_fold_sup finite_fold_fold_keys)
|
kuncar@49638
|
807 |
qed
|
kuncar@49638
|
808 |
|
kuncar@49638
|
809 |
lemma sorted_list_set[code]:
|
kuncar@49638
|
810 |
"sorted_list_of_set (Set t) = keys t"
|
kuncar@49638
|
811 |
by (auto simp add: set_keys intro: sorted_distinct_set_unique)
|
kuncar@49638
|
812 |
|
nipkow@55092
|
813 |
lemma Bleast_code [code]:
|
nipkow@55092
|
814 |
"Bleast (Set t) P = (case filter P (keys t) of
|
nipkow@55092
|
815 |
x#xs \<Rightarrow> x |
|
nipkow@55092
|
816 |
[] \<Rightarrow> abort_Bleast (Set t) P)"
|
nipkow@55092
|
817 |
proof (cases "filter P (keys t)")
|
nipkow@55092
|
818 |
case Nil thus ?thesis by (simp add: Bleast_def abort_Bleast_def)
|
nipkow@55092
|
819 |
next
|
nipkow@55092
|
820 |
case (Cons x ys)
|
nipkow@55092
|
821 |
have "(LEAST x. x \<in> Set t \<and> P x) = x"
|
nipkow@55092
|
822 |
proof (rule Least_equality)
|
nipkow@55092
|
823 |
show "x \<in> Set t \<and> P x" using Cons[symmetric]
|
nipkow@55092
|
824 |
by(auto simp add: set_keys Cons_eq_filter_iff)
|
nipkow@55092
|
825 |
next
|
nipkow@55092
|
826 |
fix y assume "y : Set t \<and> P y"
|
nipkow@55092
|
827 |
then show "x \<le> y" using Cons[symmetric]
|
nipkow@55092
|
828 |
by(auto simp add: set_keys Cons_eq_filter_iff)
|
nipkow@55092
|
829 |
(metis sorted_Cons sorted_append sorted_keys)
|
nipkow@55092
|
830 |
qed
|
nipkow@55092
|
831 |
thus ?thesis using Cons by (simp add: Bleast_def)
|
nipkow@55092
|
832 |
qed
|
nipkow@55092
|
833 |
|
nipkow@55092
|
834 |
|
kuncar@49638
|
835 |
hide_const (open) RBT_Set.Set RBT_Set.Coset
|
kuncar@49638
|
836 |
|
kuncar@49638
|
837 |
end
|