[isabelle] Vector type syntax

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

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