[isabelle-dev] Relations vs. Predicates

[Florian Haftmann]

Hi Christian,

>> 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?

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 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)?

Well, you could check with an check an »isabelle make all«, send the
patch to the mailing list,  and somebody else would take care for AFP
and the remaining technicalities.  You could also clone the existing hg
http://isabelle.in.tum.de/reports/Isabelle and provide an URL to import
your patch from.  Or think of whatever workflow hg offers.

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://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120402/689818fe/attachment-0001.asc>