Theory Sign_Classify

theory Sign_Classify
  imports
    Sign_Exec
begin

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

text ‹
  The check classifier is derived from Sign's bundle: 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 queries
  \<^const>‹sign_less›/\<^const>‹sign_eq› and evaluator, through the
  ‹sign_tf› interpretation in \<^theory>‹Voblint_Analysis_Sign.Sign_Transfer›.
  Their facts stay under ‹sign_tf.check.›; ‹classify_check›'s two soundness
  directions are ‹sign_tf.check.classify_check_proved› and
  ‹sign_tf.check.classify_check_refuted›.
  ‹Sign_Regression› in the Sign examples exercises them.
›

end