src/HOL/Data_Structures/Tree23.thy
changeset 66302 fd89f97c80c2
parent 61679 1335462046e8
child 70273 acc1749c2be9
equal deleted inserted replaced
66301:8a6a89d6cf2b 66302:fd89f97c80c2
    38 "bal Leaf = True" |
    38 "bal Leaf = True" |
    39 "bal (Node2 l _ r) = (bal l & bal r & height l = height r)" |
    39 "bal (Node2 l _ r) = (bal l & bal r & height l = height r)" |
    40 "bal (Node3 l _ m _ r) =
    40 "bal (Node3 l _ m _ r) =
    41   (bal l & bal m & bal r & height l = height m & height m = height r)"
    41   (bal l & bal m & bal r & height l = height m & height m = height r)"
    42 
    42 
       
    43 lemma ht_sz_if_bal: "bal t \<Longrightarrow> 2 ^ height t \<le> size t + 1"
       
    44 by (induction t) auto
       
    45 
    43 end
    46 end