Library PAutomata.Time

Require Export ZArith.

Parameter Time : Set.
Parameter T0 : Time.
Parameter T1 : Time.
Parameter Tplus : Time -> Time -> Time.
Parameter Tmult : Time -> Time -> Time.
Parameter Topp : Time -> Time.
Parameter Tlt : Time -> Time -> Prop.

Definition Tle (r1 r2 : Time) : Prop := Tlt r1 r2 \/ r1 = r2.
Definition Tge (r1 r2 : Time) : Prop := Tle r2 r1.
Definition Tgt (r1 r2 : Time) : Prop := Tlt r2 r1.

Hint Unfold Tle Tge Tgt: time.

Definition Tminus (r1 r2 : Time) : Time := Tplus r1 (Topp r2).


Axiom Tplus_sym : forall r1 r2 : Time, Tplus r1 r2 = Tplus r2 r1.

Axiom
  Tplus_assoc :
    forall r1 r2 r3 : Time, Tplus (Tplus r1 r2) r3 = Tplus r1 (Tplus r2 r3).

Axiom Tplus_Topp_r : forall r : Time, Tplus r (Topp r) = T0.

Hint Resolve Tplus_sym Tplus_Topp_r: time.

Axiom Tplus_T0_r : forall r : Time, Tplus r T0 = r.

Lemma Tplus_T0_l : forall r : Time, Tplus T0 r = r.
intro; rewrite Tplus_sym; apply Tplus_T0_r.
Qed.

Hint Resolve Tplus_T0_r Tplus_T0_l: time.



Axiom
  total_order : forall r1 r2 : Time, {Tlt r1 r2} + {r1 = r2} + {Tlt r2 r1}.


Axiom Tlt_antisym : forall r1 r2 : Time, Tlt r1 r2 -> ~ Tlt r2 r1.

Axiom Tlt_trans : forall r1 r2 r3 : Time, Tlt r1 r2 -> Tlt r2 r3 -> Tlt r1 r3.

Axiom
  Tlt_compatibility_l :
    forall r r1 r2 : Time, Tlt r1 r2 -> Tlt (Tplus r r1) (Tplus r r2).

Axiom Tlt_T0_T1 : Tlt T0 T1.

Hint Resolve Tlt_T0_T1 Tlt_trans Tlt_compatibility_l Tlt_antisym: time.


Fixpoint INTime (n : nat) : Time :=
  match n with
  | O => T0
  | S O => T1
  | S n => Tplus (INTime n) T1
  end.


Definition IZTime (z : Z) : Time :=
  match z with
  | Z0 => T0
  | Zpos n => INTime (nat_of_P n)
  | Zneg n => Topp (INTime (nat_of_P n))
  end.


Axiom Tmult_sym : forall r1 r2 : Time, Tmult r1 r2 = Tmult r2 r1.

Axiom
  Tmult_assoc :
    forall r1 r2 r3 : Time, Tmult (Tmult r1 r2) r3 = Tmult r1 (Tmult r2 r3).

Hint Resolve Tmult_sym Tmult_assoc: time.

Axiom Tmult_T0_r : forall r : Time, Tmult r T0 = T0.

Lemma Tmult_T0_l : forall r : Time, Tmult T0 r = T0.
intro; rewrite Tmult_sym; apply Tmult_T0_r.
Qed.

Axiom Tmult_T1_r : forall r : Time, Tmult r T1 = r.

Lemma Tmult_T1_l : forall r : Time, Tmult T1 r = r.
intro; rewrite Tmult_sym; apply Tmult_T1_r.
Qed.

Hint Resolve Tmult_T0_r Tmult_T0_l: time.