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

*To*: isabelle-users at cl.cam.ac.uk
*Subject*: [isabelle] Is it bad to instantiate "list" with custom classes to be used with "bool list"?
*From*: Gottfried Barrow <igbi at gmx.com>
*Date*: Mon, 08 Sep 2014 01:00:51 -0500
*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

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
I got that idea from the increment function in Num.thy.

`The part of instantiating "bool list" that was foggy for me was the idea
``that I needed to find a bunch of type classes which "bool" satisfies.
``The light bulb finally turned on.
`

`For the above, I executed "print_classes" and found that "bool" had been
``instantiated for 42 type classes. I picked the two above with the idea
``that I need type classes that will give "bool list" enough properites of
``"nat" to prove what I need. Those looked like a good start.
`
Is instantiating "list" like this a bad thing in general?
Thanks,
GB

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