author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 63664  9ddc48a8635e 
child 66912  a99a7cbf0fb5 
permissions  rwrr 
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)" 
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset

40 
using assms by (simp add: powr_realpow[symmetric]) 
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 

28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset

134 
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

135 

28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset

136 
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

137 
by (simp add: bitlen_def floorlog_def) 
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset

138 

28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset

139 
lemma bitlen_nonneg: "0 \<le> bitlen x" 
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset

140 
by (simp add: bitlen_def) 
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset

141 

28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset

142 
lemma bitlen_bounds: 
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset

143 
assumes "x > 0" 
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset

144 
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

145 
proof  
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset

146 
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

147 
with assms floorlog_bounds[of "nat x" 2] show ?thesis 
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset

148 
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

149 
qed 
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset

150 

28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset

151 
lemma bitlen_pow2[simp]: 
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset

152 
assumes "b > 0" 
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset

153 
shows "bitlen (b * 2 ^ c) = bitlen b + c" 
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset

154 
using assms 
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset

155 
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

156 

28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset

157 
lemma compute_bitlen[code]: 
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset

158 
"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

159 
by (simp add: bitlen_def nat_div_distrib compute_floorlog) 
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset

160 

63664  161 
lemma bitlen_eq_zero_iff: "bitlen x = 0 \<longleftrightarrow> x \<le> 0" 
162 
by (auto simp add: bitlen_alt_def) 

163 
(metis compute_bitlen add.commute bitlen_alt_def bitlen_nonneg less_add_same_cancel2 

164 
not_less zero_less_one) 

165 

166 
lemma bitlen_div: 

167 
assumes "0 < m" 

168 
shows "1 \<le> real_of_int m / 2^nat (bitlen m  1)" 

169 
and "real_of_int m / 2^nat (bitlen m  1) < 2" 

170 
proof  

171 
let ?B = "2^nat (bitlen m  1)" 

172 

173 
have "?B \<le> m" using bitlen_bounds[OF \<open>0 <m\<close>] .. 

174 
then have "1 * ?B \<le> real_of_int m" 

175 
unfolding of_int_le_iff[symmetric] by auto 

176 
then show "1 \<le> real_of_int m / ?B" by auto 

177 

178 
from assms have "m \<noteq> 0" by auto 

179 
from assms have "0 \<le> bitlen m  1" by (auto simp: bitlen_alt_def) 

180 

181 
have "m < 2^nat(bitlen m)" using bitlen_bounds[OF assms] .. 

182 
also from assms have "\<dots> = 2^nat(bitlen m  1 + 1)" 

183 
by (auto simp: bitlen_def) 

184 
also have "\<dots> = ?B * 2" 

185 
unfolding nat_add_distrib[OF \<open>0 \<le> bitlen m  1\<close> zero_le_one] by auto 

186 
finally have "real_of_int m < 2 * ?B" 

187 
by (metis (full_types) mult.commute power.simps(2) real_of_int_less_numeral_power_cancel_iff) 

188 
then have "real_of_int m / ?B < 2 * ?B / ?B" 

189 
by (rule divide_strict_right_mono) auto 

190 
then show "real_of_int m / ?B < 2" by auto 

191 
qed 

192 

63663
28d1deca302e
Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff
changeset

193 
end 