[isabelle-dev] Relations vs. Predicates

[Christian Sternagel]

Dear all,

by the way, I noticed that sometimes [to_pred] yields undesirable 
results (containing case-expressions), e.g.,

thm trancl_power[to_pred]

results in

(case ?p of (x, xa) ⇒ ?R^++ x xa) =
(∃n>0. case ?p of (x, xa) ⇒ (?R ^^ n) x xa)

is this an inherent problem or could this be "repaired" by adding 
appropriate [pred_set_conv] (I do not know how this workds in detail).

cheers

chris

On 03/31/2012 03:00 PM, Christian Sternagel wrote:
> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev