Hiding type class instances · General

In HOL-Library, there are two different instantiations of prod :: (ord, ord) ord. If I import one of them, is everyone who in turn imports my theory forced to use the instance I chose or is there a way to hide those instances?

Manuel Eberl (Aug 11 2020 at 13:06):

No, type class instances are forever. One of the reasons why Isabelle's type classes are… not great.

Lukas Stevens (Aug 11 2020 at 13:06):

Manuel Eberl (Aug 11 2020 at 13:07):

When you instantiate a type class, you're adding a definition for all the overloaded constants that it contains. You cannot have two different definitions for the same thing and you cannot "delete" definitions, so this cannot work.

Manuel Eberl (Aug 11 2020 at 13:08):

To support something like this, I think one would have to overhaul the entire type class system from ground up.

Lukas Stevens (Aug 11 2020 at 13:10):

Ok, what would be the canonical way to customize the comparison operator in linorder.sorted_list_of_set?

Lukas Stevens (Aug 11 2020 at 13:14):

I just now noticed that the type class instance I had in mind would not work anyways...

Manuel Eberl (Aug 11 2020 at 13:27):

I don't think you can simply "customise" it. You can of course make a type copy of whatever your type is, do the ord instance in whichever way you want it to be, and then convert back and forth

Manuel Eberl (Aug 11 2020 at 13:29):

fwiw I defined a sorted_wrt_list_of_set function in the AFP, in Comparison_Sort_Lower_Bound.Linorder_Relations, along with some other operations on orderings that take the ordering as an explicit relation instead of from the typeclass.

Manuel Eberl (Aug 11 2020 at 13:29):

definition sorted_wrt_list_of_set where
  "sorted_wrt_list_of_set R A =
     (if finite A then (THE xs. set xs = A ∧ distinct xs ∧sorted_wrt R xs) else [])"

Manuel Eberl (Aug 11 2020 at 13:29):

Lukas Stevens (Aug 11 2020 at 13:34):

Concerning the sorted_wrt_list_of_set: I only need sorted_key_list_of_set f ≡ folding.F (insort_key f) []. But then I need to reprove the lemmas that exist about sorted_list_of_set.

Manuel Eberl (Aug 11 2020 at 13:35):

Yeah if you really care about getting around that, you might have to do the typedef trick I told you about

Lukas Stevens (Aug 11 2020 at 13:36):

Manuel Eberl (Aug 11 2020 at 13:38):

Lukas Stevens (Aug 11 2020 at 13:42):

Manuel Eberl (Aug 11 2020 at 13:50):

Lukas Stevens (Aug 11 2020 at 13:52):

Yes, my goal is to define a fold operation on Mappings. For this I first need an ordered_entries operation (which orders the entries by the first component).

Manuel Eberl (Aug 11 2020 at 13:55):

I think something like this already exists as long as the operation with which you fold is order-independent

Manuel Eberl (Aug 11 2020 at 13:56):

at least I vaguely remember having done such a thing for PMFs in HOL-Probability

Manuel Eberl (Aug 11 2020 at 13:56):

they are implemented as mappings, and when you want to implement monadic bind/join, you need to fold over that mapping and sum up some values

Manuel Eberl (Aug 11 2020 at 13:57):

Lukas Stevens (Aug 11 2020 at 13:58):

Yes, unfortunately this does not help me since my operation depends on both 'a and 'b

Lukas Stevens (Aug 11 2020 at 14:00):

Lukas Stevens (Aug 11 2020 at 14:04):

I am thinking about going the less beautiful route and just using RBTs directly.