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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
