Theory Common_Primitive_Lemmas

theory Common_Primitive_Lemmas
imports Common_Primitive_Matcher
        "../Semantics_Ternary/Primitive_Normalization"
        "../Semantics_Ternary/MatchExpr_Fold"
begin

section‹Further Lemmas about the Common Matcher›

lemma has_unknowns_common_matcher: fixes m::"'i::len common_primitive match_expr"
  shows "has_unknowns common_matcher m ⟷ has_disc is_Extra m"
  proof -
  { fix A and p :: "('i, 'a) tagged_packet_scheme"
    have "common_matcher A p = TernaryUnknown ⟷ is_Extra A"
      by(induction A p rule: common_matcher.induct) (simp_all add: bool_to_ternary_Unknown)
  } hence "β = (common_matcher::('i::len common_primitive, ('i, 'a) tagged_packet_scheme) exact_match_tac)
            ⟹ has_unknowns β m = has_disc is_Extra m" for β
  by(induction β m rule: has_unknowns.induct)
    (simp_all)
  thus ?thesis by simp
qed



end