Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] conversions for symmetric/commutative operator...


view this post on Zulip Email Gateway (Nov 10 2021 at 10:42):

From: Emin Karayel <me@eminkarayel.de>
Hi Peter,

You can solve this using the OF attribute.

First proof (once):

lemma switch_eq:
assumes "(x=y) = z"
shows "(y=x) = z"
using assms by auto

Once you have that you can refer to the switched version of any lemma L of
the form [(x=y)=z] like this:
switch_eq[OF L]

For example:
switch_eq[OF filter_empty_conv] is the same as your empty_filter_conv

I hope this helps,

Emin


Last updated: Mar 29 2024 at 04:18 UTC