Theory Warrowing

section ‹Widening, Narrowing and Warrowing Operators›

theory Warrowing
  imports Main
begin

text ‹The operator classes are kept apart from the solvers so that abstract domains can
  instantiate them without importing solver state.›

class widening =
  fixes widen :: "'a :: order ⇒ 'a ⇒ 'a" (infixl "∇" 65)
  assumes widen_ge1: "a ≤ a ∇ b" and widen_ge2: "b ≤ a ∇ b"

class narrowing =
  fixes narrow :: "'a :: order ⇒ 'a ⇒ 'a" (infixl "Δ" 70)
  assumes narrow_ge: "b ≤ a ⟹ b ≤ a Δ b"
    and narrow_le: "b ≤ a ⟹ a Δ b ≤ a"

class warrowing = widening + narrowing
begin
  definition warrow :: "'a ⇒ 'a ⇒ 'a" (infixl "∇Δ" 65) where
    "warrow a b = (if b ≤ a then a Δ b else a ∇ b)"

  lemma warrowing_properties:
    "b ≤ a ∇Δ b"
    "a = a ∇Δ b ⟹ b ≤ a"
    unfolding warrow_def
    using narrow_ge[of b a] widen_ge2[of b a] by (auto split: if_splits)

  lemma warrow_le_when_le: "b ≤ a ⟹ a ∇Δ b ≤ a"
    unfolding warrow_def using narrow_le by simp

  lemma warrow_idem: "a ∇Δ a = a"
    unfolding warrow_def using narrow_ge[of a a] narrow_le[of a a] by (auto intro: order.antisym)
end

end