260 next |
260 next |
261 case True then have "sqrt n > 0" by simp |
261 case True then have "sqrt n > 0" by simp |
262 then have "mono (times (Max {m. m\<^sup>2 \<le> n}))" by (auto intro: mono_times_nat simp add: sqrt_def) |
262 then have "mono (times (Max {m. m\<^sup>2 \<le> n}))" by (auto intro: mono_times_nat simp add: sqrt_def) |
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})" |
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})" |
264 using sqrt_aux [of n] by (rule mono_Max_commute) |
264 using sqrt_aux [of n] by (rule mono_Max_commute) |
265 have "Max (op * (Max {m. m * m \<le> n}) ` {m. m * m \<le> n}) \<le> n" |
265 have "\<And>a. a * a \<le> n \<Longrightarrow> Max {m. m * m \<le> n} * a \<le> n" |
|
266 proof - |
|
267 fix q |
|
268 assume "q * q \<le> n" |
|
269 show "Max {m. m * m \<le> n} * q \<le> n" |
|
270 proof (cases "q > 0") |
|
271 case False then show ?thesis by simp |
|
272 next |
|
273 case True then have "mono (times q)" by (rule mono_times_nat) |
|
274 then have "q * Max {m. m * m \<le> n} = Max (times q ` {m. m * m \<le> n})" |
|
275 using sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute) |
|
276 then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: ac_simps) |
|
277 moreover have "finite (op * q ` {m. m * m \<le> n})" |
|
278 by (metis (mono_tags) finite_imageI finite_less_ub le_square) |
|
279 moreover have "\<exists>x. x * x \<le> n" |
|
280 by (metis \<open>q * q \<le> n\<close>) |
|
281 ultimately show ?thesis |
|
282 by simp (metis \<open>q * q \<le> n\<close> le_cases mult_le_mono1 mult_le_mono2 order_trans) |
|
283 qed |
|
284 qed |
|
285 then have "Max (op * (Max {m. m * m \<le> n}) ` {m. m * m \<le> n}) \<le> n" |
266 apply (subst Max_le_iff) |
286 apply (subst Max_le_iff) |
267 apply (metis (mono_tags) finite_imageI finite_less_ub le_square) |
287 apply (metis (mono_tags) finite_imageI finite_less_ub le_square) |
268 apply simp |
288 apply auto |
269 apply (metis le0 mult_0_right) |
289 apply (metis le0 mult_0_right) |
270 apply auto |
290 done |
271 proof - |
|
272 fix q |
|
273 assume "q * q \<le> n" |
|
274 show "Max {m. m * m \<le> n} * q \<le> n" |
|
275 proof (cases "q > 0") |
|
276 case False then show ?thesis by simp |
|
277 next |
|
278 case True then have "mono (times q)" by (rule mono_times_nat) |
|
279 then have "q * Max {m. m * m \<le> n} = Max (times q ` {m. m * m \<le> n})" |
|
280 using sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute) |
|
281 then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: ac_simps) |
|
282 then show ?thesis |
|
283 apply simp |
|
284 apply (subst Max_le_iff) |
|
285 apply auto |
|
286 apply (metis (mono_tags) finite_imageI finite_less_ub le_square) |
|
287 apply (metis \<open>q * q \<le> n\<close>) |
|
288 apply (metis \<open>q * q \<le> n\<close> le_cases mult_le_mono1 mult_le_mono2 order_trans) |
|
289 done |
|
290 qed |
|
291 qed |
|
292 with * show ?thesis by (simp add: sqrt_def power2_eq_square) |
291 with * show ?thesis by (simp add: sqrt_def power2_eq_square) |
293 qed |
292 qed |
294 |
293 |
295 lemma sqrt_le: "sqrt n \<le> n" |
294 lemma sqrt_le: "sqrt n \<le> n" |
296 using sqrt_aux [of n] by (auto simp add: sqrt_def intro: power2_nat_le_imp_le) |
295 using sqrt_aux [of n] by (auto simp add: sqrt_def intro: power2_nat_le_imp_le) |
297 |
296 |
|
297 text \<open>Additional facts about the discrete square root, thanks to Julian Biendarra, Manuel Eberl\<close> |
|
298 |
|
299 lemma Suc_sqrt_power2_gt: "n < (Suc (Discrete.sqrt n))^2" |
|
300 using Max_ge[OF Discrete.sqrt_aux(1), of "Discrete.sqrt n + 1" n] |
|
301 by (cases "n < (Suc (Discrete.sqrt n))^2") (simp_all add: Discrete.sqrt_def) |
|
302 |
|
303 lemma le_sqrt_iff: "x \<le> Discrete.sqrt y \<longleftrightarrow> x^2 \<le> y" |
|
304 proof - |
|
305 have "x \<le> Discrete.sqrt y \<longleftrightarrow> (\<exists>z. z\<^sup>2 \<le> y \<and> x \<le> z)" |
|
306 using Max_ge_iff[OF Discrete.sqrt_aux, of x y] by (simp add: Discrete.sqrt_def) |
|
307 also have "\<dots> \<longleftrightarrow> x^2 \<le> y" |
|
308 proof safe |
|
309 fix z assume "x \<le> z" "z ^ 2 \<le> y" |
|
310 thus "x^2 \<le> y" by (intro le_trans[of "x^2" "z^2" y]) (simp_all add: power2_nat_le_eq_le) |
|
311 qed auto |
|
312 finally show ?thesis . |
|
313 qed |
|
314 |
|
315 lemma le_sqrtI: "x^2 \<le> y \<Longrightarrow> x \<le> Discrete.sqrt y" |
|
316 by (simp add: le_sqrt_iff) |
|
317 |
|
318 lemma sqrt_le_iff: "Discrete.sqrt y \<le> x \<longleftrightarrow> (\<forall>z. z^2 \<le> y \<longrightarrow> z \<le> x)" |
|
319 using Max.bounded_iff[OF Discrete.sqrt_aux] by (simp add: Discrete.sqrt_def) |
|
320 |
|
321 lemma sqrt_leI: |
|
322 "(\<And>z. z^2 \<le> y \<Longrightarrow> z \<le> x) \<Longrightarrow> Discrete.sqrt y \<le> x" |
|
323 by (simp add: sqrt_le_iff) |
|
324 |
|
325 lemma sqrt_Suc: |
|
326 "Discrete.sqrt (Suc n) = (if \<exists>m. Suc n = m^2 then Suc (Discrete.sqrt n) else Discrete.sqrt n)" |
|
327 proof cases |
|
328 assume "\<exists> m. Suc n = m^2" |
|
329 then obtain m where m_def: "Suc n = m^2" by blast |
|
330 then have lhs: "Discrete.sqrt (Suc n) = m" by simp |
|
331 from m_def sqrt_power2_le[of n] |
|
332 have "(Discrete.sqrt n)^2 < m^2" by linarith |
|
333 with power2_less_imp_less have lt_m: "Discrete.sqrt n < m" by blast |
|
334 from m_def Suc_sqrt_power2_gt[of "n"] |
|
335 have "m^2 \<le> (Suc(Discrete.sqrt n))^2" by simp |
|
336 with power2_nat_le_eq_le have "m \<le> Suc (Discrete.sqrt n)" by blast |
|
337 with lt_m have "m = Suc (Discrete.sqrt n)" by simp |
|
338 with lhs m_def show ?thesis by fastforce |
|
339 next |
|
340 assume asm: "\<not> (\<exists> m. Suc n = m^2)" |
|
341 hence "Suc n \<noteq> (Discrete.sqrt (Suc n))^2" by simp |
|
342 with sqrt_power2_le[of "Suc n"] |
|
343 have "Discrete.sqrt (Suc n) \<le> Discrete.sqrt n" by (intro le_sqrtI) linarith |
|
344 moreover have "Discrete.sqrt (Suc n) \<ge> Discrete.sqrt n" |
|
345 by (intro monoD[OF mono_sqrt]) simp_all |
|
346 ultimately show ?thesis using asm by simp |
|
347 qed |
|
348 |
298 end |
349 end |
299 |
350 |
300 end |
351 end |