# Re: [isabelle] Quantifying over locales

```Hi Steve,

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

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

```
```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 T.ax.
Alternatively T f c --> f c > 0 can be proved the same way because free
variables are implicitly quantified.

Am I right here?

Steve

On Thu, Sep 22, 2011 at 7:42 PM, Clemens Ballarin <ballarin at in.tum.de>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
inferred.

Clemens

Quoting John Munroe <munddr at gmail.com>:

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

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?

John

```
```

```
```
```
```

```

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