(******************************************************************)
(*                  Probabilistic Analysis of DFTs in IN HOL4     *)
(*                                                                *)
(*                      Copyright 2018, Yassmeen Elderhalli       *)
(*                                                                *)
(*                      Contact: y_elderh@encs.concordia.ca       *)
(*                                                                *)
(******************************************************************)

INSTALLATION:

Requirement: HOL4 "Kanaskis" 12, polyml 5.7 

1) Download "Required-Theories.zip"
   This archive contains some required theories including
   - The extreal, measure and probability theories developed by Tarek Mhamdi for extended real datatypes 
   - The lebesgue measure theory and some other theories ported (from HOL light and Isablle/HOL) by Mohamed Qasim
   - The PIE_EXTREAL theory developed by Waqar Ahmad

2) Download "DFT-Thoeries.zip"

   This archive contains:
   - integration_before_afterScript.sml which has the Pr (X < Y /\ Y <=t) and Pr (X < Y /\ X <=t)
   - DFT_Gates_de_PROBScript.sml which has the definitions of the gates, their probabilities and the simplification theorems
   - WCSPScript.sml which has the probabilistic behavior for the Warm and Cold spare gates.
   - Holmakefile which is required to include the path for the "Required-Theories"  directory, 
     the path in the file should be changed to point to the path of the "required-Theories" directory


3) run Holmake to build the theories in the Required-Theories and DFT-Theories directories

4) Below are the names of the definitions and theorems that correspond to the definitions, lemmas and theorems in the paper:

--------------------Identity Elements Definitions-------------------------

Always element: ALWAYS_def
Never element: NEVER_def

----------------------- Operators Definitions-----------------------------

Before operator: D_BEFORE_def
Simultaneous operator: D_SIMULT_def
Inclusive Before operator: D_INCLUSIVE_BEFORE_def

--------------------------Gates Definitions-------------------------------

AND gate:  D_AND_def
OR gate:   D_OR_def
Priority AND gate: P_AND_def
Functional dependency gate: FDEP_def
Hot spare gate (HSP): HSP_def
Cold spare gate (CSP): CSP_def
Warm spare gate (WSP): WSP_def 
shared spare gate: shared_spare_def

--------------------Definitions, Lemmas and Theorems in Paper--------------

Definition 4.1: DFT_event_def
Definition 4.4: rv_gt0_ninfty_def
Definition 4.5: All_distinct_events_def
Definition 4.6: distributed_def 
Definition 4.7: den_gt0_ninfty_def
Definition 4.8: cond_density_def


Lemma 4.1: AND_INTER
Lemma 4.2: OR_UNION
Lemma 4.3: indicator_of_indicator_after
Lemma 4.4: after_set_BIGUNION_Q
Lemma 4.5: after_set_BIGUNION_IN_MESURABLE_SETS
Lemma 4.6: after_set_IN_MEASURABLE_SETS_PAIR_lborel
Lemma 4.7: lemma3_indicator_mul_after
Lemma 4.8: DFT_event_AFTER_PREIMAGE_GT0
Lemma 4.9: indicator_of_indicator_before
Lemma 4.10: BEFORE_PREIMAGE_event_GT0
Lemma 4.11: CSP_PREIMAGE_event_GT0
Lemma 4.12: CSP_indicator_of_indicator
Lemma 4.13: WSP_DFT_event

Theorem 3.1: PAND_DEF2
Theorem 3.2: FDEP_OR
Theorem 3.3: HSP_AND
Theorem 4.1: CDF_prob_DFT_event
Theorem 4.2: PROB_AND
Theorem 4.3: PROB_OR
Theorem 4.4: PROB_DFT_AFTER
Theorem 4.5: PROB_DFT_BEFORE
Theorem 4.6: distribution_lebesgue_thm2_pos_fn
Theorem 4.7: MEASURE_SPACE_BIGUNION_Q
Theorem 4.8: prob_CSP
Theorem 4.9: prob_WSP
Theorem 4.10: cond_density_joint_marginal
Theorem 4.11: prob_joint_density_iterated_integrals
Theorem 4.12: prob_joint_conditional_density