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