[isabelle-dev] NEWS: expand_fun_eq -> ext_iff, expand_set_eq -> set_ext_iff

[Brian Huffman]

The log message, "Naming in line now with multisets" seems to suggest
that consistency was the main motivation for this change. However, the
change had rather the opposite effect, since the expand_*_eq pattern
is much more common in the libraries. (Full disclosure: some, but not
all, of these lemmas were named by me.)

HOL/Complex.thy: expand_complex_eq
HOL/Limits.thy: expand_net_eq
HOL/Quotient_Examples/FSet.thy: expand_fset_eq
HOL/Library/Product_plus.thy: expand_prod_eq
HOL/Library/Formal_Power_Series.thy: expand_fps_eq
HOL/Library/Polynomial.thy: expand_poly_eq
HOLCF/Cfun.thy: expand_cfun_eq

Meanwhile, multiset_ext_iff was the only example of the *_ext_iff form
I could find.

If naming consistency was the primary goal here, then I think it would
have been much better to just rename multiset_ext_iff to
expand_multiset_eq. (Alternatively, you could try to consistently
change everything to the "ext_iff" style, but "complex_ext_iff" or
"prod_ext_iff" would be a bit weird.)

Personally, I also like the expand_*_eq naming style because it is
descriptive: When you see "simp add: expand_fun_eq" in a proof, there
is no ambiguity about which way the rule is oriented.

On the other hand, the "ext_iff" names are shorter.

- Brian


On Tue, Sep 7, 2010 at 3:06 AM, Tobias Nipkow <nipkow at in.tum.de> wrote:
>
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>