Reasoning about Value-Passing Calculi in HOL