Re: [isabelle] Quantifying over locales

Dear John,

Am 19.10.2011 17:47, schrieb John Munroe:
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.

lemma "(T f c -->  f c>  0)&  (S f' c' -->  f' c' = 0)"
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.


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