Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Thinking Intellekt

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/Library/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Log_Nat.thy Sprache: Isabelle

Original von: Isabelle^©

(* Title: HOL/Library/Log_Nat.thy
 Author: Johannes Hölzl, Fabian Immler
 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 (simp add: real_of_nat_div_aux [symmetric])
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 real_of_nat_div4 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 simp: )
 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>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

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.