Re: [isabelle] Proving theorems bridging between two theories/locales



On Tue, Nov 24, 2009 at 7:25 AM, Steve W <s.wong.731 at googlemail.com> wrote:
> Hi,
>
> I'm reposting a question from earlier:
>
> I was wondering whether Isabelle can prove theorems bridging between two
> theories or locales. For example, if I have A.thy and B.thy, can I prove
> that there is a constant c in A that equals to v, while c in B that doesn't
> equal to v? A and B can't be merged into one because together they'd be
> inconsistent.

Hi Steve,

Certainly, if A.thy and B.thy each declare axioms, a merged theory
might be inconsistent. But if each theory defines a constant called
"c", then that doesn't prevent you from merging theories: The real
constant names are qualified names like "A.c" and "B.c", so in a
merged theory you might be able to prove something like "A.c ~= B.c".

> Could locales be used here? It seems to me that: "locale C = A + B" would
> merge A and B together to form C.

That is exactly right. For example, if you want to show that the
assumptions from locales A and B are inconsistent with each other, you
can do something like this:

locale C = A + B
begin

lemma A_B_inconsistent: "False"
<proof using assumptions from locales A and B>

end

> Perhaps another operator could be used to
> indicate that two locales are involved in the proof, but are not imported.

If you don't want to define a new locale, you can combine locales
within a single proof using the "interpret" command. This involves
adding the locale predicates as assumptions of your lemma. Here is an
example:

locale A = fixes foo assumes ...
locale B = fixes bar assumes ...

lemma A_B_inconsistent:
  assumes "A foo" and "B bar"
  shows "False"
proof -
  interpret A foo
    by fact
  interpret B bar
    by fact
  show "False"
    <proof using assumptions from locales A and B>
qed

> Is there a better way for proving bridging theorems? If not, would it
> necessary for me to implement such an operator in ML? How much effort should
> the implementation require?
>
> Thanks
> Steve

Hopefully one of the above methods will work for you. I don't think it
should be necessary to implement anything at the ML level.

- Brian





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