Proving and Applying Program Transformations Expressed with Second-Order Patterns