Simplified code with prob_div_mul_refl lemma

[KaiPhan]

Hi,

This PR follows #1293 and further simplified more theorems in probabilityTheory.

Kai Phan

[mn200]

Where you are calling MATCH_MP_TAC yourlemma followed by simplification, have you tried just

    simp[yourlemma]

if the preconditions are easy for the simplifier to eliminate, it seems as if this would make the proofs simpler still.

[KaiPhan]

I already updated code by replace MATCH_MP_TAC yourlemma to simp[yourlemma].
It worked!
Thanks for your advice.

[binghe]

You can do even better by replacing the tactic pattern:

 >> Know `prob p (A1 INTER B) / prob p B * prob p B = prob p (A1 INTER B)`
 >- simp[prob_div_mul_refl]
 >> Rewr'

with just simp[prob_div_mul_refl]. In this case, the simplifier will search in the subterms of the current proof goal for all possible terms having the pattern x / prob p B * prob p B where B IN events p is in assumptions (or can be easily derived from some assumptions).

Note also that my habit of first doing a Know ... >- (...) and then Rewr' (or Rewr), all using tactics from hurdUtils, is to first prove a subgoal, say P, and immediately put it into the existing proof goal (e.g. Q), to form a new proof goal P ==> Q, and Rewr' (:= DISCH_THEN (fn th => ONCE_REWRITE_TAC [th]) will use P to rewrite Q once, and the whole process does not touch the assumptions at all. Thus, when you are replacing the old subgoal proofs with the one-line simp [...], the remaining Rewr' shouldn't be omitted, even sometimes the whole proof still works (the following rewriting tactics may still strip the subgoal to achieve the same final effects.)

[mn200]

Thanks for your work on this!