Automated proof of the transcendence of π in HOL light