# HG changeset patch
# User nipkow
# Date 1484304110 -3600
# Node ID 266fb24c80bde60d88f54ca1d8bbe6f658b55dc9
# Parent  cea327ecb8e332f24b54ccd39a4ee436217a3a2a
tuned/minimized

diff -r cea327ecb8e3 -r 266fb24c80bd src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Thu Jan 12 15:54:13 2017 +0100
+++ b/src/HOL/Library/Tree.thy	Fri Jan 13 11:41:50 2017 +0100
@@ -1,8 +1,5 @@
 (* Author: Tobias Nipkow *)
-(* Todo:
- (min_)height of balanced trees via floorlog
- minimal path_len of balanced trees
-*)
+(* Todo: minimal ipl of balanced trees *)
 
 section \<open>Binary Tree\<close>
 
@@ -11,11 +8,8 @@
 begin
 
 datatype 'a tree =
-  is_Leaf: Leaf ("\<langle>\<rangle>") |
-  Node (left: "'a tree") (val: 'a) (right: "'a tree") ("(1\<langle>_,/ _,/ _\<rangle>)")
-  where
-    "left Leaf = Leaf"
-  | "right Leaf = Leaf"
+  Leaf ("\<langle>\<rangle>") |
+  Node "'a tree" (root_val: 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)")
 datatype_compat tree
 
 text\<open>Can be seen as counting the number of leaves rather than nodes:\<close>
@@ -61,9 +55,9 @@
 "wbalanced (Node l x r) = (abs(int(size l) - int(size r)) \<le> 1 \<and> wbalanced l \<and> wbalanced r)"
 
 text \<open>Internal path length:\<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"
+fun ipl :: "'a tree \<Rightarrow> nat" where
+"ipl Leaf = 0 " |
+"ipl (Node l _ r) = ipl l + size l + ipl r + size r"
 
 fun preorder :: "'a tree \<Rightarrow> 'a list" where
 "preorder \<langle>\<rangle> = []" |
@@ -357,12 +351,12 @@
 using [[simp_depth_limit=1]] by(induction t arbitrary: s) auto
 
 
-subsection \<open>@{const path_len}\<close>
+subsection \<open>@{const ipl}\<close>
 
 text \<open>The internal path length of a tree:\<close>
 
-lemma path_len_if_bal: "complete t
-  \<Longrightarrow> path_len t = (let n = height t in 2 + n*2^n - 2^(n+1))"
+lemma ipl_if_complete: "complete t
+  \<Longrightarrow> ipl 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