*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Evaluation of List.coset*From*: Jesus Aransay <jesus-maria.aransay at unirioja.es>*Date*: Wed, 30 Jan 2013 19:49:15 +0100*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <alpine.LNX.2.00.1301301334000.30318@macbroy21.informatik.tu-muenchen.de>*References*: <CAL0S8BcgWBZ4fJApxHYECNPx-TL+yWofkFAawq73N1AEP_D=sg@mail.gmail.com> <5108C956.5020205@inf.ethz.ch> <CAL0S8BdBNq6AL72fjQYNQSBFW=eipdP72YTEuoAvZm1M1o9mAg@mail.gmail.com> <alpine.LNX.2.00.1301301334000.30318@macbroy21.informatik.tu-muenchen.de>*Sender*: jmaransay at gmail.com

Thanks Andreas and Makarius for your hints. Andreas, just to make it clear, a type which has been proven to be an instance of "enum" (and also with a finite cardinal, of course) could be proved to be an instance of the new class "card_UNIV"? Then, "List.coset" should be evaluated for instances of the "card_UNIV" type class? My intuition is that the following question is related to the previous one; The following command: value "remdups [finite_5.a_1,finite_5.a_2,finite_5.a_3]" successfully removes duplicates from the input list (none in this case), whereas the following one (I had to prove the bit0 and bit1 type constructors to be instances of "equal", and also some code abstype and code abstract lemmas for Abs_bit1, Abs_bit0, Rep_bit0 and Rep_bit1 type morphisms): value "remdups [1::5,2::5,1::5]" does not produce any output. What information is missed in the code generator to evaluate successfully the previous command? Is it related to the cardinal of the underlying type, which is needed to compute the representation of the "1::5", "2::5" or "7::5" elements? As a more general question, in the HOL library, in file "Enum.thy" there are defined "datatypes" finite_1 up to finite_5, which are defined by enumerating its constants (a1, a1 and a2, and so on). Then, in "Numeral_Type.thy", there are generic ordinal types (for any n::nat) defined ("typedef"), in terms of a bit0 and bit1 representation, as subsets of the integers. Could not be the types "finite_n" be seen as particular cases of the ordinal types? Are there good reasons to stick with the "finite_n" types, being the ordinals far more general? Sorry for the long mail, I have been a few days working with both kinds of types and still am a bit confused, thanks for any help, Jesus

**Follow-Ups**:**Re: [isabelle] Evaluation of List.coset***From:*Andreas Lochbihler

**References**:**[isabelle] Evaluation of List.coset***From:*Jesus Aransay

**Re: [isabelle] Evaluation of List.coset***From:*Andreas Lochbihler

**Re: [isabelle] Evaluation of List.coset***From:*Jesus Aransay

**Re: [isabelle] Evaluation of List.coset***From:*Makarius

- Previous by Date: Re: [isabelle] New error messages in Isabelle 2013
- Next by Date: Re: [isabelle] New error messages in Isabelle 2013
- Previous by Thread: Re: [isabelle] Evaluation of List.coset
- Next by Thread: Re: [isabelle] Evaluation of List.coset
- Cl-isabelle-users January 2013 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