Theory FWNormalisationCore

(*****************************************************************************
 * 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 ‹Policy Normalisation: Core Definitions›
theory
  FWNormalisationCore
imports
  "../PacketFilter/PacketFilter"
begin

text‹
  This theory contains all the definitions used for policy normalisation as described 
  in~\<^cite>‹"brucker.ea:icst:2010" and "brucker.ea:formal-fw-testing:2014"›.

  The normalisation procedure transforms policies into semantically equivalent  ones which are 
  ``easier'' to test. It is organized into nine phases. We impose the following two restrictions 
  on the input policies: 
  \begin{itemize}
  \item Each policy must contain a $\mathtt{DenyAll}$ rule. If this restriction were to be lifted, 
        the $\mathtt{insertDenies}$ phase would have to be adjusted accordingly.
  \item For each pair of networks $n_1$ and $n_2$, the networks are either disjoint or equal. If 
        this restriction were to be lifted, we would need some additional phases before the start 
        of the normalisation procedure presented below. This rule would split single rules into 
        several by splitting up the networks such that they are all pairwise disjoint or equal. 
        Such a transformation is clearly semantics-preserving and the condition would hold after
        these phases.
  \end{itemize}
  As a result, the procedure generates a list of policies, in which:
  \begin{itemize}
  \item each element of the list contains a policy which completely specifies the blocking behavior 
        between two networks, and
  \item there are no shadowed rules.
  \end{itemize}
  This result is desirable since the test case generation for rules between networks $A$ and $B$ 
  is independent of the rules that specify the behavior for traffic flowing between networks $C$ 
  and $D$. Thus, the different segments of the policy can be processed individually. The 
  normalization procedure does not aim to minimize the number of rules. While it does remove 
  unnecessary ones, it also adds new ones, enabling a policy to be split into several independent
  parts.
›

text‹
  Policy transformations are functions that map policies to policies.  We decided to represent
  policy transformations as \emph{syntactic rules}; this choice paves the way for expressing the 
  entire normalisation process inside HOL by functions manipulating abstract policy syntax. 
›


subsubsection‹Basics›
text‹We define a very simple policy language:›

datatype ('α,'β) Combinators = 
  DenyAll
  | DenyAllFromTo 'α 'α 
  | AllowPortFromTo 'α 'α 'β 
  | Conc "(('α,'β) Combinators)" "(('α,'β) Combinators)" (infixr ‹⊕› 80)

text‹
  And define the semantic interpretation of it. For technical reasons, we fix here the type to 
  policies over IntegerPort addresses. However, we could easily provide definitions for other
  address types as well, using a generic constants for the type definition and a primitive 
  recursive definition for each desired address model.  
›

subsubsection‹Auxiliary definitions and functions.›
text‹
  This section defines several functions which are useful later for the combinators, invariants, 
  and proofs. 
›
  
fun srcNet where 
 "srcNet (DenyAllFromTo x y) = x"
|"srcNet (AllowPortFromTo x y p) = x"
|"srcNet DenyAll = undefined"
|"srcNet (v ⊕ va) = undefined" 

fun destNet where 
 "destNet (DenyAllFromTo x y) = y"
|"destNet (AllowPortFromTo x y p) = y"
|"destNet DenyAll = undefined"
|"destNet (v ⊕ va) = undefined" 

fun srcnets where
 "srcnets DenyAll = [] " 
|"srcnets (DenyAllFromTo x y) = [x] " 
|"srcnets (AllowPortFromTo x y p) = [x] " 
|"(srcnets (x ⊕ y)) = (srcnets x)@(srcnets y)"

fun destnets where
 "destnets DenyAll = [] " 
|"destnets (DenyAllFromTo x y) = [y] " 
|"destnets (AllowPortFromTo x y p) = [y] "
|"(destnets (x ⊕ y)) = (destnets x)@(destnets y)"

fun (sequential) net_list_aux where
 "net_list_aux [] = []"
|"net_list_aux (DenyAll#xs) = net_list_aux xs"
|"net_list_aux ((DenyAllFromTo x y)#xs) = x#y#(net_list_aux xs)"
|"net_list_aux ((AllowPortFromTo x y p)#xs) = x#y#(net_list_aux xs)"
|"net_list_aux ((x⊕y)#xs) = (net_list_aux [x])@(net_list_aux [y])@(net_list_aux xs)"

fun net_list where "net_list p = remdups (net_list_aux p)"

definition bothNets where "bothNets x = (zip (srcnets x) (destnets x))"

fun (sequential) normBothNets where 
 "normBothNets ((a,b)#xs) = (if ((b,a) ∈ set xs) ∨ (a,b) ∈ set (xs) 
                            then (normBothNets xs)
                            else (a,b)#(normBothNets xs))"
|"normBothNets x = x" 

fun makeSets where 
 "makeSets ((a,b)#xs) = ({a,b}#(makeSets xs))"
|"makeSets [] = []"

fun bothNet where
 "bothNet DenyAll = {}"
|"bothNet (DenyAllFromTo a b) = {a,b}"
|"bothNet (AllowPortFromTo a b p) = {a,b}"
|"bothNet (v ⊕ va) = undefined "

text‹
  $Nets\_List$ provides from a list of rules a list where the entries are the appearing sets of 
  source and destination network of each rule. 
›

definition Nets_List 
  where 
  "Nets_List x = makeSets (normBothNets (bothNets x))"

fun (sequential) first_srcNet where 
  "first_srcNet (x⊕y) = first_srcNet x"
| "first_srcNet x = srcNet x"

fun (sequential) first_destNet where 
  "first_destNet (x⊕y) = first_destNet x"
| "first_destNet x = destNet x"

fun (sequential) first_bothNet where
 "first_bothNet (x⊕y) = first_bothNet x"
|"first_bothNet x = bothNet x"

fun (sequential) in_list where 
 "in_list DenyAll l = True"
|"in_list x l = (bothNet x ∈ set l)"

fun all_in_list where 
 "all_in_list [] l = True"
|"all_in_list (x#xs) l = (in_list x l ∧ all_in_list xs l)" 

fun (sequential) member where
 "member a (x⊕xs) = ((member a x) ∨ (member a xs))"
|"member a x = (a = x)"

fun sdnets where
  "sdnets DenyAll = {}"
| "sdnets (DenyAllFromTo a b) = {(a,b)}"
| "sdnets (AllowPortFromTo a b c) = {(a,b)}"
| "sdnets (a ⊕ b) = sdnets a ∪ sdnets b"

definition packet_Nets  where "packet_Nets x a b = ((src x ⊏ a ∧ dest x ⊏ b) ∨
                                                    (src x ⊏ b ∧ dest x ⊏ a))"

definition subnetsOfAdr where "subnetsOfAdr a = {x. a ⊏ x}"

definition fst_set where "fst_set s = {a. ∃ b. (a,b) ∈ s}"

definition snd_set where "snd_set s = {a. ∃ b. (b,a) ∈ s}"

fun memberP where
 "memberP r (x#xs) = (member r x ∨ memberP r xs)"
|"memberP r [] = False"

fun firstList where 
 "firstList (x#xs) = (first_bothNet x)"
|"firstList [] = {}"

subsubsection‹Invariants›

text‹If there is a DenyAll, it is at the first position›
fun wellformed_policy1:: "(('α, 'β) Combinators) list ⇒ bool" where 
  "wellformed_policy1 [] = True"
| "wellformed_policy1 (x#xs) = (DenyAll ∉ (set xs))" 

text‹There is a DenyAll at the first position›
fun wellformed_policy1_strong:: "(('α, 'β) Combinators) list ⇒ bool"
where 
  "wellformed_policy1_strong [] = False"
| "wellformed_policy1_strong (x#xs) = (x=DenyAll ∧ (DenyAll ∉ (set xs)))" 


text‹All two networks are either disjoint or equal.›
definition netsDistinct where "netsDistinct a b = (¬ (∃ x. x ⊏ a ∧ x ⊏ b))"

definition twoNetsDistinct where
  "twoNetsDistinct a b c d = (netsDistinct a c ∨ netsDistinct b d)"

definition allNetsDistinct where 
  "allNetsDistinct p = (∀ a b. (a ≠ b ∧ a ∈ set (net_list p) ∧
                        b ∈ set (net_list p)) ⟶ netsDistinct a b)"

definition disjSD_2 where 
 "disjSD_2 x y = (∀ a b c d. ((a,b)∈sdnets x ∧  (c,d) ∈sdnets y ⟶
      (twoNetsDistinct a b c d ∧ twoNetsDistinct a b d c)))"

text‹The policy is given as a list of single rules.›
fun singleCombinators where 
"singleCombinators [] = True"
|"singleCombinators ((x⊕y)#xs) = False"
|"singleCombinators (x#xs) = singleCombinators xs"

definition onlyTwoNets where
 "onlyTwoNets x = ((∃ a b. (sdnets x = {(a,b)})) ∨ (∃ a b. sdnets x = {(a,b),(b,a)}))" 

text‹Each entry of the list contains rules between two networks only.›
fun OnlyTwoNets where 
 "OnlyTwoNets (DenyAll#xs) = OnlyTwoNets xs"
|"OnlyTwoNets (x#xs) = (onlyTwoNets x ∧ OnlyTwoNets xs)"
|"OnlyTwoNets [] = True"

fun noDenyAll where
 "noDenyAll (x#xs) = ((¬ member DenyAll x) ∧ noDenyAll xs)"
|"noDenyAll [] = True"

fun noDenyAll1 where 
  "noDenyAll1 (DenyAll#xs) = noDenyAll xs"
| "noDenyAll1 xs = noDenyAll xs"

fun separated where
  "separated (x#xs) = ((∀ s. s ∈ set xs ⟶ disjSD_2 x s) ∧ separated xs)"
| "separated [] = True"

fun NetsCollected where 
  "NetsCollected (x#xs) = (((first_bothNet x ≠ firstList xs) ⟶
          (∀a∈set xs. first_bothNet x ≠ first_bothNet a)) ∧ NetsCollected (xs))"
| "NetsCollected [] = True"

fun NetsCollected2 where
 "NetsCollected2 (x#xs) = (xs = [] ∨ (first_bothNet x ≠ firstList xs ∧
                           NetsCollected2 xs))"
|"NetsCollected2 [] = True"

subsubsection‹Transformations›

text ‹
  The following two functions transform a policy into a list of single rules and vice-versa (by 
  staying on the combinator level).
›

fun policy2list::"('α, 'β) Combinators ⇒
                 (('α, 'β) Combinators) list" where
 "policy2list (x ⊕ y) = (concat [(policy2list x),(policy2list y)])"
|"policy2list x = [x]"

fun list2FWpolicy::"(('α, 'β) Combinators) list ⇒
                  (('α, 'β) Combinators)" where
 "list2FWpolicy [] = undefined "
|"list2FWpolicy (x#[]) = x"
|"list2FWpolicy (x#y) = x ⊕ (list2FWpolicy y)"

text‹Remove all the rules appearing before a DenyAll. There are two alternative versions.›

fun removeShadowRules1 where
  "removeShadowRules1 (x#xs) = (if (DenyAll ∈ set xs) 
                                then ((removeShadowRules1 xs))
                                else x#xs)"
| "removeShadowRules1 [] = []"

fun  removeShadowRules1_alternative_rev where
  "removeShadowRules1_alternative_rev [] = []"
| "removeShadowRules1_alternative_rev (DenyAll#xs) = [DenyAll]"
| "removeShadowRules1_alternative_rev [x] = [x]"
| "removeShadowRules1_alternative_rev (x#xs)=
                 x#(removeShadowRules1_alternative_rev xs)"

definition removeShadowRules1_alternative where
   "removeShadowRules1_alternative p =
                         rev (removeShadowRules1_alternative_rev (rev p))"

text‹
  Remove all the rules which allow a port, but are shadowed by a deny between these subnets.
›

fun removeShadowRules2::  "(('α, 'β) Combinators) list ⇒
                          (('α, 'β) Combinators) list"
where
  "(removeShadowRules2 ((AllowPortFromTo x y p)#z)) = 
        (if (((DenyAllFromTo x y) ∈ set z)) 
         then ((removeShadowRules2 z))
         else (((AllowPortFromTo x y p)#(removeShadowRules2 z))))"
| "removeShadowRules2 (x#y) = x#(removeShadowRules2 y)"
| "removeShadowRules2 [] = []"

text‹
  Sorting a policies:  We first need to define an ordering on rules.  This ordering depends 
   on the $Nets\_List$ of a policy.  
›

fun smaller :: "('α, 'β) Combinators ⇒ 
                ('α, 'β) Combinators ⇒ 
                (('α) set) list ⇒ bool" 
where
 "smaller DenyAll x l = True" 
| "smaller x DenyAll l = False"
| "smaller x y l = 
 ((x = y) ∨         (if (bothNet x) = (bothNet y) then 
                       (case y of (DenyAllFromTo a b) ⇒ (x = DenyAllFromTo b a)  
                            | _ ⇒  True)
                    else
                        (position (bothNet x) l <= position (bothNet y) l)))"

text‹We provide two different sorting algorithms: Quick Sort (qsort) and Insertion Sort (sort)›

fun qsort where
  "qsort [] l     = []"
| "qsort (x#xs) l = (qsort [y←xs. ¬ (smaller x y l)] l) @ [x] @ (qsort [y←xs. smaller x y l] l)"

lemma qsort_permutes:
  "set (qsort xs l) = set xs"
  apply (induct "xs" "l" rule: qsort.induct)
  by (auto)

lemma set_qsort [simp]: "set (qsort xs l)  = set xs" 
  by (simp add: qsort_permutes)
    
fun insort where
	  "insort a [] l = [a]"
	| "insort a (x#xs) l = (if (smaller a x l) then a#x#xs else x#(insort a xs l))"

fun sort where
  "sort [] l = []"
| "sort (x#xs) l = insort x (sort xs l) l"

fun sorted  where
  "sorted [] l = True"
| "sorted [x] l = True"
| "sorted (x#y#zs) l = (smaller x y l ∧ sorted (y#zs) l)"

fun separate where
 "separate (DenyAll#x) = DenyAll#(separate x)"
| "separate (x#y#z) = (if (first_bothNet x = first_bothNet y) 
                   then (separate ((x⊕y)#z))
                   else (x#(separate(y#z))))"
|"separate x = x"                

text ‹
  Insert the DenyAllFromTo rules, such that traffic between two networks can be tested 
  individually.
›

fun  insertDenies where
 "insertDenies (x#xs) = (case x of DenyAll ⇒ (DenyAll#(insertDenies xs))
                    | _  ⇒ (DenyAllFromTo (first_srcNet x) (first_destNet x) ⊕ 
                       (DenyAllFromTo (first_destNet x) (first_srcNet x)) ⊕ x)#
                                (insertDenies xs))"
| "insertDenies [] = []"

text‹
  Remove duplicate rules. This is especially necessary as insertDenies might have inserted 
  duplicate rules. The second function is supposed to work on a list of policies. Only
  rules which are duplicated within the same policy are removed.  
›


fun removeDuplicates where
  "removeDuplicates (x⊕xs) = (if member x xs then (removeDuplicates xs)
                              else x⊕(removeDuplicates xs))"
| "removeDuplicates x = x"

fun removeAllDuplicates where 
 "removeAllDuplicates (x#xs) = ((removeDuplicates (x))#(removeAllDuplicates xs))"
|"removeAllDuplicates x = x"

text ‹Insert a DenyAll at the beginning of a policy.›
fun insertDeny where 
 "insertDeny (DenyAll#xs) = DenyAll#xs"
|"insertDeny xs = DenyAll#xs"


definition "sort' p l = sort l p"
definition "qsort' p l = qsort l p"

declare dom_eq_empty_conv [simp del]

fun list2policyR::"(('α, 'β) Combinators) list ⇒
                   (('α, 'β) Combinators)" where
 "list2policyR (x#[]) = x"
|"list2policyR (x#y) = (list2policyR y) ⊕ x"
|"list2policyR [] = undefined "


text‹
  We provide the definitions for two address representations. 
›


subsubsection‹IntPort›

fun C :: "(adr⇩i⇩p net, port) Combinators ⇒ (adr⇩i⇩p,DummyContent) packet ↦ unit"
where
" C DenyAll = deny_all" 
|"C (DenyAllFromTo x y) = deny_all_from_to x y"
|"C (AllowPortFromTo x y p) = allow_from_to_port p x y"
|"C  (x ⊕ y) =  C x ++ C y"

fun CRotate :: "(adr⇩i⇩p net, port) Combinators ⇒ (adr⇩i⇩p,DummyContent) packet ↦ unit"
where
" CRotate DenyAll = C DenyAll" 
|"CRotate (DenyAllFromTo x y) = C (DenyAllFromTo x y)"
|"CRotate (AllowPortFromTo x y p) = C (AllowPortFromTo x y p)"
|"CRotate (x ⊕ y) = ((CRotate y) ++ ((CRotate x)))"

fun rotatePolicy where
  "rotatePolicy DenyAll = DenyAll" 
| "rotatePolicy (DenyAllFromTo a b) = DenyAllFromTo a b"
| "rotatePolicy (AllowPortFromTo a b p) = AllowPortFromTo a b p"
| "rotatePolicy (a⊕b) = (rotatePolicy b) ⊕ (rotatePolicy a)"

lemma check: "rev (policy2list (rotatePolicy p)) = policy2list p"
  apply (induct "p")
  by (simp_all) 


text‹
  All rules appearing at the left of a DenyAllFromTo, have disjunct domains from it 
  (except DenyAll). 
›
fun (sequential) wellformed_policy2 where
  "wellformed_policy2 [] = True"
| "wellformed_policy2 (DenyAll#xs) = wellformed_policy2 xs"
| "wellformed_policy2 (x#xs) = ((∀ c a b. c = DenyAllFromTo a b ∧ c ∈ set xs ⟶
                 Map.dom (C x) ∩ Map.dom (C c) = {}) ∧ wellformed_policy2 xs)"

text‹
  An allow rule is disjunct with all rules appearing at the right of it. This invariant is not 
  necessary as it is a consequence from others, but facilitates some proofs. 
›

fun (sequential) wellformed_policy3::"((adr⇩i⇩p net,port) Combinators) list ⇒ bool" where
  "wellformed_policy3 [] = True"
| "wellformed_policy3 ((AllowPortFromTo a b p)#xs) = ((∀ r. r ∈ set xs ⟶
      dom (C r) ∩ dom (C (AllowPortFromTo a b p)) = {}) ∧ wellformed_policy3 xs)"
| "wellformed_policy3 (x#xs) = wellformed_policy3 xs"


definition 
  "normalize' p  = (removeAllDuplicates o insertDenies o separate o
                   (sort' (Nets_List p))  o removeShadowRules2 o remdups o
                   (rm_MT_rules C) o insertDeny o removeShadowRules1 o
                   policy2list) p"

definition 
  "normalizeQ' p  = (removeAllDuplicates o insertDenies o separate o
                   (qsort' (Nets_List p))  o removeShadowRules2 o remdups o
                   (rm_MT_rules C) o insertDeny o removeShadowRules1 o
                   policy2list) p"

definition normalize :: 
  "(adr⇩i⇩p net, port) Combinators ⇒ 
   (adr⇩i⇩p net, port) Combinators list" 
where
   "normalize p = (removeAllDuplicates (insertDenies (separate (sort
                   (removeShadowRules2 (remdups ((rm_MT_rules C) (insertDeny
                  (removeShadowRules1 (policy2list p)))))) ((Nets_List p))))))"

definition
   "normalize_manual_order p l = removeAllDuplicates (insertDenies (separate
    (sort (removeShadowRules2 (remdups ((rm_MT_rules C) (insertDeny
    (removeShadowRules1 (policy2list p)))))) ((l)))))"

definition normalizeQ :: 
  "(adr⇩i⇩p net, port) Combinators ⇒ 
   (adr⇩i⇩p net, port) Combinators list" 
where
   "normalizeQ p = (removeAllDuplicates (insertDenies (separate (qsort
                   (removeShadowRules2 (remdups ((rm_MT_rules C) (insertDeny
                  (removeShadowRules1 (policy2list p)))))) ((Nets_List p))))))"

definition
   "normalize_manual_orderQ p l = removeAllDuplicates (insertDenies (separate
    (qsort (removeShadowRules2 (remdups ((rm_MT_rules C) (insertDeny
    (removeShadowRules1 (policy2list p)))))) ((l)))))"

text‹
  Of course, normalize is equal to normalize', the latter looks nicer though. 
›
lemma "normalize = normalize'"
  by (rule ext, simp add: normalize_def normalize'_def sort'_def)

declare C.simps [simp del]


subsubsection‹TCP\_UDP\_IntegerPort›

fun Cp :: "(adr⇩i⇩p⇩p net, protocol × port) Combinators ⇒ 
          (adr⇩i⇩p⇩p,DummyContent) packet ↦ unit"
where
 " Cp DenyAll = deny_all"  
|"Cp (DenyAllFromTo x y) = deny_all_from_to x y"
|"Cp (AllowPortFromTo x y p) = allow_from_to_port_prot (fst p) (snd p) x y"
|"Cp  (x ⊕ y) =  Cp x ++ Cp y"


fun Dp :: "(adr⇩i⇩p⇩p net, protocol × port) Combinators ⇒ 
          (adr⇩i⇩p⇩p,DummyContent) packet ↦ unit"
where
" Dp DenyAll = Cp DenyAll" 
|"Dp (DenyAllFromTo x y) = Cp (DenyAllFromTo x y)"
|"Dp (AllowPortFromTo x y p) = Cp (AllowPortFromTo x y p)"
|"Dp  (x ⊕ y) =  Cp (y ⊕ x)"

text‹
  All rules appearing at the left of a DenyAllFromTo, have disjunct domains from it 
  (except DenyAll). 
›
fun (sequential) wellformed_policy2Pr where
  "wellformed_policy2Pr [] = True"
| "wellformed_policy2Pr (DenyAll#xs) = wellformed_policy2Pr xs"
| "wellformed_policy2Pr (x#xs) = ((∀ c a b. c = DenyAllFromTo a b ∧ c ∈ set xs ⟶
                 Map.dom (Cp x) ∩ Map.dom (Cp c) = {}) ∧ wellformed_policy2Pr xs)"

text‹
  An allow rule is disjunct with all rules appearing at the right of it. This invariant is not
  necessary as it is a consequence from others, but facilitates some proofs. 
›

fun (sequential) wellformed_policy3Pr::"((adr⇩i⇩p⇩p net, protocol × port) Combinators) list ⇒ bool" where
  "wellformed_policy3Pr [] = True"
| "wellformed_policy3Pr ((AllowPortFromTo a b p)#xs) = ((∀ r. r ∈ set xs ⟶
      dom (Cp r) ∩ dom (Cp (AllowPortFromTo a b p)) = {}) ∧ wellformed_policy3Pr xs)"
| "wellformed_policy3Pr (x#xs) = wellformed_policy3Pr xs"

definition 
 normalizePr' :: "(adr⇩i⇩p⇩p net, protocol × port) Combinators
  ⇒ (adr⇩i⇩p⇩p net, protocol × port) Combinators list" where 
 "normalizePr' p = (removeAllDuplicates o insertDenies o separate o
                   (sort' (Nets_List p))  o removeShadowRules2 o remdups o
                   (rm_MT_rules Cp) o insertDeny o removeShadowRules1 o
                   policy2list) p"

definition normalizePr :: 
"(adr⇩i⇩p⇩p net, protocol × port) Combinators
  ⇒ (adr⇩i⇩p⇩p net, protocol × port) Combinators list" where
   "normalizePr p = (removeAllDuplicates (insertDenies (separate (sort
                   (removeShadowRules2 (remdups ((rm_MT_rules Cp) (insertDeny
                  (removeShadowRules1 (policy2list p)))))) ((Nets_List p))))))"

definition
   "normalize_manual_orderPr p l = removeAllDuplicates (insertDenies (separate
    (sort (removeShadowRules2 (remdups ((rm_MT_rules Cp) (insertDeny
    (removeShadowRules1 (policy2list p)))))) ((l)))))"


definition 
 normalizePrQ' :: "(adr⇩i⇩p⇩p net, protocol × port) Combinators
  ⇒ (adr⇩i⇩p⇩p net, protocol × port) Combinators list" where 
 "normalizePrQ' p = (removeAllDuplicates o insertDenies o separate o
                   (qsort' (Nets_List p))  o removeShadowRules2 o remdups o
                   (rm_MT_rules Cp) o insertDeny o removeShadowRules1 o
                   policy2list) p"

definition normalizePrQ :: 
"(adr⇩i⇩p⇩p net, protocol × port) Combinators
  ⇒ (adr⇩i⇩p⇩p net, protocol × port) Combinators list" where
   "normalizePrQ p = (removeAllDuplicates (insertDenies (separate (qsort
                   (removeShadowRules2 (remdups ((rm_MT_rules Cp) (insertDeny
                  (removeShadowRules1 (policy2list p)))))) ((Nets_List p))))))"

definition
   "normalize_manual_orderPrQ p l = removeAllDuplicates (insertDenies (separate
    (qsort (removeShadowRules2 (remdups ((rm_MT_rules Cp) (insertDeny
    (removeShadowRules1 (policy2list p)))))) ((l)))))"

text‹
  Of course, normalize is equal to normalize', the latter looks nicer though. 
›
lemma "normalizePr = normalizePr'"
  by (rule ext, simp add: normalizePr_def normalizePr'_def sort'_def)


text‹
  The following definition helps in creating the test specification for the individual parts 
  of a normalized policy. 
›
definition makeFUTPr where 
   "makeFUTPr FUT p x n = 
     (packet_Nets x (fst (normBothNets (bothNets p)!n))  
                     (snd(normBothNets (bothNets p)!n)) ⟶ 
    FUT x = Cp ((normalizePr p)!Suc n) x)"

declare Cp.simps [simp del]

lemmas PLemmas = C.simps Cp.simps dom_def PolicyCombinators.PolicyCombinators
                 PortCombinators.PortCombinatorsCore aux
                 ProtocolPortCombinators.ProtocolCombinatorsCore src_def dest_def in_subnet_def
                 adr⇩i⇩p⇩pLemmas adr⇩i⇩p⇩pLemmas

lemma aux: "⟦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
end