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
Description: S/MIME Cryptographic Signature