[isabelle-dev] simps_of_case and function types

[Lars Noschinski]

On 25.08.2015 18:16, Lars Noschinski wrote:
> Hi everyone,
> Unfortunately, simps_of_case cannot use the Splitter, as splitter
> applies the split-rule in the wrong direction. So simps_of_case either
> needs to reimplement the Splitter's logic for instantiating the split
> rule or the Splitter needs to be refactored generate the instantiated
> equation.

That being said, a shortcut is possible if one requires the equation
given to simps_of_case to be of the form

   "... = case x of ..."

Does anyone rely on the more liberal form "... = P (case x of ...)"
accepted at the moment?