# Theory Timestamp

```theory Timestamp
imports "HOL-Library.Extended_Nat" "HOL-Library.Extended_Real"
begin

class embed_nat =
fixes ι :: "nat ⇒ 'a"

class tfin =
fixes tfin :: "'a set"

class timestamp = comm_monoid_add + semilattice_sup + embed_nat + tfin +
assumes ι_mono: "⋀i j. i ≤ j ⟹ ι i ≤ ι j"
and ι_tfin: "⋀i. ι i ∈ tfin"
and ι_progressing: "x ∈ tfin ⟹ ∃j. ¬ι j ≤ ι i + x"
and zero_tfin: "0 ∈ tfin"
and tfin_closed: "c ∈ tfin ⟹ d ∈ tfin ⟹ c + d ∈ tfin"
and add_mono: "c ≤ d ⟹ a + c ≤ a + d"
and add_pos: "a ∈ tfin ⟹ 0 < c ⟹ a < a + c"
begin

fixes a :: 'a
shows "c ≤ d ⟹ c + a ≤ d + a"

end

(* Extending time domain with infinity (None). *)

instantiation option :: (timestamp) timestamp
begin

definition tfin_option :: "'a option set" where
"tfin_option = Some ` tfin"

definition ι_option :: "nat ⇒ 'a option" where
"ι_option = Some ∘ ι"

definition zero_option :: "'a option" where
"zero_option = Some 0"

definition plus_option :: "'a option ⇒ 'a option ⇒ 'a option" where
"plus_option x y = (case x of None ⇒ None | Some x' ⇒ (case y of None ⇒ None | Some y' ⇒ Some (x' + y')))"

definition sup_option :: "'a option ⇒ 'a option ⇒ 'a option" where
"sup_option x y = (case x of None ⇒ None | Some x' ⇒ (case y of None ⇒ None | Some y' ⇒ Some (sup x' y')))"

definition less_option :: "'a option ⇒ 'a option ⇒ bool" where
"less_option x y = (case x of None ⇒ False | Some x' ⇒ (case y of None ⇒ True | Some y' ⇒ x' < y'))"

definition less_eq_option :: "'a option ⇒ 'a option ⇒ bool" where
"less_eq_option x y = (case x of None ⇒ x = y | Some x' ⇒ (case y of None ⇒ True | Some y' ⇒ x' ≤ y'))"

instance
apply standard
apply (auto simp: plus_option_def add.assoc split: option.splits)[1]
apply (auto simp: plus_option_def add.commute split: option.splits)[1]
apply (auto simp: zero_option_def plus_option_def split: option.splits)[1]
apply (auto simp: less_option_def less_eq_option_def split: option.splits)[1]
apply (auto simp: less_eq_option_def split: option.splits)[3]
apply (auto simp: sup_option_def less_eq_option_def split: option.splits)[3]
apply (auto simp: ι_option_def less_eq_option_def intro: ι_mono)[1]
apply (auto simp: tfin_option_def ι_option_def intro: ι_tfin)[1]
apply (auto simp: tfin_option_def ι_option_def plus_option_def less_eq_option_def intro: ι_progressing)[1]
apply (auto simp: tfin_option_def zero_option_def intro: zero_tfin)[1]
apply (auto simp: tfin_option_def plus_option_def intro: tfin_closed)[1]
apply (auto simp: plus_option_def less_eq_option_def intro: add_mono split: option.splits)[1]
apply (auto simp: tfin_option_def zero_option_def plus_option_def less_option_def intro: add_pos split: option.splits)
done

end

instantiation enat :: timestamp
begin

definition tfin_enat :: "enat set" where
"tfin_enat = UNIV - {∞}"

definition ι_enat :: "nat ⇒ enat" where
"ι_enat n = n"

instance
by standard (auto simp add: ι_enat_def tfin_enat_def dest!: leD)

end

instantiation ereal :: timestamp
begin

definition ι_ereal :: "nat ⇒ ereal" where
"ι_ereal n = ereal n"

definition tfin_ereal :: "ereal set" where
"tfin_ereal = UNIV - {-∞, ∞}"

fixes a :: ereal
shows "a ∈ tfin ⟹ 0 < c ⟹ a < a + c"

instance

end

class timestamp_total = timestamp +
assumes timestamp_total: "a ≤ b ∨ b ≤ a"
assumes timestamp_tfin_le_not_tfin: "0 ≤ a ⟹ a ∈ tfin ⟹ 0 ≤ b ⟹ b ∉ tfin ⟹ a ≤ b"
begin

lemma add_not_tfin: "0 ≤ a ⟹ a ∈ tfin ⟹ a ≤ c ⟹ c ∈ tfin ⟹ 0 ≤ b ⟹ b ∉ tfin ⟹ c < a + b"

end

instantiation enat :: timestamp_total
begin

instance
by standard (auto simp: tfin_enat_def)

end

instantiation ereal :: timestamp_total
begin

instance
by standard (auto simp: tfin_ereal_def)

end

class timestamp_strict = timestamp +
assumes add_mono_strict: "c < d ⟹ a + c < a + d"

class timestamp_total_strict = timestamp_total + timestamp_strict

instantiation nat :: timestamp_total_strict
begin

definition tfin_nat :: "nat set" where
"tfin_nat = UNIV"

definition ι_nat :: "nat ⇒ nat" where
"ι_nat n = n"

instance
by standard (auto simp: tfin_nat_def ι_nat_def dest!: leD)

end

instantiation real :: timestamp_total_strict
begin

definition tfin_real :: "real set" where "tfin_real = UNIV"

definition ι_real :: "nat ⇒ real" where "ι_real n = real n"

instance
by standard (auto simp: tfin_real_def ι_real_def not_le reals_Archimedean2)

end

begin

definition zero_prod :: "'a × 'b" where
"zero_prod = (0, 0)"

fun plus_prod :: "'a × 'b ⇒ 'a × 'b ⇒ 'a × 'b" where
"(a, b) + (c, d) = (a + c, b + d)"

instance
by standard (auto simp: zero_prod_def ac_simps)

end

end
```