src/HOL/Data_Structures/Set2_BST2_Join_RBT.thy
changeset 68243 ddf1ead7b182
parent 67966 f13796496e82
equal deleted inserted replaced
68242:4acc029f69e9 68243:ddf1ead7b182
     7   Set2_BST2_Join
     7   Set2_BST2_Join
     8   RBT_Set
     8   RBT_Set
     9 begin
     9 begin
    10 
    10 
    11 subsection "Code"
    11 subsection "Code"
    12 
       
    13 (*
       
    14 WARNING baliL and baliR look symmetric but are not if you mirror them:
       
    15 the first two clauses need to be swapped in one of the two.
       
    16 Below we defined such a modified baliR. Is already modified in devel.
       
    17 *)
       
    18 
    12 
    19 text \<open>
    13 text \<open>
    20 Function \<open>joinL\<close> joins two trees (and an element).
    14 Function \<open>joinL\<close> joins two trees (and an element).
    21 Precondition: @{prop "bheight l \<le> bheight r"}.
    15 Precondition: @{prop "bheight l \<le> bheight r"}.
    22 Method:
    16 Method:
    29   (if bheight l = bheight r then R l x r
    23   (if bheight l = bheight r then R l x r
    30    else case r of
    24    else case r of
    31      B l' x' r' \<Rightarrow> baliL (joinL l x l') x' r' |
    25      B l' x' r' \<Rightarrow> baliL (joinL l x l') x' r' |
    32      R l' x' r' \<Rightarrow> R (joinL l x l') x' r')"
    26      R l' x' r' \<Rightarrow> R (joinL l x l') x' r')"
    33 
    27 
    34 (* rm after isabelle release > 2017 because then in distribution *)
       
    35 fun baliR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
       
    36 "baliR t1 a1 (R t2 a2 (R t3 a3 t4)) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
       
    37 "baliR t1 a1 (R (R t2 a2 t3) a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
       
    38 "baliR t1 a t2 = B t1 a t2"
       
    39 
       
    40 lemma inorder_baliR:
       
    41   "inorder(baliR l a r) = inorder l @ a # inorder r"
       
    42 by(cases "(l,a,r)" rule: baliR.cases) (auto)
       
    43 
       
    44 lemma invc_baliR:
       
    45   "\<lbrakk>invc l; invc2 r\<rbrakk> \<Longrightarrow> invc (baliR l a r)" 
       
    46 by (induct l a r rule: baliR.induct) auto
       
    47 
       
    48 lemma invh_baliR: 
       
    49   "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliR l a r)"
       
    50 by (induct l a r rule: baliR.induct) auto
       
    51 (* end rm *)
       
    52 
       
    53 fun joinR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    28 fun joinR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    54 "joinR l x r =
    29 "joinR l x r =
    55   (if bheight l \<le> bheight r then R l x r
    30   (if bheight l \<le> bheight r then R l x r
    56    else case l of
    31    else case l of
    57      B l' x' r' \<Rightarrow> baliR l' x' (joinR r' x r) |
    32      B l' x' r' \<Rightarrow> baliR l' x' (joinR r' x r) |