1(* Author: Tobias Nipkow *)
2
3section "Join-Based Implementation of Sets"
4
5theory Set2_Join
6imports
7  Isin2
8begin
9
10text \<open>This theory implements the set operations \<open>insert\<close>, \<open>delete\<close>,
11\<open>union\<close>, \<open>inter\<close>section and \<open>diff\<close>erence. The implementation is based on binary search trees.
12All operations are reduced to a single operation \<open>join l x r\<close> that joins two BSTs \<open>l\<close> and \<open>r\<close>
13and an element \<open>x\<close> such that \<open>l < x < r\<close>.
14
15The theory is based on theory @{theory "HOL-Data_Structures.Tree2"} where nodes have an additional field.
16This field is ignored here but it means that this theory can be instantiated
17with red-black trees (see theory @{file "Set2_Join_RBT.thy"}) and other balanced trees.
18This approach is very concrete and fixes the type of trees.
19Alternatively, one could assume some abstract type @{typ 't} of trees with suitable decomposition
20and recursion operators on it.\<close>
21
22locale Set2_Join =
23fixes join :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree"
24fixes inv :: "('a,'b) tree \<Rightarrow> bool"
25assumes set_join: "set_tree (join l a r) = set_tree l \<union> {a} \<union> set_tree r"
26assumes bst_join:
27  "\<lbrakk> bst l; bst r; \<forall>x \<in> set_tree l. x < a; \<forall>y \<in> set_tree r. a < y \<rbrakk>
28  \<Longrightarrow> bst (join l a r)"
29assumes inv_Leaf: "inv \<langle>\<rangle>"
30assumes inv_join: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join l k r)"
31assumes inv_Node: "\<lbrakk> inv (Node l x h r) \<rbrakk> \<Longrightarrow> inv l \<and> inv r"
32begin
33
34declare set_join [simp]
35
36subsection "\<open>split_min\<close>"
37
38fun split_min :: "('a,'b) tree \<Rightarrow> 'a \<times> ('a,'b) tree" where
39"split_min (Node l x _ r) =
40  (if l = Leaf then (x,r) else let (m,l') = split_min l in (m, join l' x r))"
41
42lemma split_min_set:
43  "\<lbrakk> split_min t = (x,t');  t \<noteq> Leaf \<rbrakk> \<Longrightarrow> x \<in> set_tree t \<and> set_tree t = Set.insert x (set_tree t')"
44proof(induction t arbitrary: t')
45  case Node thus ?case by(auto split: prod.splits if_splits dest: inv_Node)
46next
47  case Leaf thus ?case by simp
48qed
49
50lemma split_min_bst:
51  "\<lbrakk> split_min t = (x,t');  bst t;  t \<noteq> Leaf \<rbrakk> \<Longrightarrow>  bst t' \<and> (\<forall>x' \<in> set_tree t'. x < x')"
52proof(induction t arbitrary: t')
53  case Node thus ?case by(fastforce simp: split_min_set bst_join split: prod.splits if_splits)
54next
55  case Leaf thus ?case by simp
56qed
57
58lemma split_min_inv:
59  "\<lbrakk> split_min t = (x,t');  inv t;  t \<noteq> Leaf \<rbrakk> \<Longrightarrow>  inv t'"
60proof(induction t arbitrary: t')
61  case Node thus ?case by(auto simp: inv_join split: prod.splits if_splits dest: inv_Node)
62next
63  case Leaf thus ?case by simp
64qed
65
66
67subsection "\<open>join2\<close>"
68
69definition join2 :: "('a,'b) tree \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where
70"join2 l r = (if r = Leaf then l else let (x,r') = split_min r in join l x r')"
71
72lemma set_join2[simp]: "set_tree (join2 l r) = set_tree l \<union> set_tree r"
73by(simp add: join2_def split_min_set split: prod.split)
74
75lemma bst_join2: "\<lbrakk> bst l; bst r; \<forall>x \<in> set_tree l. \<forall>y \<in> set_tree r. x < y \<rbrakk>
76  \<Longrightarrow> bst (join2 l r)"
77by(simp add: join2_def bst_join split_min_set split_min_bst split: prod.split)
78
79lemma inv_join2: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join2 l r)"
80by(simp add: join2_def inv_join split_min_set split_min_inv split: prod.split)
81
82
83subsection "\<open>split\<close>"
84
85fun split :: "('a,'b)tree \<Rightarrow> 'a \<Rightarrow> ('a,'b)tree \<times> bool \<times> ('a,'b)tree" where
86"split Leaf k = (Leaf, False, Leaf)" |
87"split (Node l a _ r) k =
88  (if k < a then let (l1,b,l2) = split l k in (l1, b, join l2 a r) else
89   if a < k then let (r1,b,r2) = split r k in (join l a r1, b, r2)
90   else (l, True, r))"
91
92lemma split: "split t k = (l,kin,r) \<Longrightarrow> bst t \<Longrightarrow>
93  set_tree l = {x \<in> set_tree t. x < k} \<and> set_tree r = {x \<in> set_tree t. k < x}
94  \<and> (kin = (k \<in> set_tree t)) \<and> bst l \<and> bst r"
95proof(induction t arbitrary: l kin r)
96  case Leaf thus ?case by simp
97next
98  case Node thus ?case by(force split!: prod.splits if_splits intro!: bst_join)
99qed
100
101lemma split_inv: "split t k = (l,kin,r) \<Longrightarrow> inv t \<Longrightarrow> inv l \<and> inv r"
102proof(induction t arbitrary: l kin r)
103  case Leaf thus ?case by simp
104next
105  case Node
106  thus ?case by(force simp: inv_join split!: prod.splits if_splits dest!: inv_Node)
107qed
108
109declare split.simps[simp del]
110
111
112subsection "\<open>insert\<close>"
113
114definition insert :: "'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where
115"insert k t = (let (l,_,r) = split t k in join l k r)"
116
117lemma set_tree_insert: "bst t \<Longrightarrow> set_tree (insert x t) = Set.insert x (set_tree t)"
118by(auto simp add: insert_def split split: prod.split)
119
120lemma bst_insert: "bst t \<Longrightarrow> bst (insert x t)"
121by(auto simp add: insert_def bst_join dest: split split: prod.split)
122
123lemma inv_insert: "inv t \<Longrightarrow> inv (insert x t)"
124by(force simp: insert_def inv_join dest: split_inv split: prod.split)
125
126
127subsection "\<open>delete\<close>"
128
129definition delete :: "'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where
130"delete k t = (let (l,_,r) = split t k in join2 l r)"
131
132lemma set_tree_delete: "bst t \<Longrightarrow> set_tree (delete k t) = set_tree t - {k}"
133by(auto simp: delete_def split split: prod.split)
134
135lemma bst_delete: "bst t \<Longrightarrow> bst (delete x t)"
136by(force simp add: delete_def intro: bst_join2 dest: split split: prod.split)
137
138lemma inv_delete: "inv t \<Longrightarrow> inv (delete x t)"
139by(force simp: delete_def inv_join2 dest: split_inv split: prod.split)
140
141
142subsection "\<open>union\<close>"
143
144fun union :: "('a,'b)tree \<Rightarrow> ('a,'b)tree \<Rightarrow> ('a,'b)tree" where
145"union t1 t2 =
146  (if t1 = Leaf then t2 else
147   if t2 = Leaf then t1 else
148   case t1 of Node l1 k _ r1 \<Rightarrow>
149   let (l2,_ ,r2) = split t2 k;
150       l' = union l1 l2; r' = union r1 r2
151   in join l' k r')"
152
153declare union.simps [simp del]
154
155lemma set_tree_union: "bst t2 \<Longrightarrow> set_tree (union t1 t2) = set_tree t1 \<union> set_tree t2"
156proof(induction t1 t2 rule: union.induct)
157  case (1 t1 t2)
158  then show ?case
159    by (auto simp: union.simps[of t1 t2] split split: tree.split prod.split)
160qed
161
162lemma bst_union: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (union t1 t2)"
163proof(induction t1 t2 rule: union.induct)
164  case (1 t1 t2)
165  thus ?case
166    by(fastforce simp: union.simps[of t1 t2] set_tree_union split intro!: bst_join 
167        split: tree.split prod.split)
168qed
169
170lemma inv_union: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (union t1 t2)"
171proof(induction t1 t2 rule: union.induct)
172  case (1 t1 t2)
173  thus ?case
174    by(auto simp:union.simps[of t1 t2] inv_join split_inv
175        split!: tree.split prod.split dest: inv_Node)
176qed
177
178subsection "\<open>inter\<close>"
179
180fun inter :: "('a,'b)tree \<Rightarrow> ('a,'b)tree \<Rightarrow> ('a,'b)tree" where
181"inter t1 t2 =
182  (if t1 = Leaf then Leaf else
183   if t2 = Leaf then Leaf else
184   case t1 of Node l1 k _ r1 \<Rightarrow>
185   let (l2,kin,r2) = split t2 k;
186       l' = inter l1 l2; r' = inter r1 r2
187   in if kin then join l' k r' else join2 l' r')"
188
189declare inter.simps [simp del]
190
191lemma set_tree_inter:
192  "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> set_tree (inter t1 t2) = set_tree t1 \<inter> set_tree t2"
193proof(induction t1 t2 rule: inter.induct)
194  case (1 t1 t2)
195  show ?case
196  proof (cases t1)
197    case Leaf thus ?thesis by (simp add: inter.simps)
198  next
199    case [simp]: (Node l1 k _ r1)
200    show ?thesis
201    proof (cases "t2 = Leaf")
202      case True thus ?thesis by (simp add: inter.simps)
203    next
204      case False
205      let ?L1 = "set_tree l1" let ?R1 = "set_tree r1"
206      have *: "k \<notin> ?L1 \<union> ?R1" using \<open>bst t1\<close> by (fastforce)
207      obtain l2 kin r2 where sp: "split t2 k = (l2,kin,r2)" using prod_cases3 by blast
208      let ?L2 = "set_tree l2" let ?R2 = "set_tree r2" let ?K = "if kin then {k} else {}"
209      have t2: "set_tree t2 = ?L2 \<union> ?R2 \<union> ?K" and
210           **: "?L2 \<inter> ?R2 = {}" "k \<notin> ?L2 \<union> ?R2" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}"
211        using split[OF sp] \<open>bst t1\<close> \<open>bst t2\<close> by (force, force, force, force, force)
212      have IHl: "set_tree (inter l1 l2) = set_tree l1 \<inter> set_tree l2"
213        using "1.IH"(1)[OF _ False _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
214      have IHr: "set_tree (inter r1 r2) = set_tree r1 \<inter> set_tree r2"
215        using "1.IH"(2)[OF _ False _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
216      have "set_tree t1 \<inter> set_tree t2 = (?L1 \<union> ?R1 \<union> {k}) \<inter> (?L2 \<union> ?R2 \<union> ?K)"
217        by(simp add: t2)
218      also have "\<dots> = (?L1 \<inter> ?L2) \<union> (?R1 \<inter> ?R2) \<union> ?K"
219        using * ** by auto
220      also have "\<dots> = set_tree (inter t1 t2)"
221      using IHl IHr sp inter.simps[of t1 t2] False by(simp)
222      finally show ?thesis by simp
223    qed
224  qed
225qed
226
227lemma bst_inter: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (inter t1 t2)"
228proof(induction t1 t2 rule: inter.induct)
229  case (1 t1 t2)
230  thus ?case
231    by(fastforce simp: inter.simps[of t1 t2] set_tree_inter split Let_def
232        intro!: bst_join bst_join2 split: tree.split prod.split)
233qed
234
235lemma inv_inter: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (inter t1 t2)"
236proof(induction t1 t2 rule: inter.induct)
237  case (1 t1 t2)
238  thus ?case
239    by(auto simp: inter.simps[of t1 t2] inv_join inv_join2 split_inv Let_def
240        split!: tree.split prod.split dest: inv_Node)
241qed
242
243subsection "\<open>diff\<close>"
244
245fun diff :: "('a,'b)tree \<Rightarrow> ('a,'b)tree \<Rightarrow> ('a,'b)tree" where
246"diff t1 t2 =
247  (if t1 = Leaf then Leaf else
248   if t2 = Leaf then t1 else
249   case t2 of Node l2 k _ r2 \<Rightarrow>
250   let (l1,_,r1) = split t1 k;
251       l' = diff l1 l2; r' = diff r1 r2
252   in join2 l' r')"
253
254declare diff.simps [simp del]
255
256lemma set_tree_diff:
257  "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> set_tree (diff t1 t2) = set_tree t1 - set_tree t2"
258proof(induction t1 t2 rule: diff.induct)
259  case (1 t1 t2)
260  show ?case
261  proof (cases t2)
262    case Leaf thus ?thesis by (simp add: diff.simps)
263  next
264    case [simp]: (Node l2 k _ r2)
265    show ?thesis
266    proof (cases "t1 = Leaf")
267      case True thus ?thesis by (simp add: diff.simps)
268    next
269      case False
270      let ?L2 = "set_tree l2" let ?R2 = "set_tree r2"
271      obtain l1 kin r1 where sp: "split t1 k = (l1,kin,r1)" using prod_cases3 by blast
272      let ?L1 = "set_tree l1" let ?R1 = "set_tree r1" let ?K = "if kin then {k} else {}"
273      have t1: "set_tree t1 = ?L1 \<union> ?R1 \<union> ?K" and
274           **: "k \<notin> ?L1 \<union> ?R1" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}"
275        using split[OF sp] \<open>bst t1\<close> \<open>bst t2\<close> by (force, force, force, force)
276      have IHl: "set_tree (diff l1 l2) = set_tree l1 - set_tree l2"
277        using "1.IH"(1)[OF False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
278      have IHr: "set_tree (diff r1 r2) = set_tree r1 - set_tree r2"
279        using "1.IH"(2)[OF False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
280      have "set_tree t1 - set_tree t2 = (?L1 \<union> ?R1) - (?L2 \<union> ?R2  \<union> {k})"
281        by(simp add: t1)
282      also have "\<dots> = (?L1 - ?L2) \<union> (?R1 - ?R2)"
283        using ** by auto
284      also have "\<dots> = set_tree (diff t1 t2)"
285      using IHl IHr sp diff.simps[of t1 t2] False by(simp)
286      finally show ?thesis by simp
287    qed
288  qed
289qed
290
291lemma bst_diff: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (diff t1 t2)"
292proof(induction t1 t2 rule: diff.induct)
293  case (1 t1 t2)
294  thus ?case
295    by(fastforce simp: diff.simps[of t1 t2] set_tree_diff split Let_def
296        intro!: bst_join bst_join2 split: tree.split prod.split)
297qed
298
299lemma inv_diff: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (diff t1 t2)"
300proof(induction t1 t2 rule: diff.induct)
301  case (1 t1 t2)
302  thus ?case
303    by(auto simp: diff.simps[of t1 t2] inv_join inv_join2 split_inv Let_def
304        split!: tree.split prod.split dest: inv_Node)
305qed
306
307text \<open>Locale @{locale Set2_Join} implements locale @{locale Set2}:\<close>
308
309sublocale Set2
310where empty = Leaf and insert = insert and delete = delete and isin = isin
311and union = union and inter = inter and diff = diff
312and set = set_tree and invar = "\<lambda>t. inv t \<and> bst t"
313proof (standard, goal_cases)
314  case 1 show ?case by (simp)
315next
316  case 2 thus ?case by(simp add: isin_set_tree)
317next
318  case 3 thus ?case by (simp add: set_tree_insert)
319next
320  case 4 thus ?case by (simp add: set_tree_delete)
321next
322  case 5 thus ?case by (simp add: inv_Leaf)
323next
324  case 6 thus ?case by (simp add: bst_insert inv_insert)
325next
326  case 7 thus ?case by (simp add: bst_delete inv_delete)
327next
328  case 8 thus ?case by(simp add: set_tree_union)
329next
330  case 9 thus ?case by(simp add: set_tree_inter)
331next
332  case 10 thus ?case by(simp add: set_tree_diff)
333next
334  case 11 thus ?case by (simp add: bst_union inv_union)
335next
336  case 12 thus ?case by (simp add: bst_inter inv_inter)
337next
338  case 13 thus ?case by (simp add: bst_diff inv_diff)
339qed
340
341end
342
343interpretation unbal: Set2_Join
344where join = "\<lambda>l x r. Node l x () r" and inv = "\<lambda>t. True"
345proof (standard, goal_cases)
346  case 1 show ?case by simp
347next
348  case 2 thus ?case by simp
349next
350  case 3 thus ?case by simp
351next
352  case 4 thus ?case by simp
353next
354  case 5 thus ?case by simp
355qed
356
357end