src/HOL/Data_Structures/RBT_Map.thy
author nipkow
Wed Jun 13 15:24:20 2018 +0200 (12 months ago)
changeset 68440 6826718f732d
parent 68431 b294e095f64c
permissions -rw-r--r--
qualify interpretations to avoid clashes
nipkow@61224
     1
(* Author: Tobias Nipkow *)
nipkow@61224
     2
nipkow@61224
     3
section \<open>Red-Black Tree Implementation of Maps\<close>
nipkow@61224
     4
nipkow@61224
     5
theory RBT_Map
nipkow@61224
     6
imports
nipkow@61224
     7
  RBT_Set
nipkow@61231
     8
  Lookup2
nipkow@61224
     9
begin
nipkow@61224
    10
nipkow@63411
    11
fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
nipkow@61749
    12
"upd x y Leaf = R Leaf (x,y) Leaf" |
nipkow@61749
    13
"upd x y (B l (a,b) r) = (case cmp x a of
nipkow@64960
    14
  LT \<Rightarrow> baliL (upd x y l) (a,b) r |
nipkow@64960
    15
  GT \<Rightarrow> baliR l (a,b) (upd x y r) |
nipkow@61581
    16
  EQ \<Rightarrow> B l (x,y) r)" |
nipkow@61749
    17
"upd x y (R l (a,b) r) = (case cmp x a of
nipkow@61749
    18
  LT \<Rightarrow> R (upd x y l) (a,b) r |
nipkow@61749
    19
  GT \<Rightarrow> R l (a,b) (upd x y r) |
nipkow@61581
    20
  EQ \<Rightarrow> R l (x,y) r)"
nipkow@61224
    21
nipkow@63411
    22
definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
nipkow@61749
    23
"update x y t = paint Black (upd x y t)"
nipkow@61749
    24
nipkow@68415
    25
fun del :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt" where
nipkow@61749
    26
"del x Leaf = Leaf" |
nipkow@68415
    27
"del x (Node l (a,b) c r) = (case cmp x a of
nipkow@68415
    28
     LT \<Rightarrow> if l \<noteq> Leaf \<and> color l = Black
nipkow@68415
    29
           then baldL (del x l) (a,b) r else R (del x l) (a,b) r |
nipkow@68415
    30
     GT \<Rightarrow> if r \<noteq> Leaf\<and> color r = Black
nipkow@68415
    31
           then baldR l (a,b) (del x r) else R l (a,b) (del x r) |
nipkow@68415
    32
  EQ \<Rightarrow> combine l r)"
nipkow@61749
    33
nipkow@63411
    34
definition delete :: "'a::linorder \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
nipkow@61749
    35
"delete x t = paint Black (del x t)"
nipkow@61224
    36
nipkow@61224
    37
nipkow@61224
    38
subsection "Functional Correctness Proofs"
nipkow@61224
    39
nipkow@61749
    40
lemma inorder_upd:
nipkow@61749
    41
  "sorted1(inorder t) \<Longrightarrow> inorder(upd x y t) = upd_list x y (inorder t)"
nipkow@61749
    42
by(induction x y t rule: upd.induct)
nipkow@64960
    43
  (auto simp: upd_list_simps inorder_baliL inorder_baliR)
nipkow@61749
    44
nipkow@68440
    45
lemma inorder_update:
nipkow@61224
    46
  "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
nipkow@61749
    47
by(simp add: update_def inorder_upd inorder_paint)
nipkow@61224
    48
nipkow@61749
    49
lemma inorder_del:
nipkow@68415
    50
 "sorted1(inorder t) \<Longrightarrow>  inorder(del x t) = del_list x (inorder t)"
nipkow@68415
    51
by(induction x t rule: del.induct)
nipkow@64960
    52
  (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR)
nipkow@61224
    53
nipkow@68440
    54
lemma inorder_delete:
nipkow@61749
    55
  "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
nipkow@61749
    56
by(simp add: delete_def inorder_del inorder_paint)
nipkow@61224
    57
nipkow@68415
    58
nipkow@68415
    59
subsection \<open>Structural invariants\<close>
nipkow@68415
    60
nipkow@68415
    61
subsubsection \<open>Update\<close>
nipkow@68415
    62
nipkow@68415
    63
lemma invc_upd: assumes "invc t"
nipkow@68415
    64
  shows "color t = Black \<Longrightarrow> invc (upd x y t)" "invc2 (upd x y t)"
nipkow@68415
    65
using assms
nipkow@68415
    66
by (induct x y t rule: upd.induct) (auto simp: invc_baliL invc_baliR invc2I)
nipkow@68415
    67
nipkow@68415
    68
lemma invh_upd: assumes "invh t"
nipkow@68415
    69
  shows "invh (upd x y t)" "bheight (upd x y t) = bheight t"
nipkow@68415
    70
using assms
nipkow@68415
    71
by(induct x y t rule: upd.induct)
nipkow@68415
    72
  (auto simp: invh_baliL invh_baliR bheight_baliL bheight_baliR)
nipkow@68415
    73
nipkow@68415
    74
theorem rbt_update: "rbt t \<Longrightarrow> rbt (update x y t)"
nipkow@68415
    75
by (simp add: invc_upd(2) invh_upd(1) color_paint_Black invc_paint_Black invh_paint
nipkow@68415
    76
  rbt_def update_def)
nipkow@68415
    77
nipkow@68415
    78
nipkow@68415
    79
subsubsection \<open>Deletion\<close>
nipkow@68415
    80
nipkow@68415
    81
lemma del_invc_invh: "invh t \<Longrightarrow> invc t \<Longrightarrow> invh (del x t) \<and>
nipkow@68415
    82
   (color t = Red \<and> bheight (del x t) = bheight t \<and> invc (del x t) \<or>
nipkow@68415
    83
    color t = Black \<and> bheight (del x t) = bheight t - 1 \<and> invc2 (del x t))"
nipkow@68415
    84
proof (induct x t rule: del.induct)
nipkow@68415
    85
case (2 x _ y _ c)
nipkow@68415
    86
  have "x = y \<or> x < y \<or> x > y" by auto
nipkow@68415
    87
  thus ?case proof (elim disjE)
nipkow@68415
    88
    assume "x = y"
nipkow@68415
    89
    with 2 show ?thesis
nipkow@68415
    90
    by (cases c) (simp_all add: invh_combine invc_combine)
nipkow@68415
    91
  next
nipkow@68415
    92
    assume "x < y"
nipkow@68415
    93
    with 2 show ?thesis
nipkow@68415
    94
      by(cases c)
nipkow@68415
    95
        (auto simp: invh_baldL_invc invc_baldL invc2_baldL dest: neq_LeafD)
nipkow@68415
    96
  next
nipkow@68415
    97
    assume "y < x"
nipkow@68415
    98
    with 2 show ?thesis
nipkow@68415
    99
      by(cases c)
nipkow@68415
   100
        (auto simp: invh_baldR_invc invc_baldR invc2_baldR dest: neq_LeafD)
nipkow@68415
   101
  qed
nipkow@68415
   102
qed auto
nipkow@68415
   103
nipkow@68415
   104
theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete k t)"
nipkow@68415
   105
by (metis delete_def rbt_def color_paint_Black del_invc_invh invc_paint_Black invc2I invh_paint)
nipkow@68415
   106
nipkow@68440
   107
interpretation M: Map_by_Ordered
nipkow@68431
   108
where empty = empty and lookup = lookup and update = update and delete = delete
nipkow@68415
   109
and inorder = inorder and inv = rbt
nipkow@61224
   110
proof (standard, goal_cases)
nipkow@68431
   111
  case 1 show ?case by (simp add: empty_def)
nipkow@61224
   112
next
nipkow@61790
   113
  case 2 thus ?case by(simp add: lookup_map_of)
nipkow@61224
   114
next
nipkow@68440
   115
  case 3 thus ?case by(simp add: inorder_update)
nipkow@61224
   116
next
nipkow@68440
   117
  case 4 thus ?case by(simp add: inorder_delete)
nipkow@68415
   118
next
nipkow@68431
   119
  case 5 thus ?case by (simp add: rbt_def empty_def) 
nipkow@68415
   120
next
nipkow@68415
   121
  case 6 thus ?case by (simp add: rbt_update) 
nipkow@68415
   122
next
nipkow@68415
   123
  case 7 thus ?case by (simp add: rbt_delete) 
nipkow@68415
   124
qed
nipkow@61224
   125
nipkow@61224
   126
end