FTBFS examples/dependability

HOL-Theorem-Prover · Sep 2, 2024 · 3412be8 · 3412be8
1 parent 10aa3e3
commit 3412be8
Show file tree

Hide file tree

Showing 3 changed files with 79 additions and 72 deletions.
diff --git a/examples/dependability/AvailabilityScript.sml b/examples/dependability/AvailabilityScript.sml
@@ -372,10 +372,10 @@ RW_TAC std_ss[]
    >> DEP_REWRITE_TAC[SEQ_ADD]
    >> RW_TAC std_ss[]
    >- (RW_TAC std_ss[SEQ_CONST])
-   >- ((`(seq$--> (\t. (FST (m:real#real) / (SND m + FST m)) * exp (-(SND m + FST m) * &t)) 0) =
-         (seq$--> (\t.
+   >- ((`((\t. (FST (m:real#real) / (SND m + FST m)) * exp (-(SND m + FST m) * &t)) --> 0) =
+         ((\t.
              (\t. FST m / (SND m + FST m)) t *
-             (\t. exp (-(SND m + FST m) * &t)) t)
+             (\t. exp (-(SND m + FST m) * &t)) t) -->
          ((FST m / (SND m + FST m)) *0))` by (RW_TAC real_ss[]))
       >> POP_ORW
       >> MATCH_MP_TAC SEQ_MUL
@@ -393,8 +393,9 @@ RW_TAC std_ss[]
   >> POP_ORW
   >> MATCH_MP_TAC SEQ_ADD
   >> RW_TAC std_ss[SEQ_CONST]
-  >> (`(seq$--> (\t. FST m / (SND m + FST m) * exp (-(SND m + FST m) * &t)) 0) =
-      (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))`
+  >> (`((\t. FST m / (SND m + FST m) * exp (-(SND m + FST m) * &t)) --> 0) =
+      ((\t. (\t. FST m / (SND m + FST m))t * (\t. exp (-(SND m + FST m) * &t))t) -->
+       ((FST m / (SND m + FST m)) *0))`
        by RW_TAC real_ss[])
   >> POP_ORW
   >> MATCH_MP_TAC SEQ_MUL
@@ -406,18 +407,20 @@ RW_TAC std_ss[]
   >> RW_TAC std_ss[steady_avail_temp])
 >> RW_TAC std_ss [expec_avail_def]
 >> FULL_SIMP_TAC std_ss[inst_avail_exp_def,expec_def]
->> (`(seq$--> (\t.
+>> (`((\t.
      SND m / (SND m + FST m) +
-     FST m / (SND m + FST m) * exp (-(SND m + FST m) * &t)) (SND m / (SND m + FST m))) =
-    (seq$--> (\t.
+     FST m / (SND m + FST m) * exp (-(SND m + FST m) * &t)) --> (SND m / (SND m + FST m))) =
+    ((\t.
      (\t. SND m / (SND m + FST m)) t +
-     (\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[])
+     (\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[])
 >> POP_ORW
 >> MATCH_MP_TAC SEQ_ADD
 >> RW_TAC std_ss[]
 >- (RW_TAC std_ss[SEQ_CONST])
->> (`(seq$--> (\t. FST m / (SND m + FST m) * exp (-(SND m + FST m) * &t)) 0) =
-    (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))`
+>> (`((\t. FST m / (SND m + FST m) * exp (-(SND m + FST m) * &t)) --> 0) =
+    ((\t. (\t. FST m / (SND m + FST m))t * (\t. exp (-(SND m + FST m) * &t))t)
+     --> ((FST m / (SND m + FST m)) *0))`
       by RW_TAC real_ss[])
 >> POP_ORW
 >> MATCH_MP_TAC SEQ_MUL
@@ -529,21 +532,21 @@ GEN_TAC
 >> RW_TAC std_ss[]
 >- (FULL_SIMP_TAC list_ss[inst_avail_exp_list1_def,inst_avail_exp2_def]
    >> REWRITE_TAC[steady_state_avail_def]
-   >> (`(seq$--> (\t.
+   >> (`((\t.
      SND (h':real#real) / (SND h' + FST h') +
-     FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t))
+     FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) -->
          (SND h' / (SND h' + FST h'))) =
-     (seq$--> (\t.
+     ((\t.
      (\t. SND h' / (SND  h'+ FST h')) t +
-     (\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t))t)
+     (\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) t) -->
      (SND h' / (SND h' + FST h') + 0))` by RW_TAC real_ss[])
    >> POP_ORW
    >> MATCH_MP_TAC SEQ_ADD
    >> RW_TAC std_ss[]
    >- (RW_TAC std_ss[SEQ_CONST])
-   >- ((`(seq$--> (\t. FST  h'/ (SND h' + FST h') * exp (-(SND h'  + FST h') * &t)) 0) =
-      (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))` by RW_TAC real_ss[])
+   >- ((`((\t. FST  h'/ (SND h' + FST h') * exp (-(SND h'  + FST h') * &t)) --> 0) =
+      ((\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t)) t)
+       --> ((FST h' / (SND h' + FST h')) *0))` by RW_TAC real_ss[])
       >> POP_ORW
       >> MATCH_MP_TAC SEQ_MUL
       >> RW_TAC real_ss[SEQ_CONST]
@@ -632,19 +635,21 @@ GEN_TAC
    >> RW_TAC std_ss[SEQ_CONST]
    >> FULL_SIMP_TAC list_ss[inst_avail_exp_list1_def,inst_avail_exp2_def]
    >> REWRITE_TAC[steady_state_avail_def]
-   >> (`(seq$--> (\t.
+   >> (`((\t.
      SND (h':real#real) / (SND h' + FST h') +
-     FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) (SND h' / (SND h' + FST h'))) =
-     (seq$--> (\t.
+     FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) --> (SND h' / (SND h' + FST h'))) =
+     ((\t.
      (\t. SND h' / (SND  h'+ FST h')) t +
-     (\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t))t) (SND h' / (SND h' + FST h') + 0))`
+     (\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t))t)
+      --> (SND h' / (SND h' + FST h') + 0))`
      by RW_TAC real_ss[])
    >> POP_ORW
    >> MATCH_MP_TAC SEQ_ADD
    >> RW_TAC std_ss[]
    >- (RW_TAC std_ss[SEQ_CONST])
-   >- ((`(seq$--> (\t. FST  h'/ (SND h' + FST h') * exp (-(SND h'  + FST h') * &t)) 0) =
-        (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))`
+   >- ((`((\t. FST  h'/ (SND h' + FST h') * exp (-(SND h'  + FST h') * &t)) --> 0) =
+        ((\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t)) t)
+         --> ((FST h' / (SND h' + FST h')) *0))`
         by RW_TAC real_ss[])
       >> POP_ORW
       >> MATCH_MP_TAC SEQ_MUL
@@ -1119,19 +1124,21 @@ GEN_TAC
 >> RW_TAC std_ss[]
 >- (FULL_SIMP_TAC list_ss[inst_unavail_exp_list_def,inst_unavail_exp_def]
    >> REWRITE_TAC[steady_state_unavail_def]
-   >> (`(seq$--> (\t.
+   >> (`((\t.
      FST (h':real#real) / (SND h' + FST h') -
-     FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) (FST h' / (SND h' + FST h'))) =
-     (seq$--> (\t.
+     FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) --> (FST h' / (SND h' + FST h'))) =
+     ((\t.
      (\t. FST (h':real#real) / (SND  h'+ FST h')) t -
-     (\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t))t) (FST h' / (SND h' + FST h') - 0))`
+     (\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) t)
+      --> (FST h' / (SND h' + FST h') - 0))`
       by RW_TAC real_ss[])
    >> POP_ORW
    >> MATCH_MP_TAC SEQ_SUB
    >> RW_TAC std_ss[]
    >- (RW_TAC std_ss[SEQ_CONST])
-   >- ((`(seq$--> (\t. FST  h'/ (SND h' + FST h') * exp (-(SND h'  + FST h') * &t)) 0) =
-        (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))`
+   >- ((`((\t. FST  h'/ (SND h' + FST h') * exp (-(SND h'  + FST h') * &t)) --> 0) =
+        ((\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t)) t)
+         --> ((FST h' / (SND h' + FST h')) * 0))`
           by RW_TAC real_ss[])
       >> POP_ORW
       >> MATCH_MP_TAC SEQ_MUL
@@ -1221,19 +1228,21 @@ GEN_TAC
    >> RW_TAC std_ss[SEQ_CONST]
    >> FULL_SIMP_TAC list_ss[inst_unavail_exp_list_def,inst_unavail_exp_def]
    >> REWRITE_TAC[steady_state_unavail_def]
-   >> (`(seq$--> (\t.
+   >> (`((\t.
      FST (h':real#real) / (SND h' + FST h') -
-     FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) (FST h' / (SND h' + FST h'))) =
-     (seq$--> (\t.
+     FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) --> (FST h' / (SND h' + FST h'))) =
+     ((\t.
      (\t. FST h' / (SND  h'+ FST h')) t -
-     (\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t))t) (FST h' / (SND h' + FST h') - 0))`
+     (\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) t)
+      --> (FST h' / (SND h' + FST h') - 0))`
          by RW_TAC real_ss[])
    >> POP_ORW
    >> MATCH_MP_TAC SEQ_SUB
    >> RW_TAC std_ss[]
    >- (RW_TAC std_ss[SEQ_CONST])
-   >- ((`(seq$--> (\t. FST  h'/ (SND h' + FST h') * exp (-(SND h'  + FST h') * &t)) 0) =
-        (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))`
+   >- ((`((\t. FST  h'/ (SND h' + FST h') * exp (-(SND h'  + FST h') * &t)) --> 0) =
+        ((\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t)) t)
+         --> ((FST h' / (SND h' + FST h')) *0))`
                  by RW_TAC real_ss[])
       >> POP_ORW
       >> MATCH_MP_TAC SEQ_MUL
@@ -1408,19 +1417,21 @@ GEN_TAC
       >> POP_ORW
       >> FULL_SIMP_TAC list_ss[inst_avail_exp_list2_def,inst_avail_exp3_def]
       >> RW_TAC std_ss[steady_state_avail_def]
-      >> (`(seq$--> (\t.
+      >> (`((\t.
      SND (h':real#real) / (SND h' + FST h') +
-     FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) (SND h' / (SND h' + FST h'))) =
-     (seq$--> (\t.
+     FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) --> (SND h' / (SND h' + FST h'))) =
+     ((\t.
      (\t. SND h' / (SND  h'+ FST h')) t +
-     (\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t))t) (SND h' / (SND h' + FST h') + 0))`
+     (\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t))t)
+      --> (SND h' / (SND h' + FST h') + 0))`
             by RW_TAC real_ss[])
    >> POP_ORW
    >> MATCH_MP_TAC SEQ_ADD
    >> RW_TAC std_ss[]
    >- (RW_TAC std_ss[SEQ_CONST])
-   >- ((`(seq$--> (\t. FST  h'/ (SND h' + FST h') * exp (-(SND h'  + FST h') * &t)) 0) =
-        (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))`
+   >- ((`((\t. FST  h'/ (SND h' + FST h') * exp (-(SND h'  + FST h') * &t)) --> 0) =
+        ((\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t))t)
+         --> ((FST h' / (SND h' + FST h')) *0))`
           by RW_TAC real_ss[])
       >> POP_ORW
       >> MATCH_MP_TAC SEQ_MUL
@@ -1524,19 +1535,21 @@ Proof
 RW_TAC std_ss[]
 >> FULL_SIMP_TAC std_ss[inst_unavail_exp_def]
      >> RW_TAC std_ss[steady_state_unavail_def]
-     >> (`(seq$--> (\t.
+     >> (`((\t.
      FST (m1:real#real) / (SND m1 + FST m1) -
-     FST m1 / (SND m1 + FST m1) * exp (-(SND m1 + FST m1) * &t)) (FST m1 / (SND m1 + FST m1))) =
-    (seq$--> (\t.
+     FST m1 / (SND m1 + FST m1) * exp (-(SND m1 + FST m1) * &t)) --> (FST m1 / (SND m1 + FST m1))) =
+    ((\t.
      (\t. FST m1 / (SND  m1+ FST m1)) t -
-     (\t. FST m1 / (SND m1 + FST m1) * exp (-(SND m1 + FST m1) * &t))t) (FST m1 / (SND m1 + FST m1) - 0))`
+     (\t. FST m1 / (SND m1 + FST m1) * exp (-(SND m1 + FST m1) * &t)) t)
+      --> (FST m1 / (SND m1 + FST m1) - 0))`
            by RW_TAC real_ss[])
    >> POP_ORW
    >> MATCH_MP_TAC SEQ_SUB
    >> RW_TAC std_ss[]
    >- (RW_TAC std_ss[SEQ_CONST])
-   >> (`(seq$--> (\t. FST  (m1:real#real) / (SND m1 + FST m1) * exp (-(SND m1  + FST m1) * &t)) 0) =
-       (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))`
+   >> (`((\t. FST  (m1:real#real) / (SND m1 + FST m1) * exp (-(SND m1  + FST m1) * &t)) --> 0) =
+       ((\t. (\t. FST m1 / (SND m1 + FST m1))t * (\t. exp (-(SND m1 + FST m1) * &t)) t)
+        --> ((FST m1 / (SND m1 + FST m1)) *0))`
          by RW_TAC real_ss[])
       >> POP_ORW
       >> MATCH_MP_TAC SEQ_MUL

diff --git a/examples/dependability/case_studies/WSNScript.sml b/examples/dependability/case_studies/WSNScript.sml
@@ -14,23 +14,17 @@
 (*                                                                           *)
 (* ========================================================================= *)
 
-(*loadPath := "/home/waqar/Downloads/RBD" :: !loadPath;*)
-
-(*app load ["arithmeticTheory", "realTheory", "prim_recTheory", "seqTheory",
-          "pred_setTheory","res_quanTheory", "res_quanTools", "listTheory", "real_probabilityTheory", "numTheory",
-          "transcTheory", "rich_listTheory", "pairTheory", "extra_pred_setTools",
-          "combinTheory","limTheory","sortingTheory", "realLib", "optionTheory","satTheory",
-          "util_probTheory", "extrealTheory", "real_measureTheory", "real_lebesgueTheory","real_sigmaTheory",
-          "dep_rewrite","RBDTheory","FT_deepTheory","VDCTheory","smart_gridTheory","ASN_gatewayTheory"];*)
-open HolKernel Parse boolLib bossLib limTheory arithmeticTheory realTheory prim_recTheory real_probabilityTheory
+open HolKernel boolLib bossLib Parse;
+
+open limTheory arithmeticTheory realTheory prim_recTheory real_probabilityTheory
      seqTheory pred_setTheory res_quanTheory sortingTheory res_quanTools listTheory transcTheory
      rich_listTheory pairTheory combinTheory realLib  optionTheory util_probTheory extrealTheory real_measureTheory
-     real_lebesgueTheory real_sigmaTheory satTheory numTheory dep_rewrite extra_pred_setTools
-      RBDTheory FT_deepTheory VDCTheory smart_gridTheory ASN_gatewayTheory ;
+     real_lebesgueTheory real_sigmaTheory satTheory numTheory dep_rewrite extra_pred_setTools;
+
+open RBDTheory FT_deepTheory VDCTheory smart_gridTheory ASN_gatewayTheory;
 
 fun K_TAC _ = ALL_TAC;
 
-open HolKernel boolLib bossLib Parse;
 val _ = new_theory "WSN";
 
 (*--------------------*)
@@ -62,8 +56,10 @@ RW_TAC std_ss[]
 >> RW_TAC list_ss[]
 >> RW_TAC list_ss[exp_func_list_def,list_sum_def,list_prod_def]
 >> RW_TAC real_ss[GSYM transcTheory.EXP_ADD]
+>> AP_TERM_TAC
 >> REAL_ARITH_TAC
 QED
+
 (*------------------------------------*)
 Theorem one_minus_exp_equi :
 !t c. (one_minus_list (exp_func_list c t)) =

diff --git a/examples/dependability/case_studies/smart_gridScript.sml b/examples/dependability/case_studies/smart_gridScript.sml
@@ -14,20 +14,18 @@
 (*                                                                           *)
 (* ========================================================================= *)
 
-(*app load ["arithmeticTheory", "realTheory", "prim_recTheory", "seqTheory",
-          "pred_setTheory","res_quanTheory", "res_quanTools", "listTheory", "real_probabilityTheory", "numTheory", "dep_rewrite",
-          "transcTheory", "rich_listTheory", "pairTheory", "extra_pred_setTools",
-          "combinTheory","limTheory","sortingTheory", "realLib", "optionTheory","satTheory",
-          "util_probTheory", "extrealTheory", "real_measureTheory", "real_lebesgueTheory","real_sigmaTheory",
-          "RBDTheory","FT_deepTheory","VDCTheory","ASN_gatewayTheory"];*)
-
-open HolKernel Parse boolLib bossLib limTheory arithmeticTheory realTheory prim_recTheory real_probabilityTheory
+open HolKernel boolLib bossLib Parse;
+
+open limTheory arithmeticTheory realTheory prim_recTheory real_probabilityTheory
      seqTheory pred_setTheory res_quanTheory sortingTheory res_quanTools listTheory transcTheory
      rich_listTheory pairTheory combinTheory realLib  optionTheory dep_rewrite extra_pred_setTools
-      util_probTheory extrealTheory real_measureTheory real_lebesgueTheory real_sigmaTheory satTheory numTheory
-      RBDTheory FT_deepTheory VDCTheory ASN_gatewayTheory;
-open HolKernel boolLib bossLib Parse;
+     util_probTheory extrealTheory real_measureTheory real_lebesgueTheory real_sigmaTheory
+     satTheory numTheory;
+
+open RBDTheory FT_deepTheory VDCTheory ASN_gatewayTheory;
+
 val _ = new_theory "smart_grid";
+
 (*--------------------*)
 val op by = BasicProvers.byA;
 val POP_ORW = POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]);
@@ -933,7 +931,7 @@ RW_TAC std_ss[]
 >> `Reliability p ESWs t = exp (-C_ESWs * t)` by RW_TAC std_ss[Reliability_def]
 >- (FULL_SIMP_TAC real_ss[exp_distribution_def])
 >> POP_ORW
->> REAL_ARITH_TAC
+>> rw [REAL_NEG_LMUL]
 QED
 
 (*----------------------------------------------*)