# HG changeset patch
# User nipkow
# Date 1605026561 -3600
# Node ID 831f17da1aabbe1ff8e96d86ac03427557103c89
# Parent  ed5b907bbf50a7f1b0563c5b319781abe57c2a3a
renamed "balanced" -> "acomplete" because balanced has other meanings in the literature

diff -r ed5b907bbf50 -r 831f17da1aab src/HOL/Data_Structures/Balance.thy
--- 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)
diff -r ed5b907bbf50 -r 831f17da1aab src/HOL/Data_Structures/Braun_Tree.thy
--- 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>
diff -r ed5b907bbf50 -r 831f17da1aab src/HOL/Data_Structures/Tree23.thy
--- 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" |
diff -r ed5b907bbf50 -r 831f17da1aab src/HOL/Data_Structures/Tree23_Set.thy
--- 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" |
diff -r ed5b907bbf50 -r 831f17da1aab src/HOL/Library/Tree.thy
--- 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
 
diff -r ed5b907bbf50 -r 831f17da1aab src/HOL/Library/Tree_Real.thy
--- 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
diff -r ed5b907bbf50 -r 831f17da1aab src/HOL/ex/Tree23.thy
--- 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>