no longer necessary
Mon, 21 May 2018 18:36:30 +0200
changeset 68243 ddf1ead7b182
parent 68242 4acc029f69e9
child 68245 37974ddde928
child 68255 009f783d1bac
no longer necessary
--- 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