Theory Negation_Type_Matching

theory Negation_Type_Matching
imports  "../Common/Negation_Type" Matching_Ternary "../Datatype_Selectors" Normalized_Matches
begin

section‹Negation Type Matching›


text‹Transform a @{typ "'a negation_type list"} to a @{typ "'a match_expr"} via conjunction.›
fun alist_and :: "'a negation_type list ⇒ 'a match_expr" where
  "alist_and [] = MatchAny" |
  "alist_and ((Pos e)#es) = MatchAnd (Match e) (alist_and es)" |
  "alist_and ((Neg e)#es) = MatchAnd (MatchNot (Match e)) (alist_and es)"

lemma normalized_nnf_match_alist_and: "normalized_nnf_match (alist_and as)"
  by(induction as rule: alist_and.induct) simp_all

lemma alist_and_append: "matches γ (alist_and (l1 @ l2)) a p ⟷ matches γ  (MatchAnd (alist_and l1)  (alist_and l2)) a p"
  proof(induction l1)
  case Nil thus ?case by (simp add: bunch_of_lemmata_about_matches)
  next
  case (Cons l l1) thus ?case by (cases l) (simp_all add: bunch_of_lemmata_about_matches)
  qed

  text‹This version of @{const alist_and} avoids the trailing @{const MatchAny}. Only intended for code.›
  fun alist_and' :: "'a negation_type list ⇒ 'a match_expr" where
    "alist_and' [] = MatchAny" |
    "alist_and' [Pos e] = Match e" |
    "alist_and' [Neg e] = MatchNot (Match e)"|
    "alist_and' ((Pos e)#es) = MatchAnd (Match e) (alist_and' es)" |
    "alist_and' ((Neg e)#es) = MatchAnd (MatchNot (Match e)) (alist_and' es)"

  lemma alist_and': "matches (γ, α) (alist_and' as) = matches (γ, α) (alist_and as)"
    by(induction as rule: alist_and'.induct) (simp_all add: bunch_of_lemmata_about_matches)
 
  lemma normalized_nnf_match_alist_and': "normalized_nnf_match (alist_and' as)"
    by(induction as rule: alist_and'.induct) simp_all

  lemma matches_alist_and_alist_and':
    "matches γ (alist_and' ls) a p ⟷ matches γ (alist_and ls) a p"
    apply(induction ls rule: alist_and'.induct)
    by(simp add: bunch_of_lemmata_about_matches)+

  lemma alist_and'_append: "matches γ (alist_and' (l1 @ l2)) a p ⟷ matches γ (MatchAnd (alist_and' l1) (alist_and' l2)) a p"
    proof(induction l1)
    case Nil thus ?case by (simp add: bunch_of_lemmata_about_matches)
    next
    case (Cons l l1) thus ?case
      apply (cases l)
       by(simp_all add: matches_alist_and_alist_and' bunch_of_lemmata_about_matches)
    qed

lemma alist_and_NegPos_map_getNeg_getPos_matches: 
  "(∀m∈set (getNeg spts). matches γ (MatchNot (Match (C m))) a p) ∧
   (∀m∈set (getPos spts). matches γ (Match (C m)) a p)
    ⟷
    matches γ (alist_and (NegPos_map C spts)) a p"
  proof(induction spts rule: alist_and.induct)
  qed(auto simp add: bunch_of_lemmata_about_matches)


fun negation_type_to_match_expr_f :: "('a ⇒ 'b) ⇒ 'a negation_type ⇒ 'b match_expr" where
  "negation_type_to_match_expr_f f (Pos a) = Match (f a)" |
  "negation_type_to_match_expr_f f (Neg a) = MatchNot (Match (f a))"

lemma alist_and_negation_type_to_match_expr_f_matches:
    "matches γ (alist_and (NegPos_map C spts)) a p ⟷
        (∀m∈set spts. matches γ (negation_type_to_match_expr_f C m) a p)"
  proof(induction spts rule: alist_and.induct)
  qed(auto simp add: bunch_of_lemmata_about_matches)

definition negation_type_to_match_expr :: "'a negation_type ⇒ 'a match_expr" where
  "negation_type_to_match_expr m ≡ negation_type_to_match_expr_f id m"

lemma negation_type_to_match_expr_simps:
  "negation_type_to_match_expr (Pos e) = (Match e)"
  "negation_type_to_match_expr (Neg e) = (MatchNot (Match e))"
by(simp_all add: negation_type_to_match_expr_def)

lemma alist_and_negation_type_to_match_expr: "alist_and (n#es) =  MatchAnd (negation_type_to_match_expr n) (alist_and es)"
  by(cases n, simp_all add: negation_type_to_match_expr_simps)


fun to_negation_type_nnf :: "'a match_expr ⇒ 'a negation_type list" where
 "to_negation_type_nnf MatchAny = []" |
 "to_negation_type_nnf (Match a) = [Pos a]" |
 "to_negation_type_nnf (MatchNot (Match a)) = [Neg a]" |
 "to_negation_type_nnf (MatchAnd a b) = (to_negation_type_nnf a) @ (to_negation_type_nnf b)" |
 "to_negation_type_nnf _ = undefined"


lemma "normalized_nnf_match m ⟹ matches γ (alist_and (to_negation_type_nnf m)) a p  = matches γ m a p"
  proof(induction m rule: to_negation_type_nnf.induct)
  qed(simp_all add: bunch_of_lemmata_about_matches alist_and_append)


text‹Isolating the matching semantics›
fun nt_match_list :: "('a, 'packet) match_tac ⇒ action ⇒ 'packet ⇒ 'a negation_type list ⇒ bool" where
  "nt_match_list _ _ _ [] = True" |
  "nt_match_list γ a p ((Pos x)#xs) ⟷ matches γ (Match x) a p ∧ nt_match_list γ a p xs" |
  "nt_match_list γ a p ((Neg x)#xs) ⟷ matches γ (MatchNot (Match x)) a p ∧ nt_match_list γ a p xs"

lemma nt_match_list_matches: "nt_match_list γ a p l ⟷ matches γ (alist_and l) a p"
  apply(induction l rule: alist_and.induct)
    apply(case_tac [!] γ)
    apply(simp_all add: bunch_of_lemmata_about_matches)
  done


lemma nt_match_list_simp: "nt_match_list γ a p ms ⟷ 
      (∀m ∈ set (getPos ms). matches γ (Match m) a p) ∧ (∀m ∈ set (getNeg ms). matches γ (MatchNot (Match m)) a p)"
  proof(induction γ a p ms rule: nt_match_list.induct)
  case 3 thus ?case by fastforce
  qed(simp_all)

lemma matches_alist_and: "matches γ (alist_and l) a p ⟷ (∀m ∈ set (getPos l). matches γ (Match m) a p) ∧ (∀m ∈ set (getNeg l). matches γ (MatchNot (Match m)) a p)"
  using nt_match_list_matches nt_match_list_simp by fast




end