Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proofing across several theories

view this post on Zulip Email Gateway (Aug 18 2022 at 13:16):

From: Stephy Wong <s.wong.731@googlemail.com>
Hi,

I was wondering whether one could proof a goal across several separate
theories. For example, given two theories a.thy and b.thy, can a goal like
\exists t:T, q:Q.t -> q in a.thy and \exists t:T, p:P. t -> p, where T and P
are types, be proven. Here, I want T to be the same in both theories. Can
this information be passed from one theory to another? If so, since a.thy
and b.thy are separate, can they be inconsistent with each other?

Thanks

S

view this post on Zulip Email Gateway (Aug 18 2022 at 13:17):

From: Tobias Nipkow <nipkow@in.tum.de>
Stephy Wong wrote:
The only way one theory can refer to another is by importing it
(directly or indiectly), or by having a third theory that imports both.
You can qualify types etc from theory A by writing A.T.

Regards
Tobias

Last updated: May 03 2024 at 12:27 UTC