Email Gateway (Aug 18 2022 at 19:40): Email Gateway (Aug 18 2022 at 19:40):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
I want to do something like "Max {[0,1],[1,0]}" but I think that I need
to somehow define a linear ordering on "nat list", am I right? Is there
somewhere that I can read about how to do this?
Email Gateway (Aug 18 2022 at 19:41):From: John Wickerson <jpw48@cam.ac.uk>
I reckon this is a job for isabelle's "type classes". You should make an instantiation of the "linorder" class (defined in http://isabelle.in.tum.de/library/HOL/Orderings.html) for nat lists.
Email Gateway (Aug 18 2022 at 19:42):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
Thank you! I have not used type classes before, but after reading about
them, I think I can make it work.
Email Gateway (Aug 18 2022 at 19:45):From: Peter Gammie <peteg42@gmail.com>
Before you do, have a poke around the Isabelle sources. There are a few theories about list orders already in there (e.g. "Length Lexicographic Ordering" in src/HOL/List.thy and probably a prefix order somewhere).
cheers
peter
Email Gateway (Aug 18 2022 at 19:50):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
Maybe I am going about this the wrong way. What I really want to do is
to be able to talk about the greatest element in the domain of a function
whose domain is finite. I want this for two reasons, but one of them is
because I want to state that a property that defines a subset of these
functions that map their domains completely. The way I was thinking of
doing this was getting the Max element of the domain and then saying
something like "domain f = {x. low domain f <= x < max domain f}" or some
such.
Am I completely off base here?
Email Gateway (Aug 18 2022 at 19:56):From: Peter Gammie <peteg42@gmail.com>
On 02/05/2012, at 1:58 PM, Aaron W. Hsu wrote:
On Wed, 02 May 2012 11:14:33 +1000, Peter Gammie wrote:
Before you do, have a poke around the Isabelle sources. There are a few
theories about list orders already in there (e.g. "Length Lexicographic
Ordering" in src/HOL/List.thy and probably a prefix order somewhere).Maybe I am going about this the wrong way. What I really want to do is
to be able to talk about the greatest element in the domain of a function
whose domain is finite.
The greatest element of a finite set? Take a look at the Finite_Set theory - max is commutative so you can use the fold combinator for finite sets.
I want this for two reasons, but one of them is
because I want to state that a property that defines a subset of these
functions that map their domains completely. The way I was thinking of
doing this was getting the Max element of the domain and then saying
something like "domain f = {x. low domain f <= x < max domain f}" or some
such.Am I completely off base here?
I don't know.
One approach is simply to carry around a predicate that indicates where the function is defined.
You can see another approach in HOLCF, where the "('a, 'b) cfun" type constructor identifies the subset of HOL functions that are continuous. Coarsely put all lemmas that require continuity then have it as a side condition, e.g. beta_cfun.
See also Alex Krauss's descriptions of his fun package, which has some treatment of partially-defined functions.
It depends on how your domains and functions are parameterised. Perhaps you can give us more information on what you're trying to do.
cheers
peter
Email Gateway (Aug 18 2022 at 20:01):From: Tobias Nipkow <nipkow@in.tum.de>
Warning: HOL functions are total, there is no notion of a domain. That is, the
domain is always the whole type. If you want to express that the function is
partial, you need to do so explicitly. Peter already suggested carrying the
domain around explicitly or using HOLCF. Making it a function to type "option"
is another option ;-)
Tobias
Email Gateway (Aug 18 2022 at 20:01):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
I am trying to come up with a basic notion of multi-dimensional arrays
that I can use to model some things. Specifically, these arrays should
map indices to specific values, be finite, and should be dense. The most
basic thing I want to do with them is to get the shape. This, I want to
have functions with the following type:
f :: "'a array => 'a array"
And similar. The property of density is the one I am having trouble with
right now. I want to state that for an array of a given shape, all of
the indices of the given shape from [0,...,0] to [n_1-1,...,n_r-1] are
defined, but no others, assuming that the array is of rank r, where n_i
is the size of the array in dimension i, with 1 <= i <= r.
Any suggestions on the best way to model this would be appreciated.
Right now I am using Map.
Email Gateway (Aug 18 2022 at 20:01):From: Ramana Kumar <rk436@cam.ac.uk>
One simplistic approach to modelling those arrays would be to represent an
array as a triple (or, better, a record) of a size (of type nat) a
dimension (of type nat) and a function (of type nat list => 'a option).
Then define a predicate isArray :: 'a array_record => bool, which is
something along the lines of
isArray a = forall ls. (length ls = a.dimension) and (forall x. member x ls
==> x < a.size) <=> not (a.f ls = NONE)
which says that the function is equal to some value exactly when the index
list is valid.
(sorry I don't know the exact Isabelle syntax for that statement above - I
usually use a different theorem prover. hopefully my pseudocode is clear.)
You could then either carry that isArray predicate as a precondition on
most everything you prove (you could use locales to make that easier, i.e.
you wouldn't have to keep typing it out), or you could use isArray to
actually define a new array type, where all of those arrays would be valid,
but that may make it harder to reason about them, depending on what kind of
reasoning you need to do.
Last updated: Nov 21 2024 at 12:39 UTC