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

On Sun, Nov 29, 2009 at 7:58 AM, <s.wong.731 at googlemail.com> wrote:
> locale A =
> fixes foo
> assumes eq: "foo = 0"
>
> locale B =
> fixes bar
> assumes neq: "bar ~= 0"
>
> lemma A_B_inconsistent:
> assumes "A foo"
> and "B foo"
> shows "False"
> proof -
> interpret A foo
> by fact
> interpret B foo
> by fact
> show "False"
> using A.eq B.neq
> by simp
>
> I think the simplifier can't find rules to finish off the proof. Could you
> please shed some light on this?
What's happening here is that A.eq and B.neq do not refer to the
theorems that you want.
After the "using" command, the goal window shows the content of those theorems:
using this:
A ?foo ==> ?foo = (0::?'a)
B ?bar ==> ?bar ~= (0::?'a)
So the names "A.eq" and "B.neq" refer to the generic theorems
parameterized by the locale predicates "A" and "B".
If you say "using eq neq" or "using local.eq local.neq" instead, you
will get what you want:
using this:
foo = (0::'a)
foo ~= (0::'a)
Alternatively, you can specify a name for each interpretation; then
you can refer to the instantiated theorems unambiguously using the
qualified names. (This is especially helpful when the locales involved
have some overlapping theorem names!)
lemma A_B_inconsistent:
assumes "A foo"
and "B foo"
shows "False"
proof -
interpret localA: A foo
by fact
interpret localB: B foo
by fact
show "False"
using localA.eq localB.neq
by simp
Hope this helps,
- Brian

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