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