src/HOL/Library/Log_Nat.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 63664 9ddc48a8635e
child 66912 a99a7cbf0fb5
permissions -rw-r--r--
executable domain membership checks
     1 (*  Title:      HOL/Library/Log_Nat.thy
     2     Author:     Johannes Hölzl, Fabian Immler
     3     Copyright   2012  TU München
     4 *)
     5 
     6 section \<open>Logarithm of Natural Numbers\<close>
     7 
     8 theory Log_Nat
     9 imports Complex_Main
    10 begin
    11 
    12 definition floorlog :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
    13 "floorlog b a = (if a > 0 \<and> b > 1 then nat \<lfloor>log b a\<rfloor> + 1 else 0)"
    14 
    15 lemma floorlog_mono: "x \<le> y \<Longrightarrow> floorlog b x \<le> floorlog b y"
    16 by(auto simp: floorlog_def floor_mono nat_mono)
    17 
    18 lemma floorlog_bounds:
    19   assumes "x > 0" "b > 1"
    20   shows "b ^ (floorlog b x - 1) \<le> x \<and> x < b ^ (floorlog b x)"
    21 proof
    22   show "b ^ (floorlog b x - 1) \<le> x"
    23   proof -
    24     have "b ^ nat \<lfloor>log b x\<rfloor> = b powr \<lfloor>log b x\<rfloor>"
    25       using powr_realpow[symmetric, of b "nat \<lfloor>log b x\<rfloor>"] \<open>x > 0\<close> \<open>b > 1\<close>
    26       by simp
    27     also have "\<dots> \<le> b powr log b x" using \<open>b > 1\<close> by simp
    28     also have "\<dots> = real_of_int x" using \<open>0 < x\<close> \<open>b > 1\<close> by simp
    29     finally have "b ^ nat \<lfloor>log b x\<rfloor> \<le> real_of_int x" by simp
    30     then show ?thesis
    31       using \<open>0 < x\<close> \<open>b > 1\<close> of_nat_le_iff
    32       by (fastforce simp add: floorlog_def)
    33   qed
    34   show "x < b ^ (floorlog b x)"
    35   proof -
    36     have "x \<le> b powr (log b x)" using \<open>x > 0\<close> \<open>b > 1\<close> by simp
    37     also have "\<dots> < b powr (\<lfloor>log b x\<rfloor> + 1)"
    38       using assms by (intro powr_less_mono) auto
    39     also have "\<dots> = b ^ nat (\<lfloor>log b (real_of_int x)\<rfloor> + 1)"
    40       using assms by (simp add: powr_realpow[symmetric])
    41     finally
    42     have "x < b ^ nat (\<lfloor>log b (int x)\<rfloor> + 1)"
    43       by (rule of_nat_less_imp_less)
    44     then show ?thesis
    45       using \<open>x > 0\<close> \<open>b > 1\<close> by (simp add: floorlog_def nat_add_distrib)
    46   qed
    47 qed
    48 
    49 lemma floorlog_power[simp]:
    50   assumes "a > 0" "b > 1"
    51   shows "floorlog b (a * b ^ c) = floorlog b a + c"
    52 proof -
    53   have "\<lfloor>log b a + real c\<rfloor> = \<lfloor>log b a\<rfloor> + c" by arith
    54   then show ?thesis using assms
    55     by (auto simp: floorlog_def log_mult powr_realpow[symmetric] nat_add_distrib)
    56 qed
    57 
    58 lemma floor_log_add_eqI:
    59   fixes a::nat and b::nat and r::real
    60   assumes "b > 1" "a \<ge> 1" "0 \<le> r" "r < 1"
    61   shows "\<lfloor>log b (a + r)\<rfloor> = \<lfloor>log b a\<rfloor>"
    62 proof (rule floor_eq2)
    63   have "log b a \<le> log b (a + r)" using assms by force
    64   then show "\<lfloor>log b a\<rfloor> \<le> log b (a + r)" by arith
    65 next
    66   define l::int where "l = int b ^ (nat \<lfloor>log b a\<rfloor> + 1)"
    67   have l_def_real: "l = b powr (\<lfloor>log b a\<rfloor> + 1)"
    68     using assms by (simp add: l_def powr_add powr_real_of_int)
    69   have "a < l"
    70   proof -
    71     have "a = b powr (log b a)" using assms by simp
    72     also have "\<dots> < b powr floor ((log b a) + 1)"
    73       using assms(1) by auto
    74     also have "\<dots> = l"
    75       using assms by (simp add: l_def powr_real_of_int powr_add)
    76     finally show ?thesis by simp
    77   qed
    78   then have "a + r < l" using assms by simp
    79   then have "log b (a + r) < log b l" using assms by simp
    80   also have "\<dots> = real_of_int \<lfloor>log b a\<rfloor> + 1"
    81     using assms by (simp add: l_def_real)
    82   finally show "log b (a + r) < real_of_int \<lfloor>log b a\<rfloor> + 1" .
    83 qed
    84 
    85 lemma divide_nat_diff_div_nat_less_one:
    86   fixes x b::nat shows "x / b - x div b < 1"
    87 proof -
    88   have "int 0 \<noteq> \<lfloor>1::real\<rfloor>" by simp
    89   thus ?thesis
    90     by (metis add_diff_cancel_left' floor_divide_of_nat_eq less_eq_real_def
    91         mod_div_trivial real_of_nat_div3 real_of_nat_div_aux)
    92 qed
    93 
    94 lemma floor_log_div:
    95   fixes b x :: nat assumes "b > 1" "x > 0" "x div b > 0"
    96   shows "\<lfloor>log b x\<rfloor> = \<lfloor>log b (x div b)\<rfloor> + 1"
    97 proof-
    98   have "\<lfloor>log b x\<rfloor> = \<lfloor>log b (x / b * b)\<rfloor>" using assms by simp
    99   also have "\<dots> = \<lfloor>log b (x / b) + log b b\<rfloor>"
   100     using assms by (subst log_mult) auto
   101   also have "\<dots> = \<lfloor>log b (x / b)\<rfloor> + 1" using assms by simp
   102   also have "\<lfloor>log b (x / b)\<rfloor> = \<lfloor>log b (x div b + (x / b - x div b))\<rfloor>" by simp
   103   also have "\<dots> = \<lfloor>log b (x div b)\<rfloor>"
   104     using assms real_of_nat_div4 divide_nat_diff_div_nat_less_one
   105     by (intro floor_log_add_eqI) auto
   106   finally show ?thesis .
   107 qed
   108 
   109 lemma compute_floorlog[code]:
   110   "floorlog b x = (if x > 0 \<and> b > 1 then floorlog b (x div b) + 1 else 0)"
   111 by (auto simp: floorlog_def floor_log_div[of b x] div_eq_0_iff nat_add_distrib
   112     intro!: floor_eq2)
   113 
   114 lemma floor_log_eq_if:
   115   fixes b x y :: nat
   116   assumes "x div b = y div b" "b > 1" "x > 0" "x div b \<ge> 1"
   117   shows "floor(log b x) = floor(log b y)"
   118 proof -
   119   have "y > 0" using assms by(auto intro: ccontr)
   120   thus ?thesis using assms by (simp add: floor_log_div)
   121 qed
   122 
   123 lemma floorlog_eq_if:
   124   fixes b x y :: nat
   125   assumes "x div b = y div b" "b > 1" "x > 0" "x div b \<ge> 1"
   126   shows "floorlog b x = floorlog b y"
   127 proof -
   128   have "y > 0" using assms by(auto intro: ccontr)
   129   thus ?thesis using assms
   130     by(auto simp add: floorlog_def eq_nat_nat_iff intro: floor_log_eq_if)
   131 qed
   132 
   133 
   134 definition bitlen :: "int \<Rightarrow> int" where "bitlen a = floorlog 2 (nat a)"
   135 
   136 lemma bitlen_alt_def: "bitlen a = (if a > 0 then \<lfloor>log 2 a\<rfloor> + 1 else 0)"
   137 by (simp add: bitlen_def floorlog_def)
   138 
   139 lemma bitlen_nonneg: "0 \<le> bitlen x"
   140 by (simp add: bitlen_def)
   141 
   142 lemma bitlen_bounds:
   143   assumes "x > 0"
   144   shows "2 ^ nat (bitlen x - 1) \<le> x \<and> x < 2 ^ nat (bitlen x)"
   145 proof -
   146   from assms have "bitlen x \<ge> 1" by (auto simp: bitlen_alt_def)
   147   with assms floorlog_bounds[of "nat x" 2] show ?thesis
   148     by (auto simp add: bitlen_def le_nat_iff nat_less_iff nat_diff_distrib)
   149 qed
   150 
   151 lemma bitlen_pow2[simp]:
   152   assumes "b > 0"
   153   shows "bitlen (b * 2 ^ c) = bitlen b + c"
   154   using assms
   155   by (simp add: bitlen_def nat_mult_distrib nat_power_eq)
   156 
   157 lemma compute_bitlen[code]:
   158   "bitlen x = (if x > 0 then bitlen (x div 2) + 1 else 0)"
   159 by (simp add: bitlen_def nat_div_distrib compute_floorlog)
   160 
   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 
   193 end