Theory Voblint_Analysis_Interval.Interval_Numeric_Queries

theory Interval_Numeric_Queries
  imports Interval_Warrowing "Voblint_Domain.Backward_Numeric_Queries"
begin

section ‹Interval interpretation of the generic numeric-query interface›

text ‹
  Second-domain validation for ‹sound_numeric_queries›
  (\<^theory>‹Voblint_Domain.Numeric_Queries›): a real, minimal Interval instance,
  interpreted without touching that generic theory. Entailment/refutation of
  ‹<›/‹=› reduces to comparing bounds: two intervals' ‹<› relation is
  provable exactly when one interval's upper bound is strictly below the
  other's lower bound; ‹=› exactly when both are the same singleton point;
  ‹≠› exactly when the intervals are disjoint. Empty intervals (‹l > u›) make
  every judgment vacuously true, the same role ‹SBot› plays for Sign.
›

lemma gamma_ivlD:
  assumes "x ∈ gamma_ivl (Ivl l u)"
  shows "l ≤ Fin x" and "Fin x ≤ u"
  using assms
  by auto

lemma ivl_upper_lower_less:
  assumes "Fin i ≤ u" and "u < l" and "l ≤ Fin j"
  shows "i < j"
  using le_less_trans[OF assms(1) less_le_trans[OF assms(2,3)]]
  by (simp add: less_eint_def less_eq_eint_def)

lemma ivl_upper_lower_less_eq:
  assumes "Fin i ≤ u" and "u ≤ l" and "l ≤ Fin j"
  shows "i ≤ j"
  using order_trans[OF assms(1) order_trans[OF assms(2,3)]]
  by (simp add: less_eq_eint_def)

lemma ivl_upper_lower_not_less_eq:
  assumes "Fin j ≤ u" and "u ≤ l" and "l ≤ Fin i"
  shows "¬ i < j"
  using ivl_upper_lower_less_eq[OF assms]
  by auto


lemma ivl_separated_not_equal:
  assumes "Fin i ≤ u1"
      and "u1 < l2"
      and "l2 ≤ Fin j"
  shows "i ≠ j"
  using ivl_upper_lower_less[OF assms]
  by auto

fun interval_less_true :: "ivl ⇒ ivl ⇒ bool" where
  "interval_less_true (Ivl l1 u1) (Ivl l2 u2) =
     (¬ l1 ≤ u1 ∨ ¬ l2 ≤ u2 ∨ u1 < l2)"

lemma interval_less_true_sound:
  assumes query: "interval_less_true a b"
      and ai: "i ∈ gamma_ivl a"
      and bj: "j ∈ gamma_ivl b"
  shows "i < j"
proof -
  obtain l1 u1 where a_def: "a = Ivl l1 u1"
    by (cases a)
  obtain l2 u2 where b_def: "b = Ivl l2 u2"
    by (cases b)

  from ai have i_bounds:
    "l1 ≤ Fin i" "Fin i ≤ u1"
    unfolding a_def
    by (auto dest: gamma_ivlD)

  from bj have j_bounds:
    "l2 ≤ Fin j" "Fin j ≤ u2"
    unfolding b_def
    by (auto dest: gamma_ivlD)

  from i_bounds j_bounds have nonempty:
    "l1 ≤ u1" "l2 ≤ u2"
    by order+

  with query have separated: "u1 < l2"
    unfolding a_def b_def
    by simp

  show ?thesis
    using i_bounds(2) separated j_bounds(1)
    by (rule ivl_upper_lower_less)
qed


fun interval_less_false :: "ivl ⇒ ivl ⇒ bool" where
  "interval_less_false (Ivl l1 u1) (Ivl l2 u2) =
     (¬ l1 ≤ u1 ∨ ¬ l2 ≤ u2 ∨ u2 ≤ l1)"

lemma interval_less_false_sound:
  assumes query: "interval_less_false a b"
      and ai: "i ∈ gamma_ivl a"
      and bj: "j ∈ gamma_ivl b"
  shows "¬ i < j"
proof -
  obtain l1 u1 where a_def: "a = Ivl l1 u1"
    by (cases a)
  obtain l2 u2 where b_def: "b = Ivl l2 u2"
    by (cases b)

  from ai have i_bounds:
    "l1 ≤ Fin i" "Fin i ≤ u1"
    unfolding a_def
    by (auto dest: gamma_ivlD)

  from bj have j_bounds:
    "l2 ≤ Fin j" "Fin j ≤ u2"
    unfolding b_def
    by (auto dest: gamma_ivlD)

  from i_bounds j_bounds have nonempty:
    "l1 ≤ u1" "l2 ≤ u2"
    by order+

  with query have separated: "u2 ≤ l1"
    unfolding a_def b_def
    by simp

  show ?thesis
    using j_bounds(2) separated i_bounds(1)
    by (rule ivl_upper_lower_not_less_eq)
qed

fun interval_eq_true :: "ivl ⇒ ivl ⇒ bool" where
  "interval_eq_true (Ivl l1 u1) (Ivl l2 u2) =
     (¬ l1 ≤ u1 ∨ ¬ l2 ≤ u2 ∨ (l1 = u1 ∧ l2 = u2 ∧ l1 = l2))"

lemma interval_eq_true_sound:
  assumes query: "interval_eq_true a b"
      and ai: "i ∈ gamma_ivl a"
      and bj: "j ∈ gamma_ivl b"
  shows "i = j"
proof -
  obtain l1 u1 where a_def: "a = Ivl l1 u1"
    by (cases a)
  obtain l2 u2 where b_def: "b = Ivl l2 u2"
    by (cases b)

  from ai have i_bounds:
    "l1 ≤ Fin i" "Fin i ≤ u1"
    unfolding a_def
    by (auto dest: gamma_ivlD)

  from bj have j_bounds:
    "l2 ≤ Fin j" "Fin j ≤ u2"
    unfolding b_def
    by (auto dest: gamma_ivlD)

  from i_bounds j_bounds have nonempty:
    "l1 ≤ u1" "l2 ≤ u2"
    by (meson order_trans)+

  with query have singleton:
    "l1 = u1" "l2 = u2" "l1 = l2"
    unfolding a_def b_def
    by auto

  from ai singleton have "Fin i = l1"
    unfolding a_def
    using i_bounds(1,2) by order

  moreover from bj singleton have "Fin j = l1"
    unfolding b_def
    using j_bounds(1,2) by order

  ultimately show ?thesis
    by blast
qed

fun interval_eq_false :: "ivl ⇒ ivl ⇒ bool" where
  "interval_eq_false (Ivl l1 u1) (Ivl l2 u2) =
     (¬ l1 ≤ u1 ∨ ¬ l2 ≤ u2 ∨ u1 < l2 ∨ u2 < l1)"

lemma interval_eq_false_sound:
  assumes query: "interval_eq_false a b"
      and ai: "i ∈ gamma_ivl a"
      and bj: "j ∈ gamma_ivl b"
  shows "i ≠ j"
proof -
  obtain l1 u1 where a_def: "a = Ivl l1 u1"
    by (cases a)
  obtain l2 u2 where b_def: "b = Ivl l2 u2"
    by (cases b)

  from ai have i_bounds:
    "l1 ≤ Fin i" "Fin i ≤ u1"
    unfolding a_def
    by (auto dest: gamma_ivlD)

  from bj have j_bounds:
    "l2 ≤ Fin j" "Fin j ≤ u2"
    unfolding b_def
    by (auto dest: gamma_ivlD)

  from i_bounds j_bounds have nonempty:
    "l1 ≤ u1" "l2 ≤ u2"
    by (meson order_trans)+

  with query have separated:
    "u1 < l2 ∨ u2 < l1"
    unfolding a_def b_def
    by force

  then show ?thesis
    using i_bounds(1,2) ivl_separated_not_equal j_bounds(1,2) by blast
qed

subsection ‹Goblint-style optional-Boolean queries›

text ‹
  ‹interval_less›/‹interval_eq› are the generic packaging of the four
  bound-comparison judgments above, so one interpretation both introduces
  them and discharges the query interface. The
  ⬚‹defines› clause is what keeps them ordinary top-level
  constants, with the code equation the check layer needs.
›

global_interpretation interval_numeric_queries:
  numeric_query_judgments
    interval_less_true interval_less_false interval_eq_true interval_eq_false
  defines interval_less = interval_numeric_queries.query_less
    and interval_eq = interval_numeric_queries.query_eq
  by unfold_locales
     (auto intro: interval_less_true_sound interval_eq_true_sound
            dest: interval_less_false_sound interval_eq_false_sound)


subsection ‹Semantic intersection versus raw lattice meet›

text ‹
  Unlike Sign, whose ‹SBot› is the lattice's unique empty representative, the
  raw ‹ivl› type has infinitely many non-canonical empty representations
  (any ‹Ivl l u› with ‹l > u›, documented at ‹normalize_ivl›), and only
  ‹Ivl PlusInf MinInf› is literally ‹bot›. Testing the raw
  \<^const>‹inf› against ‹bot› therefore under-approximates disjointness:
  two disjoint, non-empty finite intervals meet to an empty-but-non-canonical
  result. The witness below is disjoint by ‹interval_eq_false›'s sound table,
  yet its representation-level meet is not ‹bot›.

  The generic ‹eq_false› derived in \<^locale>‹sound_refinement›'s own context
  (\<^theory>‹Voblint_Domain.Backward_Numeric_Queries›) instead tests semantic
  intersection via @{const is_empty}. \<^const>‹intersect_ivl› returns a value
  @{const is_empty} classifies as empty on the same witness, so the generic
  derivation classifies it correctly regardless of whether that value is the
  canonical \<^const>‹bot›.
  Interval also exposes its hand-tuned query table; both operations agree on
  this disjointness witness. ‹interval_eq_true› is independent of either
  operation because it derives equality from ‹interval_less_false› in both
  directions.
›

lemma interval_meet_of_witness_not_bot:
  "Ivl (Fin 1) (Fin 2) ⊓ Ivl (Fin 5) (Fin 6) ≠ bot"
  by (simp add: bot_ivl_def)

lemma interval_intersect_of_witness_bot:
  "intersect_ivl (Ivl (Fin 1) (Fin 2)) (Ivl (Fin 5) (Fin 6)) = bot"
  by eval

end