--- a/src/HOL/Data_Structures/AVL_Bal_Set.thy Tue May 05 20:32:57 2020 +0200
+++ b/src/HOL/Data_Structures/AVL_Bal_Set.thy Wed May 06 10:46:19 2020 +0200
@@ -1,6 +1,6 @@
(* Tobias Nipkow *)
-section "AVL Tree with Balance Tags (Set Implementation)"
+section "AVL Tree with Balance Factors"
theory AVL_Bal_Set
imports
@@ -9,7 +9,6 @@
begin
datatype bal = Lh | Bal | Rh
-(* Exercise: use 3 Node constructors instead *)
type_synonym 'a tree_bal = "('a * bal) tree"
@@ -27,9 +26,9 @@
subsection \<open>Code\<close>
-datatype 'a change = Same 'a | Diff 'a
+datatype 'a tree_bal2 = Same "'a tree_bal" | Diff "'a tree_bal"
-fun tree :: "'a change \<Rightarrow> 'a" where
+fun tree :: "'a tree_bal2 \<Rightarrow> 'a tree_bal" where
"tree(Same t) = t" |
"tree(Diff t) = t"
@@ -39,7 +38,7 @@
fun rot22 :: "bal \<Rightarrow> bal" where
"rot22 b = (if b=Lh then Rh else Bal)"
-fun balL :: "'a tree_bal change \<Rightarrow> 'a \<Rightarrow> bal \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal change" where
+fun balL :: "'a tree_bal2 \<Rightarrow> 'a \<Rightarrow> bal \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal2" where
"balL AB' c bc C = (case AB' of
Same AB \<Rightarrow> Same (Node AB (c,bc) C) |
Diff AB \<Rightarrow> (case bc of
@@ -51,7 +50,7 @@
Node B\<^sub>1 (b, bb) B\<^sub>2 \<Rightarrow>
Node (Node A (a,rot21 bb) B\<^sub>1) (b,Bal) (Node B\<^sub>2 (c,rot22 bb) C)))))"
-fun balR :: "'a tree_bal \<Rightarrow> 'a \<Rightarrow> bal \<Rightarrow> 'a tree_bal change \<Rightarrow> 'a tree_bal change" where
+fun balR :: "'a tree_bal \<Rightarrow> 'a \<Rightarrow> bal \<Rightarrow> 'a tree_bal2 \<Rightarrow> 'a tree_bal2" where
"balR A a ba BC' = (case BC' of
Same BC \<Rightarrow> Same (Node A (a,ba) BC) |
Diff BC \<Rightarrow> (case ba of
@@ -63,14 +62,14 @@
Node B\<^sub>1 (b, bb) B\<^sub>2 \<Rightarrow>
Node (Node A (a,rot21 bb) B\<^sub>1) (b,Bal) (Node B\<^sub>2 (c,rot22 bb) C)))))"
-fun insert :: "'a::linorder \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal change" where
+fun insert :: "'a::linorder \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal2" where
"insert x Leaf = Diff(Node Leaf (x, Bal) Leaf)" |
"insert x (Node l (a, b) r) = (case cmp x a of
EQ \<Rightarrow> Same(Node l (a, b) r) |
LT \<Rightarrow> balL (insert x l) a b r |
GT \<Rightarrow> balR l a b (insert x r))"
-fun baldR :: "'a tree_bal \<Rightarrow> 'a \<Rightarrow> bal \<Rightarrow> 'a tree_bal change \<Rightarrow> 'a tree_bal change" where
+fun baldR :: "'a tree_bal \<Rightarrow> 'a \<Rightarrow> bal \<Rightarrow> 'a tree_bal2 \<Rightarrow> 'a tree_bal2" where
"baldR AB c bc C' = (case C' of
Same C \<Rightarrow> Same (Node AB (c,bc) C) |
Diff C \<Rightarrow> (case bc of
@@ -83,7 +82,7 @@
Node B\<^sub>1 (b, bb) B\<^sub>2 \<Rightarrow>
Diff(Node (Node A (a,rot21 bb) B\<^sub>1) (b,Bal) (Node B\<^sub>2 (c,rot22 bb) C))))))"
-fun baldL :: "'a tree_bal change \<Rightarrow> 'a \<Rightarrow> bal \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal change" where
+fun baldL :: "'a tree_bal2 \<Rightarrow> 'a \<Rightarrow> bal \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal2" where
"baldL A' a ba BC = (case A' of
Same A \<Rightarrow> Same (Node A (a,ba) BC) |
Diff A \<Rightarrow> (case ba of
@@ -96,11 +95,11 @@
Node B\<^sub>1 (b, bb) B\<^sub>2 \<Rightarrow>
Diff(Node (Node A (a,rot21 bb) B\<^sub>1) (b,Bal) (Node B\<^sub>2 (c,rot22 bb) C))))))"
-fun split_max :: "'a tree_bal \<Rightarrow> 'a tree_bal change * 'a" where
+fun split_max :: "'a tree_bal \<Rightarrow> 'a tree_bal2 * 'a" where
"split_max (Node l (a, ba) r) =
(if r = Leaf then (Diff l,a) else let (r',a') = split_max r in (baldR l a ba r', a'))"
-fun delete :: "'a::linorder \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal change" where
+fun delete :: "'a::linorder \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal2" where
"delete _ Leaf = Same Leaf" |
"delete x (Node l (a, ba) r) =
(case cmp x a of
@@ -111,7 +110,7 @@
lemmas split_max_induct = split_max.induct[case_names Node Leaf]
-lemmas splits = if_splits tree.splits tree.splits change.splits bal.splits
+lemmas splits = if_splits tree.splits tree.splits tree_bal2.splits bal.splits
subsection \<open>Proofs\<close>
--- a/src/HOL/Data_Structures/AVL_Map.thy Tue May 05 20:32:57 2020 +0200
+++ b/src/HOL/Data_Structures/AVL_Map.thy Wed May 06 10:46:19 2020 +0200
@@ -8,14 +8,14 @@
Lookup2
begin
-fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
+fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree_ht \<Rightarrow> ('a*'b) tree_ht" where
"update x y Leaf = Node Leaf ((x,y), 1) Leaf" |
"update x y (Node l ((a,b), h) r) = (case cmp x a of
EQ \<Rightarrow> Node l ((x,y), h) r |
LT \<Rightarrow> balL (update x y l) (a,b) r |
GT \<Rightarrow> balR l (a,b) (update x y r))"
-fun delete :: "'a::linorder \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
+fun delete :: "'a::linorder \<Rightarrow> ('a*'b) tree_ht \<Rightarrow> ('a*'b) tree_ht" where
"delete _ Leaf = Leaf" |
"delete x (Node l ((a,b), h) r) = (case cmp x a of
EQ \<Rightarrow> if l = Leaf then r
--- a/src/HOL/Data_Structures/AVL_Set.thy Tue May 05 20:32:57 2020 +0200
+++ b/src/HOL/Data_Structures/AVL_Set.thy Wed May 06 10:46:19 2020 +0200
@@ -8,7 +8,7 @@
"HOL-Number_Theory.Fib"
begin
-fun avl :: "'a avl_tree \<Rightarrow> bool" where
+fun avl :: "'a tree_ht \<Rightarrow> bool" where
"avl Leaf = True" |
"avl (Node l (a,n) r) =
(abs(int(height l) - int(height r)) \<le> 1 \<and>
@@ -26,16 +26,12 @@
lemma height_balL:
"\<lbrakk> avl l; avl r; height l = height r + 2 \<rbrakk> \<Longrightarrow>
height (balL l a r) \<in> {height r + 2, height r + 3}"
-apply (cases l)
- apply (auto simp:node_def balL_def split:tree.split)
- by arith+
+by (auto simp:node_def balL_def split:tree.split)
lemma height_balR:
"\<lbrakk> avl l; avl r; height r = height l + 2 \<rbrakk> \<Longrightarrow>
height (balR l a r) : {height l + 2, height l + 3}"
-apply (cases r)
- apply(auto simp add:node_def balR_def split:tree.split)
- by arith+
+by(auto simp add:node_def balR_def split:tree.split)
lemma height_node[simp]: "height(node l a r) = max (height l) (height r) + 1"
by (simp add: node_def)
--- a/src/HOL/Data_Structures/AVL_Set_Code.thy Tue May 05 20:32:57 2020 +0200
+++ b/src/HOL/Data_Structures/AVL_Set_Code.thy Wed May 06 10:46:19 2020 +0200
@@ -13,19 +13,19 @@
subsection \<open>Code\<close>
-type_synonym 'a avl_tree = "('a*nat) tree"
+type_synonym 'a tree_ht = "('a*nat) tree"
-definition empty :: "'a avl_tree" where
+definition empty :: "'a tree_ht" where
"empty = Leaf"
-fun ht :: "'a avl_tree \<Rightarrow> nat" where
+fun ht :: "'a tree_ht \<Rightarrow> nat" where
"ht Leaf = 0" |
"ht (Node l (a,n) r) = n"
-definition node :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
+definition node :: "'a tree_ht \<Rightarrow> 'a \<Rightarrow> 'a tree_ht \<Rightarrow> 'a tree_ht" where
"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
+definition balL :: "'a tree_ht \<Rightarrow> 'a \<Rightarrow> 'a tree_ht \<Rightarrow> 'a tree_ht" where
"balL AB c C =
(if ht AB = ht C + 2 then
case AB of
@@ -36,7 +36,7 @@
Node B\<^sub>1 (b, _) B\<^sub>2 \<Rightarrow> node (node A a B\<^sub>1) b (node B\<^sub>2 c C)
else node AB c C)"
-definition balR :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
+definition balR :: "'a tree_ht \<Rightarrow> 'a \<Rightarrow> 'a tree_ht \<Rightarrow> 'a tree_ht" where
"balR A a BC =
(if ht BC = ht A + 2 then
case BC of
@@ -47,20 +47,20 @@
Node B\<^sub>1 (b, _) B\<^sub>2 \<Rightarrow> node (node A a B\<^sub>1) b (node B\<^sub>2 c C)
else node A a BC)"
-fun insert :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
+fun insert :: "'a::linorder \<Rightarrow> 'a tree_ht \<Rightarrow> 'a tree_ht" where
"insert x Leaf = Node Leaf (x, 1) Leaf" |
"insert x (Node l (a, n) r) = (case cmp x a of
EQ \<Rightarrow> Node l (a, n) 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
+fun split_max :: "'a tree_ht \<Rightarrow> 'a tree_ht * 'a" where
"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 delete :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
+fun delete :: "'a::linorder \<Rightarrow> 'a tree_ht \<Rightarrow> 'a tree_ht" where
"delete _ Leaf = Leaf" |
"delete x (Node l (a, n) r) =
(case cmp x a of
--- a/src/HOL/Data_Structures/Height_Balanced_Tree.thy Tue May 05 20:32:57 2020 +0200
+++ b/src/HOL/Data_Structures/Height_Balanced_Tree.thy Wed May 06 10:46:19 2020 +0200
@@ -12,9 +12,9 @@
The code and the proofs were obtained by small modifications of the AVL theories.
This is an implementation of sets via HBTs.\<close>
-type_synonym 'a hbt = "('a*nat) tree"
+type_synonym 'a tree_ht = "('a*nat) tree"
-definition empty :: "'a hbt" where
+definition empty :: "'a tree_ht" where
"empty = Leaf"
text \<open>The maximal amount by which the height of two siblings may differ:\<close>
@@ -26,20 +26,20 @@
text \<open>Invariant:\<close>
-fun hbt :: "'a hbt \<Rightarrow> bool" where
+fun hbt :: "'a tree_ht \<Rightarrow> bool" where
"hbt Leaf = True" |
"hbt (Node l (a,n) r) =
(abs(int(height l) - int(height r)) \<le> int(m) \<and>
n = max (height l) (height r) + 1 \<and> hbt l \<and> hbt r)"
-fun ht :: "'a hbt \<Rightarrow> nat" where
+fun ht :: "'a tree_ht \<Rightarrow> nat" where
"ht Leaf = 0" |
"ht (Node l (a,n) r) = n"
-definition node :: "'a hbt \<Rightarrow> 'a \<Rightarrow> 'a hbt \<Rightarrow> 'a hbt" where
+definition node :: "'a tree_ht \<Rightarrow> 'a \<Rightarrow> 'a tree_ht \<Rightarrow> 'a tree_ht" where
"node l a r = Node l (a, max (ht l) (ht r) + 1) r"
-definition balL :: "'a hbt \<Rightarrow> 'a \<Rightarrow> 'a hbt \<Rightarrow> 'a hbt" where
+definition balL :: "'a tree_ht \<Rightarrow> 'a \<Rightarrow> 'a tree_ht \<Rightarrow> 'a tree_ht" where
"balL AB b C =
(if ht AB = ht C + m + 1 then
case AB of
@@ -50,7 +50,7 @@
Node B\<^sub>1 (ab, _) B\<^sub>2 \<Rightarrow> node (node A a B\<^sub>1) ab (node B\<^sub>2 b C)
else node AB b C)"
-definition balR :: "'a hbt \<Rightarrow> 'a \<Rightarrow> 'a hbt \<Rightarrow> 'a hbt" where
+definition balR :: "'a tree_ht \<Rightarrow> 'a \<Rightarrow> 'a tree_ht \<Rightarrow> 'a tree_ht" where
"balR A a BC =
(if ht BC = ht A + m + 1 then
case BC of
@@ -61,20 +61,20 @@
Node B\<^sub>1 (ab, _) B\<^sub>2 \<Rightarrow> node (node A a B\<^sub>1) ab (node B\<^sub>2 b C)
else node A a BC)"
-fun insert :: "'a::linorder \<Rightarrow> 'a hbt \<Rightarrow> 'a hbt" where
+fun insert :: "'a::linorder \<Rightarrow> 'a tree_ht \<Rightarrow> 'a tree_ht" where
"insert x Leaf = Node Leaf (x, 1) Leaf" |
"insert x (Node l (a, n) r) = (case cmp x a of
EQ \<Rightarrow> Node l (a, n) r |
LT \<Rightarrow> balL (insert x l) a r |
GT \<Rightarrow> balR l a (insert x r))"
-fun split_max :: "'a hbt \<Rightarrow> 'a hbt * 'a" where
+fun split_max :: "'a tree_ht \<Rightarrow> 'a tree_ht * 'a" where
"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 delete :: "'a::linorder \<Rightarrow> 'a hbt \<Rightarrow> 'a hbt" where
+fun delete :: "'a::linorder \<Rightarrow> 'a tree_ht \<Rightarrow> 'a tree_ht" where
"delete _ Leaf = Leaf" |
"delete x (Node l (a, n) r) =
(case cmp x a of
@@ -132,16 +132,12 @@
lemma height_balL:
"\<lbrakk> hbt l; hbt r; height l = height r + m + 1 \<rbrakk> \<Longrightarrow>
height (balL l a r) \<in> {height r + m + 1, height r + m + 2}"
-apply (cases l)
- apply (auto simp:node_def balL_def split:tree.split)
- by arith+
+by (auto simp:node_def balL_def split:tree.split)
lemma height_balR:
"\<lbrakk> hbt l; hbt r; height r = height l + m + 1 \<rbrakk> \<Longrightarrow>
height (balR l a r) \<in> {height l + m + 1, height l + m + 2}"
-apply (cases r)
- apply(auto simp add:node_def balR_def split:tree.split)
- by arith+
+by(auto simp add:node_def balR_def split:tree.split)
lemma height_node[simp]: "height(node l a r) = max (height l) (height r) + 1"
by (simp add: node_def)
@@ -149,22 +145,20 @@
lemma height_balL2:
"\<lbrakk> hbt l; hbt r; height l \<noteq> height r + m + 1 \<rbrakk> \<Longrightarrow>
height (balL l a r) = 1 + max (height l) (height r)"
-by (cases l, cases r) (simp_all add: balL_def)
+by (simp_all add: balL_def)
lemma height_balR2:
"\<lbrakk> hbt l; hbt r; height r \<noteq> height l + m + 1 \<rbrakk> \<Longrightarrow>
height (balR l a r) = 1 + max (height l) (height r)"
-by (cases l, cases r) (simp_all add: balR_def)
+by (simp_all add: balR_def)
lemma hbt_balL:
"\<lbrakk> hbt l; hbt r; height r - m \<le> height l \<and> height l \<le> height r + m + 1 \<rbrakk> \<Longrightarrow> hbt(balL l a r)"
-by(cases l, cases r)
- (auto simp: balL_def node_def max_def split!: if_splits tree.split)
+by(auto simp: balL_def node_def max_def split!: if_splits tree.split)
lemma hbt_balR:
"\<lbrakk> hbt l; hbt r; height l - m \<le> height r \<and> height r \<le> height l + m + 1 \<rbrakk> \<Longrightarrow> hbt(balR l a r)"
-by(cases r, cases l)
- (auto simp: balR_def node_def max_def split!: if_splits tree.split)
+by(auto simp: balR_def node_def max_def split!: if_splits tree.split)
text\<open>Insertion maintains @{const hbt}. Requires simultaneous proof.\<close>