Theory Transformation01

(*****************************************************************************
 * Copyright (c) 2005-2010 ETH Zurich, Switzerland
 *               2008-2015 Achim D. Brucker, Germany
 *               2009-2016 Université Paris-Sud, France
 *               2015-2016 The University of Sheffield, 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 list of conditions and the following disclaimer.
 *
 *     * 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.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * 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
 * OWNER 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.
 *****************************************************************************)

subsection ‹Transformation Example 1›
theory 
  Transformation01
  imports 
    "../../UPF-Firewall"
begin

definition
  FWLink :: "adr⇩_i⇩_p net" where
  "FWLink = {{(a,b). a = 1}}"
  
definition
  any :: "adr⇩_i⇩_p net" where
  "any = {{(a,b). a > 5}}"
  
definition
  i4:: "adr⇩_i⇩_p net" where
  "i4 = {{(a,b). a = 2 }}" 
  
definition
  i27:: "adr⇩_i⇩_p net" where
  "i27 = {{(a,b). a = 3 }}" 
  
definition
  eth_intern:: "adr⇩_i⇩_p net" where
  "eth_intern = {{(a,b). a = 4 }}"
  
definition
  eth_private:: "adr⇩_i⇩_p net" where
  "eth_private = {{(a,b). a = 5 }}"

definition
  (* Mandatory: Global *)
  MG2 :: "(adr⇩_i⇩_p net,port) Combinators" where
  "MG2 = AllowPortFromTo i27 any 1 ⊕ 
       AllowPortFromTo i27 any 2 ⊕
       AllowPortFromTo i27 any 3"
  
definition
  MG3 :: "(adr⇩_i⇩_p net,port) Combinators" where
  "MG3 = AllowPortFromTo any FWLink 1"
  
definition
  MG4 :: "(adr⇩_i⇩_p net,port) Combinators" where
  "MG4 = AllowPortFromTo FWLink FWLink 4"
  
definition
  MG7 :: "(adr⇩_i⇩_p net,port) Combinators" where
  "MG7 = AllowPortFromTo FWLink i4 6 ⊕
       AllowPortFromTo FWLink i4 7"
  
definition
  MG8 :: "(adr⇩_i⇩_p net,port) Combinators" where
  "MG8 = AllowPortFromTo FWLink i4 6 ⊕
       AllowPortFromTo FWLink i4 7"
  
  (* Default Global *)
definition
  DG3:: "(adr⇩_i⇩_p net,port) Combinators" where
  "DG3 = AllowPortFromTo any any 7"

definition
  "Policy = DenyAll ⊕ MG8 ⊕  MG7 ⊕ MG4 ⊕ MG3 ⊕ MG2 ⊕ DG3"   

lemmas PolicyLemmas =  Policy_def
  FWLink_def
  any_def
  i27_def
  i4_def
  eth_intern_def
  eth_private_def
  MG2_def MG3_def MG4_def MG7_def MG8_def  
  DG3_def

lemmas PolicyL =  MG2_def MG3_def MG4_def MG7_def MG8_def DG3_def Policy_def

definition 
  not_in_same_net :: "(adr⇩_i⇩_p,DummyContent) packet ⇒ bool" where
  "not_in_same_net x =  (((src x ⊏ i27) ⟶ ( ¬ (dest x ⊏ i27))) ∧
                      ((src x ⊏  i4) ⟶ ( ¬ (dest x ⊏ i4))) ∧
                      ((src x ⊏  eth_intern) ⟶ ( ¬ (dest x ⊏ eth_intern))) ∧
                      ((src x ⊏  eth_private) ⟶ ( ¬ (dest x ⊏ eth_private))))"
                   
consts fixID :: id
consts fixContent :: DummyContent

definition "fixElements p = (id p = fixID ∧ content p = fixContent)"

lemmas fixDefs = fixElements_def NetworkCore.id_def NetworkCore.content_def



lemma sets_distinct1: "(n::int) ≠ m ⟹ {(a,b). a = n} ≠ {(a,b). a = m}"
  by auto

lemma sets_distinct2: "(m::int) ≠ n ⟹ {(a,b). a = n} ≠ {(a,b). a = m}"
  by auto

lemma sets_distinct3: "{((a::int),(b::int)). a = n} ≠ {(a,b). a > n}"
  by auto

lemma sets_distinct4: "{((a::int),(b::int)). a > n} ≠ {(a,b). a = n}"
  by auto

lemma aux: "⟦a ∈ c; a ∉ d; c = d⟧ ⟹ False"
  by auto 
    
lemma sets_distinct5: "(s::int) < g ⟹ {(a::int, b::int). a = s} ≠ {(a::int, b::int).  g < a}"
  apply (auto simp: sets_distinct3)[1]
  apply (subgoal_tac "(s,4) ∈ {(a::int,b::int). a = (s)}")
   apply (subgoal_tac "(s,4) ∉ {(a::int,b::int). g < a}")
    apply (erule aux)
     apply assumption+
   apply simp
  by blast

lemma sets_distinct6: "(s::int) < g ⟹ {(a::int, b::int).  g < a} ≠ {(a::int, b::int).  a = s}"
  apply (rule not_sym)
  apply (rule sets_distinct5)
  by simp

lemma distinctNets: "FWLink ≠  any ∧ FWLink ≠  i4 ∧ FWLink ≠  i27 ∧ FWLink ≠  eth_intern ∧ FWLink ≠   eth_private ∧ 
any ≠  FWLink ∧ any ≠  i4 ∧ any ≠  i27 ∧ any ≠  eth_intern ∧ any ≠  eth_private ∧ i4 ≠  FWLink ∧ 
i4 ≠  any ∧ i4 ≠  i27 ∧ i4 ≠  eth_intern ∧ i4 ≠  eth_private ∧ i27 ≠  FWLink ∧ i27 ≠  any ∧ 
i27 ≠  i4 ∧ i27 ≠  eth_intern ∧ i27 ≠  eth_private ∧ eth_intern ≠  FWLink ∧ eth_intern ≠  any ∧ 
eth_intern ≠  i4 ∧ eth_intern ≠  i27 ∧ eth_intern ≠  eth_private ∧ eth_private ≠  FWLink ∧ 
eth_private ≠  any ∧ eth_private ≠  i4 ∧ eth_private ≠  i27 ∧ eth_private ≠  eth_intern"
  by (simp add: PolicyLemmas sets_distinct1 sets_distinct2 sets_distinct3 sets_distinct4 
                sets_distinct5 sets_distinct6)

lemma aux5: "⟦x ≠ a; y≠b; (x ≠ y ∧ x ≠ b) ∨  (a ≠ b ∧ a ≠ y)⟧ ⟹ {x,a} ≠ {y,b}"
  by auto

lemma aux2: "{a,b} = {b,a}"
  by auto

lemma ANDex: "allNetsDistinct (policy2list Policy)"
  apply (simp add: PolicyL allNetsDistinct_def distinctNets)
  by (auto simp: PLemmas PolicyLemmas netsDistinct_def sets_distinct5 sets_distinct6)
    
fun (sequential) numberOfRules where 
  "numberOfRules (a⊕b) = numberOfRules a + numberOfRules b"
|"numberOfRules a = (1::int)" 

fun numberOfRulesList where 
 "numberOfRulesList  (x#xs) = ((numberOfRules x)#(numberOfRulesList xs)) "
 |"numberOfRulesList [] = []" 

lemma all_in_list: "all_in_list (policy2list Policy) (Nets_List Policy)"
  apply (simp add: PolicyL)
  apply (unfold Nets_List_def)
  apply (unfold bothNets_def)
  apply (insert distinctNets)
  by simp

lemmas normalizeUnfold =   normalize_def Policy_def Nets_List_def bothNets_def aux aux2 bothNets_def

end