Mechanisation of PDA and Grammar Equivalence for Context-Free Languages