# HG changeset patch # User nipkow # Date 1480958081 -3600 # Node ID f1f4ba6d02c93ab77820290e6d9c4d816c6d0919 # Parent a868c83aa66e60b452f6e20f5ca401ee2df7afb5 spelling diff -r a868c83aa66e -r f1f4ba6d02c9 src/HOL/Data_Structures/Balance.thy --- a/src/HOL/Data_Structures/Balance.thy Sun Dec 04 21:40:50 2016 +0100 +++ b/src/HOL/Data_Structures/Balance.thy Mon Dec 05 18:14:41 2016 +0100 @@ -26,7 +26,7 @@ next assume *: "\ complete t" hence "height t = min_height t + 1" - using assms min_hight_le_height[of t] + using assms min_height_le_height[of t] by(auto simp add: balanced_def complete_iff_height) hence "2 ^ min_height t \ size1 t \ size1 t < 2 ^ (min_height t + 1)" by (metis * min_height_size1 size1_height_if_incomplete) @@ -53,7 +53,7 @@ next assume *: "\ complete t" hence **: "height t = min_height t + 1" - using assms min_hight_le_height[of t] + using assms min_height_le_height[of t] by(auto simp add: balanced_def complete_iff_height) hence 0: "2 ^ min_height t < size1 t \ size1 t \ 2 ^ (min_height t + 1)" by (metis "*" min_height_size1_if_incomplete size1_height) diff -r a868c83aa66e -r f1f4ba6d02c9 src/HOL/Library/Tree.thy --- a/src/HOL/Library/Tree.thy Sun Dec 04 21:40:50 2016 +0100 +++ b/src/HOL/Library/Tree.thy Mon Dec 05 18:14:41 2016 +0100 @@ -172,7 +172,7 @@ by (induction t) auto -lemma min_hight_le_height: "min_height t \ height t" +lemma min_height_le_height: "min_height t \ height t" by(induction t) auto lemma min_height_map_tree[simp]: "min_height (map_tree f t) = min_height t" @@ -194,7 +194,7 @@ apply(induction t) apply simp apply (simp add: min_def max_def) -by (metis le_antisym le_trans min_hight_le_height) +by (metis le_antisym le_trans min_height_le_height) lemma size1_if_complete: "complete t \ size1 t = 2 ^ height t" by (induction t) auto @@ -345,7 +345,7 @@ qed hence *: "min_height t < height t'" by simp have "min_height t + 1 = height t" - using min_hight_le_height[of t] assms(1) False + using min_height_le_height[of t] assms(1) False by (simp add: complete_iff_height balanced_def) with * show ?thesis by arith qed