Email Gateway (Aug 18 2022 at 13:59): Email Gateway (Aug 18 2022 at 13:59):From: Steve W <s.wong.731@googlemail.com>
Hi,
Can a formula describing the property a function should hold across
several theories? For example, I might have 2 theories T1.thy and T2.thy,
each with its own set of axioms. Can I prove something like there exists a
function F, variables x and y, such that F x y returns r1 in T1 and r2 in T2
and r1 != r2? T1 and T2 are each internally consistent, but together may be
inconsistent.
Thanks
Steve
Email Gateway (Aug 18 2022 at 13:59):From: Alexander Krauss <krauss@in.tum.de>
Steve,
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.
Alex
Email Gateway (Aug 18 2022 at 14:00):From: Alexander Krauss <krauss@in.tum.de>
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.
I meant that you could prove something like
"(Ax1 ==> f x = r1) ==> (Ax2 ==> f x = r2) ==> r1 = r2"
Also, can I check whether F is instantiated to the same thing on each
side?
Not sure what you mean here with instantiated. If you have different
descriptions of a function f, say "Ax1 f" and "Ax2 f", then the question
can probably be expressed using the formula
"Ax1 f ==> Ax2 f' ==> f = f'"
Maybe you want to prove a statement like this.
Alex
Email Gateway (Aug 18 2022 at 14:00):From: s.wong.731@googlemail.com
On Sep 3, 2009 9:39am, Alexander Krauss <krauss@in.tum.de> wrote:
Steve,
Can a formula describing the property a function should hold across
several theories? For example, I might have 2 theories T1.thy and
T2.thy,
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
T2
and r1 != r2? T1 and T2 are each internally consistent, but together may
be
inconsistent.
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?
Thanks
Steve
Alex
Last updated: Nov 21 2024 at 12:39 UTC