*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] conversions for symmetric/commutative operators*From*: Peter Gammie <peteg42 at gmail.com>*Date*: Sun, 14 Nov 2021 09:10:30 +0930*Authentication-results*: cam.ac.uk; iprev=pass (mail-pj1-f47.google.com) smtp.remote-ip=209.85.216.47; spf=pass smtp.mailfrom=gmail.com; dkim=pass header.d=gmail.com header.s=20210112 header.a=rsa-sha256; arc=none*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <befe70c7-861a-b837-4a5c-43600c6c5234@in.tum.de>*References*: <7711F679-C145-4B57-9DB7-16D7FEBDDF0D@gmail.com> <befe70c7-861a-b837-4a5c-43600c6c5234@in.tum.de>

Tobias, Thanks for doing that. I’ll reiterate my concern that things aren’t particularly systematic. For instance we have this pair: filter_eq_Cons_iff Cons_eq_filter_iff and this pair: take_eq_Nil take_eq_Nil2 Can we settle on: - suffix `_iff` vs `_conv` vs nothing - suffix `2` vs flipping the constant names around `_eq_` - ... As I remarked before, it’d be great if we could just have a single name for each of these pairs as the common case is that you just want to use whatever works (which in my case would give more robust proofs as I rework the foundations of things). In the rarer case that you need just one or the other I think e.g. filter_eq_Cons_iff(1) is not so bad. Perhaps this is not typically an issue once the relevant simpset is sufficiently mature. cheers, peter > On 10 Nov 2021, at 16:57, Tobias Nipkow <nipkow at in.tum.de> wrote: > > Peter, > > This is really funny, I was in the middle of implementing the first part of what you suggested. There is now the lemma eq_iff_swap: (x = y) = P ==> (y = x) = P and I have simplified a number of proofs in List as a result. I have also added a handful of lemmas that were missing. Strangely enough, I missed your empty_filter_conv. Or maybe I tried and it did more harm than good - it took a couple of iterations to smooth things out. I'll double-check. > > Note that one should not apply eq_iff_swap blindly: one may want to swap some equations in P as well. > > 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

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

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

**Re: [isabelle] conversions for symmetric/commutative operators***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Isabelle2021-1-RC3. Odd sledgehammer proof reconstruction
- Next by Date: [isabelle] Theorem Proving Research Associate Position in Manchester, UK
- 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