Re: [isabelle] BNFs and sort constraints

Hi Jasmin,

BNF type variables may not have sort constraints. "map_id" is part of
the BNF structure, so it accordingly doesn't have sort constraints.
More high-level theorems and constants are declared with the sort
constraints. To overgeneralize a bit, Dmitriy's low-level BNF code
doesn't like sort constraints, whereas my higher-level "(co)datatype"
code copes with them to the extent possible. In the code, you'll see
this by grepping for "unsorted_As" in "bnf_fp_def_sugar.ML".

that sounds basically like what I guessed from my observations. Thanks for the clarification!

Incidentally, what is the motivation for your example? Is your
application related to item 5 in the "Known Bugs and Limitations" of
the "datatypes" document?

I don't intend to use this in any way. I'm merely trying to "tie up loose ends":

My dictionary construction will just ignore sort constraints from data constructors, and I was trying to figure out to what extent they might be introduced in datatypes, e.g. by having a constrained BNF through which recursion occurs.

The "meta-theorem" I am aiming for is that by dropping the sort constraints you'll still end up with exactly the same datatype; i.e., I want to argue that not supporting constraints in constructors is not a problem because I can always ask the user to remove the constraints.

NB, because you mentioned "limitation 5": The fact that the overloaded 0 is a constructor for "nat" is the bane of my existence. It messes with so many things and it is surprising that it works at all :-)


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