*To*: Dominique Unruh <unruh at ut.ee>, Manuel Eberl <eberlm at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] abelian_group*From*: Akihisa Yamada <ayamada at trs.cm.is.nagoya-u.ac.jp>*Date*: Sat, 13 Apr 2019 19:36:32 +0900*In-reply-to*: <34fc0cf8-ab4f-1afb-f66e-5de6d4979b71@ut.ee>*References*: <A80C58ED-7E98-4574-9A67-7CA0259B6885@cam.ac.uk> <c9a110dbc97a8746e664e8809c58b4b3@in.tum.de> <02fca555-ade5-1d81-f5ae-f33b4cd71532@in.tum.de> <34fc0cf8-ab4f-1afb-f66e-5de6d4979b71@ut.ee>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:60.0) Gecko/20100101 Thunderbird/60.6.1

Hello,

E.g., monoid_mult (type class, in HOL) vs. monoid (locale, inHOL-Algebra). The classes have the advantage of being easier to use thanlocales in many cases (at least I feel that way), but they have thelimitation of always having UNIV as the carrier.

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

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

Best, Akihisa

As far as I know, all proofs are simply done twice. And someone buildinga development on these things needs to pick on approach and is then"locked in", which is problematic, since some material is only availablein 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 someidea 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 carrier:=UNIV.) 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 iscreated? And then deprecating HOL-Algebra. (Or even renaming HOL-Algebrato HOL-Algebra-Old.)Then it will be optional to update old AFP material building onHOL-Algebra.I also don't think there are any "heavy" users of HOL-Algebra these daysI wonder whether that might partially be because of the incompatibilitywith the type-class approach. (I, at least, never look at HOL-Algebrabecause we are building on real_vector_space in our formalizations andthus "locked in".)Best wishes, Dominique.

**References**:**[isabelle] abelian_group***From:*Lawrence Paulson

**Re: [isabelle] abelian_group***From:*Clemens Ballarin

**Re: [isabelle] abelian_group***From:*Manuel Eberl

**Re: [isabelle] abelian_group***From:*Dominique Unruh

- Previous by Date: Re: [isabelle] abelian_group
- Next by Date: [isabelle] Types-To-Sets: a question about further development of the framework (may be of interest to the topic Re: abelian_group)
- Previous by Thread: Re: [isabelle] abelian_group
- Next by Thread: Re: [isabelle] abelian_group
- Cl-isabelle-users April 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list