# HG changeset patch
# User nipkow
# Date 1467988711 -7200
# Node ID 9fe2d9dc095eef434e6905ddece29b248065b4a2
# Parent  def97df48390daca8d829f9f8eb9f36346e3cdaf
added path_len

diff -r def97df48390 -r 9fe2d9dc095e src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Thu Jul 07 18:08:10 2016 +0200
+++ b/src/HOL/Library/Tree.thy	Fri Jul 08 16:38:31 2016 +0200
@@ -96,6 +96,26 @@
 using balanced_size1[simplified size1_def] by fastforce
 
 
+subsection \<open>Path length\<close>
+
+text \<open>The internal path length of a tree:\<close>
+
+fun path_len :: "'a tree \<Rightarrow> nat" where
+"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
+  \<Longrightarrow> path_len t = (let n = height t in 2 + n*2^n - 2^(n+1))"
+proof(induction t)
+  case (Node l x r)
+  have *: "2^(n+1) \<le> 2 + n*2^n" for n :: nat
+    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)
+qed simp
+
+
 subsection "The set of subtrees"
 
 fun subtrees :: "'a tree \<Rightarrow> 'a tree set" where