Theory Parity_Classify

theory Parity_Classify
  imports
    Parity_Exec
begin

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

text ‹
  The check classifier is derived from Parity's bundle, exactly as in
  ‹Voblint_Analysis_Sign.Sign_Classify›: the Boolean recursion over \<^typ>‹exp›,
  the three-way classification, and the node-indexed bridge to
  \<^const>‹checks_proven› come from the comparison queries
  \<^const>‹parity_less›/\<^const>‹parity_eq› and the evaluator, through the
  ‹parity_tf› interpretation in \<^theory>‹Voblint_Analysis_Parity.Parity_Transfer›.
  Their facts stay under ‹parity_tf.check.›.
›

end