Problems because of notation

[dan323]

@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. 😄

[SKolodynski]

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?

[dan323]

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.

[dan323]

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.

[dan323]

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

[SKolodynski]

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.

[dan323]

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.

[dan323]

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.

[SKolodynski]

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).

[dan323]

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.