Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] selector name in datatype_new causes proof fai...

Email Gateway (Aug 19 2022 at 16:04):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear BNF developers,

in Isabelle2014, the datatype_new declaration below results in a proof failure. If I
remove the selector name specification bar, the proof succeeds. Is there anything I can do
to get the selector names I want?

datatype_new ('t, 'id) foo =
Foo "('t list ⇒ 't) + 't"
| Bar (bar: 'id)

Andreas

Email Gateway (Aug 19 2022 at 16:05):

From: Dmitriy Traytel <traytel@in.tum.de>
Hi Andreas,

if no selector is specified for datatypes, there will be none generated
(a recent policy change). Your example shows tactic failures in the case
when selectors are generated, so the problem is even worse than just
getting the right name. Fortunately, there is a simple workaround in
this case:

datatype_new (dead 't, 'id) foo =
Foo "('t list ⇒ 't) + 't"
| Bar (bar: 'id)

Marking 't explicitly as dead, changes the underlying BNFs slightly and
the tactic succeeds. In the repository version we will make the tactic
more robust also in the other case.

Thanks for the report,
Dmitriy

Last updated: Apr 18 2024 at 08:19 UTC