IntModule_ZF rewrite

[SKolodynski]

In view of recent addition of integer power in groups in IntGroup_ZF I think IntModule_ZF can be greatly simplified.
@dan323, please let me know if you would like to do that, if not I will do it.

[dan323]

I can work on that, but after I go back home from the Christmas holidays. 😄

[dan323]

I saw you added a new locale as "notation". Now I do not have access to those theorems in the abelian_group locale. Locales are thought to have assumptions and definitions, and that is why they do not work well like this.

[dan323]

Since you are not defining powz (you are fixing it); when I sublocale, I lose all notation. Fixes implies that it should be provided from outside when the locale is used.

[SKolodynski]

pow and nat_mult are notations for the underlying notion of folding of a constant list, one used in the context of multiplicative notation and the other in the context of additive notation. They look similar in the source but are rendered differently at isarmathlib.org, see for example nat_mult_add_one and nat_pow_add_one. The situation with powz is similar, it's a notation, although the additive version of this notation is not used anywhere yet.
The idea is to rewrite IntModule_ZF in a locale that adds commutativity assumption to the group_int0 locale rather than group0 locale. I have added (temporarily) such locale and a bunch of lemmas ending with powz_maps_int_End that can replace group_action_int_fun to illustrate what I have in mind.

[dan323]

You are not understanding. There is a notation keyword and a definition keyword that allows you to do those in locales. The issue is that you are doing fixes. When fixing, you need to provide externally, when you define or mark as a notation it forwards that when the locale is interpreted or sublocaled. For example, I could do sublocale_name.powz if it was defined instead of fixed. As it is now I have to rewrite the whole thing.

[SKolodynski]

Yes, I am not understanding. Practically all notation in IsarMathLib is defined in locale specifications with fixes ... defines ... keywords. It does not create problems and allows me to remap all notation from one locale to a different one with sublocale command (which btw I learned from you). Anyway, since you say that it will be easier for you if I define powz with definition outside of locale specification I have done that now.

[dan323]

It is different when you do topology for example, your closure operation is a definition.

[dan323]

There are things you want to remap to other things, I understand; but not pow, this has the same definition everywhere.

[SKolodynski]

As I mentioned above "pow and nat_mult are notations for the underlying notion of folding of a constant list". I want to be a able to prove something about $x^n = x\cdot x\cdot ... \cdot x$ in a locale where multiplicative notation is used and then map it to a fact about $n\cdot x = x+x+ ... +x$ in a locale where additive notation is used, or vice versa - see nat_mult_add_one and nat_pow_add_one mentioned above.

[dan323]

Exactly. pow is defined as the fold of a constant list. That is independent of the notation of the operation used for the fold.

[SKolodynski]

So you suggest to have a notion of pow, defined as fold of a constant list, then in locales define various notations for it, like $n\cdot x$ named nat_mult or $x^n$ named ... what?
In my view we might have a notion of fold of a constant list named in a notation independent way, say ConstantFold and then in locales have notations for it like $n\cdot x$ named nat_mult or $x^n$ named pow . I wouldn't like to name the general notion of fold of a constant list anything that associates it with "power" as people usually think of "power" as something that looks like $x^n$ and not say $n\cdot x$.