How to pass assumptions to interpretation of locale

Question

I would like to use some properties of my structure in the proof required by a locale interpretation

As an example, suppose I defined the predicate P and proved some lemmas (add is a closed binary operation, add is associative and there exists zero the neutral element) about the add operation on elements that satisfy the predicate P

I would like to interpret then the set of my elements as a structure that satisfy some locale, e.g. monoid

interpretation "{s . P s}" :: monoid "(add)" "(zero)"
unfolding
  monoid_def
using
  add_is_associative
  zero_is_neutral

but then in the goal of my proof I am not able to get that all the elements are actually satisfying the predicate P and I am left with a generic goal such as add zero a = a which I already proved for elements in my set.

How to enforce in my goal that all the elements satisfy the predicate P?

Answer 1

I will make an attempt to provide comments on your question. Please feel free to ask further questions in the comments if you will find that my comments are not sufficient to answer your question.

---

Firstly, I would like to mention that there exists a good tutorial on locales and locale interpretation in the standard documentation of Isabelle. The name of the document is "Tutorial to Locales and Locale Interpretation" (by Clemens Ballarin). The document also contains several useful references.

After studying the tutorial and the references, it may also be useful to look at section 5.7 in the document "The Isabelle/Isar Reference Manual".

---

I would like to use some properties of my structure in the proof required by a locale interpretation

The description of the locale interpretation in the reference manual states that

Locales may be instantiated, and the resulting instantiated declarations added to the current context. This requires proof (of the instantiated specification) and is called locale interpretation.

When you invoke the command interpretation with a set of appropriately stated arguments, the goals that are discharged by the command depend solely on the arguments. The proof that you provide to prove the discharged goals will have no impact on the 'resulting instantiated declarations'. Thus, technically, it does not matter whether or not you use the properties of your functions that you mentioned explicitly to prove the interpretation.

---

I would like to interpret then the set of my elements as a structure that satisfy some locale, e.g. monoid: interpretation "{s . P s}" :: monoid "(add)" "(zero)"

If you look at the specification of the command interpretation in the reference manual (section 5.7.3), you will realise that as its input argument the command takes a 'locale expression'. The 'locale expression' is described in section 5.7.1 in the reference manual. Here, I present a significantly simplified (incomplete) description of the locale expression:

qualifier : name pos_insts

The field 'qualifier' is optional and the field 'name' is reserved for the name of the locale that you are trying to interpret. Therefore, the expression "{s . P s}" :: monoid "(add)" "(zero)" that you provided in your question is not a valid locale expression. I can only guess that you meant to use a single colon instead of the double colon ::, i.e. "{s . P s}" : monoid "(add)" "(zero)" and I will proceed with the answer based on this assumption.

In the example that you provided, the 'qualifier' is "{s . P s}", the 'name' is monoid and the 'pos_insts' are, effectively, the terms specified after the name.

Returning to the documentation you will also find the description of the field 'qualifier':

Instances have an optional qualifier which applies to names in declarations

...

Qualifiers only affect name spaces; they play no role in determining whether one locale instance subsumes another.

Thus, the qualifier "{s . P s}" that you specified can only have an effect on the names of the declarations. It will have no effect on the goals discharged by the command and its output.

---

interpretation "{s . P s}" : monoid "(add)" "(zero)"

Returning to your example, if you are referring to the locale monoid from the theory HOL-Groups, then, if you study its specification and also the specification of the locale semigroup, you will be able to infer that the locale monoid has two parameters that are associated with it: f and z. There are no other parameters and the 'carrier set' of the monoid associated with the locale consists of all terms of a given type.

locale monoid = semigroup +
  fixes z :: 'a ("❙1")
  assumes left_neutral [simp]: "❙1 ❙* a = a"
  assumes right_neutral [simp]: "a ❙* ❙1 = a"

In conclusion, the locale monoid from the theory HOL-Groups is not suitable for representation of a monoid on an explicit carrier set that is a proper subset of the terms of a given type.

For your application, you will need to use a locale that represents a monoid on an explicit carrier set, for example, the locale monoid from the theory HOL-Algebra.Group. You can see examples of its interpretation in the theory HOL-Algebra.IntRing.

---

UPDATE

Following the request of the author of the question given in the comments, I provide an example of an interpretation of the locale monoid from the theory HOL-Algebra.Group:

theory SO_Question
  imports "HOL-Algebra.Group"

begin

abbreviation even_monoid :: "int monoid" ("𝒵⇩2") where 
  "even_monoid ≡ ⦇carrier = {x. x mod 2 = 0}, mult = (+), one = 0::int⦈"

interpretation even_monoid: monoid 𝒵⇩2
  by unfold_locales auto+

end