Re: [isabelle] Lattices with explicit carrier set vs. lattices with implicit carrier set[SEC=UNCLASSIFIED]
On 27/10/2009, at 3:33 AM, Peter Lammich wrote:
> Is there a systematic/automatic way to go from theorems with the
> implicit carrier set to corresponding theorems for an explicit
> carrier set?
This is an issue that has been of interest for some time.
If you want to do interesting mathematics (eg about lattices rather
than using lattices) you really should be using explicit carrier sets.
My intuitions suggest that the existing axclass - locale binding could
be strengthened to support moving seamlessly from "pure" mathematics
(on carrier set algebras) to "applied" mathematics (on type algebras).
A "carrier" locale could be associated with the "type" axclass and new
axclasses could be developed as specialised extensions of the
"carrier" locale (restrict to single type parameter, what else?). An
instance of the axclass is induced from an interpretation of the
locale with a universal carrier set.
We have a lattice development with this sort of structure, carrier
based development of sub-lattices, lattice morphisms, and other useful
approaches to proving lattice instances. A couple of linking theorems
then connect axclass and locale to make it easy to prove type lattice
It would be nice if the Isabelle axclass mechanism gave serious
support for this sort of approach.
IMPORTANT: This email remains the property of the Australian Defence Organisation and is subject to the jurisdiction of section 70 of the CRIMES ACT 1914. If you have received this email in error, you are requested to contact the sender and delete the email.
This archive was generated by a fusion of
Pipermail (Mailman edition) and