Re: [isabelle] relating 2 theories



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.