Equivalence of EDF Predicates

This MR connects the two ways with which one can specify that a schedule is an EDF schedule in PROSA: the EDF_schedule predicate and the respects_policy_at_preemption_point - given the EDF priority policy - predicate. We connect these two predicates by showing that they're equivalent. We then restate the optimality proof of EDF schedules using the proven equivalence.

analysis/facts/edf_definitions.v

@@ -52,9 +52,9 @@ Section Equivalence.
   Hypothesis H_no_deadline_misses: all_deadlines_of_arrivals_met arr_seq sched.
 
   (** We first show that a schedule that satisfies the ad-hoc [EDF_schedule]
-      predicate is also compliant with the EDF policy in the sense of Prosa's
-      "proper" notion of scheduling policy, namely the
-      [respects_policy_at_preemption_point] predicate. *)
+      predicate is also compliant with the generic notion of EDF policy 
+      defined in Prosa, namely the [respects_policy_at_preemption_point] 
+      predicate. *)
   Lemma EDF_schedule_implies_respects_policy_at_preemption_point :
     EDF_schedule sched ->
     respects_policy_at_preemption_point arr_seq sched.