Theory Transform

section‹Optimizing and Normalizing Primitives›
theory Transform
imports Common_Primitive_Lemmas
        "../Semantics_Ternary/Semantics_Ternary"
        "../Semantics_Ternary/Negation_Type_Matching"
        Ports_Normalize
        IpAddresses_Normalize
        Interfaces_Normalize
        Protocols_Normalize
        "../Common/Remdups_Rev"
        Interface_Replace
        "../Semantics_Ternary/Optimizing"
begin

text‹This transform theory plugs a lot of stuff together. We perform several normalization and
  optimization steps on complete firewall rulesets. We show that it preserves the semantics and also,
  that structural properties are preserved. For example, if you normalize interfaces and afterwards
  normalize protocols, the interfaces remain normalized and no new interfaces are added when 
  doing the protocol normalization.›


(*Maintainer note: we plug a lot of lemmata together to show that structural properties are preserved.
  Yes, there is a huge set of apply style in there but there is no magic happening, it is just
  pushing through invariants about structural properties.*)

definition compress_normalize_besteffort
  :: "'i::len common_primitive match_expr ⇒ 'i common_primitive match_expr option" where
   "compress_normalize_besteffort m ≡ compress_normalize_primitive_monad
          [compress_normalize_protocols,
           compress_normalize_input_interfaces,
           compress_normalize_output_interfaces] m"  
  
context begin
  private lemma compress_normalize_besteffort_normalized:
  "f ∈ set [compress_normalize_protocols,
            compress_normalize_input_interfaces,
            compress_normalize_output_interfaces] ⟹
         normalized_nnf_match m ⟹ f m = Some m' ⟹ normalized_nnf_match m'"
    apply(simp)
    apply(elim disjE)
      using compress_normalize_protocols_nnf apply blast
     using compress_normalize_input_interfaces_nnf apply blast
    using compress_normalize_output_interfaces_nnf apply blast
    done
  private lemma compress_normalize_besteffort_matches:
    assumes generic: "primitive_matcher_generic β"
    shows "f ∈ set [compress_normalize_protocols,
                    compress_normalize_input_interfaces,
                    compress_normalize_output_interfaces] ⟹
           normalized_nnf_match m ⟹
           f m = Some m' ⟹
           matches (β, α) m' a p = matches (β, α) m a p"
    apply(simp)
    apply(elim disjE)
      using primitive_matcher_generic.compress_normalize_protocols_Some[OF generic] apply blast
     using compress_normalize_input_interfaces_Some[OF generic] apply blast
    using compress_normalize_output_interfaces_Some[OF generic] apply blast
    done
  
  
  lemma compress_normalize_besteffort_Some: 
    assumes generic: "primitive_matcher_generic β"
    shows "normalized_nnf_match m ⟹
           compress_normalize_besteffort m = Some m' ⟹
           matches (β, α) m' a p = matches (β, α) m a p"
    unfolding compress_normalize_besteffort_def
    apply(rule compress_normalize_primitive_monad)
    using compress_normalize_besteffort_normalized compress_normalize_besteffort_matches[OF generic] by blast+
  lemma compress_normalize_besteffort_None:
    assumes generic: "primitive_matcher_generic β"
    shows "normalized_nnf_match m ⟹
           compress_normalize_besteffort m = None ⟹
           ¬ matches (β, α) m a p"
  proof -
   have notmatches: "f ∈ set [compress_normalize_protocols, compress_normalize_input_interfaces, compress_normalize_output_interfaces] ⟹
           normalized_nnf_match m ⟹ f m = None ⟹ ¬ matches (β, α) m a p" for f m
      apply(simp)
      using primitive_matcher_generic.compress_normalize_protocols_None[OF generic]
            compress_normalize_input_interfaces_None[OF generic]
            compress_normalize_output_interfaces_None[OF generic] by blast
   show "normalized_nnf_match m ⟹ compress_normalize_besteffort m = None ⟹ ¬ matches (β, α) m a p"
     unfolding compress_normalize_besteffort_def
     apply(rule compress_normalize_primitive_monad_None)
         using compress_normalize_besteffort_normalized
               compress_normalize_besteffort_matches[OF generic]
               notmatches by blast+
  qed 
  lemma compress_normalize_besteffort_nnf:
    "normalized_nnf_match m ⟹
     compress_normalize_besteffort m = Some m' ⟹
     normalized_nnf_match m'"
    unfolding compress_normalize_besteffort_def
    apply(rule compress_normalize_primitive_monad)
       using compress_normalize_besteffort_normalized
             compress_normalize_besteffort_matches[OF primitive_matcher_generic_common_matcher]
             by blast+
  
  lemma compress_normalize_besteffort_not_introduces_Iiface:
      "¬ has_disc is_Iiface m ⟹ normalized_nnf_match m ⟹ compress_normalize_besteffort m = Some m' ⟹
       ¬ has_disc is_Iiface m'"
    unfolding compress_normalize_besteffort_def
    apply(rule compress_normalize_primitive_monad_preserves[THEN conjunct2])
        apply(drule(3) compress_normalize_besteffort_normalized)
       apply(auto dest: compress_normalize_input_interfaces_not_introduces_Iiface
                        compress_normalize_protocols_hasdisc
                        compress_normalize_output_interfaces_hasdisc)
    done
  lemma compress_normalize_besteffort_not_introduces_Oiface:
      "¬ has_disc is_Oiface m ⟹ normalized_nnf_match m ⟹ compress_normalize_besteffort m = Some m' ⟹
       ¬ has_disc is_Oiface m'"
    unfolding compress_normalize_besteffort_def
    apply(rule compress_normalize_primitive_monad_preserves[THEN conjunct2])
        apply(drule(3) compress_normalize_besteffort_normalized)
       apply(auto dest: compress_normalize_output_interfaces_hasdisc
                        compress_normalize_output_interfaces_not_introduces_Oiface
                        compress_normalize_protocols_hasdisc
                        compress_normalize_input_interfaces_hasdisc)
    done
  
  lemma compress_normalize_besteffort_not_introduces_Iiface_negated:
      "¬ has_disc_negated is_Iiface False m ⟹ normalized_nnf_match m ⟹ compress_normalize_besteffort m = Some m' ⟹
       ¬ has_disc_negated is_Iiface False m'"
    unfolding compress_normalize_besteffort_def
    apply(rule compress_normalize_primitive_monad_preserves[THEN conjunct2])
        apply(drule(3) compress_normalize_besteffort_normalized)
       apply(auto dest: compress_normalize_besteffort_normalized compress_normalize_input_interfaces_not_introduces_Iiface_negated
                        compress_normalize_protocols_hasdisc_negated
                        compress_normalize_output_interfaces_hasdisc_negated)
    done
  lemma compress_normalize_besteffort_not_introduces_Oiface_negated:
      "¬ has_disc_negated is_Oiface False m ⟹ normalized_nnf_match m ⟹ compress_normalize_besteffort m = Some m' ⟹
       ¬ has_disc_negated is_Oiface False m'"
    unfolding compress_normalize_besteffort_def
    apply(rule compress_normalize_primitive_monad_preserves[THEN conjunct2])
        apply(drule(3) compress_normalize_besteffort_normalized)
       apply(auto dest: compress_normalize_output_interfaces_not_introduces_Oiface_negated
                        compress_normalize_input_interfaces_hasdisc_negated
                        compress_normalize_protocols_hasdisc_negated)
    done
  lemma compress_normalize_besteffort_not_introduces_Prot_negated:
      "¬ has_disc_negated is_Prot False m ⟹ normalized_nnf_match m ⟹ compress_normalize_besteffort m = Some m' ⟹
       ¬ has_disc_negated is_Prot False m'"
    unfolding compress_normalize_besteffort_def
    apply(rule compress_normalize_primitive_monad_preserves[THEN conjunct2])
        apply(drule(3) compress_normalize_besteffort_normalized)
       apply(auto dest: compress_normalize_input_interfaces_hasdisc_negated
                        compress_normalize_protocols_not_introduces_Prot_negated
                        compress_normalize_output_interfaces_hasdisc_negated)
    done
  lemma compress_normalize_besteffort_hasdisc:
      "¬ has_disc disc m ⟹ (∀a. ¬ disc (IIface a)) ⟹ (∀a. ¬ disc (OIface a)) ⟹ (∀a. ¬ disc (Prot a)) ⟹
       normalized_nnf_match m ⟹ compress_normalize_besteffort m = Some m' ⟹
       normalized_nnf_match m' ∧ ¬ has_disc disc m'"
    unfolding compress_normalize_besteffort_def
    apply(rule compress_normalize_primitive_monad_preserves)
        apply(drule(3) compress_normalize_besteffort_normalized)
       apply(auto dest: compress_normalize_input_interfaces_hasdisc
                        compress_normalize_output_interfaces_hasdisc
                        compress_normalize_protocols_hasdisc)
    done
  lemma compress_normalize_besteffort_hasdisc_negated:
      "¬ has_disc_negated disc False m ⟹
       (∀a. ¬ disc (IIface a)) ⟹ (∀a. ¬ disc (OIface a)) ⟹ (∀a. ¬ disc (Prot a)) ⟹
       normalized_nnf_match m ⟹ compress_normalize_besteffort m = Some m' ⟹
       normalized_nnf_match m' ∧ ¬ has_disc_negated disc False m'"
       (*due to protocols, we can only show for neg := False*)
    unfolding compress_normalize_besteffort_def
    apply(rule compress_normalize_primitive_monad_preserves)
        apply(drule(3) compress_normalize_besteffort_normalized)
       apply(simp split: option.split_asm)
       using compress_normalize_input_interfaces_hasdisc_negated
             compress_normalize_output_interfaces_hasdisc_negated
             compress_normalize_protocols_hasdisc_negated apply blast
    apply simp_all
    done
  lemma compress_normalize_besteffort_preserves_normalized_n_primitive:
    "normalized_n_primitive (disc, sel) P m ⟹
     (∀a. ¬ disc (IIface a)) ⟹ (∀a. ¬ disc (OIface a)) ⟹ (∀a. ¬ disc (Prot a)) ⟹
     normalized_nnf_match m ⟹ compress_normalize_besteffort m = Some m' ⟹
     normalized_nnf_match m' ∧ normalized_n_primitive (disc, sel) P m'"
    unfolding compress_normalize_besteffort_def
    apply(rule compress_normalize_primitive_monad_preserves)
        apply(drule(3) compress_normalize_besteffort_normalized)
       apply(auto dest: compress_normalize_input_interfaces_preserves_normalized_n_primitive
             compress_normalize_output_interfaces_preserves_normalized_n_primitive
             compress_normalize_protocols_preserves_normalized_n_primitive)
    done
end

section‹Transforming rulesets›

subsection‹Optimizations›

lemma approximating_bigstep_fun_remdups_rev:
  "approximating_bigstep_fun γ p (remdups_rev rs) s = approximating_bigstep_fun γ p rs s"
  proof(induction γ p rs s rule: approximating_bigstep_fun.induct)
    case 1 thus ?case by(simp add: remdups_rev_def)
    next
    case 2 thus ?case by (simp add: Decision_approximating_bigstep_fun)
    next
    case (3 γ p m a rs) thus ?case
      proof(cases "matches γ m a p")
        case False with 3 show ?thesis
         by(simp add: remdups_rev_fst remdups_rev_removeAll not_matches_removeAll) 
        next
        case True
        { fix rs s
          have "approximating_bigstep_fun γ p (filter ((≠) (Rule m Log)) rs) s = approximating_bigstep_fun γ p rs s"
          proof(induction γ p rs s rule: approximating_bigstep_fun_induct)
          qed(auto simp add: Decision_approximating_bigstep_fun split: action.split)
        } note helper_Log=this
        { fix rs s
          have "approximating_bigstep_fun γ p (filter ((≠) (Rule m Empty)) rs) s = approximating_bigstep_fun γ p rs s"
          proof(induction γ p rs s rule: approximating_bigstep_fun_induct)
          qed(auto simp add: Decision_approximating_bigstep_fun split: action.split)
        } note helper_Empty=this
        from True 3 show ?thesis
          apply(simp add: remdups_rev_fst split: action.split)
          apply(safe)
             apply(simp_all)
           apply(simp_all add: remdups_rev_removeAll)
           apply(simp_all add: removeAll_filter_not_eq helper_Empty helper_Log)
          done
        qed
  qed

lemma remdups_rev_simplers: "simple_ruleset rs ⟹ simple_ruleset (remdups_rev rs)"
  by(induction rs) (simp_all add: remdups_rev_def simple_ruleset_def)

lemma remdups_rev_preserve_matches:
  "∀r∈set rs. P (get_match r) ⟹ ∀r∈set (remdups_rev rs). P (get_match r)"
  by(induction rs) (simp_all add: remdups_rev_def simple_ruleset_def)


subsection‹Optimize and Normalize to NNF form›

(*without normalize_rules_dnf, the result cannot be normalized as optimize_primitive_univ can contain MatchNot MatchAny*)
definition transform_optimize_dnf_strict :: "'i::len common_primitive rule list ⇒ 'i common_primitive rule list" where 
    "transform_optimize_dnf_strict = cut_off_after_match_any ∘
        (optimize_matches opt_MatchAny_match_expr ∘ 
        normalize_rules_dnf ∘ (optimize_matches (opt_MatchAny_match_expr ∘ optimize_primitive_univ)))"
  

theorem transform_optimize_dnf_strict_structure:
  assumes simplers: "simple_ruleset rs" and wfα: "wf_unknown_match_tac α"
  shows "simple_ruleset (transform_optimize_dnf_strict rs)"
  and "∀ r ∈ set rs. ¬ has_disc disc (get_match r) ⟹
          ∀ r ∈ set (transform_optimize_dnf_strict rs). ¬ has_disc disc (get_match r)"
  and "∀ r ∈ set (transform_optimize_dnf_strict rs). normalized_nnf_match (get_match r)"
  and "∀ r ∈ set rs. normalized_n_primitive disc_sel f (get_match r) ⟹
        ∀ r ∈ set (transform_optimize_dnf_strict rs). normalized_n_primitive disc_sel f (get_match r)"
  and "∀ r ∈ set rs. ¬ has_disc_negated disc neg (get_match r) ⟹
        ∀ r ∈ set (transform_optimize_dnf_strict rs). ¬ has_disc_negated disc neg (get_match r)"
  proof -
    show simplers_transform: "simple_ruleset (transform_optimize_dnf_strict rs)"
      unfolding transform_optimize_dnf_strict_def
      using simplers by (simp add: cut_off_after_match_any_simplers
          optimize_matches_simple_ruleset simple_ruleset_normalize_rules_dnf)

    define transform_optimize_dnf_strict_inner
      where "transform_optimize_dnf_strict_inner =
        optimize_matches (opt_MatchAny_match_expr :: 'a common_primitive match_expr ⇒ 'a common_primitive match_expr) ∘ 
          normalize_rules_dnf ∘ (optimize_matches (opt_MatchAny_match_expr ∘ optimize_primitive_univ))"
    have inner_outer: "transform_optimize_dnf_strict = (cut_off_after_match_any ∘ transform_optimize_dnf_strict_inner)"
      by(auto simp add: transform_optimize_dnf_strict_def transform_optimize_dnf_strict_inner_def)
    have tf1: "transform_optimize_dnf_strict_inner (r#rs) =
      (optimize_matches opt_MatchAny_match_expr (normalize_rules_dnf (optimize_matches (opt_MatchAny_match_expr ∘ optimize_primitive_univ) [r])))@
        transform_optimize_dnf_strict_inner rs" for r rs
      unfolding transform_optimize_dnf_strict_inner_def
      apply(simp)
      apply(subst optimize_matches_fst)
      apply(simp add: normalize_rules_dnf_append optimize_matches_append)
      done

    ― ‹if the individual optimization functions preserve a property, then the whole thing does›
    { fix P :: "'a::len common_primitive match_expr ⇒ bool"
      assume p1: "∀m. P m ⟶ P (optimize_primitive_univ m)"
      assume p2: "∀m. P m ⟶ P (opt_MatchAny_match_expr m)"
      assume p3: "∀m. P m ⟶ (∀m' ∈ set (normalize_match m). P m')"
      { fix rs
        have "∀ r ∈ set rs. P (get_match r) ⟹
          ∀ r ∈ set (optimize_matches (opt_MatchAny_match_expr ∘ optimize_primitive_univ) rs). P (get_match r)"
          apply(rule optimize_matches_preserves)
          using p1 p2 by simp
      } note opt1=this
      { fix rs
        have "∀ r ∈ set rs. P (get_match r) ⟹ ∀ r ∈ set (normalize_rules_dnf rs). P (get_match r)"
        apply(induction rs rule: normalize_rules_dnf.induct)
         apply(simp; fail)
        apply(simp)
        apply(safe)
         apply(simp_all)
        using p3 by(simp)
      } note opt2=this
      { fix rs
        have "∀ r ∈ set rs. P (get_match r) ⟹
          ∀ r ∈ set (optimize_matches opt_MatchAny_match_expr rs). P (get_match r)"
          apply(rule optimize_matches_preserves)
          using p2 by simp
      } note opt3=this
      have "∀ r ∈  set rs. P (get_match r) ⟹
        ∀ r ∈ set (transform_optimize_dnf_strict rs). P (get_match r)"
        unfolding transform_optimize_dnf_strict_def
        apply(drule opt1)
        apply(drule opt2)
        apply(drule opt3)
        using cut_off_after_match_any_preserve_matches by auto
    } note matchpred_rule=this

    { fix m
      have "¬ has_disc disc m ⟹ ¬ has_disc disc (optimize_primitive_univ m)"
      by(induction m rule: optimize_primitive_univ.induct) (simp_all)
    }  moreover { fix m
      have "¬ has_disc disc m ⟶ (∀m' ∈ set (normalize_match m). ¬ has_disc disc m')"
        using normalize_match_preserves_nodisc by fast
    } ultimately show "∀ r ∈ set rs. ¬ has_disc disc (get_match r) ⟹
      ∀ r ∈ set (transform_optimize_dnf_strict rs). ¬ has_disc disc (get_match r)"
      using not_has_disc_opt_MatchAny_match_expr matchpred_rule[of "λm. ¬ has_disc disc m"] by fast

    { fix m
      have "¬ has_disc_negated disc neg m ⟹ ¬ has_disc_negated disc neg (optimize_primitive_univ m)"
      apply(induction disc neg m rule: has_disc_negated.induct)
            apply(simp_all)
      apply(rename_tac a)
      apply(subgoal_tac "optimize_primitive_univ (Match a) = Match a ∨ optimize_primitive_univ (Match a) = MatchAny")
       apply safe
        apply simp_all
      using optimize_primitive_univ_unchanged_primitives by blast
    }  with not_has_disc_negated_opt_MatchAny_match_expr not_has_disc_normalize_match show
      "∀ r ∈ set rs. ¬ has_disc_negated disc neg (get_match r) ⟹
        ∀ r ∈ set (transform_optimize_dnf_strict rs). ¬ has_disc_negated disc neg (get_match r)"
      using matchpred_rule[of "λm. ¬ has_disc_negated disc neg m"] by fast
   
   { fix P and a::"'a common_primitive"
     have "(optimize_primitive_univ (Match a)) = (Match a) ∨ (optimize_primitive_univ (Match a)) = MatchAny"
       by(induction "(Match a)" rule: optimize_primitive_univ.induct) (auto)
     hence "((optimize_primitive_univ (Match a)) = Match a ⟹ P a) ⟹ (optimize_primitive_univ (Match a) = MatchAny ⟹ P a) ⟹ P a" by blast
   } note optimize_primitive_univ_match_cases=this

   { fix m
      have "normalized_n_primitive disc_sel f m ⟹ normalized_n_primitive disc_sel f (optimize_primitive_univ m)"
      apply(induction disc_sel f m rule: normalized_n_primitive.induct)
            apply(simp_all split: if_split_asm)
        apply(rule optimize_primitive_univ_match_cases, simp_all)+
      done
    }  moreover { fix m
      have "normalized_n_primitive disc_sel f m ⟶ (∀m' ∈ set (normalize_match m). normalized_n_primitive disc_sel f  m')"
      using normalize_match_preserves_normalized_n_primitive by blast
    } ultimately show "∀ r ∈ set rs. normalized_n_primitive disc_sel f (get_match r) ⟹ 
        ∀ r ∈ set (transform_optimize_dnf_strict rs). normalized_n_primitive disc_sel f (get_match r)"
      using matchpred_rule[of "λm. normalized_n_primitive disc_sel f m"] normalized_n_primitive_opt_MatchAny_match_expr by fast
    

    { fix rs::"'a::len common_primitive rule list"
      from normalize_rules_dnf_normalized_nnf_match[of "rs"]
      have "∀x ∈ set (normalize_rules_dnf rs). normalized_nnf_match (get_match x)" .
      hence "∀r ∈ set (optimize_matches opt_MatchAny_match_expr (normalize_rules_dnf rs)). normalized_nnf_match (get_match r)"
        apply -
        apply(rule optimize_matches_preserves)
        using normalized_nnf_match_opt_MatchAny_match_expr by blast
    } 
    from this have "∀ r ∈ set (transform_optimize_dnf_strict_inner rs). normalized_nnf_match (get_match r)"
      unfolding transform_optimize_dnf_strict_inner_def by simp
    thus "∀ r ∈ set (transform_optimize_dnf_strict rs). normalized_nnf_match (get_match r)"
      unfolding inner_outer
      apply simp
      apply(rule cut_off_after_match_any_preserve_matches)
      .
  qed

theorem transform_optimize_dnf_strict:
  assumes simplers: "simple_ruleset rs" and wfα: "wf_unknown_match_tac α"
  shows "(common_matcher, α),p⊢ ⟨transform_optimize_dnf_strict rs, s⟩ ⇒⇩α t ⟷ (common_matcher, α),p⊢ ⟨rs, s⟩ ⇒⇩α t"
  proof -
    let ?γ="(common_matcher, α)"
    let ?fw="λrs. approximating_bigstep_fun ?γ p rs s"

    have simplers_transform: "simple_ruleset (transform_optimize_dnf_strict rs)"
      unfolding transform_optimize_dnf_strict_def
      using simplers by (simp add: cut_off_after_match_any_simplers 
                                    optimize_matches_simple_ruleset simple_ruleset_normalize_rules_dnf)

    have simplers1: "simple_ruleset (optimize_matches (opt_MatchAny_match_expr ∘ optimize_primitive_univ) rs)"
      using simplers optimize_matches_simple_ruleset by (metis)

    have 1: "?γ,p⊢ ⟨rs, s⟩ ⇒⇩α t ⟷ ?fw rs = t"
      using approximating_semantics_iff_fun_good_ruleset[OF simple_imp_good_ruleset[OF simplers]] by fast

    have "?fw rs = ?fw (optimize_matches (opt_MatchAny_match_expr ∘ optimize_primitive_univ) rs)"
      apply(rule optimize_matches[symmetric])
      using optimize_primitive_univ_correct_matchexpr opt_MatchAny_match_expr_correct by (metis comp_apply)
    also have "… = ?fw (normalize_rules_dnf (optimize_matches (opt_MatchAny_match_expr ∘ optimize_primitive_univ) rs))"
      apply(rule normalize_rules_dnf_correct[symmetric])
      using simplers1 by (metis good_imp_wf_ruleset simple_imp_good_ruleset)
    also have "… = ?fw (optimize_matches opt_MatchAny_match_expr (normalize_rules_dnf (optimize_matches (opt_MatchAny_match_expr ∘ optimize_primitive_univ) rs)))"
      apply(rule optimize_matches[symmetric])
      using opt_MatchAny_match_expr_correct by (metis)
    finally have rs: "?fw rs = ?fw (transform_optimize_dnf_strict rs)"
      unfolding transform_optimize_dnf_strict_def by(simp add: cut_off_after_match_any)

    have 2: "?fw (transform_optimize_dnf_strict rs) = t ⟷ ?γ,p⊢ ⟨transform_optimize_dnf_strict rs, s⟩ ⇒⇩α t "
      using approximating_semantics_iff_fun_good_ruleset[OF simple_imp_good_ruleset[OF simplers_transform], symmetric] by fast
    from 1 2 rs show "?γ,p⊢ ⟨transform_optimize_dnf_strict rs, s⟩ ⇒⇩α t ⟷ ?γ,p⊢ ⟨rs, s⟩ ⇒⇩α t" by simp
qed


subsection‹Abstracting over unknowns›

definition transform_remove_unknowns_generic
  :: "('a, 'packet) match_tac ⇒ 'a rule list ⇒ 'a rule list"
where 
    "transform_remove_unknowns_generic γ = optimize_matches_a (remove_unknowns_generic γ) "

theorem transform_remove_unknowns_generic:
  assumes simplers: "simple_ruleset rs"
      and wfα: "wf_unknown_match_tac α" and packet_independent_α: "packet_independent_α α"
      and wfβ: "packet_independent_β_unknown β"
    shows "(β, α),p⊢ ⟨transform_remove_unknowns_generic (β, α) rs, s⟩ ⇒⇩α t ⟷ (β, α),p⊢ ⟨rs, s⟩ ⇒⇩α t"
      and "simple_ruleset (transform_remove_unknowns_generic (β, α) rs)"
      and "∀ r ∈ set rs. ¬ has_disc disc (get_match r) ⟹
            ∀ r ∈ set (transform_remove_unknowns_generic (β, α) rs). ¬ has_disc disc (get_match r)"
      and "∀ r ∈ set (transform_remove_unknowns_generic (β, α) rs). ¬ has_unknowns β (get_match r)"
      (*may return MatchNot MatchAny*)
      and "∀ r ∈ set rs. normalized_n_primitive disc_sel f (get_match r) ⟹
            ∀ r ∈ set (transform_remove_unknowns_generic (β, α) rs). normalized_n_primitive disc_sel f (get_match r)"
      and "∀ r ∈ set rs. ¬ has_disc_negated disc neg (get_match r) ⟹
            ∀ r ∈ set (transform_remove_unknowns_generic (β, α) rs). ¬ has_disc_negated disc neg (get_match r)"
  proof -
    let ?γ="(β, α)"
    let ?fw="λrs. approximating_bigstep_fun ?γ p rs s"

    show simplers1: "simple_ruleset (transform_remove_unknowns_generic ?γ rs)"
      unfolding transform_remove_unknowns_generic_def
      using simplers optimize_matches_a_simple_ruleset by blast

    show "?γ,p⊢ ⟨transform_remove_unknowns_generic ?γ rs, s⟩ ⇒⇩α t ⟷ ?γ,p⊢ ⟨rs, s⟩ ⇒⇩α t"
      unfolding approximating_semantics_iff_fun_good_ruleset[OF simple_imp_good_ruleset[OF simplers1]]
      unfolding approximating_semantics_iff_fun_good_ruleset[OF simple_imp_good_ruleset[OF simplers]]
      unfolding transform_remove_unknowns_generic_def
      using optimize_matches_a_simplers[OF simplers] remove_unknowns_generic by metis

      from remove_unknowns_generic_not_has_disc show
        "∀ r ∈ set rs. ¬ has_disc disc (get_match r) ⟹
            ∀ r ∈ set (transform_remove_unknowns_generic ?γ rs). ¬ has_disc disc (get_match r)"
      unfolding transform_remove_unknowns_generic_def
      by(intro optimize_matches_a_preserves) blast

      from remove_unknowns_generic_normalized_n_primitive show
        "∀ r ∈ set rs. normalized_n_primitive disc_sel f (get_match r) ⟹
           ∀ r ∈ set (transform_remove_unknowns_generic ?γ rs). normalized_n_primitive disc_sel f (get_match r)"
      unfolding transform_remove_unknowns_generic_def
      by(intro optimize_matches_a_preserves) blast

    show "∀ r ∈ set (transform_remove_unknowns_generic ?γ rs). ¬ has_unknowns β (get_match r)"
      unfolding transform_remove_unknowns_generic_def
      apply(rule optimize_matches_a_preserves)
      apply(rule remove_unknowns_generic_specification[OF _ packet_independent_α wfβ])
      using simplers by(simp add: simple_ruleset_def)

    from remove_unknowns_generic_not_has_disc_negated show
      "∀ r ∈ set rs. ¬ has_disc_negated disc neg (get_match r) ⟹
         ∀ r ∈ set (transform_remove_unknowns_generic ?γ rs). ¬ has_disc_negated disc neg (get_match r)"
      unfolding transform_remove_unknowns_generic_def
      by(rule optimize_matches_a_preserves) blast
qed
thm transform_remove_unknowns_generic[OF _ _ _ packet_independent_β_unknown_common_matcher]


corollary transform_remove_unknowns_upper: defines "upper ≡ optimize_matches_a upper_closure_matchexpr"
   assumes simplers: "simple_ruleset rs"
    shows "(common_matcher, in_doubt_allow),p⊢ ⟨upper rs, s⟩ ⇒⇩α t ⟷ (common_matcher, in_doubt_allow),p⊢ ⟨rs, s⟩ ⇒⇩α t"
      and "simple_ruleset (upper rs)"
      and "∀ r ∈ set rs. ¬ has_disc disc (get_match r) ⟹
            ∀ r ∈ set (upper rs). ¬ has_disc disc (get_match r)"
      and "∀ r ∈ set (upper rs). ¬ has_disc is_Extra (get_match r)"
      and "∀ r ∈ set rs. normalized_n_primitive disc_sel f (get_match r) ⟹
            ∀ r ∈ set (upper rs). normalized_n_primitive disc_sel f (get_match r)"
      and "∀ r ∈ set rs. ¬ has_disc_negated disc neg (get_match r) ⟹
            ∀ r ∈ set (upper rs). ¬ has_disc_negated disc neg (get_match r)"
proof -
  from simplers have upper: "upper rs = transform_remove_unknowns_generic (common_matcher, in_doubt_allow) rs"
    apply(simp add: transform_remove_unknowns_generic_def upper_def)
    apply(erule optimize_matches_a_simple_ruleset_eq)
    by (simp add: upper_closure_matchexpr_generic)

  note * = transform_remove_unknowns_generic[OF 
      simplers wf_in_doubt_allow packet_independent_unknown_match_tacs(1) packet_independent_β_unknown_common_matcher,
      simplified upper_closure_matchexpr_generic]

    from *(1)[where p = p]
    show "(common_matcher, in_doubt_allow),p⊢ ⟨upper rs, s⟩ ⇒⇩α t ⟷ (common_matcher, in_doubt_allow),p⊢ ⟨rs, s⟩ ⇒⇩α t"
      by(subst upper)
    from *(2) show "simple_ruleset (upper rs)" by(subst upper)
    from *(3) show "∀ r ∈ set rs. ¬ has_disc disc (get_match r) ⟹
            ∀ r ∈ set (upper rs). ¬ has_disc disc (get_match r)"
      by(subst upper) fast
    from *(4) show "∀ r ∈ set (upper rs). ¬ has_disc is_Extra (get_match r)" 
      apply(subst upper)
      using has_unknowns_common_matcher by auto
    from *(5) show "∀ r ∈ set rs. normalized_n_primitive disc_sel f (get_match r) ⟹
            ∀ r ∈ set (upper rs). normalized_n_primitive disc_sel f (get_match r)"
      apply(subst upper)
      using packet_independent_unknown_match_tacs(1) simplers
        transform_remove_unknowns_generic(5)[OF _ _ _ packet_independent_β_unknown_common_matcher] wf_in_doubt_allow
      by blast
    from *(6) show "∀ r ∈ set rs. ¬ has_disc_negated disc neg (get_match r) ⟹
            ∀ r ∈ set (upper rs). ¬ has_disc_negated disc neg (get_match r)"
      by(subst upper) fast
qed


(*copy&paste from transform_remove_unknowns_upper*)
corollary transform_remove_unknowns_lower: defines "lower ≡ optimize_matches_a lower_closure_matchexpr"
   assumes simplers: "simple_ruleset rs"
    shows "(common_matcher, in_doubt_deny),p⊢ ⟨lower rs, s⟩ ⇒⇩α t ⟷ (common_matcher, in_doubt_deny),p⊢ ⟨rs, s⟩ ⇒⇩α t"
      and "simple_ruleset (lower rs)"
      and "∀ r ∈ set rs. ¬ has_disc disc (get_match r) ⟹
            ∀ r ∈ set (lower rs). ¬ has_disc disc (get_match r)"
      and "∀ r ∈ set (lower rs). ¬ has_disc is_Extra (get_match r)"
      and "∀ r ∈ set rs. normalized_n_primitive disc_sel f (get_match r) ⟹
            ∀ r ∈ set (lower rs). normalized_n_primitive disc_sel f (get_match r)"
      and "∀ r ∈ set rs. ¬ has_disc_negated disc neg (get_match r) ⟹
            ∀ r ∈ set (lower rs). ¬ has_disc_negated disc neg (get_match r)"
proof -
  from simplers have lower: "lower rs = transform_remove_unknowns_generic (common_matcher, in_doubt_deny) rs"
    apply(simp add: transform_remove_unknowns_generic_def lower_def)
    apply(erule optimize_matches_a_simple_ruleset_eq)
    by (simp add: lower_closure_matchexpr_generic)

  note * = transform_remove_unknowns_generic[OF 
      simplers wf_in_doubt_deny packet_independent_unknown_match_tacs(2) packet_independent_β_unknown_common_matcher,
      simplified lower_closure_matchexpr_generic]

    from *(1)[where p = p]
    show "(common_matcher, in_doubt_deny),p⊢ ⟨lower rs, s⟩ ⇒⇩α t ⟷ (common_matcher, in_doubt_deny),p⊢ ⟨rs, s⟩ ⇒⇩α t" 
      by(subst lower)
    from *(2) show "simple_ruleset (lower rs)" by(subst lower)
    from *(3) show "∀ r ∈ set rs. ¬ has_disc disc (get_match r) ⟹
            ∀ r ∈ set (lower rs). ¬ has_disc disc (get_match r)"
      by(subst lower) fast
    from *(4) show "∀ r ∈ set (lower rs). ¬ has_disc is_Extra (get_match r)" 
      apply(subst lower)
      using has_unknowns_common_matcher by auto
    from *(5) show "∀ r ∈ set rs. normalized_n_primitive disc_sel f (get_match r) ⟹
            ∀ r ∈ set (lower rs). normalized_n_primitive disc_sel f (get_match r)"
      apply(subst lower)
      using packet_independent_unknown_match_tacs(1) simplers
        transform_remove_unknowns_generic(5)[OF _ _ _ packet_independent_β_unknown_common_matcher] wf_in_doubt_deny
      by blast
    from *(6) show "∀ r ∈ set rs. ¬ has_disc_negated disc neg (get_match r) ⟹
            ∀ r ∈ set (lower rs). ¬ has_disc_negated disc neg (get_match r)"
      by(subst lower) fast
qed



subsection‹Normalizing and Transforming Primitives›

text‹Rewrite the primitives IPs and Ports such that can be used by the simple firewall.›
definition transform_normalize_primitives :: "'i::len common_primitive rule list ⇒ 'i common_primitive rule list" where 
    "transform_normalize_primitives =
      optimize_matches_option compress_normalize_besteffort ∘ ― ‹normalizes protocols, needs to go last›
      normalize_rules normalize_dst_ips ∘
      normalize_rules normalize_src_ips ∘
      normalize_rules normalize_dst_ports ∘ ― ‹may introduce new matches on protocols›
      normalize_rules normalize_src_ports ∘ ― ‹may introduce new matches in protocols›
      normalize_rules rewrite_MultiportPorts ― ‹introduces ‹Src_Ports› and ‹Dst_Ports› matches›"


 thm normalize_primitive_extract_preserves_unrelated_normalized_n_primitive
 lemma normalize_rules_preserves_unrelated_normalized_n_primitive:
   assumes "∀ r ∈ set rs. normalized_nnf_match (get_match r) ∧ normalized_n_primitive (disc2, sel2) P (get_match r)" 
       and "wf_disc_sel (disc1, sel1) C"
       and "∀a. ¬ disc2 (C a)"
    shows "∀r ∈ set (normalize_rules (normalize_primitive_extract (disc1, sel1) C f) rs).
              normalized_nnf_match (get_match r) ∧ normalized_n_primitive (disc2, sel2) P (get_match r)"
    thm normalize_rules_preserves[where P="λm. normalized_nnf_match m ∧ normalized_n_primitive  (disc2, sel2) P m"
        and f="normalize_primitive_extract (disc1, sel1) C f"]
    apply(rule normalize_rules_preserves[where P="λm. normalized_nnf_match m ∧ normalized_n_primitive  (disc2, sel2) P m"
        and f="normalize_primitive_extract (disc1, sel1) C f"])
     using assms(1) apply(simp)
    apply(safe)
     using normalize_primitive_extract_preserves_nnf_normalized[OF _ assms(2)] apply fast
    using normalize_primitive_extract_preserves_unrelated_normalized_n_primitive[OF _ _ assms(2) assms(3)] by blast


  lemma normalize_rules_normalized_n_primitive:
   assumes "∀ r ∈ set rs. normalized_nnf_match (get_match r)"
       and "∀m. normalized_nnf_match m ⟶
             (∀m' ∈ set (normalize_primitive_extract (disc, sel) C f m). normalized_n_primitive (disc, sel) P m')"
    shows "∀r ∈ set (normalize_rules (normalize_primitive_extract (disc, sel) C f) rs).
           normalized_n_primitive (disc, sel) P (get_match r)"
    apply(rule normalize_rules_property[where P=normalized_nnf_match and f="normalize_primitive_extract (disc, sel) C f"])
     using assms(1) apply simp
    using assms(2) by simp

  lemma optimize_matches_option_compress_normalize_besteffort_preserves_unrelated_normalized_n_primitive:
   assumes "∀ r ∈ set rs. normalized_nnf_match (get_match r) ∧ normalized_n_primitive (disc2, sel2) P (get_match r)" 
       and "∀a. ¬ disc2 (IIface a)" and "∀a. ¬ disc2 (OIface a)" and "∀a. ¬ disc2 (Prot a)"
    shows "∀r ∈ set (optimize_matches_option compress_normalize_besteffort rs).
            normalized_nnf_match (get_match r) ∧ normalized_n_primitive (disc2, sel2) P (get_match r)"
    thm optimize_matches_option_preserves
    apply(rule optimize_matches_option_preserves[where P="λm. normalized_nnf_match m ∧ normalized_n_primitive  (disc2, sel2) P m"
        and f="compress_normalize_besteffort"])
    apply(rule compress_normalize_besteffort_preserves_normalized_n_primitive)
         apply(simp_all add: assms)
    done

(*We write (∀a. ¬ disc (Src_Ports a)) to say that, basically, disc is not the function is_Src_Ports.
  But hey, equality on functions, ....*)
theorem transform_normalize_primitives:
  ― ‹all discriminators which will not be normalized remain unchanged›
  defines "unchanged disc ≡ (∀a. ¬ disc (Src_Ports a)) ∧ (∀a. ¬ disc (Dst_Ports a)) ∧
                             (∀a. ¬ disc (Src a)) ∧ (∀a. ¬ disc (Dst a))"
      ― ‹also holds for these discriminators, but not for @{const Prot}, which might be changed›
      and "changeddisc disc ≡ ((∀a. ¬ disc (IIface a)) ∨ disc = is_Iiface) ∧
                               ((∀a. ¬ disc (OIface a)) ∨ disc = is_Oiface)"
                               (*port normalization may introduce new matches on protocols*)
  assumes simplers: "simple_ruleset (rs :: 'i::len common_primitive rule list)"
      and wfα: "wf_unknown_match_tac α"
      and normalized: "∀ r ∈ set rs. normalized_nnf_match (get_match r)"
  shows "(common_matcher, α),p⊢ ⟨transform_normalize_primitives rs, s⟩ ⇒⇩α t ⟷ (common_matcher, α),p⊢ ⟨rs, s⟩ ⇒⇩α t"
    and "simple_ruleset (transform_normalize_primitives rs)"
    and "unchanged disc1 ⟹ changeddisc disc1 ⟹ ∀a. ¬ disc1 (Prot a) ⟹
           ∀ r ∈ set rs. ¬ has_disc disc1 (get_match r) ⟹
              ∀ r ∈ set (transform_normalize_primitives rs). ¬ has_disc disc1 (get_match r)"
    and "∀ r ∈ set (transform_normalize_primitives rs). normalized_nnf_match (get_match r)"
    and "∀ r ∈ set (transform_normalize_primitives rs).
          normalized_src_ports (get_match r) ∧ normalized_dst_ports (get_match r) ∧
          normalized_src_ips (get_match r) ∧ normalized_dst_ips (get_match r) ∧
          ¬ has_disc is_MultiportPorts (get_match r)"
    and "unchanged disc2 ⟹ (∀a. ¬ disc2 (IIface a)) ⟹ (∀a. ¬ disc2 (OIface a)) ⟹ (∀a. ¬ disc2 (Prot a)) ⟹
         ∀ r ∈ set rs. normalized_n_primitive (disc2, sel2) f (get_match r) ⟹
            ∀ r ∈ set (transform_normalize_primitives rs). normalized_n_primitive (disc2, sel2) f (get_match r)"
    ― ‹For disc3, we do not allow ports and ips, because these are changed.
       Here is the complicated part:
       (It is only complicated if, basically disc3 is @{const is_Prot})
       In addition, either it must not be protocol or (complicated case) 
       there must be no negated port matches 
       in the ruleset. Note that negated @{const Src_Ports} or @{const Dst_Ports} can also be
       introduced by rewriting @{const MultiportPorts}›
    and "unchanged disc3 ⟹ changeddisc disc3 ⟹
        (∀a. ¬ disc3 (Prot a)) ∨
        (disc3 = is_Prot ∧ (∀ r ∈ set rs.
          ¬ has_disc_negated is_Src_Ports False (get_match r) ∧
          ¬ has_disc_negated is_Dst_Ports False (get_match r) ∧
          ¬ has_disc is_MultiportPorts (get_match r))) ⟹
         ∀ r ∈ set rs. ¬ has_disc_negated disc3 False (get_match r) ⟹
            ∀ r ∈ set (transform_normalize_primitives rs). ¬ has_disc_negated disc3 False (get_match r)"
  proof -
    let ?γ="(common_matcher, α)"
    let ?fw="λrs. approximating_bigstep_fun ?γ p rs s"

    show simplers_t: "simple_ruleset (transform_normalize_primitives rs)"
      unfolding transform_normalize_primitives_def
      by(simp add: simple_ruleset_normalize_rules simplers optimize_matches_option_simple_ruleset)

    let ?rs0="normalize_rules rewrite_MultiportPorts rs"
    let ?rs1="normalize_rules normalize_src_ports ?rs0"
    let ?rs2="normalize_rules normalize_dst_ports ?rs1"
    let ?rs3="normalize_rules normalize_src_ips ?rs2"
    let ?rs4="normalize_rules normalize_dst_ips ?rs3"
    let ?rs5="optimize_matches_option compress_normalize_besteffort ?rs4"

    have normalized_rs0: "∀r ∈ set ?rs0. normalized_nnf_match (get_match r)"
      apply(intro normalize_rules_preserves[OF normalized])
      apply(simp add: rewrite_MultiportPorts_def)
      using normalized_nnf_match_normalize_match by blast
    from normalize_src_ports_nnf have normalized_rs1: "∀r ∈ set ?rs1. normalized_nnf_match (get_match r)"
      apply(intro normalize_rules_preserves[OF normalized_rs0])
      using normalize_dst_ports_nnf by blast
    from normalize_dst_ports_nnf have normalized_rs2: "∀r ∈ set ?rs2. normalized_nnf_match (get_match r)"
      apply(intro normalize_rules_preserves[OF normalized_rs1])
      by blast
    from normalize_rules_primitive_extract_preserves_nnf_normalized[OF this wf_disc_sel_common_primitive(3)]
         normalize_src_ips_def
    have normalized_rs3: "∀r ∈ set ?rs3. normalized_nnf_match (get_match r)" by metis
    from normalize_rules_primitive_extract_preserves_nnf_normalized[OF this wf_disc_sel_common_primitive(4)]
         normalize_dst_ips_def
    have normalized_rs4: "∀r ∈ set ?rs4. normalized_nnf_match (get_match r)" by metis
    have normalized_rs5: "∀r ∈ set ?rs5. normalized_nnf_match (get_match r)"
      apply(intro optimize_matches_option_preserves)
      apply(erule compress_normalize_besteffort_nnf[rotated])
      by(simp add: normalized_rs4)
    thus "∀ r ∈ set (transform_normalize_primitives rs). normalized_nnf_match (get_match r)"
      unfolding transform_normalize_primitives_def by simp

    (*add this as generic simp rule somewhere? But simplifier loops? what to do? cong_rule?*)
    have local_simp: "⋀rs1 rs2. approximating_bigstep_fun ?γ p rs1 s = approximating_bigstep_fun ?γ p rs2 s ⟹
      (approximating_bigstep_fun ?γ p rs1 s = t) = (approximating_bigstep_fun ?γ p rs2 s = t)" by simp

    have opt_compress_rule:
      "approximating_bigstep_fun (common_matcher, α) p (optimize_matches_option compress_normalize_besteffort rs1) s =
           approximating_bigstep_fun (common_matcher, α) p rs2 s"
    if rs1_n: "∀r ∈ set rs1. normalized_nnf_match (get_match r)" 
    and rs1rs2: "approximating_bigstep_fun (common_matcher, α) p rs1 s =
           approximating_bigstep_fun (common_matcher, α) p rs2 s" for rs1 rs2
     apply(subst optimize_matches_option_generic[where P="λ m a. normalized_nnf_match m"])
       apply(simp_all add: normalized
                  compress_normalize_besteffort_Some[OF primitive_matcher_generic_common_matcher]
                  compress_normalize_besteffort_None[OF primitive_matcher_generic_common_matcher]
                  rs1_n)
     using rs1rs2 by simp

    show "?γ,p⊢ ⟨transform_normalize_primitives rs, s⟩ ⇒⇩α t ⟷ ?γ,p⊢ ⟨rs, s⟩ ⇒⇩α t"
     unfolding approximating_semantics_iff_fun_good_ruleset[OF simple_imp_good_ruleset[OF simplers_t]]
     unfolding approximating_semantics_iff_fun_good_ruleset[OF simple_imp_good_ruleset[OF simplers]]
     unfolding transform_normalize_primitives_def
     apply(simp)
     apply(subst local_simp, simp_all)
     apply(rule opt_compress_rule[OF normalized_rs4])
     apply(subst normalize_rules_match_list_semantics_3[of normalized_nnf_match])
        using normalize_dst_ips[where p = p] apply(simp; fail)
       using simplers simple_ruleset_normalize_rules apply blast
      using normalized_rs3 apply(simp; fail)
     apply(subst normalize_rules_match_list_semantics_3[of normalized_nnf_match])
        using normalize_src_ips[where p = p] apply(simp; fail)
       using simplers simple_ruleset_normalize_rules apply blast
      using normalized_rs2 apply(simp; fail)
     apply(subst normalize_rules_match_list_semantics_3[of normalized_nnf_match])
        using normalize_dst_ports[OF primitive_matcher_generic_common_matcher,where p = p] apply(simp; fail)
       using simplers simple_ruleset_normalize_rules apply blast
      using normalized_rs1 apply(simp; fail)
     apply(subst normalize_rules_match_list_semantics_3[of normalized_nnf_match])
        using normalize_src_ports[OF primitive_matcher_generic_common_matcher, where p = p] apply(simp; fail)
       using simplers simple_ruleset_normalize_rules apply blast
      using normalized_rs0 apply(simp; fail)
     apply(subst normalize_rules_match_list_semantics_3[of normalized_nnf_match])
        using rewrite_MultiportPorts[OF primitive_matcher_generic_common_matcher, where p = p] apply(simp; fail)
       using simplers apply blast
      using normalized apply(simp; fail)
     ..

    (*naming: does not "normalize" but eliminate all multiportPorts!*)
    from rewrite_MultiportPorts_removes_MultiportsPorts
      normalize_rules_property[OF normalized, where f=rewrite_MultiportPorts and Q="λm. ¬ has_disc is_MultiportPorts m"]
    have rewrite_MultiportPorts_normalizes_Multiports:
      "∀r ∈ set ?rs0. ¬ has_disc is_MultiportPorts (get_match r)"
      by blast
    from normalize_src_ports_normalized_n_primitive
    have normalized_src_ports: "∀r ∈ set ?rs1. normalized_src_ports (get_match r)"
    apply(intro normalize_rules_property[OF normalized_rs0, where f=normalize_src_ports and Q=normalized_src_ports])
      by blast
    from normalize_dst_ports_normalized_n_primitive
         normalize_rules_property[OF normalized_rs1, where f=normalize_dst_ports and Q=normalized_dst_ports]
    have normalized_dst_ports: "∀r ∈ set ?rs2.  normalized_dst_ports (get_match r)" by fast
    from normalize_src_ips_normalized_n_primitive
         normalize_rules_property[OF normalized_rs2, where f=normalize_src_ips and Q=normalized_src_ips]
    have normalized_src_ips: "∀r ∈ set ?rs3.  normalized_src_ips (get_match r)" by fast
    from normalize_dst_ips_normalized_n_primitive
         normalize_rules_property[OF normalized_rs3, where f=normalize_dst_ips and Q=normalized_dst_ips]
         normalized_rs4
    have normalized_dst_ips_rs4: "∀r ∈ set ?rs4. normalized_nnf_match (get_match r) ∧ normalized_dst_ips (get_match r)" by fast
    with optimize_matches_option_compress_normalize_besteffort_preserves_unrelated_normalized_n_primitive[
          of _ is_Dst dst_sel normalized_cidr_ip
          , folded normalized_dst_ips_def2]
    have normalized_dst_rs5: "∀r ∈ set ?rs5. normalized_dst_ips (get_match r)" by fastforce

    have normalize_dst_ports_preserves_normalized_src_ports:
      "m' ∈ set (normalize_dst_ports m) ⟹ normalized_nnf_match m ⟹
        normalized_src_ports m ⟹ normalized_src_ports m'" for m m' :: " 'i common_primitive match_expr"
      unfolding normalized_src_ports_def2
      apply(rule normalize_ports_generic_preserves_normalized_n_primitive[OF _ wf_disc_sel_common_primitive(2)])
           apply(simp_all)
      by (simp add: normalize_dst_ports_def normalize_ports_generic_def normalize_positive_dst_ports_def rewrite_negated_dst_ports_def)


    from normalize_rules_preserves_unrelated_normalized_n_primitive[of
         _ is_MultiportPorts multiportports_sel "λ_. False"]
    have preserve_normalized_multiport_ports: " 
      ∀r∈ set rs. normalized_nnf_match (get_match r) ⟹
      ∀r∈ set rs. ¬ has_disc is_MultiportPorts (get_match r) ⟹
      wf_disc_sel (disc, sel) C ⟹
      ∀a. ¬ is_MultiportPorts (C a) ⟹
      ∀r∈ set (normalize_rules (normalize_primitive_extract (disc, sel) C f) rs).
        ¬ has_disc is_MultiportPorts (get_match r)"
      for f :: "'c negation_type list ⇒ 'c list" and rs disc sel
      and C :: "'c ⇒ 'i::len common_primitive"
      using normalized_n_primitive_false_eq_notdisc
      by blast
    (*TODO: push through*)
    have normalized_multiportports_rs1: "∀r ∈ set ?rs1. ¬ has_disc is_MultiportPorts (get_match r)"
      apply(rule normalize_rules_property[where P="λm. normalized_nnf_match m ∧ ¬ has_disc is_MultiportPorts m"])
       using normalized_rs0 rewrite_MultiportPorts_normalizes_Multiports apply blast
      apply(intro allI impI ballI)
      apply(rule normalize_src_ports_preserves_normalized_not_has_disc)
         by(simp_all)
    have normalized_multiportports_rs2: "∀r ∈ set ?rs2. ¬ has_disc is_MultiportPorts (get_match r)"
      apply(rule normalize_rules_property[where P="λm. normalized_nnf_match m ∧ ¬ has_disc is_MultiportPorts m"])
       using normalized_rs1 normalized_multiportports_rs1 apply blast
      apply(intro allI impI ballI)
      apply(rule normalize_dst_ports_preserves_normalized_not_has_disc)
         by(simp_all)
    from preserve_normalized_multiport_ports[OF normalized_rs2 normalized_multiportports_rs2 wf_disc_sel_common_primitive(3),
         where f2=ipt_iprange_compress, folded normalize_src_ips_def]
    have normalized_multiportports_rs3: "∀r ∈ set ?rs3. ¬ has_disc is_MultiportPorts (get_match r)" by simp
    from preserve_normalized_multiport_ports[OF normalized_rs3 normalized_multiportports_rs3 wf_disc_sel_common_primitive(4),
         where f2=ipt_iprange_compress, folded normalize_dst_ips_def]
         normalized_rs4
    have normalized_multiportports_rs4: "∀r ∈ set ?rs4. normalized_nnf_match (get_match r) ∧ ¬ has_disc is_MultiportPorts (get_match r)" by simp
    with optimize_matches_option_compress_normalize_besteffort_preserves_unrelated_normalized_n_primitive[
          of _ is_MultiportPorts multiportports_sel "λ_. False"
          , simplified]
    have normalized_multiportports_rs5: "∀r ∈ set ?rs5. ¬ has_disc is_MultiportPorts (get_match r)"
      using normalized_n_primitive_false_eq_notdisc by fastforce

    from normalize_rules_preserves_unrelated_normalized_n_primitive[of _ is_Src_Ports src_ports_sel "(λps. case ps of L4Ports _ pts ⇒ length pts ≤ 1)",
         folded normalized_src_ports_def2]
    have preserve_normalized_src_ports: " 
      ∀r∈ set rs. normalized_nnf_match (get_match r) ⟹
      ∀r∈ set rs. normalized_src_ports (get_match r) ⟹
      wf_disc_sel (disc, sel) C ⟹
      ∀a. ¬ is_Src_Ports (C a) ⟹
      ∀r∈ set (normalize_rules (normalize_primitive_extract (disc, sel) C f) rs). normalized_src_ports (get_match r)"
      for f :: "'c negation_type list ⇒ 'c list" and rs disc sel and C :: "'c ⇒ 'i::len common_primitive"
      by blast
    have normalized_src_ports_rs2: "∀r ∈ set ?rs2.  normalized_src_ports (get_match r)"
      apply(rule normalize_rules_property[where P="λm. normalized_nnf_match m ∧ normalized_src_ports m"])
       using normalized_rs1 normalized_src_ports apply blast
      apply(clarify)
      using normalize_dst_ports_preserves_normalized_src_ports by blast
    from preserve_normalized_src_ports[OF normalized_rs2 normalized_src_ports_rs2 wf_disc_sel_common_primitive(3),
         where f3=ipt_iprange_compress, folded normalize_src_ips_def]
    have normalized_src_ports_rs3: "∀r ∈ set ?rs3.  normalized_src_ports (get_match r)" by simp
    from preserve_normalized_src_ports[OF normalized_rs3 normalized_src_ports_rs3 wf_disc_sel_common_primitive(4),
         where f3=ipt_iprange_compress, folded normalize_dst_ips_def]
         normalized_rs4
    have normalized_src_ports_rs4: "∀r ∈ set ?rs4. normalized_nnf_match (get_match r) ∧ normalized_src_ports (get_match r)" by simp
    with optimize_matches_option_compress_normalize_besteffort_preserves_unrelated_normalized_n_primitive[
          of _ is_Src_Ports src_ports_sel "(λps. case ps of L4Ports _ pts ⇒ length pts ≤ 1)"
          , folded normalized_src_ports_def2]
    have normalized_src_ports_rs5: "∀r ∈ set ?rs5. normalized_src_ports (get_match r)" by fastforce

    from normalize_rules_preserves_unrelated_normalized_n_primitive[of _ is_Dst_Ports dst_ports_sel "(λps. case ps of L4Ports _ pts ⇒ length pts ≤ 1)",
         folded normalized_dst_ports_def2]
    have preserve_normalized_dst_ports: "⋀rs disc sel C f. 
      ∀r∈set rs. normalized_nnf_match (get_match r) ⟹
      ∀r∈set rs. normalized_dst_ports (get_match r) ⟹
      wf_disc_sel (disc, sel) C ⟹
      ∀a. ¬ is_Dst_Ports (C a) ⟹
      ∀r∈ set (normalize_rules (normalize_primitive_extract (disc, sel) C f) rs). normalized_dst_ports (get_match r)"
      by blast
    from preserve_normalized_dst_ports[OF normalized_rs2 normalized_dst_ports wf_disc_sel_common_primitive(3),
         where f3=ipt_iprange_compress, folded normalize_src_ips_def]
    have normalized_dst_ports_rs3: "∀r ∈ set ?rs3.  normalized_dst_ports (get_match r)" by force
    from preserve_normalized_dst_ports[OF normalized_rs3 normalized_dst_ports_rs3 wf_disc_sel_common_primitive(4),
         where f3=ipt_iprange_compress, folded normalize_dst_ips_def]
         normalized_rs4
    have normalized_dst_ports_rs4: "∀r ∈ set ?rs4. normalized_nnf_match (get_match r) ∧ normalized_dst_ports (get_match r)" by force
    with optimize_matches_option_compress_normalize_besteffort_preserves_unrelated_normalized_n_primitive[
          of _ is_Dst_Ports dst_ports_sel "(λps. case ps of L4Ports _ pts ⇒ length pts ≤ 1)"
          , folded normalized_dst_ports_def2]
    have normalized_dst_ports_rs5: "∀r ∈ set ?rs5. normalized_dst_ports (get_match r)" by fastforce

    from normalize_rules_preserves_unrelated_normalized_n_primitive[of ?rs3 is_Src src_sel normalized_cidr_ip,
         OF _ wf_disc_sel_common_primitive(4),
         where f=ipt_iprange_compress, folded normalize_dst_ips_def normalized_src_ips_def2]
         normalized_rs3 normalized_src_ips
    have normalized_src_rs4: "∀r ∈ set ?rs4. normalized_nnf_match (get_match r) ∧ normalized_src_ips (get_match r)" by force
    with optimize_matches_option_compress_normalize_besteffort_preserves_unrelated_normalized_n_primitive[
          of _ is_Src src_sel normalized_cidr_ip
          , folded normalized_src_ips_def2]
    have normalized_src_rs5: "∀r ∈ set ?rs5. normalized_src_ips (get_match r)"
       by fastforce

    from normalized_multiportports_rs5 normalized_src_ports_rs5
         normalized_dst_ports_rs5 normalized_src_rs5 normalized_dst_rs5
    show "∀ r ∈ set (transform_normalize_primitives rs).
          normalized_src_ports (get_match r) ∧ normalized_dst_ports (get_match r) ∧
          normalized_src_ips (get_match r) ∧ normalized_dst_ips (get_match r) ∧
          ¬ has_disc is_MultiportPorts (get_match r)"
      unfolding transform_normalize_primitives_def by simp
   

   show  "unchanged disc2 ⟹ (∀a. ¬ disc2 (IIface a)) ⟹ (∀a. ¬ disc2 (OIface a)) ⟹ (∀a. ¬ disc2 (Prot a)) ⟹
          ∀ r ∈ set rs. normalized_n_primitive (disc2, sel2) f (get_match r) ⟹
            ∀ r ∈ set (transform_normalize_primitives rs). normalized_n_primitive  (disc2, sel2) f (get_match r)"
   unfolding unchanged_def
   proof(elim conjE)
     assume "∀r∈ set rs. normalized_n_primitive  (disc2, sel2) f (get_match r)"
     with normalized have a':
      "∀r∈ set rs. normalized_nnf_match (get_match r) ∧ normalized_n_primitive (disc2, sel2) f (get_match r)" by blast

     assume a_Src_Ports: "∀a. ¬ disc2 (Src_Ports a)"
     assume a_Dst_Ports: "∀a. ¬ disc2 (Dst_Ports a)"
     assume a_Src: "∀a. ¬ disc2 (Src a)"
     assume a_Dst: "∀a. ¬ disc2 (Dst a)"
     assume a_IIface: "(∀a. ¬ disc2 (IIface a))"
     assume a_OIface: "(∀a. ¬ disc2 (OIface a))"
     assume a_Prot: "(∀a. ¬ disc2 (Prot a))"


     have normalized_n_primitive_rs0:
     "∀r∈set ?rs0. normalized_n_primitive (disc2, sel2) f (get_match r)"
      apply(intro normalize_rules_property[where P="λm. normalized_nnf_match m ∧ normalized_n_primitive (disc2, sel2) f m"])
       using a' apply blast
      using rewrite_MultiportPorts_preserves_normalized_n_primitive[OF _ a_Src_Ports a_Dst_Ports] by blast
     have normalized_n_primitive_rs1:
     "∀r∈set ?rs1. normalized_n_primitive (disc2, sel2) f (get_match r)" (*by blast*)
      apply(rule normalize_rules_property[where P="λm. normalized_nnf_match m ∧ normalized_n_primitive (disc2, sel2) f m"])
       using normalized_n_primitive_rs0 normalized_rs0 apply blast
      using normalize_src_ports_preserves_normalized_n_primitive[OF _ a_Src_Ports] a_Prot by blast
     have "∀r∈set ?rs2. normalized_n_primitive (disc2, sel2) f (get_match r)"
      apply(rule normalize_rules_property[where P="λm. normalized_nnf_match m ∧ normalized_n_primitive (disc2, sel2) f m"])
       using normalized_n_primitive_rs1 normalized_rs1 apply blast
      using normalize_dst_ports_preserves_normalized_n_primitive[OF _ a_Dst_Ports] a_Prot by blast
     with normalized_rs2 normalize_rules_preserves_unrelated_normalized_n_primitive[OF _ wf_disc_sel_common_primitive(3) a_Src,
       of ?rs2 sel2 f ipt_iprange_compress,
       folded normalize_src_ips_def]
     have "∀r∈set ?rs3. normalized_n_primitive (disc2, sel2) f (get_match r)" by blast
     with normalized_rs3 normalize_rules_preserves_unrelated_normalized_n_primitive[OF _ wf_disc_sel_common_primitive(4) a_Dst,
       of ?rs3 sel2 f ipt_iprange_compress,
       folded normalize_dst_ips_def]
     have "∀r∈set ?rs4. normalized_nnf_match (get_match r) ∧ normalized_n_primitive (disc2, sel2) f (get_match r)" by blast
     hence "∀r∈set ?rs5. normalized_nnf_match (get_match r) ∧ normalized_n_primitive (disc2, sel2) f (get_match r)" 
       apply(intro optimize_matches_option_compress_normalize_besteffort_preserves_unrelated_normalized_n_primitive)
          using a_IIface a_OIface a_Prot by simp_all
     thus ?thesis
       unfolding transform_normalize_primitives_def by simp
   qed

   ― ‹Pushing through properties through the ip normalizer›
   { fix m and m' and disc::"('i::len common_primitive ⇒ bool)"
         and sel::"('i::len common_primitive ⇒ 'x)" and C'::" ('x ⇒ 'i::len common_primitive)"
         and f'::"('x negation_type list ⇒ 'x list)"
     assume am: "¬ has_disc disc1 m"
        and nm: "normalized_nnf_match m"
        and am': "m' ∈ set (normalize_primitive_extract (disc, sel) C' f' m)"
        and wfdiscsel: "wf_disc_sel (disc,sel) C'"
        and disc_different: "∀a. ¬ disc1 (C' a)"

        (*from wfdiscsel disc_different have "∀a. ¬ disc1 (C' a)"
          apply(simp add: wf_disc_sel.simps)*)

        from disc_different have af: "∀spts. (∀a ∈ Match ` C' ` set (f' spts). ¬ has_disc disc1 a)"
          by(simp)

        obtain as ms where asms: "primitive_extractor (disc, sel) m = (as, ms)" by fastforce

        from am' asms have "m' ∈ (λspt. MatchAnd (Match (C' spt)) ms) ` set (f' as)"
          unfolding normalize_primitive_extract_def by(simp)
        hence goalrule:"∀spt ∈ set (f' as). ¬ has_disc disc1 (Match (C' spt)) ⟹ ¬ has_disc disc1 ms ⟹ ¬ has_disc disc1 m'" by fastforce

        from am primitive_extractor_correct(4)[OF nm wfdiscsel asms] have 1: "¬ has_disc disc1 ms" by simp
        from af have 2: "∀spt ∈ set (f' as). ¬ has_disc disc1 (Match (C' spt))" by simp

        from goalrule[OF 2 1] have "¬ has_disc disc1 m'" .
        moreover from nm have "normalized_nnf_match m'" by (metis am' normalize_primitive_extract_preserves_nnf_normalized wfdiscsel)
        ultimately have "¬ has_disc disc1 m' ∧ normalized_nnf_match m'" by simp
   }
   hence x: "⋀disc sel C' f'. wf_disc_sel (disc, sel) C' ⟹ ∀a. ¬ disc1 (C' a) ⟹
   ∀m. normalized_nnf_match m ∧ ¬ has_disc disc1 m ⟶
     (∀m'∈set (normalize_primitive_extract (disc, sel) C' f' m). normalized_nnf_match m' ∧ ¬ has_disc disc1 m')"
   by blast

   ― ‹Pushing through properties through the ports normalizer›
   from normalize_src_ports_preserves_normalized_not_has_disc normalize_src_ports_nnf have x_src_ports:
    "∀a. ¬ disc (Src_Ports a) ⟹  ∀a. ¬ disc (Prot a) ⟹  
       m' ∈ set (normalize_src_ports m) ⟹
            normalized_nnf_match m ⟹ ¬ has_disc disc m ⟹ ¬ has_disc disc m' ∧ normalized_nnf_match m'"
    for m m' and disc :: "'i common_primitive ⇒ bool" by blast
   from normalize_dst_ports_preserves_normalized_not_has_disc normalize_dst_ports_nnf have x_dst_ports:
    "∀a. ¬ disc (Dst_Ports a) ⟹  ∀a. ¬ disc (Prot a) ⟹  
       m'∈ set (normalize_dst_ports m) ⟹
          normalized_nnf_match m ⟹ ¬ has_disc disc m ⟹ ¬ has_disc disc m' ∧ normalized_nnf_match m'"
    for m m' and disc :: "'i common_primitive ⇒ bool"   by blast

   { fix rs
     assume "(∀a. ¬ disc1 (IIface a)) ∨ disc1 = is_Iiface"
        and "((∀a. ¬ disc1 (OIface a)) ∨ disc1 = is_Oiface)"
        and "(∀a. ¬ disc1 (Prot a))"
     hence "∀m∈set rs. ¬ has_disc disc1 (get_match m) ∧ normalized_nnf_match (get_match m) ⟹
              ∀m∈set (optimize_matches_option compress_normalize_besteffort rs).
                  normalized_nnf_match (get_match m) ∧ ¬ has_disc disc1 (get_match m)"
     apply -
     apply(rule optimize_matches_option_preserves)
     apply(elim disjE)
            using compress_normalize_besteffort_hasdisc apply blast
           using compress_normalize_besteffort_nnf compress_normalize_besteffort_not_introduces_Iiface
                 compress_normalize_besteffort_not_introduces_Oiface by blast+
   } note y=this

   have "∀a. ¬ disc1 (Src_Ports a) ⟹ ∀a. ¬ disc1 (Dst_Ports a) ⟹ 
         ∀a. ¬ disc1 (Src a) ⟹ ∀a. ¬ disc1 (Dst a) ⟹
         (∀a. ¬ disc1 (IIface a)) ∨ disc1 = is_Iiface ⟹
         (∀a. ¬ disc1 (OIface a)) ∨ disc1 = is_Oiface ⟹ (∀a. ¬ disc1 (Prot a)) ⟹
         ∀ r∈set rs. ¬ has_disc disc1 (get_match r) ∧ normalized_nnf_match (get_match r) ⟹
    ∀ r ∈ set (transform_normalize_primitives rs). normalized_nnf_match (get_match r) ∧ ¬ has_disc disc1 (get_match r)"
   unfolding transform_normalize_primitives_def
   apply(simp)
   apply(rule y)
      apply(simp; fail)
     apply(simp; fail)
    apply(simp; fail)
   apply(rule normalize_rules_preserves)+
        apply(simp; fail)
       subgoal
       apply(intro allI impI conjI ballI)
        apply(rule rewrite_MultiportPorts_preserves_normalized_not_has_disc, simp_all)
       by(simp add: rewrite_MultiportPorts_normalized_nnf_match)
      subgoal
      apply clarify
      apply(rule x_src_ports)
          by simp+
     subgoal
     apply clarify
     by(rule x_dst_ports) simp+
    using x[OF wf_disc_sel_common_primitive(3), of ipt_iprange_compress,folded normalize_src_ips_def] apply blast
   using x[OF wf_disc_sel_common_primitive(4), of ipt_iprange_compress,folded normalize_dst_ips_def] apply blast
   done
   
   thus "unchanged disc1 ⟹ changeddisc disc1 ⟹ ∀a. ¬ disc1 (Prot a) ⟹
    ∀ r ∈ set rs. ¬ has_disc disc1 (get_match r) ⟹
      ∀ r ∈ set (transform_normalize_primitives rs). ¬ has_disc disc1 (get_match r)"
   unfolding unchanged_def changeddisc_def using normalized by blast

   (*copy pasta*)
   { fix m and m' and disc::"('i::len common_primitive ⇒ bool)"
         and sel::"('i::len common_primitive ⇒ 'x)" and C'::" ('x ⇒ 'i::len common_primitive)"
         and f'::"('x negation_type list ⇒ 'x list)" and neg
         and disc3
     assume am: "¬ has_disc_negated disc3 neg m"
        and nm: "normalized_nnf_match m"
        and am': "m' ∈ set (normalize_primitive_extract (disc, sel) C' f' m)"
        and wfdiscsel: "wf_disc_sel (disc,sel) C'"
        and disc_different: "∀a. ¬ disc3 (C' a)"

        from disc_different have af: "∀spts. (∀a ∈ Match ` C' ` set (f' spts). ¬ has_disc disc3 a)"
          by(simp)

        obtain as ms where asms: "primitive_extractor (disc, sel) m = (as, ms)" by fastforce

        from am' asms have "m' ∈ (λspt. MatchAnd (Match (C' spt)) ms) ` set (f' as)"
          unfolding normalize_primitive_extract_def by(simp)
        hence goalrule:"∀spt ∈ set (f' as). ¬ has_disc_negated disc3 neg (Match (C' spt)) ⟹
            ¬ has_disc_negated disc3 neg ms ⟹ ¬ has_disc_negated disc3 neg m'" by fastforce

        from am primitive_extractor_correct(6)[OF nm wfdiscsel asms] have 1: "¬ has_disc_negated disc3 neg ms" by simp
        from af have 2: "∀spt ∈ set (f' as). ¬ has_disc_negated disc3 neg (Match (C' spt))" by simp

        from goalrule[OF 2 1] have "¬ has_disc_negated disc3 neg m'" .
        moreover from nm have "normalized_nnf_match m'" by (metis am' normalize_primitive_extract_preserves_nnf_normalized wfdiscsel)
        ultimately have "¬ has_disc_negated disc3 neg m' ∧ normalized_nnf_match m'" by simp
   }
   note x_generic=this
   hence x: "wf_disc_sel (disc, sel) C' ⟹ ∀a. ¬ disc3 (C' a) ⟹
   ∀m. normalized_nnf_match m ∧ ¬ has_disc_negated disc3 False m ⟶
    (∀m' ∈ set (normalize_primitive_extract (disc, sel) C' f' m).
            normalized_nnf_match m' ∧ ¬ has_disc_negated disc3 False m')"
   for disc :: "'i common_primitive ⇒ bool" and sel and C' :: "'c ⇒ 'i common_primitive" and f' and disc3
   by blast

   ― ‹Pushing through properties through the ports normalizer›
   from normalize_src_ports_preserves_normalized_not_has_disc_negated normalize_src_ports_nnf have x_src_ports:
    "∀a. ¬ disc (Src_Ports a) ⟹ (∀a. ¬ disc (Prot a)) ∨ ¬ has_disc_negated is_Src_Ports False m ⟹  
       m' ∈ set (normalize_src_ports m) ⟹
         normalized_nnf_match m ⟹ ¬ has_disc_negated disc False m ⟹
            ¬ has_disc_negated disc False m' ∧ normalized_nnf_match m'"
    for m m' and disc :: "'i common_primitive ⇒ bool" by blast

   from normalize_dst_ports_preserves_normalized_not_has_disc_negated normalize_dst_ports_nnf have x_dst_ports:
    "∀a. ¬ disc (Src_Ports a) ⟹ (∀a. ¬ disc (Prot a)) ∨ ¬ has_disc_negated is_Dst_Ports False m ⟹  
       m' ∈ set (normalize_dst_ports m) ⟹
         normalized_nnf_match m ⟹ ¬ has_disc_negated disc False m ⟹
            ¬ has_disc_negated disc False m' ∧ normalized_nnf_match m'"
    for m m' and disc :: "'i common_primitive ⇒ bool" by blast

  (*push arbitrary P m through too. y is then λ_. True [simplified]*)
  { fix rs
    fix P :: "'i common_primitive match_expr ⇒ bool"
    assume "(∀a. ¬ disc3 (IIface a)) ∨ disc3 = is_Iiface"
        and "(∀a. ¬ disc3 (OIface a)) ∨ disc3 = is_Oiface"
        and "(∀a. ¬ disc3 (Prot a)) ∨ disc3 = is_Prot"
        and P_prop: "∀m m'. normalized_nnf_match m ⟶ P m ⟶ compress_normalize_besteffort m = Some m' ⟶ P m'"
     hence
      "∀r∈set rs. ¬ has_disc_negated disc3 False (get_match r) ∧ normalized_nnf_match (get_match r) ∧ P (get_match r) ⟹
       ∀r∈set (optimize_matches_option compress_normalize_besteffort rs).
                normalized_nnf_match (get_match r) ∧ ¬ has_disc_negated disc3 False (get_match r) ∧ P (get_match r)"
     apply -
     thm optimize_matches_option_preserves[where P=
        "λm. normalized_nnf_match m ∧ ¬ has_disc_negated disc3 False m ∧ P m"]
     apply(rule optimize_matches_option_preserves[where P=
        "λm. normalized_nnf_match m ∧ ¬ has_disc_negated disc3 False m ∧ P m"])
     apply(elim disjE)
            using compress_normalize_besteffort_nnf compress_normalize_besteffort_hasdisc_negated apply blast
           using compress_normalize_besteffort_nnf
                 compress_normalize_besteffort_not_introduces_Iiface_negated
                 compress_normalize_besteffort_not_introduces_Oiface_negated
                 compress_normalize_besteffort_not_introduces_Prot_negated by blast+
   } note y_generic=this
  
  note y=y_generic[of "λ_. True", simplified]

  
   have case_disc3_is_not_prot: "∀a. ¬ disc3 (Src_Ports a) ⟹ ∀a. ¬ disc3 (Dst_Ports a) ⟹ 
         ∀a. ¬ disc3 (Src a) ⟹ ∀a. ¬ disc3 (Dst a) ⟹
         (∀a. ¬ disc3 (IIface a)) ∨ disc3 = is_Iiface ⟹
         (∀a. ¬ disc3 (OIface a)) ∨ disc3 = is_Oiface ⟹
         (∀a. ¬ disc3 (Prot a)) ⟹
         ∀ r ∈ set rs. ¬ has_disc_negated disc3 False (get_match r) ∧ normalized_nnf_match (get_match r) ⟹
    ∀ r ∈ set (transform_normalize_primitives rs). normalized_nnf_match (get_match r) ∧ ¬ has_disc_negated disc3 False (get_match r)"
   unfolding transform_normalize_primitives_def
   apply(simp)
   apply(rule y)
      apply(simp; fail)
     apply(simp; fail)
    apply(blast)
   apply(rule normalize_rules_preserves)+
        apply(simp; fail)
       subgoal
       apply(intro allI impI conjI ballI)
        apply(rule rewrite_MultiportPorts_preserves_normalized_not_has_disc_negated, simp_all)
       by(simp add: rewrite_MultiportPorts_normalized_nnf_match)
      subgoal
      apply(clarify)
      apply(rule_tac m6=m in x_src_ports)
          by(simp)+
     subgoal
     apply(clarify)
     by(rule x_dst_ports) simp+
    using x[OF wf_disc_sel_common_primitive(3), of disc3 ipt_iprange_compress, folded normalize_src_ips_def] apply blast
   using x[OF wf_disc_sel_common_primitive(4), of disc3 ipt_iprange_compress, folded normalize_dst_ips_def] apply blast
   done

   have case_disc3_is_prot_optimize_matches_option:"∀r∈set rs.
         ¬ has_disc_negated is_Prot False (get_match r) ∧
         normalized_nnf_match (get_match r) ∧
         ¬ has_disc_negated is_Src_Ports False (get_match r) ∧
         ¬ has_disc_negated is_Dst_Ports False (get_match r) ⟹
      ∀r∈set (optimize_matches_option compress_normalize_besteffort rs).
         normalized_nnf_match (get_match r) ∧
         ¬ has_disc_negated is_Prot False (get_match r) ∧
         ¬ has_disc_negated is_Src_Ports False (get_match r) ∧
         ¬ has_disc_negated is_Dst_Ports False (get_match r)"
   if isprot: "disc3 = is_Prot"
   for rs :: "'i common_primitive rule list"
   apply(rule y_generic[where P8="λm. ¬ has_disc_negated is_Src_Ports False m ∧ ¬ has_disc_negated is_Dst_Ports False m", simplified isprot])
       apply simp+
    apply(clarify)
    apply(intro conjI)
     using compress_normalize_besteffort_hasdisc_negated[of is_Src_Ports] apply fastforce
    using compress_normalize_besteffort_hasdisc_negated[of is_Dst_Ports] apply fastforce
   by simp

   (*copy from above, specific version for is_Prot*)
   (*Push through things, but now more complicated because several things could introduce Prots*)
   have case_disc3_is_prot: "disc3 = is_Prot ⟹
  ∀ r ∈ set rs. ¬ has_disc_negated disc3 False (get_match r) ∧ normalized_nnf_match (get_match r) ∧
         ¬ has_disc_negated is_Src_Ports False (get_match r) ∧ ¬ has_disc_negated is_Dst_Ports False (get_match r) &
         ¬ has_disc is_MultiportPorts (get_match r) ― ‹MultiportPorts could be rewritten to negated ‹Src›/‹Dst› Ports› ⟹
    ∀ r ∈ set (transform_normalize_primitives rs). normalized_nnf_match (get_match r) ∧ ¬ has_disc_negated disc3 False (get_match r) ∧
              ¬ has_disc_negated is_Src_Ports False (get_match r) ∧ ¬ has_disc_negated is_Dst_Ports False (get_match r)"
   unfolding transform_normalize_primitives_def
   apply(simp)
   apply(rule case_disc3_is_prot_optimize_matches_option)
    apply(simp; fail)
   thm normalize_rules_property[
      where P="λm. normalized_nnf_match m ∧ ¬ has_disc_negated disc3 False m"]
   apply(rule normalize_rules_property[
      where P="λm. normalized_nnf_match m ∧
                   ¬ has_disc_negated disc3 False m ∧
                   ¬ has_disc_negated is_Src_Ports False m ∧
                   ¬ has_disc_negated is_Dst_Ports False m"]) (*dst ips*)
    apply(rule normalize_rules_property[
      where P="λm. normalized_nnf_match m ∧
                   ¬ has_disc_negated disc3 False m ∧
                   ¬ has_disc_negated is_Src_Ports False m ∧
                   ¬ has_disc_negated is_Dst_Ports False m"])(*src ips*)
     apply(rule normalize_rules_property[
      where P="λm. normalized_nnf_match m ∧
                   ¬ has_disc_negated disc3 False m ∧
                   ¬ has_disc_negated is_Src_Ports False m ∧
                   ¬ has_disc_negated is_Dst_Ports False m"])(*dst ports*)
      apply(rule normalize_rules_property[
      where P="λm. normalized_nnf_match m ∧
                   ¬ has_disc_negated disc3 False m ∧
                   ¬ has_disc_negated is_Src_Ports False m ∧
                   ¬ has_disc_negated is_Dst_Ports False m"])(*src ports*)
       apply(rule normalize_rules_property[
      where P="λm. normalized_nnf_match m ∧
                   ¬ has_disc_negated disc3 False m ∧
                   ¬ has_disc_negated is_Src_Ports False m ∧
                   ¬ has_disc_negated is_Dst_Ports False m ∧
                   ¬ has_disc is_MultiportPorts m"]) (*multiports, needs ¬ has_disc is_MultiportPorts m*)
        apply(simp; fail)
       subgoal
       apply(intro allI impI conjI ballI)
          apply(simp add: rewrite_MultiportPorts_normalized_nnf_match; fail)
         apply(rule rewrite_MultiportPorts_preserves_normalized_not_has_disc_negated, simp_all)
         ― ‹Here we need @{term "¬ has_disc is_MultiportPorts m"}›
         using rewrite_MultiportPorts_unchanged_if_not_has_disc by fastforce+
      subgoal (*yeah, just need to consider the other cases*)
      apply(clarify)
      apply(frule_tac m6=m in x_src_ports[rotated 2])
          apply(simp_all)
       apply simp
      using normalize_src_ports_preserves_normalized_not_has_disc_negated by blast
     subgoal
     apply(clarify)
     apply(frule_tac m6=m in x_dst_ports[rotated 2])
         apply(simp_all)
      apply simp
     using normalize_dst_ports_preserves_normalized_not_has_disc_negated by blast
    using x[OF wf_disc_sel_common_primitive(3), of disc3 ipt_iprange_compress, folded normalize_src_ips_def]
          x[OF wf_disc_sel_common_primitive(3), of is_Dst_Ports ipt_iprange_compress, folded normalize_src_ips_def]
          x_generic[OF _ _ _ wf_disc_sel_common_primitive(3), of is_Src_Ports False _ _ ipt_iprange_compress, folded normalize_src_ips_def]
          apply (meson common_primitive.disc(45) common_primitive.disc(56) common_primitive.disc(67); fail)
   using x[OF wf_disc_sel_common_primitive(4), of disc3 ipt_iprange_compress, folded normalize_dst_ips_def]
          x[OF wf_disc_sel_common_primitive(4), of is_Src_Ports ipt_iprange_compress, folded normalize_dst_ips_def]
          x_generic[OF _ _ _ wf_disc_sel_common_primitive(4), of is_Dst_Ports False _ _ ipt_iprange_compress, folded normalize_dst_ips_def]
          apply (meson common_primitive.disc(46) common_primitive.disc(57) common_primitive.disc(68); fail)    
   done

   show "unchanged disc3 ⟹ changeddisc disc3 ⟹
    (∀a. ¬ disc3 (Prot a)) ∨
        (disc3 = is_Prot ∧ (∀ r ∈ set rs.
          ¬ has_disc_negated is_Src_Ports False (get_match r) ∧
          ¬ has_disc_negated is_Dst_Ports False (get_match r) ∧
          ¬ has_disc is_MultiportPorts (get_match r))) ⟹
         ∀ r ∈ set rs. ¬ has_disc_negated disc3 False (get_match r) ⟹
            ∀ r ∈ set (transform_normalize_primitives rs). ¬ has_disc_negated disc3 False (get_match r)"
   unfolding unchanged_def changeddisc_def
   apply(elim disjE)
    using normalized case_disc3_is_not_prot apply blast
   using normalized case_disc3_is_prot by blast
qed


theorem iiface_constrain:
  assumes simplers: "simple_ruleset rs"
      and normalized: "∀ r ∈ set rs. normalized_nnf_match (get_match r)"
      and wf_ipassmt: "ipassmt_sanity_nowildcards ipassmt"
      and nospoofing: "⋀ips. ipassmt (Iface (p_iiface p)) = Some ips ⟹ p_src p ∈ ipcidr_union_set (set ips)"
  shows "(common_matcher, α),p⊢ ⟨optimize_matches (iiface_constrain ipassmt) rs, s⟩ ⇒⇩α t ⟷ (common_matcher, α),p⊢ ⟨rs, s⟩ ⇒⇩α t"
    and "simple_ruleset (optimize_matches (iiface_constrain ipassmt) rs)"
  proof -
    show simplers_t: "simple_ruleset (optimize_matches (iiface_constrain ipassmt) rs)"
      by (simp add: optimize_matches_simple_ruleset simplers)

    have my_arg_cong: "⋀P Q. P s = Q s ⟹ (P s = t) ⟷ (Q s = t)" by simp
    
    show "(common_matcher, α),p⊢ ⟨optimize_matches (iiface_constrain ipassmt) rs, s⟩ ⇒⇩α t ⟷ (common_matcher, α),p⊢ ⟨rs, s⟩ ⇒⇩α t"
     unfolding approximating_semantics_iff_fun_good_ruleset[OF simple_imp_good_ruleset[OF simplers_t]]
     unfolding approximating_semantics_iff_fun_good_ruleset[OF simple_imp_good_ruleset[OF simplers]]
     apply(rule my_arg_cong)
     apply(rule optimize_matches_generic[where P="λ m _. normalized_nnf_match m"])
      apply(simp add: normalized)
     apply(rule matches_iiface_constrain)
       apply(simp_all add: wf_ipassmt nospoofing)
     done
qed

text‹In contrast to @{thm iiface_constrain}, this requires  @{const ipassmt_sanity_disjoint} and 
      as much stronger nospoof assumption: This assumption requires that the packet is actually in ipassmt!›
theorem iiface_rewrite:
  assumes simplers: "simple_ruleset rs"
      and normalized: "∀ r ∈ set rs. normalized_nnf_match (get_match r)"
      and wf_ipassmt: "ipassmt_sanity_nowildcards ipassmt"
      and disjoint_ipassmt: "ipassmt_sanity_disjoint ipassmt"
      and nospoofing: "∃ips. ipassmt (Iface (p_iiface p)) = Some ips ∧ p_src p ∈ ipcidr_union_set (set ips)"
  shows "(common_matcher, α),p⊢ ⟨optimize_matches (iiface_rewrite ipassmt) rs, s⟩ ⇒⇩α t ⟷ (common_matcher, α),p⊢ ⟨rs, s⟩ ⇒⇩α t"
    and "simple_ruleset (optimize_matches (iiface_rewrite ipassmt) rs)"
  proof -
    show simplers_t: "simple_ruleset (optimize_matches (iiface_rewrite ipassmt) rs)"
      by(simp add: simplers optimize_matches_simple_ruleset)

    ― ‹packet must come from a defined interface!›
    from nospoofing have "Iface (p_iiface p) ∈ dom ipassmt" by blast

    have my_arg_cong: "⋀P Q. P s = Q s ⟹ (P s = t) ⟷ (Q s = t)" by simp
    
    show "(common_matcher, α),p⊢ ⟨optimize_matches (iiface_rewrite ipassmt) rs, s⟩ ⇒⇩α t ⟷ (common_matcher, α),p⊢ ⟨rs, s⟩ ⇒⇩α t"
     unfolding approximating_semantics_iff_fun_good_ruleset[OF simple_imp_good_ruleset[OF simplers_t]]
     unfolding approximating_semantics_iff_fun_good_ruleset[OF simple_imp_good_ruleset[OF simplers]]
     apply(rule my_arg_cong)
     apply(rule optimize_matches_generic[where P="λ m _. normalized_nnf_match m"])
      apply(simp add: normalized)
     apply(rule matches_iiface_rewrite)
        apply(simp_all add: wf_ipassmt nospoofing disjoint_ipassmt)
     done
qed

(* Copy of iiface_rewrite *)
theorem oiface_rewrite:
  assumes simplers: "simple_ruleset rs"
      and normalized: "∀ r ∈ set rs. normalized_nnf_match (get_match r)"
      and wf_ipassmt: "ipassmt_sanity_nowildcards ipassmt"
      and ipassmt_from_rt: "ipassmt = map_of (routing_ipassmt rt)"
      and correct_routing: "correct_routing rt"
      and rtbl_decided: "output_iface (routing_table_semantics rt (p_dst p)) = p_oiface p"
  shows "(common_matcher, α),p⊢ ⟨optimize_matches (oiface_rewrite ipassmt) rs, s⟩ ⇒⇩α t ⟷ (common_matcher, α),p⊢ ⟨rs, s⟩ ⇒⇩α t"
    and "simple_ruleset (optimize_matches (oiface_rewrite ipassmt) rs)"
  proof -
    show simplers_t: "simple_ruleset (optimize_matches (oiface_rewrite ipassmt) rs)"
      using simplers by(fact optimize_matches_simple_ruleset)
    show "(common_matcher, α),p⊢ ⟨optimize_matches (oiface_rewrite ipassmt) rs, s⟩ ⇒⇩α t ⟷ (common_matcher, α),p⊢ ⟨rs, s⟩ ⇒⇩α t"
     unfolding approximating_semantics_iff_fun_good_ruleset[OF simple_imp_good_ruleset[OF simplers_t]]
     unfolding approximating_semantics_iff_fun_good_ruleset[OF simple_imp_good_ruleset[OF simplers]]
     apply(rule arg_cong[where f="λx. x = t"])
     apply(rule optimize_matches_generic[where P="λ m _. normalized_nnf_match m"])
      apply(simp add: normalized ;fail)
     apply(rule matches_oiface_rewrite[OF _ _ _ ipassmt_from_rt]; assumption?)
        apply(simp_all add: wf_ipassmt correct_routing rtbl_decided)
     done
qed


definition upper_closure :: "'i::len common_primitive rule list ⇒ 'i common_primitive rule list" where
  "upper_closure rs == remdups_rev (transform_optimize_dnf_strict
      (transform_normalize_primitives (transform_optimize_dnf_strict (optimize_matches_a upper_closure_matchexpr rs))))"
definition lower_closure :: "'i::len common_primitive rule list ⇒ 'i common_primitive rule list" where
  "lower_closure rs == remdups_rev (transform_optimize_dnf_strict
      (transform_normalize_primitives (transform_optimize_dnf_strict (optimize_matches_a lower_closure_matchexpr rs))))"


text‹putting it all together›
lemma transform_upper_closure:
  assumes simplers: "simple_ruleset rs"
  ― ‹semantics are preserved›
  shows "(common_matcher, in_doubt_allow),p⊢ ⟨upper_closure rs, s⟩ ⇒⇩α t ⟷ (common_matcher, in_doubt_allow),p⊢ ⟨rs, s⟩ ⇒⇩α t"
  and "simple_ruleset (upper_closure rs)"
  ― ‹simple, normalized rules without unknowns›
  and "∀ r ∈ set (upper_closure rs). normalized_nnf_match (get_match r) ∧
                                     normalized_src_ports (get_match r) ∧
                                     normalized_dst_ports (get_match r) ∧
                                     normalized_src_ips (get_match r) ∧
                                     normalized_dst_ips (get_match r) ∧
                                     ¬ has_disc is_MultiportPorts (get_match r) ∧
                                     ¬ has_disc is_Extra (get_match r)"
  ― ‹no new primitives are introduced›
  and "∀a. ¬ disc (Src_Ports a) ⟹ ∀a. ¬ disc (Dst_Ports a) ⟹ ∀a. ¬ disc (Src a) ⟹ ∀a. ¬ disc (Dst a) ⟹
       ∀a. ¬ disc (IIface a) ∨ disc = is_Iiface ⟹ ∀a. ¬ disc (OIface a) ∨ disc = is_Oiface ⟹
       ∀a. ¬ disc (Prot a) ⟹
        ∀ r ∈ set rs. ¬ has_disc disc (get_match r) ⟹ ∀ r ∈ set (upper_closure rs). ¬ has_disc disc (get_match r)"
  and "∀a. ¬ disc (Src_Ports a) ⟹ ∀a. ¬ disc (Dst_Ports a) ⟹ ∀a. ¬ disc (Src a) ⟹ ∀a. ¬ disc (Dst a) ⟹
       ∀a. ¬ disc (IIface a) ∨ disc = is_Iiface ⟹ ∀a. ¬ disc (OIface a) ∨ disc = is_Oiface ⟹
       (∀a. ¬ disc (Prot a)) ∨
        disc = is_Prot ∧ ― ‹if it is prot, there must not be negated matches on ports›
        (∀ r ∈ set rs. ¬ has_disc_negated is_Src_Ports False (get_match r) ∧
                       ¬ has_disc_negated is_Dst_Ports False (get_match r) ∧
                       ¬ has_disc is_MultiportPorts (get_match r)) ⟹
         ∀ r ∈ set rs. ¬ has_disc_negated disc False (get_match r) ⟹
         ∀ r ∈ set (upper_closure rs). ¬ has_disc_negated disc False (get_match r)"
  proof -
    let ?rs1="optimize_matches_a upper_closure_matchexpr rs"
    let ?rs2="transform_optimize_dnf_strict ?rs1"
    let ?rs3="transform_normalize_primitives ?rs2"
    let ?rs4="transform_optimize_dnf_strict ?rs3"

    { fix m a
        have "Rule m a ∈ set (upper_closure rs) ⟹
            (a = action.Accept ∨ a = action.Drop) ∧
             normalized_nnf_match m ∧
             normalized_src_ports m ∧
             normalized_dst_ports m ∧
             normalized_src_ips m ∧
             normalized_dst_ips m ∧
             ¬ has_disc is_MultiportPorts m ∧
             ¬ has_disc is_Extra m"
        using simplers
        unfolding upper_closure_def
        apply(simp add: remdups_rev_set)
        apply(frule transform_remove_unknowns_upper(4))
        apply(drule transform_remove_unknowns_upper(2))
        thm transform_optimize_dnf_strict[OF _ wf_in_doubt_allow]
        apply(frule(1) transform_optimize_dnf_strict_structure(2)[OF _ wf_in_doubt_allow, where disc=is_Extra])
        apply(thin_tac "∀r∈ set (optimize_matches_a upper_closure_matchexpr rs). ¬ has_disc is_Extra (get_match r)")
        apply(frule transform_optimize_dnf_strict_structure(3)[OF _ wf_in_doubt_allow])
        apply(drule transform_optimize_dnf_strict_structure(1)[OF _ wf_in_doubt_allow])
        thm transform_normalize_primitives[OF _ wf_in_doubt_allow]
        apply(frule(1) transform_normalize_primitives(3)[OF _ wf_in_doubt_allow, of _ is_Extra])
            apply(simp;fail)
           apply(simp;fail)
          apply(simp;fail)
         apply blast
        apply(thin_tac "∀r∈ set ?rs2. ¬ has_disc is_Extra (get_match r)")
        apply(frule(1) transform_normalize_primitives(5)[OF _ wf_in_doubt_allow])
        apply(drule transform_normalize_primitives(2)[OF _ wf_in_doubt_allow], simp)
        thm transform_optimize_dnf_strict[OF _ wf_in_doubt_allow]
        apply(frule(1) transform_optimize_dnf_strict_structure(2)[OF _ wf_in_doubt_allow, where disc=is_Extra])
        apply(frule transform_optimize_dnf_strict_structure(2)[OF _ wf_in_doubt_allow, where disc=is_MultiportPorts])
         apply blast
        apply(frule transform_optimize_dnf_strict_structure(3)[OF _ wf_in_doubt_allow])
        apply(frule transform_optimize_dnf_strict_structure(4)[OF _ wf_in_doubt_allow, of _ "(is_Src_Ports, src_ports_sel)" "(λps. case ps of L4Ports _ pts ⇒ length pts ≤ 1)"])
         apply(simp add: normalized_src_ports_def2; fail)
        apply(frule transform_optimize_dnf_strict_structure(4)[OF _ wf_in_doubt_allow, of _ "(is_Dst_Ports, dst_ports_sel)" "(λps. case ps of L4Ports _ pts ⇒ length pts ≤ 1)"])
         apply(simp add: normalized_dst_ports_def2; fail)
        apply(frule transform_optimize_dnf_strict_structure(4)[OF _ wf_in_doubt_allow, of _ "(is_Src, src_sel)" normalized_cidr_ip])
         apply(simp add: normalized_src_ips_def2; fail)
        apply(frule transform_optimize_dnf_strict_structure(4)[OF _ wf_in_doubt_allow, of _ "(is_Dst, dst_sel)" normalized_cidr_ip])
         apply(simp add: normalized_dst_ips_def2; fail)
        apply(thin_tac "∀r∈set ?rs2. _ r")+
        apply(thin_tac "∀r∈set ?rs3. _ r")+
        apply(drule transform_optimize_dnf_strict_structure(1)[OF _ wf_in_doubt_allow])
        apply(subgoal_tac "(a = action.Accept ∨ a = action.Drop)")
         prefer 2
         apply(simp_all add: simple_ruleset_def)
         apply fastforce
        apply(simp add: normalized_src_ports_def2 normalized_dst_ports_def2 normalized_src_ips_def2 normalized_dst_ips_def2)
        apply(intro conjI)
               by fastforce+ (*1s*)
    } note 1=this

    from 1 show "simple_ruleset (upper_closure rs)"
      apply(simp add: simple_ruleset_def)
      apply(clarify)
      apply(rename_tac r)
      apply(case_tac r)
      apply(simp)
      by blast


    from 1 show "∀ r ∈ set (upper_closure rs). normalized_nnf_match (get_match r) ∧
         normalized_src_ports (get_match r) ∧
         normalized_dst_ports (get_match r) ∧
         normalized_src_ips (get_match r) ∧
         normalized_dst_ips (get_match r) ∧
         ¬ has_disc is_MultiportPorts (get_match r) ∧
         ¬ has_disc is_Extra (get_match r)"
      apply(clarify)
      apply(rename_tac r)
      apply(case_tac r)
      apply(simp)
      done
      

    show "∀a. ¬ disc (Src_Ports a) ⟹ ∀a. ¬ disc (Dst_Ports a) ⟹ ∀a. ¬ disc (Src a) ⟹ ∀a. ¬ disc (Dst a) ⟹
          ∀a. ¬ disc (IIface a) ∨ disc = is_Iiface ⟹ ∀a. ¬ disc (OIface a) ∨ disc = is_Oiface ⟹
          ∀a. ¬ disc (Prot a) ⟹
            ∀ r ∈ set rs. ¬ has_disc disc (get_match r) ⟹ ∀ r ∈ set (upper_closure rs). ¬ has_disc disc (get_match r)"
    using simplers
    unfolding upper_closure_def
    apply - 
    apply(frule(1) transform_remove_unknowns_upper(3)[where disc=disc])
    apply(drule transform_remove_unknowns_upper(2))
    apply(frule(1) transform_optimize_dnf_strict_structure(2)[OF _ wf_in_doubt_allow, where disc=disc])
    apply(frule transform_optimize_dnf_strict_structure(3)[OF _ wf_in_doubt_allow])
    apply(drule transform_optimize_dnf_strict_structure(1)[OF _ wf_in_doubt_allow])
    apply(frule(1) transform_normalize_primitives(3)[OF _ wf_in_doubt_allow, of _ disc])
        apply(simp;fail)
       apply blast
      apply(simp;fail)
     apply(simp;fail)
    apply(drule transform_normalize_primitives(2)[OF _ wf_in_doubt_allow], simp)
    apply(frule(1) transform_optimize_dnf_strict_structure(2)[OF _ wf_in_doubt_allow, where disc=disc])
    apply(simp add: remdups_rev_set)
    done

    have no_ports_1:
    "¬ has_disc_negated is_Src_Ports False (get_match m) ∧
     ¬ has_disc_negated is_Dst_Ports False (get_match m) ∧
     ¬ has_disc is_MultiportPorts (get_match m)"
    if no_ports: "∀r∈set rs.
      ¬ has_disc_negated is_Src_Ports False (get_match r) ∧
      ¬ has_disc_negated is_Dst_Ports False (get_match r) ∧
      ¬ has_disc is_MultiportPorts (get_match r)"
    and m: "m ∈ set (transform_optimize_dnf_strict (optimize_matches_a upper_closure_matchexpr rs))"
    for m
    proof -
      from no_ports transform_remove_unknowns_upper(3,6)[OF simplers] have
      "∀r∈ set (optimize_matches_a upper_closure_matchexpr rs). 
        ¬ has_disc_negated is_Src_Ports False (get_match r) ∧
        ¬ has_disc_negated is_Dst_Ports False (get_match r) ∧
        ¬ has_disc is_MultiportPorts (get_match r)"
      by blast
    with m transform_optimize_dnf_strict_structure(2,5)[OF optimize_matches_a_simple_ruleset[OF simplers] wf_in_doubt_allow, of upper_closure_matchexpr]
      show ?thesis by blast
    qed

    show"∀a. ¬ disc (Src_Ports a) ⟹ ∀a. ¬ disc (Dst_Ports a) ⟹ ∀a. ¬ disc (Src a) ⟹ ∀a. ¬ disc (Dst a) ⟹
         ∀a. ¬ disc (IIface a) ∨ disc = is_Iiface ⟹ ∀a. ¬ disc (OIface a) ∨ disc = is_Oiface ⟹
         (∀a. ¬ disc (Prot a)) ∨ disc = is_Prot ∧
         (∀ r ∈ set rs. ¬ has_disc_negated is_Src_Ports False (get_match r) ∧
                        ¬ has_disc_negated is_Dst_Ports False (get_match r) ∧
                        ¬ has_disc is_MultiportPorts (get_match r)) ⟹
         ∀ r ∈ set rs. ¬ has_disc_negated disc False (get_match r) ⟹
         ∀ r ∈ set (upper_closure rs). ¬ has_disc_negated disc False (get_match r)"
    using simplers
    unfolding upper_closure_def
    apply - 
    apply(frule(1) transform_remove_unknowns_upper(6)[where disc=disc])
    apply(drule transform_remove_unknowns_upper(2))
    apply(frule(1) transform_optimize_dnf_strict_structure(5)[OF _ wf_in_doubt_allow, where disc=disc])
    apply(frule transform_optimize_dnf_strict_structure(3)[OF _ wf_in_doubt_allow])
    apply(drule transform_optimize_dnf_strict_structure(1)[OF _ wf_in_doubt_allow])
    apply(frule(1) transform_normalize_primitives(7)[OF _ wf_in_doubt_allow, of _ disc])
        apply(simp;fail)
       apply blast
      apply(elim disjE)
       apply blast
      apply(simp)
      using no_ports_1 apply fast
     apply(simp;fail)
    apply(drule transform_normalize_primitives(2)[OF _ wf_in_doubt_allow], simp)
    apply(frule(1) transform_optimize_dnf_strict_structure(5)[OF _ wf_in_doubt_allow, where disc=disc])
    apply(simp add: remdups_rev_set)
    done

    show "(common_matcher, in_doubt_allow),p⊢ ⟨upper_closure rs, s⟩ ⇒⇩α t ⟷ (common_matcher, in_doubt_allow),p⊢ ⟨rs, s⟩ ⇒⇩α t"
    using simplers
    unfolding upper_closure_def
    apply -
    apply(frule transform_remove_unknowns_upper(1)[where p=p and s=s and t=t])
    apply(drule transform_remove_unknowns_upper(2))
    apply(frule transform_optimize_dnf_strict[OF _ wf_in_doubt_allow, where p=p and s=s and t=t])
    apply(frule transform_optimize_dnf_strict_structure(3)[OF _ wf_in_doubt_allow])
    apply(drule transform_optimize_dnf_strict_structure(1)[OF _ wf_in_doubt_allow])
    apply(frule(1) transform_normalize_primitives(1)[OF _ wf_in_doubt_allow, where p=p and s=s and t=t])
    apply(drule transform_normalize_primitives(2)[OF _ wf_in_doubt_allow], simp)
    apply(frule transform_optimize_dnf_strict[OF _ wf_in_doubt_allow, where p=p and s=s and t=t])
    apply(drule transform_optimize_dnf_strict_structure(1)[OF _ wf_in_doubt_allow])
    apply(simp)
    using approximating_bigstep_fun_remdups_rev
    by (simp add: approximating_bigstep_fun_remdups_rev approximating_semantics_iff_fun_good_ruleset remdups_rev_simplers simple_imp_good_ruleset) 
  qed


(*copy&paste from transform_upper_closure*)
lemma transform_lower_closure:
  assumes simplers: "simple_ruleset rs"
  ― ‹semantics are preserved›
  shows "(common_matcher, in_doubt_deny),p⊢ ⟨lower_closure rs, s⟩ ⇒⇩α t ⟷ (common_matcher, in_doubt_deny),p⊢ ⟨rs, s⟩ ⇒⇩α t"
  and "simple_ruleset (lower_closure rs)"
  ― ‹simple, normalized rules without unknowns›
  and "∀ r ∈ set (lower_closure rs). normalized_nnf_match (get_match r) ∧
                                     normalized_src_ports (get_match r) ∧
                                     normalized_dst_ports (get_match r) ∧
                                     normalized_src_ips (get_match r) ∧
                                     normalized_dst_ips (get_match r) ∧
                                     ¬ has_disc is_MultiportPorts (get_match r) ∧
                                     ¬ has_disc is_Extra (get_match r)"
  ― ‹no new primitives are introduced›
  and "∀a. ¬ disc (Src_Ports a) ⟹ ∀a. ¬ disc (Dst_Ports a) ⟹ ∀a. ¬ disc (Src a) ⟹ ∀a. ¬ disc (Dst a) ⟹
       ∀a. ¬ disc (IIface a) ∨ disc = is_Iiface ⟹ ∀a. ¬ disc (OIface a) ∨ disc = is_Oiface ⟹
       ∀a. ¬ disc (Prot a) ⟹
        ∀ r ∈ set rs. ¬ has_disc disc (get_match r) ⟹
        ∀ r ∈ set (lower_closure rs). ¬ has_disc disc (get_match r)"
  and "∀a. ¬ disc (Src_Ports a) ⟹ ∀a. ¬ disc (Dst_Ports a) ⟹ ∀a. ¬ disc (Src a) ⟹ ∀a. ¬ disc (Dst a) ⟹
       ∀a. ¬ disc (IIface a) ∨ disc = is_Iiface ⟹ ∀a. ¬ disc (OIface a) ∨ disc = is_Oiface ⟹
       (∀a. ¬ disc (Prot a)) ∨ disc = is_Prot ∧
       (∀ r ∈ set rs. ¬ has_disc_negated is_Src_Ports False (get_match r) ∧
                      ¬ has_disc_negated is_Dst_Ports False (get_match r) ∧
                      ¬ has_disc is_MultiportPorts (get_match r)) ⟹
       ∀ r ∈ set rs. ¬ has_disc_negated disc False (get_match r) ⟹
       ∀ r ∈ set (lower_closure rs). ¬ has_disc_negated disc False (get_match r)"
  proof -
    let ?rs1="optimize_matches_a lower_closure_matchexpr rs"
    let ?rs2="transform_optimize_dnf_strict ?rs1"
    let ?rs3="transform_normalize_primitives ?rs2"
    let ?rs4="transform_optimize_dnf_strict ?rs3"

    { fix m a
        have "Rule m a ∈ set (lower_closure rs) ⟹
            (a = action.Accept ∨ a = action.Drop) ∧
             normalized_nnf_match m ∧
             normalized_src_ports m ∧
             normalized_dst_ports m ∧
             normalized_src_ips m ∧
             normalized_dst_ips m ∧
             ¬ has_disc is_MultiportPorts m ∧
              ¬ has_disc is_Extra m"
        using simplers
        unfolding lower_closure_def
        apply(simp add: remdups_rev_set)
        apply(frule transform_remove_unknowns_lower(4))
        apply(drule transform_remove_unknowns_lower(2))
        thm transform_optimize_dnf_strict[OF _ wf_in_doubt_deny]
        apply(frule(1) transform_optimize_dnf_strict_structure(2)[OF _ wf_in_doubt_deny, where disc=is_Extra])
        apply(thin_tac "∀r∈ set (optimize_matches_a lower_closure_matchexpr rs). ¬ has_disc is_Extra (get_match r)")
        apply(frule transform_optimize_dnf_strict_structure(3)[OF _ wf_in_doubt_deny])
        apply(drule transform_optimize_dnf_strict_structure(1)[OF _ wf_in_doubt_deny])
        thm transform_normalize_primitives[OF _ wf_in_doubt_deny]
        apply(frule(1) transform_normalize_primitives(3)[OF _ wf_in_doubt_deny, of _ is_Extra])
            apply(simp;fail)
           apply(simp;fail)
          apply(simp;fail)
         apply blast
        apply(thin_tac "∀r∈ set ?rs2. ¬ has_disc is_Extra (get_match r)")
        apply(frule(1) transform_normalize_primitives(5)[OF _ wf_in_doubt_deny])
        apply(drule transform_normalize_primitives(2)[OF _ wf_in_doubt_deny], simp)
        thm transform_optimize_dnf_strict[OF _ wf_in_doubt_deny]
        apply(frule(1) transform_optimize_dnf_strict_structure(2)[OF _ wf_in_doubt_deny, where disc=is_Extra])
        apply(frule transform_optimize_dnf_strict_structure(2)[OF _ wf_in_doubt_deny, where disc=is_MultiportPorts])
         apply blast
        apply(frule transform_optimize_dnf_strict_structure(3)[OF _ wf_in_doubt_deny])
        apply(frule transform_optimize_dnf_strict_structure(4)[OF _ wf_in_doubt_deny, of _ "(is_Src_Ports, src_ports_sel)" "(λps. case ps of L4Ports _ pts ⇒ length pts ≤ 1)"])
         apply(simp add: normalized_src_ports_def2; fail)
        apply(frule transform_optimize_dnf_strict_structure(4)[OF _ wf_in_doubt_deny, of _ "(is_Dst_Ports, dst_ports_sel)" "(λps. case ps of L4Ports _ pts ⇒ length pts ≤ 1)"])
         apply(simp add: normalized_dst_ports_def2; fail)
        apply(frule transform_optimize_dnf_strict_structure(4)[OF _ wf_in_doubt_deny, of _ "(is_Src, src_sel)" normalized_cidr_ip])
         apply(simp add: normalized_src_ips_def2; fail)
        apply(frule transform_optimize_dnf_strict_structure(4)[OF _ wf_in_doubt_deny, of _ "(is_Dst, dst_sel)" normalized_cidr_ip])
         apply(simp add: normalized_dst_ips_def2; fail)
        apply(thin_tac "∀r∈set ?rs2. _ r")+
        apply(thin_tac "∀r∈set ?rs3. _ r")+
        apply(drule transform_optimize_dnf_strict_structure(1)[OF _ wf_in_doubt_deny])
        apply(subgoal_tac "(a = action.Accept ∨ a = action.Drop)")
         prefer 2
         apply(simp_all add: simple_ruleset_def)
         apply fastforce
        apply(simp add: normalized_src_ports_def2 normalized_dst_ports_def2 normalized_src_ips_def2 normalized_dst_ips_def2)
        apply(intro conjI)
               by fastforce+ (*1s*)
    } note 1=this

    from 1 show "simple_ruleset (lower_closure rs)"
      apply(simp add: simple_ruleset_def)
      apply(clarify)
      apply(rename_tac r)
      apply(case_tac r)
      apply(simp)
      by blast


    from 1 show "∀ r ∈ set (lower_closure rs). normalized_nnf_match (get_match r) ∧
         normalized_src_ports (get_match r) ∧
         normalized_dst_ports (get_match r) ∧
         normalized_src_ips (get_match r) ∧
         normalized_dst_ips (get_match r) ∧
         ¬ has_disc is_MultiportPorts (get_match r) ∧
         ¬ has_disc is_Extra (get_match r)"
      apply(clarify)
      apply(rename_tac r)
      apply(case_tac r)
      apply(simp)
      done
      

    show "∀a. ¬ disc (Src_Ports a) ⟹ ∀a. ¬ disc (Dst_Ports a) ⟹ ∀a. ¬ disc (Src a) ⟹ ∀a. ¬ disc (Dst a) ⟹
          ∀a. ¬ disc (IIface a) ∨ disc = is_Iiface ⟹ ∀a. ¬ disc (OIface a) ∨ disc = is_Oiface ⟹
          ∀a. ¬ disc (Prot a) ⟹
            ∀ r ∈ set rs. ¬ has_disc disc (get_match r) ⟹ ∀ r ∈ set (lower_closure rs). ¬ has_disc disc (get_match r)"
    using simplers
    unfolding lower_closure_def
    apply - 
    apply(frule(1) transform_remove_unknowns_lower(3)[where disc=disc])
    apply(drule transform_remove_unknowns_lower(2))
    apply(frule(1) transform_optimize_dnf_strict_structure(2)[OF _ wf_in_doubt_deny, where disc=disc])
    apply(frule transform_optimize_dnf_strict_structure(3)[OF _ wf_in_doubt_deny])
    apply(drule transform_optimize_dnf_strict_structure(1)[OF _ wf_in_doubt_deny])
    apply(frule(1) transform_normalize_primitives(3)[OF _ wf_in_doubt_deny, of _ disc])
        apply(simp;fail)
       apply blast
      apply(simp;fail)
     apply(simp;fail)
    apply(drule transform_normalize_primitives(2)[OF _ wf_in_doubt_deny], simp)
    apply(frule(1) transform_optimize_dnf_strict_structure(2)[OF _ wf_in_doubt_deny, where disc=disc])
    apply(simp add: remdups_rev_set)
    done

    have no_ports_1:
    "¬ has_disc_negated is_Src_Ports False (get_match m) ∧
     ¬ has_disc_negated is_Dst_Ports False (get_match m) ∧
     ¬ has_disc is_MultiportPorts (get_match m)"
    if no_ports: "∀r∈set rs.
      ¬ has_disc_negated is_Src_Ports False (get_match r) ∧
      ¬ has_disc_negated is_Dst_Ports False (get_match r) ∧
      ¬ has_disc is_MultiportPorts (get_match r)"
    and m: "m ∈ set (transform_optimize_dnf_strict (optimize_matches_a lower_closure_matchexpr rs))"
    for m
    proof -
      from no_ports transform_remove_unknowns_lower(3,6)[OF simplers] have
      "∀r∈ set (optimize_matches_a lower_closure_matchexpr rs). 
        ¬ has_disc_negated is_Src_Ports False (get_match r) ∧
        ¬ has_disc_negated is_Dst_Ports False (get_match r) ∧
        ¬ has_disc is_MultiportPorts (get_match r)"
      by blast
    from m this transform_optimize_dnf_strict_structure(2,5)[OF optimize_matches_a_simple_ruleset[OF simplers] wf_in_doubt_deny, of lower_closure_matchexpr]
      show ?thesis by blast
    qed

    show"∀a. ¬ disc (Src_Ports a) ⟹ ∀a. ¬ disc (Dst_Ports a) ⟹ ∀a. ¬ disc (Src a) ⟹ ∀a. ¬ disc (Dst a) ⟹
         ∀a. ¬ disc (IIface a) ∨ disc = is_Iiface ⟹ ∀a. ¬ disc (OIface a) ∨ disc = is_Oiface ⟹
         (∀a. ¬ disc (Prot a)) ∨ disc = is_Prot ∧
         (∀ r ∈ set rs. ¬ has_disc_negated is_Src_Ports False (get_match r) ∧
                        ¬ has_disc_negated is_Dst_Ports False (get_match r) ∧
                        ¬ has_disc is_MultiportPorts (get_match r)) ⟹
        ∀ r ∈ set rs. ¬ has_disc_negated disc False (get_match r) ⟹
        ∀ r ∈ set (lower_closure rs). ¬ has_disc_negated disc False (get_match r)"
    using simplers
    unfolding lower_closure_def
    apply - 
    apply(frule(1) transform_remove_unknowns_lower(6)[where disc=disc])
    apply(drule transform_remove_unknowns_lower(2))
    apply(frule(1) transform_optimize_dnf_strict_structure(5)[OF _ wf_in_doubt_deny, where disc=disc])
    apply(frule transform_optimize_dnf_strict_structure(3)[OF _ wf_in_doubt_deny])
    apply(drule transform_optimize_dnf_strict_structure(1)[OF _ wf_in_doubt_deny])
    apply(frule(1) transform_normalize_primitives(7)[OF _ wf_in_doubt_deny, of _ disc])
        apply(simp;fail)
       apply blast
      apply(elim disjE)
       apply blast
      apply(simp)
      using no_ports_1 apply fast
     apply(simp;fail)
    apply(drule transform_normalize_primitives(2)[OF _ wf_in_doubt_deny], simp)
    apply(frule(1) transform_optimize_dnf_strict_structure(5)[OF _ wf_in_doubt_deny, where disc=disc])
    apply(simp add: remdups_rev_set)
    done

    show "(common_matcher, in_doubt_deny),p⊢ ⟨lower_closure rs, s⟩ ⇒⇩α t ⟷ (common_matcher, in_doubt_deny),p⊢ ⟨rs, s⟩ ⇒⇩α t"
    using simplers
    unfolding lower_closure_def
    apply -
    apply(frule transform_remove_unknowns_lower(1)[where p=p and s=s and t=t])
    apply(drule transform_remove_unknowns_lower(2))
    apply(frule transform_optimize_dnf_strict[OF _ wf_in_doubt_deny, where p=p and s=s and t=t])
    apply(frule transform_optimize_dnf_strict_structure(3)[OF _ wf_in_doubt_deny])
    apply(drule transform_optimize_dnf_strict_structure(1)[OF _ wf_in_doubt_deny])
    apply(frule(1) transform_normalize_primitives(1)[OF _ wf_in_doubt_deny, where p=p and s=s and t=t])
    apply(drule transform_normalize_primitives(2)[OF _ wf_in_doubt_deny], simp)
    apply(frule transform_optimize_dnf_strict[OF _ wf_in_doubt_deny, where p=p and s=s and t=t])
    apply(drule transform_optimize_dnf_strict_structure(1)[OF _ wf_in_doubt_deny])
    apply(simp)
    using approximating_bigstep_fun_remdups_rev
    by (simp add: approximating_bigstep_fun_remdups_rev approximating_semantics_iff_fun_good_ruleset remdups_rev_simplers simple_imp_good_ruleset) 
  qed


definition iface_try_rewrite
  :: "(iface × ('i::len word × nat) list) list
   ⇒ 'i prefix_routing option
   ⇒ 'i common_primitive rule list
      ⇒ 'i common_primitive rule list"
where
  "iface_try_rewrite ipassmt rtblo rs ≡ 
  let o_rewrite = (case rtblo of None ⇒ id | Some rtbl ⇒ 
    transform_optimize_dnf_strict ∘ optimize_matches (oiface_rewrite (map_of_ipassmt (routing_ipassmt rtbl)))) in
  if ipassmt_sanity_disjoint (map_of ipassmt) ∧ ipassmt_sanity_defined rs (map_of ipassmt) then
  optimize_matches (iiface_rewrite (map_of_ipassmt ipassmt)) (o_rewrite rs)
  else
  optimize_matches (iiface_constrain (map_of_ipassmt ipassmt)) (o_rewrite rs)"

text‹Where @{typ "(iface × ('i::len word × nat) list) list"} is @{const map_of}@{typ "'i::len ipassignment"}. 
 The sanity checkers need to iterate over the interfaces, hence we don't pass a map but a list of tuples.›


text‹In @{file ‹Transform.thy›} there should be the final correctness theorem for ‹iface_try_rewrite›. 
     Here are some structural properties.›


lemma iface_try_rewrite_simplers: "simple_ruleset rs ⟹ simple_ruleset (iface_try_rewrite ipassmt rtblo rs)"
  by(simp add: iface_try_rewrite_def optimize_matches_simple_ruleset transform_optimize_dnf_strict_structure(1)[OF _ wf_in_doubt_allow 
     (* The wf_unknown_match_tac is only required for some other parts of that lemma group, so any wellfounded tactic will do. *)] Let_def split: option.splits)
    

lemma iiface_rewrite_preserves_nodisc:
  "∀a. ¬ disc (Src a) ⟹ ¬ has_disc disc m ⟹ ¬ has_disc disc (iiface_rewrite ipassmt m)"
  proof(induction ipassmt m rule: iiface_rewrite.induct)
  case 2 
    have "∀a. ¬ disc (Src a) ⟹ ¬ disc (IIface ifce) ⟹ ¬ has_disc disc (ipassmt_iface_replace_srcip_mexpr ipassmt ifce)"
      for ifce ipassmt
      apply(simp add: ipassmt_iface_replace_srcip_mexpr_def split: option.split)
      apply(intro allI impI, rename_tac ips)
      apply(drule_tac X=Src and ls="map (uncurry IpAddrNetmask) ips" in match_list_to_match_expr_not_has_disc)
      apply(simp)
      done
    with 2 show ?case by simp
  qed(simp_all)

lemma iiface_constrain_preserves_nodisc:
  "∀a. ¬ disc (Src a) ⟹ ¬ has_disc disc m ⟹ ¬ has_disc disc (iiface_constrain ipassmt m)"
  proof(induction ipassmt m rule: iiface_rewrite.induct)
  case 2 
    have "∀a. ¬ disc (Src a) ⟹ ¬ disc (IIface ifce) ⟹ ¬ has_disc disc (ipassmt_iface_constrain_srcip_mexpr ipassmt ifce)"
      for ifce ipassmt
      apply(simp add: ipassmt_iface_constrain_srcip_mexpr_def split: option.split)
      apply(intro allI impI, rename_tac ips)
      apply(drule_tac X=Src and ls="map (uncurry IpAddrNetmask) ips" in match_list_to_match_expr_not_has_disc)
      apply(simp)
      done
    with 2 show ?case by simp
  qed(simp_all)


lemma iface_try_rewrite_preserves_nodisc: "
      simple_ruleset rs ⟹
      ∀a. ¬ disc (Src a) ⟹ ∀a. ¬ disc (Dst a) ⟹ 
      ∀r∈ set rs. ¬ has_disc disc (get_match r) ⟹
        ∀r∈ set (iface_try_rewrite ipassmt rtblo rs). ¬ has_disc disc (get_match r)"   
  apply(insert wf_in_doubt_deny) (* to appease transform_optimize_dnf_strict_structure *)
  apply(simp add: iface_try_rewrite_def Let_def)
  apply(intro conjI impI optimize_matches_preserves)
  apply(case_tac[!] rtblo)
     apply(simp_all add: oiface_rewrite_preserves_nodisc iiface_rewrite_preserves_nodisc iiface_constrain_preserves_nodisc) (* solves the two None-cases *)
   apply(rule iiface_rewrite_preserves_nodisc; assumption?)
   apply(rule transform_optimize_dnf_strict_structure(2)[THEN bspec]; (assumption|simp add: optimize_matches_simple_ruleset; fail)?)
   apply(rule optimize_matches_preserves)
   apply(rule oiface_rewrite_preserves_nodisc; simp; fail)
  apply(rule iiface_constrain_preserves_nodisc; assumption?)
  apply(rule transform_optimize_dnf_strict_structure(2)[THEN bspec]; (assumption|simp add: optimize_matches_simple_ruleset; fail)?)
  apply(rule optimize_matches_preserves)
  apply(rule oiface_rewrite_preserves_nodisc; simp; fail)
done


theorem iface_try_rewrite_no_rtbl:
  assumes simplers: "simple_ruleset rs"
      and normalized: "∀ r ∈ set rs. normalized_nnf_match (get_match r)"
      and wf_ipassmt1: "ipassmt_sanity_nowildcards (map_of ipassmt)" and wf_ipassmt2: "distinct (map fst ipassmt)"
      and nospoofing: "∃ips. (map_of ipassmt) (Iface (p_iiface p)) = Some ips ∧ p_src p ∈ ipcidr_union_set (set ips)"
  shows "(common_matcher, α),p⊢ ⟨iface_try_rewrite ipassmt None rs, s⟩ ⇒⇩α t ⟷ (common_matcher, α),p⊢ ⟨rs, s⟩ ⇒⇩α t"
proof -
  show "(common_matcher, α),p⊢ ⟨iface_try_rewrite ipassmt None rs, s⟩ ⇒⇩α t ⟷ (common_matcher, α),p⊢ ⟨rs, s⟩ ⇒⇩α t"
    apply(simp add: iface_try_rewrite_def Let_def comp_def)
    apply(simp add: map_of_ipassmt_def wf_ipassmt1 wf_ipassmt2)
    apply(intro conjI impI)
     apply(elim conjE)
     using iiface_rewrite(1)[OF simplers normalized wf_ipassmt1 _ nospoofing] apply blast
    using iiface_constrain(1)[OF simplers normalized wf_ipassmt1, where p = p] nospoofing apply force
    done
qed

lemma optimize_matches_comp:
  assumes mono: "⋀m. matcheq_matchNone m ⟹ matcheq_matchNone (g m)"
  shows "optimize_matches (g ∘ f) rs = optimize_matches g ((optimize_matches f)  rs)"
unfolding optimize_matches_def
proof(induction rs)
  case (Cons r rs)
  obtain m a where [simp]: "r = Rule m a" by(cases r)
  show ?case 
  proof(cases "matcheq_matchNone (f m)")
    case True
    hence mn: "matcheq_matchNone (g (f m))" by(fact mono)
    show ?thesis by(unfold comp_def (* occasionally, the simplifier is weird *); simp add: mn Cons.IH[unfolded comp_def])
  next
    case False
    show ?thesis by(unfold comp_def; simp add: False Cons.IH[unfolded comp_def])
  qed
qed simp
(* optimize_matches_comp is a really nice lemma. 
The problem is that it is useless because I cannot execute the two rewrites after each other without going back to nnf.
*)
context begin

private lemma iiface_rewrite_monoNone: "matcheq_matchNone m ⟹ matcheq_matchNone (iiface_rewrite ipassmt m)"
  by(induction m rule: matcheq_matchNone.induct) auto
private lemma iiface_constrain_monoNone: "matcheq_matchNone m ⟹ matcheq_matchNone (iiface_constrain ipassmt m)"
  by(induction m rule: matcheq_matchNone.induct) auto

private lemmas optimize_matches_iiface_comp = optimize_matches_comp[OF iiface_rewrite_monoNone] 
                                      optimize_matches_comp[OF iiface_constrain_monoNone]
end

theorem iface_try_rewrite_rtbl:
  assumes simplers: "simple_ruleset rs"
      and normalized: "∀ r ∈ set rs. normalized_nnf_match (get_match r)"
      and wf_ipassmt: "ipassmt_sanity_nowildcards (map_of ipassmt)" "distinct (map fst ipassmt)"
      and nospoofing: "∃ips. (map_of ipassmt) (Iface (p_iiface p)) = Some ips ∧ p_src p ∈ ipcidr_union_set (set ips)"
      and routing_decided: "output_iface (routing_table_semantics rtbl (p_dst p)) = p_oiface p"
      and correct_routing: "correct_routing rtbl"
      and wf_ipassmt_o: "ipassmt_sanity_nowildcards (map_of (routing_ipassmt rtbl))"
      and wf_match_tac: "wf_unknown_match_tac α"
  shows "(common_matcher, α),p⊢ ⟨iface_try_rewrite ipassmt (Some rtbl) rs, s⟩ ⇒⇩α t ⟷ (common_matcher, α),p⊢ ⟨rs, s⟩ ⇒⇩α t"
proof -
  note oiface_rewrite = oiface_rewrite[OF simplers normalized wf_ipassmt_o refl correct_routing routing_decided]
  let ?ors = "optimize_matches (oiface_rewrite (map_of (routing_ipassmt rtbl))) rs"
  let ?nrs = "transform_optimize_dnf_strict ?ors"
  have osimplers: "simple_ruleset ?ors" using oiface_rewrite(2) .
  have nsimplers: "simple_ruleset ?nrs" using transform_optimize_dnf_strict_structure(1)[OF osimplers wf_match_tac] .
  have nnormalized: "∀ r ∈ set ?nrs. normalized_nnf_match (get_match r)" using transform_optimize_dnf_strict_structure(3)[OF osimplers wf_match_tac] .
  note nnf = transform_optimize_dnf_strict[OF osimplers wf_match_tac]
  have nospoofing_alt: "⋀ips. map_of ipassmt (Iface (p_iiface p)) = Some ips ⟹ p_src p ∈ ipcidr_union_set (set ips)" using nospoofing by simp
  show "(common_matcher, α),p⊢ ⟨iface_try_rewrite ipassmt (Some rtbl) rs, s⟩ ⇒⇩α t ⟷ (common_matcher, α),p⊢ ⟨rs, s⟩ ⇒⇩α t"
    apply(simp add: iface_try_rewrite_def Let_def)
    apply(simp add: map_of_ipassmt_def wf_ipassmt routing_ipassmt_distinct wf_ipassmt_o)
    apply(intro conjI impI; (elim conjE)?)
    subgoal using iiface_rewrite(1)[OF nsimplers nnormalized wf_ipassmt(1) _ nospoofing] oiface_rewrite(1) nnf by simp
    subgoal using iiface_constrain(1)[OF nsimplers nnormalized wf_ipassmt(1), where p = p] nospoofing_alt oiface_rewrite(1) nnf by simp
    done
qed

  

end