Theory Interval_Classify

theory Interval_Classify
  imports
    Interval_Exec
begin

section ‹Interval instance of the generic check-discharge interface›

text ‹
  The check classifier is derived from Interval's bundle, mirroring
  ‹Sign_Classify›: the Boolean recursion over \<^typ>‹exp› (‹Not›, ‹And›, ‹Or›), the
  three-way classification, and the node-indexed bridge to
  \<^const>‹checks_proven› come from the bundle's bound-comparison queries
  \<^const>‹interval_less›/\<^const>‹interval_eq› and evaluator, through the
  ‹ivl_tf› interpretation in \<^theory>‹Voblint_Analysis_Interval.Interval_Transfer›.

  The classifier sits below ‹Interval_Analyses›: each registration there discharges
  its ‹ClProved›/‹ClRefuted› obligations with ‹ivl_tf.check.classify_check_proved›
  and ‹ivl_tf.check.classify_check_refuted›.
›

end