[isabelle-dev] Relations vs. Predicates

[Christian Sternagel]

Hi Florian,

On 03/31/2012 01:10 AM, Florian Haftmann wrote:
> 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.
I do not fully understand. I see how [to_pred] can be used to "transfer" 
results, but what kind of theorems are you referring to? Do you mean to 
do this for every theorem on relations to have an equivalent for binary 
predicates?
>
>> 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.
I will give it a try. Anyway, how would I "commit" such a contribution? 
Sending a patch to the mailing list? And is it enough that "./build -b 
HOL" works or are there any other places I have to consider (e.g., the AFP)?

cheers

chris
>
>> In @{theory Relation} there is a typo in the lemma name
>> "prod_comp_bot1".
>
> Fixed, thanks a lot.
>
> Cheers,
> 	Florian