Re: [isabelle] Proving formulae from separate sets of axioms
On Sep 3, 2009 9:39am, Alexander Krauss <krauss at in.tum.de> wrote:
Can a formula describing the property a function should hold across
*several* theories? For example, I might have 2 theories T1.thy and
each with its own set of axioms. Can I prove something like there exists a
function F, variables x and y, such that F xy returns r1 in T1 and r2 in
and r1 != r2? T1 and T2 are each internally consistent, but together may
This is not possible. In some cases it is possible to localize axioms by
just making them assumptions of some lemmas. The locale mechanism (see
locale tutorial) gives some tool support for doing this.
If I localise axioms, then would I be able to check whether r1 != r2?
Checking r1 != r2 seems to need to look at *both* sets of axioms. Also, can
I check whether F is instantiated to the same thing on each side?
This archive was generated by a fusion of
Pipermail (Mailman edition) and