Theory Prediction_Utils

(***********************************************************************************
 * 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-2-Clause
 ***********************************************************************************)

section‹Useful Definitions for Analyzing Predictions›

theory
  Prediction_Utils 
imports 
  Complex_Main
begin 


paragraph‹Utilities›

definition max⇩l⇩i⇩s⇩t :: ‹'a::linorder list ⇒ 'a› where 
          ‹max⇩l⇩i⇩s⇩t = Max o set›

definition min⇩l⇩i⇩s⇩t :: ‹'a::linorder list ⇒ 'a› where 
          ‹min⇩l⇩i⇩s⇩t = Min o set›

lemma max⇩l⇩i⇩s⇩t_is_element: ‹l ≠ [] ⟹  max⇩l⇩i⇩s⇩t l ∈ set l › 
  by (metis List.finite_set comp_eq_dest_lhs eq_Max_iff max⇩l⇩i⇩s⇩t_def set_empty) 
lemma min⇩l⇩i⇩s⇩t_is_element: ‹l ≠ [] ⟹  min⇩l⇩i⇩s⇩t l ∈ set l › 
  by (metis List.finite_set comp_eq_dest_lhs eq_Min_iff min⇩l⇩i⇩s⇩t_def set_empty) 

lemma max⇩l⇩i⇩s⇩t_append_eq: ‹max⇩l⇩i⇩s⇩t (xs @ [x]) = max⇩l⇩i⇩s⇩t xs ∨ max⇩l⇩i⇩s⇩t (xs @ [x]) = x›
proof(cases "max⇩l⇩i⇩s⇩t (xs @ [x]) = x")
  case True
  then show ?thesis by blast
next
  case False
  then show ?thesis
    by (metis (no_types, lifting) List.finite_set Max.subset_imp Max_eq_iff comp_def insertE 
               list.discI list.set(1) list.simps(15) max⇩l⇩i⇩s⇩t_def max⇩l⇩i⇩s⇩t_is_element order_antisym 
               rotate1.simps(2) set_rotate1 set_subset_Cons singletonD)
qed
lemma min⇩l⇩i⇩s⇩t_append_eq: ‹min⇩l⇩i⇩s⇩t (xs @ [x]) = min⇩l⇩i⇩s⇩t xs ∨ min⇩l⇩i⇩s⇩t (xs @ [x]) = x›
proof(cases "min⇩l⇩i⇩s⇩t (xs @ [x]) = x")
  case True
  then show ?thesis by blast
next
  case False
  then show ?thesis
    by (metis (no_types, lifting) List.finite_set Min.subset_imp Min_eq_iff comp_def insertE 
               list.discI list.set(1) list.simps(15) min⇩l⇩i⇩s⇩t_def min⇩l⇩i⇩s⇩t_is_element order_antisym 
               rotate1.simps(2) set_rotate1 set_subset_Cons singletonD)
qed

lemma max⇩l⇩i⇩s⇩t_cons_eq: ‹max⇩l⇩i⇩s⇩t (x#xs) = max⇩l⇩i⇩s⇩t xs ∨ max⇩l⇩i⇩s⇩t (x#xs) = x›
proof(cases "max⇩l⇩i⇩s⇩t (x#xs) = x")
  case True
  then show ?thesis by blast
next
  case False
  then show ?thesis
    by (metis (no_types, lifting) List.finite_set Max.subset_imp Max_eq_iff comp_def insertE 
               list.discI list.set(1) list.simps(15) max⇩l⇩i⇩s⇩t_def max⇩l⇩i⇩s⇩t_is_element order_antisym 
               set_subset_Cons singletonD)
qed
lemma min⇩l⇩i⇩s⇩t_cons_eq: ‹min⇩l⇩i⇩s⇩t (x#xs) = min⇩l⇩i⇩s⇩t xs ∨ min⇩l⇩i⇩s⇩t (x#xs) = x›
proof(cases "min⇩l⇩i⇩s⇩t (x#xs) = x")
  case True
  then show ?thesis by blast
next
  case False
  then show ?thesis
    by (metis (no_types, lifting) List.finite_set Min.subset_imp Min_eq_iff comp_def insertE 
               list.discI list.set(1) list.simps(15) min⇩l⇩i⇩s⇩t_def min⇩l⇩i⇩s⇩t_is_element order_antisym 
               set_subset_Cons singletonD)
qed

lemma max⇩l⇩i⇩s⇩t_append_limit: assumes ‹xs ≠ []› shows ‹max⇩l⇩i⇩s⇩t xs ≤ max⇩l⇩i⇩s⇩t (xs @ [x])›
proof(cases "max⇩l⇩i⇩s⇩t (xs @ [x]) = x")
  case True 
  then show ?thesis using assms
    by (metis List.finite_set Max_ge comp_eq_dest_lhs list.set_intros(2) max⇩l⇩i⇩s⇩t_def 
              max⇩l⇩i⇩s⇩t_is_element rotate1.simps(2) set_rotate1)
next
  case False
  then show ?thesis 
    by (metis dual_order.refl max⇩l⇩i⇩s⇩t_append_eq)
qed 
lemma min⇩l⇩i⇩s⇩t_append_limit: assumes ‹xs ≠ []› shows ‹min⇩l⇩i⇩s⇩t (xs @ [x]) ≤ min⇩l⇩i⇩s⇩t xs›
proof(cases "min⇩l⇩i⇩s⇩t (xs @ [x]) = x")
  case True 
  then show ?thesis using assms
    by (metis List.finite_set Min_antimono comp_eq_dest_lhs min⇩l⇩i⇩s⇩t_def rotate1.simps(2) set_empty 
             set_rotate1 set_subset_Cons)
next
  case False
  then show ?thesis 
    by (metis dual_order.refl min⇩l⇩i⇩s⇩t_append_eq)
qed 

lemma max⇩l⇩i⇩s⇩t_cons_limit: assumes ‹xs ≠ []› shows ‹max⇩l⇩i⇩s⇩t xs ≤ max⇩l⇩i⇩s⇩t (x#xs)›
proof(cases "max⇩l⇩i⇩s⇩t (x#xs) = x")
  case True 
  then show ?thesis using assms
    by (metis List.finite_set Max_ge comp_eq_dest_lhs list.set_intros(2) max⇩l⇩i⇩s⇩t_def 
              max⇩l⇩i⇩s⇩t_is_element)
next
  case False
  then show ?thesis
    by (metis dual_order.refl max⇩l⇩i⇩s⇩t_cons_eq) 
qed 
lemma min⇩l⇩i⇩s⇩t_cons_limit: assumes ‹xs ≠ []› shows ‹min⇩l⇩i⇩s⇩t (x#xs) ≤ min⇩l⇩i⇩s⇩t xs›
proof(cases "min⇩l⇩i⇩s⇩t (x#xs) = x")
  case True 
  then show ?thesis using assms
    by (metis comp_eq_dest_lhs min⇩l⇩i⇩s⇩t_append_limit min⇩l⇩i⇩s⇩t_def rotate1.simps(2) set_rotate1)
next
  case False
  then show ?thesis
    by (metis dual_order.refl min⇩l⇩i⇩s⇩t_cons_eq) 
qed 


paragraph‹Converting Predictions to Percentages›

definition prediction2percentage :: ‹real list ⇒ real list› where
          ‹prediction2percentage l = (let m = max⇩l⇩i⇩s⇩t l in map (λ e. e / m *  100.0) l)›

lemma prediction2percentage_is_percentage:
  assumes ‹0 < max⇩l⇩i⇩s⇩t l› 
  shows ‹∀ x ∈ set (prediction2percentage l). x ≤ 100.0›
proof(insert assms, induction "l" rule: rev_induct)
  case Nil
  then show ?case 
    unfolding prediction2percentage_def Let_def max⇩l⇩i⇩s⇩t_def o_def 
    by(simp)
next
  case (snoc x xs)
  then show ?case 
    unfolding prediction2percentage_def Let_def max⇩l⇩i⇩s⇩t_def o_def 
    by(simp add: divide_le_eq) 
qed
  
lemma prediction2percentage_id: assumes ‹max⇩l⇩i⇩s⇩t p = 100› shows ‹prediction2percentage p = p›
  unfolding prediction2percentage_def 
  using assms by(simp)

lemma prediction2percentage_min_id: 
  assumes ‹0 < max⇩l⇩i⇩s⇩t p› 
  shows ‹(0 ≤ min⇩l⇩i⇩s⇩t (prediction2percentage p))= (0 ≤ min⇩l⇩i⇩s⇩t p)›
proof(insert assms, induction "p" rule: rev_induct)
  case Nil
  then show ?case
  using assms unfolding prediction2percentage_def Let_def min⇩l⇩i⇩s⇩t_def max⇩l⇩i⇩s⇩t_def o_def 
  by(simp)
next
  case (snoc x xs)
  then show ?case 
  using assms unfolding prediction2percentage_def Let_def min⇩l⇩i⇩s⇩t_def max⇩l⇩i⇩s⇩t_def o_def 
    apply(simp,safe) 
    subgoal 
      by (metis linorder_not_le not_numeral_le_zero zero_le_divide_iff zero_le_mult_iff)
    subgoal
      by (metis linorder_not_le not_numeral_le_zero zero_le_divide_iff zero_le_mult_iff)
    subgoal by simp
    subgoal by simp 
    done
qed

paragraph‹Maximum Prediction›

definition posmax_of :: ‹'a::linorder list ⇒ (nat × 'a) option› where
          ‹posmax_of l = (let m = max⇩l⇩i⇩s⇩t l in find (λ e. snd e = m) (enumerate 0 l))›
definition pos_of_max :: ‹'a::linorder list ⇒ nat option› where
          ‹pos_of_max l = map_option fst (posmax_of l)›

definition posmax_of' :: ‹'a::linorder list ⇒ (nat × 'a) option› where
          ‹posmax_of' l = (if l = [] then None else Some ((hd o rev o (sort_key snd) o (enumerate 0)) l))›
definition pos_of_max' :: ‹'a::linorder list ⇒ nat option› where
          ‹pos_of_max' l = map_option fst (posmax_of' l)›

paragraph‹Minimum Prediction›

definition posmin_of :: ‹'a::linorder list ⇒ (nat × 'a) option› where
          ‹posmin_of l = (let m = min⇩l⇩i⇩s⇩t l in find (λ e. snd e = m) (enumerate 0 l))›
definition pos_of_min :: ‹'a::linorder list ⇒ nat option› where
          ‹pos_of_min l = map_option fst (posmin_of l)›

definition posmin_of' :: ‹'a::linorder list ⇒ (nat × 'a) option› where
          ‹posmin_of' l = (if l = [] then None else Some ((hd o rev o (sort_key snd) o (enumerate 0)) l))›
definition pos_of_min' :: ‹'a::linorder list ⇒ nat option› where
          ‹pos_of_min' l = map_option fst (posmin_of' l)›

lemma find_append_eq: ‹find P (xs@[x]) = (if find P xs = None then find P [x] else find P xs)›
proof (induction xs)
  case Nil
  then show ?case by simp 
next
  case (Cons a xs)
  then show ?case by simp 
qed

lemma posmax_of_split: ‹posmax_of (xs @ [x]) = posmax_of (xs) ∨ posmax_of (xs @ [x]) = Some (length xs,x)› 
proof(cases "posmax_of (xs @ [x]) = Some (length xs,x)")
  case True
  then show ?thesis by simp 
next
  case False note * = this
  then show ?thesis 
    apply(simp)
    unfolding posmax_of_def Let_def o_def max⇩l⇩i⇩s⇩t_def
    apply clarsimp
    apply (simp add: * max⇩l⇩i⇩s⇩t_append_eq enumerate_append_eq find_append_eq)
    apply(cases "xs=[]", simp) 
    apply (cases " find (λe. snd e = Max (insert x (set xs))) (enumerate 0 xs)" , simp_all)
    subgoal by (metis max_def)
    subgoal using  comp_def list.simps(15) max⇩l⇩i⇩s⇩t_append_eq max⇩l⇩i⇩s⇩t_def rotate1.simps(2) set_rotate1 
      by (smt (verit) List.finite_set Max.in_idem enumerate_eq_zip find_None_iff find_cong in_set_conv_nth in_set_zip max_def
          option.discI) 
    done
qed

lemma posmin_of_split: ‹posmin_of (xs @ [x]) = posmin_of (xs) ∨ posmin_of (xs @ [x]) = Some (length xs,x)› 
proof(cases "posmin_of (xs @ [x]) = Some (length xs,x)")
  case True
  then show ?thesis by simp 
next
  case False note * = this
  then show ?thesis 
  apply(simp)
    unfolding posmin_of_def Let_def o_def min⇩l⇩i⇩s⇩t_def
    apply (simp add: *  min⇩l⇩i⇩s⇩t_append_eq enumerate_append_eq find_append_eq)
    apply (cases "xs = []")
     apply simp
    apply (cases " find (λe. snd e = Min (insert x (set xs))) (enumerate 0 xs)", simp_all )
    subgoal
      by (metis linorder_not_le min.absorb4 min.orderE) 
    subgoal using 
       List.finite_set Min.insert Min.insert_remove Min.remove  enumerate_eq_zip
          find_None_iff find_cong in_set_conv_nth in_set_zip length_append length_map 
          list.size(3) map_nth min.orderE min_def option.simps(3) set_append set_empty 
      by (smt (verit) insort_insert_triv set_insort_insert)  
    done 
qed

lemma pos_of_max_split: 
  ‹pos_of_max (xs @ [x]) = pos_of_max (xs) ∨ pos_of_max (xs @ [x]) = Some (length xs)›
  using  pos_of_max_def posmax_of_split
  by (metis fst_eqD option.simps(9))

lemma pos_of_min_split: 
  ‹pos_of_min (xs @ [x]) = pos_of_min (xs) ∨ pos_of_min (xs @ [x]) = Some (length xs)›
  using  pos_of_min_def posmin_of_split
  by (metis fst_eqD option.simps(9))

lemma posmax_of_none: ‹(posmax_of xs = None) = (xs = []) ›
proof(induction "xs" rule:List.rev_induct)
  case Nil
  then show ?case 
    by (simp add: posmax_of_def)
next
  case (snoc x xs) note * = this
  then show ?case 
    unfolding posmax_of_def Let_def
    apply(clarsimp simp add:enumerate_append_eq find_append_eq)
    subgoal using  max⇩l⇩i⇩s⇩t_append_eq
      by (metis append_is_Nil_conv in_set_conv_decomp_last list.discI max⇩l⇩i⇩s⇩t_is_element 
          not_Some_eq old.prod.exhaust self_append_conv2 set_ConsD)
    done
qed

lemma posmin_of_none: ‹(posmin_of xs = None) = (xs = []) ›
proof(induction "xs" rule:List.rev_induct)
  case Nil
  then show ?case 
    by (simp add: posmin_of_def)
next
  case (snoc x xs) note * = this
  then show ?case 
    unfolding posmin_of_def Let_def
    apply(clarsimp simp add:enumerate_append_eq find_append_eq)[1]
    using min⇩l⇩i⇩s⇩t_append_eq
    by (metis append_Nil eq_snd_iff in_set_conv_nth list.distinct(1) list.size(3) min⇩l⇩i⇩s⇩t_is_element 
        not_less_zero option.exhaust set_ConsD)
qed

lemma posmax_of_in_snd: ‹(posmax_of xs) = Some p ⟹ snd p ∈ set xs›
  by (metis (mono_tags, lifting) List.finite_set comp_def eq_Max_iff find_Some_iff max⇩l⇩i⇩s⇩t_def 
                                 option.discI posmax_of_def posmax_of_none set_empty) 

lemma posmin_of_in_snd: ‹(posmin_of xs) = Some p ⟹ snd p ∈ set xs›
  by (metis (mono_tags, lifting) find_Some_iff min⇩l⇩i⇩s⇩t_is_element option.discI 
                                 posmin_of_def posmin_of_none)

lemma pos_of_max_none: ‹(pos_of_max xs = None) = (xs = []) ›
  by(simp add:pos_of_max_def posmax_of_none)

lemma pos_of_min_none: ‹(pos_of_min xs = None) = (xs = []) ›
  by(simp add:pos_of_min_def posmin_of_none)

lemma take_nth_drop_eq:
  assumes ‹xs ≠ []›
  and ‹n < length xs›
shows ‹xs = ((take n xs)@[xs!n]@(drop (n+1) xs))›
  by (simp add: Cons_nth_drop_Suc assms(2))

lemma max_in: 
  assumes ‹xs ≠ []›
  and ‹n < length xs›
  and ‹∀ x ∈ set ((take n xs)@(drop (n+1) xs)). xs!n > x›
shows ‹Max (set ((take n xs)@[xs!n]@(drop (n+1) xs))) = ((take n xs)@[xs!n]@(drop (n+1) xs))!n›
  using assms 
  apply(simp)
  by (metis List.finite_set Max_insert2 id_take_nth_drop order_le_less set_append) 

lemma min_in: 
  assumes ‹xs ≠ []›
  and ‹n < length xs›
  and ‹∀ x ∈ set ((take n xs)@(drop (n+1) xs)). xs!n < x›
shows ‹Min (set ((take n xs)@[xs!n]@(drop (n+1) xs))) = ((take n xs)@[xs!n]@(drop (n+1) xs))!n›
  using assms 
  apply(simp)
  by (metis List.finite_set Min_insert2 id_take_nth_drop nless_le set_append)

lemma max_in':
  assumes ‹xs ≠ []›
  and ‹n < length xs›
  and ‹∀ x ∈ set ((take n xs)@(drop (n+1) xs)). xs!n > x›
shows ‹Max (set xs) = xs!n›
  using assms max_in take_nth_drop_eq by metis

lemma min_in':
  assumes ‹xs ≠ []›
  and ‹n < length xs›
  and ‹∀ x ∈ set ((take n xs)@(drop (n+1) xs)). xs!n < x›
shows ‹Min (set xs) = xs!n›
  using assms min_in take_nth_drop_eq by metis

lemma snd_numerate_eq: 
  "xs ≠ [] ⟹ n < length xs  ⟹  j < n ⟹ snd (List.enumerate 0 xs ! j) = xs!j"
  by (simp add: nth_enumerate_eq) 

lemma nth_lower_max: 
  assumes ‹xs ≠ []›
  and ‹n < length xs›
  and ‹∀ x ∈ set ((take n xs)@(drop (n+1) xs)). x < xs!n›
shows ‹∀ j < n. xs!j < xs!n›
proof - 
  have  x1: ‹∀ x ∈ set ((take n xs)). x < xs!n› using assms by simp 
  then have x2: "(∀ j < n . (xs!j) ∈ set ((take n xs)))" 
    using assms(2) in_set_conv_nth by fastforce
  then show ?thesis 
    using x1 assms nth_take[of _ "n" "xs"]  by simp 
qed

lemma nth_higher_min: 
  assumes ‹xs ≠ []›
  and ‹n < length xs›
  and ‹∀ x ∈ set ((take n xs)@(drop (n+1) xs)). x > xs!n›
shows ‹∀ j < n. xs!j > xs!n›
proof - 
  have  x1: ‹∀ x ∈ set ((take n xs)). x > xs!n› using assms by simp 
  then have x2: "(∀ j < n . (xs!j) ∈ set ((take n xs)))" 
    using assms(2) in_set_conv_nth by fastforce
  then show ?thesis 
    using x1 assms nth_take[of _ "n" "xs"]  by simp 
qed

lemma posmax_of_le: 
  assumes ‹xs ≠ []›
  and ‹n < length xs›
  and ‹∀ x ∈ set ((take n xs)@(drop (n+1) xs)). x < xs!n›
shows ‹posmax_of xs = Some (n,xs!n)›
unfolding posmax_of_def max⇩l⇩i⇩s⇩t_def o_def Let_def
  apply(simp add: List.find_Some_iff)  
  apply(rule exI[of _ "n"])
  apply(simp add: max_in' assms nth_enumerate_eq)
  apply(rule conjI)
  subgoal using assms max_in' by metis  
  subgoal
    apply(simp add: assms max_in'[of "xs" "n"])      
    apply(simp add: assms snd_numerate_eq[of "xs" "n"])  
    using assms nth_lower_max[of "xs" "n"] by auto 
  done 

lemma posmin_of_le: 
  assumes ‹xs ≠ []›
  and ‹n < length xs›
  and ‹∀ x ∈ set ((take n xs)@(drop (n+1) xs)). x > xs!n›
shows ‹posmin_of xs = Some (n,xs!n)›
unfolding posmin_of_def min⇩l⇩i⇩s⇩t_def o_def Let_def
  apply(simp add: List.find_Some_iff)  
  apply(rule exI[of _ "n"])
  apply(simp add: min_in' assms nth_enumerate_eq)
  apply(rule conjI)
  subgoal using assms min_in' by metis  
  subgoal
    apply(simp add: assms min_in'[of "xs" "n"])      
    apply(simp add: assms snd_numerate_eq[of "xs" "n"])  
    using assms nth_higher_min[of "xs" "n"] by auto 
  done 
     
lemma pos_max_le: 
  assumes ‹xs ≠ []›
  and ‹n < length xs›
  and ‹∀ x ∈ set ((take n xs)@(drop (n+1) xs)). x < xs!n›
shows ‹(pos_of_max xs = Some n)›
  using posmax_of_le[of "xs" "n"] assms unfolding pos_of_max_def 
  by simp 

lemma pos_min_le: 
  assumes ‹xs ≠ []›
  and ‹n < length xs›
  and ‹∀ x ∈ set ((take n xs)@(drop (n+1) xs)). x > xs!n›
shows ‹(pos_of_min xs = Some n)›
  using posmin_of_le[of "xs" "n"] assms unfolding pos_of_min_def 
  by simp 

paragraph‹Distance of Maximum Prediction to Next Highest Prediction›
definition δ⇩m⇩i⇩n :: "real list ⇒ real" where 
          ‹δ⇩m⇩i⇩n l = (let m = max⇩l⇩i⇩s⇩t l in let m' = max⇩l⇩i⇩s⇩t (remove1 m l) in ¦m - m'¦)›

lemma leq_linear_real:
  assumes b_bound: ‹(b::real) ∈ {lb..up}› 
  and is_leq_at_bounds: ‹((c⇩1 * lb + c⇩0 ≤ c⇩1' * lb + c⇩0') ∧ (c⇩1 * up + c⇩0 ≤ c⇩1' * up + c⇩0'))›
shows ‹c⇩1 * b + c⇩0 ≤ c⇩1' * b + c⇩0'›
proof(cases ‹lb ≤ up›)
  case True
  then show ?thesis 
    using assms 
    by auto (smt (verit, best) Groups.mult_ac(2) left_diff_distrib mult_right_mono) 
next
  case False
  then show ?thesis using assms by(simp)
qed
  
lemma leq_linear_real':
  assumes b_bound: ‹(b::real) ∈ {lb..up}› 
  and is_leq_at_bounds: ‹((c⇩1 * up + c⇩0 ≤ c⇩1' * up + c⇩0') ∧ (c⇩1 * lb + c⇩0 ≤ c⇩1' * lb + c⇩0'))›
shows ‹c⇩1 * b + c⇩0 ≤ c⇩1' * b + c⇩0'›
proof(cases ‹lb ≤ up›)
  case True
  then show ?thesis using assms 
    using leq_linear_real by blast
next
  case False
  then show ?thesis using assms by(simp)
qed
lemma le_linear_real:
  assumes b_bound: ‹(b::real) ∈ {lb..up}› 
  and is_leq_at_bounds: ‹((c⇩1 * lb + c⇩0 < c⇩1' * lb + c⇩0') ∧ (c⇩1 * up + c⇩0 < c⇩1' * up + c⇩0'))›
shows ‹c⇩1 * b + c⇩0 < c⇩1' * b + c⇩0'›
proof(cases ‹lb < up›)
  case True
  then show ?thesis 
    using assms 
    by auto (smt (verit, best) Groups.mult_ac(2) left_diff_distrib mult_right_mono) 
next
  case False
  then show ?thesis using assms
    by (metis atLeastAtMost_iff nless_le order_le_less_trans)
qed
  
lemma le_linear_real':
  assumes b_bound: ‹(b::real) ∈ {lb..up}› 
  and is_leq_at_bounds: ‹((c⇩1 * up + c⇩0 < c⇩1' * up + c⇩0') ∧ (c⇩1 * lb + c⇩0 < c⇩1' * lb + c⇩0'))›
shows ‹c⇩1 * b + c⇩0 < c⇩1' * b + c⇩0'›
proof(cases ‹lb ≤ up›)
  case True
  then show ?thesis using assms 
    using le_linear_real by blast
next
  case False
  then show ?thesis using assms by(simp)
qed

lemma  pos_max_leq': ‹(pos_of_max xs = Some n) ⟹ ∀ x ∈ set xs. x ≤ xs!n›
  apply(simp add: pos_of_max_def posmax_of_def max⇩l⇩i⇩s⇩t_def) 
  by (smt (verit) List.finite_set Max_ge add_0 find_Some_iff fst_conv length_enumerate 
                  nth_enumerate_eq snd_conv)

end