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

section ‹Intervals›

typedef (overloaded) ('a :: timestamp) I = "{(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_I

instantiation I :: (timestamp) equal begin

lift_definition equal_I :: "'a I → 'a I → bool" is "(=)" .

instance by standard (transfer, auto)

end

lift_definition right :: "'a :: timestamp I → 'a" is "fst ∘ snd" .

lift_definition memL :: "'a :: timestamp → 'a → 'a I → 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 I → bool" is
  "λt t' (a, b, lei, lej). if lej then t' ≤ t + b else t' < t + b" .

definition mem :: "'a :: timestamp → 'a → 'a I → 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"
  by transfer (auto simp: add.commute order_le_less_subst2 order_subst2 add_mono split: if_splits)

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)
  apply (meson add_mono_comm dual_order.trans order_less_le_trans)
  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])

lemma right_I_add_mono:
  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 I" 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 I = (l, r, b1, b2) ==> memL 0 0 I ⟷ l = 0 ∧ b1"
  by transfer auto

lift_definition dropL :: "'a :: timestamp I → 'a I" 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 I → 'a I" 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)
  apply (metis add.right_neutral add_pos antisym_conv2 dual_order.eq_iff order_less_imp_not_less)
  done

definition "full (I :: ('a :: timestamp) I) ⟷ (∀t t'. 0 ≤ t ∧ t ≤ t' ∧ t ∈ tfin ∧ t' ∈ tfin ⟶ mem t t' I)"

lemma "memL 0 0 (I :: ('a :: timestamp_total) I) ==> right I ∉ tfin ==> full I"
  unfolding full_def mem_def
  by transfer (fastforce split: if_splits dest: add_not_tfin)

(*<*)
end
(*>*)