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 log_pow_cancel[simp]: "a > 0 ⟹ a ≠ 1 ⟹ log a (a ^ b) = b"
by (metis monoid_mult_class.mult.right_neutral log_eq_one log_nat_power)
lemma real_of_rat_floor[simp]: "floor (real_of_rat x) = floor x"
by (metis Ratreal_def real_floor_code)
lemma abs_of_rat[simp]: "¦real_of_rat x¦ = real_of_rat ¦x¦"
proof (cases "x ≥ 0")
case False
define y where "y = - x"
from False have y: "y ≥ 0" "x = - y" by (auto simp: y_def)
thus ?thesis by (auto simp: of_rat_minus)
qed auto
lemma real_of_rat_ceiling[simp]: "ceiling (real_of_rat x) = ceiling x"
unfolding ceiling_def by (metis of_rat_minus real_of_rat_floor)
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 (metis eq_iff linear power_eq_imp_eq_base power_mono)
lemma compare_pow_less_iff: "p > 0 ⟹ (x :: 'a) ≥ 0 ⟹ y ≥ 0 ⟹ (x ^ p < y ^ p) = (x < y)"
by (metis power_less_imp_less_base power_strict_mono)
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