Theory Matching_Embeddings

theory Matching_Embeddings
imports "Semantics_Ternary/Matching_Ternary" Matching "Semantics_Ternary/Unknown_Match_Tacs"
begin

section‹Boolean Matching vs. Ternary Matching›

term Semantics.matches
term Matching_Ternary.matches
(*'a is the primitive match condition, e.g. IpSrc …*)


text‹The two matching semantics are related. However, due to the ternary logic, we cannot directly translate one to the other.
The problem are @{const MatchNot} expressions which evaluate to @{const TernaryUnknown} because ‹MatchNot TernaryUnknown› and
‹TernaryUnknown› are semantically equal!›
lemma "∃m β α a. Matching_Ternary.matches (β, α) m a p ≠ 
  Semantics.matches (λ atm p. case β atm p of TernaryTrue ⇒ True | TernaryFalse ⇒ False | TernaryUnknown ⇒ α a p) m p"
apply(rule_tac x="MatchNot (Match X)" in exI) ― ‹any @{term "X::'a"}›
by (auto split: ternaryvalue.split ternaryvalue.split_asm simp add: matches_case_ternaryvalue_tuple)

text‹the @{const the} in the next definition is always defined›
lemma "∀m ∈ {m. approx m p ≠ TernaryUnknown}. ternary_to_bool (approx m p) ≠ None"
  by(simp add: ternary_to_bool_None)


text‹
The Boolean and the ternary matcher agree (where the ternary matcher is defined)
›
definition matcher_agree_on_exact_matches :: "('a, 'p) matcher ⇒ ('a ⇒ 'p ⇒ ternaryvalue) ⇒ bool" where
  "matcher_agree_on_exact_matches exact approx ≡ ∀p m. approx m p ≠ TernaryUnknown ⟶ exact m p = the (ternary_to_bool (approx m p))"

text‹We say the Boolean and ternary matchers agree iff they return the same result or the ternary matcher returns @{const TernaryUnknown}.›
lemma "matcher_agree_on_exact_matches exact approx ⟷ (∀p m. exact m p = the (ternary_to_bool (approx m p)) ∨ approx m p = TernaryUnknown)"
  unfolding matcher_agree_on_exact_matches_def by blast
lemma matcher_agree_on_exact_matches_alt: (*no `the`*)
  "matcher_agree_on_exact_matches exact approx ⟷ (∀p m. approx m p ≠ TernaryUnknown ⟶ bool_to_ternary (exact m p) = approx m p)"
  unfolding matcher_agree_on_exact_matches_def
  by (metis (full_types) bool_to_ternary.simps(1) bool_to_ternary.simps(2) option.sel ternary_to_bool.simps(1)
                         ternary_to_bool.simps(2) ternaryvalue.exhaust)

lemma eval_ternary_Not_TrueD: "eval_ternary_Not m = TernaryTrue ⟹ m = TernaryFalse"
  by (metis eval_ternary_Not.simps(1) eval_ternary_idempotence_Not)


lemma matches_comply_exact: "ternary_ternary_eval (map_match_tac β p m) ≠ TernaryUnknown ⟹
       matcher_agree_on_exact_matches γ β ⟹
        Semantics.matches γ m p = Matching_Ternary.matches (β, α) m a p"
  proof(unfold matches_case_ternaryvalue_tuple,induction m)
  case Match thus ?case
       by(simp split: ternaryvalue.split add: matcher_agree_on_exact_matches_def)
  next
  case (MatchNot m) thus ?case
      apply(simp split: ternaryvalue.split add: matcher_agree_on_exact_matches_def)
      apply(case_tac "ternary_ternary_eval (map_match_tac β p m)")
        by(simp_all)
  next
  case (MatchAnd m1 m2)
    thus ?case
     apply(case_tac "ternary_ternary_eval (map_match_tac β p m1)")
       apply(case_tac [!] "ternary_ternary_eval (map_match_tac β p m2)")
                by(simp_all)
  next
  case MatchAny thus ?case by simp
  qed


lemma matcher_agree_on_exact_matches_gammaE:
  "matcher_agree_on_exact_matches γ β ⟹ β X p = TernaryTrue ⟹ γ X p"
  apply(simp add: matcher_agree_on_exact_matches_alt)
  apply(erule_tac x=p in allE)
  apply(erule_tac x=X in allE)
  apply(simp add: bool_to_ternary_simps)
  done




lemma in_doubt_allow_allows_Accept: "a = Accept ⟹ matcher_agree_on_exact_matches γ β ⟹
        Semantics.matches γ m p ⟹ Matching_Ternary.matches (β, in_doubt_allow) m a p"
  apply(case_tac "ternary_ternary_eval (map_match_tac β p m) ≠ TernaryUnknown")
   using matches_comply_exact apply fast
  apply(simp add: matches_case_ternaryvalue_tuple)
  done

lemma not_exact_match_in_doubt_allow_approx_match: "matcher_agree_on_exact_matches γ β ⟹ a = Accept ∨ a = Reject ∨ a = Drop ⟹
  ¬ Semantics.matches γ m p ⟹ 
  (a = Accept ∧ Matching_Ternary.matches (β, in_doubt_allow) m a p) ∨ ¬ Matching_Ternary.matches (β, in_doubt_allow) m a p"
  apply(case_tac "ternary_ternary_eval (map_match_tac β p m) ≠ TernaryUnknown")
   apply(drule(1) matches_comply_exact[where α=in_doubt_allow and a=a])
   apply(rule disjI2)
   apply fast
  apply(simp)
  apply(clarify)
  apply(simp add: matches_case_ternaryvalue_tuple)
  apply(cases a)
         apply(simp_all)
  done




lemma in_doubt_deny_denies_DropReject: "a = Drop ∨ a = Reject ⟹ matcher_agree_on_exact_matches γ β ⟹
        Semantics.matches γ m p ⟹ Matching_Ternary.matches (β, in_doubt_deny) m a p"
  apply(case_tac "ternary_ternary_eval (map_match_tac β p m) ≠ TernaryUnknown")
   using matches_comply_exact apply fast
   apply(simp)
  apply(auto simp add: matches_case_ternaryvalue_tuple)
  done

lemma not_exact_match_in_doubt_deny_approx_match: "matcher_agree_on_exact_matches γ β ⟹ a = Accept ∨ a = Reject ∨ a = Drop ⟹
  ¬ Semantics.matches γ m p ⟹ 
  ((a = Drop ∨ a = Reject) ∧ Matching_Ternary.matches (β, in_doubt_deny) m a p) ∨ ¬ Matching_Ternary.matches (β, in_doubt_deny) m a p"
  apply(case_tac "ternary_ternary_eval (map_match_tac β p m) ≠ TernaryUnknown")
   apply(drule(1) matches_comply_exact[where α=in_doubt_deny and a=a])
   apply(rule disjI2)
   apply fast
  apply(simp)
  apply(clarify)
  apply(simp add: matches_case_ternaryvalue_tuple)
  apply(cases a)
         apply(simp_all)
  done

text‹The ternary primitive matcher can return exactly the result of the Boolean primitive matcher›
definition β⇩m⇩a⇩g⇩i⇩c :: "('a, 'p) matcher ⇒ ('a ⇒ 'p ⇒ ternaryvalue)" where
  "β⇩m⇩a⇩g⇩i⇩c γ ≡ (λ a p. if γ a p then TernaryTrue else TernaryFalse)"

lemma "matcher_agree_on_exact_matches γ (β⇩m⇩a⇩g⇩i⇩c γ)"
  by(simp add: matcher_agree_on_exact_matches_def β⇩m⇩a⇩g⇩i⇩c_def)

lemma β⇩m⇩a⇩g⇩i⇩c_not_Unknown: "ternary_ternary_eval (map_match_tac (β⇩m⇩a⇩g⇩i⇩c γ) p m) ≠ TernaryUnknown"
  proof(induction m)
  case MatchNot thus ?case using eval_ternary_Not_UnknownD β⇩m⇩a⇩g⇩i⇩c_def
     by (simp) blast
  case (MatchAnd m1 m2) thus ?case
    apply(case_tac "ternary_ternary_eval (map_match_tac (β⇩m⇩a⇩g⇩i⇩c γ) p m1)")
      apply(case_tac [!] "ternary_ternary_eval (map_match_tac (β⇩m⇩a⇩g⇩i⇩c γ) p m2)")
            by(simp_all add: β⇩m⇩a⇩g⇩i⇩c_def)
  qed (simp_all add: β⇩m⇩a⇩g⇩i⇩c_def)

lemma β⇩m⇩a⇩g⇩i⇩c_matching: "Matching_Ternary.matches ((β⇩m⇩a⇩g⇩i⇩c γ), α) m a p ⟷ Semantics.matches γ m p"
  proof(induction m)
  case Match thus ?case 
    by(simp add: β⇩m⇩a⇩g⇩i⇩c_def matches_case_ternaryvalue_tuple)
  case MatchNot thus ?case
    by(simp add: matches_case_ternaryvalue_tuple β⇩m⇩a⇩g⇩i⇩c_not_Unknown split: ternaryvalue.split_asm)
  qed (simp_all add: matches_case_ternaryvalue_tuple split: ternaryvalue.split ternaryvalue.split_asm)
  


end