Email Gateway (Aug 18 2022 at 18:24): 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
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>:
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
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
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>:
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
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
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
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: Nov 21 2024 at 12:39 UTC