[isabelle-dev] simps_of_case and function types

Lars Noschinski 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
> 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?




More information about the isabelle-dev mailing list