Theory Parity_Regression

theory Parity_Regression
  imports
    "Voblint_Analysis_Parity.Parity_Exec"
begin

section ‹Parity regression assertions›

text ‹
  Build-checked regression assertions for the Parity domain, moved out of core.
  Each lemma evaluates a Parity operation on concrete values; nothing cites them,
  the build is their consumer.
›

subsection ‹Rendering›

text ‹
  ‹string_of_parity› prints parities in Goblint's congruence notation, and the
  ‹numeric_domain› instance's ‹to_string› prints a standalone top as ‹sym_top›.
›

lemma string_of_parity_regression:
  "string_of_parity PBot = sym_bottom"
  "string_of_parity PEven = STR ''2<int>''"
  "string_of_parity POdd = STR ''1+2<int>''"
  "string_of_parity PTop = sym_int"
  by eval+

lemma to_string_parity_regression:
  "to_string PTop = sym_top"
  "to_string POdd = STR ''1+2<int>''"
  by eval+

subsection ‹Backward refinement›

text ‹
  Evaluated regression cases: an odd sum with an even operand forces the other
  odd, and an odd product forces both factors odd.
›

lemma parity_inverse_regression:
  "inv_plus_parity POdd PTop PEven = (POdd, PEven)"
  "inv_minus_parity PEven PTop POdd = (POdd, POdd)"
  "inv_times_parity POdd PTop PTop = (POdd, POdd)"
  "inv_eq_parity True PTop PEven = (PEven, PEven)"
  by eval+

subsection ‹Guard filters›

text ‹
  ‹bfilter_parity› uses the inverse operators to narrow a variable through an
  arithmetic equality guard, and leaves it alone under an order guard.
›

definition test_env_parity :: "parity abs_state" where
  "test_env_parity = (λ_. PTop)((STR ''y'') := PEven)"

text ‹‹x + 1 == y› with ‹y› even makes ‹x› odd.›
lemma bfilter_parity_plus_narrows:
  "bfilter_parity (Eq (Plus (V (STR ''x'')) (N 1)) (V (STR ''y''))) True test_env_parity
     (STR ''x'') = POdd"
  unfolding test_env_parity_def by eval

text ‹An order guard says nothing about parity.›
lemma bfilter_parity_less_identity:
  "bfilter_parity (Less (V (STR ''x'')) (N 3)) True test_env_parity (STR ''x'') = PTop"
  unfolding test_env_parity_def by eval

subsection ‹Executable classification tests›

text ‹One state per test, built as an override of an otherwise-unconstrained
  (‹PTop›) environment, so each test exercises exactly the comparison it
  names.›

definition test_env_eo :: "parity abs_state" where
  "test_env_eo = (λ_. PTop)((STR ''x'') := PEven, (STR ''y'') := POdd)"

text ‹Disjoint parity classes: the direct equality is refuted, and its
  negation is proved --- going through ‹check_query›'s ‹Not› case on the
  un-negated equality, not a one-sided reading of the positive answer.›

lemma parity_classify_eq_refuted:
  "parity_classify_check (Eq (V (STR ''x'')) (V (STR ''y''))) test_env_eo = Check_Refuted"
  unfolding test_env_eo_def by eval

lemma parity_classify_not_eq_proved:
  "parity_classify_check (Not (Eq (V (STR ''x'')) (V (STR ''y'')))) test_env_eo = Check_Proved"
  unfolding test_env_eo_def by eval

text ‹Same abstract value on both sides: ‹x› is ‹PEven› and the literal ‹4›
  is also ‹PEven›, but Parity has no singleton representation, so the
  equality stays unknown rather than falsely proved.›

lemma parity_classify_eq_unknown:
  "parity_classify_check (Eq (V (STR ''x'')) (N 4)) test_env_eo = Check_Unknown"
  unfolding test_env_eo_def by eval

text ‹Nested ‹Or›: proved through the negated-equality branch alone.›

definition test_env_nested_proved :: "parity abs_state" where
  "test_env_nested_proved = (λ_. PTop)((STR ''x'') := PEven, (STR ''y'') := POdd)"

lemma parity_classify_nested_proved:
  "parity_classify_check
     (Or (Not (Eq (V (STR ''x'')) (V (STR ''y'')))) (Eq (V (STR ''z'')) (N 1)))
     test_env_nested_proved = Check_Proved"
  unfolding test_env_nested_proved_def by eval

text ‹Nested ‹Or›, unknown: neither branch resolves when both sides share a
  parity class.›

definition test_env_nested_unknown :: "parity abs_state" where
  "test_env_nested_unknown = (λ_. PTop)((STR ''x'') := PEven, (STR ''y'') := PEven)"

lemma parity_classify_nested_unknown:
  "parity_classify_check
     (Or (Not (Eq (V (STR ''x'')) (V (STR ''y'')))) (Eq (V (STR ''z'')) (N 1)))
     test_env_nested_unknown = Check_Unknown"
  unfolding test_env_nested_unknown_def by eval

end