[isabelle-dev] Relations vs. Predicates

[Lukas Bulwahn]

On 04/16/2012 09:13 AM, Christian Sternagel wrote:
> Hi all,
>
> On 04/03/2012 02:51 AM, Florian Haftmann wrote:
>> well, I suggest to augment the existing theory with lemmas transferred
>> from relpow to relpowp to emphasize that both worlds exists and that
>> lemmas can be found easier by find_theorems.  The typical pattern is
>>
>> lemma foo_relpow: ...
>> <proof>
>>
>> lemma foo_relpowp: ...
>>    by (fact foo_relpow [to_pred])
>>
> I did this in the meantime (tested with "isabelle makeall all"). This 
> time as a patch (in order to avoid cluttering the history) on Theory 
> Transitive_Closure. Suggested NEWS entry:
>
> ------------------------------------------------------------------
> * Theory Transitive_Closure: Duplicated facts about "relpow" for 
> "relpowp" to emphasize that both worlds exist and facilitate better 
> results with "find_theorems".
>
>   Added Lemmas:
>   relpowp_1
>   relpowp_0_I
>   relpowp_Suc_I
>   relpowp_Suc_I2
>   relpowp_0_E
>   relpowp_Suc_E
>   relpowp_E
>   relpowp_Suc_D2
>   relpowp_Suc_E2
>   relpowp_Suc_D2'
>   relpowp_E2
>   relpowp_add
>   relpowp_commute
>   relpowp_bot
>   rtranclp_imp_Sup_relpowp
>   relpowp_imp_rtranclp
>   rtranclp_is_Sup_relpowp
>   rtranclp_power
>   tranclp_power
>   rtranclp_imp_relpowp
>   relpowp_fun_conv
> ------------------------------------------------------------------
>
I pushed your changes to the public repository, but I did not consider 
the NEWS entry worth mentioning -- we add theorems on a daily basis, 
without explicitly advertising them in the NEWS.

Lukas
> cheers
>
> chris
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120416/c21d4437/attachment-0002.html>