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


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.


Rafal Kolanski.

Brian Huffman wrote:
[An ingenious idea]

theory WordsARM imports WordMain begin

class word_len_1 = len +
  assumes word_len_1: "len_of TYPE('a) = 1"

class word_len_1_2 = len +
  assumes word_len_1_2: "len_of TYPE('a) = 1 \<or> len_of TYPE('a) = 2"

class word_len_1_2_4 = len + 
  assumes word_len_1_2_4: "len_of TYPE('a) = 1 \<or> len_of TYPE('a) = 2 \<or> len_of TYPE('a) = 4"

class word_len_2_4_8 = len + 
  assumes word_len_2_4_8: "len_of TYPE('a) = 2 \<or> len_of TYPE('a) = 4 \<or> len_of TYPE('a) = 8"

class word_len_4_8_16 = len + 
  assumes word_len_4_8_16: "len_of TYPE('a) = 4 \<or> len_of TYPE('a) = 8 \<or> len_of TYPE('a) = 16"

class word_len_8_16_32 = len + 
  assumes word_len_8_16_32: "len_of TYPE('a) = 8 \<or> len_of TYPE('a) = 16 \<or> len_of TYPE('a) = 32"

instance num1 :: word_len_1
  by (intro_classes, simp)

instance bit0 :: (word_len_1) word_len_1_2
  by (intro_classes, simp add: word_len_1)

instance bit0 :: (word_len_1_2) word_len_1_2_4
  by (intro_classes, insert word_len_1_2, simp)

instance bit0 :: (word_len_1_2_4) word_len_2_4_8
  by (intro_classes, insert word_len_1_2_4, simp)

instance bit0 :: (word_len_2_4_8) word_len_4_8_16
  by (intro_classes, insert word_len_2_4_8, simp)

instance bit0 :: (word_len_4_8_16) word_len_8_16_32
  by (intro_classes, insert word_len_4_8_16, simp)


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