Theory Properties_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‹Desirable Properties of Neural Networks Predictions (\thy)›

theory Properties_Matrix
  imports
  Properties
  Prediction_Utils_Matrix
  Jordan_Normal_Form.Matrix
begin

definition zip_vec :: "'a Matrix.vec ⇒ 'b Matrix.vec ⇒ ('a × 'b) Matrix.vec" where
  "zip_vec A B ≡ Matrix.vec (dim_vec A) (λ i. ((A $ i), (B $ i)))"

fun map_vec2 :: ‹('a ⇒ 'b ⇒ 'c ) ⇒ 'a Matrix.vec ⇒ 'b Matrix.vec ⇒ 'c Matrix.vec ›
  where
"map_vec2 f xs ys = map_vec ( λ (x,y). f x y) (zip_vec xs ys)"

fun checkget_result_mat where
  ‹checkget_result_mat _ None None           = (None, True)›
 |‹checkget_result_mat ε (Some xs) (Some ys) = (Some xs, fold (∧) (list_of_vec (map_vec2 (λ x y. x ≈[ε]≈ y) xs ys)) True)›
 |‹checkget_result_mat _ r _ = (r, False)›

definition ‹check_result_mat r ε s = snd (checkget_result_mat ε r s)›
notation check_result_mat ("((_)/ ≈[(_)]≈⇩m (_))" [60, 60] 60)

definition ensure_testdata_range_mat :: ‹real ⇒ real Matrix.vec list ⇒ (real Matrix.vec ⇀ real Matrix.vec) ⇒ real Matrix.vec list ⇒ bool›
  where
 ‹ensure_testdata_range_mat delta inputs P outputs 
      = foldl (∧) True 
        (map (λ e. (P (fst e))  ≈[delta]≈⇩m Some (snd e)) 
             (zip inputs outputs))›
notation ensure_testdata_range_mat ("(_) ⊨⇩m {(_)} (_) {(_)}" [61, 3, 90, 3] 60)

paragraph‹Interval Arithmetic›

definition ‹intervals_of_mat δ A = Matrix.vec (dim_vec A) (λ i. Interval((A$i)-¦δ¦,(A$i)+¦δ¦)) ›

definition ‹intervals_of_m δ = map (intervals_of_mat δ) ›

fun check_result_mat_interval_mat :: ‹'a::preorder Matrix.vec option ⇒ 'a interval Matrix.vec option ⇒ bool› where
   ‹check_result_mat_interval_mat None None           = True› 
 | ‹check_result_mat_interval_mat (Some xs) (Some ys) = fold (∧) (list_of_vec (map_vec2 (λ x y. x ∈ set_of y) xs ys)) True› 
 | ‹check_result_mat_interval_mat _ _ = False›

notation check_result_mat_interval_mat ("((_)/ ≈⇩m (_))" [60, 60] 60)

text ‹We define @{term "check_result_mat_interval"} for checking that two matrices are approximatively 
equal (we need the error interval due to possible rounding errors in IEEE754 arithmetic in python 
compared to mathematical reals in Isabelle).›

definition ensure_testdata_interval_mat :: ‹real Matrix.vec list ⇒ (real Matrix.vec ⇀ real Matrix.vec) ⇒ real interval Matrix.vec list ⇒ bool› 
  where 
 ‹ensure_testdata_interval_mat inputs P outputs 
      = foldl (∧) True 
        (map (λ e . let a = (P  (fst e)) in let b = Some (snd e) in (a ≈⇩m b))
             (zip inputs outputs)) ›
notation ensure_testdata_interval_mat ("⊨⇩i⇩m {(_)} (_) {(_)}" [3, 90, 3] 60)


text ‹Using @{term "check_result_mat_interval"} we now define the property 
@{term "ensure_testdata_interval"} to check that the (symbolically) computed predictions of a neural 
network meet our expectations.›

subsubsection‹Maximum Classifiers›

definition
  ensure_testdata_max_mat :: ‹real Matrix.vec list ⇒ (real Matrix.vec ⇀ real Matrix.vec) ⇒ real Matrix.vec list ⇒ bool› 
  where
 ‹ensure_testdata_max_mat inputs P outputs 
   = foldl (∧) True
      (map (λ e. case P (fst e) of 
                   None ⇒ False 
                 | Some p ⇒ pos_of_max p = pos_of_max (snd e))
           (zip inputs outputs))›
notation ensure_testdata_max_mat ("⊨⇩m {(_)} (_) {(_)}" [3, 90, 3] 60)

text ‹Many classification networks use the maximum output as the result, without normalisation 
(e.g., to values between 0 and 1). In such cases, a weaker form of ensuring compliance to 
predictions might be used that only checks that checks for the maximum output of each given input, 
this can be tested using @{term "ensure_testdata_max"}›
end