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 rewrites work.


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 <=
        l_XXX UNIV".
      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 to HOL-Algebra-Old.)

Then it will be optional to update old AFP material building on HOL-Algebra.

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".)

Best wishes,

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.