--- a/src/HOL/Data_Structures/RBT_Map.thy Wed Nov 04 15:07:23 2015 +0100
+++ b/src/HOL/Data_Structures/RBT_Map.thy Thu Nov 05 08:27:14 2015 +0100
@@ -8,25 +8,26 @@
Lookup2
begin
-fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
+fun update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
"update x y Leaf = R Leaf (x,y) Leaf" |
-"update x y (B l (a,b) r) =
- (if x < a then bal (update x y l) (a,b) r else
- if x > a then bal l (a,b) (update x y r)
- else B l (x,y) r)" |
-"update x y (R l (a,b) r) =
- (if x < a then R (update x y l) (a,b) r else
- if x > a then R l (a,b) (update x y r)
- else R l (x,y) r)"
+"update x y (B l (a,b) r) = (case cmp x a of
+ LT \<Rightarrow> bal (update x y l) (a,b) r |
+ GT \<Rightarrow> bal l (a,b) (update x y r) |
+ EQ \<Rightarrow> B l (x,y) r)" |
+"update x y (R l (a,b) r) = (case cmp x a of
+ LT \<Rightarrow> R (update x y l) (a,b) r |
+ GT \<Rightarrow> R l (a,b) (update x y r) |
+ EQ \<Rightarrow> R l (x,y) r)"
-fun delete :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
-and deleteL :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
-and deleteR :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
+fun delete :: "'a::cmp \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
+and deleteL :: "'a::cmp \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
+and deleteR :: "'a::cmp \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
where
"delete x Leaf = Leaf" |
-"delete x (Node c t1 (a,b) t2) =
- (if x < a then deleteL x t1 (a,b) t2 else
- if x > a then deleteR x t1 (a,b) t2 else combine t1 t2)" |
+"delete x (Node c t1 (a,b) t2) = (case cmp x a of
+ LT \<Rightarrow> deleteL x t1 (a,b) t2 |
+ GT \<Rightarrow> deleteR x t1 (a,b) t2 |
+ EQ \<Rightarrow> combine t1 t2)" |
"deleteL x (B t1 a t2) b t3 = balL (delete x (B t1 a t2)) b t3" |
"deleteL x t1 a t2 = R (delete x t1) a t2" |
"deleteR x t1 a (B t2 b t3) = balR t1 a (delete x (B t2 b t3))" |
@@ -50,7 +51,6 @@
by(induction x t1 and x t1 a t2 and x t1 a t2 rule: delete_deleteL_deleteR.induct)
(auto simp: del_list_simps inorder_combine inorder_balL inorder_balR)
-
interpretation Map_by_Ordered
where empty = Leaf and lookup = lookup and update = update and delete = delete
and inorder = inorder and wf = "\<lambda>_. True"