Require Export prosa.model.processor.platform_properties.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.model.processor.restricted_supply.

(** In this section we establish the classes to which a
    restricted-supply schedule belongs. *)
Section ScheduleClass.

  Local Transparent scheduled_in scheduled_on service_on.

  (** We assume a restricted-supply uni-processor schedule. *)
  #[local] Existing Instance rs_processor_state.

  (** Consider any job type and the ideal processor model. *)
  Context {Job: JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

  (** We note that the restricted-supply processor model is indeed a
      uni-processor model. *)
  Lemma rs_proc_model_is_a_uniprocessor_model :
    uniprocessor_model (rs_processor_state Job).
Job: JobType
H: JobArrival Job
H0: JobCost Job
uniprocessor_model (rs_processor_state Job)
  Proof.
Job: JobType
H: JobArrival Job
H0: JobCost Job
uniprocessor_model (rs_processor_state Job)
    move=> j1 j2 sched t  /existsP[[]/eqP E1] /existsP[[]/eqP E2].
Job: JobType
H: JobArrival Job
H0: JobCost Job
j1, j2: Job
sched: schedule (rs_processor_state Job)
t: instant
E1: scheduled_on j1 (sched t) tt == true
E2: scheduled_on j2 (sched t) tt == true
j1 = j2
    by move: E1 E2; case (sched t) => //= => j /eqP /eqP -> /eqP /eqP ->.
  Qed.

  (** Restricted-supply processor model is unit-supply. *)
  Lemma rs_proc_is_unit_supply :
    unit_supply_proc_model (rs_processor_state Job).
Job: JobType
H: JobArrival Job
H0: JobCost Job
unit_supply_proc_model (rs_processor_state Job)
  Proof.
Job: JobType
H: JobArrival Job
H0: JobCost Job
unit_supply_proc_model (rs_processor_state Job)
    move=> sched.
Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: rs_processor_state Job
supply_in sched <= 1
    by rewrite /supply_in sum_unit1; case: sched.
  Qed.

  (** Restricted-supply processor model is a fully supply-consuming
      processor model. *)
  Lemma rs_proc_model_fully_consuming :
    fully_consuming_proc_model (rs_processor_state Job).
Job: JobType
H: JobArrival Job
H0: JobCost Job
fully_consuming_proc_model (rs_processor_state Job)
  Proof.
Job: JobType
H: JobArrival Job
H0: JobCost Job
fully_consuming_proc_model (rs_processor_state Job)
    move=> j S t.
Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
S: schedule (rs_processor_state Job)
t: instant
scheduled_at S j t -> service_at S j t = supply_at S t
    rewrite /scheduled_at /scheduled_in /service_at /supply_at /supply_in /service_in !sum_unit1.
Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
S: schedule (rs_processor_state Job)
t: instant
[exists c, scheduled_on j (S t) c] ->
service_on j (S t) tt = supply_on (S t) tt
    case (S t) => //=.
Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
S: schedule (rs_processor_state Job)
t: instant
[exists c, false] -> 0 = 1
Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
S: schedule (rs_processor_state Job)
t: instant
forall j0 : Job,
[exists c, j0 == j] -> (if j0 == j then 1 else 0) = 1
    -
Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
S: schedule (rs_processor_state Job)
t: instant
[exists c, false] -> 0 = 1 by move => /existsP [] => //.
    -
Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
S: schedule (rs_processor_state Job)
t: instant
forall j0 : Job,
[exists c, j0 == j] -> (if j0 == j then 1 else 0) = 1 by move => jo /existsP [_ /eqP ->]; rewrite eq_refl.
  Qed.

End ScheduleClass.

(** * Automation *)
(** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq
    will be able to apply them automatically. *)
Global Hint Resolve
       rs_proc_model_is_a_uniprocessor_model
       rs_proc_is_unit_supply
       rs_proc_model_fully_consuming : basic_rt_facts.