src/HOL/Data_Structures/Set2_BST2_Join_RBT.thy
author nipkow
Mon, 21 May 2018 18:36:30 +0200
changeset 68243 ddf1ead7b182
parent 67966 f13796496e82
permissions -rw-r--r--
no longer necessary
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
67966
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
     1
(* Author: Tobias Nipkow *)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
     2
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
     3
section "Join-Based BST2 Implementation of Sets via RBTs"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
     4
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
     5
theory Set2_BST2_Join_RBT
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
     6
imports
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
     7
  Set2_BST2_Join
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
     8
  RBT_Set
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
     9
begin
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    10
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    11
subsection "Code"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    12
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    13
text \<open>
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    14
Function \<open>joinL\<close> joins two trees (and an element).
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    15
Precondition: @{prop "bheight l \<le> bheight r"}.
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    16
Method:
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    17
Descend along the left spine of \<open>r\<close>
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    18
until you find a subtree with the same \<open>bheight\<close> as \<open>l\<close>,
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    19
then combine them into a new red node.
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    20
\<close>
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    21
fun joinL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    22
"joinL l x r =
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    23
  (if bheight l = bheight r then R l x r
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    24
   else case r of
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    25
     B l' x' r' \<Rightarrow> baliL (joinL l x l') x' r' |
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    26
     R l' x' r' \<Rightarrow> R (joinL l x l') x' r')"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    27
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    28
fun joinR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    29
"joinR l x r =
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    30
  (if bheight l \<le> bheight r then R l x r
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    31
   else case l of
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    32
     B l' x' r' \<Rightarrow> baliR l' x' (joinR r' x r) |
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    33
     R l' x' r' \<Rightarrow> R l' x' (joinR r' x r))"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    34
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    35
fun join :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    36
"join l x r =
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    37
  (if bheight l > bheight r
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    38
   then paint Black (joinR l x r)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    39
   else if bheight l < bheight r
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    40
   then paint Black (joinL l x r)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    41
   else B l x r)"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    42
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    43
declare joinL.simps[simp del]
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    44
declare joinR.simps[simp del]
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    45
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    46
text \<open>
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    47
One would expect @{const joinR} to be be completely dual to @{const joinL}.
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    48
Thus the condition should be @{prop"bheight l = bheight r"}. What we have done
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    49
is totalize the function. On the intended domain (@{prop "bheight l \<ge> bheight r"})
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    50
the two versions behave exactly the same, including complexity. Thus from a programmer's
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    51
perspective they are equivalent. However, not from a verifier's perspective:
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    52
the total version of @{const joinR} is easier
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    53
to reason about because lemmas about it may not require preconditions. In particular
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    54
@{prop"set_tree (joinR l x r) = Set.insert x (set_tree l \<union> set_tree r)"}
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    55
is provable outright and hence also
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    56
@{prop"set_tree (join l x r) = Set.insert x (set_tree l \<union> set_tree r)"}.
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    57
This is necessary because locale @{locale Set2_BST2_Join} unconditionally assumes
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    58
exactly that. Adding preconditions to this assumptions significantly complicates
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    59
the proofs within @{locale Set2_BST2_Join}, which we want to avoid.
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    60
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    61
Why not work with the partial version of @{const joinR} and add the precondition
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    62
@{prop "bheight l \<ge> bheight r"} to lemmas about @{const joinR}? After all, that is how
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    63
we worked with @{const joinL}, and @{const join} ensures that @{const joinL} and @{const joinR}
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    64
are only called under the respective precondition. But function @{const bheight}
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    65
makes the difference: it descends along the left spine, just like @{const joinL}.
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    66
Function @{const joinR}, however, descends along the right spine and thus @{const bheight}
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    67
may change all the time. Thus we would need the further precondition @{prop "invh l"}.
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    68
This is what we really wanted to avoid in order to satisfy the unconditional assumption
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    69
in @{locale Set2_BST2_Join}.
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    70
\<close>
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    71
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    72
subsection "Properties"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    73
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    74
subsubsection "Color and height invariants"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    75
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    76
lemma invc2_joinL:
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    77
 "\<lbrakk> invc l; invc r; bheight l \<le> bheight r \<rbrakk> \<Longrightarrow>
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    78
  invc2 (joinL l x r)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    79
  \<and> (bheight l \<noteq> bheight r \<and> color r = Black \<longrightarrow> invc(joinL l x r))"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    80
proof (induct l x r rule: joinL.induct)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    81
  case (1 l x r) thus ?case
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    82
    by(auto simp: invc_baliL invc2I joinL.simps[of l x r] split!: tree.splits if_splits)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    83
qed
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    84
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    85
lemma invc2_joinR:
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    86
  "\<lbrakk> invc l; invh l; invc r; invh r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow>
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    87
  invc2 (joinR l x r)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    88
  \<and> (bheight l \<noteq> bheight r \<and> color l = Black \<longrightarrow> invc(joinR l x r))"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    89
proof (induct l x r rule: joinR.induct)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    90
  case (1 l x r) thus ?case
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    91
    by(fastforce simp: invc_baliR invc2I joinR.simps[of l x r] split!: tree.splits if_splits)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    92
qed
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    93
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    94
lemma bheight_joinL:
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    95
  "\<lbrakk> invh l; invh r; bheight l \<le> bheight r \<rbrakk> \<Longrightarrow> bheight (joinL l x r) = bheight r"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    96
proof (induct l x r rule: joinL.induct)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    97
  case (1 l x r) thus ?case
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    98
    by(auto simp: bheight_baliL joinL.simps[of l x r] split!: tree.split)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
    99
qed
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   100
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   101
lemma invh_joinL:
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   102
  "\<lbrakk> invh l;  invh r;  bheight l \<le> bheight r \<rbrakk> \<Longrightarrow> invh (joinL l x r)"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   103
proof (induct l x r rule: joinL.induct)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   104
  case (1 l x r) thus ?case
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   105
    by(auto simp: invh_baliL bheight_joinL joinL.simps[of l x r] split!: tree.split color.split)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   106
qed
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   107
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   108
lemma bheight_baliR:
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   109
  "bheight l = bheight r \<Longrightarrow> bheight (baliR l a r) = Suc (bheight l)"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   110
by (cases "(l,a,r)" rule: baliR.cases) auto
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   111
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   112
lemma bheight_joinR:
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   113
  "\<lbrakk> invh l;  invh r;  bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow> bheight (joinR l x r) = bheight l"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   114
proof (induct l x r rule: joinR.induct)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   115
  case (1 l x r) thus ?case
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   116
    by(fastforce simp: bheight_baliR joinR.simps[of l x r] split!: tree.split)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   117
qed
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   118
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   119
lemma invh_joinR:
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   120
  "\<lbrakk> invh l; invh r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow> invh (joinR l x r)"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   121
proof (induct l x r rule: joinR.induct)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   122
  case (1 l x r) thus ?case
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   123
    by(fastforce simp: invh_baliR bheight_joinR joinR.simps[of l x r]
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   124
        split!: tree.split color.split)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   125
qed
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   126
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   127
(* unused *)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   128
lemma rbt_join: "\<lbrakk> invc l; invh l; invc r; invh r \<rbrakk> \<Longrightarrow> rbt(join l x r)"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   129
by(simp add: invc2_joinL invc2_joinR invc_paint_Black invh_joinL invh_joinR invh_paint rbt_def
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   130
    color_paint_Black)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   131
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   132
text \<open>To make sure the the black height is not increased unnecessarily:\<close>
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   133
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   134
lemma bheight_paint_Black: "bheight(paint Black t) \<le> bheight t + 1"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   135
by(cases t) auto
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   136
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   137
lemma "\<lbrakk> rbt l; rbt r \<rbrakk> \<Longrightarrow> bheight(join l x r) \<le> max (bheight l) (bheight r) + 1"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   138
using bheight_paint_Black[of "joinL l x r"] bheight_paint_Black[of "joinR l x r"]
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   139
  bheight_joinL[of l r x] bheight_joinR[of l r x]
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   140
by(auto simp: max_def rbt_def)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   141
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   142
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   143
subsubsection "Inorder properties"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   144
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   145
text "Currently unused. Instead @{const set_tree} and @{const bst} properties are proved directly."
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   146
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   147
lemma inorder_joinL: "bheight l \<le> bheight r \<Longrightarrow> inorder(joinL l x r) = inorder l @ x # inorder r"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   148
proof(induction l x r rule: joinL.induct)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   149
  case (1 l x r)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   150
  thus ?case by(auto simp: inorder_baliL joinL.simps[of l x r] split!: tree.splits color.splits)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   151
qed
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   152
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   153
lemma inorder_joinR:
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   154
  "inorder(joinR l x r) = inorder l @ x # inorder r"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   155
proof(induction l x r rule: joinR.induct)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   156
  case (1 l x r)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   157
  thus ?case by (force simp: inorder_baliR joinR.simps[of l x r] split!: tree.splits color.splits)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   158
qed
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   159
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   160
lemma "inorder(join l x r) = inorder l @ x # inorder r"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   161
by(auto simp: inorder_joinL inorder_joinR inorder_paint split!: tree.splits color.splits if_splits
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   162
      dest!: arg_cong[where f = inorder])
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   163
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   164
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   165
subsubsection "Set and bst properties"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   166
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   167
lemma set_baliL:
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   168
  "set_tree(baliL l a r) = Set.insert a (set_tree l \<union> set_tree r)"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   169
by(cases "(l,a,r)" rule: baliL.cases) (auto)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   170
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   171
lemma set_joinL:
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   172
  "bheight l \<le> bheight r \<Longrightarrow> set_tree (joinL l x r) = Set.insert x (set_tree l \<union> set_tree r)"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   173
proof(induction l x r rule: joinL.induct)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   174
  case (1 l x r)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   175
  thus ?case by(auto simp: set_baliL joinL.simps[of l x r] split!: tree.splits color.splits)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   176
qed
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   177
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   178
lemma set_baliR:
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   179
  "set_tree(baliR l a r) = Set.insert a (set_tree l \<union> set_tree r)"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   180
by(cases "(l,a,r)" rule: baliR.cases) (auto)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   181
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   182
lemma set_joinR:
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   183
  "set_tree (joinR l x r) = Set.insert x (set_tree l \<union> set_tree r)"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   184
proof(induction l x r rule: joinR.induct)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   185
  case (1 l x r)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   186
  thus ?case by(force simp: set_baliR joinR.simps[of l x r] split!: tree.splits color.splits)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   187
qed
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   188
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   189
lemma set_paint: "set_tree (paint c t) = set_tree t"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   190
by (cases t) auto
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   191
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   192
lemma set_join: "set_tree (join l x r) = Set.insert x (set_tree l \<union> set_tree r)"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   193
by(simp add: set_joinL set_joinR set_paint)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   194
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   195
lemma bst_baliL:
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   196
  "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>x\<in>set_tree r. k < x\<rbrakk>
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   197
   \<Longrightarrow> bst (baliL l k r)"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   198
by(cases "(l,k,r)" rule: baliL.cases) (auto simp: ball_Un)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   199
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   200
lemma bst_baliR:
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   201
  "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>x\<in>set_tree r. k < x\<rbrakk>
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   202
   \<Longrightarrow> bst (baliR l k r)"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   203
by(cases "(l,k,r)" rule: baliR.cases) (auto simp: ball_Un)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   204
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   205
lemma bst_joinL:
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   206
  "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>y\<in>set_tree r. k < y; bheight l \<le> bheight r\<rbrakk>
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   207
  \<Longrightarrow> bst (joinL l k r)"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   208
proof(induction l k r rule: joinL.induct)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   209
  case (1 l x r)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   210
  thus ?case
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   211
    by(auto simp: set_baliL joinL.simps[of l x r] set_joinL ball_Un intro!: bst_baliL
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   212
        split!: tree.splits color.splits)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   213
qed
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   214
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   215
lemma bst_joinR:
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   216
  "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>y\<in>set_tree r. k < y \<rbrakk>
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   217
  \<Longrightarrow> bst (joinR l k r)"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   218
proof(induction l k r rule: joinR.induct)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   219
  case (1 l x r)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   220
  thus ?case
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   221
    by(auto simp: set_baliR joinR.simps[of l x r] set_joinR ball_Un intro!: bst_baliR
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   222
        split!: tree.splits color.splits)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   223
qed
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   224
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   225
lemma bst_paint: "bst (paint c t) = bst t"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   226
by(cases t) auto
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   227
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   228
lemma bst_join:
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   229
  "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>y\<in>set_tree r. k < y \<rbrakk>
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   230
  \<Longrightarrow> bst (join l k r)"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   231
by(auto simp: bst_paint bst_joinL bst_joinR)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   232
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   233
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   234
subsubsection "Interpretation of @{locale Set2_BST2_Join} with Red-Black Tree"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   235
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   236
global_interpretation RBT: Set2_BST2_Join
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   237
where join = join and inv = "\<lambda>t. invc t \<and> invh t"
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   238
defines insert_rbt = RBT.insert and delete_rbt = RBT.delete and split_rbt = RBT.split
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   239
and join2_rbt = RBT.join2 and split_min_rbt = RBT.split_min
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   240
proof (standard, goal_cases)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   241
  case 1 show ?case by simp
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   242
next
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   243
  case 2 show ?case by (rule set_join)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   244
next
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   245
  case 3 thus ?case by (rule bst_join)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   246
next
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   247
  case 4 thus ?case
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   248
    by (simp add: invc2_joinL invc2_joinR invc_paint_Black invh_joinL invh_joinR invh_paint)
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   249
next
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   250
  case 5 thus ?case by simp
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   251
qed
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   252
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   253
text \<open>The invariant does not guarantee that the root node is black. This is not required
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   254
to guarantee that the height is logarithmic in the size --- Exercise.\<close>
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   255
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents:
diff changeset
   256
end