[isabelle-dev] simps_of_case and function types

Lars Noschinski noschinl at in.tum.de
Tue Aug 25 18:16:55 CEST 2015


Hi everyone,

Lars Hupel privately reported a situation where simps_of_case does not
work as expected (refering to 2015 and to 87f0f707a5f8).

I have not solved the issue yet (and will probably not find time the
next two months), so I document my findings here.

fun nosplit where "nosplit x f = (case x of [] ⇒ f | _ # xs ⇒ nosplit xs f)"
fun nosplit' where "nosplit' x (f :: 'a ⇒ 'b) = (case x of [] ⇒ f | _ #
xs ⇒ nosplit xs f)"

simps_of_case foo: nosplit.simps (* produces 2 theorems, as expected *)
simps_of_case foo: nosplit'.simps (* produces only one theorem! *)

The reason is that simps_of_case tries to apply the split rule for
lists, but without the elaborate steps done by the splitter. Instead, it
simply relies on Higher-Order-Unification, which falls short on these
examples.

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.

  -- Lars


More information about the isabelle-dev mailing list