Re: [isabelle] Evaluation of List.coset



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
Description: Binary data



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