Theory Iptables_Semantics

theory Iptables_Semantics
imports Semantics_Embeddings "Semantics_Ternary/Normalized_Matches"
begin

section‹Normalizing Rulesets in the Boolean Big Step Semantics›
corollary normalize_rules_dnf_correct_BooleanSemantics: 
  assumes "good_ruleset rs"
  shows "Γ,γ,p⊢ ⟨normalize_rules_dnf rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
proof -
  from assms have assm': "good_ruleset (normalize_rules_dnf rs)" by (metis good_ruleset_normalize_rules_dnf) 
  from normalize_rules_dnf_correct assms good_imp_wf_ruleset have
    "∀β α. approximating_bigstep_fun (β,α) p (normalize_rules_dnf rs) s = approximating_bigstep_fun (β,α) p rs s" by fast
  hence 
    "∀α. approximating_bigstep_fun (β⇩m⇩a⇩g⇩i⇩c γ,α) p (normalize_rules_dnf rs) s = approximating_bigstep_fun (β⇩m⇩a⇩g⇩i⇩c γ,α) p rs s" by fast
  with β⇩m⇩a⇩g⇩i⇩c_approximating_bigstep_fun_iff_iptables_bigstep assms assm' show ?thesis
  by metis
qed

end