[isabelle-dev] docs for new datatype package
jasmin.blanchette at inria.fr
Tue Apr 21 19:07:02 CEST 2015
> The rule set I’d need is “typ_desc_typ_struct.inducts”, which datatype_compat doesn’t generate. It does generate the four constituent rules that I can put in a set myself, but the order of premises in these rules is different to the old datatype package, which means my goal order will still be different.
Are you sure? I didn’t try to run your big theory yet, but on this example we see that it generates what you need:
datatype a = A "b list" and b = B "a list"
datatype_compat a b
The rule you’re looking for is called “compat_a_b_a_list_b_list.induct” (no s).
> (Independent of all this, it would be nice if the primrec package did that declaration now automatically in any case)
Again, I believe it does:
primrec (nonexhaustive) f and fs and g and gs where
"f (A bs) = A (gs bs)"
| "fs Nil = Nil"
| "g (B as) = B (fs as)"
| "gs Nil = Nil"
Look for “f_fs_g_gs.induct” (no s).
> Taking ?fa = ?fb = %_. 0 seems to be what throws off the proof. I think I’ll just define size as in the old one to get the proofs working and then there should be a separate cleanup pass to refactor them into something nicer.
>> Sorry about the trouble.
> The trouble is probably more in the current proof scripts than in the datatype package update.
Yes and no. The new package’s modular approach has many advantages, including performance, and I think it stands on its own feet. We’ve had quite some positive feedback about it yet, both about the flexibility it gives (e.g. recursion through non-datatypes), the nice induction rules, and the performance.
But when it comes to “size”, I’m sorry I didn’t make it more compatible with the old one. Thankfully, there’s an easy (if tedious) workaround.
More information about the isabelle-dev