no longer necessary
authornipkow
Mon May 21 18:36:30 2018 +0200 (21 months ago)
changeset 68243ddf1ead7b182
parent 68242 4acc029f69e9
child 68245 37974ddde928
child 68255 009f783d1bac
no longer necessary
src/HOL/Data_Structures/Set2_BST2_Join_RBT.thy
     1.1 --- a/src/HOL/Data_Structures/Set2_BST2_Join_RBT.thy	Sun May 20 22:10:30 2018 +0100
     1.2 +++ b/src/HOL/Data_Structures/Set2_BST2_Join_RBT.thy	Mon May 21 18:36:30 2018 +0200
     1.3 @@ -10,12 +10,6 @@
     1.4  
     1.5  subsection "Code"
     1.6  
     1.7 -(*
     1.8 -WARNING baliL and baliR look symmetric but are not if you mirror them:
     1.9 -the first two clauses need to be swapped in one of the two.
    1.10 -Below we defined such a modified baliR. Is already modified in devel.
    1.11 -*)
    1.12 -
    1.13  text \<open>
    1.14  Function \<open>joinL\<close> joins two trees (and an element).
    1.15  Precondition: @{prop "bheight l \<le> bheight r"}.
    1.16 @@ -31,25 +25,6 @@
    1.17       B l' x' r' \<Rightarrow> baliL (joinL l x l') x' r' |
    1.18       R l' x' r' \<Rightarrow> R (joinL l x l') x' r')"
    1.19  
    1.20 -(* rm after isabelle release > 2017 because then in distribution *)
    1.21 -fun baliR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    1.22 -"baliR t1 a1 (R t2 a2 (R t3 a3 t4)) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
    1.23 -"baliR t1 a1 (R (R t2 a2 t3) a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
    1.24 -"baliR t1 a t2 = B t1 a t2"
    1.25 -
    1.26 -lemma inorder_baliR:
    1.27 -  "inorder(baliR l a r) = inorder l @ a # inorder r"
    1.28 -by(cases "(l,a,r)" rule: baliR.cases) (auto)
    1.29 -
    1.30 -lemma invc_baliR:
    1.31 -  "\<lbrakk>invc l; invc2 r\<rbrakk> \<Longrightarrow> invc (baliR l a r)" 
    1.32 -by (induct l a r rule: baliR.induct) auto
    1.33 -
    1.34 -lemma invh_baliR: 
    1.35 -  "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliR l a r)"
    1.36 -by (induct l a r rule: baliR.induct) auto
    1.37 -(* end rm *)
    1.38 -
    1.39  fun joinR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    1.40  "joinR l x r =
    1.41    (if bheight l \<le> bheight r then R l x r