Theory Inclusion_Isotonicity

(***********************************************************************************
 * 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‹Interval Inclusion Isotonicity›
theory
  Inclusion_Isotonicity
imports
  "Interval_Utilities"
  "Affine_Functions"
  Interval_Division_Non_Zero
begin

section‹Interval Extension›

subsection ‹Textbook Definition of Interval Extension›
definition✐‹tag important›
  is_interval_extension_of :: ‹('a::preorder interval ⇒ 'b::preorder interval) ⇒ ('a ⇒ 'b) ⇒ bool›  
                               (infix "(is'_interval'_extension'_of)" 50)
where 
  ‹((F is_interval_extension_of f)) = (∀ x. (F (interval_of x)) = interval_of (f x))›

definition‹extend_natural f = (λ X. mk_interval (f (lower X), f(upper X)))›

lemma interval_extension_comp: 
  assumes interval_ext_F:  ‹F is_interval_extension_of f›
   and    interval_ext_G:  ‹G is_interval_extension_of g›
  shows ‹(F o G) is_interval_extension_of (f o g)›
  using assms unfolding is_interval_extension_of_def
  by simp 

lemma interval_extension_const: ‹(λ x. interval_of c) is_interval_extension_of (λ x. c)›
  unfolding is_interval_extension_of_def  
  by (simp add: interval_eq_iff) 

lemma interval_extension_id: ‹(λ x. x) is_interval_extension_of (λ x. x)›
  unfolding is_interval_extension_of_def  
  by (simp add: interval_eq_iff) 

subsection ‹A Stronger Definition of Interval Extension›
definition 
  is_natural_interval_extension_of :: ‹('a::linorder interval ⇒ 'b::linorder interval) ⇒ ('a ⇒ 'b) ⇒ bool›  
                               (infix ‹(is'_natural'_interval'_extension'_of)› 50)
where 
  ‹((F is_natural_interval_extension_of f)) = (∀ l u. (F (mk_interval (l,u))) = mk_interval (f l, f u))›

lemma ‹(extend_natural f) is_interval_extension_of f›  
  unfolding is_interval_extension_of_def extend_natural_def
  by(auto simp add: mk_interval' interval_of_def)

lemma ‹(extend_natural f) is_natural_interval_extension_of f›
  unfolding is_natural_interval_extension_of_def extend_natural_def
  by(auto simp add: mk_interval' interval_of_def)

lemma natural_interval_extension_implies_interval_extension:
  assumes ‹F is_natural_interval_extension_of f› shows ‹F is_interval_extension_of f›
  using assms unfolding is_natural_interval_extension_of_def is_interval_extension_of_def
  mk_interval_def interval_of_def
  by(auto split:if_splits)

lemma const_add_is_natural_interval_extensions: 
  ‹(λ x. (interval_of c) + x) is_natural_interval_extension_of (λ x. c + x)›
  unfolding is_natural_interval_extension_of_def mk_interval_def 
  by (simp add: add_mono_thms_linordered_semiring(1) antisym interval_eq_iff add_mono
           split:if_splits) 

lemma const_times_is_natural_interval_extensions:
  ‹(λ x. (interval_of c) * x) is_natural_interval_extension_of (λ x. c * x)›
  unfolding is_natural_interval_extension_of_def mk_interval_def 
  unfolding times_interval_def Let_def 
  by(simp add: interval_eq_iff Interval_inverse interval_of.rep_eq add_mono 
          split:if_splits)
 
lemma const_is_interval_extension: ‹F is_natural_interval_extension_of (λ x. b) ⟹ F = (λ x.(interval_of b))›
  unfolding is_natural_interval_extension_of_def
  apply(auto simp add:mk_interval' interval_of_def split:if_splits)[1]
  by (metis bounds_of_interval_eq_lower_upper bounds_of_interval_inverse lower_le_upper) 

lemma id_is_interval_extension: ‹F is_natural_interval_extension_of (λ x. x) ⟹ F = (λ x. x)›
  unfolding is_natural_interval_extension_of_def
  apply(auto simp add:mk_interval' interval_of_def split:if_splits)[1]
  by (metis bounds_of_interval_eq_lower_upper bounds_of_interval_inverse lower_le_upper) 

lemma extend_natural_is_interval_extension: 
  ‹(extend_natural f) is_natural_interval_extension_of f›
  unfolding extend_natural_def is_natural_interval_extension_of_def mk_interval'_def
  by (smt (z3) case_prod_conv mk_interval_def lower_bounds nle_le upper_bounds) 

lemma is_natural_interval_extension_implies_bounds: 
  fixes F :: ‹real interval ⇒ real interval›
   assumes ‹F is_natural_interval_extension_of f› and ‹F x ≤ F x'›
  shows
 ‹((f (lower x')) ≤   (f (lower x)) ) ∨  ((f (upper x')) ≤   (f (upper x)) )›
  by (smt (verit) assms interval_eqI is_natural_interval_extension_of_def less_eq_interval_def 
          lower_le_upper mk_interval_lower mk_interval_upper)

lemma interval_extension_lower:
   ‹((F is_interval_extension_of f)) ⟹ lower (F (interval_of x)) = (f x)›
  unfolding is_interval_extension_of_def by simp

lemma interval_extension_upper:
   ‹((F is_interval_extension_of f)) ⟹ upper (F (interval_of x)) = (f x)›
  unfolding is_interval_extension_of_def by simp

lemma is_interval_extension_eq_upper_and_lower:
   ‹((F is_interval_extension_of f)) 
        = (∀ x. lower (F (interval_of x)) = (f x) ∧ upper (F (interval_of x)) = (f x))›
  unfolding is_interval_extension_of_def
  by (simp add: interval_eq_iff) 

lemma interval_extension_lower_simp[simp]: 
  assumes ‹F is_interval_extension_of f› and ‹X = Interval(x,x)› 
  shows ‹lower (F X) = f x ›
  by (metis assms interval_extension_lower interval_of.abs_eq) 

lemma interval_extension_upper_simp[simp]: 
  assumes ‹F is_interval_extension_of f› and ‹X = Interval(x,x)› 
  shows ‹upper (F X) = f x ›
  by (metis assms interval_extension_upper interval_of.abs_eq) 

section‹Interval Inclusion Isotonicity›

text‹
  In this section, we introduce the concept of inclusion isotonicity. The formalization 
  in this theory generalises the definitions from~\<^cite>‹"ratz:inclusion:1997"›:
›
definition
  inclusion_isotonic :: ‹('a::preorder interval ⇒ 'b::preorder interval) ⇒ bool›
  where
 ‹inclusion_isotonic f = (∀ x x'. x ≤ x' ⟶ (f x) ≤ (f x'))›

text‹We can immediately show that any natural extension of an affine function of from 
type @{type ‹real›} to @{type ‹real›} is interval inclusion isotonic:
›
lemma real_affine_fun_is_inclusion_isotonicM: 
      assumes ‹affine_fun (f::real => real)› 
      shows ‹inclusion_isotonic (extend_natural f)›
  using assms  
  unfolding inclusion_isotonic_def extend_natural_def Interval.less_eq_interval_def affine_fun_real_linfun
  by(auto, (metis lower_le_upper mult_le_cancel_left nle_le)+)

definition
  inclusion_isotonic_on :: ‹('a interval ⇒ bool ) ⇒ ('a::preorder interval ⇒ 'b::preorder interval) ⇒ bool›
  where
 ‹inclusion_isotonic_on P f = (∀ x x'. P x ∧ P x' ∧ x ≤ x' ⟶ (f x) ≤ (f x'))›

lemma inclusion_isotonic_eq: ‹inclusion_isotonic_on (λ x . True) = inclusion_isotonic›
  unfolding inclusion_isotonic_on_def inclusion_isotonic_def
  by simp

definition inclusion_isotonic_binary :: ‹('a::preorder interval ⇒ 'a interval ⇒ 'b::preorder interval) ⇒ bool›
  where
‹inclusion_isotonic_binary f = (∀ x x' y y'. x ≤ x' ∧ y ≤ y' ⟶ (f x y) ≤ (f x' y'))›

definition inclusion_isotonic_binary_on :: ‹('a interval ⇒ bool ) ⇒ ('a::preorder interval ⇒ 'a interval ⇒ 'b::preorder interval) ⇒ bool›
  where
‹inclusion_isotonic_binary_on P f = (∀ x x' y y'. P x ∧ P x' ∧ P y ∧ P y' ∧ x ≤ x' ∧ y ≤ y' ⟶ (f x y) ≤ (f x' y'))›

lemma inclusion_isotonic_binary_eq: ‹inclusion_isotonic_binary_on (λ x . True) = inclusion_isotonic_binary›
  unfolding inclusion_isotonic_binary_on_def inclusion_isotonic_binary_def
  by simp

definition inclusion_isotonicM_n :: ‹nat ⇒ ('a::linorder interval list ⇒ 'a::linorder interval) ⇒ bool› where
  ‹inclusion_isotonicM_n n f = (∀ is js. (length is =  n ∧ length js = n  ∧ (is ≤⇩I js)) ⟶ f is ≤ f js)›

definition inclusion_isotonicM_n_on :: ‹('a interval ⇒ bool) ⇒  nat ⇒ ('a::linorder interval list ⇒ 'a::linorder interval) ⇒ bool› where
  ‹inclusion_isotonicM_n_on P n f = (∀ is js. (∀ i ∈ set is. P i) ∧ (∀ j ∈ set js. P j) ∧ (length is =  n ∧ length js = n  ∧ (is ≤⇩I js)) ⟶ f is ≤ f js)›


lemma inclusion_isotonicM_n_eq: ‹inclusion_isotonicM_n_on (λ x . True) = inclusion_isotonicM_n›
  unfolding inclusion_isotonicM_n_on_def inclusion_isotonicM_n_def
  by simp

text‹Finally, we extend the definition to functions over lists and show that the three definitions of 
interval inclusion isotonicity are, for their corresponding types, equivalent:›

locale inclusion_isotonicM =
  fixes  n :: nat 
     and f :: ‹('a::linorder) interval list ⇒ 'a interval list›
  assumes inclusion_isotonicM :
  ‹(∀ is js. (length is = n) ∧(length js = n) ∧ (is ≤⇩I js) ⟶ f is ≤⇩I f js)›
begin 
end

locale inclusion_isotonicM_on =
  fixes  P :: ‹'a::linorder interval ⇒ bool›
     and n :: nat 
     and f :: ‹('a::linorder) interval list ⇒ 'a interval list›
  assumes inclusion_isotonicM :
  ‹(∀ is js. (∀ i ∈ set is. P i) ∧ (∀ j ∈ set js. P j) ∧ (length is = n) ∧(length js = n) ∧ (is ≤⇩I js) ⟶ f is ≤⇩I f js)›
begin 
end

lemma inclusion_isotonicM_on_eq: ‹inclusion_isotonicM_on (λ x. True) = inclusion_isotonicM›
  unfolding inclusion_isotonicM_on_def inclusion_isotonicM_def
  by simp  

lemma inclusion_isotonic_conv:
  ‹inclusion_isotonic g = inclusion_isotonicM 1 (λ xs . case xs  of [x] ⇒  [g x])›
  unfolding inclusion_isotonic_def inclusion_isotonicM_def
  by(auto simp add: le_interval_single split:list.split)

lemma inclusion_isotonicM_n_conv1:
  ‹inclusion_isotonicM_n n f = inclusion_isotonicM n (λ xs. [f xs])›
  unfolding  inclusion_isotonicM_n_def inclusion_isotonicM_def le_interval_list_def 
  by(auto)

lemma inclusion_isotonicM_conv2:
  assumes ‹inclusion_isotonicM n f›
  and ‹∀ xs. (length xs = n) ⟶ N = (length (f xs))›  
shows ‹inclusion_isotonicM n (λ xs. if n' < N then [(f xs)!n'] else [])›
  using assms unfolding inclusion_isotonicM_def 
  apply(simp split:if_splits, safe)
  apply(subst le_interval_single[symmetric])
  apply(subst le_interval_list_all)
  subgoal by blast 
  subgoal by blast 
  subgoal by(rule TrueI)
done 

lemma inclusion_isotonicM_n_on_conv1:
  ‹inclusion_isotonicM_n_on P n f = inclusion_isotonicM_on P n (λ xs. [f xs])›
  unfolding  inclusion_isotonicM_n_on_def inclusion_isotonicM_on_def le_interval_list_def 
  by(auto)

lemma inclusion_isotonicM_on_conv2:
  assumes ‹inclusion_isotonicM_on P n f›
  and ‹∀ xs. (length xs = n) ⟶ N = (length (f xs))›  
shows ‹inclusion_isotonicM_on P n (λ xs. if n' < N then [(f xs)!n'] else [])›
  using assms unfolding inclusion_isotonicM_on_def 
  apply(simp split:if_splits, safe)
  apply(subst le_interval_single[symmetric])
  apply(subst le_interval_list_all)
  subgoal by blast 
  subgoal by blast 
  subgoal by(rule TrueI)
done 

lemma inclusion_isotonic_binary_conv1: 
  ‹inclusion_isotonic_binary f = inclusion_isotonicM_n 2 (λ xs . case xs  of [x,y] ⇒  f x y)›
  unfolding inclusion_isotonic_binary_def inclusion_isotonicM_n_def le_interval_list_def
  by(auto simp add: le_interval_list_def split:list.split)

lemma inclusion_isotonic_binary_conv2: 
  ‹inclusion_isotonic_binary f = inclusion_isotonicM 2 (λ xs . case xs  of [x,y] ⇒  [f x y])›
  apply(simp add: inclusion_isotonic_binary_conv1)
  apply(simp add: inclusion_isotonicM_n_conv1)
  unfolding inclusion_isotonicM_def 
  by(auto split:list.split)

lemma inclusion_isotonic_binary_on_conv1: 
  ‹inclusion_isotonic_binary_on P f = inclusion_isotonicM_n_on P 2 (λ xs . case xs  of [x,y] ⇒  f x y)›
  unfolding inclusion_isotonic_binary_on_def inclusion_isotonicM_n_on_def le_interval_list_def
  by(auto simp add: le_interval_list_def split:list.split)

lemma inclusion_isotonic_binary_on_conv2: 
  ‹inclusion_isotonic_binary_on P f = inclusion_isotonicM_on P 2 (λ xs . case xs  of [x,y] ⇒  [f x y])›
  apply(simp add: inclusion_isotonic_binary_on_conv1)
  apply(simp add: inclusion_isotonicM_n_on_conv1)
  unfolding inclusion_isotonicM_on_def 
  by(auto split:list.split)


subsection‹Compositionality of Interval Inclusion Isotonicy›

lemma inclusion_isotonicM_comp: 
  assumes ‹inclusion_isotonicM n f› 
      and ‹inclusion_isotonicM m g›
      and ‹∀ xs. length xs = n ⟶ length (f xs) = m›
  shows ‹inclusion_isotonicM n (g o f)›
  using assms unfolding inclusion_isotonicM_def 
  by(simp)

lemma inclusion_isotonicM_on_comp: 
  assumes ‹inclusion_isotonicM_on P n f› 
      and ‹inclusion_isotonicM_on Q m g›
      and ‹∀ xs. length xs = n ⟶ length (f xs) = m›
      and ‹∀ is. (∀ i ∈ set is. P i) ⟶ (∀x∈set (f is). Q x)›
shows ‹inclusion_isotonicM_on P n (g o f)›
  using assms  unfolding inclusion_isotonicM_on_def  o_def
  by(auto)

lemma inclusion_isotonic_comp: 
  assumes ‹inclusion_isotonic f› 
      and ‹inclusion_isotonic g›
  shows ‹inclusion_isotonic (g o f)›
  using assms unfolding inclusion_isotonic_def 
  by(simp)

lemma inclusion_isotonic_on_comp: 
  assumes ‹inclusion_isotonic_on P f› 
      and ‹inclusion_isotonic_on Q g›
      and ‹∀ x. P x ⟶ Q (f x)›
shows ‹inclusion_isotonic_on P (g o f)›
  using assms unfolding inclusion_isotonic_on_def 
  by(simp)

subsection‹Interval Inclusion Isontonicity of the Core Operator›

subsubsection‹Unary Minus (Negation)›

lemma inclusion_isotonicM_uminus[simp]: ‹inclusion_isotonic uminus›
  by (simp add: inclusion_isotonic_def less_eq_interval_def)

subsubsection‹Addition›

lemma inclusion_isotonicM_plus[simp]: ‹inclusion_isotonic_binary (+)› 
  by (simp add: inclusion_isotonic_binary_def less_eq_interval_def add_mono) 

subsubsection‹Substraction›

lemma inclusion_isotonicM_minus[simp]: ‹inclusion_isotonic_binary (-)› 
  by (simp add: inclusion_isotonic_binary_def less_eq_interval_def diff_mono) 

subsubsection‹Multiplication›

lemma inclusion_isotonicM_times[simp]: 
  ‹inclusion_isotonic_binary  (λ x y. (x::'a::{linordered_ring, real_normed_algebra, linear_continuum_topology} interval) * y)›
  unfolding inclusion_isotonic_binary_def using set_of_mul_inc interval_set_leq_eq 
  by metis 


subsection‹Interval Inclusion Isotonicity of Various Functions›

lemma inclusion_isotonicM_n_empty[simp]: ‹inclusion_isotonicM n (λ xs. [])›
unfolding inclusion_isotonicM_def by(simp)

lemma inclusion_isotonic_id[simp]: ‹inclusion_isotonic id›
  unfolding inclusion_isotonic_def le_interval_list_def 
  by(simp)

lemma inclusion_isotonicM_id[simp]: ‹inclusion_isotonicM n id›
  unfolding inclusion_isotonicM_def le_interval_list_def 
  by(simp)

lemma inclusion_isotonicM_hd[simp]: 
  assumes ‹0 < n› 
  shows ‹inclusion_isotonicM_n n hd›
unfolding inclusion_isotonicM_n_def le_interval_list_def 
proof(insert assms, induction n rule:nat_induct_non_zero)
  case 1
  then show ?case 
    by (auto, metis (no_types, lifting) Nil_eq_zip_iff case_prodD foldl_conj_set_True hd_zip insert_iff 
       length_0_conv list.map_disc_iff list.map_sel(1) list.set(2) list.set_sel(1) nat.distinct(1))
next
  case (Suc n)
  then show ?case
    by (auto, metis (no_types, lifting) Nil_eq_zip_iff Zero_not_Suc case_prodD foldl_conj_set_True hd_zip 
              insert_iff length_0_conv list.map_disc_iff list.map_sel(1) list.set(2) list.set_sel(1))
qed

lemma inclusion_isotonic_add_const1[simp]:
  ‹inclusion_isotonic  (λ x. x + c)›
  unfolding inclusion_isotonic_def
  by (simp add: add_mono_thms_linordered_semiring(3) less_eq_interval_def) 
  
lemma inclusion_isotonicM_1_add_const2[simp]: 
  ‹inclusion_isotonic  (λ x. c + x)›
  unfolding inclusion_isotonic_def
  by (simp add: add_mono_thms_linordered_semiring(2) less_eq_interval_def) 
 
lemma inclusion_isotonic_times_right[simp]: 
  ‹inclusion_isotonic  (λ x. C* (x::'a::linordered_ring interval))›
  unfolding inclusion_isotonic_def
  using times_interval_right by auto 

lemma inclusion_isotonic_times_left[simp]:
  ‹inclusion_isotonic  (λ x. (x::'a::{real_normed_algebra,linordered_ring,linear_continuum_topology} interval) * C)›
  unfolding inclusion_isotonic_def
  using times_interval_left by auto 

lemma map_inclusion_isotonicM:
  assumes ‹inclusion_isotonic  f›
  shows  ‹inclusion_isotonicM n (map f)›
  using assms map_set map_pair_set_left map_pair_set_right map_pair_set
  unfolding inclusion_isotonicM_def le_interval_list_def inclusion_isotonic_def 
  by(simp add: foldl_conj_set_True map_pair_f_all, blast)

lemma inclusion_isotonicM_fun_plus:
  assumes ‹inclusion_isotonic f› and ‹inclusion_isotonic g›
  shows ‹inclusion_isotonic (λ x. f x + g x)›
  using assms unfolding inclusion_isotonic_def
  by (simp add: add_mono_thms_linordered_semiring(1) less_eq_interval_def) 

lemma inclusion_isotonic_plus_const:
  assumes ‹inclusion_isotonic f› and ‹inclusion_isotonic g›
  shows ‹inclusion_isotonic (λ x. g x + c)›
  using assms unfolding inclusion_isotonic_def
  by (simp add: add_mono_thms_linordered_semiring(1) less_eq_interval_def) 

lemma inclusion_isotonic_times_const_real:
  assumes ‹inclusion_isotonic f›
  shows ‹inclusion_isotonic (λ x. (c::real interval) * (f x))›
  using inclusion_isotonic_comp  assms 
  unfolding inclusion_isotonic_def
  by (simp add: times_interval_right)  

lemma intervall_le_foldr: 
  assumes ‹inclusion_isotonic_binary f›
  shows ‹length js = length is ⟹ is ≤⇩I js ⟹ (foldr f is e) ≤ (foldr f js e)›
proof (induction rule:list_induct2)
  case Nil
  then show ?case 
    by (simp add: less_eq_interval_def)     
next
  case (Cons x xs y ys)
  then show ?case 
    unfolding le_interval_list_def
    by (simp, metis (no_types, lifting) assms foldl_conj_True inclusion_isotonic_binary_def 
        list_all_simps(1))
qed

lemma intervall_le_foldr_map: 
  assumes ‹inclusion_isotonic_binary f›
  and ‹inclusion_isotonic g›
  shows ‹length js = length is ⟹ is ≤⇩I js ⟹ (foldr f (map g is) e) ≤ (foldr f (map g js) e)›
proof (induction rule:list_induct2)
  case Nil
  then show ?case 
    by (simp add: less_eq_interval_def)
next
  case (Cons x xs y ys)
  then show ?case 
    using assms unfolding inclusion_isotonicM_n_def le_interval_list_def
    by(simp add: foldl_conj_True inclusion_isotonic_def inclusion_isotonic_binary_def) 
qed

lemma intervall_le_foldr_e: 
  assumes ‹inclusion_isotonic_binary f›
  and ‹is ≤ js›
  shows ‹(foldr f xs is) ≤ (foldr f xs js)›
proof (induction xs)
  case Nil
  then show ?case using assms by(simp)     
next
  case (Cons x)
  then show ?case
    using assms unfolding le_interval_list_def inclusion_isotonic_binary_def
    by (simp add: less_eq_interval_def) 
 qed

lemma foldr_inclusion_isotonicM_e:
  assumes ‹inclusion_isotonic_binary f›
  shows ‹∀ x. inclusion_isotonic  (foldr f x)›
  using assms 
  unfolding inclusion_isotonic_def
  by(simp add: intervall_le_foldr_e)

lemma foldr_inclusion_isotonicM:
  assumes ‹inclusion_isotonic_binary f›
  shows ‹inclusion_isotonicM_n n (λ x. foldr f x e)›
  using assms 
  unfolding inclusion_isotonicM_n_def using  intervall_le_foldr
  by auto 

lemma foldr_inclusion_isotonicM_g:
  assumes ‹inclusion_isotonic_binary f›
  and     ‹inclusion_isotonicM n g›
  shows ‹inclusion_isotonicM_n n (λ x. foldr f ((g x)) e)›
  using assms(2)
  unfolding inclusion_isotonicM_n_def inclusion_isotonicM_def  
  by (metis assms(1) intervall_le_foldr le_interval_list_imp_length)

lemma foldr_map_inclusion_isotonicM_g:
  assumes ‹inclusion_isotonic_binary f›
  and     ‹inclusion_isotonic g ›  
  and     ‹inclusion_isotonicM n P›
  shows ‹inclusion_isotonicM_n n (λ x. foldr f (map g (P x)) e)›
  using intervall_le_foldr_map assms(3)
  unfolding inclusion_isotonicM_n_def  inclusion_isotonicM_def
  by (metis (no_types, lifting) assms(1) assms(2) intervall_le_foldr_map le_interval_list_imp_length) 

lemma foldl_inclusion_isotonicM:
  assumes ‹inclusion_isotonic_binary f›
  shows ‹inclusion_isotonicM_n n (foldl f e)›
  unfolding inclusion_isotonicM_n_def
  apply(subst foldl_conv_foldr)
  apply(subst foldl_conv_foldr)
  using assms foldr_inclusion_isotonicM[simplified inclusion_isotonicM_def]
        le_interval_list_rev length_rev
  unfolding inclusion_isotonicM_n_def inclusion_isotonic_binary_def
  by (metis)

lemma fold_inclusion_isotonicM:
  assumes ‹inclusion_isotonic_binary f›
  shows ‹inclusion_isotonicM_n n (λ x. fold f x e)›
  unfolding inclusion_isotonicM_n_def
  apply(subst foldl_conv_fold[symmetric])
  apply(subst foldl_conv_fold[symmetric])
  using assms foldl_inclusion_isotonicM[simplified inclusion_isotonicM_def]
  unfolding inclusion_isotonic_binary_def inclusion_isotonicM_n_def
  by (metis) 


lemma map2_inclusion_isotonicM_left: assumes  ‹inclusion_isotonic_binary f›
         shows ‹inclusion_isotonicM n (map2 f xs)›
  unfolding inclusion_isotonicM_def inclusion_isotonic_binary_def
  apply(safe,subst le_interval_list_all2, simp_all)
  using le_interval_list_imp le_interval_list_all 
  by (metis assms dual_order.refl inclusion_isotonic_binary_def less_eq_interval_def)

lemma map2_inclusion_isotonicM_right: assumes  ‹inclusion_isotonic_binary f›
         shows ‹inclusion_isotonicM n (λ ys. map2 f ys xs)›
  unfolding inclusion_isotonicM_def inclusion_isotonic_binary_def
  apply(safe,subst le_interval_list_all2, simp_all)
  using le_interval_list_imp le_interval_list_all 
  by (metis assms dual_order.refl inclusion_isotonic_binary_def less_eq_interval_def)
                           

lemma map2_inclusion_isotonicM_right_g: 
  assumes  ‹inclusion_isotonic_binary f›
   and ‹∀ xs. length (g xs) = length xs›
   and ‹inclusion_isotonicM n  g›
   and ‹length xs = n›
   and ‹length is = n› 
   and ‹length js = n› 
   and ‹is ≤⇩I js› 
  shows‹map2 f (g is) (h xs) ≤⇩I map2 f (g js) (h xs)›
  using assms unfolding inclusion_isotonic_binary_def
  apply(subst le_interval_list_all2, simp_all)
  using assms unfolding inclusion_isotonic_binary_def  
  by (metis dual_order.refl inclusion_isotonicM_def
            le_interval_list_imp less_eq_interval_def) 

lemma inclusion_isotonicM_map: 
  assumes ‹∀ x ∈ set xs . g x ≤ h x›
  shows ‹(map g xs) ≤⇩I (map h xs)›
  using assms by(subst le_interval_list_all2, simp_all)

section ‹Interval Extension and Inclusion Properties›

lemma interval_extension_inclusion:
  assumes ‹F is_interval_extension_of f›
  shows ‹∀ X . interval_of (f X) ≤ F (interval_of X)›
  using assms
  unfolding is_interval_extension_of_def 
  by (simp add: in_interval_to_interval interval_of_in_eq)

lemma interval_extension_subset_const:
  assumes interval_ext_F: ‹F is_interval_extension_of f›
  shows ‹∀ X . set_of (interval_of (f X)) ⊆ set_of (F (interval_of X))›
  using assms
  unfolding is_interval_extension_of_def set_of_def by auto

lemma fundamental_theorem_of_interval_analysis:
  fixes F :: ‹real interval ⇒ real interval›
  assumes interval_ext_F: ‹F is_interval_extension_of f› 
   and   inc_isontonic_F: ‹inclusion_isotonic F› 
shows ‹∀ X . f ` (set_of X) ⊆ set_of (F X)›
proof
  fix X
  show ‹ f ` (set_of X) ⊆ set_of (F X)›
  proof
    fix y
    assume ‹y ∈ f ` (set_of X)›
    then obtain x where i: ‹x ∈ set_of X› and ‹y = f x› by auto
    then have ‹interval_of (f x) = F (interval_of x)› using assms unfolding is_interval_extension_of_def by simp
    then have ‹y ∈ set_of (F (interval_of x))› using ‹y = f x› by (metis in_interval_to_interval)
    then have ‹interval_of x ≤ X› using ‹x ∈ set_of X› using interval_of_in_eq by blast
    then have ‹F (interval_of x) ≤ F X› using inc_isontonic_F unfolding inclusion_isotonic_def by simp 
    then show ‹y ∈ set_of (F X)› using ‹y ∈ set_of(F (interval_of x))› using set_of_subset_iff' by auto 
  qed
qed 

lemma interval_extension_bounds:
  assumes "inclusion_isotonic F"
  and "F is_interval_extension_of f"
  shows "(∀ x ∈ set_of X. lower (F X) ≤  f x) ∨ (∀x ∈ set_of X. f x ≤ lower (F X))"
  using assms 
  by (metis (no_types, lifting) in_bounds inclusion_isotonic_def interval_of_in_eq 
                                is_interval_extension_of_def) 

lemma inclusion_isotonic_extension_subset:
  assumes  "inclusion_isotonic F"  
  and "F is_interval_extension_of f"
  shows ‹(f ` set_of X) ⊆ set_of (F X)›
  using assms interval_of_in_eq   
  unfolding inclusion_isotonic_def set_of_eq is_interval_extension_of_def 
  by (metis (mono_tags, lifting) image_subsetI) 

lemma inclusion_isotonic_extension_includes:
  assumes  "inclusion_isotonic F"  
  and "F is_interval_extension_of f"
  shows ‹∀ x ∈ set_of X. f x ∈ set_of (F X)›
  using assms inclusion_isotonic_extension_subset
  by blast  

lemma inclusion_isotonic_extension_lower_bound:
  assumes  "inclusion_isotonic F"  
  and "F is_interval_extension_of f"
  shows ‹∀ x ∈ set_of X. lower (F X) ≤ f x›
  using assms inclusion_isotonic_extension_includes
  using in_bounds by blast 

lemma inclusion_isotonic_extension_upper_bound:
  assumes  "inclusion_isotonic F"  
  and "F is_interval_extension_of f"
  shows ‹∀ x ∈ set_of X. f x ≤ upper (F X)›
  using assms inclusion_isotonic_extension_includes
  using in_bounds by blast 


lemma inclusion_isotonic_inf:
  fixes F::‹real interval ⇒ real interval›
  assumes  "inclusion_isotonic F"  
  and "F is_interval_extension_of f"
  shows ‹lower (F (X::real interval)) ≤ Inf (f ` set_of X)›
  using inclusion_isotonic_extension_subset[of F f X, simplified assms]
  cInf_superset_mono[of "f ` set_of X"  "set_of (F X)"]
  by (simp add: bdd_below_set_of  inf_set_of)

lemma inclusion_isotonic_sup:
  fixes F::‹real interval ⇒ real interval›
  assumes  "inclusion_isotonic F"  
  and "F is_interval_extension_of f"
  shows ‹Sup (f ` set_of X) ≤ upper (F X)›
  using inclusion_isotonic_extension_subset[of F f X, simplified assms]  
        cSup_subset_mono[of "f ` set_of X" "set_of (F X)"]
  by (simp add: bdd_above_set_of sup_set_of)

lemma lower_inf:
  fixes F::‹real interval ⇒ real interval›
  assumes  "inclusion_isotonic F"  
  and "F is_interval_extension_of f"
  shows "Inf (f ` set_of X) ≤ f (lower X)"
  using cInf_superset_mono[of "{f (lower X)}" "f ` set_of X"]
  by (metis assms(1) assms(2) bdd_below_mono bdd_below_set_of bot.extremum 
                     cInf_singleton imageI insert_not_empty insert_subsetI 
                     fundamental_theorem_of_interval_analysis lower_in_interval) 
lemma upper_sup:
  fixes F::‹real interval ⇒ real interval›
  assumes  "inclusion_isotonic F"  
  and "F is_interval_extension_of f"
  shows "f (upper X) ≤ Sup (f ` set_of X)"
  using cSup_subset_mono[of "{f (upper X)}" "f ` set_of X"]
  by (meson assms(1) assms(2) bdd_above_mono bdd_above_set_of cSup_upper 
            imageI fundamental_theorem_of_interval_analysis upper_in_interval) 
  
lemma lower_F_f:
  fixes F::‹real interval ⇒ real interval›
  assumes  "inclusion_isotonic F"  
  and "F is_interval_extension_of f"
  shows "lower (F X) ≤ f (lower X)"
  by (simp add: assms(1) assms(2) inclusion_isotonic_extension_lower_bound) 
  
lemma upper_F_f:
  fixes F::‹real interval ⇒ real interval›
  assumes  "inclusion_isotonic F"  
  and "F is_interval_extension_of f"
  shows "f (upper X) ≤ upper (F X)"
  by (simp add: assms(1) assms(2) inclusion_isotonic_extension_upper_bound)

lemma inclusion_isotonic_interval_extension_le:
    assumes inclusion_isotonic: ‹inclusion_isotonic F›
  and       interval_extension: ‹F is_interval_extension_of f›
  and       adjacent: ‹upper a = lower b›
shows ‹lower (F b) ≤ upper (F a)›
  using inclusion_isotonic_extension_lower_bound[of F f, simplified assms, simplified]  
        inclusion_isotonic_extension_upper_bound[of F f, simplified assms, simplified]
        le_left_mono lower_in_interval upper_in_interval
  by(metis adjacent)


section‹Division›

context interval_division_inverse
begin 
lemma inclusion_isotonic_on_inverse[simp]:
  ‹inclusion_isotonic_on (λ x . ¬ 0 ∈⇩i x) ((inverse::('a interval ⇒ 'a interval)))›
  using inverse_non_zero_def
  unfolding inclusion_isotonic_on_def less_eq_interval_def
  by (smt (z3) dual_order.trans in_bounds in_intervalI lower_le_upper mk_interval_lower 
      mk_interval_upper upper_leq_lower_div)

lemma inclusion_isotonic_on_division[simp]:
  ‹inclusion_isotonic_binary_on (λ x . ¬ 0 ∈⇩i x)  (λ x y. divide x y)›
  using inclusion_isotonicM_times  divide_non_zero_def inclusion_isotonic_on_inverse
  unfolding  o_def inclusion_isotonic_binary_on_def
            inclusion_isotonic_on_def inclusion_isotonic_binary_def
  by metis 

end 

end