src/HOL/Data_Structures/Tree2.thy
changeset 62650 7e6bb43e7217
parent 62390 842917225d56
child 67967 5a4280946a25
equal deleted inserted replaced
62649:d23be25c0835 62650:7e6bb43e7217
    12 
    12 
    13 fun height :: "('a,'b) tree \<Rightarrow> nat" where
    13 fun height :: "('a,'b) tree \<Rightarrow> nat" where
    14 "height Leaf = 0" |
    14 "height Leaf = 0" |
    15 "height (Node _ l a r) = max (height l) (height r) + 1"
    15 "height (Node _ l a r) = max (height l) (height r) + 1"
    16 
    16 
       
    17 definition size1 :: "('a,'b) tree \<Rightarrow> nat" where
       
    18 "size1 t = size t + 1"
       
    19 
       
    20 lemma size1_simps[simp]:
       
    21   "size1 \<langle>\<rangle> = 1"
       
    22   "size1 \<langle>u, l, x, r\<rangle> = size1 l + size1 r"
       
    23 by (simp_all add: size1_def)
       
    24 
       
    25 lemma size1_ge0[simp]: "0 < size1 t"
       
    26 by (simp add: size1_def)
       
    27 
    17 end
    28 end