HOL-Theorem-Prover
Name in namedCases should not be renamed if it already exists
Consider the following proof state:
P x
-----
y
Assuming that y is an option, namedCases_on ‘y’ ["", "x"] currently results in something like
P x
-----
SOME x'
Note that despite picking x as the name, it ended up being x'. I'd argue a more intuitive behavior would be for the x in the assumptions to be renamed instead.
The free variables of the assumptions are the result of earlier (explicit or implicit) naming choices. In general, names chosen later should respect those chosen earlier. But if those earlier choices are getting in the way, then rename1 and friends are available.
This is an interesting one. I eventually want to subsume this awful soup (namedCases, pairCases urge) into a more potent Cases_on tactic, but I think if the user has gone to the trouble of specifying names, then that can be treated as a subsidiary invocation of something like rename, and can thus be viewed as taking precedence over earlier naming choices.
