added min_height
authornipkow
Fri Aug 05 10:05:50 2016 +0200 (2016-08-05)
changeset 63598025d6e52d86f
parent 63597 bef0277ec73b
child 63599 f560147710fb
added min_height
src/HOL/Library/Tree.thy
     1.1 --- a/src/HOL/Library/Tree.thy	Fri Aug 05 09:30:20 2016 +0200
     1.2 +++ b/src/HOL/Library/Tree.thy	Fri Aug 05 10:05:50 2016 +0200
     1.3 @@ -83,12 +83,38 @@
     1.4  qed simp
     1.5  
     1.6  
     1.7 +fun min_height :: "'a tree \<Rightarrow> nat" where
     1.8 +"min_height Leaf = 0" |
     1.9 +"min_height (Node l _ r) = min (min_height l) (min_height r) + 1"
    1.10 +
    1.11 +lemma min_hight_le_height: "min_height t \<le> height t"
    1.12 +by(induction t) auto
    1.13 +
    1.14 +lemma min_height_map_tree[simp]: "min_height (map_tree f t) = min_height t"
    1.15 +by (induction t) auto
    1.16 +
    1.17 +lemma min_height_le_size1: "2 ^ min_height t \<le> size t + 1"
    1.18 +proof(induction t)
    1.19 +  case (Node l a r)
    1.20 +  have "(2::nat) ^ min_height (Node l a r) \<le> 2 ^ min_height l + 2 ^ min_height r"
    1.21 +    by (simp add: min_def)
    1.22 +  also have "\<dots> \<le> size(Node l a r) + 1" using Node.IH by simp
    1.23 +  finally show ?case .
    1.24 +qed simp
    1.25 +
    1.26 +
    1.27  subsection "Balanced"
    1.28  
    1.29  fun balanced :: "'a tree \<Rightarrow> bool" where
    1.30  "balanced Leaf = True" |
    1.31  "balanced (Node l x r) = (balanced l \<and> balanced r \<and> height l = height r)"
    1.32  
    1.33 +lemma balanced_iff_min_height: "balanced t \<longleftrightarrow> (min_height t = height t)"
    1.34 +apply(induction t)
    1.35 + apply simp
    1.36 +apply (simp add: min_def max_def)
    1.37 +by (metis le_antisym le_trans min_hight_le_height)
    1.38 +
    1.39  lemma balanced_size1: "balanced t \<Longrightarrow> size1 t = 2 ^ height t"
    1.40  by (induction t) auto
    1.41