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



Hi Peter,

it is a bit too much to expect the datatype package to instantiate the order type class while defining node. Iâm actually quite surprised that this works that well: it fails only in the size plugin (which might be fixable by Jasmin), and works if you add a (plugins del: size) annotation to node (you will need to add the size instance for node yourself). This is actually quite better than the old packageâs behavior ;-)

theory Scratch imports
  "~~/src/HOL/Library/Old_Datatype"
begin

old_datatype 'a::order undef = Undefined | Defined "'a"

old_datatype 'a::order node = Node "'a node undefâ

end

Cheers,
Dmitriy


> On 02 Feb 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:
> 
> datatype 'a undef = Undefined | Defined "'a"
> 
> setup {* Sign.add_const_constraint 
>  (@{const_name Defined}, SOME @{typ "'a::order â 'a undef"}) *}
> setup {* Sign.add_const_constraint 
>  (@{const_name Undefined}, SOME @{typ "'a::order undef"}) *}
> 
> 
> Best,
>  Peter
> 
> 





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