equal
deleted
inserted
replaced
34 |
34 |
35 text \<open>Completeness:\<close> |
35 text \<open>Completeness:\<close> |
36 |
36 |
37 fun complete :: "'a tree23 \<Rightarrow> bool" where |
37 fun complete :: "'a tree23 \<Rightarrow> bool" where |
38 "complete Leaf = True" | |
38 "complete Leaf = True" | |
39 "complete (Node2 l _ r) = (complete l & complete r & height l = height r)" | |
39 "complete (Node2 l _ r) = (height l = height r \<and> complete l & complete r)" | |
40 "complete (Node3 l _ m _ r) = |
40 "complete (Node3 l _ m _ r) = |
41 (complete l & complete m & complete r & height l = height m & height m = height r)" |
41 (height l = height m & height m = height r & complete l & complete m & complete r)" |
42 |
42 |
43 lemma ht_sz_if_complete: "complete 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 |