Theory Interval_Lattice

theory Interval_Lattice
  imports "Voblint_Domain.State_Concretization" "Voblint_VIMP.VIMP_Proc"
begin

section ‹Interval lattice›

text ‹
  An interval @{text "[l, u]"} abstracts the integers @{text "{n. l ≤ n ∧ n ≤ u}"}.
  Bounds are extended integers (@{text MinInf} / @{text "Fin n"} / @{text PlusInf}).
  Empty (e.g. @{text "[+inf, -inf]"}) is @{text bot}; @{text "[-inf, +inf]"} is @{text top}.
›

subsection ‹Extended integer bounds›

text ‹
  An interval needs endpoints that can say "no lower limit" and "no upper
  limit", so ‹eint› adds ‹MinInf› and ‹PlusInf› to the integers. Ordering
  puts ‹MinInf› below and ‹PlusInf› above everything, which makes ‹eint› a
  linear order; addition and subtraction extend the integer operations, with
  the mixed-infinity cases (‹PlusInf + MinInf› and its mirror) pinned to a
  fixed choice rather than left undefined, since a total function is what
›

datatype eint = MinInf | Fin (eint_val: int) | PlusInf

fun eint_le :: "eint => eint => bool" where
    "eint_le MinInf  _       = True"
  | "eint_le _       PlusInf = True"
  | "eint_le (Fin n) (Fin m) = (n <= m)"
  | "eint_le _       MinInf  = False"
  | "eint_le PlusInf _       = False"

lemma eint_le_refl [simp]: "eint_le x x"
  by (cases x) simp_all

lemma eint_le_antisym: "eint_le x y ⟹ eint_le y x ⟹ x = y"
  by (cases x; cases y) simp_all

lemma eint_le_trans: "eint_le x y ⟹ eint_le y z ⟹ eint_le x z"
  by (cases x; cases y; cases z) simp_all

lemma eint_le_PlusInf [simp]: "eint_le x PlusInf"
  by (cases x) simp_all

lemma eint_le_MinInf_left [simp]: "eint_le MinInf x"
  by simp

lemma eint_le_linear: "eint_le x y ∨ eint_le y x"
  by (cases x; cases y) auto

instantiation eint :: ord begin
definition less_eq_eint :: "eint => eint => bool" where "less_eq_eint = eint_le"
definition less_eint    :: "eint => eint => bool" where
  "(a :: eint) < b = (eint_le a b ∧ ¬ eint_le b a)"
instance ..
end

declare less_eq_eint_def [simp]

instance eint :: linorder
proof intro_classes
  fix x y z :: eint
  show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)" unfolding less_eint_def less_eq_eint_def by simp
  show "x ≤ x"                           unfolding less_eq_eint_def by (rule eint_le_refl)
  show "x ≤ y ⟹ y ≤ z ⟹ x ≤ z"    unfolding less_eq_eint_def by (rule eint_le_trans)
  show "x ≤ y ⟹ y ≤ x ⟹ x = y"    unfolding less_eq_eint_def by (rule eint_le_antisym)
  show "x ≤ y ∨ y ≤ x"                  unfolding less_eq_eint_def by (rule eint_le_linear)
qed


instantiation eint :: plus begin
fun plus_eint :: "eint => eint => eint" where
    "plus_eint (Fin n)   (Fin m)   = Fin (n + m)"
  | "plus_eint (Fin _)   MinInf    = MinInf"
  | "plus_eint (Fin _)   PlusInf   = PlusInf"
  | "plus_eint MinInf    MinInf    = MinInf"
  | "plus_eint MinInf    (Fin _)   = MinInf"
  | "plus_eint MinInf    PlusInf   = MinInf"
  | "plus_eint PlusInf   MinInf    = PlusInf"
  | "plus_eint PlusInf   (Fin _)   = PlusInf"
  | "plus_eint PlusInf   PlusInf   = PlusInf"
instance ..
end

instantiation eint :: minus begin
fun minus_eint :: "eint => eint => eint" where
    "minus_eint (Fin n)   (Fin m)   = Fin (n - m)"
  | "minus_eint (Fin _)   MinInf    = PlusInf"
  | "minus_eint (Fin _)   PlusInf   = MinInf"
  | "minus_eint MinInf    MinInf    = MinInf"
  | "minus_eint MinInf    (Fin _)   = MinInf"
  | "minus_eint MinInf    PlusInf   = MinInf"
  | "minus_eint PlusInf   MinInf    = PlusInf"
  | "minus_eint PlusInf   (Fin _)   = PlusInf"
  | "minus_eint PlusInf   PlusInf   = PlusInf"
instance ..
end

lemma eint_le_PlusInf_iff: "eint_le PlusInf z ⟷ z = PlusInf"
  by (cases z) auto
lemma eint_le_MinInf_iff: "eint_le z MinInf ⟷ z = MinInf"
  by (cases z) auto

lemma eint_plus_mono:
  "eint_le a1 a2 ⟹ eint_le b1 b2 ⟹ eint_le (a1 + b1) (a2 + b2)"
  by (cases a1; cases a2; cases b1; cases b2; auto)

lemma eint_minus_mono:
  "eint_le a1 a2 ⟹ eint_le b2 b1 ⟹ eint_le (a1 - b1) (a2 - b2)"
  by (cases a1; cases a2; cases b1; cases b2; auto)

text ‹‹Fin› embeds ‹int› into ‹eint› as an order isomorphism onto the finite
  bounds, so it commutes with ‹min›/‹max›.›
lemma Fin_min: "Fin (min i j) = min (Fin i) (Fin j)"
  by (simp add: min_def)

lemma Fin_max: "Fin (max i j) = max (Fin i) (Fin j)"
  by (simp add: max_def)

lemma eint_min_mono:
  "eint_le a1 a2 ⟹ eint_le b1 b2 ⟹ eint_le (min a1 b1) (min a2 b2)"
  by (cases a1; cases a2; cases b1; cases b2; auto simp: min_def)

lemma eint_max_mono:
  "eint_le a1 a2 ⟹ eint_le b1 b2 ⟹ eint_le (max a1 b1) (max a2 b2)"
  by (cases a1; cases a2; cases b1; cases b2; auto simp: max_def)

subsection ‹Carrier and concretization›

text ‹
  An interval ‹Ivl l u› over extended integers denotes the integers between
  its bounds; a reversed pair denotes the empty set, so the raw carrier has many
  empty values.
›

datatype ivl = Ivl (ivl_lower: eint) (ivl_upper: eint)   ― ‹@{text "Ivl l u = [l, u]"}›

text ‹
  Named exhaustion, cited instead of ‹(cases x) auto› at every destructuring
  site. It stays untagged on purpose: its conclusion matches any term, so the
  classical reasoner would apply it to every goal.
›

lemma ivl_exhaustE:
  obtains l u where "x = Ivl l u"
  by (cases x) auto


fun gamma_ivl :: "ivl => int set" where
    "gamma_ivl (Ivl l u) = {n. l ≤ Fin n ∧ Fin n ≤ u}"

definition ivl_of_int :: "int ⇒ ivl" where
  [simp]: "ivl_of_int n = Ivl (Fin n) (Fin n)"


subsection ‹Order›

text ‹
  Interval inclusion on the bounds, with ‹Ivl PlusInf MinInf› as bottom and
  ‹ivl_top› as the unbounded interval.
›

instantiation ivl :: ord begin
definition less_eq_ivl :: "ivl => ivl => bool" where
  "(a::ivl) <= b = (case (a, b) of (Ivl l1 u1, Ivl l2 u2) => l2 ≤ l1 ∧ u1 ≤ u2)"
definition less_ivl :: "ivl => ivl => bool" where
  "(a::ivl) < b = (a <= b ∧ ¬ b <= a)"
instance ..
end

instantiation ivl :: bot begin
definition bot_ivl :: ivl where
  "bot_ivl = Ivl PlusInf MinInf"
instance ..
end

instantiation ivl :: order begin
instance proof intro_classes
  fix x y z :: ivl
  show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)"
    unfolding less_ivl_def by simp
  show "x ≤ x"
    unfolding less_eq_ivl_def by (cases x) simp
  show "x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
    unfolding less_eq_ivl_def by (cases x; cases y; cases z) (auto intro: eint_le_trans)
  show "x ≤ y ⟹ y ≤ x ⟹ x = y"
    unfolding less_eq_ivl_def by (cases x; cases y) (auto intro: eint_le_antisym)
qed
end

instantiation ivl :: order_bot begin
instance proof intro_classes
  fix x :: ivl
  show "bot ≤ x"
    unfolding less_eq_ivl_def bot_ivl_def by (cases x) simp
qed
end

definition ivl_top :: ivl where
  "ivl_top = Ivl MinInf PlusInf"

instantiation ivl :: top begin
definition "top_ivl = ivl_top"
instance ..
end

instantiation ivl :: order_top begin
instance proof intro_classes
  fix x :: ivl
  show "x ≤ top"
    unfolding top_ivl_def by (cases x) (simp add: less_eq_ivl_def ivl_top_def)
qed
end

lemma gamma_ivl_bot: "gamma_ivl bot = {}"
  unfolding bot_ivl_def by auto

lemma gamma_ivl_top: "gamma_ivl ivl_top = UNIV"
  unfolding ivl_top_def by auto

lemma gamma_ivl_mono:
  "a ≤ b ⟹ gamma_ivl a ⊆ gamma_ivl b"
proof (cases a; cases b)
  fix l1 u1 l2 u2 :: eint
  assume "a = Ivl l1 u1" "b = Ivl l2 u2" and ab: "a ≤ b"
  from ab have le: "eint_le l2 l1" "eint_le u1 u2"
    unfolding less_eq_ivl_def ‹a = Ivl l1 u1› ‹b = Ivl l2 u2› by simp_all
  show "gamma_ivl a ⊆ gamma_ivl b"
    unfolding ‹a = Ivl l1 u1› ‹b = Ivl l2 u2›
    using le by (auto intro: eint_le_trans)
qed

lemma ivl_le_top: "(x::ivl) ≤ ivl_top"
  by (cases x) (simp add: less_eq_ivl_def ivl_top_def)

subsection ‹Join›

text ‹
  The join takes the smaller lower and the larger upper bound; the lemmas prove
  it is the least upper bound and instantiate ‹semilattice_sup›.
›

fun join_ivl :: "ivl => ivl => ivl" where
    "join_ivl (Ivl l1 u1) (Ivl l2 u2) =
       Ivl (if l1 ≤ l2 then l1 else l2)
           (if u2 ≤ u1 then u1 else u2)"

lemma join_ivl_le_ub1: "(a :: ivl) ≤ join_ivl a b"
proof (cases a; cases b)
  fix l1 u1 l2 u2 :: eint
  assume "a = Ivl l1 u1" "b = Ivl l2 u2"
  then show "a ≤ join_ivl a b"
    unfolding less_eq_ivl_def
    using eint_le_linear[of l1 l2] eint_le_linear[of u1 u2]
    by auto
qed

lemma join_ivl_le_ub2: "(b :: ivl) ≤ join_ivl a b"
proof (cases a; cases b)
  fix l1 u1 l2 u2 :: eint
  assume "a = Ivl l1 u1" "b = Ivl l2 u2"
  then show "b ≤ join_ivl a b"
    unfolding less_eq_ivl_def
    using eint_le_linear[of l1 l2] eint_le_linear[of u1 u2]
    by auto
qed

lemma join_ivl_le_least:
  "(a :: ivl) ≤ c ⟹ b ≤ c ⟹ join_ivl a b ≤ c"
proof (cases a; cases b; cases c)
  fix l1 u1 l2 u2 l3 u3 :: eint
  assume "a = Ivl l1 u1" "b = Ivl l2 u2" "c = Ivl l3 u3"
    and "a ≤ c" "b ≤ c"
  then show "join_ivl a b ≤ c"
    unfolding less_eq_ivl_def by auto
qed

instantiation ivl :: sup begin
definition sup_ivl :: "ivl => ivl => ivl" where
  "sup_ivl = join_ivl"
instance ..
end

instance ivl :: semilattice_sup
proof intro_classes
  fix x y z :: ivl
  show "x ≤ x ⊔ y" unfolding sup_ivl_def by (rule join_ivl_le_ub1)
  show "y ≤ x ⊔ y" unfolding sup_ivl_def by (rule join_ivl_le_ub2)
  show "y ≤ x ⟹ z ≤ x ⟹ y ⊔ z ≤ x"
    unfolding sup_ivl_def by (rule join_ivl_le_least)
qed

instance ivl :: bounded_semilattice_sup_bot ..

subsection ‹Meet›

text ‹
  Interval intersection.  Used by @{text bfilter_ivl} to refine a variable's
  interval on a guard (@{text "x < n"} narrows the upper bound).
›
instantiation ivl :: inf begin
fun inf_ivl :: "ivl => ivl => ivl" where
    "inf_ivl (Ivl l1 u1) (Ivl l2 u2) =
       Ivl (if l2 ≤ l1 then l1 else l2)
           (if u1 ≤ u2 then u1 else u2)"
instance ..
end

lemma meet_ivl_gamma:
  "n ∈ gamma_ivl a ⟹ n ∈ gamma_ivl b ⟹ n ∈ gamma_ivl (a ⊓ b)"
  by (cases a; cases b; auto split: if_splits intro: eint_le_trans)

lemma gamma_inf_ivl [simp]:
  "gamma_ivl (a ⊓ b) = gamma_ivl a ∩ gamma_ivl b"
  apply (cases a; cases b; simp split: if_splits )
  using eint_le_linear eint_le_trans by blast+

lemma meet_ivl_le_lb1: "(a :: ivl) ⊓ b ≤ a"
proof (cases a; cases b)
  fix l1 u1 l2 u2 :: eint
  assume h: "a = Ivl l1 u1" "b = Ivl l2 u2"
  show "a ⊓ b ≤ a"
    using h eint_le_linear[of l2 l1] eint_le_linear[of u1 u2]
    by (auto simp: less_eq_ivl_def split: if_splits)
qed

lemma meet_ivl_le_lb2: "(a :: ivl) ⊓ b ≤ b"
proof (cases a; cases b)
  fix l1 u1 l2 u2 :: eint
  assume h: "a = Ivl l1 u1" "b = Ivl l2 u2"
  show "a ⊓ b ≤ b"
    using h eint_le_linear[of l1 l2] eint_le_linear[of u1 u2]
    by (auto simp: less_eq_ivl_def split: if_splits)
qed

lemma meet_ivl_greatest: "(a :: ivl) ≤ c ⟹ a ≤ b ⟹ a ≤ c ⊓ b"
proof (cases a; cases b; cases c)
  fix l1 u1 l2 u2 l3 u3 :: eint
  assume h: "a = Ivl l1 u1" "b = Ivl l2 u2" "c = Ivl l3 u3" "a ≤ c" "a ≤ b"
  show "a ≤ c ⊓ b"
    using h by (auto simp: less_eq_ivl_def split: if_splits intro: eint_le_trans)
qed

instance ivl :: semilattice_inf
proof intro_classes
  fix x y z :: ivl
  show "x ⊓ y ≤ x" by (rule meet_ivl_le_lb1)
  show "x ⊓ y ≤ y" by (rule meet_ivl_le_lb2)
  show "x ≤ y ⟹ x ≤ z ⟹ x ≤ y ⊓ z" by (rule meet_ivl_greatest)
qed

instance ivl :: lattice ..
instance ivl :: bounded_lattice_bot ..

subsection ‹Executable interface›

text ‹
  Unlike ‹bot›, ‹top› has no other representation: \<^term>‹gamma_ivl (Ivl l u)
  = UNIV› forces ‹l ≤ Fin n› and ‹Fin n ≤ u› for every ‹n›, which pins
  ‹l = MinInf› and ‹u = PlusInf› exactly --- so a direct equality test
  against \<^const>‹ivl_top› is already exact, no bound comparison needed.
›

definition is_top_ivl :: "ivl ⇒ bool" where
  "is_top_ivl i = (i = ivl_top)"

lemma is_top_ivl_correct_gamma: "is_top_ivl i ⟷ gamma_ivl i = UNIV"
  by (cases i; case_tac x1; case_tac x2)
     (auto simp add: is_top_ivl_def ivl_top_def set_eq_iff; presburger)+

text ‹
  ‹bot› is one fixed empty interval (\<^term>‹Ivl PlusInf MinInf›), but the
  ‹≤› instance's bound comparison makes ‹x ≤ bot› true only for that exact
  representation: any other inverted bound pair (e.g. a guard refinement
  narrowing a variable against its own infeasible range,
  \<^term>‹Ivl (Fin 5) (Fin (-1))›) is just as empty by @{const gamma_ivl},
  yet not ‹≤ bot› --- the instance never normalizes. ‹is_bottom_ivl› tests
  emptiness directly against the bounds instead of against one particular
  representative.

  Bound comparison alone is not quite enough, though: \<^term>‹Ivl MinInf
  MinInf› has ‹l ≤ u› (reflexively), yet no integer is "at" ‹MinInf›
  itself, so its @{const gamma_ivl} is still empty (symmetrically for
  \<^term>‹Ivl PlusInf PlusInf›). ‹l = PlusInf› and ‹u = MinInf› are exactly
  the two cases where \<^const>‹eint_le› can hold reflexively without any
  integer ever satisfying it, so both are called out explicitly alongside
  the general inverted-bounds case.
›

definition is_bottom_ivl :: "ivl ⇒ bool" where
  "is_bottom_ivl i =
     (case i of Ivl l u ⇒ l = PlusInf ∨ u = MinInf ∨ ¬ l ≤ u)"

lemma is_bottom_ivl_correct: "is_bottom_ivl i ⟷ gamma_ivl i = {}"
proof (cases i)
  case (Ivl l u)
  show ?thesis
    unfolding Ivl is_bottom_ivl_def
    by (cases l; cases u) auto
qed

text ‹
  Goblint shows an interval as ‹[l,u]›, an unconstrained end as the machine
  integer's limit in decimal; these bounds are unbounded, so it prints as ‹∞›. Every
  empty representation prints as ‹⊥›, not only \<^const>‹bot›. A standalone
  interval prints its top as ‹⊤›, as Goblint's integer-domain lifter does,
  while a product component keeps the bounds.
›

fun string_of_eint :: "eint ⇒ String.literal" where
    "string_of_eint MinInf  = STR ''-'' + sym_infinity"
  | "string_of_eint PlusInf = STR ''+'' + sym_infinity"
  | "string_of_eint (Fin n) = string_of_int n"

fun string_of_ivl :: "ivl ⇒ String.literal" where
  "string_of_ivl (Ivl l u) =
     (if is_bottom_ivl (Ivl l u) then sym_bottom
      else STR ''['' + string_of_eint l + STR '','' + string_of_eint u + STR '']'')"

subsection ‹Canonical representatives›

text ‹
  ❙‹Canonical empty interval.›  The raw \<^typ>‹ivl› lattice has infinitely many empty
  representations (any \<^term>‹Ivl l u› with ‹l > u›, or an infinite bound on the wrong
  side).  ‹normalize_ivl› collapses every empty interval to the single \<^const>‹bot›
  representative \<^term>‹Ivl PlusInf MinInf›, leaving non-empty intervals untouched.

  Arithmetic feeds its operands through ‹normalize_ivl› first.  Since the pointwise
  sum/difference of \<^const>‹bot› with anything is again \<^const>‹bot›, this keeps every empty
  result canonical.  Without it, ‹[1,0] + [1,1] = [2,1]› would manufacture ever-new empty
  representations, which as context keys defeat fixpoint convergence in the recursive
  interval example.›

definition normalize_ivl :: "ivl ⇒ ivl" where
  "normalize_ivl v =
     (case v of Ivl l u ⇒
        if l ≤ u ∧ l ≠ PlusInf ∧ u ≠ MinInf then v else bot)"

lemma normalize_ivl_gamma: "gamma_ivl (normalize_ivl v) = gamma_ivl v"
  by (cases v) (auto simp: normalize_ivl_def bot_ivl_def
        split: eint.splits if_splits intro: eint_le_trans)


lemma normalize_ivl_mono: "x ≤ y ⟹ normalize_ivl x ≤ normalize_ivl y"
  by (cases x; cases y)
     (auto simp: normalize_ivl_def less_eq_ivl_def bot_ivl_def
        eint_le_PlusInf_iff eint_le_MinInf_iff
        split: eint.splits if_splits intro: eint_le_trans)

text ‹
  Emptiness test on intervals.  The raw @{typ ivl} lattice contains many
  unnormalised empty intervals (any @{term ‹Ivl l u›} with @{text "l > u"},
  including @{term bot}).  @{text ivl_nonempty} captures exactly the intervals
  with non-empty concretization (proved below: implied by any witness, and
  monotone along @{text "≤"}); multiplication uses it for proper bottom
  handling, which is what makes the precise corner product monotone.
›
fun ivl_nonempty :: "ivl => bool" where
  "ivl_nonempty (Ivl l u) = (l ≤ u ∧ l ≠ PlusInf ∧ u ≠ MinInf)"

lemma gamma_ivl_nonempty: "i ∈ gamma_ivl v ⟹ ivl_nonempty v"
  by (cases v; cases "case v of Ivl l _ => l"; cases "case v of Ivl _ u => u"; auto)

lemma ivl_nonempty_mono: "ivl_nonempty a ⟹ a ≤ b ⟹ ivl_nonempty b"
  by (cases a; cases b; auto simp: less_eq_ivl_def intro: eint_le_trans
        elim: eint_le.elims)

text ‹
  \<^const>‹normalize_ivl› picks one representative per abstract value: non-empty
  intervals are already determined by their bounds, and every empty one collapses
  to \<^const>‹bot›.  This mirrors the component-local normalisation each Goblint
  integer domain performs for itself (@{text Interval.norm} sending ‹l > u› to
  ‹None›, @{text Congruence.normalize} pinning the residue and modulus), which is
  what makes a structural stability test on a representation meaningful.

  \<^const>‹is_bottom_ivl› stays an exact test on arbitrary bounds rather than an
  equality against \<^const>‹bot›: \<^typ>‹ivl› is an ordinary datatype, so
  \<^term>‹Ivl (Fin 5) (Fin 3)› remains writable by any caller and must still be
  recognised as empty.
›

lemma is_bottom_ivl_bot [simp]: "is_bottom_ivl bot"
  by (simp add: is_bottom_ivl_def bot_ivl_def)

lemma normalize_ivl_bot_case [simp]:
  "is_bottom_ivl v ⟹ normalize_ivl v = bot"
  by (cases v) (auto simp: normalize_ivl_def is_bottom_ivl_def)

lemma normalize_ivl_id [simp]:
  "¬ is_bottom_ivl v ⟹ normalize_ivl v = v"
  by (cases v) (simp add: normalize_ivl_def is_bottom_ivl_def)

lemma normalize_ivl_bot [simp]: "normalize_ivl bot = bot"
  by simp

lemma normalize_ivl_idem [simp]:
  "normalize_ivl (normalize_ivl v) = normalize_ivl v"
  by (cases "is_bottom_ivl v") simp_all

lemma normalize_ivl_le: "normalize_ivl v ≤ v"
  by (cases "is_bottom_ivl v") simp_all

lemma is_bottom_ivl_normalize [simp]:
  "is_bottom_ivl (normalize_ivl v) = is_bottom_ivl v"
  by (cases "is_bottom_ivl v") simp_all

definition mk_ivl :: "eint ⇒ eint ⇒ ivl" where
  [simp]: "mk_ivl l u = normalize_ivl (Ivl l u)"

text ‹
  \<^const>‹mk_ivl› is the canonical constructor: any operation that computes new
  bounds should build its result through it instead of applying \<^const>‹Ivl› to
  possibly inverted bounds and leaving the emptiness implicit.  Its defining
  equation is a simp rule, like \<^const>‹inf›'s above, so a caller that already
  rewrites with \<^const>‹normalize_ivl›'s equations sees through it rather than
  meeting an opaque constant.
›

lemma gamma_mk_ivl [simp]: "gamma_ivl (mk_ivl l u) = gamma_ivl (Ivl l u)"
  by (simp add: normalize_ivl_gamma)

lemma normalize_ivl_mk_ivl [simp]: "normalize_ivl (mk_ivl l u) = mk_ivl l u"
  by simp

lemma mk_ivl_mono:
  "Ivl l1 u1 ≤ Ivl l2 u2 ⟹ mk_ivl l1 u1 ≤ mk_ivl l2 u2"
  by (simp add: normalize_ivl_mono)

text ‹
  \<^const>‹inf› is the one operation that is deliberately left un-normalised: it
  intersects the bounds and lets an infeasible intersection come out as an
  inverted pair.
›

lemma meet_ivl_not_canonical:
  "normalize_ivl (Ivl (Fin 0) (Fin 3) ⊓ Ivl (Fin 5) (Fin 9))
     ≠ Ivl (Fin 0) (Fin 3) ⊓ Ivl (Fin 5) (Fin 9)"
  by (simp add: normalize_ivl_def bot_ivl_def)

text ‹
  Normalising it instead would break \<^class>‹semilattice_inf›: the greatest-lower-bound
  law @{thm [source] meet_ivl_greatest} quantifies over *all* lower bounds, including
  the un-normalised empty ones a caller may write down, and those are not below
  \<^const>‹bot›.  The three facts below are exactly that counterexample --
  \<^term>‹Ivl (Fin 5) (Fin 3)› is a lower bound of both operands, yet it is not below
  the normalised meet.  Canonicity therefore belongs to the operations that build
  new values (arithmetic, \<^const>‹mk_ivl›), not to the order-theoretic \<^const>‹inf›.
›

lemma meet_ivl_normalized_breaks_greatest:
  "Ivl (Fin 5) (Fin 3) ≤ Ivl (Fin 0) (Fin 3)"
  "Ivl (Fin 5) (Fin 3) ≤ Ivl (Fin 5) (Fin 9)"
  "¬ Ivl (Fin 5) (Fin 3)
       ≤ normalize_ivl (Ivl (Fin 0) (Fin 3) ⊓ Ivl (Fin 5) (Fin 9))"
  by (simp_all add: less_eq_ivl_def normalize_ivl_def bot_ivl_def)

subsection ‹Semantic intersection›

text ‹
  ‹intersect_ivl› is the intersection a backward filter uses, distinct from
  the order's ‹inf› on this raw carrier.
›

definition intersect_ivl :: "ivl ⇒ ivl ⇒ ivl" where
  [simp]: "intersect_ivl a b = normalize_ivl (a ⊓ b)"

text ‹
  \<^const>‹inf› is the greatest lower bound of the representation order; the
  operation a backward filter actually wants is the intersection of the
  concretizations, which is a weaker requirement --- it need only preserve
  \<^const>‹gamma_ivl› and be reductive and monotone, and is free to pick any
  representative of the result. \<^const>‹intersect_ivl› is that operation:
  it normalizes the bound intersection so an infeasible result becomes
  \<^const>‹bot› rather than a reversed pair.

  Goblint's interval @{text meet} is simultaneously both, because its carrier
  keeps only canonical inhabited values --- @{text norm} maps ‹l > u› to
  @{text None}, so no element corresponding to \<^term>‹Ivl (Fin 5) (Fin 3)›
  exists there to be a common lower bound. On this larger raw carrier the two
  notions come apart, which is what
  @{thm [source] meet_ivl_normalized_breaks_greatest} records.
›

lemma gamma_intersect_ivl [simp]:
  "gamma_ivl (intersect_ivl a b) = gamma_ivl (a ⊓ b)"
  by (simp add: normalize_ivl_gamma)

lemma intersect_ivl_gamma:
  "n ∈ gamma_ivl a ⟹ n ∈ gamma_ivl b ⟹ n ∈ gamma_ivl (intersect_ivl a b)"
  using meet_ivl_gamma[of n a b] by (simp add: normalize_ivl_gamma)

lemma intersect_ivl_le1: "intersect_ivl a b ≤ a"
proof -
  have "normalize_ivl (a ⊓ b) ≤ a ⊓ b" by (rule normalize_ivl_le)
  also have "a ⊓ b ≤ a" using meet_ivl_le_lb1[of a b] by simp
  finally show ?thesis by simp
qed

lemma intersect_ivl_le2: "intersect_ivl a b ≤ b"
proof -
  have "normalize_ivl (a ⊓ b) ≤ a ⊓ b" by (rule normalize_ivl_le)
  also have "a ⊓ b ≤ b" using meet_ivl_le_lb2[of a b] by simp
  finally show ?thesis by simp
qed

lemma intersect_ivl_mono:
  assumes "a1 ≤ a2" and "b1 ≤ b2"
  shows "intersect_ivl a1 b1 ≤ intersect_ivl a2 b2"
proof -
  have "a1 ⊓ b1 ≤ a2 ⊓ b2" using inf_mono[OF assms] by simp
  then show ?thesis by (simp add: normalize_ivl_mono)
qed

lemma normalize_ivl_intersect_ivl [simp]:
  "normalize_ivl (intersect_ivl a b) = intersect_ivl a b"
  by simp

end