[isabelle-dev] Relations vs. Predicates
c-sterna at jaist.ac.jp
Tue Apr 3 09:46:30 CEST 2012
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?
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
>> 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
> 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: …
> 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
> 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.
More information about the isabelle-dev