src/HOL/Data_Structures/Tree23.thy
changeset 70273 acc1749c2be9
parent 66302 fd89f97c80c2
child 72566 831f17da1aab
equal deleted inserted replaced
70272:1d564a895296 70273:acc1749c2be9
    32 
    32 
    33 end
    33 end
    34 
    34 
    35 text \<open>Balanced:\<close>
    35 text \<open>Balanced:\<close>
    36 
    36 
    37 fun bal :: "'a tree23 \<Rightarrow> bool" where
    37 fun complete :: "'a tree23 \<Rightarrow> bool" where
    38 "bal Leaf = True" |
    38 "complete Leaf = True" |
    39 "bal (Node2 l _ r) = (bal l & bal r & height l = height r)" |
    39 "complete (Node2 l _ r) = (complete l & complete r & height l = height r)" |
    40 "bal (Node3 l _ m _ r) =
    40 "complete (Node3 l _ m _ r) =
    41   (bal l & bal m & bal r & height l = height m & height m = height r)"
    41   (complete l & complete m & complete 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"
    43 lemma ht_sz_if_complete: "complete t \<Longrightarrow> 2 ^ height t \<le> size t + 1"
    44 by (induction t) auto
    44 by (induction t) auto
    45 
    45 
    46 end
    46 end