[isabelle-dev] simps_of_case and function types
noschinl at in.tum.de
Tue Aug 25 18:26:16 CEST 2015
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
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?
More information about the isabelle-dev