[isabelle-dev] Conversions between ('a * 'a) set and 'a => 'a => bool relations
florian.haftmann at informatik.tu-muenchen.de
Sun Mar 4 10:47:23 CET 2012
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,
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev