Port instantiations

restructuring/analysis/abstract/fixed_priority/nonpr_reg/concrete_models/preemptive_run_to_compl.v

+From rt.util Require Export epsilon.
+From rt.restructuring.behavior Require Import job schedule.
+From rt.restructuring.model Require Import job task.
+From rt.restructuring.model.preemption Require Export preemption_model run_to_completion_threshold.
+
+(* TODO: fix comment *)
+Section FullyPreemptiveRTC.
+
+  (* Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+
+  (*  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+  Context `{JobPreemptable Job}.
+
+  (* TODO: comment *)
+  Instance fully_preemptive : TaskRunToCompletionThreshold Task :=
+    fun tsk => task_cost tsk.
+
+  
+  (* Consider any arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (* Assume that a job cost cannot be larger than a task cost. *)
+  Hypothesis H_job_cost_le_task_cost:
+    cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+
+  (* TODO: comment *)
+  Lemma fully_preemptive_valid_task_run_to_completion_threshold:
+    forall tsk, valid_task_run_to_completion_threshold arr_seq tsk.
+  Proof.
+    intros; split.
+    - by rewrite /task_run_to_completion_threshold_le_task_cost.
+    - intros j ARR TSK.
+      apply leq_trans with (job_cost j); first by done.
+        by rewrite-TSK; apply H_job_cost_le_task_cost.
+  Qed.
+    
+End FullyPreemptiveRTC.
+
+Hint Resolve fully_preemptive_valid_task_run_to_completion_threshold.
\ No newline at end of file