src/HOL/Data_Structures/AVL_Set.thy
changeset 61581 00d9682e8dd7
parent 61428 5e1938107371
child 61588 1d2907d0ed73
     1.1 --- a/src/HOL/Data_Structures/AVL_Set.thy	Wed Nov 04 15:07:23 2015 +0100
     1.2 +++ b/src/HOL/Data_Structures/AVL_Set.thy	Thu Nov 05 08:27:14 2015 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  section "AVL Tree Implementation of Sets"
     1.5  
     1.6  theory AVL_Set
     1.7 -imports Isin2
     1.8 +imports Cmp Isin2
     1.9  begin
    1.10  
    1.11  type_synonym 'a avl_tree = "('a,nat) tree"
    1.12 @@ -26,8 +26,8 @@
    1.13  definition node :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.14  "node l a r = Node (max (ht l) (ht r) + 1) l a r"
    1.15  
    1.16 -definition node_bal_l :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.17 -"node_bal_l l a r = (
    1.18 +definition balL :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.19 +"balL l a r = (
    1.20    if ht l = ht r + 2 then (case l of 
    1.21      Node _ bl b br \<Rightarrow> (if ht bl < ht br
    1.22      then case br of
    1.23 @@ -35,8 +35,8 @@
    1.24      else node bl b (node br a r)))
    1.25    else node l a r)"
    1.26  
    1.27 -definition node_bal_r :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.28 -"node_bal_r l a r = (
    1.29 +definition balR :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.30 +"balR l a r = (
    1.31    if ht r = ht l + 2 then (case r of
    1.32      Node _ bl b br \<Rightarrow> (if ht bl > ht br
    1.33      then case bl of
    1.34 @@ -44,19 +44,17 @@
    1.35      else node (node l a bl) b br))
    1.36    else node l a r)"
    1.37  
    1.38 -fun insert :: "'a::order \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.39 +fun insert :: "'a::cmp \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.40  "insert x Leaf = Node 1 Leaf x Leaf" |
    1.41 -"insert x (Node h l a r) = 
    1.42 -   (if x=a then Node h l a r
    1.43 -    else if x<a
    1.44 -      then node_bal_l (insert x l) a r
    1.45 -      else node_bal_r l a (insert x r))"
    1.46 +"insert x (Node h l a r) = (case cmp x a of
    1.47 +   EQ \<Rightarrow> Node h l a r |
    1.48 +   LT \<Rightarrow> balL (insert x l) a r |
    1.49 +   GT \<Rightarrow> balR l a (insert x r))"
    1.50  
    1.51  fun delete_max :: "'a avl_tree \<Rightarrow> 'a avl_tree * 'a" where
    1.52  "delete_max (Node _ l a Leaf) = (l,a)" |
    1.53 -"delete_max (Node _ l a r) = (
    1.54 -  let (r',a') = delete_max r in
    1.55 -  (node_bal_l l a r', a'))"
    1.56 +"delete_max (Node _ l a r) =
    1.57 +  (let (r',a') = delete_max r in (balL l a r', a'))"
    1.58  
    1.59  lemmas delete_max_induct = delete_max.induct[case_names Leaf Node]
    1.60  
    1.61 @@ -64,16 +62,16 @@
    1.62  "delete_root (Node h Leaf a r) = r" |
    1.63  "delete_root (Node h l a Leaf) = l" |
    1.64  "delete_root (Node h l a r) =
    1.65 -  (let (l', a') = delete_max l in node_bal_r l' a' r)"
    1.66 +  (let (l', a') = delete_max l in balR l' a' r)"
    1.67  
    1.68  lemmas delete_root_cases = delete_root.cases[case_names Leaf_t Node_Leaf Node_Node]
    1.69  
    1.70 -fun delete :: "'a::order \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.71 +fun delete :: "'a::cmp \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.72  "delete _ Leaf = Leaf" |
    1.73 -"delete x (Node h l a r) = (
    1.74 -   if x = a then delete_root (Node h l a r)
    1.75 -   else if x < a then node_bal_r (delete x l) a r
    1.76 -   else node_bal_l l a (delete x r))"
    1.77 +"delete x (Node h l a r) = (case cmp x a of
    1.78 +   EQ \<Rightarrow> delete_root (Node h l a r) |
    1.79 +   LT \<Rightarrow> balR (delete x l) a r |
    1.80 +   GT \<Rightarrow> balL l a (delete x r))"
    1.81  
    1.82  
    1.83  subsection {* Functional Correctness Proofs *}
    1.84 @@ -83,18 +81,18 @@
    1.85  
    1.86  subsubsection "Proofs for insert"
    1.87  
    1.88 -lemma inorder_node_bal_l:
    1.89 -  "inorder (node_bal_l l a r) = inorder l @ a # inorder r"
    1.90 -by (auto simp: node_def node_bal_l_def split:tree.splits)
    1.91 +lemma inorder_balL:
    1.92 +  "inorder (balL l a r) = inorder l @ a # inorder r"
    1.93 +by (auto simp: node_def balL_def split:tree.splits)
    1.94  
    1.95 -lemma inorder_node_bal_r:
    1.96 -  "inorder (node_bal_r l a r) = inorder l @ a # inorder r"
    1.97 -by (auto simp: node_def node_bal_r_def split:tree.splits)
    1.98 +lemma inorder_balR:
    1.99 +  "inorder (balR l a r) = inorder l @ a # inorder r"
   1.100 +by (auto simp: node_def balR_def split:tree.splits)
   1.101  
   1.102  theorem inorder_insert:
   1.103    "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
   1.104  by (induct t) 
   1.105 -   (auto simp: ins_list_simps inorder_node_bal_l inorder_node_bal_r)
   1.106 +   (auto simp: ins_list_simps inorder_balL inorder_balR)
   1.107  
   1.108  
   1.109  subsubsection "Proofs for delete"
   1.110 @@ -103,17 +101,17 @@
   1.111    "\<lbrakk> delete_max t = (t',a); t \<noteq> Leaf \<rbrakk> \<Longrightarrow>
   1.112     inorder t' @ [a] = inorder t"
   1.113  by(induction t arbitrary: t' rule: delete_max.induct)
   1.114 -  (auto simp: inorder_node_bal_l split: prod.splits tree.split)
   1.115 +  (auto simp: inorder_balL split: prod.splits tree.split)
   1.116  
   1.117  lemma inorder_delete_root:
   1.118    "inorder (delete_root (Node h l a r)) = inorder l @ inorder r"
   1.119  by(induction "Node h l a r" arbitrary: l a r h rule: delete_root.induct)
   1.120 -  (auto simp: inorder_node_bal_r inorder_delete_maxD split: prod.splits)
   1.121 +  (auto simp: inorder_balR inorder_delete_maxD split: prod.splits)
   1.122  
   1.123  theorem inorder_delete:
   1.124    "sorted(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
   1.125  by(induction t)
   1.126 -  (auto simp: del_list_simps inorder_node_bal_l inorder_node_bal_r
   1.127 +  (auto simp: del_list_simps inorder_balL inorder_balR
   1.128      inorder_delete_root inorder_delete_maxD split: prod.splits)
   1.129  
   1.130  
   1.131 @@ -145,17 +143,17 @@
   1.132  lemma [simp]: "avl t \<Longrightarrow> ht t = height t"
   1.133  by (induct t) simp_all
   1.134  
   1.135 -lemma height_node_bal_l:
   1.136 +lemma height_balL:
   1.137    "\<lbrakk> height l = height r + 2; avl l; avl r \<rbrakk> \<Longrightarrow>
   1.138 -   height (node_bal_l l a r) = height r + 2 \<or>
   1.139 -   height (node_bal_l l a r) = height r + 3"
   1.140 -by (cases l) (auto simp:node_def node_bal_l_def split:tree.split)
   1.141 +   height (balL l a r) = height r + 2 \<or>
   1.142 +   height (balL l a r) = height r + 3"
   1.143 +by (cases l) (auto simp:node_def balL_def split:tree.split)
   1.144         
   1.145 -lemma height_node_bal_r:
   1.146 +lemma height_balR:
   1.147    "\<lbrakk> height r = height l + 2; avl l; avl r \<rbrakk> \<Longrightarrow>
   1.148 -   height (node_bal_r l a r) = height l + 2 \<or>
   1.149 -   height (node_bal_r l a r) = height l + 3"
   1.150 -by (cases r) (auto simp add:node_def node_bal_r_def split:tree.split)
   1.151 +   height (balR l a r) = height l + 2 \<or>
   1.152 +   height (balR l a r) = height l + 3"
   1.153 +by (cases r) (auto simp add:node_def balR_def split:tree.split)
   1.154  
   1.155  lemma [simp]: "height(node l a r) = max (height l) (height r) + 1"
   1.156  by (simp add: node_def)
   1.157 @@ -166,53 +164,53 @@
   1.158     \<rbrakk> \<Longrightarrow> avl(node l a r)"
   1.159  by (auto simp add:max_def node_def)
   1.160  
   1.161 -lemma height_node_bal_l2:
   1.162 +lemma height_balL2:
   1.163    "\<lbrakk> avl l; avl r; height l \<noteq> height r + 2 \<rbrakk> \<Longrightarrow>
   1.164 -   height (node_bal_l l a r) = (1 + max (height l) (height r))"
   1.165 -by (cases l, cases r) (simp_all add: node_bal_l_def)
   1.166 +   height (balL l a r) = (1 + max (height l) (height r))"
   1.167 +by (cases l, cases r) (simp_all add: balL_def)
   1.168  
   1.169 -lemma height_node_bal_r2:
   1.170 +lemma height_balR2:
   1.171    "\<lbrakk> avl l;  avl r;  height r \<noteq> height l + 2 \<rbrakk> \<Longrightarrow>
   1.172 -   height (node_bal_r l a r) = (1 + max (height l) (height r))"
   1.173 -by (cases l, cases r) (simp_all add: node_bal_r_def)
   1.174 +   height (balR l a r) = (1 + max (height l) (height r))"
   1.175 +by (cases l, cases r) (simp_all add: balR_def)
   1.176  
   1.177 -lemma avl_node_bal_l: 
   1.178 +lemma avl_balL: 
   1.179    assumes "avl l" "avl r" and "height l = height r \<or> height l = height r + 1
   1.180      \<or> height r = height l + 1 \<or> height l = height r + 2" 
   1.181 -  shows "avl(node_bal_l l a r)"
   1.182 +  shows "avl(balL l a r)"
   1.183  proof(cases l)
   1.184    case Leaf
   1.185 -  with assms show ?thesis by (simp add: node_def node_bal_l_def)
   1.186 +  with assms show ?thesis by (simp add: node_def balL_def)
   1.187  next
   1.188    case (Node ln ll lr lh)
   1.189    with assms show ?thesis
   1.190    proof(cases "height l = height r + 2")
   1.191      case True
   1.192      from True Node assms show ?thesis
   1.193 -      by (auto simp: node_bal_l_def intro!: avl_node split: tree.split) arith+
   1.194 +      by (auto simp: balL_def intro!: avl_node split: tree.split) arith+
   1.195    next
   1.196      case False
   1.197 -    with assms show ?thesis by (simp add: avl_node node_bal_l_def)
   1.198 +    with assms show ?thesis by (simp add: avl_node balL_def)
   1.199    qed
   1.200  qed
   1.201  
   1.202 -lemma avl_node_bal_r: 
   1.203 +lemma avl_balR: 
   1.204    assumes "avl l" and "avl r" and "height l = height r \<or> height l = height r + 1
   1.205      \<or> height r = height l + 1 \<or> height r = height l + 2" 
   1.206 -  shows "avl(node_bal_r l a r)"
   1.207 +  shows "avl(balR l a r)"
   1.208  proof(cases r)
   1.209    case Leaf
   1.210 -  with assms show ?thesis by (simp add: node_def node_bal_r_def)
   1.211 +  with assms show ?thesis by (simp add: node_def balR_def)
   1.212  next
   1.213    case (Node rn rl rr rh)
   1.214    with assms show ?thesis
   1.215    proof(cases "height r = height l + 2")
   1.216      case True
   1.217        from True Node assms show ?thesis
   1.218 -        by (auto simp: node_bal_r_def intro!: avl_node split: tree.split) arith+
   1.219 +        by (auto simp: balR_def intro!: avl_node split: tree.split) arith+
   1.220    next
   1.221      case False
   1.222 -    with assms show ?thesis by (simp add: node_bal_r_def avl_node)
   1.223 +    with assms show ?thesis by (simp add: balR_def avl_node)
   1.224    qed
   1.225  qed
   1.226  
   1.227 @@ -237,10 +235,10 @@
   1.228      with Node 1 show ?thesis 
   1.229      proof(cases "x<a")
   1.230        case True
   1.231 -      with Node 1 show ?thesis by (auto simp add:avl_node_bal_l)
   1.232 +      with Node 1 show ?thesis by (auto simp add:avl_balL)
   1.233      next
   1.234        case False
   1.235 -      with Node 1 `x\<noteq>a` show ?thesis by (auto simp add:avl_node_bal_r)
   1.236 +      with Node 1 `x\<noteq>a` show ?thesis by (auto simp add:avl_balR)
   1.237      qed
   1.238    qed
   1.239    case 2
   1.240 @@ -255,12 +253,12 @@
   1.241        case True
   1.242        with Node 2 show ?thesis
   1.243        proof(cases "height (insert x l) = height r + 2")
   1.244 -        case False with Node 2 `x < a` show ?thesis by (auto simp: height_node_bal_l2)
   1.245 +        case False with Node 2 `x < a` show ?thesis by (auto simp: height_balL2)
   1.246        next
   1.247          case True 
   1.248 -        hence "(height (node_bal_l (insert x l) a r) = height r + 2) \<or>
   1.249 -          (height (node_bal_l (insert x l) a r) = height r + 3)" (is "?A \<or> ?B")
   1.250 -          using Node 2 by (intro height_node_bal_l) simp_all
   1.251 +        hence "(height (balL (insert x l) a r) = height r + 2) \<or>
   1.252 +          (height (balL (insert x l) a r) = height r + 3)" (is "?A \<or> ?B")
   1.253 +          using Node 2 by (intro height_balL) simp_all
   1.254          thus ?thesis
   1.255          proof
   1.256            assume ?A
   1.257 @@ -275,12 +273,12 @@
   1.258        with Node 2 show ?thesis 
   1.259        proof(cases "height (insert x r) = height l + 2")
   1.260          case False
   1.261 -        with Node 2 `\<not>x < a` show ?thesis by (auto simp: height_node_bal_r2)
   1.262 +        with Node 2 `\<not>x < a` show ?thesis by (auto simp: height_balR2)
   1.263        next
   1.264          case True 
   1.265 -        hence "(height (node_bal_r l a (insert x r)) = height l + 2) \<or>
   1.266 -          (height (node_bal_r l a (insert x r)) = height l + 3)"  (is "?A \<or> ?B")
   1.267 -          using Node 2 by (intro height_node_bal_r) simp_all
   1.268 +        hence "(height (balR l a (insert x r)) = height l + 2) \<or>
   1.269 +          (height (balR l a (insert x r)) = height l + 3)"  (is "?A \<or> ?B")
   1.270 +          using Node 2 by (intro height_balR) simp_all
   1.271          thus ?thesis 
   1.272          proof
   1.273            assume ?A
   1.274 @@ -306,10 +304,10 @@
   1.275    case (Node h l a rh rl b rr)
   1.276    case 1
   1.277    with Node have "avl l" "avl (fst (delete_max (Node rh rl b rr)))" by auto
   1.278 -  with 1 Node have "avl (node_bal_l l a (fst (delete_max (Node rh rl b rr))))"
   1.279 -    by (intro avl_node_bal_l) fastforce+
   1.280 +  with 1 Node have "avl (balL l a (fst (delete_max (Node rh rl b rr))))"
   1.281 +    by (intro avl_balL) fastforce+
   1.282    thus ?case 
   1.283 -    by (auto simp: height_node_bal_l height_node_bal_l2
   1.284 +    by (auto simp: height_balL height_balL2
   1.285        linorder_class.max.absorb1 linorder_class.max.absorb2
   1.286        split:prod.split)
   1.287  next
   1.288 @@ -318,7 +316,7 @@
   1.289    let ?r = "Node rh rl b rr"
   1.290    let ?r' = "fst (delete_max ?r)"
   1.291    from `avl x` Node 2 have "avl l" and "avl ?r" by simp_all
   1.292 -  thus ?case using Node 2 height_node_bal_l[of l ?r' a] height_node_bal_l2[of l ?r' a]
   1.293 +  thus ?case using Node 2 height_balL[of l ?r' a] height_balL2[of l ?r' a]
   1.294      apply (auto split:prod.splits simp del:avl.simps) by arith+
   1.295  qed auto
   1.296  
   1.297 @@ -337,8 +335,8 @@
   1.298           height ?l = height(?l') + 1" by (rule avl_delete_max,simp)+
   1.299    with `avl t` Node_Node have "height ?l' = height ?r \<or> height ?l' = height ?r + 1
   1.300              \<or> height ?r = height ?l' + 1 \<or> height ?r = height ?l' + 2" by fastforce
   1.301 -  with `avl ?l'` `avl ?r` have "avl(node_bal_r ?l' (snd(delete_max ?l)) ?r)"
   1.302 -    by (rule avl_node_bal_r)
   1.303 +  with `avl ?l'` `avl ?r` have "avl(balR ?l' (snd(delete_max ?l)) ?r)"
   1.304 +    by (rule avl_balR)
   1.305    with Node_Node show ?thesis by (auto split:prod.splits)
   1.306  qed simp_all
   1.307  
   1.308 @@ -351,7 +349,7 @@
   1.309    let ?l = "Node lh ll ln lr"
   1.310    let ?r = "Node rh rl rn rr"
   1.311    let ?l' = "fst (delete_max ?l)"
   1.312 -  let ?t' = "node_bal_r ?l' (snd(delete_max ?l)) ?r"
   1.313 +  let ?t' = "balR ?l' (snd(delete_max ?l)) ?r"
   1.314    from `avl t` and Node_Node have "avl ?r" by simp
   1.315    from `avl t` and Node_Node have "avl ?l" by simp
   1.316    hence "avl(?l')"  by (rule avl_delete_max,simp)
   1.317 @@ -360,11 +358,11 @@
   1.318    have "height t = height ?t' \<or> height t = height ?t' + 1" using  `avl t` Node_Node
   1.319    proof(cases "height ?r = height ?l' + 2")
   1.320      case False
   1.321 -    show ?thesis using l'_height t_height False by (subst  height_node_bal_r2[OF `avl ?l'` `avl ?r` False])+ arith
   1.322 +    show ?thesis using l'_height t_height False by (subst  height_balR2[OF `avl ?l'` `avl ?r` False])+ arith
   1.323    next
   1.324      case True
   1.325      show ?thesis
   1.326 -    proof(cases rule: disjE[OF height_node_bal_r[OF True `avl ?l'` `avl ?r`, of "snd (delete_max ?l)"]])
   1.327 +    proof(cases rule: disjE[OF height_balR[OF True `avl ?l'` `avl ?r`, of "snd (delete_max ?l)"]])
   1.328        case 1
   1.329        thus ?thesis using l'_height t_height True by arith
   1.330      next
   1.331 @@ -393,10 +391,10 @@
   1.332      with Node 1 show ?thesis 
   1.333      proof(cases "x<n")
   1.334        case True
   1.335 -      with Node 1 show ?thesis by (auto simp add:avl_node_bal_r)
   1.336 +      with Node 1 show ?thesis by (auto simp add:avl_balR)
   1.337      next
   1.338        case False
   1.339 -      with Node 1 `x\<noteq>n` show ?thesis by (auto simp add:avl_node_bal_l)
   1.340 +      with Node 1 `x\<noteq>n` show ?thesis by (auto simp add:avl_balL)
   1.341      qed
   1.342    qed
   1.343    case 2
   1.344 @@ -414,38 +412,38 @@
   1.345        case True
   1.346        show ?thesis
   1.347        proof(cases "height r = height (delete x l) + 2")
   1.348 -        case False with Node 1 `x < n` show ?thesis by(auto simp: node_bal_r_def)
   1.349 +        case False with Node 1 `x < n` show ?thesis by(auto simp: balR_def)
   1.350        next
   1.351          case True 
   1.352 -        hence "(height (node_bal_r (delete x l) n r) = height (delete x l) + 2) \<or>
   1.353 -          height (node_bal_r (delete x l) n r) = height (delete x l) + 3" (is "?A \<or> ?B")
   1.354 -          using Node 2 by (intro height_node_bal_r) auto
   1.355 +        hence "(height (balR (delete x l) n r) = height (delete x l) + 2) \<or>
   1.356 +          height (balR (delete x l) n r) = height (delete x l) + 3" (is "?A \<or> ?B")
   1.357 +          using Node 2 by (intro height_balR) auto
   1.358          thus ?thesis 
   1.359          proof
   1.360            assume ?A
   1.361 -          with `x < n` Node 2 show ?thesis by(auto simp: node_bal_r_def)
   1.362 +          with `x < n` Node 2 show ?thesis by(auto simp: balR_def)
   1.363          next
   1.364            assume ?B
   1.365 -          with `x < n` Node 2 show ?thesis by(auto simp: node_bal_r_def)
   1.366 +          with `x < n` Node 2 show ?thesis by(auto simp: balR_def)
   1.367          qed
   1.368        qed
   1.369      next
   1.370        case False
   1.371        show ?thesis
   1.372        proof(cases "height l = height (delete x r) + 2")
   1.373 -        case False with Node 1 `\<not>x < n` `x \<noteq> n` show ?thesis by(auto simp: node_bal_l_def)
   1.374 +        case False with Node 1 `\<not>x < n` `x \<noteq> n` show ?thesis by(auto simp: balL_def)
   1.375        next
   1.376          case True 
   1.377 -        hence "(height (node_bal_l l n (delete x r)) = height (delete x r) + 2) \<or>
   1.378 -          height (node_bal_l l n (delete x r)) = height (delete x r) + 3" (is "?A \<or> ?B")
   1.379 -          using Node 2 by (intro height_node_bal_l) auto
   1.380 +        hence "(height (balL l n (delete x r)) = height (delete x r) + 2) \<or>
   1.381 +          height (balL l n (delete x r)) = height (delete x r) + 3" (is "?A \<or> ?B")
   1.382 +          using Node 2 by (intro height_balL) auto
   1.383          thus ?thesis 
   1.384          proof
   1.385            assume ?A
   1.386 -          with `\<not>x < n` `x \<noteq> n` Node 2 show ?thesis by(auto simp: node_bal_l_def)
   1.387 +          with `\<not>x < n` `x \<noteq> n` Node 2 show ?thesis by(auto simp: balL_def)
   1.388          next
   1.389            assume ?B
   1.390 -          with `\<not>x < n` `x \<noteq> n` Node 2 show ?thesis by(auto simp: node_bal_l_def)
   1.391 +          with `\<not>x < n` `x \<noteq> n` Node 2 show ?thesis by(auto simp: balL_def)
   1.392          qed
   1.393        qed
   1.394      qed