# HG changeset patch
# User nipkow
# Date 1484843045 -3600
# Node ID 7c340dcbc323e22b7fe3a33a98829e1e125f7bf7
# Parent  3fb4d7d002305f0b2f3503c91a2e067e10f7325f
int version slicker

diff -r 3fb4d7d00230 -r 7c340dcbc323 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Thu Jan 19 12:39:46 2017 +0100
+++ b/src/HOL/Library/Tree.thy	Thu Jan 19 17:24:05 2017 +0100
@@ -356,16 +356,13 @@
 
 text \<open>The internal path length of a tree:\<close>
 
-lemma ipl_if_complete: "complete t
-  \<Longrightarrow> ipl t = (let h = height t in 2 + h*2^h - 2^(h+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: size_if_complete Let_def)
-qed simp
+lemma ipl_if_complete_int:
+  "complete t \<Longrightarrow> int(ipl t) = (int(height t) - 2) * 2^(height t) + 2"
+apply(induction t)
+ apply simp
+apply simp
+apply (simp add: algebra_simps size_if_complete of_nat_diff)
+done
 
 
 subsection "List of entries"