Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] calculational reasoning for transitive relations

view this post on Zulip Email Gateway (Aug 18 2022 at 15:56):

From: Andrei Popescu <uuomul@yahoo.com>
Joachim Breitner wrote:

Also, it would be nice if the transitivity rules for <o, <=o, =o were
set up to work with Isar’s "also... also... finally".

Good point. I actually though about this too, but did not investigate if it is
possible.

Now I see that a paper on the topic,

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.24.2082

states that

"Certainly, creative users of Isabelle/Isar may
invent further ways of calculational reasoning at any time."

It was not clear to me if this applies to the following situation:
any combination of equalities and a relation proven to be transitive.

Best regards,
Andrei

view this post on Zulip Email Gateway (Aug 18 2022 at 15:56):

From: Brian Huffman <brianh@cs.pdx.edu>
I think all you need to do is declare the transitivity rules with the
[trans] attribute. Have either of you tried this?

view this post on Zulip Email Gateway (Aug 18 2022 at 15:56):

From: Andrei Popescu <uuomul@yahoo.com>
Tried now and it works, including with all combinations:
transtitivity of <o versus <=o, of <=o versus <o, of <=o versus =o, etc.

Thank you, that was easy. :)

This database-driven customization style for Isabelle does marvels, I should
become

more familiar with it.

Best regards,
Andrei

----- Original Message ----
From: Brian Huffman <brianh@cs.pdx.edu>
To: Andrei Popescu <uuomul@yahoo.com>
Cc: cl-isabelle-users@lists.cam.ac.uk; Joachim Breitner
<mail@joachim-breitner.de>
Sent: Wed, September 22, 2010 8:35:59 PM
Subject: Re: [isabelle] calculational reasoning for transitive relations

On Wed, Sep 22, 2010 at 1:20 PM, Andrei Popescu <uuomul@yahoo.com> wrote:

Joachim Breitner wrote:

Also, it would be nice if the transitivity rules for <o, <=o, =o were
set up to work with Isar’s "also... also... finally".

Good point. I actually though about this too, but did not investigate if it
is
possible.

I think all you need to do is declare the transitivity rules with the
[trans] attribute. Have either of you tried this?

Last updated: Nov 21 2024 at 12:39 UTC