%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% File Name    : event_sequences.pvs
%
% Purpose      : Defines properties of event sequences to support
%                proofs in theory interval_clocks 
%
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


event_sequences : THEORY

  BEGIN

  t: VAR real
  i, j, k: VAR nat
  f: VAR [nat -> real]

  increasing?(f): bool =
    FORALL (i:nat): f(i) < f(i + 1)
 
  unbounded?(f):bool =
    FORALL t: EXISTS k: t < f(k)

  event_sequence: TYPE =
    { f | increasing?(f) AND unbounded?(f)}

  es, es1, es2: VAR event_sequence

  increasing_ind: LEMMA %%% ONLY NEEDED FOR LEMMA nondecreasing
    es(i) < es(i + 1 + j)

  nondecreasing: LEMMA
    i <= j IMPLIES es(i) <= es(j)

  future_events(es)(t)(k): boolean = t < es(1 + k)

  future_events_nonempty: JUDGEMENT
    future_events(es)(t) HAS_TYPE (nonempty?[nat])

  index_of(es)(t): nat = min( future_events(es)(t) )
% was:  index_of(es)(t): nat = min( {k | t < es(k + 1)} )

  index_le: LEMMA
    es(0) <= t
  IMPLIES
    es(index_of(es)(t)) <= t

  lt_index: LEMMA
    t < es(index_of(es)(t) + 1)

  index_le_alt: LEMMA
    index_of(es)(t) > 0
  IMPLIES
    es(index_of(es)(t)) <= t

  index_rewrite: LEMMA
    index_of(es)(es(i)) = i

  index_conversion_left: LEMMA
    t < es(k + 1)
  IMPLIES
    index_of(es)(t) <= k

  index_conversion_right: LEMMA
    es(k) <= t
  IMPLIES
    k <= index_of(es)(t)

  index_ordered: LEMMA
      (FORALL k: es1(k) <= es2(k))
    IMPLIES
      index_of(es2)(t) <= index_of(es1)(t)

  nonoverlap?(es1, es2): bool =
    FORALL k: es1(k) <= es2(k + 1)

  cross_nondecreasing: LEMMA  %%% NOT USED
    nonoverlap?(es1, es2) AND j < k => es1(j) <= es2(k)

  nonoverlap_index_bound: LEMMA 
      nonoverlap?(es1, es2)
    IMPLIES
      index_of(es2)(t) <= index_of(es1)(t) + 1

  END event_sequences