Value-Passing CCS in HOL