# HG changeset patch
# User nipkow
# Date 1470384350 -7200
# Node ID 025d6e52d86f254be5423b83a45ddd240224f28e
# Parent  bef0277ec73b73cf2df4e9b3a0b2a0f541b9e5fe
added min_height

diff -r bef0277ec73b -r 025d6e52d86f src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Fri Aug 05 09:30:20 2016 +0200
+++ b/src/HOL/Library/Tree.thy	Fri Aug 05 10:05:50 2016 +0200
@@ -83,12 +83,38 @@
 qed simp
 
 
+fun min_height :: "'a tree \<Rightarrow> nat" where
+"min_height Leaf = 0" |
+"min_height (Node l _ r) = min (min_height l) (min_height r) + 1"
+
+lemma min_hight_le_height: "min_height t \<le> height t"
+by(induction t) auto
+
+lemma min_height_map_tree[simp]: "min_height (map_tree f t) = min_height t"
+by (induction t) auto
+
+lemma min_height_le_size1: "2 ^ min_height t \<le> size t + 1"
+proof(induction t)
+  case (Node l a r)
+  have "(2::nat) ^ min_height (Node l a r) \<le> 2 ^ min_height l + 2 ^ min_height r"
+    by (simp add: min_def)
+  also have "\<dots> \<le> size(Node l a r) + 1" using Node.IH by simp
+  finally show ?case .
+qed simp
+
+
 subsection "Balanced"
 
 fun balanced :: "'a tree \<Rightarrow> bool" where
 "balanced Leaf = True" |
 "balanced (Node l x r) = (balanced l \<and> balanced r \<and> height l = height r)"
 
+lemma balanced_iff_min_height: "balanced t \<longleftrightarrow> (min_height t = height t)"
+apply(induction t)
+ apply simp
+apply (simp add: min_def max_def)
+by (metis le_antisym le_trans min_hight_le_height)
+
 lemma balanced_size1: "balanced t \<Longrightarrow> size1 t = 2 ^ height t"
 by (induction t) auto