src/HOL/Library/Discrete.thy
author nipkow
Tue Sep 22 14:31:22 2015 +0200 (2015-09-22)
changeset 61225 1a690dce8cfc
parent 61115 3a4400985780
child 61831 c43f87119d80
permissions -rw-r--r--
tuned references
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
wenzelm@59349
    17
lemma log_zero [simp]: "log 0 = 0"
haftmann@51174
    18
  by (simp add: log.simps)
haftmann@51174
    19
wenzelm@59349
    20
lemma log_one [simp]: "log 1 = 0"
haftmann@51174
    21
  by (simp add: log.simps)
haftmann@51174
    22
wenzelm@59349
    23
lemma log_Suc_zero [simp]: "log (Suc 0) = 0"
haftmann@51174
    24
  using log_one by simp
haftmann@51174
    25
wenzelm@59349
    26
lemma log_rec: "n \<ge> 2 \<Longrightarrow> log n = Suc (log (n div 2))"
haftmann@51174
    27
  by (simp add: log.simps)
haftmann@51174
    28
wenzelm@59349
    29
lemma log_twice [simp]: "n \<noteq> 0 \<Longrightarrow> log (2 * n) = Suc (log n)"
haftmann@51174
    30
  by (simp add: log_rec)
haftmann@51174
    31
wenzelm@59349
    32
lemma log_half [simp]: "log (n div 2) = log n - 1"
haftmann@51174
    33
proof (cases "n < 2")
haftmann@51174
    34
  case True
haftmann@51174
    35
  then have "n = 0 \<or> n = 1" by arith
haftmann@51174
    36
  then show ?thesis by (auto simp del: One_nat_def)
haftmann@51174
    37
next
wenzelm@59349
    38
  case False
wenzelm@59349
    39
  then show ?thesis by (simp add: log_rec)
haftmann@51174
    40
qed
haftmann@51174
    41
wenzelm@59349
    42
lemma log_exp [simp]: "log (2 ^ n) = n"
haftmann@51174
    43
  by (induct n) simp_all
haftmann@51174
    44
wenzelm@59349
    45
lemma log_mono: "mono log"
haftmann@51174
    46
proof
haftmann@51174
    47
  fix m n :: nat
haftmann@51174
    48
  assume "m \<le> n"
haftmann@51174
    49
  then show "log m \<le> log n"
haftmann@51174
    50
  proof (induct m arbitrary: n rule: log.induct)
haftmann@51174
    51
    case (1 m)
haftmann@51174
    52
    then have mn2: "m div 2 \<le> n div 2" by arith
haftmann@51174
    53
    show "log m \<le> log n"
haftmann@51174
    54
    proof (cases "m < 2")
haftmann@51174
    55
      case True
haftmann@51174
    56
      then have "m = 0 \<or> m = 1" by arith
haftmann@51174
    57
      then show ?thesis by (auto simp del: One_nat_def)
haftmann@51174
    58
    next
haftmann@51174
    59
      case False
haftmann@51174
    60
      with mn2 have "m \<ge> 2" and "n \<ge> 2" by auto arith
haftmann@51174
    61
      from False have m2_0: "m div 2 \<noteq> 0" by arith
haftmann@51174
    62
      with mn2 have n2_0: "n div 2 \<noteq> 0" by arith
haftmann@51174
    63
      from False "1.hyps" mn2 have "log (m div 2) \<le> log (n div 2)" by blast
haftmann@51174
    64
      with m2_0 n2_0 have "log (2 * (m div 2)) \<le> log (2 * (n div 2))" by simp
wenzelm@60500
    65
      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
    66
    qed
haftmann@51174
    67
  qed
haftmann@51174
    68
qed
haftmann@51174
    69
haftmann@51174
    70
wenzelm@60500
    71
subsection \<open>Discrete square root\<close>
haftmann@51174
    72
wenzelm@61115
    73
qualified definition sqrt :: "nat \<Rightarrow> nat"
wenzelm@59349
    74
  where "sqrt n = Max {m. m\<^sup>2 \<le> n}"
haftmann@51263
    75
haftmann@51263
    76
lemma sqrt_aux:
haftmann@51263
    77
  fixes n :: nat
wenzelm@53015
    78
  shows "finite {m. m\<^sup>2 \<le> n}" and "{m. m\<^sup>2 \<le> n} \<noteq> {}"
haftmann@51263
    79
proof -
haftmann@51263
    80
  { fix m
wenzelm@53015
    81
    assume "m\<^sup>2 \<le> n"
haftmann@51263
    82
    then have "m \<le> n"
haftmann@51263
    83
      by (cases m) (simp_all add: power2_eq_square)
haftmann@51263
    84
  } note ** = this
wenzelm@53015
    85
  then have "{m. m\<^sup>2 \<le> n} \<subseteq> {m. m \<le> n}" by auto
wenzelm@53015
    86
  then show "finite {m. m\<^sup>2 \<le> n}" by (rule finite_subset) rule
wenzelm@53015
    87
  have "0\<^sup>2 \<le> n" by simp
wenzelm@53015
    88
  then show *: "{m. m\<^sup>2 \<le> n} \<noteq> {}" by blast
haftmann@51263
    89
qed
haftmann@51263
    90
wenzelm@59349
    91
lemma [code]: "sqrt n = Max (Set.filter (\<lambda>m. m\<^sup>2 \<le> n) {0..n})"
haftmann@51263
    92
proof -
wenzelm@53015
    93
  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
    94
  then show ?thesis by (simp add: sqrt_def Set.filter_def)
haftmann@51263
    95
qed
haftmann@51174
    96
wenzelm@59349
    97
lemma sqrt_inverse_power2 [simp]: "sqrt (n\<^sup>2) = n"
haftmann@51174
    98
proof -
haftmann@51174
    99
  have "{m. m \<le> n} \<noteq> {}" by auto
haftmann@51174
   100
  then have "Max {m. m \<le> n} \<le> n" by auto
haftmann@51174
   101
  then show ?thesis
haftmann@51174
   102
    by (auto simp add: sqrt_def power2_nat_le_eq_le intro: antisym)
haftmann@51174
   103
qed
haftmann@51174
   104
wenzelm@59349
   105
lemma sqrt_zero [simp]: "sqrt 0 = 0"
haftmann@58787
   106
  using sqrt_inverse_power2 [of 0] by simp
haftmann@58787
   107
wenzelm@59349
   108
lemma sqrt_one [simp]: "sqrt 1 = 1"
haftmann@58787
   109
  using sqrt_inverse_power2 [of 1] by simp
haftmann@58787
   110
wenzelm@59349
   111
lemma mono_sqrt: "mono sqrt"
haftmann@51263
   112
proof
haftmann@51263
   113
  fix m n :: nat
haftmann@51263
   114
  have *: "0 * 0 \<le> m" by simp
haftmann@51263
   115
  assume "m \<le> n"
haftmann@51263
   116
  then show "sqrt m \<le> sqrt n"
wenzelm@60500
   117
    by (auto intro!: Max_mono \<open>0 * 0 \<le> m\<close> finite_less_ub simp add: power2_eq_square sqrt_def)
haftmann@51263
   118
qed
haftmann@51263
   119
wenzelm@59349
   120
lemma sqrt_greater_zero_iff [simp]: "sqrt n > 0 \<longleftrightarrow> n > 0"
haftmann@51174
   121
proof -
wenzelm@53015
   122
  have *: "0 < Max {m. m\<^sup>2 \<le> n} \<longleftrightarrow> (\<exists>a\<in>{m. m\<^sup>2 \<le> n}. 0 < a)"
haftmann@51263
   123
    by (rule Max_gr_iff) (fact sqrt_aux)+
haftmann@51263
   124
  show ?thesis
haftmann@51263
   125
  proof
haftmann@51263
   126
    assume "0 < sqrt n"
wenzelm@53015
   127
    then have "0 < Max {m. m\<^sup>2 \<le> n}" by (simp add: sqrt_def)
haftmann@51263
   128
    with * show "0 < n" by (auto dest: power2_nat_le_imp_le)
haftmann@51263
   129
  next
haftmann@51263
   130
    assume "0 < n"
wenzelm@53015
   131
    then have "1\<^sup>2 \<le> n \<and> 0 < (1::nat)" by simp
wenzelm@53015
   132
    then have "\<exists>q. q\<^sup>2 \<le> n \<and> 0 < q" ..
wenzelm@53015
   133
    with * have "0 < Max {m. m\<^sup>2 \<le> n}" by blast
haftmann@51263
   134
    then show "0 < sqrt n" by  (simp add: sqrt_def)
haftmann@51263
   135
  qed
haftmann@51263
   136
qed
haftmann@51263
   137
wenzelm@59349
   138
lemma sqrt_power2_le [simp]: "(sqrt n)\<^sup>2 \<le> n" (* FIXME tune proof *)
haftmann@51263
   139
proof (cases "n > 0")
haftmann@58787
   140
  case False then show ?thesis by simp
haftmann@51263
   141
next
haftmann@51263
   142
  case True then have "sqrt n > 0" by simp
wenzelm@53015
   143
  then have "mono (times (Max {m. m\<^sup>2 \<le> n}))" by (auto intro: mono_times_nat simp add: sqrt_def)
wenzelm@53015
   144
  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
   145
    using sqrt_aux [of n] by (rule mono_Max_commute)
haftmann@51263
   146
  have "Max (op * (Max {m. m * m \<le> n}) ` {m. m * m \<le> n}) \<le> n"
haftmann@51263
   147
    apply (subst Max_le_iff)
haftmann@51263
   148
    apply (metis (mono_tags) finite_imageI finite_less_ub le_square)
haftmann@51263
   149
    apply simp
haftmann@51263
   150
    apply (metis le0 mult_0_right)
haftmann@51263
   151
    apply auto
haftmann@51263
   152
    proof -
haftmann@51263
   153
      fix q
haftmann@51263
   154
      assume "q * q \<le> n"
haftmann@51263
   155
      show "Max {m. m * m \<le> n} * q \<le> n"
haftmann@51263
   156
      proof (cases "q > 0")
haftmann@51263
   157
        case False then show ?thesis by simp
haftmann@51263
   158
      next
haftmann@51263
   159
        case True then have "mono (times q)" by (rule mono_times_nat)
haftmann@51263
   160
        then have "q * Max {m. m * m \<le> n} = Max (times q ` {m. m * m \<le> n})"
haftmann@51263
   161
          using sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute)
haftmann@57514
   162
        then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: ac_simps)
wenzelm@59349
   163
        then show ?thesis
wenzelm@59349
   164
          apply simp
haftmann@51263
   165
          apply (subst Max_le_iff)
haftmann@51263
   166
          apply auto
haftmann@51263
   167
          apply (metis (mono_tags) finite_imageI finite_less_ub le_square)
wenzelm@60500
   168
          apply (metis \<open>q * q \<le> n\<close>)
wenzelm@60500
   169
          apply (metis \<open>q * q \<le> n\<close> le_cases mult_le_mono1 mult_le_mono2 order_trans)
wenzelm@59349
   170
          done
haftmann@51263
   171
      qed
haftmann@51263
   172
    qed
haftmann@51263
   173
  with * show ?thesis by (simp add: sqrt_def power2_eq_square)
haftmann@51174
   174
qed
haftmann@51174
   175
wenzelm@59349
   176
lemma sqrt_le: "sqrt n \<le> n"
haftmann@51263
   177
  using sqrt_aux [of n] by (auto simp add: sqrt_def intro: power2_nat_le_imp_le)
haftmann@51174
   178
haftmann@51174
   179
end
haftmann@51174
   180
wenzelm@61115
   181
end