Re: [isabelle] Importing classes into a locale in Isabelle and other related questions

Dear Dr Florian Haftmann,

Thank your comments.

The extracts from the post that is available on
forum/#!topic/fa.isabelle/kRHYNQ3uFCU/discussion were helpful and provide
an explanation for the observation that I made in the concluding remarks of
my question.

Also, with the help of the previous answer and your comments, I believe I
have gained a certain level of understanding of the problem that is related
to the propagation of the notation/syntax from classes to locales. However,
I would also like to gain further understanding of the meaning and
significance of clause 5 in the post that is available on
could not find any comments on clause 5 within the post, although several
comments on other clauses were made):

> 5. A result proven with locales can always be converted to the
>   equivalent result with typeclasses by interpretation. However, a result
>   proved with typeclasses cannot be converted to locales, because
>   instantiation of a typeclass is not allowed inside a proof.

Lastly, if possible, I would like to provide a copy of your reply on stack
overflow. Please let me know if this is acceptable (of course, I will
provide a link to your original answer). Alternatively, please let me know
if you would prefer to provide an answer on stack overflow yourself or you
would prefer your answer not to be copied to stack overflow.


On Thu, May 17, 2018 at 12:26 PM, Florian Haftmann <
florian.haftmann at> wrote:

> Dear xanonec,
> to start with:
> > Lastly, as a side note, I have noticed that there may be a certain
> amount> of partial code duplication in HOL. In particular, it seems to me
> that
> the> theories in HOL/Lattice/, HOL/Algebra/Order-HOL/Algebra/Lattice
> and> HOL/Library/Boolean_Algebra resemble the theory in HOL/Orderings->
> HOL/Lattices. However, I am not certain if the equivalence between
> these> theories was established through the sublocale/subclass
> relationship (e.g.> see class_deps) to a sufficient extent. Of course, I
> understand that the> theories use distinct axiomatisation and the
> theories in HOL/Algebra/ and> HOL/Library/Boolean_Algebra are based on
> locales. Furthermore, the theories> in HOL/Algebra/ contain a certain
> amount of information that has not been> formalised in other theories.
> However, I would still like to gain a better> understanding why all four
> theories co-exist in HOL and the relationship> between these theories is
> not always clearly indicated.
> This is a re-occuring topic on this mailing list, so let me quote from
> an older post
> (!topic/fa.isabelle/
> kRHYNQ3uFCU/discussion):
> > as a rule of thumb, there are basically two algebraic hierarchy
> > developments in HOL:
> >
> > HOL-Main with type classes:
> > * implicit use due to type inference
> > * pragmatic and simple sharing between similar types
> > * explicit definitions
> > * directly executable
> >
> > HOL-Algebra with locales:
> > * explicit carrier – possibility to develop proper meta theory (*)
> > * implicit definitions where possible
> > * suitable for mathematics
> (*) The meaning of »meta theory« in this context is roughly that you can
> reason *about* algebraic structures, not only on properties of their
> elements.  For example, the classification of all simple groups would be
> meta theory, whereas the statement »The integers form a group wrt. +, 0
> and -« is not.
> HOL/Library/Boolean_Algebra is somewhat special as it seems to be used
> only in HOL-Word.
> Concerning re-using classes in locales: classes carry only global
> syntax: i.e. < always refers to the global constant less, but during
> input / output occurences on local type 'a are replaces by the local
> less (»user space type system«).  Hence, when building a local upon a
> class, syntax must be installed explicitly.
> It might also be the case that you only want to take over some results
> from an existing class; then it is usually better to formulate the
> locale stand-alone and use a confined interpretation:
> class c = …
> locale l = … <operations, syntax, assumptions…>
> begin
> interpretation c: c … <proof>
> lemma result1 = c.result1
> lemma result2 = c.result2
> …
> end
> Hope this helps,
>         Florian
> --
> PGP available:
> at_informatik_tu_muenchen_de

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