If we assume that 1 and 2 are true then HMAC-SHA-512 is a better choice.
For the time comparison, as stated Paul Uzsak, if there is no specific time relevant problem around ~50% faster shouldn't be considered. If more secure, then use it.
For your comment;
The shatter attack on SHA-1 requires a degree of freeness in the hashed data as in PDF's. This attack may or may not apply to other formats, but still, SHA-1 is considered broken and it is already non-standard, kick out.
With the identical-prefix collision attack probably you cannot forge the MAC with this method. We haven't seen any complicated attack that uses the shatter attack to break some other constructions, yet.
The output of SHA-1 is 160-bit and it is in the generic birthday-attack range for our computing powers, especially for a collective like bit-coin miners who reached $2^{91.6}$ SHA-256 hashes per year on 25 September 2018.
512-bit is not prone to generic collision attacks. This will require $2^{256}$ hashes to find a collision with probability 50%. For SHA-256, it is still impractical for today's standards $2^{128}$ and this is equal to brute-forcing AES-128 up to some constant.
When a new attack occurs for a hash function we have to look at it so that what the attack can be used when the hash function used in HMAC construction. However, as noted by the Forest
In particular, an HMAC demands much weaker security guarantees from the hash function than many other applications it may have. It only requires weak collision resistance from the underlying hash.
For the security case You should be prepared to move into new standards. Even if there is not an attack to carry a collision attack into a HMAC construction, you should immediately move away from that hash function into more secure one.
note: Weak collision resistance is the second pre-image resistance:
it is computationally infeasible to find any second input which has the same output as any specified input, i.e., given $x$, to find a 2nd-preimage $x' \neq x$ such that $h(x) = h(x')$.
