[isabelle] A parametrised type class for two or more parametrised types?
Dear Isabelle Gurus,
I think I've reached the edge of Isabelle's type system again, but just
to be sure of that, I wanted to ask (Brian Huffman rode a white horse to
my rescue just recently :). I've tried to make my question as generic as
Let's say I have two parametrised types:
datatype 'a paddr_t = PAddr 'a
datatype 'a vaddr_t = VAddr 'a
which I've made a member of a type class:
class addrs = type
instance paddr_t :: (type) addrs ..
instance vaddr_t :: (type) addrs ..
The issue is having an overloaded addr_val which will pull out the
value. Currently I instantiate the types first and so have:
addr_val :: "'a::addrs => 32 word"
"addr_val (x::(32 word) paddr_t) == paddr_val x"
"addr_val (x::(32 word) vaddr_t) == vaddr_val x"
Is there any way to make this generic over the type contained in addresses?
If I just say:
addr_val :: "'a::addrs => 'b"
then I can define the overloading with:
"addr_val (x::'b paddr_t) == (paddr_val x)::'b"
"addr_val (x::'b vaddr_t) == (vaddr_val x)::'b"
but then Isabelle stops helping me whenever I try to use it during
specification or simplification, as the return type is just anything.
From what I can tell, this isn't possible, even when for any particular
type the return type can be inferred.
For nearly all architectures, the 'b will be identical for both
definitions. I'm looking for a way to somehow stick it up there with the 'a.
What I want to do is to define a type class which fixes some parameter
over multiple types. Intuitively, to go from "'a set" and "'a list" to
"'a container", which means something like "'a (set OR list)", so I
get_a_member :: "('a container) => 'a"
and then overload it for
"get_a_member (x::'a list) == ..." and
"get_a_member (x::'a set) == ..."
I know I could do this with
datatype 'a container = Set ('a set) | List ('a list)
but I want a conclusive answer whether it can be handled with just the
Could you offer some suggestions?
This archive was generated by a fusion of
Pipermail (Mailman edition) and