src/HOL/Data_Structures/Set2_BST2_Join_RBT.thy
 changeset 68243 ddf1ead7b182 parent 67966 f13796496e82
equal inserted replaced
`     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"`
`    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 `
`    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) |`