Library rt.restructuring.behavior.facts.ideal_schedule

(* Note: we do not re-export the basic definitions to avoid littering the global
   namespace with type class instances. *)

(* In this section we estlish the classes to which an ideal schedule belongs. *)
Section ScheduleClass.
  (* Consider any job type and the ideal processor model. *)
  Context {Job: JobType}.

  (* We note that the ideal processor model is a uniprocessor
     model. *)
  Lemma ideal_proc_model_is_a_uniprocessor_model:
    @uniprocessor_model _ (processor_state Job) _.

  (* We observe that the ideal processor model falls into the category
     of ideal-progress models, i.e., a scheduled job always receives
     service. *)
  Lemma ideal_proc_model_ensures_ideal_progress:
    @ideal_progress_proc_model _ (processor_state Job) _.

End ScheduleClass.