Re: [isabelle] RC1: Basic_BNFs.snds

Hi Peter,

Basic_BNFs.snds is a set function for products, and therefore it naturally (i.e. like for any other type) occurs in induction rules whenever the user write the product types in a datatype declaration explicitly (as opposed to using multiple constructor arguments). 

But indeed there should be simp rules. The rules are in principle there:

thm prod_set_simps
thm sum_set_simps

However, we (Jasmin and me) have always been very conservative about default rule. Iâm pretty sure there are more such âsafe" rules that are not registered by default.

The attached patch, which currently runs on the testboard (, makes them simp rules. However, with the testboard still not testing the AFP and isatest testing isabelle-release, we are in the unfortunate situation that it is not possible to test the AFP, unless we do it on our own machines. I currently do not have the hardware at hand to build the big guys from the AFP, although I have good hope that the patch does not break anything. If somebody can confirm that, than we could push it (but it is not a very important thing, since it is easy to add simp rules locally).


Attachment: prod_sum_set_simps.patch
Description: Binary data

> On 21 Jan 2016, at 17:33, Peter Lammich <lammich at> wrote:
> Hi,
> induction on custom data types may still produce constants like
> Basic_BNFs.snds, and these have no default simplifier setup. 
> (I reported this behaviour to Dmitry privately some time ago, and just
> stumbled over it accidentally, hoping it would long be fixed)
> Things like thm Basic_BNFs.snds.simp should be in the default simpset,
> or rules like 
> "Basic_BNFs.snds (n, T) = {T}"
> --
>  Peter

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.