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