Theory Matching_Ternary

theory Matching_Ternary
imports "../Common/Ternary" "../Firewall_Common"
begin


section‹Packet Matching in Ternary Logic›

text‹The matcher for a primitive match expression @{typ "'a"}›
type_synonym ('a, 'packet) exact_match_tac="'a ⇒ 'packet ⇒ ternaryvalue"

text‹
If the matching is @{const TernaryUnknown}, it can be decided by the action whether this rule matches.
E.g. in doubt, we allow packets
›
type_synonym 'packet unknown_match_tac="action ⇒ 'packet ⇒ bool"

type_synonym ('a, 'packet) match_tac="(('a, 'packet) exact_match_tac × 'packet unknown_match_tac)"

text‹
For a given packet, map a firewall @{typ "'a match_expr"} to a @{typ ternaryformula}
Evaluating the formula gives whether the packet/rule matches (or unknown).
›
fun map_match_tac :: "('a, 'packet) exact_match_tac ⇒ 'packet ⇒ 'a match_expr ⇒ ternaryformula" where
  "map_match_tac β p (MatchAnd m1 m2) = TernaryAnd (map_match_tac β p m1) (map_match_tac β p m2)" |
  "map_match_tac β p (MatchNot m) = TernaryNot (map_match_tac β p m)" |
  "map_match_tac β p (Match m) = TernaryValue (β m p)" |
  "map_match_tac _ _ MatchAny = TernaryValue TernaryTrue"


context
begin
  text‹the @{term ternaryformula}s we construct never have Or expressions.›
  private fun ternary_has_or :: "ternaryformula ⇒ bool" where
    "ternary_has_or (TernaryOr _ _) ⟷ True" |
    "ternary_has_or (TernaryAnd t1 t2) ⟷ ternary_has_or t1 ∨ ternary_has_or t2" |
    "ternary_has_or (TernaryNot t) ⟷ ternary_has_or t" |
    "ternary_has_or (TernaryValue _) ⟷ False"
  private lemma map_match_tac__does_not_use_TernaryOr: "¬ (ternary_has_or (map_match_tac β p m))"
    by(induction m, simp_all)
  declare ternary_has_or.simps[simp del]
end


fun ternary_to_bool_unknown_match_tac :: "'packet unknown_match_tac ⇒ action ⇒ 'packet ⇒ ternaryvalue ⇒ bool" where
  "ternary_to_bool_unknown_match_tac _ _ _ TernaryTrue = True" |
  "ternary_to_bool_unknown_match_tac _ _ _ TernaryFalse = False" |
  "ternary_to_bool_unknown_match_tac α a p TernaryUnknown = α a p"

text‹
Matching a packet and a rule:
\begin{enumerate}
  \item Translate @{typ "'a match_expr"} to ternary formula
  \item Evaluate this formula
  \item If @{const TernaryTrue}/@{const TernaryFalse}, return this value
  \item If @{const TernaryUnknown}, apply the @{typ "'a unknown_match_tac"} to get a Boolean result
\end{enumerate}
›
definition matches :: "('a, 'packet) match_tac ⇒ 'a match_expr ⇒ action ⇒ 'packet ⇒ bool" where
  "matches γ m a p ≡ ternary_to_bool_unknown_match_tac (snd γ) a p (ternary_ternary_eval (map_match_tac (fst γ) p m))"


text‹Alternative matches definitions, some more or less convenient›

lemma matches_tuple: "matches (β, α) m a p = ternary_to_bool_unknown_match_tac α a p (ternary_ternary_eval (map_match_tac β p m))"
unfolding matches_def by simp

lemma matches_case: "matches γ m a p ⟷ (case ternary_eval (map_match_tac (fst γ) p m) of None ⇒ (snd γ) a p | Some b ⇒ b)"
unfolding matches_def ternary_eval_def
by (cases "(ternary_ternary_eval (map_match_tac (fst γ) p m))") auto

lemma matches_case_tuple: "matches (β, α) m a p ⟷ (case ternary_eval (map_match_tac β p m) of None ⇒ α a p | Some b ⇒ b)"
by (auto simp: matches_case split: option.splits)

lemma matches_case_ternaryvalue_tuple: "matches (β, α) m a p ⟷ (case ternary_ternary_eval (map_match_tac β p m) of 
        TernaryUnknown ⇒ α a p | 
        TernaryTrue ⇒ True |
        TernaryFalse ⇒ False)"
  by(simp split: option.split ternaryvalue.split add: matches_case ternary_to_bool_None ternary_eval_def)
(*use together: matches_case_ternaryvalue_tuple ternaryvalue.split *)


lemma matches_casesE:
  "matches (β, α) m a p ⟹ 
    (ternary_ternary_eval (map_match_tac β p m) = TernaryUnknown ⟹ α a p ⟹ P) ⟹ 
    (ternary_ternary_eval (map_match_tac β p m) = TernaryTrue ⟹ P)
  ⟹ P"
proof(induction m)
qed(auto split: option.split_asm simp: matches_case_tuple ternary_eval_def ternary_to_bool_bool_to_ternary elim: ternary_to_bool.elims)


text‹
Example: ‹¬ Unknown› is as good as ‹Unknown›
›
lemma "⟦ ternary_ternary_eval (map_match_tac β p expr) = TernaryUnknown ⟧ ⟹ matches (β, α) expr a p ⟷ matches (β, α) (MatchNot expr) a p"
by(simp add: matches_case_ternaryvalue_tuple)


lemma bunch_of_lemmata_about_matches:
  "matches γ (MatchAnd m1 m2) a p ⟷ matches γ m1 a p ∧ matches γ m2 a p" (*split AND*)
  "matches γ MatchAny a p" (*MatchAny is True*)
  "matches γ (MatchNot MatchAny) a p ⟷ False" (*Not True*)
  "matches γ (MatchNot (MatchNot m)) a p ⟷ matches γ m a p" (*idempotence*)
proof(case_tac [!] γ)
qed (simp_all split: ternaryvalue.split add: matches_case_ternaryvalue_tuple)

lemma match_raw_bool:
  "matches (β, α) (Match expr) a p = (case ternary_to_bool (β expr p) of Some r ⇒ r | None ⇒ (α a p))" (*Match raw*)
by(simp_all split: ternaryvalue.split add: matches_case_ternaryvalue_tuple)
lemma match_raw_ternary:
  "matches (β, α) (Match expr) a p = (case (β expr p) of TernaryTrue ⇒ True | TernaryFalse ⇒ False | TernaryUnknown ⇒ (α a p))" (*Match raw explicit*)
by(simp_all split: ternaryvalue.split add: matches_case_ternaryvalue_tuple)

(*kind of the DeMorgan Rule for matches*)
lemma matches_DeMorgan: "matches γ (MatchNot (MatchAnd m1 m2)) a p ⟷ (matches γ (MatchNot m1) a p) ∨ (matches γ (MatchNot m2) a p)"
by (cases γ) (simp split: ternaryvalue.split add: matches_case_ternaryvalue_tuple eval_ternary_DeMorgan)


subsection‹Ternary Matcher Algebra›

lemma matches_and_comm: "matches γ (MatchAnd m m') a p ⟷ matches γ (MatchAnd m' m) a p"
apply(cases γ, rename_tac β α, clarify)
by(simp add: matches_case_ternaryvalue_tuple eval_ternary_And_comm)

lemma matches_not_idem: "matches γ (MatchNot (MatchNot m)) a p ⟷ matches γ m a p"
by (fact bunch_of_lemmata_about_matches)


lemma MatchOr: "matches γ (MatchOr m1 m2) a p ⟷ matches γ m1 a p ∨ matches γ m2 a p"
  by(simp add: MatchOr_def matches_DeMorgan matches_not_idem)

lemma MatchOr_MatchNot: "matches γ (MatchNot (MatchOr m1 m2)) a p ⟷ matches γ (MatchNot m1) a p ∧ matches γ (MatchNot m2) a p"
  by(simp add: MatchOr_def matches_DeMorgan bunch_of_lemmata_about_matches)


lemma "(TernaryNot (map_match_tac β p (m))) = (map_match_tac β p (MatchNot m))"
by (metis map_match_tac.simps(2))

context
begin
  private lemma matches_simp1: "matches γ m a p ⟹ matches γ (MatchAnd m m') a p ⟷ matches γ m' a p"
    apply(cases γ, rename_tac β α, clarify)
    apply(simp split: ternaryvalue.split_asm ternaryvalue.split add: matches_case_ternaryvalue_tuple)
    done
  
  private lemma matches_simp11: "matches γ m a p ⟹ matches γ (MatchAnd m' m) a p ⟷ matches γ m' a p"
    by(simp_all add: matches_and_comm matches_simp1)
  
  private lemma matches_simp2: "matches γ (MatchAnd m m') a p ⟹ ¬ matches γ m a p ⟹ False"
    by (simp add: bunch_of_lemmata_about_matches)
  private lemma matches_simp22: "matches γ (MatchAnd m m') a p ⟹ ¬ matches γ m' a p ⟹ False"
    by (simp add: bunch_of_lemmata_about_matches)
  
  (*m simplifies to MatchUnknown*)
 private  lemma matches_simp3: "matches γ (MatchNot m) a p ⟹ matches γ m a p ⟹ (snd γ) a p"
    apply(cases γ, rename_tac β α, clarify)
    apply(simp split: ternaryvalue.split_asm ternaryvalue.split add: matches_case_ternaryvalue_tuple)
    done
  private lemma "matches γ (MatchNot m) a p ⟹ matches γ m a p ⟹ (ternary_eval (map_match_tac (fst γ) p m)) = None"
    apply(cases γ, rename_tac β α, clarify)
    apply(simp split: ternaryvalue.split_asm ternaryvalue.split add: matches_case_ternaryvalue_tuple ternary_eval_def)
    done
  
  lemmas matches_simps = matches_simp1 matches_simp11
  lemmas matches_dest = matches_simp2 matches_simp22
end


lemma matches_iff_apply_f_generic: "ternary_ternary_eval (map_match_tac β p (f (β,α) a m)) = ternary_ternary_eval (map_match_tac β p m) ⟹ matches (β,α) (f (β,α) a m) a p ⟷ matches (β,α) m a p"
  by(simp split: ternaryvalue.split_asm ternaryvalue.split add: matches_case_ternaryvalue_tuple)

lemma matches_iff_apply_f: "ternary_ternary_eval (map_match_tac β p (f m)) = ternary_ternary_eval (map_match_tac β p m) ⟹ matches (β,α) (f m) a p ⟷ matches (β,α) m a p"
  by(fact matches_iff_apply_f_generic)



lemma opt_MatchAny_match_expr_correct: "matches γ (opt_MatchAny_match_expr m) = matches γ m"
  proof(case_tac γ, rename_tac β α, clarify)
  fix β α
  assume "γ = (β, α)"
  have "ternary_ternary_eval (map_match_tac β p (opt_MatchAny_match_expr_once m)) =
          ternary_ternary_eval (map_match_tac β p m)" for p m
    proof(induction m rule: opt_MatchAny_match_expr_once.induct)
    qed(simp_all add: eval_ternary_simps eval_ternary_idempotence_Not)
  thus "matches (β, α) (opt_MatchAny_match_expr m) = matches (β, α) m"
    apply(simp add: fun_eq_iff)
    apply(clarify, rename_tac a p)
    apply(rule_tac f="opt_MatchAny_match_expr" in matches_iff_apply_f)
    apply(simp)
    apply(simp add: opt_MatchAny_match_expr_def)
    apply(rule repeat_stabilize_induct)
     by(simp)+
  qed



text‹An @{typ "'p unknown_match_tac"} is wf if it behaves equal for @{const Reject} and @{const Drop}›
definition wf_unknown_match_tac :: "'p unknown_match_tac ⇒ bool" where
  "wf_unknown_match_tac α ≡ (α Drop = α Reject)"


lemma wf_unknown_match_tacD_False1: "wf_unknown_match_tac α ⟹ ¬ matches (β, α) m Reject p ⟹ matches (β, α) m Drop p ⟹ False"
unfolding wf_unknown_match_tac_def by(simp add: matches_case_ternaryvalue_tuple split: ternaryvalue.split_asm)

lemma wf_unknown_match_tacD_False2: "wf_unknown_match_tac α ⟹ matches (β, α) m Reject p ⟹ ¬ matches (β, α) m Drop p ⟹ False"
unfolding wf_unknown_match_tac_def by(simp add: matches_case_ternaryvalue_tuple split: ternaryvalue.split_asm)


subsection‹Removing Unknown Primitives›

definition unknown_match_all :: "'a unknown_match_tac ⇒ action ⇒ bool" where
   "unknown_match_all α a = (∀p. α a p)"
definition unknown_not_match_any :: "'a unknown_match_tac ⇒ action ⇒ bool" where
   "unknown_not_match_any α a = (∀p. ¬ α a p)"

(*see upper_closure_matchexpr*)
fun remove_unknowns_generic :: "('a, 'packet) match_tac ⇒ action ⇒ 'a match_expr ⇒ 'a match_expr" where
  "remove_unknowns_generic _ _ MatchAny = MatchAny" |
  "remove_unknowns_generic _ _ (MatchNot MatchAny) = MatchNot MatchAny" |
  "remove_unknowns_generic (β, α) a (Match A) = (if
      (∀p. ternary_ternary_eval (map_match_tac β p (Match A)) = TernaryUnknown)
    then
      if unknown_match_all α a then MatchAny else if unknown_not_match_any α a then MatchNot MatchAny else Match A
    else (Match A))" |
  "remove_unknowns_generic (β, α) a (MatchNot (Match A)) = (if
      (∀p. ternary_ternary_eval (map_match_tac β p (Match A)) = TernaryUnknown)
    then
      if unknown_match_all α a then MatchAny else if unknown_not_match_any α a then MatchNot MatchAny else MatchNot (Match A)
    else MatchNot (Match A))" |
  "remove_unknowns_generic (β, α) a (MatchNot (MatchNot m)) = remove_unknowns_generic (β, α) a m" |
  "remove_unknowns_generic (β, α) a (MatchAnd m1 m2) = MatchAnd
      (remove_unknowns_generic (β, α) a m1)
      (remove_unknowns_generic (β, α) a m2)" |

  ― ‹@{text "¬ (a ∧ b) = ¬ b ∨ ¬ a"}   and   @{text "¬ Unknown = Unknown"}›
  "remove_unknowns_generic (β, α) a (MatchNot (MatchAnd m1 m2)) = 
    (if (remove_unknowns_generic (β, α) a (MatchNot m1)) = MatchAny ∨
        (remove_unknowns_generic (β, α) a (MatchNot m2)) = MatchAny
        then MatchAny else 
        (if (remove_unknowns_generic (β, α) a (MatchNot m1)) = MatchNot MatchAny then 
          remove_unknowns_generic (β, α) a (MatchNot m2) else
         if (remove_unknowns_generic (β, α) a (MatchNot m2)) = MatchNot MatchAny then 
          remove_unknowns_generic (β, α) a (MatchNot m1) else
         MatchNot (MatchAnd (MatchNot (remove_unknowns_generic (β, α) a (MatchNot m1))) (MatchNot (remove_unknowns_generic (β, α) a (MatchNot m2)))))
       )"

lemma[code_unfold]: "remove_unknowns_generic γ a (MatchNot (MatchAnd m1 m2)) = 
    (let m1' = remove_unknowns_generic γ  a (MatchNot m1); m2' = remove_unknowns_generic γ  a (MatchNot m2) in
    (if m1' = MatchAny ∨ m2' = MatchAny
     then MatchAny
     else 
        if m1' = MatchNot MatchAny then m2' else
        if m2' = MatchNot MatchAny then m1'
     else
        MatchNot (MatchAnd (MatchNot m1') (MatchNot m2')))
       )"
by(cases γ)(simp)


lemma remove_unknowns_generic_simp_3_4_unfolded: "remove_unknowns_generic (β, α) a (Match A) = (if
      (∀p. ternary_ternary_eval (map_match_tac β p (Match A)) = TernaryUnknown)
    then
      if (∀p. α a p) then MatchAny else if (∀p. ¬ α a p) then MatchNot MatchAny else Match A
    else (Match A))" 
 "remove_unknowns_generic (β, α) a (MatchNot (Match A)) = (if
      (∀p. ternary_ternary_eval (map_match_tac β p (Match A)) = TernaryUnknown)
    then
      if (∀p. α a p) then MatchAny else if (∀p. ¬ α a p) then MatchNot MatchAny else MatchNot (Match A)
    else MatchNot (Match A))"
  by(auto simp add: unknown_match_all_def unknown_not_match_any_def)

declare remove_unknowns_generic.simps[simp del]

lemmas remove_unknowns_generic_simps2 = remove_unknowns_generic.simps(1) remove_unknowns_generic.simps(2) 
            remove_unknowns_generic_simp_3_4_unfolded
            remove_unknowns_generic.simps(5) remove_unknowns_generic.simps(6) remove_unknowns_generic.simps(7)


lemma "matches (β, α) (remove_unknowns_generic (β, α) a (MatchNot (Match A))) a p = matches (β, α) (MatchNot (Match A)) a p"
by(simp add: remove_unknowns_generic_simps2 matches_case_ternaryvalue_tuple)



lemma remove_unknowns_generic: "matches γ (remove_unknowns_generic γ a m) a = matches γ m a"
proof -
  have "matches γ (remove_unknowns_generic γ a m) a p = matches γ m a p"
  for p
  proof(induction γ a m rule: remove_unknowns_generic.induct)
  case 3 thus ?case
      by(simp add: bunch_of_lemmata_about_matches match_raw_ternary remove_unknowns_generic_simps2)
  next
  case 4 thus ?case
     by(simp add: matches_case_ternaryvalue_tuple remove_unknowns_generic_simps2)
  next
  case 7 thus ?case
    apply(simp add: bunch_of_lemmata_about_matches matches_DeMorgan remove_unknowns_generic_simps2)
    apply(simp add: matches_case_ternaryvalue_tuple)
    by fastforce
  qed(simp_all add: bunch_of_lemmata_about_matches remove_unknowns_generic_simps2)
  thus ?thesis by(simp add: fun_eq_iff)
qed





fun has_unknowns :: " ('a, 'p) exact_match_tac ⇒ 'a match_expr ⇒ bool" where
  "has_unknowns β (Match A) = (∃p. ternary_ternary_eval (map_match_tac β p (Match A)) = TernaryUnknown)" |
  "has_unknowns β (MatchNot m) = has_unknowns β m" |
  "has_unknowns β MatchAny = False" |
  "has_unknowns β (MatchAnd m1 m2) = (has_unknowns β m1 ∨ has_unknowns β m2)"

(* assumes simple_ruleset, thus we only care about Accept/Drop *)
definition packet_independent_α :: "'p unknown_match_tac ⇒ bool" where
  "packet_independent_α α = (∀a p1 p2. a = Accept ∨ a = Drop ⟶ α a p1 ⟷ α a p2)"

lemma packet_independent_unknown_match: "a = Accept ∨ a = Drop ⟹ packet_independent_α α ⟹ ¬ unknown_not_match_any α a ⟷ unknown_match_all α a"
  by(auto simp add: packet_independent_α_def unknown_match_all_def unknown_not_match_any_def)

text‹If for some type the exact matcher returns unknown, then it returns unknown for all these types›
definition packet_independent_β_unknown :: "('a, 'packet) exact_match_tac ⇒ bool" where
  "packet_independent_β_unknown β ≡ ∀A. (∃p. β A p ≠ TernaryUnknown) ⟶ (∀p. β A p ≠ TernaryUnknown)"


lemma remove_unknowns_generic_specification: "a = Accept ∨ a = Drop ⟹ packet_independent_α α ⟹
  packet_independent_β_unknown β ⟹
   ¬ has_unknowns β (remove_unknowns_generic (β, α) a m)"
  proof(induction "(β, α)" a m rule: remove_unknowns_generic.induct)
  case 3 thus ?case by(simp add: packet_independent_unknown_match packet_independent_β_unknown_def remove_unknowns_generic.simps)
  next
  case 4 thus ?case by(simp add: packet_independent_unknown_match packet_independent_β_unknown_def remove_unknowns_generic.simps)
  qed(simp_all add: remove_unknowns_generic.simps)





text‹Checking is something matches unconditionally›
context
begin
  private lemma no_primitives_no_unknown: "¬ has_primitive m  ⟹ (ternary_ternary_eval (map_match_tac β p m)) ≠ TernaryUnknown"
  proof(induction m)
  case Match thus ?case by auto
  next
  case MatchAny thus ?case by simp
  next
  case MatchAnd thus ?case by(auto elim: eval_ternary_And.elims)
  next
  case MatchNot thus ?case by(auto dest: eval_ternary_Not_UnknownD)
  qed


  private lemma no_primitives_matchNot: assumes "¬ has_primitive m" shows "matches γ (MatchNot m) a p ⟷ ¬ matches γ m a p"
  proof -
    obtain β α where "(β, α) = γ" by (cases γ, simp)
    thm no_primitives_no_unknown
    from assms have "matches (β, α) (MatchNot m) a p ⟷ ¬ matches (β, α) m a p"
      apply(induction m)
         apply(simp_all add: matches_case_ternaryvalue_tuple split: ternaryvalue.split )
      apply(rename_tac m1 m2)
      by(simp split: ternaryvalue.split_asm)
    with ‹(β, α) = γ› assms show ?thesis by simp
  qed
  

  lemma matcheq_matchAny: "¬ has_primitive m ⟹ matcheq_matchAny m ⟷ matches γ m a p"
  proof(induction m)
  case Match hence False by auto
    thus ?case ..
  next
  case (MatchNot m)
    from MatchNot.prems have "¬ has_primitive m" by simp
    with no_primitives_matchNot have "matches γ (MatchNot m) a p = (¬ matches γ m a p)" by metis
    with MatchNot show ?case by(simp)
  next
  case (MatchAnd m1 m2)
    thus ?case by(simp add: bunch_of_lemmata_about_matches)
  next
  case MatchAny show ?case by(simp add: Matching_Ternary.bunch_of_lemmata_about_matches)
  qed

  lemma matcheq_matchNone: "¬ has_primitive m ⟹ matcheq_matchNone m ⟷ ¬ matches γ m a p"
    by(auto dest: matcheq_matchAny matachAny_matchNone)

  lemma matcheq_matchNone_not_matches: "matcheq_matchNone m ⟹ ¬ matches γ m a p"
    proof(induction m rule: matcheq_matchNone.induct)
    qed(auto simp add: bunch_of_lemmata_about_matches matches_DeMorgan)
    
end



text‹Lemmas about @{const MatchNot} in ternary logic.›

lemma matches_MatchNot_no_unknowns:
   assumes "¬ has_unknowns β m"
   shows "matches (β,α) (MatchNot m) a p ⟷ ¬ matches (β,α) m a p"
proof -
  { fix m have "¬ has_unknowns β m ⟹
       ternary_to_bool (ternary_ternary_eval (map_match_tac β p m)) ≠ None"
    apply(induction m)
       apply(simp_all)
      using ternary_to_bool.elims apply blast
     using ternary_to_bool_Some apply fastforce
    using ternary_lift(6) ternary_to_bool_Some by auto
  } note no_unknowns_ternary_to_bool_Some=this
    from assms show ?thesis
      by(auto split: option.split_asm
              simp: matches_case_tuple no_unknowns_ternary_to_bool_Some ternary_to_bool_Some  ternary_eval_def ternary_to_bool_bool_to_ternary
              elim: ternary_to_bool.elims)
qed

lemma MatchNot_ternary_ternary_eval: "(ternary_ternary_eval (map_match_tac β p m')) = (ternary_ternary_eval (map_match_tac β p m)) ⟹
    matches (β,α) (MatchNot m') a p = matches (β,α) (MatchNot m) a p"
by(simp add: matches_tuple)



text‹For our @{typ "'p unknown_match_tac"}s ‹in_doubt_allow› and ‹in_doubt_deny›,
      when doing an induction over some function that modifies @{term "m::'a match_expr"},
      we get the @{const MatchNot} case for free (if we can set arbitrary @{term "p::'p"}).
      This does not hold for arbitrary @{typ "'p unknown_match_tac"}s.›
lemma matches_induction_case_MatchNot:
      assumes "α Drop ≠ α Accept" and "packet_independent_α α"
      and     "∀ a. matches (β,α) m' a p = matches (β,α) m a p"
      shows   "matches (β,α) (MatchNot m') a p = matches (β,α) (MatchNot m) a p"
proof -
  from assms(1) assms(2) have xxxx_xxX: "⋀b. ∀a. α a p = (¬ b) ⟹ False"
    apply(simp add: packet_independent_α_def)
    apply(case_tac "α Accept p")
     apply(simp_all)
     apply(case_tac [!] "α Drop p")
       apply(simp_all add: fun_eq_iff)
     apply blast+
    done

  have xx2: "⋀t. ternary_eval (TernaryNot t) = None ⟹ ternary_eval t = None"
  by (simp add: eval_ternary_Not_UnknownD ternary_eval_def ternary_to_bool_None)
  
  have xx3: "⋀t b. ternary_eval (TernaryNot t) = Some b ⟹  ternary_eval t = Some (¬ b)"
  by (metis eval_ternary_Not.simps(1) eval_ternary_Not.simps(2) ternary_eval_def ternary_ternary_eval.simps(3) ternary_ternary_eval_idempotence_Not ternary_to_bool_Some)

  from assms show ?thesis
    apply(simp add: matches_case_tuple)
    apply(case_tac "ternary_eval (TernaryNot (map_match_tac β p m'))")
     apply(case_tac [!] "ternary_eval (TernaryNot (map_match_tac β p m))")
       apply(simp_all)
      apply(drule xx2)
      apply(drule xx3)
      apply(simp)
      using xxxx_xxX apply metis
     apply(drule xx2)
     apply(drule xx3)
     apply(simp)
     using xxxx_xxX apply metis
    apply(drule xx3)+
    apply(simp)
    done
qed



end