Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Quantifying over locales


view this post on Zulip Email Gateway (Aug 18 2022 at 18:24):

From: John Munroe <munddr@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?

Thanks in advance.

John

view this post on Zulip Email Gateway (Aug 18 2022 at 18:24):

From: Clemens Ballarin <ballarin@in.tum.de>
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@gmail.com>:

view this post on Zulip Email Gateway (Aug 18 2022 at 18:25):

From: John Munroe <munddr@gmail.com>
But what if I want to show that there is a binary predicate/locale in the
theory such that applying the first param to the second is greater than 0
instead? Basically T f c will be the witness. How should the lemma be
formulated?

Thank you.

John

On Thursday, September 22, 2011, Clemens Ballarin <ballarin@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@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?

Thanks in advance.

John

view this post on Zulip Email Gateway (Aug 18 2022 at 18:27):

From: Steve Wong <s.wong.731@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

view this post on Zulip Email Gateway (Aug 18 2022 at 18:28):

From: Clemens Ballarin <ballarin@in.tum.de>
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@gmail.com>:

view this post on Zulip Email Gateway (Aug 18 2022 at 18:32):

From: John Munroe <munddr@gmail.com>
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
correct?

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

or

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

Thanks

John

view this post on Zulip Email Gateway (Aug 18 2022 at 18:33):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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 *)

lemma
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"
<proof>
end

Andreas

view this post on Zulip Email Gateway (Aug 18 2022 at 18:33):

From: John Munroe <munddr@gmail.com>
Thanks. Sorry, I should have made my question clearer (with a better
example): Suppose I have two different locales

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

I want to prove that f c > 0 is indeed provable in T and f c = 0 is
indeed provable in S in a single lemma. Based on your response, I
believe the appropriate formulation would be:

lemma "T f c & S f' c' --> f c > 0 & f' c' = 0"

Am I correct?

But how about

lemma "(T f c --> f c > 0) & (S f' c' --> f' c' = 0)"

Does it not fulfil my purpose as well?

Thanks

John

view this post on Zulip Email Gateway (Aug 18 2022 at 18:33):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Dear John,

In that case, this is what you want, but note that this is just the conjunction
of two separate lemmas. So I still don't see what you need this for. But that's
a different matter.

The above lemma is in general stronger than

lemma "T f c & S f' c' --> f c > 0 & f' c' = 0"

because the latter essentially expresses for each part of the conjunction in the
conclusion that the assumptions of the other locale are satisfiable.

Andreas


Last updated: Mar 28 2024 at 20:16 UTC