Theory VEBT_Space

(*by Ammer*)
theory VEBT_Space imports VEBT_Definitions Complex_Main
begin

section ‹Space Complexity and $buildup$ Time Consumption›
subsection ‹Space Comlexity of valid van Emde Boas Trees›
text ‹Space Complexity is linear in relation to universe sizes›

context VEBT_internal begin

fun space:: "VEBT  nat" where
"space (Leaf a b) = 3"|
"space (Node info deg treeList summary) = 5 + space summary + length treeList + foldr (λ a b. a+b) (map space treeList) 0"

fun space':: "VEBT  nat" where
"space' (Leaf a b) = 4"|
"space' (Node info deg treeList summary) = 6 + space' summary + foldr (λ a b. a+b) (map space' treeList) 0"

text ‹Count in reals›

fun cnt:: "VEBT  real" where
"cnt (Leaf a b) = 1"|
"cnt (Node info deg treeList summary) = 1 + cnt summary + foldr (λ a b. a+b) (map cnt treeList) 0"

subsection ‹Auxiliary Lemmas for List Summation›

lemma list_every_elemnt_bound_sum_bound:" x  set xs. f x  bound   foldr (λ a b. a+b) (map f xs) i  length xs * bound + i"
  by(induction xs) auto 

lemma list_every_elemnt_bound_sum_bound_real:" x  set (xs::'a list). (f::'areal) x  (bound::real)   foldr (λ a b. a+b) (map f xs) i  real(length xs) * bound + i"
  apply(induction xs) apply simp
  apply (simp add: algebra_simps)
  done

lemma foldr_one: "d  foldr (+) ys (d::nat)"
  by (induction ys) auto

lemma foldr_zero: " i < length xs. xs !  i > 0 
        foldr (λ a b. a+b) xs (d::nat) - d   length xs"
proof(induction xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  hence "i<length xs. 0 < xs ! i" 
    by auto
  hence " length xs  foldr (+) xs d - d" using Cons.IH by simp
  have "a  1" 
    by (metis gr0_conv_Suc length_Cons less_one local.Cons(2) not_gr0 not_less nth_Cons_0)
  then show ?case
    by (metis Nat.add_diff_assoc length xs  foldr (+) xs d - d add_mono_thms_linordered_semiring(1) foldr.simps(2) foldr_one length_Cons o_apply plus_1_eq_Suc)
qed

lemma foldr_mono: "length xs = length ys   i < length xs. xs ! i < ys ! i  c  d 
       foldr (λ a b. a+b) xs c  + length ys  foldr (λ a b. a+b) ys (d::nat)"
proof(induction xs arbitrary: d c ys)
  case Nil
  then show ?case using length_0_conv list.size(3)  foldr_one by simp
next
  case (Cons a xs)
  then obtain y ys1 where "ys = y #ys1" 
    by (metis Suc_leI Suc_le_length_iff nth_equalityI)
  hence 0:"length xs = length ys1"
    using Cons.prems(1) by force
  hence 1:"i<length xs. xs ! i < ys1 ! i" using Cons.prems(2)
    using ys = y # ys1 by force
  hence 3: "i<length ys1. ys1 ! i > 0"
    by (metis "0" less_nat_zero_code neq0_conv)
  have "foldr (+) (a # xs)c = a +foldr (+) xs (c)" by simp
  have "foldr (+) (ys) d = y +foldr (+) ys1 (d)" 
    by (simp add: ys = y # ys1)
  have 2:"a < y" using Cons.prems(2) ys = y # ys1 
    by (metis length_Cons nth_Cons_0 zero_less_Suc)
  have 4:"foldr (+) xs c  foldr (+) ys1 d - length ys1" 
    using Cons.IH[of ys1 c d] 0 1 Cons.prems(3) by simp
  have "foldr (+) ys1 d  length ys1"using foldr_zero[of ys1 d]  3 by simp
  hence "a + foldr (+) xs c < y + foldr (+) ys1 d - length ys1 " using 2 foldr_zero[of ys1 d] 4  by simp
 then show ?case 
   using ys = y # ys1 by auto
qed 

lemma two_realpow_ge_two :"(n::real) 1  (2::real)^n  2"  
  by (metis less_one not_less of_nat_1 of_nat_le_iff of_nat_numeral power_increasing power_one_right zero_neq_numeral)

lemma foldr0: "foldr (+) xs (c+d) = foldr (+) xs (d::real) + c"
  by(induction xs) auto

lemma  f_g_map_foldr_bound:" ( x  set xs.  f x  c * g x) 
  foldr (λ a b. a+b) (map f xs) d  c * foldr (λ a b. a+b) (map g xs) (0::real) + d" 
  by(induction xs) (auto simp add: algebra_simps)

lemma real_nat_list: "real (foldr (+) ( map f xs) (c::nat)) 
     = foldr (+) (map (λ x. real(f x))xs) c"
  by(induction xs arbitrary: c) auto

subsection ‹Actual Space Reasoning›

lemma space_space': "space' t > space t" 
proof(induction t)
  case (Node info deg treeList summary)
  hence " i < length treeList . (map space treeList)!i < ( map space' treeList)!i" 
    by simp
  hence 0:"foldr (+) (map space treeList) 0  + length treeList  foldr (+) (map space' treeList) 0 "
    using foldr_mono[of "(map space treeList)"  "(map space' treeList)" 0 0] by simp  
  have 1:"space summary < space' summary" using Node by simp
  hence "foldr (+) (map space treeList) 0 + length treeList + space summary 
         foldr (+) (map space' treeList) 0 + space' summary" using 0 by simp
  then show ?case using space'.simps(2)[of info deg treeList summary] 
       space.simps(2)[of info deg treeList summary] by simp
qed simp

lemma cnt_bound: 
  defines  "c  1.5" 
  shows "invar_vebt t n  cnt t  2*((2^n - c)::real)"
proof(induction t n rule: invar_vebt.induct)
case (2 treeList n summary m deg)
  hence "tset treeList.  (cnt t)  2 * (2 ^ n - c)" by simp
  hence " foldr (λ a b. a+b) (map cnt treeList) 0  2^n*2 * ((2^n - c)::real)" 
    using list_every_elemnt_bound_sum_bound_real[of treeList cnt "2*((2^n - c)::real)" 0 ] 2
    by (auto simp add: algebra_simps)
  hence "cnt ( Node None deg treeList summary)  2*(2^n+1)*(2^n-c) + 1" using 2 
    by(auto simp add: algebra_simps)
  hence "cnt ( Node None deg treeList summary)  2*(2^(n+n) + (1-c)*2^n - c + 1/2)" 
    by(auto simp add: algebra_simps power_add) 
  moreover have "2*(2^(n+n) + (1-c)*2^n - c + 1/2)  2*(2^(n+n) + -0.5*1 - 1.5 + 1/2)" 
    by(auto simp add: algebra_simps two_realpow_ge_one c_def)
  moreover hence "2*(2^(n+n) + (1-c)*2^n - c + 1/2)  2*(2^(n+n)  -  1.5 )" 
    by(auto simp add: algebra_simps power_add)
  ultimately have  "cnt ( Node None deg treeList summary)  2*(2^(n+n)  -  1.5 )" by simp
  then show ?case  using c_def 2(5) 2(6) by simp
next
  case (3 treeList n summary m deg)
  hence "tset treeList.  (cnt t)  2 * (2 ^ n - c)" by simp
  hence " foldr (λ a b. a+b) (map cnt treeList) 0  2^(n+1)*2 * ((2^n - c)::real)" 
    using list_every_elemnt_bound_sum_bound_real[of treeList cnt "2*((2^n - c)::real)" 0 ] 3
    by (auto simp add: algebra_simps)
  moreover 
  hence "cnt ( Node None deg treeList summary)  2*(2^n*2^m - c* 2^(m) + 2^(m) - c  + 1/2)"
    using 3
    by (auto simp add: algebra_simps powr_add)
  moreover have "2*(2^n*2^m - c* 2^(m) + 2^(m) - c  + 1/2) =  2*(2^(n+m) + (1-c)* 2^(m) - c  + 1/2)"
    by (auto simp add: algebra_simps power_add) 
   moreover have " 2*(2^(n+m) + (1-c)* 2^(m) - c  + 1/2)  2*(2^(n+m) + -0.5*1 - 1.5 + 1/2)" 
     by(auto simp add: algebra_simps two_realpow_ge_one c_def)
  moreover hence "2*(2^(n+m) + (1-c)*2^m - c + 1/2)  2*(2^(n+m)  -  1.5 )" 
    by(auto simp add: algebra_simps power_add)
  ultimately have  "cnt ( Node None deg treeList summary)  2*(2^(n+m)  -  1.5 )" by simp
  then show ?case  using c_def 3(5) 3(6) by simp
next
  case (4 treeList n summary m deg mi ma)
hence "tset treeList.  (cnt t)  2 * (2 ^ n - c)" by simp
  hence " foldr (λ a b. a+b) (map cnt treeList) 0  2^n*2 * ((2^n - c)::real)" 
    using list_every_elemnt_bound_sum_bound_real[of treeList cnt "2*((2^n - c)::real)" 0 ] 4
    by (auto simp add: algebra_simps)
  hence "cnt ( Node (Some (mi, ma)) deg treeList summary)  2*(2^n+1)*(2^n-c) + 1" using 4 
    by(auto simp add: algebra_simps)
  hence "cnt ( Node None deg treeList summary)  2*(2^(n+n) + (1-c)*2^n - c + 1/2)" 
    by(auto simp add: algebra_simps power_add) 
  moreover have "2*(2^(n+n) + (1-c)*2^n - c + 1/2)  2*(2^(n+n) + -0.5*1 - 1.5 + 1/2)" 
    by(auto simp add: algebra_simps two_realpow_ge_one c_def)
  moreover hence "2*(2^(n+n) + (1-c)*2^n - c + 1/2)  2*(2^(n+n)  -  1.5 )" 
    by(auto simp add: algebra_simps power_add)
  ultimately have  "cnt ( Node None deg treeList summary)  2*(2^(n+n)  -  1.5 )" by simp
  then show ?case  using c_def 4 by simp
next
  case (5 treeList n summary m deg mi ma)
 hence "tset treeList.  (cnt t)  2 * (2 ^ n - c)" by simp
  hence " foldr (λ a b. a+b) (map cnt treeList) 0  2^(n+1)*2 * ((2^n - c)::real)" 
    using list_every_elemnt_bound_sum_bound_real[of treeList cnt "2*((2^n - c)::real)" 0 ] 5
    by (auto simp add: algebra_simps)
  moreover 
  hence "cnt ( Node (Some (mi, ma)) deg treeList summary)  2*(2^n*2^m - c* 2^(m) + 2^(m) - c  + 1/2)"
    using 5
    by (auto simp add: algebra_simps powr_add)
  moreover have "2*(2^n*2^m - c* 2^(m) + 2^(m) - c  + 1/2) =  2*(2^(n+m) + (1-c)* 2^(m) - c  + 1/2)"
    by (auto simp add: algebra_simps power_add) 
   moreover have " 2*(2^(n+m) + (1-c)* 2^(m) - c  + 1/2)  2*(2^(n+m) + -0.5*1 - 1.5 + 1/2)" 
     by(auto simp add: algebra_simps two_realpow_ge_one c_def)
  moreover hence "2*(2^(n+m) + (1-c)*2^m - c + 1/2)  2*(2^(n+m)  -  1.5 )" 
    by(auto simp add: algebra_simps power_add)
  ultimately have  "cnt ( Node None deg treeList summary)  2*(2^(n+m)  -  1.5 )" by simp
  then show ?case  using c_def 5 by simp
qed (simp add: cnt.simps c_def)

theorem cnt_bound': "invar_vebt t n  cnt t  2 * (2 ^ n - 1)" 
  using cnt_bound by fastforce

lemma space_cnt: "space' t  6*cnt t" 
proof(induction t)
  case (Node info deg treeList summary)
 hence " tset treeList.  space' t  6 * cnt t" by blast
  hence " foldr (λ a b. a+b) (map space' treeList) 0 
     6 *foldr (λ a b. a+b) (map cnt treeList) 0"  
    using  f_g_map_foldr_bound[of treeList space' 6 cnt 0]
    by(auto simp add: algebra_simps real_nat_list)
then show ?case
  using Node.IH(2) by force
qed simp

lemma space_2_pow_bound:  assumes "invar_vebt t n " shows "real (space' t)  12 * (2^n -1)"
  by (smt (verit, best) assms cnt_bound' space_cnt) 

lemma space'_bound: 
  assumes "invar_vebt t n" "u = 2^n"
  shows "space' t  12 * u"
proof -
  have "real (space' t)  real (12 * u)"
    using assms using  space_2_pow_bound[of t n] by fastforce
  then have "space' t  12 * 2 ^ n"
    using assms of_nat_le_iff by blast
  then show ?thesis
    using assms by auto 
qed

text ‹Main Theorem›

theorem space_bound: 
  assumes "invar_vebt t n" "u = 2^n"
  shows "space t  12 * u"
  by (metis assms dual_order.trans less_imp_le_nat space'_bound space_space')

subsection ‹Complexity of Generation Time ›
text ‹Space complexity is closely related to tree generation time complexity›

text ‹Time approximation for replicate function. $T_{replicate} \; n \; t \;x$ denotes runnig time of the $n$-times replication of $x$ into a list. 
$t$ models runtime for generation of a single $x$.›

fun Tbuildup::"nat  nat" where
"Tbuildup 0 = 3"|
"Tbuildup (Suc 0) = 3"|
"Tbuildup  n = (if even n then 1 + (let half = n div 2 in 
                 9 + Tbuildup half +  (2^half) * (Tbuildup half  + 1))
                else (let half = n div 2 in
                      11 + Tbuildup (Suc half) +  (2^(Suc half))* (Tbuildup half + 1 )))"

fun Tbuild::"nat  nat" where
"Tbuild 0 = 4"|
"Tbuild (Suc 0) = 4"|
"Tbuild  n = (if even n then 1 + (let half = n div 2 in 
                 10 + Tbuild half +  (2^half) * (Tbuild half))
                else (let half = n div 2 in
                      12 + Tbuild (Suc half) +  (2^(Suc half))* (Tbuild half)))"

lemma buildup_build_time: "Tbuildup  n < Tbuild  n"
proof(induction n rule: Tbuildup.induct)
  case (3 va)
  then show ?case
  proof(cases "even (Suc (Suc va))")
    case True
    then show ?thesis 
      apply(subst Tbuildup.simps)
      apply(subst Tbuild.simps) 
      using True apply simp
      by (smt (z3) "3.IH"(1) Suc_1 True add_mono_thms_linordered_semiring(1) distrib_left div2_Suc_Suc less_mult_imp_div_less linorder_not_le mult.commute mult_numeral_1_right nat_0_less_mult_iff nat_less_le nat_zero_less_power_iff nonzero_mult_div_cancel_left not_less_eq numerals(1) plus_1_eq_Suc zero_le_one)
  next
    case False
    hence *: "(let half = Suc (Suc va) div 2
          in 11 + Tbuildup (Suc half) + 2 ^ Suc half * (Tbuildup half + 1))
           <  (let half = Suc (Suc va) div 2
            in 12 + Tbuild (Suc half) + 2 ^ Suc half * Tbuild half)"
      unfolding Let_def
    proof-
      assume "odd (Suc (Suc va))"
    have " 11 + Tbuildup (Suc (Suc (Suc va) div 2))
          < 12 + Tbuild (Suc (Suc (Suc va) div 2))"
      using "3.IH"(3) False add_less_mono by presburger
    moreover have " 2 ^ Suc (Suc (Suc va) div 2) * (Tbuildup (Suc (Suc va) div 2) + 1)
                    2 ^ Suc (Suc (Suc va) div 2) * Tbuild (Suc (Suc va) div 2)"
      by (metis "3.IH"(4) False Suc_leI add.commute mult_le_mono2 plus_1_eq_Suc)
    ultimately show " 11 + Tbuildup (Suc (Suc (Suc va) div 2)) +
                     2 ^ Suc (Suc (Suc va) div 2) * (Tbuildup (Suc (Suc va) div 2) + 1)
                     < 12 + Tbuild (Suc (Suc (Suc va) div 2)) +
                       2 ^ Suc (Suc (Suc va) div 2) * Tbuild (Suc (Suc va) div 2)" 
      using add_mono_thms_linordered_field(3) by blast
  qed
    show ?thesis apply(subst Tbuildup.simps)
      apply(subst Tbuild.simps) 
      using False *
      by simp
  qed
qed simp+
 

lemma listsum_bound: "( x. x  set xs  f x  (0::real)) 
        foldr (+) (map f xs) y  y"
  apply(induction xs arbitrary: y)
  apply simp
  apply(subst list.map(2))
  apply(subst foldr.simps)
  apply (simp add: add_increasing)
  done

lemma cnt_non_neg: "cnt t  0"
  by (induction t) (simp add: VEBT_internal.listsum_bound)+

lemma foldr_same: "( x y. x  set (xs::real list)  y  set xs  x = y) 
                   ( x . (x::real)  set xs  x = (y::real))  
                   foldr (λ (a::real) (b::real). a+b) xs 0 = real (length xs) * y"
  apply(induction xs)
    apply simp
  apply(subst foldr.simps)
  unfolding comp_def
proof -
  fix a :: real and xsa :: "real list"
  assume a1: "x y. x  set xsa; y  set xsa  x = y; x. x  set xsa  x = y  foldr (+) xsa 0 = real (length xsa) * y"
  assume "x y. x  set (a # xsa); y  set (a # xsa)  x = y"
assume a2: "x. x  set (a # xsa)  x = y"
  then have f3: "a = y"
    by simp
  then have "a * real (length xsa) = foldr (+) xsa 0"
    using a2 a1 by (metis (no_types) list.set_intros(2) mult.commute)
  then show "a + foldr (+) xsa 0 = real (length (a # xsa)) * y"
    using f3 by (simp add: distrib_left mult.commute)
qed 

lemma foldr_same_int: "( x y. x  set xs  y  set xs  x = y) 
                   ( x . x  set xs  x = y)  
                   foldr (+) xs 0 =  (length xs) * y"
  apply(induction xs)
    apply simp
    apply(subst foldr.simps) 
    apply fastforce
  done

lemma t_build_cnt: "Tbuild n  cnt (vebt_buildup n) * 13"  
proof(induction n rule: Tbuild.induct)
  case 1
  then show ?case by simp
next
  case 2
  then show ?case by simp
next
  case (3 va)
  then show ?case 
  proof(cases "even (Suc (Suc va))")
    case True
    hence *: "Tbuild (Suc (Suc va)) = 11+
           Tbuild (Suc (Suc va) div 2) +
         2 ^ (Suc (Suc va) div 2) * (Tbuild (Suc (Suc va) div 2))"
      apply(subst Tbuild.simps)
      by simp
    have " real (Tbuild (Suc (va div 2)))  13 * cnt (vebt_buildup (Suc (va div 2)))" 
      using "3.IH"(1) True by force
    moreover hence 1:"  2 ^ (Suc (Suc va) div 2)* (Tbuild (Suc (Suc va) div 2)) 
                    2 ^ (Suc (Suc va) div 2) * ((cnt (vebt_buildup (Suc (Suc va) div 2)))*13)"
      using ordered_semiring_class.mult_mono[of "(Tbuild (Suc (Suc va) div 2))" " ((cnt (vebt_buildup (Suc (Suc va) div 2)))*13)" 
            "2 ^ (Suc (Suc va) div 2)" "2 ^ (Suc (Suc va) div 2)"] by simp
    ultimately have " Tbuild (Suc (Suc va) div 2) +
         2 ^ (Suc (Suc va) div 2) * (Tbuild (Suc (Suc va) div 2))  
             cnt (vebt_buildup (Suc (Suc va) div 2))*13 + 
          2 ^ (Suc (Suc va) div 2) * ((cnt (vebt_buildup (Suc (Suc va) div 2)))*13)"
           by (smt (verit) "3.IH"(1) True of_nat_add)
         have 10: "(foldr (+) 
                 (replicate (l) ((cnt (vebt_buildup (Suc (Suc va) div 2)))
                  )) 0) = 
                   l * ((cnt (vebt_buildup (Suc (Suc va) div 2))))" for l
           using foldr_same[of "(replicate l (cnt (vebt_buildup (Suc (Suc va) div 2))))"
                             "cnt (vebt_buildup (Suc (Suc va) div 2))" ] 
              length_replicate by simp
         have " cnt (vebt_buildup (Suc (Suc va) div 2))*13 + 
          2 ^ (Suc (Suc va) div 2) * ((cnt (vebt_buildup (Suc (Suc va) div 2)))*13) + 11
          13* cnt (vebt_buildup (Suc (Suc va)))" 
          apply(subst vebt_buildup.simps)
      using True apply simp
      apply(subst sym[OF foldr_replicate]) 
    proof-
      assume "even va"
      have " 2* (2 ^ (va div 2) * cnt (vebt_buildup (Suc (va div 2)))) = 
             foldr (+) (replicate (2 * 2 ^ (va div 2)) (cnt (vebt_buildup (Suc (va div 2))))) 0"
        apply(rule sym)
        using 10 div2_Suc_Suc[of va] by simp
      then show "26 * (2 ^ (va div 2) * cnt (vebt_buildup (Suc (va div 2))))
     2 + 13 * foldr (+) (replicate (2 * 2 ^ (va div 2)) (cnt (vebt_buildup (Suc (va div 2))))) 0"
        by simp
    qed
    then show ?thesis
      by (smt (verit, ccfv_SIG) "*" "1" "3.IH"(1) True numeral_Bit1 numeral_plus_numeral numeral_plus_one of_nat_add of_nat_numeral semiring_norm(2))
  next
    case False
    have "12 + Tbuild (Suc ( Suc (va div 2))) + 2 ^ Suc ( Suc ( va div 2)) * Tbuild ( Suc ( va div 2))
           cnt ( Node None (Suc (Suc va)) (replicate (2 ^ Suc ( Suc ( va div 2))) (vebt_buildup ( Suc ( va div 2))))
                     (vebt_buildup (Suc ( Suc ( va div 2))))) * 13" 
      apply(subst cnt.simps)
    proof-
       have 10: "(foldr (+) 
                 (replicate (l) ((cnt (vebt_buildup (Suc (Suc va) div 2)))
                  )) 0) = 
                   l * ((cnt (vebt_buildup (Suc (Suc va) div 2))))" for l
           using foldr_same[of "(replicate l (cnt (vebt_buildup (Suc (Suc va) div 2))))"
                             "cnt (vebt_buildup (Suc (Suc va) div 2))" ] 
              length_replicate by simp
        hence map_cnt: " foldr (+) (map cnt (replicate (2 ^ Suc (Suc (va div 2))) (vebt_buildup (Suc (va div 2))))) 0 = 
                 2 ^ Suc (Suc (va div 2)) * cnt (vebt_buildup (Suc (va div 2))) " by simp
        have "Tbuild (Suc (Suc (va div 2)))  13 * cnt (vebt_buildup (Suc (Suc (va div 2))))"
          using "3.IH"(3) False by force
        moreover have "Tbuild (Suc (va div 2))  13 * cnt(vebt_buildup (Suc (va div 2)))"
          using "3.IH"(4) False by force
        moreover have add_double_trans: "(a::real)  b  c  d  
                           i  0 a + c*i  b + d*i" for a b c d i
          using mult_right_mono by fastforce
        ultimately have " real(Tbuild (Suc (Suc (va div 2)))) +  2 ^ Suc (Suc (va div 2)) * real( Tbuild (Suc (va div 2))) 
                13 * cnt (vebt_buildup (Suc (Suc (va div 2)))) + 
                    2 ^ Suc (Suc (va div 2)) * (13 * cnt(vebt_buildup (Suc (va div 2))))" 
          by (meson add_mono_thms_linordered_semiring(1) mult_mono of_nat_0_le_iff order_refl zero_le_numeral zero_le_power)
        hence 11:"(12 + Tbuild (Suc (Suc (va div 2))) +  2 ^ Suc (Suc (va div 2)) * Tbuild (Suc (va div 2))) 
               12 + 13 * cnt (vebt_buildup (Suc (Suc (va div 2)))) + 
                    2 ^ Suc (Suc (va div 2)) * 13 * cnt(vebt_buildup (Suc (va div 2)))"
          using algebra_simps by simp
        show " (12 + Tbuild (Suc (Suc (va div 2))) +
      2 ^ Suc (Suc (va div 2)) * Tbuild (Suc (va div 2)))
     (1 + cnt (vebt_buildup (Suc (Suc (va div 2)))) +
        foldr (+) (map cnt (replicate (2 ^ Suc (Suc (va div 2))) (vebt_buildup (Suc (va div 2))))) 0) * 13" 
          apply(subst map_cnt)
          using 11 algebra_simps by simp
      qed        
  then show ?thesis
    apply(subst vebt_buildup.simps)
    apply(subst Tbuild.simps)
    using False by force
qed
qed

lemma t_buildup_cnt: "Tbuildup  n  cnt (vebt_buildup n) * 13"
  apply(rule order.trans[where b = "real(Tbuild n)"])
  apply(rule order.strict_implies_order)
  apply (simp add: VEBT_internal.buildup_build_time)
  apply(rule t_build_cnt)
 done

lemma count_buildup: "cnt (vebt_buildup n)  2 * 2^n"
  by (smt (verit, ccfv_threshold) VEBT_internal.cnt_bound' add.right_neutral add_less_mono buildup_gives_valid cnt.simps(1) even_Suc lessI odd_pos one_le_power plus_1_eq_Suc vebt_buildup.elims)

lemma count_buildup': "cnt (vebt_buildup n)  2 * (2::nat)^n"
   by (simp add: VEBT_internal.count_buildup)

theorem vebt_buildup_bound: "u = 2^n  Tbuildup  n  26 * u"
  using count_buildup'[of n] t_buildup_cnt[of n] by linarith

text ‹Count in natural numbers›

fun cnt':: "VEBT  nat" where
"cnt' (Leaf a b) = 1"|
"cnt' (Node info deg treeList summary) = 1 + cnt' summary + foldr (λ a b. a+b) (map cnt' treeList) 0"

lemma cnt_cnt_eq:"cnt t = cnt' t"
proof(induction t)
  case (Node x1 x2 x3 t)
  then show ?case 
    by simp (smt (verit, best) map_eq_conv of_nat_0 real_nat_list)
qed auto

end
end