Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proving theorems bridging between two theories...

Email Gateway (Aug 18 2022 at 14:18):

From: S W <s.wong.731@googlemail.com>
Hi,

I was wondering whether Isabelle can prove theorems bridging between two
theories. For example, if I have A.thy and B.thy, can I prove that there is
a constant c in A that equals to v, while c in B doesn't equal to v? A and B
can't be merged into one because together they'd be inconsistent.

Could locales be used here? It seems to me that: "locale C = A + B" would
merge A and B together to form C. Perhaps another operator could be used to
indicate that two locales are involved in the proof, but are not imported.
Is there a better way for proving bridging theorems? If not, would it make
sense for me to implement such an operator in ML? How much effort do you
think the implementation will require?

Thanks
Steve

Email Gateway (Aug 18 2022 at 14:20):

From: Steve W <s.wong.731@googlemail.com>
Hi,

I'm reposting a question from earlier:

I was wondering whether Isabelle can prove theorems bridging between two
theories or locales. For example, if I have A.thy and B.thy, can I prove
that there is a constant c in A that equals to v, while c in B that doesn't
equal to v? A and B can't be merged into one because together they'd be
inconsistent.

Could locales be used here? It seems to me that: "locale C = A + B" would
merge A and B together to form C. Perhaps another operator could be used to
indicate that two locales are involved in the proof, but are not imported.
Is there a better way for proving bridging theorems? If not, would it
necessary for me to implement such an operator in ML? How much effort should
the implementation require?

Thanks
Steve

Last updated: Apr 25 2024 at 08:20 UTC