Formal Reasoning About Finite-State Discrete-Time Markov Chains in HOL