Re: [isabelle] Evaluation of List.coset

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.


[1] Andreas Lochbihler. Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL. TPHOLs 2009, LNCS 5674, pp. 310--326, Springer, August 2009.

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