more lemmas, tuned proofs
authornipkow
Tue Nov 29 10:53:52 2016 +0100 (2016-11-29)
changeset 64533172f3a047f4a
parent 64530 a720c3911308
child 64534 ff59fe6b6f6a
more lemmas, tuned proofs
src/HOL/Data_Structures/Balance.thy
src/HOL/Library/Tree.thy
     1.1 --- a/src/HOL/Data_Structures/Balance.thy	Mon Nov 28 15:09:23 2016 +0100
     1.2 +++ b/src/HOL/Data_Structures/Balance.thy	Tue Nov 29 10:53:52 2016 +0100
     1.3 @@ -8,6 +8,63 @@
     1.4    "~~/src/HOL/Library/Tree"
     1.5  begin
     1.6  
     1.7 +(* The following two lemmas should go into theory \<open>Tree\<close>, except that that
     1.8 +theory would then depend on \<open>Complex_Main\<close>. *)
     1.9 +
    1.10 +lemma min_height_balanced: assumes "balanced t"
    1.11 +shows "min_height t = nat(floor(log 2 (size1 t)))"
    1.12 +proof cases
    1.13 +  assume *: "complete t"
    1.14 +  hence "size1 t = 2 ^ min_height t"
    1.15 +    by (simp add: complete_iff_height size1_if_complete)
    1.16 +  hence "size1 t = 2 powr min_height t"
    1.17 +    using * by (simp add: powr_realpow)
    1.18 +  hence "min_height t = log 2 (size1 t)"
    1.19 +    by simp
    1.20 +  thus ?thesis
    1.21 +    by linarith
    1.22 +next
    1.23 +  assume *: "\<not> complete t"
    1.24 +  hence "height t = min_height t + 1"
    1.25 +    using assms min_hight_le_height[of t]
    1.26 +    by(auto simp add: balanced_def complete_iff_height)
    1.27 +  hence "2 ^ min_height t \<le> size1 t \<and> size1 t < 2 ^ (min_height t + 1)"
    1.28 +    by (metis * min_height_size1 size1_height_if_incomplete)
    1.29 +  hence "2 powr min_height t \<le> size1 t \<and> size1 t < 2 powr (min_height t + 1)"
    1.30 +    by(simp only: powr_realpow)
    1.31 +      (metis of_nat_less_iff of_nat_le_iff of_nat_numeral of_nat_power)
    1.32 +  hence "min_height t \<le> log 2 (size1 t) \<and> log 2 (size1 t) < min_height t + 1"
    1.33 +    by(simp add: log_less_iff le_log_iff)
    1.34 +  thus ?thesis by linarith
    1.35 +qed
    1.36 +
    1.37 +lemma height_balanced: assumes "balanced t"
    1.38 +shows "height t = nat(ceiling(log 2 (size1 t)))"
    1.39 +proof cases
    1.40 +  assume *: "complete t"
    1.41 +  hence "size1 t = 2 ^ height t"
    1.42 +    by (simp add: size1_if_complete)
    1.43 +  hence "size1 t = 2 powr height t"
    1.44 +    using * by (simp add: powr_realpow)
    1.45 +  hence "height t = log 2 (size1 t)"
    1.46 +    by simp
    1.47 +  thus ?thesis
    1.48 +    by linarith
    1.49 +next
    1.50 +  assume *: "\<not> complete t"
    1.51 +  hence **: "height t = min_height t + 1"
    1.52 +    using assms min_hight_le_height[of t]
    1.53 +    by(auto simp add: balanced_def complete_iff_height)
    1.54 +  hence 0: "2 ^ min_height t < size1 t \<and> size1 t \<le> 2 ^ (min_height t + 1)"
    1.55 +    by (metis "*" min_height_size1_if_incomplete size1_height)
    1.56 +  hence "2 powr min_height t < size1 t \<and> size1 t \<le> 2 powr (min_height t + 1)"
    1.57 +    by(simp only: powr_realpow)
    1.58 +      (metis of_nat_less_iff of_nat_le_iff of_nat_numeral of_nat_power)
    1.59 +  hence "min_height t < log 2 (size1 t) \<and> log 2 (size1 t) \<le> min_height t + 1"
    1.60 +    by(simp add: log_le_iff less_log_iff)
    1.61 +  thus ?thesis using ** by linarith
    1.62 +qed
    1.63 +
    1.64  (* mv *)
    1.65  
    1.66  text \<open>The lemmas about \<open>floor\<close> and \<open>ceiling\<close> of \<open>log 2\<close> should be generalized
     2.1 --- a/src/HOL/Library/Tree.thy	Mon Nov 28 15:09:23 2016 +0100
     2.2 +++ b/src/HOL/Library/Tree.thy	Tue Nov 29 10:53:52 2016 +0100
     2.3 @@ -144,29 +144,29 @@
     2.4  lemma height_le_size_tree: "height t \<le> size (t::'a tree)"
     2.5  by (induction t) auto
     2.6  
     2.7 -lemma size1_height: "size t + 1 \<le> 2 ^ height (t::'a tree)"
     2.8 +lemma size1_height: "size1 t \<le> 2 ^ height (t::'a tree)"
     2.9  proof(induction t)
    2.10    case (Node l a r)
    2.11    show ?case
    2.12    proof (cases "height l \<le> height r")
    2.13      case True
    2.14 -    have "size(Node l a r) + 1 = (size l + 1) + (size r + 1)" by simp
    2.15 -    also have "size l + 1 \<le> 2 ^ height l" by(rule Node.IH(1))
    2.16 -    also have "size r + 1 \<le> 2 ^ height r" by(rule Node.IH(2))
    2.17 +    have "size1(Node l a r) = size1 l + size1 r" by simp
    2.18 +    also have "size1 l \<le> 2 ^ height l" by(rule Node.IH(1))
    2.19 +    also have "size1 r \<le> 2 ^ height r" by(rule Node.IH(2))
    2.20      also have "(2::nat) ^ height l \<le> 2 ^ height r" using True by simp
    2.21      finally show ?thesis using True by (auto simp: max_def mult_2)
    2.22    next
    2.23      case False
    2.24 -    have "size(Node l a r) + 1 = (size l + 1) + (size r + 1)" by simp
    2.25 -    also have "size l + 1 \<le> 2 ^ height l" by(rule Node.IH(1))
    2.26 -    also have "size r + 1 \<le> 2 ^ height r" by(rule Node.IH(2))
    2.27 +    have "size1(Node l a r) = size1 l + size1 r" by simp
    2.28 +    also have "size1 l \<le> 2 ^ height l" by(rule Node.IH(1))
    2.29 +    also have "size1 r \<le> 2 ^ height r" by(rule Node.IH(2))
    2.30      also have "(2::nat) ^ height r \<le> 2 ^ height l" using False by simp
    2.31      finally show ?thesis using False by (auto simp: max_def mult_2)
    2.32    qed
    2.33  qed simp
    2.34  
    2.35  corollary size_height: "size t \<le> 2 ^ height (t::'a tree) - 1"
    2.36 -using size1_height[of t] by(arith)
    2.37 +using size1_height[of t, unfolded size1_def] by(arith)
    2.38  
    2.39  lemma height_subtrees: "s \<in> subtrees t \<Longrightarrow> height s \<le> height t"
    2.40  by (induction t) auto
    2.41 @@ -178,12 +178,12 @@
    2.42  lemma min_height_map_tree[simp]: "min_height (map_tree f t) = min_height t"
    2.43  by (induction t) auto
    2.44  
    2.45 -lemma min_height_le_size1: "2 ^ min_height t \<le> size t + 1"
    2.46 +lemma min_height_size1: "2 ^ min_height t \<le> size1 t"
    2.47  proof(induction t)
    2.48    case (Node l a r)
    2.49    have "(2::nat) ^ min_height (Node l a r) \<le> 2 ^ min_height l + 2 ^ min_height r"
    2.50      by (simp add: min_def)
    2.51 -  also have "\<dots> \<le> size(Node l a r) + 1" using Node.IH by simp
    2.52 +  also have "\<dots> \<le> size1(Node l a r)" using Node.IH by simp
    2.53    finally show ?case .
    2.54  qed simp
    2.55  
    2.56 @@ -202,102 +202,106 @@
    2.57  lemma size_if_complete: "complete t \<Longrightarrow> size t = 2 ^ height t - 1"
    2.58  using size1_if_complete[simplified size1_def] by fastforce
    2.59  
    2.60 -lemma complete_if_size: "size t = 2 ^ height t - 1 \<Longrightarrow> complete t"
    2.61 +lemma complete_if_size1_height: "size1 t = 2 ^ height t \<Longrightarrow> complete t"
    2.62  proof (induct "height t" arbitrary: t)
    2.63 -  case 0 thus ?case by (simp add: size_0_iff_Leaf)
    2.64 +  case 0 thus ?case by (simp add: height_0_iff_Leaf)
    2.65  next
    2.66    case (Suc h)
    2.67    hence "t \<noteq> Leaf" by auto
    2.68    then obtain l a r where [simp]: "t = Node l a r"
    2.69      by (auto simp: neq_Leaf_iff)
    2.70    have 1: "height l \<le> h" and 2: "height r \<le> h" using Suc(2) by(auto)
    2.71 -  have 3: "~ height l < h"
    2.72 +  have 3: "\<not> height l < h"
    2.73    proof
    2.74      assume 0: "height l < h"
    2.75 -    have "size t = size l + (size r + 1)" by simp
    2.76 -    also note size_height[of l]
    2.77 +    have "size1 t = size1 l + size1 r" by simp
    2.78 +    also note size1_height[of l]
    2.79      also note size1_height[of r]
    2.80 -    also have "(2::nat) ^ height l - 1 < 2 ^ h - 1"
    2.81 +    also have "(2::nat) ^ height l < 2 ^ h"
    2.82          using 0 by (simp add: diff_less_mono)
    2.83      also have "(2::nat) ^ height r \<le> 2 ^ h" using 2 by simp
    2.84 -    also have "(2::nat) ^ h - 1 + 2 ^ h = 2 ^ (Suc h) - 1" by (simp)
    2.85 -    also have "\<dots> = size t" using Suc(2,3) by simp
    2.86 +    also have "(2::nat) ^ h  + 2 ^ h = 2 ^ (Suc h)" by (simp)
    2.87 +    also have "\<dots> = size1 t" using Suc(2,3) by simp
    2.88      finally show False by (simp add: diff_le_mono)
    2.89    qed
    2.90    have 4: "~ height r < h"
    2.91    proof
    2.92      assume 0: "height r < h"
    2.93 -    have "size t = (size l + 1) + size r" by simp
    2.94 -    also note size_height[of r]
    2.95 +    have "size1 t = size1 l + size1 r" by simp
    2.96 +    also note size1_height[of r]
    2.97      also note size1_height[of l]
    2.98 -    also have "(2::nat) ^ height r - 1 < 2 ^ h - 1"
    2.99 +    also have "(2::nat) ^ height r < 2 ^ h"
   2.100          using 0 by (simp add: diff_less_mono)
   2.101      also have "(2::nat) ^ height l \<le> 2 ^ h" using 1 by simp
   2.102 -    also have "(2::nat) ^ h + (2 ^ h - 1) = 2 ^ (Suc h) - 1" by (simp)
   2.103 -    also have "\<dots> = size t" using Suc(2,3) by simp
   2.104 +    also have "(2::nat) ^ h +2 ^ h = 2 ^ (Suc h)" by (simp)
   2.105 +    also have "\<dots> = size1 t" using Suc(2,3) by simp
   2.106      finally show False by (simp add: diff_le_mono)
   2.107    qed
   2.108    from 1 2 3 4 have *: "height l = h" "height r = h" by linarith+
   2.109 -  hence "size l = 2 ^ height l - 1" "size r = 2 ^ height r - 1"
   2.110 -    using Suc(3) size_height[of l] size_height[of r] by (auto)
   2.111 +  hence "size1 l = 2 ^ height l" "size1 r = 2 ^ height r"
   2.112 +    using Suc(3) size1_height[of l] size1_height[of r] by (auto)
   2.113    with * Suc(1) show ?case by simp
   2.114  qed
   2.115  
   2.116 -lemma complete_iff_size: "complete t \<longleftrightarrow> size t = 2 ^ height t - 1"
   2.117 -using complete_if_size size_if_complete by blast
   2.118 -
   2.119 -text\<open>A better lower bound for incomplete trees:\<close>
   2.120 +text\<open>The following proof involves \<open>\<ge>\<close>/\<open>>\<close> chains rather than the standard
   2.121 +\<open>\<le>\<close>/\<open><\<close> chains. To chain the elements together the transitivity rules \<open>xtrans\<close>
   2.122 +are used.\<close>
   2.123  
   2.124 -lemma min_height_le_size_if_incomplete:
   2.125 -  "\<not> complete t \<Longrightarrow> 2 ^ min_height t \<le> size t"
   2.126 -proof(induction t)
   2.127 -  case Leaf thus ?case by simp
   2.128 +lemma complete_if_size1_min_height: "size1 t = 2 ^ min_height t \<Longrightarrow> complete t"
   2.129 +proof (induct "min_height t" arbitrary: t)
   2.130 +  case 0 thus ?case by (simp add: size_0_iff_Leaf size1_def)
   2.131  next
   2.132 -  case (Node l a r)
   2.133 -  show ?case (is "?l \<le> ?r")
   2.134 -  proof (cases "complete l")
   2.135 -    case l: True thus ?thesis
   2.136 -    proof (cases "complete r")
   2.137 -      case r: True
   2.138 -      have "height l \<noteq> height r" using Node.prems l r by simp
   2.139 -      hence "?l < 2 ^ min_height l + 2 ^ min_height r"
   2.140 -        using l r by (simp add: min_def complete_iff_height)
   2.141 -      also have "\<dots> = (size l + 1) + (size r + 1)"
   2.142 -        using l r size_if_complete[where ?'a = 'a]
   2.143 -        by (simp add: complete_iff_height)
   2.144 -      also have "\<dots> \<le> ?r + 1" by simp
   2.145 -      finally show ?thesis by arith
   2.146 -    next
   2.147 -      case r: False
   2.148 -      have "?l \<le> 2 ^ min_height l + 2 ^ min_height r" by (simp add: min_def)
   2.149 -      also have "\<dots> \<le> size l + 1 + size r"
   2.150 -        using Node.IH(2)[OF r] l size_if_complete[where ?'a = 'a]
   2.151 -        by (simp add: complete_iff_height)
   2.152 -      also have "\<dots> = ?r" by simp
   2.153 -      finally show ?thesis .
   2.154 -    qed
   2.155 -  next
   2.156 -    case l: False thus ?thesis
   2.157 -    proof (cases "complete r")
   2.158 -      case r: True
   2.159 -      have "?l \<le> 2 ^ min_height l + 2 ^ min_height r" by (simp add: min_def)
   2.160 -      also have "\<dots> \<le> size l + (size r + 1)"
   2.161 -        using Node.IH(1)[OF l] r size_if_complete[where ?'a = 'a]
   2.162 -        by (simp add: complete_iff_height)
   2.163 -      also have "\<dots> = ?r" by simp
   2.164 -      finally show ?thesis .
   2.165 -    next
   2.166 -      case r: False
   2.167 -      have "?l \<le> 2 ^ min_height l + 2 ^ min_height r"
   2.168 -        by (simp add: min_def)
   2.169 -      also have "\<dots> \<le> size l + size r"
   2.170 -        using Node.IH(1)[OF l] Node.IH(2)[OF r] by (simp)
   2.171 -      also have "\<dots> \<le> ?r" by simp
   2.172 -      finally show ?thesis .
   2.173 -    qed
   2.174 +  case (Suc h)
   2.175 +  hence "t \<noteq> Leaf" by auto
   2.176 +  then obtain l a r where [simp]: "t = Node l a r"
   2.177 +    by (auto simp: neq_Leaf_iff)
   2.178 +  have 1: "h \<le> min_height l" and 2: "h \<le> min_height r" using Suc(2) by(auto)
   2.179 +  have 3: "\<not> h < min_height l"
   2.180 +  proof
   2.181 +    assume 0: "h < min_height l"
   2.182 +    have "size1 t = size1 l + size1 r" by simp
   2.183 +    also note min_height_size1[of l]
   2.184 +    also(xtrans) note min_height_size1[of r]
   2.185 +    also(xtrans) have "(2::nat) ^ min_height l > 2 ^ h"
   2.186 +        using 0 by (simp add: diff_less_mono)
   2.187 +    also(xtrans) have "(2::nat) ^ min_height r \<ge> 2 ^ h" using 2 by simp
   2.188 +    also(xtrans) have "(2::nat) ^ h + 2 ^ h = 2 ^ (Suc h)" by (simp)
   2.189 +    also have "\<dots> = size1 t" using Suc(2,3) by simp
   2.190 +    finally show False by (simp add: diff_le_mono)
   2.191    qed
   2.192 +  have 4: "\<not> h < min_height r"
   2.193 +  proof
   2.194 +    assume 0: "h < min_height r"
   2.195 +    have "size1 t = size1 l + size1 r" by simp
   2.196 +    also note min_height_size1[of l]
   2.197 +    also(xtrans) note min_height_size1[of r]
   2.198 +    also(xtrans) have "(2::nat) ^ min_height r > 2 ^ h"
   2.199 +        using 0 by (simp add: diff_less_mono)
   2.200 +    also(xtrans) have "(2::nat) ^ min_height l \<ge> 2 ^ h" using 1 by simp
   2.201 +    also(xtrans) have "(2::nat) ^ h + 2 ^ h = 2 ^ (Suc h)" by (simp)
   2.202 +    also have "\<dots> = size1 t" using Suc(2,3) by simp
   2.203 +    finally show False by (simp add: diff_le_mono)
   2.204 +  qed
   2.205 +  from 1 2 3 4 have *: "min_height l = h" "min_height r = h" by linarith+
   2.206 +  hence "size1 l = 2 ^ min_height l" "size1 r = 2 ^ min_height r"
   2.207 +    using Suc(3) min_height_size1[of l] min_height_size1[of r] by (auto)
   2.208 +  with * Suc(1) show ?case
   2.209 +    by (simp add: complete_iff_height)
   2.210  qed
   2.211  
   2.212 +lemma complete_iff_size1: "complete t \<longleftrightarrow> size1 t = 2 ^ height t"
   2.213 +using complete_if_size1_height size1_if_complete by blast
   2.214 +
   2.215 +text\<open>Better bounds for incomplete trees:\<close>
   2.216 +
   2.217 +lemma size1_height_if_incomplete:
   2.218 +  "\<not> complete t \<Longrightarrow> size1 t < 2 ^ height t"
   2.219 +by (meson antisym_conv complete_iff_size1 not_le size1_height)
   2.220 +
   2.221 +lemma min_height_size1_if_incomplete:
   2.222 +  "\<not> complete t \<Longrightarrow> 2 ^ min_height t < size1 t"
   2.223 +by (metis complete_if_size1_min_height le_less min_height_size1)
   2.224 +
   2.225  
   2.226  subsection \<open>@{const balanced}\<close>
   2.227  
   2.228 @@ -332,10 +336,10 @@
   2.229    case False
   2.230    have "(2::nat) ^ min_height t < 2 ^ height t'"
   2.231    proof -
   2.232 -    have "(2::nat) ^ min_height t \<le> size t"
   2.233 -      by(rule min_height_le_size_if_incomplete[OF False])
   2.234 -    also note assms(2)
   2.235 -    also have "size t' \<le> 2 ^ height t' - 1"  by(rule size_height)
   2.236 +    have "(2::nat) ^ min_height t < size1 t"
   2.237 +      by(rule min_height_size1_if_incomplete[OF False])
   2.238 +    also have "size1 t \<le> size1 t'" using assms(2) by (simp add: size1_def)
   2.239 +    also have "size1 t' \<le> 2 ^ height t'"  by(rule size1_height)
   2.240      finally show ?thesis
   2.241        using power_eq_0_iff[of "2::nat" "height t'"] by linarith
   2.242    qed