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?

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

Hm, that is quite unfortunate.

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.

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

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

?

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

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

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.

```
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 [])"
```

If your ordering isn't linear, you'll have to switch the `THE`

to a `SOME`

.

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`

.

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

trick I told you about

The problem is that antisymmetry does not hold if `f = fst`

.

yeah the whole point of sorted_list_of_set is that it is unique

Otherwise you can just do "sort (list_of_set …)".

That's not computable though, for obvious reasons.

One would need some distinctness condition w.r.t. `f`

How would distinctness be enough? What kind of ordering do you have?

Ah you have a linear order on the keys, I see. Yeah.

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).

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

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

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

Did you look at `Mapping.combine`

?

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

More specifically, I need a nested fold where I combine all 'a with each other.

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

Manuel Eberl said:

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

Do you know where exactly? Grepping in `src/HOL/Probability`

didn't yield anything for me.

Ah maybe `fold_combine_plus`

?

Yes, but I think that used `Mapping.cobmine`

.

Last updated: Dec 07 2023 at 08:19 UTC