Quelle Log_Nat.thy Sprache: Isabelle

(* Title: HOL/Library/Log_Nat.thy
 Author: Johannes Hölzl, Fabian Immler, Manuel Eberl
 Copyright 2012 TU München
*)

section \<open>Logarithm of Natural Numbers\<close>

theory Log_Nat
imports Complex_Main
begin

subsection \<open>Preliminaries\<close>

lemma divide_nat_diff_div_nat_less_one:
 "real x / real b - real (x div b) < 1" for x b :: nat
proof (cases "b = 0")
 case True
 then show ?thesis
 by simp
next
 case False
 then have "real (x div b) + real (x mod b) / real b - real (x div b) < 1"
 by (simp add: field_simps)
 then show ?thesis
 by (metis of_nat_of_nat_div_aux)
qed

subsection \<open>Floorlog\<close>

definition floorlog :: "nat \ nat \ nat"
 where "floorlog b a = (if a > 0 \ b > 1 then nat \log b a\ + 1 else 0)"

lemma floorlog_mono: "x \ y \ floorlog b x \ floorlog b y"
 by (auto simp: floorlog_def floor_mono nat_mono)

lemma floorlog_bounds:
 "b ^ (floorlog b x - 1) \ x \ x 0" "b > 1"
proof
 show "b ^ (floorlog b x - 1) \ x"
 proof -
 have "b ^ nat \log b x\ = b powr \log b x\"
 using powr_realpow[symmetric, of b "nat \log b x\"] \x > 0\ \b > 1\
 by simp
 also have "\ \ b powr log b x" using \b > 1\ by simp
 also have "\ = real_of_int x" using \0 < x\ \b > 1\ by simp
 finally have "b ^ nat \log b x\ \ real_of_int x" by simp
 then show ?thesis
 using \<open>0 < x\<close> \<open>b > 1\<close> of_nat_le_iff
 by (fastforce simp add: floorlog_def)
 qed
 show "x 0\ \b > 1\ by simp
 also have "\ < b powr (\log b x\ + 1)"
 using that by (intro powr_less_mono) auto
 also have "\ = b ^ nat (\log b (real_of_int x)\ + 1)"
 using that by (simp flip: powr_realpow)
 finally
 have "x x > 0\<close> \<open>b > 1\<close> by (simp add: floorlog_def nat_add_distrib)
 qed
qed

lemma floorlog_power [simp]:
 "floorlog b (a * b ^ c) = floorlog b a + c" if "a > 0" "b > 1"
proof -
 have "\log b a + real c\ = \log b a\ + c" by arith
 then show ?thesis using that
 by (auto simp: floorlog_def log_mult powr_realpow[symmetric] nat_add_distrib)
qed

lemma floor_log_add_eqI:
 "\log b (a + r)\ = \log b a\" if "b > 1" "a \ 1" "0 \ r" "r < 1"
 for a b :: nat and r :: real
proof (rule floor_eq2)
 have "log b a \ log b (a + r)" using that by force
 then show "\log b a\ \ log b (a + r)" by arith
next
 define l::int where "l = int b ^ (nat \log b a\ + 1)"
 have l_def_real: "l = b powr (\log b a\ + 1)"
 using that by (simp add: l_def powr_add powr_real_of_int)
 have "a < l"
 proof -
 have "a = b powr (log b a)" using that by simp
 also have "\ < b powr floor ((log b a) + 1)"
 using that(1) by auto
 also have "\ = l"
 using that by (simp add: l_def powr_real_of_int powr_add)
 finally show ?thesis by simp
 qed
 then have "a + r < l" using that by simp
 then have "log b (a + r) < log b l" using that by simp
 also have "\ = real_of_int \log b a\ + 1"
 using that by (simp add: l_def_real)
 finally show "log b (a + r) < real_of_int \log b a\ + 1" .
qed

lemma floor_log_div:
 "\log b x\ = \log b (x div b)\ + 1" if "b > 1" "x > 0" "x div b > 0"
 for b x :: nat
proof-
 have "\log b x\ = \log b (x / b * b)\" using that by simp
 also have "\ = \log b (x / b) + log b b\"
 using that by (subst log_mult) auto
 also have "\ = \log b (x / b)\ + 1" using that by simp
 also have "\log b (x / b)\ = \log b (x div b + (x / b - x div b))\" by simp
 also have "\ = \log b (x div b)\"
 using that of_nat_div_le_of_nat divide_nat_diff_div_nat_less_one
 by (intro floor_log_add_eqI) auto
 finally show ?thesis .
qed

lemma compute_floorlog [code]:
 "floorlog b x = (if x > 0 \ b > 1 then floorlog b (x div b) + 1 else 0)"
 by (auto simp: floorlog_def floor_log_div[of b x] div_eq_0_iff nat_add_distrib
 intro!: floor_eq2)

lemma floor_log_eq_if:
 "\log b x\ = \log b y\" if "x div b = y div b" "b > 1" "x > 0" "x div b \ 1"
 for b x y :: nat
proof -
 have "y > 0" using that by (auto intro: ccontr)
 thus ?thesis using that by (simp add: floor_log_div)
qed

lemma floorlog_eq_if:
 "floorlog b x = floorlog b y" if "x div b = y div b" "b > 1" "x > 0" "x div b \ 1"
 for b x y :: nat
proof -
 have "y > 0" using that by (auto intro: ccontr)
 then show ?thesis using that
 by (auto simp add: floorlog_def eq_nat_nat_iff intro: floor_log_eq_if)
qed

lemma floorlog_leD:
 "floorlog b x \ w \ b > 1 \ x 1 \ floorlog b x \ w"
 by (drule less_imp_of_nat_less[where 'a=real])
 (auto simp: floorlog_def Suc_le_eq nat_less_iff floor_less_iff log_of_power_less)

lemma floorlog_eq_zero_iff:
 "floorlog b x = 0 \ b \ 1 \ x \ 0"
 by (auto simp: floorlog_def)

lemma floorlog_le_iff:
 "floorlog b x \ w \ b \ 1 \ b > 1 \ 0 \ w \ x 1"
 using that le_log_of_power[of b w x] power_not_zero
 by (force simp: floorlog_def Suc_le_eq powr_realpow not_less Suc_nat_eq_nat_zadd1
 zless_nat_eq_int_zless int_add_floor less_floor_iff
 simp del: floor_add2)

lemma floorlog_geI:
 "w \ floorlog b x" if "b ^ (w - 1) \ x" "b > 1"
 using floorlog_ge_SucI[of b "w - 1" x] that
 by auto

lemma floorlog_geD:
 "b ^ (w - 1) \ x" if "w \ floorlog b x" "w > 0"
proof -
 have "b > 1" "0 < x"
 using that by (auto simp: floorlog_def split: if_splits)
 have "b ^ (w - 1) \ x" if "b ^ w \ x"
 proof -
 have "b ^ (w - 1) \ b ^ w"
 using \<open>b > 1\<close>
 by (auto intro!: power_increasing)
 also note that
 finally show ?thesis .
 qed
 moreover have "b ^ nat \log (real b) (real x)\ \ x" (is "?l \ _")
 proof -
 have "0 \ log (real b) (real x)"
 using \<open>b > 1\<close> \<open>0 < x\<close>
 by auto
 then have "?l \ b powr log (real b) (real x)"
 using \<open>b > 1\<close>
 by (auto simp flip: powr_realpow intro!: powr_mono of_nat_floor)
 also have "\ = x" using \b > 1\ \0 < x\
 by auto
 finally show ?thesis
 unfolding of_nat_le_iff .
 qed
 ultimately show ?thesis
 using that
 by (auto simp: floorlog_def le_nat_iff le_floor_iff le_log_iff powr_realpow
 split: if_splits elim!: le_SucE)
qed

subsection \<open>\<close>

definition ceillog2 :: "nat \ nat" where
 "ceillog2 n = (if n = 0 then 0 else nat \log 2 (real n)\)"

lemma ceillog2_0 [simp]: "ceillog2 0 = 0"
 and ceillog2_Suc_0 [simp]: "ceillog2 (Suc 0) = 0"
 and ceillog2_2 [simp]: "ceillog2 2 = 1"
 by (auto simp: ceillog2_def)

lemma ceillog2_le1_eq_0 [simp]: "n \ 1 \ ceillog2 n = 0"
 by (cases n) auto

lemma ceillog2_2_power [simp]: "ceillog2 (2 ^ n) = n"
 by (auto simp: ceillog2_def)

lemma ceillog2_ge_log:
 assumes "n > 0"
 shows "real (ceillog2 n) \ log 2 (real n)"
proof -
 have "real_of_int \log 2 (real n)\ \ log 2 (real n)"
 by linarith
 thus ?thesis
 using assms unfolding ceillog2_def by auto
qed

lemma ceillog2_less_log:
 assumes "n > 0"
 shows "real (ceillog2 n) < log 2 (real n) + 1"
proof -
 have "real_of_int \log 2 (real n)\ < log 2 (real n) + 1"
 by linarith
 thus ?thesis
 using assms unfolding ceillog2_def by auto
qed

lemma ceillog2_le_iff:
 assumes "n > 0"
 shows "ceillog2 n \ l \ n \ 2 ^ l"
proof -
 have "ceillog2 n \ l \ real n \ 2 ^ l"
 unfolding ceillog2_def using assms by (auto simp: log_le_iff powr_realpow)
 also have "2 ^ l = real (2 ^ l)"
 by simp
 also have "real n \ real (2 ^ l) \ n \ 2 ^ l"
 by linarith
 finally show ?thesis .
qed

lemma ceillog2_ge_iff:
 assumes "n > 0"
 shows "ceillog2 n \ l \ 2 ^ l < 2 * n"
proof -
 have "-1 < (0 :: real)"
 by auto
 also have "\ \ log 2 (real n)"
 using assms by auto
 finally have "ceillog2 n \ l \ real l - 1 < log 2 (real n)"
 unfolding ceillog2_def using assms by (auto simp: le_nat_iff le_ceiling_iff)
 also have "\ \ real l < log 2 (real (2 * n))"
 using assms by (auto simp: log_mult)
 also have "\ \ 2 ^ l < real (2 * n)"
 using assms by (subst less_log_iff) (auto simp: powr_realpow)
 also have "2 ^ l = real (2 ^ l)"
 by simp
 also have "real (2 ^ l) < real (2 * n) \ 2 ^ l < 2 * n"
 by linarith
 finally show ?thesis .
qed

lemma le_two_power_ceillog2: "n \ 2 ^ ceillog2 n"
 using neq0_conv ceillog2_le_iff by blast

lemma two_power_ceillog2_gt:
 assumes "n > 0"
 shows "2 * n > 2 ^ ceillog2 n"
 using ceillog2_ge_iff[of n "ceillog2 n"] assms by simp

lemma ceillog2_eqI:
 assumes "n \ 2 ^ l" "2 ^ l < 2 * n"
 shows "ceillog2 n = l"
 by (metis Suc_leI assms bot_nat_0.not_eq_extremum ceillog2_ge_iff ceillog2_le_iff le_antisym mult_is_0
 not_less_eq_eq)

lemma ceillog2_rec_even:
 assumes "k > 0"
 shows "ceillog2 (2 * k) = Suc (ceillog2 k)"
 by (rule ceillog2_eqI) (auto simp: le_two_power_ceillog2 two_power_ceillog2_gt assms)

lemma ceillog2_mono:
 assumes "m \ n"
 shows "ceillog2 m \ ceillog2 n"
proof (cases "m = 0")
 case False
 have "\log 2 (real m)\ \ \log 2 (real n)\"
 by (intro ceiling_mono) (use False assms in auto)
 hence "nat \log 2 (real m)\ \ nat \log 2 (real n)\"
 by linarith
 thus ?thesis using False assms
 unfolding ceillog2_def by simp
qed auto

lemma ceillog2_rec_odd:
 assumes "k > 0"
 shows "ceillog2 (Suc (2 * k)) = Suc (ceillog2 (Suc k))"
proof -
 have "2 ^ ceillog2 (Suc (2 * k)) > Suc (2 * k)"
 by (metis assms diff_Suc_1 dvd_triv_left le_two_power_ceillog2 mult_pos_pos nat_power_eq_Suc_0_iff
 order_less_le pos2 semiring_parity_class.even_mask_iff)
 then have "ceillog2 (2 * k + 2) \ ceillog2 (2 * k + 1)"
 by (simp add: ceillog2_le_iff)
 moreover have "ceillog2 (2 * k + 2) \ ceillog2 (2 * k + 1)"
 by (rule ceillog2_mono) auto
 ultimately have "ceillog2 (2 * k + 2) = ceillog2 (2 * k + 1)"
 by (rule antisym)
 also have "2 * k + 2 = 2 * Suc k"
 by simp
 also have "ceillog2 (2 * Suc k) = Suc (ceillog2 (Suc k))"
 by (rule ceillog2_rec_even) auto
 finally show ?thesis
 by simp
qed

(* TODO: better code is possible using bitlen and "count trailing 0 bits" *)
lemma ceillog2_rec:
 "ceillog2 n = (if n \ 1 then 0 else 1 + ceillog2 ((n + 1) div 2))"
proof (cases "n \ 1")
 case True
 thus ?thesis
 by (cases n) auto
next
 case False
 thus ?thesis
 by (cases "even n") (auto elim!: evenE oddE simp: ceillog2_rec_even ceillog2_rec_odd)
qed

lemma funpow_div2_ceillog2_le_1:
 "((\n. (n + 1) div 2) ^^ ceillog2 n) n \ 1"
proof (induction n rule: less_induct)
 case (less n)
 show ?case
 proof (cases "n \ 1")
 case True
 thus ?thesis by (cases n) auto
 next
 case False
 have "((\n. (n + 1) div 2) ^^ Suc (ceillog2 ((n + 1) div 2))) n \ 1"
 using less.IH[of "(n+1) div 2"] False by (subst funpow_Suc_right) auto
 also have "Suc (ceillog2 ((n + 1) div 2)) = ceillog2 n"
 using False by (subst ceillog2_rec[of n]) auto
 finally show ?thesis .
 qed
qed

fun ceillog2_aux :: "nat \ nat \ nat" where
 "ceillog2_aux acc n = (if n \ 1 then acc else ceillog2_aux (acc + 1) ((n + 1) div 2))"

lemmas [simp del] = ceillog2_aux.simps

lemma ceillog2_aux_correct: "ceillog2_aux acc n = ceillog2 n + acc"
proof (induction acc n rule: ceillog2_aux.induct)
 case (1 acc n)
 show ?case
 proof (cases "n \ 1")
 case False
 thus ?thesis using ceillog2_rec[of n] "1.IH"
 by (auto simp: ceillog2_aux.simps[of acc n])
 qed (auto simp: ceillog2_aux.simps[of acc n])
qed

(* TODO: better code equation using bit operations *)
lemma ceillog2_code [code]: "ceillog2 n = ceillog2_aux 0 n"
 by (simp add: ceillog2_aux_correct)

subsection \<open>Bitlen\<close>

definition bitlen :: "int \ int"
 where "bitlen a = floorlog 2 (nat a)"

lemma bitlen_alt_def:
 "bitlen a = (if a > 0 then \log 2 a\ + 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 \ bitlen x"
 by (simp add: bitlen_def)

lemma bitlen_bounds:
 "2 ^ nat (bitlen x - 1) \ x \ x < 2 ^ nat (bitlen x)" if "x > 0"
proof -
 from that have "bitlen x \ 1" by (auto simp: bitlen_alt_def)
 with that floorlog_bounds[of "nat x" 2] show ?thesis
 by (auto simp add: bitlen_def le_nat_iff nat_less_iff nat_diff_distrib)
qed

lemma bitlen_pow2 [simp]:
 "bitlen (b * 2 ^ c) = bitlen b + c" if "b > 0"
 using that by (simp add: bitlen_def nat_mult_distrib nat_power_eq)

lemma compute_bitlen [code]:
 "bitlen x = (if x > 0 then bitlen (x div 2) + 1 else 0)"
 by (simp add: bitlen_def nat_div_distrib compute_floorlog)

lemma bitlen_eq_zero_iff:
 "bitlen x = 0 \ x \ 0"
 by (auto simp add: bitlen_alt_def)
 (metis compute_bitlen add.commute bitlen_alt_def bitlen_nonneg less_add_same_cancel2
 not_less zero_less_one)

lemma bitlen_div:
 "1 \ real_of_int m / 2^nat (bitlen m - 1)"
 and "real_of_int m / 2^nat (bitlen m - 1) < 2" if "0 < m"
proof -
 let ?B = "2^nat (bitlen m - 1)"

 have "?B \ m" using bitlen_bounds[OF \0 ] ..
 then have "1 * ?B \ real_of_int m"
 unfolding of_int_le_iff[symmetric] by auto
 then show "1 \ real_of_int m / ?B" by auto

 from that have "0 \ bitlen m - 1" by (auto simp: bitlen_alt_def)

 have "m < 2^nat(bitlen m)" using bitlen_bounds[OF that] ..
 also from that have "\ = 2^nat(bitlen m - 1 + 1)"
 by (auto simp: bitlen_def)
 also have "\ = ?B * 2"
 unfolding nat_add_distrib[OF \<open>0 \<le> bitlen m - 1\<close> zero_le_one] by auto
 finally have "real_of_int m < 2 * ?B"
 by (metis (full_types) mult.commute power.simps(2) of_int_less_numeral_power_cancel_iff)
 then have "real_of_int m / ?B < 2 * ?B / ?B"
 by (rule divide_strict_right_mono) auto
 then show "real_of_int m / ?B < 2" by auto
qed

lemma bitlen_le_iff_floorlog:
 "bitlen x \ w \ w \ 0 \ floorlog 2 (nat x) \ nat w"
 by (auto simp: bitlen_def)

lemma bitlen_le_iff_power:
 "bitlen x \ w \ w \ 0 \ x < 2 ^ nat w"
 by (auto simp: bitlen_le_iff_floorlog floorlog_le_iff)

lemma less_power_nat_iff_bitlen:
 "x < 2 ^ w \ bitlen (int x) \ w"
 using bitlen_le_iff_power[of x w]
 by auto

lemma bitlen_ge_iff_power:
 "w \ bitlen x \ w \ 0 \ 2 ^ (nat w - 1) \ x"
 unfolding bitlen_def
 by (auto simp flip: nat_le_iff intro: floorlog_geI dest: floorlog_geD)

lemma bitlen_twopow_add_eq:
 "bitlen (2 ^ w + b) = w + 1" if "0 \ b" "b < 2 ^ w"
 by (auto simp: that nat_add_distrib bitlen_le_iff_power bitlen_ge_iff_power intro!: antisym)

end

quality100%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.