Theory Normalized_Matches

theory Normalized_Matches
imports Fixed_Action
begin

section‹Normalized (DNF) matches›

text‹simplify a match expression. The output is a list of match exprissions, the semantics is ‹∨› of the list elements.›
fun normalize_match :: "'a match_expr ⇒ 'a match_expr list" where
  "normalize_match (MatchAny) = [MatchAny]" |
  "normalize_match (Match m) = [Match m]" |
  "normalize_match (MatchAnd m1 m2) = [MatchAnd x y. x <- normalize_match m1, y <- normalize_match m2]" |
  "normalize_match (MatchNot (MatchAnd m1 m2)) = normalize_match (MatchNot m1) @ normalize_match (MatchNot m2)" | (*DeMorgan*)
  "normalize_match (MatchNot (MatchNot m)) = normalize_match m" | (*idem*)
  "normalize_match (MatchNot (MatchAny)) = []" | (*false*)
  "normalize_match (MatchNot (Match m)) = [MatchNot (Match m)]"


lemma normalize_match_not_matcheq_matchNone: "∀m' ∈ set (normalize_match m). ¬ matcheq_matchNone m'"
  proof(induction m rule: normalize_match.induct)
  case 4 thus ?case by (simp) blast
  qed(simp_all)
 
lemma normalize_match_empty_iff_matcheq_matchNone: "normalize_match m = [] ⟷ matcheq_matchNone m "
  proof(induction m rule: normalize_match.induct) 
  case 3 thus ?case  by (simp) fastforce
  qed(simp_all)

lemma match_list_normalize_match: "match_list γ [m] a p ⟷ match_list γ (normalize_match m) a p"
  proof(induction m rule:normalize_match.induct)
  case 1 thus ?case by(simp add: match_list_singleton)
  next
  case 2 thus ?case by(simp add: match_list_singleton)
  next
  case (3 m1 m2) thus ?case 
    apply(simp_all add: match_list_singleton del: match_list.simps(2))
    apply(case_tac "matches γ m1 a p")
     apply(rule matches_list_And_concat)
      apply(simp)
     apply(case_tac "(normalize_match m1)")
      apply simp
     apply (auto)[1]
    apply(simp add: bunch_of_lemmata_about_matches match_list_helper)
    done
  next
  case 4 thus ?case 
    apply(simp_all add: match_list_singleton del: match_list.simps(2))
    apply(simp add: match_list_append)
    apply(safe)
        apply(simp_all add: matches_DeMorgan)
    done
  next 
  case 5 thus ?case 
    by(simp add: match_list_singleton bunch_of_lemmata_about_matches)
  next
  case 6 thus ?case 
    by(simp add: match_list_singleton bunch_of_lemmata_about_matches)
  next
  case 7 thus ?case by(simp add: match_list_singleton)
qed
  
thm match_list_normalize_match[simplified match_list_singleton]


theorem normalize_match_correct: "approximating_bigstep_fun γ p (map (λm. Rule m a) (normalize_match m)) s = approximating_bigstep_fun γ p [Rule m a] s"
apply(rule match_list_semantics[of _ _ _ _ "[m]", simplified])
using match_list_normalize_match by fastforce


lemma normalize_match_empty: "normalize_match m = [] ⟹ ¬ matches γ m a p"
  proof(induction m rule: normalize_match.induct)
  case 3 thus ?case by(fastforce dest: matches_dest)
  next
  case 4 thus ?case using match_list_normalize_match by (simp add: matches_DeMorgan)
  next
  case 5 thus ?case using matches_not_idem by fastforce
  next
  case 6 thus ?case by(simp add: bunch_of_lemmata_about_matches)
  qed(simp_all)


lemma matches_to_match_list_normalize: "matches γ m a p = match_list γ (normalize_match m) a p"
  using match_list_normalize_match[simplified match_list_singleton] .

lemma wf_ruleset_normalize_match: "wf_ruleset γ p [(Rule m a)] ⟹ wf_ruleset γ p (map (λm. Rule m a) (normalize_match m))"
proof(induction m rule: normalize_match.induct)
  case 1 thus ?case by simp
  next
  case 2 thus ?case by simp
  next
  case 3 thus ?case by(simp add: fixedaction_wf_ruleset wf_ruleset_singleton matches_to_match_list_normalize)
  next
  case 4 thus ?case 
    apply(simp add: wf_ruleset_append)
    apply(simp add: fixedaction_wf_ruleset)
    apply(unfold wf_ruleset_singleton)
    apply(safe) (*there is a simpler way but the simplifier takes for ever if we just apply it here, ...*)
           apply(simp_all add: matches_to_match_list_normalize)
         apply(simp_all add: match_list_append)
    done
  next
  case 5 thus ?case by(simp add: wf_ruleset_singleton matches_to_match_list_normalize)
  next
  case 6 thus ?case by(simp add: wf_ruleset_def)
  next
  case 7 thus ?case by(simp_all add: wf_ruleset_append)
  qed


lemma normalize_match_wf_ruleset: "wf_ruleset γ p (map (λm. Rule m a) (normalize_match m)) ⟹ wf_ruleset γ p [Rule m a]"
proof(induction m rule: normalize_match.induct)
  case 1 thus ?case by simp
  next
  case 2 thus ?case by simp
  next
  case 3 thus ?case by(simp add: fixedaction_wf_ruleset wf_ruleset_singleton matches_to_match_list_normalize)
  next
  case 4 thus ?case 
    apply(simp add: wf_ruleset_append)
    apply(simp add: fixedaction_wf_ruleset)
    apply(unfold wf_ruleset_singleton)
    apply(safe)
         apply(simp_all add: matches_to_match_list_normalize)
         apply(simp_all add: match_list_append)
    done
  next
  case 5 thus ?case 
    unfolding wf_ruleset_singleton by(simp add: matches_to_match_list_normalize)
  next
  case 6 thus ?case unfolding wf_ruleset_singleton by(simp add: bunch_of_lemmata_about_matches)
  next
  case 7 thus ?case by(simp add: wf_ruleset_append)
  qed


lemma good_ruleset_normalize_match: "good_ruleset [(Rule m a)] ⟹ good_ruleset (map (λm. Rule m a) (normalize_match m))"
by(simp add: good_ruleset_def)

section‹Normalizing rules instead of only match expressions›
  fun normalize_rules :: "('a match_expr ⇒ 'a match_expr list) ⇒ 'a rule list ⇒ 'a rule list" where
    "normalize_rules _ [] = []" |
    "normalize_rules f ((Rule m a)#rs) = (map (λm. Rule m a) (f m))@(normalize_rules f rs)"
  
  lemma normalize_rules_singleton: "normalize_rules f [Rule m a] = map (λm. Rule m a) (f m)" by(simp)
  lemma normalize_rules_fst: "(normalize_rules f (r # rs)) = (normalize_rules f [r]) @ (normalize_rules f rs)"
    by(cases r) (simp)

  lemma normalize_rules_concat_map:
    "normalize_rules f rs = concat (map (λr. map (λm. Rule m (get_action r)) (f (get_match r))) rs)"
    apply(induction rs)
     apply(simp_all)
    apply(rename_tac r rs, case_tac r)
    apply(simp)
    done

  lemma good_ruleset_normalize_rules: "good_ruleset rs ⟹ good_ruleset (normalize_rules f rs)"
    proof(induction rs)
    case Nil thus ?case by (simp)
    next
    case(Cons r rs)
      from Cons have IH: "good_ruleset (normalize_rules f rs)" using good_ruleset_tail by blast
      from Cons.prems have "good_ruleset [r]" using good_ruleset_fst by fast
      hence "good_ruleset (normalize_rules f [r])" by(cases r) (simp add: good_ruleset_alt)
      with IH good_ruleset_append have "good_ruleset (normalize_rules f [r] @ normalize_rules f rs)" by blast
      thus ?case using normalize_rules_fst by metis
    qed

  lemma simple_ruleset_normalize_rules: "simple_ruleset rs ⟹ simple_ruleset (normalize_rules f rs)"
    proof(induction rs)
    case Nil thus ?case by (simp)
    next
    case(Cons r rs)
      from Cons have IH: "simple_ruleset (normalize_rules f rs)" using simple_ruleset_tail by blast
      from Cons.prems have "simple_ruleset [r]" using simple_ruleset_append by fastforce
      hence "simple_ruleset (normalize_rules f [r])" by(cases r) (simp add: simple_ruleset_def) 
      with IH simple_ruleset_append have  "simple_ruleset (normalize_rules f [r] @ normalize_rules f rs)" by blast
      thus ?case using normalize_rules_fst by metis
    qed
    

  (*tuned version of the next lemma for usage with normalize_primitive_extract where P=normalized_nnf_match*)
  lemma normalize_rules_match_list_semantics_3: 
    assumes "∀m a. P m ⟶ match_list γ (f m) a p = matches γ m a p"
    and "simple_ruleset rs"
    and P: "∀ r ∈ set rs. P (get_match r)"
    shows "approximating_bigstep_fun γ p (normalize_rules f rs) s = approximating_bigstep_fun γ p rs s"
    proof -
      have assm_1: "∀r∈set rs. match_list γ (f (get_match r)) (get_action r) p = matches γ (get_match r) (get_action r) p" using P assms(1) by blast
      { fix r s
        assume "r ∈ set rs"
        with assm_1 have "match_list γ (f (get_match r)) (get_action r) p ⟷ match_list γ [(get_match r)] (get_action r) p" by simp
        with match_list_semantics[of γ "f (get_match r)" "(get_action r)" p "[(get_match r)]"] have
          "approximating_bigstep_fun γ p (map (λm. Rule m (get_action r)) (f (get_match r))) s = 
           approximating_bigstep_fun γ p [Rule (get_match r) (get_action r)] s" by simp
        hence "(approximating_bigstep_fun γ p (normalize_rules f [r]) s) = approximating_bigstep_fun γ p [r] s"
          by(cases r) (simp)
      }
  
    with assms show ?thesis
      proof(induction rs arbitrary: s)
        case Nil thus ?case by (simp)
      next
        case (Cons r rs)
        from Cons.prems have "simple_ruleset [r]" by(simp add: simple_ruleset_def)
        with simple_imp_good_ruleset good_imp_wf_ruleset have wf_r: "wf_ruleset γ p [r]" by fast
  
        from ‹simple_ruleset [r]› simple_imp_good_ruleset good_imp_wf_ruleset have wf_r: 
          "wf_ruleset γ p [r]" by fast
        from simple_ruleset_normalize_rules[OF ‹simple_ruleset [r]›] have "simple_ruleset (normalize_rules f [r])"
          by(simp) 
        with simple_imp_good_ruleset good_imp_wf_ruleset have wf_nr: "wf_ruleset γ p (normalize_rules f [r])" by fast
  
        from Cons have IH: "⋀s. approximating_bigstep_fun γ p (normalize_rules f rs) s = approximating_bigstep_fun γ p rs s"
          using simple_ruleset_tail by force
        
        from Cons have a: "⋀s. approximating_bigstep_fun γ p (normalize_rules f [r]) s = approximating_bigstep_fun γ p [r] s" by simp

        show ?case
          apply(subst normalize_rules_fst)
          apply(simp add: approximating_bigstep_fun_seq_wf[OF wf_nr])
          apply(subst approximating_bigstep_fun_seq_wf[OF wf_r, simplified])
          apply(simp add: a)
          apply(simp add: IH)  
          done
      qed
    qed

 corollary normalize_rules_match_list_semantics: 
  "(∀m a. match_list γ (f m) a p = matches γ m a p) ⟹ simple_ruleset rs ⟹
   approximating_bigstep_fun γ p (normalize_rules f rs) s = approximating_bigstep_fun γ p rs s"
  by(rule normalize_rules_match_list_semantics_3[where P="λ_. True"]) simp_all

lemma in_normalized_matches: "ls ∈ set (normalize_match m) ∧ matches γ ls a p ⟹ matches γ m a p"
  by (meson match_list_matches matches_to_match_list_normalize)

 text‹applying a function (with a prerequisite ‹Q›) to all rules›
 lemma normalize_rules_property:
 assumes "∀ r ∈ set rs. P (get_match r)"
     and "∀m. P m ⟶ (∀m' ∈ set (f m). Q m')"
  shows "∀r ∈ set (normalize_rules f rs). Q (get_match r)"
  proof
    fix r' assume a: "r' ∈ set (normalize_rules f rs)"
    from a assms show "Q (get_match r')"
    proof(induction rs)
    case Nil thus ?case by simp
    next
    case (Cons r rs)
      { 
        assume "r' ∈ set (normalize_rules f rs)"
        from Cons.IH this have "Q (get_match r')" using Cons.prems(2) Cons.prems(3) by fastforce
      } note 1=this
      { 
        assume "r' ∈ set (normalize_rules f [r])"
        hence a: "(get_match r') ∈ set (f (get_match r))" by(cases r) (auto)
        with Cons.prems(2) Cons.prems(3) have "∀m'∈set (f (get_match r)). Q m'" by auto
        with a have "Q (get_match r')" by blast
      } note 2=this
      from Cons.prems(1) have "r' ∈ set (normalize_rules f [r]) ∨ r' ∈ set (normalize_rules f rs)"
        by(subst(asm) normalize_rules_fst) auto
      with 1 2 show ?case
        by(elim disjE)(simp)
    qed
 qed

 text‹If a function ‹f› preserves some property of the match expressions, then this property is preserved when applying @{const normalize_rules}›

 lemma normalize_rules_preserves: assumes "∀ r ∈ set rs. P (get_match r)"
     and "∀m. P m ⟶ (∀m' ∈ set (f m). P m')"
  shows "∀r ∈ set (normalize_rules f rs). P (get_match r)"
  using normalize_rules_property[OF assms(1) assms(2)] by simp

fun normalize_rules_dnf :: "'a rule list ⇒ 'a rule list" where
  "normalize_rules_dnf [] = []" |
  "normalize_rules_dnf ((Rule m a)#rs) = (map (λm. Rule m a) (normalize_match m))@(normalize_rules_dnf rs)"

lemma normalize_rules_dnf_append: "normalize_rules_dnf (rs1@rs2) = normalize_rules_dnf rs1 @ normalize_rules_dnf rs2"
  proof(induction rs1 rule: normalize_rules_dnf.induct)
  qed(simp_all)

lemma normalize_rules_dnf_def2: "normalize_rules_dnf = normalize_rules normalize_match"
  proof(simp add: fun_eq_iff, intro allI)
    fix x::"'a rule list" show "normalize_rules_dnf x = normalize_rules normalize_match x"
    proof(induction x)
    case (Cons r rs) thus ?case by (cases r) simp
    qed(simp)
  qed

lemma wf_ruleset_normalize_rules_dnf: "wf_ruleset γ p rs ⟹ wf_ruleset γ p (normalize_rules_dnf rs)"
  proof(induction rs)
  case Nil thus ?case by simp
  next
  case(Cons r rs)
    from Cons have IH: "wf_ruleset γ p (normalize_rules_dnf rs)" by(auto dest: wf_rulesetD) 
    from Cons.prems have "wf_ruleset γ p [r]" by(auto dest: wf_rulesetD) 
    hence "wf_ruleset γ p (normalize_rules_dnf [r])" using wf_ruleset_normalize_match by(cases r) simp
    with IH wf_ruleset_append have "wf_ruleset γ p (normalize_rules_dnf [r] @ normalize_rules_dnf rs)" by fast
    thus ?case using normalize_rules_dnf_def2 normalize_rules_fst by metis
  qed

lemma good_ruleset_normalize_rules_dnf: "good_ruleset rs ⟹ good_ruleset (normalize_rules_dnf rs)"
  using normalize_rules_dnf_def2 good_ruleset_normalize_rules by metis

lemma simple_ruleset_normalize_rules_dnf: "simple_ruleset rs ⟹ simple_ruleset (normalize_rules_dnf rs)"
  using normalize_rules_dnf_def2 simple_ruleset_normalize_rules by metis


(*This is the simple correctness proof, using the generalized version.
  below, we have a more complex correctness proof with a slighter generic assumption.
  Probably, we can delete the complex proof when we only focus on simple rulesets
  *)
lemma "simple_ruleset rs ⟹ 
  approximating_bigstep_fun γ p (normalize_rules_dnf rs) s = approximating_bigstep_fun γ p rs s"
  unfolding normalize_rules_dnf_def2
  apply(rule normalize_rules_match_list_semantics)
   apply (metis matches_to_match_list_normalize)
  by simp
  
lemma normalize_rules_dnf_correct: "wf_ruleset γ p rs ⟹ 
  approximating_bigstep_fun γ p (normalize_rules_dnf rs) s = approximating_bigstep_fun γ p rs s"
  proof(induction rs)
  case Nil thus ?case by simp
  next
  case (Cons r rs)
    show ?case
    proof(induction s rule: just_show_all_approximating_bigstep_fun_equalities_with_start_Undecided)
    case Undecided
    from Cons wf_rulesetD(2) have IH: "approximating_bigstep_fun γ p (normalize_rules_dnf rs) s = approximating_bigstep_fun γ p rs s" by fast
    from Cons.prems have "wf_ruleset γ p [r]" and "wf_ruleset γ p (normalize_rules_dnf [r])"
      by(auto dest: wf_rulesetD simp: wf_ruleset_normalize_rules_dnf)
    with IH Undecided have
      "approximating_bigstep_fun γ p (normalize_rules_dnf rs) (approximating_bigstep_fun γ p (normalize_rules_dnf [r]) Undecided) = approximating_bigstep_fun γ p (r # rs) Undecided"
      apply(cases r, rename_tac m a)
      apply(simp)
      apply(case_tac a)
              apply(simp_all add: normalize_match_correct Decision_approximating_bigstep_fun wf_ruleset_singleton)
      done
    hence "approximating_bigstep_fun γ p (normalize_rules_dnf [r] @ normalize_rules_dnf rs) s = approximating_bigstep_fun γ p (r # rs) s"
      using Undecided ‹wf_ruleset γ p [r]› ‹wf_ruleset γ p (normalize_rules_dnf [r])› 
      by(simp add: approximating_bigstep_fun_seq_wf)
    thus ?thesis using normalize_rules_fst normalize_rules_dnf_def2 by metis
    qed
  qed


fun normalized_nnf_match :: "'a match_expr ⇒ bool" where
  "normalized_nnf_match MatchAny = True" |
  "normalized_nnf_match (Match _ ) = True" |
  "normalized_nnf_match (MatchNot (Match _)) = True" |
  "normalized_nnf_match (MatchAnd m1 m2) = ((normalized_nnf_match m1) ∧ (normalized_nnf_match m2))" |
  "normalized_nnf_match _ = False"


text‹Essentially, @{term normalized_nnf_match} checks for a negation normal form: Only AND is at toplevel, negation only occurs in front of literals.
 Since @{typ "'a match_expr"} does not support OR, the result is in conjunction normal form.
 Applying @{const normalize_match}, the reuslt is a list. Essentially, this is the disjunctive normal form.›

lemma normalize_match_already_normalized: "normalized_nnf_match m ⟹ normalize_match m = [m]"
  by(induction m rule: normalize_match.induct) (simp)+

lemma normalized_nnf_match_normalize_match: "∀ m' ∈ set (normalize_match m). normalized_nnf_match m'"
  proof(induction m arbitrary: rule: normalize_match.induct)
  case 4 thus ?case by fastforce
  qed (simp_all)


lemma normalized_nnf_match_MatchNot_D: "normalized_nnf_match (MatchNot m) ⟹ normalized_nnf_match m"
  by(induction m) (simp_all)


text‹Example›
lemma "normalize_match (MatchNot (MatchAnd (Match ip_src) (Match tcp))) = [MatchNot (Match ip_src), MatchNot (Match tcp)]" by simp



subsection‹Functions which preserve @{const normalized_nnf_match}›

lemma optimize_matches_option_normalized_nnf_match: "(⋀ r. r ∈ set rs ⟹ normalized_nnf_match (get_match r)) ⟹
     (⋀m m'. normalized_nnf_match m ⟹ f m = Some m' ⟹ normalized_nnf_match m') ⟹
      ∀ r ∈ set (optimize_matches_option f rs). normalized_nnf_match (get_match r)"
    proof(induction rs)
      case Nil thus ?case by simp
    next
      case (Cons r rs)
      from Cons.IH Cons.prems have IH: "∀r∈set (optimize_matches_option f rs). normalized_nnf_match (get_match r)" by simp
      from Cons.prems have "∀r∈set (optimize_matches_option f [r]). normalized_nnf_match (get_match r)"
        apply(cases r)
        apply(simp split: option.split)
        by force (*1s*)
      with IH show ?case by(cases r, simp split: option.split_asm)
    qed



lemma optimize_matches_normalized_nnf_match: "⟦∀ r ∈ set rs. normalized_nnf_match (get_match r); ∀m. normalized_nnf_match m ⟶ normalized_nnf_match (f m) ⟧ ⟹
      ∀ r ∈ set (optimize_matches f rs). normalized_nnf_match (get_match r)"
  unfolding optimize_matches_def
  apply(rule optimize_matches_option_normalized_nnf_match)
   apply(simp; fail)
  apply(simp split: if_split_asm)
  by blast


lemma normalize_rules_dnf_normalized_nnf_match: "∀x ∈ set (normalize_rules_dnf rs). normalized_nnf_match (get_match x)"
  proof(induction rs)
  case Nil thus ?case by simp
  next
  case (Cons r rs) thus ?case using normalized_nnf_match_normalize_match by(cases r) fastforce
  qed

end