[isabelle] Proving theorems bridging between two theories/locales


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?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.