Theory Check_Result

theory Check_Result
  imports Main
begin

section ‹A flat three-valued check verdict›

text ‹
  ‹check_result› as a flat join-semilattice: ‹Check_Unknown› is the top element,
  ‹Check_Proved›/‹Check_Refuted› are incomparable, and their join is
  ‹Check_Unknown›. The canonical use is aggregating a check's verdict across
  several independently-sound sources of evidence (e.g. one abstract state per
  reachable calling context) without joining the underlying abstract states
  first: two sources agreeing stay that verdict, any disagreement collapses to
  ‹Check_Unknown› rather than asserting a verdict neither source alone
  established.
›

datatype check_result = Check_Proved | Check_Refuted | Check_Unknown

instantiation check_result :: semilattice_sup
begin

definition less_eq_check_result :: "check_result ⇒ check_result ⇒ bool" where
  "less_eq_check_result x y ⟷ x = y ∨ y = Check_Unknown"

definition less_check_result :: "check_result ⇒ check_result ⇒ bool" where
  "less_check_result x y ⟷ x ≤ y ∧ ¬ y ≤ x"

definition sup_check_result :: "check_result ⇒ check_result ⇒ check_result" where
  "sup_check_result x y = (if x = y then x else Check_Unknown)"

instance
  by standard
     (auto simp: less_eq_check_result_def less_check_result_def sup_check_result_def)

end

text ‹
  There is no dual bottom: ‹Check_Proved› and ‹Check_Refuted› have no common
  lower verdict, and the absence of any evidence at all is expressed one level
  up, by ‹check_result lifted›, not inside this type.
›

instantiation check_result :: top
begin

definition top_check_result :: check_result where
  "top_check_result = Check_Unknown"

instance ..

end

instance check_result :: order_top
  by standard (simp add: less_eq_check_result_def top_check_result_def)

end