[isabelle-dev] New (Co)datatypes: Status & Plan (FYI)

[Christian Urban]

On Sunday, August 4, 2013 at 20:32:50 (+0200), Dmitriy Traytel wrote:
 > ....I.e. everything that is defined by the new package and 
 > falls into the fragment of the old package can be registered as an old 
 > datatype benefiting from all the infrastructure built around it (e.g. 
 > size function, Quickcheck, and other "datatype interpretations"). 

On the topic of size functions: I found it always odd that
the existing datatype package (however I think this particular 
functionality is now provided by the function package) defines
under <datatype_name>.simps "two" definitions of the corresponding 
size function. Consider for example


  datatype test = A1 | A2 | A3 "test"

  thm test.size

  > test_size A1 = 0
  > test_size A2 = 0
  > test_size (A3 ?test) = test_size ?test + Suc 0
  > size A1 = 0
  > size A2 = 0
  > size (A3 ?test) = size ?test + Suc 0


Surely, it would be more uniform to have just the equations for 
size, no? Is there any usage for the test_size definitions?
If not, then maybe in the course of updating the datatype 
package, this oddity can be eliminated (Nominal needed to work
around it). But I am happy to admit that I might miss something
important.

Best wishes,
Christian