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