*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Evaluation of List.coset*From*: Jesus Aransay <jesus-maria.aransay at unirioja.es>*Date*: Thu, 31 Jan 2013 11:37:56 +0100*Cc*: Makarius <makarius at sketis.net>, cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <510A2235.7080900@inf.ethz.ch>*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> <CAL0S8Bf-HGcDqzH5F9XLgjn6VF604JT7MNOrpkQHGUmuD43Efg@mail.gmail.com> <510A2235.7080900@inf.ethz.ch>*Sender*: jmaransay at gmail.com

Dear Andreas, thanks for your comments, they were really useful; I send attached a file where some examples of evaluations over "finite_n" types succeed, whereas the same evaluations over Numeral_Types (bit0 and bit1) do not terminate; in the file can be also found some instantiations that I missed in the Library (some of them were required for the bit0 and bit1 types to be evaluated): - bit0 and bit1 are intances of "equal" - bit0 and bit1 are instances of "linorder" - bit0 and bit1 are instances of "enum" Any suggestions are really welcome, Jesus On Thu, Jan 31, 2013 at 8:50 AM, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote: > Dear Jesus, > > On 01/30/2013 07:49 PM, Jesus Aransay wrote: >> >> 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"? > > The card_UNIV type class is only definitional, i.e., every type can be shown > an instance of it. The type class card_UNIV merely defines an overloaded > constant card_UNIV with the meaning of card (UNIV :: 'a set) which the > different instantiations can implement as needed, e.g. card_UNIV = 2 for > bool, card_UNIV = 256 for char and card_UNIV = card_UNIV * card_UNIV for > pairs. The idea behind card_UNIV is described in [1]. > > >> Then, "List.coset" should be evaluated for instances of the >> "card_UNIV" type class? > > If you understand "evaluated" as value "List.coset [True]" returns "set > [False]", then no. card_UNIV only evaluates comparisons between sets, i.e., > "List.coset [True] = set [False]" returns true, but without ever computing > explicitly that the left-hand side is in fact "set [False]". > > >> 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? > > I cannot guess from the information you gave what could be the reason. If > you can send your theory, I can have a look at it. The cardinality should > not matter. > > >> 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? > > Yes, they could, but the finite_n types are not meant for general-purpose > applications. Lukas introduced them such that quickcheck can instantiate > type variables in theorems with finite types before checking. > > Andreas > > [1] Andreas Lochbihler. Formalising FinFuns - Generating Code for Functions > as Data from Isabelle/HOL. TPHOLs 2009, LNCS 5674, pp. 310--326, Springer, > August 2009. > http://www.infsec.ethz.ch/people/andreloc/publications/lochbihler09tphols.pdf

**Attachment:
Num_Types_Enum_Types.thy**

**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

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

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

- Previous by Date: Re: [isabelle] Surprises with transfer method
- Next by Date: Re: [isabelle] Evaluation of List.coset
- 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