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



On 14-09-08 01:33, Andreas Lochbihler wrote:
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}.

Andreas,

Thanks. Abstract thinking, it can incapacitate a majority of neurons. In this case, among other reasons, because my goal wasn't to generalize anything for "list".

The syntax 'instantiation list :: ("{......}") binc ' required one or more type classes between the braces, so I was trying to make it concrete as possible for "bool", instead of abstract as possible for "'a list".

So now, using your tip, I've generalized it for "list" with the minimum requirements:

instantiation list :: ("{bot,top}") binc
begin
primrec binc_list :: "'a list ⇒ 'a list" where
"binc_list [] = bot # []"
|"binc_list (b # bl) = (if b = bot then top # bl else bot # (binc_list bl))"
instance ..
end

I make "binc" a syntactic type class, and I guess in future, if I build on that with "assumes" in type classes designed for my other concrete datatypes, I then should try to figure if my assumptions are applicable to "'a list".

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.

Specifically, I wanted to decide if I could instantiate "list" for "numeral", to get the convenience of using standard number syntax with "bool list", since it's 1-to-1 with non-zero nat, but I had the right, foggy idea to begin with, that I shouldn't be hijacking "list" like that.

So, I think the answer is that I can instantiate "list" for my own syntactic type classes, but I should rarely, if ever, instantiate a general HOL type for any general HOL type class.

Thanks,
GB






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