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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
