How do I prove that an object does not interpret a locale?

I want to define "big" natural numbers as those larger than 10, and "small" ones as those less than 5. I can express these definition as locales:

locale Big = 
  fixes k :: ‹nat›
  assumes ‹k > 10›

locale Small =
  fixes k :: ‹nat›
  assumes ‹k < 5›

I can then prove that 11 is a Big number and 2 is a Small one:

interpretation Big ‹11 :: nat› by (unfold_locales, simp)
interpretation Small ‹2 :: nat› by (unfold_locales, simp)

But how would I express and prove that 7 is not Small? I can prove that it is not less than 5, but the proof is unsatisfactory since it does not refer to the locale Small at all:

lemma ‹¬ ((7 :: nat) < (5 :: nat))› by simp

Moreover, how would I express that no integer exists which is both Big and Small? Again, I can prove it, but only without reference to the locales:

lemma
  fixes k :: nat
  shows ‹¬ (k < 5 ∧ k > 10)›
  by simp

In general, how do I prove that something is not an interpretation of one or more locales? Or am I misusing the locale mechanism?

Solution

The command locale is documented in Isar-ref and the document "Tutorial to Locales and Locale Interpretation". Also, there has been a number of relevant publications that describe the implementation/syntax in more detail and in a more formal manner. One document that comes to my mind is Locales and Locale Expressions in Isabelle/Isar by Clemens Ballarin. It is outdated, but (in my view) it provides more elaborate explanation of the fundamental concepts than Isar-ref and the tutorial. In particular, see section 3.3: "Locale Predicates and the Internal Representation of Locales" in the aforementioned document.

But how would I express and prove that 7 is not Small? I can prove that it is not less than 5, but the proof is unsatisfactory since it does not refer to the locale Small at all:

Using the locale predicates, you may state the theorem in your question as follows:

lemma "¬Small 7" unfolding Small_def by auto

Whether or not using a locale predicate explicitly is sensible and whether there exist better options for expressing a given idea depends on the context.

Moreover, how would I express that no integer exists which is both Big and Small?

lemma "¬(Small x ∧ Big x)" unfolding Small_def Big_def by simp

The main conclusion from the above is that locale predicates (e.g. Small) are merely constants and the command locale provides several theorems about these constants, including their definition (e.g. Small_def). The referenced documents provide further details.

In general, how do I prove that something is not an interpretation of one or more locales? Or am I misusing the locale mechanism?

Unfortunately, in my view, these questions require clarification. Overall, the decision whether a locale, a class or a plain definition should be used to define a given concept depends on the application and, to a degree, on personal preferences.