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

[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
>>>
>