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

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

> 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…>

interpretation c: c … <proof>

lemma result1 = c.result1

lemma result2 = c.result2



Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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