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



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.