[isabelle-dev] Relations vs. Predicates

[Christian Sternagel]

Sorry, I'm not familiar with the "developer" workflow. I do have a 
cloned hg repo of Isabelle (from 
http://isabelle.in.tum.de/repos/isabelle), but I don't see an 
IsaMakefile (which would be required for "isabelle make all"). Where is 
this IsaMakefile located?

cheers

chris

On 04/03/2012 02:51 AM, Florian Haftmann wrote:
> 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
>