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