--- a/src/HOL/Data_Structures/AVL_Set.thy Mon Jun 11 08:15:43 2018 +0200
+++ b/src/HOL/Data_Structures/AVL_Set.thy Mon Jun 11 16:29:27 2018 +0200
@@ -18,25 +18,25 @@
fun avl :: "'a avl_tree \<Rightarrow> bool" where
"avl Leaf = True" |
-"avl (Node h l a r) =
+"avl (Node l a h r) =
((height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1) \<and>
h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
fun ht :: "'a avl_tree \<Rightarrow> nat" where
"ht Leaf = 0" |
-"ht (Node h l a r) = h"
+"ht (Node l a h r) = h"
definition node :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
-"node l a r = Node (max (ht l) (ht r) + 1) l a r"
+"node l a r = Node l a (max (ht l) (ht r) + 1) r"
definition balL :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
"balL l a r =
(if ht l = ht r + 2 then
case l of
- Node _ bl b br \<Rightarrow>
+ Node bl b _ br \<Rightarrow>
if ht bl < ht br then
case br of
- Node _ cl c cr \<Rightarrow> node (node bl b cl) c (node cr a r)
+ Node cl c _ cr \<Rightarrow> node (node bl b cl) c (node cr a r)
else node bl b (node br a r)
else node l a r)"
@@ -44,38 +44,38 @@
"balR l a r =
(if ht r = ht l + 2 then
case r of
- Node _ bl b br \<Rightarrow>
+ Node bl b _ br \<Rightarrow>
if ht bl > ht br then
case bl of
- Node _ cl c cr \<Rightarrow> node (node l a cl) c (node cr b br)
+ Node cl c _ cr \<Rightarrow> node (node l a cl) c (node cr b br)
else node (node l a bl) b br
else node l a r)"
fun insert :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
-"insert x Leaf = Node 1 Leaf x Leaf" |
-"insert x (Node h l a r) = (case cmp x a of
- EQ \<Rightarrow> Node h l a r |
+"insert x Leaf = Node Leaf x 1 Leaf" |
+"insert x (Node l a h r) = (case cmp x a of
+ EQ \<Rightarrow> Node l a h r |
LT \<Rightarrow> balL (insert x l) a r |
GT \<Rightarrow> balR l a (insert x r))"
fun split_max :: "'a avl_tree \<Rightarrow> 'a avl_tree * 'a" where
-"split_max (Node _ l a r) =
+"split_max (Node l a _ r) =
(if r = Leaf then (l,a) else let (r',a') = split_max r in (balL l a r', a'))"
lemmas split_max_induct = split_max.induct[case_names Node Leaf]
fun del_root :: "'a avl_tree \<Rightarrow> 'a avl_tree" where
-"del_root (Node h Leaf a r) = r" |
-"del_root (Node h l a Leaf) = l" |
-"del_root (Node h l a r) = (let (l', a') = split_max l in balR l' a' r)"
+"del_root (Node Leaf a h r) = r" |
+"del_root (Node l a h Leaf) = l" |
+"del_root (Node l a h r) = (let (l', a') = split_max l in balR l' a' r)"
lemmas del_root_cases = del_root.cases[case_names Leaf_t Node_Leaf Node_Node]
fun delete :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
"delete _ Leaf = Leaf" |
-"delete x (Node h l a r) =
+"delete x (Node l a h r) =
(case cmp x a of
- EQ \<Rightarrow> del_root (Node h l a r) |
+ EQ \<Rightarrow> del_root (Node l a h r) |
LT \<Rightarrow> balR (delete x l) a r |
GT \<Rightarrow> balL l a (delete x r))"
@@ -110,8 +110,8 @@
(auto simp: inorder_balL split: if_splits prod.splits tree.split)
lemma inorder_del_root:
- "inorder (del_root (Node h l a r)) = inorder l @ inorder r"
-by(cases "Node h l a r" rule: del_root.cases)
+ "inorder (del_root (Node l a h r)) = inorder l @ inorder r"
+by(cases "Node l a h r" rule: del_root.cases)
(auto simp: inorder_balL inorder_balR inorder_split_maxD split: if_splits prod.splits)
theorem inorder_delete:
@@ -188,7 +188,7 @@
case Leaf
with assms show ?thesis by (simp add: node_def balL_def)
next
- case (Node ln ll lr lh)
+ case Node
with assms show ?thesis
proof(cases "height l = height r + 2")
case True
@@ -208,7 +208,7 @@
case Leaf
with assms show ?thesis by (simp add: node_def balR_def)
next
- case (Node rn rl rr rh)
+ case Node
with assms show ?thesis
proof(cases "height r = height l + 2")
case True
@@ -230,7 +230,7 @@
"(height (insert x t) = height t \<or> height (insert x t) = height t + 1)"
using assms
proof (induction t)
- case (Node h l a r)
+ case (Node l a h r)
case 1
with Node show ?case
proof(cases "x = a")
@@ -307,14 +307,14 @@
height x = height(fst (split_max x)) + 1"
using assms
proof (induct x rule: split_max_induct)
- case (Node h l a r)
+ case (Node l a h r)
case 1
thus ?case using Node
by (auto simp: height_balL height_balL2 avl_balL
linorder_class.max.absorb1 linorder_class.max.absorb2
split:prod.split)
next
- case (Node h l a r)
+ case (Node l a h r)
case 2
let ?r' = "fst (split_max r)"
from \<open>avl x\<close> Node 2 have "avl l" and "avl r" by simp_all
@@ -327,9 +327,9 @@
shows "avl(del_root t)"
using assms
proof (cases t rule:del_root_cases)
- case (Node_Node h lh ll ln lr n rh rl rn rr)
- let ?l = "Node lh ll ln lr"
- let ?r = "Node rh rl rn rr"
+ case (Node_Node ll ln lh lr n h rl rn rh rr)
+ let ?l = "Node ll ln lh lr"
+ let ?r = "Node rl rn rh rr"
let ?l' = "fst (split_max ?l)"
from \<open>avl t\<close> and Node_Node have "avl ?r" by simp
from \<open>avl t\<close> and Node_Node have "avl ?l" by simp
@@ -347,9 +347,9 @@
shows "height t = height(del_root t) \<or> height t = height(del_root t) + 1"
using assms
proof (cases t rule: del_root_cases)
- case (Node_Node h lh ll ln lr n rh rl rn rr)
- let ?l = "Node lh ll ln lr"
- let ?r = "Node rh rl rn rr"
+ case (Node_Node ll ln lh lr n h rl rn rh rr)
+ let ?l = "Node ll ln lh lr"
+ let ?r = "Node rl rn rh rr"
let ?l' = "fst (split_max ?l)"
let ?t' = "balR ?l' (snd(split_max ?l)) ?r"
from \<open>avl t\<close> and Node_Node have "avl ?r" by simp
@@ -382,7 +382,7 @@
shows "avl(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1"
using assms
proof (induct t)
- case (Node h l n r)
+ case (Node l n h r)
case 1
with Node show ?case
proof(cases "x = n")
@@ -403,8 +403,8 @@
with Node show ?case
proof(cases "x = n")
case True
- with 1 have "height (Node h l n r) = height(del_root (Node h l n r))
- \<or> height (Node h l n r) = height(del_root (Node h l n r)) + 1"
+ with 1 have "height (Node l n h r) = height(del_root (Node l n h r))
+ \<or> height (Node l n h r) = height(del_root (Node l n h r)) + 1"
by (subst height_del_root,simp_all)
with True show ?thesis by simp
next
@@ -459,7 +459,7 @@
lemma height_invers:
"(height t = 0) = (t = Leaf)"
- "avl t \<Longrightarrow> (height t = Suc h) = (\<exists> l a r . t = Node (Suc h) l a r)"
+ "avl t \<Longrightarrow> (height t = Suc h) = (\<exists> l a r . t = Node l a (Suc h) r)"
by (induction t) auto
text \<open>Any AVL tree of height \<open>h\<close> has at least \<open>fib (h+2)\<close> leaves:\<close>
@@ -472,7 +472,7 @@
next
case (3 h)
from "3.prems" obtain l a r where
- [simp]: "t = Node (Suc(Suc h)) l a r" "avl l" "avl r"
+ [simp]: "t = Node l a (Suc(Suc h)) r" "avl l" "avl r"
and C: "
height r = Suc h \<and> height l = Suc h
\<or> height r = Suc h \<and> height l = h