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