Rename Double cast to Float_

Replacement issue for #1104 targeting version 6:

With PHP's (double) cast being deprecated and already having only been an alias for the (float) cast, introduce Float_ as a replacement for the Double cast.