--- a/src/HOL/Data_Structures/RBT.thy Thu Feb 20 09:05:19 2020 +0100
+++ b/src/HOL/Data_Structures/RBT.thy Fri Feb 21 17:51:56 2020 +0100
@@ -39,18 +39,18 @@
"baldR (R t1 a (B t2 b t3)) c t4 = R (baliL (paint Red t1) a t2) b (B t3 c t4)" |
"baldR t1 a t2 = R t1 a t2"
-fun combine :: "'a rbt \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
-"combine Leaf t = t" |
-"combine t Leaf = t" |
-"combine (R t1 a t2) (R t3 c t4) =
- (case combine t2 t3 of
+fun app :: "'a rbt \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
+"app Leaf t = t" |
+"app t Leaf = t" |
+"app (R t1 a t2) (R t3 c t4) =
+ (case app t2 t3 of
R u2 b u3 \<Rightarrow> (R (R t1 a u2) b (R u3 c t4)) |
t23 \<Rightarrow> R t1 a (R t23 c t4))" |
-"combine (B t1 a t2) (B t3 c t4) =
- (case combine t2 t3 of
+"app (B t1 a t2) (B t3 c t4) =
+ (case app t2 t3 of
R u2 b u3 \<Rightarrow> R (B t1 a u2) b (B u3 c t4) |
t23 \<Rightarrow> baldL t1 a (B t23 c t4))" |
-"combine t1 (R t2 a t3) = R (combine t1 t2) a t3" |
-"combine (R t1 a t2) t3 = R t1 a (combine t2 t3)"
+"app t1 (R t2 a t3) = R (app t1 t2) a t3" |
+"app (R t1 a t2) t3 = R t1 a (app t2 t3)"
end