skolodynski / isarmathlib Goto Github PK
View Code? Open in Web Editor NEWIsarMathLib is a library of formalized mathematics for Isabelle/ZF.
Home Page: https://isarmathlib.org
License: Other
IsarMathLib is a library of formalized mathematics for Isabelle/ZF.
Home Page: https://isarmathlib.org
License: Other
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:
Proof that the Roelcke uniformity is a uniformity, defined in here for example.
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:
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.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.