*To*: Joao Marcos <jmarcos at dimap.ufrn.br>*Subject*: Re: [isabelle] relating 2 theories*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sun, 14 Sep 2008 15:19:30 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <a2727b60809130949l77e9351em59fffb15e7050991@mail.gmail.com>*References*: <a2727b60809130949l77e9351em59fffb15e7050991@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.16 (Macintosh/20080707)

I'm afraid that Isabelle does not interpret these activities directly on the level of theories. If you want to show implicational relations between axiomatizations, Isabelle's locales are probably a good framework. If you need to take the inductive definition of derivability into account, you need to set up your own inductive definition of the different logics involved. Tobias Joao Marcos schrieb: > Dear All: > > Suppose you have two Isabelle theories, T1.thy and T2.thy, and you > want to check which axioms of T2 are provable in T1, and, conversely, > which axioms of T1 are provable in T2. > > To make things simpler, let's suppose both theories are written in the > same signature (containing thus constructors identified by the same > strings, but possibly characterized by different sets of rules), and > are based on the same formalism (say, both are formulated as sequent > calculi, or in natural deduction). The case where the theories have > different constructors is also interesting, however, if T1 and T2 are > intended for instance to be two different axiomatizations of the same > theory (T1 could be, say, a formulation of classical logic over > negation, conjunction and disjunction, while T2 could be classical > logic over implication and co-implication). > > One way of accomplishing this task, of course, is typing the axioms of > T2 by hand as goals inside T1 and proving them, and vice-versa > (appropriate rewrite rules could be added somewhere to take care of > the case with different constructors). Another obvious way is to > write a new theory T0 containing the axioms and definitions of both T1 > and T2 and doing proofs there with some care not to mix axioms with > "different origins". > > My question is: Is there a more "natural" way of doing this in Isabelle? > (What I have in mind is some way of referring to the axioms of T2 > directly from inside T1, or referring to the axioms of both theories, > in turn, from "outside" them.) > > The next step will be then to prove things by induction using theory > T1 as the "meta-theory" of T2, that is, proving properties of T2 by > induction using the properties and axioms of T1 as facts. > How can that be smoothly done inside Isabelle without "dirty tricks"? > (Do consider that the axioms of both theories might have similar > names, and some of them might even coincide, independently of their > particular names.) > > I thank you in advance for your practical advice on this issue, > Joao Marcos

**References**:**[isabelle] relating 2 theories***From:*Joao Marcos

- Previous by Date: Re: [isabelle] I can't understand types in set-membership expressions
- Next by Date: Re: [isabelle] I can't understand types in set-membership expressions
- Previous by Thread: [isabelle] relating 2 theories
- Next by Thread: Re: [isabelle] relating 2 theories
- Cl-isabelle-users September 2008 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