  Quantum Hoare Logic (QHL) was introduced in Ying's work to specify and reason
about quantum programs. In this paper, we implement a theorem prover for QHL
based on Isabelle/HOL. By applying the theorem prover, verifying a quantum
program against a specification is transformed equivalently into an order
relation between matrices. Due to the limitation of Isabelle/HOL, the
calculation of the order relation is solved by calling an outside oracle
written in Python. To the best of our knowledge, this is the first theorem
prover for quantum programs. To demonstrate its power, the correctness of two
well-known quantum algorithms, i.e., Grover Quantum Search and Quantum Phase
Estimation (the key step in Shor's quantum algorithm of factoring in polynomial
time) are proved using the theorem prover. These are the first mechanized
proofs for both of them.
