src/HOL/Library/Discrete.thy
author wenzelm
Tue May 15 13:57:39 2018 +0200 (16 months ago)
changeset 68189 6163c90694ef
parent 67399 eab6ce8368fa
child 69064 5840724b1d71
permissions -rw-r--r--
tuned headers;
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
eberlm@64449
     6
imports Complex_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
eberlm@64449
   114
lemma log_exp2_gt: "2 * 2 ^ log n > n"
eberlm@64449
   115
proof (cases "n > 0")
eberlm@64449
   116
  case True
eberlm@64449
   117
  thus ?thesis
eberlm@64449
   118
  proof (induct n rule: log_induct)
eberlm@64449
   119
    case (double n)
eberlm@64449
   120
    thus ?case
eberlm@64449
   121
      by (cases "even n") (auto elim!: evenE oddE simp: field_simps log.simps)
eberlm@64449
   122
  qed simp_all
eberlm@64449
   123
qed simp_all
eberlm@64449
   124
eberlm@64449
   125
lemma log_exp2_ge: "2 * 2 ^ log n \<ge> n"
eberlm@64449
   126
  using log_exp2_gt[of n] by simp
eberlm@64449
   127
eberlm@64449
   128
lemma log_le_iff: "m \<le> n \<Longrightarrow> log m \<le> log n"
eberlm@64449
   129
  by (rule monoD [OF log_mono])
eberlm@64449
   130
eberlm@64449
   131
lemma log_eqI:
eberlm@64449
   132
  assumes "n > 0" "2^k \<le> n" "n < 2 * 2^k"
eberlm@64449
   133
  shows   "log n = k"
eberlm@64449
   134
proof (rule antisym)
eberlm@64449
   135
  from \<open>n > 0\<close> have "2 ^ log n \<le> n" by (rule log_exp2_le)
eberlm@64449
   136
  also have "\<dots> < 2 ^ Suc k" using assms by simp
eberlm@64449
   137
  finally have "log n < Suc k" by (subst (asm) power_strict_increasing_iff) simp_all
eberlm@64449
   138
  thus "log n \<le> k" by simp
eberlm@64449
   139
next
eberlm@64449
   140
  have "2^k \<le> n" by fact
eberlm@64449
   141
  also have "\<dots> < 2^(Suc (log n))" by (simp add: log_exp2_gt)
eberlm@64449
   142
  finally have "k < Suc (log n)" by (subst (asm) power_strict_increasing_iff) simp_all
eberlm@64449
   143
  thus "k \<le> log n" by simp
eberlm@64449
   144
qed
eberlm@64449
   145
eberlm@64449
   146
lemma log_altdef: "log n = (if n = 0 then 0 else nat \<lfloor>Transcendental.log 2 (real_of_nat n)\<rfloor>)"
eberlm@64449
   147
proof (cases "n = 0")
eberlm@64449
   148
  case False
eberlm@64449
   149
  have "\<lfloor>Transcendental.log 2 (real_of_nat n)\<rfloor> = int (log n)"
eberlm@64449
   150
  proof (rule floor_unique)
eberlm@64449
   151
    from False have "2 powr (real (log n)) \<le> real n"
eberlm@64449
   152
      by (simp add: powr_realpow log_exp2_le)
eberlm@64449
   153
    hence "Transcendental.log 2 (2 powr (real (log n))) \<le> Transcendental.log 2 (real n)"
eberlm@64449
   154
      using False by (subst Transcendental.log_le_cancel_iff) simp_all
eberlm@64449
   155
    also have "Transcendental.log 2 (2 powr (real (log n))) = real (log n)" by simp
eberlm@64449
   156
    finally show "real_of_int (int (log n)) \<le> Transcendental.log 2 (real n)" by simp
eberlm@64449
   157
  next
eberlm@64449
   158
    have "real n < real (2 * 2 ^ log n)"
eberlm@64449
   159
      by (subst of_nat_less_iff) (rule log_exp2_gt)
eberlm@64449
   160
    also have "\<dots> = 2 powr (real (log n) + 1)"
eberlm@64449
   161
      by (simp add: powr_add powr_realpow)
eberlm@64449
   162
    finally have "Transcendental.log 2 (real n) < Transcendental.log 2 \<dots>"
eberlm@64449
   163
      using False by (subst Transcendental.log_less_cancel_iff) simp_all
eberlm@64449
   164
    also have "\<dots> = real (log n) + 1" by simp
eberlm@64449
   165
    finally show "Transcendental.log 2 (real n) < real_of_int (int (log n)) + 1" by simp
eberlm@64449
   166
  qed
eberlm@64449
   167
  thus ?thesis by simp
eberlm@64449
   168
qed simp_all
eberlm@64449
   169
haftmann@51174
   170
wenzelm@60500
   171
subsection \<open>Discrete square root\<close>
haftmann@51174
   172
wenzelm@61115
   173
qualified definition sqrt :: "nat \<Rightarrow> nat"
wenzelm@59349
   174
  where "sqrt n = Max {m. m\<^sup>2 \<le> n}"
haftmann@51263
   175
haftmann@51263
   176
lemma sqrt_aux:
haftmann@51263
   177
  fixes n :: nat
wenzelm@53015
   178
  shows "finite {m. m\<^sup>2 \<le> n}" and "{m. m\<^sup>2 \<le> n} \<noteq> {}"
haftmann@51263
   179
proof -
haftmann@51263
   180
  { fix m
wenzelm@53015
   181
    assume "m\<^sup>2 \<le> n"
haftmann@51263
   182
    then have "m \<le> n"
haftmann@51263
   183
      by (cases m) (simp_all add: power2_eq_square)
haftmann@51263
   184
  } note ** = this
wenzelm@53015
   185
  then have "{m. m\<^sup>2 \<le> n} \<subseteq> {m. m \<le> n}" by auto
wenzelm@53015
   186
  then show "finite {m. m\<^sup>2 \<le> n}" by (rule finite_subset) rule
wenzelm@53015
   187
  have "0\<^sup>2 \<le> n" by simp
wenzelm@53015
   188
  then show *: "{m. m\<^sup>2 \<le> n} \<noteq> {}" by blast
haftmann@51263
   189
qed
haftmann@51263
   190
eberlm@63766
   191
lemma sqrt_unique:
eberlm@63766
   192
  assumes "m^2 \<le> n" "n < (Suc m)^2"
eberlm@63766
   193
  shows   "Discrete.sqrt n = m"
eberlm@63766
   194
proof -
eberlm@63766
   195
  have "m' \<le> m" if "m'^2 \<le> n" for m'
eberlm@63766
   196
  proof -
eberlm@63766
   197
    note that
eberlm@63766
   198
    also note assms(2)
eberlm@63766
   199
    finally have "m' < Suc m" by (rule power_less_imp_less_base) simp_all
eberlm@63766
   200
    thus "m' \<le> m" by simp
eberlm@63766
   201
  qed
eberlm@63766
   202
  with \<open>m^2 \<le> n\<close> sqrt_aux[of n] show ?thesis unfolding Discrete.sqrt_def
eberlm@63766
   203
    by (intro antisym Max.boundedI Max.coboundedI) simp_all
eberlm@63766
   204
qed
eberlm@63766
   205
eberlm@63766
   206
eberlm@63766
   207
lemma sqrt_code[code]: "sqrt n = Max (Set.filter (\<lambda>m. m\<^sup>2 \<le> n) {0..n})"
haftmann@51263
   208
proof -
wenzelm@53015
   209
  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
   210
  then show ?thesis by (simp add: sqrt_def Set.filter_def)
haftmann@51263
   211
qed
haftmann@51174
   212
wenzelm@59349
   213
lemma sqrt_inverse_power2 [simp]: "sqrt (n\<^sup>2) = n"
haftmann@51174
   214
proof -
haftmann@51174
   215
  have "{m. m \<le> n} \<noteq> {}" by auto
haftmann@51174
   216
  then have "Max {m. m \<le> n} \<le> n" by auto
haftmann@51174
   217
  then show ?thesis
haftmann@51174
   218
    by (auto simp add: sqrt_def power2_nat_le_eq_le intro: antisym)
haftmann@51174
   219
qed
haftmann@51174
   220
wenzelm@59349
   221
lemma sqrt_zero [simp]: "sqrt 0 = 0"
haftmann@58787
   222
  using sqrt_inverse_power2 [of 0] by simp
haftmann@58787
   223
wenzelm@59349
   224
lemma sqrt_one [simp]: "sqrt 1 = 1"
haftmann@58787
   225
  using sqrt_inverse_power2 [of 1] by simp
haftmann@58787
   226
wenzelm@59349
   227
lemma mono_sqrt: "mono sqrt"
haftmann@51263
   228
proof
haftmann@51263
   229
  fix m n :: nat
haftmann@51263
   230
  have *: "0 * 0 \<le> m" by simp
haftmann@51263
   231
  assume "m \<le> n"
haftmann@51263
   232
  then show "sqrt m \<le> sqrt n"
wenzelm@60500
   233
    by (auto intro!: Max_mono \<open>0 * 0 \<le> m\<close> finite_less_ub simp add: power2_eq_square sqrt_def)
haftmann@51263
   234
qed
haftmann@51263
   235
eberlm@63766
   236
lemma mono_sqrt': "m \<le> n \<Longrightarrow> Discrete.sqrt m \<le> Discrete.sqrt n"
eberlm@63766
   237
  using mono_sqrt unfolding mono_def by auto
eberlm@63766
   238
wenzelm@59349
   239
lemma sqrt_greater_zero_iff [simp]: "sqrt n > 0 \<longleftrightarrow> n > 0"
haftmann@51174
   240
proof -
wenzelm@53015
   241
  have *: "0 < Max {m. m\<^sup>2 \<le> n} \<longleftrightarrow> (\<exists>a\<in>{m. m\<^sup>2 \<le> n}. 0 < a)"
haftmann@51263
   242
    by (rule Max_gr_iff) (fact sqrt_aux)+
haftmann@51263
   243
  show ?thesis
haftmann@51263
   244
  proof
haftmann@51263
   245
    assume "0 < sqrt n"
wenzelm@53015
   246
    then have "0 < Max {m. m\<^sup>2 \<le> n}" by (simp add: sqrt_def)
haftmann@51263
   247
    with * show "0 < n" by (auto dest: power2_nat_le_imp_le)
haftmann@51263
   248
  next
haftmann@51263
   249
    assume "0 < n"
wenzelm@53015
   250
    then have "1\<^sup>2 \<le> n \<and> 0 < (1::nat)" by simp
wenzelm@53015
   251
    then have "\<exists>q. q\<^sup>2 \<le> n \<and> 0 < q" ..
wenzelm@53015
   252
    with * have "0 < Max {m. m\<^sup>2 \<le> n}" by blast
haftmann@51263
   253
    then show "0 < sqrt n" by  (simp add: sqrt_def)
haftmann@51263
   254
  qed
haftmann@51263
   255
qed
haftmann@51263
   256
wenzelm@59349
   257
lemma sqrt_power2_le [simp]: "(sqrt n)\<^sup>2 \<le> n" (* FIXME tune proof *)
haftmann@51263
   258
proof (cases "n > 0")
haftmann@58787
   259
  case False then show ?thesis by simp
haftmann@51263
   260
next
haftmann@51263
   261
  case True then have "sqrt n > 0" by simp
wenzelm@53015
   262
  then have "mono (times (Max {m. m\<^sup>2 \<le> n}))" by (auto intro: mono_times_nat simp add: sqrt_def)
wenzelm@53015
   263
  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
   264
    using sqrt_aux [of n] by (rule mono_Max_commute)
lp15@64919
   265
  have "\<And>a. a * a \<le> n \<Longrightarrow> Max {m. m * m \<le> n} * a \<le> n"
lp15@64919
   266
  proof -
lp15@64919
   267
    fix q
lp15@64919
   268
    assume "q * q \<le> n"
lp15@64919
   269
    show "Max {m. m * m \<le> n} * q \<le> n"
lp15@64919
   270
    proof (cases "q > 0")
lp15@64919
   271
      case False then show ?thesis by simp
lp15@64919
   272
    next
lp15@64919
   273
      case True then have "mono (times q)" by (rule mono_times_nat)
lp15@64919
   274
      then have "q * Max {m. m * m \<le> n} = Max (times q ` {m. m * m \<le> n})"
lp15@64919
   275
        using sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute)
lp15@64919
   276
      then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: ac_simps)
nipkow@67399
   277
      moreover have "finite (( * ) q ` {m. m * m \<le> n})"
lp15@64919
   278
        by (metis (mono_tags) finite_imageI finite_less_ub le_square)
lp15@64919
   279
      moreover have "\<exists>x. x * x \<le> n"
lp15@64919
   280
        by (metis \<open>q * q \<le> n\<close>)
lp15@64919
   281
      ultimately show ?thesis
lp15@64919
   282
        by simp (metis \<open>q * q \<le> n\<close> le_cases mult_le_mono1 mult_le_mono2 order_trans)
lp15@64919
   283
    qed
lp15@64919
   284
  qed
nipkow@67399
   285
  then have "Max (( * ) (Max {m. m * m \<le> n}) ` {m. m * m \<le> n}) \<le> n"
haftmann@51263
   286
    apply (subst Max_le_iff)
lp15@64919
   287
      apply (metis (mono_tags) finite_imageI finite_less_ub le_square)
lp15@64919
   288
     apply auto
haftmann@51263
   289
    apply (metis le0 mult_0_right)
lp15@64919
   290
    done
haftmann@51263
   291
  with * show ?thesis by (simp add: sqrt_def power2_eq_square)
haftmann@51174
   292
qed
haftmann@51174
   293
wenzelm@59349
   294
lemma sqrt_le: "sqrt n \<le> n"
haftmann@51263
   295
  using sqrt_aux [of n] by (auto simp add: sqrt_def intro: power2_nat_le_imp_le)
haftmann@51174
   296
lp15@64919
   297
text \<open>Additional facts about the discrete square root, thanks to Julian Biendarra, Manuel Eberl\<close>
lp15@64919
   298
  
lp15@64919
   299
lemma Suc_sqrt_power2_gt: "n < (Suc (Discrete.sqrt n))^2"
lp15@64919
   300
  using Max_ge[OF Discrete.sqrt_aux(1), of "Discrete.sqrt n + 1" n]
lp15@64919
   301
  by (cases "n < (Suc (Discrete.sqrt n))^2") (simp_all add: Discrete.sqrt_def)
lp15@64919
   302
lp15@64919
   303
lemma le_sqrt_iff: "x \<le> Discrete.sqrt y \<longleftrightarrow> x^2 \<le> y"
lp15@64919
   304
proof -
lp15@64919
   305
  have "x \<le> Discrete.sqrt y \<longleftrightarrow> (\<exists>z. z\<^sup>2 \<le> y \<and> x \<le> z)"    
lp15@64919
   306
    using Max_ge_iff[OF Discrete.sqrt_aux, of x y] by (simp add: Discrete.sqrt_def)
lp15@64919
   307
  also have "\<dots> \<longleftrightarrow> x^2 \<le> y"
lp15@64919
   308
  proof safe
lp15@64919
   309
    fix z assume "x \<le> z" "z ^ 2 \<le> y"
lp15@64919
   310
    thus "x^2 \<le> y" by (intro le_trans[of "x^2" "z^2" y]) (simp_all add: power2_nat_le_eq_le)
lp15@64919
   311
  qed auto
lp15@64919
   312
  finally show ?thesis .
lp15@64919
   313
qed
lp15@64919
   314
  
lp15@64919
   315
lemma le_sqrtI: "x^2 \<le> y \<Longrightarrow> x \<le> Discrete.sqrt y"
lp15@64919
   316
  by (simp add: le_sqrt_iff)
lp15@64919
   317
lp15@64919
   318
lemma sqrt_le_iff: "Discrete.sqrt y \<le> x \<longleftrightarrow> (\<forall>z. z^2 \<le> y \<longrightarrow> z \<le> x)"
lp15@64919
   319
  using Max.bounded_iff[OF Discrete.sqrt_aux] by (simp add: Discrete.sqrt_def)
lp15@64919
   320
lp15@64919
   321
lemma sqrt_leI:
lp15@64919
   322
  "(\<And>z. z^2 \<le> y \<Longrightarrow> z \<le> x) \<Longrightarrow> Discrete.sqrt y \<le> x"
lp15@64919
   323
  by (simp add: sqrt_le_iff)
lp15@64919
   324
    
lp15@64919
   325
lemma sqrt_Suc:
lp15@64919
   326
  "Discrete.sqrt (Suc n) = (if \<exists>m. Suc n = m^2 then Suc (Discrete.sqrt n) else Discrete.sqrt n)"
lp15@64919
   327
proof cases
lp15@64919
   328
  assume "\<exists> m. Suc n = m^2"
lp15@64919
   329
  then obtain m where m_def: "Suc n = m^2" by blast
lp15@64919
   330
  then have lhs: "Discrete.sqrt (Suc n) = m" by simp
lp15@64919
   331
  from m_def sqrt_power2_le[of n] 
lp15@64919
   332
    have "(Discrete.sqrt n)^2 < m^2" by linarith
lp15@64919
   333
  with power2_less_imp_less have lt_m: "Discrete.sqrt n < m" by blast
lp15@64919
   334
  from m_def Suc_sqrt_power2_gt[of "n"]
lp15@64919
   335
    have "m^2 \<le> (Suc(Discrete.sqrt n))^2" by simp
lp15@64919
   336
  with power2_nat_le_eq_le have "m \<le> Suc (Discrete.sqrt n)" by blast
lp15@64919
   337
  with lt_m have "m = Suc (Discrete.sqrt n)" by simp
lp15@64919
   338
  with lhs m_def show ?thesis by fastforce
lp15@64919
   339
next
lp15@64919
   340
  assume asm: "\<not> (\<exists> m. Suc n = m^2)"
lp15@64919
   341
  hence "Suc n \<noteq> (Discrete.sqrt (Suc n))^2" by simp
lp15@64919
   342
  with sqrt_power2_le[of "Suc n"] 
lp15@64919
   343
    have "Discrete.sqrt (Suc n) \<le> Discrete.sqrt n" by (intro le_sqrtI) linarith
lp15@64919
   344
  moreover have "Discrete.sqrt (Suc n) \<ge> Discrete.sqrt n"
lp15@64919
   345
    by (intro monoD[OF mono_sqrt]) simp_all
lp15@64919
   346
  ultimately show ?thesis using asm by simp
lp15@64919
   347
qed
lp15@64919
   348
haftmann@51174
   349
end
haftmann@51174
   350
nipkow@62390
   351
end