*To*: Joao Marcos <jmarcos at dimap.ufrn.br>*Subject*: Re: [isabelle] relating 2 theories*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Mon, 15 Sep 2008 09:22:57 +1000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <a2727b60809130949l77e9351em59fffb15e7050991@mail.gmail.com>*References*: <a2727b60809130949l77e9351em59fffb15e7050991@mail.gmail.com>*User-agent*: Thunderbird 1.5.0.12 (X11/20070604)

Joao Marcos wrote:

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

A somewhat similar question relates to axiomatic type classes.

Jeremy

**Follow-Ups**:**Re: [isabelle] relating 2 theories***From:*Clemens Ballarin

**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: Re: [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