Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Vector type syntax


view this post on Zulip Email Gateway (Aug 22 2022 at 16:38):

From: Makarius <makarius@sketis.net>
Yes, probably.

Note that this hard-wired policy comes from the following changeset by
Johannes Hölzl:

changeset: 34290:1edf0f223c6e
user: hoelzl
date: Thu Jan 07 17:43:35 2010 +0100
files: src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
description:
added syntax translation to automatically add finite typeclass to index
type of cartesian product type

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 16:38):

From: Makarius <makarius@sketis.net>
On 05/02/18 12:57, Lawrence Paulson wrote:

On 1 Feb 2018, at 12:57, Dominique Unruh <unruh@ut.ee> wrote:

The constraints imposed by ^ are relatively half-hearted in any case. The following types are accepted:

typ "real^real"
type_synonym 'a id = "'a"
typ "real^('n::{finite,wellorder} id)"
typ "real^('n::{wellorder} id)"

The reason is that the parse translation adds the ::{finite} constraint only if the second argument to ^ is a type variable.

It feels to me that no enforcement might be better than such half-hearted enforcement.

I usually also prefer a clear situation, without too much builtin magic
(here the silent addition of a sort constraint due to concrete syntax).
But this appears to be infeasible now ...

The following is not allowed: as the second occurrence of ’n is assigned a different sort from the first. This is not how sort assignment normally works, so I think we should see if there is some way to obtain more natural behaviour without forcing hundreds of theorem statements to be altered.

Systematic counting with the included ch-vec_syntax in
Isabelle/5348bea4accd + AFP/e9f2114df805 (excluding very_slow sessions)
yields the following results:

3273 T ^ 'a (type variable)
2920 T ^ U (other type)
6193 total

fixes f :: "real^'n::{finite,wellorder} ⇒ real^'n"

Maybe the following ch-dummy_sort is already sufficient (cf.
Isabelle/17874d43d3b3). With that you can write:

fixes f :: "real^'n::{finite,wellorder} ⇒ real^'n::_"

The dummmy sort looks syntactically like a sort constraint, and the vec
syntax translation will not add anything. Later the sort disappears, and
type inference proceeds as usual.

Makarius
ch-vec_syntax
ch-dummy_sort

view this post on Zulip Email Gateway (Aug 22 2022 at 16:40):

From: Johannes Hölzl <johannes.hoelzl@gmx.de>
As fas as I remember this changeset is from a time when we didn't have a euclidean_space type class.
Since then most occurrences of "'a ^ 'n" are replaced by "'a :: euclidean_space" in HOL-Analysis.
I'm okay if somebody wants to change this again.

Also I'm not sure what's the situation in the AFP (espeially Joses entries) and IsarFoR which uses
some finite dimensional modules (i.e. 'a::ring ^ 'n) .

view this post on Zulip Email Gateway (Aug 22 2022 at 16:41):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear all,

for us the change will most likely not dramatic, however it will also have
some impact on ML-code. I believe the most demanding AFP-entry from our side
is Perron-Frobenius, where we automatically generate types via local type definitions
in order to transfer type-based matrix-theorems to set-based ones. If this
machinery can be adapted, then I see no problem from our side.

Cheers,
René

view this post on Zulip Email Gateway (Aug 22 2022 at 16:43):

From: Lawrence Paulson <lp15@cam.ac.uk>
The following is not allowed: as the second occurrence of ’n is assigned a different sort from the first. This is not how sort assignment normally works, so I think we should see if there is some way to obtain more natural behaviour without forcing hundreds of theorem statements to be altered.

fixes f :: "real^'n::{finite,wellorder} ⇒ real^'n"

view this post on Zulip Email Gateway (Aug 22 2022 at 16:45):

From: Lawrence Paulson <lp15@cam.ac.uk>
Vector types, similar to those in HOL Light, have been available for some time: real^’n abbreviates (real, 'n) vec, where ’n is some finite index type. But a number of theorems require an ordering on that type, so we sometimes see types such as (real, 'n::{finite,wellorder}) vec. Such types cannot be written as real^’n because that syntax constrains the sort on ’n to {finite}.

What can we do about this? Is it possible to separate the ‘a^’n syntax from any specific sort constraints on the type ’n? And if not, should it use the sort constraint {finite,wellorder} instead? Every finite type can be well ordered, even without the axiom of choice, so the sort constraint {finite} is not really more general than {finite,wellorder}.

Larry Paulson

view this post on Zulip Email Gateway (Aug 22 2022 at 16:46):

From: Dominique Unruh <unruh@ut.ee>
The constraints imposed by ^ are relatively half-hearted in any case. The
following types are accepted:

typ "real^real"
type_synonym 'a id = "'a"
typ "real^('n::{finite,wellorder} id)"
typ "real^('n::{wellorder} id)"

The reason is that the parse translation adds the ::{finite} constraint
only if the second argument to ^ is a type variable.

It feels to me that no enforcement might be better than such half-hearted
enforcement.

Best wishes,
Dominique.


Last updated: Mar 28 2024 at 12:29 UTC