src/HOL/Data_Structures/RBT_Set.thy
author nipkow
Fri, 27 Dec 2019 10:54:15 +0100
changeset 71555 7a0a6c56015e
parent 70944 3fb16bed5d6c
child 71557 857453c0db3d
permissions -rw-r--r--
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64951
140addd19343 removed contribution by Daniel Stuewe, too detailed.
nipkow
parents: 64950
diff changeset
     1
(* Author: Tobias Nipkow *)
61224
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
     2
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
     3
section \<open>Red-Black Tree Implementation of Sets\<close>
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
     4
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
     5
theory RBT_Set
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
     6
imports
64950
10b8d31634cc added concise log height bound lemma
nipkow
parents: 64947
diff changeset
     7
  Complex_Main
61224
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
     8
  RBT
61581
00d9682e8dd7 Convertd to 3-way comparisons
nipkow
parents: 61428
diff changeset
     9
  Cmp
61224
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
    10
  Isin2
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
    11
begin
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
    12
68431
b294e095f64c more abstract naming
nipkow
parents: 68414
diff changeset
    13
definition empty :: "'a rbt" where
b294e095f64c more abstract naming
nipkow
parents: 68414
diff changeset
    14
"empty = Leaf"
b294e095f64c more abstract naming
nipkow
parents: 68414
diff changeset
    15
63411
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
    16
fun ins :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
61749
7f530d7e552d paint root black after insert and delete
nipkow
parents: 61678
diff changeset
    17
"ins x Leaf = R Leaf x Leaf" |
7f530d7e552d paint root black after insert and delete
nipkow
parents: 61678
diff changeset
    18
"ins x (B l a r) =
61678
b594e9277be3 tuned white space
nipkow
parents: 61588
diff changeset
    19
  (case cmp x a of
64960
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
    20
     LT \<Rightarrow> baliL (ins x l) a r |
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
    21
     GT \<Rightarrow> baliR l a (ins x r) |
61678
b594e9277be3 tuned white space
nipkow
parents: 61588
diff changeset
    22
     EQ \<Rightarrow> B l a r)" |
61749
7f530d7e552d paint root black after insert and delete
nipkow
parents: 61678
diff changeset
    23
"ins x (R l a r) =
61678
b594e9277be3 tuned white space
nipkow
parents: 61588
diff changeset
    24
  (case cmp x a of
61749
7f530d7e552d paint root black after insert and delete
nipkow
parents: 61678
diff changeset
    25
    LT \<Rightarrow> R (ins x l) a r |
7f530d7e552d paint root black after insert and delete
nipkow
parents: 61678
diff changeset
    26
    GT \<Rightarrow> R l a (ins x r) |
61678
b594e9277be3 tuned white space
nipkow
parents: 61588
diff changeset
    27
    EQ \<Rightarrow> R l a r)"
61224
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
    28
63411
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
    29
definition insert :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
61749
7f530d7e552d paint root black after insert and delete
nipkow
parents: 61678
diff changeset
    30
"insert x t = paint Black (ins x t)"
7f530d7e552d paint root black after insert and delete
nipkow
parents: 61678
diff changeset
    31
66087
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
    32
fun color :: "'a rbt \<Rightarrow> color" where
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
    33
"color Leaf = Black" |
70944
3fb16bed5d6c replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents: 70897
diff changeset
    34
"color (Node _ (_, c) _) = c"
66087
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
    35
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
    36
fun del :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
61749
7f530d7e552d paint root black after insert and delete
nipkow
parents: 61678
diff changeset
    37
"del x Leaf = Leaf" |
70944
3fb16bed5d6c replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents: 70897
diff changeset
    38
"del x (Node l (a, _) r) =
61678
b594e9277be3 tuned white space
nipkow
parents: 61588
diff changeset
    39
  (case cmp x a of
66087
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
    40
     LT \<Rightarrow> if l \<noteq> Leaf \<and> color l = Black
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
    41
           then baldL (del x l) a r else R (del x l) a r |
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
    42
     GT \<Rightarrow> if r \<noteq> Leaf\<and> color r = Black
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
    43
           then baldR l a (del x r) else R l a (del x r) |
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
    44
     EQ \<Rightarrow> combine l r)"
61749
7f530d7e552d paint root black after insert and delete
nipkow
parents: 61678
diff changeset
    45
63411
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
    46
definition delete :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
61749
7f530d7e552d paint root black after insert and delete
nipkow
parents: 61678
diff changeset
    47
"delete x t = paint Black (del x t)"
61224
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
    48
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
    49
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
    50
subsection "Functional Correctness Proofs"
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
    51
61749
7f530d7e552d paint root black after insert and delete
nipkow
parents: 61678
diff changeset
    52
lemma inorder_paint: "inorder(paint c t) = inorder t"
62526
nipkow
parents: 61754
diff changeset
    53
by(cases t) (auto)
61749
7f530d7e552d paint root black after insert and delete
nipkow
parents: 61678
diff changeset
    54
64960
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
    55
lemma inorder_baliL:
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
    56
  "inorder(baliL l a r) = inorder l @ a # inorder r"
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
    57
by(cases "(l,a,r)" rule: baliL.cases) (auto)
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
    58
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
    59
lemma inorder_baliR:
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
    60
  "inorder(baliR l a r) = inorder l @ a # inorder r"
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
    61
by(cases "(l,a,r)" rule: baliR.cases) (auto)
61224
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
    62
61749
7f530d7e552d paint root black after insert and delete
nipkow
parents: 61678
diff changeset
    63
lemma inorder_ins:
7f530d7e552d paint root black after insert and delete
nipkow
parents: 61678
diff changeset
    64
  "sorted(inorder t) \<Longrightarrow> inorder(ins x t) = ins_list x (inorder t)"
64960
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
    65
by(induction x t rule: ins.induct)
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
    66
  (auto simp: ins_list_simps inorder_baliL inorder_baliR)
61749
7f530d7e552d paint root black after insert and delete
nipkow
parents: 61678
diff changeset
    67
61224
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
    68
lemma inorder_insert:
61749
7f530d7e552d paint root black after insert and delete
nipkow
parents: 61678
diff changeset
    69
  "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
7f530d7e552d paint root black after insert and delete
nipkow
parents: 61678
diff changeset
    70
by (simp add: insert_def inorder_ins inorder_paint)
61224
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
    71
64960
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
    72
lemma inorder_baldL:
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
    73
  "inorder(baldL l a r) = inorder l @ a # inorder r"
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
    74
by(cases "(l,a,r)" rule: baldL.cases)
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
    75
  (auto simp:  inorder_baliL inorder_baliR inorder_paint)
61224
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
    76
64960
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
    77
lemma inorder_baldR:
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
    78
  "inorder(baldR l a r) = inorder l @ a # inorder r"
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
    79
by(cases "(l,a,r)" rule: baldR.cases)
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
    80
  (auto simp:  inorder_baliL inorder_baliR inorder_paint)
61224
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
    81
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
    82
lemma inorder_combine:
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
    83
  "inorder(combine l r) = inorder l @ inorder r"
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
    84
by(induction l r rule: combine.induct)
64960
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
    85
  (auto simp: inorder_baldL inorder_baldR split: tree.split color.split)
61224
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
    86
61749
7f530d7e552d paint root black after insert and delete
nipkow
parents: 61678
diff changeset
    87
lemma inorder_del:
7f530d7e552d paint root black after insert and delete
nipkow
parents: 61678
diff changeset
    88
 "sorted(inorder t) \<Longrightarrow>  inorder(del x t) = del_list x (inorder t)"
66087
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
    89
by(induction x t rule: del.induct)
64960
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
    90
  (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR)
61224
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
    91
61749
7f530d7e552d paint root black after insert and delete
nipkow
parents: 61678
diff changeset
    92
lemma inorder_delete:
7f530d7e552d paint root black after insert and delete
nipkow
parents: 61678
diff changeset
    93
  "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
7f530d7e552d paint root black after insert and delete
nipkow
parents: 61678
diff changeset
    94
by (auto simp: delete_def inorder_del inorder_paint)
7f530d7e552d paint root black after insert and delete
nipkow
parents: 61678
diff changeset
    95
61581
00d9682e8dd7 Convertd to 3-way comparisons
nipkow
parents: 61428
diff changeset
    96
63411
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
    97
subsection \<open>Structural invariants\<close>
61224
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
    98
64952
f11e974b47e0 removed unclear clause; slower but clearer
nipkow
parents: 64951
diff changeset
    99
text\<open>The proofs are due to Markus Reiter and Alexander Krauss.\<close>
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   100
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   101
fun bheight :: "'a rbt \<Rightarrow> nat" where
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   102
"bheight Leaf = 0" |
70944
3fb16bed5d6c replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents: 70897
diff changeset
   103
"bheight (Node l (x, c) r) = (if c = Black then bheight l + 1 else bheight l)"
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   104
63411
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   105
fun invc :: "'a rbt \<Rightarrow> bool" where
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   106
"invc Leaf = True" |
70944
3fb16bed5d6c replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents: 70897
diff changeset
   107
"invc (Node l (a,c) r) =
64947
nipkow
parents: 64242
diff changeset
   108
  (invc l \<and> invc r \<and> (c = Red \<longrightarrow> color l = Black \<and> color r = Black))"
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   109
70897
nipkow
parents: 70757
diff changeset
   110
text \<open>Weaker version:\<close>
nipkow
parents: 70757
diff changeset
   111
abbreviation invc2 :: "'a rbt \<Rightarrow> bool" where
nipkow
parents: 70757
diff changeset
   112
"invc2 t \<equiv> invc(paint Black t)"
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   113
63411
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   114
fun invh :: "'a rbt \<Rightarrow> bool" where
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   115
"invh Leaf = True" |
70944
3fb16bed5d6c replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents: 70897
diff changeset
   116
"invh (Node l (x, c) r) = (invh l \<and> invh r \<and> bheight l = bheight r)"
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   117
64953
f9cfb10761ff tuned name
nipkow
parents: 64952
diff changeset
   118
lemma invc2I: "invc t \<Longrightarrow> invc2 t"
70944
3fb16bed5d6c replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents: 70897
diff changeset
   119
by (cases t rule: tree2_cases) simp+
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   120
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   121
definition rbt :: "'a rbt \<Rightarrow> bool" where
63411
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   122
"rbt t = (invc t \<and> invh t \<and> color t = Black)"
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   123
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   124
lemma color_paint_Black: "color (paint Black t) = Black"
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   125
by (cases t) auto
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   126
70897
nipkow
parents: 70757
diff changeset
   127
lemma paint2: "paint c2 (paint c1 t) = paint c2 t"
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   128
by (cases t) auto
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   129
63411
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   130
lemma invh_paint: "invh t \<Longrightarrow> invh (paint c t)"
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   131
by (cases t) auto
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   132
64960
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   133
lemma invc_baliL:
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   134
  "\<lbrakk>invc2 l; invc r\<rbrakk> \<Longrightarrow> invc (baliL l a r)" 
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   135
by (induct l a r rule: baliL.induct) auto
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   136
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   137
lemma invc_baliR:
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   138
  "\<lbrakk>invc l; invc2 r\<rbrakk> \<Longrightarrow> invc (baliR l a r)" 
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   139
by (induct l a r rule: baliR.induct) auto
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   140
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   141
lemma bheight_baliL:
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   142
  "bheight l = bheight r \<Longrightarrow> bheight (baliL l a r) = Suc (bheight l)"
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   143
by (induct l a r rule: baliL.induct) auto
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   144
64960
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   145
lemma bheight_baliR:
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   146
  "bheight l = bheight r \<Longrightarrow> bheight (baliR l a r) = Suc (bheight l)"
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   147
by (induct l a r rule: baliR.induct) auto
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   148
64960
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   149
lemma invh_baliL: 
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   150
  "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliL l a r)"
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   151
by (induct l a r rule: baliL.induct) auto
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   152
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   153
lemma invh_baliR: 
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   154
  "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliR l a r)"
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   155
by (induct l a r rule: baliR.induct) auto
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   156
70897
nipkow
parents: 70757
diff changeset
   157
text \<open>All in one:\<close>
nipkow
parents: 70757
diff changeset
   158
nipkow
parents: 70757
diff changeset
   159
lemma inv_baliR: "\<lbrakk> invh l; invh r; invc l; invc2 r; bheight l = bheight r \<rbrakk>
nipkow
parents: 70757
diff changeset
   160
 \<Longrightarrow> invc (baliR l a r) \<and> invh (baliR l a r) \<and> bheight (baliR l a r) = Suc (bheight l)"
nipkow
parents: 70757
diff changeset
   161
by (induct l a r rule: baliR.induct) auto
nipkow
parents: 70757
diff changeset
   162
nipkow
parents: 70757
diff changeset
   163
lemma inv_baliL: "\<lbrakk> invh l; invh r; invc2 l; invc r; bheight l = bheight r \<rbrakk>
nipkow
parents: 70757
diff changeset
   164
 \<Longrightarrow> invc (baliL l a r) \<and> invh (baliL l a r) \<and> bheight (baliL l a r) = Suc (bheight l)"
nipkow
parents: 70757
diff changeset
   165
by (induct l a r rule: baliL.induct) auto
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   166
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   167
subsubsection \<open>Insertion\<close>
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   168
70897
nipkow
parents: 70757
diff changeset
   169
lemma invc_ins: "invc t \<longrightarrow> invc2 (ins x t) \<and> (color t = Black \<longrightarrow> invc (ins x t))"
64960
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   170
by (induct x t rule: ins.induct) (auto simp: invc_baliL invc_baliR invc2I)
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   171
70897
nipkow
parents: 70757
diff changeset
   172
lemma invh_ins: "invh t \<Longrightarrow> invh (ins x t) \<and> bheight (ins x t) = bheight t"
64960
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   173
by(induct x t rule: ins.induct)
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   174
  (auto simp: invh_baliL invh_baliR bheight_baliL bheight_baliR)
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   175
63411
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   176
theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)"
70897
nipkow
parents: 70757
diff changeset
   177
by (simp add: invc_ins invh_ins color_paint_Black invh_paint rbt_def insert_def)
nipkow
parents: 70757
diff changeset
   178
nipkow
parents: 70757
diff changeset
   179
text \<open>All in one variant:\<close>
nipkow
parents: 70757
diff changeset
   180
nipkow
parents: 70757
diff changeset
   181
lemma inv_ins: "\<lbrakk> invc t; invh t \<rbrakk> \<Longrightarrow>
nipkow
parents: 70757
diff changeset
   182
  invc2 (ins x t) \<and> (color t = Black \<longrightarrow> invc (ins x t)) \<and>
nipkow
parents: 70757
diff changeset
   183
  invh(ins x t) \<and> bheight (ins x t) = bheight t"
nipkow
parents: 70757
diff changeset
   184
by (induct x t rule: ins.induct) (auto simp: inv_baliL inv_baliR invc2I)
nipkow
parents: 70757
diff changeset
   185
nipkow
parents: 70757
diff changeset
   186
theorem rbt_insert2: "rbt t \<Longrightarrow> rbt (insert x t)"
nipkow
parents: 70757
diff changeset
   187
by (simp add: inv_ins color_paint_Black invh_paint rbt_def insert_def)
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   188
63411
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   189
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   190
subsubsection \<open>Deletion\<close>
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   191
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   192
lemma bheight_paint_Red:
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   193
  "color t = Black \<Longrightarrow> bheight (paint Red t) = bheight t - 1"
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   194
by (cases t) auto
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   195
66087
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
   196
lemma invh_baldL_invc:
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
   197
  "\<lbrakk> invh l;  invh r;  bheight l + 1 = bheight r;  invc r \<rbrakk>
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
   198
   \<Longrightarrow> invh (baldL l a r) \<and> bheight (baldL l a r) = bheight l + 1"
64960
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   199
by (induct l a r rule: baldL.induct)
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   200
   (auto simp: invh_baliR invh_paint bheight_baliR bheight_paint_Red)
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   201
66087
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
   202
lemma invh_baldL_Black: 
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
   203
  "\<lbrakk> invh l;  invh r;  bheight l + 1 = bheight r;  color r = Black \<rbrakk>
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
   204
   \<Longrightarrow> invh (baldL l a r) \<and> bheight (baldL l a r) = bheight r"
64960
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   205
by (induct l a r rule: baldL.induct) (auto simp add: invh_baliR bheight_baliR) 
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   206
66087
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
   207
lemma invc_baldL: "\<lbrakk>invc2 l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (baldL l a r)"
64960
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   208
by (induct l a r rule: baldL.induct) (simp_all add: invc_baliR)
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   209
66087
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
   210
lemma invc2_baldL: "\<lbrakk> invc2 l; invc r \<rbrakk> \<Longrightarrow> invc2 (baldL l a r)"
70897
nipkow
parents: 70757
diff changeset
   211
by (induct l a r rule: baldL.induct) (auto simp: invc_baliR paint2 invc2I)
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   212
66087
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
   213
lemma invh_baldR_invc:
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
   214
  "\<lbrakk> invh l;  invh r;  bheight l = bheight r + 1;  invc l \<rbrakk>
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
   215
  \<Longrightarrow> invh (baldR l a r) \<and> bheight (baldR l a r) = bheight l"
64960
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   216
by(induct l a r rule: baldR.induct)
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   217
  (auto simp: invh_baliL bheight_baliL invh_paint bheight_paint_Red)
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   218
70757
e72daea2aab6 tuned names
nipkow
parents: 68999
diff changeset
   219
lemma invc_baldR: "\<lbrakk>invc l; invc2 r; color l = Black\<rbrakk> \<Longrightarrow> invc (baldR l a r)"
e72daea2aab6 tuned names
nipkow
parents: 68999
diff changeset
   220
by (induct l a r rule: baldR.induct) (simp_all add: invc_baliL)
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   221
70757
e72daea2aab6 tuned names
nipkow
parents: 68999
diff changeset
   222
lemma invc2_baldR: "\<lbrakk> invc l; invc2 r \<rbrakk> \<Longrightarrow>invc2 (baldR l a r)"
70897
nipkow
parents: 70757
diff changeset
   223
by (induct l a r rule: baldR.induct) (auto simp: invc_baliL paint2 invc2I)
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   224
63411
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   225
lemma invh_combine:
66087
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
   226
  "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk>
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
   227
  \<Longrightarrow> invh (combine l r) \<and> bheight (combine l r) = bheight l"
64960
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   228
by (induct l r rule: combine.induct) 
66087
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
   229
   (auto simp: invh_baldL_Black split: tree.splits color.splits)
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   230
63411
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   231
lemma invc_combine: 
70897
nipkow
parents: 70757
diff changeset
   232
  "\<lbrakk> invc l; invc r \<rbrakk> \<Longrightarrow>
nipkow
parents: 70757
diff changeset
   233
  (color l = Black \<and> color r = Black \<longrightarrow> invc (combine l r)) \<and> invc2 (combine l r)"
64960
8be78855ee7a split balance into two, clearer etc
nipkow
parents: 64953
diff changeset
   234
by (induct l r rule: combine.induct)
66087
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
   235
   (auto simp: invc_baldL invc2I split: tree.splits color.splits)
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   236
70944
3fb16bed5d6c replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents: 70897
diff changeset
   237
lemma neq_LeafD: "t \<noteq> Leaf \<Longrightarrow> \<exists>l x c r. t = Node l (x,c) r"
3fb16bed5d6c replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents: 70897
diff changeset
   238
by(cases t rule: tree2_cases) auto
66087
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
   239
66088
nipkow
parents: 66087
diff changeset
   240
lemma del_invc_invh: "invh t \<Longrightarrow> invc t \<Longrightarrow> invh (del x t) \<and>
nipkow
parents: 66087
diff changeset
   241
   (color t = Red \<and> bheight (del x t) = bheight t \<and> invc (del x t) \<or>
nipkow
parents: 66087
diff changeset
   242
    color t = Black \<and> bheight (del x t) = bheight t - 1 \<and> invc2 (del x t))"
nipkow
parents: 66087
diff changeset
   243
proof (induct x t rule: del.induct)
68414
b56ed5010e69 tuned order of arguments
nipkow
parents: 67967
diff changeset
   244
case (2 x _ y c)
66088
nipkow
parents: 66087
diff changeset
   245
  have "x = y \<or> x < y \<or> x > y" by auto
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   246
  thus ?case proof (elim disjE)
66088
nipkow
parents: 66087
diff changeset
   247
    assume "x = y"
63411
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   248
    with 2 show ?thesis
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   249
    by (cases c) (simp_all add: invh_combine invc_combine)
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   250
  next
66088
nipkow
parents: 66087
diff changeset
   251
    assume "x < y"
66087
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
   252
    with 2 show ?thesis
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
   253
      by(cases c)
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
   254
        (auto simp: invh_baldL_invc invc_baldL invc2_baldL dest: neq_LeafD)
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   255
  next
66088
nipkow
parents: 66087
diff changeset
   256
    assume "y < x"
66087
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
   257
    with 2 show ?thesis
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
   258
      by(cases c)
6e0c330f4051 simplified delete/proof
nipkow
parents: 64960
diff changeset
   259
        (auto simp: invh_baldR_invc invc_baldR invc2_baldR dest: neq_LeafD)
61754
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   260
  qed
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   261
qed auto
862daa8144f3 RBT invariants for insert
nipkow
parents: 61749
diff changeset
   262
70757
e72daea2aab6 tuned names
nipkow
parents: 68999
diff changeset
   263
theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete x t)"
70897
nipkow
parents: 70757
diff changeset
   264
by (metis delete_def rbt_def color_paint_Black del_invc_invh invc2I invh_paint)
63411
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   265
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   266
text \<open>Overall correctness:\<close>
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   267
68443
6826718f732d qualify interpretations to avoid clashes
nipkow
parents: 68431
diff changeset
   268
interpretation S: Set_by_Ordered
68431
b294e095f64c more abstract naming
nipkow
parents: 68414
diff changeset
   269
where empty = empty and isin = isin and insert = insert and delete = delete
63411
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   270
and inorder = inorder and inv = rbt
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   271
proof (standard, goal_cases)
68431
b294e095f64c more abstract naming
nipkow
parents: 68414
diff changeset
   272
  case 1 show ?case by (simp add: empty_def)
63411
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   273
next
67967
5a4280946a25 moved and renamed lemmas
nipkow
parents: 67963
diff changeset
   274
  case 2 thus ?case by(simp add: isin_set_inorder)
63411
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   275
next
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   276
  case 3 thus ?case by(simp add: inorder_insert)
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   277
next
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   278
  case 4 thus ?case by(simp add: inorder_delete)
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   279
next
68431
b294e095f64c more abstract naming
nipkow
parents: 68414
diff changeset
   280
  case 5 thus ?case by (simp add: rbt_def empty_def) 
63411
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   281
next
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   282
  case 6 thus ?case by (simp add: rbt_insert) 
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   283
next
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   284
  case 7 thus ?case by (simp add: rbt_delete) 
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   285
qed
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   286
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   287
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   288
subsection \<open>Height-Size Relation\<close>
e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents: 62526
diff changeset
   289
64950
10b8d31634cc added concise log height bound lemma
nipkow
parents: 64947
diff changeset
   290
lemma neq_Black[simp]: "(c \<noteq> Black) = (c = Red)"
10b8d31634cc added concise log height bound lemma
nipkow
parents: 64947
diff changeset
   291
by (cases c) auto
10b8d31634cc added concise log height bound lemma
nipkow
parents: 64947
diff changeset
   292
67963
nipkow
parents: 67118
diff changeset
   293
lemma rbt_height_bheight_if: "invc t \<Longrightarrow> invh t \<Longrightarrow>
71555
nipkow
parents: 70944
diff changeset
   294
  height t \<le> 2 * bheight t + (if color t = Black then 0 else 1)"
64950
10b8d31634cc added concise log height bound lemma
nipkow
parents: 64947
diff changeset
   295
by(induction t) (auto split: if_split_asm)
10b8d31634cc added concise log height bound lemma
nipkow
parents: 64947
diff changeset
   296
10b8d31634cc added concise log height bound lemma
nipkow
parents: 64947
diff changeset
   297
lemma rbt_height_bheight: "rbt t \<Longrightarrow> height t / 2 \<le> bheight t "
10b8d31634cc added concise log height bound lemma
nipkow
parents: 64947
diff changeset
   298
by(auto simp: rbt_def dest: rbt_height_bheight_if)
10b8d31634cc added concise log height bound lemma
nipkow
parents: 64947
diff changeset
   299
67963
nipkow
parents: 67118
diff changeset
   300
lemma bheight_size_bound:  "invc t \<Longrightarrow> invh t \<Longrightarrow> 2 ^ (bheight t) \<le> size1 t"
64950
10b8d31634cc added concise log height bound lemma
nipkow
parents: 64947
diff changeset
   301
by (induction t) auto
10b8d31634cc added concise log height bound lemma
nipkow
parents: 64947
diff changeset
   302
10b8d31634cc added concise log height bound lemma
nipkow
parents: 64947
diff changeset
   303
lemma rbt_height_le: assumes "rbt t" shows "height t \<le> 2 * log 2 (size1 t)"
10b8d31634cc added concise log height bound lemma
nipkow
parents: 64947
diff changeset
   304
proof -
10b8d31634cc added concise log height bound lemma
nipkow
parents: 64947
diff changeset
   305
  have "2 powr (height t / 2) \<le> 2 powr bheight t"
10b8d31634cc added concise log height bound lemma
nipkow
parents: 64947
diff changeset
   306
    using rbt_height_bheight[OF assms] by (simp)
10b8d31634cc added concise log height bound lemma
nipkow
parents: 64947
diff changeset
   307
  also have "\<dots> \<le> size1 t" using assms
10b8d31634cc added concise log height bound lemma
nipkow
parents: 64947
diff changeset
   308
    by (simp add: powr_realpow bheight_size_bound rbt_def)
10b8d31634cc added concise log height bound lemma
nipkow
parents: 64947
diff changeset
   309
  finally have "2 powr (height t / 2) \<le> size1 t" .
10b8d31634cc added concise log height bound lemma
nipkow
parents: 64947
diff changeset
   310
  hence "height t / 2 \<le> log 2 (size1 t)"
68999
818898556504 more traditional formulation
nipkow
parents: 68443
diff changeset
   311
    by (simp add: le_log_iff size1_size del: divide_le_eq_numeral1(1))
64950
10b8d31634cc added concise log height bound lemma
nipkow
parents: 64947
diff changeset
   312
  thus ?thesis by simp
10b8d31634cc added concise log height bound lemma
nipkow
parents: 64947
diff changeset
   313
qed
10b8d31634cc added concise log height bound lemma
nipkow
parents: 64947
diff changeset
   314
61224
759b5299a9f2 added red black trees
nipkow
parents:
diff changeset
   315
end