skolodynski / isarmathlib Goto Github PK

The dependency for this statement is to define the natural topology on the real numbers. This is probably best done through metric spaces. Since pseudometrics play a role in the proof one probably should start from that.

A union of two subgroups is a subgroup iff one of the subgroups is a subset of the other subgroup.
If H,K are subgroups then H⋅K is a subgroup iff H⋅K=K⋅H.

Your code is smaller!

Can you tell me, where in the IsarMathLib, I could find the equivalent of the following Mizar/MML proposal ?

theorem Th56: :: GROUP_2:56
for G1, G2, G3 being Group st G1 is Subgroup of G2 & G2 is Subgroup of G3 holds
G1 is Subgroup of G3
Source: http://mizar.uwb.edu.pl/version/current/html/group_2.html

This would allow me to understand the consequences of the definition of subgroup, defined in IsarMathLib.

Regards,
Roland

It could be interesting to investigate if there is a way to apply some CI steps at PR creation, push to master and even publish the website at each release. I personally do not have any idea how to run Isabelle on the remote machine with github actions.

Cardinal_ZF is used in the GROUP_ZF_4 theory and it appears in the pdf documents thanks to its dependency on GROUP_ZF_4. It is also used in Topology_ZF_examples

Would adding Cardinal_ZF in the ROOT file be a good idea?

We need a theory of uniformly continuous mappings to really manage the structure of uniformities:

• During the rest of the steps, prove some useful lemmas about (fxg):AxC->BxD the product of 2 functions as a function on products.
• Define the uniform continuity for f:X->Y: for any entourage V in Y; (fxf)-``(V) is an entourage in X
• Show that they are continous for the associated topologies
• Give an example of continuous non uniformly continuous map

Proof that the Roelcke uniformity is a uniformity, defined in here for example.

• Define a the Roelcke uniformity
• Add a proof that it is indeed a uniformity
• Add a proof that muliplication and inverse functions are uniformly continuous

An example of the problem can be seen in the proof of the cancel_middle lemma. The name of the group0.group0_2_L14A(2) lemma is not rendered as link.

I would like to make some changes to the theory files that are currently not presented at the isarmathlib.org site so that they pass the isar2html converter. @dan323, do you have suggestions for some of your theory files that you are not working on?

I am working on adding definitions of modules and vector spaces. This will be defined as ring or field actions on abelian groups, with Ring_ZF_2 and Ring_ZF_3 as dependencies (hence recent changes to those so that they can be presented at isarmathlib.org).

It will be interesting to add the possibility to interpret locales with the interpretation key word as follows:

definition comp2 ("_{_ O _}") where
  "X{f O g} ≡ Composition(X)`⟨f,g⟩" 

interpretation comp_monoid:monoid0 "X→X" "Composition(X)" "comp2(X)"
  unfolding monoid0_def comp2_def using Group_ZF_2_5_L2(1) by auto

This newly added theory needs to be converted to the proof style enforced by isar2html.

Example:
definition (in topgroup) leftUniformity where "leftUniformity \<equiv> {V\<in>Pow(G\<times>G).\<exists>U\<in> \<N>\<^sub>0. {\<langle>s,t\<rangle>\<in>G\<times>G. (\<rm>s)\<ra>t \<in>U}\<subseteq> V}"
in TopologicalGroup_Uniformity_ZF.

It is arguable if notions should be defined in a locale. The trade off here is that on one hand such definitions can be written in a notation used in the locale which is more readable than the raw set theory notation. On the other hand I don't know how to use such definition outside of that locale, for example in the above case if someone wants to continue the subject of topological group as a uniform space, but using the multiplicative notation instead of additive notation used in the topgroup locale. Probably the best approach is to define notions in raw set theory notation and then prove a lemma in the locale that shows the definition in locale-specific notation.
Nevertheless the possibility of parsing a locale scoped definition should be added to isar2html.

The isar2html tool cannot parse TopologicalGroup_ZF.thy released with v1.12.0 so it can not be presented at isarmathlib.org.

I try to translate (and add) axioms of Tarski-Grothendieck (Mizar Tarski_0.miz) in Isabelle/ZF.

theory AxTarski imports ZF.ZF_Base

begin

(* :: Set axiom
theorem :: TARSKI_0:1
  for x being object holds x is set;
*)

theorem TARSKI_0_1:
  fixes x :: i
  shows "∃ y. x = { a ∈ y. True}" by auto

(* 
:: Extensionality axiom
theorem :: TARSKI_0:2
  (for x being object holds x in X iff x in Y) implies X = Y;
*)

theorem TARSKI_0_2:
  fixes X Y :: i
  assumes "∀ x.(x ∈ X ⟷ x ∈ Y)" 
  shows "X = Y" 
    using extension assms by auto

(*
:: Axiom of pair
theorem :: TARSKI_0:3
  for x,y being object ex z being set st
    for a being object holds
      a in z iff a = x or a = y;
*)

theorem TARSKI_0_3_a_R1:
  fixes x y
  shows "∀ a. (a ∈ ⟨x,y⟩ ⟶ (a = x ∨ a = y))" 
proof -
  {
    fix a
    assume "a ∈ ⟨x,y⟩"
    hence "a = x ∨ a = y" sorry
  }
  thus ?thesis by blast
qed

theorem TARSKI_0_3_a_R2:
  fixes x y
  shows "∀ a. ((a = x ∨ a = y) ⟶ a ∈ ⟨x,y⟩)" 
proof -
  {
  fix a
  assume "a = x ∨ a = y"
  hence "a ∈ ⟨x,y⟩" sorry
}
  thus ?thesis by blast
qed

theorem TARSKI_0_3_a:
  fixes x y ::i
  shows "∀ a :: i. (a ∈ ⟨x,y⟩ ⟷ (a = x ∨ a = y))" 
  using TARSKI_0_3_a_R1 TARSKI_0_3_a_R2 by blast

theorem TARSKI_0_3:
  shows "∃ z. ∀ a. (a ∈ z ⟷ (a = x ∨ a = y))"
proof - 
  let ?z = "⟨x,y⟩"
  { 
    fix a :: i
    assume "a ∈ ?z"
    hence "a = x ∨ a = y" using TARSKI_0_3_a by blast
  }
  moreover
  {
    fix a :: i
    assume "a = x ∨ a = y" 
    hence "a ∈ ?z" using TARSKI_0_3_a by blast
  }
  ultimately show ?thesis by blast
qed

(*
:: Axiom of union
theorem :: TARSKI_0:4
  for X being set
   ex Z being set st
    for x being object holds
      x in Z iff ex Y being set st x in Y & Y in X;
*)

theorem TARSKI_0_4:
  shows "∃ Z. ∀ x. (x ∈ Z ⟷ (∃ Y. x ∈ Y ∧ Y ∈ X))" by auto

(*
:: Axiom of regularity
theorem :: TARSKI_0:5
  x in X implies ex Y st Y in X & not ex x st x in X & x in Y;
*)

theorem TARSKI_0_5:
  assumes "x ∈ X"
  shows "∃ Y. Y ∈ X ∧ ¬ (∃ y. y ∈ X ∧ y ∈ Y)" 
proof -
  have "¬ X = 0" 
    using assms by blast
  hence "(∃x∈X. ∀y∈x. y∉X)" 
    using foundation by blast
  then obtain Y where "Y ∈ X" and "∀y∈Y. y∉X" by blast
  thus ?thesis by blast
qed

end

In the code I have 2 "sorry". Should I extend my "import ZF.ZF_base" with a file from IsarMathLib that would allow to find a proof?

Is there something similar to "object (Mizar)" in IsarMathLib?

Any ideas are welcome.

Upgrade to Isabelle 2020 is needed.

I am adding some results on rings:

• Ring ideal definition
• Product and sum of ideals
• Prime ideal definition
• Maximal ideal definition
• Spectrum and Zariski topology
• Ring homomorphism
• Quotient of ring by ideal
• Integral domain definition
• PID definition
• Euclidean ring definition
• Ideal maximal in commutative ring iff quotient field
• Ideal prime in commutative ring iff quotient integral domain
• Ring of polynomials
• Ring modules

Hello @SKolodynski,

I am wondering if we could add a list of theories or theorems you may want in the project as issues in this repo. So that everyone is in the same page. Also, just to note that my request should be merged in the next release as IsarMathlib is not executable as it is now.

Thank you,
Daniel de la Concepción Sáez

@SKolodynski I tried to create a subgroup locale and show

group0 H "restrict(P,H\<times>H)"

but it would not work as groper is defined without limitation on the elements you are operating over; hence I cannot show that

x\<cdot>y == restrict(P,H\<times>H)`\<langle>x,y\<rangle>

as x and y need not be elements in H

One thing I thought of is to write the notation as abbreviations right after the locale creation, since they are not really definitions but notations. Another is to define a new operation for each sublocale (I did this for quotients, but that makes more sense since the operation is different)

Of course, this is just a suggestion. 😄

Can you help me find, in ZF or IzarMathLib the definition of the natural numbers "3,4,5,6,7,8,9,10" (using succ)?

I already found "1" and "2" in ZF.Bool.thy

abbreviation
  one (<1>) where
  "1 ≡ succ(0)"

abbreviation
  two (<2>) where
  "2 ≡ succ(1)"

I already found "2"..."9" in IsarMathLib.Complex_ZF.thy

 fixes two ("𝟮")
  defines two_def[simp]: "𝟮 ≡ 𝟭 \<ca> 𝟭"

  fixes three ("𝟯")
  defines three_def[simp]: "𝟯 ≡ 𝟮\<ca>𝟭"

  fixes four ("𝟰")
  defines four_def[simp]: "𝟰 ≡ 𝟯\<ca>𝟭"

  fixes five ("𝟱")
  defines five_def[simp]: "𝟱 ≡ 𝟰\<ca>𝟭"

  fixes six ("𝟲")
  defines six_def[simp]: "𝟲 ≡ 𝟱\<ca>𝟭"

  fixes seven ("𝟳")
  defines seven_def[simp]: "𝟳 ≡ 𝟲\<ca>𝟭"

  fixes eight ("𝟴")
  defines eight_def[simp]: "𝟴 ≡ 𝟳\<ca>𝟭"

  fixes nine ("𝟵")
  defines nine_def[simp]: "𝟵 ≡ 𝟴\<ca>𝟭"

Informally, I suspect that the definitions for 1 and 2 are equivalent but I can't show it formally.
Any help is welcome. Thank you in advance.

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.