equal
deleted
inserted
replaced
25 fun del :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt" |
25 fun del :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt" |
26 and delL :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt" |
26 and delL :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt" |
27 and delR :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt" |
27 and delR :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt" |
28 where |
28 where |
29 "del x Leaf = Leaf" | |
29 "del x Leaf = Leaf" | |
30 "del x (Node c t1 (a,b) t2) = (case cmp x a of |
30 "del x (Node t1 (a,b) c t2) = (case cmp x a of |
31 LT \<Rightarrow> delL x t1 (a,b) t2 | |
31 LT \<Rightarrow> delL x t1 (a,b) t2 | |
32 GT \<Rightarrow> delR x t1 (a,b) t2 | |
32 GT \<Rightarrow> delR x t1 (a,b) t2 | |
33 EQ \<Rightarrow> combine t1 t2)" | |
33 EQ \<Rightarrow> combine t1 t2)" | |
34 "delL x (B t1 a t2) b t3 = baldL (del x (B t1 a t2)) b t3" | |
34 "delL x (B t1 a t2) b t3 = baldL (del x (B t1 a t2)) b t3" | |
35 "delL x t1 a t2 = R (del x t1) a t2" | |
35 "delL x t1 a t2 = R (del x t1) a t2" | |