[isabelle-dev] Datatype alt_names

[Christian Urban]

I am not sure whether this is relevant, but
I have recently introduced a similar feature in 
Nominal2. There the problem is that one often 
defines several mutual-recursive nominal 
datatypes, like

  nominal_datatype 
       foo1 = ..
  and  foo2 = ..
       ....
  and  foon = ..

with n being a non-trivial number like 5 or
even more. The problem with this is that the 
generated theorems have names like

  foo1_foo2_....._foon.induct

This naming scheme is not very user-friendly.
So I decided to allow

  nominal_datatype (bar) 
       foo1 = ..
  and  foo2 = ..
       ....
  and  foon = ..

to produce 

  bar.induct

etc instead. I do not know of anything else that 
would allow the user to have control over the
generated theorem names. Is this something which 
goes against all Isabelle conventions? Could 
this be helpful for "normal" datatypes?

Best wishes,
Christian


Florian Haftmann writes:
 > Traditionally the datatype command would accept optional "alternative
 > names" used in names of type-related facts etc., e.g.
 > 
 > datatype (foo) "/*/" = Bar
 > 
 > With all HOL types being regulary named, the question arises whether we
 > still have to keep that feature or shall just discontinue it?
 > 
 > 	Florian
 > 
 > -- 
 > 
 > Home:
 > http://www.in.tum.de/~haftmann
 > 
 > PGP available:
 > http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
 > 
 > _______________________________________________
 > Isabelle-dev mailing list
 > Isabelle-dev at mailbroy.informatik.tu-muenchen.de
 > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev