Theory Compass_Digraph

(***********************************************************************************
 * 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‹Neural Networks as Directed Graphs (\thy)›

theory
  Compass_Digraph 
  imports 
  Neural_Networks.NN_Digraph_Main 
begin

subsubsection‹Manual Encoding›

paragraph‹Definition: Neurons›

definition "m_N0 ≡ In 0"
definition "m_N1 ≡ In 1"
definition "m_N2 ≡ In 2"
definition "m_N3 ≡ In 3"
definition "m_N4 ≡ In 4"
definition "m_N5 ≡ In 5"
definition "m_N6 ≡ In 6"
definition "m_N7 ≡ In 7"
definition "m_N8 ≡ In 8"
definition "m_N9 ≡ Neuron ⦇φ = Identity, α = 1, β = 7082077 / 1000000000, uid = 9⦈"
definition "m_N10 ≡ Neuron ⦇φ = Identity, α = 1, β = 107544795 / 1000000000, uid = 10⦈"
definition "m_N11 ≡ Neuron ⦇φ = Identity, α = 1, β = - 15743796 / 1000000000, uid = 11⦈"
definition "m_N12 ≡ Neuron ⦇φ = Identity, α = 1, β = 47920802 / 100000000, uid = 12⦈"
definition "m_N13 ≡ Neuron ⦇φ = Identity, α = 1, β = - 16364478 / 100000000, uid = 13⦈"
definition "m_N14 ≡ Neuron ⦇φ = Identity, α = 1, β = - 24132763 / 100000000, uid = 14⦈"
definition "m_N15 ≡ Neuron ⦇φ = Identity, α = 1, β = - 30579916 / 100000000, uid = 15⦈"
definition "m_N16 ≡ Out 16"
definition "m_N17 ≡ Out 17"
definition "m_N18 ≡ Out 18"
definition "m_N19 ≡ Out 19"

lemmas
  m_neuron_defs = m_N0_def m_N1_def m_N2_def m_N3_def m_N4_def m_N5_def m_N6_def m_N7_def m_N8_def 
                  m_N9_def m_N10_def m_N11_def m_N12_def m_N13_def m_N14_def m_N15_def m_N16_def 
                  m_N17_def m_N18_def m_N19_def

definition "m_Neurons = [m_N0, m_N1, m_N2, m_N3, m_N4, m_N5, m_N6, m_N7, m_N8, m_N9, m_N10, m_N11, 
                         m_N12, m_N13, m_N14, m_N15, m_N16, m_N17, m_N18, m_N19]"

paragraph‹Definition: Edges›

definition "m_E12_16 ≡ ⦇ω = 1, tl = m_N12, hd = m_N16⦈"
definition "m_E13_17 ≡ ⦇ω = 1, tl = m_N13, hd = m_N17⦈"
definition "m_E14_18 ≡ ⦇ω = 1, tl = m_N14, hd = m_N18⦈"
definition "m_E15_19 ≡ ⦇ω = 1, tl = m_N15, hd = m_N19⦈"
definition "m_E9_12 ≡ ⦇ω = 8217673 / 200000000, tl = m_N9, hd = m_N12⦈"
definition "m_E10_12 ≡ ⦇ω = 2972081 / 20000000, tl = m_N10, hd = m_N12⦈"
definition "m_E11_12 ≡ ⦇ω = 2445593 / 10000000, tl = m_N11, hd = m_N12⦈"
definition "m_E9_13 ≡ ⦇ω = - (11993983 / 5000000), tl = m_N9, hd = m_N13⦈"
definition "m_E10_13 ≡ ⦇ω = - (3894687 / 50000000), tl = m_N10, hd = m_N13⦈"
definition "m_E11_13 ≡ ⦇ω = 646179 / 1250000, tl = m_N11, hd = m_N13⦈"
definition "m_E9_14 ≡ ⦇ω = - (2323241 / 5000000), tl = m_N9, hd = m_N14⦈"
definition "m_E10_14 ≡ ⦇ω = 10928257 / 10000000, tl = m_N10, hd = m_N14⦈"
definition "m_E11_14 ≡ ⦇ω = - (7042477 / 5000000), tl = m_N11, hd = m_N14⦈"
definition "m_E9_15 ≡ ⦇ω = 19465483 / 10000000, tl = m_N9, hd = m_N15⦈"
definition "m_E10_15 ≡ ⦇ω = - (9524061 / 10000000), tl = m_N10, hd = m_N15⦈"
definition "m_E11_15 ≡ ⦇ω = - (31743723 / 50000000), tl = m_N11, hd = m_N15⦈"
definition "m_E0_9 ≡ ⦇ω =  3342313 / 5000000, tl = m_N0, hd = m_N9⦈"
definition "m_E1_9 ≡ ⦇ω = - (12952799 / 10000000), tl = m_N1, hd = m_N9⦈"
definition "m_E2_9 ≡ ⦇ω = - (1428979 / 5000000), tl = m_N2, hd = m_N9⦈"
definition "m_E3_9 ≡ ⦇ω = 8650103 / 5000000, tl = m_N3, hd = m_N9⦈"
definition "m_E4_9 ≡ ⦇ω =  63918763 / 100000000, tl = m_N4, hd = m_N9⦈"
definition "m_E5_9 ≡ ⦇ω = - (6959659 / 5000000), tl = m_N5, hd = m_N9⦈"
definition "m_E6_9 ≡ ⦇ω = - (9054079 / 20000000), tl = m_N6, hd = m_N9⦈"
definition "m_E7_9 ≡ ⦇ω = 13654941 / 10000000, tl = m_N7, hd = m_N9⦈"
definition "m_E8_9 ≡ ⦇ω = - (18450487 / 100000000), tl = m_N8, hd = m_N9⦈"
definition "m_E0_10 ≡ ⦇ω = 314303 / 5000000, tl = m_N0, hd = m_N10⦈"
definition "m_E1_10 ≡ ⦇ω = 915709 / 2500000, tl = m_N1, hd = m_N10⦈"
definition "m_E2_10 ≡ ⦇ω = 6922799 / 10000000, tl = m_N2, hd = m_N10⦈"
definition "m_E3_10 ≡ ⦇ω = - (9399607 / 25000000), tl = m_N3, hd = m_N10⦈"
definition "m_E4_10 ≡ ⦇ω = 15055849 / 100000000, tl = m_N4, hd = m_N10⦈"
definition "m_E5_10 ≡ ⦇ω = 10981513 / 10000000, tl = m_N5, hd = m_N10⦈"
definition "m_E6_10 ≡ ⦇ω = 3420911 / 200000000, tl = m_N6, hd = m_N10⦈"
definition "m_E7_10 ≡ ⦇ω = 7420693 / 10000000, tl = m_N7, hd = m_N10⦈"
definition "m_E8_10 ≡ ⦇ω = 15639223 / 100000000, tl = m_N8, hd = m_N10⦈"
definition "m_E0_11 ≡ ⦇ω = 9863281 / 100000000, tl = m_N0, hd = m_N11⦈"
definition "m_E1_11 ≡ ⦇ω = 9530481 / 10000000, tl = m_N1, hd = m_N11⦈"
definition "m_E2_11 ≡ ⦇ω = 35006753 / 100000000, tl = m_N2, hd = m_N11⦈"
definition "m_E3_11 ≡ ⦇ω = 7897923 / 10000000, tl = m_N3, hd = m_N11⦈"
definition "m_E4_11 ≡ ⦇ω = - (11627171 / 20000000), tl = m_N4, hd = m_N11⦈"
definition "m_E5_11 ≡ ⦇ω = 2839861 / 5000000, tl = m_N5, hd = m_N11⦈"
definition "m_E6_11 ≡ ⦇ω = 5311743 / 10000000, tl = m_N6, hd = m_N11⦈"
definition "m_E7_11 ≡ ⦇ω = - (9090567 / 10000000), tl = m_N7, hd = m_N11⦈"
definition "m_E8_11 ≡ ⦇ω = - (181917 / 400000), tl = m_N8, hd = m_N11⦈"

lemmas
m_edge_defs = m_E12_16_def m_E13_17_def m_E14_18_def m_E15_19_def m_E9_12_def m_E10_12_def 
              m_E11_12_def m_E9_13_def m_E10_13_def m_E11_13_def m_E9_14_def m_E10_14_def 
              m_E11_14_def m_E9_15_def m_E10_15_def m_E11_15_def m_E0_9_def m_E1_9_def m_E2_9_def
              m_E3_9_def m_E4_9_def m_E5_9_def m_E6_9_def m_E7_9_def m_E8_9_def m_E0_10_def 
              m_E1_10_def m_E2_10_def m_E3_10_def m_E4_10_def m_E5_10_def m_E6_10_def m_E7_10_def
              m_E8_10_def m_E0_11_def m_E1_11_def m_E2_11_def m_E3_11_def m_E4_11_def m_E5_11_def 
              m_E6_11_def m_E7_11_def m_E8_11_def

definition
  ‹m_Edges = [m_E12_16, m_E13_17, m_E14_18, m_E15_19, m_E9_12, m_E10_12, m_E11_12, m_E9_13, m_E10_13, 
              m_E11_13, m_E9_14, m_E10_14, m_E11_14, m_E9_15, m_E10_15, m_E11_15, m_E0_9, m_E1_9, 
              m_E2_9, m_E3_9, m_E4_9, m_E5_9, m_E6_9, m_E7_9, m_E8_9, m_E0_10, m_E1_10, m_E2_10, 
              m_E3_10, m_E4_10, m_E5_10, m_E6_10, m_E7_10, m_E8_10, m_E0_11, m_E1_11, m_E2_11, 
              m_E3_11, m_E4_11, m_E5_11, m_E6_11, m_E7_11, m_E8_11]›

definition 
  ‹m_Graph ≡ mk_nn_pregraph m_Edges›

paragraph‹Definition: Activation Tab›

fun m_φ_compass where 
  ‹m_φ_compass  Identity = Some identity›
| ‹m_φ_compass _ = None›

paragraph‹Definition: Neural Network›

definition
  ‹m_NeuralNet = ⦇graph = m_Graph, activation_tab = m_φ_compass⦈›

paragraph ‹Locale Interpretations›

global_interpretation m_compass: nn_pregraph m_Graph
  apply(simp add: m_Graph_def)
  apply(simp add: nn_pregraph_mk nn_pregraph.axioms)
  done 
     

subsubsection ‹Automated Encoding Using The TensorFlow Import›

paragraph‹Single Encoding›
declare [[nn_proof_mode = eval]]
import_TensorFlow compass file "model/model.json" as digraph_single
declare [[nn_proof_mode = nbe]]


thm compass.neuron_defs       
thm compass.Neurons_def
thm compass.edge_defs
thm compass.Edges_def
thm compass.Graph_def
thm compass.verts_set_conv
thm compass.edges_set_conv
thm compass.φ_compass.simps
thm compass.NeuralNet_def
thm compass.nn_pregraph_axioms
thm compass.neural_network_digraph_single_axioms

text ‹importing the data files›

import_data_file "model/input.txt" defining input
import_data_file "model/predictions.txt" defining predictions

thm input_def
thm predictions_def

value ‹(checkget_result_singleton 0.15 (predictdigraph_single compass.NeuralNet (map_of_list (input!0)) E12_16)) (Some (predictions!0!0))›
value ‹(checkget_result_singleton 0.15 (predictdigraph_single compass.NeuralNet (map_of_list (input!0)) E12_16)) (Some (predictions!1!0))›
value ‹(checkget_result_singleton 0.15 (predictdigraph_single compass.NeuralNet (map_of_list (input!0)) E12_16)) (Some (predictions!2!0))›
value ‹(checkget_result_singleton 0.15 (predictdigraph_single compass.NeuralNet (map_of_list (input!0)) E12_16)) (Some (predictions!3!0))›

lemma compass_truth_table_predict:
  ‹(predictdigraph_single compass.NeuralNet (map_of_list (input!0)) E12_16) ≈[0.0001]≈s (Some (predictions!0!0))›
  ‹(predictdigraph_single compass.NeuralNet (map_of_list (input!1)) E12_16) ≈[0.0001]≈s (Some (predictions!1!0))›
  ‹(predictdigraph_single compass.NeuralNet (map_of_list (input!2)) E12_16) ≈[0.0001]≈s (Some (predictions!2!0))›
  ‹(predictdigraph_single compass.NeuralNet (map_of_list (input!3)) E12_16) ≈[0.0001]≈s (Some (predictions!3!0))›
  by(normalization)+

lemma compass_truth_table_predict':
  ‹(predictdigraph_single_list compass.NeuralNet (input!0) ≈[0.0001]≈l (Some (predictions!0)))›
  ‹(predictdigraph_single_list compass.NeuralNet (input!1) ≈[0.0001]≈l (Some (predictions!1)))›
  ‹(predictdigraph_single_list compass.NeuralNet (input!2) ≈[0.0001]≈l (Some (predictions!2)))›
  ‹(predictdigraph_single_list compass.NeuralNet (input!3) ≈[0.0001]≈l (Some (predictions!3)))›
  by(normalization)+

paragraph‹Multi Encoding›

declare [[nn_proof_mode = eval]]
import_TensorFlow compass_multi file "model/model.json" as digraph
declare [[nn_proof_mode = nbe]]

thm compass_multi.neuron_defs
thm compass_multi.Neurons_def

thm compass_multi.edge_defs
thm compass_multi.Edges_def

thm compass_multi.Graph_def
thm compass_multi.verts_set_conv
thm compass_multi.edges_set_conv

thm compass_multi.φ_compass_multi.simps

thm compass_multi.NeuralNet_def

thm compass_multi.nn_pregraph_axioms
thm compass_multi.neural_network_digraph_axioms

paragraph‹Checking Equivalence of Manual Definitions and Automated Import›

lemma Neurons_equiv: "compass.Neurons = m_Neurons"
  by(normalization)

lemma Edges_equiv: "compass.Edges = m_Edges"
  by(normalization)

lemma Graph_equiv: "compass.Graph = m_Graph"
  unfolding compass.Graph_def m_Graph_def
  by (simp add: Edges_equiv)

lemma φ_equiv: "compass.φ_compass f = m_φ_compass f"
  by(cases "f", simp_all)

lemma NeuralNet_equiv: "compass.NeuralNet = m_NeuralNet"
  unfolding compass.NeuralNet_def m_NeuralNet_def
  by(auto simp add: Graph_equiv φ_equiv)

lemma ‹ predictdigraph_single_list compass.NeuralNet =  predictdigraph_single_list m_NeuralNet›
  using NeuralNet_equiv by simp

paragraph‹Code Evaluation›

definition "NW = [0::nat ↦ 1, 1::nat ↦ 1, 2::nat ↦ 1,
                  3::nat ↦ 1, 4::nat ↦ 1, 5::nat ↦ 0,
                  6::nat ↦ 1, 7::nat ↦ 0, 8::nat ↦ 1]"

definition ‹eval_compass = predictdigraph_single compass.NeuralNet NW compass.Edges.E12_16›

end