Theory Prediction_Utils_Matrix

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

subsection‹Useful Definitions for Analysing Matrix Predictions (\thy)›

theory
  Prediction_Utils_Matrix 
  imports 
    Complex_Main
    Jordan_Normal_Form.Matrix
begin


definition max⇩m⇩a⇩t :: ‹'a::linorder Matrix.mat ⇒ 'a› where 
  ‹max⇩m⇩a⇩t =  Max o elements_mat›

definition min⇩m⇩a⇩t :: ‹'a::linorder Matrix.mat ⇒ 'a› where 
  ‹min⇩m⇩a⇩t  =  Min o elements_mat›


lemma finite_elements_mat: "finite (elements_mat A)"
  unfolding elements_mat_def by blast

lemma max⇩m⇩a⇩t_is_element:
  shows ‹elements_mat m ≠ {} ⟹ max⇩m⇩a⇩t m ∈ elements_mat m›
  by (simp add: finite_elements_mat max⇩m⇩a⇩t_def)

lemma min⇩m⇩a⇩t_is_element:
  ‹elements_mat m ≠ {} ⟹ min⇩m⇩a⇩t m ∈ elements_mat m›
  by (simp add: finite_elements_mat min⇩m⇩a⇩t_def)

definition max_list :: "'a::linorder list ⇒ 'a" where
  "max_list xs = fold max xs (hd xs)"

definition min_list :: "'a::linorder list ⇒ 'a" where
  "min_list xs = fold min xs (hd xs)"

definition max⇩v⇩e⇩c :: ‹'a::linorder Matrix.vec ⇒ 'a› where 
  ‹max⇩v⇩e⇩c =  max_list  o list_of_vec›

definition min⇩v⇩e⇩c :: ‹'a::linorder Matrix.vec ⇒ 'a› where 
  ‹min⇩v⇩e⇩c  =  min_list o list_of_vec›

lemma max⇩v⇩e⇩c_is_element:
  shows ‹list_of_vec m ≠ [] ⟹ max⇩v⇩e⇩c m ∈ set(list_of_vec m)›
  apply (simp add: max⇩v⇩e⇩c_def max_list_def) 
  by (metis List.finite_set Max.set_eq_fold Max_eq_iff hd_in_set list.discI set_ConsD set_empty2)

lemma min⇩v⇩e⇩c_is_element:
  shows ‹list_of_vec m ≠ [] ⟹ min⇩v⇩e⇩c m ∈ set(list_of_vec m)›
  apply (simp add: min⇩v⇩e⇩c_def min_list_def) 
  by (metis List.finite_set Min.set_eq_fold Min_in empty_iff insert_absorb list.set_sel(1) list.simps(15))


lemma max⇩v⇩e⇩c_vCons_append_eq: ‹max⇩v⇩e⇩c (vCons x xs) = max⇩v⇩e⇩c xs ∨ max⇩v⇩e⇩c (vCons x xs) = x›
proof(cases "max⇩v⇩e⇩c (vCons x xs) = x")
  case True
  then show ?thesis by blast
next
  case False
  then show ?thesis apply(simp add: max⇩v⇩e⇩c_def max_list_def Max_eq_iff insertCI insertE ) 
    by (smt (verit) List.finite_set Max.in_idem Max.set_eq_fold Max_insert comp_apply 
        fold_simps(1) list.simps(15) list.simps(3) list_of_vec_vCons max.right_idem max⇩v⇩e⇩c_def
        max⇩v⇩e⇩c_is_element max_list_def set_ConsD set_empty2) (*takes long*)

qed

lemma max⇩v⇩e⇩c_append_eq: ‹max⇩v⇩e⇩c (vec_of_list (xs @ [x])) = max⇩v⇩e⇩c (vec_of_list xs) ∨ max⇩v⇩e⇩c (vec_of_list (xs @ [x])) = x›
proof(cases "max⇩v⇩e⇩c (vec_of_list (xs @ [x])) = x")
  case True
  then show ?thesis by blast
next
  case False
  then show ?thesis 
    apply(simp add: max⇩v⇩e⇩c_def max⇩v⇩e⇩c_is_element max_list_def) 
    by (metis (no_types, lifting) append_self_conv2 comp_apply fold.simps(1) 
        fold_append fold_simps(2) hd_append2 id_apply list.sel(1) list_vec max_def)
qed

lemma min⇩v⇩e⇩c_vCons_append_eq: ‹min⇩v⇩e⇩c (vCons x xs) = min⇩v⇩e⇩c xs ∨ min⇩v⇩e⇩c (vCons x xs) = x›
proof(cases "min⇩v⇩e⇩c (vCons x xs) = x")
  case True
  then show ?thesis by blast
next
  case False
  then show ?thesis 
    apply(simp add: min⇩v⇩e⇩c_def min_list_def Min_eq_iff insertCI insertE ) 
    by (metis (no_types, lifting) List.finite_set Min.in_idem Min.insert 
        Min.semilattice_set_axioms Min_def fold_simps(1) list.set_sel(1) list.simps(15) 
        min_def semilattice_set.set_eq_fold set_empty)
qed

lemma min⇩v⇩e⇩c_append_eq: ‹min⇩v⇩e⇩c (vec_of_list (xs @ [x])) = min⇩v⇩e⇩c (vec_of_list xs) ∨ min⇩v⇩e⇩c (vec_of_list (xs @ [x])) = x›
proof(cases "min⇩v⇩e⇩c (vec_of_list (xs @ [x])) = x")
  case True
  then show ?thesis by blast
next
  case False
  then show ?thesis
    apply(simp add: min⇩v⇩e⇩c_def min⇩v⇩e⇩c_is_element min_list_def)
    by (metis (no_types, lifting) append_self_conv2 comp_apply fold.simps(1) 
        fold_append fold_simps(2) hd_append2 id_apply list.sel(1) list_vec min_def)
qed

lemma max⇩v⇩e⇩c_vec_cons_eq: ‹max⇩v⇩e⇩c ((vec_of_list [x]) @⇩v xs) = max⇩v⇩e⇩c xs ∨ max⇩v⇩e⇩c ((vec_of_list [x]) @⇩v xs) = x›
proof(cases "max⇩v⇩e⇩c ((vec_of_list [x]) @⇩v xs) = x")
  case True
  then show ?thesis by blast
next
  case False
  then show ?thesis
    apply(simp add: max⇩v⇩e⇩c_def max_list_def)
    using  max_def 
    by (metis (no_types, lifting) comp_apply fold_simps(2) list.sel(1) 
        list_of_vec_vCons max⇩v⇩e⇩c_def max⇩v⇩e⇩c_vCons_append_eq max_list_def)
qed

lemma max⇩v⇩e⇩c_cons_eq: ‹max⇩v⇩e⇩c (vec_of_list (x#xs)) = max⇩v⇩e⇩c (vec_of_list xs) ∨ max⇩v⇩e⇩c (vec_of_list (x#xs)) = x›
proof(cases "max⇩v⇩e⇩c (vec_of_list (x#xs)) = x")
  case True
  then show ?thesis by blast
next
  case False
  then show ?thesis
    apply(simp add: max⇩v⇩e⇩c_def max⇩v⇩e⇩c_is_element max_list_def) 
    by (metis (no_types, lifting) comp_apply fold_simps(2) list.sel(1) 
        list_of_vec_vCons max.idem max⇩v⇩e⇩c_def max⇩v⇩e⇩c_vCons_append_eq max_list_def)
qed

lemma min⇩v⇩e⇩c_vec_cons_eq: ‹min⇩v⇩e⇩c ((vec_of_list [x]) @⇩v xs) = min⇩v⇩e⇩c xs ∨ min⇩v⇩e⇩c ((vec_of_list [x]) @⇩v xs) = x›
proof(cases "min⇩v⇩e⇩c ((vec_of_list [x]) @⇩v xs) = x")
  case True
  then show ?thesis by blast
next
  case False
  then show ?thesis
    apply(simp add: max⇩v⇩e⇩c_def) 
    using min⇩v⇩e⇩c_vCons_append_eq by blast
qed

lemma min⇩l⇩i⇩s⇩t_cons_eq: ‹min⇩v⇩e⇩c (vec_of_list (x#xs)) = min⇩v⇩e⇩c (vec_of_list xs) ∨ min⇩v⇩e⇩c (vec_of_list (x#xs)) = x›
proof(cases "min⇩v⇩e⇩c (vec_of_list (x#xs)) = x")
  case True
  then show ?thesis by blast
next
  case False
  then show ?thesis
    apply (simp add: min⇩v⇩e⇩c_def min⇩v⇩e⇩c_is_element min_list_def)
    by (metis (no_types, lifting) comp_apply fold_simps(2) list.sel(1) 
        list_of_vec_vCons min.idem min⇩v⇩e⇩c_def min⇩v⇩e⇩c_vCons_append_eq min_list_def)
qed

lemma max⇩v⇩e⇩c_vec_append_limit: assumes ‹xs ≠ vNil› shows ‹max⇩v⇩e⇩c xs ≤ max⇩v⇩e⇩c (vCons x xs)›
proof(cases "max⇩v⇩e⇩c (vCons x xs) = x")
  case True 
  then show ?thesis using assms 
    apply (simp add: max⇩v⇩e⇩c_def max_list_def) 
    by (metis List.finite_set Max.set_eq_fold Max_insert hd_in_set insert_absorb 
        list.simps(15) max.orderI set_empty2 vec_list vec_of_list_Nil)
next
  case False
  then show ?thesis
    using dual_order.order_iff_strict max⇩v⇩e⇩c_vCons_append_eq by auto
qed 

lemma max⇩v⇩e⇩c_append_limit: assumes ‹xs ≠ []› shows ‹max⇩v⇩e⇩c (vec_of_list xs) ≤ max⇩v⇩e⇩c (vec_of_list (xs @ [x]))›
proof(cases "max⇩v⇩e⇩c (vec_of_list (xs @ [x])) = x")
  case True 
  then show ?thesis using assms
    apply (simp add: max⇩v⇩e⇩c_def  max⇩v⇩e⇩c_is_element max_list_def )
    by (metis List.finite_set Max.set_eq_fold Max_ge comp_apply list.set_intros(2) 
        list_vec max⇩v⇩e⇩c_def max⇩v⇩e⇩c_is_element max_list_def rotate1.simps(2) set_rotate1)
next
  case False
  then show ?thesis 
    by (metis dual_order.refl max⇩v⇩e⇩c_append_eq)
qed 

lemma min⇩v⇩e⇩c_vec_append_limit: assumes ‹xs ≠ vNil› shows ‹min⇩v⇩e⇩c xs ≥ min⇩v⇩e⇩c (vCons x xs)›
proof(cases " min⇩v⇩e⇩c (vCons x xs) = x")
  case True 
  then show ?thesis using assms 
    apply (simp add: min⇩v⇩e⇩c_def min_list_def)
    by (metis List.finite_set Min.insert Min.set_eq_fold 
        Orderings.order_eq_iff hd_in_set insert_absorb list.simps(15) 
        min_def set_empty2 vec_list vec_of_list_Nil)
next
  case False
  then show ?thesis 
    by (metis dual_order.refl min⇩v⇩e⇩c_vCons_append_eq)
qed 

lemma min⇩v⇩e⇩c_append_limit: assumes ‹xs ≠ []› shows ‹min⇩v⇩e⇩c (vec_of_list xs) ≥  min⇩v⇩e⇩c (vec_of_list (xs @ [x]))›
proof(cases "min⇩v⇩e⇩c (vec_of_list (xs @ [x])) = x")
  case True 
  then show ?thesis using assms
    apply (simp add: min⇩v⇩e⇩c_def  min⇩v⇩e⇩c_is_element min_list_def )
    by (metis (no_types, lifting) append.right_neutral comp_apply 
        fold_append fold_simps(2) hd_append2 linorder_linear list_vec min_def)
next
  case False
  then show ?thesis
    by (metis dual_order.refl min⇩v⇩e⇩c_append_eq)
qed 

lemma max⇩v⇩e⇩c_vec_cons_limit: assumes ‹xs ≠ vNil› shows ‹max⇩v⇩e⇩c xs ≤ max⇩v⇩e⇩c ((vec_of_list [x]) @⇩v xs)›
proof(cases "max⇩v⇩e⇩c ((vec_of_list [x]) @⇩v xs) = x")
  case True 
  then show ?thesis using assms
    by (metis append_vec_vCons append_vec_vNil max⇩v⇩e⇩c_vec_append_limit vec_of_list_Cons 
        vec_of_list_Nil)
next
  case False
  then show ?thesis
    by (simp add: assms max⇩v⇩e⇩c_vec_append_limit)
qed 

lemma max⇩v⇩e⇩c_cons_limit: assumes ‹xs ≠ []› shows ‹max⇩v⇩e⇩c (vec_of_list xs) ≤ max⇩v⇩e⇩c (vec_of_list (x#xs))›
proof(cases "max⇩v⇩e⇩c (vec_of_list (x#xs)) = x")
  case True 
  then show ?thesis using assms
    by (metis list_vec max⇩v⇩e⇩c_vec_append_limit vec_of_list_Cons vec_of_list_Nil)
next
  case False
  then show ?thesis
    by (metis dual_order.refl max⇩v⇩e⇩c_cons_eq) 
qed 

lemma min⇩v⇩e⇩c_vec_cons_limit: assumes ‹xs ≠ vNil› shows ‹min⇩v⇩e⇩c xs ≥ min⇩v⇩e⇩c ((vec_of_list [x]) @⇩v xs)›
proof(cases "min⇩v⇩e⇩c ((vec_of_list [x]) @⇩v xs) = x")
  case True 
  then show ?thesis using assms
    by (metis append_vec_vCons append_vec_vNil min⇩v⇩e⇩c_vec_append_limit vec_of_list_Cons 
        vec_of_list_Nil)
next
  case False
  then show ?thesis
    by (simp add: assms min⇩v⇩e⇩c_vec_append_limit)
qed 

lemma min⇩v⇩e⇩c_cons_limit: assumes ‹xs ≠ []› shows ‹min⇩v⇩e⇩c (vec_of_list xs) ≥  min⇩v⇩e⇩c (vec_of_list (x#xs))›
proof(cases "min⇩v⇩e⇩c (vec_of_list (x#xs)) = x")
  case True 
  then show ?thesis using assms
    by (metis list_vec min⇩v⇩e⇩c_vec_append_limit vec_of_list_Cons vec_of_list_Nil)
next
  case False
  then show ?thesis 
    by (metis min⇩l⇩i⇩s⇩t_cons_eq order_refl) 
qed

paragraph‹Converting Predictions to Percentages›

definition prediction2percentage :: ‹real Matrix.vec ⇒ real Matrix.vec› where
  ‹prediction2percentage m = (let m' = max⇩v⇩e⇩c m in map_vec (λ e. e / m' *  100.0) m)›


lemma prediction2percentage_id: 
  assumes ‹max⇩v⇩e⇩c p = 100› 
  shows ‹prediction2percentage p = p›
  using assms unfolding prediction2percentage_def
  by auto


paragraph‹Maximum Prediction›

definition posmax_of :: ‹'a::linorder Matrix.vec ⇒ (nat × 'a) option› where
  ‹posmax_of l = (let m = max⇩v⇩e⇩c l in find (λ e. snd e = m) (indexed_from 0 (list_of_vec l)))›
definition pos_of_max :: ‹'a::linorder Matrix.vec ⇒ nat option› where
  ‹pos_of_max l = map_option fst (posmax_of l)›

definition posmax_of' :: ‹'a::linorder Matrix.vec ⇒ (nat × 'a) option› where
  ‹posmax_of' l = (let l' = list_of_vec l in 
                          (if l' = [] then None
                                      else Some ((hd o rev o (sort_key snd) o (indexed_from 0)) l')))›
definition pos_of_max' :: ‹'a::linorder Matrix.vec ⇒ nat option› where
  ‹pos_of_max' l = map_option fst (posmax_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

paragraph‹Distance of Maximum Prediction to Next Highest Prediction›

definition δ⇩m⇩i⇩n :: "real mat ⇒ real" where 
  ‹δ⇩m⇩i⇩n m = (let m'  = max⇩m⇩a⇩t m; m'' = Max (elements_mat m - {m'})
                    in ¦m' - m''¦ )›

end