--- a/src/HOL/Data_Structures/RBT_Set.thy Sun Nov 15 11:27:55 2015 +0100
+++ b/src/HOL/Data_Structures/RBT_Set.thy Sun Nov 15 12:45:28 2015 +0100
@@ -11,24 +11,27 @@
fun insert :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
"insert x Leaf = R Leaf x Leaf" |
-"insert x (B l a r) = (case cmp x a of
- LT \<Rightarrow> bal (insert x l) a r |
- GT \<Rightarrow> bal l a (insert x r) |
- EQ \<Rightarrow> B l a r)" |
-"insert x (R l a r) = (case cmp x a of
- LT \<Rightarrow> R (insert x l) a r |
- GT \<Rightarrow> R l a (insert x r) |
- EQ \<Rightarrow> R l a r)"
+"insert x (B l a r) =
+ (case cmp x a of
+ LT \<Rightarrow> bal (insert x l) a r |
+ GT \<Rightarrow> bal l a (insert x r) |
+ EQ \<Rightarrow> B l a r)" |
+"insert x (R l a r) =
+ (case cmp x a of
+ LT \<Rightarrow> R (insert x l) a r |
+ GT \<Rightarrow> R l a (insert x r) |
+ EQ \<Rightarrow> R l a r)"
fun delete :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
and deleteL :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
and deleteR :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
where
"delete x Leaf = Leaf" |
-"delete x (Node _ l a r) = (case cmp x a of
- LT \<Rightarrow> deleteL x l a r |
- GT \<Rightarrow> deleteR x l a r |
- EQ \<Rightarrow> combine l r)" |
+"delete x (Node _ l a r) =
+ (case cmp x a of
+ LT \<Rightarrow> deleteL x l a r |
+ GT \<Rightarrow> deleteR x l a r |
+ EQ \<Rightarrow> combine l r)" |
"deleteL x (B t1 a t2) b t3 = balL (delete x (B t1 a t2)) b t3" |
"deleteL x l a r = R (delete x l) a r" |
"deleteR x t1 a (B t2 b t3) = balR t1 a (delete x (B t2 b t3))" |
@@ -62,9 +65,9 @@
(auto simp: inorder_balL inorder_balR split: tree.split color.split)
lemma inorder_delete:
- "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)" and
+ "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
"sorted(inorder l) \<Longrightarrow> inorder(deleteL x l a r) =
- del_list x (inorder l) @ a # inorder r" and
+ del_list x (inorder l) @ a # inorder r"
"sorted(inorder r) \<Longrightarrow> inorder(deleteR x l a r) =
inorder l @ a # del_list x (inorder r)"
by(induction x t and x l a r and x l a r rule: delete_deleteL_deleteR.induct)
@@ -81,7 +84,7 @@
next
case 3 thus ?case by(simp add: inorder_insert)
next
- case 4 thus ?case by(simp add: inorder_delete)
+ case 4 thus ?case by(simp add: inorder_delete(1))
qed (rule TrueI)+
end