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



Dear all,

sorry, no answer. Just a related question (I think). For those who prefer stackoverflow, it can also be found here:

  http://stackoverflow.com/q/16556633/476803

In NEWS I found

  * Command 'typedef' now works within a local theory context -- without
  introducing dependencies on parameters or assumptions, which is not
  possible in Isabelle/Pure/HOL.  Note that the logical environment may
  contain multiple interpretations of local typedefs (with different
  non-emptiness proofs), even in a global theory context.

(which dates back to Isabelle2009-2). Is this the latest news with respect to typedef and local theory contexts? Further, what does the restriction "without introducing dependencies on parameters or assumptions" actually mean?

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?).

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"

which sounds similar to what Randy is experiencing.

cheers

chris

On 05/15/2013 06:48 AM, Randy Pollack wrote:
Hi,

Consider the cut-down locale definition:

locale step =
   label:lattice where sup = lblsup
   for lblsup::"'a => 'a => 'a"

In the context of this locale want a type synonym:

type_synonym 'a atm = "int * 'a"

This is rejected:

*** Locally fixed type arguments "'a" in type declaration "atm"

OK, but the following is also rejected:

type_synonym atm = "int * 'a"
*** Extra variables on rhs: "'a"

Is it possible to make such a type synonym in a locale?

Thanks,
Randy






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