Re: [isabelle] Quantifying over locales
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
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 in.tum.de> wrote:
I think this is correct. You'll need some knowledge about nat in the proof,
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?
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
Quoting John Munroe<munddr at gmail.com>:
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
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
Adenauerring 20a, Geb. 50.41, Raum 031
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
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