renamed "balanced" -> "acomplete" because balanced has other meanings in the literature
--- a/src/HOL/Data_Structures/Balance.thy Sun Nov 08 21:27:08 2020 +0100
+++ b/src/HOL/Data_Structures/Balance.thy Tue Nov 10 17:42:41 2020 +0100
@@ -1,6 +1,6 @@
(* Author: Tobias Nipkow *)
-section \<open>Creating Balanced Trees\<close>
+section \<open>Creating Almost Complete Trees\<close>
theory Balance
imports
@@ -169,9 +169,9 @@
qed
qed
-lemma balanced_bal:
- assumes "n \<le> length xs" "bal n xs = (t,ys)" shows "balanced t"
-unfolding balanced_def
+lemma acomplete_bal:
+ assumes "n \<le> length xs" "bal n xs = (t,ys)" shows "acomplete t"
+unfolding acomplete_def
using height_bal[OF assms] min_height_bal[OF assms]
by linarith
@@ -192,16 +192,16 @@
"height (balance_tree t) = nat\<lceil>log 2 (size t + 1)\<rceil>"
by (simp add: bal_tree_def balance_tree_def height_bal_list)
-corollary balanced_bal_list[simp]: "n \<le> length xs \<Longrightarrow> balanced (bal_list n xs)"
-unfolding bal_list_def by (metis balanced_bal prod.collapse)
+corollary acomplete_bal_list[simp]: "n \<le> length xs \<Longrightarrow> acomplete (bal_list n xs)"
+unfolding bal_list_def by (metis acomplete_bal prod.collapse)
-corollary balanced_balance_list[simp]: "balanced (balance_list xs)"
+corollary acomplete_balance_list[simp]: "acomplete (balance_list xs)"
by (simp add: balance_list_def)
-corollary balanced_bal_tree[simp]: "n \<le> size t \<Longrightarrow> balanced (bal_tree n t)"
+corollary acomplete_bal_tree[simp]: "n \<le> size t \<Longrightarrow> acomplete (bal_tree n t)"
by (simp add: bal_tree_def)
-corollary balanced_balance_tree[simp]: "balanced (balance_tree t)"
+corollary acomplete_balance_tree[simp]: "acomplete (balance_tree t)"
by (simp add: balance_tree_def)
lemma wbalanced_bal: "\<lbrakk> n \<le> length xs; bal n xs = (t,ys) \<rbrakk> \<Longrightarrow> wbalanced t"
@@ -226,9 +226,9 @@
qed
qed
-text\<open>An alternative proof via @{thm balanced_if_wbalanced}:\<close>
-lemma "\<lbrakk> n \<le> length xs; bal n xs = (t,ys) \<rbrakk> \<Longrightarrow> balanced t"
-by(rule balanced_if_wbalanced[OF wbalanced_bal])
+text\<open>An alternative proof via @{thm acomplete_if_wbalanced}:\<close>
+lemma "\<lbrakk> n \<le> length xs; bal n xs = (t,ys) \<rbrakk> \<Longrightarrow> acomplete t"
+by(rule acomplete_if_wbalanced[OF wbalanced_bal])
lemma wbalanced_bal_list[simp]: "n \<le> length xs \<Longrightarrow> wbalanced (bal_list n xs)"
by(simp add: bal_list_def) (metis prod.collapse wbalanced_bal)
--- a/src/HOL/Data_Structures/Braun_Tree.thy Sun Nov 08 21:27:08 2020 +0100
+++ b/src/HOL/Data_Structures/Braun_Tree.thy Tue Nov 10 17:42:41 2020 +0100
@@ -30,13 +30,13 @@
thus ?case using Node.prems(1,2) Node.IH by auto
qed
-text \<open>Braun trees are balanced:\<close>
+text \<open>Braun trees are almost complete:\<close>
-lemma balanced_if_braun: "braun t \<Longrightarrow> balanced t"
+lemma acomplete_if_braun: "braun t \<Longrightarrow> acomplete t"
proof(induction t)
- case Leaf show ?case by (simp add: balanced_def)
+ case Leaf show ?case by (simp add: acomplete_def)
next
- case (Node l x r) thus ?case using balanced_Node_if_wbal2 by force
+ case (Node l x r) thus ?case using acomplete_Node_if_wbal2 by force
qed
subsection \<open>Numbering Nodes\<close>
--- a/src/HOL/Data_Structures/Tree23.thy Sun Nov 08 21:27:08 2020 +0100
+++ b/src/HOL/Data_Structures/Tree23.thy Tue Nov 10 17:42:41 2020 +0100
@@ -32,7 +32,7 @@
end
-text \<open>Balanced:\<close>
+text \<open>Completeness:\<close>
fun complete :: "'a tree23 \<Rightarrow> bool" where
"complete Leaf = True" |
--- a/src/HOL/Data_Structures/Tree23_Set.thy Sun Nov 08 21:27:08 2020 +0100
+++ b/src/HOL/Data_Structures/Tree23_Set.thy Tue Nov 10 17:42:41 2020 +0100
@@ -114,7 +114,7 @@
"split_min (Node3 l a m b r) = (let (x,l') = split_min l in (x, node31 l' a m b r))"
text \<open>In the base cases of \<open>split_min\<close> and \<open>del\<close> it is enough to check if one subtree is a \<open>Leaf\<close>,
-in which case balancedness implies that so are the others. Exercise.\<close>
+in which case completeness implies that so are the others. Exercise.\<close>
fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a upD" where
"del x Leaf = TD Leaf" |
@@ -203,7 +203,7 @@
by(simp add: delete_def inorder_del)
-subsection \<open>Balancedness\<close>
+subsection \<open>Completeness\<close>
subsubsection "Proofs for insert"
@@ -225,7 +225,7 @@
by (induct t) (auto split!: if_split upI.split) (* 15 secs in 2015 *)
text\<open>Now an alternative proof (by Brian Huffman) that runs faster because
-two properties (balance and height) are combined in one predicate.\<close>
+two properties (completeness and height) are combined in one predicate.\<close>
inductive full :: "nat \<Rightarrow> 'a tree23 \<Rightarrow> bool" where
"full 0 Leaf" |
--- a/src/HOL/Library/Tree.thy Sun Nov 08 21:27:08 2020 +0100
+++ b/src/HOL/Library/Tree.thy Tue Nov 10 17:42:41 2020 +0100
@@ -1,5 +1,5 @@
(* Author: Tobias Nipkow *)
-(* Todo: minimal ipl of balanced trees *)
+(* Todo: minimal ipl of almost complete trees *)
section \<open>Binary Tree\<close>
@@ -55,8 +55,9 @@
"complete Leaf = True" |
"complete (Node l x r) = (complete l \<and> complete r \<and> height l = height r)"
-definition balanced :: "'a tree \<Rightarrow> bool" where
-"balanced t = (height t - min_height t \<le> 1)"
+text \<open>Almost complete:\<close>
+definition acomplete :: "'a tree \<Rightarrow> bool" where
+"acomplete t = (height t - min_height t \<le> 1)"
text \<open>Weight balanced:\<close>
fun wbalanced :: "'a tree \<Rightarrow> bool" where
@@ -290,24 +291,24 @@
using complete_if_size1_height size1_if_complete by blast
-subsection \<open>\<^const>\<open>balanced\<close>\<close>
+subsection \<open>\<^const>\<open>acomplete\<close>\<close>
-lemma balanced_subtreeL: "balanced (Node l x r) \<Longrightarrow> balanced l"
-by(simp add: balanced_def)
+lemma acomplete_subtreeL: "acomplete (Node l x r) \<Longrightarrow> acomplete l"
+by(simp add: acomplete_def)
-lemma balanced_subtreeR: "balanced (Node l x r) \<Longrightarrow> balanced r"
-by(simp add: balanced_def)
+lemma acomplete_subtreeR: "acomplete (Node l x r) \<Longrightarrow> acomplete r"
+by(simp add: acomplete_def)
-lemma balanced_subtrees: "\<lbrakk> balanced t; s \<in> subtrees t \<rbrakk> \<Longrightarrow> balanced s"
+lemma acomplete_subtrees: "\<lbrakk> acomplete t; s \<in> subtrees t \<rbrakk> \<Longrightarrow> acomplete s"
using [[simp_depth_limit=1]]
by(induction t arbitrary: s)
- (auto simp add: balanced_subtreeL balanced_subtreeR)
+ (auto simp add: acomplete_subtreeL acomplete_subtreeR)
text\<open>Balanced trees have optimal height:\<close>
-lemma balanced_optimal:
+lemma acomplete_optimal:
fixes t :: "'a tree" and t' :: "'b tree"
-assumes "balanced t" "size t \<le> size t'" shows "height t \<le> height t'"
+assumes "acomplete t" "size t \<le> size t'" shows "height t \<le> height t'"
proof (cases "complete t")
case True
have "(2::nat) ^ height t \<le> 2 ^ height t'"
@@ -333,7 +334,7 @@
hence *: "min_height t < height t'" by simp
have "min_height t + 1 = height t"
using min_height_le_height[of t] assms(1) False
- by (simp add: complete_iff_height balanced_def)
+ by (simp add: complete_iff_height acomplete_def)
with * show ?thesis by arith
qed
--- a/src/HOL/Library/Tree_Real.thy Sun Nov 08 21:27:08 2020 +0100
+++ b/src/HOL/Library/Tree_Real.thy Tue Nov 10 17:42:41 2020 +0100
@@ -26,7 +26,7 @@
by (simp add: less_log2_of_power min_height_size1_if_incomplete)
-lemma min_height_balanced: assumes "balanced t"
+lemma min_height_acomplete: assumes "acomplete t"
shows "min_height t = nat(floor(log 2 (size1 t)))"
proof cases
assume *: "complete t"
@@ -37,12 +37,12 @@
assume *: "\<not> complete t"
hence "height t = min_height t + 1"
using assms min_height_le_height[of t]
- by(auto simp: balanced_def complete_iff_height)
+ by(auto simp: acomplete_def complete_iff_height)
hence "size1 t < 2 ^ (min_height t + 1)" by (metis * size1_height_if_incomplete)
from floor_log_nat_eq_if[OF min_height_size1 this] show ?thesis by simp
qed
-lemma height_balanced: assumes "balanced t"
+lemma height_acomplete: assumes "acomplete t"
shows "height t = nat(ceiling(log 2 (size1 t)))"
proof cases
assume *: "complete t"
@@ -52,41 +52,41 @@
assume *: "\<not> complete t"
hence **: "height t = min_height t + 1"
using assms min_height_le_height[of t]
- by(auto simp add: balanced_def complete_iff_height)
+ by(auto simp add: acomplete_def complete_iff_height)
hence "size1 t \<le> 2 ^ (min_height t + 1)" by (metis size1_height)
from log2_of_power_le[OF this size1_ge0] min_height_size1_log_if_incomplete[OF *] **
show ?thesis by linarith
qed
-lemma balanced_Node_if_wbal1:
-assumes "balanced l" "balanced r" "size l = size r + 1"
-shows "balanced \<langle>l, x, r\<rangle>"
+lemma acomplete_Node_if_wbal1:
+assumes "acomplete l" "acomplete r" "size l = size r + 1"
+shows "acomplete \<langle>l, x, r\<rangle>"
proof -
from assms(3) have [simp]: "size1 l = size1 r + 1" by(simp add: size1_size)
have "nat \<lceil>log 2 (1 + size1 r)\<rceil> \<ge> nat \<lceil>log 2 (size1 r)\<rceil>"
by(rule nat_mono[OF ceiling_mono]) simp
hence 1: "height(Node l x r) = nat \<lceil>log 2 (1 + size1 r)\<rceil> + 1"
- using height_balanced[OF assms(1)] height_balanced[OF assms(2)]
+ using height_acomplete[OF assms(1)] height_acomplete[OF assms(2)]
by (simp del: nat_ceiling_le_eq add: max_def)
have "nat \<lfloor>log 2 (1 + size1 r)\<rfloor> \<ge> nat \<lfloor>log 2 (size1 r)\<rfloor>"
by(rule nat_mono[OF floor_mono]) simp
hence 2: "min_height(Node l x r) = nat \<lfloor>log 2 (size1 r)\<rfloor> + 1"
- using min_height_balanced[OF assms(1)] min_height_balanced[OF assms(2)]
+ using min_height_acomplete[OF assms(1)] min_height_acomplete[OF assms(2)]
by (simp)
have "size1 r \<ge> 1" by(simp add: size1_size)
then obtain i where i: "2 ^ i \<le> size1 r" "size1 r < 2 ^ (i + 1)"
using ex_power_ivl1[of 2 "size1 r"] by auto
hence i1: "2 ^ i < size1 r + 1" "size1 r + 1 \<le> 2 ^ (i + 1)" by auto
from 1 2 floor_log_nat_eq_if[OF i] ceiling_log_nat_eq_if[OF i1]
- show ?thesis by(simp add:balanced_def)
+ show ?thesis by(simp add:acomplete_def)
qed
-lemma balanced_sym: "balanced \<langle>l, x, r\<rangle> \<Longrightarrow> balanced \<langle>r, y, l\<rangle>"
-by(auto simp: balanced_def)
+lemma acomplete_sym: "acomplete \<langle>l, x, r\<rangle> \<Longrightarrow> acomplete \<langle>r, y, l\<rangle>"
+by(auto simp: acomplete_def)
-lemma balanced_Node_if_wbal2:
-assumes "balanced l" "balanced r" "abs(int(size l) - int(size r)) \<le> 1"
-shows "balanced \<langle>l, x, r\<rangle>"
+lemma acomplete_Node_if_wbal2:
+assumes "acomplete l" "acomplete r" "abs(int(size l) - int(size r)) \<le> 1"
+shows "acomplete \<langle>l, x, r\<rangle>"
proof -
have "size l = size r \<or> (size l = size r + 1 \<or> size r = size l + 1)" (is "?A \<or> ?B")
using assms(3) by linarith
@@ -94,21 +94,21 @@
proof
assume "?A"
thus ?thesis using assms(1,2)
- apply(simp add: balanced_def min_def max_def)
- by (metis assms(1,2) balanced_optimal le_antisym le_less)
+ apply(simp add: acomplete_def min_def max_def)
+ by (metis assms(1,2) acomplete_optimal le_antisym le_less)
next
assume "?B"
thus ?thesis
- by (meson assms(1,2) balanced_sym balanced_Node_if_wbal1)
+ by (meson assms(1,2) acomplete_sym acomplete_Node_if_wbal1)
qed
qed
-lemma balanced_if_wbalanced: "wbalanced t \<Longrightarrow> balanced t"
+lemma acomplete_if_wbalanced: "wbalanced t \<Longrightarrow> acomplete t"
proof(induction t)
- case Leaf show ?case by (simp add: balanced_def)
+ case Leaf show ?case by (simp add: acomplete_def)
next
case (Node l x r)
- thus ?case by(simp add: balanced_Node_if_wbal2)
+ thus ?case by(simp add: acomplete_Node_if_wbal2)
qed
end
--- a/src/HOL/ex/Tree23.thy Sun Nov 08 21:27:08 2020 +0100
+++ b/src/HOL/ex/Tree23.thy Tue Nov 10 17:42:41 2020 +0100
@@ -12,9 +12,6 @@
in the Isabelle source code. That source is due to Makarius Wenzel and Stefan
Berghofer.
-So far this file contains only data types and functions, but no proofs. Feel
-free to have a go at the latter!
-
Note that because of complicated patterns and mutual recursion, these
function definitions take a few minutes and can also be seen as stress tests
for the function definition facility.\<close>