Rewrite topological group proofs

[dan323]

Since topgroup => group0 now and there is a locale for group operations on sets, we should make use of it to avoid proving things more than once.

[SKolodynski]

When you say "there is a locale for group operations on sets" do you mean the group4 locale in Group_ZF_1` theory? What kind of rewrite do you have in mind? Can you give an example of the theorem whose proof needs to be rewritten and how?

[dan323]

In topgroup, there are some theorems on A\B and \A that are just set theoretic. In my opinion you should provide a proof that anything in group4 is in group0, they are equivalent as sets of axioms. Then anything that is group0, in particular topgroup, can use those results in group4. After you delete those in topgroup already proven, and make use of group4 results. Also, I saw that you added that topgroup is group0; but didn't remove the group-theoretic results which you already have for free; like the result that the inverse is in the group.

[SKolodynski]

There is no need to provide a proof that anything in group4 is in group0. The group4 is defined as an extension (? not sure this is the right word) of the group0 locale:

  locale group4 = group0 +  
    fixes sdot (infixl "\<sdot>" 70)
    defines sdot_def [simp]: "A\<sdot>B  \<equiv> (P {lifted to subsets of} G)`\<langle>A,B\<rangle>"

You probably mean that the statement

  sublocale topgroup < group4 (...)

in TopologicalGroup_ZF.thy would be useful and I agree.

I am not planning to delete theorems in TopologicalGroup_ZF.thy even if they are essentially the same as some theorems in section Subgroups and interval arithmetic in Group_ZF_1.thy, just using the additive notation rather than the multiplicative one. There is value in presenting the same theorem in a different notation.

There are still some theorems in TopologicalGroup_ZF.thy whose proofs use the group0_valid_in_tgroup lemma. Those indeed should be simplified to use the sublocale statement, if possible.

[SKolodynski]

I assigned this task to myself. In general any substantial changes to the theories presented at isarmathlib.org I would prefer to do myself.

[dan323]

Once you have a locale with notation, the theorems of the other locales specialize. If you read inv_in_group from topgroup, you will see additive notation. No need to prove it again. That is what I mean.

For group4 I was thinking of group4<group0 and group0<group4

[SKolodynski]

This is mostly fixed by b39139cf15e61d6489810241387fe8e240a09098, except that I was unable to convert https://github.com/SKolodynski/IsarMathLib/blob/bc5a97fc118b4111cc71c5c04eb90cce6aa28905/IsarMathLib/TopologicalGroup_ZF.thy#L198-L203 . @dan323 , can you have a look?

[dan323]

It looks much better, yes.

[dan323]

I looked at the issue, and if you change f`<a,b> by a\b and GroupInv(G,f)`c by \c it works. It just is not undoing the notation. You can do it yourself if you prefer.

If you want to print out the basic results with the new notation, I think you can just command "print_statement group0_2_L2" in the locale, and you may also rename them with "lemmas (in topgroup) zero_in_tgroup = group0_2_L2". Just an idea. Do not know if "print_statement" will print it in the pdf.

[SKolodynski]

Indeed, I didn't notice that I invert the order of expressions there, it's corrected now and it works without referencing group0_valid_in_tgroup.