src/HOL/Data_Structures/AVL_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@61232
     1
(* Author: Tobias Nipkow *)
nipkow@61232
     2
nipkow@61232
     3
section "AVL Tree Implementation of Maps"
nipkow@61232
     4
nipkow@61232
     5
theory AVL_Map
nipkow@61232
     6
imports
nipkow@61232
     7
  AVL_Set
nipkow@61232
     8
  Lookup2
nipkow@61232
     9
begin
nipkow@61232
    10
nipkow@63411
    11
fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
nipkow@68413
    12
"update x y Leaf = Node Leaf (x,y) 1 Leaf" |
nipkow@68413
    13
"update x y (Node l (a,b) h r) = (case cmp x a of
nipkow@68413
    14
   EQ \<Rightarrow> Node l (x,y) h r |
nipkow@61581
    15
   LT \<Rightarrow> balL (update x y l) (a,b) r |
nipkow@61581
    16
   GT \<Rightarrow> balR l (a,b) (update x y r))"
nipkow@61232
    17
nipkow@63411
    18
fun delete :: "'a::linorder \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
nipkow@61232
    19
"delete _ Leaf = Leaf" |
nipkow@68413
    20
"delete x (Node l (a,b) h r) = (case cmp x a of
nipkow@68413
    21
   EQ \<Rightarrow> del_root (Node l (a,b) h r) |
nipkow@61581
    22
   LT \<Rightarrow> balR (delete x l) (a,b) r |
nipkow@61581
    23
   GT \<Rightarrow> balL l (a,b) (delete x r))"
nipkow@61232
    24
nipkow@61232
    25
nipkow@68422
    26
subsection \<open>Functional Correctness\<close>
nipkow@61232
    27
nipkow@68440
    28
theorem inorder_update:
nipkow@61232
    29
  "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
nipkow@61581
    30
by (induct t) (auto simp: upd_list_simps inorder_balL inorder_balR)
nipkow@61232
    31
nipkow@61232
    32
nipkow@68440
    33
theorem inorder_delete:
nipkow@61232
    34
  "sorted1(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
nipkow@61232
    35
by(induction t)
nipkow@61581
    36
  (auto simp: del_list_simps inorder_balL inorder_balR
nipkow@68023
    37
     inorder_del_root inorder_split_maxD split: prod.splits)
nipkow@61232
    38
nipkow@68422
    39
nipkow@68422
    40
subsection \<open>AVL invariants\<close>
nipkow@68422
    41
nipkow@68422
    42
nipkow@68422
    43
subsubsection \<open>Insertion maintains AVL balance\<close>
nipkow@68422
    44
nipkow@68422
    45
theorem avl_update:
nipkow@68422
    46
  assumes "avl t"
nipkow@68422
    47
  shows "avl(update x y t)"
nipkow@68422
    48
        "(height (update x y t) = height t \<or> height (update x y t) = height t + 1)"
nipkow@68422
    49
using assms
nipkow@68422
    50
proof (induction x y t rule: update.induct)
nipkow@68422
    51
  case eq2: (2 x y l a b h r)
nipkow@68422
    52
  case 1
nipkow@68422
    53
  show ?case
nipkow@68422
    54
  proof(cases "x = a")
nipkow@68422
    55
    case True with eq2 1 show ?thesis by simp
nipkow@68422
    56
  next
nipkow@68422
    57
    case False
nipkow@68422
    58
    with eq2 1 show ?thesis 
nipkow@68422
    59
    proof(cases "x<a")
nipkow@68422
    60
      case True with eq2 1 show ?thesis by (auto simp add:avl_balL)
nipkow@68422
    61
    next
nipkow@68422
    62
      case False with eq2 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balR)
nipkow@68422
    63
    qed
nipkow@68422
    64
  qed
nipkow@68422
    65
  case 2
nipkow@68422
    66
  show ?case
nipkow@68422
    67
  proof(cases "x = a")
nipkow@68422
    68
    case True with eq2 1 show ?thesis by simp
nipkow@68422
    69
  next
nipkow@68422
    70
    case False
nipkow@68422
    71
    show ?thesis 
nipkow@68422
    72
    proof(cases "x<a")
nipkow@68422
    73
      case True
nipkow@68422
    74
      show ?thesis
nipkow@68422
    75
      proof(cases "height (update x y l) = height r + 2")
nipkow@68422
    76
        case False with eq2 2 \<open>x < a\<close> show ?thesis by (auto simp: height_balL2)
nipkow@68422
    77
      next
nipkow@68422
    78
        case True 
nipkow@68422
    79
        hence "(height (balL (update x y l) (a,b) r) = height r + 2) \<or>
nipkow@68422
    80
          (height (balL (update x y l) (a,b) r) = height r + 3)" (is "?A \<or> ?B")
nipkow@68422
    81
          using eq2 2 \<open>x<a\<close> by (intro height_balL) simp_all
nipkow@68422
    82
        thus ?thesis
nipkow@68422
    83
        proof
nipkow@68422
    84
          assume ?A with 2 \<open>x < a\<close> show ?thesis by (auto)
nipkow@68422
    85
        next
nipkow@68422
    86
          assume ?B with True 1 eq2(2) \<open>x < a\<close> show ?thesis by (simp) arith
nipkow@68422
    87
        qed
nipkow@68422
    88
      qed
nipkow@68422
    89
    next
nipkow@68422
    90
      case False
nipkow@68422
    91
      show ?thesis
nipkow@68422
    92
      proof(cases "height (update x y r) = height l + 2")
nipkow@68422
    93
        case False with eq2 2 \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2)
nipkow@68422
    94
      next
nipkow@68422
    95
        case True 
nipkow@68422
    96
        hence "(height (balR l (a,b) (update x y r)) = height l + 2) \<or>
nipkow@68422
    97
          (height (balR l (a,b) (update x y r)) = height l + 3)"  (is "?A \<or> ?B")
nipkow@68422
    98
          using eq2 2 \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> by (intro height_balR) simp_all
nipkow@68422
    99
        thus ?thesis 
nipkow@68422
   100
        proof
nipkow@68422
   101
          assume ?A with 2 \<open>\<not>x < a\<close> show ?thesis by (auto)
nipkow@68422
   102
        next
nipkow@68422
   103
          assume ?B with True 1 eq2(4) \<open>\<not>x < a\<close> show ?thesis by (simp) arith
nipkow@68422
   104
        qed
nipkow@68422
   105
      qed
nipkow@68422
   106
    qed
nipkow@68422
   107
  qed
nipkow@68422
   108
qed simp_all
nipkow@68422
   109
nipkow@68422
   110
nipkow@68422
   111
subsubsection \<open>Deletion maintains AVL balance\<close>
nipkow@68422
   112
nipkow@68422
   113
theorem avl_delete:
nipkow@68422
   114
  assumes "avl t" 
nipkow@68422
   115
  shows "avl(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1"
nipkow@68422
   116
using assms
nipkow@68422
   117
proof (induct t)
nipkow@68422
   118
  case (Node l n h r)
nipkow@68422
   119
  obtain a b where [simp]: "n = (a,b)" by fastforce
nipkow@68422
   120
  case 1
nipkow@68422
   121
  show ?case
nipkow@68422
   122
  proof(cases "x = a")
nipkow@68422
   123
    case True with Node 1 show ?thesis by (auto simp:avl_del_root)
nipkow@68422
   124
  next
nipkow@68422
   125
    case False
nipkow@68422
   126
    show ?thesis 
nipkow@68422
   127
    proof(cases "x<a")
nipkow@68422
   128
      case True with Node 1 show ?thesis by (auto simp add:avl_balR)
nipkow@68422
   129
    next
nipkow@68422
   130
      case False with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balL)
nipkow@68422
   131
    qed
nipkow@68422
   132
  qed
nipkow@68422
   133
  case 2
nipkow@68422
   134
  show ?case
nipkow@68422
   135
  proof(cases "x = a")
nipkow@68422
   136
    case True
nipkow@68422
   137
    with 1 have "height (Node l n h r) = height(del_root (Node l n h r))
nipkow@68422
   138
      \<or> height (Node l n h r) = height(del_root (Node l n h r)) + 1"
nipkow@68422
   139
      by (subst height_del_root,simp_all)
nipkow@68422
   140
    with True show ?thesis by simp
nipkow@68422
   141
  next
nipkow@68422
   142
    case False
nipkow@68422
   143
    show ?thesis 
nipkow@68422
   144
    proof(cases "x<a")
nipkow@68422
   145
      case True
nipkow@68422
   146
      show ?thesis
nipkow@68422
   147
      proof(cases "height r = height (delete x l) + 2")
nipkow@68422
   148
        case False with Node 1 \<open>x < a\<close> show ?thesis by(auto simp: balR_def)
nipkow@68422
   149
      next
nipkow@68422
   150
        case True 
nipkow@68422
   151
        hence "(height (balR (delete x l) n r) = height (delete x l) + 2) \<or>
nipkow@68422
   152
          height (balR (delete x l) n r) = height (delete x l) + 3" (is "?A \<or> ?B")
nipkow@68422
   153
          using Node 2 by (intro height_balR) auto
nipkow@68422
   154
        thus ?thesis 
nipkow@68422
   155
        proof
nipkow@68422
   156
          assume ?A with \<open>x < a\<close> Node 2 show ?thesis by(auto simp: balR_def)
nipkow@68422
   157
        next
nipkow@68422
   158
          assume ?B with \<open>x < a\<close> Node 2 show ?thesis by(auto simp: balR_def)
nipkow@68422
   159
        qed
nipkow@68422
   160
      qed
nipkow@68422
   161
    next
nipkow@68422
   162
      case False
nipkow@68422
   163
      show ?thesis
nipkow@68422
   164
      proof(cases "height l = height (delete x r) + 2")
nipkow@68422
   165
        case False with Node 1 \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> show ?thesis by(auto simp: balL_def)
nipkow@68422
   166
      next
nipkow@68422
   167
        case True 
nipkow@68422
   168
        hence "(height (balL l n (delete x r)) = height (delete x r) + 2) \<or>
nipkow@68422
   169
          height (balL l n (delete x r)) = height (delete x r) + 3" (is "?A \<or> ?B")
nipkow@68422
   170
          using Node 2 by (intro height_balL) auto
nipkow@68422
   171
        thus ?thesis 
nipkow@68422
   172
        proof
nipkow@68422
   173
          assume ?A with \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> Node 2 show ?thesis by(auto simp: balL_def)
nipkow@68422
   174
        next
nipkow@68422
   175
          assume ?B with \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> Node 2 show ?thesis by(auto simp: balL_def)
nipkow@68422
   176
        qed
nipkow@68422
   177
      qed
nipkow@68422
   178
    qed
nipkow@68422
   179
  qed
nipkow@68422
   180
qed simp_all
nipkow@68422
   181
nipkow@68422
   182
nipkow@68440
   183
interpretation M: Map_by_Ordered
nipkow@68431
   184
where empty = empty and lookup = lookup and update = update and delete = delete
nipkow@68422
   185
and inorder = inorder and inv = avl
nipkow@61232
   186
proof (standard, goal_cases)
nipkow@68431
   187
  case 1 show ?case by (simp add: empty_def)
nipkow@61232
   188
next
nipkow@61790
   189
  case 2 thus ?case by(simp add: lookup_map_of)
nipkow@61232
   190
next
nipkow@68440
   191
  case 3 thus ?case by(simp add: inorder_update)
nipkow@61232
   192
next
nipkow@68440
   193
  case 4 thus ?case by(simp add: inorder_delete)
nipkow@68422
   194
next
nipkow@68431
   195
  case 5 show ?case by (simp add: empty_def)
nipkow@68422
   196
next
nipkow@68422
   197
  case 6 thus ?case by(simp add: avl_update(1))
nipkow@68422
   198
next
nipkow@68422
   199
  case 7 thus ?case by(simp add: avl_delete(1))
nipkow@68422
   200
qed
nipkow@61232
   201
nipkow@61232
   202
end