[isabelle-dev] Relations vs. Predicates

[Florian Haftmann]

Hi Christian,

> To come back to the subject, I'm missing "iteration" of predicates,
> i.e., what "_^^n" is on relations but for predicates ("'a => 'a =>
> bool").

this has been added in
http://isabelle.in.tum.de/testboard/Isabelle/rev/69cee87927f0 – you can
transfer theorems from the set relations in an ad-hoc using [to_pred].
You can also prove theorems for pred relations by means of … by (fact …
[to_pred]), as has been done in many places of theory Relation.  This
could also be a contribution to the Isabelle theories for the next release.

> PS: I suggest to rename "rel_comp" into "relcomp" (to be consistent with
> "relpow").

This would also mean to rename the corresponding lemmas, although I
would also appreciate consistency.  Also the »pred_comp« abbreviation
should be dropped, with the subsequent consequences for theorem names.
This would also be something you could contribute if you like.

> In @{theory Relation} there is a typo in the lemma name
> "prod_comp_bot1".

Fixed, thanks a lot.

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://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120330/26e762d1/attachment.sig>