introduce a generic notion of `is_idle`

analysis/facts/model/ideal/schedule.v

@@ -179,6 +179,17 @@ Section ScheduleClass.
         by move: (NS j) => /negP. }
     Qed.
 
+    (** Similarly, the generic and specific notions of idle instants
+        coincide, too. *)
+    Lemma is_idle_def :
+      forall t,
+        is_idle arr_seq sched t = ideal_is_idle sched t.
+    Proof.
+      move=> t.
+      rewrite /is_idle/ideal_is_idle -scheduled_job_at_def /scheduled_job_at.
+      by case: (scheduled_jobs_at _ _ _).
+    Qed.
+
   End RelationToGenericScheduledJob.
 
 End ScheduleClass.

analysis/facts/model/scheduled.v

@@ -103,6 +103,27 @@ Section ScheduledJobs.
       by case: (scheduled_jobs_at arr_seq sched t).
     Qed.
 
+    (** For convenience, we state a similar observation also for the [is_idle]
+        wrapper, both for the idle case ... *)
+    Corollary is_idle_iff :
+      forall t,
+        is_idle arr_seq sched t = (scheduled_job_at arr_seq sched t == None).
+    Proof.
+      move=> t; rewrite /is_idle/scheduled_job_at.
+      by case: (scheduled_jobs_at _ _ _).
+    Qed.
+
+    (** ... and the non-idle case. *)
+    Corollary is_nonidle_iff :
+      forall t,
+        ~~ is_idle arr_seq sched t <-> exists j, scheduled_at sched j t.
+    Proof.
+      move=> t. rewrite is_idle_iff.
+      split => [|[j]]; last by rewrite -scheduled_job_at_iff => ->.
+      case SJA: (scheduled_job_at _ _ _) => [j|//] _.
+      by exists j; rewrite -scheduled_job_at_iff.
+    Qed.
+
   End Uniprocessors.
 
   (** ** Case Analysis: a Scheduled Job Exists or no Job is Scheduled*)

model/schedule/scheduled.v

@@ -31,4 +31,8 @@ Section ScheduledJobs.
       that reduces the sequence of scheduled jobs to an [option Job]. *)
   Definition scheduled_job_at t := ohead (scheduled_jobs_at t).
 
+  (** We also provide a convenience wrapper to express the absence of scheduled
+      jobs. *)
+  Definition is_idle t := scheduled_jobs_at t == [::].
+
 End ScheduledJobs.