author | Lars Hupel <lars.hupel@mytum.de> |
Mon, 18 Jun 2018 10:50:24 +0200 | |
changeset 68462 | 8d1bf38c6fe6 |
parent 68406 | 6beb45f6cf67 |
child 70349 | 697450fd25c1 |
permissions | -rw-r--r-- |
63663
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
1 |
(* Title: HOL/Library/Log_Nat.thy |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
2 |
Author: Johannes Hölzl, Fabian Immler |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
3 |
Copyright 2012 TU München |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
4 |
*) |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
5 |
|
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
6 |
section \<open>Logarithm of Natural Numbers\<close> |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
7 |
|
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
8 |
theory Log_Nat |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
9 |
imports Complex_Main |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
10 |
begin |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
11 |
|
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
12 |
definition floorlog :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
13 |
"floorlog b a = (if a > 0 \<and> b > 1 then nat \<lfloor>log b a\<rfloor> + 1 else 0)" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
14 |
|
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
15 |
lemma floorlog_mono: "x \<le> y \<Longrightarrow> floorlog b x \<le> floorlog b y" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
16 |
by(auto simp: floorlog_def floor_mono nat_mono) |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
17 |
|
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
18 |
lemma floorlog_bounds: |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
19 |
assumes "x > 0" "b > 1" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
20 |
shows "b ^ (floorlog b x - 1) \<le> x \<and> x < b ^ (floorlog b x)" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
21 |
proof |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
22 |
show "b ^ (floorlog b x - 1) \<le> x" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
23 |
proof - |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
24 |
have "b ^ nat \<lfloor>log b x\<rfloor> = b powr \<lfloor>log b x\<rfloor>" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
25 |
using powr_realpow[symmetric, of b "nat \<lfloor>log b x\<rfloor>"] \<open>x > 0\<close> \<open>b > 1\<close> |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
26 |
by simp |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
27 |
also have "\<dots> \<le> b powr log b x" using \<open>b > 1\<close> by simp |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
28 |
also have "\<dots> = real_of_int x" using \<open>0 < x\<close> \<open>b > 1\<close> by simp |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
29 |
finally have "b ^ nat \<lfloor>log b x\<rfloor> \<le> real_of_int x" by simp |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
30 |
then show ?thesis |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
31 |
using \<open>0 < x\<close> \<open>b > 1\<close> of_nat_le_iff |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
32 |
by (fastforce simp add: floorlog_def) |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
33 |
qed |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
34 |
show "x < b ^ (floorlog b x)" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
35 |
proof - |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
36 |
have "x \<le> b powr (log b x)" using \<open>x > 0\<close> \<open>b > 1\<close> by simp |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
37 |
also have "\<dots> < b powr (\<lfloor>log b x\<rfloor> + 1)" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
38 |
using assms by (intro powr_less_mono) auto |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
39 |
also have "\<dots> = b ^ nat (\<lfloor>log b (real_of_int x)\<rfloor> + 1)" |
68406 | 40 |
using assms by (simp flip: powr_realpow) |
63663
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
41 |
finally |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
42 |
have "x < b ^ nat (\<lfloor>log b (int x)\<rfloor> + 1)" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
43 |
by (rule of_nat_less_imp_less) |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
44 |
then show ?thesis |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
45 |
using \<open>x > 0\<close> \<open>b > 1\<close> by (simp add: floorlog_def nat_add_distrib) |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
46 |
qed |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
47 |
qed |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
48 |
|
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
49 |
lemma floorlog_power[simp]: |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
50 |
assumes "a > 0" "b > 1" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
51 |
shows "floorlog b (a * b ^ c) = floorlog b a + c" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
52 |
proof - |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
53 |
have "\<lfloor>log b a + real c\<rfloor> = \<lfloor>log b a\<rfloor> + c" by arith |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
54 |
then show ?thesis using assms |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
55 |
by (auto simp: floorlog_def log_mult powr_realpow[symmetric] nat_add_distrib) |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
56 |
qed |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
57 |
|
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
58 |
lemma floor_log_add_eqI: |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
59 |
fixes a::nat and b::nat and r::real |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
60 |
assumes "b > 1" "a \<ge> 1" "0 \<le> r" "r < 1" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
61 |
shows "\<lfloor>log b (a + r)\<rfloor> = \<lfloor>log b a\<rfloor>" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
62 |
proof (rule floor_eq2) |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
63 |
have "log b a \<le> log b (a + r)" using assms by force |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
64 |
then show "\<lfloor>log b a\<rfloor> \<le> log b (a + r)" by arith |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
65 |
next |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
66 |
define l::int where "l = int b ^ (nat \<lfloor>log b a\<rfloor> + 1)" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
67 |
have l_def_real: "l = b powr (\<lfloor>log b a\<rfloor> + 1)" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
68 |
using assms by (simp add: l_def powr_add powr_real_of_int) |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
69 |
have "a < l" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
70 |
proof - |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
71 |
have "a = b powr (log b a)" using assms by simp |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
72 |
also have "\<dots> < b powr floor ((log b a) + 1)" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
73 |
using assms(1) by auto |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
74 |
also have "\<dots> = l" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
75 |
using assms by (simp add: l_def powr_real_of_int powr_add) |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
76 |
finally show ?thesis by simp |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
77 |
qed |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
78 |
then have "a + r < l" using assms by simp |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
79 |
then have "log b (a + r) < log b l" using assms by simp |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
80 |
also have "\<dots> = real_of_int \<lfloor>log b a\<rfloor> + 1" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
81 |
using assms by (simp add: l_def_real) |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
82 |
finally show "log b (a + r) < real_of_int \<lfloor>log b a\<rfloor> + 1" . |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
83 |
qed |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
84 |
|
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
85 |
lemma divide_nat_diff_div_nat_less_one: |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
86 |
fixes x b::nat shows "x / b - x div b < 1" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
87 |
proof - |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
88 |
have "int 0 \<noteq> \<lfloor>1::real\<rfloor>" by simp |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
89 |
thus ?thesis |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
90 |
by (metis add_diff_cancel_left' floor_divide_of_nat_eq less_eq_real_def |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
91 |
mod_div_trivial real_of_nat_div3 real_of_nat_div_aux) |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
92 |
qed |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
93 |
|
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
94 |
lemma floor_log_div: |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
95 |
fixes b x :: nat assumes "b > 1" "x > 0" "x div b > 0" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
96 |
shows "\<lfloor>log b x\<rfloor> = \<lfloor>log b (x div b)\<rfloor> + 1" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
97 |
proof- |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
98 |
have "\<lfloor>log b x\<rfloor> = \<lfloor>log b (x / b * b)\<rfloor>" using assms by simp |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
99 |
also have "\<dots> = \<lfloor>log b (x / b) + log b b\<rfloor>" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
100 |
using assms by (subst log_mult) auto |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
101 |
also have "\<dots> = \<lfloor>log b (x / b)\<rfloor> + 1" using assms by simp |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
102 |
also have "\<lfloor>log b (x / b)\<rfloor> = \<lfloor>log b (x div b + (x / b - x div b))\<rfloor>" by simp |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
103 |
also have "\<dots> = \<lfloor>log b (x div b)\<rfloor>" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
104 |
using assms real_of_nat_div4 divide_nat_diff_div_nat_less_one |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
105 |
by (intro floor_log_add_eqI) auto |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
106 |
finally show ?thesis . |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
107 |
qed |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
108 |
|
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
109 |
lemma compute_floorlog[code]: |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
110 |
"floorlog b x = (if x > 0 \<and> b > 1 then floorlog b (x div b) + 1 else 0)" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
111 |
by (auto simp: floorlog_def floor_log_div[of b x] div_eq_0_iff nat_add_distrib |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
112 |
intro!: floor_eq2) |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
113 |
|
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
114 |
lemma floor_log_eq_if: |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
115 |
fixes b x y :: nat |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
116 |
assumes "x div b = y div b" "b > 1" "x > 0" "x div b \<ge> 1" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
117 |
shows "floor(log b x) = floor(log b y)" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
118 |
proof - |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
119 |
have "y > 0" using assms by(auto intro: ccontr) |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
120 |
thus ?thesis using assms by (simp add: floor_log_div) |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
121 |
qed |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
122 |
|
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
123 |
lemma floorlog_eq_if: |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
124 |
fixes b x y :: nat |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
125 |
assumes "x div b = y div b" "b > 1" "x > 0" "x div b \<ge> 1" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
126 |
shows "floorlog b x = floorlog b y" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
127 |
proof - |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
128 |
have "y > 0" using assms by(auto intro: ccontr) |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
129 |
thus ?thesis using assms |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
130 |
by(auto simp add: floorlog_def eq_nat_nat_iff intro: floor_log_eq_if) |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
131 |
qed |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
132 |
|
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
133 |
|
66912
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
134 |
lemma powr_eq_one_iff[simp]: "a powr x = 1 \<longleftrightarrow> (x = 0)" |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
135 |
if "a > 1" |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
136 |
for a x::real |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
137 |
using that |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
138 |
by (auto simp: powr_def split: if_splits) |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
139 |
|
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
140 |
lemma floorlog_leD: "floorlog b x \<le> w \<Longrightarrow> b > 1 \<Longrightarrow> x < b ^ w" |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
141 |
by (metis floorlog_bounds leD linorder_neqE_nat order.strict_trans power_strict_increasing_iff |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
142 |
zero_less_one zero_less_power) |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
143 |
|
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
144 |
lemma floorlog_leI: "x < b ^ w \<Longrightarrow> 0 \<le> w \<Longrightarrow> b > 1 \<Longrightarrow> floorlog b x \<le> w" |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
145 |
by (drule less_imp_of_nat_less[where 'a=real]) |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
146 |
(auto simp: floorlog_def Suc_le_eq nat_less_iff floor_less_iff log_of_power_less) |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
147 |
|
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
148 |
lemma floorlog_eq_zero_iff: |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
149 |
"floorlog b x = 0 \<longleftrightarrow> (b \<le> 1 \<or> x \<le> 0)" |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
150 |
by (auto simp: floorlog_def) |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
151 |
|
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
152 |
lemma floorlog_le_iff: "floorlog b x \<le> w \<longleftrightarrow> b \<le> 1 \<or> b > 1 \<and> 0 \<le> w \<and> x < b ^ w" |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
153 |
using floorlog_leD[of b x w] floorlog_leI[of x b w] |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
154 |
by (auto simp: floorlog_eq_zero_iff[THEN iffD2]) |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
155 |
|
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
156 |
lemma floorlog_ge_SucI: "Suc w \<le> floorlog b x" if "b ^ w \<le> x" "b > 1" |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
157 |
using that le_log_of_power[of b w x] power_not_zero |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
158 |
by (force simp: floorlog_def Suc_le_eq powr_realpow not_less Suc_nat_eq_nat_zadd1 |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
159 |
zless_nat_eq_int_zless int_add_floor less_floor_iff |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
160 |
simp del: floor_add2) |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
161 |
|
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
162 |
lemma floorlog_geI: "w \<le> floorlog b x" if "b ^ (w - 1) \<le> x" "b > 1" |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
163 |
using floorlog_ge_SucI[of b "w - 1" x] that |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
164 |
by auto |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
165 |
|
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
166 |
lemma floorlog_geD: "b ^ (w - 1) \<le> x" if "w \<le> floorlog b x" "w > 0" |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
167 |
proof - |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
168 |
have "b > 1" "0 < x" |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
169 |
using that by (auto simp: floorlog_def split: if_splits) |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
170 |
have "b ^ (w - 1) \<le> x" if "b ^ w \<le> x" |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
171 |
proof - |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
172 |
have "b ^ (w - 1) \<le> b ^ w" |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
173 |
using \<open>b > 1\<close> |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
174 |
by (auto intro!: power_increasing) |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
175 |
also note that |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
176 |
finally show ?thesis . |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
177 |
qed |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
178 |
moreover have "b ^ nat \<lfloor>log (real b) (real x)\<rfloor> \<le> x" (is "?l \<le> _") |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
179 |
proof - |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
180 |
have "0 \<le> log (real b) (real x)" |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
181 |
using \<open>b > 1\<close> \<open>0 < x\<close> |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
182 |
by (auto simp: ) |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
183 |
then have "?l \<le> b powr log (real b) (real x)" |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
184 |
using \<open>b > 1\<close> |
68406 | 185 |
by (auto simp flip: powr_realpow intro!: powr_mono of_nat_floor) |
66912
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
186 |
also have "\<dots> = x" using \<open>b > 1\<close> \<open>0 < x\<close> |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
187 |
by auto |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
188 |
finally show ?thesis |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
189 |
unfolding of_nat_le_iff . |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
190 |
qed |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
191 |
ultimately show ?thesis |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
192 |
using that |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
193 |
by (auto simp: floorlog_def le_nat_iff le_floor_iff le_log_iff powr_realpow |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
194 |
split: if_splits elim!: le_SucE) |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
195 |
qed |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
196 |
|
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
197 |
|
63663
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
198 |
definition bitlen :: "int \<Rightarrow> int" where "bitlen a = floorlog 2 (nat a)" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
199 |
|
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
200 |
lemma bitlen_alt_def: "bitlen a = (if a > 0 then \<lfloor>log 2 a\<rfloor> + 1 else 0)" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
201 |
by (simp add: bitlen_def floorlog_def) |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
202 |
|
67573 | 203 |
lemma bitlen_zero[simp]: "bitlen 0 = 0" |
204 |
by (auto simp: bitlen_def floorlog_def) |
|
205 |
||
63663
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
206 |
lemma bitlen_nonneg: "0 \<le> bitlen x" |
67573 | 207 |
by (simp add: bitlen_def) |
63663
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
208 |
|
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
209 |
lemma bitlen_bounds: |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
210 |
assumes "x > 0" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
211 |
shows "2 ^ nat (bitlen x - 1) \<le> x \<and> x < 2 ^ nat (bitlen x)" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
212 |
proof - |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
213 |
from assms have "bitlen x \<ge> 1" by (auto simp: bitlen_alt_def) |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
214 |
with assms floorlog_bounds[of "nat x" 2] show ?thesis |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
215 |
by (auto simp add: bitlen_def le_nat_iff nat_less_iff nat_diff_distrib) |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
216 |
qed |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
217 |
|
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
218 |
lemma bitlen_pow2[simp]: |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
219 |
assumes "b > 0" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
220 |
shows "bitlen (b * 2 ^ c) = bitlen b + c" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
221 |
using assms |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
222 |
by (simp add: bitlen_def nat_mult_distrib nat_power_eq) |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
223 |
|
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
224 |
lemma compute_bitlen[code]: |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
225 |
"bitlen x = (if x > 0 then bitlen (x div 2) + 1 else 0)" |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
226 |
by (simp add: bitlen_def nat_div_distrib compute_floorlog) |
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
227 |
|
63664 | 228 |
lemma bitlen_eq_zero_iff: "bitlen x = 0 \<longleftrightarrow> x \<le> 0" |
229 |
by (auto simp add: bitlen_alt_def) |
|
230 |
(metis compute_bitlen add.commute bitlen_alt_def bitlen_nonneg less_add_same_cancel2 |
|
231 |
not_less zero_less_one) |
|
232 |
||
233 |
lemma bitlen_div: |
|
234 |
assumes "0 < m" |
|
235 |
shows "1 \<le> real_of_int m / 2^nat (bitlen m - 1)" |
|
236 |
and "real_of_int m / 2^nat (bitlen m - 1) < 2" |
|
237 |
proof - |
|
238 |
let ?B = "2^nat (bitlen m - 1)" |
|
239 |
||
240 |
have "?B \<le> m" using bitlen_bounds[OF \<open>0 <m\<close>] .. |
|
241 |
then have "1 * ?B \<le> real_of_int m" |
|
242 |
unfolding of_int_le_iff[symmetric] by auto |
|
243 |
then show "1 \<le> real_of_int m / ?B" by auto |
|
244 |
||
245 |
from assms have "m \<noteq> 0" by auto |
|
246 |
from assms have "0 \<le> bitlen m - 1" by (auto simp: bitlen_alt_def) |
|
247 |
||
248 |
have "m < 2^nat(bitlen m)" using bitlen_bounds[OF assms] .. |
|
249 |
also from assms have "\<dots> = 2^nat(bitlen m - 1 + 1)" |
|
250 |
by (auto simp: bitlen_def) |
|
251 |
also have "\<dots> = ?B * 2" |
|
252 |
unfolding nat_add_distrib[OF \<open>0 \<le> bitlen m - 1\<close> zero_le_one] by auto |
|
253 |
finally have "real_of_int m < 2 * ?B" |
|
66912
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
254 |
by (metis (full_types) mult.commute power.simps(2) of_int_less_numeral_power_cancel_iff) |
63664 | 255 |
then have "real_of_int m / ?B < 2 * ?B / ?B" |
256 |
by (rule divide_strict_right_mono) auto |
|
257 |
then show "real_of_int m / ?B < 2" by auto |
|
258 |
qed |
|
259 |
||
66912
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
260 |
lemma bitlen_le_iff_floorlog: "bitlen x \<le> w \<longleftrightarrow> w \<ge> 0 \<and> floorlog 2 (nat x) \<le> nat w" |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
261 |
by (auto simp: bitlen_def) |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
262 |
|
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
263 |
lemma bitlen_le_iff_power: "bitlen x \<le> w \<longleftrightarrow> w \<ge> 0 \<and> x < 2 ^ nat w" |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
264 |
by (auto simp: bitlen_le_iff_floorlog floorlog_le_iff) |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
265 |
|
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
266 |
lemma less_power_nat_iff_bitlen: "x < 2 ^ w \<longleftrightarrow> bitlen (int x) \<le> w" |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
267 |
using bitlen_le_iff_power[of x w] |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
268 |
by auto |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
269 |
|
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
270 |
lemma bitlen_ge_iff_power: "w \<le> bitlen x \<longleftrightarrow> w \<le> 0 \<or> 2 ^ (nat w - 1) \<le> x" |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
271 |
unfolding bitlen_def |
68406 | 272 |
by (auto simp flip: nat_le_iff intro: floorlog_geI dest: floorlog_geD) |
66912
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
273 |
|
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
274 |
lemma bitlen_twopow_add_eq: "bitlen (2 ^ w + b) = w + 1" if "0 \<le> b" "b < 2 ^ w" |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
275 |
by (auto simp: that nat_add_distrib bitlen_le_iff_power bitlen_ge_iff_power intro!: antisym) |
a99a7cbf0fb5
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
immler
parents:
63664
diff
changeset
|
276 |
|
63663
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset
|
277 |
end |