[isabelle] Datatype: Sort constraint and nested datatypes



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.