Are `subclass` and `instance` commands equivalent in defining subclass relation between typeclasses in Isabelle?

Question

Given two typeclasses (e.g. group and monoid), I have seen both the subclass and the instance commands used to establish the fact that any group is also a monoid (i.e. the subclass relation), as shown in the example below.

The two commands seem to generate similar proof requirements, but also have some differences so that the proof for one does not work for the other sometimes. For example (Isabelle 2021):

theory test
  imports Main HOL.Set
begin

declare [[show_types]] [[show_sorts]]

instance group ⊆ monoid
proof(intro_classes)
  fix x::"'a::group"
  have "÷ x ⊕ (x ⊕ 𝟬) = ÷x ⊕ x" by (simp add: invl neutl assoc_left)
  from this show "x ⊕ 𝟬 = x" by (simp add: left_cancel)
qed

subclass (in group) monoid
proof 
  fix x::"'a::group"  (* problem line*)
qed

end

The instance command generates the following proof goal:

proof (state)
goal (1 subgoal):
 1. ⋀x::'a. x ⊕ 𝟬 = x
type variables:
  'a :: group

, while the subclass command generates a similar goal but without the type constraint 'a::group:

proof (state)
goal (1 subgoal):
 1. ⋀x::'a. x ⊕ 𝟬 = x
variables:
  neutral :: 'a
  plus :: 'a ⇒ 'a ⇒ 'a
type variables:
  'a :: type

So the first command fix x::"'a::group" that worked in the instance case no longer works for the subclass case.

To me, the proof goal of the instance command seems more natural, as one starts from a group and just need to prove that it also respects the laws of monoid.

My questions are:

Are the two usages with instance/subclass supposed to be equivalent or do they express some fundamentally different facts/ideas?

If yes, when is one preferred over the other? If no, how are they different in terms of intended usage.

(I asked the same question in SO a couple of months ago, but have not received any response. Posting here to hopefully get more attention.)

Answer 1

Citing The Isabelle/Isar Reference which is part of the official documentation:

A weakened form of [subclass] is available through a further variant of instance: instance c1 ⊆ c2 opens a proof that class c2 implies c1 without reference to the underlying locales; this is useful if the properties to prove the logical connection are not sufficient on the locale level but on the theory level.

We can see this with the same example as yours in Tutorial.Axioms, on line 149 we have a theory level lemma:

theorem left_cancel:
 ((?x::?'a::group) ⊕ (?y::?'a::group) = ?x ⊕ (?z::?'a::group)) = (?y = ?z)

And on line 166 (instance group ⊆ monoid) can fix x :: 'a group as you noticed, but we also get access to left_cancel on line 172.

For subclass (in group) monoid we only get x :: 'a :: type and no access to theory level theorems (eg. left_cancel). It is still provable and will register a sublocale group < monoid which instance won't.

---

Now, to answer your two questions:

1. These usages of instance and subclass are not supposed to be equivalent. For example, as you have noticed yourself, the former carries the theory level sort 'a :: group.

2. If you the locale level is not sufficient to prove the connection, you can go with the former. The latter is useful if you want to access theorems from c2 inside the c1 context.

---

_{More references: Haskell-style type classes with Isabelle/Isar and Tutorial to Locales and Locale Interpretation}