Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Parametric theories

Email Gateway (Aug 18 2022 at 19:32):

From: Daniel Schoepe <daniel@schoepe.org>
Hi,

I'm trying to build a theory that is parametric in some types and
would like to know the recommended way for doing that. I realize that
this topic has come up before and that this problem is partially(?)
solved by locales. From what I have read on this list (for example in
[1]), my choices are the following:

1. Use type variables everywhere -- this will get very tiresome very
   quickly. Locales don't seem to offer a complete way around that either,
   at least the following does not seem to work:

locale Foo = fixes x :: "'a"
begin
type_synonym bar = "'a \times 'a"
end

2. Use typedecl, consts, and similar commands. This seems ideal apart
   from instantiating the theory later. Here I think I have two choices:
   Use the AWE tool [2], which seems to do exactly what I want, but was
   last updated for Isabelle 2009-1, or a post-hoc axiomatization using
   directives like type_definition and axioms.

Am I overlooking some possibility, or is that basically it? If so, is
there an up-to-date version of AWE, or does someone know how much work
it would take to update it (I noticed that at least the isar-keywords.el
files of 2011-1 and AWE have diverged, but there are probably more
complicated conflicts than that).

Is there some "convention" on how deal with this issue, as I can imagine
this comes up quite often?

Regards,
Daniel

[1] https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2009-July/msg00111.html
[2] http://www.informatik.uni-bremen.de/~cxl/awe/

Email Gateway (Aug 18 2022 at 19:33):

From: Makarius <makarius@sketis.net>
On Wed, 11 Apr 2012, Daniel Schoepe wrote:

I'm trying to build a theory that is parametric in some types and
would like to know the recommended way for doing that.

It depends what "parameteric on types" shall mean exactly. Depending on
plain type parameters in the manner of schematic polymorphism works quite
painlessly, and type inference sorts out things most of the time, without
too much explicit type annotations.

In contrast, depending on type constructors with their own type
arguments does not work within the logic, and requires something like AWE
from Bremen.

Use type variables everywhere -- this will get very tiresome very
quickly. Locales don't seem to offer a complete way around that either,
at least the following does not seem to work:

locale Foo = fixes x :: "'a"
begin
type_synonym bar = "'a \times 'a"
end

Normally you just refer to 'a, 'b, 'c in your specifications causally (or
implicitly), without introducing too many explicit types mentioned in the
formal text. So it might not be as tiresome as anticipated, depending on
the application.

A type_synonym within a local theory context could be made to work, but it
is not so often required in practice to induce significant demands to
implement that. Other things are more urgent, sich as datatype and record
types within local contexts.

Makarius

Email Gateway (Aug 18 2022 at 19:35):

From: Daniel Schoepe <daniel@schoepe.org>
On Sat, 14.04.2012 22:02, Makarius wrote:

It depends what "parameteric on types" shall mean exactly. Depending on
plain type parameters in the manner of schematic polymorphism works quite
painlessly, and type inference sorts out things most of the time, without
too much explicit type annotations.

In contrast, depending on type constructors with their own type
arguments does not work within the logic, and requires something like AWE
from Bremen.

Luckily, just ordinary type parameters are needed in my case.

Use type variables everywhere -- this will get very tiresome very
quickly. Locales don't seem to offer a complete way around that either,
at least the following does not seem to work:

locale Foo = fixes x :: "'a"
begin
type_synonym bar = "'a \times 'a"
end

Normally you just refer to 'a, 'b, 'c in your specifications causally (or
implicitly), without introducing too many explicit types mentioned in the
formal text. So it might not be as tiresome as anticipated, depending on
the application.

While I do have only three or four type parameters, I am using
more or less intricate combinations of them quite often, such as
"(('a \<times> 'b) list \<times> ('c \<Rightarrow> 'd)"

Hence I would prefer to have the ability to give these constructs a name
without having to mention the parameters each time again. (I could
construct a type_synonym that needs to be applied to some parameters,
but then I'd still have to write "('a, 'b, 'c, 'd) SomeSynonym").

I guess I'll give using AWE with the current Isabelle version a shot,
and use type_synonyms with parameters if that fails.

Anyway, thanks for your detailed answer!

A related issue I'm curious about: What was the rationale for
introducing typedecl without a straight-forward way to instantiate it?
Being able to define something that has only been declared earlier seems
rather natural to me.

Regards,
Daniel

Email Gateway (Aug 18 2022 at 19:35):

From: Makarius <makarius@sketis.net>
On Wed, 18 Apr 2012, Daniel Schoepe wrote:

I could construct a type_synonym that needs to be applied to some
parameters, but then I'd still have to write "('a, 'b, 'c, 'd)
SomeSynonym".

Yes, that's the normal way. Moreover, you can often suppress type
information in the input, say you write some of the type arguments as "_"
and let type inference take care of the rest. Or you don't write types at
all.

BTW, most names in Isabelle are normally just lower case like "foo_bar",
including type names. Capitalization like Foo_Bar is always used for
theory names, datatype constructors, and sometimes for special operators.
Camel-case is generally out of fashion.

A related issue I'm curious about: What was the rationale for
introducing typedecl without a straight-forward way to instantiate it?
Being able to define something that has only been declared earlier seems
rather natural to me.

The classic canon for axiomatic specifications consists of typedecl,
consts, axioms. You can do whatever you want here, but there are no
sanity checks. For example you can first "declare" some types, and then
"define" them -- all axiomatically. Here is an old example from HOL/Bali
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2011-1/src/HOL/Bali/Example.thy#l66

Historically, Isabelle theories were always axiomatic like that. Later
the vacous axiomatization of 'consts' followed by a definitional
axiomatization of 'defs' (i.e. 'axioms' with some checks) were called
definitions.

Much later, an actual definitional concept was made the main principle of
the local theory infrastructure that is commonplace today. It performs
the usual simultaneous declaration-definition of entities seen in most
other provers and in mathematics. There are also technical and conceptual
reasons for it -- definitions that depend on local contexts work out
better if the RHS is explicitly given.

The surface syntax wraps up these truly definitional primitives as
'definition', 'function', 'induction' etc. For types, this is still a bit
limited, though. (Back to start of thread.)

Makarius

Last updated: Apr 26 2024 at 01:06 UTC