author | nipkow |
Mon, 12 Aug 2019 15:57:40 +0200 | |
changeset 70504 | 8d4abdbc6de9 |
parent 69597 | ff784d5a5bfb |
child 70582 | 7beee08eb163 |
permissions | -rw-r--r-- |
67966
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
1 |
(* Author: Tobias Nipkow *) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
2 |
|
68261 | 3 |
section "Join-Based Implementation of Sets via RBTs" |
67966
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
4 |
|
68261 | 5 |
theory Set2_Join_RBT |
67966
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
6 |
imports |
68261 | 7 |
Set2_Join |
67966
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
8 |
RBT_Set |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
9 |
begin |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
10 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
11 |
subsection "Code" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
12 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
13 |
text \<open> |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
14 |
Function \<open>joinL\<close> joins two trees (and an element). |
69597 | 15 |
Precondition: \<^prop>\<open>bheight l \<le> bheight r\<close>. |
67966
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
16 |
Method: |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
17 |
Descend along the left spine of \<open>r\<close> |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
18 |
until you find a subtree with the same \<open>bheight\<close> as \<open>l\<close>, |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
19 |
then combine them into a new red node. |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
20 |
\<close> |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
21 |
fun joinL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
22 |
"joinL l x r = |
70504 | 23 |
(if bheight l \<ge> bheight r then R l x r |
67966
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
24 |
else case r of |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
25 |
B l' x' r' \<Rightarrow> baliL (joinL l x l') x' r' | |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
26 |
R l' x' r' \<Rightarrow> R (joinL l x l') x' r')" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
27 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
28 |
fun joinR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
29 |
"joinR l x r = |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
30 |
(if bheight l \<le> bheight r then R l x r |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
31 |
else case l of |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
32 |
B l' x' r' \<Rightarrow> baliR l' x' (joinR r' x r) | |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
33 |
R l' x' r' \<Rightarrow> R l' x' (joinR r' x r))" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
34 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
35 |
fun join :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
36 |
"join l x r = |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
37 |
(if bheight l > bheight r |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
38 |
then paint Black (joinR l x r) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
39 |
else if bheight l < bheight r |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
40 |
then paint Black (joinL l x r) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
41 |
else B l x r)" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
42 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
43 |
declare joinL.simps[simp del] |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
44 |
declare joinR.simps[simp del] |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
45 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
46 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
47 |
subsection "Properties" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
48 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
49 |
subsubsection "Color and height invariants" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
50 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
51 |
lemma invc2_joinL: |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
52 |
"\<lbrakk> invc l; invc r; bheight l \<le> bheight r \<rbrakk> \<Longrightarrow> |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
53 |
invc2 (joinL l x r) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
54 |
\<and> (bheight l \<noteq> bheight r \<and> color r = Black \<longrightarrow> invc(joinL l x r))" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
55 |
proof (induct l x r rule: joinL.induct) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
56 |
case (1 l x r) thus ?case |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
57 |
by(auto simp: invc_baliL invc2I joinL.simps[of l x r] split!: tree.splits if_splits) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
58 |
qed |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
59 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
60 |
lemma invc2_joinR: |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
61 |
"\<lbrakk> invc l; invh l; invc r; invh r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow> |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
62 |
invc2 (joinR l x r) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
63 |
\<and> (bheight l \<noteq> bheight r \<and> color l = Black \<longrightarrow> invc(joinR l x r))" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
64 |
proof (induct l x r rule: joinR.induct) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
65 |
case (1 l x r) thus ?case |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
66 |
by(fastforce simp: invc_baliR invc2I joinR.simps[of l x r] split!: tree.splits if_splits) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
67 |
qed |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
68 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
69 |
lemma bheight_joinL: |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
70 |
"\<lbrakk> invh l; invh r; bheight l \<le> bheight r \<rbrakk> \<Longrightarrow> bheight (joinL l x r) = bheight r" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
71 |
proof (induct l x r rule: joinL.induct) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
72 |
case (1 l x r) thus ?case |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
73 |
by(auto simp: bheight_baliL joinL.simps[of l x r] split!: tree.split) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
74 |
qed |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
75 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
76 |
lemma invh_joinL: |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
77 |
"\<lbrakk> invh l; invh r; bheight l \<le> bheight r \<rbrakk> \<Longrightarrow> invh (joinL l x r)" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
78 |
proof (induct l x r rule: joinL.induct) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
79 |
case (1 l x r) thus ?case |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
80 |
by(auto simp: invh_baliL bheight_joinL joinL.simps[of l x r] split!: tree.split color.split) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
81 |
qed |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
82 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
83 |
lemma bheight_baliR: |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
84 |
"bheight l = bheight r \<Longrightarrow> bheight (baliR l a r) = Suc (bheight l)" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
85 |
by (cases "(l,a,r)" rule: baliR.cases) auto |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
86 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
87 |
lemma bheight_joinR: |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
88 |
"\<lbrakk> invh l; invh r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow> bheight (joinR l x r) = bheight l" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
89 |
proof (induct l x r rule: joinR.induct) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
90 |
case (1 l x r) thus ?case |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
91 |
by(fastforce simp: bheight_baliR joinR.simps[of l x r] split!: tree.split) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
92 |
qed |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
93 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
94 |
lemma invh_joinR: |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
95 |
"\<lbrakk> invh l; invh r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow> invh (joinR l x r)" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
96 |
proof (induct l x r rule: joinR.induct) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
97 |
case (1 l x r) thus ?case |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
98 |
by(fastforce simp: invh_baliR bheight_joinR joinR.simps[of l x r] |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
99 |
split!: tree.split color.split) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
100 |
qed |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
101 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
102 |
(* unused *) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
103 |
lemma rbt_join: "\<lbrakk> invc l; invh l; invc r; invh r \<rbrakk> \<Longrightarrow> rbt(join l x r)" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
104 |
by(simp add: invc2_joinL invc2_joinR invc_paint_Black invh_joinL invh_joinR invh_paint rbt_def |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
105 |
color_paint_Black) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
106 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
107 |
text \<open>To make sure the the black height is not increased unnecessarily:\<close> |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
108 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
109 |
lemma bheight_paint_Black: "bheight(paint Black t) \<le> bheight t + 1" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
110 |
by(cases t) auto |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
111 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
112 |
lemma "\<lbrakk> rbt l; rbt r \<rbrakk> \<Longrightarrow> bheight(join l x r) \<le> max (bheight l) (bheight r) + 1" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
113 |
using bheight_paint_Black[of "joinL l x r"] bheight_paint_Black[of "joinR l x r"] |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
114 |
bheight_joinL[of l r x] bheight_joinR[of l r x] |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
115 |
by(auto simp: max_def rbt_def) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
116 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
117 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
118 |
subsubsection "Inorder properties" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
119 |
|
69597 | 120 |
text "Currently unused. Instead \<^const>\<open>set_tree\<close> and \<^const>\<open>bst\<close> properties are proved directly." |
67966
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
121 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
122 |
lemma inorder_joinL: "bheight l \<le> bheight r \<Longrightarrow> inorder(joinL l x r) = inorder l @ x # inorder r" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
123 |
proof(induction l x r rule: joinL.induct) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
124 |
case (1 l x r) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
125 |
thus ?case by(auto simp: inorder_baliL joinL.simps[of l x r] split!: tree.splits color.splits) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
126 |
qed |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
127 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
128 |
lemma inorder_joinR: |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
129 |
"inorder(joinR l x r) = inorder l @ x # inorder r" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
130 |
proof(induction l x r rule: joinR.induct) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
131 |
case (1 l x r) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
132 |
thus ?case by (force simp: inorder_baliR joinR.simps[of l x r] split!: tree.splits color.splits) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
133 |
qed |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
134 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
135 |
lemma "inorder(join l x r) = inorder l @ x # inorder r" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
136 |
by(auto simp: inorder_joinL inorder_joinR inorder_paint split!: tree.splits color.splits if_splits |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
137 |
dest!: arg_cong[where f = inorder]) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
138 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
139 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
140 |
subsubsection "Set and bst properties" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
141 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
142 |
lemma set_baliL: |
68261 | 143 |
"set_tree(baliL l a r) = set_tree l \<union> {a} \<union> set_tree r" |
67966
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
144 |
by(cases "(l,a,r)" rule: baliL.cases) (auto) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
145 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
146 |
lemma set_joinL: |
68261 | 147 |
"bheight l \<le> bheight r \<Longrightarrow> set_tree (joinL l x r) = set_tree l \<union> {x} \<union> set_tree r" |
67966
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
148 |
proof(induction l x r rule: joinL.induct) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
149 |
case (1 l x r) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
150 |
thus ?case by(auto simp: set_baliL joinL.simps[of l x r] split!: tree.splits color.splits) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
151 |
qed |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
152 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
153 |
lemma set_baliR: |
68261 | 154 |
"set_tree(baliR l a r) = set_tree l \<union> {a} \<union> set_tree r" |
67966
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
155 |
by(cases "(l,a,r)" rule: baliR.cases) (auto) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
156 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
157 |
lemma set_joinR: |
68261 | 158 |
"set_tree (joinR l x r) = set_tree l \<union> {x} \<union> set_tree r" |
67966
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
159 |
proof(induction l x r rule: joinR.induct) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
160 |
case (1 l x r) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
161 |
thus ?case by(force simp: set_baliR joinR.simps[of l x r] split!: tree.splits color.splits) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
162 |
qed |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
163 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
164 |
lemma set_paint: "set_tree (paint c t) = set_tree t" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
165 |
by (cases t) auto |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
166 |
|
68261 | 167 |
lemma set_join: "set_tree (join l x r) = set_tree l \<union> {x} \<union> set_tree r" |
67966
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
168 |
by(simp add: set_joinL set_joinR set_paint) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
169 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
170 |
lemma bst_baliL: |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
171 |
"\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>x\<in>set_tree r. k < x\<rbrakk> |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
172 |
\<Longrightarrow> bst (baliL l k r)" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
173 |
by(cases "(l,k,r)" rule: baliL.cases) (auto simp: ball_Un) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
174 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
175 |
lemma bst_baliR: |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
176 |
"\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>x\<in>set_tree r. k < x\<rbrakk> |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
177 |
\<Longrightarrow> bst (baliR l k r)" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
178 |
by(cases "(l,k,r)" rule: baliR.cases) (auto simp: ball_Un) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
179 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
180 |
lemma bst_joinL: |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
181 |
"\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>y\<in>set_tree r. k < y; bheight l \<le> bheight r\<rbrakk> |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
182 |
\<Longrightarrow> bst (joinL l k r)" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
183 |
proof(induction l k r rule: joinL.induct) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
184 |
case (1 l x r) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
185 |
thus ?case |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
186 |
by(auto simp: set_baliL joinL.simps[of l x r] set_joinL ball_Un intro!: bst_baliL |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
187 |
split!: tree.splits color.splits) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
188 |
qed |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
189 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
190 |
lemma bst_joinR: |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
191 |
"\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>y\<in>set_tree r. k < y \<rbrakk> |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
192 |
\<Longrightarrow> bst (joinR l k r)" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
193 |
proof(induction l k r rule: joinR.induct) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
194 |
case (1 l x r) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
195 |
thus ?case |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
196 |
by(auto simp: set_baliR joinR.simps[of l x r] set_joinR ball_Un intro!: bst_baliR |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
197 |
split!: tree.splits color.splits) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
198 |
qed |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
199 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
200 |
lemma bst_paint: "bst (paint c t) = bst t" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
201 |
by(cases t) auto |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
202 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
203 |
lemma bst_join: |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
204 |
"\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>y\<in>set_tree r. k < y \<rbrakk> |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
205 |
\<Longrightarrow> bst (join l k r)" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
206 |
by(auto simp: bst_paint bst_joinL bst_joinR) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
207 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
208 |
|
69597 | 209 |
subsubsection "Interpretation of \<^locale>\<open>Set2_Join\<close> with Red-Black Tree" |
67966
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
210 |
|
68261 | 211 |
global_interpretation RBT: Set2_Join |
67966
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
212 |
where join = join and inv = "\<lambda>t. invc t \<and> invh t" |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
213 |
defines insert_rbt = RBT.insert and delete_rbt = RBT.delete and split_rbt = RBT.split |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
214 |
and join2_rbt = RBT.join2 and split_min_rbt = RBT.split_min |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
215 |
proof (standard, goal_cases) |
68261 | 216 |
case 1 show ?case by (rule set_join) |
67966
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
217 |
next |
68261 | 218 |
case 2 thus ?case by (rule bst_join) |
67966
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
219 |
next |
68261 | 220 |
case 3 show ?case by simp |
67966
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
221 |
next |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
222 |
case 4 thus ?case |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
223 |
by (simp add: invc2_joinL invc2_joinR invc_paint_Black invh_joinL invh_joinR invh_paint) |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
224 |
next |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
225 |
case 5 thus ?case by simp |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
226 |
qed |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
227 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
228 |
text \<open>The invariant does not guarantee that the root node is black. This is not required |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
229 |
to guarantee that the height is logarithmic in the size --- Exercise.\<close> |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
230 |
|
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
diff
changeset
|
231 |
end |