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.