spelling
authornipkow
Mon Dec 05 18:14:41 2016 +0100 (2016-12-05)
changeset 64540f1f4ba6d02c9
parent 64539 a868c83aa66e
child 64541 3d4331b65861
spelling
src/HOL/Data_Structures/Balance.thy
src/HOL/Library/Tree.thy
     1.1 --- a/src/HOL/Data_Structures/Balance.thy	Sun Dec 04 21:40:50 2016 +0100
     1.2 +++ b/src/HOL/Data_Structures/Balance.thy	Mon Dec 05 18:14:41 2016 +0100
     1.3 @@ -26,7 +26,7 @@
     1.4  next
     1.5    assume *: "\<not> complete t"
     1.6    hence "height t = min_height t + 1"
     1.7 -    using assms min_hight_le_height[of t]
     1.8 +    using assms min_height_le_height[of t]
     1.9      by(auto simp add: balanced_def complete_iff_height)
    1.10    hence "2 ^ min_height t \<le> size1 t \<and> size1 t < 2 ^ (min_height t + 1)"
    1.11      by (metis * min_height_size1 size1_height_if_incomplete)
    1.12 @@ -53,7 +53,7 @@
    1.13  next
    1.14    assume *: "\<not> complete t"
    1.15    hence **: "height t = min_height t + 1"
    1.16 -    using assms min_hight_le_height[of t]
    1.17 +    using assms min_height_le_height[of t]
    1.18      by(auto simp add: balanced_def complete_iff_height)
    1.19    hence 0: "2 ^ min_height t < size1 t \<and> size1 t \<le> 2 ^ (min_height t + 1)"
    1.20      by (metis "*" min_height_size1_if_incomplete size1_height)
     2.1 --- a/src/HOL/Library/Tree.thy	Sun Dec 04 21:40:50 2016 +0100
     2.2 +++ b/src/HOL/Library/Tree.thy	Mon Dec 05 18:14:41 2016 +0100
     2.3 @@ -172,7 +172,7 @@
     2.4  by (induction t) auto
     2.5  
     2.6  
     2.7 -lemma min_hight_le_height: "min_height t \<le> height t"
     2.8 +lemma min_height_le_height: "min_height t \<le> height t"
     2.9  by(induction t) auto
    2.10  
    2.11  lemma min_height_map_tree[simp]: "min_height (map_tree f t) = min_height t"
    2.12 @@ -194,7 +194,7 @@
    2.13  apply(induction t)
    2.14   apply simp
    2.15  apply (simp add: min_def max_def)
    2.16 -by (metis le_antisym le_trans min_hight_le_height)
    2.17 +by (metis le_antisym le_trans min_height_le_height)
    2.18  
    2.19  lemma size1_if_complete: "complete t \<Longrightarrow> size1 t = 2 ^ height t"
    2.20  by (induction t) auto
    2.21 @@ -345,7 +345,7 @@
    2.22    qed
    2.23    hence *: "min_height t < height t'" by simp
    2.24    have "min_height t + 1 = height t"
    2.25 -    using min_hight_le_height[of t] assms(1) False
    2.26 +    using min_height_le_height[of t] assms(1) False
    2.27      by (simp add: complete_iff_height balanced_def)
    2.28    with * show ?thesis by arith
    2.29  qed