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 *)

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

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
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

On Tue, Sep 27, 2011 at 8:33 PM, Clemens Ballarin<ballarin at in.tum.de>  wrote:
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?

Thanks in advance.

John












--
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.edu
http://pp.info.uni-karlsruhe.de
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.