# Re: [isabelle] Proving relationships between locale predicates.

Hi Lars,
AFAIK sublocale doesn't store the proven theorem. So the best is to
prove:
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.
- Johannes
Am Dienstag, den 29.11.2011, 14:52 +0100 schrieb Lars Noschinski:
> Hi,
>
> 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
MHonArc.*