Re: [isabelle] Arity limitations of type classes? [SOLVED]



Rafal,

Your WordsARM.thy file is still missing two important instance declarations:

instance num1 :: word_len_1_2 (* necessary for 16 :: word_len_8_16_32 *)
  by (intro_classes, simp)

instance num1 :: word_len_1_2_4 (* necessary for 8 :: word_len_8_16_32 *)
  by (intro_classes, simp)

To see why these are necessary, you can trace what the type checker does when trying to prove, for example, that 16 :: word_len_8_16_32:

num1 bit0 bit0 bit0 bit0 :: word_len_8_16_32
num1 bit0 bit0 bit0 :: word_len_4_8_16
num1 bit0 bit0 :: word_len_2_4_8
num1 bit0 :: word_len_1_2_4
num1 :: word_len_1_2

Similarly, 8 :: word_len_8_16_32 reduces to num1 :: word_len_1_2_4.

Alternatively, you could prove the subclass relations word_len_1 < word_len_1_2 < word_len_1_2_4, and the system would infer the missing class instances for num1 automatically.

- Brian

Quoting Rafal Kolanski <rafalk at cse.unsw.edu.au>:

Brian,

Thank you very, very much. I've been bashing my head against this for a
while. As of now, thanks to you, I have a non-hacky class of words
which are actually storable in C on a 32-bit architecture.

Regarding Florian's comment on using new-style classes, I'm attaching
what I have (the word_len_8_16_32 class is the one I wanted). It
doesn't use axclasses, but does use instance instead of instantiation
as the proofs are relatively simple.

Sincerely,

Rafal Kolanski.

Brian Huffman wrote:
[An ingenious idea]







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