Re: [isabelle] Proving relationships between locale predicates.
AFAIK sublocale doesn't store the proven theorem. So the best is to
lemma (in A) B_f: "B (f x)"
sublocale A <= B (f x)
by (rule B_f)
and now you can use it also with:
note B_f = A.B_f[OF `A x`]
note B.lemma[OF B]
which is ugly, but fast.
Am Dienstag, den 29.11.2011, 14:52 +0100 schrieb Lars Noschinski:
> I've got two locales A (with predicate "A x") and B and
> sublocale A <= B (f x)
> holds. Now, if I have "A x", how can I show "B (f x)" without repeating
> the proof for the sublocale property?
> I only need one lemma from B, so I would really like to avoid
> instantiating A, as this takes very long (around 2.5s per instantiation).
> -- Lars
This archive was generated by a fusion of
Pipermail (Mailman edition) and