Re: [isabelle] relating 2 theories

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.

It is possible to define two type classes (defining them unrelated to each other, and in two theories which are independent of each other).

Then, in a supertheory which sees both type class definitions, it is possible to express and prove that one type class is a subclass of the other (by the <-form of the instance command). Unfortunately it is not possible to express (except, I guess, in two independent theories) that type class a < type class b, and vice versa - understandably, Isabelle doesn't like cyclic subclass relationships.


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