Re: [isabelle] type_synonym and fixed type arguments in a locale?



On Wed, 15 May 2013, Christian Sternagel wrote:

 * Command 'typedef' now works within a local theory context -- without
 introducing dependencies on parameters or assumptions, which is not
 possible in Isabelle/Pure/HOL.

It means you cannot refer to the fixes / assumes of context in the type specification -- this is logically impossible in Isabelle/Pure/HOL. Only the non-emptyness proof lives within the context, and the resulting theorems are local. (Actual dependence of the proof on logical content of the context is hard to get in practice, though.)


If it would mean that I cannot use locale parameters in the defining set of a typedef, then I would not consider 'typedef' to be localized at all (since the only allowed instances can easily be moved outside the local context, or am I missing something?).

'typedef' is formally localized within the range of what is possible. Localization means to work with the local theory infrastructure and the context in the usual ways. For typedef this means extra-logical things like name spaces, syntax, derived declarations etc.

Historically, due to the impossibility to make typedef depend on the logical part of the context, it was not localized at all, and many tool implementations suffer from that until today.


Related to Randy's question: is it (or should it, or will it ever be) possible to do the following?

 locale term_algebra =
   fixes F :: "'a set"
   fixes V :: "'b set"
 begin

 definition "domain α = {x ∈ V. α x ≠ Var x}"

 typedef ('a, 'b) subst =
   "{α :: 'b => ('a, 'b) term. finite (domain α)}"
 end

for which I currently obtain:

 Locally fixed type arguments "'a", "'b" in type declaration "subst"

You would have to evade the scope clash as for type_synonym, by using different names for the parameters of type subst.

Nonetheless, this does not work from a logical standpoint: the dependency on term parameter V cannot be used in HOL typedef. The local theory concept does not provide magic ways to augment the logic -- it is merely infrastructure for an existing logical framework.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.