Theory Int_Backward

theory Int_Backward
  imports
    Int_Arithmetic
    "Voblint_Analysis_Sign.Sign_Numeric_Queries"
    "Voblint_Analysis_Parity.Parity_Backward"
    "Voblint_Analysis_Parity.Parity_Numeric_Queries"
    "Voblint_Analysis_Congruence.Congruence_Backward"
begin

section ‹Composite integer-domain backward filtering›

text ‹
  Composite backward inversion follows the same shape as composite forward
  arithmetic (‹Int_Arithmetic›): a raw componentwise operator, reusing
  each component's own existing inverse where one exists, then a mode-aware
  wrapper that refines the returned candidates with ‹refine mode›.

  No component here invents a new inverse operator. Sign and Interval both
  already fall back to the shared identity ‹inv_conservative› for
  ‹+›/‹-›/‹*› in their own theories (‹Sign_Backward›,
  ‹Interval_Backward›); this composite reuses that same choice rather
  than inventing per-component arithmetic inversion the domains themselves
  do not have. Parity and Congruence invert arithmetic in their own theories,
  and the composite reuses both: ‹inv_plus_parity›, ‹inv_minus_parity›,
  ‹inv_times_parity› (‹Parity_Backward›) and ‹inv_plus_congruence›,
  ‹inv_minus_congruence›, ‹inv_times_congruence› (‹Congruence_Backward›).
  A comparison leaves the Parity component unchanged, as Parity's own ‹less›
  inverse does; an equality narrows it through the composite
  ‹intersect_int_dom› on the true branch below.

  Precision Sign and Interval cannot recover directly at inversion time
  is not lost: the mode-aware wrapper's ‹refine mode› step re-derives
  their bounds from the (possibly Congruence-tightened) returned operand,
  exactly as ‹refine_interval›/‹refine_congruence› already do for
  forward arithmetic.
›

subsection ‹Composite semantic intersection›

definition intersect_int_dom :: "int_dom => int_dom => int_dom" where
  "intersect_int_dom d1 d2 =
     d1⦇
       int_sign := int_sign d1 ⊓ int_sign d2,
       int_ivl := intersect_ivl (int_ivl d1) (int_ivl d2),
       int_parity := int_parity d1 ⊓ int_parity d2,
       int_congruence := int_congruence d1 ⊓ int_congruence d2
     ⦈"

text ‹
  ‹intersect_ivl›'s defining equation is globally tagged ‹[simp]›
  (‹Interval_Lattice›), so plain ‹simp›/‹auto› unfolds it to
  ‹normalize_ivl (a ⊓ b)› before ‹gamma_intersect_ivl_exact› or
  ‹intersect_ivl_le1›/‹intersect_ivl_le2›/‹intersect_ivl_mono› -- all
  stated in terms of the abstract ‹intersect_ivl› -- get a chance to match.
  ‹del: intersect_ivl_def› below keeps ‹intersect_ivl› opaque for exactly
  those calls, matching ‹is_bottom_int_dom_correct›'s own
  ‹simp only: gamma_intersect_ivl_exact ...› workaround in
  ‹Int_Lattice›.
›

lemma intersect_int_dom_sound:
  assumes "n ∈ gamma_int_dom a" and "n ∈ gamma_int_dom b"
  shows "n ∈ gamma_int_dom (intersect_int_dom a b)"
proof -
  have hn: "n ∈ gamma_sign (int_sign a)" "n ∈ gamma_ivl (int_ivl a)"
           "n ∈ gamma_parity (int_parity a)" "n ∈ gamma_congruence (int_congruence a)"
    using assms(1) by (simp_all add: gamma_int_dom_def)
  have hm: "n ∈ gamma_sign (int_sign b)" "n ∈ gamma_ivl (int_ivl b)"
           "n ∈ gamma_parity (int_parity b)" "n ∈ gamma_congruence (int_congruence b)"
    using assms(2) by (simp_all add: gamma_int_dom_def)
  have ivl_fact: "n ∈ gamma_ivl (intersect_ivl (int_ivl a) (int_ivl b))"
    unfolding intersect_ivl_def
    using meet_ivl_gamma[OF hn(2) hm(2)] normalize_ivl_gamma by simp
  have sign_fact: "n ∈ gamma_sign (int_sign a ⊓ int_sign b)"
    using hn(1) hm(1) by simp
  have parity_fact: "n ∈ gamma_parity (int_parity a ⊓ int_parity b)"
    using hn(3) hm(3) by simp
  have congruence_fact:
    "n ∈ gamma_congruence (int_congruence a ⊓ int_congruence b)"
    using hn(4) hm(4) by simp
  show ?thesis
    unfolding gamma_int_dom_def intersect_int_dom_def
    using sign_fact ivl_fact parity_fact congruence_fact
    by (simp del: intersect_ivl_def)
qed

lemma intersect_int_dom_le1: "intersect_int_dom a b ≤ a"
  unfolding intersect_int_dom_def less_eq_int_dom_ext_def
  by (simp add: inf_le1 intersect_ivl_le1
      del: intersect_ivl_def)

lemma intersect_int_dom_le2: "intersect_int_dom a b ≤ b"
  unfolding intersect_int_dom_def less_eq_int_dom_ext_def
  by (simp add: inf_le2 intersect_ivl_le2
      del: intersect_ivl_def)

lemma intersect_int_dom_mono:
  assumes "a1 ≤ a2" and "b1 ≤ b2"
  shows "intersect_int_dom a1 b1 ≤ intersect_int_dom a2 b2"
proof -
  have s: "int_sign a1 ≤ int_sign a2" "int_ivl a1 ≤ int_ivl a2"
          "int_parity a1 ≤ int_parity a2" "int_congruence a1 ≤ int_congruence a2"
    using assms(1) by (simp_all add: less_eq_int_dom_ext_def)
  have t: "int_sign b1 ≤ int_sign b2" "int_ivl b1 ≤ int_ivl b2"
          "int_parity b1 ≤ int_parity b2" "int_congruence b1 ≤ int_congruence b2"
    using assms(2) by (simp_all add: less_eq_int_dom_ext_def)
  show ?thesis
    unfolding intersect_int_dom_def less_eq_int_dom_ext_def
    using s t
    by (simp add: intersect_ivl_mono[OF s(2) t(2)] le_infI1 le_infI2
        del: intersect_ivl_def)
qed

definition intersect_int_dom_mode ::
    "refine_mode => int_dom => int_dom => int_dom"
where
  "intersect_int_dom_mode mode a b = refine mode (intersect_int_dom a b)"

lemma intersect_int_dom_mode_sound:
  assumes "n ∈ gamma_int_dom a" and "n ∈ gamma_int_dom b"
  shows "n ∈ gamma_int_dom (intersect_int_dom_mode mode a b)"
  unfolding intersect_int_dom_mode_def
  using intersect_int_dom_sound[OF assms] refine_exact by simp

text ‹
  ‹refine mode› is reductive/exact for every mode (‹Int_Refinement›)
  but only monotone off ‹Refine_Fixpoint› (‹Int_Arithmetic›'s
  ‹refine_nonfixpoint_mono›); these two helpers compose that fact with a
  reductive/monotone step once, for ‹intersect_int_dom_mode› and the
  mode-aware inverse operators below.
›

lemma refine_mode_reductive_trans:
  assumes "a ≤ d"
  shows "refine mode a ≤ d"
  using refine_reductive[of mode a] assms by (rule order_trans)

lemma refine_mode_mono_trans:
  assumes "mode ≠ Refine_Fixpoint" and "a ≤ b"
  shows "refine mode a ≤ refine mode b"
  using monoD[OF refine_nonfixpoint_mono[OF assms(1)] assms(2)] .

lemma intersect_int_dom_mode_reductive1:
  "intersect_int_dom_mode mode a b ≤ a"
  unfolding intersect_int_dom_mode_def
  using refine_mode_reductive_trans[OF intersect_int_dom_le1] .

lemma intersect_int_dom_mode_reductive2:
  "intersect_int_dom_mode mode a b ≤ b"
  unfolding intersect_int_dom_mode_def
  using refine_mode_reductive_trans[OF intersect_int_dom_le2] .

lemma intersect_int_dom_mode_mono:
  assumes "mode ≠ Refine_Fixpoint" and "a1 ≤ a2" and "b1 ≤ b2"
  shows "intersect_int_dom_mode mode a1 b1 ≤ intersect_int_dom_mode mode a2 b2"
  unfolding intersect_int_dom_mode_def
  using refine_mode_mono_trans[OF assms(1) intersect_int_dom_mono[OF assms(2,3)]] .


subsection ‹Raw componentwise inverse operators›

text ‹
  The raw inverses run each component's backward operator on its own field and
  reassemble the record. A component with no useful inverse goes through
  ‹inv_conservative›, and a true equality intersects both operands with
  ‹intersect_int_dom›.
›

definition inv_less_int_dom_raw ::
    "bool => int_dom => int_dom => int_dom * int_dom"
where
  "inv_less_int_dom_raw res d1 d2 =
     (let (s1, s2) = inv_less_sign res (int_sign d1) (int_sign d2);
          (i1, i2) = inv_less_ivl res (int_ivl d1) (int_ivl d2);
          (c1, c2) = inv_less_congruence res (int_congruence d1) (int_congruence d2)
      in
        (d1⦇int_sign := s1, int_ivl := i1, int_congruence := c1⦈,
         d2⦇int_sign := s2, int_ivl := i2, int_congruence := c2⦈))"

definition inv_eq_int_dom_raw ::
    "bool => int_dom => int_dom => int_dom * int_dom"
where
  "inv_eq_int_dom_raw res d1 d2 =
     (if res then (intersect_int_dom d1 d2, intersect_int_dom d1 d2)
      else
        (let (s1, s2) = inv_eq_sign False (int_sign d1) (int_sign d2);
             (i1, i2) = inv_eq_ivl False (int_ivl d1) (int_ivl d2);
             (c1, c2) = inv_eq_congruence False (int_congruence d1) (int_congruence d2)
         in
           (d1⦇int_sign := s1, int_ivl := i1, int_congruence := c1⦈,
            d2⦇int_sign := s2, int_ivl := i2, int_congruence := c2⦈)))"

definition inv_plus_int_dom_raw ::
    "int_dom => int_dom => int_dom => int_dom * int_dom"
where
  "inv_plus_int_dom_raw r d1 d2 =
     (let (s1, s2) = inv_conservative (int_sign r) (int_sign d1) (int_sign d2);
          (i1, i2) = inv_conservative (int_ivl r) (int_ivl d1) (int_ivl d2);
          (p1, p2) = inv_plus_parity (int_parity r) (int_parity d1) (int_parity d2);
          (c1, c2) =
            inv_plus_congruence (int_congruence r) (int_congruence d1) (int_congruence d2)
      in
        (d1⦇int_sign := s1, int_ivl := i1, int_parity := p1, int_congruence := c1⦈,
         d2⦇int_sign := s2, int_ivl := i2, int_parity := p2, int_congruence := c2⦈))"

definition inv_minus_int_dom_raw ::
    "int_dom => int_dom => int_dom => int_dom * int_dom"
where
  "inv_minus_int_dom_raw r d1 d2 =
     (let (s1, s2) = inv_conservative (int_sign r) (int_sign d1) (int_sign d2);
          (i1, i2) = inv_conservative (int_ivl r) (int_ivl d1) (int_ivl d2);
          (p1, p2) = inv_minus_parity (int_parity r) (int_parity d1) (int_parity d2);
          (c1, c2) =
            inv_minus_congruence (int_congruence r) (int_congruence d1) (int_congruence d2)
      in
        (d1⦇int_sign := s1, int_ivl := i1, int_parity := p1, int_congruence := c1⦈,
         d2⦇int_sign := s2, int_ivl := i2, int_parity := p2, int_congruence := c2⦈))"

definition inv_times_int_dom_raw ::
    "int_dom => int_dom => int_dom => int_dom * int_dom"
where
  "inv_times_int_dom_raw r d1 d2 =
     (let (s1, s2) = inv_conservative (int_sign r) (int_sign d1) (int_sign d2);
          (i1, i2) = inv_conservative (int_ivl r) (int_ivl d1) (int_ivl d2);
          (p1, p2) = inv_times_parity (int_parity r) (int_parity d1) (int_parity d2);
          (c1, c2) =
            inv_times_congruence (int_congruence r) (int_congruence d1) (int_congruence d2)
      in
        (d1⦇int_sign := s1, int_ivl := i1, int_parity := p1, int_congruence := c1⦈,
         d2⦇int_sign := s2, int_ivl := i2, int_parity := p2, int_congruence := c2⦈))"


subsection ‹Raw soundness›

text ‹
  A raw inverse keeps every concrete operand pair consistent with the observed
  outcome: if ‹x› and ‹y› lie in the inputs and produce the comparison result or
  the value in ‹r›, they lie in the refined pair. Each proof cites the component
  soundness lemmas.
›

lemma inv_less_int_dom_raw_sound:
  assumes "x ∈ gamma_int_dom d1" and "y ∈ gamma_int_dom d2" and "(x < y) = res"
  shows
    "x ∈ gamma_int_dom (fst (inv_less_int_dom_raw res d1 d2)) ∧
     y ∈ gamma_int_dom (snd (inv_less_int_dom_raw res d1 d2))"
  using assms(1,2) inv_less_sign_sound[OF _ _ assms(3)] inv_less_ivl_sound[OF _ _ assms(3)]
  by (simp add: inv_less_int_dom_raw_def Let_def case_prod_beta gamma_int_dom_def
      inv_less_congruence_def)

lemma inv_eq_int_dom_raw_sound:
  assumes "x ∈ gamma_int_dom d1" and "y ∈ gamma_int_dom d2" and "(x = y) = res"
  shows
    "x ∈ gamma_int_dom (fst (inv_eq_int_dom_raw res d1 d2)) ∧
     y ∈ gamma_int_dom (snd (inv_eq_int_dom_raw res d1 d2))"
proof (cases res)
  case True
  then show ?thesis
    using assms intersect_int_dom_sound[OF assms(1), of d2] by (simp add: inv_eq_int_dom_raw_def)
next
  case False
  then show ?thesis
    using assms(1,2) inv_eq_sign_sound[OF _ _ assms(3)] inv_eq_ivl_sound[OF _ _ assms(3)]
      inv_eq_congruence_sound[OF _ _ assms(3)]
    by (simp add: inv_eq_int_dom_raw_def Let_def case_prod_beta gamma_int_dom_def
        del: inv_eq_sign.simps)
qed

lemma inv_plus_int_dom_raw_sound:
  assumes "x ∈ gamma_int_dom d1" and "y ∈ gamma_int_dom d2" and "x + y ∈ gamma_int_dom r"
  shows
    "x ∈ gamma_int_dom (fst (inv_plus_int_dom_raw r d1 d2)) ∧
     y ∈ gamma_int_dom (snd (inv_plus_int_dom_raw r d1 d2))"
  using assms inv_plus_congruence_sound[of x _ y _ "int_congruence r"]
    inv_plus_parity_sound[of x _ y _ "int_parity r"]
  by (simp add: inv_plus_int_dom_raw_def Let_def case_prod_beta gamma_int_dom_def
      inv_conservative_def)

lemma inv_minus_int_dom_raw_sound:
  assumes "x ∈ gamma_int_dom d1" and "y ∈ gamma_int_dom d2" and "x - y ∈ gamma_int_dom r"
  shows
    "x ∈ gamma_int_dom (fst (inv_minus_int_dom_raw r d1 d2)) ∧
     y ∈ gamma_int_dom (snd (inv_minus_int_dom_raw r d1 d2))"
  using assms inv_minus_congruence_sound[of x _ y _ "int_congruence r"]
    inv_minus_parity_sound[of x _ y _ "int_parity r"]
  by (simp add: inv_minus_int_dom_raw_def Let_def case_prod_beta gamma_int_dom_def
      inv_conservative_def)

lemma inv_times_int_dom_raw_sound:
  assumes "x ∈ gamma_int_dom d1" and "y ∈ gamma_int_dom d2" and "x * y ∈ gamma_int_dom r"
  shows
    "x ∈ gamma_int_dom (fst (inv_times_int_dom_raw r d1 d2)) ∧
     y ∈ gamma_int_dom (snd (inv_times_int_dom_raw r d1 d2))"
  using assms inv_times_congruence_sound[of x _ y _ "int_congruence r"]
    inv_times_parity_sound[of x _ y _ "int_parity r"]
  by (simp add: inv_times_int_dom_raw_def Let_def case_prod_beta gamma_int_dom_def
      inv_conservative_def)


subsection ‹Raw monotonicity›

text ‹
  The raw inverses are monotone in every argument, stated as ‹le_pair› on the
  refined pair and proved from the componentwise monotonicity lemmas.
›

lemma inv_less_int_dom_raw_mono:
  assumes "d1 ≤ d2" and "e1 ≤ e2"
  shows "le_pair (inv_less_int_dom_raw res d1 e1) (inv_less_int_dom_raw res d2 e2)"
  using assms
  by (simp add: inv_less_int_dom_raw_def Let_def case_prod_beta less_eq_int_dom_ext_def
      inv_less_sign_mono inv_less_ivl_mono inv_less_congruence_def)

lemma inv_eq_int_dom_raw_mono:
  assumes "d1 ≤ d2" and "e1 ≤ e2"
  shows "le_pair (inv_eq_int_dom_raw res d1 e1) (inv_eq_int_dom_raw res d2 e2)"
proof (cases res)
  case True
  then show ?thesis
    using intersect_int_dom_mono[OF assms] by (simp add: inv_eq_int_dom_raw_def)
next
  case False
  then show ?thesis
    using assms
    by (simp add: inv_eq_int_dom_raw_def Let_def case_prod_beta less_eq_int_dom_ext_def
        inv_eq_sign_mono inv_eq_ivl_mono inv_eq_congruence_mono del: inv_eq_sign.simps)
qed

lemma inv_plus_int_dom_raw_mono:
  assumes "r1 ≤ r2" and "d1 ≤ d2" and "e1 ≤ e2"
  shows "le_pair (inv_plus_int_dom_raw r1 d1 e1) (inv_plus_int_dom_raw r2 d2 e2)"
  using assms
  by (simp add: inv_plus_int_dom_raw_def Let_def case_prod_beta less_eq_int_dom_ext_def
      inv_conservative_def inv_plus_congruence_mono inv_plus_parity_mono)

lemma inv_minus_int_dom_raw_mono:
  assumes "r1 ≤ r2" and "d1 ≤ d2" and "e1 ≤ e2"
  shows "le_pair (inv_minus_int_dom_raw r1 d1 e1) (inv_minus_int_dom_raw r2 d2 e2)"
  using assms
  by (simp add: inv_minus_int_dom_raw_def Let_def case_prod_beta less_eq_int_dom_ext_def
      inv_conservative_def inv_minus_congruence_mono inv_minus_parity_mono)

lemma inv_times_int_dom_raw_mono:
  assumes "r1 ≤ r2" and "d1 ≤ d2" and "e1 ≤ e2"
  shows "le_pair (inv_times_int_dom_raw r1 d1 e1) (inv_times_int_dom_raw r2 d2 e2)"
  using assms
  by (simp add: inv_times_int_dom_raw_def Let_def case_prod_beta less_eq_int_dom_ext_def
      inv_conservative_def inv_times_congruence_mono inv_times_parity_mono)


subsection ‹Mode-aware wrappers›

text ‹
  ‹inv_less_int_dom› and its siblings apply ‹refine mode› to both halves of the
  raw result, so backward filtering follows the same refinement policy as the
  forward arithmetic.
›

definition inv_less_int_dom ::
    "refine_mode => bool => int_dom => int_dom => int_dom * int_dom"
where
  "inv_less_int_dom mode res d1 d2 =
     (let (r1, r2) = inv_less_int_dom_raw res d1 d2
      in (refine mode r1, refine mode r2))"

definition inv_eq_int_dom ::
    "refine_mode => bool => int_dom => int_dom => int_dom * int_dom"
where
  "inv_eq_int_dom mode res d1 d2 =
     (let (r1, r2) = inv_eq_int_dom_raw res d1 d2
      in (refine mode r1, refine mode r2))"

definition inv_plus_int_dom ::
    "refine_mode => int_dom => int_dom => int_dom => int_dom * int_dom"
where
  "inv_plus_int_dom mode r d1 d2 =
     (let (r1, r2) = inv_plus_int_dom_raw r d1 d2
      in (refine mode r1, refine mode r2))"

definition inv_minus_int_dom ::
    "refine_mode => int_dom => int_dom => int_dom => int_dom * int_dom"
where
  "inv_minus_int_dom mode r d1 d2 =
     (let (r1, r2) = inv_minus_int_dom_raw r d1 d2
      in (refine mode r1, refine mode r2))"

definition inv_times_int_dom ::
    "refine_mode => int_dom => int_dom => int_dom => int_dom * int_dom"
where
  "inv_times_int_dom mode r d1 d2 =
     (let (r1, r2) = inv_times_int_dom_raw r d1 d2
      in (refine mode r1, refine mode r2))"


text ‹
  Each wrapper refines both raw candidates, so its soundness and monotonicity
  reduce to the raw operator's through ‹refine_exact› and
  ‹refine_nonfixpoint_mono›.
›

lemma inv_int_dom_map_prod:
  "inv_less_int_dom mode res d1 d2 =
     map_prod (refine mode) (refine mode) (inv_less_int_dom_raw res d1 d2)"
  "inv_eq_int_dom mode res d1 d2 =
     map_prod (refine mode) (refine mode) (inv_eq_int_dom_raw res d1 d2)"
  "inv_plus_int_dom mode r d1 d2 =
     map_prod (refine mode) (refine mode) (inv_plus_int_dom_raw r d1 d2)"
  "inv_minus_int_dom mode r d1 d2 =
     map_prod (refine mode) (refine mode) (inv_minus_int_dom_raw r d1 d2)"
  "inv_times_int_dom mode r d1 d2 =
     map_prod (refine mode) (refine mode) (inv_times_int_dom_raw r d1 d2)"
  by (simp_all add: inv_less_int_dom_def inv_eq_int_dom_def inv_plus_int_dom_def
      inv_minus_int_dom_def inv_times_int_dom_def map_prod_def case_prod_beta)


subsection ‹Backward-domain interpretation›

text ‹
  Soundness and the reductiveness of ‹intersect› hold at every mode, so every
  mode interprets @{locale sound_refinement} and shares the precise,
  dead-arm-eliminating ‹branch›/‹branch_st›. Monotonicity needs
  ‹mode ≠ Refine_Fixpoint›: ‹refine_fix›'s total wrapper has no monotonicity
  theorem (‹Int_Refinement›), a faithful transliteration of Goblint's
  ‹fixpoint› loop. So ‹Refine_Never› and ‹Refine_Once› interpret the full
  @{locale mono_refinement}, and ‹Refine_Fixpoint› stays out of reach of
  ‹branch_mono› and the rest of the monotonicity layer.
›

lemma int_backward_domain:
  "sound_refinement (intersect_int_dom_mode mode) (aval_int_dom mode) int_dom_tobool
     (inv_less_int_dom mode) (inv_eq_int_dom mode)
     (inv_plus_int_dom mode) (inv_minus_int_dom mode) (inv_times_int_dom mode)"
proof (intro sound_refinement.intro sound_intersection.intro
    int_dom_sound_evaluator mono_truth_test.axioms(1)[OF int_dom_truth_test]
    sound_inverse_ops.intro sound_inverse_ops_axioms.intro)
qed (simp_all add: inv_int_dom_map_prod refine_exact intersect_int_dom_mode_sound
       inv_less_int_dom_raw_sound inv_eq_int_dom_raw_sound inv_plus_int_dom_raw_sound
       inv_minus_int_dom_raw_sound inv_times_int_dom_raw_sound
       intersect_int_dom_mode_reductive1 intersect_int_dom_mode_reductive2)

lemma int_dom_backward_domain_mono:
  assumes "mode ≠ Refine_Fixpoint"
  shows
    "mono_refinement (intersect_int_dom_mode mode) (aval_int_dom mode) int_dom_tobool
       (inv_less_int_dom mode) (inv_eq_int_dom mode)
       (inv_plus_int_dom mode) (inv_minus_int_dom mode) (inv_times_int_dom mode)"
proof (intro mono_refinement.intro int_backward_domain
    int_dom_mono_evaluator[OF assms] int_dom_truth_test mono_refinement_axioms.intro
    mono_intersection.intro mono_intersection_axioms.intro
    sound_intersection.intro)
qed (auto simp: assms inv_int_dom_map_prod refine_mode_mono_trans intersect_int_dom_mode_mono
       refine_exact intersect_int_dom_mode_sound
       intersect_int_dom_mode_reductive1 intersect_int_dom_mode_reductive2
       inv_less_int_dom_raw_mono inv_eq_int_dom_raw_mono
       inv_plus_int_dom_raw_mono inv_minus_int_dom_raw_mono inv_times_int_dom_raw_mono)

subsection ‹The refinement operations, per mode›

text ‹
  The three refinement modes differ only in how often the four components are
  reduced against each other, so one record parametric in the mode carries all
  three. The guard filters and the branch are derived from it in ‹Int_Transfer›.
›

definition int_refine_ops :: "refine_mode ⇒ int_dom refine_ops" where
  "int_refine_ops mode =
     ⦇r_tobool = int_dom_tobool, r_inv_less = inv_less_int_dom mode,
      r_inv_eq = inv_eq_int_dom mode, r_inv_plus = inv_plus_int_dom mode,
      r_inv_minus = inv_minus_int_dom mode, r_inv_times = inv_times_int_dom mode,
      r_intersect = intersect_int_dom_mode mode⦈"

lemma int_refine_ops_simps [simp]:
  "r_tobool (int_refine_ops mode) = int_dom_tobool"
  "r_inv_less (int_refine_ops mode) = inv_less_int_dom mode"
  "r_inv_eq (int_refine_ops mode) = inv_eq_int_dom mode"
  "r_inv_plus (int_refine_ops mode) = inv_plus_int_dom mode"
  "r_inv_minus (int_refine_ops mode) = inv_minus_int_dom mode"
  "r_inv_times (int_refine_ops mode) = inv_times_int_dom mode"
  "r_intersect (int_refine_ops mode) = intersect_int_dom_mode mode"
  by (simp_all add: int_refine_ops_def)

subsection ‹Comparison queries›

text ‹
  A comparison is answered component by component, as Goblint's
  ‹IntDomTuple› answers ‹lt› and ‹eq›: it is decided when some component
  decides it on its own value, and no step here combines the components. The
  refinement mode therefore reaches a comparison only through its operands,
  which \<^const>‹aval_int_dom› reduces as the mode says; under
  \<^const>‹Refine_Never› a fact that only the reduced product knows is not
  available to a check.
›

definition int_less_true :: "int_dom ⇒ int_dom ⇒ bool" where
  "int_less_true a b ⟷
     sign_less_true (int_sign a) (int_sign b)
     ∨ interval_less_true (int_ivl a) (int_ivl b)
     ∨ parity_less_true (int_parity a) (int_parity b)
     ∨ congruence_lt (int_congruence a) (int_congruence b) = Some True"

definition int_less_false :: "int_dom ⇒ int_dom ⇒ bool" where
  "int_less_false a b ⟷
     sign_less_false (int_sign a) (int_sign b)
     ∨ interval_less_false (int_ivl a) (int_ivl b)
     ∨ parity_less_false (int_parity a) (int_parity b)
     ∨ congruence_lt (int_congruence a) (int_congruence b) = Some False"

definition int_eq_true :: "int_dom ⇒ int_dom ⇒ bool" where
  "int_eq_true a b ⟷
     sign_eq_true (int_sign a) (int_sign b)
     ∨ interval_eq_true (int_ivl a) (int_ivl b)
     ∨ parity_eq_true (int_parity a) (int_parity b)
     ∨ congruence_eqb (int_congruence a) (int_congruence b) = Some True"

definition int_eq_false :: "int_dom ⇒ int_dom ⇒ bool" where
  "int_eq_false a b ⟷
     sign_eq_false (int_sign a) (int_sign b)
     ∨ interval_eq_false (int_ivl a) (int_ivl b)
     ∨ parity_eq_false (int_parity a) (int_parity b)
     ∨ congruence_eqb (int_congruence a) (int_congruence b) = Some False"

lemma gamma_int_dom_components:
  assumes "i ∈ γ (a :: int_dom)"
  shows "i ∈ gamma_sign (int_sign a)" "i ∈ gamma_ivl (int_ivl a)"
    "i ∈ gamma_parity (int_parity a)" "i ∈ gamma_congruence (int_congruence a)"
  using assms by (simp_all add: gamma_int_dom_def)

lemma int_less_true_sound:
  assumes "int_less_true a b" and "i ∈ γ a" and "j ∈ γ b"
  shows "i < j"
  using assms(1) gamma_int_dom_components[OF assms(2)] gamma_int_dom_components[OF assms(3)]
  unfolding int_less_true_def
  by (auto dest: sign_less_true_sound interval_less_true_sound parity_less_true_sound
      congruence_lt_sound)

lemma int_less_false_sound:
  assumes "int_less_false a b" and "i ∈ γ a" and "j ∈ γ b"
  shows "¬ i < j"
  using assms(1) gamma_int_dom_components[OF assms(2)] gamma_int_dom_components[OF assms(3)]
  unfolding int_less_false_def
  by (auto dest: sign_less_false_sound interval_less_false_sound parity_less_false_sound
      congruence_lt_sound)

lemma int_eq_true_sound:
  assumes "int_eq_true a b" and "i ∈ γ a" and "j ∈ γ b"
  shows "i = j"
  using assms(1) gamma_int_dom_components[OF assms(2)] gamma_int_dom_components[OF assms(3)]
  unfolding int_eq_true_def
  by (auto dest: sign_eq_true_sound interval_eq_true_sound parity_eq_true_sound
      congruence_eqb_sound)

lemma int_eq_false_sound:
  assumes "int_eq_false a b" and "i ∈ γ a" and "j ∈ γ b"
  shows "i ≠ j"
  using assms(1) gamma_int_dom_components[OF assms(2)] gamma_int_dom_components[OF assms(3)]
  unfolding int_eq_false_def
  by (auto dest: sign_eq_false_sound interval_eq_false_sound parity_eq_false_sound
      congruence_eqb_sound)

global_interpretation int_dom_numeric_queries:
  numeric_query_judgments int_less_true int_less_false int_eq_true int_eq_false
  defines int_less = int_dom_numeric_queries.query_less
    and int_eq = int_dom_numeric_queries.query_eq
  by unfold_locales
     (fact int_less_true_sound, fact int_less_false_sound,
      fact int_eq_true_sound, fact int_eq_false_sound)

end