Theory Backward_Numeric_Queries

theory Backward_Numeric_Queries
  imports Backward_Domain Numeric_Queries
begin

section ‹Queries derived from backward inversion›

text ‹
  Any @{locale sound_inverse_ops} instance already proves ‹inv_less_sound›/
  ‹intersect_sound›, so it answers entailment/refutation of
  ‹<›/‹=› over two atomic values for free: narrowing under an assumed truth
  value yields an @{const is_empty} component only if no represented witness
  pair can satisfy that assumption. Thus emptiness of the inverse result gives
  a sound entailment/refutation test, though an imprecise inverse may still
  answer "unknown" even when the relation is already concrete-semantically
  fixed. The four judgments need the inverse operators and nothing about
  states, so they are defined in @{locale sound_inverse_ops}'s own context; every
  @{locale sound_refinement} interpretation extends it and gets them with no
  restated proof obligation. Turning the four into the
  two queries a caller asks for is not backward-specific and is not done
  here: this file ends by interpreting
  \<^locale>‹numeric_query_judgments› at them, so every
  @{locale sound_inverse_ops} instance is a numeric-query instance too.

  Classification tests @{const is_empty}, not canonical-‹bot› equality: a value
  can denote ‹{}› without being the representation's chosen ‹bot› element
  (@{class numeric_domain}'s whole reason for distinguishing the two), so a
  ‹= bot› test would under-classify any domain with non-canonical empty
  representations. ‹less_true›/‹less_false›/‹eq_true›/‹eq_false› stay implementation
  judgments, not the public interface \<^theory>‹Voblint_Domain.Numeric_Queries›
  gives: a caller after the generic default wants ‹less›/‹eq›; these four
  remain named and proved because ‹Sign_Backward› and ‹Int_Classify› cite
  them directly off a concrete @{locale sound_refinement} interpretation to
  state that a domain's own sharper, hand-tuned query agrees with this
  generic default.
›

context sound_inverse_ops
begin

subsection ‹Comparison judgments›

text ‹A comparison is decided by narrowing against its own negation: if refining the two
  values under ‹¬ a < b› empties either side, no concrete pair can violate ‹a < b›, so the
  judgment holds.  Nothing new is assumed of the domain -- the answer comes from the
  narrowing operator it already supplies.›
definition less_true :: "'a ⇒ 'a ⇒ bool" where
  "less_true a b ⟷ is_empty (fst (inv_less False a b)) ∨ is_empty (snd (inv_less False a b))"

definition less_false :: "'a ⇒ 'a ⇒ bool" where
  "less_false a b ⟷ is_empty (fst (inv_less True a b)) ∨ is_empty (snd (inv_less True a b))"

lemma less_true_sound:
  assumes "less_true a b" and "i ∈ γ a" and "j ∈ γ b"
  shows "i < j"
  using assms inv_less_sound[OF assms(2,3), of False]
  unfolding less_true_def
  by (auto simp: is_empty_correct)

lemma less_false_sound:
  assumes "less_false a b" and "i ∈ γ a" and "j ∈ γ b"
  shows "¬ i < j"
  using assms inv_less_sound[OF assms(2,3), of True]
  unfolding less_false_def
  by (auto simp: is_empty_correct)

subsection ‹Equality judgments›

text ‹
  Two independent derivations, from different existing capabilities:
  ‹eq_true› from ‹less_false› in both directions (integer trichotomy -- if
  every pair is provably ‹¬ i < j› and every pair is provably ‹¬ j < i›,
  every pair is ‹i = j›); ‹eq_false› from ‹intersect› (a common witness
  would belong to its concretization, so an @{const is_empty} intersection
  rules one out).
›

definition eq_true :: "'a ⇒ 'a ⇒ bool" where
  "eq_true a b ⟷ less_false a b ∧ less_false b a"

lemma eq_true_sound:
  assumes "eq_true a b" and "i ∈ γ a" and "j ∈ γ b"
  shows "i = j"
  using assms less_false_sound[of a b i j] less_false_sound[of b a j i]
  unfolding eq_true_def
  by fastforce

definition eq_false :: "'a ⇒ 'a ⇒ bool" where
  "eq_false a b ⟷ is_empty (intersect a b)"

lemma eq_false_sound:
  assumes "eq_false a b" and "i ∈ γ a" and "j ∈ γ b"
  shows "i ≠ j"
  using assms intersect_sound
  unfolding eq_false_def
  by (fastforce simp: is_empty_correct)

end

subsection ‹Packaging the derived judgments›

text ‹
  The qualifier is mandatory rather than cosmetic: the packaging locale
  assumes the same four soundness statements this context proves, under the
  same four names, so an unqualified registration would try to declare each
  twice in every @{command global_interpretation} of
  @{locale sound_inverse_ops}.
›

sublocale sound_inverse_ops ⊆ queries:
  numeric_query_judgments less_true less_false eq_true eq_false
  by unfold_locales
     (fact less_true_sound, fact less_false_sound, fact eq_true_sound, fact eq_false_sound)

end