# Theory Interval

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

section ‹Intervals›

typedef (overloaded) ('a :: timestamp) ℐ = "{(i :: 'a, j :: 'a, lei :: bool, lej :: bool). 0 ≤ i ∧ i ≤ j ∧ i ∈ tfin ∧ ¬(j = 0 ∧ ¬lej)}"
by (intro exI[of _ "(0, 0, True, True)"]) (auto intro: zero_tfin)

setup_lifting type_definition_ℐ

instantiation ℐ :: (timestamp) equal begin

lift_definition equal_ℐ :: "'a ℐ ⇒ 'a ℐ ⇒ bool" is "(=)" .

instance by standard (transfer, auto)

end

lift_definition right :: "'a :: timestamp ℐ ⇒ 'a" is "fst ∘ snd" .

lift_definition memL :: "'a :: timestamp ⇒ 'a ⇒ 'a ℐ ⇒ bool" is
"λt t' (a, b, lei, lej). if lei then t + a ≤ t' else t + a < t'" .

lift_definition memR :: "'a :: timestamp ⇒ 'a ⇒ 'a ℐ ⇒ bool" is
"λt t' (a, b, lei, lej). if lej then t' ≤ t + b else t' < t + b" .

definition mem :: "'a :: timestamp ⇒ 'a ⇒ 'a ℐ ⇒ bool" where
"mem t t' I ⟷ memL t t' I ∧ memR t t' I"

lemma memL_mono: "memL t t' I ⟹ t'' ≤ t ⟹ memL t'' t' I"

lemma memL_mono': "memL t t' I ⟹ t' ≤ t'' ⟹ memL t t'' I"
by transfer (auto split: if_splits)

lemma memR_mono: "memR t t' I ⟹ t ≤ t'' ⟹ memR t'' t' I"
apply transfer
apply (simp split: prod.splits)
done

lemma memR_mono': "memR t t' I ⟹ t'' ≤ t' ⟹ memR t t'' I"
by transfer (auto split: if_splits)

lemma memR_dest: "memR t t' I ⟹ t' ≤ t + right I"
by transfer (auto split: if_splits)

lemma memR_tfin_refl:
assumes fin: "t ∈ tfin"
shows "memR t t I"
by (transfer fixing: t) (force split: if_splits intro: order_trans[OF _ add_mono, where ?x=t and ?a1=t and ?c1=0] add_pos[OF fin])

fixes x :: "'a :: timestamp"
shows "x ≤ x + right I"
by transfer (auto split: if_splits intro: order_trans[OF _ add_mono, of _ _ 0])

lift_definition interval :: "'a :: timestamp ⇒ 'a ⇒ bool ⇒ bool ⇒ 'a ℐ" is
"λi j lei lej. (if 0 ≤ i ∧ i ≤ j ∧ i ∈ tfin ∧ ¬(j = 0 ∧ ¬lej)then (i, j, lei, lej) else Code.abort (STR ''malformed interval'') (λ_. (0, 0, True, True)))"
by (auto intro: zero_tfin)

lemma "Rep_ℐ I = (l, r, b1, b2) ⟹ memL 0 0 I ⟷ l = 0 ∧ b1"
by transfer auto

lift_definition dropL :: "'a :: timestamp ℐ ⇒ 'a ℐ" is
"λ(l, r, b1, b2). (0, r, True, b2)"
by (auto intro: zero_tfin)

lemma memL_dropL: "t ≤ t' ⟹ memL t t' (dropL I)"
by transfer auto

lemma memR_dropL: "memR t t' (dropL I) = memR t t' I"
by transfer auto

lift_definition flipL :: "'a :: timestamp ℐ ⇒ 'a ℐ" is
"λ(l, r, b1, b2). if ¬(l = 0 ∧ b1) then (0, l, True, ¬b1) else Code.abort (STR ''invalid flipL'') (λ_. (0, 0, True, True))"
by (auto intro: zero_tfin split: if_splits)

lemma memL_flipL: "t ≤ t' ⟹ memL t t' (flipL I)"
by transfer (auto split: if_splits)

lemma memR_flipLD: "¬memL 0 0 I ⟹ memR t t' (flipL I) ⟹ ¬memL t t' I"
by transfer (auto split: if_splits)

lemma memR_flipLI:
fixes t :: "'a :: timestamp"
shows "(⋀u v. (u :: 'a :: timestamp) ≤ v ∨ v ≤ u) ⟹ ¬memL t t' I ⟹ memR t t' (flipL I)"
by transfer (force split: if_splits)

lemma "t ∈ tfin ⟹ memL 0 0 I ⟷ memL t t I"
apply transfer
apply (simp split: prod.splits)