Theory Ports_Normalize
theory Ports_Normalize
imports Common_Primitive_Lemmas
begin
section‹Normalizing L4 Ports›
subsection‹Defining Normalized Ports›
fun normalized_src_ports :: "'i::len common_primitive match_expr ⇒ bool" where
"normalized_src_ports MatchAny = True" |
"normalized_src_ports (Match (Src_Ports (L4Ports _ []))) = True" |
"normalized_src_ports (Match (Src_Ports (L4Ports _ [_]))) = True" |
"normalized_src_ports (Match (Src_Ports _)) = False" |
"normalized_src_ports (Match _) = True" |
"normalized_src_ports (MatchNot (Match (Src_Ports _))) = False" |
"normalized_src_ports (MatchNot (Match _)) = True" |
"normalized_src_ports (MatchAnd m1 m2) = (normalized_src_ports m1 ∧ normalized_src_ports m2)" |
"normalized_src_ports (MatchNot (MatchAnd _ _)) = False" |
"normalized_src_ports (MatchNot (MatchNot _)) = False" |
"normalized_src_ports (MatchNot MatchAny) = True"
fun normalized_dst_ports :: "'i::len common_primitive match_expr ⇒ bool" where
"normalized_dst_ports MatchAny = True" |
"normalized_dst_ports (Match (Dst_Ports (L4Ports _ []))) = True" |
"normalized_dst_ports (Match (Dst_Ports (L4Ports _ [_]))) = True" |
"normalized_dst_ports (Match (Dst_Ports _)) = False" |
"normalized_dst_ports (Match _) = True" |
"normalized_dst_ports (MatchNot (Match (Dst_Ports _))) = False" |
"normalized_dst_ports (MatchNot (Match _)) = True" |
"normalized_dst_ports (MatchAnd m1 m2) = (normalized_dst_ports m1 ∧ normalized_dst_ports m2)" |
"normalized_dst_ports (MatchNot (MatchAnd _ _)) = False" |
"normalized_dst_ports (MatchNot (MatchNot _)) = False" |
"normalized_dst_ports (MatchNot MatchAny) = True"
lemma normalized_src_ports_def2: "normalized_src_ports ms = normalized_n_primitive (is_Src_Ports, src_ports_sel) (λps. case ps of L4Ports _ pts ⇒ length pts ≤ 1) ms"
by(induction ms rule: normalized_src_ports.induct, simp_all)
lemma normalized_dst_ports_def2: "normalized_dst_ports ms = normalized_n_primitive (is_Dst_Ports, dst_ports_sel) (λps. case ps of L4Ports _ pts ⇒ length pts ≤ 1) ms"
by(induction ms rule: normalized_dst_ports.induct, simp_all)
text‹Idea: first, remove all negated matches, then @{const normalize_match},
then only work with @{const primitive_extractor} on @{const Pos} ones.
They only need an intersect and split later on.
This is not very efficient because normalizing nnf will blow up a lot.
but we can tune performance later on go for correctness first!
Anything with @{const MatchOr} and @{const normalize_match} later is a bit inefficient.
›
subsection‹Compressing Positive Matches on Ports into a Single Match›
fun l4_ports_compress :: "ipt_l4_ports list ⇒ ipt_l4_ports match_compress" where
"l4_ports_compress [] = MatchesAll" |
"l4_ports_compress [L4Ports proto ps] = MatchExpr (L4Ports proto (wi2l (wordinterval_compress (l2wi ps))))" |
"l4_ports_compress (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss) =
(if
proto1 ≠ proto2
then
CannotMatch
else
l4_ports_compress (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss)
)"
value[code] "l4_ports_compress [L4Ports TCP [(22,22), (23,23)]]"
lemma raw_ports_compress_src_CannotMatch:
fixes p :: "('i::len, 'a) tagged_packet_scheme"
assumes generic: "primitive_matcher_generic β"
and c: "l4_ports_compress pss = CannotMatch"
shows "¬ matches (β, α) (alist_and (map (Pos ∘ Src_Ports) pss)) a p"
using c apply(induction pss rule: l4_ports_compress.induct)
apply(simp; fail)
apply(simp; fail)
apply(simp add: primitive_matcher_generic.Ports_single[OF generic] bunch_of_lemmata_about_matches split: if_split_asm)
apply meson
by(simp add: l2wi_wi2l ports_to_set_wordinterval)
lemma raw_ports_compress_dst_CannotMatch:
fixes p :: "('i::len, 'a) tagged_packet_scheme"
assumes generic: "primitive_matcher_generic β"
and c: "l4_ports_compress pss = CannotMatch"
shows "¬ matches (β, α) (alist_and (map (Pos ∘ Dst_Ports) pss)) a p"
using c apply(induction pss rule: l4_ports_compress.induct)
apply(simp; fail)
apply(simp; fail)
apply(simp add: primitive_matcher_generic.Ports_single[OF generic] bunch_of_lemmata_about_matches split: if_split_asm)
apply meson
by(simp add: l2wi_wi2l ports_to_set_wordinterval)
lemma l4_ports_compress_length_Matchall: "length pss > 0 ⟹ l4_ports_compress pss ≠ MatchesAll"
by(induction pss rule: l4_ports_compress.induct) simp+
lemma raw_ports_compress_MatchesAll:
fixes p :: "('i::len, 'a) tagged_packet_scheme"
assumes generic: "primitive_matcher_generic β"
and c: "l4_ports_compress pss = MatchesAll"
shows "matches (β, α) (alist_and (map (Pos ∘ Src_Ports) pss)) a p"
and "matches (β, α) (alist_and (map (Pos ∘ Dst_Ports) pss)) a p"
using c apply(induction pss rule: l4_ports_compress.induct)
by(simp add: l4_ports_compress_length_Matchall bunch_of_lemmata_about_matches split: if_split_asm)+
lemma raw_ports_compress_src_MatchExpr:
fixes p :: "('i::len, 'a) tagged_packet_scheme"
assumes generic: "primitive_matcher_generic β"
and c: "l4_ports_compress pss = MatchExpr m"
shows "matches (β, α) (Match (Src_Ports m)) a p ⟷ matches (β, α) (alist_and (map (Pos ∘ Src_Ports) pss)) a p"
using c apply(induction pss arbitrary: m rule: l4_ports_compress.induct)
apply(simp add: bunch_of_lemmata_about_matches; fail)
subgoal
apply(simp add: bunch_of_lemmata_about_matches)
apply(drule sym, simp)
by(simp add: primitive_matcher_generic.Ports_single[OF generic] wordinterval_compress l2wi_wi2l ports_to_set_wordinterval)
apply(case_tac m)
apply(simp add: bunch_of_lemmata_about_matches split: if_split_asm)
apply(simp add: primitive_matcher_generic.Ports_single[OF generic])
apply(simp add: l2wi_wi2l ports_to_set_wordinterval)
by fastforce
lemma raw_ports_compress_dst_MatchExpr:
fixes p :: "('i::len, 'a) tagged_packet_scheme"
assumes generic: "primitive_matcher_generic β"
and c: "l4_ports_compress pss = MatchExpr m"
shows "matches (β, α) (Match (Dst_Ports m)) a p ⟷ matches (β, α) (alist_and (map (Pos ∘ Dst_Ports) pss)) a p"
using c apply(induction pss arbitrary: m rule: l4_ports_compress.induct)
apply(simp add: bunch_of_lemmata_about_matches; fail)
subgoal
apply(simp add: bunch_of_lemmata_about_matches)
apply(drule sym, simp)
by(simp add: primitive_matcher_generic.Ports_single[OF generic] wordinterval_compress l2wi_wi2l ports_to_set_wordinterval)
apply(case_tac m)
apply(simp add: bunch_of_lemmata_about_matches split: if_split_asm)
apply(simp add: primitive_matcher_generic.Ports_single[OF generic])
apply(simp add: l2wi_wi2l ports_to_set_wordinterval)
by fastforce
subsection‹Rewriting Negated Matches on Ports›
fun l4_ports_negate_one
:: "(ipt_l4_ports ⇒ 'i common_primitive) ⇒ ipt_l4_ports ⇒ ('i::len common_primitive) match_expr"
where
"l4_ports_negate_one C (L4Ports proto pts) = MatchOr
(MatchNot (Match (Prot (Proto proto))))
(Match (C (L4Ports proto (raw_ports_invert pts))))"
lemma l4_ports_negate_one:
fixes p :: "('i::len, 'a) tagged_packet_scheme"
assumes generic: "primitive_matcher_generic β"
shows "matches (β, α) (l4_ports_negate_one Src_Ports ports) a p ⟷
matches (β, α) (MatchNot (Match (Src_Ports ports))) a p"
and "matches (β, α) (l4_ports_negate_one Dst_Ports ports) a p ⟷
matches (β, α) (MatchNot (Match (Dst_Ports ports))) a p"
apply(case_tac [!] ports)
by(auto simp add: primitive_matcher_generic.Ports_single_not[OF generic]
MatchOr bunch_of_lemmata_about_matches
primitive_matcher_generic.Prot_single_not[OF generic]
primitive_matcher_generic.Ports_single[OF generic]
raw_ports_invert)
lemma l4_ports_negate_one_nodisc:
"∀a. ¬ disc (C a) ⟹ ∀a. ¬ disc (Prot a) ⟹ ¬ has_disc disc (l4_ports_negate_one C pt)"
apply(cases pt)
by(simp add: MatchOr_def)
lemma l4_ports_negate_one_not_has_disc_negated_generic:
assumes noProt: "∀a. ¬ disc (Prot a)"
shows "¬ has_disc_negated disc False (l4_ports_negate_one C ports)"
apply(cases ports, rename_tac proto pts)
by(simp add: MatchOr_def noProt)
lemma l4_ports_negate_one_not_has_disc_negated:
"¬ has_disc_negated is_Src_Ports False (l4_ports_negate_one Src_Ports ports)"
"¬ has_disc_negated is_Dst_Ports False (l4_ports_negate_one Dst_Ports ports)"
by(simp add: l4_ports_negate_one_not_has_disc_negated_generic)+
lemma negated_normalized_folded_ports_nodisc:
"∀a. ¬ disc (C a) ⟹ (∀a. ¬ disc (Prot a)) ∨ pts = [] ⟹
m ∈ set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts))) ⟹
¬ has_disc disc m"
apply(subgoal_tac "¬ has_disc disc (andfold_MatchExp (map (l4_ports_negate_one C) pts))")
prefer 2
apply(rule andfold_MatchExp_not_discI)
apply(simp)
apply(elim disjE)
using l4_ports_negate_one_nodisc apply blast
apply(simp; fail)
using normalize_match_preserves_nodisc by blast
lemma negated_normalized_folded_ports_normalized_n_primitive:
"∀a. ¬ disc (C a) ⟹ (∀a. ¬ disc (Prot a)) ∨ pts = [] ⟹
x ∈ set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts))) ⟹
normalized_n_primitive (disc, sel) f x"
apply(rule normalized_n_primitive_if_no_primitive)
using normalized_nnf_match_normalize_match apply blast
apply(rule negated_normalized_folded_ports_nodisc)
by simp_all
text‹beware, the result is not nnf normalized!›
lemma "¬ normalized_nnf_match (l4_ports_negate_one C ports)"
by(cases ports) (simp add: MatchOr_def)
text‹Warning: does not preserve negated primitive property in general.
Might be violated for @{const Prot}. We will nnf normalize after applying the function.›
lemma "∀a. ¬ disc (C a) ⟹ ¬ normalized_n_primitive (disc, sel) f (l4_ports_negate_one C a)"
by(cases a)(simp add: MatchOr_def)
declare l4_ports_negate_one.simps[simp del]
lemma "((normalize_match (l4_ports_negate_one Src_Ports (L4Ports TCP [(22,22),(80,90)]))):: 32 common_primitive match_expr list)
=
[ MatchNot (Match (Prot (Proto TCP)))
, Match (Src_Ports (L4Ports 6 [(0, 21), (23, 79), (91, 0xFFFF)]))]" by eval
definition rewrite_negated_primitives
:: "(('a ⇒ bool) × ('a ⇒ 'b)) ⇒ ('b ⇒ 'a) ⇒
(('b ⇒ 'a) ⇒ 'b ⇒ 'a match_expr) ⇒
'a match_expr ⇒ 'a match_expr" where
"rewrite_negated_primitives disc_sel C negate m ≡
let (spts, rst) = primitive_extractor disc_sel m
in if getNeg spts = [] then m else
MatchAnd
(andfold_MatchExp (map (negate C) (getNeg spts)))
(MatchAnd
(andfold_MatchExp (map (Match ∘ C) (getPos spts)))
rst)"
text‹It does nothing of there is not even a negated primitive in it›
lemma rewrite_negated_primitives_unchanged_if_not_has_disc_negated:
assumes n: "normalized_nnf_match m"
and wf_disc_sel: "wf_disc_sel (disc,sel) C"
and noDisc: "¬ has_disc_negated disc False m"
shows "rewrite_negated_primitives (disc,sel) C negate_f m = m"
apply(simp add: rewrite_negated_primitives_def)
apply(case_tac "primitive_extractor (disc,sel) m", rename_tac spts rst)
apply(simp)
apply(frule primitive_extractor_correct(8)[OF n wf_disc_sel])
using noDisc by blast
lemma rewrite_negated_primitives_normalized_no_modification:
assumes wf_disc_sel: "wf_disc_sel (disc, sel) C"
and disc_p: "¬ has_disc_negated disc False m"
and n: "normalized_nnf_match m"
and a: "a ∈ set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))"
shows "a = m"
proof -
from rewrite_negated_primitives_unchanged_if_not_has_disc_negated[OF n wf_disc_sel disc_p]
have m: "rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m = m" by simp
from a show ?thesis
apply(subst(asm) m)
using normalize_match_already_normalized[OF n] by fastforce
qed
lemma rewrite_negated_primitives_preserves_not_has_disc:
assumes n: "normalized_nnf_match m"
and wf_disc_sel: "wf_disc_sel (disc, sel) C"
and nodisc: "¬ has_disc disc2 m"
and noNeg: "¬ has_disc_negated disc False m"
and disc2_noC: "∀a. ¬ disc2 (C a)"
shows "¬ has_disc disc2 (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)"
apply(subst rewrite_negated_primitives_unchanged_if_not_has_disc_negated)
using n wf_disc_sel noNeg nodisc by(simp)+
lemma rewrite_negated_primitives:
assumes n: "normalized_nnf_match m" and wf_disc_sel: "wf_disc_sel disc_sel C"
and negate_f: "∀pts. matches γ (negate_f C pts) a p ⟷ matches γ (MatchNot (Match (C pts))) a p"
shows "matches γ (rewrite_negated_primitives disc_sel C negate_f m) a p ⟷ matches γ m a p"
proof -
obtain spts rst where pext: "primitive_extractor disc_sel m = (spts, rst)"
by(cases "primitive_extractor disc_sel m") simp
obtain disc sel where disc_sel: "disc_sel = (disc, sel)" by(cases disc_sel) simp
with wf_disc_sel have wf_disc_sel': "wf_disc_sel (disc, sel) C" by simp
from disc_sel pext have pext': "primitive_extractor (disc, sel) m = (spts, rst)" by simp
have "matches γ (andfold_MatchExp (map (negate_f C) (getNeg spts))) a p ∧
matches γ (andfold_MatchExp (map (Match ∘ C) (getPos spts))) a p ∧ matches γ rst a p ⟷
matches γ m a p"
apply(subst primitive_extractor_correct(1)[OF n wf_disc_sel' pext', symmetric])
apply(simp add: andfold_MatchExp_matches)
apply(simp add: negate_f)
using alist_and_NegPos_map_getNeg_getPos_matches by fast
thus ?thesis by(simp add: rewrite_negated_primitives_def pext bunch_of_lemmata_about_matches)
qed
lemma rewrite_negated_primitives_not_has_disc:
assumes n: "normalized_nnf_match m" and wf_disc_sel: "wf_disc_sel (disc,sel) C"
and nodisc: "¬ has_disc disc2 m"
and negate_f: "has_disc_negated disc False m ⟹ ∀pts. ¬ has_disc disc2 (negate_f C pts)"
and no_disc: "∀a. ¬ disc2 (C a)"
shows "¬ has_disc disc2 (rewrite_negated_primitives (disc,sel) C negate_f m)"
apply(simp add: rewrite_negated_primitives_def)
apply(case_tac "primitive_extractor (disc,sel) m", rename_tac spts rst)
apply(simp)
apply(frule primitive_extractor_correct(4)[OF n wf_disc_sel])
apply(frule primitive_extractor_correct(8)[OF n wf_disc_sel])
apply(intro conjI impI)
using nodisc apply(simp; fail)
apply(rule andfold_MatchExp_not_discI)
apply(simp add: negate_f; fail)
using andfold_MatchExp_not_disc_mapMatch no_disc apply blast
using nodisc by blast
lemma rewrite_negated_primitives_not_has_disc_negated:
assumes n: "normalized_nnf_match m" and wf_disc_sel: "wf_disc_sel (disc,sel) C"
and negate_f: "has_disc_negated disc False m ⟹ ∀pts. ¬ has_disc_negated disc False (negate_f C pts)"
shows "¬ has_disc_negated disc False (rewrite_negated_primitives (disc,sel) C negate_f m)"
apply(simp add: rewrite_negated_primitives_def)
apply(case_tac "primitive_extractor (disc,sel) m", rename_tac spts rst)
apply(simp)
apply(frule primitive_extractor_correct(3)[OF n wf_disc_sel])
apply(frule primitive_extractor_correct(8)[OF n wf_disc_sel])
apply(intro conjI impI)
apply blast
apply(rule andfold_MatchExp_not_disc_negatedI)
apply(simp add: negate_f; fail)
using andfold_MatchExp_not_disc_negated_mapMatch apply blast
using has_disc_negated_has_disc by blast
lemma rewrite_negated_primitives_preserves_not_has_disc_negated:
assumes n: "normalized_nnf_match m" and wf_disc_sel: "wf_disc_sel (disc,sel) C"
and negate_f: "has_disc_negated disc False m ⟹ ∀pts. ¬ has_disc_negated disc2 False (negate_f C pts)"
and no_disc: "¬ has_disc_negated disc2 False m"
shows "¬ has_disc_negated disc2 False (rewrite_negated_primitives (disc,sel) C negate_f m)"
apply(simp add: rewrite_negated_primitives_def)
apply(case_tac "primitive_extractor (disc,sel) m", rename_tac spts rst)
apply(simp)
apply(frule primitive_extractor_correct(3)[OF n wf_disc_sel])
apply(frule primitive_extractor_correct(8)[OF n wf_disc_sel])
apply(intro conjI impI)
using no_disc apply blast
apply(rule andfold_MatchExp_not_disc_negatedI)
apply(simp add: negate_f; fail)
using andfold_MatchExp_not_disc_negated_mapMatch apply blast
apply(drule primitive_extractor_correct(6)[OF n wf_disc_sel, where neg=False])
using no_disc by blast
lemma rewrite_negated_primitives_normalized_preserves_unrelated_helper:
assumes wf_disc_sel: "wf_disc_sel (disc, sel) C"
and disc: "∀a. ¬ disc2 (C a)"
and disc_p: "(∀a. ¬ disc2 (Prot a)) ∨ ¬ has_disc_negated disc False m"
shows "normalized_nnf_match m ⟹
normalized_n_primitive (disc2, sel2) f m ⟹
a ∈ set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)) ⟹
normalized_n_primitive (disc2, sel2) f a"
proof -
have helper_a_normalized: "a ∈ MatchAnd x ` (⋃x∈set spts. MatchAnd x ` set (normalize_match rst)) ⟹
normalized_n_primitive (disc, sel) f x ⟹
(∀s ∈ set spts. normalized_n_primitive (disc, sel) f s) ⟹
normalized_n_primitive (disc, sel) f rst ⟹
normalized_n_primitive (disc, sel) f a"
for a x spts rst f disc and sel::"'a common_primitive ⇒ 'b"
apply(subgoal_tac "∃ s r. a = MatchAnd x (MatchAnd s r) ∧ s ∈ set spts ∧ r ∈ set (normalize_match rst)")
prefer 2
apply blast
apply(elim exE conjE, rename_tac s r)
apply(simp)
using normalize_match_preserves_normalized_n_primitive by blast
show "normalized_nnf_match m ⟹
normalized_n_primitive (disc2, sel2) f m ⟹
a ∈ set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)) ⟹
normalized_n_primitive (disc2, sel2) f a"
apply(case_tac "¬ has_disc_negated disc False m")
subgoal
using rewrite_negated_primitives_normalized_no_modification[OF wf_disc_sel] by blast
apply(simp add: rewrite_negated_primitives_def)
apply(case_tac "primitive_extractor (disc, sel) m", rename_tac spts rst)
apply(simp)
apply(subgoal_tac "normalized_n_primitive (disc2, sel2) f rst")
prefer 2 subgoal for spts rst
apply(drule primitive_extractor_correct(5)[OF _ wf_disc_sel, where P="f"])
apply blast
by(simp)
apply(insert disc_p, simp)
apply(drule(1) primitive_extractor_correct(8)[OF _ wf_disc_sel])
apply(simp)
apply(elim bexE)
apply(erule helper_a_normalized)
subgoal for spts
apply(rule_tac pts="(getNeg spts)" in negated_normalized_folded_ports_normalized_n_primitive[where C=C])
using disc apply(simp; fail)
using disc_p primitive_extractor_correct(8)[OF _ wf_disc_sel] apply blast
by simp
subgoal for x
apply(intro ballI)
apply(rule andfold_MatchExp_normalized_normalized_n_primitive_single[where C=C])
using disc disc_p by(simp)+
by blast
qed
definition rewrite_negated_src_ports
:: "'i::len common_primitive match_expr ⇒ 'i common_primitive match_expr" where
"rewrite_negated_src_ports m ≡
rewrite_negated_primitives (is_Src_Ports, src_ports_sel) Src_Ports l4_ports_negate_one m"
definition rewrite_negated_dst_ports
:: "'i::len common_primitive match_expr ⇒ 'i common_primitive match_expr" where
"rewrite_negated_dst_ports m ≡
rewrite_negated_primitives (is_Dst_Ports, dst_ports_sel) Dst_Ports l4_ports_negate_one m"
value "rewrite_negated_src_ports (MatchAnd (Match (Dst (IpAddrNetmask (ipv4addr_of_dotdecimal (127, 0, 0, 0)) 8)))
(MatchAnd (Match (Prot (Proto TCP)))
(MatchNot (Match (Src_Ports (L4Ports UDP [(80,80)]))))
))"
value "rewrite_negated_src_ports (MatchAnd (Match (Dst (IpAddrNetmask (ipv4addr_of_dotdecimal (127, 0, 0, 0)) 8)))
(MatchAnd (Match (Prot (Proto TCP)))
(MatchNot (Match (Extra ''foobar'')))
))"
lemma rewrite_negated_src_ports:
assumes generic: "primitive_matcher_generic β" and n: "normalized_nnf_match m"
shows "matches (β, α) (rewrite_negated_src_ports m) a p ⟷ matches (β, α) m a p"
apply(simp add: rewrite_negated_src_ports_def)
apply(rule rewrite_negated_primitives)
by(simp add: l4_ports_negate_one[OF generic] n wf_disc_sel_common_primitive(1))+
lemma rewrite_negated_dst_ports:
assumes generic: "primitive_matcher_generic β" and n: "normalized_nnf_match m"
shows "matches (β, α) (rewrite_negated_dst_ports m) a p ⟷ matches (β, α) m a p"
apply(simp add: rewrite_negated_dst_ports_def)
apply(rule rewrite_negated_primitives)
by(simp add: l4_ports_negate_one[OF generic] n wf_disc_sel_common_primitive(2))+
lemma rewrite_negated_src_ports_not_has_disc_negated:
assumes n: "normalized_nnf_match m"
shows "¬ has_disc_negated is_Src_Ports False (rewrite_negated_src_ports m)"
apply(simp add: rewrite_negated_src_ports_def)
apply(rule rewrite_negated_primitives_not_has_disc_negated)
by(simp add: n wf_disc_sel_common_primitive(1) l4_ports_negate_one_not_has_disc_negated)+
lemma rewrite_negated_dst_ports_not_has_disc_negated:
assumes n: "normalized_nnf_match m"
shows "¬ has_disc_negated is_Dst_Ports False (rewrite_negated_dst_ports m)"
apply(simp add: rewrite_negated_dst_ports_def)
apply(rule rewrite_negated_primitives_not_has_disc_negated)
by(simp add: n wf_disc_sel_common_primitive(2) l4_ports_negate_one_not_has_disc_negated)+
lemma "¬ has_disc_negated disc t m ⟹ ∀m' ∈ set (normalize_match m). ¬ has_disc_negated disc t m'"
by(fact i_m_giving_this_a_funny_name_so_i_can_thank_my_future_me_when_sledgehammer_will_find_this_one_day)
corollary normalize_rewrite_negated_src_ports_not_has_disc_negated:
assumes n: "normalized_nnf_match m"
shows "∀m' ∈ set (normalize_match (rewrite_negated_src_ports m)). ¬ has_disc_negated is_Src_Ports False m'"
apply(rule i_m_giving_this_a_funny_name_so_i_can_thank_my_future_me_when_sledgehammer_will_find_this_one_day)
apply(rule rewrite_negated_src_ports_not_has_disc_negated)
using n by simp
subsection‹Normalizing Positive Matches on Ports›
fun singletonize_L4Ports :: "ipt_l4_ports ⇒ ipt_l4_ports list" where
"singletonize_L4Ports (L4Ports proto pts) = map (λp. L4Ports proto [p]) pts"
lemma singletonize_L4Ports_src: assumes generic: "primitive_matcher_generic β"
shows "match_list (β, α) (map (Match ∘ Src_Ports) (singletonize_L4Ports pts)) a p ⟷
matches (β, α) (Match (Src_Ports pts)) a p"
apply(cases pts)
apply(simp add: match_list_matches primitive_matcher_generic.Ports_single[OF generic])
apply(simp add: ports_to_set)
by auto
lemma singletonize_L4Ports_dst: assumes generic: "primitive_matcher_generic β"
shows "match_list (β, α) (map (Match ∘ Dst_Ports) (singletonize_L4Ports pts)) a p ⟷
matches (β, α) (Match (Dst_Ports pts)) a p"
apply(cases pts)
apply(simp add: match_list_matches primitive_matcher_generic.Ports_single[OF generic])
apply(simp add: ports_to_set)
by auto
lemma singletonize_L4Ports_normalized_generic:
assumes wf_disc_sel: "wf_disc_sel (disc,sel) C"
and "m' ∈ (λspt. Match (C spt)) ` set (singletonize_L4Ports pt)"
shows "normalized_n_primitive (disc, sel) (case_ipt_l4_ports (λx pts. length pts ≤ 1)) m'"
using assms
apply(case_tac pt)
apply(simp)
apply(induction m')
by(auto simp: wf_disc_sel.simps)
lemma singletonize_L4Ports_normalized_src_ports:
"m' ∈ (λspt. Match (Src_Ports spt)) ` set (singletonize_L4Ports pt) ⟹ normalized_src_ports m'"
apply(simp add: normalized_src_ports_def2)
using singletonize_L4Ports_normalized_generic[OF wf_disc_sel_common_primitive(1)] by blast
lemma singletonize_L4Ports_normalized_dst_ports:
"m' ∈ (λspt. Match (Dst_Ports spt)) ` set (singletonize_L4Ports pt) ⟹ normalized_dst_ports m'"
apply(simp add: normalized_dst_ports_def2)
using singletonize_L4Ports_normalized_generic[OF wf_disc_sel_common_primitive(2)] by blast
declare singletonize_L4Ports.simps[simp del]
lemma normalized_ports_singletonize_combine_rst:
assumes wf_disc_sel: "wf_disc_sel (disc,sel) C"
shows "normalized_n_primitive (disc, sel) (case_ipt_l4_ports (λx pts. length pts ≤ 1)) rst ⟹
m' ∈ (λspt. MatchAnd (Match (C spt)) rst) ` set (singletonize_L4Ports pt) ⟹
normalized_n_primitive (disc, sel) (case_ipt_l4_ports (λx pts. length pts ≤ 1)) m'"
apply simp
apply(rule normalized_n_primitive_MatchAnd_combine_map)
apply(simp_all)
using singletonize_L4Ports_normalized_generic[OF wf_disc_sel] by fastforce
text‹Normalizing match expressions such that at most one port will exist in it.
Returns a list of match expressions (splits one firewall rule into several rules).›
definition normalize_positive_ports_step
:: "(('i::len common_primitive ⇒ bool) × ('i common_primitive ⇒ ipt_l4_ports)) ⇒
(ipt_l4_ports ⇒ 'i common_primitive) ⇒
'i common_primitive match_expr ⇒ 'i common_primitive match_expr list" where
"normalize_positive_ports_step disc_sel C m ≡
let (spts, rst) = primitive_extractor disc_sel m in
case (getPos spts, getNeg spts)
of (pspts, []) ⇒ (case l4_ports_compress pspts of CannotMatch ⇒ []
| MatchesAll ⇒ [rst]
| MatchExpr m ⇒ map (λspt. (MatchAnd (Match (C spt)) rst)) (singletonize_L4Ports m)
)
| (_, _) ⇒ undefined"
lemma normalize_positive_ports_step_nnf:
assumes n: "normalized_nnf_match m" and wf_disc_sel: "wf_disc_sel (disc,sel) C"
and noneg: "¬ has_disc_negated disc False m"
shows "m' ∈ set (normalize_positive_ports_step (disc,sel) C m) ⟹ normalized_nnf_match m'"
apply(simp add: normalize_positive_ports_step_def)
apply(elim exE conjE, rename_tac rst spts)
apply(drule sym)
apply(frule primitive_extractor_correct(2)[OF n wf_disc_sel])
apply(subgoal_tac "getNeg spts = []")
prefer 2 subgoal
apply(drule primitive_extractor_correct(8)[OF n wf_disc_sel])
using noneg by simp+
apply(simp split: match_compress.split_asm)
by fastforce
lemma normalize_positive_ports_step_normalized_n_primitive:
assumes n: "normalized_nnf_match m" and wf_disc_sel: "wf_disc_sel (disc,sel) C"
and noneg: "¬ has_disc_negated disc False m"
shows "∀m' ∈ set (normalize_positive_ports_step (disc,sel) C m).
normalized_n_primitive (disc,sel) (λps. case ps of L4Ports _ pts ⇒ length pts ≤ 1) m'"
unfolding normalize_positive_ports_step_def
apply(intro ballI, rename_tac m')
apply(simp)
apply(elim exE conjE, rename_tac rst spts)
apply(drule sym)
apply(frule primitive_extractor_correct(2)[OF n wf_disc_sel])
apply(frule primitive_extractor_correct(3)[OF n wf_disc_sel])
apply(subgoal_tac "getNeg spts = []")
prefer 2 subgoal
apply(drule primitive_extractor_correct(8)[OF n wf_disc_sel])
using noneg by simp+
apply(subgoal_tac "normalized_n_primitive (disc,sel) (λps. case ps of L4Ports _ pts ⇒ length pts ≤ 1) rst")
prefer 2 subgoal
by(drule(2) normalized_n_primitive_if_no_primitive)
apply(simp split: match_compress.split_asm)
using normalized_ports_singletonize_combine_rst[OF wf_disc_sel] by blast
definition normalize_positive_src_ports :: "'i::len common_primitive match_expr ⇒ 'i common_primitive match_expr list" where
"normalize_positive_src_ports = normalize_positive_ports_step (is_Src_Ports, src_ports_sel) Src_Ports"
definition normalize_positive_dst_ports :: "'i::len common_primitive match_expr ⇒ 'i common_primitive match_expr list" where
"normalize_positive_dst_ports = normalize_positive_ports_step (is_Dst_Ports, dst_ports_sel) Dst_Ports"
lemma noNeg_mapNegPos_helper: "getNeg ls = [] ⟹
map (Pos ∘ C) (getPos ls) = NegPos_map C ls"
by(induction ls rule: getPos.induct) simp+
lemma normalize_positive_src_ports:
assumes generic: "primitive_matcher_generic β"
and n: "normalized_nnf_match m"
and noneg: "¬ has_disc_negated is_Src_Ports False m"
shows
"match_list (β, α) (normalize_positive_src_ports m) a p ⟷ matches (β, α) m a p"
apply(simp add: normalize_positive_src_ports_def normalize_positive_ports_step_def)
apply(case_tac "primitive_extractor (is_Src_Ports, src_ports_sel) m", rename_tac spts rst)
apply(simp)
apply(subgoal_tac "getNeg spts = []")
prefer 2 subgoal
apply(drule primitive_extractor_correct(8)[OF n wf_disc_sel_common_primitive(1)])
using noneg by simp+
apply(simp)
apply(drule primitive_extractor_correct(1)[OF n wf_disc_sel_common_primitive(1), where γ="(β, α)" and a=a and p=p])
apply(case_tac "l4_ports_compress (getPos spts)")
apply(simp)
apply(drule raw_ports_compress_src_CannotMatch[OF generic, where α=α and a=a and p=p])
apply(simp add: noNeg_mapNegPos_helper; fail)
apply(simp)
apply(drule raw_ports_compress_MatchesAll[OF generic, where α=α and a=a and p=p])
apply(simp add: noNeg_mapNegPos_helper; fail)
apply(simp add: bunch_of_lemmata_about_matches)
apply(drule raw_ports_compress_src_MatchExpr[OF generic, where α=α and a=a and p=p])
apply(insert singletonize_L4Ports_src[OF generic, where α=α and a=a and p=p])
apply(simp add: match_list_matches)
apply(simp add: bunch_of_lemmata_about_matches)
apply(simp add: noNeg_mapNegPos_helper; fail)
done
lemma normalize_positive_dst_ports:
assumes generic: "primitive_matcher_generic β"
and n: "normalized_nnf_match m"
and noneg: "¬ has_disc_negated is_Dst_Ports False m"
shows "match_list (β, α) (normalize_positive_dst_ports m) a p ⟷ matches (β, α) m a p"
apply(simp add: normalize_positive_dst_ports_def normalize_positive_ports_step_def)
apply(case_tac "primitive_extractor (is_Dst_Ports, dst_ports_sel) m", rename_tac spts rst)
apply(simp)
apply(subgoal_tac "getNeg spts = []")
prefer 2 subgoal
apply(drule primitive_extractor_correct(8)[OF n wf_disc_sel_common_primitive(2)])
using noneg by simp+
apply(simp)
apply(drule primitive_extractor_correct(1)[OF n wf_disc_sel_common_primitive(2), where γ="(β, α)" and a=a and p=p])
apply(case_tac "l4_ports_compress (getPos spts)")
apply(simp)
apply(drule raw_ports_compress_dst_CannotMatch[OF generic, where α=α and a=a and p=p])
apply(simp add: noNeg_mapNegPos_helper; fail)
apply(simp)
apply(drule raw_ports_compress_MatchesAll(2)[OF generic, where α=α and a=a and p=p])
apply(simp add: noNeg_mapNegPos_helper; fail)
apply(simp add: bunch_of_lemmata_about_matches)
apply(drule raw_ports_compress_dst_MatchExpr[OF generic, where α=α and a=a and p=p])
apply(insert singletonize_L4Ports_dst[OF generic, where α=α and a=a and p=p])
apply(simp add: match_list_matches)
apply(simp add: bunch_of_lemmata_about_matches)
apply(simp add: noNeg_mapNegPos_helper; fail)
done
lemma normalize_positive_src_ports_nnf:
assumes n: "normalized_nnf_match m"
and noneg: "¬ has_disc_negated is_Src_Ports False m"
shows "m' ∈ set (normalize_positive_src_ports m) ⟹ normalized_nnf_match m'"
apply(rule normalize_positive_ports_step_nnf[OF n wf_disc_sel_common_primitive(1) noneg])
by(simp add: normalize_positive_src_ports_def)
lemma normalize_positive_dst_ports_nnf:
assumes n: "normalized_nnf_match m"
and noneg: "¬ has_disc_negated is_Dst_Ports False m"
shows "m' ∈ set (normalize_positive_dst_ports m) ⟹ normalized_nnf_match m'"
apply(rule normalize_positive_ports_step_nnf[OF n wf_disc_sel_common_primitive(2) noneg])
by(simp add: normalize_positive_dst_ports_def)
lemma normalize_positive_src_ports_normalized_n_primitive:
assumes n: "normalized_nnf_match m"
and noneg: "¬ has_disc_negated is_Src_Ports False m"
shows "∀m' ∈ set (normalize_positive_src_ports m). normalized_src_ports m'"
unfolding normalized_src_ports_def2
unfolding normalize_positive_src_ports_def
using normalize_positive_ports_step_normalized_n_primitive[OF n wf_disc_sel_common_primitive(1) noneg] by blast
lemma normalize_positive_dst_ports_normalized_n_primitive:
assumes n: "normalized_nnf_match m"
and noneg: "¬ has_disc_negated is_Dst_Ports False m"
shows "∀m' ∈ set (normalize_positive_dst_ports m). normalized_dst_ports m'"
unfolding normalized_dst_ports_def2
unfolding normalize_positive_dst_ports_def
using normalize_positive_ports_step_normalized_n_primitive[OF n wf_disc_sel_common_primitive(2) noneg] by blast
subsection‹Complete Normalization›
definition normalize_ports_generic
:: "('i common_primitive match_expr ⇒ 'i common_primitive match_expr list) ⇒
('i common_primitive match_expr ⇒ 'i common_primitive match_expr) ⇒
'i::len common_primitive match_expr ⇒ 'i common_primitive match_expr list"
where
"normalize_ports_generic normalize_pos rewrite_neg m = concat (map normalize_pos (normalize_match (rewrite_neg m)))"
lemma normalize_ports_generic_nnf:
assumes n: "normalized_nnf_match m"
and inset: "m' ∈ set (normalize_ports_generic normalize_pos rewrite_neg m)"
and noNeg: "¬ has_disc_negated disc False (rewrite_neg m)"
and normalize_nnf_pos: "⋀m m'.
normalized_nnf_match m ⟹ ¬ has_disc_negated disc False m ⟹
m' ∈ set (normalize_pos m) ⟹ normalized_nnf_match m'"
shows "normalized_nnf_match m'"
using inset apply(simp add: normalize_ports_generic_def)
apply(elim bexE, rename_tac a)
apply(subgoal_tac "normalized_nnf_match a")
prefer 2
using normalized_nnf_match_normalize_match apply blast
apply(erule normalize_nnf_pos, simp_all)
apply(rule not_has_disc_normalize_match)
using noNeg n by blast+
lemma normalize_ports_generic:
assumes n: "normalized_nnf_match m"
and normalize_pos: "⋀m. normalized_nnf_match m ⟹ ¬ has_disc_negated disc False m ⟹
match_list γ (normalize_pos m) a p ⟷ matches γ m a p"
and rewrite_neg: "⋀m. normalized_nnf_match m ⟹
matches γ (rewrite_neg m) a p = matches γ m a p"
and noNeg: "⋀m. normalized_nnf_match m ⟹ ¬ has_disc_negated disc False (rewrite_neg m)"
shows
"match_list γ (normalize_ports_generic normalize_pos rewrite_neg m) a p ⟷ matches γ m a p"
unfolding normalize_ports_generic_def
proof
have 1: "ls ∈ set (normalize_match (rewrite_neg m)) ⟹
match_list γ (normalize_pos ls) a p ⟹ normalized_nnf_match ls ⟹ matches γ m a p"
for ls
apply(subst(asm) normalize_pos)
subgoal using normalized_nnf_match_normalize_match by blast
subgoal apply(rule_tac m="rewrite_neg m" in not_has_disc_normalize_match)
using noNeg n apply blast
by blast
apply(subgoal_tac "matches γ (rewrite_neg m) a p")
using rewrite_neg[OF n] apply blast
using in_normalized_matches[where γ=γ and a=a and p=p] by blast
show "match_list γ (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p ⟹ matches γ m a p"
apply(simp add: match_list_concat)
apply(clarify, rename_tac ls)
apply(subgoal_tac "normalized_nnf_match ls")
using 1 apply(simp; fail)
using normalized_nnf_match_normalize_match by blast
next
have 1: "ls ∈ set (normalize_match (rewrite_neg m)) ⟹
matches γ ls a p ⟹
normalized_nnf_match ls ⟹
match_list γ (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p" for ls
apply(simp add: match_list_concat)
apply(rule_tac x=ls in bexI)
prefer 2 apply(simp; fail)
apply(subst normalize_pos)
apply(simp_all)
apply(rule_tac m="rewrite_neg m" in not_has_disc_normalize_match)
using noNeg n apply blast
by blast
show "matches γ m a p ⟹ match_list γ (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p"
apply(subst(asm) rewrite_neg[OF n, symmetric])
apply(subst(asm) matches_to_match_list_normalize)
apply(subst(asm) match_list_matches)
apply(elim bexE, rename_tac ls)
apply(subgoal_tac "normalized_nnf_match ls")
using 1 apply blast
using normalized_nnf_match_normalize_match by blast
qed
lemma normalize_ports_generic_normalized_n_primitive:
assumes n: "normalized_nnf_match m" and wf_disc_sel: "wf_disc_sel (disc,sel) C"
and noNeg: "⋀m. normalized_nnf_match m ⟹ ¬ has_disc_negated disc False (rewrite_neg m)"
and normalize_nnf_pos: "⋀m m'.
normalized_nnf_match m ⟹ ¬ has_disc_negated disc False m ⟹
m' ∈ set (normalize_pos m) ⟹ normalized_nnf_match m'"
and normalize_pos: "⋀m m'.
normalized_nnf_match m ⟹ ¬ has_disc_negated disc False m ⟹
∀m'∈set (normalize_pos m).
normalized_n_primitive (disc,sel) (λps. case ps of L4Ports _ pts ⇒ length pts ≤ 1) m'"
shows "∀m' ∈ set (normalize_ports_generic normalize_pos rewrite_neg m).
normalized_n_primitive (disc,sel) (λps. case ps of L4Ports _ pts ⇒ length pts ≤ 1) m'"
unfolding normalize_ports_generic_def
apply(intro ballI, rename_tac m')
apply(simp)
apply(elim bexE, rename_tac a)
apply(subgoal_tac "normalized_nnf_match a")
prefer 2
using normalized_nnf_match_normalize_match apply blast
apply(subgoal_tac "¬ has_disc_negated disc False a")
prefer 2
subgoal for ls
apply(rule_tac m="rewrite_neg m" in not_has_disc_normalize_match)
using noNeg n apply blast
by blast
apply(subgoal_tac "normalized_nnf_match m'")
prefer 2
using normalize_nnf_pos apply blast
using normalize_pos by blast
lemma normalize_ports_generic_normalize_positive_ports_step_erule:
assumes n: "normalized_nnf_match m"
and wf_disc_sel: "wf_disc_sel (disc, sel) C"
and noProt: "∀a. ¬ disc (Prot a)"
and P: "P (disc2, sel2) m"
and P1: "⋀a. normalized_nnf_match a ⟹
a ∈ set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)) ⟹
P (disc2, sel2) a"
and P2: "⋀a dpts rst. normalized_nnf_match a ⟹
primitive_extractor (disc, sel) a = (dpts, rst) ⟹
getNeg dpts = [] ⟹ P (disc2, sel2) a ⟹ P (disc2, sel2) rst"
and P3: "⋀ a spt rst. P (disc2, sel2) rst ⟹ P (disc2, sel2) (MatchAnd (Match (C spt)) rst)"
shows "m' ∈ set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m) ⟹
P (disc2, sel2) m'"
using P apply(simp add: normalize_ports_generic_def)
apply(elim bexE, rename_tac a)
apply(subgoal_tac "normalized_nnf_match a")
prefer 2 using normalized_nnf_match_normalize_match apply blast
apply(simp add: normalize_positive_ports_step_def)
apply(elim exE conjE, rename_tac rst dpts)
apply(drule sym)
apply(subgoal_tac "getNeg dpts = []")
prefer 2 subgoal for a rst dpts
apply(erule iffD1[OF primitive_extractor_correct(8)[OF _ wf_disc_sel]])
apply(simp; fail)
apply(rule not_has_disc_normalize_match)
apply(simp_all)
apply(rule rewrite_negated_primitives_not_has_disc_negated[OF n wf_disc_sel])
apply(intro allI)
apply(rule l4_ports_negate_one_not_has_disc_negated_generic)
by(simp add: noProt)
apply(subgoal_tac "P (disc2, sel2) a")
prefer 2 subgoal
apply(rule P1)
by(simp)
apply(frule_tac a=a in P2)
apply blast+
apply(simp split: match_compress.split_asm)
using P3 by auto
lemma normalize_ports_generic_preserves_normalized_n_primitive:
assumes n: "normalized_nnf_match m"
and wf_disc_sel: "wf_disc_sel (disc, sel) C"
and noProt: "∀a. ¬ disc (Prot a)"
and disc2_noC: "∀a. ¬ disc2 (C a)"
and disc2_noProt: "(∀a. ¬ disc2 (Prot a)) ∨ ¬ has_disc_negated disc False m"
shows "m' ∈ set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m) ⟹
normalized_n_primitive (disc2, sel2) f m ⟹
normalized_n_primitive (disc2, sel2) f m'"
thm normalize_ports_generic_normalize_positive_ports_step_erule
apply(rule normalize_ports_generic_normalize_positive_ports_step_erule[OF n wf_disc_sel noProt])
apply(simp_all add: disc2_noC disc2_noProt)
apply(rule rewrite_negated_primitives_normalized_preserves_unrelated_helper[OF wf_disc_sel _ _ n])
apply(simp_all add: disc2_noC disc2_noProt)
apply(frule_tac m=a in primitive_extractor_correct(5)[OF _ wf_disc_sel, where P=f])
by blast+
lemma normalize_ports_generic_preserves_normalized_not_has_disc:
assumes n: "normalized_nnf_match m" and nodisc: "¬ has_disc disc2 m"
and wf_disc_sel: "wf_disc_sel (disc, sel) C"
and noProt: "∀a. ¬ disc (Prot a)"
and disc2_noC: "∀a. ¬ disc2 (C a)"
and disc2_noProt: "(∀a. ¬ disc2 (Prot a)) ∨ ¬ has_disc_negated disc False m"
shows "m'∈ set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m)
⟹ ¬ has_disc disc2 m'"
apply(rule normalize_ports_generic_normalize_positive_ports_step_erule[OF n wf_disc_sel noProt])
apply(simp_all add: disc2_noC disc2_noProt nodisc)
subgoal for a
thm normalize_match_preserves_nodisc
apply(rule_tac m="rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m" in normalize_match_preserves_nodisc)
apply(simp_all)
apply(insert disc2_noProt)
apply(elim disjE)
thm rewrite_negated_primitives_not_has_disc[of _ disc2]
subgoal apply(rule rewrite_negated_primitives_not_has_disc[OF n wf_disc_sel nodisc _ disc2_noC])
using l4_ports_negate_one_nodisc[OF disc2_noC] by blast
using rewrite_negated_primitives_preserves_not_has_disc[OF n wf_disc_sel nodisc _ disc2_noC] by blast
apply(frule_tac m=a in primitive_extractor_correct(4)[OF _ wf_disc_sel])
by blast+
lemma normalize_ports_generic_preserves_normalized_not_has_disc_negated:
assumes n: "normalized_nnf_match m" and nodisc: "¬ has_disc_negated disc2 False m"
and wf_disc_sel: "wf_disc_sel (disc, sel) C"
and noProt: "∀a. ¬ disc (Prot a)"
and disc2_noProt: "(∀a. ¬ disc2 (Prot a)) ∨ ¬ has_disc_negated disc False m"
shows "m'∈ set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m)
⟹ ¬ has_disc_negated disc2 False m'"
apply(rule normalize_ports_generic_normalize_positive_ports_step_erule[OF n wf_disc_sel noProt])
apply(simp_all add: disc2_noProt nodisc)
subgoal for a
apply(rule_tac m="rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m" in not_has_disc_normalize_match)
apply(simp_all)
apply(rule rewrite_negated_primitives_preserves_not_has_disc_negated[OF n wf_disc_sel ])
using disc2_noProt l4_ports_negate_one_not_has_disc_negated_generic apply blast
using nodisc by blast
subgoal for a dpts rst
apply(frule_tac m=a and as=dpts and ms=rst and neg=False in primitive_extractor_correct(6)[OF _ wf_disc_sel])
by blast+
done
definition normalize_src_ports
:: "'i::len common_primitive match_expr ⇒ 'i common_primitive match_expr list"
where
"normalize_src_ports m = normalize_ports_generic normalize_positive_src_ports rewrite_negated_src_ports m"
definition normalize_dst_ports
:: "'i::len common_primitive match_expr ⇒ 'i common_primitive match_expr list"
where
"normalize_dst_ports m = normalize_ports_generic normalize_positive_dst_ports rewrite_negated_dst_ports m"
lemma normalize_src_ports:
assumes generic: "primitive_matcher_generic β"
and n: "normalized_nnf_match m"
shows "match_list (β, α) (normalize_src_ports m) a p ⟷ matches (β, α) m a p"
apply(simp add: normalize_src_ports_def)
apply(rule normalize_ports_generic[OF n])
using normalize_positive_src_ports[OF generic]
rewrite_negated_src_ports[OF generic, where α=α and a=a and p=p]
rewrite_negated_src_ports_not_has_disc_negated by blast+
lemma normalize_dst_ports:
assumes generic: "primitive_matcher_generic β"
and n: "normalized_nnf_match m"
shows "match_list (β, α) (normalize_dst_ports m) a p ⟷ matches (β, α) m a p"
apply(simp add: normalize_dst_ports_def)
apply(rule normalize_ports_generic[OF n])
using normalize_positive_dst_ports[OF generic]
rewrite_negated_dst_ports[OF generic, where α=α and a=a and p=p]
rewrite_negated_dst_ports_not_has_disc_negated by blast+
lemma normalize_src_ports_normalized_n_primitive:
assumes n:"normalized_nnf_match m"
shows "∀m' ∈ set (normalize_src_ports m). normalized_src_ports m'"
unfolding normalize_src_ports_def normalized_src_ports_def2
apply(rule normalize_ports_generic_normalized_n_primitive[OF n wf_disc_sel_common_primitive(1)])
using rewrite_negated_src_ports_not_has_disc_negated apply blast
using normalize_positive_src_ports_nnf apply blast
unfolding normalized_src_ports_def2[symmetric]
using normalize_positive_src_ports_normalized_n_primitive by blast
lemma normalize_dst_ports_normalized_n_primitive:
assumes n: "normalized_nnf_match m"
shows "∀m' ∈ set (normalize_dst_ports m). normalized_dst_ports m'"
unfolding normalize_dst_ports_def normalized_dst_ports_def2
apply(rule normalize_ports_generic_normalized_n_primitive[OF n wf_disc_sel_common_primitive(2)])
using rewrite_negated_dst_ports_not_has_disc_negated apply blast
using normalize_positive_dst_ports_nnf apply blast
unfolding normalized_dst_ports_def2[symmetric]
using normalize_positive_dst_ports_normalized_n_primitive by blast
lemma normalize_src_ports_nnf:
assumes n: "normalized_nnf_match m"
shows "m' ∈ set (normalize_src_ports m) ⟹ normalized_nnf_match m'"
apply(simp add: normalize_src_ports_def)
apply(erule normalize_ports_generic_nnf[OF n])
using n rewrite_negated_src_ports_not_has_disc_negated apply blast
using normalize_positive_src_ports_nnf by blast
lemma normalize_dst_ports_nnf:
assumes n: "normalized_nnf_match m"
shows "m' ∈ set (normalize_dst_ports m) ⟹ normalized_nnf_match m'"
apply(simp add: normalize_dst_ports_def)
apply(erule normalize_ports_generic_nnf[OF n])
using n rewrite_negated_dst_ports_not_has_disc_negated apply blast
using normalize_positive_dst_ports_nnf by blast
lemma normalize_src_ports_preserves_normalized_n_primitive:
assumes n: "normalized_nnf_match m"
and disc2_noC: "∀a. ¬ disc2 (Src_Ports a)"
and disc2_noProt: "(∀a. ¬ disc2 (Prot a)) ∨ ¬ has_disc_negated is_Src_Ports False m"
shows "m' ∈ set (normalize_src_ports m) ⟹
normalized_n_primitive (disc2, sel2) f m ⟹
normalized_n_primitive (disc2, sel2) f m'"
apply(rule normalize_ports_generic_preserves_normalized_n_primitive[OF n wf_disc_sel_common_primitive(1)])
by(simp_all add: disc2_noC disc2_noProt normalize_src_ports_def normalize_ports_generic_def
normalize_positive_src_ports_def rewrite_negated_src_ports_def)
lemma normalize_dst_ports_preserves_normalized_n_primitive:
assumes n: "normalized_nnf_match m"
and disc2_noC: "∀a. ¬ disc2 (Dst_Ports a)"
and disc2_noProt: "(∀a. ¬ disc2 (Prot a)) ∨ ¬ has_disc_negated is_Dst_Ports False m"
shows "m' ∈ set (normalize_dst_ports m) ⟹
normalized_n_primitive (disc2, sel2) f m ⟹
normalized_n_primitive (disc2, sel2) f m'"
apply(rule normalize_ports_generic_preserves_normalized_n_primitive[OF n wf_disc_sel_common_primitive(2)])
by(simp_all add: disc2_noC disc2_noProt normalize_dst_ports_def normalize_ports_generic_def
normalize_positive_dst_ports_def rewrite_negated_dst_ports_def)
lemma normalize_src_ports_preserves_normalized_not_has_disc:
assumes n: "normalized_nnf_match m" and nodisc: "¬ has_disc disc2 m"
and disc2_noC: "∀a. ¬ disc2 (Src_Ports a)"
and disc2_noProt: "(∀a. ¬ disc2 (Prot a)) ∨ ¬ has_disc_negated is_Src_Ports False m"
shows "m'∈ set (normalize_src_ports m)
⟹ ¬ has_disc disc2 m'"
apply(rule normalize_ports_generic_preserves_normalized_not_has_disc[OF n nodisc wf_disc_sel_common_primitive(1)])
apply(simp add: disc2_noC disc2_noProt)+
by (simp add: normalize_ports_generic_def normalize_positive_src_ports_def normalize_src_ports_def rewrite_negated_src_ports_def)
lemma normalize_dst_ports_preserves_normalized_not_has_disc:
assumes n: "normalized_nnf_match m" and nodisc: "¬ has_disc disc2 m"
and disc2_noC: "∀a. ¬ disc2 (Dst_Ports a)"
and disc2_noProt: "(∀a. ¬ disc2 (Prot a)) ∨ ¬ has_disc_negated is_Dst_Ports False m"
shows "m'∈ set (normalize_dst_ports m)
⟹ ¬ has_disc disc2 m'"
apply(rule normalize_ports_generic_preserves_normalized_not_has_disc[OF n nodisc wf_disc_sel_common_primitive(2)])
apply(simp add: disc2_noC disc2_noProt)+
by (simp add: normalize_ports_generic_def normalize_positive_dst_ports_def normalize_dst_ports_def rewrite_negated_dst_ports_def)
lemma normalize_src_ports_preserves_normalized_not_has_disc_negated:
assumes n: "normalized_nnf_match m" and nodisc: "¬ has_disc_negated disc2 False m"
and disc2_noProt: "(∀a. ¬ disc2 (Prot a)) ∨ ¬ has_disc_negated is_Src_Ports False m"
shows "m'∈ set (normalize_src_ports m)
⟹ ¬ has_disc_negated disc2 False m'"
apply(rule normalize_ports_generic_preserves_normalized_not_has_disc_negated[OF n nodisc wf_disc_sel_common_primitive(1)])
apply(simp add: disc2_noProt)+
by (simp add: normalize_ports_generic_def normalize_positive_src_ports_def normalize_src_ports_def rewrite_negated_src_ports_def)
lemma normalize_dst_ports_preserves_normalized_not_has_disc_negated:
assumes n: "normalized_nnf_match m" and nodisc: "¬ has_disc_negated disc2 False m"
and disc2_noProt: "(∀a. ¬ disc2 (Prot a)) ∨ ¬ has_disc_negated is_Dst_Ports False m"
shows "m'∈ set (normalize_dst_ports m)
⟹ ¬ has_disc_negated disc2 False m'"
apply(rule normalize_ports_generic_preserves_normalized_not_has_disc_negated[OF n nodisc wf_disc_sel_common_primitive(2)])
apply(simp add: disc2_noProt)+
by (simp add: normalize_ports_generic_def normalize_positive_dst_ports_def normalize_dst_ports_def rewrite_negated_dst_ports_def)
value[code] "normalize_src_ports
(MatchAnd (Match (Dst (IpAddrNetmask (ipv4addr_of_dotdecimal (127, 0, 0, 0)) 8)))
(MatchAnd (Match (Prot (Proto TCP)))
(MatchNot (Match (Src_Ports (L4Ports UDP [(80,80)]))))
))"
lemma "map opt_MatchAny_match_expr (normalize_src_ports
(MatchAnd (Match (Dst (IpAddrNetmask (ipv4addr_of_dotdecimal (127, 0, 0, 0)) 8)))
(MatchAnd (Match (Prot (Proto TCP)))
(MatchNot (Match (Src_Ports (L4Ports UDP [(80,80)]))))
))) =
[MatchAnd (MatchNot (Match (Prot (Proto UDP)))) (MatchAnd (Match (Dst (IpAddrNetmask 0x7F000000 8))) (Match (Prot (Proto TCP)))),
MatchAnd (Match (Src_Ports (L4Ports UDP [(0, 79)]))) (MatchAnd (Match (Dst (IpAddrNetmask 0x7F000000 8))) (Match (Prot (Proto TCP)))),
MatchAnd (Match (Src_Ports (L4Ports UDP [(81, 0xFFFF)]))) (MatchAnd (Match (Dst (IpAddrNetmask 0x7F000000 8))) (Match (Prot (Proto TCP))))]" by eval
lemma "map opt_MatchAny_match_expr (normalize_src_ports
(MatchAnd (Match (Dst (IpAddrNetmask (ipv4addr_of_dotdecimal (127, 0, 0, 0)) 8)))
(MatchAnd (Match (Prot (Proto ICMP)))
(MatchAnd (Match (Src_Ports (L4Ports TCP [(22,22)])))
(MatchNot (Match (Src_Ports (L4Ports UDP [(80,80)]))))
))))
=
[MatchAnd (Match (Src_Ports (L4Ports TCP [(22, 22)])))
(MatchAnd (MatchNot (Match (Prot (Proto UDP)))) (MatchAnd (Match (Dst (IpAddrNetmask 0x7F000000 8))) (Match (Prot (Proto ICMP)))))]" by eval
lemma "map opt_MatchAny_match_expr (normalize_src_ports
(MatchAnd (Match ((Src_Ports (L4Ports UDP [(21,21), (22,22)])) :: 32 common_primitive))
(Match (Prot (Proto UDP)))))
=
[MatchAnd (Match (Src_Ports (L4Ports UDP [(21, 22)]))) (Match (Prot (Proto UDP)))]" by eval
lemma "normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) [])) = [MatchAny]" by(simp)
definition replace_primitive_matchexpr
:: "(('a ⇒ bool) × ('a ⇒ 'b)) ⇒
('b negation_type ⇒ 'a match_expr) ⇒
'a match_expr ⇒ 'a match_expr" where
"replace_primitive_matchexpr disc_sel replace_f m ≡
let (as, rst) = primitive_extractor disc_sel m
in if as = [] then m else
MatchAnd
(andfold_MatchExp (map replace_f as))
rst"
text‹It does nothing of there is not even a primitive in it›
lemma replace_primitive_matchexpr_unchanged_if_not_has_disc:
assumes n: "normalized_nnf_match m"
and wf_disc_sel: "wf_disc_sel (disc,sel) C"
and noDisc: "¬ has_disc disc m"
shows "replace_primitive_matchexpr (disc,sel) replace_f m = m"
apply(simp add: replace_primitive_matchexpr_def)
apply(case_tac "primitive_extractor (disc,sel) m", rename_tac spts rst)
apply(simp)
apply(frule primitive_extractor_correct(7)[OF n wf_disc_sel])
using noDisc by blast+
lemma replace_primitive_matchexpr:
assumes n: "normalized_nnf_match m" and wf_disc_sel: "wf_disc_sel disc_sel C"
and replace_f: "∀pt. matches γ (replace_f pt) a p ⟷
matches γ (negation_type_to_match_expr_f C pt) a p"
shows "matches γ (replace_primitive_matchexpr disc_sel replace_f m) a p ⟷ matches γ m a p"
proof -
obtain spts rst where pext: "primitive_extractor disc_sel m = (spts, rst)"
by(cases "primitive_extractor disc_sel m") simp
obtain disc sel where disc_sel: "disc_sel = (disc, sel)" by(cases disc_sel) simp
with wf_disc_sel have wf_disc_sel': "wf_disc_sel (disc, sel) C" by simp
from disc_sel pext have pext': "primitive_extractor (disc, sel) m = (spts, rst)" by simp
have "matches γ (andfold_MatchExp (map replace_f spts)) a p ∧ matches γ rst a p ⟷
matches γ m a p"
apply(subst primitive_extractor_correct(1)[OF n wf_disc_sel' pext', symmetric])
apply(simp add: andfold_MatchExp_matches)
apply(simp add: replace_f)
using alist_and_negation_type_to_match_expr_f_matches by fast
thus ?thesis by(simp add: replace_primitive_matchexpr_def pext bunch_of_lemmata_about_matches)
qed
lemma replace_primitive_matchexpr_replaces_disc:
assumes n: "normalized_nnf_match m" and wf_disc_sel: "wf_disc_sel (disc, sel) C"
and replace_f: "∀a. ¬ has_disc disc (replace_f a)"
shows "¬ has_disc disc (replace_primitive_matchexpr (disc, sel) replace_f m)"
apply(simp add: replace_primitive_matchexpr_def)
apply(case_tac "primitive_extractor (disc,sel) m", rename_tac spts rst)
apply(simp)
apply(frule primitive_extractor_correct(3)[OF n wf_disc_sel])
apply simp
apply(frule primitive_extractor_correct(7)[OF n wf_disc_sel])
apply simp
apply(case_tac "¬ has_disc disc m")
apply(simp)
apply(simp)
apply(frule(1) primitive_extractor_correct(9)[OF n wf_disc_sel])
apply(simp)
apply(rule MatchExpr_Fold.andfold_MatchExp_not_discI)
using replace_f by simp
lemma replace_primitive_matchexpr_preserves_not_has_disc:
assumes n: "normalized_nnf_match m" and wf_disc_sel: "wf_disc_sel (disc,sel) C"
and nodisc: "¬ has_disc disc2 m"
and replace_f: "has_disc disc m ⟹ ∀pts. ¬ has_disc disc2 (replace_f pts)"
shows "¬ has_disc disc2 (replace_primitive_matchexpr (disc,sel) replace_f m)"
apply(simp add: replace_primitive_matchexpr_def)
apply(case_tac "primitive_extractor (disc,sel) m", rename_tac spts rst)
apply(simp)
apply(frule primitive_extractor_correct(4)[OF n wf_disc_sel])
apply(case_tac "¬ has_disc disc m")
subgoal
apply(frule primitive_extractor_correct(7)[OF n wf_disc_sel])
using nodisc by blast
apply(simp)
apply(intro conjI impI)
using nodisc apply(simp; fail)
apply(rule andfold_MatchExp_not_discI)
apply(simp add: replace_f; fail)
using nodisc by blast
lemma normalize_replace_primitive_matchexpr_preserves_normalized_n_primitive:
assumes n: "normalized_nnf_match m"
and wf_disc_sel: "wf_disc_sel (disc, sel) C"
and replace_f:
"⋀a m'. m' ∈ set (normalize_match (replace_f a)) ⟹ normalized_n_primitive (disc2, sel2) f m'"
and nprim: "normalized_n_primitive (disc2, sel2) f m"
and m': "m' ∈ set (normalize_match (replace_primitive_matchexpr (disc,sel) replace_f m))"
shows "normalized_n_primitive (disc2, sel2) f m'"
proof -
have x: "x ∈ set (normalize_match (andfold_MatchExp (map replace_f as))) ⟹
normalized_n_primitive (disc2, sel2) f x" for x as
apply(rule normalize_andfold_MatchExp_normalized_n_primitive )
apply(simp_all)
using replace_f by blast
from m' show ?thesis
apply(simp add: replace_primitive_matchexpr_def)
apply(case_tac "primitive_extractor (disc, sel) m", rename_tac as rst)
apply(simp split: if_split_asm)
using normalize_match_preserves_normalized_n_primitive nprim apply blast
apply(frule_tac P=f in primitive_extractor_correct(5)[OF n wf_disc_sel])
apply(clarify)
apply(simp)
apply(intro conjI)
prefer 2
using normalize_match_preserves_normalized_n_primitive nprim apply blast
by(simp add: x)
qed
lemma normalize_replace_primitive_matchexpr_preserves_normalized_not_has_disc:
assumes n: "normalized_nnf_match m"
and wf_disc_sel: "wf_disc_sel (disc, sel) C"
and nodisc: "¬ has_disc disc2 m"
and replace_f: "⋀a. ¬ has_disc disc2 (replace_f a)"
shows "m'∈ set (normalize_match (replace_primitive_matchexpr (disc,sel) replace_f m))
⟹ ¬ has_disc disc2 m'"
apply(simp add: replace_primitive_matchexpr_def)
apply(case_tac "primitive_extractor (disc, sel) m", rename_tac as rst)
apply(simp split: if_split_asm)
using nodisc normalize_match_preserves_nodisc apply blast
apply(frule primitive_extractor_correct(4)[OF n wf_disc_sel])
apply(elim bexE, rename_tac x)
apply(erule Set.imageE, rename_tac xright)
apply(simp)
apply(intro conjI)
apply(rule normalize_match_preserves_nodisc, simp_all)
apply(rule andfold_MatchExp_not_discI, simp)
using replace_f apply blast
apply(rule normalize_match_preserves_nodisc)
apply(insert nodisc)
by(simp_all)
lemma normalize_replace_primitive_matchexpr_preserves_normalized_not_has_disc_negated:
assumes n: "normalized_nnf_match m"
and wf_disc_sel: "wf_disc_sel (disc, sel) C"
and nodisc: "¬ has_disc_negated disc2 neg m"
and replace_f: "⋀a. ¬ has_disc_negated disc2 neg (replace_f a)"
shows "m'∈ set (normalize_match (replace_primitive_matchexpr (disc,sel) replace_f m))
⟹ ¬ has_disc_negated disc2 neg m'"
apply(simp add: replace_primitive_matchexpr_def)
apply(case_tac "primitive_extractor (disc, sel) m", rename_tac as rst)
apply(simp split: if_split_asm)
using nodisc not_has_disc_normalize_match apply blast
apply(frule primitive_extractor_correct(6)[OF n wf_disc_sel, where neg=neg])
apply(elim bexE, rename_tac x)
apply(erule Set.imageE, rename_tac xright)
apply(simp)
apply(intro conjI)
apply(rule not_has_disc_normalize_match, simp_all)
apply(rule andfold_MatchExp_not_disc_negatedI, simp)
using replace_f apply blast
apply(rule not_has_disc_normalize_match)
apply(insert nodisc)
by(simp_all)
corollary normalize_replace_primitive_matchexpr:
assumes n: "normalized_nnf_match m"
and replace_f:
"⋀m. normalized_nnf_match m ⟹
matches γ (replace_primitive_matchexpr disc_sel replace_f m) a p ⟷ matches γ m a p"
shows
"match_list γ (normalize_match (replace_primitive_matchexpr disc_sel replace_f m)) a p ⟷
matches γ m a p"
by(simp add: matches_to_match_list_normalize[symmetric] replace_f n)
fun rewrite_MultiportPorts_one
:: "ipt_l4_ports negation_type⇒ 'i::len common_primitive match_expr" where
"rewrite_MultiportPorts_one (Pos pts) =
MatchOr (Match (Src_Ports pts)) (Match (Dst_Ports pts))" |
"rewrite_MultiportPorts_one (Neg pts) =
MatchAnd (MatchNot (Match (Src_Ports pts))) (MatchNot (Match (Dst_Ports pts)))"
lemma rewrite_MultiportPorts_one:
assumes generic: "primitive_matcher_generic β" and n: "normalized_nnf_match m"
shows
"matches (β, α) (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m) a p ⟷
matches (β, α) m a p"
apply(rule replace_primitive_matchexpr[OF n wf_disc_sel_common_primitive(11)])
apply(rule allI, rename_tac pt)
apply(case_tac pt)
apply(simp add: primitive_matcher_generic.MultiportPorts_single_rewrite_MatchOr[OF generic]; fail)
apply(simp add: primitive_matcher_generic.MultiportPorts_single_not_rewrite_MatchAnd[OF generic]; fail)
done
lemma "∀a. ¬ disc (Src_Ports a) ⟹ ∀a. ¬ disc (Dst_Ports a) ⟹
normalized_n_primitive (disc, sel) f m ⟹
∀m' ∈ set (normalize_match (rewrite_MultiportPorts_one a)).
normalized_n_primitive (disc, sel) f m'"
apply(cases a)
by(simp_all add: MatchOr_def)
lemma rewrite_MultiportPorts_one_nodisc:
"∀a. ¬ disc (Src_Ports a) ⟹ ∀a. ¬ disc (Dst_Ports a) ⟹
¬ has_disc disc (rewrite_MultiportPorts_one a)"
"∀a. ¬ disc (Src_Ports a) ⟹ ∀a. ¬ disc (Dst_Ports a) ⟹
¬ has_disc_negated disc neg (rewrite_MultiportPorts_one a)"
by(cases a, simp_all add: MatchOr_def)+
definition rewrite_MultiportPorts
:: "'i::len common_primitive match_expr ⇒ 'i common_primitive match_expr list" where
"rewrite_MultiportPorts m ≡ normalize_match
(replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)"
lemma rewrite_MultiportPorts:
assumes generic: "primitive_matcher_generic β"
and n: "normalized_nnf_match m"
shows
"match_list (β, α) (rewrite_MultiportPorts m) a p ⟷ matches (β, α) m a p"
unfolding rewrite_MultiportPorts_def
apply(intro normalize_replace_primitive_matchexpr[OF n])
by(simp add: rewrite_MultiportPorts_one[OF generic])
lemma rewrite_MultiportPorts_normalized_nnf_match:
"m' ∈ set (rewrite_MultiportPorts m) ⟹ normalized_nnf_match m'"
apply(simp add: rewrite_MultiportPorts_def)
using normalized_nnf_match_normalize_match by blast
text‹It does nothing of there is not even the primitive in it›
lemma rewrite_MultiportPorts_unchanged_if_not_has_disc:
assumes n: "normalized_nnf_match m"
and noDisc: "¬ has_disc is_MultiportPorts m"
shows "rewrite_MultiportPorts m = [m]"
apply(simp add: rewrite_MultiportPorts_def)
apply(subst replace_primitive_matchexpr_unchanged_if_not_has_disc[OF n
wf_disc_sel_common_primitive(11) noDisc])
using n by(fact normalize_match_already_normalized)
lemma rewrite_MultiportPorts_preserves_normalized_n_primitive:
assumes n: "normalized_nnf_match m"
and disc2_noSrcPorts: "∀a. ¬ disc2 (Src_Ports a)"
and disc2_noDstPorts: "∀a. ¬ disc2 (Dst_Ports a)"
shows "m' ∈ set (rewrite_MultiportPorts m) ⟹
normalized_n_primitive (disc2, sel2) f m ⟹
normalized_n_primitive (disc2, sel2) f m'"
unfolding rewrite_MultiportPorts_def
apply(rule normalize_replace_primitive_matchexpr_preserves_normalized_n_primitive[OF
n wf_disc_sel_common_primitive(11)])
apply simp_all
apply(rename_tac a a')
apply(case_tac a)
apply(simp_all add: MatchOr_def)
using disc2_noSrcPorts disc2_noDstPorts by fastforce+
lemma rewrite_MultiportPorts_preserves_normalized_not_has_disc:
assumes n: "normalized_nnf_match m"
and nodisc: "¬ has_disc disc2 m"
and disc2_noSrcPorts: "∀a. ¬ disc2 (Src_Ports a)"
and disc2_noDstPorts: "∀a. ¬ disc2 (Dst_Ports a)"
shows "m'∈ set (rewrite_MultiportPorts m)
⟹ ¬ has_disc disc2 m'"
apply(simp add: rewrite_MultiportPorts_def)
apply(rule normalize_replace_primitive_matchexpr_preserves_normalized_not_has_disc[OF n wf_disc_sel_common_primitive(11) nodisc])
by(simp_all add: rewrite_MultiportPorts_one_nodisc disc2_noSrcPorts disc2_noDstPorts)
lemma rewrite_MultiportPorts_preserves_normalized_not_has_disc_negated:
assumes n: "normalized_nnf_match m"
and nodisc: "¬ has_disc_negated disc2 neg m"
and disc2_noSrcPorts: "∀a. ¬ disc2 (Src_Ports a)"
and disc2_noDstPorts: "∀a. ¬ disc2 (Dst_Ports a)"
shows "m'∈ set (rewrite_MultiportPorts m)
⟹ ¬ has_disc_negated disc2 neg m'"
apply(simp add: rewrite_MultiportPorts_def)
apply(rule normalize_replace_primitive_matchexpr_preserves_normalized_not_has_disc_negated[OF n wf_disc_sel_common_primitive(11) nodisc])
by(simp_all add: rewrite_MultiportPorts_one_nodisc disc2_noSrcPorts disc2_noDstPorts)
lemma rewrite_MultiportPorts_removes_MultiportsPorts:
assumes n: "normalized_nnf_match m"
shows "m' ∈ set (rewrite_MultiportPorts m) ⟹ ¬ has_disc is_MultiportPorts m'"
apply(simp add: rewrite_MultiportPorts_def)
apply(rule normalize_match_preserves_nodisc)
apply(simp_all)
apply(rule replace_primitive_matchexpr_replaces_disc[OF n wf_disc_sel_common_primitive(11)])
apply(intro allI, rename_tac a)
by(case_tac a, simp_all add: MatchOr_def)
end