*To*: Rafal Kolanski <rafalk at cse.unsw.edu.au>*Subject*: Re: [isabelle] Arity limitations of type classes?*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Sun, 30 Nov 2008 09:53:37 -0800*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <49323C9D.9070005@cse.unsw.edu.au>*References*: <492CD723.9070308@cse.unsw.edu.au> <20081129161802.xhxt0ml40kwwc88c@webmail.pdx.edu> <49323C9D.9070005@cse.unsw.edu.au>*User-agent*: Internet Messaging Program (IMP) H3 (4.1.6)

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

What I really want is a type class representing words of length 8, 16 or 32. I would then be able to show that words of this class are "storable" (another class) in the C sense (byte, short, int). However, once I declare word_len8 to be storable, I can't do that for word_len16 because bit0 takes word_len8 to word_len16. Sadly, I don't think there is a way to get around this nicely.

axclass card_8_16_32 < finite card_8_16_32: "CARD('a) = 8 | CARD('a) = 16 | CARD('a) = 32"

instance bit0 :: (???) card_8_16_32

axclass card_4_8_16 < finite card_4_8_16: "CARD('a) = 4 | CARD('a) = 8 | CARD('a) = 16" Now you can prove the following: instance bit0 :: (card_4_8_16) card_8_16_32

axclass card_2_4_8 < finite card_2_4_8: "CARD('a) = 2 | CARD('a) = 4 | CARD('a) = 8" axclass card_1_2_4 < finite card_1_2_4: "CARD('a) = Suc 0 | CARD('a) = 2 | CARD('a) = 4" axclass card_1_2 < finite card_1_2: "CARD('a) = Suc 0 | CARD('a) = 2" axclass card_1 < finite card_1: "CARD('a) = Suc 0" instance bit0 :: (card_2_4_8) card_4_8_16 instance bit0 :: (card_1_2_4) card_2_4_8 instance bit0 :: (card_1_2) card_1_2_4 instance bit0 :: (card_1) card_1_2 instance num1 :: card_1_2_4 instance num1 :: card_1_2 instance num1 :: card_1

consts store :: "'a::card_8_16_32 => int list" term "store (x::32)" (* OK *) term "store (x::16)" (* OK *) term "store (x::8)" (* OK *) term "store (x::64)" (* type error *) term "store (x::20)" (* type error *)

- Brian

**References**:**[isabelle] Arity limitations of type classes?***From:*Rafal Kolanski

**Re: [isabelle] Arity limitations of type classes?***From:*Brian Huffman

**Re: [isabelle] Arity limitations of type classes?***From:*Rafal Kolanski

- Previous by Date: Re: [isabelle] conversion in Isabelle
- Previous by Thread: Re: [isabelle] Arity limitations of type classes?
- Next by Thread: [isabelle] about longer computation syntax sugar
- Cl-isabelle-users November 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list