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.

Andreas

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