author  nipkow 
Mon, 21 May 2018 18:36:30 +0200  
changeset 68243  ddf1ead7b182 
parent 67966  f13796496e82 
permissions  rwrr 
67966
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

1 
(* Author: Tobias Nipkow *) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

2 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

3 
section "JoinBased BST2 Implementation of Sets via RBTs" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

4 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

5 
theory Set2_BST2_Join_RBT 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

6 
imports 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

7 
Set2_BST2_Join 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

8 
RBT_Set 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

9 
begin 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

10 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

11 
subsection "Code" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

12 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

13 
text \<open> 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

14 
Function \<open>joinL\<close> joins two trees (and an element). 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

15 
Precondition: @{prop "bheight l \<le> bheight r"}. 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

16 
Method: 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

17 
Descend along the left spine of \<open>r\<close> 
f13796496e82
Added binary set operations with joinbased 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 joinbased implementation
nipkow
parents:
diff
changeset

19 
then combine them into a new red node. 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

20 
\<close> 
f13796496e82
Added binary set operations with joinbased 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 joinbased implementation
nipkow
parents:
diff
changeset

22 
"joinL l x r = 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

23 
(if bheight l = bheight r then R l x r 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

24 
else case r of 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

25 
B l' x' r' \<Rightarrow> baliL (joinL l x l') x' r'  
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

26 
R l' x' r' \<Rightarrow> R (joinL l x l') x' r')" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

27 

f13796496e82
Added binary set operations with joinbased 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 joinbased implementation
nipkow
parents:
diff
changeset

29 
"joinR l x r = 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

30 
(if bheight l \<le> bheight r then R l x r 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

31 
else case l of 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

32 
B l' x' r' \<Rightarrow> baliR l' x' (joinR r' x r)  
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

33 
R l' x' r' \<Rightarrow> R l' x' (joinR r' x r))" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

34 

f13796496e82
Added binary set operations with joinbased 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 joinbased implementation
nipkow
parents:
diff
changeset

36 
"join l x r = 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

37 
(if bheight l > bheight r 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

38 
then paint Black (joinR l x r) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

39 
else if bheight l < bheight r 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

40 
then paint Black (joinL l x r) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

41 
else B l x r)" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

42 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

43 
declare joinL.simps[simp del] 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

44 
declare joinR.simps[simp del] 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

45 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

46 
text \<open> 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

47 
One would expect @{const joinR} to be be completely dual to @{const joinL}. 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

48 
Thus the condition should be @{prop"bheight l = bheight r"}. What we have done 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

49 
is totalize the function. On the intended domain (@{prop "bheight l \<ge> bheight r"}) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

50 
the two versions behave exactly the same, including complexity. Thus from a programmer's 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

51 
perspective they are equivalent. However, not from a verifier's perspective: 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

52 
the total version of @{const joinR} is easier 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

53 
to reason about because lemmas about it may not require preconditions. In particular 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

54 
@{prop"set_tree (joinR l x r) = Set.insert x (set_tree l \<union> set_tree r)"} 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

55 
is provable outright and hence also 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

56 
@{prop"set_tree (join l x r) = Set.insert x (set_tree l \<union> set_tree r)"}. 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

57 
This is necessary because locale @{locale Set2_BST2_Join} unconditionally assumes 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

58 
exactly that. Adding preconditions to this assumptions significantly complicates 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

59 
the proofs within @{locale Set2_BST2_Join}, which we want to avoid. 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

60 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

61 
Why not work with the partial version of @{const joinR} and add the precondition 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

62 
@{prop "bheight l \<ge> bheight r"} to lemmas about @{const joinR}? After all, that is how 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

63 
we worked with @{const joinL}, and @{const join} ensures that @{const joinL} and @{const joinR} 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

64 
are only called under the respective precondition. But function @{const bheight} 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

65 
makes the difference: it descends along the left spine, just like @{const joinL}. 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

66 
Function @{const joinR}, however, descends along the right spine and thus @{const bheight} 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

67 
may change all the time. Thus we would need the further precondition @{prop "invh l"}. 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

68 
This is what we really wanted to avoid in order to satisfy the unconditional assumption 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

69 
in @{locale Set2_BST2_Join}. 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

70 
\<close> 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

71 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

72 
subsection "Properties" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

73 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

74 
subsubsection "Color and height invariants" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

75 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

76 
lemma invc2_joinL: 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

77 
"\<lbrakk> invc l; invc r; bheight l \<le> bheight r \<rbrakk> \<Longrightarrow> 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

78 
invc2 (joinL l x r) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

79 
\<and> (bheight l \<noteq> bheight r \<and> color r = Black \<longrightarrow> invc(joinL l x r))" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

80 
proof (induct l x r rule: joinL.induct) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

81 
case (1 l x r) thus ?case 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

82 
by(auto simp: invc_baliL invc2I joinL.simps[of l x r] split!: tree.splits if_splits) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

83 
qed 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

84 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

85 
lemma invc2_joinR: 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

86 
"\<lbrakk> invc l; invh l; invc r; invh r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow> 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

87 
invc2 (joinR l x r) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

88 
\<and> (bheight l \<noteq> bheight r \<and> color l = Black \<longrightarrow> invc(joinR l x r))" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

89 
proof (induct l x r rule: joinR.induct) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

90 
case (1 l x r) thus ?case 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

91 
by(fastforce simp: invc_baliR invc2I joinR.simps[of l x r] split!: tree.splits if_splits) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

92 
qed 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

93 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

94 
lemma bheight_joinL: 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

95 
"\<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 joinbased implementation
nipkow
parents:
diff
changeset

96 
proof (induct l x r rule: joinL.induct) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

97 
case (1 l x r) thus ?case 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

98 
by(auto simp: bheight_baliL joinL.simps[of l x r] split!: tree.split) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

99 
qed 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

100 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

101 
lemma invh_joinL: 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

102 
"\<lbrakk> invh l; invh r; bheight l \<le> bheight r \<rbrakk> \<Longrightarrow> invh (joinL l x r)" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

103 
proof (induct l x r rule: joinL.induct) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

104 
case (1 l x r) thus ?case 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

105 
by(auto simp: invh_baliL bheight_joinL joinL.simps[of l x r] split!: tree.split color.split) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

106 
qed 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

107 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

108 
lemma bheight_baliR: 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

109 
"bheight l = bheight r \<Longrightarrow> bheight (baliR l a r) = Suc (bheight l)" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

110 
by (cases "(l,a,r)" rule: baliR.cases) auto 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

111 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

112 
lemma bheight_joinR: 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

113 
"\<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 joinbased implementation
nipkow
parents:
diff
changeset

114 
proof (induct l x r rule: joinR.induct) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

115 
case (1 l x r) thus ?case 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

116 
by(fastforce simp: bheight_baliR joinR.simps[of l x r] split!: tree.split) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

117 
qed 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

118 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

119 
lemma invh_joinR: 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

120 
"\<lbrakk> invh l; invh r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow> invh (joinR l x r)" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

121 
proof (induct l x r rule: joinR.induct) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

122 
case (1 l x r) thus ?case 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

123 
by(fastforce simp: invh_baliR bheight_joinR joinR.simps[of l x r] 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

124 
split!: tree.split color.split) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

125 
qed 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

126 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

127 
(* unused *) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

128 
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 joinbased implementation
nipkow
parents:
diff
changeset

129 
by(simp add: invc2_joinL invc2_joinR invc_paint_Black invh_joinL invh_joinR invh_paint rbt_def 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

130 
color_paint_Black) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

131 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

132 
text \<open>To make sure the the black height is not increased unnecessarily:\<close> 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

133 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

134 
lemma bheight_paint_Black: "bheight(paint Black t) \<le> bheight t + 1" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

135 
by(cases t) auto 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

136 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

137 
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 joinbased implementation
nipkow
parents:
diff
changeset

138 
using bheight_paint_Black[of "joinL l x r"] bheight_paint_Black[of "joinR l x r"] 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

139 
bheight_joinL[of l r x] bheight_joinR[of l r x] 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

140 
by(auto simp: max_def rbt_def) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

141 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

142 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

143 
subsubsection "Inorder properties" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

144 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

145 
text "Currently unused. Instead @{const set_tree} and @{const bst} properties are proved directly." 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

146 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

147 
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 joinbased implementation
nipkow
parents:
diff
changeset

148 
proof(induction l x r rule: joinL.induct) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

149 
case (1 l x r) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

150 
thus ?case by(auto simp: inorder_baliL joinL.simps[of l x r] split!: tree.splits color.splits) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

151 
qed 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

152 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

153 
lemma inorder_joinR: 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

154 
"inorder(joinR l x r) = inorder l @ x # inorder r" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

155 
proof(induction l x r rule: joinR.induct) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

156 
case (1 l x r) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

157 
thus ?case by (force simp: inorder_baliR joinR.simps[of l x r] split!: tree.splits color.splits) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

158 
qed 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

159 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

160 
lemma "inorder(join l x r) = inorder l @ x # inorder r" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

161 
by(auto simp: inorder_joinL inorder_joinR inorder_paint split!: tree.splits color.splits if_splits 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

162 
dest!: arg_cong[where f = inorder]) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

163 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

164 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

165 
subsubsection "Set and bst properties" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

166 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

167 
lemma set_baliL: 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

168 
"set_tree(baliL l a r) = Set.insert a (set_tree l \<union> set_tree r)" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

169 
by(cases "(l,a,r)" rule: baliL.cases) (auto) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

170 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

171 
lemma set_joinL: 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

172 
"bheight l \<le> bheight r \<Longrightarrow> set_tree (joinL l x r) = Set.insert x (set_tree l \<union> set_tree r)" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

173 
proof(induction l x r rule: joinL.induct) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

174 
case (1 l x r) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

175 
thus ?case by(auto simp: set_baliL joinL.simps[of l x r] split!: tree.splits color.splits) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

176 
qed 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

177 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

178 
lemma set_baliR: 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

179 
"set_tree(baliR l a r) = Set.insert a (set_tree l \<union> set_tree r)" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

180 
by(cases "(l,a,r)" rule: baliR.cases) (auto) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

181 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

182 
lemma set_joinR: 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

183 
"set_tree (joinR l x r) = Set.insert x (set_tree l \<union> set_tree r)" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

184 
proof(induction l x r rule: joinR.induct) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

185 
case (1 l x r) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

186 
thus ?case by(force simp: set_baliR joinR.simps[of l x r] split!: tree.splits color.splits) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

187 
qed 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

188 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

189 
lemma set_paint: "set_tree (paint c t) = set_tree t" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

190 
by (cases t) auto 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

191 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

192 
lemma set_join: "set_tree (join l x r) = Set.insert x (set_tree l \<union> set_tree r)" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

193 
by(simp add: set_joinL set_joinR set_paint) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

194 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

195 
lemma bst_baliL: 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

196 
"\<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 joinbased implementation
nipkow
parents:
diff
changeset

197 
\<Longrightarrow> bst (baliL l k r)" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

198 
by(cases "(l,k,r)" rule: baliL.cases) (auto simp: ball_Un) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

199 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

200 
lemma bst_baliR: 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

201 
"\<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 joinbased implementation
nipkow
parents:
diff
changeset

202 
\<Longrightarrow> bst (baliR l k r)" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

203 
by(cases "(l,k,r)" rule: baliR.cases) (auto simp: ball_Un) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

204 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

205 
lemma bst_joinL: 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

206 
"\<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 joinbased implementation
nipkow
parents:
diff
changeset

207 
\<Longrightarrow> bst (joinL l k r)" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

208 
proof(induction l k r rule: joinL.induct) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

209 
case (1 l x r) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

210 
thus ?case 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

211 
by(auto simp: set_baliL joinL.simps[of l x r] set_joinL ball_Un intro!: bst_baliL 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

212 
split!: tree.splits color.splits) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

213 
qed 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

214 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

215 
lemma bst_joinR: 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

216 
"\<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 joinbased implementation
nipkow
parents:
diff
changeset

217 
\<Longrightarrow> bst (joinR l k r)" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

218 
proof(induction l k r rule: joinR.induct) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

219 
case (1 l x r) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

220 
thus ?case 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

221 
by(auto simp: set_baliR joinR.simps[of l x r] set_joinR ball_Un intro!: bst_baliR 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

222 
split!: tree.splits color.splits) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

223 
qed 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

224 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

225 
lemma bst_paint: "bst (paint c t) = bst t" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

226 
by(cases t) auto 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

227 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

228 
lemma bst_join: 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

229 
"\<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 joinbased implementation
nipkow
parents:
diff
changeset

230 
\<Longrightarrow> bst (join l k r)" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

231 
by(auto simp: bst_paint bst_joinL bst_joinR) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

232 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

233 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

234 
subsubsection "Interpretation of @{locale Set2_BST2_Join} with RedBlack Tree" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

235 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

236 
global_interpretation RBT: Set2_BST2_Join 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

237 
where join = join and inv = "\<lambda>t. invc t \<and> invh t" 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

238 
defines insert_rbt = RBT.insert and delete_rbt = RBT.delete and split_rbt = RBT.split 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

239 
and join2_rbt = RBT.join2 and split_min_rbt = RBT.split_min 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

240 
proof (standard, goal_cases) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

241 
case 1 show ?case by simp 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

242 
next 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

243 
case 2 show ?case by (rule set_join) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

244 
next 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

245 
case 3 thus ?case by (rule bst_join) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

246 
next 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

247 
case 4 thus ?case 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

248 
by (simp add: invc2_joinL invc2_joinR invc_paint_Black invh_joinL invh_joinR invh_paint) 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

249 
next 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

250 
case 5 thus ?case by simp 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

251 
qed 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

252 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

253 
text \<open>The invariant does not guarantee that the root node is black. This is not required 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

254 
to guarantee that the height is logarithmic in the size  Exercise.\<close> 
f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

255 

f13796496e82
Added binary set operations with joinbased implementation
nipkow
parents:
diff
changeset

256 
end 