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