*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] conversions for symmetric/commutative operators*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 10 Nov 2021 08:27:18 +0100*Authentication-results*: cam.ac.uk; iprev=pass (mail-out2.in.tum.de) smtp.remote-ip=131.159.0.36; spf=pass smtp.mailfrom=in.tum.de; arc=none*In-reply-to*: <7711F679-C145-4B57-9DB7-16D7FEBDDF0D@gmail.com>*References*: <7711F679-C145-4B57-9DB7-16D7FEBDDF0D@gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:91.0) Gecko/20100101 Thunderbird/91.3.0

Peter,

Tobias On 09/11/2021 13:34, Peter Gammie wrote:

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

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] conversions for symmetric/commutative operators***From:*Peter Gammie

**References**:**[isabelle] conversions for symmetric/commutative operators***From:*Peter Gammie

- 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] conversions for symmetric/commutative operators
- 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