equal
deleted
inserted
replaced
4 imports |
4 imports |
5 Complex_Main |
5 Complex_Main |
6 Tree |
6 Tree |
7 begin |
7 begin |
8 |
8 |
9 text \<open>This theory is separate from @{theory Tree} because the former is discrete and builds on |
9 text \<open> |
10 @{theory Main} whereas this theory builds on @{theory Complex_Main}.\<close> |
10 This theory is separate from @{theory "HOL-Library.Tree"} because the former is discrete and |
|
11 builds on @{theory Main} whereas this theory builds on @{theory Complex_Main}. |
|
12 \<close> |
11 |
13 |
12 |
14 |
13 lemma size1_height_log: "log 2 (size1 t) \<le> height t" |
15 lemma size1_height_log: "log 2 (size1 t) \<le> height t" |
14 by (simp add: log2_of_power_le size1_height) |
16 by (simp add: log2_of_power_le size1_height) |
15 |
17 |