Theory Three_Valued

theory Three_Valued
  imports Main
begin

section ‹Three-valued Boolean combinators›

text ‹
  ‹bin_log f ann› lifts a Boolean connective ‹f› to ‹bool option› with the
  short-circuit reading ‹f› already has: one definite operand equal to the
  annihilator ‹ann› decides the result regardless of the other side, two
  definite operands are combined by ‹f›, and anything else is ‹None›.
  Goblint's ‹id_binary_log› (‹base.ml›) has the same shape; ‹and_opt› and
  ‹or_opt› are its two instances.

  Both expression evaluation and check classification combine three-valued
  answers this way, so the combinators sit below either of them.
›

definition bin_log ::
  "(bool ⇒ bool ⇒ bool) ⇒ bool ⇒ bool option ⇒ bool option ⇒ bool option" where
  "bin_log f ann x y =
     (if x = Some ann ∨ y = Some ann then Some ann
      else case (x, y) of (Some a, Some b) ⇒ Some (f a b) | _ ⇒ None)"

abbreviation and_opt :: "bool option ⇒ bool option ⇒ bool option" where
  "and_opt ≡ bin_log (∧) False"

abbreviation or_opt :: "bool option ⇒ bool option ⇒ bool option" where
  "or_opt ≡ bin_log (∨) True"

text ‹
  The semantic reading a caller actually wants: given what ‹x›/‹y› mean
  (‹px›/‹py›, via the same Horn-clause shape an induction hypothesis already
  has), the combined answer agrees with ‹f› on those meanings, provided ‹ann›
  really annihilates ‹f›. Stated this way, a consumer never has to know
  ‹bin_log›'s own case split.
›

lemma bin_log_sound:
  assumes "bin_log f ann x y = Some r"
    and "⋀b. f ann b = ann" and "⋀b. f b ann = ann"
    and "⋀b. x = Some b ⟹ px = b"
    and "⋀b. y = Some b ⟹ py = b"
  shows "f px py = r"
  using assms unfolding bin_log_def
  by (cases x; cases y) (auto split: if_splits)

lemma and_opt_sound:
  assumes "and_opt x y = Some r"
    and "⋀b. x = Some b ⟹ px = b"
    and "⋀b. y = Some b ⟹ py = b"
  shows "(px ∧ py) = r"
  using bin_log_sound[OF assms(1) _ _ assms(2,3)] by simp

lemma or_opt_sound:
  assumes "or_opt x y = Some r"
    and "⋀b. x = Some b ⟹ px = b"
    and "⋀b. y = Some b ⟹ py = b"
  shows "(px ∨ py) = r"
  using bin_log_sound[OF assms(1) _ _ assms(2,3)] by simp

text ‹
  A definite answer survives widening the operands, so the combinators keep every
  definite answer of their wider inputs.
›

lemma bin_log_mono:
  assumes "⋀b. x2 = Some b ⟹ x1 = Some b" and "⋀b. y2 = Some b ⟹ y1 = Some b"
  shows "bin_log f ann x2 y2 = Some b ⟹ bin_log f ann x1 y1 = Some b"
  using assms unfolding bin_log_def
  by (cases x2; cases y2) (auto split: if_splits)

lemma and_opt_mono:
  assumes "⋀b. x2 = Some b ⟹ x1 = Some b" and "⋀b. y2 = Some b ⟹ y1 = Some b"
  shows "and_opt x2 y2 = Some b ⟹ and_opt x1 y1 = Some b"
  using bin_log_mono[OF assms] .

lemma or_opt_mono:
  assumes "⋀b. x2 = Some b ⟹ x1 = Some b" and "⋀b. y2 = Some b ⟹ y1 = Some b"
  shows "or_opt x2 y2 = Some b ⟹ or_opt x1 y1 = Some b"
  using bin_log_mono[OF assms] .

end