Theory Interval

(*<*)
theory Interval
  imports "HOL-Library.Extended_Nat" "HOL-Library.Product_Lexorder"
begin
(*>*)

section ‹Intervals›

typedef ℐ = "{(i :: nat, j :: enat). i ≤ j}"
  by (intro exI[of _ "(0, ∞)"]) auto

setup_lifting type_definition_ℐ

instantiation ℐ :: equal begin
lift_definition equal_ℐ :: "ℐ ⇒ ℐ ⇒ bool" is "(=)" .
instance by standard (transfer, auto)
end

instantiation ℐ :: linorder begin
lift_definition less_eq_ℐ :: "ℐ ⇒ ℐ ⇒ bool" is "(≤)" .
lift_definition less_ℐ :: "ℐ ⇒ ℐ ⇒ bool" is "(<)" .
instance by standard (transfer, auto)+
end


lift_definition all :: ℐ is "(0, ∞)" by simp
lift_definition left :: "ℐ ⇒ nat" is fst .
lift_definition right :: "ℐ ⇒ enat" is snd .
lift_definition point :: "nat ⇒ ℐ" is "λn. (n, enat n)" by simp
lift_definition init :: "nat ⇒ ℐ" is "λn. (0, enat n)" by auto
abbreviation mem where "mem n I ≡ (left I ≤ n ∧ n ≤ right I)"
lift_definition subtract :: "nat ⇒ ℐ ⇒ ℐ" is
  "λn (i, j). (i - n, j - enat n)" by (auto simp: diff_enat_def split: enat.splits)
lift_definition add :: "nat ⇒ ℐ ⇒ ℐ" is
  "λn (a, b). (a, b + enat n)" by (auto simp add: add_increasing2)

lemma left_right: "left I ≤ right I"
  by transfer auto

lemma point_simps[simp]:
  "left (point n) = n"
  "right (point n) = n"
  by (transfer; auto)+

lemma init_simps[simp]:
  "left (init n) = 0"
  "right (init n) = n"
  by (transfer; auto)+

lemma subtract_simps[simp]:
  "left (subtract n I) = left I - n"
  "right (subtract n I) = right I - n"
  "subtract 0 I = I"
  "subtract x (point y) = point (y - x)"
  by (transfer; auto)+

definition shifted :: "ℐ ⇒ ℐ set" where
  "shifted I = (λn. subtract n I) ` {0 .. (case right I of ∞ ⇒ left I | enat n ⇒ n)}"

lemma subtract_too_much: "i > (case right I of ∞ ⇒ left I | enat n ⇒ n) ⟹
  subtract i I = subtract (case right I of ∞ ⇒ left I | enat n ⇒ n) I"
  by transfer (auto split: enat.splits)

lemma subtract_shifted: "subtract n I ∈ shifted I"
  by (cases "n ≤ (case right I of ∞ ⇒ left I | enat n ⇒ n)")
    (auto simp: shifted_def subtract_too_much)

lemma finite_shifted: "finite (shifted I)"
  unfolding shifted_def by auto

definition interval :: "nat ⇒ enat ⇒ ℐ" where
  "interval l r = (if l ≤ r then Abs_ℐ (l, r) else undefined)"

lemma [code abstract]: "Rep_ℐ (interval l r) = (if l ≤ r then (l, r) else Rep_ℐ undefined)"
  unfolding interval_def using Abs_ℐ_inverse by simp

(*<*)
end
(*>*)