Theory Interval_Regression

theory Interval_Regression
  imports
    "Voblint_Analysis_Interval.Interval_Transfer"
begin

section ‹Interval regression assertions›

text ‹
  Build-checked regression assertions for the Interval domain, moved out of the
  core theories. Each lemma evaluates a concrete value; nothing cites them.
›

subsection ‹Rendering›

text ‹
  ‹string_of_ivl› prints bounds as ‹[l,u]› and every empty representation as
  ‹sym_bottom›; ‹to_string› prints the standalone top as ‹sym_top›.
›

lemma string_of_ivl_regression:
  "string_of_ivl (Ivl (Fin (-3)) (Fin 5)) = STR ''[-3,5]''"
  "string_of_ivl (Ivl MinInf (Fin 0)) = STR ''[-<infinity>,0]''"
  "string_of_ivl (Ivl MinInf PlusInf) = STR ''[-<infinity>,+<infinity>]''"
  "string_of_ivl (Ivl (Fin 5) (Fin (-1))) = sym_bottom"
  "string_of_ivl (Ivl PlusInf PlusInf) = sym_bottom"
  by eval+

lemma to_string_ivl_regression:
  "to_string (top :: ivl) = sym_top"
  "to_string (Ivl (Fin 0) PlusInf) = STR ''[0,+<infinity>]''"
  by eval+

subsection ‹Check classification›

text ‹One state per test, built as an override of an otherwise-unconstrained
  (‹ivl_top›) environment, so each test exercises exactly the comparison it
  names, and one showing the precision gain over Sign: a bounded range proves
  both a wider upper bound and a tighter lower bound in one classification,
  which Sign's four-value lattice cannot distinguish from ‹STop›.›

definition test_env_bounded :: "ivl abs_state" where
  "test_env_bounded = (λ_. ivl_top)((STR ''x'') := Ivl (Fin 4) (Fin 7))"

lemma interval_classify_less_proved:
  "interval_classify_check (Less (V (STR ''x'')) (N 11)) test_env_bounded = Check_Proved"
  unfolding test_env_bounded_def by eval

lemma interval_classify_less_refuted:
  "interval_classify_check (Less (V (STR ''x'')) (N 0)) test_env_bounded = Check_Refuted"
  unfolding test_env_bounded_def by eval

lemma interval_classify_eq_unknown:
  "interval_classify_check (Eq (V (STR ''x'')) (N 5)) test_env_bounded = Check_Unknown"
  unfolding test_env_bounded_def by eval

text ‹The precision gain over Sign: ‹0 < x› and ‹x < 8› both hold outright
  once ‹x› is known to lie strictly between ‹3› and ‹8›, a fact only a
  domain that tracks numeric bounds can prove; Sign's ‹SPos›/‹SNonNeg› would
  classify ‹x < 8› \<^term>‹Check_Unknown› on the same information.›

definition test_env_precision :: "ivl abs_state" where
  "test_env_precision = (λ_. ivl_top)((STR ''x'') := Ivl (Fin 4) (Fin 7))"

lemma interval_classify_precision_lower_proved:
  "interval_classify_check (Less (N 2) (V (STR ''x''))) test_env_precision = Check_Proved"
  unfolding test_env_precision_def by eval

lemma interval_classify_precision_upper_proved:
  "interval_classify_check (Less (V (STR ''x'')) (N 9)) test_env_precision = Check_Proved"
  unfolding test_env_precision_def by eval

subsection ‹Numeric queries›

text ‹
  Permanent regression witnesses for the touching-boundary case: before
  ‹Interval_Numeric_Queries›'s ‹u2 < l1› was weakened to ‹u2 ≤ l1›,
  ‹interval_less_false› could not refute ‹0 < x› for ‹x = [-inf,0]› (a range entirely ‹≤ 0›) because the
  witnessing bound touches rather than strictly separates.
›

lemma interval_less_false_witness_touching_boundary:
  "interval_less_false (Ivl (Fin 0) (Fin 0)) (Ivl MinInf (Fin 0))"
  by simp

lemma interval_less_false_witness_touching_boundary_finite:
  "interval_less_false (Ivl (Fin 1) (Fin 1)) (Ivl MinInf (Fin 1))"
  by simp

text ‹‹interval_eq_false› refutes equality of the disjoint intervals ‹[1,2]›
  and ‹[5,6]›, the witness whose raw meet is not ‹bot›.›

lemma interval_eq_false_witness_disjoint:
  "interval_eq_false (Ivl (Fin 1) (Fin 2)) (Ivl (Fin 5) (Fin 6))"
  by (simp add: less_eint_def)

end