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

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Sun Mar 4 10:47:23 CET 2012

Hi all,

recently I did some work to setup Stefan's ancient pred_set_conv utility
for relation predicates like sym(p) etc., see

A few couple of things then came to surface:
* Naming: »inductive_set foo« yields »foop« as the name of the
corresponding predicate, whereas e.g. »wf« has »wfP«.  We should
consolidate this.  I personally have a slight preference for lower case »p«.
* Abbreviation vs. constant: considering that both kinds of relations
coexist, constants would be better for all twins.  The pred_set_conv
utility can convert theorems on the fly if needed.
* 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.

Maybe one day prep_set_conv can be subsumed by a generic lifting
machinery a la quotient,



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120304/69fa75d8/attachment.asc>

More information about the isabelle-dev mailing list