# Theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary

```(*  Title:       Computing Square Roots using the Babylonian Method
Author:      René Thiemann       <rene.thiemann@uibk.ac.at>
Maintainer:  René Thiemann
*)

(*

This file is part of IsaFoR/CeTA.

IsaFoR/CeTA is free software: you can redistribute it and/or modify it under the
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"

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
```