src/HOL/Library/Discrete.thy
author Manuel Eberl <eberlm@in.tum.de>
Thu Sep 01 11:53:07 2016 +0200 (2016-09-01)
changeset 63766 695d60817cb1
parent 63540 f8652d0534fa
child 64449 8c44dfb4ca8a
permissions -rw-r--r--
Some facts about factorial and binomial coefficients
wenzelm@59349
     1
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@51174
     2
wenzelm@60500
     3
section \<open>Common discrete functions\<close>
haftmann@51174
     4
haftmann@51174
     5
theory Discrete
haftmann@51174
     6
imports Main
haftmann@51174
     7
begin
haftmann@51174
     8
wenzelm@60500
     9
subsection \<open>Discrete logarithm\<close>
haftmann@51174
    10
wenzelm@61115
    11
context
wenzelm@61115
    12
begin
wenzelm@61115
    13
wenzelm@61115
    14
qualified fun log :: "nat \<Rightarrow> nat"
wenzelm@59349
    15
  where [simp del]: "log n = (if n < 2 then 0 else Suc (log (n div 2)))"
haftmann@51174
    16
haftmann@61831
    17
lemma log_induct [consumes 1, case_names one double]:
haftmann@61831
    18
  fixes n :: nat
haftmann@61831
    19
  assumes "n > 0"
haftmann@61831
    20
  assumes one: "P 1"
haftmann@61831
    21
  assumes double: "\<And>n. n \<ge> 2 \<Longrightarrow> P (n div 2) \<Longrightarrow> P n"
haftmann@61831
    22
  shows "P n"
wenzelm@61975
    23
using \<open>n > 0\<close> proof (induct n rule: log.induct)
haftmann@61831
    24
  fix n
haftmann@61831
    25
  assume "\<not> n < 2 \<Longrightarrow>
haftmann@61831
    26
          0 < n div 2 \<Longrightarrow> P (n div 2)"
haftmann@61831
    27
  then have *: "n \<ge> 2 \<Longrightarrow> P (n div 2)" by simp
haftmann@61831
    28
  assume "n > 0"
haftmann@61831
    29
  show "P n"
haftmann@61831
    30
  proof (cases "n = 1")
wenzelm@63540
    31
    case True
wenzelm@63540
    32
    with one show ?thesis by simp
haftmann@61831
    33
  next
wenzelm@63540
    34
    case False
wenzelm@63540
    35
    with \<open>n > 0\<close> have "n \<ge> 2" by auto
wenzelm@63540
    36
    with * have "P (n div 2)" .
wenzelm@63540
    37
    with \<open>n \<ge> 2\<close> show ?thesis by (rule double)
haftmann@61831
    38
  qed
haftmann@61831
    39
qed
haftmann@61831
    40
  
wenzelm@59349
    41
lemma log_zero [simp]: "log 0 = 0"
haftmann@51174
    42
  by (simp add: log.simps)
haftmann@51174
    43
wenzelm@59349
    44
lemma log_one [simp]: "log 1 = 0"
haftmann@51174
    45
  by (simp add: log.simps)
haftmann@51174
    46
wenzelm@59349
    47
lemma log_Suc_zero [simp]: "log (Suc 0) = 0"
haftmann@51174
    48
  using log_one by simp
haftmann@51174
    49
wenzelm@59349
    50
lemma log_rec: "n \<ge> 2 \<Longrightarrow> log n = Suc (log (n div 2))"
haftmann@51174
    51
  by (simp add: log.simps)
haftmann@51174
    52
wenzelm@59349
    53
lemma log_twice [simp]: "n \<noteq> 0 \<Longrightarrow> log (2 * n) = Suc (log n)"
haftmann@51174
    54
  by (simp add: log_rec)
haftmann@51174
    55
wenzelm@59349
    56
lemma log_half [simp]: "log (n div 2) = log n - 1"
haftmann@51174
    57
proof (cases "n < 2")
haftmann@51174
    58
  case True
haftmann@51174
    59
  then have "n = 0 \<or> n = 1" by arith
haftmann@51174
    60
  then show ?thesis by (auto simp del: One_nat_def)
haftmann@51174
    61
next
wenzelm@59349
    62
  case False
wenzelm@59349
    63
  then show ?thesis by (simp add: log_rec)
haftmann@51174
    64
qed
haftmann@51174
    65
wenzelm@59349
    66
lemma log_exp [simp]: "log (2 ^ n) = n"
haftmann@51174
    67
  by (induct n) simp_all
haftmann@51174
    68
wenzelm@59349
    69
lemma log_mono: "mono log"
haftmann@51174
    70
proof
haftmann@51174
    71
  fix m n :: nat
haftmann@51174
    72
  assume "m \<le> n"
haftmann@51174
    73
  then show "log m \<le> log n"
haftmann@51174
    74
  proof (induct m arbitrary: n rule: log.induct)
haftmann@51174
    75
    case (1 m)
haftmann@51174
    76
    then have mn2: "m div 2 \<le> n div 2" by arith
haftmann@51174
    77
    show "log m \<le> log n"
haftmann@61831
    78
    proof (cases "m \<ge> 2")
haftmann@61831
    79
      case False
haftmann@51174
    80
      then have "m = 0 \<or> m = 1" by arith
haftmann@51174
    81
      then show ?thesis by (auto simp del: One_nat_def)
haftmann@51174
    82
    next
haftmann@61831
    83
      case True then have "\<not> m < 2" by simp
haftmann@61831
    84
      with mn2 have "n \<ge> 2" by arith
haftmann@61831
    85
      from True have m2_0: "m div 2 \<noteq> 0" by arith
haftmann@51174
    86
      with mn2 have n2_0: "n div 2 \<noteq> 0" by arith
wenzelm@61975
    87
      from \<open>\<not> m < 2\<close> "1.hyps" mn2 have "log (m div 2) \<le> log (n div 2)" by blast
haftmann@51174
    88
      with m2_0 n2_0 have "log (2 * (m div 2)) \<le> log (2 * (n div 2))" by simp
wenzelm@60500
    89
      with m2_0 n2_0 \<open>m \<ge> 2\<close> \<open>n \<ge> 2\<close> show ?thesis by (simp only: log_rec [of m] log_rec [of n]) simp
haftmann@51174
    90
    qed
haftmann@51174
    91
  qed
haftmann@51174
    92
qed
haftmann@51174
    93
haftmann@61831
    94
lemma log_exp2_le:
haftmann@61831
    95
  assumes "n > 0"
haftmann@61831
    96
  shows "2 ^ log n \<le> n"
wenzelm@63516
    97
  using assms
wenzelm@63516
    98
proof (induct n rule: log_induct)
wenzelm@63516
    99
  case one
wenzelm@63516
   100
  then show ?case by simp
haftmann@61831
   101
next
wenzelm@63516
   102
  case (double n)
haftmann@61831
   103
  with log_mono have "log n \<ge> Suc 0"
haftmann@61831
   104
    by (simp add: log.simps)
haftmann@61831
   105
  assume "2 ^ log (n div 2) \<le> n div 2"
wenzelm@61975
   106
  with \<open>n \<ge> 2\<close> have "2 ^ (log n - Suc 0) \<le> n div 2" by simp
haftmann@61831
   107
  then have "2 ^ (log n - Suc 0) * 2 ^ 1 \<le> n div 2 * 2" by simp
wenzelm@61975
   108
  with \<open>log n \<ge> Suc 0\<close> have "2 ^ log n \<le> n div 2 * 2"
haftmann@61831
   109
    unfolding power_add [symmetric] by simp
haftmann@61831
   110
  also have "n div 2 * 2 \<le> n" by (cases "even n") simp_all
wenzelm@63516
   111
  finally show ?case .
haftmann@61831
   112
qed
haftmann@61831
   113
haftmann@51174
   114
wenzelm@60500
   115
subsection \<open>Discrete square root\<close>
haftmann@51174
   116
wenzelm@61115
   117
qualified definition sqrt :: "nat \<Rightarrow> nat"
wenzelm@59349
   118
  where "sqrt n = Max {m. m\<^sup>2 \<le> n}"
haftmann@51263
   119
haftmann@51263
   120
lemma sqrt_aux:
haftmann@51263
   121
  fixes n :: nat
wenzelm@53015
   122
  shows "finite {m. m\<^sup>2 \<le> n}" and "{m. m\<^sup>2 \<le> n} \<noteq> {}"
haftmann@51263
   123
proof -
haftmann@51263
   124
  { fix m
wenzelm@53015
   125
    assume "m\<^sup>2 \<le> n"
haftmann@51263
   126
    then have "m \<le> n"
haftmann@51263
   127
      by (cases m) (simp_all add: power2_eq_square)
haftmann@51263
   128
  } note ** = this
wenzelm@53015
   129
  then have "{m. m\<^sup>2 \<le> n} \<subseteq> {m. m \<le> n}" by auto
wenzelm@53015
   130
  then show "finite {m. m\<^sup>2 \<le> n}" by (rule finite_subset) rule
wenzelm@53015
   131
  have "0\<^sup>2 \<le> n" by simp
wenzelm@53015
   132
  then show *: "{m. m\<^sup>2 \<le> n} \<noteq> {}" by blast
haftmann@51263
   133
qed
haftmann@51263
   134
eberlm@63766
   135
lemma sqrt_unique:
eberlm@63766
   136
  assumes "m^2 \<le> n" "n < (Suc m)^2"
eberlm@63766
   137
  shows   "Discrete.sqrt n = m"
eberlm@63766
   138
proof -
eberlm@63766
   139
  have "m' \<le> m" if "m'^2 \<le> n" for m'
eberlm@63766
   140
  proof -
eberlm@63766
   141
    note that
eberlm@63766
   142
    also note assms(2)
eberlm@63766
   143
    finally have "m' < Suc m" by (rule power_less_imp_less_base) simp_all
eberlm@63766
   144
    thus "m' \<le> m" by simp
eberlm@63766
   145
  qed
eberlm@63766
   146
  with \<open>m^2 \<le> n\<close> sqrt_aux[of n] show ?thesis unfolding Discrete.sqrt_def
eberlm@63766
   147
    by (intro antisym Max.boundedI Max.coboundedI) simp_all
eberlm@63766
   148
qed
eberlm@63766
   149
eberlm@63766
   150
eberlm@63766
   151
lemma sqrt_code[code]: "sqrt n = Max (Set.filter (\<lambda>m. m\<^sup>2 \<le> n) {0..n})"
haftmann@51263
   152
proof -
wenzelm@53015
   153
  from power2_nat_le_imp_le [of _ n] have "{m. m \<le> n \<and> m\<^sup>2 \<le> n} = {m. m\<^sup>2 \<le> n}" by auto
haftmann@51263
   154
  then show ?thesis by (simp add: sqrt_def Set.filter_def)
haftmann@51263
   155
qed
haftmann@51174
   156
wenzelm@59349
   157
lemma sqrt_inverse_power2 [simp]: "sqrt (n\<^sup>2) = n"
haftmann@51174
   158
proof -
haftmann@51174
   159
  have "{m. m \<le> n} \<noteq> {}" by auto
haftmann@51174
   160
  then have "Max {m. m \<le> n} \<le> n" by auto
haftmann@51174
   161
  then show ?thesis
haftmann@51174
   162
    by (auto simp add: sqrt_def power2_nat_le_eq_le intro: antisym)
haftmann@51174
   163
qed
haftmann@51174
   164
wenzelm@59349
   165
lemma sqrt_zero [simp]: "sqrt 0 = 0"
haftmann@58787
   166
  using sqrt_inverse_power2 [of 0] by simp
haftmann@58787
   167
wenzelm@59349
   168
lemma sqrt_one [simp]: "sqrt 1 = 1"
haftmann@58787
   169
  using sqrt_inverse_power2 [of 1] by simp
haftmann@58787
   170
wenzelm@59349
   171
lemma mono_sqrt: "mono sqrt"
haftmann@51263
   172
proof
haftmann@51263
   173
  fix m n :: nat
haftmann@51263
   174
  have *: "0 * 0 \<le> m" by simp
haftmann@51263
   175
  assume "m \<le> n"
haftmann@51263
   176
  then show "sqrt m \<le> sqrt n"
wenzelm@60500
   177
    by (auto intro!: Max_mono \<open>0 * 0 \<le> m\<close> finite_less_ub simp add: power2_eq_square sqrt_def)
haftmann@51263
   178
qed
haftmann@51263
   179
eberlm@63766
   180
lemma mono_sqrt': "m \<le> n \<Longrightarrow> Discrete.sqrt m \<le> Discrete.sqrt n"
eberlm@63766
   181
  using mono_sqrt unfolding mono_def by auto
eberlm@63766
   182
wenzelm@59349
   183
lemma sqrt_greater_zero_iff [simp]: "sqrt n > 0 \<longleftrightarrow> n > 0"
haftmann@51174
   184
proof -
wenzelm@53015
   185
  have *: "0 < Max {m. m\<^sup>2 \<le> n} \<longleftrightarrow> (\<exists>a\<in>{m. m\<^sup>2 \<le> n}. 0 < a)"
haftmann@51263
   186
    by (rule Max_gr_iff) (fact sqrt_aux)+
haftmann@51263
   187
  show ?thesis
haftmann@51263
   188
  proof
haftmann@51263
   189
    assume "0 < sqrt n"
wenzelm@53015
   190
    then have "0 < Max {m. m\<^sup>2 \<le> n}" by (simp add: sqrt_def)
haftmann@51263
   191
    with * show "0 < n" by (auto dest: power2_nat_le_imp_le)
haftmann@51263
   192
  next
haftmann@51263
   193
    assume "0 < n"
wenzelm@53015
   194
    then have "1\<^sup>2 \<le> n \<and> 0 < (1::nat)" by simp
wenzelm@53015
   195
    then have "\<exists>q. q\<^sup>2 \<le> n \<and> 0 < q" ..
wenzelm@53015
   196
    with * have "0 < Max {m. m\<^sup>2 \<le> n}" by blast
haftmann@51263
   197
    then show "0 < sqrt n" by  (simp add: sqrt_def)
haftmann@51263
   198
  qed
haftmann@51263
   199
qed
haftmann@51263
   200
wenzelm@59349
   201
lemma sqrt_power2_le [simp]: "(sqrt n)\<^sup>2 \<le> n" (* FIXME tune proof *)
haftmann@51263
   202
proof (cases "n > 0")
haftmann@58787
   203
  case False then show ?thesis by simp
haftmann@51263
   204
next
haftmann@51263
   205
  case True then have "sqrt n > 0" by simp
wenzelm@53015
   206
  then have "mono (times (Max {m. m\<^sup>2 \<le> n}))" by (auto intro: mono_times_nat simp add: sqrt_def)
wenzelm@53015
   207
  then have *: "Max {m. m\<^sup>2 \<le> n} * Max {m. m\<^sup>2 \<le> n} = Max (times (Max {m. m\<^sup>2 \<le> n}) ` {m. m\<^sup>2 \<le> n})"
haftmann@51263
   208
    using sqrt_aux [of n] by (rule mono_Max_commute)
haftmann@51263
   209
  have "Max (op * (Max {m. m * m \<le> n}) ` {m. m * m \<le> n}) \<le> n"
haftmann@51263
   210
    apply (subst Max_le_iff)
haftmann@51263
   211
    apply (metis (mono_tags) finite_imageI finite_less_ub le_square)
haftmann@51263
   212
    apply simp
haftmann@51263
   213
    apply (metis le0 mult_0_right)
haftmann@51263
   214
    apply auto
haftmann@51263
   215
    proof -
haftmann@51263
   216
      fix q
haftmann@51263
   217
      assume "q * q \<le> n"
haftmann@51263
   218
      show "Max {m. m * m \<le> n} * q \<le> n"
haftmann@51263
   219
      proof (cases "q > 0")
haftmann@51263
   220
        case False then show ?thesis by simp
haftmann@51263
   221
      next
haftmann@51263
   222
        case True then have "mono (times q)" by (rule mono_times_nat)
haftmann@51263
   223
        then have "q * Max {m. m * m \<le> n} = Max (times q ` {m. m * m \<le> n})"
haftmann@51263
   224
          using sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute)
haftmann@57514
   225
        then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: ac_simps)
wenzelm@59349
   226
        then show ?thesis
wenzelm@59349
   227
          apply simp
haftmann@51263
   228
          apply (subst Max_le_iff)
haftmann@51263
   229
          apply auto
haftmann@51263
   230
          apply (metis (mono_tags) finite_imageI finite_less_ub le_square)
wenzelm@60500
   231
          apply (metis \<open>q * q \<le> n\<close>)
wenzelm@60500
   232
          apply (metis \<open>q * q \<le> n\<close> le_cases mult_le_mono1 mult_le_mono2 order_trans)
wenzelm@59349
   233
          done
haftmann@51263
   234
      qed
haftmann@51263
   235
    qed
haftmann@51263
   236
  with * show ?thesis by (simp add: sqrt_def power2_eq_square)
haftmann@51174
   237
qed
haftmann@51174
   238
wenzelm@59349
   239
lemma sqrt_le: "sqrt n \<le> n"
haftmann@51263
   240
  using sqrt_aux [of n] by (auto simp add: sqrt_def intro: power2_nat_le_imp_le)
haftmann@51174
   241
haftmann@51174
   242
end
haftmann@51174
   243
nipkow@62390
   244
end