equal
deleted
inserted
replaced
24 |
24 |
25 fun size1 :: "('a,'b) tree \<Rightarrow> nat" where |
25 fun size1 :: "('a,'b) tree \<Rightarrow> nat" where |
26 "size1 \<langle>\<rangle> = 1" | |
26 "size1 \<langle>\<rangle> = 1" | |
27 "size1 \<langle>l, _, _, r\<rangle> = size1 l + size1 r" |
27 "size1 \<langle>l, _, _, r\<rangle> = size1 l + size1 r" |
28 |
28 |
|
29 fun complete :: "('a,'b) tree \<Rightarrow> bool" where |
|
30 "complete Leaf = True" | |
|
31 "complete (Node l _ _ r) = (complete l \<and> complete r \<and> height l = height r)" |
|
32 |
29 lemma size1_size: "size1 t = size t + 1" |
33 lemma size1_size: "size1 t = size t + 1" |
30 by (induction t) simp_all |
34 by (induction t) simp_all |
31 |
35 |
32 lemma size1_ge0[simp]: "0 < size1 t" |
36 lemma size1_ge0[simp]: "0 < size1 t" |
33 by (simp add: size1_size) |
37 by (simp add: size1_size) |