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