Hi Brian, first of all, your report has indeed exposed a flaw in the processing of class declarations which has been corrected in http://isabelle.in.tum.de/repos/isabelle/rev/eddda8e38360,
Unfortunately, the processing of class declarations is notoriously
difficult, especially if the infamous "base sort" is something else than
{type}.
> class foo = cpo +
> fixes foo :: "'a → 'a"
>
> class bar = foo + pcpo +
> assumes "foo⋅⊥ = ⊥"
The main issue is that ⊥ is just "global" as ⊥::pcpo; for be able to
cope with such class specification may feature a specific "base sort":
> class foo =
> fixes foo :: "'a → 'a"
>
> class bar =
> assumes "foo⋅⊥ = (⊥::'a::{foo, pcpo})"
But is extremely difficult if not impossible to mix base-sort-based
inheritance with the regular class inheritance. If ⊥ would exist in a
local variant in class pcpo, you would just write:
> class foo = cpo +
> fixes foo :: "'a::type → 'a"
>
> class bar = foo + pcpo +
> assumes "foo⋅(⊥'a::::type) = ⊥"
I admit that the class command comes with a strong assumption that users
develop their specifications locally if they want refer to them in class
specifications and if not the old-style axclass sometimes appeared more
leigthweight. However additional options etc. emulating this old
behaviour complicate the whole matter notoriously.
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
