# Theory Lib_Enum_toString

section‹Enum toString Functions›
theory Lib_Enum_toString
begin

fun bool_toString :: "bool ⇒ string" where
"bool_toString True = ''True''" |
"bool_toString False = ''False''"

subsection‹Enum set to string›
fun enum_set_get_one :: "'a list ⇒ 'a set ⇒ 'a option" where
"enum_set_get_one []     S = None" |
"enum_set_get_one (s#ss) S = (if s ∈ S then Some s else enum_set_get_one ss S)"

lemma enum_set_get_one_empty: "enum_set_get_one ss {} = None"
by(induction ss) simp_all

lemma enum_set_get_one_None: "S ⊆ set ss ⟹ enum_set_get_one ss S = None ⟷ S = {}"
apply(induction ss)
apply(simp; fail)
apply(simp)
apply(intro conjI)
apply blast
by fast

lemma enum_set_get_one_Some: "S ⊆ set ss ⟹ enum_set_get_one ss S = Some x ⟹ x ∈ S"
apply(induction ss)
apply(simp; fail)
apply(simp split: if_split_asm)
apply(blast)
done
corollary enum_set_get_one_enum_Some: "enum_set_get_one enum_class.enum S = Some x ⟹ x ∈ S"
using enum_set_get_one_Some[where ss=enum_class.enum, simplified enum_UNIV] by auto

lemma enum_set_get_one_Ex_Some: "S ⊆ set ss ⟹ S ≠ {} ⟹ ∃x. enum_set_get_one ss S = Some x"
apply(induction ss)
apply(simp; fail)
apply(simp split: if_split_asm)
apply(blast)
done
corollary enum_set_get_one_enum_Ex_Some:
"S ≠ {} ⟹ ∃x. enum_set_get_one enum_class.enum S = Some x"
using enum_set_get_one_Ex_Some[where ss=enum_class.enum, simplified enum_UNIV] by auto

function enum_set_to_list :: "('a::enum) set ⇒ 'a list" where
"enum_set_to_list S = (if S = {} then [] else
case enum_set_get_one Enum.enum S of None ⇒ []
|  Some a ⇒ a#enum_set_to_list (S - {a}))"
by(pat_completeness) auto

termination enum_set_to_list
apply(relation "measure (λ(S). card S)")
apply(drule enum_set_get_one_enum_Some)
apply(subgoal_tac "finite S")
prefer 2
apply force
apply (meson card_Diff1_less)
done

(*this definition is simpler*)
lemma enum_set_to_list_simps: "enum_set_to_list S =
(case enum_set_get_one (Enum.enum) S of None ⇒ []
|  Some a ⇒ a#enum_set_to_list (S - {a}))"
declare enum_set_to_list.simps[simp del]

lemma enum_set_to_list: "set (enum_set_to_list A) = A"
apply(induction A rule: enum_set_to_list.induct)
apply(case_tac "S = {}")
apply(simp)
apply(subst enum_set_to_list_simps)
apply(simp)
apply(drule enum_set_get_one_enum_Ex_Some)
apply(clarify)
apply(simp)
apply(drule enum_set_get_one_enum_Some)
by blast

lemma "list_toString bool_toString (enum_set_to_list {True, False}) = ''[False, True]''" by eval

end


# Theory L4_Protocol

theory L4_Protocol
imports "../Common/Lib_Enum_toString" "HOL-Library.Word"
begin

section‹Transport Layer Protocols›
type_synonym primitive_protocol = "8 word"

definition "ICMP ≡ 1 :: 8 word"
definition "TCP ≡ 6 :: 8 word"
definition "UDP ≡ 17 :: 8 word"
context begin (*let's not pollute the namespace too much*)
qualified definition "SCTP ≡ 132  :: 8 word"
qualified definition "IGMP ≡ 2 :: 8 word"
qualified definition "GRE ≡ 47 :: 8 word"
qualified definition "ESP ≡ 50 :: 8 word"
qualified definition "AH ≡ 51 :: 8 word"
qualified definition "IPv6ICMP ≡ 58 :: 8 word"
end
(* turn http://www.iana.org/assignments/protocol-numbers/protocol-numbers.xhtml into a separate file or so? *)

datatype protocol = ProtoAny | Proto "primitive_protocol"

fun match_proto :: "protocol ⇒ primitive_protocol ⇒ bool" where
"match_proto ProtoAny _ ⟷ True" |
"match_proto (Proto (p)) p_p ⟷ p_p = p"

fun simple_proto_conjunct :: "protocol ⇒ protocol ⇒ protocol option" where
"simple_proto_conjunct ProtoAny proto = Some proto" |
"simple_proto_conjunct proto ProtoAny = Some proto" |
"simple_proto_conjunct (Proto p1) (Proto p2) = (if p1 = p2 then Some (Proto p1) else None)"
lemma simple_proto_conjunct_asimp[simp]: "simple_proto_conjunct proto ProtoAny = Some proto"
by(cases proto) simp_all

lemma simple_proto_conjunct_correct: "match_proto p1 pkt ∧ match_proto p2 pkt ⟷
(case simple_proto_conjunct p1 p2 of None ⇒ False | Some proto ⇒ match_proto proto pkt)"
apply(cases p1)
apply(simp_all)
apply(cases p2)
apply(simp_all)
done

lemma simple_proto_conjunct_Some: "simple_proto_conjunct p1 p2 = Some proto ⟹
match_proto proto pkt ⟷ match_proto p1 pkt ∧ match_proto p2 pkt"
using simple_proto_conjunct_correct by simp
lemma simple_proto_conjunct_None: "simple_proto_conjunct p1 p2 = None ⟹
¬ (match_proto p1 pkt ∧ match_proto p2 pkt)"
using simple_proto_conjunct_correct by simp

lemma conjunctProtoD:
"simple_proto_conjunct a (Proto b) = Some x ⟹ x = Proto b ∧ (a = ProtoAny ∨ a = Proto b)"
by(cases a) (simp_all split: if_splits)
lemma conjunctProtoD2:
"simple_proto_conjunct (Proto b) a = Some x ⟹ x = Proto b ∧ (a = ProtoAny ∨ a = Proto b)"
by(cases a) (simp_all split: if_splits)

text‹Originally, there was a @{typ nat} in the protocol definition, allowing infinitely many protocols
This was intended behavior. We want to prevent things such as @{term "¬TCP = UDP"}.
So be careful with what you prove...›
lemma primitive_protocol_Ex_neq: "p = Proto pi ⟹ ∃p'. p' ≠ pi" for pi
proof
show "pi + 1 ≠ pi" by simp
qed
lemma protocol_Ex_neq: "∃p'. Proto p' ≠ p"

section‹TCP flags›
datatype tcp_flag = TCP_SYN | TCP_ACK | TCP_FIN | TCP_RST | TCP_URG | TCP_PSH (*| TCP_ALL | TCP_NONE*)

lemma UNIV_tcp_flag: "UNIV = {TCP_SYN, TCP_ACK, TCP_FIN, TCP_RST, TCP_URG, TCP_PSH}" using tcp_flag.exhaust by auto
instance tcp_flag :: finite
proof
from UNIV_tcp_flag show "finite (UNIV:: tcp_flag set)" using finite.simps by auto
qed
instantiation "tcp_flag" :: enum
begin
definition "enum_tcp_flag = [TCP_SYN, TCP_ACK, TCP_FIN, TCP_RST, TCP_URG, TCP_PSH]"

definition "enum_all_tcp_flag P ⟷ P TCP_SYN ∧ P TCP_ACK ∧ P TCP_FIN ∧ P TCP_RST ∧ P TCP_URG ∧ P TCP_PSH"

definition "enum_ex_tcp_flag P ⟷ P TCP_SYN ∨ P TCP_ACK ∨ P TCP_FIN ∨ P TCP_RST ∨ P TCP_URG ∨ P TCP_PSH"
instance proof
show "UNIV = set (enum_class.enum :: tcp_flag list)"
next
show "distinct (enum_class.enum :: tcp_flag list)"
next
show "⋀P. (enum_class.enum_all :: (tcp_flag ⇒ bool) ⇒ bool) P = Ball UNIV P"
next
show "⋀P. (enum_class.enum_ex :: (tcp_flag ⇒ bool) ⇒ bool) P = Bex UNIV P"
qed
end

subsection‹TCP Flags to String›
fun tcp_flag_toString :: "tcp_flag ⇒ string" where
"tcp_flag_toString TCP_SYN = ''TCP_SYN''" |
"tcp_flag_toString TCP_ACK = ''TCP_ACK''" |
"tcp_flag_toString TCP_FIN = ''TCP_FIN''" |
"tcp_flag_toString TCP_RST = ''TCP_RST''" |
"tcp_flag_toString TCP_URG = ''TCP_URG''" |
"tcp_flag_toString TCP_PSH = ''TCP_PSH''"

definition ipt_tcp_flags_toString :: "tcp_flag set ⇒ char list" where
"ipt_tcp_flags_toString flags ≡ list_toString tcp_flag_toString (enum_set_to_list flags)"

lemma "ipt_tcp_flags_toString {TCP_SYN,TCP_SYN,TCP_ACK} = ''[TCP_SYN, TCP_ACK]''" by eval

end


# Theory Simple_Packet

section‹Simple Packet›
theory Simple_Packet
imports "Primitives/L4_Protocol"
begin

text‹Packet constants are prefixed with ‹p››

text‹@{typ "'i::len word"} is an IP address of variable length. 32bit for IPv4, 128bit for IPv6›

text‹A simple packet with IP addresses and layer four ports.
Also has the following phantom fields:
Input and Output network interfaces›

record (overloaded) 'i simple_packet = p_iiface :: string
p_oiface :: string
p_src :: "'i::len word"
p_dst :: "'i::len word"
p_proto :: primitive_protocol
p_sport :: "16 word"
p_dport :: "16 word"
p_tcp_flags :: "tcp_flag set"

value [nbe] "⦇
p_iiface = ''eth1'', p_oiface = '''',
p_src = 0, p_dst = 0,
p_proto = TCP, p_sport = 0, p_dport = 0,
p_tcp_flags = {TCP_SYN},
⦈"

text‹We suggest to use @{typ "('i,'pkt_ext) simple_packet_scheme"} instead of
@{typ "'i simple_packet"} because of its extensibility which naturally

definition simple_packet_unext :: "('i::len, 'a) simple_packet_scheme ⇒ 'i simple_packet" where
"simple_packet_unext p ≡
⦇p_iiface = p_iiface p, p_oiface = p_oiface p, p_src = p_src p, p_dst = p_dst p, p_proto = p_proto p,
p_sport = p_sport p, p_dport = p_dport p, p_tcp_flags = p_tcp_flags p,

record (overloaded) 'i simple_packet_ext = "'i::len simple_packet" +
p_l2type :: "16 word"
p_l2src :: "48 word"
p_l2dst :: "48 word"
p_vlanid :: "16 word"
p_vlanprio :: "16 word"

end


# Theory Firewall_Common_Decision_State

section‹The state of a firewall, abstracted only to the packet filtering outcome›
theory Firewall_Common_Decision_State
imports Main
begin

datatype final_decision = FinalAllow | FinalDeny

text‹
The state during packet processing. If undecided, there are some remaining rules to process. If
decided, there is an action which applies to the packet
›
datatype state = Undecided | Decision final_decision

end


# Theory Iface

section‹Network Interfaces›
theory Iface
imports "HOL-Library.Char_ord" (*WARNING: importing char ord*)
begin

text‹Network interfaces, e.g. \texttt{eth0}, \texttt{wlan1}, ...

iptables supports wildcard matching, e.g. \texttt{eth+} will match \texttt{eth}, \texttt{eth1}, \texttt{ethFOO}, ...
The character +' is only a wildcard if it appears at the end.
›

datatype iface = Iface (iface_sel: "string")  ― ‹no negation supported, but wildcards›

text‹Just a normal lexicographical ordering on the interface strings. Used only for optimizing code.
WARNING: not a semantic ordering.›
(*We cannot use List_lexord because it clashed with the Word_Lib imported ordering!*)
instantiation iface :: linorder
begin
function (sequential) less_eq_iface :: "iface ⇒ iface ⇒ bool" where
"(Iface []) ≤ (Iface _) ⟷ True" |
"(Iface _) ≤ (Iface []) ⟷ False" |
"(Iface (a#as)) ≤ (Iface (b#bs)) ⟷ (if a = b then Iface as ≤ Iface bs else a ≤ b)"
by(pat_completeness) auto
termination "less_eq :: iface ⇒ _ ⇒ bool"
apply(relation "measure (λis. size (iface_sel (fst is)) + size (iface_sel (snd is)))")
apply(rule wf_measure, unfold in_measure comp_def)
apply(simp)
done

lemma Iface_less_eq_empty: "Iface x ≤ Iface [] ⟹ x = []"
by(induction "Iface x" "Iface []" rule: less_eq_iface.induct) auto
lemma less_eq_empty: "Iface [] ≤ q"
by(induction "Iface []" q rule: less_eq_iface.induct) auto
lemma iface_cons_less_eq_i:
"Iface (b # bs) ≤ i ⟹ ∃ q qs. i=Iface (q#qs) ∧ (b < q ∨ (Iface bs) ≤ (Iface qs))"
apply(induction "Iface (b # bs)" i rule: less_eq_iface.induct)
apply(simp_all split: if_split_asm)
apply(clarify)
apply(simp)
done

function (sequential) less_iface :: "iface ⇒ iface ⇒ bool" where
"(Iface []) < (Iface []) ⟷ False" |
"(Iface []) < (Iface _) ⟷ True" |
"(Iface _) < (Iface []) ⟷ False" |
"(Iface (a#as)) < (Iface (b#bs)) ⟷ (if a = b then Iface as < Iface bs else a < b)"
by(pat_completeness) auto
termination "less :: iface ⇒ _ ⇒ bool"
apply(relation "measure (λis. size (iface_sel (fst is)) + size (iface_sel (snd is)))")
apply(rule wf_measure, unfold in_measure comp_def)
apply(simp)
done
instance
proof
fix n m :: iface
show "n < m ⟷ n ≤ m ∧ ¬ m ≤ n"
proof(induction rule: less_iface.induct)
case 4 thus ?case by simp fastforce
qed(simp+)
next
fix n :: iface have "n = m ⟹ n ≤ m" for m
by(induction n m rule: less_eq_iface.induct) simp+
thus "n ≤ n" by simp
next
fix n m :: iface
show "n ≤ m ⟹ m ≤ n ⟹ n = m"
proof(induction n m rule: less_eq_iface.induct)
case 1 thus ?case using Iface_less_eq_empty by blast
next
case 3 thus ?case by (simp split: if_split_asm)
qed(simp)+
next
fix n m q :: iface show "n ≤ m ⟹ m ≤ q ⟹ n ≤ q"
proof(induction n q arbitrary: m rule: less_eq_iface.induct)
case 1 thus ?case by simp
next
case 2 thus ?case
apply simp
apply(drule iface_cons_less_eq_i)
apply(elim exE conjE disjE)
apply(simp; fail)
by fastforce
next
case 3 thus ?case
apply simp
apply(frule iface_cons_less_eq_i)
by(auto split: if_split_asm)
qed
next
fix n m :: iface show "n ≤ m ∨ m ≤ n"
apply(induction n m rule: less_eq_iface.induct)
apply(simp_all)
by fastforce
qed
end

definition ifaceAny :: iface where
"ifaceAny ≡ Iface ''+''"
(* there is no IfaceFalse, proof below *)

text‹If the interface name ends in a +'', then any interface which begins with this name will match.
(man iptables)

Here is how iptables handles this wildcard on my system.
A packet for the loopback interface \texttt{lo} is matched by the following expressions
▪ lo
▪ lo+
▪ l+
▪ +

It is not matched by the following expressions
▪ lo++
▪ lo+++
▪ lo1+
▪ lo1

By the way: \texttt{Warning: weird characters in interface  ' ('/' and ' ' are not allowed by the kernel).}
However, happy snowman and shell colors are fine.
›

context
begin
subsection‹Helpers for the interface name (@{typ string})›
(*Do not use outside this thy! Type is really misleading.*)
text‹
argument 1: interface as in firewall rule - Wildcard support
argument 2: interface a packet came from - No wildcard support›
fun internal_iface_name_match :: "string ⇒ string ⇒ bool" where
"internal_iface_name_match []     []         ⟷ True" |
"internal_iface_name_match (i#is) []         ⟷ (i = CHR ''+'' ∧ is = [])" |
"internal_iface_name_match []     (_#_)      ⟷ False" |
"internal_iface_name_match (i#is) (p_i#p_is) ⟷ (if (i = CHR ''+'' ∧ is = []) then True else (
(p_i = i) ∧ internal_iface_name_match is p_is
))"

(*<*)
― ‹Examples›
lemma "internal_iface_name_match ''lo'' ''lo''" by eval
lemma "internal_iface_name_match ''lo+'' ''lo''" by eval
lemma "internal_iface_name_match ''l+'' ''lo''" by eval
lemma "internal_iface_name_match ''+'' ''lo''" by eval
lemma "¬ internal_iface_name_match ''lo++'' ''lo''" by eval
lemma "¬ internal_iface_name_match ''lo+++'' ''lo''" by eval
lemma "¬ internal_iface_name_match ''lo1+'' ''lo''" by eval
lemma "¬ internal_iface_name_match ''lo1'' ''lo''" by eval
text‹The wildcard interface name›
lemma "internal_iface_name_match ''+'' ''''" by eval (*>*)

fun iface_name_is_wildcard :: "string ⇒ bool" where
"iface_name_is_wildcard [] ⟷ False" |
"iface_name_is_wildcard [s] ⟷ s = CHR ''+''" |
"iface_name_is_wildcard (_#ss) ⟷ iface_name_is_wildcard ss"
private lemma iface_name_is_wildcard_alt: "iface_name_is_wildcard eth ⟷ eth ≠ [] ∧ last eth = CHR ''+''"
proof(induction eth rule: iface_name_is_wildcard.induct)
qed(simp_all)
private lemma iface_name_is_wildcard_alt': "iface_name_is_wildcard eth ⟷ eth ≠ [] ∧ hd (rev eth) = CHR ''+''"
unfolding iface_name_is_wildcard_alt by (simp add: hd_rev)
private lemma iface_name_is_wildcard_fst: "iface_name_is_wildcard (i # is) ⟹ is ≠ [] ⟹ iface_name_is_wildcard is"

private fun internal_iface_name_to_set :: "string ⇒ string set" where
"internal_iface_name_to_set i = (if ¬ iface_name_is_wildcard i
then
{i}
else
{(butlast i)@cs | cs. True})"
private lemma "{(butlast i)@cs | cs. True} = (λs. (butlast i)@s)  (UNIV::string set)" by fastforce
private lemma internal_iface_name_to_set: "internal_iface_name_match i p_iface ⟷ p_iface ∈ internal_iface_name_to_set i"
proof(induction i p_iface rule: internal_iface_name_match.induct)
case 4 thus ?case
apply(simp)
apply(safe)
apply (metis (full_types) iface_name_is_wildcard.simps(3) list.exhaust)
by (metis append_butlast_last_id)
qed(simp_all)
private lemma internal_iface_name_to_set2: "internal_iface_name_to_set ifce = {i. internal_iface_name_match ifce i}"

private lemma internal_iface_name_match_refl: "internal_iface_name_match i i"
proof -
{ fix i j
have "i=j ⟹ internal_iface_name_match i j"
by(induction i j rule: internal_iface_name_match.induct)(simp_all)
} thus ?thesis by simp
qed

subsection‹Matching›
fun match_iface :: "iface ⇒ string ⇒ bool" where
"match_iface (Iface i) p_iface ⟷ internal_iface_name_match i p_iface"

― ‹Examples›
lemma "  match_iface (Iface ''lo'')    ''lo''"
"  match_iface (Iface ''lo+'')   ''lo''"
"  match_iface (Iface ''l+'')    ''lo''"
"  match_iface (Iface ''+'')     ''lo''"
"¬ match_iface (Iface ''lo++'')  ''lo''"
"¬ match_iface (Iface ''lo+++'') ''lo''"
"¬ match_iface (Iface ''lo1+'')  ''lo''"
"¬ match_iface (Iface ''lo1'')   ''lo''"
"  match_iface (Iface ''+'')     ''eth0''"
"  match_iface (Iface ''+'')     ''eth0''"
"  match_iface (Iface ''eth+'')  ''eth0''"
"¬ match_iface (Iface ''lo+'')   ''eth0''"
"  match_iface (Iface ''lo+'')   ''loX''"
"¬ match_iface (Iface '''')      ''loX''"
(*<*)by eval+(*>*)

lemma match_ifaceAny: "match_iface ifaceAny i"
lemma match_IfaceFalse: "¬(∃ IfaceFalse. (∀i. ¬ match_iface IfaceFalse i))"
apply(simp)
apply(intro allI, rename_tac IfaceFalse)
apply(case_tac IfaceFalse, rename_tac name)
apply(rule_tac x="name" in exI)

― ‹@{const match_iface} explained by the individual cases›
lemma match_iface_case_nowildcard: "¬ iface_name_is_wildcard i ⟹ match_iface (Iface i) p_i ⟷ i = p_i"
proof(induction i p_i rule: internal_iface_name_match.induct)
qed(auto simp add: iface_name_is_wildcard_alt split: if_split_asm)
lemma match_iface_case_wildcard_prefix:
"iface_name_is_wildcard i ⟹ match_iface (Iface i) p_i ⟷ butlast i = take (length i - 1) p_i"
apply(induction i p_i rule: internal_iface_name_match.induct)
apply(simp; fail)
apply(simp add: iface_name_is_wildcard_alt split: if_split_asm; fail)
apply(simp; fail)
apply(simp)
apply(intro conjI)
apply(simp add: iface_name_is_wildcard_alt split: if_split_asm; fail)
by (metis One_nat_def length_0_conv list.sel(1) list.sel(3) take_Cons')
lemma match_iface_case_wildcard_length: "iface_name_is_wildcard i ⟹ match_iface (Iface i) p_i ⟹ length p_i ≥ (length i - 1)"
proof(induction i p_i rule: internal_iface_name_match.induct)
corollary match_iface_case_wildcard:
"iface_name_is_wildcard i ⟹ match_iface (Iface i) p_i ⟷ butlast i = take (length i - 1) p_i ∧ length p_i ≥ (length i - 1)"
using match_iface_case_wildcard_length match_iface_case_wildcard_prefix by blast

lemma match_iface_set: "match_iface (Iface i) p_iface ⟷ p_iface ∈ internal_iface_name_to_set i"
using internal_iface_name_to_set by simp

private definition internal_iface_name_wildcard_longest :: "string ⇒ string ⇒ string option" where
"internal_iface_name_wildcard_longest i1 i2 = (
if
take (min (length i1 - 1) (length i2 - 1)) i1 = take (min (length i1 - 1) (length i2 - 1)) i2
then
Some (if length i1 ≤ length i2 then i2 else i1)
else
None)"
private lemma "internal_iface_name_wildcard_longest ''eth+'' ''eth3+'' = Some ''eth3+''" by eval
private lemma "internal_iface_name_wildcard_longest ''eth+'' ''e+'' = Some ''eth+''" by eval
private lemma "internal_iface_name_wildcard_longest ''eth+'' ''lo'' = None" by eval

private  lemma internal_iface_name_wildcard_longest_commute: "iface_name_is_wildcard i1 ⟹ iface_name_is_wildcard i2 ⟹
internal_iface_name_wildcard_longest i1 i2 = internal_iface_name_wildcard_longest i2 i1"
apply(safe)
apply (metis One_nat_def append_butlast_last_id butlast_conv_take)
by (metis min.commute)+
private  lemma internal_iface_name_wildcard_longest_refl: "internal_iface_name_wildcard_longest i i = Some i"

private lemma internal_iface_name_wildcard_longest_correct:
"iface_name_is_wildcard i1 ⟹ iface_name_is_wildcard i2 ⟹
match_iface (Iface i1) p_i ∧ match_iface (Iface i2) p_i ⟷
(case internal_iface_name_wildcard_longest i1 i2 of None ⇒ False | Some x ⇒ match_iface (Iface x) p_i)"
proof -
assume assm1: "iface_name_is_wildcard i1"
and assm2: "iface_name_is_wildcard i2"
{ assume assm3: "internal_iface_name_wildcard_longest i1 i2 = None"
have "¬ (internal_iface_name_match i1 p_i ∧ internal_iface_name_match i2 p_i)"
proof -
from match_iface_case_wildcard_prefix[OF assm1] have 1:
"internal_iface_name_match i1 p_i = (take (length i1 - 1) i1 = take (length i1 - 1) p_i)" by(simp add: butlast_conv_take)
from match_iface_case_wildcard_prefix[OF assm2] have 2:
"internal_iface_name_match i2 p_i = (take (length i2 - 1) i2 = take (length i2 - 1) p_i)" by(simp add: butlast_conv_take)
from assm3 have 3: "take (min (length i1 - 1) (length i2 - 1)) i1 ≠ take (min (length i1 - 1) (length i2 - 1)) i2"
from 3 show ?thesis using 1 2 min.commute take_take by metis
qed
} note internal_iface_name_wildcard_longest_correct_None=this

{ fix X
assume assm3: "internal_iface_name_wildcard_longest i1 i2 = Some X"
have "(internal_iface_name_match i1 p_i ∧ internal_iface_name_match i2 p_i) ⟷ internal_iface_name_match X p_i"
proof -
from assm3 have assm3': "take (min (length i1 - 1) (length i2 - 1)) i1 = take (min (length i1 - 1) (length i2 - 1)) i2"
unfolding internal_iface_name_wildcard_longest_def by(simp split: if_split_asm)

{ fix i1 i2
assume iw1: "iface_name_is_wildcard i1" and iw2: "iface_name_is_wildcard i2" and len: "length i1 ≤ length i2" and
take_i1i2: "take (length i1 - 1) i1 = take (length i1 - 1) i2"
from len have len': "length i1 - 1 ≤ length i2 - 1" by fastforce
{ fix x::string
from len' have "take (length i1 - 1) x = take (length i1 - 1) (take (length i2 - 1) x)" by(simp add: min_def)
} note takei1=this

{ fix m::nat and n::nat and a::string and b c
have "m ≤ n ⟹ take n a = take n b ⟹ take m a = take m c ⟹ take m c = take m b" by (metis min_absorb1 take_take)
} note takesmaller=this

from match_iface_case_wildcard_prefix[OF iw1, simplified] have 1:
"internal_iface_name_match i1 p_i ⟷ take (length i1 - 1) i1 = take (length i1 - 1) p_i" by(simp add: butlast_conv_take)
also have "… ⟷ take (length i1 - 1) (take (length i2 - 1) i1) = take (length i1 - 1) (take (length i2 - 1) p_i)" using takei1 by simp
finally have  "internal_iface_name_match i1 p_i = (take (length i1 - 1) (take (length i2 - 1) i1) = take (length i1 - 1) (take (length i2 - 1) p_i))" .
from match_iface_case_wildcard_prefix[OF iw2, simplified] have 2:
"internal_iface_name_match i2 p_i ⟷ take (length i2 - 1) i2 = take (length i2 - 1) p_i" by(simp add: butlast_conv_take)

have "internal_iface_name_match i2 p_i ⟹ internal_iface_name_match i1 p_i"
unfolding 1 2
apply(rule takesmaller[of "(length i1 - 1)" "(length i2 - 1)" i2 p_i])
using len' apply (simp; fail)
apply (simp; fail)
using take_i1i2 by simp
} note longer_iface_imp_shorter=this

show ?thesis
proof(cases "length i1 ≤ length i2")
case True
with assm3 have "X = i2" unfolding internal_iface_name_wildcard_longest_def by(simp split: if_split_asm)
from True assm3' have take_i1i2: "take (length i1 - 1) i1 = take (length i1 - 1) i2" by linarith
from longer_iface_imp_shorter[OF assm1 assm2 True take_i1i2] ‹X = i2›
show "(internal_iface_name_match i1 p_i ∧ internal_iface_name_match i2 p_i) ⟷ internal_iface_name_match X p_i" by fastforce
next
case False
with assm3 have "X = i1" unfolding internal_iface_name_wildcard_longest_def by(simp split: if_split_asm)
from False assm3' have take_i1i2: "take (length i2 - 1) i2 = take (length i2 - 1) i1" by (metis min_def min_diff)
from longer_iface_imp_shorter[OF assm2 assm1 _ take_i1i2] False ‹X = i1›
show "(internal_iface_name_match i1 p_i ∧ internal_iface_name_match i2 p_i) ⟷ internal_iface_name_match X p_i" by auto
qed
qed
} note internal_iface_name_wildcard_longest_correct_Some=this

from internal_iface_name_wildcard_longest_correct_None internal_iface_name_wildcard_longest_correct_Some show ?thesis
by(simp split:option.split)
qed

fun iface_conjunct :: "iface ⇒ iface ⇒ iface option" where
"iface_conjunct (Iface i1) (Iface i2) = (case (iface_name_is_wildcard i1, iface_name_is_wildcard i2) of
(True,  True) ⇒ map_option Iface  (internal_iface_name_wildcard_longest i1 i2) |
(True,  False) ⇒ (if match_iface (Iface i1) i2 then Some (Iface i2) else None) |
(False, True) ⇒ (if match_iface (Iface i2) i1 then Some (Iface i1) else None) |
(False, False) ⇒ (if i1 = i2 then Some (Iface i1) else None))"

lemma iface_conjunct_Some: "iface_conjunct i1 i2 = Some x ⟹
match_iface x p_i ⟷ match_iface i1 p_i ∧ match_iface i2 p_i"
apply(cases i1, cases i2, rename_tac i1name i2name)
apply(simp)
apply(case_tac "iface_name_is_wildcard i1name")
apply(case_tac [!] "iface_name_is_wildcard i2name")
apply(simp_all)
using internal_iface_name_wildcard_longest_correct apply auto[1]
apply (metis match_iface.simps match_iface_case_nowildcard option.distinct(1) option.sel)
apply (metis match_iface.simps match_iface_case_nowildcard option.distinct(1) option.sel)
by (metis match_iface.simps option.distinct(1) option.inject)
lemma iface_conjunct_None: "iface_conjunct i1 i2 = None ⟹ ¬ (match_iface i1 p_i ∧ match_iface i2 p_i)"
apply(cases i1, cases i2, rename_tac i1name i2name)
apply(simp split: bool.split_asm if_split_asm)
using internal_iface_name_wildcard_longest_correct apply fastforce
apply (metis match_iface.simps match_iface_case_nowildcard)+
done
lemma iface_conjunct: "match_iface i1 p_i ∧ match_iface i2 p_i ⟷
(case iface_conjunct i1 i2 of None ⇒ False | Some x ⇒ match_iface x p_i)"
apply(simp split: option.split)
by(blast dest: iface_conjunct_Some iface_conjunct_None)

lemma match_iface_refl: "match_iface (Iface x) x" by (simp add: internal_iface_name_match_refl)
lemma match_iface_eqI: assumes "x = Iface y" shows "match_iface x y"
unfolding assms using match_iface_refl .

lemma iface_conjunct_ifaceAny: "iface_conjunct ifaceAny i = Some i"
apply(case_tac i, rename_tac iname)
apply(simp)
apply(case_tac "iface_name_is_wildcard iname")
apply(simp add: internal_iface_name_wildcard_longest_def iface_name_is_wildcard_alt Suc_leI; fail)
apply(simp)
using internal_iface_name_match.elims(3) by fastforce

lemma iface_conjunct_commute: "iface_conjunct i1 i2 = iface_conjunct i2 i1"
apply(induction i1 i2 rule: iface_conjunct.induct)
apply(rename_tac i1 i2, simp)
apply(case_tac "iface_name_is_wildcard i1")
apply(case_tac [!] "iface_name_is_wildcard i2")
apply(simp_all)

private definition internal_iface_name_subset :: "string ⇒ string ⇒ bool" where
"internal_iface_name_subset i1 i2 = (case (iface_name_is_wildcard i1, iface_name_is_wildcard i2) of
(True,  True) ⇒ length i1 ≥ length i2 ∧ take ((length i2) - 1) i1 = butlast i2 |
(True,  False) ⇒ False |
(False, True) ⇒ take (length i2 - 1) i1 = butlast i2 |
(False, False) ⇒ i1 = i2
)"

private lemma butlast_take_length_helper:
fixes x ::"char list"
assumes a1: "length i2 ≤ length i1"
assumes a2: "take (length i2 - Suc 0) i1 = butlast i2"
assumes a3: "butlast i1 = take (length i1 - Suc 0) x"
shows "butlast i2 = take (length i2 - Suc 0) x"
proof - (*sledgehammer spass Isar proof*)
have f4: "List.gen_length 0 i2 ≤ List.gen_length 0 i1"
using a1 by (simp add: length_code)
have f5: "⋀cs. List.gen_length 0 (cs::char list) - Suc 0 = List.gen_length 0 (tl cs)"
by (metis (no_types) One_nat_def length_code length_tl)
obtain nn :: "(nat ⇒ nat) ⇒ nat" where
"⋀f. ¬ f (nn f) ≤ f (Suc (nn f)) ∨ f (List.gen_length 0 i2) ≤ f (List.gen_length 0 i1)"
using f4 by (meson lift_Suc_mono_le)
hence "¬ nn (λn. n - Suc 0) - Suc 0 ≤ nn (λn. n - Suc 0) ∨ List.gen_length 0 (tl i2) ≤ List.gen_length 0 (tl i1)"
using f5 by (metis (lifting) diff_Suc_Suc diff_zero)
hence f6: "min (List.gen_length 0 (tl i2)) (List.gen_length 0 (tl i1)) = List.gen_length 0 (tl i2)"
using diff_le_self min.absorb1 by blast
{ assume "take (List.gen_length 0 (tl i2)) i1 ≠ take (List.gen_length 0 (tl i2)) x"
have "List.gen_length 0 (tl i2) = 0 ∨ take (List.gen_length 0 (tl i2)) i1 = take (List.gen_length 0 (tl i2)) x"
using f6 f5 a3 by (metis (lifting) One_nat_def butlast_conv_take length_code take_take)
hence "take (List.gen_length 0 (tl i2)) i1 = take (List.gen_length 0 (tl i2)) x"
by force }
thus "butlast i2 = take (length i2 - Suc 0) x"
using f5 a2 by (metis (full_types) length_code)
qed

private lemma internal_iface_name_subset: "internal_iface_name_subset i1 i2 ⟷
{i. internal_iface_name_match i1 i} ⊆ {i. internal_iface_name_match i2 i}"
unfolding internal_iface_name_subset_def
proof(cases "iface_name_is_wildcard i1", case_tac [!] "iface_name_is_wildcard i2", simp_all)
assume a1: "iface_name_is_wildcard i1"
assume a2: "iface_name_is_wildcard i2"
show "(length i2 ≤ length i1 ∧ take (length i2 - Suc 0) i1 = butlast i2) ⟷
({i. internal_iface_name_match i1 i} ⊆ {i. internal_iface_name_match i2 i})" (is "?l ⟷ ?r")
proof(rule iffI)
assume ?l with a1 a2 show ?r
apply(clarify, rename_tac x)
apply(drule_tac p_i=x in match_iface_case_wildcard_prefix)+
apply(simp)
using butlast_take_length_helper by blast
next
assume ?r hence r': "internal_iface_name_to_set i1 ⊆ internal_iface_name_to_set i2 "
apply -
apply(subst(asm) internal_iface_name_to_set2[symmetric])+
by assumption
have hlp1: "⋀i1 i2. {x. ∃cs. x = i1 @ cs} ⊆ {x. ∃cs. x = i2 @ cs} ⟹ length i2 ≤ length i1"
by force
have hlp2: "⋀i1 i2. {x. ∃cs. x = i1 @ cs} ⊆ {x. ∃cs. x = i2 @ cs} ⟹ take (length i2) i1 = i2"
by force
from r' a1 a2 show ?l
apply(safe)
apply(drule hlp1)
apply(simp)
apply (metis One_nat_def Suc_pred diff_Suc_eq_diff_pred diff_is_0_eq iface_name_is_wildcard.simps(1) length_greater_0_conv)
apply(drule hlp2)
apply(simp)
by (metis One_nat_def butlast_conv_take length_butlast length_take take_take)
qed
next
show "iface_name_is_wildcard i1 ⟹ ¬ iface_name_is_wildcard i2 ⟹
¬ Collect (internal_iface_name_match i1) ⊆ Collect (internal_iface_name_match i2)"
using internal_iface_name_match_refl match_iface_case_nowildcard by fastforce
next
show "¬ iface_name_is_wildcard i1 ⟹ iface_name_is_wildcard i2 ⟹
(take (length i2 - Suc 0) i1 = butlast i2) ⟷ ({i. internal_iface_name_match i1 i} ⊆ {i. internal_iface_name_match i2 i})"
using match_iface_case_nowildcard match_iface_case_wildcard_prefix by force
next
show " ¬ iface_name_is_wildcard i1 ⟹ ¬ iface_name_is_wildcard i2 ⟹
(i1 = i2) ⟷ ({i. internal_iface_name_match i1 i} ⊆ {i. internal_iface_name_match i2 i})"
using match_iface_case_nowildcard  by force
qed

definition iface_subset :: "iface ⇒ iface ⇒ bool" where
"iface_subset i1 i2 ⟷ internal_iface_name_subset (iface_sel i1) (iface_sel i2)"

lemma iface_subset: "iface_subset i1 i2 ⟷ {i. match_iface i1 i} ⊆ {i. match_iface i2 i}"
unfolding iface_subset_def
apply(cases i1, cases i2)

definition iface_is_wildcard :: "iface ⇒ bool" where
"iface_is_wildcard ifce ≡ iface_name_is_wildcard (iface_sel ifce)"

lemma iface_is_wildcard_ifaceAny: "iface_is_wildcard ifaceAny"

subsection‹Enumerating Interfaces›
private definition all_chars :: "char list" where
"all_chars ≡ Enum.enum"
private lemma all_chars: "set all_chars = (UNIV::char set)"

text‹we can compute this, but its horribly inefficient!›
(*valid chars in an interface are NOT limited to the printable ones!*)
private lemma strings_of_length_n: "set (List.n_lists n all_chars) = {s::string. length s = n}"
apply(induction n)
apply(simp; fail)
apply(safe)
apply(simp; fail)
apply(simp)
apply(rename_tac n x)
apply(rule_tac x="drop 1 x" in exI)
apply(simp)
apply(case_tac x)
apply(simp_all)
done

text‹Non-wildacrd interfaces of length @{term n}›
private definition non_wildcard_ifaces :: "nat ⇒ string list" where
"non_wildcard_ifaces n ≡ filter (λi. ¬ iface_name_is_wildcard i) (List.n_lists n all_chars)"

text‹Example: (any number higher than zero are probably too inefficient)›
private lemma "non_wildcard_ifaces 0 = ['''']" by eval

private lemma non_wildcard_ifaces: "set (non_wildcard_ifaces n) = {s::string. length s = n ∧ ¬ iface_name_is_wildcard s}"
using strings_of_length_n non_wildcard_ifaces_def by auto

private lemma "(⋃ i ∈ set (non_wildcard_ifaces n). internal_iface_name_to_set i) = {s::string. length s = n ∧ ¬ iface_name_is_wildcard s}"

text‹Non-wildacrd interfaces up to length @{term n}›
private fun non_wildcard_ifaces_upto :: "nat ⇒ string list" where
"non_wildcard_ifaces_upto 0 = [[]]" |
"non_wildcard_ifaces_upto (Suc n) = (non_wildcard_ifaces (Suc n)) @ non_wildcard_ifaces_upto n"
private lemma non_wildcard_ifaces_upto: "set (non_wildcard_ifaces_upto n) = {s::string. length s ≤ n ∧ ¬ iface_name_is_wildcard s}"
apply(induction n)
apply fastforce
using non_wildcard_ifaces by fastforce

subsection‹Negating Interfaces›
private lemma inv_iface_name_set: "- (internal_iface_name_to_set i) = (
if iface_name_is_wildcard i
then
{c |c. length c < length (butlast i)} ∪ {c @ cs |c cs. length c = length (butlast i) ∧ c ≠ butlast i}
else
{c | c. length c < length i} ∪ {c@cs | c cs. length c ≥ length i ∧ c ≠ i}
)"
proof -
{ fix i::string
have inv_i_wildcard: "- {i@cs | cs. True} = {c | c. length c < length i} ∪ {c@cs | c cs. length c = length i ∧ c ≠ i}"
apply(rule Set.equalityI)
prefer 2
apply(safe)[1]
apply(simp;fail)
apply(simp;fail)
apply(simp)
apply(rule Compl_anti_mono[where B="{i @ cs |cs. True}" and A="- ({c | c. length c < length i} ∪ {c@cs | c cs. length c = length i ∧ c ≠ i})", simplified])
apply(safe)
apply(simp)
apply(case_tac "(length i) = length x")
apply(erule_tac x=x in allE, simp)
apply(erule_tac x="take (length i) x" in allE)
by (metis append_take_drop_id)
} note inv_i_wildcard=this
{ fix i::string
have inv_i_nowildcard: "- {i::string} = {c | c. length c < length i} ∪ {c@cs | c cs. length c ≥ length i ∧ c ≠ i}"
proof -
have x: "{c | c. length c = length i ∧ c ≠ i}  ∪ {c | c. length c > length i} = {c@cs | c cs. length c ≥ length i ∧ c ≠ i}"
apply(safe)
apply force+
done
have "- {i::string} = {c |c . c ≠ i}"
by(safe, simp)
also have "… = {c | c. length c < length i} ∪ {c | c. length c = length i ∧ c ≠ i}  ∪ {c | c. length c > length i}"
by(auto)
finally show ?thesis using x by auto
qed
} note inv_i_nowildcard=this
show ?thesis
proof(cases "iface_name_is_wildcard i")
case True with inv_i_wildcard show ?thesis by force
next
case False with inv_i_nowildcard show ?thesis by force
qed
qed

text‹Negating is really not intuitive.
The Interface @{term "''et''"} is in the negated set of @{term "''eth+''"}.
And the Interface @{term "''et+''"} is also in this set! This is because @{term "''+''"}
is a normal interface character and not a wildcard here!
In contrast, the set described by @{term "''et+''"} (with @{term "''+''"} a wildcard)
is not a subset of the previously negated set.›
lemma "''et'' ∈ - (internal_iface_name_to_set ''eth+'')" by(simp)
lemma "''et+'' ∈ - (internal_iface_name_to_set ''eth+'')" by(simp)
lemma "''+'' ∈ - (internal_iface_name_to_set ''eth+'')" by(simp)
lemma "¬ {i. match_iface (Iface ''et+'') i} ⊆ - (internal_iface_name_to_set ''eth+'')" by force

text‹Because @{term "''+''"} can appear as interface wildcard and normal interface character,
we cannot take negate an @{term "Iface i"} such that we get back @{typ "iface list"} which
describe the negated interface.›
lemma "''+'' ∈ - (internal_iface_name_to_set ''eth+'')" by(simp)

fun compress_pos_interfaces :: "iface list ⇒ iface option" where
"compress_pos_interfaces [] = Some ifaceAny" |
"compress_pos_interfaces [i] = Some i" |
"compress_pos_interfaces (i1#i2#is) = (case iface_conjunct i1 i2 of None ⇒ None | Some i ⇒ compress_pos_interfaces (i#is))"

lemma compress_pos_interfaces_Some: "compress_pos_interfaces ifces = Some ifce ⟹
match_iface ifce p_i ⟷ (∀ i∈ set ifces. match_iface i p_i)"
proof(induction ifces rule: compress_pos_interfaces.induct)
case 1 thus ?case by (simp add: match_ifaceAny)
next
case 2 thus ?case by simp
next
case (3 i1 i2) thus ?case
apply(simp)
apply(case_tac "iface_conjunct i1 i2")
apply(simp; fail)
apply(simp)
using iface_conjunct_Some by presburger
qed

lemma compress_pos_interfaces_None: "compress_pos_interfaces ifces = None ⟹
¬ (∀ i∈ set ifces. match_iface i p_i)"
proof(induction ifces rule: compress_pos_interfaces.induct)
case 1 thus ?case by (simp add: match_ifaceAny)
next
case 2 thus ?case by simp
next
case (3 i1 i2) thus ?case
apply(cases "iface_conjunct i1 i2", simp_all)
apply (blast dest: iface_conjunct_None)
by (blast dest: iface_conjunct_Some)
qed
end

end


# Theory SimpleFw_Syntax

section‹Simple Firewall Syntax›
theory SimpleFw_Syntax
Firewall_Common_Decision_State
"Primitives/Iface"
"Primitives/L4_Protocol"
Simple_Packet
begin

text‹For for IP addresses of arbitrary length›

datatype simple_action = Accept | Drop

text‹Simple match expressions do not allow negated expressions.
However, Most match expressions can still be transformed into simple match expressions.

A negated IP address range can be represented as a set of non-negated IP ranges.
For example ‹!8 = {0..7} ∪ {8 .. ipv4max}›.
Using CIDR notation (i.e. the ‹a.b.c.d/n› notation), we can represent negated IP
ranges as a set of non-negated IP ranges with only fair blowup.
Another handy result is that the conjunction of two IP ranges in CIDR notation is
either the smaller of the two ranges or the empty set.
An empty IP range cannot be represented.
If one wants to represent the empty range, then the complete rule needs to be removed.

The same holds for layer 4 ports.
In addition, there exists an empty port range, e.g. ‹(1,0)›.
The conjunction of two port ranges is again just one port range.

But negation of interfaces is not supported. Since interfaces support a wildcard character,
transforming a negated interface would either result in an infeasible blowup or requires
knowledge about the existing interfaces (e.g. there only is eth0, eth1, wlan3, and vbox42)
An empirical test shows that negated interfaces do not occur in our data sets.
Negated interfaces can also be considered bad style: What is !eth0? Everything that is
not eth0, experience shows that interfaces may come up randomly, in particular in combination
with virtual machines, so !eth0 might not be the desired match.
At the moment, if an negated interface occurs which prevents translation to a simple match,
we recommend to abstract the negated interface to unknown and remove it (upper or lower closure
rule set) before translating to a simple match.
The same discussion holds for negated protocols.

Noteworthy, simple match expressions are both expressive and support conjunction:
‹simple-match1 ∧ simple-match2 = simple-match3›
›
(*It took very long to design the simple match such that it can represent everything we need
and that you can calculate with it. Disjunction is easy: just have two consecutive rules with the same action.
Conjunction was a tough fight! It is needed to translate:
common_primitive_match_to_simple_match (MatchAny e1 e2) =
simple_match_and (common_primitive_match_to_simple_match e1) (common_primitive_match_to_simple_match e2)
This is key to translate common_primitive_match to simple_match

It may seem a simple enhancement to support iiface :: "iface negation_type", but then you
can no longer form the conjunction of two simple_matches.
*)

iiface :: "iface" ― ‹in-interface›
(*we cannot (and don't want to) express negated interfaces*)
(*We could also drop interface wildcard support and try negated interfaces again …*)
oiface :: "iface" ― ‹out-interface›
src :: "('i::len word × nat) " ― ‹source IP address›
dst :: "('i::len word × nat) " ― ‹destination›
proto :: "protocol"
sports :: "(16 word × 16 word)" ― ‹source-port first:last›
dports :: "(16 word × 16 word)" ― ‹destination-port first:last›

context
begin
datatype 'i simple_rule = SimpleRule (match_sel: "'i simple_match") (action_sel: simple_action)
end

text‹Simple rule destructor. Removes the @{typ "'a simple_rule"} type, returns a tuple with the match and action.›
definition simple_rule_dtor :: "'a simple_rule ⇒ 'a simple_match × simple_action" where
"simple_rule_dtor r ≡ (case r of SimpleRule m a ⇒ (m,a))"

lemma simple_rule_dtor_ids:
"uncurry SimpleRule ∘ simple_rule_dtor = id"
"simple_rule_dtor ∘ uncurry SimpleRule = id"
unfolding simple_rule_dtor_def comp_def fun_eq_iff
by(simp_all split: simple_rule.splits)

end


# Theory SimpleFw_Semantics

section‹Simple Firewall Semantics›
theory SimpleFw_Semantics
imports SimpleFw_Syntax
begin

fun simple_match_ip :: "('i::len word × nat) ⇒ 'i::len word ⇒ bool" where
"simple_match_ip (base, len) p_ip ⟷ p_ip ∈ ipset_from_cidr base len"

lemma wordinterval_to_set_ipcidr_tuple_to_wordinterval_simple_match_ip_set:
"wordinterval_to_set (ipcidr_tuple_to_wordinterval ip) = {d. simple_match_ip ip d}"
proof -
{ fix s and d :: "'a::len word × nat"
from wordinterval_to_set_ipcidr_tuple_to_wordinterval have
"s ∈ wordinterval_to_set (ipcidr_tuple_to_wordinterval d) ⟷ simple_match_ip d s"
by(cases d) auto
} thus ?thesis by blast
qed

― ‹by the way, the words do not wrap around›
lemma "{(253::8 word) .. 8} = {}" by simp

fun simple_match_port :: "(16 word × 16 word) ⇒ 16 word ⇒ bool" where
"simple_match_port (s,e) p_p ⟷ p_p ∈ {s..e}"

fun simple_matches :: "'i::len simple_match ⇒ ('i, 'a) simple_packet_scheme ⇒ bool" where
"simple_matches m p ⟷
(match_iface (iiface m) (p_iiface p)) ∧
(match_iface (oiface m) (p_oiface p)) ∧
(simple_match_ip (src m) (p_src p)) ∧
(simple_match_ip (dst m) (p_dst p)) ∧
(match_proto (proto m) (p_proto p)) ∧
(simple_match_port (sports m) (p_sport p)) ∧
(simple_match_port (dports m) (p_dport p))"

text‹The semantics of a simple firewall: just iterate over the rules sequentially›
fun simple_fw :: "'i::len simple_rule list ⇒ ('i, 'a) simple_packet_scheme ⇒ state" where
"simple_fw [] _ = Undecided" |
"simple_fw ((SimpleRule m Accept)#rs) p = (if simple_matches m p then Decision FinalAllow else simple_fw rs p)" |
"simple_fw ((SimpleRule m Drop)#rs) p = (if simple_matches m p then Decision FinalDeny else simple_fw rs p)"

fun simple_fw_alt where
"simple_fw_alt [] _ = Undecided" |
"simple_fw_alt (r#rs) p = (if simple_matches (match_sel r) p then
(case action_sel r of Accept ⇒ Decision FinalAllow | Drop ⇒ Decision FinalDeny) else simple_fw_alt rs p)"

lemma simple_fw_alt: "simple_fw r p = simple_fw_alt r p" by(induction rule: simple_fw.induct) simp_all

definition simple_match_any :: "'i::len simple_match" where
"simple_match_any ≡ ⦇iiface=ifaceAny, oiface=ifaceAny, src=(0,0), dst=(0,0), proto=ProtoAny, sports=(0,65535), dports=(0,65535) ⦈"
lemma simple_match_any: "simple_matches simple_match_any p"
proof -
have *: "(65535::16 word) = max_word"
by simp
show ?thesis
by (simp add: simple_match_any_def ipset_from_cidr_0 match_ifaceAny *)
qed

text‹we specify only one empty port range›
definition simple_match_none :: "'i::len simple_match" where
"simple_match_none ≡
⦇iiface=ifaceAny, oiface=ifaceAny, src=(1,0), dst=(0,0),
proto=ProtoAny, sports=(1,0), dports=(0,65535) ⦈"
lemma simple_match_none: "¬ simple_matches simple_match_none p"
proof -
qed

fun empty_match :: "'i::len simple_match ⇒ bool" where
"empty_match ⦇iiface=_, oiface=_, src=_, dst=_, proto=_,
sports=(sps1, sps2), dports=(dps1, dps2) ⦈ ⟷ (sps1 > sps2) ∨ (dps1 > dps2)"

lemma empty_match: "empty_match m ⟷ (∀(p::('i::len, 'a) simple_packet_scheme). ¬ simple_matches m p)"
proof
assume "empty_match m"
thus "∀p. ¬ simple_matches m p" by(cases m) fastforce
next
assume assm: "∀(p::('i::len, 'a) simple_packet_scheme). ¬ simple_matches m p"
obtain iif oif sip dip protocol sps1 sps2 dps1 dps2 where m:
"m = ⦇iiface = iif, oiface = oif, src = sip, dst = dip, proto = protocol, sports = (sps1, sps2), dports = (dps1, dps2)⦈"
by(cases m) force

show "empty_match m"
let ?x="λp. dps1 ≤ p_dport p ⟶ p_sport p ≤ sps2 ⟶ sps1 ≤ p_sport p ⟶
match_proto protocol (p_proto p) ⟶ simple_match_ip dip (p_dst p) ⟶ simple_match_ip sip (p_src p) ⟶
match_iface oif (p_oiface p) ⟶ match_iface iif (p_iiface p) ⟶ ¬ p_dport p ≤ dps2"
from assm have nomatch: "∀(p::('i::len, 'a) simple_packet_scheme). ?x p" by(simp add: m)
{ fix ips::"'i::len word × nat"
have "a ∈ ipset_from_cidr a n" for a::"'i::len word" and n
using ipset_from_cidr_lowest by auto
hence "simple_match_ip ips (fst ips)" by(cases ips) simp
} note ips=this
have proto: "match_proto protocol (case protocol of ProtoAny ⇒ TCP | Proto p ⇒ p)"
by(simp split: protocol.split)
{ fix ifce
have "match_iface ifce (iface_sel ifce)"
} note ifaces=this
{ fix p::"('i, 'a) simple_packet_scheme"
from nomatch have "?x p" by blast
} note pkt1=this
obtain p::"('i, 'a) simple_packet_scheme" where [simp]:
"p_iiface p = iface_sel iif"
"p_oiface p = iface_sel oif"
"p_src p = fst sip"
"p_dst p = fst dip"
"p_proto p = (case protocol of ProtoAny ⇒ TCP | Proto p ⇒ p)"
"p_sport p = sps1"
"p_dport p = dps1"
by (meson simple_packet.select_convs)
note pkt=pkt1[of p, simplified]
from pkt ips proto ifaces have " sps1 ≤ sps2 ⟶ ¬ dps1 ≤ dps2" by blast
thus "sps2 < sps1 ∨ dps2 < dps1" by fastforce
qed
qed

lemma nomatch: "¬ simple_matches m p ⟹ simple_fw (SimpleRule m a # rs) p = simple_fw rs p"
by(cases a, simp_all del: simple_matches.simps)

subsection‹Simple Ports›
fun simpl_ports_conjunct :: "(16 word × 16 word) ⇒ (16 word × 16 word) ⇒ (16 word × 16 word)" where
"simpl_ports_conjunct (p1s, p1e) (p2s, p2e) = (max p1s p2s, min p1e p2e)"

lemma "{(p1s:: 16 word) .. p1e} ∩ {p2s .. p2e} = {max p1s p2s .. min p1e p2e}" by(simp)

lemma simple_ports_conjunct_correct:
"simple_match_port p1 pkt ∧ simple_match_port p2 pkt ⟷ simple_match_port (simpl_ports_conjunct p1 p2) pkt"
apply(cases p1, cases p2, simp)
by blast

lemma simple_match_port_code[code] :"simple_match_port (s,e) p_p = (s ≤ p_p ∧ p_p ≤ e)" by simp

lemma simple_match_port_UNIV: "{p. simple_match_port (s,e) p} = UNIV ⟷ (s = 0 ∧ e = max_word)"
apply(simp)
apply(rule)
apply(case_tac "s = 0")
using antisym_conv apply blast
using word_le_0_iff apply blast
using word_zero_le by blast

subsection‹Simple IPs›
lemma simple_match_ip_conjunct:
fixes ip1 :: "'i::len word × nat"
shows "simple_match_ip ip1 p_ip ∧ simple_match_ip ip2 p_ip ⟷
(case ipcidr_conjunct ip1 ip2 of None ⇒ False | Some ipx ⇒ simple_match_ip ipx p_ip)"
proof -
{
fix b1 m1 b2 m2
have "simple_match_ip (b1, m1) p_ip ∧ simple_match_ip (b2, m2) p_ip ⟷
p_ip ∈ ipset_from_cidr b1 m1 ∩ ipset_from_cidr b2 m2"
by simp
also have "… ⟷ p_ip ∈ (case ipcidr_conjunct (b1, m1) (b2, m2) of None ⇒ {} | Some (bx, mx) ⇒ ipset_from_cidr bx mx)"
using ipcidr_conjunct_correct by blast
also have "… ⟷ (case ipcidr_conjunct (b1, m1) (b2, m2) of None ⇒ False | Some ipx ⇒ simple_match_ip ipx p_ip)"
by(simp split: option.split)
finally have "simple_match_ip (b1, m1) p_ip ∧ simple_match_ip (b2, m2) p_ip ⟷
(case ipcidr_conjunct (b1, m1) (b2, m2) of None ⇒ False | Some ipx ⇒ simple_match_ip ipx p_ip)" .
} thus ?thesis by(cases ip1, cases ip2, simp)
qed

declare simple_matches.simps[simp del]

subsection‹Merging Simple Matches›
text‹@{typ "'i::len simple_match"} ‹∧› @{typ "'i::len simple_match"}›

fun simple_match_and :: "'i::len simple_match ⇒ 'i simple_match ⇒ 'i simple_match option" where
"simple_match_and ⦇iiface=iif1, oiface=oif1, src=sip1, dst=dip1, proto=p1, sports=sps1, dports=dps1 ⦈
⦇iiface=iif2, oiface=oif2, src=sip2, dst=dip2, proto=p2, sports=sps2, dports=dps2 ⦈ =
(case ipcidr_conjunct sip1 sip2 of None ⇒ None | Some sip ⇒
(case ipcidr_conjunct dip1 dip2 of None ⇒ None | Some dip ⇒
(case iface_conjunct iif1 iif2 of None ⇒ None | Some iif ⇒
(case iface_conjunct oif1 oif2 of None ⇒ None | Some oif ⇒
(case simple_proto_conjunct p1 p2 of None ⇒ None | Some p ⇒
Some ⦇iiface=iif, oiface=oif, src=sip, dst=dip, proto=p,
sports=simpl_ports_conjunct sps1 sps2, dports=simpl_ports_conjunct dps1 dps2 ⦈)))))"

lemma simple_match_and_correct: "simple_matches m1 p ∧ simple_matches m2 p ⟷
(case simple_match_and m1 m2 of None ⇒ False | Some m ⇒ simple_matches m p)"
proof -
obtain iif1 oif1 sip1 dip1 p1 sps1 dps1 where m1:
"m1 = ⦇iiface=iif1, oiface=oif1, src=sip1, dst=dip1, proto=p1, sports=sps1, dports=dps1 ⦈" by(cases m1, blast)
obtain iif2 oif2 sip2 dip2 p2 sps2 dps2 where m2:
"m2 = ⦇iiface=iif2, oiface=oif2, src=sip2, dst=dip2, proto=p2, sports=sps2, dports=dps2 ⦈" by(cases m2, blast)

have sip_None: "ipcidr_conjunct sip1 sip2 = None ⟹ ¬ simple_match_ip sip1 (p_src p) ∨ ¬ simple_match_ip sip2 (p_src p)"
using simple_match_ip_conjunct[of sip1 "p_src p" sip2] by simp
have dip_None: "ipcidr_conjunct dip1 dip2 = None ⟹ ¬ simple_match_ip dip1 (p_dst p) ∨ ¬ simple_match_ip dip2 (p_dst p)"
using simple_match_ip_conjunct[of dip1 "p_dst p" dip2] by simp
have sip_Some: "⋀ip. ipcidr_conjunct sip1 sip2 = Some ip ⟹
simple_match_ip ip (p_src p) ⟷ simple_match_ip sip1 (p_src p) ∧ simple_match_ip sip2 (p_src p)"
using simple_match_ip_conjunct[of sip1 "p_src p" sip2] by simp
have dip_Some: "⋀ip. ipcidr_conjunct dip1 dip2 = Some ip ⟹
simple_match_ip ip (p_dst p) ⟷ simple_match_ip dip1 (p_dst p) ∧ simple_match_ip dip2 (p_dst p)"
using simple_match_ip_conjunct[of dip1 "p_dst p" dip2] by simp

have iiface_None: "iface_conjunct iif1 iif2 = None ⟹ ¬ match_iface iif1 (p_iiface p) ∨ ¬ match_iface iif2 (p_iiface p)"
using iface_conjunct[of iif1 "(p_iiface p)" iif2] by simp
have oiface_None: "iface_conjunct oif1 oif2 = None ⟹ ¬ match_iface oif1 (p_oiface p) ∨ ¬ match_iface oif2 (p_oiface p)"
using iface_conjunct[of oif1 "(p_oiface p)" oif2] by simp
have iiface_Some: "⋀iface. iface_conjunct iif1 iif2 = Some iface ⟹
match_iface iface (p_iiface p) ⟷ match_iface iif1 (p_iiface p) ∧ match_iface iif2 (p_iiface p)"
using iface_conjunct[of iif1 "(p_iiface p)" iif2] by simp
have oiface_Some: "⋀iface. iface_conjunct oif1 oif2 = Some iface ⟹
match_iface iface (p_oiface p) ⟷ match_iface oif1 (p_oiface p) ∧ match_iface oif2 (p_oiface p)"
using iface_conjunct[of oif1 "(p_oiface p)" oif2] by simp

have proto_None: "simple_proto_conjunct p1 p2 = None ⟹ ¬ match_proto p1 (p_proto p) ∨ ¬ match_proto p2 (p_proto p)"
using simple_proto_conjunct_correct[of p1 "(p_proto p)" p2] by simp
have proto_Some: "⋀proto. simple_proto_conjunct p1 p2 = Some proto ⟹
match_proto proto (p_proto p) ⟷ match_proto p1 (p_proto p) ∧ match_proto p2 (p_proto p)"
using simple_proto_conjunct_correct[of p1 "(p_proto p)" p2] by simp

have case_Some: "⋀m. Some m = simple_match_and m1 m2 ⟹
(simple_matches m1 p ∧ simple_matches m2 p) ⟷ simple_matches m p"
apply(simp add: m1 m2 simple_matches.simps split: option.split_asm)
using simple_ports_conjunct_correct by(blast dest: sip_Some dip_Some iiface_Some oiface_Some proto_Some)
have case_None: "simple_match_and m1 m2 = None ⟹ ¬ (simple_matches m1 p ∧ simple_matches m2 p)"
apply(simp add: m1 m2 simple_matches.simps split: option.split_asm)
apply(blast dest: sip_None dip_None iiface_None oiface_None proto_None)+
done
from case_Some case_None show ?thesis by(cases "simple_match_and m1 m2") simp_all
qed

lemma simple_match_and_SomeD: "simple_match_and m1 m2 = Some m ⟹
simple_matches m p ⟷ (simple_matches m1 p ∧ simple_matches m2 p)"
lemma simple_match_and_NoneD: "simple_match_and m1 m2 = None ⟹
¬(simple_matches m1 p ∧ simple_matches m2 p)"
lemma simple_matches_andD: "simple_matches m1 p ⟹ simple_matches m2 p ⟹
∃m. simple_match_and m1 m2 = Some m ∧ simple_matches m p"
by (meson option.exhaust_sel simple_match_and_NoneD simple_match_and_SomeD)

subsection‹Further Properties of a Simple Firewall›
fun has_default_policy :: "'i::len simple_rule list ⇒ bool" where
"has_default_policy [] = False" |
"has_default_policy [(SimpleRule m _)] = (m = simple_match_any)" |
"has_default_policy (_#rs) = has_default_policy rs"

lemma has_default_policy: "has_default_policy rs ⟹
simple_fw rs p = Decision FinalAllow ∨ simple_fw rs p = Decision FinalDeny"
proof(induction rs rule: has_default_policy.induct)
case 1 thus ?case by (simp)
next
case (2 m a) thus ?case by(cases a) (simp_all add: simple_match_any)
next
case (3 r1 r2 rs)
from 3 obtain a m where "r1 = SimpleRule m a" by (cases r1) simp
with 3 show ?case by (cases a) simp_all
qed

lemma has_default_policy_fst: "has_default_policy rs ⟹ has_default_policy (r#rs)"
apply(cases r, rename_tac m a, simp)
apply(cases rs)
by(simp_all)

text‹We can stop after a default rule (a rule which matches anything) is observed.›
fun cut_off_after_match_any :: "'i::len simple_rule list ⇒ 'i simple_rule list" where
"cut_off_after_match_any [] = []" |
"cut_off_after_match_any (SimpleRule m a # rs) =
(if m = simple_match_any then [SimpleRule m a] else SimpleRule m a # cut_off_after_match_any rs)"

lemma cut_off_after_match_any: "simple_fw (cut_off_after_match_any rs) p = simple_fw rs p"
apply(induction rs p rule: simple_fw.induct)

lemma simple_fw_not_matches_removeAll: "¬ simple_matches m p ⟹
simple_fw (removeAll (SimpleRule m a) rs) p = simple_fw rs p"
apply(induction rs p rule: simple_fw.induct)
apply(simp)
apply(simp_all)
apply blast+
done

subsection‹Reality check: Validity of Simple Matches›
text‹While it is possible to construct a ‹simple_fw› expression that only matches a source
or destination port, such a match is not meaningful, as the presence of the port information is
dependent on the protocol. Thus, a match for a port should always include the match for a protocol.
Additionally, prefixes should be zero on bits beyond the prefix length.
›

definition "valid_prefix_fw m = valid_prefix (uncurry PrefixMatch m)"

lemma ipcidr_conjunct_valid:
"⟦valid_prefix_fw p1; valid_prefix_fw p2; ipcidr_conjunct p1 p2 = Some p⟧ ⟹ valid_prefix_fw p"
unfolding valid_prefix_fw_def
by(cases p; cases p1; cases p2) (simp add: ipcidr_conjunct.simps split: if_splits)

definition simple_match_valid :: "('i::len, 'a) simple_match_scheme ⇒ bool" where
"simple_match_valid m ≡
({p. simple_match_port (sports m) p} ≠ UNIV ∨ {p. simple_match_port (dports m) p} ≠ UNIV ⟶
proto m ∈ Proto {TCP, UDP, L4_Protocol.SCTP}) ∧
valid_prefix_fw (src m) ∧ valid_prefix_fw (dst m)"

lemma simple_match_valid_alt[code_unfold]: "simple_match_valid = (λ m.
(let c = (λ(s,e). (s ≠ 0 ∨ e ≠ max_word)) in (
if c (sports m) ∨ c (dports m) then proto m = Proto TCP ∨ proto m = Proto UDP ∨ proto m = Proto L4_Protocol.SCTP else True)) ∧
valid_prefix_fw (src m) ∧ valid_prefix_fw (dst m))"
proof -
have simple_match_valid_alt_hlp1: "{p. simple_match_port x p} ≠ UNIV ⟷ (case x of (s,e) ⇒ s ≠ 0 ∨ e ≠ max_word)"
for x using simple_match_port_UNIV by auto
have simple_match_valid_alt_hlp2: "{p. simple_match_port x p} ≠ {} ⟷ (case x of (s,e) ⇒ s ≤ e)" for x by auto
show ?thesis
unfolding fun_eq_iff
unfolding simple_match_valid_def Let_def
unfolding simple_match_valid_alt_hlp1 simple_match_valid_alt_hlp2
apply(clarify, rename_tac m, case_tac "sports m"; case_tac "dports m"; case_tac "proto m")
by auto
qed

text‹Example:›
context
begin
private definition "example_simple_match1 ≡
⦇iiface = Iface ''+'', oiface = Iface ''+'', src = (0::32 word, 0), dst = (0, 0),
proto = Proto TCP, sports = (0, 1024), dports = (0, 1024)⦈"

lemma "simple_fw [SimpleRule example_simple_match1 Drop]
⦇p_iiface = '''', p_oiface = '''',  p_src = (1::32 word), p_dst = 2, p_proto = TCP, p_sport = 8,
p_dport = 9, p_tcp_flags = {}, p_payload = ''''⦈ =
Decision FinalDeny" by eval

private definition "example_simple_match2 ≡ example_simple_match1⦇ proto := ProtoAny ⦈"
text‹Thus, ‹example_simple_match1› is valid, but if we set its protocol match to any, it isn't anymore›
private lemma "simple_match_valid example_simple_match1" by eval
private lemma "¬ simple_match_valid example_simple_match2" by eval
end

lemma simple_match_and_valid:
fixes m1 :: "'i::len simple_match"
assumes mv: "simple_match_valid m1" "simple_match_valid m2"
assumes mj: "simple_match_and m1 m2 = Some m"
shows "simple_match_valid m"
proof -
have simpl_ports_conjunct_not_UNIV:
"Collect (simple_match_port x) ≠ UNIV ⟹
x = simpl_ports_conjunct p1 p2 ⟹
Collect (simple_match_port p1) ≠ UNIV ∨ Collect (simple_match_port p2) ≠ UNIV"
for x p1 p2 by (metis Collect_cong mem_Collect_eq simple_ports_conjunct_correct)

(* prefix validity. That's simple. *)
have "valid_prefix_fw (src m1)" "valid_prefix_fw (src m2)" "valid_prefix_fw (dst m1)" "valid_prefix_fw (dst m2)"
using mv unfolding simple_match_valid_alt by simp_all
moreover have "ipcidr_conjunct (src m1) (src m2) = Some (src m)"
"ipcidr_conjunct (dst m1) (dst m2) = Some (dst m)"
using mj by(cases m1; cases m2; cases m; simp split: option.splits)+
ultimately have pv: "valid_prefix_fw (src m)" "valid_prefix_fw (dst m)"
using ipcidr_conjunct_valid by blast+

(* now for the source ports… *)
define nmu where "nmu ps ⟷ {p. simple_match_port ps p} ≠ UNIV" for ps
have "simpl_ports_conjunct (sports m1) (sports m2) = (sports m)" (is "?ph1 sports")
using mj by(cases m1; cases m2; cases m; simp split: option.splits)
hence sp: "nmu (sports m) ⟶ nmu (sports m1) ∨ nmu (sports m2)"
(is "?ph2 sports")
unfolding nmu_def using simpl_ports_conjunct_not_UNIV by metis

(* dst ports: mutatis mutandem *)
have "?ph1 dports" using mj by(cases m1; cases m2; cases m; simp split: option.splits)
hence dp: "?ph2 dports" unfolding nmu_def using simpl_ports_conjunct_not_UNIV by metis

(* And an argument for the protocol. *)
define php where "php mr ⟷ proto mr ∈ Proto  {TCP, UDP, L4_Protocol.SCTP}"
for mr :: "'i simple_match"
have pcj: "simple_proto_conjunct (proto m1) (proto m2) = Some (proto m)"
using mj by(cases m1; cases m2; cases m; simp split: option.splits)
hence p: "php m1 ⟹ php m"
"php m2 ⟹ php m"
using conjunctProtoD conjunctProtoD2 pcj unfolding php_def by auto

(* Since I'm trying to trick the simplifier with these defs, I need these as explicit statements: *)
have "⋀mx. simple_match_valid mx ⟹ nmu (sports mx) ∨ nmu (dports mx) ⟹ php mx"
unfolding nmu_def php_def simple_match_valid_def by blast
hence mps: "nmu (sports m1) ⟹ php m1" "nmu (dports m1) ⟹ php m1"
"nmu (sports m2) ⟹ php m2" "nmu (dports m2) ⟹ php m2" using mv by blast+

have pa: "nmu (sports m) ∨ nmu (dports m) ⟶ php m"
(*  apply(intro impI)
apply(elim disjE)
apply(drule sp[THEN mp])
apply(elim disjE)
apply(drule mps)
apply(elim p; fail) *)
using sp dp mps p by fast

show ?thesis
unfolding simple_match_valid_def
using pv pa[unfolded nmu_def php_def] by blast
qed

definition "simple_fw_valid ≡ list_all (simple_match_valid ∘ match_sel)"

text‹The simple firewall does not care about tcp flags, payload, or any other packet extensions.›
lemma simple_matches_extended_packet:
"simple_matches m
⦇p_iiface = iifce,
oiface = oifce,
p_src = s, dst = d,
p_proto = prot,
p_sport = sport, p_dport = dport,
⟷
simple_matches m
⦇p_iiface = iifce,
oiface = oifce,
p_src = s, p_dst = d,
p_proto = prot,
p_sport = sport, p_dport = dport,
"
end


# Theory List_Product_More

section‹List Product Helpers›
theory List_Product_More
imports Main
begin

(*TODO: this definition could also go to Main*)
lemma List_product_concat_map: "List.product xs ys = concat (map (λx. map (λy. (x,y)) ys) xs)"
by(induction xs) (simp)+

definition all_pairs :: "'a list ⇒ ('a × 'a) list" where
"all_pairs xs ≡ concat (map (λx. map (λy. (x,y)) xs) xs)"

lemma all_pairs_list_product: "all_pairs xs = List.product xs xs"

lemma all_pairs: "∀ (x,y) ∈ (set xs × set xs). (x,y) ∈ set (all_pairs xs)"

lemma all_pairs_set: "set (all_pairs xs) = set xs × set xs"

end


# Theory Option_Helpers

section‹Option to List and Option to Set›
theory Option_Helpers
imports Main
begin

text‹Those are just syntactic helpers.›

definition option2set :: "'a option ⇒ 'a set" where
"option2set n ≡ (case n of None ⇒ {} | Some s ⇒ {s})"

definition option2list :: "'a option ⇒ 'a list" where
"option2list n ≡ (case n of None ⇒ [] | Some s ⇒ [s])"

lemma set_option2list[simp]: "set (option2list k) = option2set k"
unfolding option2list_def option2set_def by (simp split: option.splits)

lemma option2list_simps[simp]: "option2list (Some x) = [x]" "option2list (None) = []"
unfolding option2list_def option.simps by(fact refl)+

lemma option2set_None: "option2set None = {}"

lemma option2list_map: "option2list (map_option f n) = map f (option2list n)"

lemma option2set_map: "option2set (map_option f n) = f  option2set n"

end


# Theory Generic_SimpleFw

section‹Generalize Simple Firewall›
theory Generic_SimpleFw
imports SimpleFw_Semantics "Common/List_Product_More" "Common/Option_Helpers"
begin

subsection‹Semantics›
text‹The semantics of the @{term simple_fw} is quite close to @{const List.find}.
The idea of the generalized @{term simple_fw} semantics is that you can have anything as the
resulting action, not only a @{type simple_action}.›

definition generalized_sfw
:: "('i::len simple_match × 'a) list ⇒ ('i, 'pkt_ext) simple_packet_scheme ⇒ ('i simple_match × 'a) option"
where
"generalized_sfw l p ≡ find (λ(m,a). simple_matches m p) l"

subsection‹Lemmas›
lemma generalized_sfw_simps:
"generalized_sfw [] p = None"
"generalized_sfw (a # as) p = (if (case a of (m,_) ⇒ simple_matches m p) then Some a else generalized_sfw as p)"
unfolding generalized_sfw_def by simp_all

lemma generalized_sfw_append:
"generalized_sfw (a @ b) p = (case generalized_sfw a p of Some x ⇒ Some x
|  None ⇒ generalized_sfw b p)"

lemma simple_generalized_undecided:
"simple_fw fw p ≠ Undecided ⟹ generalized_sfw (map simple_rule_dtor fw) p ≠ None"
by(induction fw)
(clarsimp simp add: generalized_sfw_def simple_fw_alt simple_rule_dtor_def
split: prod.splits if_splits simple_action.splits simple_rule.splits)+

lemma generalized_sfwSomeD: "generalized_sfw fw p = Some (r,d) ⟹ (r,d) ∈ set fw ∧ simple_matches r p"
unfolding generalized_sfw_def
by(induction fw) (simp split: if_split_asm)+

lemma generalized_sfw_NoneD: "generalized_sfw fw p = None ⟹ ∀(a,b) ∈ set fw. ¬ simple_matches a p"
by(induction fw) (clarsimp simp add: generalized_sfw_simps split: if_splits)+

lemma generalized_fw_split: "generalized_sfw fw p = Some r ⟹ ∃fw1 fw3. fw = fw1 @ r # fw3 ∧ generalized_sfw fw1 p = None"
apply(induction fw rule: rev_induct)
apply(simp add: generalized_sfw_simps generalized_sfw_append split: option.splits;fail)
apply(clarsimp simp add: generalized_sfw_simps generalized_sfw_append split: option.splits if_splits)
apply blast+
done

lemma generalized_sfw_filterD:
"generalized_sfw (filter f fw) p = Some (r,d) ⟹ simple_matches r p ∧ f (r,d)"
by(induction fw) (simp_all add: generalized_sfw_simps split: if_splits)

lemma generalized_sfw_mapsnd:
"generalized_sfw (map (apsnd f) fw) p = map_option (apsnd f) (generalized_sfw fw p)"
by(induction fw) (simp add: generalized_sfw_simps split: prod.splits)+

subsection‹Equality with the Simple Firewall›

text‹A matching action of the simple firewall directly corresponds to a filtering decision›
definition simple_action_to_decision :: "simple_action ⇒ state" where
"simple_action_to_decision a ≡ case a of Accept ⇒ Decision FinalAllow
|   Drop ⇒ Decision FinalDeny"

text‹The @{const simple_fw} and the @{const generalized_sfw} are equal, if the state is translated appropriately.›
lemma simple_fw_iff_generalized_fw:
"simple_fw fw p = simple_action_to_decision a ⟷ (∃r. generalized_sfw (map simple_rule_dtor fw) p = Some (r,a))"
by(induction fw)
(clarsimp simp add: generalized_sfw_simps simple_rule_dtor_def simple_fw_alt simple_action_to_decision_def
split: simple_rule.splits if_splits simple_action.splits)+

lemma simple_fw_iff_generalized_fw_accept:
"simple_fw fw p = Decision FinalAllow ⟷ (∃r. generalized_sfw (map simple_rule_dtor fw) p = Some (r, Accept))"
by(fact simple_fw_iff_generalized_fw[where a = simple_action.Accept,
unfolded simple_action_to_decision_def simple_action.simps])
lemma simple_fw_iff_generalized_fw_drop:
"simple_fw fw p = Decision FinalDeny ⟷ (∃r. generalized_sfw (map simple_rule_dtor fw) p = Some (r, Drop))"
by(fact simple_fw_iff_generalized_fw[where a = simple_action.Drop,
unfolded simple_action_to_decision_def simple_action.simps])

subsection‹Joining two firewalls, i.e. a packet is send through both sequentially.›

definition generalized_fw_join
:: "('i::len simple_match × 'a) list ⇒ ('i simple_match × 'b) list ⇒ ('i simple_match × 'a × 'b) list"
where
"generalized_fw_join l1 l2 ≡ [(u,(a,b)). (m1,a) ← l1, (m2,b) ← l2, u ← option2list (simple_match_and m1 m2)]"

lemma generalized_fw_join_1_Nil[simp]: "generalized_fw_join [] f2 = []"
unfolding generalized_fw_join_def by(induction f2) simp+

lemma generalized_fw_join_2_Nil[simp]: "generalized_fw_join f1 [] = []"
unfolding generalized_fw_join_def by(induction f1) simp+

lemma generalized_fw_join_cons_1:
"generalized_fw_join ((am,ad) # l1) l2 =
[(u,(ad,b)). (m2,b) ← l2, u ← option2list (simple_match_and am m2)] @ generalized_fw_join l1 l2"
unfolding generalized_fw_join_def by(simp)

lemma generalized_fw_join_1_nomatch:
"¬ simple_matches am p ⟹
generalized_sfw [(u,(ad,b)). (m2,b) ← l2, u ← option2list (simple_match_and am m2)] p = None"
by(induction l2)
(clarsimp simp add: generalized_sfw_simps generalized_sfw_append option2list_def simple_match_and_SomeD
split: prod.splits option.splits)+

lemma generalized_fw_join_2_nomatch:
"¬ simple_matches bm p ⟹
generalized_sfw (generalized_fw_join as ((bm, bd) # bs)) p = generalized_sfw (generalized_fw_join as bs) p"
proof(induction as)
case (Cons a as)
note mIH = Cons.IH[OF Cons.prems]
have *: "generalized_sfw (concat (map (λ(m2, b). map (λu. (u, ad, b)) (option2list (simple_match_and am m2))) ((bm, bd) # bs))) p =
generalized_sfw (concat (map (λ(m2, b). map (λu. (u, ad, b)) (option2list (simple_match_and am m2))) bs)) p"
unfolding list.map prod.simps
apply(cases "simple_match_and am bm")
apply(frule simple_match_and_SomeD[of _ _ _ p])
apply(subst option2list_def)
apply(unfold concat.simps)
done
show ?case
unfolding a
unfolding generalized_fw_join_cons_1
unfolding generalized_sfw_append
unfolding mIH
unfolding *
..

lemma generalized_fw_joinI:
"⟦generalized_sfw f1 p = Some (r1,d1); generalized_sfw f2 p = Some (r2,d2)⟧ ⟹
generalized_sfw (generalized_fw_join f1 f2) p = Some (the (simple_match_and r1 r2), d1,d2)"
proof(induction f1)
case (Cons a as)
obtain am ad where a[simp]: "a = Pair am ad" by(cases a)
show ?case proof(cases "simple_matches am p")
case True
hence dra: "d1 = ad" "r1 = am" using Cons.prems by(simp_all add: generalized_sfw_simps)
from Cons.prems(2) show ?thesis unfolding a dra
proof(induction f2)
case (Cons b bs)
obtain bm bd where b[simp]: "b = Pair bm bd" by(cases b)
thus ?case
proof(cases "simple_matches bm p")
case True
hence drb: "d2 = bd" "r2 = bm" using Cons.prems by(simp_all add: generalized_sfw_simps)
from True ‹simple_matches am p› obtain ruc where sma[simp]:
"simple_match_and am bm = Some ruc" "simple_matches ruc p"
using simple_match_and_correct[of am p bm]
by(simp split: option.splits)
show ?thesis unfolding b
by(simp add: generalized_fw_join_def option2list_def generalized_sfw_simps drb)
next
case False
with Cons.prems have bd:
"generalized_sfw (b # bs) p = generalized_sfw bs p"
"generalized_sfw (b # bs) p = Some (r2, d2)"
note mIH = Cons.IH[OF bd(2)[unfolded bd(1)]]
show ?thesis
unfolding mIH[symmetric] b
using generalized_fw_join_2_nomatch[OF False, of "(am, ad) # as" bd bs]
.
qed
(*and empty_concat: "concat (map (λx. []) ms) = []" by simp*)
next
case False
with Cons.prems have "generalized_sfw (a # as) p = generalized_sfw as p"
with Cons.prems have "generalized_sfw as p = Some (r1, d1)" by simp
note mIH = Cons.IH[OF this Cons.prems(2)]
show ?thesis
unfolding mIH[symmetric] a
unfolding generalized_fw_join_cons_1
unfolding generalized_sfw_append
unfolding generalized_fw_join_1_nomatch[OF False, of ad f2]
by simp
qed

(* The structure is nearly the same as with generalized_fw_joinI, so it should be possible to show
it in one proof. But I felt like this is the better way *)
lemma generalized_fw_joinD:
"generalized_sfw (generalized_fw_join f1 f2) p = Some (u, d1,d2) ⟹
∃r1 r2. generalized_sfw f1 p = Some (r1,d1) ∧ generalized_sfw f2 p = Some (r2,d2) ∧ Some u = simple_match_and r1 r2"
proof(induction f1)
case (Cons a as)
obtain am ad where a[simp]: "a = Pair am ad" by(cases a)
show ?case proof(cases "simple_matches am p", rule exI)
case True
show "∃r2. generalized_sfw (a # as) p = Some (am, d1) ∧ generalized_sfw f2 p = Some (r2, d2) ∧ Some u = simple_match_and am r2"
using Cons.prems
proof(induction f2)
case (Cons b bs)
obtain bm bd where b[simp]: "b = Pair bm bd" by(cases b)
show ?case
proof(cases "simple_matches bm p", rule exI)
case True
with ‹simple_matches am p› obtain u' (* u' = u, but I don't need that yet. *)
where sma: "simple_match_and am bm = Some u' ∧ simple_matches u' p"
using simple_match_and_correct[of am p bm] by(simp split: option.splits)
show "generalized_sfw (a # as) p = Some (am, d1) ∧ generalized_sfw (b # bs) p = Some (bm, d2) ∧ Some u = simple_match_and am bm"
using Cons.prems True ‹simple_matches am p›
by(simp add: generalized_fw_join_def generalized_sfw_append sma generalized_sfw_simps)
next
case False
have "generalized_sfw (generalized_fw_join (a # as) bs) p = Some (u, d1, d2)"
using Cons.prems unfolding b unfolding generalized_fw_join_2_nomatch[OF False] .
note Cons.IH[OF this]
moreover have "generalized_sfw (b # bs) p = generalized_sfw bs p" using False by(simp add: generalized_sfw_simps)
ultimately show ?thesis by presburger
qed
next
case False
with Cons.prems have "generalized_sfw (generalized_fw_join as f2) p = Some (u, d1, d2)" by(simp add: generalized_fw_join_cons_1 generalized_sfw_append generalized_fw_join_1_nomatch)
note Cons.IH[OF this]
moreover have "generalized_sfw (a # as) p = generalized_sfw as p" using False by(simp add: generalized_sfw_simps)
ultimately show ?thesis by presburger
qed

text‹We imagine two firewalls are positioned directly after each other.
The first one has ruleset rs1 installed, the second one has ruleset rs2 installed.
A packet needs to pass both firewalls.›

theorem simple_fw_join:
defines "rule_translate ≡
map (λ(u,a,b). SimpleRule u (if a = Accept ∧ b = Accept then Accept else Drop))"
shows
"simple_fw rs1 p = Decision FinalAllow ∧ simple_fw rs2 p = Decision FinalAllow ⟷
simple_fw (rule_translate (generalized_fw_join (map simple_rule_dtor rs1) (map simple_rule_dtor rs2))) p = Decision FinalAllow"
proof -
have hlp1:
"simple_rule_dtor ∘ (λ(u, a, b). SimpleRule u (if a = Accept ∧ b = Accept then Accept else Drop)) =
apsnd (λ(a, b). if a = Accept ∧ b = Accept then Accept else Drop)"
unfolding fun_eq_iff comp_def by(simp add: simple_rule_dtor_def)
show ?thesis
unfolding simple_fw_iff_generalized_fw_accept
apply(rule)
apply(clarify)
apply(drule (1) generalized_fw_joinI)
apply(simp add: hlp1 rule_translate_def generalized_sfw_mapsnd ;fail)
apply(clarsimp simp add: hlp1 generalized_sfw_mapsnd rule_translate_def)
apply(drule generalized_fw_joinD)
apply(clarsimp split: if_splits)
done
qed

theorem simple_fw_join2:
― ‹translates a @{text "(match, action1, action2)"} tuple of the joined generalized
firewall to a @{typ "'i::len simple_rule list"}. The two actions are translated such
that you only get @{const Accept} if both actions are @{const Accept}›
defines "to_simple_rule_list ≡ map (apsnd (λ(a,b) ⇒ (case a of Accept ⇒ b
|  Drop ⇒ Drop)))"
shows "simple_fw rs1 p = Decision FinalAllow ∧ simple_fw rs2 p = Decision FinalAllow ⟷
(∃m. (generalized_sfw (to_simple_rule_list
(generalized_fw_join (map simple_rule_dtor rs1) (map simple_rule_dtor rs2))) p) = Some (m, Accept))"
unfolding simple_fw_iff_generalized_fw_accept
apply(rule)
apply(clarify)
apply(drule (1) generalized_fw_joinI)
apply(clarsimp simp add: to_simple_rule_list_def generalized_sfw_mapsnd; fail)
apply(drule generalized_fw_joinD)
apply(clarsimp split: if_splits simple_action.splits)
done

lemma generalized_fw_join_1_1:
"generalized_fw_join [(m1,d1)] fw2 = foldr (λ(m2,d2). (@) (case simple_match_and m1 m2 of None ⇒ [] | Some mu ⇒ [(mu,d1,d2)])) fw2 []"
proof -
have concat_map_foldr: "concat (map (λx. f x) l) = foldr (λx. (@) (f x)) l []" for f :: "'x ⇒ 'y list" and l
by(induction l) simp_all
show ?thesis
apply(unfold list.map  prod.case_distrib option.case_distrib)
by simp
qed

lemma generalized_sfw_2_join_None:
"generalized_sfw fw2 p = None ⟹ generalized_sfw (generalized_fw_join fw1 fw2) p = None"
by(induction fw2) (simp_all add: generalized_sfw_simps generalized_sfw_append generalized_fw_join_2_nomatch split: if_splits option.splits prod.splits)

lemma generalized_sfw_1_join_None:
"generalized_sfw fw1 p = None ⟹ generalized_sfw (generalized_fw_join fw1 fw2) p = None"
by(induction fw1) (simp_all add: generalized_sfw_simps generalized_fw_join_cons_1 generalized_sfw_append generalized_fw_join_1_nomatch split: if_splits option.splits prod.splits)

lemma generalized_sfw_join_set: "(a, b1, b2) ∈ set (generalized_fw_join f1 f2) ⟷
(∃a1 a2. (a1, b1) ∈ set f1 ∧ (a2, b2) ∈ set f2 ∧ simple_match_and a1 a2 = Some a)"
unfolding generalized_fw_join_def
apply(rule iffI)
subgoal unfolding generalized_fw_join_def by(clarsimp simp: option2set_def split: option.splits) blast
by(clarsimp simp: option2set_def split: option.splits) fastforce

subsection‹Validity›
text‹There's validity of matches on @{const generalized_sfw}, too, even on the join.›

definition gsfw_valid :: "('i::len simple_match × 'c) list ⇒ bool" where
"gsfw_valid ≡ list_all (simple_match_valid ∘ fst)"

lemma gsfw_join_valid: "gsfw_valid f1 ⟹ gsfw_valid f2 ⟹ gsfw_valid (generalized_fw_join f1 f2)"
unfolding gsfw_valid_def
apply(induction f1)
apply(simp;fail)
apply(simp)
apply(rename_tac a f1)
apply(case_tac a)
apply(clarify)
apply(thin_tac "list_all _ f1")
apply(thin_tac "list_all _ (generalized_fw_join _ _)")
apply(induction f2)
apply(simp;fail)
apply(simp)
using simple_match_and_valid apply metis
done

lemma gsfw_validI: "simple_fw_valid fw ⟹ gsfw_valid (map simple_rule_dtor fw)"
unfolding gsfw_valid_def simple_fw_valid_def
by(clarsimp simp add: simple_rule_dtor_def list_all_iff split: simple_rule.splits) fastforce

end


section‹Shadowed Rules›
imports SimpleFw_Semantics
begin

text‹Testing, not executable›

text‹Assumes: @{term "simple_ruleset"}›
fun rmshadow :: "'i::len simple_rule list ⇒ 'i simple_packet set ⇒ 'i simple_rule list" where
"rmshadow [] _ = []" |
"rmshadow ((SimpleRule m a)#rs) P = (if (∀p∈P. ¬ simple_matches m p)
then
else
(SimpleRule m a) # (rmshadow rs {p ∈ P. ¬ simple_matches m p}))"

subsubsection‹Soundness›
"p ∈ P ⟹ simple_fw (rmshadow rs P) p = simple_fw rs p"
proof(induction rs arbitrary: P)
case Nil thus ?case by simp
next
case (Cons r rs)
from Cons.IH Cons.prems have IH1: "simple_fw (rmshadow rs P) p = simple_fw rs p" by (simp)
let ?P'="{p ∈ P. ¬ simple_matches (match_sel r) p}"
from Cons.IH Cons.prems have IH2: "⋀m. p ∈ ?P' ⟹ simple_fw (rmshadow rs ?P') p = simple_fw rs p" by simp
from Cons.prems show ?case
apply(cases r, rename_tac m a)
apply(simp)
apply(case_tac "∀p∈P. ¬ simple_matches m p")
apply(case_tac "p ∈ ?P'")
apply(frule IH2)
apply(simp)
apply(case_tac a)
apply(simp_all)
by fast+
qed

fixes p :: "'i::len simple_packet"
shows "simple_fw (rmshadow rs UNIV) p = simple_fw rs p"

text‹A different approach where we start with the empty set of packets and collect packets which are already matched-away''.›
fun rmshadow' :: "'i::len simple_rule list ⇒ 'i simple_packet set ⇒ 'i simple_rule list" where
"rmshadow' [] _ = []" |
"rmshadow' ((SimpleRule m a)#rs) P = (if {p. simple_matches m p} ⊆ P
then
else
(SimpleRule m a) # (rmshadow' rs (P ∪ {p. simple_matches m p})))"

"p ∉ P ⟹ simple_fw (rmshadow' rs P) p = simple_fw rs p"
proof(induction rs arbitrary: P)
case Nil thus ?case by simp
next
case (Cons r rs)
from Cons.IH Cons.prems have IH1: "simple_fw (rmshadow' rs P) p = simple_fw rs p" by (simp)
let ?P'="{p. simple_matches (match_sel r) p}"
from Cons.IH Cons.prems have IH2: "⋀m. p ∉ (Collect (simple_matches m)) ⟹ simple_fw (rmshadow' rs (P ∪ Collect (simple_matches m))) p = simple_fw rs p" by simp
have nomatch_m: "⋀m. p ∉ P ⟹ {p. simple_matches m p} ⊆ P ⟹ ¬ simple_matches m p" by blast
from Cons.prems show ?case
apply(cases r, rename_tac m a)
apply(simp)
apply(case_tac "{p. simple_matches m p} ⊆ P")
apply(drule nomatch_m)
apply(assumption)
apply(simp)
apply(case_tac a)
apply(simp_all)
done
qed

corollary
fixes p :: "'i::len simple_packet"
shows "simple_fw (rmshadow rs UNIV) p = simple_fw (rmshadow' rs {}) p"

text‹Previous algorithm is not executable because we have no code for @{typ "'i::len simple_packet set"}.
To get some code, some efficient set operations would be necessary.
We either need union and subset or intersection and negation.
Both subset and negation are complicated.
Probably the BDDs which related work uses is really necessary.
›

(*Drafting set operations which might be necessary for an executable implementation. But BDDs might just be the thing here.*)
context
begin
private type_synonym 'i simple_packet_set = "'i simple_match list"

private definition simple_packet_set_toSet :: "'i::len simple_packet_set ⇒ 'i simple_packet set" where
"simple_packet_set_toSet ms = {p. ∃m ∈ set ms. simple_matches m p}"

private lemma simple_packet_set_toSet_alt: "simple_packet_set_toSet ms = (⋃ m ∈ set ms. {p. simple_matches m p})"
unfolding simple_packet_set_toSet_def by blast

private definition simple_packet_set_union :: "'i::len simple_packet_set ⇒'i  simple_match ⇒ 'i simple_packet_set" where
"simple_packet_set_union ps m = m # ps"

private lemma "simple_packet_set_toSet (simple_packet_set_union ps m) = simple_packet_set_toSet ps ∪ {p. simple_matches m p}"
unfolding simple_packet_set_toSet_def simple_packet_set_union_def by simp blast

(*either a sound but not complete executable implementation or a better idea to implement subset*)
private lemma "(∃m' ∈ set ms.
{i. match_iface iif i} ⊆ {i. match_iface (iiface m') i} ∧
{i. match_iface oif i} ⊆ {i. match_iface (oiface m') i} ∧
{ip. simple_match_ip sip ip} ⊆ {ip. simple_match_ip (src m') ip} ∧
{ip. simple_match_ip dip ip} ⊆ {ip. simple_match_ip (dst m') ip} ∧
{p. match_proto protocol p} ⊆ {p. match_proto (proto m') p} ∧
{p. simple_match_port sps p} ⊆ {p. simple_match_port (sports m') p} ∧
{p. simple_match_port dps p} ⊆ {p. simple_match_port (dports m') p}
)
⟹ {p. simple_matches ⦇iiface=iif, oiface=oif, src=sip, dst=dip, proto=protocol, sports=sps, dports=dps ⦈ p} ⊆ (simple_packet_set_toSet ms)"
unfolding simple_packet_set_toSet_def simple_packet_set_union_def
apply clarify
apply meson
done

text‹subset or negation ... One efficient implementation would suffice.›
private lemma "{p:: 'i::len simple_packet. simple_matches m p} ⊆ (simple_packet_set_toSet ms) ⟷
{p:: 'i::len simple_packet. simple_matches m p} ∩ (⋂ m ∈ set ms. {p. ¬ simple_matches m p}) = {}" (is "?l ⟷ ?r")
proof -
have "?l ⟷ {p. simple_matches m p} - (simple_packet_set_toSet ms) = {}" by blast
also have "… ⟷ {p. simple_matches m p} - (⋃ m ∈ set ms. {p:: 'i::len simple_packet. simple_matches m p}) = {}"
using simple_packet_set_toSet_alt by blast
also have "… ⟷ ?r" by blast
finally show ?thesis .
qed

end
end


# Theory IP_Partition_Preliminaries

(*  Title:      IP_Partition_Preliminaries
Authors:    Cornelius Diekmann, Max Haslbeck
*)
(*SetPartitioning.thy
Original Author: Max Haslbeck, 2015*)
section‹Partition a Set by a Specific Constraint›
theory IP_Partition_Preliminaries
imports Main
begin

text‹Will be used for the IP address space partition of a firewall.
However, this file is completely generic in terms of sets, it only imports Main.

It will be used in @{file ‹../Service_Matrix.thy›}.
Core idea: This file partitions @{typ "'a set set"} by some magic condition.
Later, we will show that this magic condition implies that all IPs that have been grouped
by the magic condition show the same behaviour for a simple firewall.›

(* disjoint, ipPartition definitions *)

definition disjoint :: "'a set set ⇒ bool" where
"disjoint ts ≡ ∀A ∈ ts. ∀B ∈ ts. A ≠ B ⟶ A ∩ B = {}"

text_raw‹We will call two partitioned sets \emph{complete} iff @{term "⋃ ss = ⋃ ts"}.›

text‹The condition we use to partition a set. If this holds and
@{term A} is the set of IP addresses in each rule in a firewall,
then @{term B} is a partition of @{term "⋃ A"} where each member has the same behavior
w.r.t the firewall ruleset.›
text‹@{term A} is the carrier set and @{term B}* should be a partition of @{term "⋃ A"}
which fulfills the following condition:›
definition ipPartition :: "'a set set ⇒ 'a set set ⇒ bool" where
"ipPartition A B ≡ ∀a ∈ A. ∀b ∈ B. a ∩ b = {} ∨ b ⊆ a"

definition disjoint_list :: "'a set list ⇒ bool" where
"disjoint_list ls ≡ distinct ls ∧ disjoint (set ls)"

context begin
(*internal*)
private fun disjoint_list_rec :: "'a set list ⇒ bool" where
"disjoint_list_rec [] = True" |
"disjoint_list_rec (x#xs) = (x ∩ ⋃(set xs) = {} ∧ disjoint_list_rec xs)"

private lemma disjoint_equi: "disjoint_list_rec ts ⟹ disjoint (set ts)"
apply(induction ts)
by fast

private lemma disjoint_list_disjoint_list_rec: "disjoint_list ts ⟹ disjoint_list_rec ts"
apply(induction ts)
by fast

private definition addSubsetSet :: "'a set ⇒ 'a set set ⇒ 'a set set" where
"addSubsetSet s ts = insert (s - ⋃ts) (((∩) s)  ts) ∪ ((λx. x - s)  ts)"

private fun partitioning :: "'a set list ⇒ 'a set set ⇒ 'a set set" where
"partitioning [] ts = ts" |
"partitioning (s#ss) ts = partitioning ss (addSubsetSet s ts)"

text‹simple examples›
lemma "partitioning [{1::nat,2},{3,4},{5,6,7},{6},{10}] {} = {{10}, {6}, {5, 7}, {}, {3, 4}, {1, 2}}" by eval
lemma "⋃ {{1::nat,2},{3,4},{5,6,7},{6},{10}} = ⋃ (partitioning [{1,2},{3,4},{5,6,7},{6},{10}] {})" by eval
lemma "disjoint (partitioning [{1::nat,2},{3,4},{5,6,7},{6},{10}] {})" by eval
lemma "ipPartition {{1::nat,2},{3,4},{5,6,7},{6},{10}} (partitioning [{1::nat,2},{3,4},{5,6,7},{6},{10}] {})" by eval

lemma "ipPartition A {}" by(simp add: ipPartition_def)

lemma ipPartitionUnion: "ipPartition As Cs ∧ ipPartition Bs Cs ⟷ ipPartition (As ∪ Bs) Cs"
unfolding ipPartition_def by fast

apply(safe)
apply blast
apply blast+
done

private lemma ipPartitioningAddSubset1: "disjoint ts ⟹ ipPartition (insert a ts) (addSubsetSet a ts)"
apply(safe)
apply blast
apply blast+
done

"s - ⋃ts ∈ addSubsetSet s ts"
"t ∈ ts ⟹ s ∩ t ∈ addSubsetSet s ts"
"t ∈ ts ⟹ t - s ∈ addSubsetSet s ts"

assumes "A ∈ addSubsetSet s ts"
obtains "A = s - ⋃ts" | T where "T ∈ ts" "A = s ∩ T" | T where "T ∈ ts" "A = T - s"
using assms unfolding addSubsetSet_def by blast

proof -
{
fix A a b assume "A ∈ addSubsetSet a (addSubsetSet b As)"
proof(goal_cases)
case 1
assume "A = a - ⋃(addSubsetSet b As)"
hence "A = (a - ⋃As) - b" by (auto simp add: Union_addSubsetSet)
thus ?thesis by (auto intro: addSubsetSetI)
next
case (2 T)
have "A = b ∩ (a - ⋃As) ∨ (∃S∈As. A = b ∩ (a ∩ S)) ∨ (∃S∈As. A = (a ∩ S) - b)"
by (rule addSubsetSetE[OF 2(1)]) (auto simp: 2(2))
thus ?thesis by (blast intro: addSubsetSetI)
next
case (3 T)
have "A = b - ⋃(addSubsetSet a As) ∨ (∃S∈As. A = b ∩ (S - a)) ∨ (∃S∈As. A = (S - a) - b)"
thus ?thesis by (blast intro: addSubsetSetI)
qed
}
thus ?thesis by blast
qed

by blast

private lemma disjointPartitioning_helper :"disjoint As ⟹ disjoint (partitioning ss As)"
proof(induction ss arbitrary: As)
case Nil thus ?case by(simp)
next
case (Cons s ss)
from Cons.IH d have "disjoint (partitioning ss (addSubsetSet s As))" .
thus ?case by simp
qed

private lemma disjointPartitioning: "disjoint (partitioning ss {})"
proof -
have "disjoint {}" by(simp add: disjoint_def)
from this disjointPartitioning_helper show ?thesis by fast
qed

private lemma coversallPartitioning:"⋃ (set ts) = ⋃ (partitioning ts {})"
proof -
have "⋃ (set ts ∪ As) = ⋃ (partitioning ts As)" for As
apply(induction ts arbitrary: As)
apply(simp_all)
thus ?thesis by (metis sup_bot.right_neutral)
qed

private lemma "⋃ As = ⋃ Bs ⟹ ipPartition As Bs ⟹ ipPartition As (addSubsetSet a Bs)"

private lemma ipPartitionSingleSet: "ipPartition {t} (addSubsetSet t Bs)
⟹ ipPartition {t} (partitioning ts (addSubsetSet t Bs))"
apply(induction ts arbitrary: Bs t)
apply(simp_all)

private lemma ipPartitioning_helper: "disjoint As ⟹ ipPartition (set ts) (partitioning ts As)"
proof(induction ts arbitrary: As)
case Nil thus ?case by(simp add: ipPartition_def)
next
case (Cons t ts)
from Cons.prems ipPartioningAddSubset0 have d: "ipPartition As (addSubsetSet t As)" by blast
have e: "ipPartition (set ts) (partitioning ts (addSubsetSet t As))" by blast
have "ipPartition {t} (addSubsetSet t As)" by blast
from this Cons.prems ipPartitionSingleSet
have f: "ipPartition {t} (partitioning ts (addSubsetSet t As))" by fast
have "set (t#ts) = insert t (set ts)" by auto
from ipPartitionUnion have "⋀ As Bs Cs. ipPartition As Cs ⟹ ipPartition Bs Cs ⟹ ipPartition (As ∪ Bs) Cs" by fast
with this e f
have "ipPartition (set (t # ts)) (partitioning ts (addSubsetSet t As))" by fastforce
thus ?case by simp
qed

private lemma ipPartitioning: "ipPartition (set ts) (partitioning ts {})"
proof -
have "disjoint {}" by(simp add: disjoint_def)
from this ipPartitioning_helper show ?thesis by fast
qed

(* OPTIMIZATION PROOFS *)

private lemma inter_dif_help_lemma: "A ∩ B = {}  ⟹ B - S = B - (S - A)"
by blast

private lemma disjoint_list_lem: "disjoint_list ls ⟹ ∀s ∈ set(ls). ∀t ∈ set(ls). s ≠ t ⟶ s ∩ t = {}"
proof(induction ls)

private lemma disjoint_list_empty: "disjoint_list []"

private lemma disjoint_sublist: "disjoint_list (t#ts) ⟹ disjoint_list ts"
proof(induction ts arbitrary: t)

private fun intersection_list :: "'a set ⇒ 'a set list ⇒ 'a set list" where
"intersection_list _ [] = []" |
"intersection_list s (t#ts) = (s ∩ t)#(intersection_list s ts)"

private fun intersection_list_opt :: "'a set ⇒ 'a set list ⇒ 'a set list" where
"intersection_list_opt _ [] = []" |
"intersection_list_opt s (t#ts) = (s ∩ t)#(intersection_list_opt (s - t) ts)"

private lemma disjoint_subset: "disjoint A ⟹ a ∈ A ⟹ b ⊆ a ⟹ disjoint ((A - {a}) ∪ {b})"
by blast

private lemma disjoint_intersection: "disjoint A ⟹ a ∈ A ⟹ disjoint ({a ∩ b} ∪ (A - {a}))"
by(blast)

private lemma intList_equi: "disjoint_list_rec ts ⟹ intersection_list s ts = intersection_list_opt s ts"
proof(induction ts)
case Nil thus ?case by simp
next
case (Cons t ts)
from Cons.prems have "intersection_list_opt s ts = intersection_list_opt (s - t) ts"
proof(induction ts arbitrary: s t)
case Nil thus ?case by simp
next
case Cons
have "∀t ∈ set ts. u ∩ t = {} ⟹ intersection_list_opt s ts = intersection_list_opt (s - u) ts"
for u
apply(induction ts arbitrary: s u)
apply(simp_all)
by (metis Diff_Int_distrib2 Diff_empty Diff_eq Un_Diff_Int sup_bot.right_neutral)
with Cons show ?case
apply(simp)
by (metis Diff_Int_distrib2 Diff_empty Un_empty inf_sup_distrib1)
qed
with Cons show ?case by simp
qed

private fun difference_list :: "'a set ⇒ 'a set list ⇒ 'a set list" where
"difference_list _ [] = []" |
"difference_list s (t#ts) = (t - s)#(difference_list s ts)"

private fun difference_list_opt :: "'a set ⇒ 'a set list ⇒ 'a set list" where
"difference_list_opt _ [] = []" |
"difference_list_opt s (t#ts) = (t - s)#(difference_list_opt (s - t) ts)"

private lemma difList_equi: "disjoint_list_rec ts ⟹ difference_list s ts = difference_list_opt s ts"
proof(induction ts arbitrary: s)
case Nil thus ?case by simp
next
case (Cons t ts)
have difference_list_opt_lem0: "∀t ∈ set(ts). u ∩ t = {} ⟹
difference_list_opt s ts = difference_list_opt (s - u) ts"
for u proof(induction ts arbitrary: s u)
case Cons thus ?case
by (metis Diff_Int_distrib2 Diff_eq Un_Diff_Int sup_bot.right_neutral)
qed(simp)
have "disjoint_list_rec (t # ts) ⟹ difference_list_opt s ts = difference_list_opt (s - t) ts"
proof(induction ts arbitrary: s t)
case Cons thus ?case
by (metis Un_empty inf_sup_distrib1 inter_dif_help_lemma)
qed(simp)
with Cons show ?case by simp
qed

private fun partList0 :: "'a set ⇒ 'a set list ⇒ 'a set list" where
"partList0 s [] = []" |
"partList0 s (t#ts) = (s ∩ t)#((t - s)#(partList0 s ts))"

private lemma partList0_set_equi: "set(partList0 s ts) = (((∩) s)  (set ts)) ∪ ((λx. x - s)  (set ts))"
by(induction ts arbitrary: s) auto

private lemma partList_sub_equi0: "set(partList0 s ts) =
set(difference_list s ts) ∪ set(intersection_list s ts)"
by(induction ts arbitrary: s) simp+

private fun partList1 :: "'a set ⇒ 'a set list ⇒ 'a set list" where
"partList1 s [] = []" |
"partList1 s (t#ts) = (s ∩ t)#((t - s)#(partList1 (s - t) ts))"

private lemma partList_sub_equi: "set(partList1 s ts) =
set(difference_list_opt s ts) ∪ set(intersection_list_opt s ts)"
by(induction ts arbitrary: s) (simp_all)

private lemma partList0_partList1_equi: "disjoint_list_rec ts ⟹ set (partList0 s ts) = set (partList1 s ts)"
by (simp add: partList_sub_equi partList_sub_equi0 intList_equi difList_equi)

private fun partList2 :: "'a set ⇒ 'a set list ⇒ 'a set list" where
"partList2 s [] = []" |
"partList2 s (t#ts) = (if s ∩ t = {} then  (t#(partList2 (s - t) ts))
else (s ∩ t)#((t - s)#(partList2 (s - t) ts)))"

private lemma partList2_empty: "partList2 {} ts = ts"
by(induction ts) (simp_all)

private lemma partList1_partList2_equi: "set(partList1 s ts) - {{}} = set(partList2 s ts) - {{}}"
by(induction ts arbitrary: s) (auto)

private fun partList3 :: "'a set ⇒ 'a set list ⇒ 'a set list" where
"partList3 s [] = []" |
"partList3 s (t#ts) = (if s = {} then (t#ts) else
(if s ∩ t = {} then (t#(partList3 (s - t) ts))
else
(if t - s = {} then (t#(partList3 (s - t) ts))
else (t ∩ s)#((t - s)#(partList3 (s - t) ts)))))"

private lemma partList2_partList3_equi: "set(partList2 s ts) - {{}} = set(partList3 s ts) - {{}}"
apply(induction ts arbitrary: s)
apply(simp; fail)
by blast

fun partList4 :: "'a set ⇒ 'a set list ⇒ 'a set list" where
"partList4 s [] = []" |
"partList4 s (t#ts) = (if s = {} then (t#ts) else
(if s ∩ t = {} then (t#(partList4 s ts))
else
(if t - s = {} then (t#(partList4 (s - t) ts))
else (t ∩ s)#((t - s)#(partList4 (s - t) ts)))))"

private lemma partList4: "partList4 s ts = partList3 s ts"
apply(induction ts arbitrary: s)
apply(simp; fail)
done

private lemma partList0_addSubsetSet_equi: "s ⊆ ⋃(set ts) ⟹
addSubsetSet s (set ts) - {{}} = set(partList0 s ts) - {{}}"

private fun partitioning_nontail :: "'a set list ⇒ 'a set set ⇒ 'a set set" where
"partitioning_nontail [] ts = ts" |
"partitioning_nontail (s#ss) ts = addSubsetSet s (partitioning_nontail ss ts)"

private lemma partitioningCom: "addSubsetSet a (partitioning ss ts) = partitioning ss (addSubsetSet a ts)"
apply(induction ss arbitrary: a ts)
apply(simp; fail)
done

private lemma partitioning_nottail_equi: "partitioning_nontail ss ts = partitioning ss ts"
apply(induction ss arbitrary: ts)
apply(simp; fail)
done

fun partitioning1 :: "'a set list ⇒ 'a set list ⇒ 'a set list" where
"partitioning1 [] ts = ts" |
"partitioning1 (s#ss) ts = partList4 s (partitioning1 ss ts)"

lemma partList4_empty: "{} ∉ set ts ⟹ {} ∉ set (partList4 s ts)"
apply(induction ts arbitrary: s)
apply(simp; fail)
by auto

lemma partitioning1_empty0: "{} ∉ set ts ⟹ {} ∉ set (partitioning1 ss ts)"
apply(induction ss arbitrary: ts)
apply(simp; fail)
done

lemma partitioning1_empty1: "{} ∉ set ts ⟹
set(partitioning1 ss ts) - {{}} = set(partitioning1 ss ts)"

lemma partList4_subset: "a ⊆ ⋃(set ts) ⟹ a ⊆ ⋃(set (partList4 b ts))"
apply(induction ts arbitrary: a b)
apply(simp; fail)
apply(simp)
by fast

private lemma "a ≠ {} ⟹ disjoint_list_rec (a # ts) ⟷ disjoint_list_rec ts ∧ a ∩ ⋃ (set ts) = {}" by auto

lemma partList4_complete0: "s ⊆ ⋃(set ts) ⟹ ⋃(set (partList4 s ts)) = ⋃(set ts)"
unfolding partList4
proof(induction ts arbitrary: s)
case Nil thus ?case by(simp)
next
case Cons thus ?case by (simp add: Diff_subset_conv Un_Diff_Int inf_sup_aci(7) sup.commute)
qed

private lemma partList4_disjoint: "s ⊆ ⋃(set ts) ⟹ disjoint_list_rec ts ⟹
disjoint_list_rec (partList4 s ts)"
apply(induction ts arbitrary: s)
apply(simp; fail)
apply(rule conjI)
apply (metis Diff_subset_conv Int_absorb1 Int_lower2 Un_absorb1 partList4_complete0)
apply(safe)
using partList4_complete0 apply (metis Diff_subset_conv Diff_triv IntI UnionI)
apply (metis Diff_subset_conv Diff_triv)
using partList4_complete0 by (metis Diff_subset_conv IntI UnionI)+

lemma union_set_partList4: "⋃(set (partList4 s ts)) = ⋃(set ts)"
by (induction ts arbitrary: s, auto)

private lemma partList4_distinct_hlp: assumes "a ≠ {}" "a ∉ set ts" "disjoint (insert a (set ts))"
shows "a ∉ set (partList4 s ts)"
proof -
from assms have "¬ a ⊆ ⋃(set ts)" unfolding disjoint_def by fastforce
hence "¬ a ⊆ ⋃(set (partList4 s ts))" using union_set_partList4 by metis
thus ?thesis by blast
qed

private lemma partList4_distinct: "{} ∉ set ts ⟹ disjoint_list ts ⟹ distinct (partList4 s ts)"
proof(induction ts arbitrary: s)
case Nil thus ?case by simp
next
case(Cons t ts)
have x1: "⋀x xa xb xc.
t ∉ set ts ⟹
disjoint (insert t (set ts)) ⟹
xa ∈ t ⟹
xb ∈ s ⟹
xb ∈ t ⟹
xb ∉ {} ⟹
xc ∈ s ⟹
xc ∉ {} ⟹
t ∩ s ∈ set (partList4 (s - t) ts) ⟹
¬ t ∩ s ⊆ ⋃(set (partList4 (s - t) ts))"
by(simp add: union_set_partList4 disjoint_def, force) (*1s*)
have x2: "⋀x xa xb xc.
t ∉ set ts ⟹
disjoint (insert t (set ts)) ⟹
x ∈ t ⟹
xa ∈ t ⟹
xa ∉ s ⟹
xb ∈ s ⟹
xc ∈ s ⟹
¬ t - s ⊆ ⋃(set (partList4 (s - t) ts))"
by(simp add: union_set_partList4 disjoint_def, force) (*1s*)
from Cons have IH: "distinct (partList4 s ts)" for s
using disjoint_sublist list.set_intros(2) by auto
from Cons.prems(1,2) IH show ?case
unfolding disjoint_list_def
apply(simp)
apply(safe)
apply(metis partList4_distinct_hlp)
apply(metis partList4_distinct_hlp)
apply(metis partList4_distinct_hlp)
apply blast
using x1 apply blast
using x2 by blast
qed

lemma partList4_disjoint_list: assumes "s ⊆ ⋃(set ts)" "disjoint_list ts" "{} ∉ set ts"
shows "disjoint_list (partList4 s ts)"
unfolding disjoint_list_def
proof
from assms(2,3) show "distinct (partList4 s ts)"
using partList4_distinct disjoint_list_def by auto
show "disjoint (set (partList4 s ts))"
proof -
have disjoint_list_disjoint_list_rec: "disjoint_list ts ⟹ disjoint_list_rec ts"
proof(induction ts)
case Cons thus ?case by(auto simp add: disjoint_list_def disjoint_def)
qed(simp)
with partList4_disjoint disjoint_equi assms(1,2) show ?thesis by blast
qed
qed

lemma partitioning1_subset: "a ⊆ ⋃ (set ts) ⟹ a ⊆ ⋃ (set (partitioning1 ss ts))"
apply(induction ss arbitrary: ts a)
apply(simp)
done

lemma partitioning1_disjoint_list: "{} ∉ (set ts) ⟹ ⋃ (set ss) ⊆ ⋃ (set ts) ⟹
disjoint_list ts ⟹ disjoint_list (partitioning1 ss ts)"
proof(induction ss)
case Nil thus ?case by simp
next
case(Cons t ts) thus ?case
apply(clarsimp)
apply(rule partList4_disjoint_list)
using partitioning1_subset apply(metis)
apply(blast)
using partitioning1_empty0 apply(metis)
done
qed

private lemma partitioning1_disjoint: "⋃ (set ss) ⊆ ⋃ (set ts) ⟹
disjoint_list_rec ts ⟹ disjoint_list_rec (partitioning1 ss ts)"
proof(induction ss arbitrary: ts)

private lemma partitioning_equi: "{} ∉ set ts ⟹ disjoint_list_rec ts ⟹ ⋃ (set ss) ⊆ ⋃ (set ts) ⟹
set(partitioning1 ss ts) = partitioning_nontail ss (set ts) - {{}}"
proof(induction ss)
case Nil thus ?case by simp
next
case (Cons s ss)
for s and ts::"'a set set"
have r: "disjoint_list_rec ts ⟹ s ⊆ ⋃(set ts) ⟹
addSubsetSet s (set ts) - {{}} = set (partList4 s ts) - {{}}"
for ts::"'a set list"
unfolding partList4
partList2_partList3_equi)
have 1: "disjoint_list_rec (partitioning1 ss ts)"
using partitioning1_disjoint Cons.prems by auto
from Cons.prems have 2: "s ⊆ ⋃(set (partitioning1 ss ts))"
by (meson Sup_upper dual_order.trans list.set_intros(1) partitioning1_subset)
from Cons have IH: "set (partitioning1 ss ts) = partitioning_nontail ss (set ts) - {{}}" by auto
qed

lemma ipPartitioning_helper_opt: "{} ∉ set ts ⟹ disjoint_list ts ⟹ ⋃ (set ss) ⊆ ⋃ (set ts)
⟹ ipPartition (set ss) (set (partitioning1 ss ts))"
apply(drule disjoint_list_disjoint_list_rec)
by (meson Diff_subset disjoint_equi ipPartition_def ipPartitioning_helper subsetCE)

lemma complete_helper: "{} ∉ set ts ⟹ ⋃ (set ss) ⊆ ⋃ (set ts)⟹
⋃ (set ts) = ⋃ (set (partitioning1 ss ts))"
apply(induction ss arbitrary: ts)
apply(simp_all)
by (metis partList4_complete0)

lemma "partitioning1  [{1::nat},{2},{}] [{1},{},{2},{3}] = [{1}, {}, {2}, {3}]" by eval

lemma partitioning_foldr: "partitioning X B = foldr addSubsetSet X B"
apply(induction X)
apply(simp; fail)
apply(simp)
by (metis partitioningCom)

lemma "ipPartition (set X) (foldr addSubsetSet X {})"
apply(subst partitioning_foldr[symmetric])
using ipPartitioning by auto

lemma "⋃ (set X) = ⋃ (foldr addSubsetSet X {})"
apply(subst partitioning_foldr[symmetric])

lemma "partitioning1 X B = foldr partList4 X B"
by(induction X)(simp_all)

lemma "ipPartition (set X) (set (partitioning1 X [UNIV]))"
apply(rule ipPartitioning_helper_opt)

lemma "(⋃(set (partitioning1 X [UNIV]))) = UNIV"
apply(subgoal_tac "UNIV = ⋃ (set (partitioning1 X [UNIV]))")
prefer 2
apply(rule complete_helper[where ts="[UNIV]", simplified])
apply(simp)
done

end
end


# Theory GroupF

section‹Group by Function›
theory GroupF
imports Main
begin

text‹Grouping elements of a list according to a function.›

fun groupF ::  "('a ⇒ 'b) ⇒ 'a list ⇒ 'a list list"  where
"groupF f [] = []" |
"groupF f (x#xs) = (x#(filter (λy. f x = f y) xs))#(groupF f (filter (λy. f x ≠ f y) xs))"

text‹trying a more efficient implementation of @{term groupF}›
context
begin
private fun select_p_tuple :: "('a ⇒ bool) ⇒ 'a ⇒ ('a list × 'a list) ⇒ ('a list × 'a list)"
where
"select_p_tuple p x (ts,fs) = (if p x then (x#ts, fs) else (ts, x#fs))"

private definition partition_tailrec :: "('a ⇒ bool) ⇒ 'a list ⇒ ('a list × 'a list)"
where
"partition_tailrec p xs = foldr (select_p_tuple p) xs ([],[])"

private lemma partition_tailrec: "partition_tailrec f as =  (filter f as,  filter (λx. ¬f x) as)"
proof -
{fix ts_accu fs_accu
have "foldr (select_p_tuple f) as (ts_accu, fs_accu) =
(filter f as @ ts_accu,  filter (λx. ¬f x) as @ fs_accu)"
by(induction as arbitrary: ts_accu fs_accu) simp_all
} thus ?thesis unfolding partition_tailrec_def by simp
qed

private lemma
"groupF f (x#xs) = (let (ts, fs) = partition_tailrec (λy. f x = f y) xs in (x#ts)#(groupF f fs))"

(*is this more efficient?*)
private function groupF_code ::  "('a ⇒ 'b) ⇒ 'a list ⇒ 'a list list"  where
"groupF_code f [] = []" |
"groupF_code f (x#xs) = (let
(ts, fs) = partition_tailrec (λy. f x = f y) xs
in
(x#ts)#(groupF_code f fs))"
by(pat_completeness) auto

private termination groupF_code
apply(relation "measure (λ(f,as). length (filter (λx. (λy. f x = f y) x) as))")
apply(simp; fail)
using le_imp_less_Suc length_filter_le by blast

lemma groupF_code[code]: "groupF f as = groupF_code f as"
by(induction f as rule: groupF_code.induct) (simp_all add: partition_tailrec)

export_code groupF checking SML
end

lemma groupF_concat_set: "set (concat (groupF f xs)) = set xs"
proof(induction f xs rule: groupF.induct)
case 2 thus ?case by (simp) blast
qed(simp)

lemma groupF_Union_set: "(⋃x ∈ set (groupF f xs). set x) = set xs"
proof(induction f xs rule: groupF.induct)
case 2 thus ?case by (simp) blast
qed(simp)

lemma groupF_set: "∀X ∈ set (groupF f xs). ∀x ∈ set X. x ∈ set xs"
using groupF_concat_set by fastforce

lemma groupF_equality:
defines "same f A ≡ ∀a1 ∈ set A. ∀a2 ∈ set A. f a1 = f a2"
shows "∀A ∈ set (groupF f xs). same f A"
proof(induction f xs rule: groupF.induct)
case 1 thus ?case by simp
next
case (2 f x xs)
have groupF_fst:
"groupF f (x # xs) = (x # [y←xs . f x = f y]) # groupF f [y←xs . f x ≠ f y]" by force
have step: " ∀A∈set [x # [y←xs . f x = f y]]. same f A" unfolding same_def by fastforce
with 2 show ?case unfolding groupF_fst by fastforce
qed

lemma groupF_nequality: "A ∈ set (groupF f xs) ⟹ B ∈ set (groupF f xs) ⟹ A ≠ B ⟹
∀a ∈ set A. ∀b ∈ set B. f a ≠ f b"
proof(induction f xs rule: groupF.induct)
case 1 thus ?case by simp
next
case 2 thus ?case
apply -
apply(subst (asm) groupF.simps)+
using groupF_set by fastforce (*1s*)
qed

lemma groupF_cong: fixes xs::"'a list" and f1::"'a ⇒ 'b" and f2::"'a ⇒ 'c"
assumes "∀x ∈ set xs. ∀y ∈ set xs. (f1 x = f1 y ⟷ f2 x = f2 y)"
shows "groupF f1 xs = groupF f2 xs"
using assms proof(induction f1 xs rule: groupF.induct)
case (2 f x xs) thus ?case using filter_cong[of xs xs "λy. f x = f y" "λy. f2 x = f2 y"]
filter_cong[of xs xs "λy. f x ≠ f y" "λy. f2 x ≠ f2 y"] by auto
qed (simp)

lemma groupF_empty: "groupF f xs ≠ [] ⟷ xs ≠ []"
by(induction f xs rule: groupF.induct) auto
lemma groupF_empty_elem: "x ∈ set (groupF f xs) ⟹ x ≠ []"
by(induction f xs rule: groupF.induct) auto

lemma groupF_distinct: "distinct xs ⟹ distinct (concat (groupF f xs))"
by (induction f xs rule: groupF.induct) (auto simp add: groupF_Union_set)

text‹It is possible to use
@{term "map (map fst) (groupF snd (map (λx. (x, f x)) P))"}
@{term "groupF f P"}
for the following reasons:
@{const groupF} executes its compare function (first parameter) very often;
it always tests for @{term "(f x = f y)"}.
The function @{term f} may be really expensive.
At least polyML does not share the result of @{term f} but (probably) always recomputes (part of) it.
The optimization pre-computes @{term f} and tells @{const groupF} to use
a really cheap function (@{const snd}) to compare.
The following lemma tells that those are equal.›
(* is this also faster for Haskell?*)

lemma groupF_tuple: "groupF f xs = map (map fst) (groupF snd (map (λx. (x, f x)) xs))"
proof(induction f xs rule: groupF.induct)
case (1 f) thus ?case by simp
next
case (2 f x xs)
have g1: "[y←xs . f x = f y] = map fst [y←map (λx. (x, f x)) xs . f x = snd y]"
proof(induction xs arbitrary: f x)
case Cons thus ?case by fastforce
qed(simp)
have g2: "(map (λx. (x, f x)) [y←xs . f x ≠ f y]) = [y←map (λx. (x, f x)) xs . f x ≠ snd y]"
proof(induction xs)
case Cons thus ?case by fastforce
qed(simp)
from 2 g1 g2 show ?case by simp
qed
end


section‹Helper: Pretty Printing Word Intervals which correspond to IP address Ranges›
begin

(*The "u" stands for union. I guess you may want to customize this pretty printing syntax :D*)

fun ipv4addr_wordinterval_toString :: "32 wordinterval ⇒ string" where

fun ipv6addr_wordinterval_toString :: "128 wordinterval ⇒ string" where

end


# Theory Primitives_toString

section‹toString Functions for Primitives›
theory Primitives_toString
imports "../Common/Lib_Enum_toString"
Iface
L4_Protocol
begin

definition ipv4_cidr_toString :: "(ipv4addr × nat) ⇒ string" where
"ipv4_cidr_toString ip_n = (case ip_n of (base, n) ⇒  (ipv4addr_toString base @''/''@ string_of_nat n))"
lemma "ipv4_cidr_toString (ipv4addr_of_dotdecimal (192,168,0,1), 22) = ''192.168.0.1/22''" by eval

definition ipv6_cidr_toString :: "(ipv6addr × nat) ⇒ string" where
"ipv6_cidr_toString ip_n = (case ip_n of (base, n) ⇒  (ipv6addr_toString base @''/''@ string_of_nat n))"
lemma "ipv6_cidr_toString (42540766411282592856906245548098208122, 64) = ''2001:db8::8:800:200c:417a/64''" by eval

definition primitive_protocol_toString :: "primitive_protocol ⇒ string" where
"primitive_protocol_toString protid ≡ (
if protid = TCP then ''tcp'' else
if protid = UDP then ''udp'' else
if protid = ICMP then ''icmp'' else
if protid = L4_Protocol.SCTP then ''sctp'' else
if protid = L4_Protocol.IGMP then ''igmp'' else
if protid = L4_Protocol.GRE then ''gre'' else
if protid = L4_Protocol.ESP then ''esp'' else
if protid = L4_Protocol.AH then ''ah'' else
if protid = L4_Protocol.IPv6ICMP then ''ipv6-icmp'' else
''protocolid:''@dec_string_of_word0 protid)"

fun protocol_toString :: "protocol ⇒ string" where
"protocol_toString (ProtoAny) = ''all''" |
"protocol_toString (Proto protid) = primitive_protocol_toString protid"

definition iface_toString :: "string ⇒ iface ⇒ string" where
"iface_toString descr iface = (if iface = ifaceAny then '''' else
(case iface of (Iface name) ⇒ descr@name))"
lemma "iface_toString ''in: '' (Iface ''+'') = ''''" by eval
lemma "iface_toString ''in: '' (Iface ''eth0'') = ''in: eth0''" by eval

definition port_toString :: "16 word ⇒ string" where
"port_toString p ≡ dec_string_of_word0 p"

fun ports_toString :: "string ⇒ (16 word × 16 word) ⇒ string" where
"ports_toString descr (s,e) = (if s = 0 ∧ e = max_word then '''' else descr @ (if s=e then port_toString s else port_toString s@'':''@port_toString e))"
lemma "ports_toString ''spt: '' (0,65535) = ''''" by eval
lemma "ports_toString ''spt: '' (1024,2048) = ''spt: 1024:2048''" by eval
lemma "ports_toString ''spt: '' (1024,1024) = ''spt: 1024''" by eval

definition ipv4_cidr_opt_toString :: "string ⇒ ipv4addr × nat ⇒ string" where
"ipv4_cidr_opt_toString descr ip = (if ip = (0,0) then '''' else
descr@ipv4_cidr_toString ip)"

definition protocol_opt_toString :: "string ⇒ protocol ⇒ string" where
"protocol_opt_toString descr prot = (if prot = ProtoAny then '''' else
descr@protocol_toString prot)"

end


# Theory Service_Matrix

(*  Title:      Service_Matrix.thy
Authors:    Cornelius Diekmann, Max Haslbeck
*)
(*IPPartitioning.thy
Original Author: Max Haslbeck, 2015*)
section‹Service Matrices›
theory Service_Matrix
imports "Common/List_Product_More"
"Common/IP_Partition_Preliminaries"
"Common/GroupF"
"Primitives/Primitives_toString"
SimpleFw_Semantics
begin

(* could be generalized more *)
fun extract_IPSets_generic0
:: "('i::len simple_match ⇒ 'i word × nat) ⇒ 'i simple_rule list ⇒ ('i wordinterval) list"
where
"extract_IPSets_generic0 _ [] = []" |
"extract_IPSets_generic0 sel ((SimpleRule m _)#ss) = (ipcidr_tuple_to_wordinterval (sel m)) #
(extract_IPSets_generic0 sel ss)"

lemma extract_IPSets_generic0_length: "length (extract_IPSets_generic0 sel rs) = length rs"
by(induction rs rule: extract_IPSets_generic0.induct) (simp_all)

(*
The order in which extract_IPSets returns the collected IP ranges heavily influences the running time
of the subsequent algorithms.
For example:
1) iterating through the ruleset and collecting all source and destination ips:
10:10:49 elapsed time, 38:41:17 cpu time, factor 3.80
2) iterating through the ruleset and first returning all source ips and iterating again and then return all destination ips:
3:39:56 elapsed time, 21:08:34 cpu time, factor 5.76

To get a more deterministic runtime, we are sorting the output. As a performance optimization, we also remove duplicate entries.
We use mergesort_remdups, which does a mergesort (i.e sorts!) and removes duplicates and mergesort_by_rel which does a mergesort
(without removing duplicates) and allows to specify the relation we use to sort.
In theory, the largest ip ranges (smallest prefix length) should be put first, the following evaluation shows that this may not
be the fastest solution. The reason might be that access_matrix_pretty_ipv4 picks (almost randomly) one IP from the result and
there are fast and slower choices. The faster choices are the ones where the firewall ruleset has a decision very early.
Therefore, the running time is still a bit unpredictable.

Here is the data:
map ipcidr_tuple_to_wordinterval (mergesort_by_rel (λ (a1,a2) (b1, b2). (a2, a1) ≤ (b2, b1)) (mergesort_remdups
((map (src ∘ match_sel) rs) @ (map (dst ∘ match_sel) rs))))
(2:47:04 elapsed time, 17:08:01 cpu time, factor 6.15)

map ipcidr_tuple_to_wordinterval (mergesort_remdups ((map (src ∘ match_sel) rs) @ (map (dst ∘ match_sel) rs)))
(2:41:03 elapsed time, 16:56:46 cpu time, factor 6.31)

map ipcidr_tuple_to_wordinterval (mergesort_by_rel (λ (a1,a2) (b1, b2). (a2, a1) ≤ (b2, b1)) (
((map (src ∘ match_sel) rs) @ (map (dst ∘ match_sel) rs)))
(5:52:28 elapsed time, 41:50:10 cpu time, factor 7.12)

map ipcidr_tuple_to_wordinterval (mergesort_by_rel (≤)
((map (src ∘ match_sel) rs) @ (map (dst ∘ match_sel) rs))))
(3:10:57 elapsed time, 19:12:25 cpu time, factor 6.03)

map ipcidr_tuple_to_wordinterval (mergesort_by_rel (λ (a1,a2) (b1, b2). (a2, a1) ≤ (b2, b1)) (mergesort_remdups
(extract_src_dst_ips rs [])))
(2:49:57 elapsed time, 17:10:49 cpu time, factor 6.06)

map ipcidr_tuple_to_wordinterval ((mergesort_remdups (extract_src_dst_ips rs [])))
(2:43:44 elapsed time, 16:57:49 cpu time, factor 6.21)

map ipcidr_tuple_to_wordinterval (mergesort_by_rel (λ (a1,a2) (b1, b2). (a2, a1) ≥ (b2, b1)) (mergesort_remdups (extract_src_dst_ips rs [])))
(2:47:37 elapsed time, 16:54:47 cpu time, factor 6.05)

There is a clear looser: not using mergesort_remdups
There is no clear winner. We will just stick to mergesort_remdups.

*)

(*check the the order of mergesort_remdups did not change*)
lemma "mergesort_remdups [(1::ipv4addr, 2::nat), (8,0), (8,1), (2,2), (2,4), (1,2), (2,2)] =
[(1, 2), (2, 2), (2, 4), (8, 0), (8, 1)]" by eval

(*a tail-recursive implementation*)
fun extract_src_dst_ips
:: "'i::len simple_rule list ⇒ ('i word × nat) list ⇒ ('i word × nat) list" where
"extract_src_dst_ips [] ts = ts" |
"extract_src_dst_ips ((SimpleRule m _)#ss) ts = extract_src_dst_ips ss  (src m # dst m # ts)"

lemma extract_src_dst_ips_length: "length (extract_src_dst_ips rs acc) = 2*length rs + length acc"
proof(induction rs arbitrary: acc)
case (Cons r rs) thus ?case by(cases r, simp)
qed(simp)

definition extract_IPSets
:: "'i::len simple_rule list ⇒ ('i wordinterval) list" where
"extract_IPSets rs ≡ map ipcidr_tuple_to_wordinterval (mergesort_remdups (extract_src_dst_ips rs []))"
lemma extract_IPSets:
"set (extract_IPSets rs) = set (extract_IPSets_generic0 src rs) ∪ set (extract_IPSets_generic0 dst rs)"
proof -
{ fix acc
have "ipcidr_tuple_to_wordinterval  set (extract_src_dst_ips rs acc) =
ipcidr_tuple_to_wordinterval  set acc ∪ set (extract_IPSets_generic0 src rs) ∪
set (extract_IPSets_generic0 dst rs)"
proof(induction rs arbitrary: acc)
case (Cons r rs ) thus ?case
apply(cases r)
apply(simp)
by fast
qed(simp)
} thus ?thesis unfolding extract_IPSets_def by(simp_all add: extract_IPSets_def mergesort_remdups_correct)
qed

lemma "(a::nat) div 2 + a mod 2 ≤ a" by fastforce

lemma merge_length: "length (merge l1 l2) ≤ length l1 + length l2"
by(induction l1 l2 rule: merge.induct) auto

lemma merge_list_length: "length (merge_list as ls) ≤ length (concat (as @ ls))"
proof(induction as ls rule: merge_list.induct)
case (5 l1 l2 acc2 ls)
have "length (merge l2 acc2) ≤ length l2 + length acc2" using merge_length by blast
with 5 show ?case by simp
qed(simp_all)

lemma mergesort_remdups_length: "length (mergesort_remdups as) ≤ length as"
unfolding mergesort_remdups_def
proof -
have "concat ([] @ (map (λx. [x]) as)) = as" by simp
with merge_list_length show "length (merge_list [] (map (λx. [x]) as)) ≤ length as" by metis
qed

lemma extract_IPSets_length: "length (extract_IPSets rs) ≤ 2 * length rs"
using extract_src_dst_ips_length mergesort_remdups_length by (metis add.right_neutral list.size(3))

(*
export_code extract_IPSets in SML
why you no work?
*)

lemma extract_equi0:
"set (map wordinterval_to_set (extract_IPSets_generic0 sel rs)) =
(λ(base,len). ipset_from_cidr base len)  sel  match_sel  set rs"
proof(induction rs)
case (Cons r rs) thus ?case
apply(cases r, simp)
using wordinterval_to_set_ipcidr_tuple_to_wordinterval by fastforce
qed(simp)

lemma src_ipPart_motivation:
fixes   rs
defines "X ≡ (λ(base,len). ipset_from_cidr base len)  src  match_sel  set rs"
assumes "∀A ∈ X. B ⊆ A ∨ B ∩ A = {}" and "s1 ∈ B" and "s2 ∈ B"
shows "simple_fw rs (p⦇p_src:=s1⦈) = simple_fw rs (p⦇p_src:=s2⦈)"
proof -
have "∀A ∈ (λ(base,len). ipset_from_cidr base len)  src  match_sel  set rs. B ⊆ A ∨ B ∩ A = {} ⟹ ?thesis"
proof(induction rs)
case Nil thus ?case by simp
next
case (Cons r rs)
{ fix m
from ‹s1 ∈ B› ‹s2 ∈ B› have
"B ⊆ (case src m of (x, xa) ⇒ ipset_from_cidr x xa) ∨ B ∩ (case src m of (x, xa)
⇒ ipset_from_cidr x xa) = {} ⟹
simple_matches m (p⦇p_src := s1⦈) ⟷ simple_matches m (p⦇p_src := s2⦈)"
apply(cases m)
apply(rename_tac iiface oiface srca dst proto sports dports)
apply(case_tac srca)
by blast
} note helper=this
from Cons[simplified] show ?case
apply(cases r, rename_tac m a)
apply(simp)
apply(case_tac a)
using helper apply force+
done
qed
with assms show ?thesis by blast
qed

lemma src_ipPart:
assumes "ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 src rs))) A"
"B ∈ A" "s1 ∈ B" "s2 ∈ B"
shows "simple_fw rs (p⦇p_src:=s1⦈) = simple_fw rs (p⦇p_src:=s2⦈)"
proof -
from src_ipPart_motivation[OF _ assms(3) assms(4)]
have "∀A ∈ (λ(base,len). ipset_from_cidr base len)  src  match_sel  set rs. B ⊆ A ∨ B ∩ A = {} ⟹
simple_fw rs (p⦇p_src:=s1⦈) = simple_fw rs (p⦇p_src:=s2⦈)" by fast
thus ?thesis using assms(1) assms(2)
unfolding ipPartition_def
by (metis (full_types) Int_commute extract_equi0)
qed

(*basically a copy of src_ipPart*)
lemma dst_ipPart:
assumes "ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 dst rs))) A"
"B ∈ A" "s1 ∈ B" "s2 ∈ B"
shows "simple_fw rs (p⦇p_dst:=s1⦈) = simple_fw rs (p⦇p_dst:=s2⦈)"
proof -
have "∀A ∈ (λ(base,len). ipset_from_cidr base len)  dst  match_sel  set rs. B ⊆ A ∨ B ∩ A = {} ⟹
simple_fw rs (p⦇p_dst:=s1⦈) = simple_fw rs (p⦇p_dst:=s2⦈)"
proof(induction rs)
case Nil thus ?case by simp
next
case (Cons r rs)
{ fix m
from ‹s1 ∈ B› ‹s2 ∈ B› have
"B ⊆ (case dst m of (x, xa) ⇒ ipset_from_cidr x xa) ∨ B ∩ (case dst m of (x, xa)
⇒ ipset_from_cidr x xa) = {} ⟹
simple_matches m (p⦇p_dst := s1⦈) ⟷ simple_matches m (p⦇p_dst := s2⦈)"
apply(cases m)
apply(rename_tac iiface oiface src dsta proto sports dports)
apply(case_tac dsta)
by blast
} note helper=this
from Cons show ?case
apply(simp)
apply(case_tac r, rename_tac m a)
apply(simp)
apply(case_tac a)
using helper apply force+
done
qed
thus ?thesis using assms(1) assms(2)
unfolding ipPartition_def
by (metis (full_types) Int_commute extract_equi0)
qed

(* OPTIMIZED PARTITIONING *)

definition wordinterval_list_to_set :: "'a::len wordinterval list ⇒ 'a::len word set" where
"wordinterval_list_to_set ws = ⋃(set (map wordinterval_to_set ws))"

lemma wordinterval_list_to_set_compressed:
"wordinterval_to_set (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval)) =
wordinterval_list_to_set xs"
proof(induction xs)

fun partIps :: "'a::len wordinterval ⇒ 'a::len wordinterval list
⇒ 'a::len wordinterval list" where
"partIps _ [] = []" |
"partIps s (t#ts) = (if wordinterval_empty s then (t#ts) else
(if wordinterval_empty (wordinterval_intersection s t)
then (t#(partIps s ts))
else
(if wordinterval_empty (wordinterval_setminus t s)
then (t#(partIps (wordinterval_setminus s t) ts))
else (wordinterval_intersection t s)#((wordinterval_setminus t s)#
(partIps (wordinterval_setminus s t) ts)))))"

lemma "partIps (WordInterval (1::ipv4addr) 1) [WordInterval 0 1] = [WordInterval 1 1, WordInterval 0 0]" by eval

lemma partIps_length: "length (partIps s ts) ≤ (length ts) * 2"
proof(induction ts arbitrary: s)
case Cons thus ?case
apply(simp)
using le_Suc_eq by blast
qed(simp)

fun partitioningIps :: "'a::len wordinterval list ⇒ 'a::len wordinterval list ⇒
'a::len wordinterval list" where
"partitioningIps [] ts = ts" |
"partitioningIps (s#ss) ts = partIps s (partitioningIps ss ts)"

lemma partitioningIps_length: "length (partitioningIps ss ts) ≤ (2^length ss) * length ts"
proof(induction ss)
case Nil thus ?case by simp
next
case (Cons s ss)
have "length (partIps s (partitioningIps ss ts)) ≤ length (partitioningIps ss ts) * 2"
using partIps_length by fast
with Cons show  ?case by force
qed

lemma partIps_equi: "map wordinterval_to_set (partIps s ts) =
partList4 (wordinterval_to_set s) (map wordinterval_to_set ts)"
proof(induction ts arbitrary: s)
qed(simp_all)

lemma partitioningIps_equi: "map wordinterval_to_set (partitioningIps ss ts)
= (partitioning1 (map wordinterval_to_set ss) (map wordinterval_to_set ts))"
apply(induction ss arbitrary: ts)
apply(simp; fail)
done

definition getParts :: "'i::len simple_rule list ⇒ 'i wordinterval list" where
"getParts rs = partitioningIps (extract_IPSets rs) [wordinterval_UNIV]"

lemma partitioningIps_foldr: "partitioningIps ss ts = foldr partIps ss ts"
by(induction ss) (simp_all)

lemma getParts_foldr: "getParts rs = foldr partIps (extract_IPSets rs) [wordinterval_UNIV]"

lemma getParts_length: "length (getParts rs) ≤ 2^(2 * length rs)"
proof -
from partitioningIps_length[where ss="extract_IPSets rs" and ts="[wordinterval_UNIV]"] have
1: "length (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]) ≤ 2 ^ length (extract_IPSets rs)" by simp
from extract_IPSets_length have "(2::nat) ^ length (extract_IPSets rs) ≤ 2 ^ (2 * length rs)" by simp
with 1 have "length (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]) ≤ 2 ^ (2 * length rs)" by linarith
qed

lemma getParts_ipPartition: "ipPartition (set (map wordinterval_to_set (extract_IPSets rs)))
(set (map wordinterval_to_set (getParts rs)))"
proof -
have hlp_rule: "{} ∉ set (map wordinterval_to_set ts) ⟹ disjoint_list (map wordinterval_to_set ts) ⟹
(wordinterval_list_to_set ss) ⊆ (wordinterval_list_to_set ts) ⟹
ipPartition (set (map wordinterval_to_set ss))
(set (map wordinterval_to_set (partitioningIps ss ts)))" for ts ss::"'a wordinterval list"
by (metis ipPartitioning_helper_opt partitioningIps_equi wordinterval_list_to_set_def)
have "disjoint_list [UNIV]" by(simp add: disjoint_list_def disjoint_def)
have "ipPartition (set (map wordinterval_to_set ss))
(set (map wordinterval_to_set (partitioningIps ss [wordinterval_UNIV])))"
for ss::"'a wordinterval list"
apply(rule hlp_rule)
done
thus ?thesis
unfolding getParts_def by blast
qed

lemma getParts_complete: "wordinterval_list_to_set (getParts rs) = UNIV"
proof -
have "{} ∉ set (map wordinterval_to_set ts) ⟹
(wordinterval_list_to_set ss) ⊆ (wordinterval_list_to_set ts) ⟹
wordinterval_list_to_set (partitioningIps ss ts) = (wordinterval_list_to_set ts)"
for ss ts::"'a wordinterval list"
using complete_helper by (metis partitioningIps_equi wordinterval_list_to_set_def)
hence "wordinterval_list_to_set (getParts rs) = wordinterval_list_to_set [wordinterval_UNIV]"
also have "… = UNIV" by (simp add: wordinterval_list_to_set_def)
finally show ?thesis .
qed

theorem getParts_samefw:
assumes "A ∈ set (map wordinterval_to_set (getParts rs))" "s1 ∈ A" "s2 ∈ A"
shows "simple_fw rs (p⦇p_src:=s1⦈) = simple_fw rs (p⦇p_src:=s2⦈) ∧
simple_fw rs (p⦇p_dst:=s1⦈) = simple_fw rs (p⦇p_dst:=s2⦈)"
proof -
let ?X="(set (map wordinterval_to_set (getParts rs)))"
from getParts_ipPartition have "ipPartition (set (map wordinterval_to_set (extract_IPSets rs))) ?X" .
hence "ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 src rs))) ?X ∧
ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 dst rs))) ?X"
thus ?thesis using assms dst_ipPart src_ipPart by blast
qed

lemma partIps_nonempty: "ts ≠ [] ⟹ partIps s ts ≠ []"
by(induction ts arbitrary: s) simp_all
lemma partitioningIps_nonempty: "ts ≠ [] ⟹ partitioningIps ss ts ≠ []"
proof(induction ss arbitrary: ts)
case Nil thus ?case by simp
next
case (Cons s ss) thus ?case
apply(cases ts)
apply(simp; fail)
apply(simp)
using partIps_nonempty by blast
qed

(*
lemma partIps_nonempty: "∀t ∈ set ts. ¬ wordinterval_empty t
⟹ {} ∉ set (map wordinterval_to_set (partIps s ts))"
apply(induction ts arbitrary: s)
apply(simp; fail)
apply(simp)
by blast
*)

lemma getParts_nonempty: "getParts rs ≠ []" by(simp add: getParts_def partitioningIps_nonempty)
lemma getParts_nonempty_elems: "∀w∈set (getParts rs). ¬ wordinterval_empty w"
unfolding getParts_def
proof -
have partitioning_nonempty: "∀t ∈ set ts. ¬ wordinterval_empty t ⟹
{} ∉ set (map wordinterval_to_set (partitioningIps ss ts))"
for ts ss::"'a wordinterval list"
proof(induction ss arbitrary: ts)
case Nil thus ?case by auto
case Cons thus ?case by (simp add: partIps_equi partList4_empty)
qed
have "∀t ∈ set [wordinterval_UNIV].¬ wordinterval_empty t" by(simp)
with partitioning_nonempty have
"{} ∉ set (map wordinterval_to_set (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]))"
by blast
thus "∀w∈set (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]). ¬ wordinterval_empty w" by auto
qed

(* HELPER FUNCTIONS UNIFICATION *)

fun getOneIp :: "'a::len wordinterval ⇒ 'a::len word" where
"getOneIp (WordInterval b _) = b" |
"getOneIp (RangeUnion r1 r2) = (if wordinterval_empty r1 then getOneIp r2
else getOneIp r1)"

lemma getOneIp_elem: "¬ wordinterval_empty W ⟹ wordinterval_element (getOneIp W) W"
by (induction W) simp_all

record parts_connection = pc_iiface :: string
pc_oiface :: string
pc_proto :: primitive_protocol
pc_sport :: "16 word"
pc_dport :: "16 word"

(* SAME FW DEFINITIONS AND PROOFS *)

definition same_fw_behaviour :: "⌦‹'pkt_ext itself ⇒› 'i::len word ⇒ 'i word ⇒ 'i simple_rule list ⇒ bool" where
"same_fw_behaviour ⌦‹TYPE('pkt_ext)› a b rs ≡
∀(p:: 'i::len simple_packet).
simple_fw rs (p⦇p_src:=a⦈) = simple_fw rs (p⦇p_src:=b⦈) ∧
simple_fw rs (p⦇p_dst:=a⦈) = simple_fw rs (p⦇p_dst:=b⦈)"

lemma getParts_same_fw_behaviour:
"A ∈ set (map wordinterval_to_set (getParts rs)) ⟹  s1 ∈ A ⟹ s2 ∈ A ⟹
same_fw_behaviour s1 s2 rs"
unfolding same_fw_behaviour_def
using getParts_samefw by blast

definition "runFw s d c rs = simple_fw rs ⦇p_iiface=pc_iiface c,p_oiface=pc_oiface c,
p_src=s,p_dst=d,
p_proto=pc_proto c,
p_sport=pc_sport c,p_dport=pc_dport c,
p_tcp_flags={TCP_SYN},

text‹We use @{const runFw} for executable code, but in general, everything applies to generic packets›
definition runFw_scheme :: "'i::len word ⇒ 'i word ⇒ 'b parts_connection_scheme ⇒
('i, 'a) simple_packet_scheme ⇒ 'i simple_rule list ⇒ state"
where
"runFw_scheme s d c p rs = simple_fw rs
(p⦇p_iiface:=pc_iiface c,
p_oiface:=pc_oiface c,
p_src:=s,
p_dst:=d,
p_proto:=pc_proto c,
p_sport:=pc_sport c,
p_dport:=pc_dport c⦈)"

lemma runFw_scheme: "runFw s d c rs = runFw_scheme s d c p rs"
apply(case_tac p)
apply(simp)
apply(thin_tac _, simp)
proof(induction rs)
case Nil thus ?case by(simp; fail)
next
case(Cons r rs)
obtain m a where r: "r = SimpleRule m a" by(cases r) simp
from simple_matches_extended_packet[symmetric, of _ "pc_iiface c" "pc_oiface c"
s d "pc_proto c" "pc_sport c" "pc_dport c" _ _ _ "{TCP_SYN}" "[]"]
have pext: "simple_matches m
⦇p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c,
simple_matches m
⦇p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c,
p_tcp_flags = {TCP_SYN}, p_payload = []⦈" for tcp_flags2 payload2 and aux::'c by fast
show ?case
apply(simp add: r, cases a, simp)
qed

lemma has_default_policy_runFw: "has_default_policy rs ⟹ runFw s d c rs = Decision FinalAllow ∨ runFw s d c rs = Decision FinalDeny"

definition same_fw_behaviour_one :: "'i::len word ⇒ 'i word ⇒ 'a parts_connection_scheme ⇒ 'i simple_rule list ⇒ bool" where
"same_fw_behaviour_one ip1 ip2 c rs ≡
∀d s. runFw ip1 d c rs = runFw ip2 d c rs ∧ runFw s ip1 c rs = runFw s ip2 c rs"

lemma same_fw_spec: "same_fw_behaviour ip1 ip2 rs ⟹ same_fw_behaviour_one ip1 ip2 c rs"
apply(rule conjI)
apply(clarify)
apply(erule_tac x="⦇p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = ip1, p_dst= d,
p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c,
p_tcp_flags = {TCP_SYN},
apply(simp;fail)
apply(clarify)
apply(erule_tac x="⦇p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst= ip1,
p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c,
p_tcp_flags = {TCP_SYN},
apply(simp)
done

text‹Is an equivalence relation›
lemma same_fw_behaviour_one_equi:
"same_fw_behaviour_one x x c rs"
"same_fw_behaviour_one x y c rs = same_fw_behaviour_one y x c rs"
"same_fw_behaviour_one x y c rs ∧ same_fw_behaviour_one y z c rs ⟹ same_fw_behaviour_one x z c rs"
unfolding same_fw_behaviour_one_def by metis+

lemma same_fw_behaviour_equi:
"same_fw_behaviour x x rs"
"same_fw_behaviour x y rs = same_fw_behaviour y x rs"
"same_fw_behaviour x y rs ∧ same_fw_behaviour y z rs ⟹ same_fw_behaviour x z rs"
unfolding same_fw_behaviour_def by auto

lemma runFw_sameFw_behave:
fixes W :: "'i::len word set set"
shows
"∀A ∈ W. ∀a1 ∈ A. ∀a2 ∈ A. same_fw_behaviour_one a1 a2 c rs ⟹ ⋃ W = UNIV ⟹
∀B ∈ W. ∃b ∈ B. runFw ip1 b c rs = runFw ip2 b c rs ⟹
∀B ∈ W. ∃b ∈ B. runFw b ip1 c rs = runFw b ip2 c rs ⟹
same_fw_behaviour_one ip1 ip2 c rs"
proof -
assume a1: "∀A ∈ W. ∀a1 ∈ A. ∀a2 ∈ A. same_fw_behaviour_one a1 a2 c rs"
and a2: "⋃ W = UNIV "
and a3: "∀B ∈ W. ∃b ∈ B. runFw ip1 b c rs = runFw ip2 b c rs"
and a4: "∀B ∈ W. ∃b ∈ B. runFw b ip1 c rs = runFw b ip2 c rs"

have relation_lem: "∀D ∈ W. ∀d1 ∈ D. ∀d2 ∈ D. ∀s. f s d1 = f s d2 ⟹ ⋃ W = UNIV ⟹
∀B ∈ W. ∃b ∈ B. f s1 b = f s2 b ⟹
f s1 d = f s2 d" for W and f::"'c ⇒ 'b ⇒ 'd" and s1 d s2
by (metis UNIV_I Union_iff)

from a1 have a1':"∀A∈W. ∀a1∈A. ∀a2∈A. ∀s. runFw s a1 c rs = runFw s a2 c rs"
unfolding same_fw_behaviour_one_def by fast
from relation_lem[OF a1' a2 a3] have s1: "⋀ d. runFw ip1 d c rs = runFw ip2 d c rs" by simp

from a1 have a1'':"∀A∈W. ∀a1∈A. ∀a2∈A. ∀d. runFw a1 d c rs = runFw a2 d c rs"
unfolding same_fw_behaviour_one_def by fast
from relation_lem[OF a1'' a2 a4] have s2: "⋀ s. runFw s ip1 c rs = runFw s ip2 c rs" by simp
from s1 s2 show "same_fw_behaviour_one ip1 ip2 c rs"
unfolding same_fw_behaviour_one_def by fast
qed

lemma sameFw_behave_sets:
"∀w∈set A. ∀a1 ∈ w. ∀a2 ∈ w. same_fw_behaviour_one a1 a2 c rs ⟹
∀w1∈set A. ∀w2∈set A. ∃a1∈w1. ∃a2∈w2. same_fw_behaviour_one a1 a2 c rs ⟹
∀w1∈set A. ∀w2∈set A.
∀a1∈w1. ∀a2∈w2. same_fw_behaviour_one a1 a2 c rs"
proof -
assume a1: "∀w∈set A. ∀a1 ∈ w. ∀a2 ∈ w. same_fw_behaviour_one a1 a2 c rs" and
"∀w1∈set A. ∀w2∈set A. ∃a1∈w1. ∃a2∈w2.  same_fw_behaviour_one a1 a2 c rs"
from this have "∀w1∈set A. ∀w2∈set A. ∃a1∈w1. ∀a2∈w2.  same_fw_behaviour_one a1 a2 c rs"
using same_fw_behaviour_one_equi(3) by metis
from a1 this show "∀w1∈set A. ∀w2∈set A. ∀a1∈w1. ∀a2∈w2. same_fw_behaviour_one a1 a2 c rs"
using same_fw_behaviour_one_equi(3) by metis
qed

definition groupWIs :: "parts_connection ⇒ 'i::len simple_rule list ⇒ 'i wordinterval list list" where
"groupWIs c rs = (let W = getParts rs in
(let f = (λwi. (map (λd. runFw (getOneIp wi) d c rs) (map getOneIp W),
map (λs. runFw s (getOneIp wi) c rs) (map getOneIp W))) in
groupF f W))"

lemma groupWIs_not_empty: "groupWIs c rs ≠ []"
proof -
have "getParts rs ≠ []" by(simp add: getParts_def partitioningIps_nonempty)
with groupF_empty have "⋀f. groupF f (getParts rs) ≠ []" by blast
thus ?thesis by(simp add: groupWIs_def Let_def) blast
qed
lemma groupWIs_not_empty_elem: "V ∈ set (groupWIs c rs) ⟹ V ≠ []"
lemma groupWIs_not_empty_elems:
assumes V: "V ∈ set (groupWIs c rs)" and w: "w ∈ set V"
shows "¬ wordinterval_empty w"
proof -
have "∀w∈set (concat (groupWIs c rs)). ¬ wordinterval_empty w"
apply(subst groupWIs_def)
apply(subst Let_def)+
apply(subst groupF_concat_set)
using getParts_nonempty_elems by blast
from this V w show ?thesis by auto
qed

lemma groupParts_same_fw_wi0:
assumes "V ∈ set (groupWIs c rs)"
shows "∀w ∈ set (map wordinterval_to_set V). ∀a1 ∈ w. ∀a2 ∈ w. same_fw_behaviour_one a1 a2 c rs"
proof -
have "∀A∈set (map wordinterval_to_set (concat (groupWIs c rs))).
∀a1∈A. ∀a2∈A. same_fw_behaviour_one a1 a2 c rs"
apply(subst groupWIs_def)
apply(subst Let_def)+
apply(subst set_map)
apply(subst groupF_concat_set)
using getParts_same_fw_behaviour same_fw_spec by fastforce
from this assms show ?thesis by force
qed

lemma groupWIs_same_fw_not: "A ∈ set (groupWIs c rs) ⟹ B ∈ set (groupWIs c rs) ⟹
A ≠ B ⟹
∀aw ∈ set (map wordinterval_to_set A).
∀bw ∈ set (map wordinterval_to_set B).
∀a ∈ aw. ∀b ∈ bw. ¬ same_fw_behaviour_one a b c rs"
proof -
assume asm: "A ∈ set (groupWIs c rs)" "B ∈ set (groupWIs c rs)" "A ≠ B"
from this have b1: "∀aw ∈ set A. ∀bw ∈ set B.
(map (λd. runFw (getOneIp aw) d c rs) (map getOneIp (getParts rs)),
map (λs. runFw s (getOneIp aw) c rs) (map getOneIp (getParts rs))) ≠
(map (λd. runFw (getOneIp bw) d c rs) (map getOneIp (getParts rs)),
map (λs. runFw s (getOneIp bw) c rs) (map getOneIp (getParts rs)))"
using groupF_nequality by fastforce
have same_behave_runFw_not:
"(map (λd. runFw x1 d c rs) W, map (λs. runFw s x1 c rs) W) ≠
(map (λd. runFw x2 d c rs) W, map (λs. runFw s x2 c rs) W) ⟹
¬ same_fw_behaviour_one x1 x2 c rs" for x1 x2 W
have "∀C ∈ set (groupWIs c rs). ∀c ∈ set C. getOneIp c ∈ wordinterval_to_set c"
using getParts_nonempty_elems groupF_set getOneIp_elem by fastforce
from this b1 asm have
"∀aw ∈ set (map wordinterval_to_set A). ∀bw ∈ set (map wordinterval_to_set B).
∃a ∈ aw. ∃b ∈ bw. (map (λd. runFw a d c rs) (map getOneIp (getParts rs)), map (λs. runFw s a c rs) (map getOneIp (getParts rs))) ≠
(map (λd. runFw b d c rs) (map getOneIp (getParts rs)), map (λs. runFw s b c rs) (map getOneIp (getParts rs)))"
by (simp) (blast)
from this same_behave_runFw_not asm
have " ∀aw ∈ set (map wordinterval_to_set A). ∀bw ∈ set (map wordinterval_to_set B).
∃a ∈ aw. ∃b ∈ bw. ¬ same_fw_behaviour_one a b c rs" by fast
from this groupParts_same_fw_wi0[of A c rs]  groupParts_same_fw_wi0[of B c rs] asm
have "∀aw ∈ set (map wordinterval_to_set A).
∀bw ∈ set (map wordinterval_to_set B).
∀a ∈ aw. ∃b ∈ bw. ¬ same_fw_behaviour_one a b c rs"
apply(simp) using same_fw_behaviour_one_equi(3) by blast
from this groupParts_same_fw_wi0[of A c rs]  groupParts_same_fw_wi0[of B c rs] asm
show "∀aw ∈ set (map wordinterval_to_set A).
∀bw ∈ set (map wordinterval_to_set B).
∀a ∈ aw. ∀b ∈ bw. ¬ same_fw_behaviour_one a b c rs"
apply(simp) using same_fw_behaviour_one_equi(3) by fast
qed

(*beginning is copy&paste of previous proof*)
lemma groupParts_same_fw_wi1:
"V ∈ set (groupWIs c rs) ⟹ ∀w1 ∈ set V. ∀w2 ∈ set V.
∀a1 ∈ wordinterval_to_set w1. ∀a2 ∈ wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs"
proof -
assume asm: "V ∈ set (groupWIs c rs)"
from getParts_same_fw_behaviour same_fw_spec
have b1: "∀A ∈ set (map wordinterval_to_set (getParts rs)) . ∀a1 ∈ A. ∀a2 ∈ A.
same_fw_behaviour_one a1 a2 c rs" by fast
from getParts_complete have complete: "⋃(set (map wordinterval_to_set (getParts rs))) = UNIV"
from getParts_nonempty_elems have nonempty: "∀w∈set (getParts rs). ¬ wordinterval_empty w" by simp

{ fix W x1 x2
assume a1: "∀A ∈ set (map wordinterval_to_set W). ∀a1 ∈ A. ∀a2 ∈ A. same_fw_behaviour_one a1 a2 c rs"
and a2: "wordinterval_list_to_set W = UNIV"
and a3: "∀w ∈ set W. ¬ wordinterval_empty w"
and a4: "(map (λd. runFw x1 d c rs) (map getOneIp W), map (λs. runFw s x1 c rs) (map getOneIp W)) =
(map (λd. runFw x2 d c rs) (map getOneIp W), map (λs. runFw s x2 c rs) (map getOneIp W))"
from a3 a4 getOneIp_elem
have b1: "∀B ∈ set (map wordinterval_to_set W). ∃b ∈ B. runFw x1 b c rs = runFw x2 b c rs"
by fastforce
from a3 a4 getOneIp_elem
have b2: "∀B ∈ set (map wordinterval_to_set W). ∃b ∈ B. runFw b x1 c rs = runFw b x2 c rs"
by fastforce
from runFw_sameFw_behave[OF a1 _ b1 b2] a2[unfolded wordinterval_list_to_set_def] have
"same_fw_behaviour_one x1 x2 c rs" by simp
} note same_behave_runFw=this

from same_behave_runFw[OF b1 getParts_complete nonempty]
groupF_equality[of "(λwi. (map (λd. runFw (getOneIp wi) d c rs) (map getOneIp (getParts rs)),
map (λs. runFw s (getOneIp wi) c rs) (map getOneIp (getParts rs))))"
"(getParts rs)"] asm
have b2: "∀a1∈set V. ∀a2∈set V. same_fw_behaviour_one (getOneIp a1) (getOneIp a2) c rs"
apply(subst (asm) groupWIs_def)
apply(subst (asm) Let_def)+
by fast
from groupWIs_not_empty_elems asm have "∀w ∈ set V. ¬ wordinterval_empty w" by blast
from this b2 getOneIp_elem
have b3: "∀w1∈set (map wordinterval_to_set V). ∀w2∈set (map wordinterval_to_set V).
∃ip1∈ w1. ∃ip2∈w2.
same_fw_behaviour_one ip1 ip2 c rs" by (simp) (blast)
from groupParts_same_fw_wi0 asm
have "∀A∈set (map wordinterval_to_set V). ∀a1∈ A. ∀a2∈ A. same_fw_behaviour_one a1 a2 c rs"
by metis
from sameFw_behave_sets[OF this b3]
show "∀w1 ∈ set V. ∀w2 ∈ set V.
∀a1 ∈ wordinterval_to_set w1. ∀a2 ∈ wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs"
by force
qed

lemma groupParts_same_fw_wi2: "V ∈ set (groupWIs c rs) ⟹
∀ip1 ∈ wordinterval_list_to_set V.
∀ip2 ∈ wordinterval_list_to_set V.
same_fw_behaviour_one ip1 ip2 c rs"
using groupParts_same_fw_wi0 groupParts_same_fw_wi1
by fast

lemma groupWIs_same_fw_not2: "A ∈ set (groupWIs c rs) ⟹ B ∈ set (groupWIs c rs) ⟹
A ≠ B ⟹
∀ip1 ∈ wordinterval_list_to_set A.
∀ip2 ∈ wordinterval_list_to_set B.
¬ same_fw_behaviour_one ip1 ip2 c rs"
using groupWIs_same_fw_not by fastforce

(*I like this version -- corny*)
lemma "A ∈ set (groupWIs c rs) ⟹ B ∈ set (groupWIs c rs) ⟹
∃ip1 ∈ wordinterval_list_to_set A.
∃ip2 ∈ wordinterval_list_to_set B. same_fw_behaviour_one ip1 ip2 c rs
⟹ A = B"
using groupWIs_same_fw_not2 by blast

lemma groupWIs_complete: "(⋃x∈ set (groupWIs c rs). wordinterval_list_to_set x) = (UNIV::'i::len word set)"
proof -
have "(⋃ y ∈ (⋃x∈ set (groupWIs c rs). set x). wordinterval_to_set y) = (UNIV::'i word set)"
using getParts_complete wordinterval_list_to_set_def by fastforce
qed

(*begin groupWIs1 and groupWIs2 optimization*)
definition groupWIs1 :: "'a parts_connection_scheme ⇒ 'i::len simple_rule list ⇒ 'i wordinterval list list" where
"groupWIs1 c rs = (let P = getParts rs in
(let W = map getOneIp P in
(let f = (λwi. (map (λd. runFw (getOneIp wi) d c rs) W,
map (λs. runFw s (getOneIp wi) c rs) W)) in
map (map fst) (groupF snd (map (λx. (x, f x)) P)))))"

lemma groupWIs_groupWIs1_equi: "groupWIs1 c rs = groupWIs c rs"
apply(subst groupWIs1_def)
apply(subst groupWIs_def)
using groupF_tuple by metis

definition simple_conn_matches :: "'i::len simple_match ⇒ parts_connection ⇒ bool" where
"simple_conn_matches m c ⟷
(match_iface (iiface m) (pc_iiface c)) ∧
(match_iface (oiface m) (pc_oiface c)) ∧
(match_proto (proto m) (pc_proto c)) ∧
(simple_match_port (sports m) (pc_sport c)) ∧
(simple_match_port (dports m) (pc_dport c))"

lemma simple_conn_matches_simple_match_any: "simple_conn_matches simple_match_any c"
apply (simp add: simple_conn_matches_def simple_match_any_def match_ifaceAny)
apply (subgoal_tac "(65535::16 word) = max_word")
apply (simp only:)
apply simp_all
done

lemma has_default_policy_simple_conn_matches:
"has_default_policy rs ⟹ has_default_policy [r←rs . simple_conn_matches (match_sel r) c]"
apply(induction rs rule: has_default_policy.induct)
apply(simp; fail)
apply(simp)
apply(intro conjI)
apply(simp split: if_split_asm; fail)
done

lemma filter_conn_fw_lem:
"runFw s d c (filter (λr. simple_conn_matches (match_sel r) c) rs) = runFw s d c rs"
apply(induction rs "⦇p_iiface = pc_iiface c, p_oiface = pc_oiface c,
p_src = s, p_dst = d, p_proto = pc_proto c,
p_sport = pc_sport c, p_dport = pc_dport c,
rule: simple_fw.induct)
done

(*performance: despite optimization, this function takes quite long and can be optimized*)
definition groupWIs2 :: "parts_connection ⇒ 'i::len simple_rule list ⇒ 'i wordinterval list list" where
"groupWIs2 c rs =  (let P = getParts rs in
(let W = map getOneIp P in
(let filterW = (filter (λr. simple_conn_matches (match_sel r) c) rs) in
(let f = (λwi. (map (λd. runFw (getOneIp wi) d c filterW) W,
map (λs. runFw s (getOneIp wi) c filterW) W)) in
map (map fst) (groupF snd (map (λx. (x, f x)) P))))))"

lemma groupWIs1_groupWIs2_equi: "groupWIs2 c rs = groupWIs1 c rs"

lemma groupWIs_code[code]: "groupWIs c rs = groupWIs2 c rs"
using groupWIs1_groupWIs2_equi groupWIs_groupWIs1_equi by metis
(*end groupWIs1 and groupWIs2 optimization*)

(*begin groupWIs3 optimization*)
fun matching_dsts :: "'i::len word ⇒ 'i simple_rule list ⇒ 'i wordinterval ⇒ 'i wordinterval" where
"matching_dsts _ [] _ = Empty_WordInterval" |
"matching_dsts s ((SimpleRule m Accept)#rs) acc_dropped =
(if simple_match_ip (src m) s then
wordinterval_union (wordinterval_setminus (ipcidr_tuple_to_wordinterval (dst m)) acc_dropped) (matching_dsts s rs acc_dropped)
else
matching_dsts s rs acc_dropped)" |
"matching_dsts s ((SimpleRule m Drop)#rs) acc_dropped =
(if simple_match_ip (src m) s then
matching_dsts s rs (wordinterval_union (ipcidr_tuple_to_wordinterval (dst m)) acc_dropped)
else
matching_dsts s rs acc_dropped)"

lemma matching_dsts_pull_out_accu:
"wordinterval_to_set (matching_dsts s rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_dsts s rs a2) - wordinterval_to_set a1"
apply(induction s rs a2 arbitrary: a1 a2 rule: matching_dsts.induct)
apply(simp_all)
by blast+

(*a copy of matching_dsts*)
fun matching_srcs :: "'i::len word ⇒ 'i simple_rule list ⇒ 'i wordinterval ⇒ 'i wordinterval" where
"matching_srcs _ [] _ = Empty_WordInterval" |
"matching_srcs d ((SimpleRule m Accept)#rs) acc_dropped =
(if simple_match_ip (dst m) d then
wordinterval_union (wordinterval_setminus (ipcidr_tuple_to_wordinterval (src m)) acc_dropped) (matching_srcs d rs acc_dropped)
else
matching_srcs d rs acc_dropped)" |
"matching_srcs d ((SimpleRule m Drop)#rs) acc_dropped =
(if simple_match_ip (dst m) d then
matching_srcs d rs (wordinterval_union (ipcidr_tuple_to_wordinterval (src m)) acc_dropped)
else
matching_srcs d rs acc_dropped)"

lemma matching_srcs_pull_out_accu:
"wordinterval_to_set (matching_srcs d rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_srcs d rs a2) - wordinterval_to_set a1"
apply(induction d rs a2 arbitrary: a1 a2 rule: matching_srcs.induct)
apply(simp_all)
by blast+

lemma matching_dsts: "∀r ∈ set rs. simple_conn_matches (match_sel r) c ⟹
wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}"
proof(induction rs)
case Nil thus ?case by (simp add: runFw_def)
next
case (Cons r rs)
obtain m a where r: "r = SimpleRule m a" by(cases r, blast)

from Cons.prems r have simple_match_ip_Accept: "⋀d. simple_match_ip (src m) s ⟹
runFw s d c (SimpleRule m Accept # rs) = Decision FinalAllow ⟷ simple_match_ip (dst m) d ∨ runFw s d c rs = Decision FinalAllow"

{ fix d a
have "¬ simple_match_ip (src m) s ⟹
runFw s d c (SimpleRule m a # rs) = Decision FinalAllow ⟷ runFw s d c rs = Decision FinalAllow"
apply(cases a)
} note not_simple_match_ip=this

from Cons.prems r have simple_match_ip_Drop: "⋀d. simple_match_ip (src m) s ⟹
runFw s d c (SimpleRule m Drop # rs) = Decision FinalAllow ⟷ ¬ simple_match_ip (dst m) d ∧ runFw s d c rs = Decision FinalAllow"

show ?case
proof(cases a)
case Accept with r Cons show ?thesis
apply(simp, intro conjI impI)
apply blast
done
next
case Drop with r Cons show ?thesis
apply(simp,intro conjI impI)
apply blast
done
qed
qed
lemma matching_srcs: "∀r ∈ set rs. simple_conn_matches (match_sel r) c ⟹
wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}"
proof(induction rs)
case Nil thus ?case by (simp add: runFw_def)
next
case (Cons r rs)
obtain m a where r: "r = SimpleRule m a" by(cases r, blast)

from Cons.prems r have simple_match_ip_Accept: "⋀s. simple_match_ip (dst m) d ⟹
runFw s d c (SimpleRule m Accept # rs) = Decision FinalAllow ⟷
simple_match_ip (src m) s ∨ runFw s d c rs = Decision FinalAllow"

{ fix s a
have "¬ simple_match_ip (dst m) d ⟹
runFw s d c (SimpleRule m a # rs) = Decision FinalAllow ⟷ runFw s d c rs = Decision FinalAllow"
apply(cases a)
} note not_simple_match_ip=this

from Cons.prems r have simple_match_ip_Drop: "⋀s. simple_match_ip (dst m) d ⟹
runFw s d c (SimpleRule m Drop # rs) = Decision FinalAllow ⟷
¬ simple_match_ip (src m) s ∧ runFw s d c rs = Decision FinalAllow"

show ?case
proof(cases a)
case Accept with r Cons show ?thesis
apply(simp, intro conjI impI)
apply blast
done
next
case Drop with r Cons show ?thesis
apply(simp,intro conjI impI)
apply blast
done
qed
qed

(*TODO: if we can get wordinterval_element to log runtime ...*)
definition groupWIs3_default_policy :: "parts_connection ⇒ 'i::len simple_rule list ⇒ 'i wordinterval list list" where
"groupWIs3_default_policy c rs =  (let P = getParts rs in
(let W = map getOneIp P in
(let filterW = (filter (λr. simple_conn_matches (match_sel r) c) rs) in
(let f = (λwi. let mtch_dsts = (matching_dsts (getOneIp wi) filterW Empty_WordInterval);
mtch_srcs = (matching_srcs (getOneIp wi) filterW Empty_WordInterval) in
(map (λd. wordinterval_element d mtch_dsts) W,
map (λs. wordinterval_element s mtch_srcs) W)) in
map (map fst) (groupF snd (map (λx. (x, f x)) P))))))"

lemma groupWIs3_default_policy_groupWIs2:
fixes rs :: "'i::len simple_rule list"
assumes "has_default_policy rs"
shows "groupWIs2 c rs = groupWIs3_default_policy c rs"
proof -
{ fix filterW s d
from matching_dsts[where c=c] have "filterW = filter (λr. simple_conn_matches (match_sel r) c) rs ⟹
wordinterval_element d (matching_dsts s filterW Empty_WordInterval) ⟷ runFw s d c filterW = Decision FinalAllow"
by force
} note matching_dsts_filterW=this[simplified]

{ fix filterW s d
from matching_srcs[where c=c] have "filterW = filter (λr. simple_conn_matches (match_sel r) c) rs ⟹
wordinterval_element s (matching_srcs d filterW Empty_WordInterval) ⟷ runFw s d c filterW = Decision FinalAllow"
by force
} note matching_srcs_filterW=this[simplified]

{ fix W and rs<`