src/HOL/Library/Tree_Real.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (3 months ago)
changeset 69946 494934c30f38
parent 69593 3dda49e08b9d
child 70350 571ae57313a4
permissions -rw-r--r--
improved code equations taken over from AFP
nipkow@66510
     1
(* Author: Tobias Nipkow *)
nipkow@66510
     2
nipkow@66510
     3
theory Tree_Real
nipkow@66510
     4
imports
nipkow@66510
     5
  Complex_Main
nipkow@66510
     6
  Tree
nipkow@66510
     7
begin
nipkow@66510
     8
wenzelm@68484
     9
text \<open>
wenzelm@69593
    10
  This theory is separate from \<^theory>\<open>HOL-Library.Tree\<close> because the former is discrete and
wenzelm@69593
    11
  builds on \<^theory>\<open>Main\<close> whereas this theory builds on \<^theory>\<open>Complex_Main\<close>.
wenzelm@68484
    12
\<close>
nipkow@66510
    13
nipkow@66510
    14
nipkow@66510
    15
lemma size1_height_log: "log 2 (size1 t) \<le> height t"
nipkow@66510
    16
by (simp add: log2_of_power_le size1_height)
nipkow@66510
    17
nipkow@66510
    18
lemma min_height_size1_log: "min_height t \<le> log 2 (size1 t)"
nipkow@66510
    19
by (simp add: le_log2_of_power min_height_size1)
nipkow@66510
    20
nipkow@66510
    21
lemma size1_log_if_complete: "complete t \<Longrightarrow> height t = log 2 (size1 t)"
nipkow@66510
    22
by (simp add: log2_of_power_eq size1_if_complete)
nipkow@66510
    23
nipkow@66510
    24
lemma min_height_size1_log_if_incomplete:
nipkow@66510
    25
  "\<not> complete t \<Longrightarrow> min_height t < log 2 (size1 t)"
nipkow@66510
    26
by (simp add: less_log2_of_power min_height_size1_if_incomplete)
nipkow@66510
    27
nipkow@66510
    28
nipkow@66510
    29
lemma min_height_balanced: assumes "balanced t"
nipkow@66510
    30
shows "min_height t = nat(floor(log 2 (size1 t)))"
nipkow@66510
    31
proof cases
nipkow@66510
    32
  assume *: "complete t"
nipkow@66510
    33
  hence "size1 t = 2 ^ min_height t"
nipkow@66510
    34
    by (simp add: complete_iff_height size1_if_complete)
nipkow@66510
    35
  from log2_of_power_eq[OF this] show ?thesis by linarith
nipkow@66510
    36
next
nipkow@66510
    37
  assume *: "\<not> complete t"
nipkow@66510
    38
  hence "height t = min_height t + 1"
nipkow@66510
    39
    using assms min_height_le_height[of t]
nipkow@69117
    40
    by(auto simp: balanced_def complete_iff_height)
nipkow@69117
    41
  hence "size1 t < 2 ^ (min_height t + 1)" by (metis * size1_height_if_incomplete)
nipkow@69117
    42
  from floor_log_nat_eq_if[OF min_height_size1 this] show ?thesis by simp
nipkow@66510
    43
qed
nipkow@66510
    44
nipkow@66510
    45
lemma height_balanced: assumes "balanced t"
nipkow@66510
    46
shows "height t = nat(ceiling(log 2 (size1 t)))"
nipkow@66510
    47
proof cases
nipkow@66510
    48
  assume *: "complete t"
nipkow@69117
    49
  hence "size1 t = 2 ^ height t" by (simp add: size1_if_complete)
nipkow@69117
    50
  from log2_of_power_eq[OF this] show ?thesis by linarith
nipkow@66510
    51
next
nipkow@66510
    52
  assume *: "\<not> complete t"
nipkow@66510
    53
  hence **: "height t = min_height t + 1"
nipkow@66510
    54
    using assms min_height_le_height[of t]
nipkow@66510
    55
    by(auto simp add: balanced_def complete_iff_height)
nipkow@66510
    56
  hence "size1 t \<le> 2 ^ (min_height t + 1)" by (metis size1_height)
nipkow@69117
    57
  from log2_of_power_le[OF this size1_ge0] min_height_size1_log_if_incomplete[OF *] **
nipkow@66510
    58
  show ?thesis by linarith
nipkow@66510
    59
qed
nipkow@66510
    60
nipkow@66515
    61
lemma balanced_Node_if_wbal1:
nipkow@66515
    62
assumes "balanced l" "balanced r" "size l = size r + 1"
nipkow@66515
    63
shows "balanced \<langle>l, x, r\<rangle>"
nipkow@66515
    64
proof -
nipkow@68998
    65
  from assms(3) have [simp]: "size1 l = size1 r + 1" by(simp add: size1_size)
nipkow@66515
    66
  have "nat \<lceil>log 2 (1 + size1 r)\<rceil> \<ge> nat \<lceil>log 2 (size1 r)\<rceil>"
nipkow@66515
    67
    by(rule nat_mono[OF ceiling_mono]) simp
nipkow@66515
    68
  hence 1: "height(Node l x r) = nat \<lceil>log 2 (1 + size1 r)\<rceil> + 1"
nipkow@66515
    69
    using height_balanced[OF assms(1)] height_balanced[OF assms(2)]
nipkow@66515
    70
    by (simp del: nat_ceiling_le_eq add: max_def)
nipkow@66515
    71
  have "nat \<lfloor>log 2 (1 + size1 r)\<rfloor> \<ge> nat \<lfloor>log 2 (size1 r)\<rfloor>"
nipkow@66515
    72
    by(rule nat_mono[OF floor_mono]) simp
nipkow@66515
    73
  hence 2: "min_height(Node l x r) = nat \<lfloor>log 2 (size1 r)\<rfloor> + 1"
nipkow@66515
    74
    using min_height_balanced[OF assms(1)] min_height_balanced[OF assms(2)]
nipkow@66515
    75
    by (simp)
nipkow@68998
    76
  have "size1 r \<ge> 1" by(simp add: size1_size)
nipkow@66515
    77
  then obtain i where i: "2 ^ i \<le> size1 r" "size1 r < 2 ^ (i + 1)"
nipkow@66515
    78
    using ex_power_ivl1[of 2 "size1 r"] by auto
nipkow@66515
    79
  hence i1: "2 ^ i < size1 r + 1" "size1 r + 1 \<le> 2 ^ (i + 1)" by auto
nipkow@66515
    80
  from 1 2 floor_log_nat_eq_if[OF i] ceiling_log_nat_eq_if[OF i1]
nipkow@66515
    81
  show ?thesis by(simp add:balanced_def)
nipkow@66515
    82
qed
nipkow@66515
    83
nipkow@66515
    84
lemma balanced_sym: "balanced \<langle>l, x, r\<rangle> \<Longrightarrow> balanced \<langle>r, y, l\<rangle>"
nipkow@66515
    85
by(auto simp: balanced_def)
nipkow@66515
    86
nipkow@66515
    87
lemma balanced_Node_if_wbal2:
nipkow@66515
    88
assumes "balanced l" "balanced r" "abs(int(size l) - int(size r)) \<le> 1"
nipkow@66515
    89
shows "balanced \<langle>l, x, r\<rangle>"
nipkow@66515
    90
proof -
nipkow@66515
    91
  have "size l = size r \<or> (size l = size r + 1 \<or> size r = size l + 1)" (is "?A \<or> ?B")
nipkow@66515
    92
    using assms(3) by linarith
nipkow@66515
    93
  thus ?thesis
nipkow@66515
    94
  proof
nipkow@66515
    95
    assume "?A"
nipkow@66515
    96
    thus ?thesis using assms(1,2)
nipkow@66515
    97
      apply(simp add: balanced_def min_def max_def)
nipkow@66515
    98
      by (metis assms(1,2) balanced_optimal le_antisym le_less)
nipkow@66515
    99
  next
nipkow@66515
   100
    assume "?B"
nipkow@66515
   101
    thus ?thesis
nipkow@66515
   102
      by (meson assms(1,2) balanced_sym balanced_Node_if_wbal1)
nipkow@66515
   103
  qed
nipkow@66515
   104
qed
nipkow@66515
   105
nipkow@66515
   106
lemma balanced_if_wbalanced: "wbalanced t \<Longrightarrow> balanced t"
nipkow@66515
   107
proof(induction t)
nipkow@66515
   108
  case Leaf show ?case by (simp add: balanced_def)
nipkow@66515
   109
next
nipkow@66515
   110
  case (Node l x r)
nipkow@66515
   111
  thus ?case by(simp add: balanced_Node_if_wbal2)
nipkow@66515
   112
qed
nipkow@66515
   113
nipkow@67399
   114
end