Email Gateway (Aug 18 2022 at 11:18): Email Gateway (Aug 18 2022 at 11:18):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Greetings,
I have defined my own type, pptr_t which encapsulates another type such
as machine words, nats or whatnot:
datatype 'a pptr_t = PPtr 'a
I have a function pptr_val which gives back the encapsulated type, and
I've proved:
instance pptr_t :: (type)ord
instance pptr_t :: (order)order
Now, I am curious at to why I can't seem to prove:
finite {PPtr a..<PPtr (a + of_nat lev1pt_size)}
Where a is a 32 bit machine word. Note that
finite {(j::32 word)..<k}
goes away by simp.
What is the minimum I need to do to mimic this behaviour? (I've tried
stating membership in linorder, but that doesn't seem to be it)
Any guidance would be much appreciated!
Yours Sincerely,
Rafal Kolanski.
Email Gateway (Aug 18 2022 at 11:18):From: Lawrence Paulson <lp15@cam.ac.uk>
That set isn't finite, because "a" could have type real. You have to
express that type 'a can be order-embedded into the naturals.
Larry Paulson
Email Gateway (Aug 18 2022 at 11:18):From: Lawrence Paulson <lp15@cam.ac.uk>
Something like
EX f:: 'a => nat. ALL x y. x<y ==> f x < f y
Larry
Email Gateway (Aug 18 2022 at 11:18):From: Brian Huffman <brianh@cs.pdx.edu>
Hi Rafal,
I would suggest that you prove
instance pptr_t :: (finite) finite
A useful lemma would be that (UNIV::'a pptr_t set) = PPtr ` UNIV.
I am assuming that type word also has an instance of class finite; if
not, then you will have to prove this as well. Then the simplifier
should be able to prove
finite {PPtr a..<PPtr (a + of_nat lev1pt_size)}
just because of its type.
Quoting Rafal Kolanski <rafalk@cse.unsw.edu.au>:
Email Gateway (Aug 18 2022 at 11:19):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
I think that that particular set is finite, because of_nat will return a
word of some kind (making a that same kind of word), and words are, in
my understanding, finite.
So what I really want is to say that if 'a can be order-embedded into
the naturals, then so can my type carrying 'a. Unfortunately, I don't
know the isabelle statement that states this.
Any further pointers?
Sincerely,
Rafal Kolanski.
Lawrence Paulson wrote:
Email Gateway (Aug 18 2022 at 11:19):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Brian,
Thank you! That was exactly what was needed and the lemma you suggested
was the way to go.
Now all other lemmas about finiteness of pointer sets go away by simp,
based just on type.
Sincerely,
Rafal Kolanski.
P.S. For those who are curious why I would ever want to have carrier
types in the first place, it's so I can have type safety (and
overloading) between virtual and physical pointers; on most machines
they are identical (e.g. 32 word).
Brian Huffman wrote:
Last updated: May 03 2024 at 04:19 UTC