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

[Randy Pollack]

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

[Christian Sternagel]

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

[Jasmin Blanchette]

Hi Randy,

Am 14.05.2013 um 23:48 schrieb Randy Pollack <rpol...@inf.ed.ac.uk>:

> 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"

The above looks like a bug. However, there's an easy workaround:

type_synonym 'b atm = "int * 'b"

Cheers,

Jasmin

[Makarius]

On Tue, 14 May 2013, Randy Pollack wrote:

> 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"

Witin the locale context type 'a is locally fixed, i.e. a local type
constant. Thus it cannot be used again as parameter for the type_synonym.
You have to avoid the clash of scope manually like this:

type_synonym 'b atm = "int * 'b"

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

It is in principle possible to support that, but adding even more
infrastructure to local context. The localized version of type_synonym in
Isabelle2013 is still a bit crude in that respect. I did not push this
further so far, because so many other tools that introduce types are not
fully localized yet and need to catch up with the advances from 2009/2010.


Makarius

[Makarius]

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