changeset 67573 | ed0a7090167d |
parent 66912 | a99a7cbf0fb5 |
child 68406 | 6beb45f6cf67 |
--- a/src/HOL/Library/Log_Nat.thy Sat Feb 03 20:46:28 2018 +0100 +++ b/src/HOL/Library/Log_Nat.thy Mon Feb 05 08:30:19 2018 +0100 @@ -200,8 +200,11 @@ lemma bitlen_alt_def: "bitlen a = (if a > 0 then \<lfloor>log 2 a\<rfloor> + 1 else 0)" by (simp add: bitlen_def floorlog_def) +lemma bitlen_zero[simp]: "bitlen 0 = 0" + by (auto simp: bitlen_def floorlog_def) + lemma bitlen_nonneg: "0 \<le> bitlen x" -by (simp add: bitlen_def) + by (simp add: bitlen_def) lemma bitlen_bounds: assumes "x > 0"