Theory Interval_Division_Non_Zero

(***********************************************************************************
 * Copyright (c) University of Exeter, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *
 * SPDX-License-Identifier: BSD-3-Clause
 ***********************************************************************************)

chapter‹Basic Properties of Interval Division›

theory
  Interval_Division_Non_Zero
  imports
  Interval_Utilities
begin

text ‹
  The theory @{theory "HOL-Library.Interval"} does not define a division operation on intervals.
  In the following we define a locale capturing the core properties of division by an interval that
  does not contain zero. ›

section‹Preliminaries›

lemma division_leq_neg:
  fixes x :: "'a::{linordered_field}"
  assumes "0 < x" and "y < 0" and "z < 0" and "y ≤ z"
  shows "x / z ≤ x / y"
proof -
  have "x * y ≤ x * z" using assms by simp
  hence "(x * y) / (y * z) ≤ (x * z) / (y * z)" 
    using assms
    by (simp add: divide_right_mono zero_less_mult_iff neg_divide_le_eq)
  thus ?thesis using assms by auto[1]  
qed

lemma division_leq:
  fixes x :: "'a::{linordered_field}"
  assumes "0 < x" and "y ≤ z" and ‹y ≠ 0 ∧ z ≠ 0› and ‹(y < 0 ∧ z < 0) ∨ (0 < y ∧ 0 < z) ›
  shows "x / z ≤ x / y"
proof (cases ‹(y < 0 ∧ z < 0)›)
  case True
  then show ?thesis using assms division_leq_neg by blast
next
  case False
  have ‹(0 < y ∧ 0 < z)› using assms False by blast
  then show ?thesis 
    using assms
    by (simp add: frac_le)
qed

lemma upper_leq_lower_div:
  fixes Y :: "'a::{linordered_field} interval"
  assumes ‹lower Y ≤ upper Y› and ‹¬ 0 ∈⇩i Y›
  shows ‹1 / upper Y ≤ 1 / lower Y›
  using assms division_leq frac_le 
  by (metis atLeastAtMost_iff inverse_eq_divide le_imp_inverse_le 
            le_imp_inverse_le_neg linorder_not_less set_of_eq)

section‹A Locale for Interval Division Where the Quotient-Interval does not Contain Zero›

locale interval_division = inverse +
  constrains inverse :: ‹'a::{linordered_field, real_normed_algebra,linear_continuum_topology} interval ⇒ 'a interval›
         and divide  :: ‹'a::{linordered_field, real_normed_algebra,linear_continuum_topology} interval ⇒ 'a interval ⇒ 'a interval›
       assumes inverse_left: ‹¬ 0 ∈⇩i x ⟹ 1 ≤ (inverse x) * x›
           and divide:      ‹¬ 0 ∈⇩i y ⟹ x ≤ (divide x y) * y› 
begin 
end 

lemma interval_non_zero_eq:  
  ‹¬ 0 ∈⇩i (i::'a::{linorder, zero} interval) = (lower i < 0 ∧ upper i < 0) ∨ (lower i > 0 ∧ upper i > 0)›
  by (metis in_bounds in_intervalI linorder_not_less lower_le_upper order_le_less_trans) 

lemma inverse_includes_one:
  assumes ‹¬ 0 ∈⇩i (i::'a::{division_ring,linordered_ring} interval)›
  shows   ‹1 ∈⇩i (mk_interval (1 / upper i, 1 / lower i)) * i›
  using assms interval_non_zero_eq[of i] 
  apply(simp add: set_of_eq)
  apply(safe, simp_all)
  by (metis in_bounds lower_in_interval mk_interval_upper nonzero_eq_divide_eq times_in_intervalI 
            upper_in_interval)+ 
 
lemma inverse_includes_one': 
  assumes ‹¬ 0 ∈⇩i (i::'a::{division_ring,linordered_ring} interval)›
  shows   ‹1 ≤ (mk_interval (1 / upper i, 1 / lower i)) * i›
  by (simp add: assms in_bounds inverse_includes_one less_eq_interval_def) 


locale interval_division_inverse = inverse + 
  constrains inverse :: ‹'a::{linordered_field, real_normed_algebra,linear_continuum_topology} interval ⇒ 'a interval›
         and divide  :: ‹'a::{linordered_field, real_normed_algebra,linear_continuum_topology} interval ⇒ 'a interval ⇒ 'a interval›
       assumes inverse_non_zero_def: ‹¬ 0 ∈⇩i x ⟹ (inverse x) = mk_interval(1 / (upper x), 1 / (lower x))›
           and divide_non_zero_def:  ‹¬ 0 ∈⇩i y ⟹ (divide x y) = inverse y * x› 
begin 

sublocale interval_division divide inverse
  apply(standard)
  subgoal 
    by (simp add: inverse_includes_one' inverse_non_zero_def) 
  subgoal
    by (metis (no_types, opaque_lifting) divide_non_zero_def interval_mul_commute inverse_includes_one' inverse_non_zero_def mult.assoc one_times_ivl_right times_interval_right) 
  done 

lemma inverse_left_ge_one:
  assumes ‹¬ 0 ∈⇩i x› 
  shows ‹1 ≤ (inverse x) * x›
proof - 
  have lower_ne_zero: ‹lower x ≠ 0›
    using assms lower_in_interval by metis 
  have upper_ne_zero: ‹lower x ≠ 0›
    using assms lower_in_interval by metis 
  have ‹1 ≤ (mk_interval ( 1 / (upper x), 1 / (lower x))) * x› 
  proof(cases "1 / upper x ≤ 1 / lower x")
    case True note * = this
    then show ?thesis 
    proof(cases "upper x = lower x")
      case True
      then show ?thesis 
        using upper_times[of "mk_interval (1 / upper x, 1 / lower x)" x] 
              lower_times[of "mk_interval (1 / upper x, 1 / lower x)" x] 
              interval_eq_iff[of "mk_interval (1 / upper x, 1 / lower x) * x" 1]
              lower_ne_zero upper_ne_zero
        unfolding mk_interval'
        by simp
    next
      case False
      then show ?thesis 
        using interval_eq_iff[of "mk_interval (1 / upper x, 1 / lower x) * x" 1]
              upper_times[of "mk_interval (1 / upper x, 1 / lower x)" x] 
              lower_times[of "mk_interval (1 / upper x, 1 / lower x)" x]
      proof -
        have "1 / lower x = upper (mk_interval (1 / upper x, 1 / lower x))"
          by (simp add: "*")
        then show ?thesis
          by (metis (no_types) in_bounds less_eq_interval_def lower_in_interval lower_one 
              nonzero_divide_eq_eq times_in_intervalI upper_in_interval upper_ne_zero upper_one)
      qed
    qed
  next
    case False
    then show ?thesis 
        using interval_eq_iff[of "mk_interval (1 / upper x, 1 / lower x) * x" 1]
              upper_times[of "mk_interval (1 / upper x, 1 / lower x)" x] 
              lower_times[of "mk_interval (1 / upper x, 1 / lower x)" x]
        using assms lower_le_upper upper_leq_lower_div by blast 
    qed
    then show ?thesis 
  by (simp add: assms inverse_non_zero_def) 
  qed

lemma division_right_ge_refl: 
  assumes ‹¬ 0 ∈⇩i y›
  shows ‹x ≤ x * ((inverse y) * y)›
proof - 
  have a1: ‹set_of 1 ⊆ set_of ((inverse y) * y)›
    using inverse_left_ge_one[of y, simplified assms, simplified]
    by (simp add: interval_set_leq_eq) 
  show ?thesis
    using set_of_mul_inc_right[of 1 "mk_interval (1 / upper y, 1 / lower y) * y" x, 
              simplified one_times_ivl_right[of x] a1, simplified]
    by (metis a1 interval_set_leq_eq one_times_ivl_right times_interval_right)
qed

lemma division_right_ge_refl': 
  assumes ‹¬ 0 ∈⇩i y› 
  shows ‹x ≤ x * inverse y * y›
  by (simp add: assms division_right_ge_refl mult.assoc) 

lemma interval_div_constant:
  assumes  ‹0 ∉ set_of Y› and ‹0 ≤ x›
  shows ‹divide (interval_of x)  Y = Interval( x / upper Y, x / lower Y)›
proof -
  have l:  ‹lower Y ≤ upper Y› using lower_le_upper by simp
  have ‹1 / upper Y ≤ 1 / lower Y› using assms l
    by (metis divide_left_mono frac_le in_intervalI linorder_not_less mult_neg_neg order_less_le 
        zero_less_one_class.zero_le_one)
  then show ?thesis 
    using
    interval_of.abs_eq[of x]
    assms divide_non_zero_def[of Y "interval_of x", simplified assms, simplified] 
    inverse_non_zero_def[of Y, simplified assms, simplified]
    interval_times_scalar_pos_l interval_times_scalar_pos_r by fastforce
qed

lemma interval_of_width:  
  assumes ‹¬ 0 ∈⇩i Y› 
  shows ‹interval_of(width (divide (interval_of 1) Y)) = Interval( 1 / lower Y -  1 / upper Y,  1 / lower Y -  1 / upper Y) ›
proof(cases "Y" rule:interval_linorder_case_split[of _ 0 "λ Y. interval_of(width (divide (interval_of 1) Y)) 
                                                               = Interval( 1 / lower Y -  1 / upper Y,  1 / lower Y -  1 / upper Y)" ])
  case LeftOf
  have ‹1 / upper Y ≤ 1 / lower Y›
    using assms division_leq_neg LeftOf 
    by (simp add: le_divide_eq)  
  then show ?case 
    using interval_div_constant upper_bounds lower_bounds assms
    unfolding width_def interval_of_def by fastforce
next
  case Including
  then show ?case using assms by simp
next
  case RightOf
  have ‹1 / upper Y ≤ 1 / lower Y›
    by (simp add: assms upper_leq_lower_div) 
  then show ?case
    using interval_div_constant upper_bounds lower_bounds assms
    unfolding width_def interval_of_def by fastforce
qed

lemma abs_pos:
  assumes ‹0 < lower Y › and ‹¬ 0 ∈⇩i Y›
  shows ‹abs_interval(divide (interval_of 1) Y) = Interval( 1 / upper Y, 1 / lower Y)›
proof -
  have l:  ‹lower Y ≤ upper Y› using lower_le_upper by simp
  have ‹0 < 1 / upper Y › 
    by (metis assms(1) l dual_order.strict_trans1 zero_less_divide_1_iff)
  moreover have ‹ 0 < 1 / lower Y›
    by (metis assms(1) zero_less_divide_1_iff)
  moreover have ‹1 / upper Y ≤ 1 / lower Y›
    using assms by (simp add: frac_le)
  moreover have ‹divide (interval_of 1) Y = Interval( 1 / upper Y, 1 / lower Y)›
    using assms interval_div_constant[of Y 1] by simp
  ultimately show ?thesis 
    unfolding abs_interval_def by (simp add: bounds_of_interval_eq_lower_upper)
qed

lemma abs_neg:
  assumes ‹upper Y < 0 › and ‹¬ 0 ∈⇩i Y›
  shows ‹abs_interval(divide (interval_of 1) Y) = Interval(1 / ¦lower Y¦, 1 / ¦upper Y¦)›
proof -
  have l:  ‹lower Y ≤ upper Y› using lower_le_upper by simp
  have i0: ‹ 1 / upper Y < 0 › and i1: ‹ 1 / lower Y < 0›
    using assms by (simp, meson assms(1) divide_less_0_1_iff lower_le_upper order_le_less_trans)
  moreover have i2: ‹¦upper Y¦ ≤ ¦lower Y¦›
    using assms l by linarith
  then have i3: ‹¦1 / lower Y¦ ≤ ¦1 / upper Y¦›
    using assms division_leq_neg i1 
    by (simp add: division_leq)
  moreover have ‹divide (interval_of 1) Y = Interval( 1 / upper Y, 1 / lower Y)›
    using assms interval_div_constant[of Y 1] by simp
  moreover have ‹abs_interval(Interval( 1 / upper Y, 1 / lower Y)) = Interval(¦1 / lower Y¦, ¦1 / upper Y¦)›
    using assms i0 i1 i2 i3 unfolding abs_interval_def min_def max_def
    by (simp add: bounds_of_interval_eq_lower_upper)
  moreover have ‹... = Interval(1 / ¦lower Y¦, 1 / ¦upper Y¦)›
    by auto[1]
  ultimately show ?thesis 
    using assms interval_div_constant by force
qed


end 


end