Quelle  Interval.thy

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

section ‹Intervals›

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

setup_lifting type_definition_I

instantiation I :: equal begin
lift_definition equal_I :: "I ==> I ==> bool" is "(=)" .
instance by standard (transfer, auto)
end

instantiation I :: linorder begin
lift_definition less_eq_I :: "I ==> I ==> bool" is "(≤)" .
lift_definition less_I :: "I ==> I ==> bool" is "(<)" .
instance by standard (transfer, auto)+
end


lift_definition all :: I is "(0, ∞)" by simp
lift_definition left :: "I ==> nat" is fst .
lift_definition right :: "I ==> enat" is snd .
lift_definition point :: "nat ==> I" is "λn. (n, enat n)" by simp
lift_definition init :: "nat ==> I" is "λn. (0, enat n)" by auto
abbreviation mem where "mem n I ≡ (left I ≤ n ∧ n ≤ right I)"
lift_definition subtract :: "nat ==> I ==> I" is
  "λn (i, j). (i - n, j - enat n)" by (auto simp: diff_enat_def split: enat.splits)
lift_definition add :: "nat ==> I ==> I" 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 :: "I ==> I 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 ==> I" where
  "interval l r = (if l ≤ r then Abs_I (l, r) else undefined)"

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

(*<*)
end
(*>*)