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