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.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
```