Suppose I wanted to formalize Turing's proof regarding the halting problem so that a machine could check it. Some of the well-known automated theorem proving systems include Mizar, Coq, and HOL4. I downloaded and experimented with Coq, but it doesn't have a library for Turing machines. I thought to code one myself, but found the tutorial lacking and the language difficult to pick up.
My question is: Is there an automated theorem prover that is generally good at proving theorems that involve Turing machines? I would consider such a theorem prover "good" if it can formalize a proof of the undecidability of the halting problem using already-existing libraries. I would consider it even better if it's relatively easy to pick up. (For the record, I don't usually have difficulty with programming languages.)
Here is an Isabelle/HOL library containing Rice's theorem, which states undecidability of a wide range of problems. Since this library models computability via recursive functions, you have to encode a universal Turing machine as a recursive function in order to use this theorem for proving undecidability of the halting problem of Turing machines. However, the essential parts of the undecidability proof is already done.
External links referenced by this document: