Simplified code with prob_div_mul_refl lemma (#1298)

* Simplified code with prob_div_mul_refl lemma * Replace MATCH_MP_TAC by simp[prob_div_mul_refl]
HOL-Theorem-Prover · Sep 10, 2024 · 14b4197 · 14b4197
1 parent 7bf55e0
commit 14b4197
Showing 1 changed file with 24 additions and 48 deletions.
diff --git a/src/probability/probabilityScript.sml b/src/probability/probabilityScript.sml
@@ -8617,6 +8617,19 @@ Proof
  >> METIS_TAC [PROB_FINITE]
 QED
 
+Theorem prob_div_mul_refl :
+  !p A x. prob_space p /\ A IN events p /\ prob p A <> 0 ==>
+          x / prob p A * prob p A = x
+Proof
+  rpt STRIP_TAC
+  >> `prob p A <> PosInf /\ prob p A <> NegInf` by METIS_TAC [PROB_FINITE]
+  >> `?a. prob p A = Normal a` by METIS_TAC [extreal_cases]
+  >> ‘a <> 0’ by METIS_TAC [extreal_of_num_def, extreal_11]
+  >> Q.PAT_X_ASSUM ‘prob p A = Normal a’ (ONCE_REWRITE_TAC o wrap)
+  >> ONCE_REWRITE_TAC [EQ_SYM_EQ]
+  >> MATCH_MP_TAC div_mul_refl >> art []
+QED
+
 Theorem COND_PROB_COMPL :
     !p A B. prob_space p /\ A IN events p /\ COMPL A IN events p /\
             B IN events p /\ prob p B <> 0 ==>
@@ -8639,10 +8652,7 @@ Proof
  >> STRIP_TAC
  >> ASM_SIMP_TAC std_ss [sub_rdistrib, num_not_infty, mul_lone]
  >> Know `prob p (A INTER B) / prob p B * prob p B = prob p (A INTER B)`
- >- (MATCH_MP_TAC EQ_SYM \\
-    `?b. prob p B = Normal b` by METIS_TAC [extreal_cases] \\
-    `b <> 0` by METIS_TAC [extreal_of_num_def, extreal_11] >> art [] \\
-     MATCH_MP_TAC div_mul_refl >> art []) >> Rewr'
+ >- simp[prob_div_mul_refl]
  >> ASM_SIMP_TAC std_ss [eq_sub_ladd]
  >> `prob p ((COMPL A) INTER B) + prob p (A INTER B) =
      prob p (((COMPL A) INTER B) UNION (A INTER B))`
@@ -8683,16 +8693,10 @@ Proof
      METIS_TAC [div_not_infty]) >> STRIP_TAC
  >> ASM_SIMP_TAC std_ss [sub_rdistrib]
  >> Know `prob p (A1 INTER B) / prob p B * prob p B = prob p (A1 INTER B)`
- >- (MATCH_MP_TAC EQ_SYM \\
-    `?b. prob p B = Normal b` by METIS_TAC [extreal_cases] \\
-    `b <> 0` by METIS_TAC [extreal_of_num_def, extreal_11] >> art [] \\
-     MATCH_MP_TAC div_mul_refl >> art []) >> Rewr'
+ >- simp[prob_div_mul_refl]
  >> Know `prob p (A1 INTER A2 INTER B) / prob p B * prob p B =
           prob p (A1 INTER A2 INTER B)`
- >- (MATCH_MP_TAC EQ_SYM \\
-    `?b. prob p B = Normal b` by METIS_TAC [extreal_cases] \\
-    `b <> 0` by METIS_TAC [extreal_of_num_def, extreal_11] >> art [] \\
-     MATCH_MP_TAC div_mul_refl >> art []) >> Rewr'
+ >- simp[prob_div_mul_refl]
  >> ASM_SIMP_TAC std_ss [eq_sub_ladd]
  >> `prob p ((A1 DIFF A2) INTER B) + prob p (A1 INTER A2 INTER B) =
         prob p (((A1 DIFF A2) INTER B) UNION (A1 INTER A2 INTER B))`
@@ -8731,15 +8735,9 @@ Proof
  >> `prob p B < PosInf` by METIS_TAC [lt_infty]
  >> `0 < prob p B` by METIS_TAC [le_lt, PROB_POSITIVE]
  >> Know `prob p (B INTER A) / prob p A * prob p A = prob p (B INTER A)`
- >- (MATCH_MP_TAC EQ_SYM \\
-    `?a. prob p A = Normal a` by METIS_TAC [extreal_cases] \\
-    `a <> 0` by METIS_TAC [extreal_of_num_def, extreal_11] >> art [] \\
-     MATCH_MP_TAC div_mul_refl >> art []) >> Rewr'
+ >- simp[prob_div_mul_refl]
  >> Know `prob p (B INTER A) / prob p B * prob p B = prob p (B INTER A)`
- >- (MATCH_MP_TAC EQ_SYM \\
-    `?b. prob p B = Normal b` by METIS_TAC [extreal_cases] \\
-    `b <> 0` by METIS_TAC [extreal_of_num_def, extreal_11] >> art [] \\
-     MATCH_MP_TAC div_mul_refl >> art []) >> Rewr
+ >- simp[prob_div_mul_refl] >> rw[]
 QED
 
 Theorem COND_PROB_UNION :
@@ -8781,16 +8779,10 @@ Proof
     `A1 DIFF A2 IN events p` by METIS_TAC [EVENTS_DIFF] \\
      METIS_TAC [COND_PROB_FINITE]) >> Rewr'
  >> Know `prob p (A2 INTER B) / prob p B * prob p B = prob p (A2 INTER B)`
- >- (MATCH_MP_TAC EQ_SYM \\
-    `?b. prob p B = Normal b` by METIS_TAC [extreal_cases] \\
-    `b <> 0` by METIS_TAC [extreal_of_num_def, extreal_11] >> art [] \\
-     MATCH_MP_TAC div_mul_refl >> art []) >> Rewr'
+ >- simp[prob_div_mul_refl]
  >> Know `prob p ((A1 DIFF A2) INTER B) / prob p B * prob p B =
           prob p ((A1 DIFF A2) INTER B)`
- >- (MATCH_MP_TAC EQ_SYM \\
-    `?b. prob p B = Normal b` by METIS_TAC [extreal_cases] \\
-    `b <> 0` by METIS_TAC [extreal_of_num_def, extreal_11] >> art [] \\
-     MATCH_MP_TAC div_mul_refl >> art []) >> Rewr'
+ >- simp[prob_div_mul_refl]
  >> `(A1 UNION A2) INTER B IN events p` by METIS_TAC [EVENTS_UNION, EVENTS_INTER]
  >> `A2 INTER B IN events p` by METIS_TAC [EVENTS_INTER]
  >> `(A1 DIFF A2) INTER B IN events p` by METIS_TAC [EVENTS_INTER, EVENTS_DIFF]
@@ -8827,10 +8819,7 @@ Proof
  >> BETA_TAC >> Rewr'
  >> REWRITE_TAC [cond_prob_def, Once mul_comm]
  >> Know `!i. prob p (A i INTER B) / prob p B * prob p B = prob p (A i INTER B)`
- >- (GEN_TAC >> MATCH_MP_TAC EQ_SYM \\
-    `?b. prob p B = Normal b` by METIS_TAC [extreal_cases] \\
-    `b <> 0` by METIS_TAC [extreal_of_num_def, extreal_11] >> art [] \\
-     MATCH_MP_TAC div_mul_refl >> art []) >> Rewr'
+ >- simp[prob_div_mul_refl] >> Rewr'
  >> `SIGMA (\i. prob p (A i INTER B)) (count n) = SIGMA (prob p o (\i. A i INTER B)) (count n)`
         by METIS_TAC [] >> POP_ORW
  >> Know `BIGUNION (IMAGE A (count n)) INTER B = BIGUNION (IMAGE (\i. A i INTER B) (count n))`
@@ -8852,19 +8841,6 @@ Proof
  >> PROVE_TAC []
 QED
 
-Theorem prob_div_mul_refl :
-  !p A x. prob_space p /\ A IN events p /\ prob p A <> 0 ==>
-          x / prob p A * prob p A = x
-Proof
-    rpt STRIP_TAC
- >> `prob p A <> PosInf /\ prob p A <> NegInf` by METIS_TAC [PROB_FINITE]
- >> `?a. prob p A = Normal a` by METIS_TAC [extreal_cases]
- >> ‘a <> 0’ by METIS_TAC [extreal_of_num_def, extreal_11]
- >> Q.PAT_X_ASSUM ‘prob p A = Normal a’ (ONCE_REWRITE_TAC o wrap)
- >> ONCE_REWRITE_TAC [EQ_SYM_EQ]
- >> MATCH_MP_TAC div_mul_refl >> art []
-QED
-
 Theorem BAYES_RULE :
     !p A B. prob_space p /\ A IN events p /\ B IN events p /\
             prob p A <> 0 /\ prob p B <> 0 ==>
@@ -8881,11 +8857,11 @@ Proof
  >> ASM_SIMP_TAC bool_ss [ldiv_eq]
  >> Know `cond_prob p A B * prob p B / prob p A * prob p A =
           cond_prob p A B * prob p B`
- >- (MATCH_MP_TAC prob_div_mul_refl >> art [])
+ >- simp[ prob_div_mul_refl]
  >> Rewr'
  >> REWRITE_TAC [cond_prob_def]
  >> Know `prob p (A INTER B) / prob p B * prob p B = prob p (A INTER B)`
- >- (MATCH_MP_TAC prob_div_mul_refl >> art []) >> Rewr'
+ >- simp[prob_div_mul_refl] >> Rewr'
  >> REWRITE_TAC [Once INTER_COMM]
 QED
 
@@ -8951,7 +8927,7 @@ Proof
      RW_TAC std_ss [COND_PROB_FINITE]) >> BETA_TAC >> Rewr'
  >> RW_TAC std_ss [cond_prob_def, Once mul_comm]
  >> Know `!i. prob p (A i INTER B) / prob p B * prob p B = prob p (A i INTER B)`
- >- (GEN_TAC >> MATCH_MP_TAC prob_div_mul_refl >> art []) >> Rewr'
+ >- (GEN_TAC >> simp[prob_div_mul_refl]) >> Rewr'
  >> REWRITE_TAC [mul_rone, Once EQ_SYM_EQ, Once INTER_COMM]
  >> MATCH_MP_TAC PROB_EXTREAL_SUM_IMAGE_FN
  >> RW_TAC std_ss [INTER_IDEMPOT, EVENTS_INTER]