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 MHonArc.