Email Gateway (Aug 19 2022 at 10:54): Email Gateway (Aug 19 2022 at 10:54):From: Leo Freitas <leo.freitas@newcastle.ac.uk>
Hi,
I am new to Isabelle and its type ways of declaring / defining new types.
In particular when extending type classes like say nat1 as an extension of nat (n > 0).
I couldn't find it in the sources and I wondered if someone has done this already.
Looking at Nat.thy and Orderings.thy I saw the main aspects of Nat characterisation
but failed to properly extend my theory to cope with something like nat1.
Any help / clues is much appreciated.
Best,
Leo
Email Gateway (Aug 19 2022 at 10:54):From: John Wickerson <jpw48@cam.ac.uk>
Hi Leo,
You can use the "typedef" command to create new types like this. See
http://isabelle.in.tum.de/dist/Isabelle2013/doc/tutorial.pdf
on pages 173-176 for more information.
Best wishes,
John
Email Gateway (Aug 19 2022 at 10:54):From: Tobias Nipkow <nipkow@in.tum.de>
Am 15/04/2013 17:39, schrieb Leo Freitas:
Hi,
I am new to Isabelle and its type ways of declaring / defining new types.
In particular when extending type classes like say nat1 as an extension of nat (n > 0).
You will not become a happy person if you define your own type nat1 because
there will be zero automation for it. You will have to duplicate everything that
is there for nat already, slowly, over time. Or you constantly convert between
nat and nat1, because all the predefined functions operate on nat. I don't
recommend it.
Just for terminology: nat is a type, not a type class.
Tobias
I couldn't find it in the sources and I wondered if someone has done this already.
Looking at Nat.thy and Orderings.thy I saw the main aspects of Nat characterisation
but failed to properly extend my theory to cope with something like nat1.Any help / clues is much appreciated.
Best,
Leo
Email Gateway (Aug 19 2022 at 10:54):From: Stephan van Staden <Stephan.vanStaden@inf.ethz.ch>
Hi John,
I think this use of "typedef" is deprecated. Although Isabelle still
accepts it, I remember seeing warnings.
All the best,
Stephan
Email Gateway (Aug 19 2022 at 10:55):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Stephan,
"Typedef" is still as encouraged as ever (modulo Tobias's warnings about the lack of automation). The warnings were probably tied to a specific usage of typedef. This is from the "NEWS" file:
* Simplified 'typedef' specifications: historical options for implicit
set definition and alternative name have been discontinued. The
former behavior of "typedef (open) t = A" is now the default, but
written just "typedef t = A". INCOMPATIBILITY, need to adapt theories
accordingly.
If I recall right, during the transition period, "typedef" without "open" used to generate a warning.
Regards,
Jasmin
Last updated: Nov 21 2024 at 12:39 UTC