Given two typeclasses (e.g.
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
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
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
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.)