Theory Interval

(*
  File: Interval.thy
  Author: Bohua Zhan
*)

section ‹Intervals›

theory Interval
  imports "Auto2_HOL.Auto2_Main"
begin

text ‹Basic definition of intervals.›

subsection ‹Definition of interval›

datatype 'a interval = Interval (low: 'a) (high: 'a)
setup ‹add_simple_datatype "interval"›

instantiation interval :: (linorder) linorder begin

definition int_less: "(a < b) = (low a < low b | (low a = low b ∧ high a < high b))"
definition int_less_eq: "(a ≤ b) = (low a < low b | (low a = low b ∧ high a ≤ high b))"

instance proof
  fix x y z :: "'a interval"
  show a: "(x < y) = (x ≤ y ∧ ¬ y ≤ x)"
    using int_less int_less_eq by force
  show b: "x ≤ x"
    by (simp add: int_less_eq)
  show c: "x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
    by (smt int_less_eq dual_order.trans less_trans)
  show d: "x ≤ y ⟹ y ≤ x ⟹ x = y"
    using int_less_eq a interval.expand int_less by fastforce
  show e: "x ≤ y ∨ y ≤ x"
    by (meson int_less_eq leI not_less_iff_gr_or_eq)
qed end

definition is_interval :: "('a::linorder) interval ⇒ bool" where [rewrite]:
  "is_interval it ⟷ (low it ≤ high it)"

subsection ‹Definition of interval with an index›

datatype 'a idx_interval = IdxInterval (int: "'a interval") (idx: nat)
setup ‹add_simple_datatype "idx_interval"›

instantiation idx_interval :: (linorder) linorder begin

definition iint_less: "(a < b) = (int a < int b | (int a = int b ∧ idx a < idx b))"
definition iint_less_eq: "(a ≤ b) = (int a < int b | (int a = int b ∧ idx a ≤ idx b))"

instance proof
  fix x y z :: "'a idx_interval"
  show a: "(x < y) = (x ≤ y ∧ ¬ y ≤ x)"
    using iint_less iint_less_eq by force
  show b: "x ≤ x"
    by (simp add: iint_less_eq)
  show c: "x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
    by (smt iint_less_eq dual_order.trans less_trans)
  show d: "x ≤ y ⟹ y ≤ x ⟹ x = y"
    using a idx_interval.expand iint_less iint_less_eq by auto
  show e: "x ≤ y ∨ y ≤ x"
    by (meson iint_less_eq leI not_less_iff_gr_or_eq)
qed end

lemma interval_less_to_le_low [forward]:
  "(a::('a::linorder idx_interval)) < b ⟹ low (int a) ≤ low (int b)"
  by (metis eq_iff iint_less int_less less_imp_le)

subsection ‹Overlapping intervals›

definition is_overlap :: "('a::linorder) interval ⇒ 'a interval ⇒ bool" where [rewrite]:
  "is_overlap x y ⟷ (high x ≥ low y ∧ high y ≥ low x)"

definition has_overlap :: "('a::linorder) idx_interval set ⇒ 'a interval ⇒ bool" where [rewrite]:
  "has_overlap xs y ⟷ (∃x∈xs. is_overlap (int x) y)"

end