[isabelle-dev] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]

[Florian Haftmann]

Hi Clemens,

>>> Concerning \mu and \nu, I am currently investigating whether an import
>>> swap could re-establish the situation known from Isabelle2016-1
>>
>> see http://isabelle.in.tum.de/repos/isabelle/rev/5a42eddc11c1

> I had overlooked that \mu and \nu are global constants when importing
> this material, which I had received from Simon Foster.  This needs to be
> addressed properly.

I did have a look at the overall situation but IMHO there are too many
open ends which cannot be resolved before the upcoming release:

* »no_notation« would mess up the material considerably and is difficult
to place: traditionally, HOL-Algebra has no universal entry point which
is guaranteed to be imported after all other theories.

* Specific syntax could be placed into bundles, but this cannot be done
incrementally.

* Giving up \mu and \nu and coming up with an alternative syntax.

* …

Each of these requires subtantial thinking and appears much too invasive
to me.

> Your workaround merely helps users of Group, not of Complete_Lattice. 

That is the relevant point for the upcoming release: users of Group in
Isabelle2016-1 (and there are many, since Group is used in substantial
parts of both distribution of AFP) need not to worry about additional
syntactic artefacts in Isabelle2017 either; Complete_Lattice is new in
Isabelle2017 and does not induce any regression problems.

> Moreover, it doesn't make sense that Complete_Lattice imports Group, and
> that the structure theorem about subgroups is now in lattice theory.

The theorem in question requires both the notion of subgroup and
complete lattices, hence the import order dictates in which theory the
theorem has to reside (btw. the current import order is similar to
HOL-Main where Complete_Lattices comes after Groups).  When placing it,
I followed the pre-existing textual reference
(http://isabelle.in.tum.de/repos/isabelle/rev/5a42eddc11c1#l1.16).  I am
happy to add the symmetric textual reference to Group.thy if this
clarifies the situation.

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170831/07129b79/attachment.sig>