[isabelle-dev] Quotient example with partiality?

[Makarius]

On Tue, 29 Nov 2011, Cezary Kaliszyk wrote:

> It would be nice to get it fully localized but still the meaning of 
> typedef that restricts a type fixed in a locale is quite unclear. Or has 
> this been cleared in the meantime?

Locales are the standard example for a local theory target, but not the 
only one.

"Localization" means to conform to certain operations of the generic 
context, say when introducing local parameters ("fixes") or working with 
implicit polymorphism (via declare_term), and further extra-logical things 
like name spaces and notation, and more.  There is a spectrum here, and 
full localization is an ogoing process, to update things according to the 
system APIs of 2008, say; many tools are still stuck in 1998.


Brushed-up interfacing to the infrastructure leads to new possibilities in 
the applications.

For the logical part one could also think of AWE as local theory target, 
and then one could actually depend on axiomatic parameters and premises in 
type definitions.

For the non-logical part, a trivial target like this would help a lot in 
writing manuals in a fully formal way, without auxiliary perl patching of 
the sources (or generated latex):

   example
   begin

   datatype foo = Foo | Bar foo

   definition ...

   lemma ...

   end

This would merely manage the name spaces, to keep the typical many 
variants of similar examples disjoint.  Currently one needs workarounds 
like foo, foo', foo'', foo\<zeta> etc.


 	Makarius