--- a/src/HOL/Data_Structures/Set2_BST2_Join_RBT.thy Sun May 20 22:10:30 2018 +0100
+++ b/src/HOL/Data_Structures/Set2_BST2_Join_RBT.thy Mon May 21 18:36:30 2018 +0200
@@ -10,12 +10,6 @@
subsection "Code"
-(*
-WARNING baliL and baliR look symmetric but are not if you mirror them:
-the first two clauses need to be swapped in one of the two.
-Below we defined such a modified baliR. Is already modified in devel.
-*)
-
text \<open>
Function \<open>joinL\<close> joins two trees (and an element).
Precondition: @{prop "bheight l \<le> bheight r"}.
@@ -31,25 +25,6 @@
B l' x' r' \<Rightarrow> baliL (joinL l x l') x' r' |
R l' x' r' \<Rightarrow> R (joinL l x l') x' r')"
-(* rm after isabelle release > 2017 because then in distribution *)
-fun baliR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
-"baliR t1 a1 (R t2 a2 (R t3 a3 t4)) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
-"baliR t1 a1 (R (R t2 a2 t3) a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
-"baliR t1 a t2 = B t1 a t2"
-
-lemma inorder_baliR:
- "inorder(baliR l a r) = inorder l @ a # inorder r"
-by(cases "(l,a,r)" rule: baliR.cases) (auto)
-
-lemma invc_baliR:
- "\<lbrakk>invc l; invc2 r\<rbrakk> \<Longrightarrow> invc (baliR l a r)"
-by (induct l a r rule: baliR.induct) auto
-
-lemma invh_baliR:
- "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliR l a r)"
-by (induct l a r rule: baliR.induct) auto
-(* end rm *)
-
fun joinR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
"joinR l x r =
(if bheight l \<le> bheight r then R l x r