[isabelle-dev] docs for new datatype package

[Jasmin Blanchette]

Hi Gerwin,

> 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
    print_theorems

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"
    print_theorems

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.

Sounds reasonable.

>> 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.

Jasmin