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