[isabelle-dev] Conversions between ('a * 'a) set and 'a => 'a => bool relations

[Stefan Berghofer]

Florian Haftmann wrote:
> * This is mainly a question to Stefan: there are some theorems commented
> out (e.g. »thm sym_INTER [to_pred]«) on which pred_set_conv chokes.  I
> guess this is due to a higher-order situation, but I would be reassuring
> if you can confirm that.

Hi Florian,

I have fixed this bug now, see changeset b1d15637381a. Note that converting
the above theorem (and the other theorems in Relation.thy marked with "FIXME")
to predicate notation requires the generalized versions of theorems
INF_INT_eq2 and SUP_UN_eq2, which should replace the more specific versions.
Unfortunately, the Relation theory is currently a bit of a mess. Larger blocks
of conversion lemmas are commented out for no good reason, which means that they
are not tested by our nightly builds, and for some of them it still remains to
be examined whether they can be added to the database of predicate/set conversion
rules by default without breaking any of the examples in the AFP. What is the
strategy for cleaning up this theory?

Greetings,
Stefan