[isabelle] Quantifying over locales



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.