added AVL and lookup function
authornipkow
Wed Sep 23 09:47:04 2015 +0200 (2015-09-23)
changeset 61232c46faf9762f7
parent 61231 cc6969542f8d
child 61237 5c9a9504f713
added AVL and lookup function
src/HOL/Data_Structures/AVL_Map.thy
src/HOL/Data_Structures/AVL_Set.thy
src/HOL/Data_Structures/Lookup2.thy
src/HOL/ROOT
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Data_Structures/AVL_Map.thy	Wed Sep 23 09:47:04 2015 +0200
     1.3 @@ -0,0 +1,54 @@
     1.4 +(* Author: Tobias Nipkow *)
     1.5 +
     1.6 +section "AVL Tree Implementation of Maps"
     1.7 +
     1.8 +theory AVL_Map
     1.9 +imports
    1.10 +  AVL_Set
    1.11 +  Lookup2
    1.12 +begin
    1.13 +
    1.14 +fun update :: "'a::order \<Rightarrow> 'b \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
    1.15 +"update x y Leaf = Node 1 Leaf (x,y) Leaf" |
    1.16 +"update x y (Node h l (a,b) r) = 
    1.17 +   (if x = a then Node h l (x,y) r else
    1.18 +    if x < a then node_bal_l (update x y l) (a,b) r
    1.19 +    else node_bal_r l (a,b) (update x y r))"
    1.20 +
    1.21 +fun delete :: "'a::order \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
    1.22 +"delete _ Leaf = Leaf" |
    1.23 +"delete x (Node h l (a,b) r) = (
    1.24 +   if x = a then delete_root (Node h l (a,b) r) else
    1.25 +   if x < a then node_bal_r (delete x l) (a,b) r
    1.26 +   else node_bal_l l (a,b) (delete x r))"
    1.27 +
    1.28 +
    1.29 +subsection {* Functional Correctness Proofs *}
    1.30 +
    1.31 +theorem inorder_update:
    1.32 +  "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
    1.33 +by (induct t) 
    1.34 +   (auto simp: upd_list_simps inorder_node_bal_l inorder_node_bal_r)
    1.35 +
    1.36 +
    1.37 +theorem inorder_delete:
    1.38 +  "sorted1(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
    1.39 +by(induction t)
    1.40 +  (auto simp: del_list_simps inorder_node_bal_l inorder_node_bal_r
    1.41 +     inorder_delete_root inorder_delete_maxD split: prod.splits)
    1.42 +
    1.43 +
    1.44 +interpretation Map_by_Ordered
    1.45 +where empty = Leaf and lookup = lookup and update = update and delete = delete
    1.46 +and inorder = inorder and wf = "\<lambda>_. True"
    1.47 +proof (standard, goal_cases)
    1.48 +  case 1 show ?case by simp
    1.49 +next
    1.50 +  case 2 thus ?case by(simp add: lookup_eq)
    1.51 +next
    1.52 +  case 3 thus ?case by(simp add: inorder_update)
    1.53 +next
    1.54 +  case 4 thus ?case by(simp add: inorder_delete)
    1.55 +qed (rule TrueI)+
    1.56 +
    1.57 +end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Data_Structures/AVL_Set.thy	Wed Sep 23 09:47:04 2015 +0200
     2.3 @@ -0,0 +1,457 @@
     2.4 +(*
     2.5 +Author:     Tobias Nipkow
     2.6 +Derived from AFP entry AVL.
     2.7 +*)
     2.8 +
     2.9 +section "AVL Tree Implementation of Sets"
    2.10 +
    2.11 +theory AVL_Set
    2.12 +imports Isin2
    2.13 +begin
    2.14 +
    2.15 +type_synonym 'a avl_tree = "('a,nat) tree"
    2.16 +
    2.17 +text {* Invariant: *}
    2.18 +
    2.19 +fun avl :: "'a avl_tree \<Rightarrow> bool" where
    2.20 +"avl Leaf = True" |
    2.21 +"avl (Node h l a r) =
    2.22 + ((height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1) \<and> 
    2.23 +  h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
    2.24 +
    2.25 +fun ht :: "'a avl_tree \<Rightarrow> nat" where
    2.26 +"ht Leaf = 0" |
    2.27 +"ht (Node h l a r) = h"
    2.28 +
    2.29 +definition node :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    2.30 +"node l a r = Node (max (ht l) (ht r) + 1) l a r"
    2.31 +
    2.32 +definition node_bal_l :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    2.33 +"node_bal_l l a r = (
    2.34 +  if ht l = ht r + 2 then (case l of 
    2.35 +    Node _ bl b br \<Rightarrow> (if ht bl < ht br
    2.36 +    then case br of
    2.37 +      Node _ cl c cr \<Rightarrow> node (node bl b cl) c (node cr a r)
    2.38 +    else node bl b (node br a r)))
    2.39 +  else node l a r)"
    2.40 +
    2.41 +definition node_bal_r :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    2.42 +"node_bal_r l a r = (
    2.43 +  if ht r = ht l + 2 then (case r of
    2.44 +    Node _ bl b br \<Rightarrow> (if ht bl > ht br
    2.45 +    then case bl of
    2.46 +      Node _ cl c cr \<Rightarrow> node (node l a cl) c (node cr b br)
    2.47 +    else node (node l a bl) b br))
    2.48 +  else node l a r)"
    2.49 +
    2.50 +fun insert :: "'a::order \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    2.51 +"insert x Leaf = Node 1 Leaf x Leaf" |
    2.52 +"insert x (Node h l a r) = 
    2.53 +   (if x=a then Node h l a r
    2.54 +    else if x<a
    2.55 +      then node_bal_l (insert x l) a r
    2.56 +      else node_bal_r l a (insert x r))"
    2.57 +
    2.58 +fun delete_max :: "'a avl_tree \<Rightarrow> 'a avl_tree * 'a" where
    2.59 +"delete_max (Node _ l a Leaf) = (l,a)" |
    2.60 +"delete_max (Node _ l a r) = (
    2.61 +  let (r',a') = delete_max r in
    2.62 +  (node_bal_l l a r', a'))"
    2.63 +
    2.64 +lemmas delete_max_induct = delete_max.induct[case_names Leaf Node]
    2.65 +
    2.66 +fun delete_root :: "'a avl_tree \<Rightarrow> 'a avl_tree" where
    2.67 +"delete_root (Node h Leaf a r) = r" |
    2.68 +"delete_root (Node h l a Leaf) = l" |
    2.69 +"delete_root (Node h l a r) =
    2.70 +  (let (l', a') = delete_max l in node_bal_r l' a' r)"
    2.71 +
    2.72 +lemmas delete_root_cases = delete_root.cases[case_names Leaf_t Node_Leaf Node_Node]
    2.73 +
    2.74 +fun delete :: "'a::order \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    2.75 +"delete _ Leaf = Leaf" |
    2.76 +"delete x (Node h l a r) = (
    2.77 +   if x = a then delete_root (Node h l a r)
    2.78 +   else if x < a then node_bal_r (delete x l) a r
    2.79 +   else node_bal_l l a (delete x r))"
    2.80 +
    2.81 +
    2.82 +subsection {* Functional Correctness Proofs *}
    2.83 +
    2.84 +text{* Very different from the AFP/AVL proofs *}
    2.85 +
    2.86 +
    2.87 +subsubsection "Proofs for insert"
    2.88 +
    2.89 +lemma inorder_node_bal_l:
    2.90 +  "inorder (node_bal_l l a r) = inorder l @ a # inorder r"
    2.91 +by (auto simp: node_def node_bal_l_def split:tree.splits)
    2.92 +
    2.93 +lemma inorder_node_bal_r:
    2.94 +  "inorder (node_bal_r l a r) = inorder l @ a # inorder r"
    2.95 +by (auto simp: node_def node_bal_r_def split:tree.splits)
    2.96 +
    2.97 +theorem inorder_insert:
    2.98 +  "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
    2.99 +by (induct t) 
   2.100 +   (auto simp: ins_list_simps inorder_node_bal_l inorder_node_bal_r)
   2.101 +
   2.102 +
   2.103 +subsubsection "Proofs for delete"
   2.104 +
   2.105 +lemma inorder_delete_maxD:
   2.106 +  "\<lbrakk> delete_max t = (t',a); t \<noteq> Leaf \<rbrakk> \<Longrightarrow>
   2.107 +   inorder t' @ [a] = inorder t"
   2.108 +by(induction t arbitrary: t' rule: delete_max.induct)
   2.109 +  (auto simp: inorder_node_bal_l split: prod.splits tree.split)
   2.110 +
   2.111 +lemma inorder_delete_root:
   2.112 +  "inorder (delete_root (Node h l a r)) = inorder l @ inorder r"
   2.113 +by(induction "Node h l a r" arbitrary: l a r h rule: delete_root.induct)
   2.114 +  (auto simp: inorder_node_bal_r inorder_delete_maxD split: prod.splits)
   2.115 +
   2.116 +theorem inorder_delete:
   2.117 +  "sorted(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
   2.118 +by(induction t)
   2.119 +  (auto simp: del_list_simps inorder_node_bal_l inorder_node_bal_r
   2.120 +    inorder_delete_root inorder_delete_maxD split: prod.splits)
   2.121 +
   2.122 +
   2.123 +subsubsection "Overall functional correctness"
   2.124 +
   2.125 +interpretation Set_by_Ordered
   2.126 +where empty = Leaf and isin = isin and insert = insert and delete = delete
   2.127 +and inorder = inorder and wf = "\<lambda>_. True"
   2.128 +proof (standard, goal_cases)
   2.129 +  case 1 show ?case by simp
   2.130 +next
   2.131 +  case 2 thus ?case by(simp add: isin_set)
   2.132 +next
   2.133 +  case 3 thus ?case by(simp add: inorder_insert)
   2.134 +next
   2.135 +  case 4 thus ?case by(simp add: inorder_delete)
   2.136 +next
   2.137 +  case 5 thus ?case ..
   2.138 +qed
   2.139 +
   2.140 +
   2.141 +subsection {* AVL invariants *}
   2.142 +
   2.143 +text{* Essentially the AFP/AVL proofs *}
   2.144 +
   2.145 +
   2.146 +subsubsection {* Insertion maintains AVL balance *}
   2.147 +
   2.148 +declare Let_def [simp]
   2.149 +
   2.150 +lemma [simp]: "avl t \<Longrightarrow> ht t = height t"
   2.151 +by (induct t) simp_all
   2.152 +
   2.153 +lemma height_node_bal_l:
   2.154 +  "\<lbrakk> height l = height r + 2; avl l; avl r \<rbrakk> \<Longrightarrow>
   2.155 +   height (node_bal_l l a r) = height r + 2 \<or>
   2.156 +   height (node_bal_l l a r) = height r + 3"
   2.157 +by (cases l) (auto simp:node_def node_bal_l_def split:tree.split)
   2.158 +       
   2.159 +lemma height_node_bal_r:
   2.160 +  "\<lbrakk> height r = height l + 2; avl l; avl r \<rbrakk> \<Longrightarrow>
   2.161 +   height (node_bal_r l a r) = height l + 2 \<or>
   2.162 +   height (node_bal_r l a r) = height l + 3"
   2.163 +by (cases r) (auto simp add:node_def node_bal_r_def split:tree.split)
   2.164 +
   2.165 +lemma [simp]: "height(node l a r) = max (height l) (height r) + 1"
   2.166 +by (simp add: node_def)
   2.167 +
   2.168 +lemma avl_node:
   2.169 +  "\<lbrakk> avl l; avl r;
   2.170 +     height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1
   2.171 +   \<rbrakk> \<Longrightarrow> avl(node l a r)"
   2.172 +by (auto simp add:max_def node_def)
   2.173 +
   2.174 +lemma height_node_bal_l2:
   2.175 +  "\<lbrakk> avl l; avl r; height l \<noteq> height r + 2 \<rbrakk> \<Longrightarrow>
   2.176 +   height (node_bal_l l a r) = (1 + max (height l) (height r))"
   2.177 +by (cases l, cases r) (simp_all add: node_bal_l_def)
   2.178 +
   2.179 +lemma height_node_bal_r2:
   2.180 +  "\<lbrakk> avl l;  avl r;  height r \<noteq> height l + 2 \<rbrakk> \<Longrightarrow>
   2.181 +   height (node_bal_r l a r) = (1 + max (height l) (height r))"
   2.182 +by (cases l, cases r) (simp_all add: node_bal_r_def)
   2.183 +
   2.184 +lemma avl_node_bal_l: 
   2.185 +  assumes "avl l" "avl r" and "height l = height r \<or> height l = height r + 1
   2.186 +    \<or> height r = height l + 1 \<or> height l = height r + 2" 
   2.187 +  shows "avl(node_bal_l l a r)"
   2.188 +proof(cases l)
   2.189 +  case Leaf
   2.190 +  with assms show ?thesis by (simp add: node_def node_bal_l_def)
   2.191 +next
   2.192 +  case (Node ln ll lr lh)
   2.193 +  with assms show ?thesis
   2.194 +  proof(cases "height l = height r + 2")
   2.195 +    case True
   2.196 +    from True Node assms show ?thesis
   2.197 +      by (auto simp: node_bal_l_def intro!: avl_node split: tree.split) arith+
   2.198 +  next
   2.199 +    case False
   2.200 +    with assms show ?thesis by (simp add: avl_node node_bal_l_def)
   2.201 +  qed
   2.202 +qed
   2.203 +
   2.204 +lemma avl_node_bal_r: 
   2.205 +  assumes "avl l" and "avl r" and "height l = height r \<or> height l = height r + 1
   2.206 +    \<or> height r = height l + 1 \<or> height r = height l + 2" 
   2.207 +  shows "avl(node_bal_r l a r)"
   2.208 +proof(cases r)
   2.209 +  case Leaf
   2.210 +  with assms show ?thesis by (simp add: node_def node_bal_r_def)
   2.211 +next
   2.212 +  case (Node rn rl rr rh)
   2.213 +  with assms show ?thesis
   2.214 +  proof(cases "height r = height l + 2")
   2.215 +    case True
   2.216 +      from True Node assms show ?thesis
   2.217 +        by (auto simp: node_bal_r_def intro!: avl_node split: tree.split) arith+
   2.218 +  next
   2.219 +    case False
   2.220 +    with assms show ?thesis by (simp add: node_bal_r_def avl_node)
   2.221 +  qed
   2.222 +qed
   2.223 +
   2.224 +(* It appears that these two properties need to be proved simultaneously: *)
   2.225 +
   2.226 +text{* Insertion maintains the AVL property: *}
   2.227 +
   2.228 +theorem avl_insert_aux:
   2.229 +  assumes "avl t"
   2.230 +  shows "avl(insert x t)"
   2.231 +        "(height (insert x t) = height t \<or> height (insert x t) = height t + 1)"
   2.232 +using assms
   2.233 +proof (induction t)
   2.234 +  case (Node h l a r)
   2.235 +  case 1
   2.236 +  with Node show ?case
   2.237 +  proof(cases "x = a")
   2.238 +    case True
   2.239 +    with Node 1 show ?thesis by simp
   2.240 +  next
   2.241 +    case False
   2.242 +    with Node 1 show ?thesis 
   2.243 +    proof(cases "x<a")
   2.244 +      case True
   2.245 +      with Node 1 show ?thesis by (auto simp add:avl_node_bal_l)
   2.246 +    next
   2.247 +      case False
   2.248 +      with Node 1 `x\<noteq>a` show ?thesis by (auto simp add:avl_node_bal_r)
   2.249 +    qed
   2.250 +  qed
   2.251 +  case 2
   2.252 +  from 2 Node show ?case
   2.253 +  proof(cases "x = a")
   2.254 +    case True
   2.255 +    with Node 1 show ?thesis by simp
   2.256 +  next
   2.257 +    case False
   2.258 +    with Node 1 show ?thesis 
   2.259 +     proof(cases "x<a")
   2.260 +      case True
   2.261 +      with Node 2 show ?thesis
   2.262 +      proof(cases "height (insert x l) = height r + 2")
   2.263 +        case False with Node 2 `x < a` show ?thesis by (auto simp: height_node_bal_l2)
   2.264 +      next
   2.265 +        case True 
   2.266 +        hence "(height (node_bal_l (insert x l) a r) = height r + 2) \<or>
   2.267 +          (height (node_bal_l (insert x l) a r) = height r + 3)" (is "?A \<or> ?B")
   2.268 +          using Node 2 by (intro height_node_bal_l) simp_all
   2.269 +        thus ?thesis
   2.270 +        proof
   2.271 +          assume ?A
   2.272 +          with 2 `x < a` show ?thesis by (auto)
   2.273 +        next
   2.274 +          assume ?B
   2.275 +          with True 1 Node(2) `x < a` show ?thesis by (simp) arith
   2.276 +        qed
   2.277 +      qed
   2.278 +    next
   2.279 +      case False
   2.280 +      with Node 2 show ?thesis 
   2.281 +      proof(cases "height (insert x r) = height l + 2")
   2.282 +        case False
   2.283 +        with Node 2 `\<not>x < a` show ?thesis by (auto simp: height_node_bal_r2)
   2.284 +      next
   2.285 +        case True 
   2.286 +        hence "(height (node_bal_r l a (insert x r)) = height l + 2) \<or>
   2.287 +          (height (node_bal_r l a (insert x r)) = height l + 3)"  (is "?A \<or> ?B")
   2.288 +          using Node 2 by (intro height_node_bal_r) simp_all
   2.289 +        thus ?thesis 
   2.290 +        proof
   2.291 +          assume ?A
   2.292 +          with 2 `\<not>x < a` show ?thesis by (auto)
   2.293 +        next
   2.294 +          assume ?B
   2.295 +          with True 1 Node(4) `\<not>x < a` show ?thesis by (simp) arith
   2.296 +        qed
   2.297 +      qed
   2.298 +    qed
   2.299 +  qed
   2.300 +qed simp_all
   2.301 +
   2.302 +
   2.303 +subsubsection {* Deletion maintains AVL balance *}
   2.304 +
   2.305 +lemma avl_delete_max:
   2.306 +  assumes "avl x" and "x \<noteq> Leaf"
   2.307 +  shows "avl (fst (delete_max x))" "height x = height(fst (delete_max x)) \<or>
   2.308 +         height x = height(fst (delete_max x)) + 1"
   2.309 +using assms
   2.310 +proof (induct x rule: delete_max_induct)
   2.311 +  case (Node h l a rh rl b rr)
   2.312 +  case 1
   2.313 +  with Node have "avl l" "avl (fst (delete_max (Node rh rl b rr)))" by auto
   2.314 +  with 1 Node have "avl (node_bal_l l a (fst (delete_max (Node rh rl b rr))))"
   2.315 +    by (intro avl_node_bal_l) fastforce+
   2.316 +  thus ?case 
   2.317 +    by (auto simp: height_node_bal_l height_node_bal_l2
   2.318 +      linorder_class.max.absorb1 linorder_class.max.absorb2
   2.319 +      split:prod.split)
   2.320 +next
   2.321 +  case (Node h l a rh rl b rr)
   2.322 +  case 2
   2.323 +  let ?r = "Node rh rl b rr"
   2.324 +  let ?r' = "fst (delete_max ?r)"
   2.325 +  from `avl x` Node 2 have "avl l" and "avl ?r" by simp_all
   2.326 +  thus ?case using Node 2 height_node_bal_l[of l ?r' a] height_node_bal_l2[of l ?r' a]
   2.327 +    apply (auto split:prod.splits simp del:avl.simps) by arith+
   2.328 +qed auto
   2.329 +
   2.330 +lemma avl_delete_root:
   2.331 +  assumes "avl t" and "t \<noteq> Leaf"
   2.332 +  shows "avl(delete_root t)" 
   2.333 +using assms
   2.334 +proof (cases t rule:delete_root_cases)
   2.335 +  case (Node_Node h lh ll ln lr n rh rl rn rr)
   2.336 +  let ?l = "Node lh ll ln lr"
   2.337 +  let ?r = "Node rh rl rn rr"
   2.338 +  let ?l' = "fst (delete_max ?l)"
   2.339 +  from `avl t` and Node_Node have "avl ?r" by simp
   2.340 +  from `avl t` and Node_Node have "avl ?l" by simp
   2.341 +  hence "avl(?l')" "height ?l = height(?l') \<or>
   2.342 +         height ?l = height(?l') + 1" by (rule avl_delete_max,simp)+
   2.343 +  with `avl t` Node_Node have "height ?l' = height ?r \<or> height ?l' = height ?r + 1
   2.344 +            \<or> height ?r = height ?l' + 1 \<or> height ?r = height ?l' + 2" by fastforce
   2.345 +  with `avl ?l'` `avl ?r` have "avl(node_bal_r ?l' (snd(delete_max ?l)) ?r)"
   2.346 +    by (rule avl_node_bal_r)
   2.347 +  with Node_Node show ?thesis by (auto split:prod.splits)
   2.348 +qed simp_all
   2.349 +
   2.350 +lemma height_delete_root:
   2.351 +  assumes "avl t" and "t \<noteq> Leaf" 
   2.352 +  shows "height t = height(delete_root t) \<or> height t = height(delete_root t) + 1"
   2.353 +using assms
   2.354 +proof (cases t rule: delete_root_cases)
   2.355 +  case (Node_Node h lh ll ln lr n rh rl rn rr)
   2.356 +  let ?l = "Node lh ll ln lr"
   2.357 +  let ?r = "Node rh rl rn rr"
   2.358 +  let ?l' = "fst (delete_max ?l)"
   2.359 +  let ?t' = "node_bal_r ?l' (snd(delete_max ?l)) ?r"
   2.360 +  from `avl t` and Node_Node have "avl ?r" by simp
   2.361 +  from `avl t` and Node_Node have "avl ?l" by simp
   2.362 +  hence "avl(?l')"  by (rule avl_delete_max,simp)
   2.363 +  have l'_height: "height ?l = height ?l' \<or> height ?l = height ?l' + 1" using `avl ?l` by (intro avl_delete_max) auto
   2.364 +  have t_height: "height t = 1 + max (height ?l) (height ?r)" using `avl t` Node_Node by simp
   2.365 +  have "height t = height ?t' \<or> height t = height ?t' + 1" using  `avl t` Node_Node
   2.366 +  proof(cases "height ?r = height ?l' + 2")
   2.367 +    case False
   2.368 +    show ?thesis using l'_height t_height False by (subst  height_node_bal_r2[OF `avl ?l'` `avl ?r` False])+ arith
   2.369 +  next
   2.370 +    case True
   2.371 +    show ?thesis
   2.372 +    proof(cases rule: disjE[OF height_node_bal_r[OF True `avl ?l'` `avl ?r`, of "snd (delete_max ?l)"]])
   2.373 +      case 1
   2.374 +      thus ?thesis using l'_height t_height True by arith
   2.375 +    next
   2.376 +      case 2
   2.377 +      thus ?thesis using l'_height t_height True by arith
   2.378 +    qed
   2.379 +  qed
   2.380 +  thus ?thesis using Node_Node by (auto split:prod.splits)
   2.381 +qed simp_all
   2.382 +
   2.383 +text{* Deletion maintains the AVL property: *}
   2.384 +
   2.385 +theorem avl_delete_aux:
   2.386 +  assumes "avl t" 
   2.387 +  shows "avl(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1"
   2.388 +using assms
   2.389 +proof (induct t)
   2.390 +  case (Node h l n r)
   2.391 +  case 1
   2.392 +  with Node show ?case
   2.393 +  proof(cases "x = n")
   2.394 +    case True
   2.395 +    with Node 1 show ?thesis by (auto simp:avl_delete_root)
   2.396 +  next
   2.397 +    case False
   2.398 +    with Node 1 show ?thesis 
   2.399 +    proof(cases "x<n")
   2.400 +      case True
   2.401 +      with Node 1 show ?thesis by (auto simp add:avl_node_bal_r)
   2.402 +    next
   2.403 +      case False
   2.404 +      with Node 1 `x\<noteq>n` show ?thesis by (auto simp add:avl_node_bal_l)
   2.405 +    qed
   2.406 +  qed
   2.407 +  case 2
   2.408 +  with Node show ?case
   2.409 +  proof(cases "x = n")
   2.410 +    case True
   2.411 +    with 1 have "height (Node h l n r) = height(delete_root (Node h l n r))
   2.412 +      \<or> height (Node h l n r) = height(delete_root (Node h l n r)) + 1"
   2.413 +      by (subst height_delete_root,simp_all)
   2.414 +    with True show ?thesis by simp
   2.415 +  next
   2.416 +    case False
   2.417 +    with Node 1 show ?thesis 
   2.418 +     proof(cases "x<n")
   2.419 +      case True
   2.420 +      show ?thesis
   2.421 +      proof(cases "height r = height (delete x l) + 2")
   2.422 +        case False with Node 1 `x < n` show ?thesis by(auto simp: node_bal_r_def)
   2.423 +      next
   2.424 +        case True 
   2.425 +        hence "(height (node_bal_r (delete x l) n r) = height (delete x l) + 2) \<or>
   2.426 +          height (node_bal_r (delete x l) n r) = height (delete x l) + 3" (is "?A \<or> ?B")
   2.427 +          using Node 2 by (intro height_node_bal_r) auto
   2.428 +        thus ?thesis 
   2.429 +        proof
   2.430 +          assume ?A
   2.431 +          with `x < n` Node 2 show ?thesis by(auto simp: node_bal_r_def)
   2.432 +        next
   2.433 +          assume ?B
   2.434 +          with `x < n` Node 2 show ?thesis by(auto simp: node_bal_r_def)
   2.435 +        qed
   2.436 +      qed
   2.437 +    next
   2.438 +      case False
   2.439 +      show ?thesis
   2.440 +      proof(cases "height l = height (delete x r) + 2")
   2.441 +        case False with Node 1 `\<not>x < n` `x \<noteq> n` show ?thesis by(auto simp: node_bal_l_def)
   2.442 +      next
   2.443 +        case True 
   2.444 +        hence "(height (node_bal_l l n (delete x r)) = height (delete x r) + 2) \<or>
   2.445 +          height (node_bal_l l n (delete x r)) = height (delete x r) + 3" (is "?A \<or> ?B")
   2.446 +          using Node 2 by (intro height_node_bal_l) auto
   2.447 +        thus ?thesis 
   2.448 +        proof
   2.449 +          assume ?A
   2.450 +          with `\<not>x < n` `x \<noteq> n` Node 2 show ?thesis by(auto simp: node_bal_l_def)
   2.451 +        next
   2.452 +          assume ?B
   2.453 +          with `\<not>x < n` `x \<noteq> n` Node 2 show ?thesis by(auto simp: node_bal_l_def)
   2.454 +        qed
   2.455 +      qed
   2.456 +    qed
   2.457 +  qed
   2.458 +qed simp_all
   2.459 +
   2.460 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Data_Structures/Lookup2.thy	Wed Sep 23 09:47:04 2015 +0200
     3.3 @@ -0,0 +1,21 @@
     3.4 +(* Author: Tobias Nipkow *)
     3.5 +
     3.6 +section \<open>Function \textit{lookup} for Tree2\<close>
     3.7 +
     3.8 +theory Lookup2
     3.9 +imports
    3.10 +  Tree2
    3.11 +  Map_by_Ordered
    3.12 +begin
    3.13 +
    3.14 +fun lookup :: "('a::linorder * 'b, 'c) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
    3.15 +"lookup Leaf x = None" |
    3.16 +"lookup (Node _ l (a,b) r) x =
    3.17 +  (if x < a then lookup l x else
    3.18 +   if x > a then lookup r x else Some b)"
    3.19 +
    3.20 +lemma lookup_eq:
    3.21 +  "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
    3.22 +by(induction t) (auto simp: map_of_simps split: option.split)
    3.23 +
    3.24 +end
    3.25 \ No newline at end of file
     4.1 --- a/src/HOL/ROOT	Wed Sep 23 09:14:22 2015 +0200
     4.2 +++ b/src/HOL/ROOT	Wed Sep 23 09:47:04 2015 +0200
     4.3 @@ -176,6 +176,7 @@
     4.4    theories
     4.5      Tree_Set
     4.6      Tree_Map
     4.7 +    AVL_Map
     4.8      RBT_Map
     4.9    document_files "root.tex" "root.bib"
    4.10