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