*To*: cl-isabelle-users at lists.cam.ac.uk, peteg42 at gmail.com*Subject*: Re: [isabelle] conversions for symmetric/commutative operators (Peter Gammie)*From*: Emin Karayel <me at eminkarayel.de>*Date*: Tue, 9 Nov 2021 16:06:35 +0100*Authentication-results*: cam.ac.uk; iprev=pass (mo4-p00-ob.smtp.rzone.de) smtp.remote-ip=85.215.255.23; spf=none smtp.mailfrom=eminkarayel.de; dkim=pass header.d=eminkarayel.de header.s=strato-dkim-0002 header.a=rsa-sha256; arc=none*Authentication-results*: strato.com; dkim=none*In-reply-to*: <mailman.4977.1636465456.48434.cl-isabelle-users@lists.cam.ac.uk>*References*: <mailman.4977.1636465456.48434.cl-isabelle-users@lists.cam.ac.uk>

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

Date: Tue, 9 Nov 2021 22:04:13 +0930

From: Peter Gammie <peteg42 at gmail.com>

Subject: [isabelle] conversions for symmetric/commutative operators

To: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>

Message-ID: <7711F679-C145-4B57-9DB7-16D7FEBDDF0D at gmail.com>

Content-Type: text/plain; charset=utf-8

Hello,

I find myself with a sea of conversions of the form exhibited by `filter_empty_conv`. `HOL.List` is missing its obvious friend:

lemma empty_filter_conv:

shows "([] = filter P xs) = (\<forall>x\<in>set xs. \<not> P x)"

by (induct xs) simp_all

which could also be derived via a rule of the form:

(x = y) = z ==> (y = x) = z

(and so forth for other symmetric or commutative operators such as inf and sup).

One could imagine defining an attribute `symconv` like `symmetric` to handle this:

lemmas empty_filter_conv = filter_empty_conv[symconv]

But in my ideal world I wouldn’t need to type this out and make up another name, but would instead bind both theorems to the same name, e.g.

lemma empty_filter_conv[symconv]:

shows "([] = filter P xs) = (\<forall>x\<in>set xs. \<not> P x)”

…

thm empty_filter_conv

> ([] = filter P xs) = (\<forall>x\<in>set xs. \<not> P x)

> (filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)

However AIUI attributes map a single theorem to a single theorem, so this isn’t going to work.

All I can think of is to create another keyword like `lemma` that does a bit of post-processing before the binding is made. This feels a bit heavyweight.

Has anyone got a better solution? It might help to make these sorts of lemma pairs more systematic in the distribution.

cheers,

peter

------------------------------

Message: 9

Date: Tue, 09 Nov 2021 14:28:23 +0100

From: Peter Lammich <lammich at in.tum.de>

Subject: Re: [isabelle] conversions for symmetric/commutative

operators

To: Peter Gammie <peteg42 at gmail.com>

Cc: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>

Message-ID: <207d7151-b15a-456e-9538-1aa3d9158635 at email.android.com>

Content-Type: text/plain; charset="utf-8"

An HTML attachment was scrubbed...

URL: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/attachments/20211109/8f8d0519/attachment.htm

- Previous by Date: Re: [isabelle] Isabelle2021-1-RC2: Invoking smt-method in theory loaded via Isabelle/Scala
- Next by Date: Re: [isabelle] Isabelle2021-1-RC2: Invoking smt-method in theory loaded via Isabelle/Scala
- Previous by Thread: Re: [isabelle] conversions for symmetric/commutative operators
- Next by Thread: Re: [isabelle] Code generation for typedefs with an invariant
- Cl-isabelle-users November 2021 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list