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