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

[Tobias Nipkow]

I wanted to emphasize the mathematical concept, not the operational 
view. And indeed, it is shorter. For functional objects the ext_iff 
convention fits perfectly. For example, for polynomials we already have 
poly_ext in one direction. I have to admit, though, that for pairs it 
would be a bit unusual, although it fits a certain view of pairs.

Tobias

Am 07/09/2010 17:22, schrieb 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
>>