author nipkow Thu, 01 Sep 2016 17:44:21 +0200 changeset 63756 6b6bf5c0f9c1 parent 63754 23b013b6b2fb (current diff) parent 63755 182c111190e5 (diff) child 63758 20ef5c1291da
merged
```--- a/src/HOL/Data_Structures/Balance_List.thy	Thu Sep 01 17:35:17 2016 +0200
+++ b/src/HOL/Data_Structures/Balance_List.thy	Thu Sep 01 17:44:21 2016 +0200
@@ -20,7 +20,8 @@
definition "balance xs = fst (bal xs (length xs))"

lemma bal_inorder:
-  "bal xs n = (t,ys) \<Longrightarrow> n \<le> length xs \<Longrightarrow> inorder t = take n xs \<and> ys = drop n xs"
+  "\<lbrakk> bal xs n = (t,ys); n \<le> length xs \<rbrakk>
+  \<Longrightarrow> inorder t = take n xs \<and> ys = drop n xs"
proof(induction xs n arbitrary: t ys rule: bal.induct)
case (1 xs n) show ?case
proof cases
@@ -112,14 +113,14 @@
qed

lemma balanced_bal:
-  assumes "bal xs n = (t,ys)" shows "height t - min_height t \<le> 1"
+  assumes "bal xs n = (t,ys)" shows "balanced t"
proof -
have "floorlog 2 n \<le> floorlog 2 (n+1)" by (rule floorlog_mono) auto
thus ?thesis
using bal_height[OF assms] bal_min_height[OF assms] by arith
qed

-corollary balanced_balance: "height(balance xs) - min_height(balance xs) \<le> 1"
+corollary balanced_balance: "balanced (balance xs)"
by (metis balance_def balanced_bal prod.collapse)

end```
```--- a/src/HOL/Library/Tree.thy	Thu Sep 01 17:35:17 2016 +0200
+++ b/src/HOL/Library/Tree.thy	Thu Sep 01 17:44:21 2016 +0200
@@ -1,4 +1,8 @@
(* Author: Tobias Nipkow *)
+(* Todo:
+ size t = 2^h - 1 \<Longrightarrow> complete t
+ (min_)height of balanced trees via floorlog
+*)

section \<open>Binary Tree\<close>

@@ -85,6 +89,9 @@
qed
qed simp

+corollary size_height: "size t \<le> 2 ^ height (t::'a tree) - 1"
+using size1_height[of t] by(arith)
+

fun min_height :: "'a tree \<Rightarrow> nat" where
"min_height Leaf = 0" |
@@ -106,23 +113,114 @@
qed simp

-subsection "Balanced"
+subsection \<open>Complete\<close>

-fun balanced :: "'a tree \<Rightarrow> bool" where
-"balanced Leaf = True" |
-"balanced (Node l x r) = (balanced l \<and> balanced r \<and> height l = height r)"
+fun complete :: "'a tree \<Rightarrow> bool" where
+"complete Leaf = True" |
+"complete (Node l x r) = (complete l \<and> complete r \<and> height l = height r)"

-lemma balanced_iff_min_height: "balanced t \<longleftrightarrow> (min_height t = height t)"
+lemma complete_iff_height: "complete t \<longleftrightarrow> (min_height t = height t)"
apply(induction t)
apply simp
by (metis le_antisym le_trans min_hight_le_height)

-lemma balanced_size1: "balanced t \<Longrightarrow> size1 t = 2 ^ height t"
+lemma complete_size1: "complete t \<Longrightarrow> size1 t = 2 ^ height t"
by (induction t) auto

-lemma balanced_size: "balanced t \<Longrightarrow> size t = 2 ^ height t - 1"
-using balanced_size1[simplified size1_def] by fastforce
+lemma size_if_complete: "complete t \<Longrightarrow> size t = 2 ^ height t - 1"
+using complete_size1[simplified size1_def] by fastforce
+
+text\<open>A better lower bound for incomplete trees:\<close>
+
+lemma min_height_le_size_if_incomplete:
+  "\<not> complete t \<Longrightarrow> 2 ^ min_height t \<le> size t"
+proof(induction t)
+  case Leaf thus ?case by simp
+next
+  case (Node l a r)
+  show ?case (is "?l \<le> ?r")
+  proof (cases "complete l")
+    case l: True thus ?thesis
+    proof (cases "complete r")
+      case r: True
+      have "height l \<noteq> height r" using Node.prems l r by simp
+      hence "?l < 2 ^ min_height l + 2 ^ min_height r"
+        using l r by (simp add: min_def complete_iff_height)
+      also have "\<dots> = (size l + 1) + (size r + 1)"
+        using l r size_if_complete[where ?'a = 'a]
+      also have "\<dots> \<le> ?r + 1" by simp
+      finally show ?thesis by arith
+    next
+      case r: False
+      have "?l \<le> 2 ^ min_height l + 2 ^ min_height r" by (simp add: min_def)
+      also have "\<dots> \<le> size l + 1 + size r"
+        using Node.IH(2)[OF r] l size_if_complete[where ?'a = 'a]
+      also have "\<dots> = ?r" by simp
+      finally show ?thesis .
+    qed
+  next
+    case l: False thus ?thesis
+    proof (cases "complete r")
+      case r: True
+      have "?l \<le> 2 ^ min_height l + 2 ^ min_height r" by (simp add: min_def)
+      also have "\<dots> \<le> size l + (size r + 1)"
+        using Node.IH(1)[OF l] r size_if_complete[where ?'a = 'a]
+      also have "\<dots> = ?r" by simp
+      finally show ?thesis .
+    next
+      case r: False
+      have "?l \<le> 2 ^ min_height l + 2 ^ min_height r"
+      also have "\<dots> \<le> size l + size r"
+        using Node.IH(1)[OF l] Node.IH(2)[OF r] by (simp)
+      also have "\<dots> \<le> ?r" by simp
+      finally show ?thesis .
+    qed
+  qed
+qed
+
+
+subsection \<open>Balanced\<close>
+
+abbreviation "balanced t \<equiv> (height t - min_height t \<le> 1)"
+
+text\<open>Balanced trees have optimal height:\<close>
+
+lemma balanced_optimal:
+fixes t :: "'a tree" and t' :: "'b tree"
+assumes "balanced t" "size t \<le> size t'" shows "height t \<le> height t'"
+proof (cases "complete t")
+  case True
+  have "(2::nat) ^ height t - 1 \<le> 2 ^ height t' - 1"
+  proof -
+    have "(2::nat) ^ height t - 1 = size t"
+      using True by (simp add: complete_iff_height size_if_complete)
+    also note assms(2)
+    also have "size t' \<le> 2 ^ height t' - 1" by (rule size_height)
+    finally show ?thesis .
+  qed
+  thus ?thesis by (simp add: le_diff_iff)
+next
+  case False
+  have "(2::nat) ^ min_height t < 2 ^ height t'"
+  proof -
+    have "(2::nat) ^ min_height t \<le> size t"
+      by(rule min_height_le_size_if_incomplete[OF False])
+    also note assms(2)
+    also have "size t' \<le> 2 ^ height t' - 1"  by(rule size_height)
+    finally show ?thesis
+      using power_eq_0_iff[of "2::nat" "height t'"] by linarith
+  qed
+  hence *: "min_height t < height t'" by simp
+  have "min_height t + 1 = height t"
+    using min_hight_le_height[of t] assms(1) False
+  with * show ?thesis by arith
+qed

subsection \<open>Path length\<close>
@@ -133,7 +231,7 @@
"path_len Leaf = 0 " |
"path_len (Node l _ r) = path_len l + size l + path_len r + size r"

-lemma path_len_if_bal: "balanced t
+lemma path_len_if_bal: "complete t
\<Longrightarrow> path_len t = (let n = height t in 2 + n*2^n - 2^(n+1))"
proof(induction t)
case (Node l x r)
@@ -141,7 +239,7 @@
by(induction n) auto
have **: "(0::nat) < 2^n" for n :: nat by simp
let ?h = "height r"
-  show ?case using Node *[of ?h] **[of ?h] by (simp add: balanced_size Let_def)
+  show ?case using Node *[of ?h] **[of ?h] by (simp add: size_if_complete Let_def)
qed simp

```