imports SimpleFw_Semantics
```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
```