Re: [isabelle] Datatype: Sort constraint and nested datatypes



Hi Peter,

Coming back to an old thread:

> On 02.02.2016, at 15:14, Peter Lammich <lammich at in.tum.de> wrote:
> 
> Consider:
> 
> datatype 'a::order undef = Undefined | Defined "'a"
> 
> datatype 'a::order node = Node "'a node undef"
> 
> The second command raises:
> 
> Tactic failed
> The error(s) above occurred for the goal statementâ:
> âf g. size_node f â map_node g = size_node (f â g)
> 
> 
> This does not occur if one removes the sort constraint on undef. The
> sort constraint on Node seems to be unrelated.
> 
> This behaviour is present in Isabelle2015, and also in 2016-RC3.
> 
> 
> (Partial) workaround: The well-known Imperative-HOL hack gives you back
> some of the sort contraints:

Another workaround would be to pass (plugins del: size) right after the "datatype" keyword. Then you can define the size function manually.

In any case, I have just pushed a change to Testboard to address this. The change will likely not be part of the next release, but of Isabelle2017, since there are many workarounds.

Cheers,

Jasmin





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