Re: [isabelle] Evaluation of List.coset



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





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