Re: [isabelle] conversions for symmetric/commutative operators

I second Peter that having attributes that create more than one lemma as output may be a useful thing. I also often write things like [simp, THEN xxx, simp], to register two simp rules derived from the same lemma.


On 9 Nov 2021 13:34, Peter Gammie <peteg42 at> wrote:


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.


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