author | nipkow |
Thu, 27 Oct 2016 12:54:55 +0200 | |
changeset 64414 | f8be2208e99c |
parent 64413 | c0d5e78eb647 |
child 64415 | 7ca48c274553 |
--- a/src/HOL/Library/Tree.thy Wed Oct 26 22:40:28 2016 +0200 +++ b/src/HOL/Library/Tree.thy Thu Oct 27 12:54:55 2016 +0200 @@ -141,6 +141,9 @@ lemma height_map_tree[simp]: "height (map_tree f t) = height t" by (induction t) auto +lemma height_le_size_tree: "height t \<le> size (t::'a tree)" +by (induction t) auto + lemma size1_height: "size t + 1 \<le> 2 ^ height (t::'a tree)" proof(induction t) case (Node l a r)