(*------------------------------------------------------ *) (* Formal Fault Tree Analysis in Higher-order Logic *) (* *) (* by Waqar Ahmed *) (* Phd Candidate *) (* School of Electrical Engineering and Computer Sciences *) (* National University of Sciences and Technology (NUST) *) (* Islamabad, Pakistan *) (*---------------------------------------------------------*) app load ["arithmeticTheory", "realTheory", "prim_recTheory", "seqTheory", "pred_setTheory","res_quanTheory", "res_quanTools", "listTheory", "probabilityTheory", "numTheory", "transcTheory", "rich_listTheory", "pairTheory", "combinTheory","limTheory","sortingTheory", "realLib", "optionTheory","satTheory", "util_probTheory", "extrealTheory", "measureTheory", "lebesgueTheory","real_sigmaTheory"]; open HolKernel Parse boolLib bossLib limTheory arithmeticTheory realTheory prim_recTheory probabilityTheory seqTheory pred_setTheory res_quanTheory sortingTheory res_quanTools listTheory transcTheory rich_listTheory pairTheory combinTheory realLib optionTheory util_probTheory extrealTheory measureTheory lebesgueTheory real_sigmaTheory satTheory numTheory; fun K_TAC _ = ALL_TAC; (* ------------------------------------------------------------------------- *) (* Definition *) (* ------------------------------------------------------------------------- *) val fail_event_def = Define `fail_event p X t = PREIMAGE X {y | y <= Normal t} INTER p_space p`; val fail_event_list_def = Define `fail_event_list p L t = MAP (\a. fail_event p a t) L`; val list_fail_event_list_def = Define `list_fail_event_list p L t = MAP (\a. fail_event_list p a t) L`; (* ------------------------------------------------------------------------- *) (* exp_func *) (* ------------------------------------------------------------------------- *) val exp_func_def = Define `exp_func (x:real) (c:real) = exp(-(c * x))`; (* ------------------------------------------------------------------------- *) (* One Minus exponential *) (* ------------------------------------------------------------------------- *) val one_minus_exp_def = Define ` one_minus_exp t C = MAP (\c. 1 - exp(-(t * c))) C`; (* ------------------------------------------------------------------------- *) (* list of exponentials *) (* ------------------------------------------------------------------------- *) val exp_func_list_def = Define ` ( exp_func_list [] x = []) /\ ( exp_func_list (h::t) x = exp_func x h :: exp_func_list (t) x)`; (* ------------------------------------------------------------------------- *) (* One Minus exponential product *) (* ------------------------------------------------------------------------- *) val one_minus_exp_prod_def = Define `(one_minus_exp_prod t C = MAP (\a. 1- list_prod (one_minus_list (exp_func_list a t))) C ) `; (* ------------------------------------------------------------------------- *) (* list_sum *) (* ------------------------------------------------------------------------- *) val list_sum_def = Define `(list_sum [] = 0 ) /\ (!h t. list_sum (h::t) = ((h:real) + list_sum(t)))`; (* ------------------------------------------------------------------------- *) (* Definition . Cummulative Distributive Function *) (* ------------------------------------------------------------------------- *) val CDF_def = Define `CDF p X (x:real) = distribution p X {y | y <= Normal x}`; (* ------------------------------------------------------------------------- *) (* Definition : Exponential Distribution Function *) (* ------------------------------------------------------------------------- *) val exp_distribution_def = Define `exp_dist p X l = !x:real. CDF p X (x) = (if (0 <= x) then 1 - exp(-l * x) else 0)`; (* ------------------------------------------------------------------------- *) (* Definition : List of Exponential Distribution Functions *) (* ------------------------------------------------------------------------- *) val list_exp_def = Define `(list_exp p [] L = T ) /\ (list_exp p (h::t) L = ( exp_dist p (HD(L)) (h)) /\ (list_exp p (t) (TL L)))`; (* (* ------------------------------------------------------------------------- *) (* Definition. Fault Tree *) (* ------------------------------------------------------------------------- *) val D8_AND_FT_gate_def = Define `D8_AND_FT_gate p E11 E12 E21 = FTree p (AND [OR(gate_list([E11;E12]);E21]])) `; (* ------------------------------------------------------------------------- *) val D9_OR_FT_gate_def = Define `D9_OR_FT_gate E13 E14 E15 = OR_FT_gate[E13;E14;E15] `; (* ------------------------------------------------------------------------- *) val D11_AND_FT_gate_def = Define `D11_AND_FT_gate p E16 E17 E21 = AND_FT_gate p [OR_FT_gate[E16;E17];E21] `; (* ------------------------------------------------------------------------- *) val D12_OR_FT_gate_def = Define `D12_OR_FT_gate E18 E19 E20 = OR_FT_gate[E18;E19;E20] `; (* ------------------------------------------------------------------------- *) val C3_OR_FT_gate_def = Define `C3_OR_FT_gate p D7 E11 E12 E21 E13 E14 E15 = OR_FT_gate [D7;D8_AND_FT_gate p E11 E12 E21;D9_OR_FT_gate E13 E14 E15] `; (* ------------------------------------------------------------------------- *) val C4_OR_FT_gate_def = Define `C4_OR_FT_gate p D10 E16 E17 E18 E19 E20 E21 = OR_FT_gate[D10; D11_AND_FT_gate p E16 E17 E21; D12_OR_FT_gate E18 E19 E20] `; (* ------------------------------------------------------------------------- *) val B2_event_FT_def = Define `B2_event_FT p D7 D10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21 = OR_FT_gate[C3_OR_FT_gate p D7 E11 E12 E21 E13 E14 E15 ; C4_OR_FT_gate p D10 E16 E17 E18 E19 E20 E21]`; (* ------------------------------------------------------------------------- *) val D2_AND_FT_gate_def = Define `D2_AND_FT_gate p E1 E2 E21 = AND_FT_gate p [OR_FT_gate[E1;E2];E21] `; (* ------------------------------------------------------------------------- *) val D3_OR_FT_gate_def = Define `D3_OR_FT_gate E3 E4 E5 = OR_FT_gate[E3;E4;E5] `; (* ------------------------------------------------------------------------- *) val D5_AND_FT_gate_def = Define `D5_AND_FT_gate p E6 E7 E21 = AND_FT_gate p [OR_FT_gate[E6;E7];E21] `; (* ------------------------------------------------------------------------- *) val D6_OR_FT_gate_def = Define `D6_OR_FT_gate E8 E9 E10 = OR_FT_gate[E8;E9;E10] `; (* ------------------------------------------------------------------------- *) val C1_OR_FT_gate_def = Define `C1_OR_FT_gate p D1 E1 E2 E3 E4 E5 E21 = OR_FT_gate [D1;D2_AND_FT_gate p E1 E2 E21;D3_OR_FT_gate E3 E4 E5] `; (* ------------------------------------------------------------------------- *) val C2_OR_FT_gate_def = Define `C2_OR_FT_gate p D4 E6 E7 E8 E9 E10 E21 = OR_FT_gate[D4; D5_AND_FT_gate p E6 E7 E21; D6_OR_FT_gate E8 E9 E10] `; (* ------------------------------------------------------------------------- *) val B1_event_FT_def = Define `B1_event_FT p D1 D4 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E21 = OR_FT_gate[C1_OR_FT_gate p D1 E1 E2 E3 E4 E5 E21 ; C2_OR_FT_gate p D4 E6 E7 E8 E9 E10 E21]`; (* ------------------------------------------------------------------------- *) val B3_AND_FT_gate_def = Define `B3_AND_FT_gate p C5 C6 C7 C8 = AND_FT_gate p [OR_FT_gate[C5;C6;C7];C8] `; (* ------------------------------------------------------------------------- *) val A_event_FT_def = Define `A_event_FT p D1 D4 D7 D10 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21 C5 C6 C7 C8 = OR_FT_gate[B1_event_FT p D1 D4 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E21 ;B2_event_FT p D7 D10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21; B3_AND_FT_gate p C5 C6 C7 C8]`; (* ------------------------------------------------------------------------- *) val Latency_OR_FT_gate_def = Define `Latency_OR_FT_gate AL SL PD Others = OR_FT_gate[AL ;SL ;PD ;Others] `; (* ------------------------------------------------------------------------- *) val RT_event_FT_def = Define `RT_event_FT p AL SL PD Others time = AND_FT_gate p [Latency_OR_FT_gate AL SL PD Others ; time] `; (* ------------------------------------------------------------------------- *) val Flight_func_mish_AND_FT_gate_def = Define `Flight_func_mish_AND_FT_gate p FD AP FF1 = AND_FT_gate p [OR_FT_gate[FD;AP];FF1] `; (* ------------------------------------------------------------------------- *) val Transm_OR_FT_gate_def = Define `Transm_OR_FT_gate p D1 D4 D7 D10 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21 C5 C6 C7 C8 notshw AL SL PD Others time = OR_FT_gate[A_event_FT p D1 D4 D7 D10 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21 C5 C6 C7 C8 ;notshw; RT_event_FT p AL SL PD Others time] `; (* ------------------------------------------------------------------------- *) val Internal_event_FT_gate_def = Define `Internal_event_FT_gate p FD AP FF1 D1 D4 D7 D10 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21 C5 C6 C7 C8 notshw AL SL PD Others time = OR_FT_gate[Flight_func_mish_AND_FT_gate p FD AP FF1; Transm_OR_FT_gate p D1 D4 D7 D10 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21 C5 C6 C7 C8 notshw AL SL PD Others time] `; (* ------------------------------------------------------------------------- *) val Equip_AND_FT_gate_def = Define `Equip_AND_FT_gate p ED EQ1 = AND_FT_gate p [ED ;EQ1] `; (* ------------------------------------------------------------------------- *) val Envir_AND_FT_gate_def = Define `Envir_AND_FT_gate p EN1 EN2 EN3 EN4 = AND_FT_gate p [EN1; EN2 ;EN3; EN4] `; (* ------------------------------------------------------------------------- *) val Extern_OR_FT_gate_def = Define `Extern_OR_FT_gate p EN1 EN2 EN3 EN4 human = OR_FT_gate [Envir_AND_FT_gate p EN1 EN2 EN3 EN4 ; human] `; (* ------------------------------------------------------------------------- *) val OP_OR_FT_gate_def = Define `OP_OR_FT_gate p FD AP FF1 D1 D4 D7 D10 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21 C5 C6 C7 C8 notshw AL SL PD Others time ED EQ1 EN1 EN2 EN3 EN4 human = OR_FT_gate[Equip_AND_FT_gate p ED EQ1; Extern_OR_FT_gate p EN1 EN2 EN3 EN4 human; Internal_event_FT_gate p FD AP FF1 D1 D4 D7 D10 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21 C5 C6 C7 C8 notshw AL SL PD Others time] `; (* ------------------------------------------------------------------------- *) val ASN_gateway_event_FT_def = Define `ASN_gateway_event_FT p control FD AP FF1 D1 D4 D7 D10 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21 C5 C6 C7 C8 notshw AL SL PD Others time ED EQ1 EN1 EN2 EN3 EN4 human = AND_FT_gate p [OP_OR_FT_gate p FD AP FF1 D1 D4 D7 D10 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21 C5 C6 C7 C8 notshw AL SL PD Others time ED EQ1 EN1 EN2 EN3 EN4 human ; control] `; *) (*=================probability of B1=====================================*) val B1_FT_def = Define `B1_FT p t D1 D4 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E21 = (OR [OR [ atomic (fail_event p D1 t); AND [OR (gate_list (fail_event_list p [E1; E2] t)); atomic (fail_event p E21 t)]; OR (gate_list(fail_event_list p [E3; E4; E5] t))]; OR [atomic (fail_event p D4 t); AND [OR (gate_list(fail_event_list p [E6; E7] t)); atomic (fail_event p E21 t) ]; OR (gate_list(fail_event_list p [E8; E9; E10] t))]])`; (*=================probability of B2=====================================*) val B2_FT_def = Define `B2_FT p t D7 D10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21 = (OR [OR [ atomic (fail_event p D7 t); AND [OR (gate_list (fail_event_list p [E11; E12] t)); atomic (fail_event p E21 t)]; OR (gate_list(fail_event_list p [E13; E14; E15] t))]; OR [atomic (fail_event p D10 t); AND [OR (gate_list(fail_event_list p [E16; E17] t)); atomic (fail_event p E21 t) ]; OR (gate_list(fail_event_list p [E18; E19; E20] t))]])`; (*=================probability of A=====================================*) val A_FT_def = Define ` A_FT p t D1 D4 D7 D10 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21 C5 C6 C7 C8 = (OR [B1_FT p t D1 D4 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E21; B2_FT p t D7 D10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21; AND [OR (gate_list (fail_event_list p [C5; C6; C7] t )); atomic (fail_event p C8 t)]])`; (*=================probability of RT=====================================*) val RT_FT_def = Define `RT_FT p t AL SL PD Others time = AND [OR (gate_list (fail_event_list p [AL; SL; PD; Others] t)) ; atomic (fail_event p time t)] `; (*=================probability of RT=====================================*) g`!p t AL SL PD Others time. RT_FT p t AL SL PD Others time = OR_AND_FT_struct p ( [fail_event_list p [AL;time] t ;fail_event_list p [SL;time] t; fail_event_list p [PD;time] t;fail_event_list p [Others;time] t] )`; e (RW_TAC list_ss[RT_FT_def,OR_AND_FT_struct_def]); e (RW_TAC list_ss[List_inter_list_def,parallel_struct_def]); e (RW_TAC list_ss[AND_FT_gate_def,OR_FT_gate_def,inter_list_def,union_list_def]); e (RW_TAC list_ss[fail_event_list_def,inter_list_def,union_list_def]); e (RW_TAC list_ss[UNION_EMPTY,INTER_ASSOC]); e (SRW_TAC[][IN_INTER,IN_UNION,EXTENSION,GSPECIFICATION]); e (METIS_TAC[]); val RT_FT_lemma1 = top_thm(); drop(); (*=================probability of internal=====================================*) val Internal_FT_def = Define `Internal_FT p t FD AP FF1 D1 D4 D7 D10 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21 C5 C6 C7 C8 notshw AL SL PD Others time = OR[AND [OR (gate_list(fail_event_list p [FD; AP] t)); atomic (fail_event p FF1 t)]; OR [A_FT p t D1 D4 D7 D10 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21 C5 C6 C7 C8; atomic (fail_event p notshw t); RT_FT p t AL SL PD Others time]] `; (*=================probability of ASN gateway =====================================*) val ASN_gateway_FT_def = Define `ASN_gateway_FT p t FD AP FF1 D1 D4 D7 D10 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21 C5 C6 C7 C8 notshw AL SL PD Others time ED EQ1 EN1 EN2 EN3 EN4 human = FTree p (OR [AND (gate_list(fail_event_list p [ED; EQ1] t)); OR [AND (gate_list(fail_event_list p [EN1; EN2; EN3; EN4] t)); atomic (fail_event p human t) ]; Internal_FT p t FD AP FF1 D1 D4 D7 D10 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21 C5 C6 C7 C8 notshw AL SL PD Others time]) `; (*================= =====================================*) val ASN_FT_eq_parallel_series_RBD = store_thm("ASN_FT_eq_parallel_series_RBD", ``!p t FD AP FF1 D1 D4 D7 D10 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21 C5 C6 C7 C8 notshw AL SL PD Others time ED EQ1 EN1 EN2 EN3 EN4 human. (ASN_gateway_FT p t FD AP FF1 D1 D4 D7 D10 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21 C5 C6 C7 C8 notshw AL SL PD Others time ED EQ1 EN1 EN2 EN3 EN4 human = rbd_struct p ((parallel of (λa. series (rbd_list a ))) (list_fail_event_list p [[ED; EQ1];[EN1; EN2; EN3; EN4];[human];[FD; FF1];[FF1; AP];[D1];[D4];[E1;E21];[E2;E21];[E3];[E4];[E5];[E6;E21];[E7;E21];[E8];[E9];[E10];[D7];[D10];[E11;E21];[E12;E21];[E13];[E14];[E15];[E16;E21];[E17;E21];[E18];[E19];[E20];[C5; C8];[C6; C8];[C7; C8];[notshw];[AL; time];[SL; time];[PD; time];[Others;time]] t)))``, RW_TAC list_ss[ASN_gateway_FT_def,Internal_FT_def,A_FT_def,B1_FT_def,B2_FT_def,RT_FT_def,FTree_def,INTER_DEF,rbd_struct_def,list_fail_event_list_def,fail_event_list_def,fail_event_def,gate_list_def,rbd_list_def,of_DEF,o_DEF,UNION_DEF] ++ SET_TAC[]); (*======================================================*) g `! a b c d e f g h i j k l:real. 1 - (a *b *c *d *e *f *g *h *i *j *k * l) = (1 - (a * b * e * f * g * j * k * l * c * d * h* i))`; e (REAL_ARITH_TAC); val B1_FT_lemma2 = top_thm(); drop(); (*======================================================*) g `! a b c d e f g h i j k l:real. (a *b *c *d *e *f *g *h *i *j *k * l) = ( (a * b * e * f * g * j * k * l * c * d * h* i))`; e (REAL_ARITH_TAC); val B1_FT_lemma2_new = top_thm(); drop(); (*======================================================*) g `! a b c d e f g h i j k l:real. (a *b *c *d *e *f *g *h *i *j *k * l) = ((a * b * e * f * g * j * k * l * c * d * h* i))`; e (REAL_ARITH_TAC); val B1_FT_lemma5 = top_thm(); drop(); (*======================================================*) val B1_FT_lemma3 = store_thm("B1_FT_lemma3", ``!p D1 D4 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E21 t. (1 - list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[D1]; [D4]; [E1; E21]; [E2; E21]; [E3]; [E4]; [E5]; [E6; E21]; [E7; E21]; [E8]; [E9]; [E10]] t ))) = 1 - list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[D1]; [D4]; [E3]; [E4]; [E5]; [E8]; [E9]; [E10]] t ))) * list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [ [E1; E21]; [E2; E21]; [E6; E21]; [E7; E21]] t))))``, RW_TAC list_ss[list_fail_event_list_def,fail_event_list_def,fail_event_def,list_prod_rel_def,one_minus_list_def,list_prob_def,list_prod_def] ++ RW_TAC real_ss[REAL_MUL_ASSOC] ++ RW_TAC std_ss[REAL_MUL_ASSOC] ++ RW_TAC std_ss[B1_FT_lemma2]); (*=================*) val B1_FT_lemma3_new = store_thm("B1_FT_lemma3_new", ``!p D1 D4 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E21 t. (list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[D1]; [D4]; [E1; E21]; [E2; E21]; [E3]; [E4]; [E5]; [E6; E21]; [E7; E21]; [E8]; [E9]; [E10]] t ))) = list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[D1]; [D4]; [E3]; [E4]; [E5]; [E8]; [E9]; [E10]] t ))) * list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [ [E1; E21]; [E2; E21]; [E6; E21]; [E7; E21]] t))))``, RW_TAC list_ss[list_fail_event_list_def,fail_event_list_def,fail_event_def,list_prod_rel_def,one_minus_list_def,list_prob_def,list_prod_def] ++ RW_TAC real_ss[REAL_MUL_ASSOC] ++ RW_TAC std_ss[REAL_MUL_ASSOC] ++ RW_TAC std_ss[B1_FT_lemma2_new]); (*======================================================*) val B1_FT_lemma6 = store_thm("B1_FT_lemma6", ``! p t E1 E2 E6 E7 E21 C_E1 C_E2 C_E6 C_E7 C_E21. (0<= t) /\ prob_space p /\ (list_exp p (FLAT [[C_E1; C_E21]; [C_E2; C_E21]; [C_E6; C_E21]; [C_E7; C_E21]]) (FLAT [[E1; E21]; [E2; E21]; [E6; E21]; [E7; E21]])) ==> (list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[E1; E21]; [E2; E21]; [E6; E21]; [E7; E21]] t))) = list_prod (one_minus_exp_prod t [[C_E1; C_E21]; [C_E2; C_E21]; [C_E6; C_E21]; [C_E7; C_E21]]))``, RW_TAC list_ss[list_exp_def,exp_distribution_def,distribution_def,CDF_def,list_fail_event_list_def,fail_event_list_def,fail_event_def,list_prod_rel_def,list_prod_def,list_prob_def] ++ RW_TAC list_ss[one_minus_list_def,list_prod_def,one_minus_exp_prod_def,exp_func_list_def,list_sum_def,exp_func_def] ++ RW_TAC std_ss[REAL_MUL_ASSOC] ++ RW_TAC real_ss[]); (*=====================================================================*) val RT_FT_lemma2 = store_thm("RT_FT_lemma2", ``!p t AL SL PD Others time C_AL C_SL C_PD C_Others C_time. (0<= t) /\ prob_space p/\ (list_exp p (FLAT [[C_AL;C_time]; [C_SL;C_time]; [C_PD;C_time]; [C_Others;C_time]]) (FLAT [[AL;time]; [SL;time]; [PD;time]; [Others;time]])) ==> (list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[AL; time]; [SL; time]; [PD; time]; [Others; time]] t))) = list_prod (one_minus_exp_prod t [[C_AL;C_time]; [C_SL;C_time]; [C_PD;C_time]; [C_Others;C_time]]))``, RW_TAC list_ss[list_exp_def,exp_distribution_def,distribution_def,CDF_def,list_fail_event_list_def,fail_event_list_def,fail_event_def,list_prod_rel_def,list_prod_def,list_prob_def] ++ RW_TAC list_ss[one_minus_list_def,list_prod_def,one_minus_exp_prod_def,exp_func_list_def,list_sum_def,exp_func_def] ++ RW_TAC std_ss[REAL_MUL_ASSOC] ++ RW_TAC real_ss[]); (*======================================================*) val B1_FT_lemma4 = store_thm("B1_FT_lemma4", ``! p t D1 D4 E1 E3 E4 E5 E8 E9 E10 C_D1 C_D4 C_E3 C_E4 C_E5 C_E8 C_E9 C_E10. (0<= t) /\ prob_space p /\ (list_exp p ([C_D1; C_D4; C_E3; C_E4; C_E5; C_E8; C_E9; C_E10]) (FLAT [[D1]; [D4]; [E3]; [E4]; [E5]; [E8]; [E9]; [E10]])) ==> (list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[D1]; [D4]; [E3]; [E4]; [E5]; [E8]; [E9]; [E10]] t ))) = exp (-(t * list_sum [C_D1; C_D4; C_E3; C_E4; C_E5; C_E8; C_E9; C_E10])))``, RW_TAC list_ss[list_exp_def,exp_distribution_def,distribution_def,CDF_def,list_fail_event_list_def,fail_event_list_def,fail_event_def,list_prod_rel_def,list_prod_def,list_prob_def] ++ RW_TAC list_ss[one_minus_list_def,list_prod_def,one_minus_exp_prod_def,exp_func_list_def,list_sum_def,exp_func_def] ++ RW_TAC std_ss[REAL_MUL_ASSOC] ++ RW_TAC real_ss[] ++ RW_TAC real_ss[GSYM EXP_ADD] ++ RW_TAC real_ss[EXP_NEG] ++ RW_TAC real_ss[REAL_LDISTRIB] ++ RW_TAC real_ss[GSYM EXP_NEG] ++ RW_TAC real_ss[REAL_NEG_ADD] ++ RW_TAC real_ss[REAL_MUL_COMM,REAL_ADD_ASSOC]); (*================================================*) val A_FT_lemma1 = store_thm("A_FT_lemma1", ``!p t D1 D4 D7 D10 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21 C5 C6 C7 C8 notshw AL time SL PD Others. list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[D1]; [D4]; [E1; E21]; [E2; E21]; [E3]; [E4]; [E5]; [E6; E21]; [E7; E21]; [E8]; [E9]; [E10]; [D7]; [D10]; [E11; E21]; [E12; E21]; [E13]; [E14]; [E15]; [E16; E21]; [E17; E21]; [E18]; [E19]; [E20]; [C5; C8]; [C6; C8]; [C7; C8]; [notshw]; [AL; time]; [SL; time]; [PD; time]; [Others; time]] t))) = list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[D1]; [D4]; [E1; E21]; [E2; E21]; [E3]; [E4]; [E5]; [E6; E21]; [E7; E21]; [E8]; [E9]; [E10]] t))) * list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[D7]; [D10]; [E11; E21]; [E12; E21]; [E13]; [E14]; [E15]; [E16; E21]; [E17; E21]; [E18]; [E19]; [E20]] t ))) * list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[C5; C8]; [C6; C8]; [C7; C8]; [notshw]; [AL; time]; [SL; time]; [PD; time]; [Others; time]] t))) ``, RW_TAC list_ss[list_exp_def,exp_distribution_def,distribution_def,CDF_def,list_fail_event_list_def,fail_event_list_def,fail_event_def,list_prod_rel_def,list_prod_def,list_prob_def] ++ RW_TAC list_ss[one_minus_list_def,list_prod_def,one_minus_exp_prod_def,exp_func_list_def,list_sum_def,exp_func_def] ++ RW_TAC std_ss[REAL_MUL_ASSOC] ++ RW_TAC real_ss[]); (*================================================*) val Internal_FT_lemma1 = store_thm("Internal_FT_lemma1", ``!p t FD AP FF1 D1 D4 D7 D10 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21 C5 C6 C7 C8 notshw AL SL PD Others time. list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[FD; FF1]; [FF1; AP]; [D1]; [D4]; [E1; E21]; [E2; E21]; [E3]; [E4]; [E5]; [E6; E21]; [E7; E21]; [E8]; [E9]; [E10]; [D7]; [D10]; [E11; E21]; [E12; E21]; [E13]; [E14]; [E15]; [E16; E21]; [E17; E21]; [E18]; [E19]; [E20]; [C5; C8]; [C6; C8]; [C7; C8]; [notshw]; [AL; time]; [SL; time]; [PD; time]; [Others; time]] t))) = list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[FD; FF1]; [FF1; AP]] t))) * list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[D1]; [D4]; [E1; E21]; [E2; E21]; [E3]; [E4]; [E5]; [E6; E21]; [E7; E21]; [E8]; [E9]; [E10]; [D7]; [D10]; [E11; E21]; [E12; E21]; [E13]; [E14]; [E15]; [E16; E21]; [E17; E21]; [E18]; [E19]; [E20]; [C5; C8]; [C6; C8]; [C7; C8]; [notshw]; [AL; time]; [SL; time]; [PD; time]; [Others; time]] t)))``, RW_TAC list_ss[list_fail_event_list_def,fail_event_list_def,fail_event_def,list_prod_rel_def,one_minus_list_def,list_prob_def,list_prod_def] ++ RW_TAC real_ss[REAL_MUL_ASSOC]); (*================================================*) val Internal_FT_lemma2 = store_thm("Internal_FT_lemma2", ``! p t FD AP FF1 C_FD C_AP C_FF1. (0<= t) /\ prob_space p /\ (list_exp p (FLAT [[C_FD;C_FF1];[C_AP;C_FF1]]) (FLAT [[FD;FF1];[AP;FF1]])) ==> (list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[FD; FF1]; [FF1; AP]] t))) = list_prod (one_minus_exp_prod t [[C_FD; C_FF1]; [C_AP; C_FF1]]))``, RW_TAC list_ss[list_exp_def,exp_distribution_def,distribution_def,CDF_def,list_fail_event_list_def,fail_event_list_def,fail_event_def,list_prod_rel_def,list_prod_def,list_prob_def] ++ RW_TAC list_ss[one_minus_list_def,list_prod_def,one_minus_exp_prod_def,exp_func_list_def,list_sum_def,exp_func_def] ++ RW_TAC std_ss[REAL_MUL_ASSOC] ++ RW_TAC real_ss[] ++ REAL_ARITH_TAC); (*================================================*) (*=========================================================================*) val ASN_gateway_lemma1 = store_thm("ASN_gateway_lemma1", ``!p t FD AP FF1 D1 D4 D7 D10 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21 C5 C6 C7 C8 notshw AL SL PD Others time ED EQ1 EN1 EN2 EN3 EN4 human. (list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[ED; EQ1]; [EN1; EN2; EN3; EN4]; [human]; [FD; FF1]; [FF1; AP]; [D1]; [D4]; [E1; E21]; [E2; E21]; [E3]; [E4]; [E5]; [E6; E21]; [E7; E21]; [E8]; [E9]; [E10]; [D7]; [D10]; [E11; E21]; [E12; E21]; [E13]; [E14]; [E15]; [E16; E21]; [E17; E21]; [E18]; [E19]; [E20]; [C5; C8]; [C6; C8]; [C7; C8]; [notshw]; [AL; time]; [SL; time]; [PD; time]; [Others; time]] t))) = list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[ED; EQ1]; [EN1; EN2; EN3; EN4]; [human]] t))) * list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[FD; FF1]; [FF1; AP]; [D1]; [D4]; [E1; E21]; [E2; E21]; [E3]; [E4]; [E5]; [E6; E21]; [E7; E21]; [E8]; [E9]; [E10]; [D7]; [D10]; [E11; E21]; [E12; E21]; [E13]; [E14]; [E15]; [E16; E21]; [E17; E21]; [E18]; [E19]; [E20]; [C5; C8]; [C6; C8]; [C7; C8]; [notshw]; [AL; time]; [SL; time]; [PD; time]; [Others; time]] t))))``, RW_TAC list_ss[list_fail_event_list_def,fail_event_list_def,fail_event_def,list_prod_rel_def,one_minus_list_def,list_prob_def,list_prod_def] ++ RW_TAC real_ss[REAL_MUL_ASSOC]); (*----------------------*) val ASN_gateway_lemma2 = store_thm("ASN_gateway_lemma2", ``!p t ED EQ1 EN1 EN2 EN3 EN4 human C_ED C_EQ1 C_EN1 C_EN2 C_EN3 C_EN4 C_human. (0 <= t) /\ prob_space p /\ (list_exp p (FLAT [[C_ED;C_EQ1];[C_EN1;C_EN2;C_EN3;C_EN4];[C_human]]) (FLAT [[ED;EQ1];[EN1;EN2;EN3;EN4];[human]])) ==> (list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[ED; EQ1]; [EN1; EN2; EN3; EN4]; [human]] t))) = list_prod (one_minus_exp_prod t [[C_ED; C_EQ1]; [C_EN1; C_EN2; C_EN3; C_EN4]; [C_human]]))``, RW_TAC list_ss[list_exp_def,exp_distribution_def,distribution_def,CDF_def,list_fail_event_list_def,fail_event_list_def,fail_event_def,list_prod_rel_def,list_prod_def,list_prob_def] ++ RW_TAC list_ss[one_minus_list_def,list_prod_def,one_minus_exp_prod_def,exp_func_list_def,list_sum_def,exp_func_def] ++ RW_TAC std_ss[REAL_MUL_ASSOC] ++ RW_TAC real_ss[]); (*---------------------------*) val ASN_gateway_lem5 = store_thm("ASN_gateway_lem5", ``! p t C5 C6 C7 C8 notshw AL time SL PD Others. (list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[C5; C8]; [C6; C8]; [C7; C8]; [notshw]; [AL; time]; [SL; time]; [PD; time]; [Others; time]] t))) = list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[C5; C8]; [C6; C8]; [C7; C8]] t))) * list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[notshw]; [AL; time]; [SL; time]; [PD; time]; [Others; time]] t))))``, RW_TAC list_ss[list_fail_event_list_def,fail_event_list_def,fail_event_def,list_prod_rel_def,one_minus_list_def,list_prob_def,list_prod_def] ++ RW_TAC real_ss[REAL_MUL_ASSOC]); (*-----------------*) val ASN_gateway_lem6 = store_thm("ASN_gateway_lem6",``! p t C5 C6 C7 C8 C_C5 C_C6 C_C7 C_C8. (0<= t) /\ prob_space p /\ (list_exp p (FLAT [[C_C5;C_C8]; [C_C6;C_C8]; [C_C7;C_C8]]) (FLAT [[C5;C8]; [C6;C8]; [C7;C8]])) ==> (list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[C5; C8]; [C6; C8]; [C7; C8]] t))) = list_prod (one_minus_exp_prod t [[C_C5;C_C8]; [C_C6;C_C8]; [C_C7;C_C8]]))``, RW_TAC list_ss[list_exp_def,exp_distribution_def,distribution_def,CDF_def,list_fail_event_list_def,fail_event_list_def,fail_event_def,list_prod_rel_def,list_prod_def,list_prob_def] ++ RW_TAC list_ss[one_minus_list_def,list_prod_def,one_minus_exp_prod_def,exp_func_list_def,list_sum_def,exp_func_def] ++ RW_TAC std_ss[REAL_MUL_ASSOC] ++ RW_TAC real_ss[]); (*=========================================================================*) val ASN_gateway_thm = store_thm("ASN_gateway_thm", ``!p t FD AP FF1 D1 D4 D7 D10 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21 C5 C6 C7 C8 notshw AL SL PD Others time ED EQ1 EN1 EN2 EN3 EN4 human C_ED C_EQ1 C_EN1 C_EN2 C_EN3 C_EN4 C_human C_FD C_AP C_FF1 C_notshw C_AL C_SL C_PD C_Others C_time C_C5 C_C6 C_C7 C_C8 C_E1 C_E2 C_E6 C_E7 C_D1 C_D4 C_E3 C_E4 C_E5 C_E8 C_E9 C_E10 C_E11 C_E12 C_E16 C_E17 C_D7 C_D10 C_E13 C_E14 C_E15 C_E18 C_E19 C_E20 C_E21. (0 <= t) /\ prob_space p /\ (!x'. MEM x' (FLAT (list_fail_event_list p [[ED; EQ1]; [EN1; EN2; EN3; EN4]; [human]; [FD; FF1]; [FF1; AP]; [D1]; [D4]; [E1; E21]; [E2; E21]; [E3]; [E4]; [E5]; [E6; E21]; [E7; E21]; [E8]; [E9]; [E10]; [D7]; [D10]; [E11; E21]; [E12; E21]; [E13]; [E14]; [E15]; [E16; E21]; [E17; E21]; [E18]; [E19]; [E20]; [C5; C8]; [C6; C8]; [C7; C8]; [notshw]; [AL; time]; [SL; time]; [PD; time]; [Others; time]] t)) ==> x' IN events p) /\ mutual_indep p (FLAT (list_fail_event_list p [[ED; EQ1]; [EN1; EN2; EN3; EN4]; [human]; [FD; FF1]; [FF1; AP]; [D1]; [D4]; [E1; E21]; [E2; E21]; [E3]; [E4]; [E5]; [E6; E21]; [E7; E21]; [E8]; [E9]; [E10]; [D7]; [D10]; [E11; E21]; [E12; E21]; [E13]; [E14]; [E15]; [E16; E21]; [E17; E21]; [E18]; [E19]; [E20]; [C5; C8]; [C6; C8]; [C7; C8]; [notshw]; [AL; time]; [SL; time]; [PD; time]; [Others; time]] t)) /\ (list_exp p (FLAT [[C_C5; C_C6; C_C7; C_C8]; [C_D1]; [C_D4]; [C_E1; C_E21]; [C_E2; C_E21]; [C_E3]; [C_E4]; [C_E5]; [C_E6; C_E21]; [C_E7; C_E21]; [C_E8]; [C_E9]; [C_E10]; [C_D7]; [C_D10]; [C_E11; C_E21]; [C_E12; C_E21]; [C_E13]; [C_E14]; [C_E15]; [C_E16; C_E21]; [C_E17; C_E21]; [C_E18]; [C_E19]; [C_E20]; [C_AL; C_time]; [C_SL; C_time]; [C_PD; C_time]; [C_Others; C_time]; [C_FD; C_FF1]; [C_AP; C_FF1]; [C_notshw];[C_ED;C_EQ1];[C_EN1;C_EN2;C_EN3;C_EN4];[C_human]]) (FLAT [[C5; C6; C7; C8]; [D1]; [D4]; [E1; E21]; [E2; E21]; [E3]; [E4]; [E5]; [E6; E21]; [E7; E21]; [E8]; [E9]; [E10]; [D7]; [D10]; [E11; E21]; [E12; E21]; [E13]; [E14]; [E15]; [E16; E21]; [E17; E21]; [E18]; [E19]; [E20]; [AL; time]; [SL; time]; [PD; time]; [Others; time]; [FD; FF1]; [AP; FF1]; [notshw];[ED;EQ1];[EN1;EN2;EN3;EN4];[human]])) ==> (prob p (ASN_gateway_FT p t FD AP FF1 D1 D4 D7 D10 E1 E2 E3 E4 E5 E6 E7 E8 E9 E10 E11 E12 E13 E14 E15 E16 E17 E18 E19 E20 E21 C5 C6 C7 C8 notshw AL SL PD Others time ED EQ1 EN1 EN2 EN3 EN4 human) = 1 - list_prod (one_minus_exp_prod t [[C_ED; C_EQ1]; [C_EN1; C_EN2; C_EN3; C_EN4]; [C_human]]) * (list_prod (one_minus_exp_prod t [[C_FD; C_FF1]; [C_AP; C_FF1]]) * (exp (-(t * list_sum [C_D1; C_D4; C_E3; C_E4; C_E5; C_E8; C_E9; C_E10])) * list_prod (one_minus_exp_prod t [[C_E1; C_E21]; [C_E2; C_E21]; [C_E6; C_E21]; [C_E7; C_E21]]) * (exp (-(t * list_sum [C_D7; C_D10; C_E13; C_E14; C_E15; C_E18; C_E19; C_E20])) * list_prod (one_minus_exp_prod t [[C_E11; C_E21]; [C_E12; C_E21]; [C_E16; C_E21]; [C_E17; C_E21]])) * list_prod (one_minus_exp_prod t [[C_C5; C_C8]; [C_C6; C_C8]; [C_C7; C_C8]])) * exp (-(C_notshw * t)) * list_prod (one_minus_exp_prod t [[C_AL; C_time]; [C_SL; C_time]; [C_PD; C_time]; [C_Others; C_time]])))``, RW_TAC std_ss[ASN_FT_eq_parallel_series_RBD] ++ DEP_REWRITE_TAC[rel_parallel_series_rbd] ++ RW_TAC std_ss[] >> (FULL_SIMP_TAC list_ss[list_fail_event_list_def,fail_event_list_def]) ++ RW_TAC std_ss[ASN_gateway_lemma1] ++ DEP_ASM_REWRITE_TAC[ASN_gateway_lemma2] ++ RW_TAC list_ss[] >> (FULL_SIMP_TAC list_ss[list_exp_def]) ++ AP_TERM_TAC ++ AP_TERM_TAC ++ RW_TAC std_ss[Internal_FT_lemma1] ++ DEP_ASM_REWRITE_TAC[Internal_FT_lemma2] ++ RW_TAC list_ss[] >> (FULL_SIMP_TAC list_ss[list_exp_def]) ++ RW_TAC std_ss[GSYM REAL_MUL_ASSOC] ++ AP_TERM_TAC ++ RW_TAC real_ss[A_FT_lemma1] ++ RW_TAC real_ss[B1_FT_lemma3_new] ++ DEP_ONCE_ASM_REWRITE_TAC[B1_FT_lemma4] ++ RW_TAC list_ss[] >> (FULL_SIMP_TAC list_ss[list_exp_def]) ++ RW_TAC std_ss[GSYM REAL_MUL_ASSOC] ++ AP_TERM_TAC ++ DEP_ONCE_ASM_REWRITE_TAC[B1_FT_lemma6] ++ RW_TAC list_ss[] >> (FULL_SIMP_TAC list_ss[list_exp_def]) ++ RW_TAC std_ss[GSYM REAL_MUL_ASSOC] ++ AP_TERM_TAC ++ (`list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[D7]; [D10]; [E13]; [E14]; [E15]; [E18]; [E19]; [E20]] t))) = exp (-(t * list_sum [C_D7; C_D10; C_E13; C_E14; C_E15; C_E18; C_E19; C_E20]))` by MATCH_MP_TAC B1_FT_lemma4) >> (RW_TAC list_ss[] ++ FULL_SIMP_TAC list_ss[list_exp_def]) ++ RW_TAC std_ss[GSYM REAL_MUL_ASSOC] ++ AP_TERM_TAC ++ (`list_prod (one_minus_list (list_prod_rel p (list_fail_event_list p [[E11; E21]; [E12; E21]; [E16; E21]; [E17; E21]] t))) = list_prod (one_minus_exp_prod t [[C_E11; C_E21]; [C_E12; C_E21]; [C_E16; C_E21]; [C_E17; C_E21]])` by MATCH_MP_TAC B1_FT_lemma6) >> (RW_TAC list_ss[] ++ FULL_SIMP_TAC list_ss[list_exp_def]) ++ RW_TAC std_ss[GSYM REAL_MUL_ASSOC] ++ AP_TERM_TAC ++ RW_TAC std_ss[ASN_gateway_lem5] ++ DEP_ONCE_ASM_REWRITE_TAC[ASN_gateway_lem6] ++ RW_TAC list_ss[] >> (FULL_SIMP_TAC list_ss[list_exp_def]) ++ RW_TAC std_ss[GSYM REAL_MUL_ASSOC] ++ AP_TERM_TAC ++ NTAC 4 (POP_ASSUM MP_TAC) ++ RW_TAC list_ss[list_exp_def,exp_distribution_def,distribution_def,CDF_def,list_fail_event_list_def,fail_event_list_def,fail_event_def,list_prod_rel_def,list_prod_def,list_prob_def] ++ RW_TAC list_ss[one_minus_list_def,list_prod_def,one_minus_exp_prod_def,exp_func_list_def,list_sum_def,exp_func_def] ++ RW_TAC real_ss[]); (*=========================================================================*)