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