Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Multiple equivalences


view this post on Zulip Email Gateway (Aug 18 2022 at 16:41):

From: Victor Porton <porton@narod.ru>
What is the right way to formulate in Isabelle a theorem which states that
every two of 10 logical expressions are equivalent?

This is equivalent to 9 equivalences:

(1) <-> (2)

...

(1) <-> (10)

but that seems not the best way to formulate it.

What is the right way?

(The same for 10 equal (not necessarily logical) terms?)

\--
Victor Porton - http://portonvictor.org

view this post on Zulip Email Gateway (Aug 18 2022 at 16:41):

From: John Matthews <matthews@galois.com>
Hi Victor,

You can formulate this concisely using set notation:

lemma "{F1, F2, F3, F4, F5, F6, F7, F8, F9, F10} = {F1}"

Similarly for showing that ten expressions are equal.

-john
smime.p7s


Last updated: Mar 29 2024 at 04:18 UTC