Overloading in ZF?

[Victor Porton]

I'm a novice with Isabelle.

What's about overloading in Isabelle/ZF?

Can I define the same function/relation name for different sets?

Or how this issue should be solved in Isabelle/ZF?

Specifically. Can this be formalized: Let K is an arbitrary set, we
will order it by the strict order relation "<". (The issue that < is
already defined e.g. for natural numbers and I doubt whether we can
reuse it.)

Huh?

[Slawomir Kolodynski]

> What's about overloading in Isabelle/ZF?

Overloading here means that you want to make Isabelle/ZF interpret the same symbol depending on the context. This is usually possible if the meaning is defined in different locales ("locale" is a keyword in Isabelle, just think "context" instead). This means it is not possible for the < symbol, since its meaning is not defined in a locale.
The same symbols in different locales can have different meaning. However, this is not the usual overloading known from the type theory - Isabelle/ZF can not figure out the meaning of the symbol just by looking at the types of the operands, because those types are always "o" (set).

You can get an effect very similar to overloading even when you want to "overload" operators in the same locale. For example you may want to use the + symbol to denote both adding real numbers and pointwise addition of real-valued functions. This can be done by using different symbols and instructing Isabelle to print them the same way. Isabelle allows to define unlimited number of symbols using markup like \<plusforaddingnumbers> and \<plusforaddingfunctions>. Then define those symbols in the root.tex file as + and the they will show up as + in the proof document.

An almost complete setup for your example would be as follows

theory example imports Order_ZF_1

begin

text{*We import IsarMathLib's Order_ZF_1 theory that defines
the notion of strict linear order.*}

text{*Next we define a locale with assumptions and notation. The symbol
*}

locale my_ordered_set =

fixes K r
assumes "r Orders K"

fixes myless (infix "\<ls>" 68)
defines myless_def: "x \<ls> y \<equiv> \langle x, y\rangle \<in> r"

text{*Now we can prove a theorem in my_ordered_set context.*}

theorem (in my_ordered_set)

[Slawomir Kolodynski]

I sent the previous message too early.

The example should look like this:

theory example imports Order_ZF_1

begin

text{*We have imported IsarMathLib's Order_ZF_1 theory that defines

the notion of strict linear order.*}

text{*Next we define a locale with assumptions and notation.

The symbol "\<ls>" is defined in IsarMathLib's root.tex
file to print as "<".
*}

locale my_ordered_set =

fixes K r
assumes "r Orders K"

fixes myless (infix "\<ls>" 68)
defines myless_def: "x \<ls> y \<equiv> \langle x, y\rangle \<in> r"

text{*Now we can prove a theorem in my_ordered_set context.*}

theorem (in my_ordered_set) ord_not_refl:
assumes "x \<in> K" shows "\<not> (x \<ls> x)"
sorry

end