Re: [isabelle] Evaluation of List.coset
On 01/30/2013 07:49 PM, Jesus Aransay wrote:
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
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"?
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]".
Then, "List.coset" should be evaluated for instances of the
"card_UNIV" type class?
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.
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?
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
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?
 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