Comments (9)
Can you attach a small theory file that illustrates the problem?
I think moving notation setup outside of locale definitions is an interesting idea that is worth exploring. How would that influence the sublocale
functionality? I like sublocales because they make remapping notation easy. Would that be lost when the notation is defined with abbreviations? For example if groper
was outside the group0
locale definition then how would the proof of inv_cancel_two_add
look like?
from isarmathlib.
What I did for ideals is have the definitions in ring0
, and then have an abbreviation in ring_quotient
of
J \<triangleleft> R/I == ring0.ideal(R//I,AI,MI,J)
So, as you suspect, the notation is not carried over.
However, the issue is that for every sublocale I have to provide something for everything defined in the locale; and sometimes that is difficult. Another solution I thought of is to have context in the definitions
a:G ==> b:G ==> a\<cdot>b == P`\<langle>a,b\<rangle>
This would not change the proofs, as the application P can only be used in that context; and that would make life easier, since when having a subgroup I would deal only with elements in H \<subseteq> G
as it would make me proof:
x:H ==> y:H ==> P`\<langle>x,y\<rangle> == restrict(P,H\<times>H)`\<langle>x,y\<rangle>
which is trivial. Without the context of x y living in H, the statement is not true.
from isarmathlib.
I found this in here:
The body consists of context elements:
fixes x :: τ (mx) declares a local parameter of type τ and mixfix
annotation mx (both are optional). The special syntax declaration
“(structure)” means that x may be referenced implicitly in this
context.
constrains x :: τ introduces a type constraint τ on the local parameter x. This element is deprecated. The type constraint should be
introduced in the for clause or the relevant fixes element.
assumes a: ϕ1 . . . ϕn introduces local premises, similar to assume
within a proof (cf. §6.2.1).
defines a: x ≡ t defines a previously declared parameter. This is
similar to define within a proof (cf. §6.2.1), but defines is restricted to Pure equalities and the defined variable needs to be
declared beforehand via fixes. The left-hand side of the equation
may have additional arguments, e.g. “defines f x1 . . . xn ≡ t”,
which need to be free in the context.
notes a = b1 . . . bn reconsiders facts within a local context. Most
notably, this may include arbitrary declarations in any attribute
specifications included here, e.g. a local simp rule.
Both assumes and defines elements contribute to the locale specification. When defining an operation derived from the parameters,
definition (§5.4) is usually more appropriate.
Note that “(is p1 . . . pn)” patterns given in the syntax of assumes and
defines above are illegal in locale definitions. In the long goal format
of §6.2.4, term bindings may be included as expected, though.
In conclusion, they ask to not use defines
in locales for parameters (P
in your case); as they cannot be used with a context like definition
. I also read that constrains
and defines
are kept for backwards compatibility only; but I doubt they will remove them as they are widely used.
from isarmathlib.
I did the monoid
file, since it was simpler. I added a sublocale
for a submonoid with an abbreviation
(*
This file is a part of IsarMathLib -
a library of formalized mathematics for Isabelle/Isar.
Copyright (C) 2005 - 2008 Slawomir Kolodynski
This program is free software; Redistribution and use in source and binary forms,
with or without modification, are permitted provided that the
following conditions are met:
1. Redistributions of source code must retain the above copyright notice,
this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright notice,
this list of conditions and the following disclaimer in the documentation and/or
other materials provided with the distribution.
3. The name of the author may not be used to endorse or promote products
derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED
WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS;
OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR
OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE,
EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)
section ‹Monoids›
theory Monoid_ZF imports func_ZF Loop_ZF
begin
text‹This theory provides basic facts about monoids.›
subsection‹Definition and basic properties›
text‹In this section we talk about monoids.
The notion of a monoid is similar to the notion of a semigroup
except that we require the existence of a neutral element.
It is also similar to the notion of group except that
we don't require existence of the inverse.›
text‹Monoid is a set $G$ with an associative operation and a neutral element.
The operation is a function on $G\times G$ with values in $G$.
In the context of ZF set theory this means that it is a set of pairs
$\langle x,y \rangle$, where $x\in G\times G$ and $y\in G$. In other words
the operation is a certain subset of $(G\times G)\times G$. We express
all this by defing a predicate ‹IsAmonoid(G,f)›. Here $G$ is the
''carrier'' of the monoid and $f$ is the binary operation on it.
›
definition
"IsAmonoid(G,f) ≡
f {is associative on} G ∧
(∃e∈G. (∀g∈G. ( (f`(⟨e,g⟩) = g) ∧ (f`(⟨g,e⟩) = g))))"
text‹The next locale called ''monoid0'' defines a context for theorems
that concern monoids. In this contex we assume that the pair $(G,f)$
is a monoid. We will use
the ‹⊕› symbol to denote the monoid operation (for
no particular reason).›
locale monoid0 =
fixes G f
assumes monoidAssum: "IsAmonoid(G,f)"
definition (in monoid0) monoper (infixl "⊕" 70)
where "a ⊕ b ≡ f`⟨a,b⟩"
lemmas (in monoid0) [simp] = monoper_def
text‹The result of the monoid operation is in the monoid (carrier).›
lemma (in monoid0) group0_1_L1:
assumes "a∈G" "b∈G" shows "a⊕b ∈ G"
proof-
have "f:G×G → G"
using assms monoidAssum IsAmonoid_def IsAssociative_def
by auto
then show ?thesis using apply_funtype assms by auto
qed
text‹There is only one neutral element in a monoid.›
lemma (in monoid0) group0_1_L2: shows
"∃!e. e∈G ∧ (∀ g∈G. ( (e⊕g = g) ∧ g⊕e = g))"
proof
fix e y
assume "e ∈ G ∧ (∀g∈G. e ⊕ g = g ∧ g ⊕ e = g)"
and "y ∈ G ∧ (∀g∈G. y ⊕ g = g ∧ g ⊕ y = g)"
then have "y⊕e = y" "y⊕e = e" by auto
thus "e = y" by simp
next from monoidAssum show
"∃e. e∈ G ∧ (∀ g∈G. e⊕g = g ∧ g⊕e = g)"
using IsAmonoid_def by auto
qed
text‹The neutral element is neutral.›
lemma (in monoid0) unit_is_neutral:
defines "e ≡ TheNeutralElement(G,f)"
shows "e ∈ G ∧ (∀g∈G. e ⊕ g = g ∧ g ⊕ e = g)"
proof -
let ?n = "THE b. b∈ G ∧ (∀ g∈G. b⊕g = g ∧ g⊕b = g)"
have "∃!b. b∈ G ∧ (∀ g∈G. b⊕g = g ∧ g⊕b = g)"
using group0_1_L2 by simp
then have "?n∈ G ∧ (∀ g∈G. ?n⊕g = g ∧ g⊕?n = g)"
by (rule theI)
then show ?thesis
unfolding e_def TheNeutralElement_def by simp
qed
text‹The monoid carrier is not empty.›
lemma (in monoid0) group0_1_L3A: shows "G≠0"
proof -
have "TheNeutralElement(G,f) ∈ G" using unit_is_neutral
by simp
thus ?thesis by auto
qed
text‹The range of the monoid operation is the whole monoid carrier.›
lemma (in monoid0) group0_1_L3B: shows "range(f) = G"
proof
from monoidAssum have "f : G×G→G"
using IsAmonoid_def IsAssociative_def by simp
then show "range(f) ⊆ G"
using func1_1_L5B by simp
show "G ⊆ range(f)"
proof
fix g assume A1: "g∈G"
let ?e = "TheNeutralElement(G,f)"
from A1 have "⟨?e,g⟩ ∈ G×G" "g = f`⟨?e,g⟩"
using unit_is_neutral by auto
with ‹f : G×G→G› show "g ∈ range(f)"
using func1_1_L5A by blast
qed
qed
text‹Another way to state that the range of the monoid operation
is the whole monoid carrier.›
lemma (in monoid0) range_carr: shows "f``(G×G) = G"
using monoidAssum IsAmonoid_def IsAssociative_def
group0_1_L3B range_image_domain by auto
text‹In a monoid any neutral element is the neutral element.›
lemma (in monoid0) group0_1_L4:
assumes A1: "e ∈ G"
and A2: "∀g∈G. e ⊕ g = g ∧ g ⊕ e = g"
shows "e = TheNeutralElement(G,f)"
proof -
let ?n = "THE b. b∈ G ∧ (∀ g∈G. b⊕g = g ∧ g⊕b = g)"
have "∃!b. b∈ G ∧ (∀ g∈G. b⊕g = g ∧ g⊕b = g)"
using group0_1_L2 by simp
moreover
from A1 A2 have "e∈ G ∧ (∀ g∈G. e⊕g = g ∧ g⊕e = g)" by auto
ultimately have "?n = e" by (rule the_equality2)
then show ?thesis using TheNeutralElement_def by simp
qed
text‹The next lemma shows that if the if we restrict the monoid operation to
a subset of $G$ that contains the neutral element, then the
neutral element of the monoid operation is also neutral with the
restricted operation.›
lemma (in monoid0) group0_1_L5:
fixes H
defines "e ≡ TheNeutralElement(G,f)"
and "g ≡ restrict(f,H×H)"
assumes A1: "∀x∈H.∀y∈H. x⊕y ∈ H"
and A2: "H⊆G"
and A3: "e∈H"
and A4: "h∈H"
shows "g`⟨e,h⟩ = h ∧ g`⟨h,e⟩ = h"
proof -
from A4 A3 have
"g`⟨e,h⟩ = e⊕h ∧ g`⟨h,e⟩ = h⊕e"
using restrict_if unfolding g_def by simp
with A3 A4 A2 show
"g`⟨e,h⟩ = h ∧ g`⟨h,e⟩ = h"
using unit_is_neutral unfolding e_def by auto
qed
text‹The next theorem shows that if the monoid operation is closed
on a subset of $G$ then this set is a (sub)monoid (although
we do not define this notion). This fact will be
useful when we study subgroups.›
theorem (in monoid0) group0_1_T1:
assumes A1: "H {is closed under} f"
and A2: "H⊆G"
and A3: "TheNeutralElement(G,f) ∈ H"
shows "IsAmonoid(H,restrict(f,H×H))"
proof -
let ?g = "restrict(f,H×H)"
let ?e = "TheNeutralElement(G,f)"
from monoidAssum have "f ∈ G×G→G"
using IsAmonoid_def IsAssociative_def by simp
moreover from A2 have "H×H ⊆ G×G" by auto
moreover from A1 have "∀p ∈ H×H. f`(p) ∈ H"
using IsOpClosed_def by auto
ultimately have "?g ∈ H×H→H"
using func1_2_L4 by simp
moreover have "∀x∈H.∀y∈H.∀z∈H.
?g`⟨?g`⟨x,y⟩ ,z⟩ = ?g`⟨x,?g`⟨y,z⟩⟩"
proof -
from A1 have "∀x∈H.∀y∈H.∀z∈H.
?g`⟨?g`⟨x,y⟩,z⟩ = x⊕y⊕z"
using IsOpClosed_def restrict_if by simp
moreover have "∀x∈H.∀y∈H.∀z∈H. x⊕y⊕z = x⊕(y⊕z)"
proof -
from monoidAssum have
"∀x∈G.∀y∈G.∀z∈G. x⊕y⊕z = x⊕(y⊕z)"
using IsAmonoid_def IsAssociative_def
by simp
with A2 show ?thesis by auto
qed
moreover from A1 have
"∀x∈H.∀y∈H.∀z∈H. x⊕(y⊕z) = ?g`⟨ x,?g`⟨y,z⟩ ⟩"
using IsOpClosed_def restrict_if by simp
ultimately show ?thesis by simp
qed
moreover have
"∃n∈H. (∀h∈H. ?g`⟨n,h⟩ = h ∧ ?g`⟨h,n⟩ = h)"
proof -
from A1 have "∀x∈H.∀y∈H. x⊕y ∈ H"
using IsOpClosed_def by simp
with A2 A3 have
"∀ h∈H. ?g`⟨?e,h⟩ = h ∧ ?g`⟨h,?e⟩ = h"
using group0_1_L5 by blast
with A3 show ?thesis by auto
qed
ultimately show ?thesis using IsAmonoid_def IsAssociative_def
by simp
qed
locale monoidClosedSubset = monoid0 +
fixes H
assumes closed: "H {is closed under} f"
and sub: "H⊆G"
and neutral: "TheNeutralElement(G,f) ∈ H"
sublocale monoidClosedSubset < submonoid: monoid0 H "restrict(f,H×H)"
unfolding monoid0_def using group0_1_T1
sub neutral closed by auto
abbreviation (in monoidClosedSubset) subOper (infixl "⊕⇩H" 70)
where "a ⊕⇩H b ≡ submonoid.monoper(a,b)"
text‹Under the assumptions of ‹ group0_1_T1›
the neutral element of a
submonoid is the same as that of the monoid.›
lemma (in monoidClosedSubset) group0_1_L6:
shows "TheNeutralElement(H,restrict(f,H×H)) = TheNeutralElement(G,f)"
proof -
let ?e = "TheNeutralElement(G,f)"
let ?g = "restrict(f,H×H)"
have
"?e ∈ H ∧ (∀h∈H. ?e⊕⇩Hh = h ∧ h⊕⇩H?e = h)"
proof -
{
fix h assume "h ∈ H"
with closed sub neutral have "∀x∈H.∀y∈H. x⊕y ∈ H" "H⊆G" "?e ∈ H" "h ∈ H"
unfolding IsOpClosed_def by auto
then have "?e⊕⇩Hh = h ∧ h⊕⇩H?e = h"
using group0_1_L5
by simp
} hence "∀h∈H. ?e⊕⇩Hh = h ∧ h⊕⇩H?e = h" by simp
with neutral show ?thesis by simp
qed
then have "?e = TheNeutralElement(H,?g)"
using submonoid.group0_1_L4 by auto
thus ?thesis by simp
qed
text‹If a sum of two elements is not zero,
then at least one has to be nonzero.›
lemma (in monoid0) sum_nonzero_elmnt_nonzero:
assumes "a ⊕ b ≠ TheNeutralElement(G,f)"
shows "a ≠ TheNeutralElement(G,f) ∨ b ≠ TheNeutralElement(G,f)"
using assms unit_is_neutral by auto
text‹The monoid operation is associative.›
lemma (in monoid0) sum_associative:
assumes "a∈G" "b∈G" "c∈G"
shows "(a⊕b)⊕c = a⊕(b⊕c)"
using assms monoidAssum unfolding IsAmonoid_def IsAssociative_def
by auto
end
from isarmathlib.
So to summarize the issue as I understand it:
So far I have been defining notation in locale with defines
statements. Now suppose that I want in some locale, say reals
reference theorems proven in some other locale. Then I have two possibilities.
A. Sublocale, for example sublocale reals < group0 (...)
. This has the advantage that it remaps the notation and the usage is seamless, the propositions proven in group0
are automatically available in reals0
. The disadvantage is that all notation in group0
has to map to something in reals
.
B. A lemma that proves the predicate defining the other locale, like the lemma pmetric_space_valid
. This has the advantage that only the assumes
of the other locale have to be proven, but has the disadvantage that the notation is not mapped and the usage is clunky - a lemma like pmetric_space_valid
has to be referenced together with each referenced proposition from pmetric_space_valid
.
So it is usually better to use the A. (i.e. a sublocale), unless the other locale has notation that we don't want in the reals
locale. For example I did not want to prove the sublocale reals < pmetric_space (...)
because pmetric_space
inherits from loop1
which defines notation for left and right division that does not map sensibly in real numbers.
If we decide to move the notation outside of locales we do not have to map the notation with each sublocale
command, but we also loose the advantage of the sublocale
command being able to map notation. I don't see either of these two approaches (notation inside or outside of locale definition) as clearly better than the other, each has it's tradeoffs. So I propose we do not modify the existing stuff (as it would trigger work to modify dependent proofs) and for new development do whichever seems better in the specific case.
The theory file you included shows how one can define the notation outside of the locale so that the existing proofs in the locale are not affected. I think that
abbreviation (in monoid0) monoper (infixl "⊕" 70)
where "a ⊕ b ≡ f`⟨a,b⟩"
looks better than
definition (in monoid0) monoper (infixl "⊕" 70)
where "a ⊕ b ≡ f`⟨a,b⟩"
lemmas (in monoid0) [simp] = monoper_def
and seems to achieve the same thing.
In my request for a theory file illustrating the problem I was more interested in seeing the situation when defining notation in a locale (without additional assumptions) causes problems when you later reference propositions proven in that locale from some other locale. I have not encountered such situation so far.
from isarmathlib.
I agree with your last point that abbreviation looks better than a definition; but definitions carry over (in an ugly way t monoid.monoper(x,y)
) and abbreviations do not. What was thinking of is definitions for new things and abbreviations for inherited definitions; just to carry them over. You have been making a distinction between a definition, what you define outside any locale context (Closure), and notations, what you define inside locales (cl). I think definitions like Closure, Interior, etc should be definitions inside the locale context, but outside the locale definition; and notations like \<oplus>
I would just leave as abbreviations.
from isarmathlib.
There are no problems referencing results from a parent locale. The problem is proving something is a sublocale. I gave you the example of a subgroup. Since restrict(P,HxH)
does not reduce to P
applied to arbitrary elements; I cannot invoke group0 results on H with groper
; I have to define a groperH
. This is shown in the monoid case I gave too.
from isarmathlib.
So I understand the problem may be illustrated by the following example:
locale monoid0 =
fixes G f
assumes monoidAssum: "IsAmonoid(G,f)"
fixes monoper (infixl "\<oplus>" 70)
defines monoper_def [simp]: "a \<oplus> b \<equiv> f`\<langle>a,b\<rangle>"
locale monoidClosedSubset = monoid0 +
fixes H
assumes closed: "H {is closed under} f"
and sub: "H⊆G"
and neutral: "TheNeutralElement(G,f) ∈ H"
sublocale monoidClosedSubset < submonoid: monoid0 H "restrict(f,H×H)"
proof - (* no way to prove this *)
that is, in monoidClosedSubset
locale you inherit the meaning of ⊕
notation from monoid0
to be
f`\<langle>a,b\<rangle>
but then you can't map that to mean
restrict(P,HxH) `\<langle>a,b\<rangle>
in the sublocale
?
So the new recommended way of handling notation that you propose is to:
A. Define notation using definition
outside of locale specification, adding the definitions to the simplifier with lemmas
command.
B. When you need to use theorems from another locale prove the sublocale
statement (which now only needs to show the assumes
) and then map the notation using abbreviation
as needed.
I like this, but I would like to see a couple of examples of this style, maybe you can do this when possible in the new development about rings. Don't worry about the style check for new theory files, we will deal with it later.
making a distinction between a definition, what you define outside any locale context (Closure), and notations, what you define inside locales (cl)
yes, I like to have such distinction between notion definitions and notation. The approach with all definitions in a locale (but outside of the locale definition) loses that. It is not a showstopper, just an aesthetic concern.
definitions carry over (in an ugly way t monoid.monoper(x,y)) and abbreviations do not
How about the notation
command, do you know? If it carries over like definition
it would be a good way to distinguish notions (defined with definition
) and notation (defined by notation
).
from isarmathlib.
I have not been looking at this, as I have been sick lately. Sorry.
After thinking on it, to carry things over the way you intend to leave it as is.
from isarmathlib.
Related Issues (20)
- TopologicalGroup_Uniformity_ZF.thy not presented at isarmathlib.org HOT 1
- isar2html does not support references to theorems with statement number
- Rewrite topological group proofs HOT 9
- A topological space is uniformizable iff it is completely regular.
- IsarMathLib version 1.15.0: comparison with Mizar HOT 4
- Cardinal_ZF in ROOT ? HOT 1
- Adding issues and milestones HOT 2
- Tarski-Grothendieck Axioms HOT 1
- Definition natural number "1,2,3,4,5,6,7,8,9,10" HOT 4
- Ring ideals HOT 1
- Add interpretation to the parser HOT 5
- More theories presented at isarmathlib.org HOT 1
- Vector spaces and modules HOT 4
- Topological group uniformities. Roelcke uniformity. HOT 2
- Isabelle2020 released, IsarMathLib still at Isabelle2019
- Possibility of CI with github actions HOT 2
- TopologicalGroup_ZF.thy HTML rendering broken for v1.12.0 HOT 2
- Uniformly continuous mappings
- isar2html does not support definitions in a locale HOT 8
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from isarmathlib.