I want to abbreviate create a synonym for a type class name. Here's how I'm doing it now:
class fooC = linordered_idom
instance int :: fooC
proof qed
definition foof :: "'a::fooC ⇒ 'a" where
"foof x = x"
term "foof (x::int)"
value "foof (x::int)"
This works fine if there's not a better way to do it. The disadvantage is that I have to instantiate int
, and the class
command takes time to implement itself.
Update 140314
This update is to clarify for Makarius what it is I want, to explain my purpose in wanting it, and give a list of commands that I'm familiar with for creating notation, abbreviations, and synonyms, but commands which I couldn't get to work for what I want.
My initial choice of "abbreviation" rather than "synonym"
I guess "synonym" would have been a better word, but I chose "abbreviation" because it describes what I want, which is to be able to create a shorter name for for a type class, like renaming linordered_semidom
to losdC
. Though Isar abbreviation
has some of the attributes of definition
, it also just defines syntax. So, because "abbreviate" describes what I want, and abbreviation
just defines syntax, I chose "abbreviation" instead of "synonym" or "alias".
Synonym/alias, Isar commands I couldn't get to work for that
"Alias" would describe what I want. As to the sentence "If you just want to save typing in the editor, you could use some abbreviations there," here are the commands I've experimented with to try and rename linordered_idom
, but I couldn't get them to work for me:
type_notation
type_synonym
notation
abbreviation
syntax
Rather than explain what I've tried, and try to remember what I tried, I just list them. I did searches on "class" and only found the Isar commands class
and classes
. I thought maybe locale commands might be applicable, but I didn't find anything.
What I want is simple, like how type_synonym
is used to define synonyms for types.
The purpose
There is my general desire to shorten type class names such as linordered_idom
, because eventually, I plan on using the algebra type classes extensively.
However, there is a second reason, and that is to rename something like linordered_semidom
to be part of a naming scheme of three types.
For any algebraic type class, such as linordered_semidom
, I can use that type class, along with quotient_type
, to create what I'll call a number system, such as how nat
is used to define int
.
Using Int.thy
as a template, I did that with linordered_semidom
, and then instantiated it as comm_ring_1
, which is as far as I have time to go these days.
Additionally, with typedef
, for any algebraic type class which has the dependencies of zero
and one
(and others such as ord
), I can define a type of all elements greater than or equal to zero, and another one for all elements greater than zero. I did that for linordered_idom
, but then I figured out that I actually needed to go the quotient_type
route, to get things that model rat
.
That's the long explanation. Eventually, I'll start working with numerous algebraic type classes, and from one type class, I'll get two more. If I do that for 20 type classes, and also use them, then long, descriptive names don't work, and renaming type classes will help me in knowing what type classes go together.
Here would be the scheme for linordered_semidom
, where I don't know how this will actually work out, until I'm able to try it all:
linordered_semidom
is the base class. I rename it to losdC
. It's the numbers greater than or equal to zero for these three types.
losdQ
is defined from losdC
using quotient_type
. It gives me the negative numbers, and the ability to coerce losdC
to losdQ
.
losd1
is defined using typedef
, and is the numbers greater than zero.
I need a consistent naming scheme, to keep it all straight: losdC
, losdQ
, and losd1
.
Finally, eventually even 4 types instead of 3 types
I haven't completely worked and thought things out (I'm not even close), but analogously, it's all related to implementing, for algebra type classes, the basic relationship between nat
, int
, and rat
, where real
might eventually come into play. Additionally, it's about getting a type, from these types, of the non-negative or positive members, if those don't come by default.
There is nat
used for int
, and int
used for rat
.
With nat
used for int
, we get the non-negative integers by default, which is nat
.
With int
used for rat
, we don't get the non-negative members of rat
, we get fractions. (Again, I'm talking about a type of non-negatives and positives, not a set of non-negatives and positives.)
So, if I use linordered_idom
and quotient_type
to define fractions, then I have to use typedef
twice to get the non-negative and positive members of those fractions, which means I would have 4 types to keep track of, liodC
, liodQ
, liod0
, and liod1
.
If there's a simple solution to renaming type classes, then I've unnecessarily said about 600 words.