Re: [isabelle] instance declaration problem with axiomatic classes



Brian Huffman wrote:

> Instead of using the type class mechanism here, you could accomplish
> what you want using predicates on types. ...

> This is much more flexible than any instance declaration in Isabelle
> could be.  But the drawback is that you lose automation: Instead of
> sort annotations you will need to add explicit sizelimit assumptions
> to your theorems, which you will then have to discharge manually
> using inference rules like the one above.

Yes, this would definitely suffice.  But I'm afraid it's not really an
option given what we're doing and where we're up to at the moment.  We
are making pretty heavy use of our "memtype" class, which encodes "is
representable in memory", and it would be a pain to lose that
automation.  We also don't have the time to go back and re-engineer
everything.

We will get round the problem by showing

  instance array :: (oneMB_orless, lt_four_thousand) mem_type

once and for all, and then showing that the examples we're working
with satisfy those constraints.  (Declaring an array of 5000 ints
won't be allowed, but we're working with a pretty restricted codebase,
so we can be confident that we're happy with this restriction.)

Michael.





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