From e0dac8a3ab4b270eb056c48fed6890b319bb4004 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Tue, 27 Dec 2016 23:43:47 +0000 Subject: [PATCH] Checked style. --- PacketFilter/DatatypeAddress.thy | 6 +-- PacketFilter/DatatypePort.thy | 10 ++-- PacketFilter/IPv4.thy | 8 +-- PacketFilter/IPv4_TCPUDP.thy | 11 ++-- PacketFilter/IntegerAddress.thy | 10 ++-- PacketFilter/IntegerPort.thy | 6 +-- PacketFilter/IntegerPort_TCPUDP.thy | 16 +++--- PacketFilter/NetworkCore.thy | 20 +++---- PacketFilter/NetworkModels.thy | 18 +++---- PacketFilter/PacketFilter.thy | 8 +-- PacketFilter/PolicyCombinators.thy | 15 +++--- PacketFilter/PolicyCore.thy | 4 +- PacketFilter/PortCombinators.thy | 66 +++++++++++------------- PacketFilter/Ports.thy | 17 +++--- PacketFilter/ProtocolPortCombinators.thy | 46 ++++++++--------- 15 files changed, 127 insertions(+), 134 deletions(-) diff --git a/PacketFilter/DatatypeAddress.thy b/PacketFilter/DatatypeAddress.thy index e01a5ef..5b1f9a6 100644 --- a/PacketFilter/DatatypeAddress.thy +++ b/PacketFilter/DatatypeAddress.thy @@ -38,8 +38,8 @@ subsection {* Datatype Addresses *} theory DatatypeAddress -imports - NetworkCore + imports + NetworkCore begin text{* @@ -58,5 +58,5 @@ definition definition internet::"DatatypeAddress net" where "internet = {{internet_adr}}" - + end diff --git a/PacketFilter/DatatypePort.thy b/PacketFilter/DatatypePort.thy index c036948..7498326 100644 --- a/PacketFilter/DatatypePort.thy +++ b/PacketFilter/DatatypePort.thy @@ -36,8 +36,10 @@ *****************************************************************************) subsection {* Datatype Addresses with Ports *} -theory DatatypePort -imports NetworkCore +theory + DatatypePort + imports + NetworkCore begin text{* @@ -67,7 +69,7 @@ definition overloading src_port_datatype \ "src_port :: ('\::adr,'\) packet \ '\::port" begin definition - "src_port_datatype (x::(DatatypePort,'\) packet) \ (snd o fst o snd) x" + "src_port_datatype (x::(DatatypePort,'\) packet) \ (snd o fst o snd) x" end overloading dest_port_datatype \ "dest_port :: ('\::adr,'\) packet \ '\::port" @@ -87,7 +89,7 @@ lemma src_port : "src_port ((a,x,d,e)::(DatatypePort,'\) packet) = snd x" lemma dest_port : "dest_port ((a,d,x,e)::(DatatypePort,'\) packet) = snd x" by (simp add: dest_port_datatype_def in_subnet) - + lemmas DatatypePortLemmas = src_port dest_port src_port_datatype_def dest_port_datatype_def end diff --git a/PacketFilter/IPv4.thy b/PacketFilter/IPv4.thy index 4e9f124..908f7b9 100644 --- a/PacketFilter/IPv4.thy +++ b/PacketFilter/IPv4.thy @@ -38,8 +38,8 @@ subsection {* Formalizing IPv4 Addresses *} theory IPv4 -imports - NetworkCore + imports + NetworkCore begin text{* A theory describing IPv4 addresses with ports. The host address is a four-tuple of Integers, @@ -58,7 +58,7 @@ type_synonym overloading src_port_ipv4 \ "src_port :: ('\::adr,'\) packet \ '\::port" begin definition - "src_port_ipv4 (x::(ipv4,'\) packet) \ (snd o fst o snd) x" + "src_port_ipv4 (x::(ipv4,'\) packet) \ (snd o fst o snd) x" end overloading dest_port_ipv4 \ "dest_port :: ('\::adr,'\) packet \ '\::port" @@ -74,7 +74,7 @@ definition end definition subnet_of_ip :: "ipv4_ip \ ipv4 net" -where "subnet_of_ip ip = {{(a,b). (a = ip)}}" + where "subnet_of_ip ip = {{(a,b). (a = ip)}}" lemma src_port: "src_port (a,(x::ipv4),d,e) = snd x" by (simp add: src_port_ipv4_def in_subnet) diff --git a/PacketFilter/IPv4_TCPUDP.thy b/PacketFilter/IPv4_TCPUDP.thy index 0949002..b0a5ba5 100644 --- a/PacketFilter/IPv4_TCPUDP.thy +++ b/PacketFilter/IPv4_TCPUDP.thy @@ -36,8 +36,9 @@ *****************************************************************************) subsection {* IPv4 with Ports and Protocols *} -theory IPv4_TCPUDP -imports IPv4 +theory + IPv4_TCPUDP + imports IPv4 begin type_synonym @@ -48,7 +49,7 @@ instance protocol :: adr .. overloading src_port_ipv4_TCPUDP \ "src_port :: ('\::adr,'\) packet \ '\::port" begin definition - "src_port_ipv4_TCPUDP (x::(ipv4_TCPUDP,'\) packet) \ (fst o snd o fst o snd) x" + "src_port_ipv4_TCPUDP (x::(ipv4_TCPUDP,'\) packet) \ (fst o snd o fst o snd) x" end overloading dest_port_ipv4_TCPUDP \ "dest_port :: ('\::adr,'\) packet \ '\::port" @@ -70,7 +71,7 @@ definition end definition subnet_of_ip :: "ipv4_ip \ ipv4_TCPUDP net" -where "subnet_of_ip ip = {{(a,b). (a = ip)}}" + where "subnet_of_ip ip = {{(a,b). (a = ip)}}" lemma src_port: "src_port (a,(x::ipv4_TCPUDP),d,e) = fst (snd x)" by (simp add: src_port_ipv4_TCPUDP_def in_subnet) @@ -79,5 +80,5 @@ lemma dest_port: "dest_port (a,d,(x::ipv4_TCPUDP),e) = fst (snd x)" by (simp add: dest_port_ipv4_TCPUDP_def in_subnet) lemmas Ipv4_TCPUDPLemmas = src_port dest_port src_port_ipv4_TCPUDP_def dest_port_ipv4_TCPUDP_def - dest_protocol_ipv4_TCPUDP_def subnet_of_ipv4_TCPUDP_def + dest_protocol_ipv4_TCPUDP_def subnet_of_ipv4_TCPUDP_def end diff --git a/PacketFilter/IntegerAddress.thy b/PacketFilter/IntegerAddress.thy index 95ae2e7..8f2ff6b 100644 --- a/PacketFilter/IntegerAddress.thy +++ b/PacketFilter/IntegerAddress.thy @@ -36,13 +36,15 @@ *****************************************************************************) subsection {* Integer Addresses *} -theory IntegerAddress -imports NetworkCore +theory + IntegerAddress + imports + NetworkCore begin text{* A theory where addresses are modelled as Integers.*} type_synonym - adr\<^sub>i = "int" - + adr\<^sub>i = "int" + end diff --git a/PacketFilter/IntegerPort.thy b/PacketFilter/IntegerPort.thy index c935229..ec0a97e 100644 --- a/PacketFilter/IntegerPort.thy +++ b/PacketFilter/IntegerPort.thy @@ -38,8 +38,8 @@ subsection{* Integer Addresses with Ports *} theory IntegerPort -imports - NetworkCore + imports + NetworkCore begin text{* @@ -59,7 +59,7 @@ type_synonym overloading src_port_int \ "src_port :: ('\::adr,'\) packet \ '\::port" begin definition - "src_port_int (x::(adr\<^sub>i\<^sub>p,'\) packet) \ (snd o fst o snd) x" + "src_port_int (x::(adr\<^sub>i\<^sub>p,'\) packet) \ (snd o fst o snd) x" end overloading dest_port_int \ "dest_port :: ('\::adr,'\) packet \ '\::port" diff --git a/PacketFilter/IntegerPort_TCPUDP.thy b/PacketFilter/IntegerPort_TCPUDP.thy index 5502433..efae0a0 100644 --- a/PacketFilter/IntegerPort_TCPUDP.thy +++ b/PacketFilter/IntegerPort_TCPUDP.thy @@ -38,8 +38,8 @@ subsection {* Integer Addresses with Ports and Protocols *} theory IntegerPort_TCPUDP -imports - NetworkCore + imports + NetworkCore begin text{* A theory describing addresses which are modelled as a pair of Integers - the first being @@ -59,7 +59,7 @@ instance protocol :: adr .. overloading src_port_int_TCPUDP \ "src_port :: ('\::adr,'\) packet \ '\::port" begin definition - "src_port_int_TCPUDP (x::(adr\<^sub>i\<^sub>p\<^sub>p,'\) packet) \ (fst o snd o fst o snd) x" + "src_port_int_TCPUDP (x::(adr\<^sub>i\<^sub>p\<^sub>p,'\) packet) \ (fst o snd o fst o snd) x" end overloading dest_port_int_TCPUDP \ "dest_port :: ('\::adr,'\) packet \ '\::port" @@ -94,18 +94,16 @@ lemma dest_port: "dest_port (a,d,x::adr\<^sub>i\<^sub>p\<^sub>p,e) = fst (snd x) text {* Common test constraints: *} - definition port_positive :: "(adr\<^sub>i\<^sub>p\<^sub>p,'b) packet \ bool" where - "port_positive x = (dest_port x > (0::port))" + "port_positive x = (dest_port x > (0::port))" definition fix_values :: "(adr\<^sub>i\<^sub>p\<^sub>p,DummyContent) packet \ bool" where - "fix_values x = (src_port x = (1::port) \ src_protocol x = udp \ content x = data \ id x = 1)" + "fix_values x = (src_port x = (1::port) \ src_protocol x = udp \ content x = data \ id x = 1)" lemmas adr\<^sub>i\<^sub>p\<^sub>pLemmas = src_port dest_port src_port_int_TCPUDP_def dest_port_int_TCPUDP_def - src_protocol_int_TCPUDP_def dest_protocol_int_TCPUDP_def - subnet_of_int_TCPUDP_def + src_protocol_int_TCPUDP_def dest_protocol_int_TCPUDP_def subnet_of_int_TCPUDP_def lemmas adr\<^sub>i\<^sub>p\<^sub>pTestConstraints = port_positive_def fix_values_def - + end diff --git a/PacketFilter/NetworkCore.thy b/PacketFilter/NetworkCore.thy index e302800..8031497 100644 --- a/PacketFilter/NetworkCore.thy +++ b/PacketFilter/NetworkCore.thy @@ -38,8 +38,8 @@ subsection{* Packets and Networks *} theory NetworkCore -imports - Main + imports + Main begin text{* @@ -94,7 +94,7 @@ text{* *} definition src :: "('\::adr,'\) packet \ '\" -where "src = fst o snd " + where "src = fst o snd " text{* Port numbers (which are part of an address) are also modelled in a generic way. The integers and @@ -116,24 +116,24 @@ text{* To access the different parts of a packet directly, we define a couple of projectors: *} definition id :: "('\::adr,'\) packet \ id" -where "id = fst" + where "id = fst" definition dest :: "('\::adr,'\) packet \ '\ dest" -where "dest = fst o snd o snd" + where "dest = fst o snd o snd" definition content :: "('\::adr,'\) packet \ '\ content" -where "content = snd o snd o snd" + where "content = snd o snd o snd" datatype protocol = tcp | udp lemma either: "\a \ tcp;a \ udp\ \ False" -by (case_tac a,simp_all) + by (case_tac a,simp_all) lemma either2[simp]: "(a \ tcp) = (a = udp)" -by (case_tac a,simp_all) + by (case_tac a,simp_all) lemma either3[simp]: "(a \ udp) = (a = tcp)" -by (case_tac a,simp_all) + by (case_tac a,simp_all) text{* The following two constants give the source and destination port number of a packet. Address @@ -164,7 +164,7 @@ lemma in_subnet: lemma src_in_subnet: "src(q,(a,e),r,t) \ {{(x1,y). P x1 y}} = P a e" - by (simp add: in_subnet_def in_subnet src_def) + by (simp add: in_subnet_def in_subnet src_def) lemma dest_in_subnet: "dest (q,r,((a),e),t) \ {{(x1,y). P x1 y}} = P a e" diff --git a/PacketFilter/NetworkModels.thy b/PacketFilter/NetworkModels.thy index 4ec19ea..cb5b3e9 100644 --- a/PacketFilter/NetworkModels.thy +++ b/PacketFilter/NetworkModels.thy @@ -36,18 +36,18 @@ *****************************************************************************) section{* Network Models *} -theory +theory NetworkModels -imports - DatatypeAddress - DatatypePort + imports + DatatypeAddress + DatatypePort - IntegerAddress - IntegerPort - IntegerPort_TCPUDP + IntegerAddress + IntegerPort + IntegerPort_TCPUDP - IPv4 - IPv4_TCPUDP + IPv4 + IPv4_TCPUDP begin text{* diff --git a/PacketFilter/PacketFilter.thy b/PacketFilter/PacketFilter.thy index 6a272b8..4a7af22 100644 --- a/PacketFilter/PacketFilter.thy +++ b/PacketFilter/PacketFilter.thy @@ -37,9 +37,9 @@ subsection {* Network Policies: Packet Filter *} theory PacketFilter -imports - NetworkModels - ProtocolPortCombinators - Ports + imports + NetworkModels + ProtocolPortCombinators + Ports begin end diff --git a/PacketFilter/PolicyCombinators.thy b/PacketFilter/PolicyCombinators.thy index e68ba39..5691e38 100644 --- a/PacketFilter/PolicyCombinators.thy +++ b/PacketFilter/PolicyCombinators.thy @@ -36,9 +36,10 @@ *****************************************************************************) subsection {* Policy Combinators *} -theory PolicyCombinators -imports -PolicyCore +theory + PolicyCombinators + imports + PolicyCore begin text{* In order to ease the specification of a concrete policy, we @@ -69,8 +70,7 @@ definition definition deny_all_from_to :: "'\::adr net \ '\::adr net \ (('\,'\) packet \ unit)" where - "deny_all_from_to src_net dest_net = - {pa. src pa \ src_net \ dest pa \ dest_net} \ D\<^sub>U" + "deny_all_from_to src_net dest_net = {pa. src pa \ src_net \ dest pa \ dest_net} \ D\<^sub>U" text{* All these combinators and the default rules are put into one @@ -81,6 +81,5 @@ text{* All these combinators and the default rules are put into one lemmas PolicyCombinators = allow_all_from_def deny_all_from_def allow_all_to_def deny_all_to_def allow_all_from_to_def deny_all_from_to_def UPFDefs - - -end + +end \ No newline at end of file diff --git a/PacketFilter/PolicyCore.thy b/PacketFilter/PolicyCore.thy index 7a10078..e1f4fae 100644 --- a/PacketFilter/PolicyCore.thy +++ b/PacketFilter/PolicyCore.thy @@ -38,8 +38,8 @@ subsection {* Policy Core *} theory PolicyCore -imports NetworkCore - "$AFP/UPF/UPF" + imports NetworkCore + "$AFP/UPF/UPF" begin diff --git a/PacketFilter/PortCombinators.thy b/PacketFilter/PortCombinators.thy index 4c59ea2..2f900c0 100644 --- a/PacketFilter/PortCombinators.thy +++ b/PacketFilter/PortCombinators.thy @@ -36,8 +36,10 @@ *****************************************************************************) subsection {* Policy Combinators with Ports *} -theory PortCombinators -imports PolicyCombinators +theory + PortCombinators + imports + PolicyCombinators begin text{* @@ -54,38 +56,34 @@ text{* definition allow_all_from_port :: "'\::adr net \ ('\::port) \ (('\,'\) packet \ unit)" where - "allow_all_from_port src_net s_port = - {pa. src_port pa = s_port} \ allow_all_from src_net" - + "allow_all_from_port src_net s_port = {pa. src_port pa = s_port} \ allow_all_from src_net" + definition deny_all_from_port :: "'\::adr net \ '\::port \ (('\,'\) packet \ unit)" where - "deny_all_from_port src_net s_port = - {pa. src_port pa = s_port} \ deny_all_from src_net " + "deny_all_from_port src_net s_port = {pa. src_port pa = s_port} \ deny_all_from src_net " definition allow_all_to_port :: "'\::adr net \ '\::port \ (('\,'\) packet \ unit)" where - "allow_all_to_port dest_net d_port = - {pa. dest_port pa = d_port} \ allow_all_to dest_net" + "allow_all_to_port dest_net d_port = {pa. dest_port pa = d_port} \ allow_all_to dest_net" definition deny_all_to_port :: "'\::adr net \ '\::port \ (('\,'\) packet \ unit)" where - "deny_all_to_port dest_net d_port = - {pa. dest_port pa = d_port} \ deny_all_to dest_net" + "deny_all_to_port dest_net d_port = {pa. dest_port pa = d_port} \ deny_all_to dest_net" definition -allow_all_from_port_to:: "'\::adr net \ '\::port \ '\::adr net \ (('\,'\) packet \ unit)" -where - "allow_all_from_port_to src_net s_port dest_net + allow_all_from_port_to:: "'\::adr net \ '\::port \ '\::adr net \ (('\,'\) packet \ unit)" + where + "allow_all_from_port_to src_net s_port dest_net = {pa. src_port pa = s_port} \ allow_all_from_to src_net dest_net" definition -deny_all_from_port_to::"'\::adr net \ '\::port \ '\::adr net \ (('\,'\) packet \ unit)" + deny_all_from_port_to::"'\::adr net \ '\::port \ '\::adr net \ (('\,'\) packet \ unit)" where - "deny_all_from_port_to src_net s_port dest_net + "deny_all_from_port_to src_net s_port dest_net = {pa. src_port pa = s_port} \ deny_all_from_to src_net dest_net " definition -allow_all_from_port_to_port::"'\::adr net \ '\::port \ '\::adr net \ '\::port \ + allow_all_from_port_to_port::"'\::adr net \ '\::port \ '\::adr net \ '\::port \ (('\,'\) packet \ unit)" where "allow_all_from_port_to_port src_net s_port dest_net d_port = {pa. dest_port pa = d_port} \ allow_all_from_port_to src_net s_port dest_net" @@ -105,30 +103,31 @@ definition definition deny_all_from_to_port :: "'\::adr net \ '\::adr net \ '\::port \ (('\,'\) packet \ unit)" where - "deny_all_from_to_port src_net dest_net d_port = {pa. dest_port pa = d_port} \ deny_all_from_to src_net dest_net" + "deny_all_from_to_port src_net dest_net d_port = + {pa. dest_port pa = d_port} \ deny_all_from_to src_net dest_net" definition allow_from_port_to :: "'\::port \ '\::adr net \ '\::adr net \ (('\,'\) packet \ unit)" -where - "allow_from_port_to port src_net dest_net = + where + "allow_from_port_to port src_net dest_net = {pa. src_port pa = port} \ allow_all_from_to src_net dest_net" definition deny_from_port_to :: "'\::port \ '\::adr net \ '\::adr net \ (('\,'\) packet \ unit)" -where - "deny_from_port_to port src_net dest_net = + where + "deny_from_port_to port src_net dest_net = {pa. src_port pa = port} \ deny_all_from_to src_net dest_net" definition allow_from_to_port :: "'\::port \ '\::adr net \ '\::adr net \ (('\,'\) packet \ unit)" -where - "allow_from_to_port port src_net dest_net = + where + "allow_from_to_port port src_net dest_net = {pa. dest_port pa = port} \ allow_all_from_to src_net dest_net" definition deny_from_to_port :: "'\::port \ '\::adr net \ '\::adr net \ (('\,'\) packet \ unit)" -where - "deny_from_to_port port src_net dest_net = + where + "deny_from_to_port port src_net dest_net = {pa. dest_port pa = port} \ deny_all_from_to src_net dest_net" definition @@ -137,7 +136,6 @@ definition "allow_from_ports_to ports src_net dest_net = {pa. src_port pa \ ports} \ allow_all_from_to src_net dest_net" - definition allow_from_to_ports :: "'\::port set \ '\::adr net \ '\::adr net \ (('\,'\) packet \ unit)" where @@ -150,17 +148,16 @@ definition "deny_from_ports_to ports src_net dest_net = {pa. src_port pa \ ports} \ deny_all_from_to src_net dest_net" - definition deny_from_to_ports :: "'\::port set \ '\::adr net \ '\::adr net \ (('\,'\) packet \ unit)" where "deny_from_to_ports ports src_net dest_net = {pa. dest_port pa \ ports} \ deny_all_from_to src_net dest_net" - + definition -allow_all_from_port_tos:: "'\::adr net \ ('\::port) set \ '\::adr net \ (('\,'\) packet \ unit)" -where - "allow_all_from_port_tos src_net s_port dest_net + allow_all_from_port_tos:: "'\::adr net \ ('\::port) set \ '\::adr net \ (('\,'\) packet \ unit)" + where + "allow_all_from_port_tos src_net s_port dest_net = {pa. dest_port pa \ s_port} \ allow_all_from_to src_net dest_net" text{* @@ -177,7 +174,6 @@ lemmas PortCombinatorsCore = allow_from_port_to_def allow_from_to_port_def deny_from_to_port_def deny_from_port_to_def allow_all_from_port_tos_def -lemmas PortCombinators = - PortCombinatorsCore PolicyCombinators +lemmas PortCombinators = PortCombinatorsCore PolicyCombinators -end +end \ No newline at end of file diff --git a/PacketFilter/Ports.thy b/PacketFilter/Ports.thy index 0f3bb3a..fa60be2 100644 --- a/PacketFilter/Ports.thy +++ b/PacketFilter/Ports.thy @@ -37,7 +37,8 @@ subsection {* Ports *} theory Ports -imports Main + imports + Main begin text{* @@ -48,28 +49,26 @@ text{* definition http::int where "http = 80" lemma http1: "x \ 80 \ x \ http" -by (simp add: http_def) + by (simp add: http_def) lemma http2: "x \ 80 \ http \ x" -by (simp add: http_def) - + by (simp add: http_def) definition smtp::int where "smtp = 25" lemma smtp1: "x \ 25 \ x \ smtp" -by (simp add: smtp_def) + by (simp add: smtp_def) lemma smtp2: "x \ 25 \ smtp \ x" -by (simp add: smtp_def) - + by (simp add: smtp_def) definition ftp::int where "ftp = 21" lemma ftp1: "x \ 21 \ x \ ftp" -by (simp add: ftp_def) + by (simp add: ftp_def) lemma ftp2: "x \ 21 \ ftp \ x" -by (simp add: ftp_def) + by (simp add: ftp_def) text{* And so on for all desired port numbers. *} diff --git a/PacketFilter/ProtocolPortCombinators.thy b/PacketFilter/ProtocolPortCombinators.thy index d695979..3af0099 100644 --- a/PacketFilter/ProtocolPortCombinators.thy +++ b/PacketFilter/ProtocolPortCombinators.thy @@ -37,8 +37,10 @@ subsection {* Policy Combinators with Ports and Protocols *} -theory ProtocolPortCombinators -imports PortCombinators +theory + ProtocolPortCombinators + imports + PortCombinators begin text{* @@ -74,19 +76,19 @@ definition {pa. dest_protocol pa = p} \ deny_all_to_port dest_net d_port" definition -allow_all_from_port_to_prot:: "protocol =>'\::adr net \ '\::port \ '\::adr net \ (('\,'\) packet \ unit)" -where - "allow_all_from_port_to_prot p src_net s_port dest_net = + allow_all_from_port_to_prot:: "protocol =>'\::adr net \ '\::port \ '\::adr net \ (('\,'\) packet \ unit)" + where + "allow_all_from_port_to_prot p src_net s_port dest_net = {pa. dest_protocol pa = p} \ allow_all_from_port_to src_net s_port dest_net" definition -deny_all_from_port_to_prot::"protocol \ '\::adr net \ '\::port \ '\::adr net \ (('\,'\) packet \ unit)" + deny_all_from_port_to_prot::"protocol \ '\::adr net \ '\::port \ '\::adr net \ (('\,'\) packet \ unit)" where - "deny_all_from_port_to_prot p src_net s_port dest_net = + "deny_all_from_port_to_prot p src_net s_port dest_net = {pa. dest_protocol pa = p} \ deny_all_from_port_to src_net s_port dest_net" definition -allow_all_from_port_to_port_prot::"protocol \ '\::adr net \ '\::port \ '\::adr net \ '\::port \ + allow_all_from_port_to_port_prot::"protocol \ '\::adr net \ '\::port \ '\::adr net \ '\::port \ (('\,'\) packet \ unit)" where "allow_all_from_port_to_port_prot p src_net s_port dest_net d_port = {pa. dest_protocol pa = p} \ allow_all_from_port_to_port src_net s_port dest_net d_port " @@ -111,26 +113,26 @@ definition definition allow_from_port_to_prot :: "protocol =>'\::port \ '\::adr net \ '\::adr net \ (('\,'\) packet \ unit)" -where - "allow_from_port_to_prot p port src_net dest_net = + where + "allow_from_port_to_prot p port src_net dest_net = {pa. dest_protocol pa = p} \ allow_from_port_to port src_net dest_net" definition deny_from_port_to_prot :: "protocol =>'\::port \ '\::adr net \ '\::adr net \ (('\,'\) packet \ unit)" -where - "deny_from_port_to_prot p port src_net dest_net = + where + "deny_from_port_to_prot p port src_net dest_net = {pa. dest_protocol pa = p} \ deny_from_port_to port src_net dest_net" definition allow_from_to_port_prot :: "protocol =>'\::port \ '\::adr net \ '\::adr net \ (('\,'\) packet \ unit)" -where - "allow_from_to_port_prot p port src_net dest_net = + where + "allow_from_to_port_prot p port src_net dest_net = {pa. dest_protocol pa = p} \ allow_from_to_port port src_net dest_net" definition deny_from_to_port_prot :: "protocol =>'\::port \ '\::adr net \ '\::adr net \ (('\,'\) packet \ unit)" -where - "deny_from_to_port_prot p port src_net dest_net = + where + "deny_from_to_port_prot p port src_net dest_net = {pa. dest_protocol pa = p} \ deny_from_to_port port src_net dest_net" definition @@ -139,7 +141,6 @@ definition "allow_from_ports_to_prot p ports src_net dest_net = {pa. dest_protocol pa = p} \ allow_from_ports_to ports src_net dest_net" - definition allow_from_to_ports_prot :: "protocol =>'\::port set \ '\::adr net \ '\::adr net \ (('\,'\) packet \ unit)" where @@ -152,16 +153,13 @@ definition "deny_from_ports_to_prot p ports src_net dest_net = {pa. dest_protocol pa = p} \ deny_from_ports_to ports src_net dest_net" - definition deny_from_to_ports_prot :: "protocol =>'\::port set \ '\::adr net \ '\::adr net \ (('\,'\) packet \ unit)" where "deny_from_to_ports_prot p ports src_net dest_net = {pa. dest_protocol pa = p} \ deny_from_to_ports ports src_net dest_net" - -text{* As before, we put all the rules into one lemma - to ease writing later. *} +text{* As before, we put all the rules into one lemma to ease writing later. *} lemmas ProtocolCombinatorsCore = allow_all_from_port_prot_def deny_all_from_port_prot_def allow_all_to_port_prot_def @@ -173,8 +171,6 @@ lemmas ProtocolCombinatorsCore = allow_from_port_to_prot_def allow_from_to_port_prot_def deny_from_to_port_prot_def deny_from_port_to_prot_def -lemmas ProtocolCombinators = PortCombinators.PortCombinators -ProtocolCombinatorsCore +lemmas ProtocolCombinators = PortCombinators.PortCombinators ProtocolCombinatorsCore - -end +end \ No newline at end of file