I'd like to include example instances of various structures in an Isabelle document, just as is often done in mathematics textbooks.
If we look at the formalisation of an algebra text by Clemens Ballarin, we see a lot of structures and theorems, but ... most algebra texts not only describe structures and theorems, but also give examples. If you were writing a text about manifolds, for instance, it'd make a lot of sense to give the $n$-dimensional sphere $S^n$, the $n$-dimensional projective space $P^n$, and the $n$-dimensional torus $T^n = S^1 \times S^1 \times \ldots \times S^1$ as examples, and then use these examples throughout multiple chapters. I've love to do the last of these (use in multiple places), but I'd be happy to just be able to make a concrete example and say "Here, this is one of these.".
To be clear: Ballarin diverges from the Algebra module in Isabelle by basing things onsets rather than types. Here's Ballarin's definition of a monoid, for instance:
locale monoid =
fixes M and
composition (infixl "·" 70) and
unit ("1")
assumes
composition_closed: "[[ a ∈ M; b ∈ M ]] ⇒ a · b ∈ M" and
unit_closed: "1 ∈ M" and
associative: "[[ a ∈ M; b ∈ M; c ∈ M ]] ⇒ (a · b) · c=a· (b · c)"
and left_unit: "a ∈ M ⇒ 1 · a=a"
and right_unit: "a ∈ M ⇒ a · 1 =a
(my apologies for any formatting mistakes resulting from copy-paste). Clearly in this example, $M$, the "carrier" of the monoid, is a set.
As an example:
The set U = {3, 5} with the operation $$ T : U \times U \to U $$ defined by $$T(a,3) = a; \\ T(3, b) = b;\\ T(5,5) = 3$$
is a monoid. (It's just a thinly-disguised version of the usual 2-element group, with 3 serving as the identity element).
I'd imagine doing this by saying the "Set" portion of my monoid is U = {3, 5}, a subset of the naturals; the group operation is defined on the naturals, with $T(a, b)$ undefined unless $a$ and $b$ are both in $U$, and then I'd use the automatically-generated local predicate to assert
theorem: monoid U T 3
and then give a (presumably very short) proof.
My question then is "How can I describe and name the set U and the function T outside of the context of a theorem?" I could presumably phrase everything in a form like
theorem:
fixes U T
assumes "U = {3, 5}" and
"T(3, 3) = 3" and
"T(3, 5) = 5" and
"T(5, 3) = 5" and
"T(5, 5) = 3"
shows "monoid U T 3"
but if (a) if the definition of $T$ was more complex, it might be nice to do it separately, and
(b) I'd done something similar to describe $S_3$, the symmetric group on 3 elements, I might want to go on and say more about $S_3$, like "it has several 2-element subgroups" and "it has an element of order 3" and "it has no element of order 6". So (back to the simpler example) I'd like not only to be able to name $U$ and $T$, but I'd also like to give a name to the monoid 'locale' that they together constitute --- maybe $M_2$.
Is there a way to do this? I recognize that introducing new named constants is generally a bad idea, but one could presumably do all this in a notepad
context (at least if there was no reason to refer to $M_2$ or $S_3$ later in the text).
BTW, it'll be tempting to say "You COULD have just made $U$ be the type bool
, and replaced $T$ with and
, and this would all have been easy." By my question is not "how could I have done this differently?" but "How can I (even temporarily, for a few theorems, say) give names to particular sets/functions/whatever?"
The actually context I care about is synthetic projective geometry, where I have two sets (Points and Lines), a function 'join' from pairs of points to lines (undefined if the two arguments are equal), a function 'meet' from pairs of lines to point (undefined if the two arguments are equal), etc. I'd like to be able to describe the 7-point projective plane (and the associated 4-point affine plane) and repeatedly use it as an example. That requires a set of 7 points to start with, and I figured I could just use the natural numbers $1$ through $7$ as my points, and have join
be a nat => nat => ... function that's undefined when either argument is outside the range $[1, 7]$.
alternatingGroup A
which uses any finite typeA
as a carrier, but the official $A_n$ isalternatingGroup (Fin n)
, whereFin n
is the canonical typen
elements. $\endgroup$