Skip to content

Commit 3f726a4

Browse files
binghebinghe
authored
Updates to convergence concepts for potential infinite-valued r.v.'s (#1295)
* Updates to convergence concepts for potential infinite-valued r.v.'s * Remove unfinished work... * FTBFS * Added missing NUM_FLOOR_POS, etc. in realTheory * FTBFS examples/dependability
1 parent 0f9ee5c commit 3f726a4

17 files changed

+875
-564
lines changed

‎examples/dependability/AvailabilityScript.sml

Lines changed: 61 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -372,10 +372,10 @@ RW_TAC std_ss[]
372372
>> DEP_REWRITE_TAC[SEQ_ADD]
373373
>> RW_TAC std_ss[]
374374
>- (RW_TAC std_ss[SEQ_CONST])
375-
>- ((`(seq$--> (\t. (FST (m:real#real) / (SND m + FST m)) * exp (-(SND m + FST m) * &t)) 0) =
376-
(seq$--> (\t.
375+
>- ((`((\t. (FST (m:real#real) / (SND m + FST m)) * exp (-(SND m + FST m) * &t)) --> 0) =
376+
((\t.
377377
(\t. FST m / (SND m + FST m)) t *
378-
(\t. exp (-(SND m + FST m) * &t)) t)
378+
(\t. exp (-(SND m + FST m) * &t)) t) -->
379379
((FST m / (SND m + FST m)) *0))` by (RW_TAC real_ss[]))
380380
>> POP_ORW
381381
>> MATCH_MP_TAC SEQ_MUL
@@ -393,8 +393,9 @@ RW_TAC std_ss[]
393393
>> POP_ORW
394394
>> MATCH_MP_TAC SEQ_ADD
395395
>> RW_TAC std_ss[SEQ_CONST]
396-
>> (`(seq$--> (\t. FST m / (SND m + FST m) * exp (-(SND m + FST m) * &t)) 0) =
397-
(seq$--> (\t. (\t. FST m / (SND m + FST m))t * (\t. exp (-(SND m + FST m) * &t))t) ((FST m / (SND m + FST m)) *0))`
396+
>> (`((\t. FST m / (SND m + FST m) * exp (-(SND m + FST m) * &t)) --> 0) =
397+
((\t. (\t. FST m / (SND m + FST m))t * (\t. exp (-(SND m + FST m) * &t))t) -->
398+
((FST m / (SND m + FST m)) *0))`
398399
by RW_TAC real_ss[])
399400
>> POP_ORW
400401
>> MATCH_MP_TAC SEQ_MUL
@@ -406,18 +407,20 @@ RW_TAC std_ss[]
406407
>> RW_TAC std_ss[steady_avail_temp])
407408
>> RW_TAC std_ss [expec_avail_def]
408409
>> FULL_SIMP_TAC std_ss[inst_avail_exp_def,expec_def]
409-
>> (`(seq$--> (\t.
410+
>> (`((\t.
410411
SND m / (SND m + FST m) +
411-
FST m / (SND m + FST m) * exp (-(SND m + FST m) * &t)) (SND m / (SND m + FST m))) =
412-
(seq$--> (\t.
412+
FST m / (SND m + FST m) * exp (-(SND m + FST m) * &t)) --> (SND m / (SND m + FST m))) =
413+
((\t.
413414
(\t. SND m / (SND m + FST m)) t +
414-
(\t. FST m / (SND m + FST m) * exp (-(SND m + FST m) * &t))t) ((SND m / (SND m + FST m)) + 0))` by RW_TAC real_ss[])
415+
(\t. FST m / (SND m + FST m) * exp (-(SND m + FST m) * &t))t) -->
416+
((SND m / (SND m + FST m)) + 0))` by RW_TAC real_ss[])
415417
>> POP_ORW
416418
>> MATCH_MP_TAC SEQ_ADD
417419
>> RW_TAC std_ss[]
418420
>- (RW_TAC std_ss[SEQ_CONST])
419-
>> (`(seq$--> (\t. FST m / (SND m + FST m) * exp (-(SND m + FST m) * &t)) 0) =
420-
(seq$--> (\t. (\t. FST m / (SND m + FST m))t * (\t. exp (-(SND m + FST m) * &t))t) ((FST m / (SND m + FST m)) *0))`
421+
>> (`((\t. FST m / (SND m + FST m) * exp (-(SND m + FST m) * &t)) --> 0) =
422+
((\t. (\t. FST m / (SND m + FST m))t * (\t. exp (-(SND m + FST m) * &t))t)
423+
--> ((FST m / (SND m + FST m)) *0))`
421424
by RW_TAC real_ss[])
422425
>> POP_ORW
423426
>> MATCH_MP_TAC SEQ_MUL
@@ -529,21 +532,21 @@ GEN_TAC
529532
>> RW_TAC std_ss[]
530533
>- (FULL_SIMP_TAC list_ss[inst_avail_exp_list1_def,inst_avail_exp2_def]
531534
>> REWRITE_TAC[steady_state_avail_def]
532-
>> (`(seq$--> (\t.
535+
>> (`((\t.
533536
SND (h':real#real) / (SND h' + FST h') +
534-
FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t))
537+
FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) -->
535538
(SND h' / (SND h' + FST h'))) =
536-
(seq$--> (\t.
539+
((\t.
537540
(\t. SND h' / (SND h'+ FST h')) t +
538-
(\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t))t)
541+
(\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) t) -->
539542
(SND h' / (SND h' + FST h') + 0))` by RW_TAC real_ss[])
540543
>> POP_ORW
541544
>> MATCH_MP_TAC SEQ_ADD
542545
>> RW_TAC std_ss[]
543546
>- (RW_TAC std_ss[SEQ_CONST])
544-
>- ((`(seq$--> (\t. FST h'/ (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) 0) =
545-
(seq$--> (\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t))t)
546-
((FST h' / (SND h' + FST h')) *0))` by RW_TAC real_ss[])
547+
>- ((`((\t. FST h'/ (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) --> 0) =
548+
((\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t)) t)
549+
--> ((FST h' / (SND h' + FST h')) *0))` by RW_TAC real_ss[])
547550
>> POP_ORW
548551
>> MATCH_MP_TAC SEQ_MUL
549552
>> RW_TAC real_ss[SEQ_CONST]
@@ -632,19 +635,21 @@ GEN_TAC
632635
>> RW_TAC std_ss[SEQ_CONST]
633636
>> FULL_SIMP_TAC list_ss[inst_avail_exp_list1_def,inst_avail_exp2_def]
634637
>> REWRITE_TAC[steady_state_avail_def]
635-
>> (`(seq$--> (\t.
638+
>> (`((\t.
636639
SND (h':real#real) / (SND h' + FST h') +
637-
FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) (SND h' / (SND h' + FST h'))) =
638-
(seq$--> (\t.
640+
FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) --> (SND h' / (SND h' + FST h'))) =
641+
((\t.
639642
(\t. SND h' / (SND h'+ FST h')) t +
640-
(\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t))t) (SND h' / (SND h' + FST h') + 0))`
643+
(\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t))t)
644+
--> (SND h' / (SND h' + FST h') + 0))`
641645
by RW_TAC real_ss[])
642646
>> POP_ORW
643647
>> MATCH_MP_TAC SEQ_ADD
644648
>> RW_TAC std_ss[]
645649
>- (RW_TAC std_ss[SEQ_CONST])
646-
>- ((`(seq$--> (\t. FST h'/ (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) 0) =
647-
(seq$--> (\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t))t) ((FST h' / (SND h' + FST h')) *0))`
650+
>- ((`((\t. FST h'/ (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) --> 0) =
651+
((\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t)) t)
652+
--> ((FST h' / (SND h' + FST h')) *0))`
648653
by RW_TAC real_ss[])
649654
>> POP_ORW
650655
>> MATCH_MP_TAC SEQ_MUL
@@ -1119,19 +1124,21 @@ GEN_TAC
11191124
>> RW_TAC std_ss[]
11201125
>- (FULL_SIMP_TAC list_ss[inst_unavail_exp_list_def,inst_unavail_exp_def]
11211126
>> REWRITE_TAC[steady_state_unavail_def]
1122-
>> (`(seq$--> (\t.
1127+
>> (`((\t.
11231128
FST (h':real#real) / (SND h' + FST h') -
1124-
FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) (FST h' / (SND h' + FST h'))) =
1125-
(seq$--> (\t.
1129+
FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) --> (FST h' / (SND h' + FST h'))) =
1130+
((\t.
11261131
(\t. FST (h':real#real) / (SND h'+ FST h')) t -
1127-
(\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t))t) (FST h' / (SND h' + FST h') - 0))`
1132+
(\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) t)
1133+
--> (FST h' / (SND h' + FST h') - 0))`
11281134
by RW_TAC real_ss[])
11291135
>> POP_ORW
11301136
>> MATCH_MP_TAC SEQ_SUB
11311137
>> RW_TAC std_ss[]
11321138
>- (RW_TAC std_ss[SEQ_CONST])
1133-
>- ((`(seq$--> (\t. FST h'/ (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) 0) =
1134-
(seq$--> (\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t))t) ((FST h' / (SND h' + FST h')) *0))`
1139+
>- ((`((\t. FST h'/ (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) --> 0) =
1140+
((\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t)) t)
1141+
--> ((FST h' / (SND h' + FST h')) * 0))`
11351142
by RW_TAC real_ss[])
11361143
>> POP_ORW
11371144
>> MATCH_MP_TAC SEQ_MUL
@@ -1221,19 +1228,21 @@ GEN_TAC
12211228
>> RW_TAC std_ss[SEQ_CONST]
12221229
>> FULL_SIMP_TAC list_ss[inst_unavail_exp_list_def,inst_unavail_exp_def]
12231230
>> REWRITE_TAC[steady_state_unavail_def]
1224-
>> (`(seq$--> (\t.
1231+
>> (`((\t.
12251232
FST (h':real#real) / (SND h' + FST h') -
1226-
FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) (FST h' / (SND h' + FST h'))) =
1227-
(seq$--> (\t.
1233+
FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) --> (FST h' / (SND h' + FST h'))) =
1234+
((\t.
12281235
(\t. FST h' / (SND h'+ FST h')) t -
1229-
(\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t))t) (FST h' / (SND h' + FST h') - 0))`
1236+
(\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) t)
1237+
--> (FST h' / (SND h' + FST h') - 0))`
12301238
by RW_TAC real_ss[])
12311239
>> POP_ORW
12321240
>> MATCH_MP_TAC SEQ_SUB
12331241
>> RW_TAC std_ss[]
12341242
>- (RW_TAC std_ss[SEQ_CONST])
1235-
>- ((`(seq$--> (\t. FST h'/ (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) 0) =
1236-
(seq$--> (\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t))t) ((FST h' / (SND h' + FST h')) *0))`
1243+
>- ((`((\t. FST h'/ (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) --> 0) =
1244+
((\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t)) t)
1245+
--> ((FST h' / (SND h' + FST h')) *0))`
12371246
by RW_TAC real_ss[])
12381247
>> POP_ORW
12391248
>> MATCH_MP_TAC SEQ_MUL
@@ -1408,19 +1417,21 @@ GEN_TAC
14081417
>> POP_ORW
14091418
>> FULL_SIMP_TAC list_ss[inst_avail_exp_list2_def,inst_avail_exp3_def]
14101419
>> RW_TAC std_ss[steady_state_avail_def]
1411-
>> (`(seq$--> (\t.
1420+
>> (`((\t.
14121421
SND (h':real#real) / (SND h' + FST h') +
1413-
FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) (SND h' / (SND h' + FST h'))) =
1414-
(seq$--> (\t.
1422+
FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) --> (SND h' / (SND h' + FST h'))) =
1423+
((\t.
14151424
(\t. SND h' / (SND h'+ FST h')) t +
1416-
(\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t))t) (SND h' / (SND h' + FST h') + 0))`
1425+
(\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t))t)
1426+
--> (SND h' / (SND h' + FST h') + 0))`
14171427
by RW_TAC real_ss[])
14181428
>> POP_ORW
14191429
>> MATCH_MP_TAC SEQ_ADD
14201430
>> RW_TAC std_ss[]
14211431
>- (RW_TAC std_ss[SEQ_CONST])
1422-
>- ((`(seq$--> (\t. FST h'/ (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) 0) =
1423-
(seq$--> (\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t))t) ((FST h' / (SND h' + FST h')) *0))`
1432+
>- ((`((\t. FST h'/ (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) --> 0) =
1433+
((\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t))t)
1434+
--> ((FST h' / (SND h' + FST h')) *0))`
14241435
by RW_TAC real_ss[])
14251436
>> POP_ORW
14261437
>> MATCH_MP_TAC SEQ_MUL
@@ -1524,19 +1535,21 @@ Proof
15241535
RW_TAC std_ss[]
15251536
>> FULL_SIMP_TAC std_ss[inst_unavail_exp_def]
15261537
>> RW_TAC std_ss[steady_state_unavail_def]
1527-
>> (`(seq$--> (\t.
1538+
>> (`((\t.
15281539
FST (m1:real#real) / (SND m1 + FST m1) -
1529-
FST m1 / (SND m1 + FST m1) * exp (-(SND m1 + FST m1) * &t)) (FST m1 / (SND m1 + FST m1))) =
1530-
(seq$--> (\t.
1540+
FST m1 / (SND m1 + FST m1) * exp (-(SND m1 + FST m1) * &t)) --> (FST m1 / (SND m1 + FST m1))) =
1541+
((\t.
15311542
(\t. FST m1 / (SND m1+ FST m1)) t -
1532-
(\t. FST m1 / (SND m1 + FST m1) * exp (-(SND m1 + FST m1) * &t))t) (FST m1 / (SND m1 + FST m1) - 0))`
1543+
(\t. FST m1 / (SND m1 + FST m1) * exp (-(SND m1 + FST m1) * &t)) t)
1544+
--> (FST m1 / (SND m1 + FST m1) - 0))`
15331545
by RW_TAC real_ss[])
15341546
>> POP_ORW
15351547
>> MATCH_MP_TAC SEQ_SUB
15361548
>> RW_TAC std_ss[]
15371549
>- (RW_TAC std_ss[SEQ_CONST])
1538-
>> (`(seq$--> (\t. FST (m1:real#real) / (SND m1 + FST m1) * exp (-(SND m1 + FST m1) * &t)) 0) =
1539-
(seq$--> (\t. (\t. FST m1 / (SND m1 + FST m1))t * (\t. exp (-(SND m1 + FST m1) * &t))t) ((FST m1 / (SND m1 + FST m1)) *0))`
1550+
>> (`((\t. FST (m1:real#real) / (SND m1 + FST m1) * exp (-(SND m1 + FST m1) * &t)) --> 0) =
1551+
((\t. (\t. FST m1 / (SND m1 + FST m1))t * (\t. exp (-(SND m1 + FST m1) * &t)) t)
1552+
--> ((FST m1 / (SND m1 + FST m1)) *0))`
15401553
by RW_TAC real_ss[])
15411554
>> POP_ORW
15421555
>> MATCH_MP_TAC SEQ_MUL

‎examples/dependability/case_studies/WSNScript.sml

Lines changed: 8 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -14,23 +14,17 @@
1414
(* *)
1515
(* ========================================================================= *)
1616

17-
(*loadPath := "/home/waqar/Downloads/RBD" :: !loadPath;*)
18-
19-
(*app load ["arithmeticTheory", "realTheory", "prim_recTheory", "seqTheory",
20-
"pred_setTheory","res_quanTheory", "res_quanTools", "listTheory", "real_probabilityTheory", "numTheory",
21-
"transcTheory", "rich_listTheory", "pairTheory", "extra_pred_setTools",
22-
"combinTheory","limTheory","sortingTheory", "realLib", "optionTheory","satTheory",
23-
"util_probTheory", "extrealTheory", "real_measureTheory", "real_lebesgueTheory","real_sigmaTheory",
24-
"dep_rewrite","RBDTheory","FT_deepTheory","VDCTheory","smart_gridTheory","ASN_gatewayTheory"];*)
25-
open HolKernel Parse boolLib bossLib limTheory arithmeticTheory realTheory prim_recTheory real_probabilityTheory
17+
open HolKernel boolLib bossLib Parse;
18+
19+
open limTheory arithmeticTheory realTheory prim_recTheory real_probabilityTheory
2620
seqTheory pred_setTheory res_quanTheory sortingTheory res_quanTools listTheory transcTheory
2721
rich_listTheory pairTheory combinTheory realLib optionTheory util_probTheory extrealTheory real_measureTheory
28-
real_lebesgueTheory real_sigmaTheory satTheory numTheory dep_rewrite extra_pred_setTools
29-
RBDTheory FT_deepTheory VDCTheory smart_gridTheory ASN_gatewayTheory ;
22+
real_lebesgueTheory real_sigmaTheory satTheory numTheory dep_rewrite extra_pred_setTools;
23+
24+
open RBDTheory FT_deepTheory VDCTheory smart_gridTheory ASN_gatewayTheory;
3025

3126
fun K_TAC _ = ALL_TAC;
3227

33-
open HolKernel boolLib bossLib Parse;
3428
val _ = new_theory "WSN";
3529

3630
(*--------------------*)
@@ -62,8 +56,10 @@ RW_TAC std_ss[]
6256
>> RW_TAC list_ss[]
6357
>> RW_TAC list_ss[exp_func_list_def,list_sum_def,list_prod_def]
6458
>> RW_TAC real_ss[GSYM transcTheory.EXP_ADD]
59+
>> AP_TERM_TAC
6560
>> REAL_ARITH_TAC
6661
QED
62+
6763
(*------------------------------------*)
6864
Theorem one_minus_exp_equi :
6965
!t c. (one_minus_list (exp_func_list c t)) =

‎examples/dependability/case_studies/smart_gridScript.sml

Lines changed: 10 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -14,20 +14,18 @@
1414
(* *)
1515
(* ========================================================================= *)
1616

17-
(*app load ["arithmeticTheory", "realTheory", "prim_recTheory", "seqTheory",
18-
"pred_setTheory","res_quanTheory", "res_quanTools", "listTheory", "real_probabilityTheory", "numTheory", "dep_rewrite",
19-
"transcTheory", "rich_listTheory", "pairTheory", "extra_pred_setTools",
20-
"combinTheory","limTheory","sortingTheory", "realLib", "optionTheory","satTheory",
21-
"util_probTheory", "extrealTheory", "real_measureTheory", "real_lebesgueTheory","real_sigmaTheory",
22-
"RBDTheory","FT_deepTheory","VDCTheory","ASN_gatewayTheory"];*)
23-
24-
open HolKernel Parse boolLib bossLib limTheory arithmeticTheory realTheory prim_recTheory real_probabilityTheory
17+
open HolKernel boolLib bossLib Parse;
18+
19+
open limTheory arithmeticTheory realTheory prim_recTheory real_probabilityTheory
2520
seqTheory pred_setTheory res_quanTheory sortingTheory res_quanTools listTheory transcTheory
2621
rich_listTheory pairTheory combinTheory realLib optionTheory dep_rewrite extra_pred_setTools
27-
util_probTheory extrealTheory real_measureTheory real_lebesgueTheory real_sigmaTheory satTheory numTheory
28-
RBDTheory FT_deepTheory VDCTheory ASN_gatewayTheory;
29-
open HolKernel boolLib bossLib Parse;
22+
util_probTheory extrealTheory real_measureTheory real_lebesgueTheory real_sigmaTheory
23+
satTheory numTheory;
24+
25+
open RBDTheory FT_deepTheory VDCTheory ASN_gatewayTheory;
26+
3027
val _ = new_theory "smart_grid";
28+
3129
(*--------------------*)
3230
val op by = BasicProvers.byA;
3331
val POP_ORW = POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]);
@@ -933,7 +931,7 @@ RW_TAC std_ss[]
933931
>> `Reliability p ESWs t = exp (-C_ESWs * t)` by RW_TAC std_ss[Reliability_def]
934932
>- (FULL_SIMP_TAC real_ss[exp_distribution_def])
935933
>> POP_ORW
936-
>> REAL_ARITH_TAC
934+
>> rw [REAL_NEG_LMUL]
937935
QED
938936

939937
(*----------------------------------------------*)

0 commit comments

Comments
 (0)