Re: [isabelle] Proving relationships between locale predicates.

Hi Lars,

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.

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