# [isabelle] conversions for symmetric/commutative operators

*To*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>
*Subject*: [isabelle] conversions for symmetric/commutative operators
*From*: Peter Gammie <peteg42 at gmail.com>
*Date*: Tue, 9 Nov 2021 22:04:13 +0930
*Authentication-results*: cam.ac.uk; iprev=pass (mail-pg1-f169.google.com) smtp.remote-ip=209.85.215.169; spf=pass smtp.mailfrom=gmail.com; dkim=pass header.d=gmail.com header.s=20210112 header.a=rsa-sha256; arc=none

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

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*