[isabelle] Proving relationships between locale predicates.
- To: isabelle-users at cl.cam.ac.uk
- Subject: [isabelle] Proving relationships between locale predicates.
- From: Lars Noschinski <noschinl at in.tum.de>
- Date: Tue, 29 Nov 2011 14:52:52 +0100
- User-agent: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:188.8.131.52) Gecko/20111010 Icedove/3.1.15
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).
This archive was generated by a fusion of
Pipermail (Mailman edition) and