Re: [isabelle] Quantifying over locales

Dear John,

all of your statements essentially involve only the parameters of *one* locale, so it is hard to say which is the right one. Also, your original question involved only one locale T, now there seems to be another called S. I am confused.

Here's an example how I would do it. Maybe this helps.

locale T = fixes f c assumes "f c > 0"

lemma "T f1 c1 & T f2 c2 ==> f1 c1 > 0 & f2 c2 > 0 & ..."

(* or in Isar syntax *)

  assumes "T f1 c1" and "T f2 c2"
  shows "f1 c1 > 0" and "f2 c2 > 0" and "..."

If you have two different locales S and T, it essentially looks the same:

locale T = fixes f c assumes ...
locale S = fixes a b assumes ...

lemma "T f c & S a b ==> P f c a b"

where P is the property that you wish to prove about the parameters of both locales.

If you want to use the convenient locale mechanism, you can also combine locales as follows:

locale T_and_S = T + S begin
lemma "P f c a b"


Am 19.10.2011 17:29, schrieb John Munroe:
Digging up a slightly old post: So if I want to have a lemma that
speaks about 2 locales, T f c and S a b, which of the following is

lemma "(T f c -->  f c>  0)&  (S a b -->  a b>  0)"


lemma "T f c&  S a b -->  f c>  0&  a b>  0"



On Tue, Sep 27, 2011 at 8:33 PM, Clemens Ballarin<ballarin at>  wrote:
Hi Steve,

I think this is correct.  You'll need some knowledge about nat in the proof,
of course.


Quoting Steve Wong<s.wong.731 at>:

Just to confirm my understanding:

EX f c. T f c&  f c>  0 can be proved with the fact T_def.

ALL f c. T f c -->  f c>  0 can also be proved with the fact
Alternatively T f c -->  f c>  0 can be proved the same way because free
variables are implicitly quantified.

Am I right here?


On Thu, Sep 22, 2011 at 7:42 PM, Clemens Ballarin
<ballarin at>wrote:

A locale is a predicate and its existence is trivial.  What you probably
wanted to show is that there is an instance of T for which f c>  0:

  EX f c. T f c&  f c>  0

If you get the locale predicate (T in your case) involved, types are


Quoting John Munroe<munddr at>:


I'm trying to see how one could quantify over locales. For example, if I

locale T =
  fixes f :: "nat =>  nat"
  and c :: nat
  assumes ax: "f c = 1"

and if I want to prove that there exists a locale taking 2 parameters
such that applying the first parameter to the second is equal to 0
(essentially T):

lemma "EX P. P (f::real=>real) (c::real) -->  f c>  0"

but that would be a trivial lemma since P f c can simply be False. So
how should one properly formulate the lemma? Is there a way of doing
so without specifying on the type that each parameter should take?

Thanks in advance.


Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.