*To*: Alexander Krauss <krauss at in.tum.de>*Subject*: Re: [isabelle] Proving formulae from separate sets of axioms*From*: s.wong.731 at googlemail.com*Date*: Thu, 03 Sep 2009 10:29:22 +0000*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4A9F80CE.9010206@in.tum.de>

On Sep 3, 2009 9:39am, Alexander Krauss <krauss at 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 andT2.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 inT2

and r1 != r2? T1 and T2 are each internally consistent, but together maybe

inconsistent.

This is not possible. In some cases it is possible to localize axioms byjust making them assumptions of some lemmas. The locale mechanism (seelocale tutorial) gives some tool support for doing this.

Thanks Steve

Alex

**Follow-Ups**:**Re: [isabelle] Proving formulae from separate sets of axioms***From:*Alexander Krauss

**References**:**Re: [isabelle] Proving formulae from separate sets of axioms***From:*Alexander Krauss

- Previous by Date: Re: [isabelle] Quick question about rule+
- Next by Date: Re: [isabelle] Proving formulae from separate sets of axioms
- Previous by Thread: Re: [isabelle] Proving formulae from separate sets of axioms
- Next by Thread: Re: [isabelle] Proving formulae from separate sets of axioms
- Cl-isabelle-users September 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list