(* Title: Computing Square Roots using the Babylonian Method Author: René Thiemann <rene.thiemann@uibk.ac.at> Maintainer: René Thiemann License: LGPL *) (* Copyright 2009-2014 René Thiemann This file is part of IsaFoR/CeTA. IsaFoR/CeTA is free software: you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. IsaFoR/CeTA is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with IsaFoR/CeTA. If not, see <http://www.gnu.org/licenses/>. *) section ‹Auxiliary lemmas which might be moved into the Isabelle distribution.› theory Sqrt_Babylonian_Auxiliary imports Complex_Main begin lemma mod_div_equality_int: "(n :: int) div x * x = n - n mod x" using div_mult_mod_eq[of n x] by arith lemma div_is_floor_divide_rat: "n div y = ⌊rat_of_int n / rat_of_int y⌋" unfolding Fract_of_int_quotient[symmetric] floor_Fract by simp lemma div_is_floor_divide_real: "n div y = ⌊real_of_int n / of_int y⌋" unfolding div_is_floor_divide_rat[of n y] by (metis Ratreal_def of_rat_divide of_rat_of_int_eq real_floor_code) lemma floor_div_pos_int: fixes r :: "'a :: floor_ceiling" assumes n: "n > 0" shows "⌊r / of_int n⌋ = ⌊r⌋ div n" (is "?l = ?r") proof - let ?of_int = "of_int :: int ⇒ 'a" define rhs where "rhs = ⌊r⌋ div n" let ?n = "?of_int n" define m where "m = ⌊r⌋ mod n" let ?m = "?of_int m" from div_mult_mod_eq[of "floor r" n] have dm: "rhs * n + m = ⌊r⌋" unfolding rhs_def m_def by simp have mn: "m < n" and m0: "m ≥ 0" using n m_def by auto define e where "e = r - ?of_int ⌊r⌋" have e0: "e ≥ 0" unfolding e_def by (metis diff_self eq_iff floor_diff_of_int zero_le_floor) have e1: "e < 1" unfolding e_def by (metis diff_self dual_order.refl floor_diff_of_int floor_le_zero) have "r = ?of_int ⌊r⌋ + e" unfolding e_def by simp also have "⌊r⌋ = rhs * n + m" using dm by simp finally have "r = ?of_int (rhs * n + m) + e" . hence "r / ?n = ?of_int (rhs * n) / ?n + (e + ?m) / ?n" using n by (simp add: field_simps) also have "?of_int (rhs * n) / ?n = ?of_int rhs" using n by auto finally have *: "r / ?of_int n = (e + ?of_int m) / ?of_int n + ?of_int rhs" by simp have "?l = rhs + floor ((e + ?m) / ?n)" unfolding * by simp also have "floor ((e + ?m) / ?n) = 0" proof (rule floor_unique) show "?of_int 0 ≤ (e + ?m) / ?n" using e0 m0 n by (metis add_increasing2 divide_nonneg_pos of_int_0 of_int_0_le_iff of_int_0_less_iff) show "(e + ?m) / ?n < ?of_int 0 + 1" proof (rule ccontr) from n have n': "?n > 0" "?n ≥ 0" by simp_all assume "¬ ?thesis" hence "(e + ?m) / ?n ≥ 1" by auto from mult_right_mono[OF this n'(2)] have "?n ≤ e + ?m" using n'(1) by simp also have "?m ≤ ?n - 1" using mn by (metis of_int_1 of_int_diff of_int_le_iff zle_diff1_eq) finally have "?n ≤ e + ?n - 1" by auto with e1 show False by arith qed qed finally show ?thesis unfolding rhs_def by simp qed lemma floor_div_neg_int: fixes r :: "'a :: floor_ceiling" assumes n: "n < 0" shows "⌊r / of_int n⌋ = ⌈r⌉ div n" proof - from n have n': "- n > 0" by auto have "⌊r / of_int n⌋ = ⌊ - r / of_int (- n)⌋" using n by (metis floor_of_int floor_zero less_int_code(1) minus_divide_left minus_minus nonzero_minus_divide_right of_int_minus) also have "… = ⌊ - r ⌋ div (- n)" by (rule floor_div_pos_int[OF n']) also have "… = ⌈ r ⌉ div n" using n by (metis ceiling_def div_minus_right) finally show ?thesis . qed lemma divide_less_floor1: "n / y < of_int (floor (n / y)) + 1" by (metis floor_less_iff less_add_one of_int_1 of_int_add) context linordered_idom begin lemma sgn_int_pow_if [simp]: "sgn x ^ p = (if even p then 1 else sgn x)" if "x ≠ 0" using that by (induct p) simp_all lemma compare_pow_le_iff: "p > 0 ⟹ (x :: 'a) ≥ 0 ⟹ y ≥ 0 ⟹ (x ^ p ≤ y ^ p) = (x ≤ y)" by (rule power_mono_iff) lemma compare_pow_less_iff: "p > 0 ⟹ (x :: 'a) ≥ 0 ⟹ y ≥ 0 ⟹ (x ^ p < y ^ p) = (x < y)" using compare_pow_le_iff [of p x y] using local.dual_order.order_iff_strict local.power_strict_mono by blast end lemma quotient_of_int[simp]: "quotient_of (of_int i) = (i,1)" by (metis Rat.of_int_def quotient_of_int) lemma quotient_of_nat[simp]: "quotient_of (of_nat i) = (int i,1)" by (metis Rat.of_int_def Rat.quotient_of_int of_int_of_nat_eq) lemma square_lesseq_square: "⋀ x y. 0 ≤ (x :: 'a :: linordered_field) ⟹ 0 ≤ y ⟹ (x * x ≤ y * y) = (x ≤ y)" by (metis mult_mono mult_strict_mono' not_less) lemma square_less_square: "⋀ x y. 0 ≤ (x :: 'a :: linordered_field) ⟹ 0 ≤ y ⟹ (x * x < y * y) = (x < y)" by (metis mult_mono mult_strict_mono' not_less) lemma sqrt_sqrt[simp]: "x ≥ 0 ⟹ sqrt x * sqrt x = x" by (metis real_sqrt_pow2 power2_eq_square) lemma abs_lesseq_square: "abs (x :: real) ≤ abs y ⟷ x * x ≤ y * y" using square_lesseq_square[of "abs x" "abs y"] by auto end