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

[Tobias Nipkow]

For compatibility, I will follow Michael and reintroduce the old names 
as synonyms. I am unsure about other types. For HOLCF functions the 
ext_iff scheme makes sense, too, but I would leave that to you. 
Concerning products: I agree we should get rid of "Pair_fst_snd_iff" and 
"complex_Re_Im_cancel_iff" and am happy with {prod,complex}_eqI and 
{prod,complex}_eq_iff.

Tobias

Am 07/09/2010 21:04, schrieb Brian Huffman:
> OK, this makes sense. It is nice to have the pair of lemmas "foo_ext"
> and "foo_ext_iff" for each function-like type "foo".
>
> So do you propose that we rename all of the expand_*_eq lemmas that I
> listed before? (It would also be good to make sure there is a
> properly-named *_ext lemma corresponding to each one.)
>
> We should also come up with a consistent naming scheme for the
> analogous lemmas for product-like types (incl. prod and complex). Here
> are the names currently in use:
>
> "fst a = fst b ==>  snd a = snd b ==>  a = b" .... prod_eqI
> "a = b<-->  fst a = fst b /\ snd a = snd b" .... Pair_fst_snd_iff,
> expand_prod_eq
>
> "Re x = Re y ==>  Im x = Im y ==>  x = y" .... complex_equality
> "x = y<-->  Re x = Re y /\ Im x = Im y" .... complex_Re_Im_cancel_iff,
> expand_complex_eq
>
> The names {prod,complex}_ext and {prod,complex}_ext_iff would be a bit
> strange. But how about {prod,complex}_eqI and {prod,complex}_eq_iff ?
>
> I'm open to other suggestions, but I would like to be rid of the names
> "Pair_fst_snd_iff" (a bit long, and the lemma doesn't even mention the
> "Pair" constructor) and "complex_Re_Im_cancel_iff" (also long, and I
> don't know what "cancel" is supposed to mean here).
>
> - Brian
>
>
> On Tue, Sep 7, 2010 at 9:45 AM, Tobias Nipkow<nipkow at in.tum.de>  wrote:
>> 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
>>>>
>>