Re: [isabelle] abelian_group
E.g., monoid_mult (type class, in HOL) vs. monoid (locale, in
HOL-Algebra). The classes have the advantage of being easier to use than
locales in many cases (at least I feel that way), but they have the
limitation of always having UNIV as the carrier.
(I had asked this question long ago here, though.) I had tried to unify
them, but gave up due to a locale behavior that I don't understand.
My approach was defining locales with a predicate for carrier, like
locale magma =
fixes f (infixl "❙*" 70) and member
assumes closed: "⋀a b. member a ⟹ member b ⟹ member (a ❙* b)"
By instantiating member by "λx. True", and simplifying "True ⟹" away we
get unrestricted statements. However, after
interpretation mult: magma where member = "λx. True" and f = "( * )"
rewrites "⋀P. (True ⟹ PROP P) ≡ PROP P"
by (unfold_locales, simp_all)
mult.closed is still "True ⟹ True ⟹ True" not "True".
I'm happy to contribute my code and some work if someone can make this
As far as I know, all proofs are simply done twice. And someone building
a development on these things needs to pick on approach and is then
"locked in", which is problematic, since some material is only available
in the HOL approach and some only in the HOL-Algebra approach.
In case of an overhaul, perhaps these concepts could be unified as well?
I am not sure what the best approach is for such a unification, but some
idea would be:
* Have compatible names as far as possible. E.g., if the class is
called XXX, then the locale is called l_XXX or something.
* Have the possibility to transfer theorems between compatible classes
and locales. (Compatible means: when the class is the locale with
o For transferring from locale to class, that might work
automatically (haven't checked) if we prove "sublocale XXX <=
o For transferring from class to locale it more difficult.
Possibly something involving the Types_To_Sets tools might work?
Unfortunately, I fear that even though there is not /that/ much material
building on HOL-Algebra, it would involve a lot of work.
What if instead of editing HOL-Algebra, a new session HOL-Algebra2 is
created? And then deprecating HOL-Algebra. (Or even renaming HOL-Algebra
Then it will be optional to update old AFP material building on
I also don't think there are any "heavy" users of HOL-Algebra these days
I wonder whether that might partially be because of the incompatibility
with the type-class approach. (I, at least, never look at HOL-Algebra
because we are building on real_vector_space in our formalizations and
thus "locked in".)
This archive was generated by a fusion of
Pipermail (Mailman edition) and