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

[Florian Haftmann]

Hi all,

recently I did some work to setup Stefan's ancient pred_set_conv utility
for relation predicates like sym(p) etc., see
http://isabelle.in.tum.de/reports/Isabelle/file/tip/src/HOL/Relation.thy

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,

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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