Re: [isabelle] Is it bad to instantiate "list" with custom classes to be used with "bool list"?



Dear Gottfried,


On 08/09/14 08:00, Gottfried Barrow wrote:
Hi,

I work with limited knowledge, so if I stumble onto something useful then I resort to it a
lot.

I've resorted a lot to wrapping a type in a datatype to be able to instantiate the type
with type classes.

This question is about "bool list" in particular, but it's also of interest to me in general.

What I have is "bool list" in a 1-1 relation with non-zero nat, but I don't use it
directly. I put it in a datatype like this:

datatype_new boD = bo_C "bool list"

I did that in the past because:

1) I didn't know how to do what has now come to my mind,

2) but also, I thought that doing such a thing would be hijacking "list".

I have a type class, which I eventually will want to prove some things about:

   class binc =
     fixes binc :: "'a => 'a"

This is a binary increment function, which for "bool list" is in this instantiation, for
the moment:

   instantiation list :: ("{complete_boolean_algebra, linorder}") binc
   begin
   primrec binc_list :: "bool list => bool list" where
     "binc_list []       = False # []"
    |"binc_list (b # bl) = (if b = False then True # bl else False # (binc_list bl))"
   instance ..
   end
This will not work the way you expect. To make the list type an instance of binc, you have to do this for lists of arbitrary elements of the assumed sort ("{complete_boolean_algebra, linorder}" in this example), not for a specific type bool. As it is now, you define a function binc_list which is completely unrelated to binc. You will realise this at the latest when you introcude some assumptions about binc and are unable to prove them for your attempted instantiation.

Note that if you replace False by bot and True by top, then your definition should generalise to 'a :: {complete_boolean_algebra, linorder}.

Is instantiating "list" like this a bad thing in general?
If you define your own type classes and instantiate them for list, that is all right. However, you should be very careful when you instantiate list for type classes of HOL/Main or other people, because this may restrict the interoperability with the formalisations of others, as type classes may only be instantiated once for each type in one session.

Andreas




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