src/HOL/Data_Structures/AVL_Set.thy
changeset 68413 b56ed5010e69
parent 68342 b80734daf7ed
child 68422 0a3a36fa1d63
     1.1 --- a/src/HOL/Data_Structures/AVL_Set.thy	Mon Jun 11 08:15:43 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/AVL_Set.thy	Mon Jun 11 16:29:27 2018 +0200
     1.3 @@ -18,25 +18,25 @@
     1.4  
     1.5  fun avl :: "'a avl_tree \<Rightarrow> bool" where
     1.6  "avl Leaf = True" |
     1.7 -"avl (Node h l a r) =
     1.8 +"avl (Node l a h r) =
     1.9   ((height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1) \<and> 
    1.10    h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
    1.11  
    1.12  fun ht :: "'a avl_tree \<Rightarrow> nat" where
    1.13  "ht Leaf = 0" |
    1.14 -"ht (Node h l a r) = h"
    1.15 +"ht (Node l a h r) = h"
    1.16  
    1.17  definition node :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.18 -"node l a r = Node (max (ht l) (ht r) + 1) l a r"
    1.19 +"node l a r = Node l a (max (ht l) (ht r) + 1) r"
    1.20  
    1.21  definition balL :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.22  "balL l a r =
    1.23    (if ht l = ht r + 2 then
    1.24       case l of 
    1.25 -       Node _ bl b br \<Rightarrow>
    1.26 +       Node bl b _ br \<Rightarrow>
    1.27           if ht bl < ht br then
    1.28             case br of
    1.29 -             Node _ cl c cr \<Rightarrow> node (node bl b cl) c (node cr a r)
    1.30 +             Node cl c _ cr \<Rightarrow> node (node bl b cl) c (node cr a r)
    1.31           else node bl b (node br a r)
    1.32     else node l a r)"
    1.33  
    1.34 @@ -44,38 +44,38 @@
    1.35  "balR l a r =
    1.36     (if ht r = ht l + 2 then
    1.37        case r of
    1.38 -        Node _ bl b br \<Rightarrow>
    1.39 +        Node bl b _ br \<Rightarrow>
    1.40            if ht bl > ht br then
    1.41              case bl of
    1.42 -              Node _ cl c cr \<Rightarrow> node (node l a cl) c (node cr b br)
    1.43 +              Node cl c _ cr \<Rightarrow> node (node l a cl) c (node cr b br)
    1.44            else node (node l a bl) b br
    1.45    else node l a r)"
    1.46  
    1.47  fun insert :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.48 -"insert x Leaf = Node 1 Leaf x Leaf" |
    1.49 -"insert x (Node h l a r) = (case cmp x a of
    1.50 -   EQ \<Rightarrow> Node h l a r |
    1.51 +"insert x Leaf = Node Leaf x 1 Leaf" |
    1.52 +"insert x (Node l a h r) = (case cmp x a of
    1.53 +   EQ \<Rightarrow> Node l a h r |
    1.54     LT \<Rightarrow> balL (insert x l) a r |
    1.55     GT \<Rightarrow> balR l a (insert x r))"
    1.56  
    1.57  fun split_max :: "'a avl_tree \<Rightarrow> 'a avl_tree * 'a" where
    1.58 -"split_max (Node _ l a r) =
    1.59 +"split_max (Node l a _ r) =
    1.60    (if r = Leaf then (l,a) else let (r',a') = split_max r in (balL l a r', a'))"
    1.61  
    1.62  lemmas split_max_induct = split_max.induct[case_names Node Leaf]
    1.63  
    1.64  fun del_root :: "'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.65 -"del_root (Node h Leaf a r) = r" |
    1.66 -"del_root (Node h l a Leaf) = l" |
    1.67 -"del_root (Node h l a r) = (let (l', a') = split_max l in balR l' a' r)"
    1.68 +"del_root (Node Leaf a h r) = r" |
    1.69 +"del_root (Node l a h Leaf) = l" |
    1.70 +"del_root (Node l a h r) = (let (l', a') = split_max l in balR l' a' r)"
    1.71  
    1.72  lemmas del_root_cases = del_root.cases[case_names Leaf_t Node_Leaf Node_Node]
    1.73  
    1.74  fun delete :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.75  "delete _ Leaf = Leaf" |
    1.76 -"delete x (Node h l a r) =
    1.77 +"delete x (Node l a h r) =
    1.78    (case cmp x a of
    1.79 -     EQ \<Rightarrow> del_root (Node h l a r) |
    1.80 +     EQ \<Rightarrow> del_root (Node l a h r) |
    1.81       LT \<Rightarrow> balR (delete x l) a r |
    1.82       GT \<Rightarrow> balL l a (delete x r))"
    1.83  
    1.84 @@ -110,8 +110,8 @@
    1.85    (auto simp: inorder_balL split: if_splits prod.splits tree.split)
    1.86  
    1.87  lemma inorder_del_root:
    1.88 -  "inorder (del_root (Node h l a r)) = inorder l @ inorder r"
    1.89 -by(cases "Node h l a r" rule: del_root.cases)
    1.90 +  "inorder (del_root (Node l a h r)) = inorder l @ inorder r"
    1.91 +by(cases "Node l a h r" rule: del_root.cases)
    1.92    (auto simp: inorder_balL inorder_balR inorder_split_maxD split: if_splits prod.splits)
    1.93  
    1.94  theorem inorder_delete:
    1.95 @@ -188,7 +188,7 @@
    1.96    case Leaf
    1.97    with assms show ?thesis by (simp add: node_def balL_def)
    1.98  next
    1.99 -  case (Node ln ll lr lh)
   1.100 +  case Node
   1.101    with assms show ?thesis
   1.102    proof(cases "height l = height r + 2")
   1.103      case True
   1.104 @@ -208,7 +208,7 @@
   1.105    case Leaf
   1.106    with assms show ?thesis by (simp add: node_def balR_def)
   1.107  next
   1.108 -  case (Node rn rl rr rh)
   1.109 +  case Node
   1.110    with assms show ?thesis
   1.111    proof(cases "height r = height l + 2")
   1.112      case True
   1.113 @@ -230,7 +230,7 @@
   1.114          "(height (insert x t) = height t \<or> height (insert x t) = height t + 1)"
   1.115  using assms
   1.116  proof (induction t)
   1.117 -  case (Node h l a r)
   1.118 +  case (Node l a h r)
   1.119    case 1
   1.120    with Node show ?case
   1.121    proof(cases "x = a")
   1.122 @@ -307,14 +307,14 @@
   1.123           height x = height(fst (split_max x)) + 1"
   1.124  using assms
   1.125  proof (induct x rule: split_max_induct)
   1.126 -  case (Node h l a r)
   1.127 +  case (Node l a h r)
   1.128    case 1
   1.129    thus ?case using Node
   1.130      by (auto simp: height_balL height_balL2 avl_balL
   1.131        linorder_class.max.absorb1 linorder_class.max.absorb2
   1.132        split:prod.split)
   1.133  next
   1.134 -  case (Node h l a r)
   1.135 +  case (Node l a h r)
   1.136    case 2
   1.137    let ?r' = "fst (split_max r)"
   1.138    from \<open>avl x\<close> Node 2 have "avl l" and "avl r" by simp_all
   1.139 @@ -327,9 +327,9 @@
   1.140    shows "avl(del_root t)" 
   1.141  using assms
   1.142  proof (cases t rule:del_root_cases)
   1.143 -  case (Node_Node h lh ll ln lr n rh rl rn rr)
   1.144 -  let ?l = "Node lh ll ln lr"
   1.145 -  let ?r = "Node rh rl rn rr"
   1.146 +  case (Node_Node ll ln lh lr n h rl rn rh rr)
   1.147 +  let ?l = "Node ll ln lh lr"
   1.148 +  let ?r = "Node rl rn rh rr"
   1.149    let ?l' = "fst (split_max ?l)"
   1.150    from \<open>avl t\<close> and Node_Node have "avl ?r" by simp
   1.151    from \<open>avl t\<close> and Node_Node have "avl ?l" by simp
   1.152 @@ -347,9 +347,9 @@
   1.153    shows "height t = height(del_root t) \<or> height t = height(del_root t) + 1"
   1.154  using assms
   1.155  proof (cases t rule: del_root_cases)
   1.156 -  case (Node_Node h lh ll ln lr n rh rl rn rr)
   1.157 -  let ?l = "Node lh ll ln lr"
   1.158 -  let ?r = "Node rh rl rn rr"
   1.159 +  case (Node_Node ll ln lh lr n h rl rn rh rr)
   1.160 +  let ?l = "Node ll ln lh lr"
   1.161 +  let ?r = "Node rl rn rh rr"
   1.162    let ?l' = "fst (split_max ?l)"
   1.163    let ?t' = "balR ?l' (snd(split_max ?l)) ?r"
   1.164    from \<open>avl t\<close> and Node_Node have "avl ?r" by simp
   1.165 @@ -382,7 +382,7 @@
   1.166    shows "avl(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1"
   1.167  using assms
   1.168  proof (induct t)
   1.169 -  case (Node h l n r)
   1.170 +  case (Node l n h r)
   1.171    case 1
   1.172    with Node show ?case
   1.173    proof(cases "x = n")
   1.174 @@ -403,8 +403,8 @@
   1.175    with Node show ?case
   1.176    proof(cases "x = n")
   1.177      case True
   1.178 -    with 1 have "height (Node h l n r) = height(del_root (Node h l n r))
   1.179 -      \<or> height (Node h l n r) = height(del_root (Node h l n r)) + 1"
   1.180 +    with 1 have "height (Node l n h r) = height(del_root (Node l n h r))
   1.181 +      \<or> height (Node l n h r) = height(del_root (Node l n h r)) + 1"
   1.182        by (subst height_del_root,simp_all)
   1.183      with True show ?thesis by simp
   1.184    next
   1.185 @@ -459,7 +459,7 @@
   1.186  
   1.187  lemma height_invers: 
   1.188    "(height t = 0) = (t = Leaf)"
   1.189 -  "avl t \<Longrightarrow> (height t = Suc h) = (\<exists> l a r . t = Node (Suc h) l a r)"
   1.190 +  "avl t \<Longrightarrow> (height t = Suc h) = (\<exists> l a r . t = Node l a (Suc h) r)"
   1.191  by (induction t) auto
   1.192  
   1.193  text \<open>Any AVL tree of height \<open>h\<close> has at least \<open>fib (h+2)\<close> leaves:\<close>
   1.194 @@ -472,7 +472,7 @@
   1.195  next
   1.196    case (3 h)
   1.197    from "3.prems" obtain l a r where
   1.198 -    [simp]: "t = Node (Suc(Suc h)) l a r" "avl l" "avl r"
   1.199 +    [simp]: "t = Node l a (Suc(Suc h)) r" "avl l" "avl r"
   1.200      and C: "
   1.201        height r = Suc h \<and> height l = Suc h
   1.202      \<or> height r = Suc h \<and> height l = h