Theory Interfaces_Normalize
theory Interfaces_Normalize
imports Common_Primitive_Lemmas
begin
subsection‹Optimizing interfaces in match expressions›
definition compress_interfaces :: "iface negation_type list ⇒ (iface list × iface list) option" where
"compress_interfaces ifces ≡ case (compress_pos_interfaces (getPos ifces))
of None ⇒ None
| Some i ⇒ if
∃negated_ifce ∈ set (getNeg ifces). iface_subset i negated_ifce
then
None
else if
¬ iface_is_wildcard i
then
Some ([i], [])
else
Some ((if i = ifaceAny then [] else [i]), getNeg ifces)"
context
begin
private lemma compress_interfaces_None:
assumes generic: "primitive_matcher_generic β"
shows
"compress_interfaces ifces = None ⟹ ¬ matches (β, α) (alist_and (NegPos_map IIface ifces)) a p"
"compress_interfaces ifces = None ⟹ ¬ matches (β, α) (alist_and (NegPos_map OIface ifces)) a p"
apply(simp_all add: compress_interfaces_def)
apply(simp_all add: nt_match_list_matches[symmetric] nt_match_list_simp)
apply(simp_all add: NegPos_map_simps primitive_matcher_generic.Iface_single[OF generic]
primitive_matcher_generic.Iface_single_not[OF generic])
apply(case_tac [!] "compress_pos_interfaces (getPos ifces)")
apply(simp_all)
apply(drule_tac p_i="p_iiface p" in compress_pos_interfaces_None)
apply(simp; fail)
apply(drule_tac p_i="p_iiface p" in compress_pos_interfaces_Some)
apply(simp split:if_split_asm)
using iface_subset apply blast
apply(drule_tac p_i="p_oiface p" in compress_pos_interfaces_None)
apply(simp; fail)
apply(drule_tac p_i="p_oiface p" in compress_pos_interfaces_Some)
apply(simp split:if_split_asm)
using iface_subset by blast
private lemma compress_interfaces_Some:
assumes generic: "primitive_matcher_generic β"
shows
"compress_interfaces ifces = Some (i_pos, i_neg) ⟹
matches (β, α) (alist_and (NegPos_map IIface ((map Pos i_pos)@(map Neg i_neg)))) a p ⟷
matches (β, α) (alist_and (NegPos_map IIface ifces)) a p"
"compress_interfaces ifces = Some (i_pos, i_neg) ⟹
matches (β, α) (alist_and (NegPos_map OIface ((map Pos i_pos)@(map Neg i_neg)))) a p ⟷
matches (β, α) (alist_and (NegPos_map OIface ifces)) a p"
apply(simp_all add: compress_interfaces_def)
apply(simp_all add: bunch_of_lemmata_about_matches(1) alist_and_append NegPos_map_append)
apply(simp_all add: nt_match_list_matches[symmetric] nt_match_list_simp)
apply(simp_all add: NegPos_map_simps primitive_matcher_generic.Iface_single[OF generic]
primitive_matcher_generic.Iface_single_not[OF generic])
apply(case_tac [!] "compress_pos_interfaces (getPos ifces)")
apply(simp_all)
apply(drule_tac p_i="p_iiface p" in compress_pos_interfaces_Some)
apply(simp split:if_split_asm add: match_ifaceAny)
unfolding iface_is_wildcard_def using iface_subset match_iface_case_nowildcard
apply (metis (no_types, lifting) Collect_mono_iff iface.collapse list.distinct(1) list.set_cases list.set_intros(1) set_ConsD)
apply force
apply(drule_tac p_i="p_oiface p" in compress_pos_interfaces_Some)
apply(simp split:if_split_asm add: match_ifaceAny)
unfolding iface_is_wildcard_def iface_subset using match_iface_case_nowildcard
apply (metis iface.collapse list.distinct(1) list.inject list.set_cases list.set_intros(1) mem_Collect_eq subsetI)
by force
definition compress_normalize_input_interfaces :: "'i::len common_primitive match_expr ⇒ 'i common_primitive match_expr option" where
"compress_normalize_input_interfaces m ≡ compress_normalize_primitive (is_Iiface, iiface_sel) IIface compress_interfaces m"
lemma compress_normalize_input_interfaces_Some:
assumes generic: "primitive_matcher_generic β"
and "normalized_nnf_match m" and "compress_normalize_input_interfaces m = Some m'"
shows "matches (β, α) m' a p ⟷ matches (β, α) m a p"
apply(rule compress_normalize_primitive_Some[OF assms(2) wf_disc_sel_common_primitive(5)])
using assms(3) apply(simp add: compress_normalize_input_interfaces_def; fail)
using compress_interfaces_Some[OF generic] by simp
lemma compress_normalize_input_interfaces_None:
assumes generic: "primitive_matcher_generic β"
and "normalized_nnf_match m" and "compress_normalize_input_interfaces m = None"
shows "¬ matches (β, α) m a p"
apply(rule compress_normalize_primitive_None[OF assms(2) wf_disc_sel_common_primitive(5)])
using assms(3) apply(simp add: compress_normalize_input_interfaces_def; fail)
using compress_interfaces_None[OF generic] by simp
lemma compress_normalize_input_interfaces_nnf: "normalized_nnf_match m ⟹ compress_normalize_input_interfaces m = Some m' ⟹
normalized_nnf_match m'"
unfolding compress_normalize_input_interfaces_def
using compress_normalize_primitive_nnf[OF wf_disc_sel_common_primitive(5)] by blast
lemma compress_normalize_input_interfaces_not_introduces_Iiface:
"¬ has_disc is_Iiface m ⟹ normalized_nnf_match m ⟹ compress_normalize_input_interfaces m = Some m' ⟹
¬ has_disc is_Iiface m'"
apply(simp add: compress_normalize_input_interfaces_def)
apply(drule compress_normalize_primitive_not_introduces_C[where m=m and C'=IIface])
apply(simp_all add: wf_disc_sel_common_primitive(5))
by(simp add: compress_interfaces_def iface_is_wildcard_ifaceAny)
lemma compress_normalize_input_interfaces_not_introduces_Iiface_negated:
assumes notdisc: "¬ has_disc_negated is_Iiface False m"
and nm: "normalized_nnf_match m"
and some: "compress_normalize_input_interfaces m = Some m'"
shows "¬ has_disc_negated is_Iiface False m'"
apply(rule compress_normalize_primitive_not_introduces_C_negated[OF notdisc wf_disc_sel_common_primitive(5) nm])
using some apply(simp add: compress_normalize_input_interfaces_def)
by(simp add: compress_interfaces_def split: option.split_asm if_split_asm)
lemma compress_normalize_input_interfaces_hasdisc:
"¬ has_disc disc m ⟹ (∀a. ¬ disc (IIface a)) ⟹ normalized_nnf_match m ⟹ compress_normalize_input_interfaces m = Some m' ⟹
normalized_nnf_match m' ∧ ¬ has_disc disc m'"
unfolding compress_normalize_input_interfaces_def
using compress_normalize_primitive_hasdisc[OF _ wf_disc_sel_common_primitive(5)] by blast
lemma compress_normalize_input_interfaces_hasdisc_negated:
"¬ has_disc_negated disc neg m ⟹ (∀a. ¬ disc (IIface a)) ⟹ normalized_nnf_match m ⟹ compress_normalize_input_interfaces m = Some m' ⟹
normalized_nnf_match m' ∧ ¬ has_disc_negated disc neg m'"
unfolding compress_normalize_input_interfaces_def
using compress_normalize_primitive_hasdisc_negated[OF _ wf_disc_sel_common_primitive(5)] by blast
lemma compress_normalize_input_interfaces_preserves_normalized_n_primitive:
"normalized_n_primitive (disc, sel) P m ⟹ (∀a. ¬ disc (IIface a)) ⟹ normalized_nnf_match m ⟹ compress_normalize_input_interfaces m = Some m' ⟹
normalized_nnf_match m' ∧ normalized_n_primitive (disc, sel) P m'"
unfolding compress_normalize_input_interfaces_def
using compress_normalize_primitve_preserves_normalized_n_primitive[OF _ wf_disc_sel_common_primitive(5)] by blast
value[code] "compress_normalize_input_interfaces
(MatchAnd (MatchAnd (MatchAnd (Match ((IIface (Iface ''eth+'')::32 common_primitive))) (MatchNot (Match (IIface (Iface ''eth4''))))) (Match (IIface (Iface ''eth1''))))
(Match (Prot (Proto TCP))))"
value[code] "compress_normalize_input_interfaces (MatchAny:: 32 common_primitive match_expr)"
definition compress_normalize_output_interfaces :: "'i::len common_primitive match_expr ⇒ 'i common_primitive match_expr option" where
"compress_normalize_output_interfaces m ≡ compress_normalize_primitive (is_Oiface, oiface_sel) OIface compress_interfaces m"
lemma compress_normalize_output_interfaces_Some:
assumes generic: "primitive_matcher_generic β"
and "normalized_nnf_match m" and "compress_normalize_output_interfaces m = Some m'"
shows "matches (β, α) m' a p ⟷ matches (β, α) m a p"
apply(rule compress_normalize_primitive_Some[OF assms(2) wf_disc_sel_common_primitive(6)])
using assms(3) apply(simp add: compress_normalize_output_interfaces_def; fail)
using compress_interfaces_Some[OF generic] by simp
lemma compress_normalize_output_interfaces_None:
assumes generic: "primitive_matcher_generic β"
and "normalized_nnf_match m" and "compress_normalize_output_interfaces m = None"
shows "¬ matches (β, α) m a p"
apply(rule compress_normalize_primitive_None[OF assms(2) wf_disc_sel_common_primitive(6)])
using assms(3) apply(simp add: compress_normalize_output_interfaces_def; fail)
using compress_interfaces_None[OF generic] by simp
lemma compress_normalize_output_interfaces_nnf: "normalized_nnf_match m ⟹ compress_normalize_output_interfaces m = Some m' ⟹
normalized_nnf_match m'"
unfolding compress_normalize_output_interfaces_def
using compress_normalize_primitive_nnf[OF wf_disc_sel_common_primitive(6)] by blast
lemma compress_normalize_output_interfaces_not_introduces_Oiface:
"¬ has_disc is_Oiface m ⟹ normalized_nnf_match m ⟹ compress_normalize_output_interfaces m = Some m' ⟹
¬ has_disc is_Oiface m'"
apply(simp add: compress_normalize_output_interfaces_def)
apply(drule compress_normalize_primitive_not_introduces_C[where m=m and C'=OIface])
apply(simp_all add: wf_disc_sel_common_primitive(6))
by(simp add: compress_interfaces_def iface_is_wildcard_ifaceAny)
lemma compress_normalize_output_interfaces_not_introduces_Oiface_negated:
assumes notdisc: "¬ has_disc_negated is_Oiface False m"
and nm: "normalized_nnf_match m"
and some: "compress_normalize_output_interfaces m = Some m'"
shows "¬ has_disc_negated is_Oiface False m'"
apply(rule compress_normalize_primitive_not_introduces_C_negated[OF notdisc wf_disc_sel_common_primitive(6) nm])
using some apply(simp add: compress_normalize_output_interfaces_def)
by(simp add: compress_interfaces_def split: option.split_asm if_split_asm)
lemma compress_normalize_output_interfaces_hasdisc:
"¬ has_disc disc m ⟹ (∀a. ¬ disc (OIface a)) ⟹ normalized_nnf_match m ⟹ compress_normalize_output_interfaces m = Some m' ⟹
normalized_nnf_match m' ∧ ¬ has_disc disc m'"
unfolding compress_normalize_output_interfaces_def
using compress_normalize_primitive_hasdisc[OF _ wf_disc_sel_common_primitive(6)] by blast
lemma compress_normalize_output_interfaces_hasdisc_negated:
"¬ has_disc_negated disc neg m ⟹ (∀a. ¬ disc (OIface a)) ⟹ normalized_nnf_match m ⟹ compress_normalize_output_interfaces m = Some m' ⟹
normalized_nnf_match m' ∧ ¬ has_disc_negated disc neg m'"
unfolding compress_normalize_output_interfaces_def
using compress_normalize_primitive_hasdisc_negated[OF _ wf_disc_sel_common_primitive(6)] by blast
lemma compress_normalize_output_interfaces_preserves_normalized_n_primitive:
"normalized_n_primitive (disc, sel) P m ⟹ (∀a. ¬ disc (OIface a)) ⟹ normalized_nnf_match m ⟹ compress_normalize_output_interfaces m = Some m' ⟹
normalized_nnf_match m' ∧ normalized_n_primitive (disc, sel) P m'"
unfolding compress_normalize_output_interfaces_def
using compress_normalize_primitve_preserves_normalized_n_primitive[OF _ wf_disc_sel_common_primitive(6)] by blast
end
end