Email Gateway (Aug 18 2022 at 12:22): Email Gateway (Aug 18 2022 at 12:22):From: Joao Marcos <jmarcos@dimap.ufrn.br>
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
Email Gateway (Aug 18 2022 at 12:23):From: Tobias Nipkow <nipkow@in.tum.de>
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:
Email Gateway (Aug 18 2022 at 12:23):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Joao Marcos wrote:
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.
Jeremy
Email Gateway (Aug 18 2022 at 12:23):From: Clemens Ballarin <ballarin@in.tum.de>
In contrast, locales permit cyclic relationships. That is, if two
locales have equivalent specifications and the parameters are the
same (up to renaming) you can declare them to interpret each other.
Clemens
Last updated: May 03 2024 at 08:18 UTC