equal
deleted
inserted
replaced
355 subsection \<open>@{const ipl}\<close> |
355 subsection \<open>@{const ipl}\<close> |
356 |
356 |
357 text \<open>The internal path length of a tree:\<close> |
357 text \<open>The internal path length of a tree:\<close> |
358 |
358 |
359 lemma ipl_if_complete: "complete t |
359 lemma ipl_if_complete: "complete t |
360 \<Longrightarrow> ipl t = (let n = height t in 2 + n*2^n - 2^(n+1))" |
360 \<Longrightarrow> ipl t = (let h = height t in 2 + h*2^h - 2^(h+1))" |
361 proof(induction t) |
361 proof(induction t) |
362 case (Node l x r) |
362 case (Node l x r) |
363 have *: "2^(n+1) \<le> 2 + n*2^n" for n :: nat |
363 have *: "2^(n+1) \<le> 2 + n*2^n" for n :: nat |
364 by(induction n) auto |
364 by(induction n) auto |
365 have **: "(0::nat) < 2^n" for n :: nat by simp |
365 have **: "(0::nat) < 2^n" for n :: nat by simp |