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

lemma add_mono_comm:
  fixes a :: 'a
  shows "c ≤ d ⟹ c + a ≤ d + a"
  by (auto simp: add.commute add_mono)

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 - {-∞, ∞}"

lemma ereal_add_pos:
  fixes a :: ereal
  shows "a ∈ tfin ⟹ 0 < c ⟹ a < a + c"
  by (auto simp: tfin_ereal_def) (metis add.right_neutral ereal_add_cancel_left ereal_le_add_self order_less_le)

instance
  by standard (auto simp add: ι_ereal_def tfin_ereal_def add.commute ereal_add_le_add_iff2 not_le
      less_PInf_Ex_of_nat ereal_less_ereal_Ex reals_Archimedean2 intro: ereal_add_pos)

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"
  by (metis add_0_left local.add_mono_comm timestamp_tfin_le_not_tfin dual_order.order_iff_strict dual_order.strict_trans1)

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

instantiation prod :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
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