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



I should add: Why this works at all with the new package is, because the bnf structure that constitutes the abstract interface to nested recursion is mostly type-class agnostic, see e.g.

term map_undef

which has no class constraints on the parameters. In contrast the constructors and high-level theorems, such as

thm undef.map

are constrained.

Dmitriy


> On 02 Feb 2016, at 16:17, Dmitriy Traytel <traytel at inf.ethz.ch> wrote:
> 
> 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.