Concrete examples in an Isabelle theory

Question

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]$.

Answer 1

The answer turns out to be relatively simple (as Jason Rute suggests): you can use definition to define not only functions, but other constants. Ballarin in the HOL-Algebra document does this (after 318 pages was the first place I found it, but I probably missed it earlier!):

definition integer_group
  where "integer_group = (|carrier = UNIV, monoid.mult = (+), one = (0::int)|)"

What about establishing that this thing is not just a tuple, but is actually a group as well? That's easy too:

lemma group_integer_group [simp]: "group integer_group"
  unfolding integer_group_def
proof (rule groupI; simp)
  show "/\ x::int. ∃ y. y + x = 0"
  by presburger
qed

And to make it useful in subsequent proofs? As in the lemma above, you add a bunch of lemmas to "simp" that show basic properties of the group:

lemma carrier_integer_group [simp]: "carrier integer_group = UNIV"
  by (auto simp: integer_group_def)

lemma one_integer_group [simp]: "1integer_group = 0"
  by (auto simp: integer_group_def)

and so on.

Obviously things like this should be used judiciously -- polluting the namespace with a ton of examples can make it hard for others to get things done.