# 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 \The internal path length of a tree:\ -lemma ipl_if_complete: "complete t - \ 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) \ 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 \ 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"