src/HOL/Data_Structures/AVL_Set.thy
author nipkow
Thu Nov 05 08:27:14 2015 +0100 (2015-11-05)
changeset 61581 00d9682e8dd7
parent 61428 5e1938107371
child 61588 1d2907d0ed73
permissions -rw-r--r--
Convertd to 3-way comparisons
     1 (*
     2 Author:     Tobias Nipkow
     3 Derived from AFP entry AVL.
     4 *)
     5 
     6 section "AVL Tree Implementation of Sets"
     7 
     8 theory AVL_Set
     9 imports Cmp Isin2
    10 begin
    11 
    12 type_synonym 'a avl_tree = "('a,nat) tree"
    13 
    14 text {* Invariant: *}
    15 
    16 fun avl :: "'a avl_tree \<Rightarrow> bool" where
    17 "avl Leaf = True" |
    18 "avl (Node h l a r) =
    19  ((height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1) \<and> 
    20   h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
    21 
    22 fun ht :: "'a avl_tree \<Rightarrow> nat" where
    23 "ht Leaf = 0" |
    24 "ht (Node h l a r) = h"
    25 
    26 definition node :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    27 "node l a r = Node (max (ht l) (ht r) + 1) l a r"
    28 
    29 definition balL :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    30 "balL l a r = (
    31   if ht l = ht r + 2 then (case l of 
    32     Node _ bl b br \<Rightarrow> (if ht bl < ht br
    33     then case br of
    34       Node _ cl c cr \<Rightarrow> node (node bl b cl) c (node cr a r)
    35     else node bl b (node br a r)))
    36   else node l a r)"
    37 
    38 definition balR :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    39 "balR l a r = (
    40   if ht r = ht l + 2 then (case r of
    41     Node _ bl b br \<Rightarrow> (if ht bl > ht br
    42     then case bl of
    43       Node _ cl c cr \<Rightarrow> node (node l a cl) c (node cr b br)
    44     else node (node l a bl) b br))
    45   else node l a r)"
    46 
    47 fun insert :: "'a::cmp \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    48 "insert x Leaf = Node 1 Leaf x Leaf" |
    49 "insert x (Node h l a r) = (case cmp x a of
    50    EQ \<Rightarrow> Node h l a r |
    51    LT \<Rightarrow> balL (insert x l) a r |
    52    GT \<Rightarrow> balR l a (insert x r))"
    53 
    54 fun delete_max :: "'a avl_tree \<Rightarrow> 'a avl_tree * 'a" where
    55 "delete_max (Node _ l a Leaf) = (l,a)" |
    56 "delete_max (Node _ l a r) =
    57   (let (r',a') = delete_max r in (balL l a r', a'))"
    58 
    59 lemmas delete_max_induct = delete_max.induct[case_names Leaf Node]
    60 
    61 fun delete_root :: "'a avl_tree \<Rightarrow> 'a avl_tree" where
    62 "delete_root (Node h Leaf a r) = r" |
    63 "delete_root (Node h l a Leaf) = l" |
    64 "delete_root (Node h l a r) =
    65   (let (l', a') = delete_max l in balR l' a' r)"
    66 
    67 lemmas delete_root_cases = delete_root.cases[case_names Leaf_t Node_Leaf Node_Node]
    68 
    69 fun delete :: "'a::cmp \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    70 "delete _ Leaf = Leaf" |
    71 "delete x (Node h l a r) = (case cmp x a of
    72    EQ \<Rightarrow> delete_root (Node h l a r) |
    73    LT \<Rightarrow> balR (delete x l) a r |
    74    GT \<Rightarrow> balL l a (delete x r))"
    75 
    76 
    77 subsection {* Functional Correctness Proofs *}
    78 
    79 text{* Very different from the AFP/AVL proofs *}
    80 
    81 
    82 subsubsection "Proofs for insert"
    83 
    84 lemma inorder_balL:
    85   "inorder (balL l a r) = inorder l @ a # inorder r"
    86 by (auto simp: node_def balL_def split:tree.splits)
    87 
    88 lemma inorder_balR:
    89   "inorder (balR l a r) = inorder l @ a # inorder r"
    90 by (auto simp: node_def balR_def split:tree.splits)
    91 
    92 theorem inorder_insert:
    93   "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
    94 by (induct t) 
    95    (auto simp: ins_list_simps inorder_balL inorder_balR)
    96 
    97 
    98 subsubsection "Proofs for delete"
    99 
   100 lemma inorder_delete_maxD:
   101   "\<lbrakk> delete_max t = (t',a); t \<noteq> Leaf \<rbrakk> \<Longrightarrow>
   102    inorder t' @ [a] = inorder t"
   103 by(induction t arbitrary: t' rule: delete_max.induct)
   104   (auto simp: inorder_balL split: prod.splits tree.split)
   105 
   106 lemma inorder_delete_root:
   107   "inorder (delete_root (Node h l a r)) = inorder l @ inorder r"
   108 by(induction "Node h l a r" arbitrary: l a r h rule: delete_root.induct)
   109   (auto simp: inorder_balR inorder_delete_maxD split: prod.splits)
   110 
   111 theorem inorder_delete:
   112   "sorted(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
   113 by(induction t)
   114   (auto simp: del_list_simps inorder_balL inorder_balR
   115     inorder_delete_root inorder_delete_maxD split: prod.splits)
   116 
   117 
   118 subsubsection "Overall functional correctness"
   119 
   120 interpretation Set_by_Ordered
   121 where empty = Leaf and isin = isin and insert = insert and delete = delete
   122 and inorder = inorder and wf = "\<lambda>_. True"
   123 proof (standard, goal_cases)
   124   case 1 show ?case by simp
   125 next
   126   case 2 thus ?case by(simp add: isin_set)
   127 next
   128   case 3 thus ?case by(simp add: inorder_insert)
   129 next
   130   case 4 thus ?case by(simp add: inorder_delete)
   131 qed (rule TrueI)+
   132 
   133 
   134 subsection {* AVL invariants *}
   135 
   136 text{* Essentially the AFP/AVL proofs *}
   137 
   138 
   139 subsubsection {* Insertion maintains AVL balance *}
   140 
   141 declare Let_def [simp]
   142 
   143 lemma [simp]: "avl t \<Longrightarrow> ht t = height t"
   144 by (induct t) simp_all
   145 
   146 lemma height_balL:
   147   "\<lbrakk> height l = height r + 2; avl l; avl r \<rbrakk> \<Longrightarrow>
   148    height (balL l a r) = height r + 2 \<or>
   149    height (balL l a r) = height r + 3"
   150 by (cases l) (auto simp:node_def balL_def split:tree.split)
   151        
   152 lemma height_balR:
   153   "\<lbrakk> height r = height l + 2; avl l; avl r \<rbrakk> \<Longrightarrow>
   154    height (balR l a r) = height l + 2 \<or>
   155    height (balR l a r) = height l + 3"
   156 by (cases r) (auto simp add:node_def balR_def split:tree.split)
   157 
   158 lemma [simp]: "height(node l a r) = max (height l) (height r) + 1"
   159 by (simp add: node_def)
   160 
   161 lemma avl_node:
   162   "\<lbrakk> avl l; avl r;
   163      height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1
   164    \<rbrakk> \<Longrightarrow> avl(node l a r)"
   165 by (auto simp add:max_def node_def)
   166 
   167 lemma height_balL2:
   168   "\<lbrakk> avl l; avl r; height l \<noteq> height r + 2 \<rbrakk> \<Longrightarrow>
   169    height (balL l a r) = (1 + max (height l) (height r))"
   170 by (cases l, cases r) (simp_all add: balL_def)
   171 
   172 lemma height_balR2:
   173   "\<lbrakk> avl l;  avl r;  height r \<noteq> height l + 2 \<rbrakk> \<Longrightarrow>
   174    height (balR l a r) = (1 + max (height l) (height r))"
   175 by (cases l, cases r) (simp_all add: balR_def)
   176 
   177 lemma avl_balL: 
   178   assumes "avl l" "avl r" and "height l = height r \<or> height l = height r + 1
   179     \<or> height r = height l + 1 \<or> height l = height r + 2" 
   180   shows "avl(balL l a r)"
   181 proof(cases l)
   182   case Leaf
   183   with assms show ?thesis by (simp add: node_def balL_def)
   184 next
   185   case (Node ln ll lr lh)
   186   with assms show ?thesis
   187   proof(cases "height l = height r + 2")
   188     case True
   189     from True Node assms show ?thesis
   190       by (auto simp: balL_def intro!: avl_node split: tree.split) arith+
   191   next
   192     case False
   193     with assms show ?thesis by (simp add: avl_node balL_def)
   194   qed
   195 qed
   196 
   197 lemma avl_balR: 
   198   assumes "avl l" and "avl r" and "height l = height r \<or> height l = height r + 1
   199     \<or> height r = height l + 1 \<or> height r = height l + 2" 
   200   shows "avl(balR l a r)"
   201 proof(cases r)
   202   case Leaf
   203   with assms show ?thesis by (simp add: node_def balR_def)
   204 next
   205   case (Node rn rl rr rh)
   206   with assms show ?thesis
   207   proof(cases "height r = height l + 2")
   208     case True
   209       from True Node assms show ?thesis
   210         by (auto simp: balR_def intro!: avl_node split: tree.split) arith+
   211   next
   212     case False
   213     with assms show ?thesis by (simp add: balR_def avl_node)
   214   qed
   215 qed
   216 
   217 (* It appears that these two properties need to be proved simultaneously: *)
   218 
   219 text{* Insertion maintains the AVL property: *}
   220 
   221 theorem avl_insert_aux:
   222   assumes "avl t"
   223   shows "avl(insert x t)"
   224         "(height (insert x t) = height t \<or> height (insert x t) = height t + 1)"
   225 using assms
   226 proof (induction t)
   227   case (Node h l a r)
   228   case 1
   229   with Node show ?case
   230   proof(cases "x = a")
   231     case True
   232     with Node 1 show ?thesis by simp
   233   next
   234     case False
   235     with Node 1 show ?thesis 
   236     proof(cases "x<a")
   237       case True
   238       with Node 1 show ?thesis by (auto simp add:avl_balL)
   239     next
   240       case False
   241       with Node 1 `x\<noteq>a` show ?thesis by (auto simp add:avl_balR)
   242     qed
   243   qed
   244   case 2
   245   from 2 Node show ?case
   246   proof(cases "x = a")
   247     case True
   248     with Node 1 show ?thesis by simp
   249   next
   250     case False
   251     with Node 1 show ?thesis 
   252      proof(cases "x<a")
   253       case True
   254       with Node 2 show ?thesis
   255       proof(cases "height (insert x l) = height r + 2")
   256         case False with Node 2 `x < a` show ?thesis by (auto simp: height_balL2)
   257       next
   258         case True 
   259         hence "(height (balL (insert x l) a r) = height r + 2) \<or>
   260           (height (balL (insert x l) a r) = height r + 3)" (is "?A \<or> ?B")
   261           using Node 2 by (intro height_balL) simp_all
   262         thus ?thesis
   263         proof
   264           assume ?A
   265           with 2 `x < a` show ?thesis by (auto)
   266         next
   267           assume ?B
   268           with True 1 Node(2) `x < a` show ?thesis by (simp) arith
   269         qed
   270       qed
   271     next
   272       case False
   273       with Node 2 show ?thesis 
   274       proof(cases "height (insert x r) = height l + 2")
   275         case False
   276         with Node 2 `\<not>x < a` show ?thesis by (auto simp: height_balR2)
   277       next
   278         case True 
   279         hence "(height (balR l a (insert x r)) = height l + 2) \<or>
   280           (height (balR l a (insert x r)) = height l + 3)"  (is "?A \<or> ?B")
   281           using Node 2 by (intro height_balR) simp_all
   282         thus ?thesis 
   283         proof
   284           assume ?A
   285           with 2 `\<not>x < a` show ?thesis by (auto)
   286         next
   287           assume ?B
   288           with True 1 Node(4) `\<not>x < a` show ?thesis by (simp) arith
   289         qed
   290       qed
   291     qed
   292   qed
   293 qed simp_all
   294 
   295 
   296 subsubsection {* Deletion maintains AVL balance *}
   297 
   298 lemma avl_delete_max:
   299   assumes "avl x" and "x \<noteq> Leaf"
   300   shows "avl (fst (delete_max x))" "height x = height(fst (delete_max x)) \<or>
   301          height x = height(fst (delete_max x)) + 1"
   302 using assms
   303 proof (induct x rule: delete_max_induct)
   304   case (Node h l a rh rl b rr)
   305   case 1
   306   with Node have "avl l" "avl (fst (delete_max (Node rh rl b rr)))" by auto
   307   with 1 Node have "avl (balL l a (fst (delete_max (Node rh rl b rr))))"
   308     by (intro avl_balL) fastforce+
   309   thus ?case 
   310     by (auto simp: height_balL height_balL2
   311       linorder_class.max.absorb1 linorder_class.max.absorb2
   312       split:prod.split)
   313 next
   314   case (Node h l a rh rl b rr)
   315   case 2
   316   let ?r = "Node rh rl b rr"
   317   let ?r' = "fst (delete_max ?r)"
   318   from `avl x` Node 2 have "avl l" and "avl ?r" by simp_all
   319   thus ?case using Node 2 height_balL[of l ?r' a] height_balL2[of l ?r' a]
   320     apply (auto split:prod.splits simp del:avl.simps) by arith+
   321 qed auto
   322 
   323 lemma avl_delete_root:
   324   assumes "avl t" and "t \<noteq> Leaf"
   325   shows "avl(delete_root t)" 
   326 using assms
   327 proof (cases t rule:delete_root_cases)
   328   case (Node_Node h lh ll ln lr n rh rl rn rr)
   329   let ?l = "Node lh ll ln lr"
   330   let ?r = "Node rh rl rn rr"
   331   let ?l' = "fst (delete_max ?l)"
   332   from `avl t` and Node_Node have "avl ?r" by simp
   333   from `avl t` and Node_Node have "avl ?l" by simp
   334   hence "avl(?l')" "height ?l = height(?l') \<or>
   335          height ?l = height(?l') + 1" by (rule avl_delete_max,simp)+
   336   with `avl t` Node_Node have "height ?l' = height ?r \<or> height ?l' = height ?r + 1
   337             \<or> height ?r = height ?l' + 1 \<or> height ?r = height ?l' + 2" by fastforce
   338   with `avl ?l'` `avl ?r` have "avl(balR ?l' (snd(delete_max ?l)) ?r)"
   339     by (rule avl_balR)
   340   with Node_Node show ?thesis by (auto split:prod.splits)
   341 qed simp_all
   342 
   343 lemma height_delete_root:
   344   assumes "avl t" and "t \<noteq> Leaf" 
   345   shows "height t = height(delete_root t) \<or> height t = height(delete_root t) + 1"
   346 using assms
   347 proof (cases t rule: delete_root_cases)
   348   case (Node_Node h lh ll ln lr n rh rl rn rr)
   349   let ?l = "Node lh ll ln lr"
   350   let ?r = "Node rh rl rn rr"
   351   let ?l' = "fst (delete_max ?l)"
   352   let ?t' = "balR ?l' (snd(delete_max ?l)) ?r"
   353   from `avl t` and Node_Node have "avl ?r" by simp
   354   from `avl t` and Node_Node have "avl ?l" by simp
   355   hence "avl(?l')"  by (rule avl_delete_max,simp)
   356   have l'_height: "height ?l = height ?l' \<or> height ?l = height ?l' + 1" using `avl ?l` by (intro avl_delete_max) auto
   357   have t_height: "height t = 1 + max (height ?l) (height ?r)" using `avl t` Node_Node by simp
   358   have "height t = height ?t' \<or> height t = height ?t' + 1" using  `avl t` Node_Node
   359   proof(cases "height ?r = height ?l' + 2")
   360     case False
   361     show ?thesis using l'_height t_height False by (subst  height_balR2[OF `avl ?l'` `avl ?r` False])+ arith
   362   next
   363     case True
   364     show ?thesis
   365     proof(cases rule: disjE[OF height_balR[OF True `avl ?l'` `avl ?r`, of "snd (delete_max ?l)"]])
   366       case 1
   367       thus ?thesis using l'_height t_height True by arith
   368     next
   369       case 2
   370       thus ?thesis using l'_height t_height True by arith
   371     qed
   372   qed
   373   thus ?thesis using Node_Node by (auto split:prod.splits)
   374 qed simp_all
   375 
   376 text{* Deletion maintains the AVL property: *}
   377 
   378 theorem avl_delete_aux:
   379   assumes "avl t" 
   380   shows "avl(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1"
   381 using assms
   382 proof (induct t)
   383   case (Node h l n r)
   384   case 1
   385   with Node show ?case
   386   proof(cases "x = n")
   387     case True
   388     with Node 1 show ?thesis by (auto simp:avl_delete_root)
   389   next
   390     case False
   391     with Node 1 show ?thesis 
   392     proof(cases "x<n")
   393       case True
   394       with Node 1 show ?thesis by (auto simp add:avl_balR)
   395     next
   396       case False
   397       with Node 1 `x\<noteq>n` show ?thesis by (auto simp add:avl_balL)
   398     qed
   399   qed
   400   case 2
   401   with Node show ?case
   402   proof(cases "x = n")
   403     case True
   404     with 1 have "height (Node h l n r) = height(delete_root (Node h l n r))
   405       \<or> height (Node h l n r) = height(delete_root (Node h l n r)) + 1"
   406       by (subst height_delete_root,simp_all)
   407     with True show ?thesis by simp
   408   next
   409     case False
   410     with Node 1 show ?thesis 
   411      proof(cases "x<n")
   412       case True
   413       show ?thesis
   414       proof(cases "height r = height (delete x l) + 2")
   415         case False with Node 1 `x < n` show ?thesis by(auto simp: balR_def)
   416       next
   417         case True 
   418         hence "(height (balR (delete x l) n r) = height (delete x l) + 2) \<or>
   419           height (balR (delete x l) n r) = height (delete x l) + 3" (is "?A \<or> ?B")
   420           using Node 2 by (intro height_balR) auto
   421         thus ?thesis 
   422         proof
   423           assume ?A
   424           with `x < n` Node 2 show ?thesis by(auto simp: balR_def)
   425         next
   426           assume ?B
   427           with `x < n` Node 2 show ?thesis by(auto simp: balR_def)
   428         qed
   429       qed
   430     next
   431       case False
   432       show ?thesis
   433       proof(cases "height l = height (delete x r) + 2")
   434         case False with Node 1 `\<not>x < n` `x \<noteq> n` show ?thesis by(auto simp: balL_def)
   435       next
   436         case True 
   437         hence "(height (balL l n (delete x r)) = height (delete x r) + 2) \<or>
   438           height (balL l n (delete x r)) = height (delete x r) + 3" (is "?A \<or> ?B")
   439           using Node 2 by (intro height_balL) auto
   440         thus ?thesis 
   441         proof
   442           assume ?A
   443           with `\<not>x < n` `x \<noteq> n` Node 2 show ?thesis by(auto simp: balL_def)
   444         next
   445           assume ?B
   446           with `\<not>x < n` `x \<noteq> n` Node 2 show ?thesis by(auto simp: balL_def)
   447         qed
   448       qed
   449     qed
   450   qed
   451 qed simp_all
   452 
   453 end