Theory Interfaces_Normalize

theory Interfaces_Normalize
imports Common_Primitive_Lemmas
begin



subsection‹Optimizing interfaces in match expressions›

  (*returns: (list of positive interfaces × a list of negated interfaces)
    it matches the conjunction of both
    None if the expression cannot match*)
  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)

  (* only for arbitrary discs that do not match Iiface*)
  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

   (* only for arbitrary discs that do not match Iiface*)
  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)

  (* only for arbitrary discs that do not match Oiface*)
  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

   (* only for arbitrary discs that do not match Oiface*)
  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